CIF 3

Model migration for backward incompatible language changes

Sometimes new features are introduced to the language that break existing CIF 3 models. This page explains how to upgrade the existing models to the new situation. This page only describes backward incompatible language changes. The changes are listed in reverse chronological order.

2015-09-11 Removal of using events as variables/values in invariants

The use of events as variables/values in invariants has been removed. The following is no longer a valid:

event evt;
invariant evt => true;

This syntax was a remnant of earlier CIF versions, and none of the CIF 3 tools support models with this kind of invariants. Removing it should not affect any practical CIF models that are in use. This kind of invariants has been superseded by state/event exclusion invariants.

2015-09-11 Introduction of state/event exclusion invariants

With the introduction of state/event exclusion invariants, the needs and disables keywords have been introduced in the textual syntax. Older models using these names (for instance for variables), will become invalid. There are two solutions. The first solution is to rename the variables. The second is to escape the names by changing them to $needs and $disables respectively, ensuring they are interpreted as identifiers/names instead of keywords.

2015-09-11 Deprecation of invariant kind inheritance

Consider the following CIF specification:

plant lamp:
  invariant 1 = 2;          // Inherits 'plant' kind from automaton.
  plant invariant 1 = 2;    // Explicit plant invariant.

  location:
    initial;
end

The first invariant has no explicit supervisory kind specified, and therefore inherits the plant kind from the automaton. It is thus an invariant that is implicitly a plant invariant. Such kind inheritance is now deprecated, and results in a warning.

To get rid of the warning, simplify specify the supervisory kind explicitly. The second invariant above is identical, except for the explicit specification of the plant kind. It is also a plant invariant, but due to the explicit kind specification, there is no warning.

While kind inheritance is now deprecated and gives a warning, it still works as before. That is, the semantics of kind inheritance have not changed. For more information, see the section on invariant kinds as part of the language tutorial.

2014-11-10 Enumerations

Previously, enumerations with the same number of literals in different orders were compatible. That is, the following CIF specification used to be valid:

automaton x:
  enum E = {A, B};
  disc E v;

  location:
    initial;
    edge do v := y.v;
end

automaton y:
  enum E = {B, A};
  disc E v;

  location:
    initial;
    edge do v := x.v;
end

Both automaton x and automaton y have an enumeration E with two literals A and B. However, the orders of the literals differ. They also both have a variable v that has as type the enumeration from its own automaton. The edges assign the value of the variable from the other automaton to the variable of the automaton itself. This used to be allowed, as both enumerations were considered compatible (had the same number of literals, with the same names, in any order).

One of the problems is that variable v of automaton x has initial value A, while variable v of automaton y has initial value B, as the default value of an enumeration is its first literal. This leads to complications for transformations, where a representative needs to be used for compatible enumerations, or the default value of variables needs to be made explicit. The default initial value can be quite large, leading to even more problems.

To solve these issues, enumerations are now only compatible if they have the same number of literals, with the same names, in the same order. That is, the order is now relevant. As the literals are no longer unordered, notation for declaring the literals of an enumeration is changed:

enum E = A, B;

That is, the { and } brackets are no longer written around the literals. For backward compatibility, the brackets may optionally still be written. It is highly recommended to omit them in new CIF specifications, as the old syntax may be removed in the future.

The change that type compatibility of enumerations takes the order of the literals into account is a backward incompatible language change. We expect very few existing specifications to be affected by this change. To make the existing specifications valid again, change the order of the literals to be the same for all previously compatible enumerations that are now no longer compatible, and update the default values of variables accordingly, if needed.

Due the brackets syntax change, it is no longer possible to declare multiple enumerations without repeating the enum keyword. This is a backward incompatible syntax change. We also expect very few existing specifications to be affected by this change. Existing models can be easily rewritten, by prefixing each enumeration declaration by an enum keyword, making sure it ends with a semicolon (;), and (preferably) removing the curly brackets:

// Old syntax.
enum A = {B, C},
     D = {E, F};

