Spinroot

A forum for Spin users

You are not logged in.

#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

spinroot
forum
Registered: 2010-11-18
Posts: 694
Website

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

#5 2012-12-30 06:28:15

lili
Member
Registered: 2012-12-30
Posts: 2
Website

Re: end label

Could I get a clarification.

Offline

Board footer

Powered by FluxBB