Skip to content

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.

Edited by Dennis Hendriks