Я надеюсь, что кто-то здесь может дать мне ваш совет или знания.
Я уже читал о примере железнодорожных ворот в Уппале и в Спине. Я также пытался использовать Uppaal для проверки своих планов, и результаты были отличными. Тем не мение. Я хотел бы немного расширить свой план. Поэтому я попытался использовать Spin для проверки некоторых свойств, не относящихся ко времени.
Мой вопрос: могу ли я понять, что, если я уберу относительное время (часы), Уппал сможет справиться с одним и тем же Спином. если нет, можете ли вы привести пример или свойство для демонстрации?
Любая информация или совет полезны для меня.
Искренне благодарю вас за чтение.