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

*From*: Isaac DeFrain <isaacdefrain@xxxxxxxxx>*Date*: Sat, 13 Feb 2021 11:59:36 -0700*References*: <df6d03b4-d15c-480b-860c-8cf7d0cbc346n@googlegroups.com> <CAM3xQxGaRG9b08j+=yX4sxF51V31jCN-k3zHHyCEPAVYGoYkuw@mail.gmail.com>

Also, you can simplify Flip to:

Flip(bool) == ~bool

Isaac DeFrain

On Sat, Feb 13, 2021 at 11:58 AM Isaac DeFrain <isaacdefrain@xxxxxxxxx> wrote:

Hey Brian,Try changing your Next action to:Next ==

\/ ((A' = Flip(A)) /\ (UNCHANGED <<B, C>>))

\/ ((B' = Flip(B)) /\ (UNCHANGED <<C, A>>))

\/ ((C' = Flip(C)) /\ (UNCHANGED <<A, B>>))Isaac DeFrainOn Sat, Feb 13, 2021 at 11:56 AM Brian Beckman <bc.beckman@xxxxxxxxx> 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/df6d03b4-d15c-480b-860c-8cf7d0cbc346n%40googlegroups.com.

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/CAM3xQxGU10tfaBmXNUGhpvqjKFf122vEy8WR6SCtApvZ9VQoFA%40mail.gmail.com.

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

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

- Prev by Date:
**Re: [tlaplus] Generating an 8-slot truth table?** - Next by Date:
**Re: [tlaplus] Generating an 8-slot truth table?** - Previous by thread:
**Re: [tlaplus] Generating an 8-slot truth table?** - Next by thread:
**[tlaplus] Seeking clarification of "continuously enabled" in weak fairness (video 9a)** - Index(es):