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

Re: [tlaplus] Erroring on SimpleProgram.tla from Lamport's tutorial


On 18.06.21 19:47, migu...@xxxxxxxxxxxxxxxx wrote:


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?


Hi,
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. 

Thanks,
Markus

[1] https://github.com/tlaplus/CommunityModules/issues/22

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/85bd97a4-633e-7106-baf8-8227dbf58a7f%40lemmster.de.