Skip to content
Choose a tag to compare


Choose a tag to compare


Bug fixing:

  • Fixed a "+ 0" that appeared in some of the text and graphical outputs

Major features

  • New accepting cycle synthesis (-mode AccLoopSynth)
  • New NDFS-based accepting cycle synthesis (-mode AccLoopSynthNDFS) with several exploration strategies [NPP18]. Additional option -counterexample terminates the analysis as soon as one cycle is found.
  • In mode EF -counterexample, IMITATOR outputs an example of parameter valuation, and a full concrete run, with a graphical representation of the clocks and discrete variables evolution. An absolute time clock (initially set to 0 and never reset) named global_time needs to be defined in the model. [EXPERIMENTAL]
  • New check-syntax mode (-mode checksyntax), that simply checks the syntax and terminates without doing any analysis.

Minor features

  • Removed the creation and deletion of an (unused) script when generating graphics

Syntax improvement

  • if-then-else conditions are now allowed in updates. Example syntax: when x = 2 sync a do {if l <= 10 then x := 0, l := 0 else (i := 2) end} goto l1;
  • Partial model inclusion is now possible thanks to keyword #include. Notably, properties can now be included from other files.


  • Removed the -merge-before option (that was not documented nor properly tested)


  • The result in the terminal tries to be more precise about what the synthesized constraints actually guarantees
  • Added a (tentative) translation to Uppaal (option -PTA2Uppaal); see limitations in the user manual
  • In the graphical state space and states description, the projection onto a selected set of parameters is added if the model contains projectresult(…)
  • In the text files, state and transition descriptions are now ordered by increasing order
  • The cartography and tile graphics are now larger (1024x1024), and the margins are a bit reduced


  • Changed the internal representation of the state space: (state, action, state) is now (state, edge, state)