Spinroot
A forum for Spin users
You are not logged in.
- Topics: Active | Unanswered
#1 2012-12-06 09:12:13
- lz
- Member
- Registered: 2012-05-14
- Posts: 9
end label
Hello,
Could I get a clarification.
The following example generates an error (invalid end state),
although with the indication than valid end state (label end_sem:).
mtype {p, v}
chan sem = [0] of {mtype}
active proctype semaphore() {
bit binaire = 1;
end_sem: do :: binaire==1 -> sem ! p; binaire = 0;
:: binaire==0 -> sem ? v; binaire = 1;
od;
}
active[3] proctype concurrent() {
byte cnt=0;
do :: cnt<3 -> sem ? p;
section_critique: cnt++;
sem ! v
od
}
While the following (and others) does not throw an error,
as expected (label end_service:):
proctype verrou(chan ver, dev) {
end_service: do :: ver ? _ -> dev ? _; od;
}
byte cnt;
proctype tache(chan ver, dev) {
byte essais = 2;
do :: ver ! 1 -> cnt++; assert(cnt<=1); cnt--;
dev ! 1;
if :: essais>0 -> essais--;
:: else -> break;
fi;
od;
}
init { chan verrouiller = [0] of {bit};
chan deverrouiller = [0] of {bit};
atomic { run verrou(verrouiller, deverrouiller);
run tache(verrouiller, deverrouiller);
run tache(verrouiller, deverrouiller);
run tache(verrouiller, deverrouiller);
}
}
With my best thanks.
Offline
#2 2012-12-06 14:28:19
- lz
- Member
- Registered: 2012-05-14
- Posts: 9
Re: end label
Oops, ...
missing a line (break) in process declaration:
active[3] proctype concurrent() {
byte cnt=0;
do :: cnt<3 -> sem ? p;
section_critique: cnt++;
sem ! v
:: else -> break
od
}
...
Offline
#3 2012-12-08 06:41:25
Re: end label
the problem with the first example is that the semaphore process is not waiting at the do loop, but at the sem ! p operation, which does not have an invalid end-state
the report from spin -t -p spec.pml is that the wait state for the semaphore process is state 2
you can lookup which state that is by executing: ./pan -d
Offline
#4 2012-12-10 12:10:56
- lz
- Member
- Registered: 2012-05-14
- Posts: 9
Re: end label
Indeed, it is clear.
At the origin of my confusion, the fig 4.1 in SPIN Model Checker...
Thank you very much for your clarification.
Offline