// New syntax (allowed for backward compatibility).
enum A = {B, C};
enum D = {E, F};

// New syntax (preferred).
enum A = B, C;
enum D = E, F;

2014-10-02 Empty lists and arrays

With the addition of arrays, list literals have an array type (list type with a fixed length), rather than a regular list type (of arbitrary length). This applies to empty lists as well. If the type of an empty list can’t be determined from the context, a cast must be added to help the type checker. This cast must now use an array type. For instance, the following is no longer valid:

<list real>[];

It can be replaced by the following:

<list[0] real>[];

The type checker is smart enough to determine the type of empty lists in most cases. This language change should therefore affect very few existing specifications.

2014-04-28 Empty lists, sets, and dictionaries

This release has improved type checking, allowing the type of empty lists, sets and dictionaries to be derived from their context. Due to these changes, it is no longer allowed to specify the element type of an empty list or set, or the key and value types of an empty dictionary. Instead, if the type checker can’t derive the type, it is now allowed to cast to the type of the entire empty container.

For instance, the following is no longer valid:

automaton a:
  disc list int      x1;
  disc set  int      x2;
  disc dict(int:int) x3;

  location loc:
    initial;
    edge do x1 := <int>[], x2 := <int>{}, x3 := <int:int>{};
end

Instead, the types can now be automatically derived:

automaton a:
  disc list int      x1;
  disc set  int      x2;
  disc dict(int:int) x3;

  location loc:
    initial;
    edge do x1 := [], x2 := {}, x3 := {};
end

Or they can now be explicitly specified using a cast:

automaton a:
  disc list int      x1;
  disc set  int      x2;
  disc dict(int:int) x3;

  location loc:
    initial;
    edge do x1 := <list int>[], x2 := <set int>{}, x3 := <dict(int:int)>{};
end

2014-04-14 CIF/SVG declaration changes

Previously, SVG output mappings had a body, with one or more values, and an optional pattern. The values could optionally have a value transformation. Formatted text (pattern "...";) and value transformations however, are also useful in other contexts, such as for print output. Therefore, we have moved several concepts from SVG output mappings to expressions, making them more generally available.

Furthermore, SVG output mappings had a block-like syntax, spanning multiple lines. To reduce the number of lines needed for such declarations, especially the simpler ones, the syntax of all CIF/SVG declarations, has been changed to a single line syntax, similar to print declarations.

Concretely, for SVG copy declarations, SVG move declarations, SVG output mappings, and SVG input mappings, the local SVG file declaration is now no longer put in the body (svgfile "...";), but instead is part of the single line declaration (file "..."). For instance, consider the following:

// Old syntax.
svgcopy id "..." post "...":
  svgfile "some_file1.svg";
end

svgout id "..." attr "width":
  svgfile "some_file2.svg";
  value 5;
end

// New syntax.
svgcopy id "..." post "..." file "some_file1.svg";

svgout id "..." attr "width" value 5 file "some_file2.svg";

For copy and move declarations, that is the only change.

For SVG output mappings, the values and optional pattern of the body are replaced by a single value expression. For instance, consider the following:

// Old syntax.
svgout id "..." attr "transform":
  value 5;
  value 6;
  pattern "translate(%d, %d)";
end

// New syntax.
svgout id "..." attr "transform" value fmt("translate(%d, %d)", 5, 6);

The format pattern has been replaced by the use of the fmt standard library function, which can use multiple values to construct a textual value. For more information, see the text formatting tutorial.

It is no longer possible to use an automaton self reference as a value directly. Instead, automaton self references can now be cast to a string typed value, as a general expression. This still results in the name of current location of that automaton as text. For instance, consider the following:

// Old syntax.
automaton a:
  location loc:
    initial;

  svgout id "..." text:
    value self;
  end
end

// New syntax.
automaton a:
  location loc:
    initial;

  svgout id "..." text value <string>self;
end

Additionally, it is now also possible to refer to any other automaton, and cast it to a string value. For instance, consider the following:

group g:
  automaton a:
    location loc:
      initial;
  end
