Spinroot
A forum for Spin users
You are not logged in.
- Topics: Active | Unanswered
Pages: 1
#1 2012-06-05 10:24:51
- lz
- Member
- Registered: 2012-05-14
- Posts: 9
Priorities and verification
Hello,
Is this a mistake or I misconfigured the verifier?
Normally the process M should not be executed before the end of H.
Do you have a comment...
With my thanks.
byte cnt;
active proctype M() priority 5 {
int temp;
...
set_priority(0, get_priority(1));
temp = cnt; temp++; cnt = temp;
}
active proctype H() priority 10 {
int temp;
temp = cnt; temp++; cnt = temp;
}
active proctype B() priority 1 {
assert(_priority == 1 && cnt == 2);
}
spin -a priorite1.pml
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DSAFETY -DNOCLAIM -DNOREDUCE -w -o pan pan.c
./pan -m10000 -E
Pid: 4584
pan:1: assertion violated ((_priority==1)&&(cnt==2)) (at depth 10)
pan: wrote priorite1.pml.trail
(Spin Version 6.2.1 -- 14 May 2012)
Offline
#3 2012-06-06 10:49:14
- feng_lei_76
- Member
- Registered: 2011-05-13
- Posts: 43
Re: Priorities and verification
I might find another bug from this example. If I add a useless statement in process M before set_priority, then verification results with DFS and BFS searches are different. DFS search finds the error, but BFS doesn't.
This is my Promela modle.
/******************************************************/
byte cnt;
active proctype M() priority 5
{
int temp;
temp = 0;
set_priority(0, get_priority(1));
temp = cnt; temp++; cnt = temp
}
active proctype H() priority 10
{
int temp;
temp = cnt; temp++; cnt = temp
}
active proctype B() priority 1
{
assert(_priority == 1 && cnt == 2)
}
Offline
Pages: 1