------------------------------ MODULE ICenSet1 ------------------------------
(***************************************************************************)
(* The first part of this module defines the TLA+ representation of the    *)
(* abstract program ICenSet1 of Figure 7.8 of the book "A Science of       *)
(* Computer Programs" by Leslie Lamport.  The second part defines a        *)
(* program ICen1Set_p obtained by adding a prophecy set variable p to      *)
(* ICenSet1 as described in Section 7.4.3.2, and it asserts that           *)
(* ICen1Set_p implements ICenSet2 under a suitable refinement mapping.     *)
(* For that purpose, it instantiates module ICenSet2 that defines program  *)
(* ICenSet2.                                                               *)
(***************************************************************************)

EXTENDS Integers, Sequences

CONSTANT Art, NotArt

VARIABLES inp, aw, disp, old
v ==  <<inp, aw, disp, old>>

TypeOKSet == /\ inp \in Art \cup {NotArt}
             /\ disp \in Art \X {0,1}
             /\ aw \subseteq Art
             /\ old \subseteq Art

InitSet == /\ inp = NotArt
           /\ aw = {}
           /\ disp \in Art \X {0,1}
           /\ old = {}
          
InputSet == /\ inp = NotArt 
            /\ inp' \in Art \ old
            /\ aw' = aw \cup {inp'}
            /\ old' = old \cup {inp'}
            /\ disp' = disp
         
AckSet == /\ inp \in Art 
          /\ inp' = NotArt
          /\ UNCHANGED <<aw, disp, old>>

DispOrNotSet == \E w \in aw : 
                   /\ \/ disp' = <<w, 1-disp[2]>>
                      \/ disp' = disp
                   /\ aw' = aw \ {w}
                   /\ UNCHANGED <<inp, old>>
                  
           
NextSet1 == InputSet \/ AckSet \/ DispOrNotSet

ICenSet1 == InitSet /\ [][NextSet1]_v

(***************************************************************************)
(* Although not done in the book, we define a fairness requirement for the *)
(* ICenSet1 program.  It is weak fairness of all the actions except the    *)
(* InputSet action, since we don't want to require that the artist keep    *)
(* submitting works of art.                                                *)
(***************************************************************************)
Fairness1 == WF_v(AckSet \/ DispOrNotSet)

ICensSet1Live == ICenSet1 /\ Fairness1
-----------------------------------------------------------------------------
(***************************************************************************)
(* We now define the program ICenSet1_p obtained by adding a variable p    *)
(* that makes a set of predictions, as described in Section 7.4.3.2.       *)
(***************************************************************************)
CONSTANTS Yes, No
Pi == {Yes, No}
ASSUME /\ Yes # No
       /\ Pi \cap Art = {}

FcnPlus(f, w, d) == 
   [x \in {w} \cup DOMAIN f |-> IF x = w THEN d ELSE f[x]]

FcnMinus(f, w) == [x \in (DOMAIN f) \ {w} |-> f[x]]

VARIABLE p
v_p ==  <<inp, aw, disp, old, p>>

TypeOKSet_p == TypeOKSet /\ (p \in [aw -> Pi])

InitSet_p == InitSet /\ (p = << >>)
 
InputSet_p == InputSet /\ (\E i \in Pi : p' = FcnPlus(p, inp', i))  

AckSet_p == AckSet /\ (p'=p)

DorNSet(w, i) ==  /\ \/ (i = Yes) /\ (disp' = <<w, 1-disp[2]>>)
                     \/ (i = No)  /\ (disp' = disp)
                  /\ aw' = aw \ {w}
                  /\ UNCHANGED <<inp, old>>

DispOrNotSet_p ==\E w \in aw :
                     /\ DorNSet(w, p[w])
                     /\ p' = FcnMinus(p, w)

NextSet1_p == InputSet_p \/ AckSet_p \/ DispOrNotSet_p

ICenSet1_p ==  InitSet_p /\ [][NextSet1_p]_v_p /\ Fairness1
-----------------------------------------------------------------------------
(***************************************************************************)
(* The program ICenSet2 is defined in module ICenSet2.  We now define      *)
(* awBar as in the book and instantiate that module to define IC2!ICenSet2 *)
(* to be ICenSet2 WITH aw <- awBar, and we assert that it is implied by    *)
(* ICenSet1_p.                                                             *)
(***************************************************************************)
awBar == {w \in aw : p[w] = Yes}

IC2 == INSTANCE ICenSet2 WITH aw <- awBar
THEOREM ICenSet1 => IC2!ICenSet2
=============================================================================
\* Modification History
\* Last modified Fri Oct 18 15:16:28 CEST 2024 by lamport
\* Created Sat Oct 22 07:58:56 PDT 2022 by lamport
