@etienneandre etienneandre released this Feb 21, 2018 · 93 commits to master since this release

Major features:

  • New algorithms EFmin and EFmax synthesizing the min (resp. max) valuation of a single given parameter for which a given state is reachable
  • Arithmetic expressions are now supported in discrete updates; this includes in particular the use of divisions (clock updates are not impacted, and remain linear only)
  • Distributed version of the non-Zeno cycle emptiness checking [still in an experimental phase]
  • The GrML syntax (in and out) is now discontinued, as CosyVerif is not maintained anymore, and the next version may not support GrML.

Minor features:

  • New option to convert exact-valued discrete variables into (possibly approximated) floats in all outputs
  • Reintroduced the -counterexample option (stops the analysis as soon as a counterexample is found) for EF and PRP
  • New options -PTA2PNG and -PTA2PDF, to convert the model as a graphics in PNG and PDF formats, respectively
  • New verbose mode 'experiments', displaying slightly more information than the standard verbosity
  • New option -romeo (April 1st 2017 feature)… Try it ;-)


  • Simplified the terminal output by IMITATOR by removing most technical (states, memory, statistics) information. The former information can be retrieved using the new mode -verbose experiments.

Bug fixing

  • Fixed a bug in the parsing module that crashed IMITATOR when a discrete was assigned to an undeclared variable


  • Better separation between the discrete variables and other variables in guards, so as to first check whether the discrete part is satisfiable (which is cheap) before checking the continuous part (which is expensive)
Assets 6