end

svgout id "..." text value <string>g.a;

Interval value transformations are replaced by the scale standard library function. For instance, consider the following:

// Old syntax.
svgout id "..." attr "...":
  value x:
    inmin 0;
    inmax max_x;
    outmin 15;
    outmax 30;
  end
end

// New syntax.
svgout id "..." attr "..." value scale(x, 0, max_x, 15, 30);

Value to value mappings have been replaced by switch expressions. For instance, consider the following:

// Old syntax.
svgout id "..." attr "...":
  value x:
    1    : "a";
    2    : "b";
    else : "c";
  end
end

// New syntax.
svgout id "..." attr "..."
  value switch x:
    case 1: "a"
    case 2: "b"
    else    "c"
  end;

The syntax of switch expressions is similar to the syntax of if expressions in many ways. To keep the two similar in functionality as well, the else is made mandatory for switch expressions. This is a small regression in functionality, as for value to value mappings the else was optional. We plan to make the else optional for both if and switch expressions in the future.

Location to value mappings have also been replaced by switch expressions. For instance, consider the following:

// Old syntax.
automaton a:
  location loc1;
  location loc2;

  svgout id "..." attr "...":
    value self:
      loc1 : "a";
      loc2 : "b";
    end
  end
end

// New syntax.
automaton a:
  location loc1;
  location loc2;

  svgout id "..." attr "..."
    value switch self:
      case loc1: "a"
      case loc2: "b"
    end;
end

This switch expression is similar to the switch expression of the previous example. For switch expressions over automata however, the else is optional, and the cases are checked for completeness over all the locations of the automaton. As such, there is no regression in functionality for location to value mappings. Similar to the automaton to string casts described above, switch expressions can now use automaton references as well as automaton self references.

For automata with two locations however, using an if expression rather than a switch expression is much more compact:

automaton a:
  location loc1;
  location loc2;

  svgout id "..." attr "..." value if loc1: "a" else "b" end;
end

An additional benefit of having the value transformations as expressions is that they can be combined. This was not possible for values previously, as only one transformation could be applied to them.

Besides the syntax of SVG output mappings, the syntax of SVG input mappings has changed a bit as well:

// Old syntax.
svgin id "...":
  some_event;
end

svgin id "...":
  x = 1 : some_event1;
  x = 2 : some_event2;
  else  : some_event3;
end

// New syntax.
svgin id "..." event some_event;

svgin id "..."
  event if   x = 1: some_event1
        elif x = 2: some_event2
        else        some_event3
        end;

The body has been replaced by the event keyword and a specification of what event is to be chosen. For a single event, the event name or reference is used. For multiple events, the mapping is replaced by an if expression. The syntax of this if expression is similar to the ‘normal’ if expressions, but the else is optional for SVG input mappings, and the result is an event rather than a value.

The documentation has been updated to reflect all changes. Consult the SVG visualizer and SVG input mode documentation for further information, updated examples, etc.

2014-03-24 Invariant kinds

Previously, invariants had no kind. For supervisor synthesis, different tools would interpret the invariants in different ways. That is, one tool would interpret an invariant as a requirement invariant, while another tool would interpret the same invariant as a plant invariant.

It is now possible to specify the kind of invariant, directly in a CIF specification. Invariants with an explicit kind (plant, requirement or supervisor) have that kind, wherever they are specified (in the specification, a group or group definition, an automaton or automaton definition, or in a location of an automaton). Invariants that don’t specify a kind, and are defined in an automaton (or one of its locations) with a kind that can be inherited (plant, requirement or supervisor) implicitly have the kind that they inherit from the automaton. Invariants that don’t specify a kind, and are defined in the specification, a group or group definition, or an automaton or automaton definition (or in one of their locations) with an automaton kind, don’t have a kind, neither implicit nor explicit.

For instance, consider the following CIF specification:

invariant p0;
plant invariant p1;
requirement invariant p2;

plant p:
  invariant p3;
  plant invariant p4;
  requirement invariant p5;

  location:
    initial;
