Data Race Free Synchronization Model (from F.Pong and M.Dubois "Formal Verification of Delayed Consistency Protocols" IPPS96).

--- DATA RACE FREE EXECUTION MODEL

var  out,cs,scs:discrete;

automaton p
synclabs : ;

initially ss & True;
           
loc ss : while out >= 0 & scs >=0 & cs >=0 wait {} 
         when 
           out >=1 & cs=0 & scs=0
         do {out'=out-1,cs'=cs+1} goto ss;
         when 
           out >=1 & cs=0 & scs>=0
         do {out'=out-1,scs'=scs+1} goto ss;
         when 
           cs>=1 
         do {out'=out+1,cs'=cs-1} goto ss;
         when 
           scs>=1 
         do {out'=out+1,scs'=scs-1} goto ss;
end

var 
   init_reg, final_reg, reached, old, new, Aux : region;

init_reg  := loc[p]=ss & out>=1 & cs=0 & scs=0;
final_reg := loc[p]=ss & cs>=1 & scs>=1;

 reached:= reach backward from final_reg endreach;
--  reached:= reach forward  from init_reg  endreach;
  print reached;