## 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 11.0 (2026-03-31)

CIF type checker

  - The CIF type checker now warns when a CIF model refers to an SVG image that has a text element with a `shape-inside` style property, an unsupported SVG version 2 feature (issue #1293).

CIF information generator

  - The CIF toolset now includes a new tool, the CIF information generator, which can be used to generate information about a CIF specification. The first version generates event participants information and event-enablement conditions. See the tool’s documentation for more information (issue #1378).

CIF simulator

  - The SVG visualizer and plot visualizer now no longer scale on hi-DPI displays on Windows. This prevents severe performance regressions observed in ESCET v10.0. ESCET v10.0 adopted the Eclipse IDE 2025-09, which comes with improved hi-DPI support on Windows, which caused the regressions (issue #1334).

  - The SVG input mode now supports resetting the simulation, by right clicking the SVG visualizer and choosing the relevant menu item (issue #1338).

  - The simulator has a new 'SVG input outline style' option to configure the style to use for the outline when hovering or clicking an interactive SVG element. It can be used to configure the hover and click colors as well as the stroke width. It can also be used to disable such outlines (issue #1352).

  - The simulator now uses a stroke width of 1.5 pixels for the outline when hovering or clicking an interactive SVG element, and properly compensates for scale factors when displaying such an outline (issue #1352).

  - The simulator now has an 'SVG input outline filters' option to selectively disable hover/click outlines for interactive SVG elements (issue #1352).

  - The SVG visualizer now uses the SVG filename, without path and file extension, as its tab name. This allows users to fully customize the tab names and more easily distinguish multiple SVG visualizer tabs (issue #1351).

  - The SVG visualizer no longer hangs when showing SVG files with inline images encoded using base64 that contain spaces (issue #1324).

  - The 'Debug output' option now additionally allows for CIF/SVG real-time timing debug output to be printed to the console (issue #1355).

  - The simulator has greatly improved performance in generating code and compiling it, leading to faster start times of the simulator, for CIF models with many events and automata, where most automata don’t have any state/event exclusion invariants in their locations (issue #1396).

  - The simulator has improved performance and robustness for writing generated code files, when the 'Debug output' option is configured to write the code generated for the CIF model to disk (issue #1394).

  - The simulator documentation has multiple small improvements and extensions (issues #1293, #1346 and #1352).

CIF explorer

  - The CIF explorer no longer crashes when exploring CIF models with assignments to tuples where the projection index is a field reference (issue #1379).

CIF data-based synthesis

  - The tool now supports CIF models with tuple-typed variables, tuple-typed expressions, multi-assignments on edges, partial variable assignments on edges, and internal user-defined functions that have multiple return types (issue #1218).

  - Slightly improved performance of the conversion of the CIF specification to the internal BDD representation, preventing a linear search for when synthesis variables need to be found for CIF objects (issue #1218).

  - Slightly improved performance of the conversion of the CIF specification to the internal BDD representation, on average for the CIF benchmarks, by using the reverse variable order for variables assigned on edges (issue #1218).

  - The tool now uses smaller BDD variable support sets for transition relations. This may affect performance, although the effect differs per model and the difference is generally minor (issue #1365).

  - The tool now converts updates on edges in a different way, which may impact the performance of the conversion of CIF models to the internal BDD representation. The effect differs per model, but the difference is generally minor (issue #1218).

  - The debug output for variable ordering has been fixed, for BDD variable indices of interleaved synthesis variables (issue #1360).

  - Improved the performance for printing assignments of synthesis edges in debug output (issue #1218).

  - The documentation about variable ordering has several small improvements (issue #1367).

  - The documentation about supported specifications now lists receiving values of supported types as supported. This was already supported, but is now properly documented (issue #1367).

CIF multi-level splitter

  - Fixed missing filenames of partial specifications in generated ToolDef scripts, for partial specifications that have only partially been checked for being supported by data-based synthesis (issue #1337).

  - The tool has improved performance and robustness for writing generated ToolDef scripts to disk (issue #1394).

  - The tool’s documentation has some small improvements and additions (issue #1310).

CIF relations collector

  - The CIF toolset now includes a new tool, the CIF relations collector, which analyzes a CIF specification for relations between its various elements and produces three Domain Mapping Matrices (DMMs) with the results. See the tool’s documentation for more information (issue #1310).

CIF to UPPAAL transformer

  - The transformation now generates a proper `false` guard for non-channel events that are not in the alphabet of the specification (issue #1354).

CIF to mCRL2 transformer

  - The transformer has improved performance and robustness for writing generated mCRL2 files to disk (issue #1394).

CIF controller properties checker

  - For the bounded response, confluence and non-blocking under control checks, the tool now supports CIF models with tuple-typed variables, tuple-typed expressions, multi-assignments on edges, partial variable assignments on edges, and internal user-defined functions that have multiple return types (issue #1218).

  - For the bounded response, confluence and non-blocking under control checks, the tool now has slightly improved performance of the conversion of the CIF specification to the internal BDD representation, preventing a linear search for when synthesis variables need to be found for CIF objects (issue #1218).

  - For the bounded response, confluence and non-blocking under control checks, the tool now has slightly improved performance of the conversion of the CIF specification to the internal BDD representation, by using the reverse variable order for variables assigned on edges (issue #1218).

  - For the bounded response, confluence and non-blocking under control checks, the tool now uses smaller BDD variable support sets for transition relations. This may affect performance, although the effect differs per model and the difference is generally minor (issue #1365).

  - For the bounded response, confluence and non-blocking under control checks, the tool now converts updates on edges in a different way, which may impact the performance of the conversion of CIF models to the internal BDD representation. The effect differs per model, but the difference is generally minor (issue #1218).

  - For the bounded response, confluence and non-blocking under control checks, the tool now has improved performance for printing assignments of edges in debug output (issue #1218).

  - The documentation about supported specifications had layout issues that have been fixed (issue #1367).

  - The documentation about supported specifications now lists receiving values of supported types as supported, for the bounded response, confluence and non-blocking under control checks. This was already supported, but is now properly documented (issue #1367).

CIF code generator

  - Generated JavaScript code and HTML pages now allow logging algebraic variables as part of logging states. It is disabled by default (issue #1381).

  - The HTML code generator now has a new 'HTML speeds' option, to configure the minimum, default and maximum speed for the execution of the generated HTML page. Generated HTML pages now have a slider to configure the speed (within the configured range), in their 'settings' menu (issue #715).

  - Some error messages of the 'HTML frequencies' option have textual fixes (issue #715).

  - Generated HTML pages have 'settings' menus with improved positioning and layout (issue #715).

  - Generated HTML pages now have their frequency and 'show SVG image' configuration inside the 'settings' menu (issue #715).

  - Generated Simulink code has been fixed, for time-dependent guard evaluation functions, which could have duplicate names, leading to compile errors (issue #1384).

  - Small improvements and a textual fix in the code generator documentation (issue #715).

CIF PLC code generator (stable)

  - Fixed a bug relating to generating code for tuple projections that use field names, which could occur under certain circumstances (issue #1366).

  - The generator has improved performance and robustness for writing generated PLC code to disk (issue #1394).

CIF PLC code generator (deprecated)

  - The generator has improved performance and robustness for writing generated PLC code to disk (issue #1394).

CIF examples

  - CIF FIFO example: The ToolDef scripts to check that the manually-written and synthesized supervisors are language equivalent, have several small improvements. Additionally, the script that uses mCRL2 for the check has been fixed (issue #769).

CIF website

  - The CIF history page had some broken links that have now been fixed (issue #1386).

CIF documentation

  - Small improvements and a textual fix for the FIFO example in the SBE in practice documentation (issue #769).

  - The CIF tutorial lesson on 'Inkscape' now documents that text areas are not supported, and the lesson also has some slight textual improvements (issue #1293).

  - The CIF reference manual now documents that CIF supports only SVG 1.1, not SVG 2, in the documentation about SVG file declarations (issue #1293).

### Version 10.0 (2025-12-19)

CIF language

  - CIF now features a `requirement:reachable` annotation, to specify reachability requirements, which can be used to specify stronger liveness requirements in combination with marking. See the documentation for more information (issue #1296).

CIF type checker

  - The type checker no longer crashes on checking for effectively-constant variables in automata with at least one discrete variable and at least one invalid addressable in an assignment of an edge of the automaton (issue #1295).

CIF simulator

  - The CIF simulator SVG visualizer has been fixed for handling of vendor-specific CSS properties starting with a `-`, such as Inkscape CSS properties, in `style` attributes of SVG elements. Vendor-specific properties are now removed to ensure that the Batik SVG library, used to render SVG images, properly processes the properties that follow the vendor-specific properties (issue #886).

  - The CIF simulator SVG visualizer now properly handles and reports CSS rendering errors, similar to SVG XML/DOM errors (issue #888).

  - The trace input mode documentation has been slightly improved (issue #1285).

CIF data-based synthesis

  - The tool now supports reachability requirements, ensuring a correct-by-construction controlled system where every reachable state adheres to all these requirements (issue #1296).

  - The tool now uses the 'Linearize (product with merge)' CIF to CIF transformation instead of the 'Linearize (product)' CIF to CIF transformation, for the creation of linearized hyper edge relations for variable ordering, and when converting edges to BDD transition relations. For some models, this can prevent exponential blow-ups in the number of linearized edges. On average, for the CIF benchmarks, there is a 12% reduction in the maximum number of nodes and a 45% reduction in the number of operations. However, the results differ per model, as is often the case with changes that affect variable ordering heuristics (issue #1203).

  - The tool has reduced memory usage for conversion of linearized edges to BDDs, by lazily creating and converting them one by one, rather than first creating all of them before they are converted to BDDs (issue #1203).

  - The tool now prevents duplicate work and, in certain situations, even prevents exponential blow-ups during the computation of variable relations by hyper-edge creators when collecting variables and/or comparison binary expressions (issue #1303).

  - The tool now no longer collects duplicate comparison binary expression instances in the legacy hyper-edge creator. This may affect variable relations and therefore variable ordering, although the CIF benchmarks are not affected (issue #1303).

  - The tool’s 'Fixed-point computations order' option now requires that the names of the fixed-point computations are separated by commas, rather than by dashes. This is a backwards incompatible change. If the old option syntax is used, a warning is printed (issue #1296).

  - The tool’s 'Fixed-point computations order' option now requires specifying four instead of three computations, to include the new fixed-point computations for the reachability requirements. For the old option syntax, the new fourth computation cannot be specified, and is always performed after the non-blockingness computation. For more information, see the tool documentation (issue #1296).

  - The tool now prints the configured statistics even if synthesis results in an empty supervisor (issue #1284).

  - The tool now prints the fixed-point computations timings in the order that the fixed-point computations are configured and performed, rather than always printing them in the default order (issue #1289).

  - The tool’s debug output for fixed-point computations has improved terminology (issue #1296).

  - The tool’s timing statistics now use better terminology for the fixed-point computation timings (issue #1296).

  - The tool’s 'BDD cache' statistic has been renamed to 'BDD node and operation' statistic. The tool’s `bdd-perf-cache` statistic name has similarly been renamed to `bdd-perf-node-op`. For backward compatibility, the old statistic name can still be used for the option, but will lead to a warning. Some of the node creation counts that are printed for this statistic have been renamed as well. Furthermore, the order of the node creation counts has changed in the printed output (issue #1304).

  - The tool’s performance documentation page has been extended with some easy-to-use high-impact recommendations to improve synthesis time (issue #1290).

  - The tool’s documentation page about statistics has various improvements and fixes related to the BDD node and cache statistic, has improved terminology use (BDDs are graphs, not trees), and is clearer about the 'Maximum used BDD nodes' statistic being very costly (issue #1304).

  - The tool’s documentation page about operation caches has multiple small improvements (issue #1304).

  - The tool’s documentation now links from the forward reachability page to the fixed-point computations order page, pointing out that it is by default performed last (issue #1290).

  - The tool’s option documentation has been slightly improved (issue #1290).

  - The tool’s documentation now has an extra paper reference that provides further details on the synthesis algorithm and how it handles the various CIF language constructs (issue #1296).

CIF to CIF transformer

  - A new CIF to CIF 'Linearize (product with merge)' transformation has been added. It preserves all behavior like 'Linearize (product)', but prevents blow-ups by merging linearized edges where possible (so, if it can statically detect that there is no non-determinism) like 'Linearize (merge)'. Compared to 'Linearize (product)' this can in certain cases prevent exponential blow-ups in the number of linearized edges (issue #1203).

  - The CIF to CIF 'Convert to interface' transformation now generates interface specifications with an `@@partial` annotation (issue #1280).

  - The CIF to CIF 'Eliminate state invariant' transformation no longer eliminates requirement state invariants (issue #1188).

  - The CIF to CIF 'Remove requirements' transformation now removes all reachability requirement annotations from the specification (issue #1296).

  - Small improvements/fixes for the documentation of the CIF to CIF 'Linearize' transformations (issue #1203).

CIF to mCRL2 transformer

  - The transformer no longer supports requirement state invariants (issue #1188).

  - The transformer now uses the 'Linearize (product with merge)' CIF to CIF transformation instead of the 'Linearize (product)' CIF to CIF transformation, in certain cases preventing exponential blow-ups in the number of linearized edges (issue #1305).

CIF controller properties checker

  - For the bounded response, confluence and non-blocking under control checks, the tool now uses the 'Linearize (product with merge)' CIF to CIF transformation instead of the 'Linearize (product)' CIF to CIF transformation, for the creation of linearized hyper edge relations for variable ordering, and when converting edges to BDD transition relations. For some models, this can prevent exponential blow-ups in the number of linearized edges. The results differ per model, as is often the case with changes that affect variable ordering heuristics (issue #1203).

  - For the bounded response, confluence and non-blocking under control checks, the tool has reduced memory usage for conversion of linearized edges to BDDs, by lazily creating and converting them one by one, rather than first computing all of them before they are converted to BDDs (issue #1203).

  - For the bounded response, confluence and non-blocking under control checks, the tool now prevents duplicate work and, in certain situations, even prevents exponential blow-ups during the computation of variable relations by hyper-edge creators when collecting variables and/or comparison binary expressions (issue #1303).

  - For the bounded response, confluence and non-blocking under control checks, the tool now no longer collects duplicate comparison binary expression instances in the legacy hyper-edge creator. This may affect variable relations and therefore variable ordering (issue #1303).

CIF code generator

  - The Simulink code generation documentation has been slightly improved (issue #1285).

CIF merger

  - The CIF merger now has an option to disable the removal of controller properties annotations of the input specifications, allowing these annotations to be included in the merged specifications. This option must be used with care, to ensure the annotations remain valid in the merged specifications. Consult the tool documentation for more information before using this new option (issue #1316).

CIF examples

  - Improved the CIF `button_lamp_timer` example to use decreasing timers instead of increasing ones, generate code using the new PLC code generator, perform controller properties checks before generating PLC code, and have improved console output from the PLC code generation script (issue #1316).

CIF benchmarks

  - The benchmarks overview generation script now has improved handling and reporting of missing values (issue #1284).

  - The 'bridge' benchmark model has some whitespace improvements (issue #1285).

CIF language tutorial

  - The annotations lesson has been split into multiple lessons (issue #1297).

  - The section about language extensions has been renamed to a section about synthesis, and the synthesis lesson has been split into multiple lessons (issue #1302).

CIF documentation

  - The CIF language tutorial lesson on synthesis has some fixes, textual improvements and small extensions (issue #1291).

  - The CIF documentation no longer contains zero width space characters generated by AsciiDoc, ensuring that there are no undesired line breaks caused by them (issue #1279).

  - The CIF documentation no longer links to `index.html` in link URLs, but instead now links to the parent that contains the `index.html`, resulting in nicer URLs (issue #1317).

  - The CIF history page has an updated paper reference (issue #1319).

  - Where relevant, the documentation now refers to the recommended PLC code generator rather than to the deprecated one (issue #1315).

### Version 9.0 (2025-09-30)

CIF language

  - CIF now features the `@@partial` built-in annotation. It can be added to partial specifications to suppress certain warnings that are often false positives for partial specifications. See the language tutorial and language reference manual for further information (issue #995).

CIF simulator

  - The trace input mode now supports a new type of command in trace files: input commands. An input command allows assigning a new value to an input variable during simulation (issue #710).

  - The plot visualizer no longer crashes if the specification has no initial state (issue #1250).

  - The plot visualizer is no longer shown if the specification has no initial state (issue #1250).

CIF to CIF transformer

  - The Eliminate state invariants CIF to CIF transformation no longer supports synchronizing events, events that are in the alphabet of multiple automata. You can eliminate synchronization by applying the Linearize (product) CIF to CIF transformation, before applying the Eliminate state invariants transformation (issue #1247).

CIF merger

  - The tool now has an option to control whether the resulting merged specification is a partial specification. By default, a merged specification is non-partial, but this can be changed by enabling the option (issue #995).

CIF data-based synthesis

  - The tool now supports CIF models with multiplication (binary `*` operator) and `if` updates (issue #1216).

  - The tool now supports internal user-defined functions and calls to such functions (with supported arguments), provided that the functions satisfy some conditions: they have exactly one return type; they don’t use recursive calls; they don’t contain `while` statements; they don’t perform assignments that may result in runtime out-of-range errors; they are only used in function calls (so not used as data); and only use boolean, ranged integer and enumeration types as parameter and return types, and as types of their local variables (issue #1237).

  - The tool now preserves valid cache entries when performing BDD garbage collection, improving synthesis performance (issue #1241).

  - The tool now has additional caching, to prevent duplicate work, and in certain situations even prevent exponential blow-ups. This concerns: the result of the pre-condition check for supported expression forms. It was already cached for references to algebraic variables being checked in predicates, but not yet in other expressions (issue #1233).

  - The tool now has improved performance for BDD variable ordering of models with many linearized edges and variable relations (issue #1258).

  - For the `nodes` BDD output mode, now only ranged integer types are used to represent BDD variable and node indices (issue #1238).

  - The tool no longer crashes on using the `sign` function on a `real`-typed value. It is still unsupported (except if it can be statically evaluated), but it now properly reports the problem rather than crashing (issue #1216).

  - The BDD library initial node table size option now requires a size that is at least 2, preventing crashes (issue #1246).

  - Improved the tool documentation for multi-assignments and partial-variable assignment constraints, using similar texts as in the CIF controller properties checker documentation (issue #1216).

  - Removed unnecessary precondition constraints that are implied by other constraints, from the tool documentation (issue #1216).

CIF event-based tools

  - The event-based language equivalence check has been fixed for the only difference being in the marking of initial states, or the language from initial states. Previously, this was not detected, leading the tool to wrongly conclude that the specifications were language equivalent (issue #1264).

  - The event-based language equivalence check has improved output in case the counter example concerns a pair of initial states (issue #1264).

  - The event-based language equivalence check and DFA minimization have improved readability of partitioning blocks printed as part of debug output (issue #1264).

CIF controller properties checker

  - The tool now supports, for the bounded response, confluence and non-blocking under control checks, CIF models with multiplication (binary `*` operator) and `if` updates (issue #1216).

  - The tool now supports, for the bounded response, confluence and non-blocking under control checks, internal user-defined functions and calls to such functions (with supported arguments), provided that the functions satisfy some conditions: they have exactly one return type; they don’t use recursive calls; they don’t contain `while` statements; they don’t perform assignments that may result in runtime out-of-range errors; they are only used in function calls (so not used as data); and only use boolean, ranged integer and enumeration types as parameter and return types, and as types of their local variables (issue #1237).

  - The tool now preserves, for the bounded response, confluence and non-blocking under control checks, valid cache entries when performing BDD garbage collection, improving synthesis performance (issue #1241).

  - The tool now has additional caching, for the bounded response, confluence and non-blocking under control checks, to prevent duplicate work, and in certain situations even prevent exponential blow-ups. This concerns: the result of the pre-condition check for supported expression forms. It was already cached for references to algebraic variables being checked in predicates, but not yet in other expressions (issue #1233).

  - The tool now has, for the bounded response, confluence and non-blocking under control checks, improved performance for BDD variable ordering of models with many linearized edges and variable relations (issue #1258).

  - The tool, for the bounded response, confluence and non-blocking under control checks, no longer crashes on using the `sign` function on a `real`-typed value. It is still unsupported (except if it can be statically evaluated), but it now properly reports the problem rather than crashing (issue #1216).

  - Removed unnecessary constraints that are implied by other constraints, from the tool documentation, for the bounded response, confluence and non-blocking under control checks (issue #1216).

CIF to mCRL2 transformer

  - The transformer now applies the Eliminate state invariants CIF to CIF transformation as preprocessing after linearization, rather than before linearization (issue #1247).

CIF code generator

  - Fixed JS/HTML code generated for real division (`/`) on integer arguments where the divisor is never zero (issue #1242).

  - Fixed real overflow error message of the `divide` utility function for generated JS/HTML code (issue #1242).

  - Generated JS/HTML code for the `divide` utility function has JSDoc improvements (issue #1242).

  - Small improvement for comments in generated JS/HTML code (issue #1262).

CIF PLC code generator (stable)

  - The tool now has improved precondition checking, skipping to report certain precondition violations if they are already covered by other violations (issue #1255).

CIF benchmarks

  - The `wafer_scanner` benchmark has improved tuned variable order settings (issue #1234).

CIF website

  - The CIF website home page now shows some news teasers and links to the new 'News' page with all the news (issue #982).

  - The CIF website home page now has a more-prominent SBE course link (issue #1240).

  - The CIF website home page now links to the 'Community' page (issue #982).

  - The CIF history page has been slightly improved (issue #982).

CIF documentation

  - The documentation about built-in annotations, in the CIF tutorial and CIF language reference manual, no longer categorizes the different annotations (issue #995).

  - The documentation pages for the different built-in annotations in the CIF language reference manual now have additional section headings (issue #995).

  - The 'Annotation' section of the Merge enumerations CIF to CIF documentation has been fixed (issue #1253).

  - The documentation has various small textual improvements (issue #1262).

### Version 8.0 (2025-06-30)

CIF general

  - CIF has a new logo and icon. The logo and icon have been updated on the CIF website, in the CIF documentation, and in the UI of the ESCET IDE (issue #1143).

  - All CIF tools can now be started in the ESCET IDE from right click menus of `.cifx` files and editors (issue #1229).

  - The documentation of all CIF tools now indicate that the tools can be started from `.cifx` files (issue #1229).

  - Various screenshots of CIF in the ESCET IDE, as part of the CIF documentation, CIF website and CIF examples, have been updated to include the ESCET icon introduced in release v3.0 (issue #1197).

CIF language

  - The order of the arguments of annotations may now be relevant, and in general arguments can thus no longer be freely re-ordered. Specific annotations may however allow the order to be irrelevant. For `@doc` annotations the argument order is relevant. For `@state` and `@controller:properties` annotations the argument order is not relevant (issue #1192).

CIF text editor

  - The CIF text editor now has greatly improved performance when the CIF model has many warnings or errors. This may in certain cases also prevent the IDE from freezing indefinitely (issue #995).

CIF type checker

  - The CIF type checker now warns about discrete variables that are effectively constant, if this can be detected statically (issue #1163).

  - The CIF type checker no longer crashes when checking certain annotations in invalid models (issue #1175).

CIF data-based synthesis

  - Synthesis now supports CIF models with discrete and input variables that have integer types that allow negative integer values (issue #458).

  - Synthesis now supports CIF models with discrete and input variables that have integer types that include value 2,147,483,647 as possible value. Instead, now the total number of possible values of the integer type must not exceed 2,147,483,647 (issue #458).

  - Synthesis now supports CIF models with expressions that contain negative integer literals and unary `-` operations (issue #458).

  - Synthesis now supports CIF models with expressions that contain binary `-` operations, regardless of where the binary subtractions are used, as long as the arguments of the binary subtractions are supported expressions as well. This removes the restriction that binary subtractions were only supported directly in the right-hand sides of assignments (issue #458).

  - Synthesis now supports CIF models with expressions that use the `abs`, `sign`, `max` or `min` standard library functions on supported arguments (issue #1216).

  - Synthesis now has improved performance in certain cases for CIF models with `-` (binary), `+` (binary), `div`, or `mod` operations (issue #458).

  - Synthesis now has additional caching, to prevent duplicate work, and in certain situations even prevent exponential blow-ups. This concerns: the result of the pre-condition check for supported expression forms, for references to algebraic variables; the 'plants refer to requirements check' result for references to constants, discrete variables, continuous variables and algebraic variables; and the conversion result for converting references to algebraic variables in predicates and other expressions to the internal BDD representation (issue #1187).

  - Synthesis now more efficiently creates BDD predicates for variables with many possible values. This concerns initial value predicates for discrete variables initialized using `in any`, update relation predicates for input variables, and implicit variable-never-out-of-range requirements (issue #1199).

  - Synthesis now uses less memory when converting the synthesis result back to a CIF specification, in case the `nodes` BDD output mode is used (issue #1227).

  - Removed some unnecessary computations related to BDD variable pairings, which may make synthesis faster, although it is unlikely this will be noticeable in practice (issue #1178).

  - The advanced variable ordering option has a new variable orderer, the repeat orderer, that allows to repeatedly apply a given orderer a number of times (issue #1165).

  - The custom variable ordering (for both the basic and advanced options) no longer crashes or produces invalid results for name patterns with characters that have a special meaning in Java regular expressions (issue #1176).

  - The custom edge ordering no longer crashes or produces invalid results for name patterns with characters that have a special meaning in Java regular expressions (issue #1185).

  - Fixed the error message that is shown if an invalid custom BDD variable order is used (issue #1176).

  - Fixed the debug output of the saturation exploration strategy for reachability computations, for variables in the edges/variables matrix, in case of custom variable orders where different CIF variables are interleaved (issue #1205).

  - The documentation about supported specifications has been reduced and simplified (issue #458).

  - Fixed a small issue in the advanced variable ordering documentation, for the reverse orderer (issue #1165).

CIF event-based toolset

  - The event-based toolset documentation has some small textual improvements (issue #1229).

CIF multi-level splitter

  - The CIF toolset now includes a new tool, the CIF multi-level splitter, which enables a form of non-monolithic synthesis. The multi-level splitter can be used to split a CIF specification into a multi-level tree of smaller co-operating partial specifications. The partial specifications can be synthesized individually, which is typically more efficiently than synthesizing the entire original specification. The resulting supervisors, synthesized from the partial specifications, can then together be used to control the system. See the tool’s documentation for more information (issue #318).

CIF to mCRL2 transformer

  - The tool now supports CIF models with multiple initial states. That is, it supports discrete variables with multiple initial values as well as automata with multiple initial locations. See the tool’s documentation for more information (issue #1220).

  - The tool now supports CIF models with input variables (issue #1220).

  - The tool now supports CIF models with arbitrary initialization predicates in locations, so also those that are not statically-evaluable. It now also supports CIF models with initialization predicates in components, so outside locations. And it supports models without an initial state. See the tool’s documentation for more information (issue #1220).

  - The tool now supports CIF models with state/event exclusion invariants (issue #1220).

  - The tool now supports CIF models with state invariants that do not depend on input variables (issue #1220).

  - The tool now generates mCRL2 files with improved header comments and improved comments for value actions (issue #1220).

  - The tool now uses the proper tool name in precondition violation reports (issue #1220).

  - The tool no longer performs the Add default initial values CIF to CIF transformation as pre-processing (issue #1220).

  - The description of the tool’s Generate 'value' actions option has been fixed (issue #1220).

  - The tool’s documentation has some small improvements and fixes (issues #1182 and #1220).

CIF controller properties checker

  - The tool now supports, for the bounded response, confluence and non-blocking under control checks, CIF models with discrete and input variables that have integer types that allow negative integer values (issue #458).

  - The tool now supports, for the bounded response, confluence and non-blocking under control checks, CIF models with discrete and input variables that have integer types that include value 2,147,483,647 as possible value. Instead, now the total number of possible values of the integer type must not exceed 2,147,483,647 (issue #458).

  - The tool now supports, for the bounded response, confluence and non-blocking under control checks, CIF models with expressions that contain negative integer literals and unary `-` operations (issue #458).

  - The tool now supports, for the bounded response, confluence and non-blocking under control checks, CIF models with expressions that contain binary `-` operations, regardless of where the binary subtractions are used, as long as the arguments of the binary subtractions are supported expressions as well. This removes the restriction that binary subtractions were only supported directly in the right-hand sides of assignments (issue #458).

  - the tool now supports, for the bounded response, confluence and non-blocking under control checks, CIF models with expressions that use the `abs`, `sign`, `max` or `min` standard library functions on supported arguments (issue #1216).

  - The tool now has, for the bounded response, confluence and non-blocking under control checks, improved performance in certain cases for CIF models with `-` (binary), `+` (binary), `div`, or `mod` operations (issue #458).

  - The tool now has, for the bounded response, confluence and non-blocking under control checks, additional caching, to prevent duplicate work, and in certain situations even prevent exponential blow-ups. This concerns: the result of the pre-condition check for supported expression forms, for references to algebraic variables; and the conversion result for converting references to algebraic variables in predicates and other expressions to the internal BDD representation (issue #1187).

  - The tool now more efficiently creates BDD predicates for variables with many possible values. This concerns initial value predicates for discrete variables initialized using `in any`, and update relation predicates for input variables (issue #1199).

  - The bounded response check no longer crashes in certain cases where bounded response doesn’t hold and there are very many possible states where there is no bounded response. There was already a limit on the number of states to print, but the calculation could result in integer overflow, which could lead to crashes. Some of such cases where already fixed in release v7.0, and the remaining cases have now been fixed as well (issue #1225).

  - The Maximum number of printed cycle states option now accepts 2,147,483,639 as the largest number of cycle states to print, instead of 2,147,483,637 (issue #1225).

CIF PLC code generator (stable)

  - Real literal values in generated code now have no more precision than is supported by the particular target for which the code is generated. This may prevent warnings when the generated code is imported into PLC environments. As a result of this change, real literals may now be generated in a different syntax, even if those literals were already within the precision of the target (issue #1146).

CIF documentation

  - The CIF history page’s ESCET papers section now includes an extra paper reference (issue #1230).

### Version 7.0 (2025-03-31)

CIF language

  - The CIF language now features input parameters, a new kind of parameters for component definitions (automaton and group definitions). For such parameters, only input variables and input parameters can be used as arguments in component instantiations. A primary use case for using input parameters instead of algebraic parameters, is that input parameters can be assigned by SVG input mappings within component definitions. See for more information the CIF tutorial lesson on automaton definition parameters, which has been extended to include input parameters (issue #1118).

  - SVG input mappings with updates are no longer an experimental language feature. It is now considered a stable language feature (issue #1085).

  - Using a `min` or `max` function with integer arguments now results in a ranged `int` value if at least one argument has a ranged `int` type. Previously, they both had to have a range for the result to be ranged. This for instance allows to convert the value of a variable `x` with a rangeless `int` type to a ranged `int` value of type `int[0..1000]` using `max(0, min(x, 1000))` (issue #1129).

CIF simulator

  - The plot visualizer no longer crashes if the simulator is started as a command line tool and the plot visualizer window is resized, not even when the window is resized to an empty size. Note that this does not affect the CIF simulator plot visualizer in the ESCET IDE; not even if the plot visualizer is put into a separate window (issue #1142).

  - The simulator documentation now documents the default value of the simulator’s complete mode option (issue #1133).

  - The simulator documentation now indicates that, with complete mode enabled, there are situations where not all possible transitions are printed (issue #1134).

CIF explorer

  - The CIF explorer has various improvements and fixes relating to the precondition that there may not be too many initial states. These changes primarily prevent crashes and incorrect results. They may also lead to better estimates of the possible number of initial states, as well as improved output in case of a precondition violation. Performance of computing the initial states has also been improved in certain cases, but the tool could now give less feedback in case there is no initial state (issue #1110).

CIF data-based synthesis

  - The tool may internally produce simpler predicates, such as `true or X` now becoming `true`, in the conversion of the specification to BDDs. This may lead to differences in conversion performance, variable ordering, and debug output. The benchmarks shown only minimal changes (less than 0.1% change in memory/time). However, for the `wafer_scanner_n1` benchmark, synthesis requires about 12% less BDD operations (issue #1154).

  - Models with discrete variables or input variables with an integer type with a range that includes value 2,147,483,647 (the maximum integer value) are no longer supported, preventing crashes (issue #903).

  - Debug output for models with large integer values is now proper, as it for instance no longer shows overflown values, and has improved readability by including thousand separators (issue #903).

  - Debug output for variable ordering now shows BDD variable indices in the variable order overview tables (issue #903).

CIF controller properties checker

  - The tool may internally produce simpler predicates, such as `true or X` now becoming `true`, in the conversion of the specification to BDDs. This may lead to differences in conversion performance, variable ordering, and debug output (issue #1154).

  - Models with discrete variables or input variables with an integer type with a range that includes value 2,147,483,647 (the maximum integer value) are no longer supported, preventing crashes (issue #903).

  - Debug output for models with large integer values is now proper, as it for instance no longer shows overflown values, and has improved readability by including thousand separators (issue #903).

  - Debug output for variable ordering now shows BDD variable indices in the variable order overview tables (issue #903).

  - The bounded response check no longer crashes when bounded response doesn’t hold and there are too many possible states where there is no bounded response. There was already a limit on the number of states to print, but the calculation could result in integer overflow, which could lead to crashes. This has been fixed (issue #1138).

  - The tool is now more responsive to termination requests (issue #996).

CIF code generator

  - The generator now has an HTML frequencies option to configure the minimum, default and maximum frequency for generated HTML pages. The frequencies can be changed, to for instance ensure that the execution is fluent and accurate enough. See the documentation of the option for further information (issue #1127).

  - Generated HTML pages now properly handle SVG output mappings for all attributes, regardless of whether the attributes are supported as SVG presentation attributes and/or CSS style properties, regardless of which of those takes precedence, and regardless of whether they are already present on the element or not (issue #715).

  - Generated HTML pages now properly handle SVG output mappings where the value is not a valid CSS value for the corresponding CSS style property, ensuring that the last-set valid value is not preserved (issue #1157).

  - Fixed a typo in the HTML code generation documentation (issue #1127).

CIF PLC code generator (stable)

  - The generator now supports models that use the `ceil`, `floor`, `round`, `scale` and `sign` functions (issue #1109).

  - The ESCET IDE now ships with CIF PLC code generator 'self-certification' tests. There is an extra option on the Welcome screen to import them. The import wizard can also be accessed via File New Example. These 'self-certification' tests can be used to test the PLC code generator in external PLC development environments. See also the tool’s documentation for more information (issues #1104 and #1109).

  - Fixed a syntax highlighting issue in the code generator’s documentation (issue #1147).

CIF to CIF transformer

  - A new Eliminate state invariants CIF to CIF transformation has been added. It comes in three variants: one that eliminates all state invariants, one that only eliminates plant state invariants, and one that only eliminates supervisor state invariants. For more information, see the documentation of the new transformation (issue #1087).

  - The Eliminate 'if' updates CIF to CIF transformation no longer supports CIF specifications with component definitions/instantiations. Eliminate component definitions/instantiations using the corresponding CIF to CIF transformation before applying the Eliminate 'if' updates transformation (issue #1118).

  - The Anonymize names CIF to CIF transformation now uses the `iparam` prefix when renaming input parameters (issue #1118).

  - Fixed some typos in the CIF to CIF transformer documentation (issues #1106 and #1118).

  - The Linearize (merge) and Linearize (product) transformations may produce simpler linearized predicates, such as `true or X` now becoming `true`, for edge guards, urgency guards, and initialization/marker predicates from locations (issue #1154).

  - The Eliminate monitors transformation may produce simpler predicates, such as `true or X` now becoming `true`, for edge guards and send values (issue #1154).

CIF to Supremica transformer

  - The transformer may produce simpler Supremica predicates, such as `1 | X` now becoming `1`, for edge guards and state invariant predicates (issue #1154).

CIF to UPPAAL transformer

  - The transformer may produce simpler UPPAAL predicates, such as `true || X` now becoming `true`, for edge guards (issue #1154).

CIF website

  - The CIF website now shows the CIF logo (issue #1140).

CIF documentation

  - The CIF reference manual has small textual improvements (issue #1071).

  - The Developers section of the documentation now contains a page about how to reliably extract information from a CIF specification, by converting the CIF specification to XML and using XML queries (issue #1071).

### Version 6.0 (2024-12-20)

CIF type checker

  - Warnings are now added for SVG output mappings that overwrite (rather than set) the `transform` attribute of an SVG element (issue #1021).

  - Warnings are now added for SVG output mappings with a transformation on an element whose ancestor has a `matrix`, `rotate`, `scale` or `skew` transformation or a variant of them (issue #1021).

  - Warnings are now added for all convoluted references to addressables in updates of edges of automata, regardless of whether the reference is via a component instantiation or component parameter or not (issue #227).

CIF text editor

  - The dark theme now uses a lighter red color for string literals, for better contrast (issue #966).

CIF simulator

  - The simulator now supports SVG input mappings with updates to input variables (issues #227 and #778).

  - The simulator now has an Execution mode option, to enable execution mode. Execution mode is disabled by default. With execution mode, the simulator adheres to the execution scheme defined by the CIF controller properties checker. See the documentation of the new option for further information (issue #1045).

  - The simulator now has a new Non-urgent events option that replaces the Environment events option, which is no longer supported (issue #1063).

  - The simulator can no longer execute external user-defined functions asynchronously; it now always executes them synchronously. This means that termination requests are no longer processed during the execution of external user-defined functions. The simulator’s External functions asynchronous execution option is no longer supported (issue #656).

  - The simulator runtime error messages for variables getting assigned out of bounds values now use absolute variable names for clarity (issue #227).

  - The simulator documentation has some small improvements and fixes (issues #1063 and #1090).

CIF data-based synthesis

  - When using the saturation exploration strategy for reachability computations, the debug output now includes an edges/variables matrix that gives insights into the complexity of the model (issue #957).

  - A BDD variable leak in computing edge support variable sets has been fixed, which may slightly improve synthesis performance (issue #1006).

CIF controller properties checker

  - The confluence check’s performance has been greatly improved, by interleaving the internally added 'zero' BDD variables (issue #1006).

  - The confluence check is now more responsive to termination requests (issue #1008).

  - The confluence check now produces improved debug output in case the model has exactly one controllable event (issue #1007).

  - The bounded response check now prints the edges that are part of cycles, in case bounded response doesn’t hold due to cycles (issue #621).

  - The bounded response check now prints states that are part of cycles, in case bounded response doesn’t hold due to cycles. By default 10 states are printed, but this can be configured through the new Maximum number of cycle states option (issue #621).

  - The bounded response check’s debug output has been slightly improved (issue #621).

  - The non-blocking under control check’s debug output now includes an edges/variables matrix that gives insights into the complexity of the model (issue #957).

  - The performance of the bounded response, confluence and non-blocking under control checks may have slightly improved, due to fixing a BDD variable leak in computing edge support variable sets (issue #1006).

  - The order of the checker’s options has changed. It now first lists all enablement options, before their more detailed configuration. This now matches the order in the documentation (issue #621).

  - The documentation now explains for each check that prints additional details what details are printed (issue #621).

  - The documentation has some small fixes (issue #1045).

CIF code generator

  - The generator now by default generates HTML, not Simulink code (issue #715).

  - The generator now automatically adapts the default code prefix to be a valid prefix, preventing having to specify a custom code prefix. If the user specifies a custom code prefix, it is not automatically adapted and thus still a valid CIF identifier must be specified manually (issue #1084).

  - The generator for HTML now supports SVG input mappings with updates to input variables (issue #227).

  - The generator for HTML now produces code that initializes input variables to their default values (issue #227).

  - The generator for HTML now produces code that includes input variables and their values when printing states to the log panel (issue #227).

  - The generator for HTML now produces code that properly executes SVG input events before uncontrollable events (issue #227).

  - The generator for HTML now produces code that processes all SVG image interactive element clicks in a single execution of the corresponding event loop, even if certain SVG input events are not enabled, thus ensuring that all clicks have been processed before executing the uncontrollable events event loop (issue #227).

  - The generator for HTML now produces code that logs runtime errors to the log panel (issue #715).

  - The generator for HTML now produces code that results in a runtime error if an SVG input mapping does not map to an event at runtime (issue #1069).

  - The generator for HTML now produces code with nicer layout for SVG input mappings with event mappings (issue #1069).

  - The generator’s documentation has some textual improvements (issues #227 and #1045).

  - The generator for JavaScript and HTML now wraps runtime errors in more context, making them easier to understand (issue #715).

  - The generator for JavaScript and HTML now generates code with improved type hint consistency in generated JSDocs (issue #715).

  - The generator for Java now takes the new keywords of Java 21 into account (issue #656).

  - The generator now properly handles type declarations, by eliminating them as preprocessing. This among others fixes a bug for generation of out of range checks for variables with as type a type declaration with a ranged integer type (issue #998).

  - The generator now properly handles tuple field projections in case of compatible tuple types (issue #998).

CIF PLC code generator (deprecated)

  - The CIF PLC code generator that was previously labeled as the 'stable' version, is now the 'deprecated' version (issue #1092).

CIF PLC code generator (stable)

  - The CIF PLC code generator that was previously labeled as the 'experimental' version, is now the 'stable' version. Support for some targets is still experimental. See the tool’s documentation for further information (issue #1092).

  - The new Input/output code form option can be used to generate functions for reading inputs and writing outputs, rather than having the code be generated in the main program (issue #1055).

  - The Event transitions form option now has an extra possibility. Use Event code is combined into a function by event controllability and CIF scope to obtain event functions for all (un)controllable events in each scope (issue #1031).

  - The generator now writes, for the S7 target, a text file `derived_type_dependencies.txt`. The file contains the dependency information between structs, and from structs to enumerations if the latter types are used in a struct. The information from this file can be used to determine the order in which to create program blocks from the various data types (issue #944).

  - The `loopsKilled` variable in the generated code is now named `loopsExhausted`. Its existence and objective are now documented in the generator’s documentation (issue #1013).

  - The model overview has been moved to the very end of the body of the generated main program. Its title has also been improved (issue #1022).

  - The generated code now has improved documentation and comments for PLC internal variables, i.e., current-location variables and edge selection variables for automata (issue #1023).

  - Due to internal changes in the generator, the order of the declarations in the generated code may be different (issue #993).

  - The generator no longer crashes on models with nested arrays. Note that nested arrays were already unsupported, as indicated in the documentation (issues #1017 and #1025).

  - The generator now correctly handles compatible enumerations if enumerations are kept in the generated code (issue #1018).

  - The generator now provides improved error messages when reading invalid CSV files, in general, as well as specifically when not all rows have the same number of fields (issue #1044).

  - Fixed a typo in the command line description of the generator’s Simplify values option (issue #1055).

  - Improved the command line and GUI option descriptions of the generator’s PLC maximum iterations option (issue #1055).

  - For the TwinCAT target, the generator now properly considers (in)equality and comparison operators to have the same priority, where applicable forcing the use of parentheses in the generated code (issue #1040).

  - For the TwinCAT target, the generated code now properly uses `VAR` for temporary variables in functions, rather than `VAR_TEMP` (issue #1038).

  - For non-S7 targets, if any code is generated in functions rather than in the main program, state variables are now stored in a global variable list instead of in the main program (issue #1039).

  - For non-S7 targets, the generated code now correctly ensures short-circuit evaluation semantics for the `=>`, `and` and `or` binary operators (issue #1037).

  - For non-S7 targets, the generated code no longer has type extensions for the `SEL` function (issues #1036 and #1041).

  - For the S7 targets, `any_derived` is now considered a keyword, rather than the misspelled `and_derived` keyword (issue #679).

  - For the S7-1200/1500 targets, the generator now considers the same naming restrictions as for the S7-300/400 targets (issue #1061).

  - The documentation for the S7 targets now lists a potential fix for the System Fault PLC error (issue #1034).

  - Various documentation improvements (issues #1044, #1045 and #1055).

CIF merger

  - The documentation has been slightly improved (issue #1045).

CIF to CIF transformer

  - A new Convert to interface transformation is now available that converts a CIF specification to its interface. It comes in two flavors, one to generate a full interface and one to generate a reduced interface (issues #1067 and #1086).

  - The Anonymize names, Eliminate groups and Lift events transformations now remove controller properties annotations (issue #1001).

  - The Linearize (merge) transformation no longer removes controller properties annotations (issue #1001).

  - The documentation of the Linearize transformations has been improved (issue #1045).

CIF to Supremica transformer

  - Fixed a typo in the command line description of the tool’s Eliminate enumerations option (issue #1066).

CIF examples

  - Fixed a duplicate section name in the bridge example readme (issue #1081).

CIF documentation

  - The CIF/SVG visualization and interaction documentation that is not specific to the simulator has been moved from the CIF simulator documentation to the CIF language tutorial and CIF language reference manual (issue #1015).

  - The print declarations and text formatting documentation that is not specific to the simulator has been moved from the CIF simulator documentation to the CIF language tutorial and CIF language reference manual (issue #1048).

  - The CIF tutorial lesson on input variables now has an example of using input variables with SVG interaction, by means of SVG input mappings with updates (issue #227).

  - The CIF tutorial lesson on imports has been slightly improved (issue #1045).

  - The CIF documentation on the ESCET website and in the Eclipse help now use a darker green color for numbers in source code, for better contrast (issue #1030).

### Version 5.0 (2024-10-03)

Language changes:

- Annotations are now a stable CIF language feature (issue #869).

- The semantics of the uncontrollable/controllable events bounds of the controller properties annotation have changed. They no longer represent bounds on the lengths of sequences of uncontrollable/controllable events. Instead, they now represent bounds on the number of iterations of the uncontrollable/controllable event loops, under the assumption of the execution scheme prescribed by the controller properties checker (issue #971).

Deprecations and removals:

- The CIF to mCRL2 transformer has been re-implemented and is now based on first linearizing the CIF specification. It generates mCRL2 models with a single process. Therefore, the options related to specifying and debugging instance trees have been removed. For further details, see below (issue #352).

- The CIF to mCRL2 transformer’s Generate value actions option has been renamed from `--read-values`/`-r` to `--value-actions`/`-v` (issue #352).

- The CIF data-based synthesis tool’s 'Edge workset algorithm' option is no longer supported, and is replaced by the new 'Exploration strategy' option. This new option is also described below (issue #947).

Improvements and fixes:

- The CIF type checker now reports component definition parameter count versus instantiation argument count mismatches on the component definition reference, rather than on the instantiation name (issue #973).

- Various CIF tools have improved termination checking performance (issue #936).

- CIF tools that fail to save a CIF XML file now give the correct error message (issue #881).

- CIF tools that write CIF files have improved performance, especially when using Eclipse platform paths (issue #42).

- The CIF simulator has improved output in case of precondition violations (issue #424).

- The CIF to yEd transformer has improved output in case of precondition violations (issue #424).

- The CIF to CIF transformer’s linearization transformations have an improved unsupported message in case linearization is applied to a CIF specification without automata (issue #944).

- The CIF to CIF transformer’s linearization transformations now produces models with the elements of the specification in a certain specific order, for compatibility with the execution scheme prescribed by the CIF controller properties checker (issue #935).

- The CIF to CIF transformer’s linearize merge transformation now removes the controller properties annotation from the input specification, if present (issue #896).

- The CIF to CIF transformer’s convert (un)controllable events to (un)controllable transformations now remove the controller properties annotation from the input specification, if present (issue #896).

- The CIF to CIF transformer’s remove requirements transformation now removes the controller properties annotation from the input specification, if present (issue #896).

- The CIF explorer has improved output in case of precondition violations (issue #424).

- The CIF explorer precondition check for not having too many potential initial states has been improved (issue #424).

- The CIF merger now removes the controller properties annotation from the input specification, if present (issue #896).

- The CIF data-based synthesis tool now has a new 'Exploration strategy' option, featuring not only regular fixed edge order and the workset algorithm, but also a new third strategy, the saturation strategy. This new saturation strategy improves the performance of reachability computations. On average, for the CIF benchmark models, synthesis performance is improved 14.5 times, although the results differ per model. Saturation is now the new default exploration strategy. The 'Edge workset algorithm' option is no longer supported (issues #947, #957, #958 and #992).

- The CIF data-based synthesis tool now has improved debug and warning output (issues #938 and #953).

- The CIF data-based synthesis tool now has improved numbers for the number of states in the controlled system, and the number of true paths in the debug output of BDDs for large predicates. It indicates more precise numbers for larger BDDs, and no longer indicates wrong numbers for very large BDDs. This comes at the cost of computing these numbers taking longer, and the cache for computing these numbers requiring more memory (issue #951).

- The CIF data-based synthesis tool no longer crashes when a termination request is given while converting updates to BDDs (issue #909).

- The CIF data-based synthesis tool has improved output in case of precondition violations (issue #424).

- The CIF data-based synthesis tool now supports CIF specifications with predicates that are not one of the supported forms, but that can be statically evaluated to a single value without giving evaluation errors (issue #424).

- The CIF data-based synthesis tool’s 'BDD debug max paths' option now supports any non-negative integer value (however large it is). The value may no longer be entered as a real value, e.g., no more '1e38' (issue #951).

- The CIF data-based synthesis tool now removes the controller properties annotation from the input specification, if present (issue #896).

- The CIF data-based synthesis tool has a fix for an integer overflow bug, which may trigger while checking for the need to resize the node array, causing large node arrays to grow unnecessary (issue #947).

- The CIF controller properties checker now uses the saturation strategy for reachability computations, improving the performance of the non-blocking under control check (issues #947, #957 and #958).

- The CIF controller properties checker now computes confluence internally using BDDs rather than MDDs, for better performance (issues #693, #695 and #997).

- The CIF controller properties checker now computes bounded response differently, using the execution scheme, which improves the performance of the check, and generally leads to lower bounds (issue #971).

- The CIF controller properties checker no longer supports non-determinism for controllable events, regardless of what checks are performed, as was already documented (issue #695).

- The CIF controller properties checker now converts the input CIF specification to an internal representation before each check, rather than at the start. This may reduce the required memory if multiple internal representations are required (issue #971).

- The CIF controller properties checker now warns if the input specification has no input variables, indicating that the hardware mapping is missing (issue #977).

- The CIF controller properties checker has improved output in case of precondition violations (issue #424).

- The CIF controller properties checker has improved debug output (issues #695, #937 and #938).

- The CIF controller properties checker now has improved numbers for the number of true paths in the debug output of BDDs for large predicates. It indicates more precise numbers for larger BDDs, and no longer indicates wrong numbers for very large BDDs. This comes at the cost of computing these numbers taking longer, and the cache for computing these numbers requiring more memory (issue #951).

- The CIF controller properties checker no longer has indented empty lines in its console output (issue #406).

- The CIF controller properties checker no longer crashes when a termination request is given, and is more responsive to termination requests (issues #909 and #964).

- The CIF controller properties checker for bounded response and non-blocking under control, now supports CIF specifications with predicates that are not one of the supported forms, but that can be statically evaluated to a single value without giving evaluation errors (issue #424).

- The CIF controller properties checker for bounded response and non-blocking under control, has a fix for an integer overflow bug, which may trigger while checking for the need to resize the node array, causing large node arrays to grow unnecessary (issue #947).

- The CIF controller properties checker documentation now documents the prescribed execution scheme (issue #970).

- The CIF code generator no longer supports specifications with events that are not controllable or uncontrollable (issue #628).

- The CIF code generator now generates code that adheres to the execution scheme prescribed by the CIF controller properties checker. As a result of this, some parts of the generated code are now in a different order. Also, the generated code now has separate event loops for SVG input events (HTML output only), uncontrollable events, and controllable events. Furthermore, if in an event loop a transition for an event is executed, the iteration now continues with the next event, rather than starting at the first event in a next iteration. Finally, in generated C code, the configurable value `MAX_NUM_EVENTS` has been renamed to `MAX_NUM_ITERS` (issues #628 and #970).

- The CIF code generator now generates code that avoids ambiguity between event and edge indices (issue #952).

- The CIF code generator now generates code with improved comments (issue #952).

- The (still experimental) new CIF PLC code generator now allows to custom I/O variable names in the I/O table file, using an optional fourth column (issue #897).

- The (still experimental) new CIF PLC code generator now allows algebraic variables to be used as outputs in the I/O table file (issue #956).

- The (still experimental) new CIF PLC code generator will now by default, through its 'PLC maximum iterations' option, compute the iteration limits from the bounds captured in the bounded response information of the input specification’s controller properties annotation, if available. It still has a fallback to infinite loop bounds, and the limits can still be specified manually (issues #816 and #965).

- The (still experimental) new CIF PLC code generator now supports documentation annotations of various CIF objects and includes them in the generated PLC code (issue #814).

- The (still experimental) new CIF PLC code generator now allows differently sized types for the I/O port and the corresponding CIF variable (issue #884).

- The (still experimental) new CIF PLC code generator now generates code that adheres to the execution scheme prescribed by the CIF controller properties checker. As a result of this, some parts of the generated code may be in a different order (issues #935 and #970).

- The (still experimental) new CIF PLC code generator now warns about generating PLC code for a specification that was not checked using the CIF controller checker, or if it was checked but some of the checks didn’t hold (issues #816 and #965).

- The (still experimental) new CIF PLC code generator now allows generating event transition code in separate functions. That is, it has a new 'Event transitions form' option, to allow generating all event code in the `MAIN` program (still the default), or in a function per event (avoids issues if code becomes large). Due to these changes, some generated code may now be in a different order in the generated PLC code (issues #912, #935, #980 and #986).

- The (still experimental) new CIF PLC code generator has various improvements for generated edge selection variables, such as not generating one for automata that don’t need it, improved naming, using smaller data types if possible, and starting at zero rather than one to more often allow using smaller data types (issue #923).

- The (still experimental) new CIF PLC code generator has an improved option description for the 'PLC maximum iterations' option (issue #965).

- The (still experimental) new CIF PLC code generator has improved error messages in case invalid values are provided for the 'PLC maximum iterations' option (issue #965).

- The (still experimental) new CIF PLC code generator has improved handling of enumerations (including those generated for locations of automata), using bit-like types rather than integers, using smaller types when possible, and having more direct traceability to the input CIF model (issue #934).

- The (still experimental) new CIF PLC code generator has improved comments for applying updates of monitor automata (issue #814).

- The (still experimental) new CIF PLC code generator has improved layout for the model overview in the generated code (issue #814).

- The (still experimental) new CIF PLC code generator has improved names for generated PLC tuple types, in general, but especially for CIF tuple types that are part of a CIF type declaration (issue #679).

- The (still experimental) new CIF PLC code generator has improved names in the generated code (issue #945).

- The (still experimental) new CIF PLC code generator has improved loop killed detection in the generated code (issue #965).

- The (still experimental) new CIF PLC code generator now ensures that generated S7 temporary variable tables have the required minimum size (issue #860).

- The (still experimental) new CIF PLC code generator now avoids generating parentheses around real literal values for variable and constant declarations (issue #877).

- The (still experimental) new CIF PLC code generator now checks that only boolean, integer and real-typed discrete and input variables in a CIF specification are used for I/O, regardless of whether explicit PLC types are given in the I/O table file (issue #884).

- The (still experimental) new CIF PLC code generator no longer crashes on reading an invalid I/O table file, but instead gives a proper error message (issue #967).

- The (still experimental) new CIF PLC code generator now generates correct code for constants having the value of another constant as its value, if enumeration literals are eliminated to constants (issue #969).

- The (still experimental) new CIF PLC code generator now generates code based on the correct operator priority for the binary subtraction operator (issue #968).

- The (still experimental) new CIF PLC code generator for S7-300 and S7-400 now handles additional keywords, reserved identifiers, and so on (issues #901 and #921).

- The (still experimental) new CIF PLC code generator now has improved error messages when reading invalid I/O table files (issue #967).

- The (still experimental) new CIF PLC code generator rename warnings for location pointers no longer print a spurious period at the end of the location pointer names (issue #984).

- The (still experimental) new CIF PLC code generator check whether an I/O address exceeds the size of the largest compatible type supported by the target, now correctly considers the different possible I/O types, rather than always checking for integer types (issue #884).

- The (still experimental) new CIF PLC code generator documentation for S7 now explains how to ensure that properly-compiling program blocks can be generated in TIA Portal for PLC struct types generated for CIF tuple types (issue #863).

- The CIF to mCRL2 transformer has been re-implemented and is now based on first linearizing the CIF specification. For recursive process call, now only the assigned variables are included, not all variables, and the arguments are named rather than positional, which reduces the model size and improves readability. No more summations, nor location pointers (sorts) for automata with only one location, are generated (issues #352, #950, #954 and #955).

- The CIF to mCRL2 transformer no longer supports specifications with urgent locations and edges (issue #352).

- The CIF to mCRL2 transformer now supports specifications with `tau` events, the `<=>` binary operator, the `div` and `mod` binary operators on positive divisors, cast expressions that don’t change the type, location references, channels and receive expressions, initialization predicates in components that are trivially `true`, non-restrictive invariants, `if` expressions, `switch` expressions, algebraic variables with equations, and `if` updates (issues #226, #229 and #948).

- The CIF to mCRL2 transformer now generates mCRL2 specifications with a `marked` action. This action can be used in properties for verification. The generation of the action is enabled by default, but can be disabled using the new 'Generate marked action' option (issue #353).

- The CIF to mCRL2 transformer now uses a different naming scheme, based on absolute names. See the tool’s documentation for details (issues #352 and #224).

- The CIF to mCRL2 transformer now generates comments in the generated mCRL2 models (issue #352).

- The CIF to mCRL2 transformer now performs less preprocessing before the precondition check, for improved traceability of precondition violations.

- The CIF to mCRL2 transformer no longer eliminates automaton `self` references as preprocessing, and additionally eliminates type declarations and performs linearization as preprocessing (issue #352).

- The CIF to mCRL2 transformer has improved output in case of precondition violations (issue #424).

- The CIF to mCRL2 transformer has improved documentation (issues #352 and #424).

- The CIF event-based tools have improved output in case of precondition violations (issue #424).

- The CIF event-based tools no longer support unused channels (issue #424).

- The CIF event-based tools now support non-restrictive invariants in components, non-restrictive state/event exclusion invariants in locations, multiple non-restrictive state invariants per location, and any statically-determinable non-restrictive state invariant rather than only literal `true` (issue #424).

- The CIF event-based tools now support having multiple initialization/marker predicates in a location, and any initialization/marker predicate in locations that can be statically evaluated rather than only boolean literals (issue #424).

- The CIF event-based tools now support having multiple guards on an edge of a location, and any guard predicate that can be statically evaluated rather than only boolean literals (issue #424).

- The CIF event-based controllability check no longer supports unused events that are not controllable or uncontrollable (issue #424).

- The CIF event-based supervisory synthesis tool no longer supports unused events that are not controllable or uncontrollable (issue #424).

- The CIF event-based supervisory synthesis tool no longer checks for no marking during precondition checking, but now does so as a first step during synthesis. Having no marking still results in an empty supervisor (issue #424).

- The CIF event-based language equivalence check no longer has indented empty lines in its console output (issue #406).

- The CIF event-based DFA minimization tool no longer has indented empty lines in its console output (issue #406).

- The CIF event disabler now supports component definitions/instantiations and eliminates them as preprocessing (issue #424).

- The CIF event disabler now removes the controller properties annotation from the input specification, if present (issue #896).

- The CIF benchmarks overview generation script now consistently generates `?` instead of `-1` (issue #906).

- The CIF benchmarks have improved and newly-added model description (issue #949).

- The CIF tutorial lesson on initialization predicates has been improved (issue #739).

- Various documentation improvements and fixes (issues #424, #628, #742, #816, #849, #863, #929, #931, #943, #946, #956, #965, #970, #971, #976 and #987).

### Version 4.0 (2024-06-30)

Language changes:

- The syntax of annotation arguments has changed, to allow annotation arguments without a name. Each annotation has its own requirements, for instance requiring names for all its arguments, requiring all its arguments to not have a name, requiring names only for some of its arguments, or even allowing arguments to optionally have a name. If both the argument name and value are present, a colon (`:`) should now be used between them rather than an equal sign (`=`). Annotations are still an experimental work-in-progress language feature. Their design may change in a backward incompatible manner (issue #801).

- The `@doc` annotation now requires one or more unnamed arguments, rather than a single argument named `text`. See the documentation about documentation annotations for further details (issue #801).

- The CIF language now features a new `controller:properties` annotation. It is used by the CIF controller properties checker, to add the results of the performed checks to the input model (issues #410 and #621).

- Annotations may now be added to algebraic parameters of component definitions, automata, automaton definitions, automaton instantiations, edges, enumerations, enumeration literals, events, functions, function parameters, function variables, groups, group definitions, group instantiations, invariants, specifications and type declarations. Annotations on specifications, invariants in locations, and edges require double `@`-signs, such as `@@doc` instead of `@doc` (issues #593 and #824).

- The CIF type checker now warns about certain declarations that have a type that supports only one value. This new check is enabled for algebraic parameters, algebraic variables, channel parameters, channels, discrete variables, function parameters, function variables, function return types and input variables. To resolve such a warning, check the type, or use a constant instead (issues #797 and #827).

- The CIF type checker now warns about state/event exclusion invariants with events that are not in the send, receive or synchronization alphabet of the specification. Such state/event exclusion invariants do not restrict any behavior (issue #838).

- The CIF type checker now has extended convoluted references detection. It now also detects certain convoluted references for types of component parameters (issue #856).

Deprecations and removals:

- The ball sorting model has been removed from the CIF benchmark models set (issue #745).

New features:

- The CIF to CIF transformer now has a new transformation to relabel supervisors as plants (issue #834).

- The CIF controller properties checker now has an additional check, the bounded response check. The bounded response check improves upon the finite response check, by checking for finite response also for uncontrollable events, not just for controllable events. Additionally, for both controllable and uncontrollable events, the new check also computes the bounds on the number of transitions that can be executed. Furthermore, the new check does not suffer from false negatives. The bounded response check is now recommended instead of the finite response check (issue #621).

- The CIF controller properties checker now has an additional check, the non-blocking under control check, that should hold for all supervisor models before controller code is generated from them. See the tool’s documentation for further information (issue #410).

Improvements and fixes:

- The CIF parser is now more efficient in parsing elements that can have annotations, but do not have them (issue #593).

- The CIF pretty printer, which is used by all CIF tools to write output CIF models, now uses a separate `initial`, `marked` or `equation` keyword for each initialization predicate, marker predicate or equations, respectively. This also improves the traceability for certain precondition violations being reported by tools that use the new precondition checking framework (issue #807).

- The CIF simulator has a fix to prevent resource leaks for specifications with external user-defined Java functions (issue #635).

- The CIF simulator now removes all annotations from the input model as pre-processing (issue #736).

- The CIF to CIF transformation to anonymize names now renames local variables of functions to `fvarNN` rather than to `discNN`, with `NN` a number (issue #811).

- The CIF to CIF transformation to eliminate state/event exclusion invariants to automata now creates a separate automaton for each named state/event exclusion invariant, to preserve their names as best as possible (issue #830).

- The CIF to CIF transformation to eliminate state/event exclusion invariants to automata now creates the automata for state/event exclusion invariants of groups within those groups, rather than besides those groups (issue #830).

- The CIF to CIF transformation to eliminate state/event exclusion invariants to automata now correctly handles `disables` state/event exclusion invariants of locations of automata with more than one location (issue #830).

- The CIF to CIF transformation to eliminate state/event exclusion invariants now removes state/event exclusion invariants for events that are not in the send, receive or synchronization alphabet of the specification, rather than converting them to automata. This prevents the events from becoming part of the synchronization alphabet of the specification, which would mean transitions could then become possible for these events, while that was not the case before the transformation. If any such invariants are encountered, the transformation now prints a warning (issue #838).

- The CIF to CIF transformation to transform `switch` expressions to `if` expressions now also transforms nested `switch` expressions (issue #858).

- The CIF to CIF transformer now checks the output model for annotation constraint violations (issues #823 and #853).

- The CIF merger now has improved output in case of annotation constraint violations detected on the merged model (issue #823).

- The CIF data-based synthesis tool has improved performance, by using compounded operations for applying edges, using partial transition relations, and taking runtime errors into account once before the main synthesis fixed point computations, rather than repeatedly during synthesis. On average it is about 3.4 times faster, and it also uses less memory. However, the gain depends on the model being synthesized (issues #865, #866, #867 and #878).

- The CIF data-based synthesis tool no longer crashes when the node table gets too big (issue #625).

- The CIF data-based synthesis tool now runs for a little bit longer before running out of BDD nodes array memory, as the nodes array is increased one more time to the maximum limit, before failing due to running out of memory (issue #625).

- The CIF data-based synthesis tool now allows converting resulting predicates explicitly to only CNF or only DNF, through configuration of its BDD output mode option (issue #873).

- The CIF data-based synthesis tool now detects and warns about more potential issues for events that are disabled already before the main synthesis fixed point computations are started (issue #878).

- The CIF data-based synthesis tool now has improved warnings about state/event exclusion invariants with events that are not in the send, receive or synchronization alphabet of the specification (issue #838).

- The CIF data-based synthesis tool now has slightly improved debug output for applying plant invariants (issue #269).

- The CIF data-based synthesis tool now checks the output model for annotation constraint violations (issue #823).

- The CIF data-based synthesis tool now has workset algorithm dependency sets that take into account the potential for runtime errors to occur as edges are applied, which may reduce the number of dependencies and potentially improves synthesis performance if the workset algorithm is used (issue #878).

- The CIF explorer now uses proper terminology related to locations and edges versus states and transitions in its statistics output, debug output, report files, option descriptions and documentation (issues #691 and #882).

- The CIF explorer now has a new Remove duplicate transitions option that replaces the Enable edge minimization option. The latter is no longer supported. Functionally, the new option works as the old one (issue #691).

- The CIF explorer now removes all annotations from the input model as pre-processing (issue #736).

- The CIF code generator now supports documentation annotations for enumeration literals, events, functions, function parameters, function variables and specifications (issue #593).

- The CIF code generator for HTML now properly escapes SVG element identifiers when used in CSS selectors, making it possible to use SVG element identifiers with dots and colons (issue #715).

- The CIF code generator for C and Simulink now quote event names in generated comments (issue #593).

- The CIF code generator for Simulink now generates an empty line between the file header and imports (issue #593).

- The CIF code generator for Java, JavaScript and HTML now always uses proper paragraph syntax in the generated code for documentation from documentation annotations (issue #802).

- The CIF code generator for Java, JavaScript and HTML now generates improved comments in the generated code for user-defined functions (issue #593).

- The CIF code generator no longer crashes on reporting static evaluation errors for documentation annotations on nameless objects (issue #621).

- The CIF code generator now removes all non-`doc` annotations from the input model as pre-processing, and ignores annotations arguments during precondition checking (issue #736).

- The (still stable) current CIF PLC code generator now removes all annotations from the input model as pre-processing (issue #736).

- The (still experimental) new CIF PLC code generator now only supports events that are declared as controllable or uncontrollable. This thus also excludes `tau` events, and edges without events that implicitly have a `tau` event (issue #800).

- The (still experimental) new CIF PLC code generator no longer supports the `cbrt` and `pow` standard library functions (issue #876).

- The (still experimental) new CIF PLC code generator no longer supports events that are only used as monitor events, and could thus be executed infinitely often during a PLC cycle (issue #679).

- The (still experimental) new CIF PLC code generator no longer supports arrays of size zero (issues #679 and #794).

- The (still experimental) new CIF PLC code generator no longer supports `switch` expressions on array or tuple-typed values, or parts of values (issue #859).

- The (still experimental) new CIF PLC code generator no longer crashes for specifications with nested tuples (issue #818).

- The (still experimental) new CIF PLC code generator no longer crashes for models with `switch` expressions (issue #857).

- The (still experimental) new CIF PLC code generator has some robustness improvements (issues #628 and #770).

- The (still experimental) new CIF PLC code generator now generates additional and improved comments, such as section comments for different parts of the generated code (issue #815).

- The (still experimental) new CIF PLC code generator now generates a comment with an overview of the generated code as it relates to the elements of the input CIF model (issue #815).

- The (still experimental) new CIF PLC code generator now generates a header comment in the generated code that lists the name and version of the code generator, the date/time of generation, and a brief explanation of how to interpret the generated code and how it links to the concepts of CIF. A new Program header text file path option has been added to the tool to customize/extend the generated header comment (issue #815).

- The (still experimental) new CIF PLC code generator now generates PLC code with two event loops, first one for the uncontrollable events and then one for the controllable events. The option to set a maximum on the number of iterations now accepts either one limit (for both loops) or two limits (separate limits for the two loops). And the tool now warns if the configured limit is reduced due to the target PLC model not supporting such large numbers (issue #628).

- The (still experimental) new CIF PLC code generator now treats `timer` as a reserved keyword of PLCs, to ensure proper code is generated for various targets (issue #679).

- The (still experimental) new CIF PLC code generator now explicitly documents that it reads the inputs at the start of the PLC program, and writes the outputs at the end of the PLC program (issue #831).

- The (still experimental) new CIF PLC code generator now generates proper code for models with double negations, such as `--5`. This affects the code generated for all unary expressions (issue #848).

- The (still experimental) new CIF PLC code generator now generates proper code for the projection on arrays through negative integer values (issues #854 and #862).

- The (still experimental) new CIF PLC code generator now generates proper code for the `min` and `max` standard library functions, for S7 targets (issue #847).

- The (still experimental) new CIF PLC code generator now generates proper code for models without any behavior (issue #860).

- The (still experimental) new CIF PLC code generator has various fixes related to handling timers (issues #770, #854 and #862).

- The (still experimental) new CIF PLC code generator no longer inlines `bool`, `int`, `real` and `enum`-typed constants, for IEC 61131-3, PLCopen XML, S7 and TwinCAT targets (issues #679 and #877).

- The (still experimental) new CIF PLC code generator now removes all non-`doc` annotations from the input model as pre-processing, and ignores annotations arguments during precondition checking (issue #736).

- The CIF controller properties checker no longer supports models without automata, which was already reported through warnings before (issue #621).

- The CIF controller properties checker no longer supports models with automata and invariants that are kindless or requirements. It only supports automata with invariants that are plants or supervisors (issue #621).

- The CIF controller properties checker now adds the results of the performed checks to a `controller:properties` annotation, adapting the input model and writing it to a file. By default the output file is named after the input file, with its `.cif` file extension replaced by `.checked.cif`. Use the tool’s new Output file option to change the output file path (issues #621, #823 and #853).

- The CIF controller properties checker now uses consistent names for the tool itself in the command line help, option dialog, error messages and documentation (issue #621).

- The CIF controller properties checker now has slightly improved console output about the results of the performed checks (issue #621).

- The CIF controller properties checker now stops earlier if no checks are enabled (issue #621).

- The CIF controller properties checker now has improved warnings for specifications without events, as it now also checks for no uncontrollable events, and it now bases the checks on the alphabet of the specification, rather than event declarations (issue #621).

- The CIF controller properties checker now has improved precondition checking, as well as improved output in case of precondition violations (issues #424, #621 and #736).

- The CIF controller properties checker now has improved performance for its non-determinism check that is performed on the input model for the confluence and finite response checks (issue #424).

- The CIF controller properties checker documentation has been split into multiple pages and has various improvements (issues #424, #621 and #736).

- The CIF to mCRL2 transformation now removes all annotations from the input model as pre-processing (issue #736).

- The CIF to Supremica transformation now has improved precondition violation markers for reporting unsupported partial variable assignments (issue #790).

- The CIF to Supremica transformation now removes all annotations from the input model as pre-processing (issue #736).

- The CIF to UPPAAL transformation now have improved precondition violation markers for reporting unsupported partial variable assignments (issue #790).

- The CIF to UPPAAL transformation now removes all annotations from the input model as pre-processing (issue #736).

- The CIF to yEd transformation now removes all annotations from the input model as pre-processing (issue #736).

- The CIF event disabler now checks the output model for annotation constraint violations (issue #823).

- The CIF button/lamp/timer example’s ToolDef script for code generation has been slightly improved (issue #736).

- The CIF benchmarks overview generation script now uses row-based averages also for relative values (issue #887).

- The CIF benchmarks overview generation script now has improved weighted averages, preventing skewing of the results by a few models that are very difficult to synthesize (issue #887).

- The CIF documentation on SBE has various improved descriptions related to verification (issue #828).

- The CIF documentation has various small improvements and fixes (issues #410, #424, #593, #621, #628, #691, #736, #804, #810, #811, #830 and #852).

### Version 3.0 (2024-03-31)

Language changes:

- SVG input mappings can now either assign values to input variables (new feature), or map to an event to take (existing feature). This new feature is currently an experimental work-in-progress language feature, and is not yet supported by all CIF tools (issues #227 and #787).

- The syntax for addressables (the left hand side of an assignment) has changed to allow names like `automaton.variable`, but this is only meant to be used for SVG input mappings. It should be avoided for assignments in functions or on edges (issue #227).

- Annotations may now be added to constants, as well as discrete, continuous and algebraic variables. Annotations are still an experimental work-in-progress language feature. Their design may change in a backward incompatible manner (issue #593).

New features:

- All CIF tools now support reading `.cifx` files, CIF files in an XML format. CIF tools that write CIF specifications also support writing `.cifx` files. See the CIF reference manual for more information (issues #701 and #731).

- The CIF to CIF transformer now features a new Remove annotations transformation (issue #735).

- The CIF benchmark models have been extended with the `mri_event`, `mri_state` and `wafer_scanner` benchmark models (issue #364).

Improvements and fixes:

- All tools that produce empty CIF files now produce CIF files with an explicit comment indicating that the CIF specification is empty (issue #768).

- The CIF simulator no longer crashes on print output to a file in a non-existing directory, but instead now creates the missing directories (issue #730).

- The CIF data-based synthesis tool has internally been changed significantly, to in the future allow reusing the BDD-related parts of it in other tools. As a result of this, the tool has some changes in error messages for invalid option values (issue #706).

- The CIF data-based synthesis tool’s Supervisor name option no longer defaults to `sup` if explicitly given an empty option value. The default of the option is still `sup`, but setting the option value to empty now gives an error (issue #269).

- The CIF data-based synthesis tool’s warnings for plants that reference requirement state had typos that have been fixed (issue #750).

- The CIF code generator now has more readable output in case of precondition violations, as it has been migrated to the new precondition checking framework introduced earlier already for some of the other CIF tools (issue #424).

- The CIF code generator now supports `doc` annotations on constants, as well as discrete, continuous and algebraic variables. The comments in the generated C, Java, JavaScript, HTML, and Simulink code for `doc`-annotated constants, as well as discrete and algebraic variables now include the documentation from their documentation annotations. The comments in the generated C, Java, JavaScript, and HTML code for `doc`-annotated continuous variables now include the documentation from their documentation annotations (issue #593).

- The CIF code generator now has improved comments for algebraic variables in generated C and Simulink code (issue #593).

- The CIF code generator now generates correct JavaScript and HTML code for tuples (issue #715).

- The CIF code generator now generates correct JavaScript and HTML code for references to parameters and local variables of internal user-defined functions (issue #715).

- The CIF code generator now generates correct JavaScript and HTML code for the `acos`, `asin`, `atan`, `cos`, `exp`, `ln`, `log`, `sin`, and `tan` standard library functions (issue #715).

- The CIF code generator now generates correct JavaScript and HTML code for the string representations of enumeration literals, for instance in error messages, output of `fmt`, output of print declarations, and state logging (issue #715).

- The CIF code generator now generates correct JavaScript and HTML code for string escaping, for instance for log output, certain runtime errors, and state printing (issue #715).

- The CIF code generator now generates correct JavaScript and HTML code for constants whose value is defined using other constants (issue #715).

- The CIF code generator now generates JavaScript and HTML code for SVG copy and move declarations (issue #715).

- The CIF code generator now generates JavaScript and HTML code that can log the initial state and states reached after event transitions. This additional logging is disabled by default (issue #715).

- The CIF code generator now generates JavaScript and HTML code that include variables to enable or disable state and transition logging (issue #715).

- The CIF code generator now generates JavaScript and HTML code that takes into account the target of print declarations (issue #715).

- The CIF code generator now generates HTML pages with a 'Settings' menu, in which state logging (new feature) and transition logging (existing feature) can be enabled or disabled (issue #715).

- The CIF code generator now generates HTML pages with a log panel that has improved performance (issue #715).

- The CIF code generator now generates HTML pages with a log panel that has a horizontal scrollbar, rather than wrapping long lines (issue #715).

- The CIF code generator now generates HTML pages with less horizontal margin (issue #715).

- The CIF code generator now generates HTML pages that apply proper HTML escaping for the log panel (issue #715).

- The CIF code generator now generates HTML pages that consistently use Unix newlines for the log panel (issue #715).

- The CIF code generator now generates HTML pages that use a queue for SVG input clicks, preserving the order of the clicks, properly deciding the event to take on the current state, ignoring clicks for non-enabled events (printing a warning about it), and handling each click exactly once (issue #715).

- The CIF code generator now generates HTML pages where hovering over interactive SVG elements works correctly in case there are multiple SVG images that have interactive elements with the same ids (issue #715).

- The CIF code generator now generates improved and simpler JavaScript and HTML code for internal user-defined functions (issue #715).

- The CIF code generator now generates comments and reports with the original CIF names for location pointer variables (issue #715).

- The CIF code generator no longer wrongly reports certain warnings when generating Simulink code, for warnings on local variables and arguments of internal user-defined functions that should only be reported for discrete variables. The warning messages have also been improved (issue #424).

- The CIF code generator documentation has some fixes, improvements and extensions (issues #424 and #715).

- The (still experimental) new CIF PLC code generator now has an option to let the generator decide the best way to handle enumerations, based on the configured target PLC model (issue #679).

- The (still experimental) new CIF PLC code generator has various fixes related to code generated for variables, timers and functions (issue #679).

- The (still experimental) new CIF PLC code generator has various improvements and fixes related to names in the generated code, including among others better handling of keywords, not generating names with multiple consecutive underscores, and improved naming of edge selection variables (issue #679).

- The (still experimental) new CIF PLC code generator now generates improved and extended comments in the generated PLC code, for the part of the code related to executing transitions (issue #782).

- The (still experimental) new CIF PLC code generator has improved precondition checking for continuous variables, with better messages in case of unsupported specifications (issue #681).

- The CIF to CIF transformation to eliminate 'if' updates now not only eliminates 'if' updates on edges, but also for SVG input mappings with updates (issue #227).

- The CIF to CIF transformation to simplify values now not only simplifies the guards of 'if' and 'elif' updates on edges, but also for SVG input mappings with updates (issue #227).

- The CIF button/lamp/timer example has been fixed such that code can once more be generated (issue #772).

- The CIF button/lamp/timer and FIFO examples have formatting improvements for their ToolDef scripts (issue #773).

- The CIF ball sorting benchmark model source information had a typo that has been fixed (issue #751).

- The CIF production cell benchmark model has a fixed comment (issue #767).

- The CIF language tutorial 'Variable overview' lesson now also includes input variables (issue #792).

- The CIF documentation breadcrumbs are now consistent with the table of contents (issue #38).

- The CIF documentation table of contents now has proper links for items that link to sections on pages rather than to entire pages (issue #38).

- The CIF website and documentation have various small improvements and extensions (issues #38, #227, #715, #727, #752, #756, #764 and #766).

### 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 `else`s (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.