search

apalache-mc / apalache

APALACHE: symbolic model checker for TLA+ and Quint
https://apalache-mc.org/
Apache License 2.0
439 stars 40 forks source link

Improve documentation of Apalache's behavior when combining state & action invariants #1644

Open heidihoward opened 2 years ago

heidihoward commented 2 years ago

Description

I would expect that if one of two invariants, A and B, are found to be incorrect when separately model checked in Apalache (same length, same spec etc) then A /\ B should also be incorrect. However, this is not always the case if one is a state invariant and one is an action invariant.

Input specification

Invariants.tla from the provided examples with the following addition:

Test1 == 
    /\ Done = {}

Test2 == 
    /\ Test1
    /\ ActionInv

The command line parameters used to run the tool

apalache-mc check --length=1 --inv=Test1 Invariants.tla
apalache-mc check --length=1 --inv=Test2 Invariants.tla

Expected behavior

Test 1 and Test 2 to both find a counter example

Log files

18:34:02.729 [main] INFO  a.f.a.t.Tool$ - Checker options: check --length=1 --inv=Test1 Invariants.tla
18:34:02.735 [main] INFO  a.f.a.t.Tool$ - Tuning: 
18:34:02.740 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser
18:34:03.327 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser [OK]
18:34:03.329 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #1: TypeCheckerSnowcat
18:34:03.329 [main] INFO  a.f.a.t.t.p.EtcTypeCheckerPassImpl -  > Running Snowcat .::.
18:34:03.969 [main] INFO  a.f.a.t.t.p.EtcTypeCheckerPassImpl -  > Your types are purrfect!
18:34:03.969 [main] INFO  a.f.a.t.t.p.EtcTypeCheckerPassImpl -  > All expressions are typed
18:34:03.971 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #1: TypeCheckerSnowcat [OK]
18:34:03.973 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #2: ConfigurationPass
18:34:03.983 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Invariants.cfg: Loading TLC configuration
18:34:03.992 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > No TLC configuration found. Skipping.
18:34:03.995 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Command line option --init is not set. Using Init
18:34:03.996 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Command line option --next is not set. Using Next
18:34:03.998 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set the initialization predicate to Init
18:34:04.000 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set the transition predicate to Next
18:34:04.002 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set an invariant to Test1
18:34:04.010 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #2: ConfigurationPass [OK]
18:34:04.011 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #3: DesugarerPass
18:34:04.012 [main] INFO  a.f.a.t.p.p.DesugarerPassImpl -   > Desugaring...
18:34:04.040 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #3: DesugarerPass [OK]
18:34:04.041 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #4: InlinePass
18:34:04.043 [main] INFO  a.f.a.t.p.p.InlinePassImpl - Leaving only relevant operators: CInitPrimed, Init, InitPrimed, Next, Test1
18:34:04.101 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #4: InlinePass [OK]
18:34:04.101 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #5: PrimingPass
18:34:04.105 [main] INFO  a.f.a.t.a.p.PrimingPassImpl -   > Introducing InitPrimed for Init'
18:34:04.108 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #5: PrimingPass [OK]
18:34:04.109 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #6: VCGen
18:34:04.112 [main] INFO  a.f.a.t.b.p.VCGenPassImpl -   > Producing verification conditions from the invariant Test1
18:34:04.121 [main] INFO  a.f.a.t.b.VCGenerator -   > VCGen produced 1 verification condition(s)
18:34:04.123 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #6: VCGen [OK]
18:34:04.123 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #7: PreprocessingPass
18:34:04.124 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Before preprocessing: unique renaming
18:34:04.144 [main] INFO  a.f.a.t.p.p.PreproPassImpl -  > Applying standard transformations:
18:34:04.146 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > PrimePropagation
18:34:04.149 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Desugarer
18:34:04.152 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > UniqueRenamer
18:34:04.162 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Normalizer
18:34:04.167 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Keramelizer
18:34:04.177 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > After preprocessing: UniqueRenamer
18:34:04.190 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #7: PreprocessingPass [OK]
18:34:04.192 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #8: TransitionFinderPass
18:34:04.229 [main] INFO  a.f.a.t.a.p.TransitionPassImpl -   > Found 1 initializing transitions
18:34:04.243 [main] INFO  a.f.a.t.a.p.TransitionPassImpl -   > Found 2 transitions
18:34:04.245 [main] INFO  a.f.a.t.a.p.TransitionPassImpl -   > No constant initializer
18:34:04.247 [main] INFO  a.f.a.t.a.p.TransitionPassImpl -   > Applying unique renaming
18:34:04.253 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #8: TransitionFinderPass [OK]
18:34:04.254 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #9: OptimizationPass
18:34:04.264 [main] INFO  a.f.a.t.p.p.OptPassImpl -  > Applying optimizations:
18:34:04.266 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ConstSimplifier
18:34:04.272 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ExprOptimizer
18:34:04.276 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > SetMembershipSimplifier
18:34:04.278 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ConstSimplifier
18:34:04.281 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #9: OptimizationPass [OK]
18:34:04.282 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #10: AnalysisPass
18:34:04.288 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -  > Marking skolemizable existentials and sets to be expanded...
18:34:04.289 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Skolemization
18:34:04.291 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Expansion
18:34:04.293 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Remove unused let-in defs
18:34:04.298 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -  > Running analyzers...
18:34:04.304 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Introduced expression grades
18:34:04.305 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #10: AnalysisPass [OK]
18:34:04.306 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #11: PostTypeCheckerSnowcat
18:34:04.306 [main] INFO  a.f.a.t.b.p.PostTypeCheckerPassImpl -  > Running Snowcat .::.
18:34:04.469 [main] INFO  a.f.a.t.b.p.PostTypeCheckerPassImpl -  > Your types are purrfect!
18:34:04.469 [main] INFO  a.f.a.t.b.p.PostTypeCheckerPassImpl -  > All expressions are typed
18:34:04.470 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #11: PostTypeCheckerSnowcat [OK]
18:34:04.471 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #12: BoundedChecker
18:34:04.837 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #0, transition #0
18:34:04.838 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
18:34:04.931 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 0: Transition #0. Is it enabled?
18:34:04.934 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 0: Transition #0 is enabled
18:34:04.936 [main] INFO  a.f.a.t.b.SeqModelChecker - State 0: Checking 1 state invariants
18:34:04.938 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 0: Checking state invariant 0
18:34:04.951 [main] INFO  a.f.a.t.b.t.TransitionExecutorImpl - Step 0: picking a transition out of 1 transition(s)
18:34:04.968 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #0
18:34:04.969 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
18:34:05.015 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 1: Transition #0. Is it enabled?
18:34:05.017 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 1: Transition #0 is enabled
18:34:05.018 [main] INFO  a.f.a.t.b.SeqModelChecker - State 1: Checking 1 state invariants
18:34:05.019 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 1: Checking state invariant 0
18:34:05.269 [main] ERROR a.f.a.t.b.DumpCounterexamplesModelCheckerListener$ - Check an example state in: /mnt/c/Users/heidihoward/apalache/test/tla/_apalache-out/Invariants.tla/2022-04-19T18-34-02_3497060018105022808/counterexample1.tla, /mnt/c/Users/heidihoward/apalache/test/tla/_apalache-out/Invariants.tla/2022-04-19T18-34-02_3497060018105022808/MC1.out, /mnt/c/Users/heidihoward/apalache/test/tla/_apalache-out/Invariants.tla/2022-04-19T18-34-02_3497060018105022808/counterexample1.json, /mnt/c/Users/heidihoward/apalache/test/tla/_apalache-out/Invariants.tla/2022-04-19T18-34-02_3497060018105022808/counterexample1.itf.json
18:34:05.271 [main] ERROR a.f.a.t.b.SeqModelChecker - State 1: state invariant 0 violated.
18:34:05.273 [main] INFO  a.f.a.t.b.SeqModelChecker - Found 1 error(s)
18:34:05.279 [main] INFO  a.f.a.t.b.p.BoundedCheckerPassImpl - The outcome is: Error
18:34:05.281 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #12: BoundedChecker [FAIL]
18:34:05.284 [main] INFO  a.f.a.t.Tool$ - Checker has found an error
18:34:05.286 [main] INFO  a.f.a.t.Tool$ - It took me 0 days  0 hours  0 min  3 sec
18:34:05.287 [main] INFO  a.f.a.t.Tool$ - Total time: 3.230 sec