end

automaton q:
  invariant p6;
  plant invariant p7;
  requirement invariant p8;

  location:
    initial;
end

group g:
  invariant p9;
  plant invariant p10;
  requirement invariant p11;
end

Invariants p1, p4, p7, and p10 are all explicitly plant invariants. Invariant p3 is a plant invariant as well, as it is specified in plant automaton p, and does not specify a kind of its own. Invariants p2, p5, p8, and p11 are all explicitly requirement invariants. Invariants p0, p6, and p9 don’t have a kind at all.

All tools now honor this new language concept, and thus treat invariants in a consistent manner.

2014-03-24 Edge syntax

Some issues have been identified relating to the syntax of edges. Edges can be difficult to read, especially if they are longer, and span multiple lines. It can also be difficult to see where one edge ends and another starts. Furthermore, edges are not clearly marked as being edges, and their syntax partly overlaps with event declarations.

To remedy these issues, the edge keyword is introduced. Every edge now starts with that keyword. Edges with an event no longer use the event keyword. The other keywords (when, now, do, and goto) are unchanged.

For instance, consider the following CIF fragment in the old syntax:

location loc1:
  initial;
  event e goto loc2;
  event f;
  when x = 2 goto loc2;
  do x := 3;

location loc2:
  event e when x = 3 do y := 5;
  event e when x = 4 do y := y + 1 goto loc1;

In the new syntax, this should be written as follows:

location loc1:
  initial;
  edge e goto loc2;
  edge f;
  edge when x = 2 goto loc2;
  edge do x := 3;

location loc2:
  edge e when x = 3 do y := 5;
  edge e when x = 4 do y := y + 1 goto loc1;

2013-12-10 CIF/SVG

Several problems with CIF/SVG Mappings files (.cifsvg files) were identified. The major problems were in reuse and scalability, as well as readability, traceability, and maintainability. Specifically, the CIF/SVG Mappings files were lacking a definition/instantiation mechanism, constants, algebraic variables, functions, etc. Also, using separate files meant switching between the CIF file and the mapping file, and keeping them consistent was not always easy. If a part of the CIF model changes, the entire mappings file needed to be copied, while only a part of the mappings needed to change.

To remedy all of these problems, the CIF/SVG Mappings language is no longer available as a separate language, but instead CIF/SVG declarations can now be sued as an extension to the CIF language. As such, we no longer have .cifsvg files. It is now possible to specify the mappings in a CIF file. We can then use CIF constants, algebraic variables, functions, etc. We can also use the definition/instantiation mechanism of CIF for the CIF/SVG declarations.

Since the mappings are now defined in CIF files, the ciffile declaration has become obsolete, and is no longer available. The svgfile declaration however, still exists. These declarations may now be declared in all components (including component definitions), and apply to the component and all its child components (recursively). SVG file declaration may now be overridden in child components, and locally in CIF/SVG mappings, allowing the use of multiple SVG images for a single CIF specification. This also makes it possible to merge CIF specifications that use different SVG images for their visualizations together into a single CIF specification, and simulate that merged CIF specification with multiple SVG visualizers.

SVG output mappings and SVG input mappings still exist, and have mostly the same syntax and functionality as before. The output and input keywords have been replaced by the svgout and svgin keywords respectively.

The SVG element ids are now specified using CIF expressions, making it possible to compute the id to use for a mapping, based on the values of for instance constants and algebraic parameters. For an example of this, see the updated documentation for the workstation example. This change also means that hard coded element ids now require double quotes around them, while this was previously optional. Perform the following steps to add double quotes around all the ids in your current mappings, and thus ease migration:

  • In Eclipse, click Search ‣ File... to open the Search dialog with the File Search tab active.
  • Make sure the Regular expression option is enabled, and the Case sensitive option is disabled.
  • For Containing text, enter id +([_a-zA-Z][_a-zA-Z0-9]*), and make sure there are no spaces at the beginning or the end.
  • For File name patterns, enter *.cifsvg.
  • For Scope select Workspace.
  • Click the Replace... button.
  • In the Replace Text Matches dialog that shows if any matches are found, make sure the Regular expression option is enabled.
  • For With, enter id "\1", and make sure there are no spaces at the beginning or the end.
  • Click OK to apply the replacement to all CIF/SVG Mapping files in your workspace, or click Preview to first check the result of those replacements before clicking OK to apply them.

