search

tlaplus / Examples

A collection of TLA⁺ specifications of varying complexities
Other
1.29k stars 200 forks source link

Models failing smoke testing #65

Closed ahelwer closed 1 year ago

ahelwer commented 1 year ago 
# 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 commented 1 year ago

'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 commented 1 year ago

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

ahelwer commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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