Erroring on SimpleProgram.tla from Lamport's tutorial

Skip to first unread message

Jun 18, 2021, 10:47:54 PMJun 18
to tlaplus

Hello all!
I'm getting back into TLA+, but the SimpleProgram.tla from Lamport's demo is erroring with this trace:
TLC2 Version 2.16 of 31 December 2020 (rev: cdddf55)
Running breadth-first search Model-Checking with fp 99 and seed -205797279665965416 with 4 workers on 8 cores with 1180MB heap and 2653MB offheap memory [pid: 216691] (Linux 5.10.30-1-MANJARO amd64, AdoptOpenJDK 14.0.1 x86_64, OffHeapDiskFPSet, DiskStateQueue).
Starting SANY...
Parsing file /home/mrg/projects/tla/Simple2.toolbox/Model_1/MC.tla
Parsing file /home/mrg/projects/tla/Simple2.toolbox/Model_1/Simple2.tla
Parsing file /home/mrg/deps/toolbox/plugins/org.lamport.tlatools_1.0.0.202012311918/tla2sany/StandardModules/TLC.tla
Parsing file /home/mrg/deps/toolbox/plugins/org.lamport.tlatools_1.0.0.202012311918/tla2sany/StandardModules/Integers.tla
Parsing file /home/mrg/deps/toolbox/plugins/org.lamport.tlatools_1.0.0.202012311918/tla2sany/StandardModules/Naturals.tla
Parsing file /home/mrg/deps/toolbox/plugins/org.lamport.tlatools_1.0.0.202012311918/tla2sany/StandardModules/Sequences.tla
Parsing file /home/mrg/deps/toolbox/plugins/org.lamport.tlatools_1.0.0.202012311918/tla2sany/StandardModules/FiniteSets.tla
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module Simple2
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module MC
SANY finished.
Starting... (2021-06-18 21:44:27)
TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.NoClassDefFoundError
: tlc2/value/impl/KSubsetValue
Finished in 561ms at (2021-06-18 21:44:27)

Can anyone help?

Markus Kuppe

Jun 18, 2021, 11:30:38 PMJun 18

you seem to be hit by what was covered in issue #22 [1]. I've just
verified, and #22 is fixed in the Toolbox 1.7.1 release. Please check
your version of the CommunityModules.jar? If you can't make it work, I
suggest we move the discussion to issue #22.


Reply all
Reply to author
0 new messages