Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Uncaught TBuilderTypeException: Operator SET_ENUM cannot be applied to arguments #2690

Closed
3 tasks
will62794 opened this issue Aug 8, 2023 · 7 comments · Fixed by #2697
Closed
3 tasks

Uncaught TBuilderTypeException: Operator SET_ENUM cannot be applied to arguments #2690

will62794 opened this issue Aug 8, 2023 · 7 comments · Fixed by #2697
Assignees
@thpani
Labels
bug

Comments

@will62794
Copy link

will62794 commented Aug 8, 2023 •
edited
Loading

Impact

Uncaught TBuilderTypeException exception terminates Apalache model checking unexpectedly.

Input specification

---- MODULE AbstractStaticRaft ----

EXTENDS Naturals, Integers, FiniteSets, Sequences, TLC, Apalache

CONSTANTS 
    \* @type: Set(SERVER);
    Server

CONSTANTS 
    \* @type: Str;
    Secondary, 
    \* @type: Str;
    Primary, 
    \* @type: Str;
    Nil

CONSTANT
    \* @type: Int; 
    InitTerm

VARIABLE 
    \* @type: SERVER -> Int; 
    currentTerm

VARIABLE 
    \* @type: SERVER -> Str;
    state

VARIABLE 
    \* @type: SERVER -> Seq(Int);
    log

VARIABLE
   \* @type: Set( <<Int, Int, Int>> );
    committed

vars == <<currentTerm, state, log, committed>>

\* Is a sequence empty.
Empty(s) == Len(s) = 0

\* Is log entry e = <<index, term>> in the log of node 'i'.
\* @type: (<<Int,Int>>,SERVER) => Bool;
InLog(e, i) == \E x \in DOMAIN log[i] : x = e[1] /\ log[i][x] = e[2]

\* The term of the last entry in a log, or 0 if the log is empty.
LastTerm(xlog) == IF Len(xlog) = 0 THEN 0 ELSE xlog[Len(xlog)]

\* @type: Seq(Int) => <<Int, Int>>;
LastEntry(xlog) == <<Len(xlog),xlog[Len(xlog)]>>

\* @type: (Seq(Int), Int) => Int;
GetTerm(xlog, index) == IF index = 0 THEN 0 ELSE xlog[index]
LogTerm(i, index) == GetTerm(log[i], index)

\* The set of all quorums in a given set.
Quorums(S) == {i \in SUBSET(S) : Cardinality(i) * 2 > Cardinality(S)}

\* Is it possible for log 'i' to roll back against log 'j'. 
\* If this is true, it implies that log 'i' should remove entries from the end of its log.
CanRollback(i, j) ==
    /\ Len(log[i]) > 0
    /\ \* The log with later term is more up-to-date.
       LastTerm(log[i]) < LastTerm(log[j])
    /\ \/ Len(log[i]) > Len(log[j])
       \* There seems no short-cut of OR clauses, so we specify the negative case.
       \/ /\ Len(log[i]) <= Len(log[j])
          /\ LastTerm(log[i]) /= LogTerm(j, Len(log[i]))

\* Can node 'i' currently cast a vote for node 'j' in term 'term'.
CanVoteForOplog(i, j, term) ==
    LET logOk ==
        \/ LastTerm(log[j]) > LastTerm(log[i])
        \/ /\ LastTerm(log[j]) = LastTerm(log[i])
           /\ Len(log[j]) >= Len(log[i]) IN
    /\ currentTerm[i] < term
    /\ logOk

\* Is a log entry 'e'=<<i, t>> immediately committed in term 't' with a quorum 'Q'.
\* @type: (<<Int, Int>>, Set(SERVER)) => Bool;
ImmediatelyCommitted(e, Q) == 
    LET eind == e[1] 
        eterm == e[2] IN
    \A s \in Q :
        /\ Len(log[s]) >= eind
        /\ InLog(e, s) \* they have the entry.
        /\ currentTerm[s] = eterm  \* they are in the same term as the log entry. 

\* Helper operator for actions that propagate the term between two nodes.
UpdateTermsExpr(i, j) ==
    /\ currentTerm[i] > currentTerm[j]
    /\ currentTerm' = [currentTerm EXCEPT ![j] = currentTerm[i]]
    /\ state' = [state EXCEPT ![j] = Secondary] 

--------------------------------------------------------------------------------

\*
\* Next state actions.
\*

\* Node 'i', a primary, handles a new client request and places the entry 
\* in its log.    
ClientRequest(i) ==
    /\ state[i] = Primary
    /\ log' = [log EXCEPT ![i] = Append(log[i], currentTerm[i])]
    /\ UNCHANGED <<currentTerm, state, committed>>

