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

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

0 голосов
/ 04 сентября 2018

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

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

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

enter image description here

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

Расположение поезда (1). Безопасно [Поезд (0) .x = +19,641971035860478878021240234375 Поезд (1) .x = 4,758311911486089229583740234375 Поезд (2) .x = +19,416877078358083963394165039062 Поезд (3) .x = 19,25746748410165309906005859375 Поезд (4) .x = 19,96133429370820522308349609375 Поезд (5) .x = +19,875009718351066112518310546875 # время = 20,623387750703841447830200195312] Gate.list [0] = 4 Gate.list 1 = 5 Gate.list [2] = 0 Gate.list [3] = 2 Gate.list [4] = 3 Gate.list [5] = 0 Gate.list [6] = 0 Gate.len = 5 нарушает разумность модели при переходе Поезд (1). Кросс-> Поезд (1). Безопасно {x> = 3, оставьте [id] !, 1} Gate.Occ-> Gate.Free {1 == front (), выход 1 ?, dequeue ()}

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

Спасибо!

1 Ответ

0 голосов
/ 26 марта 2019

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

Исправлена ​​ошибка, при которой часы сбрасывались с x=0 на грани с Cross до Safe.

В SMC много предположений:

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

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

...