search

apalache-mc / apalache

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

TBuilderTypeException in type checking of TwoPhase spec #2682

Closed will62794 closed 11 months ago

will62794 commented 1 year ago

Impact

Type-checking fails on a relatively small spec of two-phase commit, preventing successful bounded model checking or checking of inductive invariants.

Input specification

------------------------------- MODULE TwoPhase ----------------------------- 
\* benchmark: tla-twophase
EXTENDS TLC, Naturals

(***************************************************************************)
(* This specification describes the Two-Phase Commit protocol, in which a  *)
(* transaction manager (TM) coordinates the resource managers (RMs) to     *)
(* implement the Transaction Commit specification of module $TCommit$.  In *)
(* this specification, RMs spontaneously issue $Prepared$ messages.  We    *)
(* ignore the $Prepare$ messages that the TM can send to the               *)
(* RMs.\vspace{.4em}                                                       *)
(*                                                                         *)
(* For simplicity, we also eliminate $Abort$ messages sent by an RM when   *)
(* it decides to abort.  Such a message would cause the TM to abort the    *)
(* transaction, an event represented here by the TM spontaneously deciding *)
(* to abort.\vspace{.4em}                                                  *)
(*                                                                         *)
(* This specification describes only the safety properties of the          *)
(* protocol--that is, what is allowed to happen.  What must happen would   *)
(* be described by liveness properties, which we do not specify.           *)
(***************************************************************************)

CONSTANT 
    \* @type: Set(RM);
    RM \* The set of resource managers

