search

tlaplus / vscode-tlaplus

TLA+ language support for Visual Studio Code
MIT License
353 stars 31 forks source link

Tlaplus > Java: Options ignored by "Evaluate selected expression" #156

Open lemmy opened 4 years ago

lemmy commented 4 years ago

Let A be a module that EXTENDS module B that happens to be in a library L. Library L is added to TLC's classpath in Tlaplus > Java: Options. Ordinary model-checking works fine. However, selecting and evaluating a (constant) expressions fails with:

Error evaluating expression:
Cannot find source file for module B imported in module A.
Parsing or semantic analysis failed.
alygin commented 4 years ago

@lemmy, could you, please, reproduce the error again and check the TLC output channel to see the full command line? Are there any problems with it? Could it be that we have the same case here as in #157 -- switching between Win and WSL2?

lemmy commented 4 years ago

This appears to be a classpath issue. With Java: Options set to -classpath CommunityModules.jar, evaluation fails whereas it succeeds with a full qualified path -classpath /home/markus/blockingqueue/CommunityModules.jar.

Fails:

/usr/lib/jvm/java-11-openjdk-amd64//bin/java -classpath CommunityModules.jar:/home/markus/.vscode-server/extensions/alygin.vscode-tlaplus-1.5.0/tools/tla2tools.jar -XX:+UseParallelGC -Dtlc2.TLC.ide=vscode tlc2.TLC t1592236841015.tla -tool -modelcheck -coverage 0 -config t1592236841015.cfg -deadlock -workers 4 -dump dot BlockingQueue

TLC2 Version 2.15 of Day Month 20?? (rev: eb3ff99)
Running breadth-first search Model-Checking with fp 63 and seed 4041244455921528276 with 4 workers on 8 cores with 17148MB heap and 64MB offheap memory [pid: 307] (Linux 4.19.84-microsoft-standard amd64, Ubuntu 11.0.7 x86_64, MSBDiskFPSet, DiskStateQueue).
Starting SANY...
Parsing file /tmp/vscode-tlaplus-1592236841011/t1592236841015.tla
Parsing file /tmp/vscode-tlaplus-1592236841011/BlockingQueue.tla
Parsing file /tmp/TLC.tla
Parsing file /tmp/Naturals.tla
Parsing file /tmp/Sequences.tla
Parsing file /tmp/FiniteSets.tla
Fatal errors while parsing TLA+ spec in file t1592236841015
tla2sany.semantic.AbortException
*** Abort messages: 1
Unknown location
Cannot find source file for module SequencesExt imported in module BlockingQueue.
SANY finished.
Starting... (2020-06-15 09:00:41)
Parsing or semantic analysis failed.
Finished in 380ms at (2020-06-15 09:00:41)

Works:

/usr/lib/jvm/java-11-openjdk-amd64//bin/java -classpath /home/markus/blockingqueue/CommunityModules.jar:/home/markus/.vscode-server/extensions/alygin.vscode-tlaplus-1.5.0/tools/tla2tools.jar -XX:+UseParallelGC -Dtlc2.TLC.ide=vscode tlc2.TLC t1592237137714.tla -tool -modelcheck -coverage 0 -config t1592237137714.cfg -deadlock -workers 4 -dump dot BlockingQueue

TLC2 Version 2.15 of Day Month 20?? (rev: eb3ff99)
Running breadth-first search Model-Checking with fp 74 and seed -8785635609764670148 with 4 workers on 8 cores with 17148MB heap and 64MB offheap memory [pid: 449] (Linux 4.19.84-microsoft-standard amd64, Ubuntu 11.0.7 x86_64, MSBDiskFPSet, DiskStateQueue).
Starting SANY...
Parsing file /tmp/vscode-tlaplus-1592237137711/t1592237137714.tla
Parsing file /tmp/vscode-tlaplus-1592237137711/BlockingQueue.tla
Parsing file /tmp/TLC.tla
Parsing file /tmp/Naturals.tla
Parsing file /tmp/Sequences.tla
Parsing file /tmp/FiniteSets.tla
Parsing file /tmp/SequencesExt.tla
Parsing file /tmp/vscode-tlaplus-1592237137711/TLAPS.tla
Parsing file /tmp/FiniteSetsExt.tla
Parsing file /tmp/Functions.tla
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module FiniteSetsExt
Semantic processing of module Functions
Semantic processing of module SequencesExt
Semantic processing of module TLAPS
Semantic processing of module BlockingQueue
Semantic processing of module TLC
Semantic processing of module t1592237137714
SANY finished.
Starting... (2020-06-15 09:05:38)
com.fasterxml.jackson dependencies of Json overrides not found, Json module won't work unless the libraries in the lib/ folder of the CommunityModules have been added to the classpath of TLC.
<<"$!@$!@$!@$!@$!", TRUE>>
Computing initial states...
Finished computing initial states: 0 distinct states generated at 2020-06-15 09:05:38.
Model checking completed. No error has been found.
  Estimates of the probability that TLC did not check all reachable states
  because two distinct states had the same fingerprint:
  calculated (optimistic):  val = 0.0
The coverage statistics at 2020-06-15 09:05:38
<Init_1592237137711 line 7, col 1 to line 7, col 18 of module t1592237137714>: 0:0
<Next_1592237137711 line 8, col 1 to line 8, col 18 of module t1592237137714>: 0:0
  line 8, col 32 to line 8, col 65 of module t1592237137714: 0
