Skip to content

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))
Edited by erwan