\* Message ==
\*   (*************************************************************************)
\*   (* The set of all possible messages.  Messages of type $"Prepared"$ are  *)
\*   (* sent from the RM indicated by the message's $rm$ field to the TM\@.   *)
\*   (* Messages of type $"Commit"$ and $"Abort"$ are broadcast by the TM, to *)
\*   (* be received by all RMs.  The set $msgs$ contains just a single copy   *)
\*   (* of such a message.                                                    *)
\*   (*************************************************************************)
\*   [type : {"Prepared"}, rm : RM]  \cup  [type : {"Commit", "Abort"}]
\*   [type : {"Prepared", "Commit", "Abort"}, rm : RM] 

VARIABLES
  \* @type: RM -> Str;
  rmState,       \* $rmState[rm]$ is the state of resource manager RM.
  \* @type: Str;
  tmState,       \* The state of the transaction manager.
  \* @type: Set(RM);
  tmPrepared,    \* The set of RMs from which the TM has received "Prepared" messages
  \* @type: Set( { type: Str, rm: RM } );
  msgsPrepared,
  \* @type: Set( { type: Str } );
  msgsAbortCommit

vars == <<rmState, tmState, tmPrepared, msgsPrepared, msgsAbortCommit>>

    (***********************************************************************)
    (* In the protocol, processes communicate with one another by sending  *)
    (* messages.  Since we are specifying only safety, a process is not    *)
    (* required to receive a message, so there is no need to model message *)
    (* loss.  (There's no difference between a process not being able to   *)
    (* receive a message because the message was lost and a process simply *)
    (* ignoring the message.)  We therefore represent message passing with *)
    (* a variable $msgs$ whose value is the set of all messages that have  *)
    (* been sent.  Messages are never removed from $msgs$.  An action      *)
    (* that, in an implementation, would be enabled by the receipt of a    *)
    (* certain message is here enabled by the existence of that message in *)
    (* $msgs$.  (Receipt of the same message twice is therefore allowed;   *)
    (* but in this particular protocol, receiving a message for the second *)
    (* time has no effect.)                                                *)
    (***********************************************************************)

TypeOK ==  
  (*************************************************************************)
  (* The type-correctness invariant                                        *)
  (*************************************************************************)
  /\ rmState \in [RM -> {"working", "prepared", "committed", "aborted"}]
  /\ tmState \in {"init", "committed", "aborted"}
  /\ tmPrepared \in SUBSET RM
  /\ msgsPrepared \in SUBSET [type : {"Prepared"}, rm : RM]
  /\ msgsAbortCommit \in SUBSET [type : {"Commit", "Abort"}]

Init ==   
  (*************************************************************************)
  (* The initial predicate.                                                *)
  (*************************************************************************)
  /\ rmState = [rm \in RM |-> "working"]
  /\ tmState = "init"
  /\ tmPrepared   = {}
  /\ msgsPrepared = {}
  /\ msgsAbortCommit = {}
-----------------------------------------------------------------------------
(***************************************************************************)
(* We now define the actions that may be performed by the processes, first *)
(* the TM's actions, then the RMs' actions.                                *)
(***************************************************************************)
TMRcvPrepared(rm) ==
  (*************************************************************************)
  (* The TM receives a $"Prepared"$ message from resource manager $rm$.    *)
  (*************************************************************************)
  /\ tmState = "init"
  /\ [type |-> "Prepared", rm |-> rm] \in msgsPrepared
  /\ tmPrepared' = tmPrepared \cup {rm}
  /\ UNCHANGED <<rmState, tmState, msgsPrepared, msgsAbortCommit>>

TMCommit ==
  (*************************************************************************)
  (* The TM commits the transaction; enabled iff the TM is in its initial  *)
  (* state and every RM has sent a $"Prepared"$ message.                   *)
  (*************************************************************************)
  /\ tmState = "init"
  /\ tmPrepared = RM
  /\ tmState' = "committed"
  /\ msgsAbortCommit' = msgsAbortCommit \cup {[type |-> "Commit"]}
  /\ UNCHANGED <<rmState, tmPrepared, msgsPrepared>>

TMAbort ==
  (*************************************************************************)
  (* The TM spontaneously aborts the transaction.                          *)
  (*************************************************************************)
  /\ tmState = "init"
  /\ tmState' = "aborted"
  /\ msgsAbortCommit' = msgsAbortCommit \cup {[type |-> "Abort"]}
  /\ UNCHANGED <<rmState, tmPrepared, msgsPrepared>>

RMPrepare(rm) == 
  (*************************************************************************)
  (* Resource manager $rm$ prepares.                                       *)
  (*************************************************************************)
  /\ rmState[rm] = "working"
  /\ rmState' = [rmState EXCEPT ![rm] = "prepared"]
  /\ msgsPrepared' = msgsPrepared \cup {[type |-> "Prepared", rm |-> rm]}
  /\ UNCHANGED <<tmState, tmPrepared, msgsAbortCommit>>

RMChooseToAbort(rm) ==
  (*************************************************************************)
  (* Resource manager $rm$ spontaneously decides to abort.  As noted       *)
  (* above, $rm$ does not send any message in our simplified spec.         *)
  (*************************************************************************)
  /\ rmState[rm] = "working"
  /\ rmState' = [rmState EXCEPT ![rm] = "aborted"]
  /\ UNCHANGED <<tmState, tmPrepared, msgsPrepared, msgsAbortCommit>>

RMRcvCommitMsg(rm) ==
  (*************************************************************************)
  (* Resource manager $rm$ is told by the TM to commit.                    *)
  (*************************************************************************)
  /\ [type |-> "Commit"] \in msgsAbortCommit
  /\ rmState[rm] # "committed" \* no need to commit twice.
  /\ rmState' = [rmState EXCEPT ![rm] = "committed"]
  /\ UNCHANGED <<tmState, tmPrepared, msgsPrepared, msgsAbortCommit>>

RMRcvAbortMsg(rm) ==
  (*************************************************************************)
  (* Resource manager $rm$ is told by the TM to abort.                     *)
  (*************************************************************************)
  /\ [type |-> "Abort"] \in msgsAbortCommit
  /\ rmState[rm] # "aborted" \* no need to abort twice.
  /\ rmState' = [rmState EXCEPT ![rm] = "aborted"]
  /\ UNCHANGED <<tmState, tmPrepared, msgsPrepared, msgsAbortCommit>>

Next ==
  \/ TMCommit 
  \/ TMAbort
  \/ \E rm \in RM : TMRcvPrepared(rm) 
  \/ \E rm \in RM : RMPrepare(rm) 
  \/ \E rm \in RM : RMChooseToAbort(rm)
  \/ \E rm \in RM : RMRcvCommitMsg(rm) 
  \/ \E rm \in RM : RMRcvAbortMsg(rm)
-----------------------------------------------------------------------------
TPSpec == Init /\ [][Next]_<<rmState, tmState, tmPrepared, msgsPrepared, msgsAbortCommit>>

NextUnchanged == UNCHANGED vars

Symmetry == Permutations(RM)

TCConsistent ==  
  (*************************************************************************)
  (* A state predicate asserting that two RMs have not arrived at          *)
  (* conflicting decisions.                                                *)
  (*************************************************************************)
  \A rm1, rm2 \in RM : ~ (rmState[rm1] = "aborted" /\ rmState[rm2] = "committed")

  (*************************************************************************)
  (* The complete spec of the Two-Phase Commit protocol.                   *)
  (*************************************************************************)

THEOREM TPSpec => []TypeOK

ApaInv == TypeOK /\ TCConsistent

=============================================================================

The command line parameters used to run the tool

--init=ApaInv --next=Next --inv=ApaInv --config=benchmarks/TwoPhase.cfg

Expected behavior

Expected type-checking to pass and model checker to start checking specified invariant.

Log files

``` 2023-07-31T16:22:41,660 [main] INFO a.f.a.t.Tool\$ - # APALACHE version: 0.40.6 | build: 626668c 2023-07-31T16:22:41,683 [main] INFO a.f.a.i.p.o.OptionGroup\$ - > TwoPhase.cfg: Loading TLC configuration 2023-07-31T16:22:41,742 [main] WARN a.f.a.i.p.o.OptionGroup\$ - > init is set in TLC config but overridden via `init` cli option or apalache.cfg; using ApaInv 2023-07-31T16:22:41,742 [main] WARN a.f.a.i.p.o.OptionGroup\$ - > next is set in TLC config but overridden via `next` cli option or apalache.cfg; using Next 2023-07-31T16:22:41,743 [main] WARN a.f.a.i.p.o.OptionGroup\$ - > inv is set in TLC config but overridden via `inv` cli option or apalache.cfg; using ApaInv 2023-07-31T16:22:41,744 [main] INFO a.f.a.t.t.o.CheckCmd - Tuning: search.outputTraces=false 2023-07-31T16:22:41,960 [main] INFO a.f.a.i.p.PassChainExecutor\$ - PASS #0: SanyParser 2023-07-31T16:22:42,365 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #0: SanyParser [OK] 2023-07-31T16:22:42,366 [main] INFO a.f.a.i.p.PassChainExecutor\$ - PASS #1: TypeCheckerSnowcat 2023-07-31T16:22:42,366 [main] INFO a.f.a.t.p.t.EtcTypeCheckerPassImpl - > Running Snowcat .::. 2023-07-31T16:22:42,932 [main] INFO a.f.a.t.p.t.EtcTypeCheckerPassImpl - > Your types are purrfect! 2023-07-31T16:22:42,932 [main] INFO a.f.a.t.p.t.EtcTypeCheckerPassImpl - > All expressions are typed 2023-07-31T16:22:42,932 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #1: TypeCheckerSnowcat [OK] 2023-07-31T16:22:42,933 [main] INFO a.f.a.i.p.PassChainExecutor\$ - PASS #2: ConfigurationPass 2023-07-31T16:22:42,945 [main] INFO a.f.a.t.p.p.ConfigurationPassImpl - > TwoPhase.cfg: found INVARIANTS: ApaInv 2023-07-31T16:22:42,950 [main] INFO a.f.a.t.p.p.ConfigurationPassImpl - > Set the initialization predicate to ApaInv 2023-07-31T16:22:42,951 [main] INFO a.f.a.t.p.p.ConfigurationPassImpl - > Set the transition predicate to Next 2023-07-31T16:22:42,952 [main] INFO a.f.a.t.p.p.ConfigurationPassImpl - > Set the constant initialization predicate to CInit 2023-07-31T16:22:42,952 [main] INFO a.f.a.t.p.p.ConfigurationPassImpl - > Set an invariant to ApaInv 2023-07-31T16:22:42,960 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #2: ConfigurationPass [OK] 2023-07-31T16:22:42,960 [main] INFO a.f.a.i.p.PassChainExecutor\$ - PASS #3: DesugarerPass 2023-07-31T16:22:42,961 [main] INFO a.f.a.t.p.p.DesugarerPassImpl - > Desugaring... 2023-07-31T16:22:43,160 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #3: DesugarerPass [OK] 2023-07-31T16:22:43,161 [main] INFO a.f.a.i.p.PassChainExecutor\$ - PASS #4: InlinePass 2023-07-31T16:22:43,161 [main] INFO a.f.a.t.p.p.InlinePassImpl - Leaving only relevant operators: ApaInv, ApaInvPrimed, CInit, CInitPrimed, Next 2023-07-31T16:22:43,205 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #4: InlinePass [OK] 2023-07-31T16:22:43,206 [main] INFO a.f.a.i.p.PassChainExecutor\$ - PASS #5: TemporalPass 2023-07-31T16:22:43,206 [main] INFO a.f.a.t.p.p.TemporalPassImpl - > Rewriting temporal operators... 2023-07-31T16:22:43,206 [main] INFO a.f.a.t.p.p.TemporalPassImpl - > No temporal property specified, nothing to encode 2023-07-31T16:22:43,207 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #5: TemporalPass [OK] 2023-07-31T16:22:43,207 [main] INFO a.f.a.i.p.PassChainExecutor\$ - PASS #6: InlinePass 2023-07-31T16:22:43,207 [main] INFO a.f.a.t.p.p.InlinePassImpl - Leaving only relevant operators: ApaInv, ApaInvPrimed, CInit, CInitPrimed, Next 2023-07-31T16:22:43,213 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #6: InlinePass [OK] 2023-07-31T16:22:43,213 [main] INFO a.f.a.i.p.PassChainExecutor\$ - PASS #7: PrimingPass 2023-07-31T16:22:43,215 [main] INFO a.f.a.t.p.a.PrimingPassImpl - > Introducing CInitPrimed for CInit' 2023-07-31T16:22:43,217 [main] INFO a.f.a.t.p.a.PrimingPassImpl - > Introducing ApaInvPrimed for ApaInv' 2023-07-31T16:22:43,220 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #7: PrimingPass [OK] 2023-07-31T16:22:43,221 [main] INFO a.f.a.i.p.PassChainExecutor\$ - PASS #8: VCGen 2023-07-31T16:22:43,222 [main] INFO a.f.a.t.b.p.VCGenPassImpl - > Producing verification conditions from the invariant ApaInv 2023-07-31T16:22:43,230 [main] INFO a.f.a.t.b.VCGenerator - > VCGen produced 6 verification condition(s) 2023-07-31T16:22:43,231 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #8: VCGen [OK] 2023-07-31T16:22:43,231 [main] INFO a.f.a.i.p.PassChainExecutor\$ - PASS #9: PreprocessingPass 2023-07-31T16:22:43,232 [main] INFO a.f.a.t.p.p.PreproPassImpl - > Before preprocessing: unique renaming 2023-07-31T16:22:43,240 [main] INFO a.f.a.t.p.p.PreproPassImpl - > Applying standard transformations: 2023-07-31T16:22:43,241 [main] INFO a.f.a.t.p.p.PreproPassImpl - > PrimePropagation 2023-07-31T16:22:43,246 [main] INFO a.f.a.t.p.p.PreproPassImpl - > Desugarer 2023-07-31T16:22:43,250 [main] INFO a.f.a.t.p.p.PreproPassImpl - > UniqueRenamer 2023-07-31T16:22:43,260 [main] INFO a.f.a.t.p.p.PreproPassImpl - > Normalizer 2023-07-31T16:22:43,267 [main] INFO a.f.a.t.p.p.PreproPassImpl - > Keramelizer 2023-07-31T16:22:43,283 [main] INFO a.f.a.t.p.p.PreproPassImpl - > After preprocessing: UniqueRenamer 2023-07-31T16:22:43,291 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #9: PreprocessingPass [OK] 2023-07-31T16:22:43,292 [main] INFO a.f.a.i.p.PassChainExecutor\$ - PASS #10: TransitionFinderPass 2023-07-31T16:22:43,319 [main] INFO a.f.a.t.p.a.TransitionPassImpl - > Found 1 initializing transitions 2023-07-31T16:22:43,327 [main] INFO a.f.a.t.p.a.TransitionPassImpl - > Found 7 transitions 2023-07-31T16:22:43,328 [main] INFO a.f.a.t.p.a.TransitionPassImpl - > Found constant initializer CInit 2023-07-31T16:22:43,337 [main] INFO a.f.a.t.p.a.TransitionPassImpl - > Applying unique renaming 2023-07-31T16:22:43,342 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #10: TransitionFinderPass [OK] 2023-07-31T16:22:43,343 [main] INFO a.f.a.i.p.PassChainExecutor\$ - PASS #11: OptimizationPass 2023-07-31T16:22:43,348 [main] INFO a.f.a.t.p.p.OptPassImpl - > Applying optimizations: 2023-07-31T16:22:43,349 [main] INFO a.f.a.t.p.p.OptPassImpl - > ConstSimplifier 2023-07-31T16:22:43,355 [main] INFO a.f.a.t.p.p.OptPassImpl - > ExprOptimizer 2023-07-31T16:22:43,360 [main] INFO a.f.a.t.p.p.OptPassImpl - > SetMembershipSimplifier 2023-07-31T16:22:43,362 [main] INFO a.f.a.t.p.p.OptPassImpl - > ConstSimplifier 2023-07-31T16:22:43,367 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #11: OptimizationPass [OK] 2023-07-31T16:22:43,367 [main] INFO a.f.a.i.p.PassChainExecutor\$ - PASS #12: AnalysisPass 2023-07-31T16:22:43,370 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Marking skolemizable existentials and sets to be expanded... 2023-07-31T16:22:43,371 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Skolemization 2023-07-31T16:22:43,372 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Expansion 2023-07-31T16:22:43,374 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Remove unused let-in defs 2023-07-31T16:22:43,378 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Running analyzers... 2023-07-31T16:22:43,383 [main] INFO a.f.a.t.b.p.AnalysisPassImpl - > Introduced expression grades 2023-07-31T16:22:43,383 [main] DEBUG a.f.a.i.p.PassChainExecutor\$ - PASS #12: AnalysisPass [OK] 2023-07-31T16:22:43,384 [main] INFO a.f.a.i.p.PassChainExecutor\$ - PASS #13: BoundedChecker 2023-07-31T16:22:43,398 [main] DEBUG a.f.a.t.b.s.Z3SolverContext - Creating Z3 solver context 0 2023-07-31T16:22:43,641 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Initializing CONSTANTS 2023-07-31T16:22:43,680 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Step #0, transition #0 2023-07-31T16:22:43,680 [main] DEBUG a.f.a.t.b.t.TransitionExecutorImpl - Translating to SMT 2023-07-31T16:22:43,763 [main] ERROR a.f.a.t.Tool\$ - Unhandled exception at.forsyte.apalache.tla.typecomp.package\$TBuilderTypeException: Operator SET_IN cannot be applied to arguments of types ({ rm: Str, type: Str }, Set({ rm: RM, type: Str })) 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\$\$nestedInanonfun\$getMap\$2\$1.applyOrElse(SetOperSignatures.scala:40) at at.forsyte.apalache.tla.typecomp.signatures.SetOperSignatures\$\$anonfun\$\$nestedInanonfun\$getMap\$2\$1.applyOrElse(SetOperSignatures.scala:40) 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.in(UnsafeSetBuilder.scala:38) at at.forsyte.apalache.tla.typecomp.subbuilder.SetBuilder.\$anonfun\$in\$1(SetBuilder.scala:33) at at.forsyte.apalache.tla.typecomp.BuilderUtil\$.\$anonfun\$binaryFromUnsafe\$2(BuilderUtil.scala:167) 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:13) 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.smt.Z3SolverContext.toExpr(Z3SolverContext.scala:813) at at.forsyte.apalache.tla.bmcmt.smt.Z3SolverContext.toExpr(Z3SolverContext.scala:746) at at.forsyte.apalache.tla.bmcmt.smt.Z3SolverContext.assertGroundExpr(Z3SolverContext.scala:325) at at.forsyte.apalache.tla.bmcmt.smt.RecordingSolverContext.assertGroundExpr(RecordingSolverContext.scala:158) at at.forsyte.apalache.tla.bmcmt.rules.aux.MapBase.\$anonfun\$mapCellsManyArgs\$3(MapBase.scala:118) at at.forsyte.apalache.tla.bmcmt.rules.aux.MapBase.\$anonfun\$mapCellsManyArgs\$3\$adapted(MapBase.scala:107) 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.rules.aux.MapBase.mapCellsManyArgs(MapBase.scala:107) at at.forsyte.apalache.tla.bmcmt.rules.aux.MapBase.rewriteSetMapManyArgs(MapBase.scala:74) at at.forsyte.apalache.tla.bmcmt.rules.SetMapRule.apply(SetMapRule.scala:29) at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:355) at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive\$1(SymbStateRewriterImpl.scala:388) at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:422) at at.forsyte.apalache.tla.bmcmt.rules.PowSetCtorRule.apply(PowSetCtorRule.scala:26) at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:355) at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive\$1(SymbStateRewriterImpl.scala:388) at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:422) at at.forsyte.apalache.tla.bmcmt.rules.QuantRule.apply(QuantRule.scala:46) at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:355) at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive\$1(SymbStateRewriterImpl.scala:388) at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:422) at at.forsyte.apalache.tla.bmcmt.rules.AndRule.mapArg\$1(AndRule.scala:62) at at.forsyte.apalache.tla.bmcmt.rules.AndRule.\$anonfun\$apply\$2(AndRule.scala:66) at scala.collection.immutable.List.map(List.scala:250) at scala.collection.immutable.List.map(List.scala:79) at at.forsyte.apalache.tla.bmcmt.rules.AndRule.apply(AndRule.scala:66) at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:355) at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive\$1(SymbStateRewriterImpl.scala:388) at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:422) at at.forsyte.apalache.tla.bmcmt.rules.AndRule.mapArg\$1(AndRule.scala:62) at at.forsyte.apalache.tla.bmcmt.rules.AndRule.\$anonfun\$apply\$2(AndRule.scala:66) at scala.collection.immutable.List.map(List.scala:246) at scala.collection.immutable.List.map(List.scala:79) at at.forsyte.apalache.tla.bmcmt.rules.AndRule.apply(AndRule.scala:66) at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteOnce(SymbStateRewriterImpl.scala:355) at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.doRecursive\$1(SymbStateRewriterImpl.scala:388) at at.forsyte.apalache.tla.bmcmt.SymbStateRewriterImpl.rewriteUntilDone(SymbStateRewriterImpl.scala:422) at at.forsyte.apalache.tla.bmcmt.trex.TransitionExecutorImpl.prepareTransition(TransitionExecutorImpl.scala:107) at at.forsyte.apalache.tla.bmcmt.trex.FilteredTransitionExecutor.prepareTransition(FilteredTransitionExecutor.scala:48) at at.forsyte.apalache.tla.bmcmt.trex.ConstrainedTransitionExecutor.prepareTransition(ConstrainedTransitionExecutor.scala:98) at at.forsyte.apalache.tla.bmcmt.SeqModelChecker.\$anonfun\$prepareTransitionsAndCheckInvariants\$5(SeqModelChecker.scala:213) 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

Triage checklist (for maintainers)

shonfeder commented 1 year ago

Thank you for the report, @will62794, and sorry for the gnarly error message there!

Fortunately the problem can be easily addressed in this case. You have

CONSTANT 
    \* @type: Set(RM);
    RM \* The set of resource managers

Which says the constant RM is typed as a set of values of type RM, but RM itself is not defined. This leads our type checker to interpret RM as an abstract type. But it looks like something else in you spec or configuration is expecting the set RM to contain strings. To fix this, you can just make RM a type alias.

This addition will make your spec go thru

+ \* @typeAlias: RM = Str;
+ TypeAliases == TRUE
+ 
+ CInit ==
+   RM = {"a", "b"}

  CONSTANT
      \* @type: Set(RM);
      RM \* The set of resource managers

with 

$  apalache-mc check --init=ApaInv --next=Next --inv=ApaInv --cinit=CInit TwoPhase.tla

Note that I am only using CInit here to make the constant initialization plain.

This is discussed a bit in our manual here https://apalache.informal.systems/docs/adr/002adr-types.html?highlight=type%20alias#11-type-grammar-type-system-1-or-ts1 -- tho I apologize in advance for the documentation not being extremely clear on this point.

You may also find https://apalache.informal.systems/docs/HOWTOs/howto-write-type-annotations.html?highlight=type%20alias#recipe-6-type-aliases useful.

Please let me know if this doesn't unblock you!

will62794 commented 1 year ago

Thanks @shonfeder. I think your workaround makes sense but shouldn't there be a way to have Apalache correctly treat RM as an uninterpreted type in this case, as discussed here? I guess I am still just a bit confused as to whether the behavior reported above is a bug in Apalache or simply incorrect usage on my part.

To give a bit more detail, in my config file I was setting 

CONSTANT RM = {r1,r2,r3}

which perhaps isn't supported by Apalache in this setting. Based on that documentation page, perhaps it is more correct to instantiate the uninterpreted type concretely as 

CONSTANT RM = {"1_OF_RM","2_OF_RM","3_OF_RM"}

following the convention mentioned there. When I just tried defining

CInit == RM = {"1_OF_RM", "2_OF_RM", "3_OF_RM"}

in my spec and then running

$ apalache/bin/apalache-mc check  --init=ApaInv --next=Next --inv=ApaInv --cinit=CInit benchmarks/TwoPhase.tla

this appeared to avoid the error and model checking completed successfully.

shonfeder commented 1 year ago

@will62794 you’ve found the correct way to set RM as an uninterpreted type and create value for it! Not knowing what was in your .cfg I assumed you wanted to assign these as strings, which was a mistake on my part :)

I guess I am still just a bit confused as to whether the behavior reported above is a bug in Apalache or simply incorrect usage on my part.

there is a bug in Apalache in that we are letting an unhandled exception thru, and not catching this earlier in typechecking. But it looks like you also had an invalid cfg, which is arguably due to a bug in our documentation.

thanks for following up with your fix, and again for the report. Let us know if you hit more snags!

Kukovec commented 1 year ago

Alright, so here's the actual underlying problem:

PASS #1: TypeCheckerSnowcat
...
PASS #1: TypeCheckerSnowcat [OK]
PASS #2: ConfigurationPass
...
PASS #2: ConfigurationPass [OK]

Basically, Apalache typechecks the spec, which passes, since RM is annotated with Set(RM). Then, it loads up the TLC config, and overrides the definition of RM with {"ModelValue_r1","ModelValue_r2","ModelValue_r3"}, a set of strings. Now, had this happened before typechecking, we'd have no problem (or rather, Apalache'd throw a type error, since the RM in config does not contain elements of the correct type). However, since the substitution happens afterwards, we have broken type-correctness, and the tool proceeds with the assumption that typechecking has succeeded, until a point where a sanity check expects a value from RM (the set) to have type RM (the uniterpreted type).

Kukovec commented 1 year ago

The issue with fixing this is, we'd have to somehow be able to support apalache type-annotations, and apalache uninterpreted-type values inside TLC config files to get sensible feedback on error (even if you write X_OF_T inside cfg files, it gets read as a string, not a T-typed value) . My recommendation is to use the Apalache-native --cinit, instead of TLC config files going forward, as I don't think this will get fixed in the near future, as the cfg format is out of our control.

Kukovec commented 11 months ago

TODO note to self: investigate whether #2757 closed this issue too.

Kukovec commented 11 months ago

Confirmed, using CONSTANT RM = {r1,r2,r3} triggers a type error warning (as expected):

ASS #2: ConfigurationPass                                        I@15:17:20.973
  > test.cfg: found INVARIANTS: Inv                               I@15:17:21.236
<unknown>: type input error: Constant RM declared in the specification has the type tag Typed(Set(RM)), while the value defined in the .cfg file has the type tag Typed(Set(Str)).
Please make sure the values in the .cfg file have types matching those in the specification, or use --cinit instead. E@15:17:21.248
It took me 0 days  0 hours  0 min  2 sec                          I@15:17:21.249
Total time: 2.98 sec                                              I@15:17:21.250
EXITCODE: ERROR (255)

and using CONSTANT RM = {"1_OF_RM","2_OF_RM","3_OF_RM"} successfully runs MC.

Kukovec commented 11 months ago

Closed by #2757