A forum for Spin users
You are not logged in.
Pages: 1
Consider the following extract of code :
#define PRIO_MAX 35 // or 255
proctype T(byte calcul, periode, id) {
int prio_normale;
/**/ prio_normale = get_priority(_pid);
// or
/**/ prio_normale = _priority;
set_priority(_pid, PRIO_MAX);
skip;
set_priority(_pid, prio_normale);
}
init { atomic { run T(25, 100, 0) priority 30;
run T(30, 150, 1) priority 20;
run T(75, 200, 2) priority 10;
//run idle(3);
}
}
Simulation is OK, but the verification (partial order reduction disabled)
generates the following message:
spin -a Error_Prio.pml
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DSAFETY -DNOCLAIM -DNOREDUCE -w -o pan pan.c
./pan -m10000 -E -n
Pid: 2076
pan:1: priority is out of range (at depth 5)
pan: wrote Error_Prio.pml.trail
Do you have a comment, thanking you.
Thank you, for your explanation.
(the array was used only to analyse the behavior of process in simulation)
Best regards
In this example:
------------------------------------------------------------------------------
int traversant;
int tvs[2];
bit Feux[2];
active[2] proctype processus() { /* adapt. from Burns & Lynch ... */
int vehic = _pid;
L0: Feux[ vehic] = 0;
if :: vehic==1 && Feux[0]==1 -> goto L0
:: else -> Feux[vehic] = 1
fi;
if :: vehic==1 && Feux[0]==1 -> goto L0
:: else -> L1: if :: vehic==0 && Feux[1]==1 -> goto L1
:: else -> traversant++; tvs[vehic]++;
progress_sc: assert(traversant==1);
traversant--
fi
fi;
goto L0
}
------------------------------------------------------------------------------
If I simply replace the variable "tvs" by "t", the following error is reported ...
------------------------------------------------------------------------------
spin -a croisement_minimal.pml
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DSAFETY -DNOCLAIM -DREACH -w -o pan pan.c
In file included from pan.c:5562:0:
pan.m: In function 'do_transit':
pan.m:73:36: error: incompatible types when assigning to type 'int' from type 'Trans'
pan.m:74:89: error: invalid operands to binary + (have 'Trans' and 'int')
In file included from pan.c:6920:0:
pan.b: In function 'new_state':
pan.b:33:52: error: incompatible types when assigning to type 'Trans' from type 'int'
./pan -m10000 -i
Best regards
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.
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
}
...
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.
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)
Hello,
Is this a mistake or I misconfigured the verifier?
Normally the process M should not be executed before the end of H.
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)
Hello,
the select statement is inconsistent
with syntax version 6.2
from manual:
i = 8;
do
:: i < 17 -> i++
:: break
od
Could it be fixed?
With my thanks, best regards.
LZ
Pages: 1