search

tlaplus / tlaplus

TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.
https://lamport.azurewebsites.net/tla/tla.html
MIT License
2.26k stars 189 forks source link

Scoping error when referencing substituted state variable through INSTANCE in a liveness property #748

Open fhackett-ms opened 1 year ago

fhackett-ms commented 1 year ago

Description

This example causes TLC to be unable to reference variable i, when using the refinement mapping foo. Many other methods of referencing i work fine, including directly stating Spec1 == test1!Spec, where test1!Spec contains an equivalent definition, changing only how operators inside test1 are referenced.

I found this because my real spec requires me to specify a slightly different Spec1, relative to test1!Spec, so I expanded and altered the definition in my top-level spec, causing the issue.

---- MODULE test ----
EXTENDS Naturals

VARIABLE i

vars == <<i>>

foo == i - 6

test1 == INSTANCE test1

Spec1 ==
    /\ test1!Init
    /\ [][test1!Next]_vars
    /\ WF_vars(test1!Next)

Init ==
    /\ i = 7

Next ==
    /\ i' = i + 1

Spec ==
    /\ Init
    /\ [][Next]_vars

THEOREM Spec => test1!Spec

====
---- MODULE test1 ----
EXTENDS Naturals

VARIABLE foo

vars == <<foo>>

Init ==
    /\ foo = 1

Next ==
    /\ foo' = foo + 1

Spec ==
    /\ Init
    /\ [][Next]_vars
    /\ WF_vars(Next)

====

With config:

SPECIFICATION Spec
PROPERTIES Spec1

Expected Behavior

(by changing to Spec1 == test1!Spec)

java -Xmx50g -cp /workspaces/azure-cosmos-db/tools/tla2tools.jar -DTLA-Library=/workspaces/azure-cosmos-db/CommunityModules-deps.jar -XX:+UseParallelGC tlc2.TLC test.tla -tool -modelcheck -config test.cfg -gzip -metadir /tmp -cleanup -workers auto

