Consider warning for /disallowing plant referencing requirements in CIF
In CIF, we can reference variables from requirement automata in plant automata and plant invariants. We support this for data-based synthesis.
The problem is that it doesn't really fit with the theory. A plant model should be independent of the requirements.
@ddennis noted:
I do think it makes sense to forbid using requirement things in plant things, as precondition check for the data-based synthesis tool. It is conceptually as a plant is just there and requirements restrict it. Physically the requirements are not there in the system, so defining the plant in terms of requirements doesn't fit the concepts. An observer of the plant for instance should be a plant automaton and not a requirement, since it doesn't actually impose restrictions. This precondition check would mean checking all plant guards, plant invariants, etc for references to requirement state (disc vars, locations, etc).
Some thing to consider:
- Forbidding it is backward incompatible, do we want that. Alternatively, we could generate a warning.
- Do we want it to be part of the data-based synthesis tool or the type checker?