EWD998 model checking failure when running TLC from outside tlaplus/examples repo

[ahelwer]

Steps to reproduce:

1. Open shell and navigate to directory above tlaplus/examples repo
2. Run ./examples/.github/scripts/linux-setup.sh examples/.github/scripts examples/deps true to install dependencies on Linux & macOS
3. Run the following command to execute TLC:

   java -Dtlc2.TLC.ide=Github -Dutil.ExecutionStatisticsCollector.id=abcdef60f238424fa70d124d0c77ffff -XX:+UseParallelGC -cp examples/deps/tools/tla2tools.jar:examples/deps/community/modules.jar:examples/deps/tlapm/library tlc2.TLC examples/specifications/ewd998/EWD998ChanTrace.tla -config examples/specifications/ewd998/EWD998ChanTrace.cfg -workers auto -lncheck final -cleanup

   Observe the following error:

   TLC2 Version 2.18 of Day Month 20?? (rev: 23f7650)
   Running breadth-first search Model-Checking with fp 125 and seed 7822221676660054780 with 8 workers on 8 cores with 3541MB heap and 64MB offheap memory [pid: 34002] (Linux 6.8.2-arch2-1 amd64, N/A 22 x86_64, MSBDiskFPSet, DiskStateQueue).
   Parsing file /home/ahelwer/src/tlaplus/examples/specifications/ewd998/EWD998ChanTrace.tla
   Parsing file /home/ahelwer/src/tlaplus/examples/specifications/ewd998/EWD998Chan.tla
   Parsing file /tmp/tlc-16960620422673853593/Json.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/Json.tla)
   Parsing file /tmp/tlc-16960620422673853593/TLC.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
   Parsing file /tmp/tlc-16960620422673853593/IOUtils.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/community/modules.jar!/IOUtils.tla)
   Parsing file /tmp/tlc-16960620422673853593/VectorClocks.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/community/modules.jar!/VectorClocks.tla)
   Parsing file /tmp/tlc-16960620422673853593/_TLCTrace.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla)
   Parsing file /tmp/tlc-16960620422673853593/Integers.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
   Parsing file /tmp/tlc-16960620422673853593/Sequences.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
   Parsing file /tmp/tlc-16960620422673853593/FiniteSets.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
   Parsing file /home/ahelwer/src/tlaplus/examples/specifications/ewd998/Utils.tla
   Parsing file /tmp/tlc-16960620422673853593/Naturals.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
   Parsing file /tmp/tlc-16960620422673853593/Functions.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/community/modules.jar!/Functions.tla)
   Parsing file /tmp/tlc-16960620422673853593/SequencesExt.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/community/modules.jar!/SequencesExt.tla)
   Parsing file /home/ahelwer/src/tlaplus/examples/specifications/ewd998/EWD998.tla
   Parsing file /tmp/tlc-16960620422673853593/Randomization.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/Randomization.tla)
   Parsing file /tmp/tlc-16960620422673853593/Folds.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/community/modules.jar!/Folds.tla)
   Parsing file /tmp/tlc-16960620422673853593/FiniteSetsExt.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/community/modules.jar!/FiniteSetsExt.tla)
   Parsing file /home/ahelwer/src/tlaplus/examples/specifications/ewd998/AsyncTerminationDetection.tla
   Parsing file /tmp/tlc-16960620422673853593/TLCExt.tla (jar:file:/home/ahelwer/src/tlaplus/examples/deps/tools/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla)
   Semantic processing of module Naturals
   Semantic processing of module Integers
   Semantic processing of module Sequences
   Semantic processing of module FiniteSets
   Semantic processing of module TLC
   Semantic processing of module Folds
   Semantic processing of module Functions
   Semantic processing of module FiniteSetsExt
   Semantic processing of module SequencesExt
   Semantic processing of module Utils
   Semantic processing of module Randomization
   Semantic processing of module AsyncTerminationDetection
   Semantic processing of module EWD998
   Semantic processing of module EWD998Chan
   Semantic processing of module Json
   Semantic processing of module IOUtils
   Semantic processing of module VectorClocks
   Semantic processing of module TLCExt
   Semantic processing of module _TLCTrace
   Semantic processing of module EWD998ChanTrace
   Starting... (2024-04-07 09:56:50)
   Error: The configuration file substitutes constant N with non-constant TraceN - specifically: Attempted to apply the operator overridden by the Java method
   public static tlc2.value.IValue tlc2.overrides.Json.ndDeserialize(tlc2.value.impl.StringValue) throws java.io.IOException,
   but it produced the following error:
   specifications/ewd998/EWD998ChanTrace.ndjson (No such file or directory)
   Finished in 00s at (2024-04-07 09:56:50)

   Found during execution of CI in tlaplus/tlaplus repo. It seems like a path is hardcoded somewhere assuming cwd is repo root.

[lemmy]

How can this particular model be excluded from being checked? It seems one can only skip a folder with .ciignore.

[ahelwer]

You can use the -skip parameter in the CI, I added it to my Unicode PR

[lemmy]

Where does -skip go?

[ahelwer]

It's already being used, look at the existing PR CI in tlaplus/tlaplus. The model doesn't have to be skipped in this repo's CI because it passes just fine.

[ahelwer]

Here is the change that currently lives in my unicode branch omitting checking this file using -skip: https://github.com/tlaplus/tlaplus/blob/b90fa3b1ff3b95cb45a1a7aa1a0e67da6f64bbe6/.github/workflows/pr.yml#L120