And 

18:35:09.257 [main] INFO  a.f.a.t.Tool$ - Checker options: check --length=1 --inv=Test2 Invariants.tla
18:35:09.262 [main] INFO  a.f.a.t.Tool$ - Tuning: 
18:35:09.268 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser
18:35:09.819 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser [OK]
18:35:09.820 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #1: TypeCheckerSnowcat
18:35:09.821 [main] INFO  a.f.a.t.t.p.EtcTypeCheckerPassImpl -  > Running Snowcat .::.
18:35:10.405 [main] INFO  a.f.a.t.t.p.EtcTypeCheckerPassImpl -  > Your types are purrfect!
18:35:10.406 [main] INFO  a.f.a.t.t.p.EtcTypeCheckerPassImpl -  > All expressions are typed
18:35:10.407 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #1: TypeCheckerSnowcat [OK]
18:35:10.414 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #2: ConfigurationPass
18:35:10.423 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Invariants.cfg: Loading TLC configuration
18:35:10.431 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > No TLC configuration found. Skipping.
18:35:10.435 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Command line option --init is not set. Using Init
18:35:10.436 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Command line option --next is not set. Using Next
18:35:10.437 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set the initialization predicate to Init
18:35:10.439 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set the transition predicate to Next
18:35:10.440 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set an invariant to Test2
18:35:10.447 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #2: ConfigurationPass [OK]
18:35:10.448 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #3: DesugarerPass
18:35:10.449 [main] INFO  a.f.a.t.p.p.DesugarerPassImpl -   > Desugaring...
18:35:10.474 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #3: DesugarerPass [OK]
18:35:10.475 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #4: InlinePass
18:35:10.477 [main] INFO  a.f.a.t.p.p.InlinePassImpl - Leaving only relevant operators: CInitPrimed, Init, InitPrimed, Next, Test2
18:35:10.545 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #4: InlinePass [OK]
18:35:10.546 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #5: PrimingPass
18:35:10.550 [main] INFO  a.f.a.t.a.p.PrimingPassImpl -   > Introducing InitPrimed for Init'
18:35:10.554 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #5: PrimingPass [OK]
18:35:10.555 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #6: VCGen
18:35:10.558 [main] INFO  a.f.a.t.b.p.VCGenPassImpl -   > Producing verification conditions from the invariant Test2
18:35:10.570 [main] INFO  a.f.a.t.b.VCGenerator -   > VCGen produced 2 verification condition(s)
18:35:10.572 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #6: VCGen [OK]
18:35:10.572 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #7: PreprocessingPass
18:35:10.573 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Before preprocessing: unique renaming
18:35:10.588 [main] INFO  a.f.a.t.p.p.PreproPassImpl -  > Applying standard transformations:
18:35:10.589 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > PrimePropagation
18:35:10.593 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Desugarer
18:35:10.599 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > UniqueRenamer
18:35:10.612 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Normalizer
18:35:10.618 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Keramelizer
18:35:10.631 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > After preprocessing: UniqueRenamer
18:35:10.647 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #7: PreprocessingPass [OK]
18:35:10.648 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #8: TransitionFinderPass
18:35:10.687 [main] INFO  a.f.a.t.a.p.TransitionPassImpl -   > Found 1 initializing transitions
18:35:10.707 [main] INFO  a.f.a.t.a.p.TransitionPassImpl -   > Found 2 transitions
18:35:10.709 [main] INFO  a.f.a.t.a.p.TransitionPassImpl -   > No constant initializer
18:35:10.711 [main] INFO  a.f.a.t.a.p.TransitionPassImpl -   > Applying unique renaming
18:35:10.722 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #8: TransitionFinderPass [OK]
18:35:10.723 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #9: OptimizationPass
18:35:10.734 [main] INFO  a.f.a.t.p.p.OptPassImpl -  > Applying optimizations:
18:35:10.737 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ConstSimplifier
18:35:10.744 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ExprOptimizer
18:35:10.748 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > SetMembershipSimplifier
18:35:10.754 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ConstSimplifier
18:35:10.759 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #9: OptimizationPass [OK]
18:35:10.760 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #10: AnalysisPass
18:35:10.766 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -  > Marking skolemizable existentials and sets to be expanded...
18:35:10.768 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Skolemization
18:35:10.770 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Expansion
18:35:10.773 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Remove unused let-in defs
18:35:10.777 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -  > Running analyzers...
18:35:10.784 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Introduced expression grades
18:35:10.785 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #10: AnalysisPass [OK]
18:35:10.786 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #11: PostTypeCheckerSnowcat
18:35:10.787 [main] INFO  a.f.a.t.b.p.PostTypeCheckerPassImpl -  > Running Snowcat .::.
18:35:11.012 [main] INFO  a.f.a.t.b.p.PostTypeCheckerPassImpl -  > Your types are purrfect!
18:35:11.013 [main] INFO  a.f.a.t.b.p.PostTypeCheckerPassImpl -  > All expressions are typed
18:35:11.014 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #11: PostTypeCheckerSnowcat [OK]
18:35:11.015 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #12: BoundedChecker
18:35:11.359 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #0, transition #0
18:35:11.360 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
18:35:11.448 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 0: Transition #0. Is it enabled?
18:35:11.452 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 0: Transition #0 is enabled
18:35:11.462 [main] INFO  a.f.a.t.b.t.TransitionExecutorImpl - Step 0: picking a transition out of 1 transition(s)
18:35:11.475 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #0
18:35:11.475 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
18:35:11.510 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 1: Transition #0. Is it enabled?
18:35:11.512 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 1: Transition #0 is enabled
18:35:11.512 [main] INFO  a.f.a.t.b.SeqModelChecker - State 0: Checking 2 action invariants
18:35:11.513 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 0: Checking action invariant 0
18:35:11.517 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 0: Checking action invariant 1
18:35:11.542 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #1
18:35:11.543 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
18:35:11.550 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 1: Transition #1. Is it enabled?
18:35:11.551 [main] INFO  a.f.a.t.b.SeqModelChecker - Step 1: Transition #1 is disabled
18:35:11.554 [main] INFO  a.f.a.t.b.t.TransitionExecutorImpl - Step 1: picking a transition out of 1 transition(s)
18:35:11.562 [main] INFO  a.f.a.t.b.p.BoundedCheckerPassImpl - The outcome is: NoError
18:35:11.563 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #12: BoundedChecker [OK]
18:35:11.564 [main] INFO  a.f.a.t.Tool$ - Checker reports no error up to computation length 1
18:35:11.565 [main] INFO  a.f.a.t.Tool$ - It took me 0 days  0 hours  0 min  2 sec
18:35:11.566 [main] INFO  a.f.a.t.Tool$ - Total time: 2.950 sec

System information

Additional context

I'm not sure if this is a bug or by design but if the latter users like me might benefit for some more documentation.

konnov commented 2 years ago

We will have a closer look. State and action properties are treated slightly differently. There may be a one-off issue somewhere.

heidihoward commented 2 years ago

Cheers! The issue seems to be that state invariants are checked upto the length (inclusive) whereas the unprimed variables in action invariants are checked up to length (exclusive)