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

*From*: Brian Beckman <bc.beckman@xxxxxxxxx>*Date*: Sat, 13 Feb 2021 10:58:16 -0800 (PST)*References*: <df6d03b4-d15c-480b-860c-8cf7d0cbc346n@googlegroups.com>

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

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

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

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

- Prev by Date:
**[tlaplus] Generating an 8-slot truth table?** - Next by Date:
**Re: [tlaplus] Generating an 8-slot truth table?** - Previous by thread:
**[tlaplus] Generating an 8-slot truth table?** - Next by thread:
**[tlaplus] Re: Generating an 8-slot truth table?** - Index(es):