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

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



If you want more suggestions, BOOLEAN = { TRUE, FALSE } is built-in so you don't need to define True and False as constants.

Isaac DeFrain


On Sat, Feb 13, 2021 at 11:59 AM Brian Beckman <bc.beckman@xxxxxxxxx> wrote:
yeah, tyvm :) 

On Saturday, February 13, 2021 at 10:58:27 AM UTC-8 isaacd...@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 DeFrain


On Sat, Feb 13, 2021 at 11:56 AM Brian Beckman <bc.be...@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+u...@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/067579ee-197a-4ea5-b6ab-6233502b6480n%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/CAM3xQxFVizu9G-tr8VkV63c8YGLe8LJxMwVY%3D%2BxzcVFH5X1i3Q%40mail.gmail.com.