------------------------------- MODULE ICen1 -------------------------------
(***************************************************************************)
(* The first part of this module defines the TLA+ representation of the    *)
(* abstract program ICen1 of Figure 7.4 of the book "A Science of Computer *)
(* Programs" by Leslie Lamport.  The second part defines a program ICen1_p *)
(* by adding a prophecy p variable to ICen1 as described in Section 7.4.1, *)
(* and it asserts that ICen1_p implements ICen2 under a suitable           *)
(* refinement mapping.  For that purpose, it instantiates module ICen2     *)
(* that defines program ICen2.  That second part is commented out (by      *)
(* ending the module before it) when this module is instantiated by ICen2, *)
(* which is done when ICen2 is the root module.                            *)
(*                                                                         *)
(* Proving that ICen1_p implements ICen2 under a refinement mapping shows  *)
(* that \EE aw : ICen1 implies \EE aw : ICen2.  To write that theorem in   *)
(* TLA+, we need to define a new module that declares the constants Art    *)
(* and NotArt and the variables inp and disp and instantiates modules      *)
(* ICen1 and ICen2 as follows:                                             *)
(*                                                                         *)
(*     I1(aw) == INSTANCE ICen1                                            *)
(*     I2(aw) == INSTANCE ICen2                                            *)
(*                                                                         *)
(* In that module, we can then write \EE aw : ICen1 as \EE aw :            *)
(* I1(a2)!ICen1 and can write ICen2 similarly.  However, since TLC and     *)
(* TLAPS can't handle the \EE operator, there is no practical reason to do *)
(* that.  As the book says in Section 7.1.1:                               *)
(*                                                                         *)
(*    \EE is of little use in practice.  The only role it plays is telling *)
(*    us that, when implementing the program, it doesn’t matter how the    *)
(*    internal variables are refined.  That can be stated just as well in  *)
(*    a comment.                                                           *)
(***************************************************************************)
EXTENDS Integers, Sequences

(***************************************************************************)
(* We declare Art and NotArt to be constants and assume that NotArt is not *)
(* an element of Art.  (We don't have to declare that Art is a set because *)
(* in ZF set theory, on which TLA+ is based, every value is a set.)        *)
(***************************************************************************)
CONSTANT Art, NotArt
ASSUME NotArt \notin Art

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

(***************************************************************************)
(* It's a good idea to define a type-correctness invariant after declaring *)
(* the variables to help the reader understand the definitions of the      *)
(* initial predicate and next-step predicate.                              *)
(***************************************************************************)
TypeOK == /\ inp \in Art \cup {NotArt}
          /\ disp \in Art \X {0,1}
          /\ aw \in Seq(Art)

Init ==   /\ inp = NotArt 
          /\ aw = << >>
          /\ disp \in Art \X {0,1}
        
Input == /\ (inp = NotArt) /\ (aw = << >>)
         /\ inp' \in Art
         /\ aw' = <<inp'>>
         /\ disp' = disp
         
       
DispOrNot == /\ aw # << >>
             /\ \/ disp' = <<aw[1], 1-disp[2]>>
                \/ disp' = disp
             /\ aw' = << >>
             /\ inp' = inp

Ack   == /\ (inp \in Art) /\ (aw = << >>)
         /\ inp' = NotArt
         /\ (aw' = aw) /\ (disp' = disp)
           
Next1 == Input \/ Ack \/ DispOrNot

(***************************************************************************)
(* Although not done in the book, we now define a fairness requirement for *)
(* the ICen1 program.  It is weak fairness of all the actions except the   *)
(* Input action, since we don't want to require that the artist keep       *)
(* submitting works of art.                                                *)
(***************************************************************************)
Fairness1 == WF_v(Ack \/ DispOrNot)
 
ICen1 == Init /\ [][Next1]_v /\ Fairness1
(***************************************************************************)
(* When ICen1 is the root module, comment out the following line that ends *)
(* the module at this point.                                               *)
(***************************************************************************)
============================================================================
-----------------------------------------------------------------------------
(***************************************************************************)
(* We now add the simple prophecy variable p to ICen1 as it is done in     *)
(* Section 7.4.1 of the book.  For simplicity, we use the strings "Yes"    *)
(* and "No" instead of the constants Yes and No used in the book.          *)
(***************************************************************************)
VARIABLE p
Pi == {"Yes", "No"}

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

TypeOK_p == TypeOK /\ (p\in Pi)

Init_p == Init /\ (p\in Pi)
 
Input_p == Input /\ \E i \in Pi : p' = i

Ack_p == Ack /\ (p'=p)

DorN(i) == /\ aw # << >>
               /\ \/ (i = "Yes") /\ (disp' = <<aw[1], 1-disp[2]>>)
                  \/ (i = "No") /\ (disp' = disp)
               /\ aw' = << >>
               /\ UNCHANGED inp

DispOrNot_p == DorN(p) /\ (p'\in Pi)

Next1_p == Input_p \/ Ack_p \/ DispOrNot_p

ICen1_p == Init_p /\ [][Next1_p]_v_p /\ Fairness1

\*ICen1Live_p == ICen1_p /\ Fairness1
-----------------------------------------------------------------------------
(***************************************************************************)
(* We now define I!ICen2 to be (ICen2 WITH aw <- awBar), where awBar is    *)
(* definedd in Section 7.4.1.                                              *)
(***************************************************************************)
awBar == IF (aw # << >>) /\ (p = "Yes") THEN aw ELSE << >> 

I == INSTANCE ICen2 WITH aw <- awBar

THEOREM ICen1_p => I!ICen2
=============================================================================
\* Modification History
\* Last modified Wed Oct 16 15:58:34 CEST 2024 by lamport
\* Created Fri Oct 21 06:36:45 PDT 2022 by lamport

=============================================================================
\* Modification History
\* Created Fri May 05 16:41:44 CEST 2023 by lamport
