[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

State contraint



I copied the bakery algorithm from the book. When I added a check for StarvationFree, I indeed got "Temporal properties were violated.". But when I added a state contraint as in the book, the same happened. 

When I played with the numbers (e.g. define Int as 1..10, but constrain 
\A p \in Procs : num [p]  < 7
) the error trace stopped with num = <0,0,6>, not with any higher number.

What is wrong? and why is state-constraint not needed for DeadlockFree?

Thanks

Module enclosed:
-----------------------------


--------------------------- MODULE bakery ---------------------------
EXTENDS Integers
CONSTANT N
ASSUME N \in Nat
Procs == 1..N
a \prec b == \/ a[1] < b[1]
             \/ (a[1] = b[1]) /\ (a[2] < b[2])
(*
--fair algorithm BigStepBakery
{ variable num = [i \in Procs |-> 0] ;
process (pr \in Procs)
variable unchecked = {} ;
   { ncs:- while (TRUE)
         { enter: with (i \in { j \in Nat : \A q \in Procs : j > num[q] })
                { num[self] := i } ;
               unchecked := Procs \ {self} ;
         wait: while (unchecked # {})
                { with (i \in unchecked)
                     { await \/ num[i] = 0
                             \/ <<num[self], self>> \prec <<num[i], i>> ;
                       unchecked := unchecked \ {i}
                     }
                } ;
           cs: skip ; \* critical section
         exit: num[self] := 0
         }
    }
} *)
\* BEGIN TRANSLATION
VARIABLES num, pc, unchecked

vars == << num, pc, unchecked >>

ProcSet == (Procs)

Init == (* Global variables *)
        /\ num = [i \in Procs |-> 0]
        (* Process pr *)
        /\ unchecked = [self \in Procs |-> {}]
        /\ pc = [self \in ProcSet |-> "ncs"]

ncs(self) == /\ pc[self] = "ncs"
             /\ pc' = [pc EXCEPT ![self] = "enter"]
             /\ UNCHANGED << num, unchecked >>

enter(self) == /\ pc[self] = "enter"
               /\ \E i \in { j \in Nat : \A q \in Procs : j > num[q] }:
                    num' = [num EXCEPT ![self] = i]
               /\ unchecked' = [unchecked EXCEPT ![self] = Procs \ {self}]
               /\ pc' = [pc EXCEPT ![self] = "wait"]

wait(self) == /\ pc[self] = "wait"
              /\ IF unchecked[self] # {}
                    THEN /\ \E i \in unchecked[self]:
                              /\ \/ num[i] = 0
                                 \/ <<num[self], self>> \prec <<num[i], i>>
                              /\ unchecked' = [unchecked EXCEPT ![self] = unchecked[self] \ {i}]
                         /\ pc' = [pc EXCEPT ![self] = "wait"]
                    ELSE /\ pc' = [pc EXCEPT ![self] = "cs"]
                         /\ UNCHANGED unchecked
              /\ num' = num

cs(self) == /\ pc[self] = "cs"
            /\ TRUE
            /\ pc' = [pc EXCEPT ![self] = "exit"]
            /\ UNCHANGED << num, unchecked >>

exit(self) == /\ pc[self] = "exit"
              /\ num' = [num EXCEPT ![self] = 0]
              /\ pc' = [pc EXCEPT ![self] = "ncs"]
              /\ UNCHANGED unchecked

pr(self) == ncs(self) \/ enter(self) \/ wait(self) \/ cs(self)
               \/ exit(self)

Next == (\E self \in Procs: pr(self))

Spec == /\ Init /\ [][Next]_vars
        /\ WF_vars(Next)

\* END TRANSLATION
-----------------------------------------------------------------------------
TypeOK == /\ num \in [Procs -> Nat]
          /\ unchecked \in [Procs -> SUBSET Procs]
          /\ pc \in [Procs -> {"ncs", "enter", "wait", "cs", "exit"}]
MutualExclusion ==
      \A p, q \in Procs : (p # q) => ~((pc[p] = "cs") /\ (pc[q] = "cs"))
\* liveness stuff below      
Trying(p) == pc[p] \in {"enter", "wait"}
InCS(p) == pc[p] = "cs"
DeadlockFree == (\E p \in Procs : Trying(p)) ~> (\E p \in Procs : InCS(p))
StarvationFree == \A p \in Procs : Trying(p) ~> InCS(p)
=============================================================================

=============================================================================
\* Modification History
\* Last modified Sun Apr 06 15:06:48 PDT 2014 by Gideon
\* Created Sun Apr 06 13:55:30 PDT 2014 by Gideon