TLC2 Version 2.18 of Day Month 20?? (rev: d5baa32)
Running breadth-first search Model-Checking with fp 31 and seed 300072030778518226 with 32 workers on 32 cores with 45511MB heap and 64MB offheap memory [pid: 28759] (Linux 5.4.0-1086-azure amd64, Oracle Corporation 17.0.2 x86_64, MSBDiskFPSet, DiskStateQueue).
Starting SANY...
Parsing file /workspaces/azure-cosmos-db/simple-model/test.tla
Parsing file /tmp/tlc-2011723707208327597/Naturals.tla (jar:file:/workspaces/azure-cosmos-db/tools/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/test1.tla (/workspaces/azure-cosmos-db/simple-model/test.tla)
Semantic processing of module Naturals
Semantic processing of module test1
Semantic processing of module test
SANY finished.
Starting... (2022-08-03 21:26:27)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2022-08-03 21:26:27.
Checking temporal properties for the current state space with 786463 total distinct states at (2022-08-03 21:26:31)
Temporal properties were violated.
The following behavior constitutes a counter-example:
1: <Initial predicate>
i = 7
2: Stuttering
Finished checking temporal properties in 00s at 2022-08-03 21:26:31
Progress(786464) at 2022-08-03 21:26:31: 786,464 states generated (12,576,716 s/min), 786,464 distinct states found (12,576,716 ds/min), 1 states left on queue.
786464 states generated, 786464 distinct states found, 1 states left on queue.
The depth of the complete state graph search is 786464.
Finished in 3756ms at (2022-08-03 21:26:31)

Actual Behavior

java -Xmx50g -cp /workspaces/azure-cosmos-db/tools/tla2tools.jar -DTLA-Library=/workspaces/azure-cosmos-db/CommunityModules-deps.jar -XX:+UseParallelGC tlc2.TLC test.tla -tool -modelcheck -config test.cfg -gzip -metadir /tmp -cleanup -workers auto

TLC2 Version 2.18 of Day Month 20?? (rev: d5baa32)
Running breadth-first search Model-Checking with fp 87 and seed 6535673262321096158 with 32 workers on 32 cores with 45511MB heap and 64MB offheap memory [pid: 27329] (Linux 5.4.0-1086-azure amd64, Oracle Corporation 17.0.2 x86_64, MSBDiskFPSet, DiskStateQueue).
Starting SANY...
Parsing file /workspaces/azure-cosmos-db/simple-model/test.tla
Parsing file /tmp/tlc-5734856578524846382/Naturals.tla (jar:file:/workspaces/azure-cosmos-db/tools/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/test1.tla (/workspaces/azure-cosmos-db/simple-model/test.tla)
Semantic processing of module Naturals
Semantic processing of module test1
Semantic processing of module test
SANY finished.
Starting... (2022-08-03 21:23:09)
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2022-08-03 21:23:10.
The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. Line 15, column 16 to line 15, column 25 in test
1. Line 10, column 1 to line 10, column 23 in test
2. Line 12, column 5 to line 12, column 21 in test1
3. Line 12, column 8 to line 12, column 21 in test1
4. Line 12, column 8 to line 12, column 11 in test1
5. Line 12, column 8 to line 12, column 10 in test1
6. Line 10, column 1 to line 10, column 23 in test
7. Line 8, column 8 to line 8, column 12 in test
8. Line 8, column 8 to line 8, column 8 in test
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.RuntimeException
: 
In evaluation, the identifier i is either undefined or not an operator.
line 8, col 8 to line 8, col 8 of module test
The behavior up to this point is:
1: <Initial predicate>
i = 7
2: <Next line 21, col 5 to line 21, col 17 of module test>
i = 8
Progress(22) at 2022-08-03 21:23:10: 22 states generated (2,241 s/min), 22 distinct states found (2,241 ds/min), 1 states left on queue.
22 states generated, 22 distinct states found, 1 states left on queue.
The depth of the complete state graph search is 22.
The average outdegree of the complete state graph is 1 (minimum is 1, the maximum 1 and the 95th percentile is 1).
Finished in 594ms at (2022-08-03 21:23:10)

Steps to Reproduce

See above.

Steps Taken to Fix

I minimized the issue, isolating what I think is the specific thing I did that caused it. Because of how specific the problem is and how every other variation works, I'm confident it's not an error in my TLA+ code.

Possible Fix

This is probably a bug in TLC's scope handling, an edge case that comes from mixing ! and non-trivial INSTANCE substitutions in an unexpected pattern.

Your Environment

It is listed in the outputs I provide, as part of TLC's command-line output.

Calvin-L commented 1 year ago

Unlike #725 (which is related), I believe this is not actually a bug, but just a very confusing error message.

In the test module, the expression WF_vars(test1!Next) breaks down like this:

WF_vars(test1!Next)
    = ([]<>(~ENABLED <test1!Next>_vars)) \/ ([]<> <test1!Next>_vars)
    =    ... ENABLED (test1!Next /\ vars' /= vars) ...
    =    ... ENABLED ((i - 6)' = (i - 6) + 1 /\ i' /= i) ...
    =    ... ENABLED ((i' - 6) = (i - 6) + 1 /\ i' /= i) ...
    =    ... \E i_prime: (i_prime - 6) = (i - 6) + 1 /\ i_prime /= i ...

TLC is unable to evaluate that last expression; it isn't smart enough to synthesize a value for i_prime that satisfies the formula. This is the exact same error you would see if you wrote e.g. Next == foo' = foo + 1 in module test and disabled liveness checking entirely. foo' = foo+1 is the same as i' - 6 = (i - 6) + 1, and TLC isn't smart enough to figure out what to do with that either.

Oh, and another quick (?) note:

Many other methods of referencing i work fine, including directly stating Spec1 == test1!Spec

Unfortunately, within the test module, Spec1 and test1!Spec are not actually equivalent! I left a comment about this here. Because they are different, you should not expect TLC to handle them the same way.

For comparison, within test, the WF-expression within test1!Spec desugars like this:

test1!Spec = ... WF_vars(Next) ...                                                   [with foo <- i - 6]
           = ... ([]<>(~ENABLED <Next>_vars)) \/ ([]<> <Next>_vars) ...              [with foo <- i - 6]
           =        ... ENABLED (Next /\ vars' /= vars) ...                          [with foo <- i - 6]
           =        ... ENABLED (foo' = foo + 1 /\ foo' /= foo) ...                  [with foo <- i - 6]
           =        ... \E foo_prime: foo_prime = foo + 1 /\ foo_prime /= foo ...    [with foo <- i - 6]
           =        ... \E foo_prime: foo_prime = (i - 6) + 1 /\ foo_prime /= (i - 6)

This is a different expression, and it is one that TLC can handle, since there is a plain variable on the left side of the equals sign. So, it can synthesize values for foo_prime that satisfy the expression.