Models failing smoke testing

[ahelwer]

# Attempted to access index 0 of tuple <<>>
'specifications/SpecifyingSystems/AdvancedExamples/MCInnerSerial.cfg',
# Attempted to select nonexistent field "traces" from record
'specifications/ewd426/SimTokenRing.cfg',
# Initial error cannot find TLAPS; if fixed, cannot find property "Stable"
'specifications/ewd998/AsyncTerminationDetection_proof.cfg',
# Property is violated by the initial state
'specifications/ewd998/SmokeEWD998.cfg'

[lemmy]

'specifications/ewd998/AsyncTerminationDetection_proof.cfg'

The proof relies on reasoning about ENABLED and will, thus, only work with the upcoming TLAPS 1.5.

'specifications/ewd998/SmokeEWD998.cfg'

Running TLC in simulation mode makes TLC not report the violation of refinement.

The underlying problem is that the Init predicates of AsyncTerminationDetection and EWD998 should be changed to hold for counter and pending values that satisfy EWD998!Inv!P0. @muenchnerkindl I don't have TLAPS 1.5 available. Can you please check if "weakening" Init in the two specs does not break the existing proofs?

[muenchnerkindl]

The same holds for specifications/ewd998/EWD998_proof.tla.

[ahelwer]

There is one other thing which doesn't really constitute a bug but does keep the model from being smoke-tested. SimKnuthYao.cfg requires certain number of states to have been generated before termination or else it fails. This makes it not amenable to smoke-testing by running it for five seconds. Not sure how this could be reconciled really.

[lemmy]

The CI could preprocess SimKnuthYao.cfg and comment POSTCONDITION PostCondition before the CI executes. I don't think it is worth it, though, and suggest to simply ignore this spec.

[ahelwer]

These are nearly all fixed except SimTokenRing fails on Windows with this error:

Error: Attempted to apply the operator overridden by the Java method
public static tlc2.value.impl.Value tlc2.overrides.IOUtils.ioExec(tlc2.value.impl.Value) throws java.io.IOException,java.lang.InterruptedException,
but it produced the following error:
Cannot run program "/usr/bin/env": CreateProcess error=2, The system cannot find the file specified
While working on the initial state:
c = (0 :> 0 @@ 1 :> 0 @@ 2 :> 0 @@ 3 :> 0 @@ 4 :> 0 @@ 5 :> 0 @@ 6 :> 0)


The number of states generated: 823543
Simulation using seed 7810331937980164339 and aril 0

Finished in 01s at (2023-02-14 15:59:50)

It succeeds on Linux and MacOS, see this workflow run: https://github.com/tlaplus/Examples/actions/runs/4175552460/jobs/7230627213

[lemmy]

SmokeTokenRing is not intended to work on Windows (should work on WSL).