TBuilderTypeException in type checking of TwoPhase spec #2682

will62794 · 2023-07-31T16:45:41Z

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

Apalache version: 0.40.6 build 626668c
OS: Linux
JDK version: 17.0.7

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.

The text was updated successfully, but these errors were encountered:

shonfeder · 2023-07-31T17:38:11Z

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 · 2023-07-31T20:57:26Z

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 · 2023-07-31T21:21:40Z

@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 · 2023-08-09T09:45:14Z

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 · 2023-08-09T09:51:54Z

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 · 2023-10-12T12:37:47Z

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

Kukovec · 2023-10-17T13:29:46Z

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 · 2023-10-17T13:30:16Z

Closed by #2757

will62794 added the bug label Jul 31, 2023

Kukovec mentioned this issue Oct 11, 2023

Unexpected exception #2750

Closed

3 tasks

thpani assigned Kukovec Oct 17, 2023

Kukovec closed this as completed Oct 17, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

TBuilderTypeException in type checking of TwoPhase spec #2682

TBuilderTypeException in type checking of TwoPhase spec #2682

will62794 commented Jul 31, 2023 •

edited

Loading

shonfeder commented Jul 31, 2023

will62794 commented Jul 31, 2023

shonfeder commented Jul 31, 2023

Kukovec commented Aug 9, 2023

Kukovec commented Aug 9, 2023

Kukovec commented Oct 12, 2023

Kukovec commented Oct 17, 2023

Kukovec commented Oct 17, 2023

TBuilderTypeException in type checking of TwoPhase spec #2682

TBuilderTypeException in type checking of TwoPhase spec #2682

Comments

will62794 commented Jul 31, 2023 • edited Loading

Impact

Input specification

The command line parameters used to run the tool

Expected behavior

Log files

System information

Triage checklist (for maintainers)

shonfeder commented Jul 31, 2023

will62794 commented Jul 31, 2023

shonfeder commented Jul 31, 2023

Kukovec commented Aug 9, 2023

Kukovec commented Aug 9, 2023

Kukovec commented Oct 12, 2023

Kukovec commented Oct 17, 2023

Kukovec commented Oct 17, 2023

will62794 commented Jul 31, 2023 •

edited

Loading