Event-based synthesis analysis tool has wrong conclusion
Consider plant G
and requirement H
, as shown below. The synchronous product has 10 states. The synthesized supervisor has 6 states (also shown below).
Yet, the synthesis analysis tool shows the following message:
Synthesis analysis tool
1 plant automaton.
1 requirement automaton.
Synthesis created 10 states, removed 2 states, giving 8 states in the result.
It incorrectly states that 2 states were removed and 8 states remain. In reality, 4 states were removed, and 6 remained.
plant G:
location G0: initial;
edge a1 goto G1;
edge a2 goto G3;
location G1:
edge b1 goto G2;
edge a2 goto G4;
location G2:
edge a2 goto G5;
location G3:
edge a1 goto G4;
edge b2 goto G6;
location G4:
edge b1 goto G5;
edge b2 goto G7;
location G5:
edge b2 goto G8;
location G6:
edge a1 goto G7;
location G7:
edge b1 goto G8;
location G8: marked;
end
requirement H:
location H0: initial;
edge a1 goto H1;
edge a2 goto H3;
location H1:
edge b1 goto H2;
edge a2 goto H9;
location H2:
edge a2 goto H5;
location H3:
edge a1 goto H4;
edge b2 goto H6;
location H4:
edge b2 goto H7;
location H9:
edge b1 goto H5;
location H5:
edge b2 goto H8;
location H6:
edge a1 goto H7;
location H7:
edge b1 goto H8;
location H8: marked;
end
controllable a1;
uncontrollable a2;
controllable b1;
uncontrollable b2;
supervisor automaton S:
alphabet a1, a2, b1, b2;
location s1:
initial;
edge a2 goto s2;
location s2:
edge b2 goto s3;
edge a1 goto s4;
location s3:
edge a1 goto s5;
location s4:
edge b2 goto s5;
location s5:
edge b1 goto s6;
location s6:
marked;
end