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

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



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


On Saturday, February 13, 2021 at 2:21:34 PM UTC-8 Brian Beckman wrote:
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.

On Saturday, February 13, 2021 at 11:01:40 AM UTC-8 isaacd...@xxxxxxxxx wrote:
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.be...@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+u...@xxxxxxxxxxxxxxxx.

--
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/eac79e63-9edb-43af-afd1-0918eaacb58bn%40googlegroups.com.