CIF to UPPAAL transformer
The CIF to UPPAAL transformer can be used to transform CIF specifications to UPPAAL systems (*.xml
files). UPPAAL is a tool modeling, validation, and verification of networks of timed automata with variables. The transformer only transforms untimed CIF specifications.
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 . 
In Eclipse, right click an open text editor for a
.cif
file and choose . 
Use the
cif2uppaal
tool in a ToolDef script. See the scripting documentation and tools overview page for details. 
Use the
cif2uppaal
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 UPPAAL file. If not specified, defaults to the input file path, where the
.cif
file extension is removed (if present), and a.xml
file extension is added.
Supported specifications
The CIF to UPPAAL transformer supports a subset of CIF specifications. The following restrictions apply:

Specifications without automata are not supported.

Channels (events with data types) are not supported.

Initialization predicates in components are not supported.

Automata that do not have exactly one initial location are not supported.

Locations with initialization predicates that are too complex to evaluate statically, are not supported. That is, those predicates must essentially be constant. For instance,
true
andtrue or false
are supported, as isc
ifc
is a constant. However,v => c
withv
a discrete variable that can initially have several different values, is not supported. 
Discrete variables with multiple potential initial values are not supported.

Discrete variables with initial values that are too complex to evaluate statically, are not supported. That is, their initial values must essentially be constant. For instance,
1 + 1
and2 * 5
are supported, as isc + 1
ifc
is a constant. However,v * 2
withv
a discrete variable that can initially have several different values, is not supported. 
Continuous variables are not supported.

Input variables are not supported.

Userdefined functions are not supported.

Urgent edges are not supported.

Multiassignments 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 (
if
updates) on edges (such asdo if b: x := 5 end
) are not supported. 
Only the following data types are supported: boolean, integer (both with a range and without a range), and enumeration types.

Only the following expressions are supported: boolean literal values (
true
andfalse
), integer literal values, enumeration literal values, binary expressions (partially, see below), unary expressions (partially, see below), casts that don’t change the type,if
expressions, and references to constants, discrete variables, algebraic variables, and locations. 
Only the following binary operators are supported: logical equivalence (
<=>
), logical implication (=>
), logical conjunction (and
on boolean operands), logical disjunction (or
on boolean operands), addition (+
) on integer operands, subtraction (
) on integer operands, multiplication (*
) on integer operands, integer division (div
), integer modulus (mod
), equality (=
) on integer and enumeration operands, inequality (!=
) on integer and enumeration operands, less than (<
) on integer operands, less than or equal to (<=
) on integer operands, greater than (>
) on integer operands, and greater than or equal to (>=
) on integer operands. 
Only the following unary operators are supported: logical inverse (
not
), negation (
) on an integer operand, and plus (+
) on an integer operand. 
The controllability of events is ignored.

The supervisory kinds of automata are ignored.

The supervisory kinds of invariants are ignored.

Marker predicates are ignored.

I/O declarations are ignored. A warning is printed if a CIF/SVG input declaration is encountered.
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
CIF features synchronizing events, while UPPAAL only supports channels. A SendAut
automaton/template is added to the UPPAAL system to ensure proper event synchronization. The UPPAAL template has a single location, and self loops for every event in the CIF specification. The guards of the self loops express the conditions (from edge guards and state/event exclusion invariants) under which the events are globally enabled (guard wise) in the CIF specification. Every CIF event is a broadcast channel in UPPAAL. If the self loop is enabled (guard wise), the SendAut
template broadcasts over the channel. All the other templates (for the CIF automata) receive the event. They can actually receive, as the guard of the self loop ensures that. Together the SendAut
self loops and the receive edges form the synchronization.
As the SendAut
template needs to refer to locations of the other templates, location pointer variables are added for all the other templates. For every CIF automaton some.aut
, a location pointer variable LP_some_aut
is added. The location pointers are integer variables with range [0,n1]
, for an automaton with n
locations. Updates are added to the edges to ensure the location pointer variables have the proper values. The location pointers are similar to those created by the CIF to CIF transformation that eliminates the use of locations in expressions.
In CIF, assignments interpret the right hand side of the assignment (the new value of the variable) in the source state of the transition. In UPPAAL, assignments have order, and the right hand sides are interpreted over the current state, after any preceding assignments. Furthermore, the order in which the assignments of the edges of different participating templates are executed is not defined. To ensure the proper CIF semantics, 'old' versions of all variables (including the location pointer variables) are added. For a variable x
, OLD_x
is added. The SendAut
automaton assigns the current values of all variables to their 'old' counterparts. The assignments on the edges of the other automata then use the 'old' variables to compute the new values of the variables. As the values of the 'old' variables are only used during the transitions, the 'old' variables are meta variables in the UPPAAL system.
The state invariants from CIF components are added to the location of the SendAut
template.
For CIF variables with an int
type, the UPPAAL type is int[2147483648,2147483647]
.
The names of templates, variables, etc in UPPAAL are based on the absolute names of their CIF counterparts. For a variable a.b.c
in CIF, the UPPAAL name is a_b_c
. If there are conflicts between the UPPAAL names, or if one of the UPPAAL names conflicts with a UPPAAL keyword, renaming is performed, and a warning is printed to the console.
No geometry is generated. When the generated UPPAAL file is opened in UPPAAL, UPPAAL will perform some layouting.