Goal

Create 4 models containing :

• False guard
• True guard
• Discrete guard
• Continuous guard
• Discrete continuous guard

has invariant should be only "False" when there is True guard

Finish

Tests created and all passed

Several filenames in benchmark directory contain the character ":" which results in an illegal file name under Windows.
As a result, the imitator repository cannot be checked out under Windows.
Example:
error: invalid path 'benchmarks/ATM/fig1-DCLXZL18:fixed.imi'

Description

Missing parenthesis on arithmetic and boolean expressions on parsing structure

Description

A Not_Found error is raised when we using a variable in a init expression (discrete or continuous section) that was previously removed by auto remove. This bug already exist in version 3.0.0.

Example :

int i;
(* i is not used *)

b := i > 0

Solution

Variables that are dependent of a used variable are keep.

Goal

Study of binary word expressions integration:

• Literal form of binary word
• Operations we can make on binary word expressions
• Definition of functions that can act on binary word expressions

Finish

The study is validated by Etienne and collaborators.

Description

An error is raised when using a constant and a literal in the init section, because the literal is not inferred before the init expression trying to reduce.

Example :

b := i = 0 with i = 0 : int;

Solution

Just have to return inferred expression when doing the type checking on assignment. Then use this inferred expression when trying to reduce.

Allow several reachability conditions… and not only one loc in one PTA
(at least several pairs PTA/location or, even better, pairs PTA/set of locations)

Allow committed locations in the input model.
Problem: need to consider multiple orderings between variables, and hence multiple successor states.

Finish

• not operator is moved in grammar, parsing structure, abstract model
• not operator is moved on all pattern matching
• All non regression tests pass successfully
• Behavior of IMITATOR with not is the same as previously

Goal

Add a pow function that compute power of an arithmetic expression.

Finish

• Can use pow function without parsing error
• pow function used with a non arithmetic expression should raise a type error
• pow function has correct behavior
• Non regression tests are created and all passed : type checking, pow function works
• Use manual, grammar and built-in functions section are updated

Add the automaton name in the following warning:

*** Warning: The synclab 'yUp' is not used in some of the automata where it is declared: it will thus be removed.

Allow urgent locations in the input model.
No theoretical issue (and can be already be simulated using an extra clock), but having it coded in the tool would probably make the analysis faster.

Allowing testing locations of automata in guards:
e.g.
when x > p & i <> 1 & loc[pta1] = loc1 & loc[pta2] <> loc2 do …

Additional questions: what about invariants?
invariant x > p & i <> 1 & loc[pta1] = loc1 & loc[pta2] <> loc2
needs to control whether pta1 stays in loc1 and pta2 stays out of loc2 during the entire time when this invariant is satisfied. Not easy! Just forbid this syntax in invariants?!

Goal

Compare grammar of manual with grammar parser

Finish

• Grammar manual and grammar parser are equivalent
• Grammar manual highlight semantic use

Description

We can assign a int to a clock / parameter in continuous init. The behavior of IMITATOR is altered, so we should forbid incompatible type assignment.

Solution

We check that all constraints initialization only use rational valued variables.

Goal

