The generated synchronous Lutin demon is wrong
Indeed, sasa -gld generates something like that
loop
(Enab_p1_a = p1_a) and (Enab_p1_b = p1_b) and (Enab_p1_c = p1_c) and
(Enab_p2_a = p2_a) and (Enab_p2_b = p2_b) and (Enab_p2_c = p2_c) and
(Enab_p3_a = p3_a) and (Enab_p3_b = p3_b) and (Enab_p3_c = p3_c) and
(Enab_p4_a = p4_a) and (Enab_p4_b = p4_b) and (Enab_p4_c = p4_c)
whereas exactly one rule should be activated an the same step in the same algo
loop
(xor(Enab_p1_a = p1_a, Enab_p1_b = p1_b, Enab_p1_c = p1_c)) and
(xor(Enab_p2_a = p2_a, Enab_p2_b = p2_b, Enab_p2_c = p2_c)) and
(xor(Enab_p3_a = p3_a, Enab_p3_b = p3_b, Enab_p3_c = p3_c)) and
(xor(Enab_p4_a = p4_a, Enab_p4_b = p4_b, Enab_p4_c = p4_c))