/******************************
 Peterson's algorithm
 Init:   r[0] = r[1] = false t = 0

 For i elem {0,1}
    L0: // The noncritical section
        either stay in this state or advance to L1
    L1: r[i] := true
    L2: t := 1-i
    L3: if not r[1-i] goto L5
    L4: if t not=i goto L5
    L5: // This is the critical section
    L6: r[i] := false; goto L1
******************************/

typedef INDEX 0..1 ;
typedef PC {L0, L1, L2, L3, L4, L5, L6};

module main() {
    /*****************
     *  The variable set
     ************/
    pc: array INDEX of PC;
    r: array INDEX of boolean;
    t: INDEX;
    
    /******************
     * Arbitrary value
     ******************/
    act: INDEX ; /* The active process. */
    arb : boolean ;
    
    /* The initial state */
    init(t) := 0 ;
    forall (i in INDEX) {
        init(r[i]) := 0;
        init(pc[i]) := L0 ; }
    
    /* The algorithm */
    switch( pc[act] ) {
    L0: { if( arb ) {
          next(pc[act]) := L0 ; }
        else { 
          next(pc[act] ) := L1 ;
          next(t) := 1-act ; } }             # Assignment to t is first
    L1: { next(pc[act] ) := L2 ; next( r[act] ) := 1 ; } # Then assignment to r
    L2: { next(pc[act] ) := L3 ; }
    L3: { if( ~r[1-act] ) next(pc[act]) := L5 ; else next(pc[act]) := L4 ; }
    L4: { if( t=act )     next(pc[act]) := L5 ; else next(pc[act]) := L3 ; }
    L5: { next(pc[act]) := L6 ; next(r[act]) := 0 ;}
    L6: { next(pc[act]) := L0 ; } }
    
    /*****************
     *  Fairness assumption :
     *          For each process, it is always the case that
     *          eventually the process becomes active
     ************/
    forall (i in INDEX) { fair[i]: assert G F(act = i); }
    forall (i in INDEX) { assume fair[i];  }
    
    /****************
     * Mutual exclusion property (safety) 
     *      It is never the case that both processes are in the critical
     *      section at the same time
     */
    mutex : assert G ( pc[0] ~= L5 | pc[1] ~= L5 ) ;
    
    
    
    /****************
     * Non starvation property (liveness)
     *      If a process reaches L1, then eventually it will reach L5
     */
    forall (i in INDEX) { 
        nonstarve[i] : assert G( pc[i]=L1 -> F( pc[i]=L5 ) ) ; }
    
    /*****************
     * To prove the liveness property we must
     * Explicitly tell SMV to use the fairness properties
     */
     forall (i in INDEX) { 
        using fair[i], fair[1-i] prove nonstarve[i] ; }
}