LET block with temporal checking leads to undeclared operator skolem error crash #3119
Description
Description
We get an unexpected unexpected expression: undeclared operator variableName$1$_skolem error only when all of the below conditions are enabled:
- Temporal property checking via
--temporalis enabled - Multiple variables are used in the spec
- An action's guard is specified in a
LETblock
Impact
We can avoid it by eliminating the LET block (using multiple variables and using temporal specifications are difficult to avoid) and writing the condition directly (could be overly verbose / harder to read / etc), but the error message is extremely confusing and frustrating.
Input specification
\* apalache-mc check --debug --write-intermediate --temporal=EmptyProperty SkolemBug.tla
------------------------------- MODULE SkolemBug -------------------------------
EXTENDS Integers, Sequences, FiniteSets, TLC, Option
VARIABLES
\* @type: Int -> Set(<<Int, Int>>);
myMainVar,
\* Seems to be necessary to trigger the bug
\* @type: Int -> Str;
myOther
vars == << myOther, myMainVar >>
MyInit(t) ==
/\ myMainVar = [ x \in t |-> {} ]
/\ myOther = [ x \in t |-> "Idle" ]
ThreadNext(self) ==
LET
myLetCondition == (myMainVar[self] /= {})
IN
myLetCondition /\
\* Putting the condition without the LET doesn't trigger the error
\*(myMainVar[self] /= {}) /\
UNCHANGED << myOther, myMainVar>>
Threads == {1, 2, 3}
Init == MyInit(Threads)
\* --temporal=EmptyProperty is necessary to trigger the bug
EmptyProperty == TRUE
Terminating == UNCHANGED vars
Next ==
(\E self \in Threads: ThreadNext(self))
\/ Terminating
Spec == Init /\ [][Next]_vars
=============================================================================
The command line parameters used to run the tool
--debug --write-intermediate --temporal=EmptyProperty
Expected behavior
No crash, or a clear error message explaining to the user why this spec is unsupported by Apalache.
Note that the spec does not cause TLC to crash.
Log files
PASS #1: TypeCheckerSnowcat I@17:54:57.408
> Running Snowcat .::. I@17:54:57.408
> Your types are purrfect! I@17:54:58.045
> All expressions are typed I@17:54:58.046
PASS #2: ConfigurationPass I@17:54:58.083
> Set the initialization predicate to Init I@17:54:58.088
> Set the transition predicate to Next I@17:54:58.088
> Set a temporal property to EmptyProperty I@17:54:58.089
PASS #3: DesugarerPass I@17:54:58.133
> Desugaring... I@17:54:58.133
PASS #4: InlinePass I@17:54:58.454
Leaving only relevant operators: CInitPrimed, EmptyProperty, Init, InitPrimed, Next I@17:54:58.454
PASS #5: TemporalPass I@17:54:58.535
> Rewriting temporal operators... I@17:54:58.535
> Temporal property EmptyProperty has no temporal operators, so it specifies a property of the initial state. Should EmptyProperty be an invariant instead (--inv)? W@17:54:58.541
> Found 1 temporal properties I@17:54:58.542
> Adding logic for loop finding I@17:54:58.543
PASS #6: InlinePass I@17:54:58.603
Leaving only relevant operators: CInitPrimed, EmptyProperty, Init, InitPrimed, Next I@17:54:58.604
PASS #7: PrimingPass I@17:54:58.624
> Introducing InitPrimed for Init' I@17:54:58.630
PASS #8: VCGen I@17:54:58.655
> Producing verification conditions from the invariant EmptyProperty I@17:54:58.657
> VCGen produced 1 verification condition(s) I@17:54:58.665
PASS #9: PreprocessingPass I@17:54:58.685
> Before preprocessing: unique renaming I@17:54:58.685
> Applying standard transformations: I@17:54:58.701
> PrimePropagation I@17:54:58.702
> Desugarer I@17:54:58.720
> UniqueRenamer I@17:54:58.743
> Normalizer I@17:54:58.754
> Keramelizer I@17:54:58.768
> After preprocessing: UniqueRenamer I@17:54:58.787
No source location for expr@13332: (myMainVar = ([x$1 ∈ {1, 2, 3} ↦ {}])) ∧ (myOther = ([x$2 ∈ {1, 2, 3}... E@17:54:58.803
No source location for expr@13367: ((∃self$1 ∈ {1, 2, 3}: LET myLetCondition$1 ≜ myMainVar[self$1] ≠ {} ... E@17:54:58.805
No source location for expr@13384: (__InLoop ∧ (myMainVar = __saved_myMainVar) ∧ (myOther = __saved_myOt... E@17:54:58.806
No source location for expr@13435: (myMainVar' = ([x$1 ∈ {1, 2, 3} ↦ {}])) ∧ (myOther' = ([x$2 ∈ {1, 2, ... E@17:54:58.807
No source location for expr@13384: (__InLoop ∧ (myMainVar = __saved_myMainVar) ∧ (myOther = __saved_myOt... E@17:54:58.807
No source location for expr@13448: ¬((__InLoop ∧ (myMainVar = __saved_myMainVar) ∧ (myOther = __saved_my... E@17:54:58.807
PASS #10: TransitionFinderPass I@17:54:58.810
> Found 1 initializing transitions I@17:54:58.828
> Found 4 transitions I@17:54:58.840
> No constant initializer I@17:54:58.842
> Applying unique renaming I@17:54:58.844
PASS #11: OptimizationPass I@17:54:58.858
> Applying optimizations: I@17:54:58.868
> ConstSimplifier I@17:54:58.869
> ExprOptimizer I@17:54:58.879
> SetMembershipSimplifier I@17:54:58.883
> ConstSimplifier I@17:54:58.885
PASS #12: AnalysisPass I@17:54:58.908
> Marking skolemizable existentials and sets to be expanded... I@17:54:58.913
> Skolemization I@17:54:58.914
> Expansion I@17:54:58.915
SkolemBug.tla:38:4-38:40: unexpected expression: undeclared operator myLetCondition$1$_skolem E@17:54:58.927
Unexpected expressions in the specification (see the error messages) E@17:54:58.929
It took me 0 days 0 hours 0 min 2 sec I@17:54:58.930
Total time: 2.180 sec I@17:54:58.930
EXITCODE: ERROR (255)
System information
- Apalache version:
56462d3 build 56462d3(revision56462d384d63853ceb503c8eb86a4eff02572529frommainbranch) - OS: Ubuntu Linux x86_64 24.04
- JDK version:
21.0.3
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.