Error in resets

[schlepil]

Hi everyone,

there is a bug in how the resets are performed if multiple "diagonal" updates are performed.
In the current code they are performed sequentially instead of "at once".

For instance if there are the clocks x,y and z and we have the resets
y':=x and z':=y the result will be
x'=x, y'=x and z'=x as the update y':=x is performed before z':=y and therefore y is already y'.

The error can be reproduced with the attached tchecker file.
I wrote a fix for the problem (see pull-request), but only for normal dbm's, not offset-dbm's.

A+
Philipp

multiple_value_reset.txt

[fredher]

Dear Philipp,

Thanks for reporting this problem. The assignments in TChecker input file format are supposed to be sequential. This may not be clear enough in the documentation (https://github.com/ticktac-project/tchecker/wiki/TChecker-file-format#statements), so I will clarify it.

Notice that this follows UPPAAL's semantics: "Note: Assignments are evaluated sequentially (not concurrently) (source: UPPAAL's documentation).

This choice is more natural (although it can be discussed), since when writing i=i+1; j=i one usually expects to get j=i and not j=i-1 at the end. So, if you put clock assignments in the middle, they should have the same semantics: x=y+1; i=i+1; z=x+1; j=i should be executed sequentially as well.

Best regards,
Frédéric

[fredher]

I forgot to add in my previous message that we can extend TChecker with parallel assignments if you need this feature. For instance, the syntax could be:

i=1; x=y+i || z=x+1; i=i+1     (read as: i=1; (x=y+i || z=x+1); i=i+1)

with the following semantics:

• first i is assigned value 1
• then the tuple <x,y> takes value <y+i,x+1> (i.e. <y+1,x+1>)
• then i takes value i+1

So the grammar of statements would be a sequence of assignments (i.e. assignments applied sequentially), where each assignment is either an atomic assignment like i=i+1 or a parallel assignment like x=y+i || x=x+1 (i.e. a parallel composition of atomic assignments).

statement ::= simple_statement
           |  simple_statement ; statement

simple_statement ::= parallel_assignment
                  |  nop

parallel_assignment ::= atomic_assignment
                     |  atomic_assignment || parallel_assignment

atomic_assignment ::=  lvalue = rvalue

lvalue ::= ...

rvalue ::= ...

Let me know if you need it.