Unable to disable deadlock detection

[heidihoward]

Description

I am unable to disable deadlock detection using --no-deadlock

Input specification

---- MODULE RaftLeader ----

EXTENDS Integers

Server == {"s1", "s2", "s3"}
Quorum == {{"s1","s2"},{"s2","s3"},{"s1","s3"}}
Term == 0..2

Message ==  
    [type : {"RequestVote"}, term : Term, from: Server]
    \cup [type : {"Vote"}, from : Server, to: Server, term : Term]
    \cup [type : {"AppendEntries"}, term : Term, from: Server]

States == {"Follower","Candidate","Leader"}

VARIABLE 
    \* @type: Str -> Int;
    currentTerm,
     \* @type: Set([type: Str, term: Int, from: Str, to:Str]);
    messages,
    \* @type: Str -> Str;
    state

vars == <<currentTerm,state,messages>>

Init ==
    /\ currentTerm = [s \in Server |-> 0]
    /\ state =  [s \in Server |-> "Follower"]
    /\ messages = {}

BecomeCandidate(s) ==
    /\ currentTerm[s]<2
    /\ currentTerm' = [currentTerm EXCEPT ![s] = currentTerm[s] + 1]
    /\ state' = [state EXCEPT ![s] = "Candidate"]
    /\ messages' = messages \union {[type |-> "RequestVote", term |-> currentTerm[s]+1, from |-> s]}

Vote(s) ==
    /\ \E m \in messages:
        /\ m.type = "RequestVote"
        /\ m.term > currentTerm[s]
        /\ currentTerm' = [currentTerm EXCEPT ![s] = m.term]
        /\ messages' = messages \union {[type |-> "Vote", 
                                            term |-> m.term, from |-> s, to |-> m.from]}
    /\ UNCHANGED <<state>>

BecomeLeader(s) ==
    /\ \E Q \in Quorum:
        \A s1 \in Server: 
            \E m \in messages: 
                /\ m.type = "Vote"
                /\ m.term = currentTerm[s]
                /\ m.from = s1
                /\ m.to = s
    /\ state' = [state EXCEPT ![s] = "Leader"]
    /\ messages' = messages \union {[type |-> "AppendEntries", 
                                        term |-> currentTerm[s], from |-> s]}
    /\ UNCHANGED <<currentTerm>>

Noop ==
    /\ UNCHANGED <<currentTerm,messages,state>>    

Next ==
    \/ \E s \in Server:
        \/ BecomeCandidate(s)
        \/ Vote(s)
        \/ BecomeLeader(s)
    \* \/ Noop

Safety ==
    \A t \in Term: \A m1,m2 \in messages: 
        /\ m1.type = "AppendEntries" 
        /\ m2.type = "AppendEntries" 
        /\ m1.term = m2.term 
        => m1.from = m2.from 

TypeOK ==
    /\ currentTerm \in [Server -> Term]
    /\ state \in [Server -> States]
    /\ messages \in SUBSET Message

Leader(s,t) ==
     /\ \E Q \in Quorum:
        \A s1 \in Server: 
            \E m \in messages: 
                /\ m.type = "Vote"
                /\ m.term = t
                /\ m.from = s1
                /\ m.to = s

Inv == 
    /\ TypeOK
    /\ \A s \in Server, m \in messages: 
        m.from = s => currentTerm[s] \geq m.term
    /\ \A m1,m2 \in messages: \A s \in Server: 
       /\ m1.type = "Vote" 
       /\ m2.type = "Vote" 
       /\ m1.from = s 
       /\ m2.from = s 
       /\ m1.term = m2.term 
       => m1.to = m2.to
    /\ \A t \in Term: \A s1,s2 \in Server:
       /\ Leader(s1,t) 
       /\ Leader(s2,t) 
       => s1=s2

====

The command line parameters used to run the tool

apalache-mc check --no-deadlock --debug --inv=Safety --length=8 RaftLeader.tla

Expected behavior

NoError

Log files

