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

[Damien Doligez <plarwazir@xxxxxxxxx>]

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)'

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