In this final version, I promoted the check to a THEOREM. It's perhaps more idiomatic.
----------------------- 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 *)
(* *)
(* In ordinary speech, this ambiguous, on its face. It could mean, *)
(* informally, in 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 or not; if (~A) it's *)
(* not raining, then (C) birds are singing and (B or ~B) *)
(* the ground might be wet or not. *)
(* *)
(* Alternatively, it might mean, instead, again informally, in a *)
(* possibility we call "strict," possibility 2: *)
(* *)
(* If (A) it's raining, then (B) the ground is wet and (~C) birds *)
(* are not singing; 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 *)
(* *)
(* One way to check is to let TLC run over all the possible states and to *)
(* print the values of two expressions: "built-in equals lenient" and *)
(* "built-in equals strict." If we ever see a FALSE value for built-in *)
(* equals lenient, then we know the built-in is strict, or vice versa. If *)
(* it is not the case that one of the two expressions is always TRUE, then *)
(* we have a bug in the spec. *)
(* *)
(* The fireworks are below. *)
(* *)
(***************************************************************************)
EXTENDS TLC \* to get "PrintT"
(* Here are the model variables: *)
VARIABLES ItsRaining, GroundIsWet, BirdsSinging
vars == <<ItsRaining, GroundIsWet, BirdsSinging>>
(* Each model Boolean 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 the ground is wet and birds aren't singing;
if it's not raining, then the ground is not wet and birs are
singing. *)
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. *)
Init ==
/\ ItsRaining = FALSE
/\ GroundIsWet = FALSE
/\ BirdsSinging = TRUE
/\ IF ItsRaining THEN GroundIsWet ELSE BirdsSinging
(***************************************************************************)
(* Run TLC. The following produces all TRUE for "lenient," and two FALSE *)
(* cases for our "strict," proving that TLA+'s IF A THEN B ELSE B is *)
(* always equal to our "lenient" and sometimes not equal to our "strict." *)
(***************************************************************************)
Report(a, b, c) == LET ite == IF a THEN b ELSE c
IN PrintT(<<"lenient", ite = LenientIfThenElse(a, b, c),
"strict ", ite = StrictIfThenElse(a, b, c) >>)
Next ==
Report(ItsRaining, GroundIsWet, BirdsSinging) /\
\/ /\ ItsRaining' = ~ItsRaining
/\ (UNCHANGED <<GroundIsWet, BirdsSinging>>)
\/ /\ GroundIsWet' = ~GroundIsWet
/\ (UNCHANGED <<BirdsSinging, ItsRaining>>)
\/ /\ BirdsSinging' = ~BirdsSinging
/\ (UNCHANGED <<ItsRaining, GroundIsWet>>)
Spec == Init /\ [][Next]_vars
Echo(v) == PrintT(v) /\ v
-----------------------------------------------------------------------------
(* Let's make a theorem for TLC to check. Include "BuiltInIsLenient" in the
Invariants section of the Model Overview. *)
BuiltInIsLenient ==
(* It's important to parenthesize the whole IF because, if you don't,
TLC will read it as ... ELSE (BirdsSinging = Lenient(...)) *)
((IF ItsRaining THEN GroundIsWet ELSE BirdsSinging) =
LenientIfThenElse(ItsRaining, GroundIsWet, BirdsSinging))
THEOREM Spec => []BuiltInIsLenient
-----------------------------------------------------------------------------
(* Here is the customary type-safety theorem. There is one of these in every
spec *)
THEOREM Spec => []TypeOK
=============================================================================
\* Modification History
\* Last modified Sun Feb 14 07:04:40 PST 2021 by bcbeckman
\* Created Sat Feb 13 10:12:25 PST 2021 by bcbeckman