Parsing issues with prime operator in user-defined operators

[Ugur Y. Yavuz]

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.

[Andrew Helwer]

Is this an issue with SANY or the TLAPM parser?

[Leslie Lamport]

It’s not a bug.  The expression WellFormed(full_indices)' has a double prime.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c0587e72-002b-45c9-9b5b-c15ff269a298n%40googlegroups.com.

[Damien Doligez]

On Monday, July 8, 2024 at 4:48:54 PM UTC+2 Ugur Y. Yavuz wrote:

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

Not quite. What you have is:

 

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

So if you pass an expression with a primed variable for IdxSet you get a double prime, which is forbidden.

You could DEFINE full_indices == {idx \in 0..(L-1) : A[idx] > 0}

and then you get the expression you wanted for WellFormed(full_indices)'

[Ugur Y. Yavuz]

> Is this an issue with SANY or the TLAPM parser?

This is regarding SANY. It came up while I was working on a TLAPS proof, but it would also happen if I tried to define the action elsewhere.

> It's not a bug. The expression WellFormed(full_indices)' has a double prime.

It doesn't have a double prime, in the sense that once you substitute the provided argument's definition in the predicate, there is no variable which is double primed (see the expression it is semantically equivalent to). That's why I wasn't sure if the parser rejecting this expression was intended behavior.

[Ugur Y. Yavuz]

@Damien: That is also correct, but IdxSet = IdxSet' as IdxSet is a constant (under the quantifier). On my end, the following claim goes through trivially:

WellFormedTest(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

LEMMA WellFormedTestPrime == 

   \A IdxSet \in 0..L'-1 : 

      WellFormedTest(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)

  BY DEF WellFormedTest

[Damien Doligez]

In your lemma, IdxSet is indeed under a quantifier and thus a constant, so your lemma is true.

But in the definition of WellFormedTest, IdxSet is a parameter, which is not necessarily a constant. When you pass a non-constant expression as argument to WellFormedTest, it is simply substituted for IdxSet. When you then apply the prime operator to it, it gets primed just like the rest of the body of WellFormedTest.

In other words, your lemma doesn't prove that IdxSet is a constant, it proves that, when you substitute IdxSet with a constant, then your equation is true.

It's important to understand that, unlike variables quantified with \A and \E, the parameter of an operator is not restricted to be a constant.