Skip to content

IMITATOR 2.9
Compare
Choose a tag to compare
@etienneandre etienneandre released this 23 Mar 14:14
· 3571 commits to master since this release
v2.9
aa3dd87

Major

  • New algorithm LoopSynthesis (option -mode LoopSynth): synthesizes valuations for which there exists an infinite run in the model.
  • New algorithms for non-Zeno cycle emptiness checking: with CUB-detection (-mode NZCUBcheck) or transformation to a CUB-PTA (-mode NZCUBtrans) [still in an experimental phase]
  • EFsynth rewritten to output a single, disjunctive constraint (instead of a list of constraints as until version 2.8); Legacy version still usable using option -mode EFold
  • PRP and PRPC now disconnected from IM and BC: new syntax (-mode PRP and -mode PRPC), and result in the form of a single good and/or bad constraint.

Minor features

  • Variables not used in a model apart from resets (or updates) are simply removed entirely, so as to speed up the execution. If that behavior is not the one intended by the user, this automatic removal can be disabled using the new option -no-var-autoremove.
  • (Limited) colored terminal output :-)

Bug fixing

  • Solved a bug for EF / PRP when the initial state is already bad
  • Solved a bug in the equality and inclusion check of non-convex parameter constraints (wrong PPL function used)

Export

  • PDFC now outputs both an under-approximated good constraint and an under-approximated bad constraint (instead of an over-approximated good constraint for the latter); so presentation of the result changes compared to version 2.8
  • Field "State space nature" becomes "Constraint nature" in result (.res) files
  • Add L/U status to result (.res) files
  • The file name for the graphical cartography becomes model_cart.png for any algorithm (instead of model_cart_ef.png, model_cart_im.png and so on).

Install and compile

  • To compile, now use build.sh to compile IMITATOR (in non-distributed mode) and build-patator.sh to compile PaTATOR (distributed mode)

Internal

  • In cartography algorithms, the list of tiles is now externalized to a dedicated manager (that can store a list of tiles, or a single good/bad constraints)
  • New experimental version of PRPC using an external compositional verifier; hidden option "-mode coverlearning"
Assets 6
Loading