Skip to content

IMITATOR 2.8
Compare
Choose a tag to compare
@etienneandre etienneandre released this 13 Aug 14:47
· 3878 commits to master since this release
v2.8
5c7607c

Major

  • New algorithm: parametric deadlock-freeness checking
  • Allow for more complex unreachable states in property definition: several locations in several IPTAs can be tested, and discrete variables can be compared with <, <=, =, >=, > and intervals; all this can be mixed using and/or operators.
  • Automatic detection of L/U-PTAs, U-PTAs and L-PTAs
  • Standardized output for the results of IMITATOR (including a notion of validity of the constraint output)

Bug fixing

  • Corrected a problem in the generation of the observer patterns
  • Solved an inconsistency in the property syntax of the "always sequence" observer pattern
  • Remove three observer patterns that were allowed in the input syntax but not implemented
  • Correct the depth-limit option behavior (that used to compute one step further than requested)
  • All error messages now displayed on stderr (instead of stdout)

Options

  • Added an option "-output-trace-set-verbose" to print trace set with all information contained in the .states file (i.e., the constraint and the constraint projected onto the parameters)
  • New options -cart-tiles-limit and -cart-time-limit that operate on the cartography algorithms

Graphics

  • Added a visualization of the bad states on the trace set (using red color + a frowney)

Misc

  • Memory information now displayed at the end of the execution even in -verbose standard
  • Memory information now added to the .res files

Export

  • Result file (.res) much more nicely structured. Statistics better integrated both in the terminal output and in the .res files
  • Added an export to HyTech (option -PTA2HyTech)
  • Removed the automatically generated observer from the PTA export (option -PTA2JPG)
  • When exporting to jpg (option -PTA2JPG), the urgent locations are now colored in yellow, and the nosync action (no synchronization name) are now dashed

Versioning

  • Now IMITATOR integrates the hash number of GitHub in all outputs

Install and compile

  • Using "strip" the binary is now (much) smaller

Internal

  • Entire reorganization of the core of IMITATOR: all algorithms rewritten in an object-oriented fashion
  • Added a mode to regenerate the IMITATOR input file (helpful to test input/output models)
  • Automaton.ml becomes Location.ml (and new module Automaton.ml created); and reorganization of numerous other modules
  • Build number only incremented when a flag file "iamadeveloper" is present in the imitator root directory
  • "examples" directory becomes "benchmarks"
  • New experimental version of EFsynth (usable with a hidden option)
  • Non-regression tests now implemented in an external Python script
  • Comparator of efficiency with former versions now implemented in an external Python script
Assets 5
Loading