GitLab

This CIF to CIF transformation removes requirement invariants and requirement automata from a specification. It is used by databased synthesis to post-process the resulting specification.

For requirement automata, everything declared inside them is removed, except for kindless, plant, and supervisor invariants. Those are moved to the parent component. If from the outside a declaration inside the automaton is referenced, the transformation fails. However, the following question remains:

What about removing initialization predicates, marker predicates in requirement automata, that really restrict or apply to the plant? Probably somewhat difficult to detect in a robust way? What to do with that? Maybe there are similar things that could break?