\* Node 'i' gets a new log entry from node 'j'.
GetEntries(i, j) ==
    /\ state[i] = Secondary
    \* Node j must have more entries than node i.
    /\ Len(log[j]) > Len(log[i])
       \* Ensure that the entry at the last index of node i's log must match the entry at
       \* the same index in node j's log. If the log of node i is empty, then the check
       \* trivially passes. This is the essential 'log consistency check'.
    /\ LET logOk == IF Empty(log[i])
                        THEN TRUE
                        ELSE log[j][Len(log[i])] = log[i][Len(log[i])] IN
       /\ logOk \* log consistency check
       \* If the log of node i is empty, then take the first entry from node j's log.
       \* Otherwise take the entry following the last index of node i.
       /\ LET newEntryIndex == IF Empty(log[i]) THEN 1 ELSE Len(log[i]) + 1
              newEntry      == log[j][newEntryIndex]
              newLog        == Append(log[i], newEntry) IN
              /\ log' = [log EXCEPT ![i] = newLog]
    /\ UNCHANGED <<committed, currentTerm, state>>

\*  Node 'i' rolls back against the log of node 'j'.  
RollbackEntries(i, j) ==
    /\ state[i] = Secondary
    /\ CanRollback(i, j)
    \* Roll back one log entry.
    /\ log' = [log EXCEPT ![i] = SubSeq(log[i], 1, Len(log[i])-1)]
    /\ UNCHANGED <<committed, currentTerm, state>>

\* Node 'i' gets elected as a primary.
BecomeLeader(i, voteQuorum) == 
    \* Primaries make decisions based on their current configuration.
    LET newTerm == currentTerm[i] + 1 IN
    /\ i \in voteQuorum \* The new leader should vote for itself.
    /\ \A v \in voteQuorum : CanVoteForOplog(v, i, newTerm)
    \* Update the terms of each voter.
    /\ currentTerm' = [s \in Server |-> IF s \in voteQuorum THEN newTerm ELSE currentTerm[s]]
    /\ state' = [s \in Server |->
                    IF s = i THEN Primary
                    ELSE IF s \in voteQuorum THEN Secondary \* All voters should revert to secondary state.
                    ELSE state[s]]
    /\ UNCHANGED <<log, committed>>   
            
\* Primary 'i' commits its latest log entry.
CommitEntry(i, commitQuorum) ==
    LET ind == Len(log[i]) IN
    \* Must have some entries to commit.
    /\ ind > 0
    \* This node is leader.
    /\ state[i] = Primary
    \* The entry was written by this leader.
    /\ log[i][ind] = currentTerm[i]
    \* all nodes have this log entry and are in the term of the leader.
    /\ ImmediatelyCommitted(<<ind,currentTerm[i]>>, commitQuorum)
    \* Don't mark an entry as committed more than once.
    \* /\ ~\E c \in committed : c.entry = <<ind, currentTerm[i]>>
    \* /\ ~\E c \in committed : <<c[1],c[2]>> = <<ind, currentTerm[i]>>
    /\ committed' = committed \cup {}
            \* {[ entry  |-> <<ind, currentTerm[i]>>,
            \*    term  |-> currentTerm[i]]}
    /\ UNCHANGED <<currentTerm, state, log>>

\* Action that exchanges terms between two nodes and step down the primary if
\* needed.
UpdateTerms(i, j) == 
    /\ UpdateTermsExpr(i, j)
    /\ UNCHANGED <<log, committed>>

Init == 
    /\ currentTerm = [i \in Server |-> InitTerm]
    /\ state       = [i \in Server |-> Secondary]
    /\ log = [i \in Server |-> <<>>]
    /\ committed = {}

ClientRequestAction == \E s \in Server : ClientRequest(s)
GetEntriesAction == \E s, t \in Server : GetEntries(s, t)
RollbackEntriesAction == \E s, t \in Server : RollbackEntries(s, t)
BecomeLeaderAction == \E s \in Server : \E Q \in Quorums(Server) : BecomeLeader(s, Q)
UpdateTermsActions == \E s,t \in Server : UpdateTerms(s, t)

Next == 
    \/ ClientRequestAction
    \/ GetEntriesAction
    \/ RollbackEntriesAction
    \/ BecomeLeaderAction
    \/ UpdateTermsActions

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

NextUnchanged == UNCHANGED vars

--------------------------------------------------------------------------------

OnePrimaryPerTerm == 
    \A s,t \in Server :
        (/\ state[s] = Primary 
         /\ state[t] = Primary
         /\ currentTerm[s] = currentTerm[t]) => (s = t)

