CIF release notes

The release notes for the versions of CIF and the associated tools, as part of the Eclipse ESCET project, are listed below in reverse chronological order.

The release notes may refer to issues, the details for which can be found at the Eclipse ESCET GitLab issues page.

See also the Eclipse ESCET toolkit release notes covering those aspects that are common to the various Eclipse ESCET tools.

Version 0.3

Language changes:

  • Removed inheritance of a supervisory kind for invariants. This was deprecated over 6 years ago and already led to warnings in the specification. Invariants without a supervisory kind specification (plant, requirement, supervisor) that reside in an automaton or location of an automaton, and where that automaton has a supervisory kind, now no longer inherit the supervisory kind of that automaton. Instead they remain kindless. This is a backward incompatible change (issue #139).

New features:

  • CIF controller property checker application added to check supervisory controllers for finite response (issue #122).

  • CIF data-based synthesis has a new option to print warnings for events that are never enabled in the input specification or the synthesized controlled system. This new option is enabled by default (issues #108, #150, #162 and #164).

  • CIF data-based synthesis now supports boolean constants in predicates (issue #143).

  • CIF data-based synthesis now supports switch expressions (issue #148).

Improvements and fixes:

  • CIF to CIF transformation to remove requirements no longer supports removing requirement automata that contain locations with non-requirement (kindless, plant, or supervisor) invariants, preventing the loss of invariants (issue #140).

  • CIF to CIF transformation to remove requirements now properly moves invariants from requirement automata to their parents, rather than also removing them (issue #140).

  • CIF data-based synthesis simplification of supervisor guards for false guards under false assumption now correctly results in true simplified guards, to indicate the supervisor doesn’t enforce a restriction (issue #144).

  • CIF data-based synthesis documentation updated to reflect that code generator tools support state/event exclusion invariants (issue #163).

  • CIF PLC code generator error message now indicates correct TwinCAT XAE project file path (issue #154).

  • CIF type checker improved to report more issues for list projections with impossible bounds, rather than deferring to runtime checks (issue #177).

  • The CIF simulator, CIF to UPPAAL transformation, and CIF to mCRL2 transformation are now all under the 'CIF simulation, validation and verification tools' part of right-click menus on CIF files and editors (issue #122).

  • The website and Eclipse help now use multi-page HTML rather than a single HTML file, although the website still contains a link to the single-page HTML that allows easily searching the full documentation (issue #36).

  • Enabled section anchors for documentation on the website, and disabled section anchors for Eclipse help (issue #36).

  • Several small documentation fixes and improvements (issues #36 and #166).

Version 0.2

Language changes:

  • A switch case key must now have a type that is compatible (ignoring ranges) with the type of the switch value, rather than the type needing to be fully contained in the type of the switch value. This is a backward compatible change (issue #105).

Deprecations and removals:

  • CIF deprecated enumeration declaration syntax (with curly brackets) now leads to deprecation warnings. The documentation now properly reflects the deprecation as well (issue #45).

  • CIF to CIF transformation to eliminate enumerations (elim-enums) is now deprecated. Use the transformation to convert enumerations to integers instead, as it has the same functionality (issue #78).

  • CIF PLC code generator option to either eliminate enumerations (to integers) or not is now deprecated. Use the new option to choose whether to convert enumerations to constants or integers, or not at all. See the documentation of the PLC code generator for further details (issue #78).

  • CIF simulator deprecated 'interactive input mode' (interactive value) has been removed. Use the 'interactive console input mode' instead (issue #81).

New features:

  • CIF to CIF transformation to convert enumerations to constants (enums-to-consts) and enumerations to integers (enums-to-ints) has been added (issue #78).

  • CIF explorer now has an option to specify the name of the resulting statespace automaton (issue #55).

  • CIF PLC code generator now has an option to choose whether to convert enumerations to constants or integers, or not at all. This replaces the old option to either eliminate enumerations (to integers) or not, which is now deprecated. See the documentation of the PLC code generator for further details (issue #78).

Improvements and fixes:

  • Various fixes for handling component definition/instantiation as well as references via component instantiations and component parameters (issues #25, #39 and #66).

  • CIF type checker now properly detects cycles for algebraic variables and derivatives of continuous variables defined via equations per location of an automaton (issue #106).

  • CIF to CIF 'eliminate the use of locations in expressions' transformation no longer generates location pointer variables for automata with exactly one location (issue #99).

  • CIF to CIF linearize transformations no longer generate location pointer variables for automata with exactly one location (issue #99).

  • CIF to CIF linearize merge transformation no longer crashes for channels without a sender (issue #56).

  • CIF simulator no longer crashes on enumeration literals that have a name that is a Java keyword (issue #104).

  • CIF simulator initialization fixed to properly account for algebraic variables and derivatives of continuous variables defined via equations per location of an automaton (issue #106).

  • CIF simulator now correctly determines initial value for locations without initialization predicates, when those locations are used in initial values of variables (issue #37).

  • CIF simulator no longer crashes on assignments to dictionaries with non-int keys (issue #47).

  • CIF simulator no longer crashes when using the Eclipse Compiler for Java (ecj) as Java compiler (issue #46).

  • CIF simulator is now more robust for larger numbers of state invariants in components (issue #49).

  • CIF data-based synthesis now supports state/event exclusion plant invariants (issue #84).

  • CIF data-based synthesis now properly ensures requirement invariants are rebranded as supervisor invariants in the synthesis output. Therefore, simulating a synthesized supervisor no longer gives warnings for simulating requirement invariants (issues #116 and #117).

  • CIF data-based synthesis documentation, debug output and warnings improved/fixed regarding invariants vs requirement invariants and controlled vs uncontrolled system (issue #83).

  • CIF PLC code generator now supports state/event exclusion invariants (issue #94).

  • CIF PLC code generator no longer generates location pointer variables for automata with exactly one location when performing linearization as preprocessing (issue #99).

  • CIF PLC code generator now creates output folder if it does not yet exist, rather than giving an error, if IEC 61131-3 output is requested (issue #74).

  • CIF PLC code generator documentation now correctly indicates the order in which CIF to CIF transformations are applied (issue #78).

  • CIF PLC code generator PLCOpen XML output fixes for PLC tasks (issue #75).

  • CIF code generator now supports state/event exclusion invariants (issue #94).

  • CIF code generator no longer generates location pointer variables for automata with exactly one location when performing linearization as preprocessing (issue #99).

  • CIF to mCRL2 transformation now supports algebraic variables (issue #120).

  • CIF to mCRL2 transformation precondition check messages and documentation improvements (issues #59, #60 and #120).

  • CIF to Supremica precondition check message wording for discrete variables with multiple potential initial values has been fixed (issue #58).

  • CIF to Supremica transformation now supports state/event exclusion invariants (issue #94).

  • CIF to UPPAAL precondition check message wording for discrete variables with multiple potential initial values has been fixed (issue #58).

  • CIF to UPPAAL transformation now supports state/event exclusion invariants (issue #94).

  • CIF to UPPAAL transformation now supports algebraic variables and enumerations (issue #129).

  • CIF tutorial updated to remove explanation of list subtraction operator that doesn’t exist in the language and implementation (issue #77).

  • CIF documentation updated to fix two broken links (issue #80).

Version 0.1

The first release of CIF as part of the Eclipse ESCET project. This release is based on the initial contribution by the Eindhoven University of Technology (TU/e).

Most notable changes compared to the last TU/e release:

  • The names of the CIF command line tools and tools available in ToolDef scripts have changed. For more information, check the list of currently available tools.

  • The CIF simulator no longer crashes on code generation.

  • The CIF simulator plot visualizer has been re-implemented using different third party libraries.