# [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 -----------------------
CONSTANTS True, False

VARIABLES A, B, C
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