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

[tlaplus] Re: Generating an 8-slot truth table?

I got it to work by changing UNCHANGED {B, C} to UNCHANGED <<B,C>> etc.

On Saturday, February 13, 2021 at 10:56:08 AM UTC-8 Brian Beckman wrote:
I'm trying to write a spec that will be true in any behavior with A \in {True, False}, B \in {True, False}, and C \in {True, False}. My attempt is pasted below. TLC tells me right away that B is either undefined or not an operator (I don't know how to copy-paste from the "TLC errors" pane, but it points to the first line in my Next. In the TLC Model Overview, I tried setting True <- "True" and False <- "False", and I also tried "Model Variables". The module parses well. Not sure what I did wrong, here. Looks a lot like the Hour-Clock spec from the book to me. Perhaps I should try it with 0, 1 from the Naturals?

----------------------- MODULE checking_if_then_else -----------------------

vars == <<A, B, C>>

Flip(bool) == IF (bool = True) THEN False ELSE True

TypeOK ==
    /\ (A \in {True, False})
    /\ (B \in {True, False})
    /\ (C \in {True, False})

Init ==
    /\ (A = False)
    /\ (B = False)
    /\ (C = False)
Next ==
    \/ ((A' = Flip(A)) /\ (UNCHANGED {B, C}))
    \/ ((B' = Flip(B)) /\ (UNCHANGED {C, A}))
    \/ ((C' = Flip(C)) /\ (UNCHANGED {A, B}))
Spec == Init /\ [][Next]_vars
THEOREM Spec => []TypeOK
\* Modification History
\* Last modified Sat Feb 13 10:46:31 PST 2021 by bcbeckman
\* Created Sat Feb 13 10:12:25 PST 2021 by bcbeckman

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/3620d34f-5666-48fa-aca2-a198d42630b5n%40googlegroups.com.