13:25:46.431 [main] INFO  a.f.a.t.Tool$ - Checker options: check --no-deadlock --debug --inv=Safety --length=8 RaftLeader.tla
13:25:46.437 [main] INFO  a.f.a.t.Tool$ - Tuning: 
13:25:46.443 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser
13:25:47.041 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser [OK]
13:25:47.042 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #1: TypeCheckerSnowcat
13:25:47.044 [main] INFO  a.f.a.t.t.p.EtcTypeCheckerPassImpl -  > Running Snowcat .::.
13:25:48.123 [main] INFO  a.f.a.t.t.p.EtcTypeCheckerPassImpl -  > Your types are purrfect!
13:25:48.124 [main] INFO  a.f.a.t.t.p.EtcTypeCheckerPassImpl -  > All expressions are typed
13:25:48.125 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #1: TypeCheckerSnowcat [OK]
13:25:48.128 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #2: ConfigurationPass
13:25:48.137 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > RaftLeader.cfg: Loading TLC configuration
13:25:48.145 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > No TLC configuration found. Skipping.
13:25:48.149 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Command line option --init is not set. Using Init
13:25:48.150 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Command line option --next is not set. Using Next
13:25:48.151 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set the initialization predicate to Init
13:25:48.152 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set the transition predicate to Next
13:25:48.153 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set an invariant to Safety
13:25:48.165 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #2: ConfigurationPass [OK]
13:25:48.166 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #3: DesugarerPass
13:25:48.167 [main] INFO  a.f.a.t.p.p.DesugarerPassImpl -   > Desugaring...
13:25:48.196 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #3: DesugarerPass [OK]
13:25:48.197 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #4: InlinePass
13:25:48.200 [main] INFO  a.f.a.t.p.p.InlinePassImpl - Leaving only relevant operators: CInitPrimed, Init, InitPrimed, Next, Safety
13:25:48.290 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #4: InlinePass [OK]
13:25:48.291 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #5: PrimingPass
13:25:48.296 [main] INFO  a.f.a.t.a.p.PrimingPassImpl -   > Introducing InitPrimed for Init'
13:25:48.300 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #5: PrimingPass [OK]
13:25:48.302 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #6: VCGen
13:25:48.303 [main] INFO  a.f.a.t.b.p.VCGenPassImpl -   > Producing verification conditions from the invariant Safety
13:25:48.312 [main] INFO  a.f.a.t.b.VCGenerator -   > VCGen produced 1 verification condition(s)
13:25:48.315 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #6: VCGen [OK]
13:25:48.316 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #7: PreprocessingPass
13:25:48.317 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Before preprocessing: unique renaming
13:25:48.331 [main] INFO  a.f.a.t.p.p.PreproPassImpl -  > Applying standard transformations:
13:25:48.334 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > PrimePropagation
13:25:48.337 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Desugarer
13:25:48.343 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > UniqueRenamer
13:25:48.359 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Normalizer
13:25:48.371 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Keramelizer
13:25:48.383 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > After preprocessing: UniqueRenamer
13:25:48.420 [main] ERROR a.f.a.t.l.s.SourceLocator - No source location for expr@25732: ∀t$1 ∈ (0 .. 2): (∀m1$1 ∈ messages: (∀m2$1 ∈ messages: (((m1$1["type"...
13:25:48.425 [main] ERROR a.f.a.t.l.s.SourceLocator - No source location for expr@25734: ¬(∀t$1 ∈ (0 .. 2): (∀m1$1 ∈ messages: (∀m2$1 ∈ messages: (((m1$1["typ...
13:25:48.428 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #7: PreprocessingPass [OK]
13:25:48.429 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #8: TransitionFinderPass
13:25:48.457 [main] INFO  a.f.a.t.a.p.TransitionPassImpl -   > Found 1 initializing transitions
13:25:48.477 [main] INFO  a.f.a.t.a.p.TransitionPassImpl -   > Found 3 transitions
13:25:48.479 [main] INFO  a.f.a.t.a.p.TransitionPassImpl -   > No constant initializer
13:25:48.481 [main] INFO  a.f.a.t.a.p.TransitionPassImpl -   > Applying unique renaming
13:25:48.491 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #8: TransitionFinderPass [OK]
13:25:48.493 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #9: OptimizationPass
13:25:48.505 [main] INFO  a.f.a.t.p.p.OptPassImpl -  > Applying optimizations:
13:25:48.508 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ConstSimplifier
13:25:48.515 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ExprOptimizer
13:25:48.526 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > SetMembershipSimplifier
13:25:48.529 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ConstSimplifier
13:25:48.533 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #9: OptimizationPass [OK]
13:25:48.534 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #10: AnalysisPass
13:25:48.542 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -  > Marking skolemizable existentials and sets to be expanded...
13:25:48.544 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Skolemization
13:25:48.546 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Expansion
13:25:48.549 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Remove unused let-in defs
13:25:48.557 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -  > Running analyzers...
13:25:48.567 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Introduced expression grades
13:25:48.568 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #10: AnalysisPass [OK]
13:25:48.568 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #11: PostTypeCheckerSnowcat
13:25:48.569 [main] INFO  a.f.a.t.b.p.PostTypeCheckerPassImpl -  > Running Snowcat .::.
13:25:49.122 [main] INFO  a.f.a.t.b.p.PostTypeCheckerPassImpl -  > Your types are purrfect!
13:25:49.123 [main] INFO  a.f.a.t.b.p.PostTypeCheckerPassImpl -  > All expressions are typed
13:25:49.124 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #11: PostTypeCheckerSnowcat [OK]
13:25:49.125 [main] INFO  a.f.a.i.p.PassChainExecutor - PASS #12: BoundedChecker
13:25:49.543 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #0, transition #0
13:25:49.545 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
13:25:49.666 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 0: Transition #0. Is it enabled?
13:25:49.669 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 0: Transition #0 is enabled
13:25:49.670 [main] INFO  a.f.a.t.b.SeqModelChecker - State 0: Checking 1 state invariants
13:25:49.673 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 0: Checking state invariant 0
13:25:49.703 [main] INFO  a.f.a.t.b.t.TransitionExecutorImpl - Step 0: picking a transition out of 1 transition(s)
13:25:49.721 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #0
13:25:49.722 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
13:25:49.919 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 1: Transition #0. Is it enabled?
13:25:49.921 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 1: Transition #0 is enabled
13:25:49.921 [main] INFO  a.f.a.t.b.SeqModelChecker - State 1: Checking 1 state invariants
13:25:49.922 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 1: Checking state invariant 0
13:25:49.957 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #1
13:25:49.957 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
13:25:49.975 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 1: Transition #1. Is it enabled?
13:25:49.976 [main] INFO  a.f.a.t.b.SeqModelChecker - Step 1: Transition #1 is disabled
13:25:49.980 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #1, transition #2
13:25:49.980 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
13:25:50.062 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 1: Transition #2. Is it enabled?
13:25:50.063 [main] INFO  a.f.a.t.b.SeqModelChecker - Step 1: Transition #2 is disabled
13:25:50.067 [main] INFO  a.f.a.t.b.t.TransitionExecutorImpl - Step 1: picking a transition out of 1 transition(s)
13:25:50.070 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #2, transition #0
13:25:50.070 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
13:25:50.151 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 2: Transition #0. Is it enabled?
13:25:50.152 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 2: Transition #0 is enabled
13:25:50.153 [main] INFO  a.f.a.t.b.SeqModelChecker - State 2: Checking 1 state invariants
13:25:50.154 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 2: Checking state invariant 0
13:25:50.194 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #2, transition #1
13:25:50.195 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
13:25:50.241 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 2: Transition #1. Is it enabled?
13:25:50.242 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 2: Transition #1 is enabled
13:25:50.243 [main] INFO  a.f.a.t.b.SeqModelChecker - State 2: Checking 1 state invariants
13:25:50.243 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 2: Checking state invariant 0
13:25:50.310 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #2, transition #2
13:25:50.310 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
13:25:50.409 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 2: Transition #2. Is it enabled?
13:25:50.410 [main] INFO  a.f.a.t.b.SeqModelChecker - Step 2: Transition #2 is disabled
13:25:50.414 [main] INFO  a.f.a.t.b.t.TransitionExecutorImpl - Step 2: picking a transition out of 2 transition(s)
13:25:50.470 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #3, transition #0
13:25:50.471 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
13:25:50.536 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 3: Transition #0. Is it enabled?
13:25:50.539 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 3: Transition #0 is enabled
13:25:50.539 [main] INFO  a.f.a.t.b.SeqModelChecker - State 3: Checking 1 state invariants
13:25:50.540 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 3: Checking state invariant 0
13:25:50.588 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #3, transition #1
13:25:50.588 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
13:25:50.632 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 3: Transition #1. Is it enabled?
13:25:50.634 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 3: Transition #1 is enabled
13:25:50.635 [main] INFO  a.f.a.t.b.SeqModelChecker - State 3: Checking 1 state invariants
13:25:50.635 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 3: Checking state invariant 0
13:25:50.693 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #3, transition #2
13:25:50.693 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
13:25:50.792 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 3: Transition #2. Is it enabled?
13:25:50.793 [main] INFO  a.f.a.t.b.SeqModelChecker - Step 3: Transition #2 is disabled
13:25:50.796 [main] INFO  a.f.a.t.b.t.TransitionExecutorImpl - Step 3: picking a transition out of 2 transition(s)
13:25:50.830 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #4, transition #0
13:25:50.831 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
13:25:50.895 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 4: Transition #0. Is it enabled?
13:25:50.905 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 4: Transition #0 is enabled
13:25:50.906 [main] INFO  a.f.a.t.b.SeqModelChecker - State 4: Checking 1 state invariants
13:25:50.906 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 4: Checking state invariant 0
13:25:50.957 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #4, transition #1
13:25:50.958 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
13:25:51.000 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 4: Transition #1. Is it enabled?
13:25:51.003 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 4: Transition #1 is enabled
13:25:51.004 [main] INFO  a.f.a.t.b.SeqModelChecker - State 4: Checking 1 state invariants
13:25:51.004 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 4: Checking state invariant 0
13:25:51.057 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #4, transition #2
13:25:51.058 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
13:25:51.154 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 4: Transition #2. Is it enabled?
13:25:51.157 [main] INFO  a.f.a.t.b.SeqModelChecker - Step 4: Transition #2 is disabled
13:25:51.160 [main] INFO  a.f.a.t.b.t.TransitionExecutorImpl - Step 4: picking a transition out of 2 transition(s)
13:25:51.193 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #5, transition #0
13:25:51.193 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
13:25:51.248 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 5: Transition #0. Is it enabled?
13:25:51.251 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 5: Transition #0 is enabled
13:25:51.252 [main] INFO  a.f.a.t.b.SeqModelChecker - State 5: Checking 1 state invariants
13:25:51.253 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 5: Checking state invariant 0
13:25:51.298 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #5, transition #1
13:25:51.298 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
13:25:51.332 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 5: Transition #1. Is it enabled?
13:25:51.335 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 5: Transition #1 is enabled
13:25:51.336 [main] INFO  a.f.a.t.b.SeqModelChecker - State 5: Checking 1 state invariants
13:25:51.336 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 5: Checking state invariant 0
13:25:51.383 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #5, transition #2
13:25:51.383 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
13:25:51.483 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 5: Transition #2. Is it enabled?
13:25:51.500 [main] INFO  a.f.a.t.b.SeqModelChecker - Step 5: Transition #2 is disabled
13:25:51.503 [main] INFO  a.f.a.t.b.t.TransitionExecutorImpl - Step 5: picking a transition out of 2 transition(s)
13:25:51.542 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #6, transition #0
13:25:51.542 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
13:25:51.588 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 6: Transition #0. Is it enabled?
13:25:51.609 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 6: Transition #0 is enabled
13:25:51.609 [main] INFO  a.f.a.t.b.SeqModelChecker - State 6: Checking 1 state invariants
13:25:51.610 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 6: Checking state invariant 0
13:25:51.657 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #6, transition #1
13:25:51.658 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
13:25:51.699 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 6: Transition #1. Is it enabled?
13:25:51.746 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 6: Transition #1 is enabled
13:25:51.747 [main] INFO  a.f.a.t.b.SeqModelChecker - State 6: Checking 1 state invariants
13:25:51.747 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 6: Checking state invariant 0
13:25:51.798 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #6, transition #2
13:25:51.798 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
13:25:51.943 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 6: Transition #2. Is it enabled?
13:25:52.070 [main] INFO  a.f.a.t.b.SeqModelChecker - Step 6: Transition #2 is disabled
13:25:52.075 [main] INFO  a.f.a.t.b.t.TransitionExecutorImpl - Step 6: picking a transition out of 2 transition(s)
13:25:52.116 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #7, transition #0
13:25:52.116 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
13:25:52.172 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 7: Transition #0. Is it enabled?
13:25:57.689 [main] INFO  a.f.a.t.b.SeqModelChecker - Step 7: Transition #0 is disabled
13:25:57.696 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #7, transition #1
13:25:57.697 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
13:25:57.735 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 7: Transition #1. Is it enabled?
13:26:04.066 [main] INFO  a.f.a.t.b.SeqModelChecker - Step 7: Transition #1 is disabled
13:26:04.073 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #7, transition #2
13:26:04.073 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
13:26:04.160 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 7: Transition #2. Is it enabled?
13:26:04.694 [main] INFO  a.f.a.t.b.SeqModelChecker - Step 7: Transition #2 is disabled
13:26:05.157 [main] ERROR a.f.a.t.b.DumpCounterexamplesModelCheckerListener$ - Check an example state in: /mnt/c/Users/heidihoward/apalache-tests/performance/raftleader/_apalache-out/RaftLeader.tla/2022-04-19T13-25-45_14406619126286059932/counterexample0.tla, /mnt/c/Users/heidihoward/apalache-tests/performance/raftleader/_apalache-out/RaftLeader.tla/2022-04-19T13-25-45_14406619126286059932/MC0.out, /mnt/c/Users/heidihoward/apalache-tests/performance/raftleader/_apalache-out/RaftLeader.tla/2022-04-19T13-25-45_14406619126286059932/counterexample0.json, /mnt/c/Users/heidihoward/apalache-tests/performance/raftleader/_apalache-out/RaftLeader.tla/2022-04-19T13-25-45_14406619126286059932/counterexample0.itf.json
13:26:05.158 [main] ERROR a.f.a.t.b.SeqModelChecker - Found a deadlock.
13:26:05.187 [main] INFO  a.f.a.t.b.p.BoundedCheckerPassImpl - The outcome is: Deadlock
13:26:05.188 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #12: BoundedChecker [FAIL]
13:26:05.188 [main] INFO  a.f.a.t.Tool$ - Checker has found an error
13:26:05.190 [main] INFO  a.f.a.t.Tool$ - It took me 0 days  0 hours  0 min 19 sec
13:26:05.192 [main] INFO  a.f.a.t.Tool$ - Total time: 19.372 sec

System information

• Apalache version [apalache-mc version]: 0.24.0
• OS [e.g. Ubuntu Linux or Mac OS, and the current version]: Ubuntu 20.04 LTS (on Windows 11 using WSL)
• JDK version [e.g. OpenJDK 0.8.0]: openjdk 11.0.14 2022-01-18

Additional context

[konnov]

I guess, this message is confusing in the presence of --no-deadlock:

13:25:52.116 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #7, transition #0
13:25:52.116 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
13:25:52.172 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 7: Transition #0. Is it enabled?
13:25:57.689 [main] INFO  a.f.a.t.b.SeqModelChecker - Step 7: Transition #0 is disabled
13:25:57.696 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #7, transition #1
13:25:57.697 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
13:25:57.735 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 7: Transition #1. Is it enabled?
13:26:04.066 [main] INFO  a.f.a.t.b.SeqModelChecker - Step 7: Transition #1 is disabled
13:26:04.073 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #7, transition #2
13:26:04.073 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT...
13:26:04.160 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 7: Transition #2. Is it enabled?
13:26:04.694 [main] INFO  a.f.a.t.b.SeqModelChecker - Step 7: Transition #2 is disabled
...
13:26:05.158 [main] ERROR a.f.a.t.b.SeqModelChecker - Found a deadlock.
13:26:05.187 [main] INFO  a.f.a.t.b.p.BoundedCheckerPassImpl - The outcome is: Deadlock

The reason for the message is that a symbolic execution cannot be extended at Step 7. As far as I understand, this is due to Term == 0..2. When I define Term to be 0..3, the execution can be extended.

Would you like to see no error, when you pass --no-deadlock, though the model checker cannot produce a single execution of length 8? I can also see how such a behavior of the model checker would make sense.

[heidihoward]

Yes, that's correct.

I appreciate that deadlock can be avoided by adding more terms or adding a no-op action (which I did the example but commented out to demonstrate the problem).

I expected that the --no-deadlock flag would completely disable deadlock detection so that Apalache would report NoError. It would be useful to me to be able to limit the state space in the spec instead of using --length so I can easily compare and support both TLC & Apalache.

[konnov]

I see your point. We will fix that.