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

*From*: "Ugur Y. Yavuz" <uguryagmuryavuz@xxxxxxxxx>*Date*: Wed, 10 Jul 2024 10:00:51 -0700 (PDT)*References*: <AQHa0muwUW+l52aE+0GNlvoBTAtuwLHvWazA> <4214df27-e567-444c-91d1-ccce22998a79n@googlegroups.com> <c0587e72-002b-45c9-9b5b-c15ff269a298n@googlegroups.com> <MN0PR21MB372708FE12C5DCAE8360AA3CB8A42@MN0PR21MB3727.namprd21.prod.outlook.com> <dd24104b-74c8-4cbc-b4e8-813fd716b6d1n@googlegroups.com>

@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:

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

[] pc[p] = "L1" /\ l[p] \notin IdxSet -> FALSE

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

WellFormedTest(IdxSet)' = (\A p \in ProcSet :

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

[] pc'[p] = "L1" /\ l'[p] \notin IdxSet -> FALSE)

On Wednesday 10 July 2024 at 10:46:27 UTC-4 Ugur Y. Yavuz wrote:

> 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.On Wednesday 10 July 2024 at 00:13:07 UTC-4 Leslie Lamport wrote:It’s not a bug. The _expression_ WellFormed(full_indices)' has a double prime.

From:tla...@xxxxxxxxxxxxxxxx <tla...@xxxxxxxxxxxxxxxx>On Behalf OfAndrew Helwer

Sent:Tuesday, July 9, 2024 18:51

To:tlaplus <tla...@xxxxxxxxxxxxxxxx>

Subject:[tlaplus] Re: Parsing issues with prime operator in user-defined operators

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 -> FALSE

Note 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} -> 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.

--

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

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

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/bcf02596-0030-4fe3-9a72-a51bcfcc1556n%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Re: Parsing issues with prime operator in user-defined operators***From:*Damien Doligez

**Re: [tlaplus] Re: Parsing issues with prime operator in user-defined operators***From:*Damien Doligez

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

**[tlaplus] Re: Parsing issues with prime operator in user-defined operators***From:*Andrew Helwer

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

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

- Prev by Date:
**Re: [tlaplus] Re: Parsing issues with prime operator in user-defined operators** - Next by Date:
**Re: [tlaplus] Re: Parsing issues with prime operator in user-defined operators** - Previous by thread:
**Re: [tlaplus] Re: 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):