Refal encoding

* Java Meta-Locking algorithm
*--------------------------------------------------------------------------------------
*$MST_FROM_ENTRY;
*$STRATEGY Applicative;
*$LENGTH 0;


trans {
 get_fast (obj_trans not_busy) t.race
          (idle s.1 e.idle) (owner e.owner) (handin e.handin) (handout e.handout) (wait e.wait)
     =    (obj_trans (busy)) t.race 
          (idle e.idle) (owner s.1 e.owner) (handin e.handin) (handout e.handout) (wait e.wait);
 put_fast (obj_trans (busy)) t.race
          (idle e.idle) (owner s.1 e.owner) (handin e.handin) (handout e.handout) (wait e.wait)
     =    (obj_trans not_busy) t.race
          (idle s.1 e.idle) (owner e.owner) (handin e.handin) (handout e.handout) (wait e.wait);
 get_slow (obj_trans (busy e.busy)) t.race
          (idle s.1 e.idle) (owner e.owner) (handin e.handin) (handout e.handout) (wait e.wait)
     =    (obj_trans (busy I e.busy)) t.race
          (idle e.idle) (owner e.owner) (handin s.1 e.handin) (handout e.handout) (wait e.wait);
 put_slow (obj_trans (busy s.1 e.busy)) t.race
          (idle e.idle) (owner s.2 e.owner) (handin e.handin) (handout e.handout) (wait e.wait)
     =    (obj_trans (busy e.busy)) t.race
          (idle e.idle) (owner e.owner) (handin e.handin) (handout s.2 e.handout) (wait e.wait);

 request  t.obj_trans (race h0)
          (idle e.idle) (owner e.owner) (handin s.1 e.handin) (handout e.handout) (wait e.wait)
      =   t.obj_trans (race h1)
          (idle e.idle) (owner e.owner) (handin e.handin) (handout e.handout) (wait s.1 e.wait);
 request  t.obj_trans (race h2)
          (idle e.idle) (owner e.owner) (handin s.1 e.handin) (handout e.handout) (wait e.wait)
      =   t.obj_trans (race h3)
          (idle e.idle) (owner e.owner) (handin e.handin) (handout e.handout) (wait s.1 e.wait);

 release  t.obj_trans (race h0)
          (idle e.idle) (owner e.owner) (handin e.handin) (handout s.1 e.handout) (wait e.wait)
      =   t.obj_trans (race h2)
          (idle s.1 e.idle) (owner e.owner) (handin e.handin) (handout e.handout) (wait e.wait);
 release  t.obj_trans (race h2)
          (idle e.idle) (owner e.owner) (handin e.handin) (handout s.1 e.handout) (wait e.wait)
      =   t.obj_trans (race h3)
          (idle s.1 e.idle) (owner e.owner) (handin e.handin) (handout e.handout) (wait e.wait);

 go  t.obj_trans (race h3)
          (idle e.idle) (owner e.owner) (handin e.handin) (handout e.handout) (wait s.1 e.wait)
      = t.obj_trans (race h3)
          (idle e.idle) (owner s.1 e.owner) (handin e.handin) (handout e.handout) (wait e.wait);
 s.act  t.obj_trans t.race
          t.idle t.owner t.handin t.handout t.wait
      =   t.obj_trans t.race
          t.idle t.owner t.handin t.handout t.wait;
}

$ENTRY Go {
*/*
 e.A (e.threads) 
    = <Loop1 (e.A) (obj_trans not_busy) (race h0)
                   (idle e.threads) (owner) (handin) (handout) (wait) 
      >;
*/

/*
 e.A (e.threads) 
    = <Loop1 () (obj_trans not_busy) (race h0)
                   (idle e.threads) (owner) (handin) (handout) (wait) 
      >;
*/

/*
    = <Prout <Loop1 () 
                    (obj_trans not_busy) (race h0)
                   (idle I I) (owner) (handin) (handout) (wait) 
      >>;
*/
/*
    = <Prout <Loop1 (get_fast put_fast get_fast get_slow put_slow get_fast put_slow request releas go) 
                    (obj_trans not_busy) (race h0)
                   (idle I I) (owner) (handin) (handout) (wait) 
      >>;
*/
}

Loop1 {
  () (obj_trans e.busy) t.race
     (idle e.idle) (owner e.owner) (handin e.handin) (handout e.handout) (wait e.wait)
        =  <Result3 (obj_trans e.busy) t.race
                    (idle e.idle) (owner e.owner) (handin e.handin) (handout e.handout) (wait e.wait)>;

  (s.A e.A) (obj_trans e.busy) t.race
            (idle e.idle) (owner e.owner) (handin e.handin) (handout e.handout) (wait e.wait) = 
         <Loop1 (e.A) 
         <trans s.A (obj_trans e.busy) t.race
         (idle e.idle) (owner e.owner) (handin e.handin) (handout e.handout) (wait e.wait)>>;
}

Result3 {
 (obj_trans e.busy) t.race
 (idle e.idle) (owner s.1 s.2 e.owner) (handin e.handin) (handout e.handout) (wait e.wait) = False; 
 (obj_trans e.busy) t.race
 (idle e.idle) (owner e.owner) (handin e.handin) (handout s.1 s.2 e.handout) (wait e.wait) = False; 
 (obj_trans e.busy) t.race
 (idle e.idle) (owner s.1 e.owner) (handin e.handin) (handout s.2 e.handout) (wait e.wait) = False; 

 (obj_trans e.busy) t.race
 (idle e.idle) (owner e.owner) (handin e.handin) (handout e.handout) (wait e.wait) = True; 
}