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.

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

Version 2.0 (2023-12-22)

Language changes:

  • Annotations may now be added to locations of automata. Annotations are still an experimental work-in-progress language feature. Their design may change in a backward incompatible manner (issue #593).

  • A single element of a CIF specification may now be annotated multiple times with the same annotation (typically with different arguments). Annotations are still an experimental work-in-progress language feature. Their design may change in a backward incompatible manner (issue #692).

  • The CIF toolset now comes bundled with the state annotation. It is currently an experimental work-in-progress annotation. Its design may change in a backward incompatible manner (issues #687 and #697).

  • The CIF type checker now warns about certain duplicate state invariants (issue #542).

New features:

  • A new CIF PLC code generator has been added to the CIF toolset. The new PLC code generator is currently being developed, and should be considered experimental. In due time, it will replace the current stable CIF PLC code generator (issues #397, #676 and #679).

  • The CIF code generator can now generate HTML files. The HTML files allow executing the model in a browser. The HTML code generation is currently an experimental feature (issues #272 and #715).

  • The CIF code generator can now generate JavaScript code. The JavaScript code generation is currently an experimental feature (issues #272 and #715).

  • The CIF explorer now generates an output CIF model with state annotations. This can be disabled using the tool’s new Add state annotations option (issues #687 and #698).

  • The tools from the event-based toolset that output CIF models, now generate CIF models with state annotations. This can be disabled using the tools' new Add state annotations options (issue #708).

  • The CIF documentation now includes a history page, that explains the history of CIF, as well as what 'CIF' used to stand for (issue #669).

Improvements and fixes:

  • All CIF tools that produce an output CIF file, no longer produce an invalid CIF file when a model contains integer types that only support the minimum integer value (issue #689).

  • The CIF type checker now produces improved error messages in case of a mismatch between an argument of a component instantiation and the corresponding parameter of the instantiated component definition (issue #672).

  • The CIF simulator no longer crashes when simulating models with large expressions (issue #611).

  • The CIF simulator now truncates messages for runtime errors that include large expressions (issue #661).

  • The CIF to CIF transformation to 'add default initial values' now produces correct results for models with discrete variables with an integer type that only supports negative integer values (issue #689).

  • The CIF to CIF transformation to 'simplify values' now produces correct results for models with integer expressions that are simplified to the minimum integer value (issue #689).

  • The CIF merger now produces correct models when merging models with annotations (issue #680).

  • The CIF explorer no longer crashes for models with discrete variables that have a function type and that are not explicitly initialized (issue #690).

  • The CIF explorer no longer crashes for models with discrete variables with integer types that only support the minimum integer value (issue #689).

  • The CIF explorer no longer crashes for models with expressions that evaluate to the minimum integer value (issue #689).

  • The CIF explorer documentation has some fixes, improvements and extensions (issue #687).

  • The CIF controller checker now produces more debug output (if debug output is enabled), to be able to better track its progress (issue #686).

  • The CIF controller checker is now more responsive to termination requests (issue #686).

  • The CIF to mCRL2 transformer now supports CIF models with logical implication binary operators (issue #667).

  • The CIF code generator now generates better-formatted Java code for checking range violations (issue #272).

  • The CIF code generator now generates valid Java and Simulink code for models without enumerations and without any automata that have at least two locations (issues #272 and #715).

  • The CIF code generator no longer crashes for certain models with more complex initialization. Previously, if an automaton had multiple locations with initialization predicates that contained variables, but only one of those locations was an initial location, the code generator could crash (issue #683).

  • The CIF PLC code generator (stable version) no longer crashes for certain models with more complex initialization, if its Simplify values option is disabled. Previously, if an automaton had multiple locations with initialization predicates that contained variables, but only one of those locations was an initial location, the code generator could crash (issue #684).

  • The 'lithography_init' benchmark model has been changed, removing a duplicate invariant (issue #712).

  • The CIF language tutorial has various improvements and extensions for the documentation about annotations (issue #593).

  • The CIF language reference manual now includes additional detailed information about annotations (issue #593).

  • The CIF tool manual now indicates for each tool which annotations it supports, and how it handles them (issue #593).

  • The CIF documentation has various small improvements and fixes (issues #593, #648, #669, #682, #687 and #708).

Version 1.0 (2023-09-30)

Language changes:

  • The CIF language now features annotations, that can be used to annotate elements of the specification with extra information. Annotations are currently an experimental work-in-progress language feature. Their design may change in a backward incompatible manner (issue #593).

  • The CIF toolset now comes bundled with the doc annotation. It is currently an experimental work-in-progress annotation. Its design may change in a backward incompatible manner (issue #593).

Improvements and fixes:

  • The CIF simulator no longer deadlocks if an element of an SVG image is clicked, and the corresponding CIF/SVG input mapping maps to an event that is disabled in the current state. Instead, it now prints a warning and ignores the click (issue #469).

  • The CIF controller checker had a performance regression since version 0.7, in case finite response is checked, and confluence is not checked. This performance regression has been fixed (issue #639).

  • The CIF controller checker now requires at least one check to be enabled (issue #639).

  • The CIF data-based synthesis tool’s workset algorithm now has improved edge selection heuristics, improving the performance of the workset algorithm (issues #520 and #605).

  • The CIF data-based synthesis tool’s workset algorithm is no longer considered experimental (issue #655).

  • The CIF data-based synthesis tool’s workset algorithm documentation has been improved, to better explain when to use and not to use the workset algorithm (issue #655).

  • The CIF to Supremica transformation now correctly transforms multiple guards on an edge. Multiple guards are now combined into a single conjunction (issue #620).

  • The CIF merger does not allow merging two input variables with the same annotations (issue #593).

  • The CIF code generator now supports doc annotations on input variables. The comments in the generated C, Java and Simulink code for doc-annotated input variables, now include the documentation from their documentation annotations (issue #593).

  • The CIF event disabler tool now properly closes the event names file after reading it, preventing a resource leak (issue #649).

  • The CIF explorer command line script no longer crashes due to a failure to find the application to execute (issue #658).

  • The 'festo' benchmark model has been changed, removing a duplicate invariant (issue #646).

  • The FIFO CIF example now uses SVG input, rather than GUI input. It is now possible to click the arrows in the SVG image to control the simulation (issue #639).

  • The Wolf/Goat/Cabbage CIF example now has simpler CIF/SVG input mappings (issue #639).

  • The CIF documentation pages for the CIF code generator now use syntax highlighting for C and Java code (issue #569).

Version 0.10 (2023-06-30)

Language changes:

  • Switch expressions with only a single case or else are now deprecated (issue #612).

  • The CIF type checker now allows omitting the else part of switch expressions in more situations, when it can be statically determined that the switch expression is complete without it. The type checker has also been improved, regarding detection of duplicate and missing switch cases, and superfluous elses (issue #548).

Deprecations and removals:

  • The curly-brackets syntax for declaring enumerations was deprecated in 2014 and has now been removed. Use the syntax without curly brackets instead (issue #613).

  • The CIF PLC code generator’s Eliminate enumerations option was deprecated in release v0.2 and has now been removed. Use the Convert enumerations option instead, which allows for more control (issue #613).

  • The CIF to CIF transformation to eliminate enumerations (elim-enums) was deprecated in release v0.2 and has now been removed. Use the transformation to convert enumerations to integers (enums-to-ints) instead, as it has the same functionality (issue #613).

New features:

  • The CIF data-based synthesis tool has a new Edge granularity option to configure the granularity of edges to use during synthesis. Previously, the linearized edges were used 'as is'. Now, they are merged per event, to obtain a single edge per event. The option can be used to restore the old behavior. The new edge granularity has been shown to reduce both the memory usage and time required to perform synthesis, but this may depend on the model being synthesized. For more information, see the documentation of the new option (issue #586).

  • The CIF data-based synthesis tool has a new Fixed-point computations order option to configure the order in which the fixed-point computations are to be performed during synthesis. By default, the fixed-point computations have the same order as before. First the non-blocking states are computed, then the controllable states, and finally the reachable states (the reachable states are still only computed if the Forward reachability option is enabled). Using the new option, the order can be changed. This may significantly improve synthesis performance, but the effect greatly depends on the model being synthesized (issue #609).

  • The CIF data-based synthesis tool now features an experimental workset algorithm to dynamically determine the order in which edges are considered during reachability fixed-point computations. It is currently considered to be experimental and is disabled by default. It can be enabled using the new Edge workset algorithm option. It can only be used when a per-event edge granularity is configured, and duplicate events are allowed in the edge order (issues #520 and #602).

Improvements and fixes:

  • The position information of invariants has been improved. All CIF tools that may report on invariants give improved file position information, for example in type checker errors and precondition violation reports (issue #591).

  • The CIF simulator’s command line script has been fixed for handling dark theme detection, preventing crashes and improving dark theme support, when using the simulator’s plot visualizer or interactive GUI input component (issue #567).

  • The CIF simulator’s SVG visualizer Save as dialog now properly starts in the directory that contains the SVG file, also on Windows. And it now properly handles paths with spaces and other special characters in them (issue #221).

  • The CIF explorer now warns about exploring specifications with requirements (issue #585).

  • The CIF event-based synthesis toolset’s command line scripts now have correct information to start the tools, where previously they always crashed (issue #567).

  • The CIF event-based synthesis analysis tool’s command line script has been fixed for handling dark theme detection, preventing crashes and improving dark theme support (issue #567).

  • The CIF event-based synthesis analysis tool’s command line script has been fixed to not immediately terminate after starting the tool (issue #567).

  • The CIF event-based synthesis tool now warns about synthesizing specifications without requirement automata (issue #553).

  • The CIF data-based synthesis tool no longer prints the number of states in the controlled system as part of its debug output. Instead, this information is now one of the statistics of the Statistics options. The new statistic is disabled by default, and if enabled the statistic is now printed to normal output. The output itself has some whitespace changes (issue #526).

  • The CIF data-based synthesis tool now has better performance for converting updates of the CIF specification to their internal BDD representations (issue #580).

  • The CIF data-based synthesis tool now has slightly better performance due to skipping some unnecessary calculations for applying edges during reachability fixed-point computations (issue #520).

  • The CIF data-based synthesis tool now enforces state plant invariants like it does state requirement invariants, when they are applied per edge. This may improve synthesis performance for models with state plant invariants (issue #523).

  • The CIF data-based synthesis tool’s BDD library operation cache ratio option has been fixed. It now functions as documented, rather than having the inverse effect. It now also has improved precision (issue #610).

  • The CIF data-based synthesis tool’s legacy hyper-edge creation algorithm now properly considers invariants in locations for variable ordering. Previously, for every location, the invariants of the automaton that contains the location were considered, rather than considering the invariants of the location itself. This change could affect synthesis performance (issue #377).

  • The CIF data-based synthesis benchmarking scripts no longer produce debug output when performing synthesis, making benchmarking faster and producing less output, while still reporting the platform-independent metrics and the number of states in the controlled system (issues #526 and #564).

  • The CIF data-based synthesis documentation has several improvements and extensions (issues #609 and #610).

  • The CIF controller property checker’s finite response check may now have improved performance (issue #583).

  • The CIF to CIF transformation to merge all enumerations of the specification into a single enumeration has been changed. It now converts the last case of all switch expressions to an else, for switch expressions that switch over a value that has a type that includes an enumeration type. Hereby, the keys of these last cases are removed from the model (issue #548).

  • The CIF language tutorial has an additional lesson on if and switch expressions (issue #598).

  • The CIF language tutorial lesson on function statements has been improved and extended (issue #598).

  • The website has been fixed to ensure all version-specific URLs are now properly replaced by non-version-specific ones when a version-specific website is promoted to become the main website. Previously, a few URLs remained version-specific (issue #577).

Version 0.9 (2023-03-31)

New features:

  • The CIF type checker now warns about certain duplicate state/event exclusion invariants (issue #299).

  • The CIF transformer has a new additional CIF to CIF transformation, to remove unused events (issue #525).

  • The CIF data-based synthesis tool variable ordering configuration has been generalized and extended. This includes the addition of a new BDD advanced variable ordering option. It offers much more flexibility in configuring variable ordering, including configuration of the order in which to apply various algorithms, and configuration of the settings to use per algorithm. As a result of the changes, the debug output has been changed considerably. See the documentation of the new option for more information (issues #378 and #530).

  • The CIF data-based synthesis tool Edge order option has been replaced by two separate Edge order for backward reachability and Edge order for forward reachability options. This allows to specify the orders separately for forward and backward reachability computations, which may improve synthesis performance. The defaults have not been changed (issue #492).

  • The CIF data-based synthesis tool has a new Edge order duplicate events option to allow duplicate events in custom event orders (issue #426).

  • The CIF data-based synthesis tool now has a State requirement invariant enforcement option, adding an alternative second approach to apply state requirement invariants during synthesis. Both approaches have potential benefits and drawbacks, making for a trade-off between their various effects. Which approach is most efficient depends on the model. The default has not been changed. As a result of the changes, the debug output of the tool has changed as well (issue #198).

  • The CIF data-based synthesis tool statistics option has been extended to allow measuring the maximum amount of memory used during synthesis. See the documentation for more information on how to best use this new feature (issue #531).

  • The CIF data-based synthesis tool benchmarking scripts have newly added functionality. The settings to configure the configurations to benchmark have been generalized, making it more powerful. It is also possible to execute benchmarking for only a subset of the configurations. The generated HTML overviews now allow switching between absolute and relative values, feature extra columns with average values, and some of the columns can now be sorted (issues #538, #539 and #551).

  • The CIF benchmarking set of models now includes more than 10 additional benchmarking models (issues #364, #522, #532 and #537).

  • The CIF bridge example model now includes a readme file that describes several simulation scenarios (issue #489).

Improvements and fixes:

  • The CIF type checker now reports various errors at better positions, including for function calls to standard library functions (issue #454).

  • The CIF simulator state visualizer performance has been greatly improved (issue #485).

  • The CIF simulator error message for unsupported specifications with time-dependent state invariants has been improved (issue #513).

  • The CIF data-based synthesis tool now detects reachability fixed points sooner, reducing fixed point computations by at most one iteration. The effect on synthesis performance greatly depends on the model (issue #493).

  • The CIF data-based synthesis tool no longer skips variable ordering if representations of relations between variables are empty, but unused (issue #378).

  • The CIF data-based synthesis tool options that influence the variable ordering have some new defaults. The DCSH variable ordering algorithm is no longer considered experimental, and is now enabled by default. The BDD hyper-edge creation algorithm option has a new default value that is set by default. It uses the linearized hyper-edges for the FORCE and sliding window algorithms, while for all other variable orderers the legacy hyper-edges are still used. These changes to the default variable ordering configuration have been shown to improve the out-of-the-box performance of data-based synthesis in many cases, especially for models that take longer to synthesize or require more memory to synthesize. However, the effect greatly depends on the model being synthesized, and for some models synthesis using default settings may now be slower (issues #378) and #379).

  • The CIF data-based synthesis tool documentation has various small improvements (issues #426, #492 and #531).

  • The CIF data-based synthesis tool documentation related to variable ordering has been split into multiple pages, and has been extended and improved (issues #378 and #530).

  • The CIF data-based synthesis tool error messages for invalid custom event orders have been improved (issues #426 and #492).

  • The CIF data-based synthesis tool BDD variable order option has been renamed to BDD initial variable ordering. The command line name of the option has not been changed (issue #530).

  • The CIF data-based synthesis tool BDD initial variable ordering option now supports values with leading and trailing whitespace (issue #378).

  • The CIF data-based synthesis tool termination request detection has been improved, by reducing the number of times it unnecessarily checks for termination requests (issue #198).

  • The CIF data-based synthesis tool benchmarking scripts have been improved in various ways. The scripts and generated overviews now use improved and consistent terminology. The script to execute benchmarks no longer warns about events in the models that are disabled. The script to generate HTML overviews is more robust in handling unknown values, partial or missing information, as well as inconsistent and duplicate information. The generated HTML overviews feature more colors to more easily see which configurations work better or worse, have various styling improvements, contain additional information, and warn about potential issues in the experiment data. There are some other smaller improvements as well (issues #522, #538, #539 and #551).

  • The CIF event-based synthesis tool now allows synthesis for specifications without requirements (issue #544).

  • The CIF event-based language equivalence check tool now prints a counter example path if the two automata are not language equivalent (issue #413).

  • The CIF code generator has small improvements to the Java code that it generates (issue #450).

  • The CIF PLC code generator option description for the PLC number bits option has been fixed (issue #418).

  • Various CIF tools have completely redesigned output in case of precondition violations. The new output groups similar violations, has improved readability, and provides more context and information about where in the model the violations occur. There are some other smaller improvements as well. The new output is produced by the CIF code generator, CIF PLC code generator, CIF to UPPAAL transformer, and the CIF to Supremica transformer (issue #454).

  • The CIF tutorial has various small fixes and other improvements (issues #501, #502, #503, #504, #506, #509, #510 and #512).

  • The CIF documentation has some improvements related to 'file separator' terminology (issue #450).

Version 0.8 (2022-12-21)

Language changes:

  • Improved type checking for the = and != binary expressions. The type checker now not only uses the type of the left operand as type hint for the right operand, but also the type of the right operand as type hint for the left operand, in case the former is not sufficient. This allows for instance type widening for the left operand to be derived from the right operand, such that both expressions x = 1 and 1 = x are now supported, with x a real-valued variable (issue #446).

New features:

  • The CIF data-based synthesis tool now has a second hyper-edge creator, the linearized hyper-edge creator, which may improve performance. The legacy hyper-edge creator is still used by default. The hyper-edge creator can be configured using the new BDD hyper-edge creation algorithm option (issue #380).

  • A new CIF example model has been added (issue #465).

  • A new CIF benchmarking model has been added (issue #451).

  • The CIF benchmarking models now come with scripts to easily benchmark data-based synthesis (issues #375 and #455).

Improvements and fixes:

  • Normally, .cif files are opened with the CIF text editor. Large files are now however opened with the default non-CIF text editor to avoid performance issues. You can open a file in an editor of your choosing by right clicking it and selecting Open With and then selecting the editor of your choosing, or choosing Other…​ to open a dialog to choose from a larger selection of editors (issue #199).

  • The CIF simulator no longer creates a directory named cifcode in the root of your drives or file systems when using the Eclipse Compiler for Java (ECJ) to compile Java code (issue #176).

  • The CIF simulator state visualizer performance has been slightly improved (issue #477).

  • The CIF simulator state visualizer’s Value column width adjustments are now less 'jittery' (issue #477).

  • The CIF simulator plot visualizer and GUI input component now have theming support, and come with a dark theme in addition to the existing light theme. They now automatically use their dark theme when the Eclipse built-in dark theme is used, and use a light theme otherwise (issue #417).

  • The CIF simulator plot visualizer now has slightly darker gridlines in the light theme, for enhanced contrast (issue #417).

  • The CIF event-based synthesis analysis tool now has theming support, and comes with a dark theme in addition to the existing light theme. It now automatically uses its dark theme when the Eclipse built-in dark theme is used, and uses a light theme otherwise (issue #417).

  • The CIF event-based synthesis analysis tool now has slightly wider colored boxes that distinguish between disabled and different types of enabled choices, for enhanced visual clarity (issue #417).

  • The CIF to Supremica transformation precondition check has improved output. The preconditions themselves have not changed (issues #368, #424, #442 and #470).

  • The CIF to UPPAAL transformation precondition check has been migrated to the new precondition check framework, which is already used by the CIF to Supremica transformation, resulting in improved output. The preconditions themselves have not changed (issue #424).

  • The CIF PLC code generator precondition check has been migrated to the new precondition check framework, which is already used by the CIF to Supremica transformation, resulting in improved output. The preconditions themselves have not changed (issue #457).

  • Very long lines in the Console view, for instance outputted by the CIF simulator, and long lines in text editors, for instance long lines in synthesized CIF models, now render correctly on Windows (issue #76).

  • The CIF documentation has been updated to account for changes in recent Inkscape versions (issue #357).

  • The CIF data-based synthesis documentation has been split into multiple pages, as it was getting quite long (issue #460).

  • The CIF data-based synthesis documentation on supported updates, expressions and predicates has been improved (issue #459).

  • Some very small other documentation improvements (issues #199, #438 and #460).

Version 0.7 (2022-09-30)

New features:

  • The CIF controller property checker can now also check whether controllers satisfy the confluence property. As the checker now has multiple properties that it can check, each property check can be individually enabled and disabled, and all checks are enabled by default (issue #145).

  • The CIF examples contain a new bridge example, to showcase the real-world usage of CIF for synthesis-based engineering (issue #419).

  • Two new CIF benchmarking models have been added (issue #364).

  • The CIF text editor now has theming support, and comes with a dark theme in addition to the existing light theme. The text editor now automatically uses its dark theme when the Eclipse built-in dark theme is used, and uses a light theme otherwise. The text editor theming behavior can be configured via the Eclipse Preferences dialog (issue #347).

Improvements and fixes:

  • The CIF event-based synthesis tool now records removal of non-reachable locations in the synthesis dump file. This new information in synthesis dump files is now also taken into account by the CIF event-based synthesis analysis tool (issue #404).

  • The CIF event-based language equivalence check tool now produces correct counter examples (issues #297 and #405).

  • The CIF controller checker output has been improved in terms of readability (issue #145).

  • The CIF controller checker option descriptions and UI have been slightly improved (issue #145).

  • The CIF controller checker documentation has been improved (issue #145).

  • The CIF to Supremica transformation precondition check has improved output and no longer crashes on reporting certain precondition violations. The preconditions themselves have not changed (issues #398 and #416).

  • The CIF text editor light theme’s default color has changed from a near-black slightly-brown color to pure black (issue #347).

  • The CIF to yEd transformer syntax highligher’s default color has changed from a near-black slightly-brown color to pure black (issue #347).

Version 0.6 (2022-07-07)

Language changes:

  • Invariants can now be given a name (issue #323).

New features:

  • Added a CIF benchmark models import wizard, with several benchmarking models, similar to the CIF examples import wizard (issue #364).

  • The CIF data-based synthesis tool now warns about input models where plants refer to requirement state. The new functionality is enabled by default, but can be disabled using an option (issue #311).

  • The CIF data-based synthesis tool features the DCSH algorithm as new additional variable ordering algorithm. It is considered experimental for now, and therefore disabled by default, but can be enabled using an option (issue #196).

Improvements and fixes:

  • The CIF data-based synthesis tool’s automatic variable ordering has various internal improvements in preparation for further upcoming improvements. As a result the debug output has been extended and changed a bit (issues #196 and #371).

  • The CIF data-based synthesis tool’s automatic variable ordering documentation has been improved and extended (issue #196).

  • The CIF data-based synthesis tool has some small consistency improvements for its command line option descriptions (issue #311).

  • Some improvements to the documentation of the CIF to CIF linearize merge/product transformations (issue #354).

  • The CIF to Supremica transformation precondition check has been redesigned, producing different output. The preconditions themselves have not changed (issue #370).

  • Links in the documentation to non-CIF ESCET documentation webpages now use version-specific URLs (issue #386).

  • Improved bibliography references in documentation (issue #365).

  • The issue numbers in the release notes now link to the corresponding GitLab issue (issue #396).

  • Small website style improvements (issue #367).

Version 0.5 (2022-03-29)

New features:

  • The CIF documentation contains an extensive new section on synthesis-based engineering of supervisory controllers (issues #325 and #334).

  • The CIF examples contain a new FIFO example, to showcase the power of supervisory controller synthesis. It is also described in the new synthesis-based engineering documentation (issue #325).

  • The CIF PLC code generator now supports S7 output for SIMATIC controllers (issue #142).

  • The CIF data-based synthesis tool now supports state plant invariants (issue #107).

  • The CIF to CIF transformer has several new transformations, to anonymize the names of all named objects, convert controllable events to uncontrollable ones and vice versa, and remove unused algebraic variables and their equations (issues #306, #308 and #320).

Improvements and fixes:

  • The CIF type checker no longer produces the wrong warning for globally disabled event that are monitored, for events referred to via component parameters or component instantiations (issue #300).

  • The CIF type checker no longer produces false positive/negative warnings and errors related to the use of events in component definitions/instantiations. This applies to the following checks: duplicate events in alphabets, duplicate monitor events, duplicate events on edges, events on edges not in alphabets, monitoring events not in alphabets, events in alphabet not on any edge, monitored event not on any edge, and monitoring an empty alphabet. It also has several other small improvements related to these checks, including improved warning messages and reporting the warnings at better positions. As a result of the changes, problems are no longer reported for non-instantiated component definitions (issues #298 and #301).

  • The CIF simulator interactive GUI input component now has a horizontal scrollbar from the start, if applicable (issue #217).

  • The CIF simulator being terminated by the red stop button no longer leaves the interactive GUI input component buttons enabled (issue #274).

  • The CIF PLC code generator PLC number bits option now has a new automatic mode. The default remains 64-bit for PLCopen XML, IEC 61131-3 and TwinCAT output (issue #142).

  • The CIF PLC code generator now generates correct assignments to temporary variables for multi-assignments (issue #282).

  • The CIF PLC code generator now generates calls to the NOT function without formal argument names (issue #286).

  • The CIF documentation has several small improvements (issues #271, #324 and #326).

  • The release notes for each version now contain the release date, with the exception of milestone releases and release candidates (issue #314).

Version 0.4 (2021-12-17)

Language changes:

  • Component parameters can now be used as values, for instance as arguments to component instantiations. See the CIF language tutorial lesson on group definitions for more information (issue #222).

New features:

  • The CIF simulator now supports simulating specifications with input variables. Use the CIF specification initialization option to specify the initial value of input variables. Support for modifying the value of input variables during simulation is planned for future versions (issue #203).

  • The CIF data-based synthesis tool now has an Edge order option to influence the order in which edges are considered, which can significantly influence the performance (issue #197).

Improvements and fixes:

  • Introduced a brand new website (issue #35).

  • Many website URLs have changed due to various website structure changes (issues #35 and #73).

  • Various documentation/website textual improvements, style improvements and other changes (issues #35, #54, #188 and #236).

  • Various CIF tools now correctly handle a tuple projection index that is a constant reference with a name that is hidden by a tuple field name. In particular the CIF pretty printer now generates correct references for such indices (issue #258).

  • The CIF to CIF transformation to eliminate component definition/instantiation now correctly handles cases where component definitions are referred to via component instantiations (issue #244).

  • The CIF type checker now warns about some overly-convoluted references (issue #234).

  • The CIF simulator interactive GUI input mode now is fully responsive to termination requests when asking users for the next transition to take (issue #216).

  • The CIF simulator SVG visualizer functionality to save the image as an SVG file no longer crashes (issue #205).

  • The CIF simulator plot visualizer and SVG visualizer functionality to save as an image no longer ask duplicate overwrite questions (issue #223).

  • The CIF simulator no longer crashes when showing an SVG visualizer if the SVG file can’t be loaded (issue #207).

  • The CIF simulator trajectory data file option description has been improved (issue #248).

  • The CIF data-based synthesis tool now supports collecting additional statistics, i.e., maximum used BDD nodes, continuous BDD performance, and BDD cache statistics (issue #171).

  • The CIF data-based synthesis tool statistics option now has different option value names for various statistics. This is a backward incompatible change. Use bdd-gc-collect instead of bdd-gc, and bdd-gc-resize instead of bdd-resize (issue #235).

  • The CIF data-based synthesis tool documentation has various small improvements (issue #171).

  • The CIF to CIF linearization transformation now preserves more of the model structure. Groups are no longer eliminated, I/O file declarations are no longer pushed inwards, I/O declarations are no longer merged, and enumerations are no longer merged. The original automata are replaced by groups to allow keeping most declarations (e.g., algebraic variables) declared within them in their original scope, allowing them to keep their original absolute identities. Initialization predicates, marker predicates and invariants are also kept (close to) where they were. Linearization may now result in models with scope absolute references. Some warning messages now include proper absolute names. The documentation has been improved as well (issues #155 and #245).

  • The CIF to CIF linearization transformation now uses temporary location pointer variable names that are less likely to lead to name clashes and renamings (issue #245).

  • The CIF to CIF transformation to eliminate the use of locations in expressions now generates location pointer variables and enumerations with simpler names. This also affects the CIF to Supremica transformation (issue #245).

  • The CIF to CIF transformation to eliminate the use of locations in expressions has improved renaming warnings (issue #245).

  • The CIF PLC code generator has some backward incompatible name changes in the generated PLC code due to changes the CIF to CIF linearization transformation (issue #155).

  • The CIF PLC code generator has improved absolute names in error messages, generated comments, etc (issue #155).

  • The CIF PLC code generator now generates proper PLC names for CIF objects that have a CIF keyword as name (issue #249).

  • The CIF code generator has improved absolute names in generated comments, improved absolute original event names, and improved print declarations order in generated code (issue #155).

  • The CIF code generator has improved error and warning messages for Simulink code generation (issue #250).

  • The CIF code generator now takes into account all Java 11 keywords, literals and identifiers with special meaning for Java code generation (issue #238).

  • The CIF code generator now generates simpler and better performing code for (in)equality binary operators that compare enumeration literals (issue #247).

  • All CIF tools that support but ignore SVG input declarations now print a warning for specifications that contain SVG input declarations (issue #218).

  • The CIF to mCRL2 tool Generate value actions option has been improved to not generate any value actions if an empty option value is provided. This is a backward incompatible change. The documentation of the option has also been improved (issue #225).

  • The CIF to mCRL2 tool no longer eliminates enumerations to integers, but instead generates mCRL2 sorts for CIF enumerations. This allows referring to the enumeration literals by name when specifying properties to verify (issue #156).

  • The CIF to mCRL2 documentation on supported CIF specifications has been improved (issue #156).

  • The CIF to yEd transformation is now part of the miscellaneous tools. In the Eclipse ESCET IDE it can now be found in the CIF miscellaneous tools sub-menu (issue #188).

  • The CIF to yEd documentation has been updated for changes to recent yEd versions (issue #209).

Version 0.3 (2021-10-01)

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 (2021-07-07)

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 (2021-04-02)

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.