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

[tlaplus] Defining functions in TLAPS

I'm experimenting again with TLPAS in order to learn stuff, and I guess this is the open/closed world problem.

I was trying to see if it's possible to define predicate P as TRUE only for value 1 and 2 and FALSE implicitly for any other value. Of course, none of the options below worked. 
Is the any way to do this?

THEOREM TestFunction ==
        NEW S,
        NEW P \in [S -> BOOLEAN],
\*        \A s \in S : P[s] = IF s \in {1, 2} THEN TRUE ELSE FALSE
\*        P = (1 :> TRUE @@ 2 :> TRUE)
        P[1], P[2]
        P[3] => FALSE

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/c86392a7-d2d4-4b62-935b-265874627159n%40googlegroups.com.