On Monday, July 8, 2024 at 10:48:54 AM UTC-4 Ugur Y. Yavuz wrote:
Hello, I have a question about the prime operator, particularly how it gets parsed in conjunction with user-defined operators.
Consider the following operator definition, where pc and l are among the variables of the specification, and ProcSet is a constant:
WellFormed(IdxSet) ==
\A p \in ProcSet :
CASE pc[p] = "L0" -> TRUE
[] pc[p] = "L1" /\ l[p] \in IdxSet -> TRUE
[] pc[p] = "L1" /\ l[p] \notin IdxSet -> FALSE
Note that we have:
WellFormed(IdxSet)' =
\A p \in ProcSet :
CASE pc'[p] = "L0" -> TRUE
[] pc'[p] = "L1" /\ l'[p] in IdxSet -> TRUE
[] pc'[p] = "L1" /\ l'[p] \notin IdxSet -> FALSE
Suppose L and A are also variables of the specification, and that we aim to prove the invariant \E IdxSet \in SUBSET 0..L-1 : WellFormed(IdxSet) in TLAPS. After proving it for the initial configuration, we need to prove it for a subsequent configuration, reached from one where the inductive invariant holds; i.e., \E IdxSet \in SUBSET 0..L'-1 : WellFormed(IdxSet)'. Suppose the witness for this claim needs to be a function of the specification variables' values in the next configuration. Say we want to proceed as follows:
...
<3> DEFINE full_indices == {idx \in 0..(L'-1) : A'[idx] > 0}
<3>1. WellFormed(full_indices)'
However, this results in a parser error: "Level error in applying operator ': The level of argument 1 exceeds the maximum level allowed by the operator."
Is this intended behavior? The _expression_ seems equivalent to:
\A p \in ProcSet :
CASE pc'[p] = "L0" -> TRUE
[] pc'[p] = "L1" /\ l'[p] in {idx \in 0..(L'-1) : A'[idx] > 0} -> TRUE
[] pc'[p] = "L1" /\ l'[p] \notin {idx \in 0..(L'-1) : A'[idx] > 0} -> FALSE
which I can express in TLA+. This issue arose in a larger proof, and I simplified it as much as possible. I circumvented it with several rewrites, which I believe shouldn't be necessary at a first glance. I can provide more context if needed.