[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Andrew Helwer <andrew.helwer@xxxxxxxxx>*Date*: Tue, 9 Jul 2024 18:51:06 -0700 (PDT)*References*: <4214df27-e567-444c-91d1-ccce22998a79n@googlegroups.com>

Is this an issue with SANY or the TLAPM parser?

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 :

CASEpc[p] = "L0" -> TRUE

[] pc[p] = "L1" /\ l[p] \in IdxSet -> TRUE

[] pc[p] = "L1" /\ l[p] \notin IdxSet -> FALSENote that we have:WellFormed(IdxSet)' =

\A p \in ProcSet :

CASEpc'[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 \inSUBSET0..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 \inSUBSET0..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>DEFINEfull_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 :

CASEpc'[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} -> FALSEwhich 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.

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+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/c0587e72-002b-45c9-9b5b-c15ff269a298n%40googlegroups.com.

**Follow-Ups**:**RE: [tlaplus] Re: Parsing issues with prime operator in user-defined operators***From:*'Leslie Lamport' via tlaplus

**References**:**[tlaplus] Parsing issues with prime operator in user-defined operators***From:*Ugur Y. Yavuz

- Prev by Date:
**RE: [tlaplus] Possible TLC soundness bug when checking temporal properties** - Next by Date:
**RE: [tlaplus] Re: Parsing issues with prime operator in user-defined operators** - Previous by thread:
**[tlaplus] Parsing issues with prime operator in user-defined operators** - Next by thread:
**RE: [tlaplus] Re: Parsing issues with prime operator in user-defined operators** - Index(es):