在 proctype 错误中未达到 Promela SPIN
Promela SPIN unreached in proctype error
我是 SPIN 和 Promela 的新手,我在尝试验证模型中的活性 属性 时遇到了这个错误。
错误代码:
unreached in proctype P
(0 of 29 states)
unreached in proctype monitor
mutex_assert.pml:39, state 1, "assert(!((mutex>1)))"
mutex_assert.pml:42, state 2, "-end-"
(2 of 2 states)
unreached in init
(0 of 3 states)
unreached in claim ltl_0
_spin_nvr.tmp:10, state 13, "-end-"
(1 of 13 states)
pan: elapsed time 0 seconds
该代码基本上是彼得森算法的一个实现,我检查了安全性,它似乎是有效的。但是每当我尝试使用 ltl {[]((wait -> <> (cs)))} 验证活性 属性 时,它都会出现上述错误。我不确定它们是什么意思,所以我不知道如何继续...
我的代码如下:
#define N 3
#define wait (P[1]@WAIT)
#define cs (P[1]@CRITICAL)
int pos[N];
int step[N];
int enter;
byte mutex;
ltl {[]((wait -> <> (cs)))}
proctype P(int i) {
int t;
int k;
WAIT:
for (t : 1 .. (N-1)){
pos[i] = t
step[t] = i
k = 0;
do
:: atomic {(k != i && k < N && (pos[k] < t|| step[t] != i)) -> k++}
:: atomic {k == i -> k++}
:: atomic {k == N -> break}
od;
}
CRITICAL:
atomic {mutex++;
printf("MSC: P(%d) HAS ENTERED THE CRITICAL SECTION.\n", i);
mutex--;}
pos[i] = 0;
}
init {
atomic { run P(0); }
}
一般答案
这是一个警告,告诉您某些状态无法到达,因为从未进行过转换。
一般来说,这不是一个错误,但它是一个好的做法仔细查看 您建模的每个例程 的无法访问状态,并检查您是否期望其中的 none 可以访问。 即在模型不正确的情况下。预期的行为.
注意可以在特定代码行前使用标签end:来标记有效的终止状态,这样摆脱那些警告,例如当您的程序没有终止时。更多信息 here.
具体答案
我无法重现你的输出。特别是 运行
~$ spin -a file.pml
~$ gcc pan.c
~$ ./a.out -a
我得到以下输出,与你的不同:
(Spin Version 6.4.3 -- 16 December 2014)
+ Partial Order Reduction
Full statespace search for:
never claim + (ltl_0)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 64 byte, depth reached 47, errors: 0
41 states, stored (58 visited)
18 states, matched
76 transitions (= visited+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.004 equivalent memory usage for states (stored*(State-vector + overhead))
0.288 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
128.730 total actual memory usage
unreached in proctype P
(0 of 29 states)
unreached in init
(0 of 3 states)
unreached in claim ltl_0
_spin_nvr.tmp:10, state 13, "-end-"
(1 of 13 states)
pan: elapsed time 0 seconds
特别是,我缺少有关 monitor 进程中未达到状态的警告。就我而言,从源代码来看,我得到的警告none是有问题的。
您使用的 Spin 版本与我不同,或者您没有在问题中包含完整的源代码。在后一种情况下,您可以编辑您的问题并添加代码吗?之后我会更新我的答案。
EDIT:在评论中,您问以下消息是什么意思:"unreached in claim ltl_0 _spin_nvr.tmp:10, state 13, "-end-"" .
如果打开文件_spin_nvr.tmp,可以看到如下一段Promela代码,对应一个Büchi 自动机 接受所有且只接受违反你的 ltl 的执行 属性 []((wait -> <> (cs))).
never ltl_0 { /* !([] ((! ((P[1]@WAIT))) || (<> ((P[1]@CRITICAL))))) */
T0_init:
do
:: (! ((! ((P[1]@WAIT)))) && ! (((P[1]@CRITICAL)))) -> goto accept_S4
:: (1) -> goto T0_init
od;
accept_S4:
do
:: (! (((P[1]@CRITICAL)))) -> goto accept_S4
od;
}
该消息只是警告您此代码的执行永远不会到达最后一个右括号 }(状态 "-end-"), 这意味着该过程永远不会终止。
我是 SPIN 和 Promela 的新手,我在尝试验证模型中的活性 属性 时遇到了这个错误。
错误代码:
unreached in proctype P
(0 of 29 states)
unreached in proctype monitor
mutex_assert.pml:39, state 1, "assert(!((mutex>1)))"
mutex_assert.pml:42, state 2, "-end-"
(2 of 2 states)
unreached in init
(0 of 3 states)
unreached in claim ltl_0
_spin_nvr.tmp:10, state 13, "-end-"
(1 of 13 states)
pan: elapsed time 0 seconds
该代码基本上是彼得森算法的一个实现,我检查了安全性,它似乎是有效的。但是每当我尝试使用 ltl {[]((wait -> <> (cs)))} 验证活性 属性 时,它都会出现上述错误。我不确定它们是什么意思,所以我不知道如何继续...
我的代码如下:
#define N 3
#define wait (P[1]@WAIT)
#define cs (P[1]@CRITICAL)
int pos[N];
int step[N];
int enter;
byte mutex;
ltl {[]((wait -> <> (cs)))}
proctype P(int i) {
int t;
int k;
WAIT:
for (t : 1 .. (N-1)){
pos[i] = t
step[t] = i
k = 0;
do
:: atomic {(k != i && k < N && (pos[k] < t|| step[t] != i)) -> k++}
:: atomic {k == i -> k++}
:: atomic {k == N -> break}
od;
}
CRITICAL:
atomic {mutex++;
printf("MSC: P(%d) HAS ENTERED THE CRITICAL SECTION.\n", i);
mutex--;}
pos[i] = 0;
}
init {
atomic { run P(0); }
}
一般答案
这是一个警告,告诉您某些状态无法到达,因为从未进行过转换。
一般来说,这不是一个错误,但它是一个好的做法仔细查看 您建模的每个例程 的无法访问状态,并检查您是否期望其中的 none 可以访问。 即在模型不正确的情况下。预期的行为.
注意可以在特定代码行前使用标签end:来标记有效的终止状态,这样摆脱那些警告,例如当您的程序没有终止时。更多信息 here.
具体答案
我无法重现你的输出。特别是 运行
~$ spin -a file.pml
~$ gcc pan.c
~$ ./a.out -a
我得到以下输出,与你的不同:
(Spin Version 6.4.3 -- 16 December 2014)
+ Partial Order Reduction
Full statespace search for:
never claim + (ltl_0)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)
State-vector 64 byte, depth reached 47, errors: 0
41 states, stored (58 visited)
18 states, matched
76 transitions (= visited+matched)
0 atomic steps
hash conflicts: 0 (resolved)
Stats on memory usage (in Megabytes):
0.004 equivalent memory usage for states (stored*(State-vector + overhead))
0.288 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
128.730 total actual memory usage
unreached in proctype P
(0 of 29 states)
unreached in init
(0 of 3 states)
unreached in claim ltl_0
_spin_nvr.tmp:10, state 13, "-end-"
(1 of 13 states)
pan: elapsed time 0 seconds
特别是,我缺少有关 monitor 进程中未达到状态的警告。就我而言,从源代码来看,我得到的警告none是有问题的。
您使用的 Spin 版本与我不同,或者您没有在问题中包含完整的源代码。在后一种情况下,您可以编辑您的问题并添加代码吗?之后我会更新我的答案。
EDIT:在评论中,您问以下消息是什么意思:"unreached in claim ltl_0 _spin_nvr.tmp:10, state 13, "-end-"" .
如果打开文件_spin_nvr.tmp,可以看到如下一段Promela代码,对应一个Büchi 自动机 接受所有且只接受违反你的 ltl 的执行 属性 []((wait -> <> (cs))).
never ltl_0 { /* !([] ((! ((P[1]@WAIT))) || (<> ((P[1]@CRITICAL))))) */
T0_init:
do
:: (! ((! ((P[1]@WAIT)))) && ! (((P[1]@CRITICAL)))) -> goto accept_S4
:: (1) -> goto T0_init
od;
accept_S4:
do
:: (! (((P[1]@CRITICAL)))) -> goto accept_S4
od;
}
该消息只是警告您此代码的执行永远不会到达最后一个右括号 }(状态 "-end-"), 这意味着该过程永远不会终止。