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

*From*: Markus Alexander Kuppe <tlaplus-go...@xxxxxxxxxxx>*Date*: Mon, 8 Jan 2018 11:25:49 -0800 (PST)

Hi,

a new TLA+ Toolbox 1.5.5 release has been made available [1][2]. This

release primarily fixes a rare but serious bug that has been in TLC

since its initial implementation. TLC could generate an incorrect set

of initial states, and hence not examine all reachable states, in the

following situation:

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.

An example 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 == /\ \/ var \in 0..99 /\ var % 2 = 0

\/ var = -1

/\ ...

We advise all users to update as soon as possible.

Thanks

Markus

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

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

a new TLA+ Toolbox 1.5.5 release has been made available [1][2]. This

release primarily fixes a rare but serious bug that has been in TLC

since its initial implementation. TLC could generate an incorrect set

of initial states, and hence not examine all reachable states, in the

following situation:

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.

An example 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 == /\ \/ var \in 0..99 /\ var % 2 = 0

\/ var = -1

/\ ...

We advise all users to update as soon as possible.

Thanks

Markus

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

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

**Follow-Ups**:**TLA+ Toolbox 1.5.5 release - warning incomplete bug fix***From:*Markus Alexander Kuppe

**Re: TLA+ Toolbox 1.5.5 release - please update***From:*Andrew Helwer

**Re: TLA+ Toolbox 1.5.5 release - please update***From:*Andrew Helwer

- Prev by Date:
**Re: Call for papers: ABZ 2018** - Next by Date:
**Re: TLA+ Toolbox 1.5.5 release - please update** - Previous by thread:
**Re: [tlaplus] How can this lemma (involving []) be applied?** - Next by thread:
**Re: TLA+ Toolbox 1.5.5 release - please update** - Index(es):