v3.4.0-alpha

release 3.4.0-alpha (2024-03-21) Cheese Durian

Major features

• 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

Syntax improvement

• The Boolean implication (a => b) is now allowed both in the model and in the property.

Syntax changes in the model

• Actions declaration is now defined using the actions keyword instead of synclabs; backward-compatibility remains ensured
• Terminate backward-compatibility on updates syntax: updates are now only defined using the var := expr syntax
• Terminate backward-compatibility on the permissive initially: declarations in automata (already not taken into account in the semantics)
• Both ; and , instruction separators accepted

Internal

• Source code entirely moved and restructured as a more standard tree

Known issues

• Some divisions by zero (e.g., explicitly written 0 / 0 in the model) may not be detected; dynamic divisions by zero (j := 2 / i, with i = 0) are however in principle detected.

v3.3.0

release 3.3 (2022-07-21) Cheese Caramel au beurre salé

Syntax improvement

• New complex types for discrete global variables: lists, arrays, stacks, queues, and associated functions

Major features

• 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)

v3.3.0-beta-2

release 3.3-beta-2 (2022-05-02) Cheese Caramel au beurre salé

Syntax improvement

• New complex types for discrete global variables: lists, arrays, stacks, queues, and associated functions

Major features

• New: extrapolation for parametric zones [AA22]
• Refactoring of merging functions, with more efficient heuristics [AMPP2x]
• 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)

v3.3.0-beta

release 3.3-beta (2022-04-27) Cheese Caramel au beurre salé

Syntax improvement

• New complex types for discrete global variables: lists, arrays, stacks, queues, and associated functions

Major features

• New: extrapolation for parametric zones [AA22]
• Refactoring of merging functions, with more efficient heuristics [AMPP2x]
• 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)

v3.3.0-alpha

release 3.3-alpha (2022-03-24) Cheese Caramel au beurre salé

Syntax improvement

• New complex types for discrete global variables: lists, arrays, stacks, queues, and associated functions

Major features

• New: extrapolation for parametric zones [AA22]
• Refactoring of merging functions, with more efficient heuristics [AMPP2x]
• 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)

v3.2.0+merging

Experiments for merging

v3.2.0

release 3.2 (2021-11-03) Cheese Blueberries

Syntax improvement

• 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' := expr in updates is discontinued. Official syntax remains var := expr (backward-compatibility for var' = expr remains ensured until further notice)

Major features

• 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.

v3.1.0+extrapolation

IMITATOR 3.1 + extrapolation

This is a fork version of IMITATOR 3.1 "Cheese Artichoke", extended with extrapolation functions.
This tag is saved for reproducibility of the associated experiments.

Last modification of the code: 16th September 2021

v3.1.0

release 3.1.0 (2021-07-20) Cheese Artichoke

Syntax improvement

• New types for discrete global variables: Boolean variables (bool), integer (int, over 32 bits) variables
• discrete become rational (still encoded using exact arithmetics, as opposed to the new int type)
• New power operator pow(v, i) over discrete variables, with v an integer or rational expression, and i an integer expression (possibly involving integer variables)

Result

• 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

Syntax changes in the model

• 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).

Syntax changes in the property

• property := AcceptingCycle now allowed as a shortcut for property := CycleThrough(accepting)

Export

• New translation to the JANI interchange format

Benchmarks

• Entire refactoring of the benchmarks library [AMP21]

Bug fixing:

• 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

v3.1.0-beta

release 3.1.0-beta (2021-04-28) Cheese Artichoke

Syntax changes in the property

• property := AcceptingCycle now allowed as a shortcut for property := CycleThrough(accepting)

Result

• 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

Export

• New translation to the JANI interchange format

Bug fixing:

• Fixed an issue met in v3 when a division by 0 is encountered.

Benchmarks

• Entire refactoring of the benchmarks library [AMP21]