Простая базовая проблема проверки в uppal

Я борюсь с простой проверкой. У меня есть автоматы и значение x следующим образом:

automataautomata2

Когда x в начале отличен от 0, выполняется E‹> x !=0, но когда x = 0, то оно не выполняется, и выполняются E‹> x == 0 и A‹> x == 0. Но я хотел бы получить неудовлетворительное для E‹> x !=0, даже если x отличается от 0 в начале.

Что мне следует изменить? Как именно работает этот верификатор? Пустой путь, когда ничего не выполнялось, тоже правильный путь? И множество всех возможных путей содержит и этот пустой путь?


verification uppaal
person Robert Ruska    schedule 12.02.2019    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Начальное состояние — это такое же состояние, как и любое другое, поэтому, если x в начальном состоянии равен 0, то все пути, начинающиеся в этом состоянии, в конечном итоге окажутся в состоянии, в котором выполняется x = 0. Если вы хотите проверить, находится ли x = 0 в любом другом состоянии, вам нужно исключить начальное состояние в запросе. Например E<> x=0 and not line1.S0.

person Johan    schedule 18.02.2019
comment
Ty для ответа решил проблему с E‹›, но я все еще борюсь с A‹›. Вы можете найти другой скриншот в определении. Как вообще возможно то, что вы видите на скриншоте? - person Robert Ruska; 21.02.2019
comment
@RobertRuska Случай A‹› связан с часами. Поскольку нет ничего, что заставляло бы прогрессировать, автомат может бесконечно оставаться в положении S0, и в этом случае он никогда не достигнет состояния, в котором выполняется x==0 and not line1.S0. - person Johan; 21.02.2019