LeaderAppendOnly == 
    [][\A s \in Server : state[s] = Primary => Len(log'[s]) >= Len(log[s])]_vars

\* <<index, term>> pairs uniquely identify log prefixes.
LogMatching == 
    \A s,t \in Server : 
    \A i \in DOMAIN log[s] :
        (\E j \in DOMAIN log[t] : i = j /\ log[s][i] = log[t][j]) => 
        (SubSeq(log[s],1,i) = SubSeq(log[t],1,i)) \* prefixes must be the same.

\* When a node gets elected as primary it contains all entries committed in previous terms.
LeaderCompleteness == 
    \A s \in Server : (state[s] = Primary) => 
        \A c \in committed : (c[3] < currentTerm[s] => InLog(<<c[1],c[2]>>, s))

--------------------------------------------------------------------------------

CONSTANTS 
    \* @type: Int;
    MaxTerm, 
    \* @type: Int;
    MaxLogLen

\* State Constraint. Used for model checking only.
StateConstraint == \A s \in Server :
                    /\ currentTerm[s] <= MaxTerm
                    /\ Len(log[s]) <= MaxLogLen

Symmetry == Permutations(Server)

Terms == InitTerm..MaxTerm
LogIndices == 1..MaxLogLen

\* Statement of type correctness.
TypeOK ==
    /\ currentTerm \in [Server -> Nat]
    /\ state \in [Server -> {Secondary, Primary}]
    /\ log = Gen(3)
    /\ \A s \in Server : \A i \in DOMAIN log[s] : log[s][i] \in Terms
    /\ committed \in SUBSET (LogIndices \X Terms \X Terms)

\* Used for Apalache, if we convert over to use that.
CInit == 
    /\ Primary = "P"
    /\ Secondary = "S"
    /\ Nil = "Nil"
    /\ Server = {"1_OF_SERVER", "2_OF_SERVER", "3_OF_SERVER"}
    /\ MaxLogLen = 3
    /\ MaxTerm = 3
    /\ InitTerm = 0

\* 
\* Helper lemmas.
\* 

\* If a primary has been elected at term T, then there must exist a quorum at term >= T.
H_QuorumsSafeAtTerms == 
    \A s \in Server : (state[s] = Primary) =>
        (\A Q \in Quorums(Server) : \E n \in Q : currentTerm[n] >= currentTerm[s])

H_TermsOfEntriesGrowMonotonically ==
    \A s \in Server : \A i,j \in DOMAIN log[s] : (i <= j) => (log[s][i] <= log[s][j])

H_PrimaryTermAtLeastAsLargeAsLogTerms == 
    \A s \in Server : (state[s] = Primary) => 
        \A i \in DOMAIN log[s] : currentTerm[s] >= log[s][i]



\* Existence of an entry in term T implies a past election in T, so 
\* there must be some quorum at this term or greater.
H_LogEntryInTermImpliesSafeAtTerm == 
    \A s \in Server : 
    \A i \in DOMAIN log[s] :
        \E Q \in Quorums(Server) : \A n \in Q : currentTerm[n] >= log[s][i]


Safety == LeaderCompleteness
InvStrengthened ==
    /\ Safety

InvStrengthened_Constraint == StateConstraint => InvStrengthened 
IndCand ==
    /\ TypeOK
    /\ InvStrengthened
    
=============================================================================

The command line parameters used to run the tool

--out-dir=gen_tla/apalache_ctigen --max-error=250 --view=vars --run-dir=gen_tla/apalache_ctigen --cinit=CInit --init=IndCand --next=Next --inv=InvStrengthened --length=1

Expected behavior

Expected Apalache to complete model checking successfully. Note that, similar to #2683, removing the --max-error=250 --view=vars flags appears to avoid the exception.

Log files

2023-08-07T12:27:48,084 [main] INFO  a.f.a.t.Tool\$ - # APALACHE version: 0.41.3 | build: 6ffe450
2023-08-07T12:27:48,124 [main] INFO  a.f.a.t.t.o.CheckCmd - Tuning: search.outputTraces=false
2023-08-07T12:27:48,423 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #0: SanyParser
2023-08-07T12:27:49,001 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #0: SanyParser [OK]
2023-08-07T12:27:49,002 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #1: TypeCheckerSnowcat
2023-08-07T12:27:49,002 [main] INFO  a.f.a.t.p.t.EtcTypeCheckerPassImpl -  > Running Snowcat .::.
2023-08-07T12:27:49,807 [main] INFO  a.f.a.t.p.t.EtcTypeCheckerPassImpl -  > Your types are purrfect!
2023-08-07T12:27:49,807 [main] INFO  a.f.a.t.p.t.EtcTypeCheckerPassImpl -  > All expressions are typed
2023-08-07T12:27:49,808 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #1: TypeCheckerSnowcat [OK]
2023-08-07T12:27:49,809 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #2: ConfigurationPass
2023-08-07T12:27:49,816 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set the initialization predicate to IndCand
2023-08-07T12:27:49,817 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set the transition predicate to Next
2023-08-07T12:27:49,818 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set the constant initialization predicate to CInit
2023-08-07T12:27:49,819 [main] INFO  a.f.a.t.p.p.ConfigurationPassImpl -   > Set an invariant to InvStrengthened
2023-08-07T12:27:49,827 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #2: ConfigurationPass [OK]
2023-08-07T12:27:49,827 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #3: DesugarerPass
2023-08-07T12:27:49,828 [main] INFO  a.f.a.t.p.p.DesugarerPassImpl -   > Desugaring...
2023-08-07T12:27:50,039 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #3: DesugarerPass [OK]
2023-08-07T12:27:50,039 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #4: InlinePass
2023-08-07T12:27:50,040 [main] INFO  a.f.a.t.p.p.InlinePassImpl - Leaving only relevant operators: CInit, CInitPrimed, IndCand, IndCandPrimed, InvStrengthened, Next, vars
2023-08-07T12:27:50,107 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #4: InlinePass [OK]
2023-08-07T12:27:50,108 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #5: TemporalPass
2023-08-07T12:27:50,108 [main] INFO  a.f.a.t.p.p.TemporalPassImpl -   > Rewriting temporal operators...
2023-08-07T12:27:50,108 [main] INFO  a.f.a.t.p.p.TemporalPassImpl -   > No temporal property specified, nothing to encode
2023-08-07T12:27:50,108 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #5: TemporalPass [OK]
2023-08-07T12:27:50,109 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #6: InlinePass
2023-08-07T12:27:50,109 [main] INFO  a.f.a.t.p.p.InlinePassImpl - Leaving only relevant operators: CInit, CInitPrimed, IndCand, IndCandPrimed, InvStrengthened, Next, vars
2023-08-07T12:27:50,122 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #6: InlinePass [OK]
2023-08-07T12:27:50,122 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #7: PrimingPass
2023-08-07T12:27:50,127 [main] INFO  a.f.a.t.p.a.PrimingPassImpl -   > Introducing CInitPrimed for CInit'
2023-08-07T12:27:50,128 [main] INFO  a.f.a.t.p.a.PrimingPassImpl -   > Introducing IndCandPrimed for IndCand'
2023-08-07T12:27:50,129 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #7: PrimingPass [OK]
2023-08-07T12:27:50,130 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #8: VCGen
2023-08-07T12:27:50,135 [main] INFO  a.f.a.t.b.p.VCGenPassImpl -   > Producing verification conditions from the invariant InvStrengthened
2023-08-07T12:27:50,136 [main] INFO  a.f.a.t.b.p.VCGenPassImpl -   > Using state view vars
2023-08-07T12:27:50,143 [main] INFO  a.f.a.t.b.VCGenerator -   > VCGen produced 1 verification condition(s)
2023-08-07T12:27:50,145 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #8: VCGen [OK]
2023-08-07T12:27:50,149 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #9: PreprocessingPass
2023-08-07T12:27:50,150 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Before preprocessing: unique renaming
2023-08-07T12:27:50,156 [main] INFO  a.f.a.t.p.p.PreproPassImpl -  > Applying standard transformations:
2023-08-07T12:27:50,157 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > PrimePropagation
2023-08-07T12:27:50,161 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Desugarer
2023-08-07T12:27:50,164 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > UniqueRenamer
2023-08-07T12:27:50,171 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Normalizer
2023-08-07T12:27:50,181 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > Keramelizer
2023-08-07T12:27:50,198 [main] INFO  a.f.a.t.p.p.PreproPassImpl -   > After preprocessing: UniqueRenamer
2023-08-07T12:27:50,208 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #9: PreprocessingPass [OK]
2023-08-07T12:27:50,209 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #10: TransitionFinderPass
2023-08-07T12:27:50,248 [main] INFO  a.f.a.t.p.a.TransitionPassImpl -   > Found 1 initializing transitions
2023-08-07T12:27:50,262 [main] INFO  a.f.a.t.p.a.TransitionPassImpl -   > Found 5 transitions
2023-08-07T12:27:50,263 [main] INFO  a.f.a.t.p.a.TransitionPassImpl -   > Found constant initializer CInit
2023-08-07T12:27:50,270 [main] INFO  a.f.a.t.p.a.TransitionPassImpl -   > Applying unique renaming
2023-08-07T12:27:50,276 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #10: TransitionFinderPass [OK]
2023-08-07T12:27:50,276 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #11: OptimizationPass
2023-08-07T12:27:50,283 [main] INFO  a.f.a.t.p.p.OptPassImpl -  > Applying optimizations:
2023-08-07T12:27:50,284 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ConstSimplifier
2023-08-07T12:27:50,296 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ExprOptimizer
2023-08-07T12:27:50,304 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > SetMembershipSimplifier
2023-08-07T12:27:50,307 [main] INFO  a.f.a.t.p.p.OptPassImpl -   > ConstSimplifier
2023-08-07T12:27:50,316 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #11: OptimizationPass [OK]
2023-08-07T12:27:50,316 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #12: AnalysisPass
2023-08-07T12:27:50,321 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -  > Marking skolemizable existentials and sets to be expanded...
2023-08-07T12:27:50,322 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Skolemization
2023-08-07T12:27:50,325 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Expansion
2023-08-07T12:27:50,331 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Remove unused let-in defs
2023-08-07T12:27:50,339 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -  > Running analyzers...
2023-08-07T12:27:50,345 [main] INFO  a.f.a.t.b.p.AnalysisPassImpl -   > Introduced expression grades
2023-08-07T12:27:50,345 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #12: AnalysisPass [OK]
2023-08-07T12:27:50,345 [main] INFO  a.f.a.i.p.PassChainExecutor\$ - PASS #13: BoundedChecker
2023-08-07T12:27:50,362 [main] DEBUG a.f.a.t.b.s.Z3SolverContext - Creating Z3 solver context 0
2023-08-07T12:27:50,588 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Initializing CONSTANTS
2023-08-07T12:27:50,630 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #0, transition #0
2023-08-07T12:27:50,631 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT
2023-08-07T12:27:52,503 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 0: Transition #0. Is it enabled?
2023-08-07T12:27:52,751 [main] DEBUG a.f.a.t.b.SeqModelChecker - Step 0: Transition #0 is enabled
2023-08-07T12:27:52,751 [main] INFO  a.f.a.t.b.SeqModelChecker - State 0: Checking 1 state invariants
2023-08-07T12:27:52,752 [main] DEBUG a.f.a.t.b.SeqModelChecker - State 0: Checking state invariant 0
2023-08-07T12:27:53,115 [main] INFO  a.f.a.t.b.DumpFilesModelCheckerListener\$ - Check the trace in: /home/willyschultz/endive/benchmarks/gen_tla/apalache_ctigen/AbstractStaticRaft.tla/2023-08-07T12-27-48_5650781419301164953/violation1.tla, /home/willyschultz/endive/benchmarks/gen_tla/apalache_ctigen/AbstractStaticRaft.tla/2023-08-07T12-27-48_5650781419301164953/MCviolation1.out, /home/willyschultz/endive/benchmarks/gen_tla/apalache_ctigen/AbstractStaticRaft.tla/2023-08-07T12-27-48_5650781419301164953/violation1.json, /home/willyschultz/endive/benchmarks/gen_tla/apalache_ctigen/AbstractStaticRaft.tla/2023-08-07T12-27-48_5650781419301164953/violation1.itf.json
2023-08-07T12:27:53,116 [main] INFO  a.f.a.t.b.SeqModelChecker - State 0: state invariant 0 violated.
2023-08-07T12:27:53,898 [main] INFO  a.f.a.t.b.DumpFilesModelCheckerListener\$ - Check the trace in: /home/willyschultz/endive/benchmarks/gen_tla/apalache_ctigen/AbstractStaticRaft.tla/2023-08-07T12-27-48_5650781419301164953/violation2.tla, /home/willyschultz/endive/benchmarks/gen_tla/apalache_ctigen/AbstractStaticRaft.tla/2023-08-07T12-27-48_5650781419301164953/MCviolation2.out, /home/willyschultz/endive/benchmarks/gen_tla/apalache_ctigen/AbstractStaticRaft.tla/2023-08-07T12-27-48_5650781419301164953/violation2.json, /home/willyschultz/endive/benchmarks/gen_tla/apalache_ctigen/AbstractStaticRaft.tla/2023-08-07T12-27-48_5650781419301164953/violation2.itf.json
2023-08-07T12:27:53,899 [main] INFO  a.f.a.t.b.SeqModelChecker - State 0: state invariant 0 violated.
2023-08-07T12:27:54,382 [main] ERROR a.f.a.t.Tool\$ - Unhandled exception
at.forsyte.apalache.tla.typecomp.package\$TBuilderTypeException: Operator SET_ENUM cannot be applied to arguments of types (<<Str, Seq(Int)>>, <<Str, Seq(Int)>>, <<SERVER, Seq(Int)>>)
	at at.forsyte.apalache.tla.typecomp.BuilderUtil\$.leftTypeException(BuilderUtil.scala:181)
	at at.forsyte.apalache.tla.typecomp.BuilderUtil\$.onElse\$1(BuilderUtil.scala:187)
	at at.forsyte.apalache.tla.typecomp.BuilderUtil\$.\$anonfun\$completePartial\$2(BuilderUtil.scala:193)
	at at.forsyte.apalache.tla.typecomp.signatures.SetOperSignatures\$\$anonfun\$8.applyOrElse(SetOperSignatures.scala:97)
	at at.forsyte.apalache.tla.typecomp.signatures.SetOperSignatures\$\$anonfun\$8.applyOrElse(SetOperSignatures.scala:97)
	at at.forsyte.apalache.tla.typecomp.BuilderUtil\$.\$anonfun\$completePartial\$1(BuilderUtil.scala:193)
	at at.forsyte.apalache.tla.typecomp.BuilderUtil\$.\$anonfun\$checkForArityException\$1(BuilderUtil.scala:203)
	at at.forsyte.apalache.tla.typecomp.TypeComputationFactory.\$anonfun\$computationFromSignature\$1(TypeComputationFactory.scala:40)
	at at.forsyte.apalache.tla.typecomp.package\$.\$anonfun\$fromPure\$1(package.scala:339)
	at at.forsyte.apalache.tla.typecomp.BuilderUtil\$.composeAndValidateTypes(BuilderUtil.scala:20)
	at at.forsyte.apalache.tla.typecomp.unsafe.ProtoBuilder.buildBySignatureLookup(ProtoBuilder.scala:23)
	at at.forsyte.apalache.tla.typecomp.unsafe.ProtoBuilder.buildBySignatureLookup\$(ProtoBuilder.scala:22)
	at at.forsyte.apalache.tla.typecomp.unsafe.UnsafeSetBuilder.buildBySignatureLookup(UnsafeSetBuilder.scala:17)
	at at.forsyte.apalache.tla.typecomp.unsafe.UnsafeSetBuilder.enumSet(UnsafeSetBuilder.scala:31)
	at at.forsyte.apalache.tla.typecomp.subbuilder.SetBuilder.\$anonfun\$enumSet\$1(SetBuilder.scala:26)
	at scalaz.IndexedStateT.\$anonfun\$map\$3(StateT.scala:89)
	at scalaz.IdInstances\$\$anon\$1.point(Id.scala:20)
	at scalaz.IndexedStateT.\$anonfun\$map\$2(StateT.scala:89)
	at scalaz.IndexedStateT.apply(StateT.scala:14)
	at scalaz.IndexedStateT.\$anonfun\$apply\$1(StateT.scala:19)
	at scalaz.IdInstances\$\$anon\$1.bind(Id.scala:22)
	at scalaz.IndexedStateT.apply(StateT.scala:14)
	at scalaz.IndexedStateT.\$anonfun\$apply\$1(StateT.scala:19)
	at scalaz.IdInstances\$\$anon\$1.bind(Id.scala:22)
	at scalaz.IndexedStateT.apply(StateT.scala:14)
	at scalaz.IndexedStateT.\$anonfun\$apply\$1(StateT.scala:19)
	at scalaz.IdInstances\$\$anon\$1.bind(Id.scala:22)
	at scalaz.IndexedStateT.apply(StateT.scala:14)
	at scalaz.IndexedStateT.\$anonfun\$apply\$1(StateT.scala:19)
	at scalaz.IdInstances\$\$anon\$1.bind(Id.scala:22)
	at scalaz.IndexedStateT.apply(StateT.scala:14)
	at scalaz.IndexedStateT.\$anonfun\$apply\$1(StateT.scala:19)
	at scalaz.IdInstances\$\$anon\$1.bind(Id.scala:22)
	at scalaz.IndexedStateT.apply(StateT.scala:14)
	at scalaz.IndexedStateT.\$anonfun\$apply\$1(StateT.scala:19)
	at scalaz.IdInstances\$\$anon\$1.bind(Id.scala:22)
	at scalaz.IndexedStateT.apply(StateT.scala:14)
	at scalaz.IndexedStateT.\$anonfun\$apply\$1(StateT.scala:19)
	at scalaz.IdInstances\$\$anon\$1.bind(Id.scala:22)
	at scalaz.IndexedStateT.apply(StateT.scala:14)
	at scalaz.IndexedStateT.\$anonfun\$apply\$1(StateT.scala:19)
	at scalaz.IdInstances\$\$anon\$1.bind(Id.scala:22)
	at scalaz.IndexedStateT.apply(StateT.scala:14)
	at scalaz.IndexedStateT.\$anonfun\$apply\$1(StateT.scala:19)
	at scalaz.IdInstances\$\$anon\$1.bind(Id.scala:22)
	at scalaz.IndexedStateT.apply(StateT.scala:14)
	at scalaz.IndexedStateT.\$anonfun\$apply\$1(StateT.scala:19)
	at scalaz.IdInstances\$\$anon\$1.bind(Id.scala:22)
	at scalaz.IndexedStateT.apply(StateT.scala:14)
	at scalaz.IndexedStateT.\$anonfun\$apply\$1(StateT.scala:19)
	at scalaz.IdInstances\$\$anon\$1.bind(Id.scala:22)
	at scalaz.IndexedStateT.apply(StateT.scala:14)
	at scalaz.IndexedStateT.\$anonfun\$apply\$1(StateT.scala:19)
	at scalaz.IdInstances\$\$anon\$1.bind(Id.scala:22)
	at scalaz.IndexedStateT.apply(StateT.scala:14)
	at scalaz.IndexedStateT.\$anonfun\$apply\$1(StateT.scala:19)
	at scalaz.IdInstances\$\$anon\$1.bind(Id.scala:22)
	at scalaz.IndexedStateT.apply(StateT.scala:14)
	at scalaz.IndexedStateT.\$anonfun\$apply\$1(StateT.scala:19)
	at scalaz.IdInstances\$\$anon\$1.bind(Id.scala:22)
	at scalaz.IndexedStateT.apply(StateT.scala:14)
	at scalaz.IndexedStateT.\$anonfun\$apply\$1(StateT.scala:19)
	at scalaz.IdInstances\$\$anon\$1.bind(Id.scala:22)
	at scalaz.IndexedStateT.apply(StateT.scala:14)
	at scalaz.IndexedStateT.\$anonfun\$apply\$1(StateT.scala:19)
	at scalaz.IdInstances\$\$anon\$1.bind(Id.scala:22)
	at scalaz.IndexedStateT.apply(StateT.scala:14)
	at scalaz.IndexedStateT.\$anonfun\$apply\$1(StateT.scala:19)
	at scalaz.IdInstances\$\$anon\$1.bind(Id.scala:22)
	at scalaz.IndexedStateT.apply(StateT.scala:14)
	at scalaz.IndexedStateT.\$anonfun\$apply\$1(StateT.scala:19)
	at scalaz.IdInstances\$\$anon\$1.bind(Id.scala:22)
	at scalaz.IndexedStateT.apply(StateT.scala:14)
	at scalaz.IndexedStateT.\$anonfun\$apply\$1(StateT.scala:19)
	at scalaz.IdInstances\$\$anon\$1.bind(Id.scala:22)
	at scalaz.IndexedStateT.apply(StateT.scala:14)
	at scalaz.IndexedStateT.\$anonfun\$apply\$1(StateT.scala:19)
	at scalaz.IdInstances\$\$anon\$1.bind(Id.scala:22)
	at scalaz.IndexedStateT.apply(StateT.scala:14)
	at scalaz.IndexedStateT.\$anonfun\$apply\$1(StateT.scala:19)
	at scalaz.IdInstances\$\$anon\$1.bind(Id.scala:22)
	at scalaz.IndexedStateT.apply(StateT.scala:14)
	at scalaz.IndexedStateT.\$anonfun\$apply\$1(StateT.scala:19)
	at scalaz.IdInstances\$\$anon\$1.bind(Id.scala:22)
	at scalaz.IndexedStateT.apply(StateT.scala:14)
	at scalaz.IndexedStateT.run(StateT.scala:19)
	at at.forsyte.apalache.tla.typecomp.package\$.build(package.scala:241)
	at at.forsyte.apalache.tla.bmcmt.SymbStateDecoder.\$anonfun\$decodeStateVariables\$1(SymbStateDecoder.scala:28)
	at scala.collection.StrictOptimizedMapOps.map(StrictOptimizedMapOps.scala:28)
	at scala.collection.StrictOptimizedMapOps.map\$(StrictOptimizedMapOps.scala:27)
	at scala.collection.immutable.HashMap.map(HashMap.scala:39)
	at at.forsyte.apalache.tla.bmcmt.SymbStateDecoder.decodeStateVariables(SymbStateDecoder.scala:28)
	at at.forsyte.apalache.tla.bmcmt.trex.TransitionExecutorImpl.decodePair\$1(TransitionExecutorImpl.scala:329)
	at at.forsyte.apalache.tla.bmcmt.trex.TransitionExecutorImpl.\$anonfun\$decodedExecution\$1(TransitionExecutorImpl.scala:333)
	at scala.collection.immutable.List.map(List.scala:250)
	at at.forsyte.apalache.tla.bmcmt.trex.TransitionExecutorImpl.decodedExecution(TransitionExecutorImpl.scala:333)
	at at.forsyte.apalache.tla.bmcmt.trex.FilteredTransitionExecutor.decodedExecution(FilteredTransitionExecutor.scala:191)
	at at.forsyte.apalache.tla.bmcmt.trex.ConstrainedTransitionExecutor.decodedExecution(ConstrainedTransitionExecutor.scala:115)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.\$anonfun\$checkInvariants\$2(SeqModelChecker.scala:356)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.\$anonfun\$checkInvariants\$2\$adapted(SeqModelChecker.scala:340)
	at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:576)
	at scala.collection.IterableOnceOps.foreach\$(IterableOnce.scala:574)
	at scala.collection.AbstractIterable.foreach(Iterable.scala:933)
	at scala.collection.IterableOps\$WithFilter.foreach(Iterable.scala:903)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.checkInvariants(SeqModelChecker.scala:340)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.\$anonfun\$prepareTransitionsAndCheckInvariants\$5(SeqModelChecker.scala:243)
	at scala.runtime.java8.JFunction1\$mcVI\$sp.apply(JFunction1\$mcVI\$sp.scala:18)
	at scala.collection.immutable.Range.foreach(Range.scala:190)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.prepareTransitionsAndCheckInvariants(SeqModelChecker.scala:207)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.makeStep(SeqModelChecker.scala:123)
	at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.run(SeqModelChecker.scala:62)
	at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.runIncrementalChecker(BoundedCheckerPassImpl.scala:135)
	at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.execute(BoundedCheckerPassImpl.scala:88)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.exec(PassChainExecutor.scala:64)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.\$anonfun\$runPassOnModule\$3(PassChainExecutor.scala:53)
	at scala.util.Either.flatMap(Either.scala:352)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.\$anonfun\$runPassOnModule\$1(PassChainExecutor.scala:51)
	at scala.collection.LinearSeqOps.foldLeft(LinearSeq.scala:183)
	at scala.collection.LinearSeqOps.foldLeft\$(LinearSeq.scala:179)
	at scala.collection.immutable.List.foldLeft(List.scala:79)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.runOnPasses(PassChainExecutor.scala:44)
	at at.forsyte.apalache.infra.passes.PassChainExecutor\$.run(PassChainExecutor.scala:34)
	at at.forsyte.apalache.tla.tooling.opt.CheckCmd.run(CheckCmd.scala:132)
	at at.forsyte.apalache.tla.Tool\$.runCommand(Tool.scala:138)
	at at.forsyte.apalache.tla.Tool\$.run(Tool.scala:118)
	at at.forsyte.apalache.tla.Tool\$.main(Tool.scala:40)
	at at.forsyte.apalache.tla.Tool.main(Tool.scala)

System information

  • Apalache version: 0.41.3 build 6ffe450
  • OS: Linux
  • JDK version: 17.0.8

Triage checklist (for maintainers)

  • Reproduce the bug on the main development branch.
  • Add the issue to the apalache GitHub project.
  • If the bug is high impact, ensure someone available is assigned to fix it.
@will62794 will62794 added the bug label Aug 8, 2023
@will62794 will62794 changed the title TBuilderTypeException: Operator SET_ENUM cannot be applied to arguments Uncaught TBuilderTypeException: Operator SET_ENUM cannot be applied to arguments Aug 8, 2023
@thpani thpani self-assigned this Aug 8, 2023
@thpani
Copy link
Collaborator

thpani commented Aug 8, 2023

Thanks for the report, and apologies for the broken counter-example enumeration!
It seems that some internal upgrades have broken this feature in subtle ways.

Debugging notes:

The culprit here is the decoding of ConstT1 cells in SymbStateDecoder:
if there is a ModelValueCache miss, cell is decoded into a string literal equal to the cell name:

https://github.com/informalsystems/apalache/blob/b374361ad14308921375a0d83b28a6f11a50f904/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateDecoder.scala#L54-L57

Even though we could use tla.const here (depending on tt), a secondary issue arises when rewriting this value in StrConstRule. Instead of using the type tag on the ValEx, it delegates to a regexp matching routine in ModelValueHandler to decide whether the ValEx is a ConstT1 or a StrT1:

https://github.com/informalsystems/apalache/blob/b374361ad14308921375a0d83b28a6f11a50f904/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/StrConstRule.scala#L26-L29

https://github.com/informalsystems/apalache/blob/b374361ad14308921375a0d83b28a6f11a50f904/tlair/src/main/scala/at/forsyte/apalache/tla/types/ModelValueHandler.scala#L26

https://github.com/informalsystems/apalache/blob/b374361ad14308921375a0d83b28a6f11a50f904/tlair/src/main/scala/at/forsyte/apalache/tla/types/ModelValueHandler.scala#L52-L56

Since the cell naming scheme $C$XX does not match the regex, the value is encoded as StrT1. In the end, when we assert equality for enumerating counter-examples, this StrT1-typed cell ends up being compared to a ConstT1-typed arena cell, which throws in LazyEquality as in #2683:

https://github.com/informalsystems/apalache/blob/b374361ad14308921375a0d83b28a6f11a50f904/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/LazyEquality.scala#L171-L172

@Kukovec I'm not sure how to fix the latter part, since we don't have a name for that ConstT1 arena cell. Can we rely on the expression's type tag in StrConstRule?

@will62794
Copy link
Author

@thpani Is it clear to you what part of the spec is actually causing the issue? It wasn't obvious to me from reading the error message or the stack trace. Just curious in case there might be a temporary workaround.

@thpani
Copy link
Collaborator

thpani commented Aug 9, 2023 •
edited
Loading

Is it clear to you what part of the spec is actually causing the issue?

One of the SERVER-typed function domains gets misinterpreted as Str when Apalache tries to exclude the first counter-example.

You can try to work around it by switching to Str:

--- AbstractStaticRaft.old.tla	2023-08-09 10:12:31
+++ AbstractStaticRaft.tla	2023-08-09 10:11:11
@@ -3,6 +3,7 @@
 EXTENDS Naturals, Integers, FiniteSets, Sequences, TLC, Apalache
 
 CONSTANTS 
+    \* @typeAlias: SERVER = Str;
     \* @type: Set(SERVER);
     Server
 
@@ -249,7 +249,7 @@
     /\ Primary = "P"
     /\ Secondary = "S"
     /\ Nil = "Nil"
-    /\ Server = {"1_OF_SERVER", "2_OF_SERVER", "3_OF_SERVER"}
+    /\ Server = {"1", "2", "3"}
     /\ MaxLogLen = 3
     /\ MaxTerm = 3
     /\ InitTerm = 0

Apalache will give you a warning about deprecated type alias syntax, but this should provide a workaround until we fix the issue.

@will62794
Copy link
Author

@thpani Great, thanks! I'll try that for now.

@Kukovec
Copy link
Collaborator

Kukovec commented Aug 9, 2023

I'm not sure how to fix the latter part, since we don't have a name for that ConstT1 arena cell. Can we rely on the expression's type tag in StrConstRule?

So, I've tested it with the fix in SymbStateDecoder plus adding a $ into the model value regex, and that seems to fix it. Otherwise, as you've seen, you get a str-to-const comparison error. However, that's more of a bandaid, imo. The "correct" fix, to me, would be to add a getUniqueModelValue sort of method, such that instead of relying on generating a string by name, the method would create, e.g. 4_OF_SERVER, instead of $C$XY_OF_SERVER where it's forced to create a new value of an uninterpreted sort.

@konnov
Copy link
Collaborator

konnov commented Aug 14, 2023

@thpani, @Kukovec, it looks like you have an idea of a fix already. Are you going to open a PR?

@Kukovec
Copy link
Collaborator

Kukovec commented Aug 14, 2023 •
edited
Loading

@thpani, @Kukovec, it looks like you have an idea of a fix already. Are you going to open a PR?

Yes, we discussed it in a call. I think it's on Thomas' TODO list, but he can tell you more once he gets back on Wed.

@thpani thpani mentioned this issue Aug 16, 2023
Merged
4 tasks
@coffeeinprogress coffeeinprogress mentioned this issue Oct 2, 2024
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@thpani thpani

Labels
bug
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Construct fresh model values apalache-mc/apalache
4 participants
@thpani @konnov @will62794 @Kukovec