1

我正在运行 Train Gate 示例，并且我想运行验证属性

Pr[<=100] (<> Train(0).Cross)以100 个时间单位表示Train(0)交叉的
概率是多少。

我已将时钟添加到安全状态，如附件所示。

在此处输入图像描述

通过运行上面给出的属性，它给了我以下错误；

Location Train(1).Safe [ Train(0).x=19.641971035860478878021240234375 Train(1).x=4.758311911486089229583740234375 Train(2).x=19.416877078358083963394165039062 Train(3).x=19.25746748410165309906005859375 Train(4).x=19.96133429370820522308349609375 Train( 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 Gate .list[5]=0 Gate.list[6]=0 Gate.len=5 与转换 Train(1).Cross->Train(1).Safe { x >= 3, leave[id]! , 1 } Gate.Occ->Gate.Free { 1 == front(), leave 1 ?, dequeue() }

在倒数第二行中，它说“通过过渡违反了模型健全性”。我一直在寻找（谷歌搜索）这个错误，但到目前为止没有运气，有人可以帮我解决它。

谢谢！

4

1 回答 1

1

问题是，当 train 从Cross到Safe时钟时x，估值大于或等于 3，这与Safe( x<=2) 上的不变量相矛盾，因此 SMC 抱怨该模型没有满足关于模型的假设。

解决方法是x=0在边缘从Cross到重置时钟Safe。

SMC中有很多假设：

  1. 系统不应包含死锁
  2. 系统不应包含时间锁（不应停止时间）
  3. 系统不应包含芝诺行为
  4. 输入处理应该是确定性的
  5. 进程应该能够独立进行：只允许广播同步，输入不能强制输出。

仅举几个...

于 2019-03-26T10:52:28.807 回答