This download includes a README file 
and the benchmarks for the risk analysis  
and TCTL model-checking of the Fischer algorithm. 
The model file is in 

  hf.d     : mutual exclusion with constants A=10 and B=19 
  hf.38.d  : the same as hf.d except A=20 and B=38
  hf.76.d  : the same as hf.d except A=40 and B=76
  hf.152.d : the same as hf.d except A=80 and B=152
  hf.304.d : the same as hf.d except A=160 and B=304
  hfb.d    : the same as hf.d except that in critical section, 
             we can only stay for 30 sec.
  hfn.d    : failing mutual exclusion with A=10 and B=19

The specification file are  

  hf1.2.risk : a risk predicate that should never be true. 
  hf.always.sequence.tctl : a TCTL formula. 
  hf.critical.critical.safety.tctl : a TCTL formula
  hf.nonpreempty.tctl : a TCTL formula 
  hf.ready.deadlock.liveness.tctl: a TCTL formula
  hf.ready.deadlock.tctl: a TCTL formula
  
To use RED version 7, you can type in the following command. 

  % red -Tr -M4 hf.d hf1.2.risk 
  
    risk analysis for 4 processes 
    
  % red -Tm -M5 hf.d hf.critical.critical.safety.tctl 
  
    model-checking for 5 processes 
    
  % red -Tm -M3 hf.d hcd.nonpreempty.tctl 
  
    model-checking for 3 processes




