Well I resolved my surprise and made some sense out of the following spec. It's probably stupidly over-engineered and horribly unidiomatic, but I'd be delighted to see critique! I'm working on a physical device that can actually tell the kinds of differences I'm exploring in this spec.
----------------------- MODULE checking_if_then_else -----------------------
(***************************************************************************)
(* *)
(* The purpose of this spec is to check whether TLA+'s built-in "IF A THEN *)
(* B ELSE C" construct is lenient or strict in a sense to be explained. *)
(* Consider this concrete example: *)
(* *)
(* IF ItsRaining THEN GroundIsWet ELSE BirdsSinging *)
(* *)
(* This could mean, informally: *)
(* *)
(* If (A) it's raining, then (B) the ground is wet and *)
(* if (~A) it's not raining, then (C) birds are singing. *)
(* *)
(* which means, more fully, a possibility we call "lenient," possibility *)
(* 1: *)
(* *)
(* If (A) it's raining, then (B) the ground is wet and (C or ~C) birds *)
(* might be singing (some birds might sing in the rain), and if (~A) *)
(* it's not raining, then (C) birds are singing and (B or ~B) the *)
(* ground might be wet (we could have on the lawn sprinkler, *)
(* for instance). *)
(* *)
(* Alternatively, the TLA+ built-in "IF A THEN B ELSE C" construct might *)
(* mean, instead, again informally, a possibility we call "strict," *)
(* possibility 2: *)
(* *)
(* If (A) it's raining, then (B) the ground is wet and (~C) birds *)
(* are not singing, and if (~A) it's not raining, then (C) birds are *)
(* singing and (~B) the ground is not wet. *)
(* *)
(* These two possibilities have different truth tables. *)
(* *)
(* A (raining) B (ground wet) C (birds sing) Poss 1 Poss 2 Diff *)
(* True True True True False * *)
(* True True False True True *)
(* True False True False False *)
(* True False False False False *)
(* False True True True False * *)
(* False True False False False *)
(* False False True True True *)
(* False False False False False *)
(* *)
(* If we include the built-in "IF A THEN B ELSE C" in our Init predicate *)
(* and in our Next action and if it's lenient, we should see four distinct *)
(* states reached in the model checker. If the built-in is strict, we *)
(* should see two distinct states. In the case that the built-in is *)
(* lenient, we can apply the "strict" interpretation and watch the *)
(* model-checker reduce the distinct states from four to two. That's what *)
(* happens, in fact. So we conclude that TLA+'s built-in "IF A THEN B *)
(* ELSE C" is lenient, analogously to the ways that mathematical *)
(* disjunction and implication are lenient. *)
(* *)
(* The fireworks are below. *)
(* *)
(***************************************************************************)
(* Here are the model variables: *)
VARIABLES ItsRaining, GroundIsWet, BirdsSinging
vars == <<ItsRaining, GroundIsWet, BirdsSinging>>
(* Each of our model Booleans is either TRUE or FALSE. *)
TypeOK ==
/\ (ItsRaining \in BOOLEAN)
/\ (GroundIsWet \in BOOLEAN)
/\ (BirdsSinging \in BOOLEAN)
(* Here is an operator that models our lenient possibility 1.
It makes no statement about birds singing when it's raining and no
statement about wetness of the ground when it's not raining. *)
LenientIfThenElse(a, b, c) ==
\/ a /\ b
\/ ~a /\ c
(* Here is an operator that models our strict possibility 2: if
it's raining, then birds aren't singing, and if it's not raining, then
the ground is not wet. *)
StrictIfThenElse(a, b, c) ==
\/ a /\ b /\ ~c
\/ ~a /\ ~b /\ c
(* Start off not raining, dry ground, and birds singing, a state
consistent with the built-in "IF A THEN B ELSE C" and with both
the lenient and strict hypotheses. With "Interpretation = TRUE"
in the Next action, and if the built-in is lenient, the model
checker will report four distinct states. *)
Init ==
/\ ItsRaining = FALSE
/\ GroundIsWet = FALSE
/\ BirdsSinging = TRUE
/\ IF ItsRaining THEN GroundIsWet ELSE BirdsSinging
(***************************************************************************)
(* The following "Next" action tests all eight possibilities for raining, *)
(* ground wet or not, and birds singing or not. To check whether the *)
(* built-in is lenient, alternately comment and uncomment the following *)
(* definitions for "Interpretation." Expect to see four distict states if *)
(* the built-in is lenient. Force the strict interpretation *)
(* and see the distinct states go to 2 or fewer. *)
(***************************************************************************)
\* Interpretation(a, b, c) == TRUE \* Exepct 8 distinct states
Interpretation(a, b, c) == LenientIfThenElse(a, b, c) \* Expect four
\* Interpretation(a, b, c) == StrictIfThenElse(a, b, c) \* Expect 2 or fewer
Next ==
\/ /\ ItsRaining' = ~ItsRaining
/\ Interpretation(ItsRaining', GroundIsWet, BirdsSinging)
/\ (UNCHANGED <<GroundIsWet, BirdsSinging>>)
\/ /\ GroundIsWet' = ~GroundIsWet
/\ Interpretation(ItsRaining, GroundIsWet', BirdsSinging)
/\ (UNCHANGED <<BirdsSinging, ItsRaining>>)
\/ /\ BirdsSinging' = ~BirdsSinging
/\ Interpretation(ItsRaining, GroundIsWet, BirdsSinging')
/\ (UNCHANGED <<ItsRaining, GroundIsWet>>)
Spec == Init /\ [][Next]_vars
-----------------------------------------------------------------------------
THEOREM Spec => []TypeOK
=============================================================================
\* Modification History
\* Last modified Sat Feb 13 14:19:20 PST 2021 by bcbeckman
\* Created Sat Feb 13 10:12:25 PST 2021 by bcbeckman
On Saturday, February 13, 2021 at 12:28:01 PM UTC-8 Brian Beckman wrote:
Nice! TY. I will have a surprising (to me) example soon, much shorter with these suggestions.
If you want more suggestions, BOOLEAN = { TRUE, FALSE } is built-in so you don't need to define True and False as constants.
yeah, tyvm :)
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>>))
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.