RULE_SET Transition vars p, p1, p2, q, q1, q2 : process a,b : action m, s, i, o : signal l : relabeling list r : strl_relation rules error_1 -------- ?? -- tau --> ?? nothing_1 -------- nothing -- exit_ --> nothing halt_1 -------- halt -- tau --> halt stop_1 -------- stop -- tau --> nothing emit_1 -------- emit o -- o!.exit_ --> nothing await_1 -------- await(i) -- i? --> nothing await_2 -------- await(i) -- i# --> await(i) present_1 p1 -- a --> q , not i# divides a -------- present i then p1 else p2 end -- i?.a --> q present_2 p2 -- a --> q , not i? divides a -------- present s then p1 else p2 end -- i#.a --> q watching_immediate_1 p2 -- a --> q , isterminal a -------- watching immediate p2 do p1 end -- a --> nothing watching_immediate_2 p1 -- a --> q1 , p2 -- b --> q2 , isnotterminal b % isnotterminal is true less often than (not isterminal) -------- watching immediate p2 do p1 end -- a.b --> watching immediate q2 do q1 end watching_1 p1 -- a --> q1 -------- watching p2 do p1 end -- a --> watching immediate p2 do q1 end sequence_1 p1 -- a --> q , not (isnotterminal a) -------- p1 >> p2 -- a --> q >> p2 sequence_2 p1 -- a --> q1 , p2 -- b --> q2 , isterminal a , a compatible b -------- p1 >> p2 -- a.b --> q2 parallel_1 p1 -- a --> q1 , p2 -- b --> q2 , a compatible b -------- p1 // p2 -- a.b --> q1 // q2 local_signal_1 p1 -- a --> q1 , a restriction s -------- localsignal s in p1 end -- a hiding s --> localsignal s in q1 end renaming_1 p1 -- a --> q -------- p1[l] -- a --> q[l] simplrel_1 p1 -- a --> p , check r in a end -------- simpl r in p1 -- simplAct r in a --> simpl r in p complrel_1 p1 -- a --> p , check r in a end -------- compl r in p1 -- complAct r in a --> compl r in p end RULE_SET Sort vars p, p1, p2, q, q1, q2 : process a,b : action m, s, i, o : signal s1, s2 : signal set l : relabeling list r : strl_relation rules error_sort -------- sort(??, {}) nothing_sort -------- sort(nothing, {exit_}) halt_sort -------- sort(halt, {}) stop_sort -------- sort(stop, {}) await_sort -------- sort(await i, {i}) emit_sort -------- sort(emit o, {o}) present_sort sort(p1, s1) , sort(p2, s2) -------- sort(present i then p1 else p2 end, ({i} U s1 U s2)) watching_immediate_sort sort(p1, s1) , sort (p2, s2) -------- sort(watching immediate p2 do p1 end, ({exit_} U s1 U s2)) watching_sort sort(p1, s1) , sort (p2, s2) -------- sort(watching p2 do p1 end, ({exit_} U s1 U s2)) sequence_sort_1 sort(p1, s1) , exit_ notin s1 -------- sort(p1 >> p2, s1) sequence_sort_2 sort(p1,s1) , sort(p2, s2) , exit_ member s1 -------- sort (p1 >> p2, (s1 diff exit_) U s2) parallel_sort_1 sort(p1, s1) , sort(p2, s2) , exit_ member (s1^s2) -------- sort(p1 // p2, s1 U s2) parallel_sort_2 sort(p1, s1) , sort(p2, s2) , exit_ notin (s1^s2) -------- sort(p1 // p2, (s1 U s2) diff exit_) local_signal_sort sort (p1, s1) -------- sort(localsignal s in p1 end, s1 hidesig s) renaming_sort sort (p1, s1) -------- sort(p[l], s1 rename l) simplrel_sort sort(p1, s1) -------- sort(simpl r in p1, s1 U relsort r) complrel_sort sort(p1, s1) -------- sort(compl r in p1, s1 U relsort r) end RULE_SET Halting vars p, p1, p2, q, q1, q2 : process a,b : action m, s, i, o : signal l : relabeling list r : strl_relation rules halt_halting -------- halt V stop_halting -------- stop V await_halting -------- await i V present_halting p1 V , p2 V -------- present i then p1 else p2 end V watching_immediate_halting p1 V -------- watching immediate p2 do p1 end V watching_halting -------- watching p2 do p1 end V sequence_halting p1 V -------- p1 >>p2 V parallel_halting_ p1 V , p2 V -------- p1 // p2 V local_signal_halting p V -------- localsignal s in p end V renaming_halting p V -------- p[l] V simplrel_halting p1 V -------- simpl r in p1 V complrel_halting p1 V -------- compl r in p1 V end