Простая основная проблема проверки в Уппале

Question

Я борюсь с простой проверкой.У меня есть автоматы и значение х, как это:

автоматы2

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

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

Answer 1

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