We can use shift_left(b, i), shift_right(b, i), fill_left(b, i) and fill_right(b, i)` logical functions on binary word expressions.

Finish

• No parsing error
• We can use shift_left(b, i), shift_right(b, i), fill_left(b, i) and fill_right(b, i)` functions in inits / constant declarations / guards / invariants / updates / conditionals
• shift_left(b, i), shift_right(b, i), fill_left(b, i) and fill_right(b, i)` functions behavior is correct
• Type checking is make and correct
• Non regression tests created and succeed

Description

There is a parsing error when comparing variable, constant to literal boolean.
For example :
b = True should be written as b = (True) in order to work.

Solution

We have to move True and False literals from boolean_expression to discrete_boolean_expression and manage it as constants.

Goal

We can use logand(b1, b2), logor(b1, b2), logxor(b1, b2) and lognot(b) bitwise logical functions on binary word expressions.

Finish

• No parsing error
• We can use functions in inits / constant declarations / guards / invariants / updates / conditionals
• functions behavior is correct
• Type checking is make and correct
• Non regression tests created and succeed
• User manual updated

Allow symbolic variables, equivalent to "clocks" stopped in any location (no elapsing, but can be compared to, and assigned to, clocks and parameters).
E.g.:

s : symbolic;

invariant x < s + p 
when x = s + p - 1 do {x := s; s := p + i} goto …

So implementation would be a simple equivalence to stopwatches.

Goal

Check that is not possible to compare two boolean with ordinal operator

Finish

• An error is raised when comparing two boolean with any ordinal operator
• Non regression tests created

Consider the following PTA:

var x,y: clock;
automaton P
   loc s0: invariant True when x<=1 goto s0;
end
init := loc[P]=s0 & x>=0 & x=y;

This PTA is refuted by imitator:
imitator error1.imi

Apparently, clock y is removed, despite the fact that it is used in the initial condition.
But then imitator complains that clock y has not been declared:

*** Warning: The clock `y` is declared but never used in the model; it is therefore removed from the model.
*** ERROR: The variable `y` used in a linear constraint was not declared.

In the attached model (see here: Sched2.50.0.zip) the safe set is reported as

  b >= 10
 & C3_WORST >= 20
 & 50 > b + C3_WORST
 & 22 >= b

which includes the point C3_WORST=19 & b=23.

However, modifying the model to add these as initial constraints and re-running with -mode EF leads to the False predicate over the parameters (modified model included in zip).

This is also validated by translating the model to uppaal.

A possibly valid set of (negative) constraints is given in SMT-format here:
https://rise4fun.com/Z3/xhg6

Description

When initializing a constant with not compatibles types or operators, it raise a fatal exception ComputingException. We should handle theses exceptions.

Study

Type checking is made after constants evaluations !

for example run FlipFlop example with command : mpiexec -n 4 ./bin/imitator ~/imitator/examples/Flipflop/flipflop.imi ~/imitator/examples/Flipflop/flipflop.v0 -mode cover -distributed sequential

END OF THE BEHAVIORAL CARTOGRAPHY ALGORITHM
[Worker 3] Total waiting time : 2.37452983857 s
[Worker 3] Total working time : 65.4569101334 s
[Worker 3] Occupancy : 96.499366902 %
Size of V0: 2000
Unsuccessful points: 3461016356684568350
139 different constraints were computed.
Average number of states : 473
Average number of transitions : 705
Global time spent : 67.8365471364 s
Time spent on IM : 189.584782363 s
Time spent to compute next point: 2.1892092228 s

[Master] Total waiting time : 64.8895375729 s

Add new algorithm AF-synthesis (see, e.g., [JLR13, TACAS]).

(this is just a first test of handling features using github)

Description

• Add necessary grammar rules that permit declaration and use of array as variable or literal
• Add type inference and type checking on array
• Add possibility to declare and use nested array
• Add possibility to compare structurally two arrays
• Add possibility to use arrays in property

Finish

• We can declare and use array of any discrete type
• Literal numbers of arrays are correctly inferred
• Array are correctly type checked
• Comparison of two arrays has a correct behavior

Goal

Introduce a new type: binary word. It's a type that represent an array of bits. We should be able to make any bit-wise logical operations on binary word.

Goal

We can use mod(x, i) functions on arithmetic expressions.

Finish

• No parsing error
• We can use mod(x, i) function in inits / constant declarations / guards / invariants / updates / conditionals
• mod(x, i) function behavior is correct
• Type checking is make and correct
• Non regression tests created and succeed

So far, we have:

" Final constraint such that the property is violated (0 inequalities): "

A more explicit would be welcome.

Goal

In case we doesn't want to use a property file, it can be useful to call IMITATOR with a given property directly in command line

Description

Should update grammar of new init section in user manual.

Finish

• User manual is updated according lex grammar

Goal

• Rename regression tests
• Rename in test data

Finish

• All regression tests renamed
• All regression tests succeed

Signal the potential deadlocks (i.e., for some parameter valuations and/or for some clock values, a deadlock is possible) on the trace set output as a graphics.

Description

JSON format for Jani specification seems to be wrong when converting complex expression. For example :

when True do { b := b1 = b2 } goto lend; was converted to {"ref": "b", "value" : b1 = b2}

Solution

Add (or correct!) a "verbose" mode that only displays the result. Useful to compare the speed of algorithms without being slowed down by pretty printings.

Currently, "not equal" can be simulated with 2 transitions, one using >, the other using <.
But a syntax allowing "not equal" (<> or =!=) would be more intuitive and make models more compact.

The following program raises an exception (The variable 'x2' used in a linear constraint was not declared.) because of the automated variable elimination.

var

(* Clocks *)
 	x1, x2
		: clock;

(************************************************************)
  automaton myPTA
(************************************************************)
synclabs: ;

loc myLoc: while True wait {}

end (* train *)


(************************************************************)
(* Initial state *)
(************************************************************)

init :=
	(*------------------------------------------------------------*)
	(* Initial location *)
	(*------------------------------------------------------------*)
	& loc[myPTA]     = myLoc

	(*------------------------------------------------------------*)
	(* Initial clock constraints *)
	(*------------------------------------------------------------*)
		&
		x1 > x2
;


(************************************************************)
(* The end *)
(************************************************************)
end

Goal

Add a cast_rational_to_int function that try to convert a rational expression to an int expression.

Finish

• Can use cast_rational_to_int function without parsing error
• cast_rational_to_int function used with a non arithmetic expression should raise a type error
• cast_rational_to_int function used with a int expression should raise a type error
• cast_rational_to_int function has correct behavior
• Non regression tests are created and all passed : type checking, cast_rational_to_int function works
• User manual, grammar and built-in functions section are updated

Goal

Able to compare two boolean expressions with relational operators

Finish

• Able to compare two boolean expressions, nested boolean expressions with no error
• Non regression tests created
• All non regression tests pass successfully

Goal

Create a int function for making int from literals

Description

• Add necessary grammar rules that permit access to an array or nested array
• Add type inference and type checking on array access
• Add possibility to use array access in property

Finish

• We can access to an element of an array
• Element types of arrays are correctly inferred and type checked

Allow to check other PTA's location in guard conditions

Description

• Ability to create array of any discrete type
• Ability to access to an element of an array
• Add some utility functions on array

Goal

We can use new binary word type through variables, constant and literal form.

Finish

• We can declare a binary word constant or variable
• We can initialize a binary word expressions
• We can compare two binary word expressions
• We can use literal binary word in guards / invariant / update / conditionals
• Type checking on binary word is correct
• The behavior when comparing two binary word expressions is correct
• Non regression tests created and succeed
• User manual updated

Goal

Permit boolean comparison with equal, different operator in any non linear expression : guard, invariant, update, conditional.

Finish

• We can compare two boolean expressions without any syntax or semantic error
• We cannot compare two boolean expression with relational operator
• The behavior of IMITATOR reachability algorithm is correct
• Boolean expression comparison are correctly printed (graphics, translation)
• New and old non regression tests pass with success

Description

A Not_Found error is raised when assign a constant in a discrete init

var 
    x,
        : clock;
    i = 1, 
        : int;
    p
        : parameter;

init := {

    discrete = 
        i := 1
    ;
    
}

## Solution

I just had to check that variable is a constant or variable. In case of constant, it raise an `InvalidExpression` exception with an appropriate message. 

Goal

We can use int_of_binary(b), binary_of_int(i) functions on binary word expressions.

Finish

• No parsing error
• We can use functions in inits / constant declarations / guards / invariants / updates / conditionals
• functions behavior is correct
• Type checking is make and correct
• Non regression tests created and succeed
• User manual updated

Goal

Create non regressions tests that try to make a full coverage of type checking on guard, invariant, constants declarations, init section, assignment, conditional expression

Finish

• All non regression tests are make
• All tests pass successfully

Description

Being able to initialize a constant with another previously declared constant. For the moment it raise an error "Assignment of variable x is forbidden" because it doesn't found any constant in parsed_model, when reducing the parse tree at let evaluated_constants

Example :

    i = 1, j = i + 1
        : rational;

Finish

• We are able to initialize a constant with another constant without any semantic or syntactic error
• Behavior is correct
• Non regression test init_state/init-constant-with-constant pass