Alternatively, to apply the changes for a single file:

  • In Eclipse, click Edit ‣ Find/Replace... to open the Find/Replace dialog.
  • Make sure the Regular expression option is enabled, and the Case sensitive option is disabled.
  • For Find, enter id +([_a-zA-Z][_a-zA-Z0-9]*), and make sure there are no spaces at the beginning or the end.
  • For Replace with, enter id "\1", and make sure there are no spaces at the beginning or the end.
  • Click Replace All to apply the replacement to the entire file.

For consistency, the SVG attribute names of CIF/SVG output mappings now also require double quotes around them, although expressions are not supported for attribute names. A similar replacement as for the SVG element ids can be employed, by replacing id with attr in the instructions above.

It is no longer possible to use value <automaton name> to refer to the current location of an automaton, or for location to value mapping transformations. Instead, you can now use value self if you declare the output mapping in the automaton (or automaton definition) itself.

The in ... syntax to change the scope of mappings and values is no longer available. Instead, the mappings can now be directly put in the correct scope (component or component definition).

Due to the addition of CIF/SVG declarations as an extension of the CIF, the following identifiers are now reserved keywords in CIF: attr, id, inmax, inmin, outmax, outmin, pattern, self, svgfile, svgin, svgout, text, value.

For further information on the new CIF/SVG declarations, see the updated SVG visualization documentation.

2013-11-11 Imports and namespaces

Previously, there were several problems with imports. One of the problems was that the imported specification ended up in a sub-scope (group) of where it was imported. The name of the sub-scope could be specified using the as keyword, but it was not possible to get rid of this additional scope. A second problem was that the imported file ‘lived’ at the place it was imported. As such, if a file was imported multiple times, this resulted in multiple ‘copies’ of the imported file. Such ‘copies’ were no longer linked to the original imported file, and were thus incompatible. For instance, if an automaton definition was imported twice, instantiations from those two ‘copies’ of the automaton definition would be incompatible, and could not be used as parameters of component definitions that had the ‘wrong’ copy as their type.

Imports have been completely redesigned, to get rid of all such problems. The basic idea of the new imports is that they bring the contents of the imported file into existence globally, instead of locally. Importing another CIF file now leads to the content of that imported file becoming available in (or merged into) the importing file. As an example, consider the following two CIF files (file1.cif and file2.cif):

import "file2.cif";

const real c1 = 1.0;

group a:
  const real c2 = c5;

  group b:
    const real c3 = 3.0;

    automaton a:
      location:
        initial;
    end
  end
end
const real c4 = 4.0;

group a:
  const real c5 = 5.0;

  group b:
    const real c6 = 6.0;
  end

  group c:
    automaton b:
      location:
        initial;
    end
  end
end

If we eliminate the imports from the first file, we get:

const real c1 = 1.0;
const real c4 = 4.0;

group a:
  const real c2 = c5;
  const real c5 = 5.0;

  group b:
    const real c3 = 3.0;
    const real c6 = 6.0;

    automaton a:
      location:
        initial;
    end
  end

  group c:
    automaton b:
      location:
        initial;
    end
  end
end

Groups that exist in multiple files are merged together, similar to how the CIF merger tool merges CIF files. However, unlike the tool, imports only merge top level groups, and not group definitions, automata, variables, etc. All other declarations must have unique absolute names in order to be allowed to be imported.

In the above example, constant c2 in group a refers to c5. No such declaration exists in that file, but it does exist in the other file. The import of file file2.cif makes the constants from that file available in file file1.cif. It is then possible to directly to refer to constant c5, as it also lives in group a, albeit in the imported file.

