CIF 3

Supported specificationsΒΆ

The CIF 3 simulator supports a subset of CIF specifications. The following restrictions apply:

Specifications with component definitions/instantiations are not natively supported by the CIF 3 simulator. Therefore, they are automatically eliminated by the simulator, as a preprocessing step, using the CIF to CIF transformation to eliminate component definition/instantiation.

Automata with multiple possible initial locations and discrete variables with multiple possible initial values (including any) are not supported, unless additional initialization is provided.

The controllability of events is ignored by the simulator, as are marker predicates.

All automata are simulated as plants. That is, all automaton kinds are ignored by the simulator. However, simulating requirements as plants may lead to unexpected results. Therefore, the simulator prints warnings to the console, whenever requirements are simulated. It is highly recommended to first apply supervisor synthesis to the specification, and simulate the resulting specification using the simulator. Alternatively, apply verification to the specification, remove the verified requirements, and simulate the resulting specification using the simulator.

Similar to requirement automata, the simulator warns about simulation of requirement invariants.