作者热门文章
- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
我对旋转模型检查很陌生,想知道这个错误意味着什么:
unreached in proctype P1
ex2.pml:16, state 11, "-end-"
(1 of 11 states)
unreached in proctype P2
ex2.pml:29, state 11, "-end-"
(1 of 11 states)
这是我的代码:
int y1, y2;
byte insideCritical;
active proctype P1(){
do
::true->
y2 = y1 + 1;
(y1 == 0 || y2 < y1);
/* Entering critical section */
insideCritical++;
assert(insideCritical < 2);
insideCritical--;
/* Exiting critical section */
y2 = 0;
od
}
active proctype P2(){
do
::true->
y1 = y2 + 1;
(y2 == 0 || y1 < y2);
/* Entering critical section */
insideCritical++;
assert(insideCritical < 2);
insideCritical--;
/* Exiting critical section */
y1 = 0;
od
}
它实际上不必结束,它是一个互斥程序,用于检查两个进程是否不在临界区。该错误是否意味着程序没有结束?谢谢!
最佳答案
Spin 通知您您的 proctypes 永远不会达到“结束”状态,这当然是正确的,因为它们由无限循环组成。如果这不是预期的行为,那么这将是一个有用的信息。但是,在您的情况下,您可以通过在代码中添加结束标签来告诉 Spin 允许程序以与 do 循环相对应的状态结束,例如:
active proctype P1(){
endHere:
do
:: true->
y2 = y1 + 1;
(y1 == 0 || y2 < y1);
/* Entering critical section */
insideCritical++;
assert(insideCritical < 2);
insideCritical--;
/* Exiting critical section */
y2 = 0;
od
}
结束标签是任何以“end”开头的标签。如果您的 proctype 以这种方式标记的状态结束,Spin 将不会向您显示这些警告。
关于process - proctype "-end-"中未达到自旋,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/22759202/
我对旋转模型检查很陌生,想知道这个错误意味着什么: unreached in proctype P1 ex2.pml:16, state 11, "-end-" (1 of 11 st
我是一名优秀的程序员,十分优秀!