Requirement invariants are incorrectly transformed into plants by 'eliminate state invariants' CIF to CIF transformation
Currently, the CIF to CIF transformation to eliminate state invariants transforms state-based requirements into plant automata. This change from requirement to plant is incorrect with respect to the synthesis problem being solved.
A master student found this bug and created a minimal working example Minimal example wrong transformation.cif. For this model, synthesis results in an empty supervisor. But after transforming this using elim-state-invs into Minimal example wrong transformation.transformed.cif, synthesis obtains a supervisor with 3 states (i.e., no longer the empty supervisor).
Possible solutions:
-
Disallow requirements in the transformation. (!1403 (merged)) -
Support requirements in the transformation.
We could start with the 1st, while we think about the 2nd.