UPPAAL: что заставило часы перестать работать

Question

В настоящее время я использую симулятор UPPAAL. Мой симулятор перестает запускать код после определенного момента. Этот момент варьируется в зависимости от декларации, которую я предоставляю. Но я хотел бы знать, вообще, когда часы перестают работать? Есть ли что-то, что вызывает это?

Answer 1

Я не уверен, правильно ли я интерпретирую ваш вопрос, если бы я мог прочитать вашу модель, я мог бы дать вам точный совет.

Пытаясь угадать, в чем проблема, я могу сказать, что бывают случаи, когда симулятор Уппаала делает бесконечно много дискретных шагов (переходов), не увеличивая ни одну из переменных часов.

Ощущение такое, что "часы остановлены", пока идет остальная часть симуляции. В этом случае время фактически не останавливается: Uppaal, среди всех возможных путей, он просто исследует тот, где часы не развиваются. Если симулятор (или средство проверки модели) может выполнять бесконечно много переходов без увеличения переменных часов, это пример "пути Zeno".

Человек, который пишет модель, несет ответственность за то, чтобы избежать возможности выбора путей дзено.

Если вы не уверены, что ваша модель не содержит путей Zeno, вы можете использовать известные методы для проверки того, что у Timed Automaton нет путей Zeno (в Уппале).

Другая возможность состоит в том, что симулятор вообще перестает работать, говоря, что существует тупик. В этом случае проблема не в том, что часы перестали работать, а в том, что вы попали в ситуацию, когда все возможные переходы отключены (возможно, потому что все возможные средства защиты никогда не включены, или потому что все возможные целевые состояния ваших включенных переходов имеют некоторое время инварианты, которые являются ложными)