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).

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).

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 values, 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 add 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).

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).

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

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).

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 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).

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).

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).

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).

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).

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).

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).

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).

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).

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

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

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).

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).

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).

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).

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).

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).

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).

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).

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).

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).

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

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).

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).

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).

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).

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).

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).

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).

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).

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).

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).

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).

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).

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).

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).

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.