Supported specifications

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

Specifications with component definitions/instantiations are not natively supported by the CIF 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, input variables, and discrete variables with multiple possible initial values (including any) are not supported, unless additional initialization is provided.

Input variables are in principle simulated as having a constant value. The only way for them to change value, is by having SVG input mappings update them. Alternatively, input variables may first be merged with other variables that provide their values.

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.

Annotations are ignored.