critical_bad.csp

var Thread0inside  = 0;
var Thread1inside  = 0;

ThreadZero() = 
    [!(Thread1inside == 1)]
    T0Start
    ->CriticalSectionZero{Thread0inside = 1}
    ->T0End{Thread0inside = 0}
    ->OtherStuffZero
    ->ThreadZero();

ThreadOne() = 
  [!(Thread0inside == 1)]
   T1Start
    ->CriticalSectionOne{Thread1inside = 1}
    ->T1End{Thread1inside = 0}
    ->OtherStuffOne
    ->ThreadOne();

System = ThreadZero() || ThreadOne();

#assert System deadlockfree;
#define badstatus (Thread0inside==1 && Thread1inside == 1);
#assert System reaches badstatus;