RULE_SET functionality

vars
	p, q, p', q' : process
	a, b : action
	f : funct
	S : action set

rules
prefix_f
  ---------- 
  stop -: noexit

hide_f
  p -: f 
  ---------- 
  hide S in p -: f

exit_f
  ----------
   exit -: yesexit

prefixing_f
  p -: f ----------
   a;p -: f

end

RULE_SET transitions

vars
	p, q, p', q': process
	a, b: action
	S, G: action set

rules
% Stop has no rules

% Exit:
exit_tr
   ----------
   exit -- delta --> stop

% Prefixing:
prefix_tr
   ----------
   a;p -- a --> p

% Hiding:
hiding_i
    p -- a --> p'  ,  a member S
    ----------
    hide S in p -- i --> hide S in p'

hiding_act
    p -- a --> p'  ,  not (a member S)
    ----------
    hide S in p -- a --> hide S in p'

% Choice:
choice_left
  p -- a --> p'
  ----------
  p [] q -- a --> p'

choice_right
  q -- a --> q'
  ----------
  p [] q -- a --> q'

% Parallel (full synchronization):
parallel_all
  p -- a -->p'  ,  q -- b -->q'  ,  (b equal a)
  ----------
  p || q -- a --> p' || q'

% Rendez-vous (synchronization on a gate set)
% Note that Interleave is p // {} // q

rdv_left
  p -- a -->p'  ,  (not(a member G)) and (not (a equal delta))
  ----------
  p // G // q -- a --> p' // G // q

rdv_right
  q -- a -->q'  ,  (not(a member G)) and (not (a equal delta))
  ----------
  p // G // q -- a --> p // G // q'

rdv_synch
  p -- a -->p'  ,  q -- b --> q' , ((a member G) and (a equal b))
  ----------
  p // G // q -- a --> p' // G // q'

rdv_delta
  p -- a -->p'  ,  q -- b --> q' , ((a equal delta) and (b equal delta))
  ----------
  p // G // q -- delta --> p' // G // q'

% Disable:
disable_left
  p -- a -->p'  ,  (not (a equal delta))
  ----------
  p [> q -- a --> p' [> q 

disable_delta
  p -- a -->p'  ,  (a equal delta)
  ----------
  p [> q -- a --> p'

disable_right
  q -- a --> q'
  ----------
  p [> q -- a --> q'

% Enable:
enable_left
  p -- a -->p'  ,  (not (a equal delta))
  ----------
  p >> q -- a --> p' >> q 

disable_delta
  p -- a -->p'  ,  (a equal delta)
  ----------
  p >> q -- i --> q

end