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

Re: TLA+ Toolbox 1.5.5 release - please update



After update, when running the model checker I get a modal dialog box pop up saying "TLC run for Model_1 has encountered a problem. An internal error occurred during: TLC run for Model_1" with detail:

An internal error occurred during: "TLC run for Model_1".
tlc2.tool.fp.OffHeapDiskFPSet.isSupported()Z

I've attached all relevant files. Toolbox version:

This is Version 1.5.5 of 05 January 2018 and includes:
  - SANY Version 2.1 of 23 July 2017
  - TLC Version 2.11 of 05 January 2018
  - PlusCal Version 1.8 of 07 December 2015
  - TLATeX Version 1.0 of 20 September 2017

I'm on Windows 10 with the following Java version:

java version "1.8.0_151"
Java(TM) SE Runtime Environment (build 1.8.0_151-b12)
Java HotSpot(TM) 64-Bit Server VM (build 25.151-b12, mixed mode)

Andrew

On Monday, January 8, 2018 at 7:26:20 AM UTC-8, Markus Alexander Kuppe wrote:
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/

Attachment: .project
Description: Binary data

Attachment: RiverCrossing___Model_1.launch
Description: Binary data

Attachment: org.lamport.tla.toolbox.prefs
Description: Binary data

\* CONSTANT definitions
CONSTANT
People <- const_15154468443212000
\* CONSTANT definitions
CONSTANT
TimeLimit <- const_15154468443223000
\* INIT definition
INIT
init_15154468443224000
\* NEXT definition
NEXT
next_15154468443225000
\* INVARIANT definition
INVARIANT
inv_15154468443226000
inv_15154468443227000
inv_15154468443228000
\* Generated on Mon Jan 08 13:27:24 PST 2018

Attachment: MC.out
Description: Binary data

Attachment: MC.tla
Description: Binary data

Attachment: RiverCrossing.tla
Description: Binary data