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

*From*: Brian Beckman <bc.beckman@xxxxxxxxx>*Date*: Sat, 13 Feb 2021 10:56:07 -0800 (PST)

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

\* Last modified Sat Feb 13 10:46:31 PST 2021 by bcbeckman

\* Created Sat Feb 13 10:12:25 PST 2021 by bcbeckman

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

\* 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/df6d03b4-d15c-480b-860c-8cf7d0cbc346n%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Generating an 8-slot truth table?***From:*Isaac DeFrain

**[tlaplus] Re: Generating an 8-slot truth table?***From:*Brian Beckman

- Prev by Date:
**Re: [tlaplus] Lecture 9, part 1, Alternating-Bit Protocol** - Next by Date:
**[tlaplus] Re: Generating an 8-slot truth table?** - Previous by thread:
**[tlaplus] Re: Question on Video 8a** - Next by thread:
**[tlaplus] Re: Generating an 8-slot truth table?** - Index(es):