CIF to Supremica transformer | CIF documentation

Starting the transformation

The transformation can be started in the following ways:

In Eclipse, right click a .cif file in the Project Explorer tab or Package Explorer tab and choose CIF synthesis tools Convert CIF to Supremica….
In Eclipse, right click an open text editor for a .cif file and choose CIF synthesis tools Convert CIF to Supremica….
Use the cif2supremica tool in a ToolDef script. See the scripting documentation and tools overview page for details.
Use the cif2supremica command 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 .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 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, and supervisor automata are supported.
Events not declared as controllable or uncontrollable are not supported. This includes the tau event, 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, and supervisor state/event exclusion invariants are supported.
Discrete variables that have multiple potential initial values (in {...} or in 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 as do 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:

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;
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.