@etienneandre etienneandre released this Jul 22, 2015 · 959 commits to master since this release

release 2.7 (2015-07-22)

Major algorithmic features since 2.6.1

  • Added EF-synthesis (option "-mode EF"): synthesize all parameter valuations such that a given state is reachable [AHV93,JLR15]
  • Added PRP and PRPC algorithms (option "-PRP") [ALNS15]
  • Added a distributed version of the behavioral cartography (option "-distributed"), with several distribution schemes:
    • static [ACN15]
    • sequential [ACE14]
    • random [ACE14]
    • shuffle [ACN15]
    • dynamic [ACN15]
    • unsupervised / unsupervised multi-threaded (unpublished, EXPERIMENTAL)

Syntax improvement

  • Urgent locations now handled natively (keyword: "urgent loc")
  • Constant now supported in the input model

Options

  • Add two new verbose modes: mute and warning-only
  • Add export to LaTeX/TikZ
  • The result (text) can be exported to a file (option "-output-result")
  • Time elapsing can be applied either at the beginning (new mode, option -no-time-elapsing) or at the end (classical IMITATOR semantics) of the computation of a new state
  • New options to specify min/max values for x/y axes for the graphical output of the cartography
  • Removed -counterex option (stops the analysis as soon as a counterexample is found)

Changes in options syntax

  • mode "reachability" becomes mode "statespace"
  • "-cart" becomes "-output-cart"
  • "-fancy" becomes true by default; to disable it, use "-output-trace-set-nodetails"
  • "-log-prefix" becomes "-output-prefix"
  • "-with-dot" becomes "-output-trace-set"
  • "-with-graphics-source" becomes "-output-graphics-source"
  • "-with-log" becomes "-output-states"
  • "-with-parametric-log" is removed (becomes always true when option "-output-states" is enabled)

Interfacing with CosyVerif (and GrML support)

  • Add EF mode support to the CosyVerif interface (using options -fromGrML and -cosyProp)
  • Fix a bug in the GrML output (action labels were removed when exporting to GrML)
  • Add the initial constraint to both the GrML input and the GrML output

Misc

  • Add suffix "-pta.jpg" to PTA2JPG files
  • In BC mode: try to reduce the number of constraint (inclusion test in both directions)
  • Warning displayed if parameters are not constrained to be >= 0 in the model
  • Improve printing floating numbers (in time and memory statistics)

Versioning

  • Now IMITATOR has a build number (since May 2013)
  • Now IMITATOR has a version name and a version logo (based on traditional Breton "galettes" ingredients): 2.7 is "Butter Guéméné"

Install and compile

  • Main binary now in lower case ("imitator")
  • Two versions:
    • non-distributed (sh compile.sh), that creates a static binary "imitator", or
    • distributed (sh compile-distr.sh), that creates a dynamic binary "patator"

Internal

  • Moved to OCaml 4.01.0
  • Replaced Makefile with _oasis 0.3
  • Refactored constraints
  • Renamed "Graph.ml" with "StateSpace.ml"
  • Much refactoring of the code, in particular in Cartography.ml
Assets 5