RULE_SET transitions

vars
  
  a , b : act
  p , p' , p1 , p1' , p2 , p2' : agent
  s : id_set
  r, r1, r2 : relabeling
  ae : (agent env)
  se : (id_set env)
  A : id
  s_id : id
  ag_frame : (agent frame)
  aut, aut' : automaton

rules

prefix

 --------------------------
  ae, se : a.p -- a --> p

sum_1

     ae, se : p1 -- a --> p1'
 -------------------------------
  ae, se : p1 + p2 -- a --> p1'

sum_2

     ae, se : p2 -- a --> p2'
 -------------------------------
  ae, se : p1 + p2 -- a --> p2'

parallel_1

        ae, se : p1 -- a --> p1' 
 ------------------------------------
  ae, se : p1 | p2 -- a --> p1' | p2

parallel_2

       ae, se : p2 -- a --> p2' 
 ------------------------------------
  ae, se : p1 | p2 -- a --> p1 | p2'

parallel_3

  ae, se : p1 -- a --> p1' , ae, se : p2 -- b --> p2', inverses(a,b)
 ---------------------------------------------------------------------
               ae, se : p1 | p2 -- t --> p1' | p2'

relabel1

    ae, se : p[compose(r1 : r2)] -- a --> p'
  -------------------------------------------
       ae, se : p[r1][r2] -- a --> p'

relabel2

           ae, se : p -- a --> p' 
 ------------------------------------------
    ae, se : p[r] -- apply(a,r) --> p'[r]

restrict_1

     ae, se : p -- a --> p', not (labelof(a) in s)
 --------------------------------------------------
            ae, se : p\s -- a --> p'\s   

restrict_2

     ae, se : p -- a --> p', not (labelof(a) in lookup(s_id,se))
 ------------------------------------------------------------------
                ae, se : p\s_id -- a --> p'\s_id

aut_rule

        aut - a -> aut'
 ------------------------------
   ae, se : aut -- a --> aut'

process_constant

   ae, se : lookup(A,ae) -- a --> p'
 ------------------------------------
       ae, se : A -- a --> p'

fixpoint

           push_frame(ag_frame,ae), se : p -- a --> p'
 ---------------------------------------------------------------
   ae, se : p where ag_frame end -- a --> p' where ag_frame end

end

RULE_SET diverges

vars

  a : act
  ae : (agent env)
  se : (id_set env)
  A : id
  p, p1, p2 : agent
  r : restriction
  rel : relabeling
  ag_frame : (agent frame)
  
rules

bottom

 ---------------------
   ae, se : @ ^

var

   ae, se : lookup(A,ae) ^
 ---------------------------
     ae, se : A ^

sum_1

      ae, se : p1 ^ 
 ------------------------
   ae, se : (p1 + p2) ^

sum_2

     ae, se : p2 ^ 
 -----------------------
  ae, se : (p1 + p2) ^

par_1 

      ae, se : p1 ^ 
 -----------------------
  ae, se : (p1 | p2) ^

par_2 

      ae, se : p2 ^ 
 -----------------------
  ae, se : (p1 | p2) ^

restrict

     ae, se : p ^
 --------------------
   ae, se : p \ r ^

relabel

     ae, se : p ^
 ---------------------
   ae, se : p[rel] ^

fixpoint

   push_frame(ag_frame,ae), se : p ^
 ------------------------------------------
    ae, se : p where ag_frame end ^

end