CIF 3
The CIF to Supremica transformer can be used to transform CIF 3 specifications to Supremica modules (*.wmod files). Supremica is a tool for synthesis of discrete event supervisors.
The transformation can be started in the following ways:
Besides the general application options, this application has the following options:
Input file path: The absolute or relative local file system path to the input CIF specification.
Output file path: The absolute or relative local file system path to the output Supremica module file. If not specified, defaults to the input file path, where the .cif file extension is removed (if present), and a .wmod file extension is added.
Supremica module name: The name of the Supremica module. If not specified, defaults to the name of the output file, after removal of the .wmod extension (if present).
Eliminate enumerations: Enable this option to eliminate enumerations before generating transforming to Supremica. Disable this option to keep enumerations in the generated Supremica module. By default this option is disabled.
Even though Supremica supports enumerations in its language, it doesn’t support them in all its algorithms. Even if the original CIF transformation being transformed does not use enumerations, enumerations may still be generated internally during preprocessing.
The CIF to Supremica transformer supports a subset of CIF specifications. The following restrictions apply:
The following CIF to CIF transformations are applied as preprocessing (in the given order), to increase the subset of CIF specifications that can be transformed:
The CIF automata kinds plant, requirement, and supervisor are mapped to Supremica kinds Plant, Specification, and Supervisor, respectively.
All generated Supremica automata are tagged as non-deterministic, as CIF automata may be non-deterministic.
Nameless CIF locations are given the name X in Supremica automata.
Supremica does not support boolean values. Instead of true, value 1 is used, and instead of false, value 0 is used. For boolean types (bool), ranged integer types (int[0..1]) are used.
The absolute names of all CIF objects (automata, variables, etc) are used, where the . characters are replaced by : characters. For enumeration literals, the non-absolute name of the enumeration literal is used, prefixed with :lit:.
No geometry is generated. When the generated Supremica file is opened in Supremica, Supremica will perform auto layouting.
For the initial values of the variables, initialization predicates are generated (e.g. x == 3). Earlier versions of Supremica that support variables allowed deterministic initialization (only the initial value), and non-deterministic initialization (initialization predicates). The most recent version only allows non-deterministic initialization, which is why we generate initialization predicates.
In CIF, if none of the locations of an automaton are indicated as marked, the automaton has no marked locations. In Supremica, if none of the locations of an automaton are indicated as marked (:accepting), all locations of the automaton are implicitly marked. When transforming a CIF automaton without any marked locations, a warning is printed to the console to inform the user of this difference.
In CIF, if none of the values of a variable is indicated as marked, the variable has no marked values. In Supremica, if none of the values of a variable is indicated as marked (:accepting), all values of the variable are implicitly marked. When transforming a CIF variable without any marked values, a warning is printed to the console to inform the user of this difference.
Location pointer variables that are automatically generated, such as the ones generated by the Eliminate the use of locations in expressions CIF to CIF transformation, have no marking and thus lead to warnings.
If the CIF model being transformed contains state invariants, an uncontrollable u_inv_bad event is added to the Supremica module. It is renamed if the name is not unique. A plant automaton named inv_plant (renamed if not unique) is added as well. This plant enables the u_inv_bad event if and only if at least one of the invariants doesn’t hold. A requirement automaton inv_req (renamed if not unique) is added as well. The requirement disables the event globally. Since blocking an uncontrollable plant event in a requirement is forbidden, synthesis will prevent such blockage (by disabling controllable events), thereby ensuring that the state invariants hold after synthesis.
In CIF, it is possible to explicitly specify the alphabet of an automaton. This alphabet may include more events than occur on the edges of the automaton, thereby globally disabling those additional events. Supremica automatically determines the alphabet automatically, based on the events that occur on the edges of the automaton, just like CIF does if no explicit alphabet is specified. If a CIF automaton with ‘additional’ events is transformed, a self loop is added to the initial state for each ‘additional’ event, with a false guard (0 in Supremica). This ensures that the event occurs on an edge, and is thus part of the alphabet, but is not enabled.
In CIF, if an update of an edge results in out of range values of variables, the CIF specification is considered invalid, and the simulation will result in a runtime error. In Supremica, the simulation does not result in a runtime error, but instead the offending transition is disabled/forbidden.
Consider the following CIF model:
plant automaton p: controllable c_event; disc int[0..3] v = 0; location loc1: initial; marked; edge c_event do v := v + 1 goto loc2; location loc2: edge c_event goto loc1; end
There are two locations, and the edges allow for moving from one location to the other. Both edges use the same event. Every odd transition (the first transition, the third transition, etc), the value of variable v is increased by one. Every even transition, the value of variable v is not changed. After a few transitions, the simulation crashes due to overflow of variable v.
To ensure the same semantics in Supremica, such that for every even transition the value of variable v does not change, the CIF model is modified by the transformation, to the following:
plant automaton p: controllable c_event; disc int[0..3] v = 0; location loc1: initial; marked; edge c_event do v := v + 1 goto loc2; location loc2: edge c_event do v := v goto loc1; end
Users of the transformation don’t have to do anything themselves, as the tool automatically adds the dummy assignments as needed. If the tool would not have added such dummy assignments, then the value of variable v would have been able to jump to any value (in its range [0..3]) for every even transition, according to the Supremica semantics.