[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Markus Alexander Kuppe <tlaplus-go...@xxxxxxxxxxx>*Date*: Wed, 31 Jan 2018 10:45:16 -0800 (PST)

Hi,

a new TLA+ Toolbox 1.5.6 release has been made available [1][2]. This release fixes an uncommon but serious bug in TLC that has existed since its initial implementation. The bug can cause TLC to generate an incorrect set of initial states, or an incorrect set of possible next states when examining a state. Either can cause TLC not to examine all reachable states. The error can occur in the following two cases:

The possible initial values of some variable*var* are specified by a subformula *F(..., var, ...)* in the initial predicate, for some operator *F* such that expanding the definition of *F* results in a formula containing more than one occurrence of *var*, not all occurring in separate disjuncts of that formula.

The possible next values of some variable*var* are specified by a subformula *F(..., var', ...)* in the next-state relation, for some operator *F* such that expanding the definition of *F* results in a formula containing more than one occurrence of *var'* , not all occurring in separate disjuncts of that formula.

An example of the first case is an initial predicate*Init* defined as follows:

VARIABLES x, ...

F(var) == \/ var \in 0..99 /\ var % 2 = 0

\/ var = -1

Init == /\ F(x)

/\ ...

The error would not appear if*F* were defined by:

F(var) == \/ var \in {i \in 0..99 : i % 2 = 0}

\/ var = -1

or if the definition of*F(x)* were expanded in *Init* :

Init == /\ \/ x \in 0..99 /\ x % 2 = 0

\/ x = -1

/\ ...

A similar example holds for case 2 with the same operator*F* and the next-state formula

Next == /\ F(x')

/\ ...

If your specs are affected by the bug described above, you should re-run TLC on them.

Please consult the changelog for a list of all noteworthy changes [3].

Thanks

Markus

[1] https://github.com/tlaplus/tlaplus/releases/tag/v1.5.6

[2] https://tla.msr-inria.inria.fr/tlatoolbox/products/

[3] https://lamport.azurewebsites.net/tla/toolbox.html#155bug

a new TLA+ Toolbox 1.5.6 release has been made available [1][2]. This release fixes an uncommon but serious bug in TLC that has existed since its initial implementation. The bug can cause TLC to generate an incorrect set of initial states, or an incorrect set of possible next states when examining a state. Either can cause TLC not to examine all reachable states. The error can occur in the following two cases:

The possible initial values of some variable

The possible next values of some variable

An example of the first case is an initial predicate

VARIABLES x, ...

F(var) == \/ var \in 0..99 /\ var % 2 = 0

\/ var = -1

Init == /\ F(x)

/\ ...

The error would not appear if

F(var) == \/ var \in {i \in 0..99 : i % 2 = 0}

\/ var = -1

or if the definition of

Init == /\ \/ x \in 0..99 /\ x % 2 = 0

\/ x = -1

/\ ...

A similar example holds for case 2 with the same operator

Next == /\ F(x')

/\ ...

If your specs are affected by the bug described above, you should re-run TLC on them.

Please consult the changelog for a list of all noteworthy changes [3].

Thanks

Markus

[1] https://github.com/tlaplus/

[2] https://tla.msr-inria.inria.

[3] https://lamport.azurewebsites.net/tla/toolbox.html#155bug

**Follow-Ups**:**Re: [tlaplus] TLA+ Toolbox 1.5.6 release***From:*sglaser.com

- Prev by Date:
**Re: [tlaplus] Verification of Temporal Property** - Next by Date:
**Re: [tlaplus] Verification of Temporal Property** - Previous by thread:
**Re: [tlaplus] Verification of Temporal Property** - Next by thread:
**Re: [tlaplus] TLA+ Toolbox 1.5.6 release** - Index(es):