Простая основная проблема проверки в Уппале
Я борюсь с простой проверкой. У меня есть автоматы и значение х, как это:
Когда x в начале отличается от 0, то E<> x!=0 удовлетворяется, но когда x = 0, тогда его не удовлетворяют, и E<> x == 0 и A<> x == 0 удовлетворяются. Но я хотел бы получить неудовлетворенный для E<> x!=0, даже если x отличается от 0 в начале.
Что я должен изменить? Как работает этот верификатор? Пустой путь, когда ничего не было выполнено - это тоже правильный путь? И множество всех возможных путей содержит этот пустой путь?
1 ответ
Начальное состояние - это состояние, подобное любому другому, поэтому, если x в начальном состоянии равно 0, то все пути, начинающиеся в этом состоянии, в конечном итоге окажутся в состоянии, в котором x = 0 держит. Если вы хотите проверить, если x = 0 в любом другом состоянии вам необходимо исключить начальное состояние в запросе. Например E<> x=0 and not line1.S0,