Уппал: оценка вероятности на примере железнодорожных ворот

Question

Я использую пример Train Gate и хочу запустить свойство проверки

Pr[<=100] (<> Train(0).Cross)
Сказать, какова вероятность пересечения поезда (0) в 100-кратных единицах.

Я добавил часы в безопасное состояние, как показано в прикрепленном файле.

Запустив указанное выше свойство, я получаю следующую ошибку;

Расположение Поезд (1).Safe [Поезд (0).x= +19,641971035860478878021240234375 Поезд (1).x=4,758311911486089229583740234375 Поезд (2).x=19,416877078358083963394165039062 Поезд (3).x=19,25746748410165309906005859375 Поезд (4).x=19,96133429370820522308349609375 Поезд (5).x = 19.875009718351066112518310546875 # time = 20.623387750703841447830200195312 ] Gate.list[0]= 4 Gate.list 1 = 5 Gate.list[2 ]= 0 Gate.list[3]= 2 Gate.list[4]= 3 шлюза.list[5]=0 Gate.list[6]=0 Gate.len=5 нарушает разумность модели при переходе Train(1).Cross->Train(1).Safe { x >= 3, оставьте [id]!, 1 } Gate.Occ->Gate.Free { 1 == front(), оставьте 1?, Dequeue() }

Во второй последней строке написано, что "нарушает разумность модели при переходе". Я искал (гуглил) эту ошибку, но пока не повезло, может кто-нибудь помочь мне исправить ее.

Спасибо!

Answer 1

Проблема в том, что когда поезд идет из Cross в Safe часы x имеет оценку, большую или равную 3, что противоречит инварианту на Safe (x<=2), таким образом, SMC жалуется, что модель не полностью соответствует предположениям о модели.

Исправление - сбросить часы с x=0 на краю от Cross в Safe,

Есть много предположений в SMC:

1. система не должна содержать тупиков
2. система не должна содержать временные блокировки (не должна останавливать время)
3. система не должна содержать поведение Zeno
4. обработка ввода должна быть детерминированной
5. процессы должны иметь возможность развиваться независимо: разрешена только широковещательная синхронизация, входы не могут форсировать выходы.

Просто назвать несколько...