CIF to Supremica transformer
The CIF to Supremica transformer can be used to transform CIF specifications to Supremica modules (*.wmod files). Supremica is a tool for synthesis of discrete event supervisors.
Starting the transformation
The transformation can be started in the following ways:
In Eclipse, right click a
.ciffile in the Project Explorer tab or Package Explorer tab and choose .In Eclipse, right click an open text editor for a
.ciffile and choose .Use the
cif2supremicatool in a ToolDef script. See the scripting documentation and tools overview page for details.Use the
cif2supremicacommand line tool.
Options
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
.ciffile extension is removed (if present), and a.wmodfile 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
.wmodextension (if present).Eliminate enumerations: Enable this option to eliminate enumerations and replace them with integers before 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.
Supported specifications
The CIF to Supremica transformer supports a subset of CIF specifications. The following restrictions apply:
Kindless/regular automata (without a supervisory kind) are not supported. Only
plant,requirement, andsupervisorautomata are supported.Events not declared as controllable or uncontrollable are not supported. This includes the
tauevent, both explicitly used on edges, as well as implicitly for edges without explicitly mentioned events.Initialization predicates outside of locations are not supported.
Marker predicates outside of locations are only supported if they have the form
discrete_variable = marked_value.Discrete variables with multiple marker predicates are not supported.
Locations with initialization or marker predicates that are not trivially true or false are not supported.
Automata that do not have exactly one initial location are not supported.
State invariants in locations are not supported.
State invariants are only supported if they are requirement invariants.
Kindless/regular state/event exclusion invariants (without a supervisory kind) are not supported. Only
plant,requirement, andsupervisorstate/event exclusion invariants are supported.Discrete variables that have multiple potential initial values (
in {...}orin any) are not supported.Continuous variables are not supported.
Input variables are currently unsupported.
Multi-assignments on edges (such as
do (x, y) := (1, 2)) are not supported. However, it is allowed to use multiple assignments on an edge (such asdo x := 1, y := 2).Partial variable assignments (such as
do x[0] := 5) are not supported.Conditional updates on edges (such as
do if b: x := 5 end) are not supported.Urgent locations and urgent edges are not supported.
User-defined functions are not supported.
Channels (events with data types) are not supported.
Only the following data types are supported: boolean types, ranged integer types, and enumeration types.
Only the following expressions are supported: boolean literal values, integer literal values, binary expressions (partially, see below), unary expressions (partially, see below), and references to constants, discrete variables, enumeration literals, and casts that don’t change the type.
Only the following binary operators are supported: logical equivalence (
<=>), logical implication (=>), conjunction (and) on boolean operands, disjunction (or) on boolean operands, addition (+) on ranged integer operands, subtraction (-) on ranged integer operands, multiplication (*) on ranged integer operands, integer division (div) on ranged integer operands, integer modulus (mod) on ranged integer operands, equality (=), inequality (!=), less than (<) on ranged integer operands, less than or equal to (<=) on ranged integer operands, greater than (>) on ranged integer operands, and greater than or equal to (>=) on ranged integer operands.Only the following unary operators are supported: logical inverse (
not), negation (-) on a ranged integer operand, and plus (+) on a ranged integer operand.I/O declarations are ignored. A warning is printed if a CIF/SVG input declaration is encountered.
Annotations are ignored.
Preprocessing
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:
Convert enumerations to integers (if enabled via the corresponding option)
Transformation result
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.
Initialization
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.
Marking
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.
State invariants
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.
Alphabets
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.
Range semantics
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.
Jumping semantics
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;
endThere 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;
endUsers 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.