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

*From*: Damien Doligez <plarwazir@xxxxxxxxx>*Date*: Wed, 10 Jul 2024 07:25:38 -0700 (PDT)*References*: <4214df27-e567-444c-91d1-ccce22998a79n@googlegroups.com>

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 :

CASEpc'[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 : [] 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)'

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/ad2ce5f1-b79a-4d09-a6d0-39847ffcb4c4n%40googlegroups.com.

**References**:**[tlaplus] 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:
**[tlaplus] Possible TLC soundness bug when checking temporal properties** - Index(es):