End of statistics.
Progress(1) at 2020-06-15 09:05:38: 0 states generated (0 s/min), 0 distinct states found (0 ds/min), 0 states left on queue.
0 states generated, 0 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 1.
Finished in 660ms at (2020-06-15 09:05:38)

Model-checking with a relative path:

/usr/lib/jvm/java-11-openjdk-amd64//bin/java -classpath CommunityModules.jar:/home/markus/.vscode-server/extensions/alygin.vscode-tlaplus-1.5.0/tools/tla2tools.jar -XX:+UseParallelGC -Dtlc2.TLC.ide=vscode tlc2.TLC BlockingQueue.tla -tool -modelcheck -coverage 0 -config BlockingQueue.cfg -deadlock -workers 4 -dump dot BlockingQueue

TLC2 Version 2.15 of Day Month 20?? (rev: eb3ff99)
Running breadth-first search Model-Checking with fp 58 and seed 3561912150791825383 with 4 workers on 8 cores with 17148MB heap and 64MB offheap memory [pid: 540] (Linux 4.19.84-microsoft-standard amd64, Ubuntu 11.0.7 x86_64, MSBDiskFPSet, DiskStateQueue).
Starting SANY...
Parsing file /home/markus/blockingqueue/BlockingQueue.tla
Parsing file /tmp/Naturals.tla
Parsing file /tmp/Sequences.tla
Parsing file /tmp/FiniteSets.tla
Parsing file /tmp/SequencesExt.tla
Parsing file /home/markus/blockingqueue/TLAPS.tla
Parsing file /tmp/FiniteSetsExt.tla
Parsing file /tmp/Functions.tla
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module FiniteSetsExt
Semantic processing of module Functions
Semantic processing of module SequencesExt
Semantic processing of module TLAPS
Semantic processing of module BlockingQueue
SANY finished.
Starting... (2020-06-15 09:13:34)
com.fasterxml.jackson dependencies of Json overrides not found, Json module won't work unless the libraries in the lib/ folder of the CommunityModules have been added to the classpath of TLC.
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2020-06-15 09:13:34.
Progress(16) at 2020-06-15 09:13:35: 12,313 states generated, 1,600 distinct states found, 0 states left on queue.
Checking temporal properties for the complete state space with 1600 total distinct states at (2020-06-15 09:13:35)
Temporal properties were violated.
The following behavior constitutes a counter-example:
1: <Initial predicate>
/\ buffer = <<>>
/\ waitSet = {}
2: <Put line 34, col 1 to line 39, col 16 of module BlockingQueue>
/\ buffer = <<p4>>
/\ waitSet = {}
3: <Put line 34, col 1 to line 39, col 16 of module BlockingQueue>
/\ buffer = <<p4, p4>>
/\ waitSet = {}
4: <Put line 34, col 1 to line 39, col 16 of module BlockingQueue>
/\ buffer = <<p4, p4, p3>>
/\ waitSet = {}
5: <Put line 34, col 1 to line 39, col 16 of module BlockingQueue>
/\ buffer = <<p4, p4, p3>>
/\ waitSet = {p1}
6: <Put line 34, col 1 to line 39, col 16 of module BlockingQueue>
/\ buffer = <<p4, p4, p3>>
/\ waitSet = {p1, p2}
7: <Put line 34, col 1 to line 39, col 16 of module BlockingQueue>
/\ buffer = <<p4, p4, p3>>
/\ waitSet = {p1, p2, p4}
8: <Put line 34, col 1 to line 39, col 16 of module BlockingQueue>
/\ buffer = <<p4, p4, p3>>
/\ waitSet = {p1, p2, p3, p4}
9: <Get line 42, col 1 to line 47, col 16 of module BlockingQueue>
/\ buffer = <<p4, p3>>
/\ waitSet = {p1, p2, p4}
10: <Get line 42, col 1 to line 47, col 16 of module BlockingQueue>
/\ buffer = <<p3>>
/\ waitSet = {p1, p2}
11: <Get line 42, col 1 to line 47, col 16 of module BlockingQueue>
/\ buffer = <<>>
/\ waitSet = {p1}
12: <Put line 34, col 1 to line 39, col 16 of module BlockingQueue>
/\ buffer = <<p4>>
/\ waitSet = {p1}
13: <Put line 34, col 1 to line 39, col 16 of module BlockingQueue>
/\ buffer = <<p4, p4>>
/\ waitSet = {p1}
5: Back to state: <Put line 34, col 1 to line 39, col 16 of module BlockingQueue>
Finished checking temporal properties in 00s at 2020-06-15 09:13:35
Progress(16) at 2020-06-15 09:13:35: 12,313 states generated (568,729 s/min), 1,600 distinct states found (73,903 ds/min), 0 states left on queue.
12313 states generated, 1600 distinct states found, 0 states left on queue.
Finished in 1310ms at (2020-06-15 09:13:35)

By the way, you could filter the coverage parameter to improve performance of constant expression evaluation. Likewise, using https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/tool/fp/NoopFPSet.java might shave off a few milliseconds.

alygin commented 4 years ago

Thank you! The cause of the problem is clear now. Expression evaluation is executed in a temporary directory, not in the original one. That's why a relative path has no effect there. I'll fix that.