Refal encoding

* Reader-Writer mutual exclusion protocol from the paper 
* "Petri Nets, Flat Languages and Linear Arithmetic", by Laurent Fribourg
* 
*$MST_FROM_ENTRY;
*$STRATEGY Applicative;
*$LENGTH 0;


$ENTRY Go {e.A (e.q) (s.i) = <Loop (e.A)(x2 s.i)(x3)(x4)(x5 e.q)(x6)(x7) >;}

Loop {
  () (x2 e.2)(x3 e.3)(x4 e.4)(x5 e.5)(x6 e.6)(x7 e.7) =
                                <Test (x2 e.2)(x3 e.3)(x4 e.4)(x5 e.5)(x6 e.6)(x7 e.7)>;
  (s.A e.A)(x2 e.2)(x3 e.3)(x4 e.4)(x5 e.5)(x6 e.6)(x7 e.7) =
         <Loop (e.A) 
         <RandomAction s.A
         (x2 e.2)(x3 e.3)(x4 e.4)(x5 e.5)(x6 e.6)(x7 e.7)>>;
}



RandomAction {
*r1
A (x2 s.2 e.2)(x3 e.3)(x4)(x5 e.5)(x6 e.6)(x7 s.7 e.7)
   = (x2 e.2)(x3 s.2 e.3)(x4)(x5 e.5)(x6 e.6)(x7 e.7);

*r2
B (x2 s.2 e.2)(x3 e.3)(x4 e.4)(x5 e.5)(x6 s.6 e.6)(x7 e.7)
   = (x2 s.2 e.2)(x3 e.3)(x4 s.6 e.4)(x5 e.5)(x6 e.6)(x7 e.7);
   

*r3
C (x2 e.2)(x3 s.3 e.3)(x4 e.4)(x5 e.5)(x6 e.6)(x7 e.7)
   = (x2 s.3 e.2)(x3 e.3)(x4 e.4)(x5 s.3 e.5)(x6 e.6)(x7 e.7);
*r4
D (x2 e.2)(x3 e.3)(x4 s.4 e.4)(x5 e.5)(x6 e.6)(x7 e.7)
   = (x2 e.2)(x3 e.3)(x4 e.4)(x5 s.4 e.5)(x6 e.6)(x7 e.7);

*r5
E (x2 e.2)(x3 e.3)(x4 e.4)(x5 s.5 e.5)(x6 e.6)(x7 e.7)
   = (x2 e.2)(x3 e.3)(x4 e.4)(x5 e.5)(x6 s.5 e.6)(x7 e.7);

*r6
F (x2 e.2)(x3 e.3)(x4 e.4)(x5 s.5 e.5)(x6 e.6)(x7 e.7)
   = (x2 e.2)(x3 e.3)(x4 e.4)(x5 e.5)(x6 e.6)(x7 s.5 e.7);
}



Test{
(x2 e.2)(x3 s.3 e.3)(x4 s.4 e.4)(x5 e.5)(x6 e.6)(x7 e.7) = False;
(x2 e.2)(x3 e.3)(x4 e.4)(x5 e.5)(x6 e.6)(x7 e.7)= True;
}