June 1, 2023: Version 2.7.0 released
A maintenance release. Added a preliminary distribution for Apple Silicon; please report any issues.June 11, 2020: Version 2.6.0 released.
Mostly compiler improvements, including: better code generation for cases, conditionals and loops;March 16, 2016: Version 2.5.0 released.
Improved -j option; Fixed and improved exception handling when exceptions handled by tts clients;January 6, 2016: Version 2.4.0 released.
Bug fixes + revised libraries. Revised tts exception handling. Added option -j and json output to frac (to be used in future tools).October 22, 2015: Version 2.3.0 released.
Bug fixes, revised libraries. Refreshed the development environment for the tools.June 23, 2015: Version 2.2.8 released.
March 23, 2015: Version 2.2.6 released.
Mostly a maintenance release.Feb 02, 2014: Version 2.2.4 released.
A maintenance release. Various improvements. Fixed operator precedence in ltl properties.June 18, 2013: Version 2.2.2 released.
A maintenance release. Fixed check of returns in functions.January 11, 2013: Version 2.2.0 released.
Mostly a maintenance release. Fixed translation of absent ... after ... within .... Fixed/enriched translation of values probes (variables optimized out while needed).October 9, 2012: Version 2.1.2 released.
Version 2.1.2 enriches the assert command of the language of properties with optional -true STRING and -false STRING flags specifying the message to be printed when the asserted expression holds or does not.September 20, 2012: Version 2.1.0 beta released.
Version 2.1.0 enriches the language of properties accepted in 2.0.2 with timed patterns, please check that page for the updated language of patterns.May 10, 2012: Version 2.0.2 released.
A maintenance release. Fixes compilation of event observables in properties.February 27, 2012: Version 2.0.0 released.
Improves frac-1.7.2; added some options (-arch, -unsafe, -strip); added man page to distributions;The experimental tool rset is no more distributed with frac as it is now provided by the tina toolbox (as of Version 3.0.0). This tool, now named sift, can output its results in ktz format and can perform on the fly verification of reachability properties.
November 24, 2011: Versions 1.6.2 and 1.7.2 released.
Compared to 1.6.0, the code generator of 1.6.2 enables sharing between state representations, contributing, in addition to state compression, to decrease memory requirements for building the state spaces.Compared to 1.7.0, the code generator of 1.7.2 enables substate sharing (as in 1.6.2 versus 1.6.0). In addition, 1.7.2 enriches the language of properties of 1.7.0 with straight ltl properties (in addition to patterns). Also, 1.7.2 extends fiacre boolean expressons, the language of observables and that of properties with an "implies" operator, written "=>".
The updated language of properties is described in that page.
Added -unsafe flag, that transforms non-interference errors into simple warnings;
October 18, 2011: Version 1.7.0 released.
Added fiacre properties and patterns (experimental).September 30, 2011: Version 1.6.0 released.
Added fiacre functions, native and extern.June 20, 2011: Version 1.5.2 released.
A maintenance release. Mainly fixes a code generation bug concerning unions hitting most likely Windows targets but potentially all.May 6, 2011: Version 1.5.0 released.
frac-1.5.0 is a major release. It implements the same language as frac-1.4.0, but introduces important improvements in the code generated, notably:A more efficient treatment of queues;
A more space efficient representation of states, in particular for queues and unions;
April 8, 2011: Version 1.4.2 released.
Maintenance release. Fixes a bug potentially leading to a default of initialization of some variables;January 4, 2011: Version 1.4.0 released.
Shared variables may be written everywhere; frac performs a conservative non-interference check and rejects programs not passing it;Improved storage libraries and headers for 64 bit targets;
"any" is allowed as messages in output statements;
December 13, 2010: Version 1.3.3 released.
A maintenance release.December 6, 2010: Version 1.3.2 released.
A maintenance release.May 27, 2010: Version 1.3.0 released.
Finalized treatment of wait, loop, on, unless;Slight syntax simplification: access expressions like a[3] or r.f are now considered atomic;
Frac now checks compositionality and cycle-freeness of the priority relation;
Improved code generation;
October 1, 2009: Version 1.2.0 released.
Towards Fiacre V3.0:Added statements wait (at most one along each path), loop, on (guards);
Shared variables may be read everywhere;
Added unless clauses (priorities within select statements);