- Updates are now fully sequential in the model, including clock updates; WARNING: this might result in backward-incompatibility for elaborate models involving discrete and continuous updates in the same transition.
- New user-defined functions: imperative instructions, function calls, definition of local variables, variable shadowing…
- New AG ("global invariant") algorithm
- New EU ("Exists … until") algorithm
- New AF ("always eventually") algorithm, and variants:
- AR ("always … release")
- AU ("always … until")
- AW ("always … weak until")
- New timed variants of EF, EU, AF, AR, AU, AW
- The Boolean implication (
a => b) is now allowed both in the model and in the property.
- Actions declaration is now defined using the
actionskeyword instead ofsynclabs; backward-compatibility remains ensured - Terminate backward-compatibility on updates syntax: updates are now only defined using the
var := exprsyntax - Terminate backward-compatibility on the permissive
initially:declarations in automata (already not taken into account in the semantics) - Both
;and,instruction separators accepted
- Source code entirely moved and restructured as a more standard tree
- Some divisions by zero (e.g., explicitly written
0 / 0in the model) may not be detected; dynamic divisions by zero (j := 2 / i, withi = 0) are however in principle detected.
- New complex types for discrete global variables: lists, arrays, stacks, queues, and associated functions
- New: extrapolation for parametric zones [AA22]
- Refactoring of merging functions, with more efficient heuristics [AMPP22]
- Exemplification algorithm: given a parametric timed specification, exhibit concrete parameter valuations, and concrete positive and negative runs, with a graphical representation of the evolution over time of the clock and discrete variables [AWUH22] (slightly experimental)
- New type: "binary words", of the form
0b00111, for bitwise binary operations. Can be used in guards, invariants, updates. Example:when logor(bw1, 0b1011) <> bw1 do {shift_left(bw1, 2)} - The syntax
var' := exprin updates is discontinued. Official syntax remainsvar := expr(backward-compatibility forvar' = exprremains ensured until further notice)
- New accepting cycle synthesis with generalized condition. Syntax
property := #synth CycleThrough(condition_1, …, condition_n)Each of the conditions must hold on at least one state of the same cycle, in order for this cycle to be accepting.
- New types for discrete global variables: Boolean variables (
bool), integer variables (int, over 32 bits) discretebecomerational(still encoded using exact arithmetic, as opposed to the newinttype)- New power operator
pow(v, i)over discrete variables, withvan integer or rational expression, andian integer expression (possibly involving integer variables)
- IMITATOR now attempts to generate a result (
.res) file even in the case of an error such as parsing error of the model or of the property
- New syntax for the initial state definition, with a separation between the discrete and the continuous parts (the former syntax remains accepted for backward-compatibility, but a warning is triggered).
property := #synth AcceptingCyclenow allowed as a shortcut forproperty := #synth CycleThrough(accepting)
- New translation to the JANI interchange format
- Entire refactoring of the benchmarks library [AMP21]
- Fixed an issue met in v3.0 when a division by 0 is encountered.
- Solved a bug (introduced in v3.0) related to variable automatic removal in the initial state definition
- Solved a bug that crashed the tool when an included file was not found
MAJOR RELEASE
The calling paradigm switches from a single file with numerous options (some of them compulsory) to two files and a few options (none of them compulsory):
- a model file, containing the model
- a property file, containing the property (and optionally the projection onto some parameters) The model syntax is almost entirely backward-compatible with (at least) the IMITATOR 2.10.1 syntax. The property syntax is entirely new.
- New variants of the NDFS-based accepting cycle synthesis with several exploration strategies [AAPP21]
- IMITATOR now supports multi-rate clocks with a syntax of the form
flow {x' = 1, y' = 2.5, z' = -3/5}
- Terminate support for HyTech-style comments (
-- comment) and C-style comments (/* comment */) - Terminate support for some HyTech-style optional syntax (regions declaration…)
- Many backward-compatible useless syntactic features now raise warnings (e.g., using
whileinstead ofinvariant, usingWait {}…)
- Most options changed since version 2.x
- Some options were discarded, and are now part of the property syntax
- Result is always output to a file by default; use
-no-output-resultto disable
- By default, all files are now exported in the current directory instead of the model directory. Option
-output-prefixcan still be used to change the directory.
- The build number is discontinued (and replaced by the sole short Git hash)
- Created a new
Unsolvablesection in thebenchmarksrepository, containing very simple models for which IMITATOR cannot (yet) provide a result.
minor release
- Fix bugs for option
-counterexample - Fix issues in NDFS-based accepting cycle synthesis [NPP18], and options names
MAJOR RELEASE
- Fixed a "+ 0" that appeared in some of the text and graphical outputs
- New accepting cycle synthesis (
-mode AccLoopSynth) - New NDFS-based accepting cycle synthesis (
-mode AccLoopSynthNDFS) with several exploration strategies [NPP18]. Additional option-counterexampleterminates 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) namedglobal_timeneeds to be defined in the model. [EXPERIMENTAL] - New check-syntax mode (
-mode checksyntax), that simply checks the syntax and terminates without doing any analysis.
- Removed the creation and deletion of an (unused) script when generating graphics
if-then-elseconditions 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-beforeoption (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)
MAJOR RELEASE
- New algorithm for optimal reachability with priority queue (queue-based, with priority to the earliest successor for the selection of the next state)
- Removed the
Gc.major()instruction, that used to require a huge time for large models, while not bringing any benefit for smaller models
- Using the syntax
initially <loc name>in the beginning of a PTA (which is not taken into account) now raises a warning. - In translation mode, some metrics (numbers of automata, actions, variables, locations…) are printed on the terminal.
- New option to avoid the inclusion check in EFsynth: useful when very large parameter constraints are manipulated
- Correct errors in displaying PTA (graphics in PDF, PNG, etc.): arithmetic expressions on discrete variables did not print correctly
- Fix a bug (or an unclarity) in the options for trace set generation
- The prime (
') in transition updates becomes optional; the=in transition updates becomes:=(backward-compatibility remains ensured until further notices) That is, an updatex' = 0becomesx := 0 while [invariant condition] wait{}becomesinvariant [invariant condition](backward-compatibility remains ensured until further notices)
- The graphical state space now comes in .pdf instead of .jpg for better readability
- Some metrics are printed in the PTA graphical exports (PTA2PDF, PTA2PNG, PTA2JPG)
- The trace set now depicts the automaton name in addition to the location name (for example:
automaton: locationinstead oflocation)
minor release
- Fix a bug (or an unclarity) in the options for trace set generation
- Removed the
Gc.major()instruction, that used to require a huge time for large models, while not bringing any benefit for smaller models
- The graphical state space now comes in .pdf instead of .jpg for better readability
minor release
- Correct errors in displaying PTA (graphics in PDF, PNG, etc.): arithmetic expressions on discrete variables did not print correctly
minor release
- New option to avoid the inclusion check in EFsynth: useful when very large parameter constraints are manipulated
minor release
- The prime (
') in transition updates becomes optional; the=in transition updates becomes:=(backward-compatibility remains ensured until further notices) That is, an updatex' = 0becomesx := 0 while [invariant condition] wait{}becomesinvariant [invariant condition](backward-compatibility remains ensured until further notices)
MAJOR RELEASE
- 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.
- New option to convert exact-valued discrete variables into (possibly approximated) floats in all outputs
- Reintroduced the
-counterexampleoption (stops the analysis as soon as a counterexample is found) for EF and PRP - New options
-PTA2PNGand-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.
- 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)
MINOR RELEASE
- The GrML syntax (in and out) is now discontinued, as CosyVerif is not maintained anymore, and the next version will not support GrML.
- New option
-romeo(April 1st 2017 feature)… Try it 😉 🐟
MAJOR RELEASE
- 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 PRPand-mode PRPC), and result in the form of a single good and/or bad constraint.
- 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 :-)
- 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)
- 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 naturebecomesConstraint naturein result (.res) files - Add L/U status to result (
.res) files - The file name for the graphical cartography becomes
model_cart.pngfor any algorithm (instead ofmodel_cart_ef.png,model_cart_im.pngand so on).
- To compile, now use
build.shto compile IMITATOR (in non-distributed mode) andbuild-patator.shto compile PaTATOR (distributed mode)
- 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
MAJOR RELEASE
- 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)
- Corrected a problem in the generation of the observer patterns
- Solved an inconsistency in the property syntax of the
always sequenceobserver 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)
- Added an option
-output-trace-set-verboseto print trace set with all information contained in the.statesfile (i.e., the constraint and the constraint projected onto the parameters) - New options
-cart-tiles-limitand-cart-time-limitthat operate on the cartography algorithms
- Added a visualization of the bad states on the trace set (using red color + a frowney)
- Memory information now displayed at the end of the execution even in
-verbose standard - Memory information now added to the
.resfiles
- Result file (
.res) much more nicely structured. Statistics better integrated both in the terminal output and in the.resfiles - 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
- Now IMITATOR integrates the hash number of GitHub in all outputs
- Using
stripthe binary is now (much) smaller
- 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.mlbecomesLocation.ml(and new moduleAutomaton.mlcreated); and reorganization of numerous other modules- Build number only incremented when a flag file
iamadeveloperis present in the imitator root directory examplesdirectory becomesbenchmarks- 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
INTERMEDIATE RELEASE
- Corrected a problem in the generation of the observer patterns
examplesdirectory becomesbenchmarksAutomaton.mlbecomesLocation.ml(and new moduleAutomaton.mlcreated)
INTERMEDIATE RELEASE
- Allow for more complex unreachable states in property definition: several locations in several IPTA can be tested, and discrete variables can be compared with
<,<=,=,>=,>and intervals; all this can be mixed using and/or operators. - Detection of L/U-PTA, U-PTA and L-PTA
- Solved an inconsistency in the property syntax of the
always sequenceobserver pattern - Remove three observer patterns that were allowed in the input syntax but not implemented
- Added an option
-output-trace-set-verboseto print trace set with all information contained in the.statesfile (i.e., the constraint and the constraint projected onto the parameters)
- Added a visualization of the bad states on the trace set (using red color + a frowney)
- Removed the automatically generated observer from the PTA export
- 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:
- Urgent locations now handled natively (keyword:
urgent loc) - Constant now supported in the input model
- Add two new verbose modes:
muteandwarning-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
-counterexoption (stops the analysis as soon as a counterexample is found)
- mode
reachabilitybecomes modestatespace -cartbecomes-output-cart-fancybecomes true by default; to disable it, use-output-trace-set-nodetails-log-prefixbecomes-output-prefix-with-dotbecomes-output-trace-set-with-graphics-sourcebecomes-output-graphics-source-with-logbecomes-output-states-with-parametric-logis removed (becomes always true when option-output-statesis enabled)
- Add EF mode support to the CosyVerif interface (using options
-fromGrMLand-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
- Add suffix
-pta.jpgto 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)
- 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é"
- Main binary now in lower case (
imitator) - Two versions:
- non-distributed (
sh compile.sh), that creates a static binaryimitator, or - distributed (
sh compile-distr.sh), that creates a dynamic binarypatator
- non-distributed (
- Moved to OCaml 4.01.0
- Replaced
Makefilewith_oasis0.3 - Refactored constraints
- Renamed
Graph.mlwithStateSpace.ml - Much refactoring of the code, in particular in
Cartography.ml
PRIVATE RELEASE
- Added EF-synthesis (option
-EF): synthesize all parameter valuations such that a given state is reachable - Added a distributed version of IMITATOR
reachabilitybecomesstatespace
- Improve printing floating numbers (in time and memory statistics)
- Now IMITATOR has a build number
- replaced
Makefilewith_oasis - Refactored constraints
- Renamed
Graph.mlwithStateSpace.ml - Much refactoring of the code, in particular in
Cartography.ml
PRIVATE RELEASE
Nothing really new, just a backup before refactoring constraints
- dynamic clock elimination now implemented (option
-dynamic)
- tile nature now written in the source file for plot in border cartography (available with option
-with-graphics-source) - GrML input / output is no longer "experimental", and now fully integrated
- graphic cartography is now
.pnginstead of.ps
- Correction of the memory used in 64 bits (before, gave the same number as in 32 bits)
- Added observer patterns
- Changed and improved bad state definition (that was not really used anyway)
- The random cartography is temporarily suspended
- Cartography can color in green and red according to the bad state definition
- Added a new cartography mode with border detection (ongoing work)
- Added dynamic clock elimination (ongoing work)
- Added branch and bound (ONGOING WORK)
-IMorigbecomes-IMK-debugbecomes-verbose-with-dot-sourcebecomes-with-graphics-source- Merging option becomes (again?)
-merge - Added
-baboption (for branch and bound) [work in progress] - Added
-counterexoption (stops the analysis as soon as a counterexample is found) [work in progress]
- region declaration not compulsory anymore (that was only used for Hytech backward compatibility)
- bad state definition added
- Not everything allowed anymore at the end of the file! (before, everything was allowed for backward compatibility with HyTech) Now need to add (optional) keyword
endfirst
- output files for model
XXXX.imiare nowXXXX.extinstead ofXXXX.imi.ext
- Refactored BC code
- The bounds for V0 are now NumConst (not "int" anymore)
- Added arbitrary clock updates (not only to 0).
- Partial code refactoring.
- Options: Merging is still not enabled by default; inverted options
-no-logand-no-logto-with-dotand-with-log.-post-limitbecomes-depth-limit. - Added experimental and ongoing features (import from and export to GML, depth first exploration).
- Added support for stopwatches [CL00] with new keyword
stop. Syntax, semantics and computation time are backward-compatible for models without stopwatches.
PRIVATE RELEASE
- Added merging of states [AFS12], several optimizations; added and changed input options
PRIVATE RELEASE
- Fully removed
X'anddvariables: large gain in both memory and time
PRIVATE RELEASE
- Starting removing
Xanddvariables - Addition of an optional optimization of the inverse method algorithm
- Several optimizations to speed up post image computation, including a simple but efficient one for programs with discrete variables
- Addition of variants of the inverse method algorithm
- Addition of an optional optimization of the inverse method algorithm
- Several optimizations to speed up post image computation
- Several optimizations to speed up post image computation
- More detailed presentation of reachability graph
- Graphical output of behavioral cartography
- Refactoring of source code to improve maintainability
- Replaced APRON and POLKA libraries by PPL (Parma Polyhedra Library)
- Tool completely rewritten in OCaml
- Polyhedra handled thanks to APRON
First version (in Python)