Refal encoding

*$MST_FROM_ENTRY;
*$STRATEGY Applicative;
*$LENGTH 0;


$ENTRY Go {e.A (e.i) = <Loop (e.A) (Invalid e.i)(Dirty )(Shared )(Exclusive ) >;}

Loop {
  () (Invalid e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4) =
             <Result (Invalid e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4)>;
  (s.A e.A) (Invalid e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4) = 
         <Loop (e.A) 
         <RandomAction s.A
         (Invalid e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4)>>;
}

RandomAction {
* r1 Trivial 
* r2
A (Invalid s.1 e.1) (Dirty ) (Shared ) (Exclusive)
   =(Invalid e.1)  (Dirty )  (Shared ) (Exclusive s.1);
* r3
B (Invalid s.1 e.1)(Dirty s.2 e.2)(Shared e.3)(Exclusive e.4) =
  (Invalid e.1)(Dirty e.2)(Shared s.1 s.2 e.3)(Exclusive e.4);
* r4 
C (Invalid s.1 e.1)(Dirty e.2)(Shared s.3 e.3)(Exclusive e.4) =
  (Invalid e.1)(Dirty e.2)(Shared s.1 e.4 s.3 e.3)(Exclusive);
* r4'  
D (Invalid s.1 e.1)(Dirty e.2)(Shared e.3)(Exclusive s.4 e.4) =
  (Invalid e.1)(Dirty e.2)(Shared s.1 s.4 e.4 e.3)(Exclusive);
* r5 Trivial 
* r6 
E (Invalid e.1)(Dirty e.2)(Shared e.3)(Exclusive s.4 e.4) =
  (Invalid e.1)(Dirty s.4 e.2)(Shared e.3)(Exclusive e.4);
* r7
F (Invalid e.1)(Dirty e.2)(Shared s.3 e.3)(Exclusive e.4) = 
   (Invalid e.1 e.3)(Dirty s.3 e.2)(Shared )(Exclusive e.4);
* r8 
G  (Invalid s.1 e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4) =
   (Invalid  e.4 e.3 e.2 e.1)(Dirty s.1)(Shared )(Exclusive );
* r9 
H  (Invalid e.1)(Dirty s.2 e.2)(Shared e.3)(Exclusive e.4) =
   (Invalid s.2 e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4);
* r10
I (Invalid e.1)(Dirty e.2)(Shared s.3 e.3)(Exclusive e.4) =
  (Invalid s.3 e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4);
* r11 
J (Invalid e.1)(Dirty e.2)(Shared e.3)(Exclusive s.4 e.4) =
   (Invalid s.4 e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4); 
}

Result{
(Invalid e.1)(Dirty s.2 e.2)(Shared s.3 e.3)(Exclusive e.4) = False;
(Invalid e.1)(Dirty s.21 s.22 e.2)(Shared e.3)(Exclusive e.4) = False;
(Invalid e.1)(Dirty e.2)(Shared e.3)(Exclusive e.4) = True;
}