Imports can now only be specified at the top level of a CIF file, and no longer in groups. This expresses more clearly that the contents of the file is to be made available globally, instead of locally. The as keyword can no longer be used, as it has become irrelevant now that imported files are not put in a sub-scope.

It is now allowed to have cycles in imports, for instance by having two sub-systems (specified in different files) import each other, in order to share their interfacing events, variables, etc.

One way to use imports, is to have a file per sub-system. The sub-systems will usually live in some nested groups. For instance, for a factory consisting of several machines, with parts and sub-parts, one file may look like this:

group machine1:
  group part1:
    automaton subpart1:
      ...
    end
  end
end

Since this is a common case, and the surrounding groups clutter the file and cause deep indentations, this can now be specified as follows:

namespace machine1.part1;

automaton subpart1:
  ...
end

The namespace declaration is simply a shortcut for putting two groups (machine1 and part1) around the entire body of the file. Using a namespace declaration, a CIF file can indicate where its content ‘lives’, regardless of by which file it is imported.

Namespaces may only be declared at the top level of CIF files. It is recommended to first specify the imports, and then the namespace, as not to give the impression that the contents of the imported CIF files is made available in the given namespace.

2013-06-07 Components, groups, and kinds

Previously in CIF, all components had a kind. This included not only automata, but also composites (components used for grouping). The available kinds were plant, requirement, synthesis, verification, supervisor, group, and the unspecified kind (no keyword).

The synthesis and verification kinds have been removed from the language. To migrate your specifications, replace them by requirement instead. The unspecified kind (no keyword) has been replaced by the automaton kind. All automata that don’t have a kind can be migrated by putting the automaton kind before the name of the automaton.

Composites no longer have a kind. Instead, composites must now always be groups, with the group keyword (which is no longer a kind). Thus, only automata have a kind, which can be automaton, plant, requirement, or supervisor.

Component definitions must use the group keyword if their body is a group, and an automaton kind keyword if their body is an automaton. It is no longer possible/allowed to specify a kind with the instantiation of component definitions. The instantiated component will be a group if the component definition was a group, and the instantiated component will inherit the automaton kind if the instantiated component definition was an automaton. To migrate, simply remove the kinds from the automaton instantiations.

Due to these changes, automaton is now a keyword, and synthesis and verification are no longer keywords.

As an example, consider the following CIF specification:

g:
  a:
    location:
      initial;
  end

end

synthesis r:
  location:
    initial;
end

requirement def X():
  event e;
end

def Y():
  location:
    initial;
end

plant def Z():
  location:
    initial;
end

synthesis x: X();
y: Y();
plant z: Z();

This specification can be migrated to:

group g:
  automaton a:
    location:
      initial;
  end
end

requirement r:
  location:
    initial;
end

group def X():
  event e;
end

automaton def Y():
  location:
    initial;
end

plant def Z():
  location:
    initial;
end

x: X();
y: Y();
z: Z();

2013-05-14 Monitors and inputs

Since monitors are an additional property of a component, and we want to be able to express monitor plants as well as monitor requirements, the concept of a monitor components (including monitor automata) has been removed. Since a monitor component is essentially a shortcut for defining all events as inputs, using input events is an alternative. It is however no longer possible to define monitors outside automata.

Input events have been renamed to monitor events, as that name better expresses the concept. To alleviate the removal of monitor components, it is now possible to define a set of monitor events without specifying any events, which means that all events of the alphabet of the automaton are monitored by that automaton, similar to the automaton previously being declared a monitor automaton.

To migrate this monitor automaton:

monitor m:
  event e;
  location:
    initial;
    event e when time > 5;
end

change it to:

plant m:
  monitor;
  event e;
  location:
    initial;
    event e when time > 5;
end

Assuming you wish to make the automaton a plant. To migrate this automaton with input events:

requirement r:
  event e;
  input e;
  location:
    initial;
    event e when time > 5;
end

change it to:

requirement r:
  event e;
  monitor e;
  location:
    initial;
    event e when time > 5;
end