/*
 Parallel composition of two copies of the thread:
  let rec sync f = lock; f(); unlock; sync f in
  let rec cr x = if _ then () else cr x; enter; exit in 
    sync cr
 */
%BEGING
S -> Sched M M.
Sched x y -> x(Sched y).
M g -> Sync Cr E g.
E g -> end.
Sync f k g -> lock(br (C1 f k g) (g (C1 f k))).
C1 f k g ->  f (C2 f k) g.
C2 f k g -> unlock(br (Sync f k g) (g (Sync f k))).
Cr k g -> br (k g) (Cr (C3 k) g).
C3 k g -> enter(br (C4 k g) (g (C4 k))).
C4 k g -> exit (br (k g) (g k)).
%ENDG

%BEGINA
/* state qij:
     i: whether locked (1) or not
     j: whether critical section is entered (1) or not (0)
 */
q00 br -> q00 q00. 
q01 br -> q01 q01.
q10 br -> q10 q10.
q11 br -> q11 q11.
qany br -> qany qany.
qany unlock -> qany.
qany end -> .
qany enter -> qany.
qany exit -> qany.
q00 lock -> q10.
q01 lock -> q11.
q10 lock -> qany.
q11 lock -> qany.
qany lock -> qany.
q00 unlock -> qany.
q01 unlock -> qany.
q10 unlock -> q00.
q11 unlock -> q01.
q00 enter -> q01.
q10 enter -> q11.
q01 exit -> q00.
q11 exit -> q10.
q00 end -> .
q10 end -> .
q01 end -> .
q11 end -> .
%ENDA