------------------------------ MODULE ICenSeq1 ------------------------------
(***************************************************************************)
(* This first part of this module defines the TLA+ representation of the   *)
(* abstract program ICenSeq1 of Figure 7.6 of the book "A Science of       *)
(* Computer Programs" by Leslie Lamport.  The second part defines a        *)
(* program ICen1Seq_p obtained by adding a prophecy prophecy sequence      *)
(* variable p to ICen1 as described in Section 7.4.3.1, and it asserts     *)
(* that ICen1Seq_p implements ICenSeq2 under a suitable refinement         *)
(* mapping.  For that purpose, it instantiates module ICen2 that defines   *)
(* program ICen2.                                                          *)
(***************************************************************************)

EXTENDS Integers, Sequences

CONSTANT Art, NotArt

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

TypeOKSeq == /\ inp \in Art \cup {NotArt}
             /\ disp \in Art \X {0,1}
             /\ aw \in Seq(Art)

InitSeq == /\ inp = NotArt
           /\ aw = << >>
           /\ disp \in Art \X {0,1}
        
InputSeq == /\ inp = NotArt 
            /\ inp' \in Art
            /\ aw' = Append(aw, inp')
            /\ disp' = disp
         
AckSeq == /\ inp \in Art 
          /\ inp' = NotArt
          /\ UNCHANGED <<aw, disp>>
       
DispOrNotSeq == /\ aw # << >>
                /\ \/ disp' = <<aw[1], 1-disp[2]>>
                   \/ disp' = disp
                /\ aw' = Tail(aw)
                /\ UNCHANGED inp
           
NextSeq1 == InputSeq \/ AckSeq \/ DispOrNotSeq

(***************************************************************************)
(* Although not done in the book, we define a fairness requirement for the *)
(* ICensor1 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_vars(AckSeq \/ DispOrNotSeq)

ICensSeq1 ==  InitSeq /\ [][NextSeq1]_vars /\ Fairness1
-----------------------------------------------------------------------------
(***************************************************************************)
(* We now define the program ICen1Seq_p of Figure 7.7.                     *)
(***************************************************************************)
CONSTANTS Yes, No
Pi == {Yes, No}
ASSUME Yes # No

DorNSeq(i) == /\ aw # << >>
              /\ \/ (i = Yes) /\ (disp' = <<aw[1], 1-disp[2]>>)
                 \/ (i = No)  /\ (disp' = disp) 
              /\ aw' = Tail(aw)
              /\ UNCHANGED inp
           
VARIABLE p
vars_p ==  <<inp, aw, disp, p>>

TypeOKSeq_p == TypeOKSeq /\ (p \in Seq(Pi))

InitSeq_p == InitSeq /\ (p = << >>)
 
InputSeq_p == InputSeq /\ \E i \in Pi : p' = Append(p, i)

AckSeq_p == AckSeq /\ (p'=p)

DispOrNotSeq_p == DorNSeq(p[1]) /\ (p' = Tail(p))

NextSeq1_p == InputSeq_p \/ AckSeq_p \/ DispOrNotSeq_p

ICenSeq1_p ==  InitSeq_p /\ [][NextSeq1_p]_vars_p /\ Fairness1
-----------------------------------------------------------------------------
(***************************************************************************)
(* We now define the mapping OnlyYes and state predicate awBar of Section  *)
(* 7.4.3.2 of the book.                                                    *)
(***************************************************************************)
RECURSIVE OnlyYes(_,_)
OnlyYes(wsq, ysq) ==
   IF wsq = << >> THEN << >>
                  ELSE (IF Head(ysq) = Yes THEN <<Head(wsq)>>
                                                ELSE << >> 
                       ) \o OnlyYes(Tail(wsq), Tail(ysq))
                        
awBar == OnlyYes(aw, p)

(***************************************************************************)
(* We now assert the theorem (7.16).                                       *)
(***************************************************************************)
IC2 == INSTANCE ICenSeq2 WITH aw <- awBar
THEOREM ICenSeq1_p => IC2!ICenSeq2
=============================================================================
\* Modification History
\* Last modified Thu Oct 17 15:37:48 CEST 2024 by lamport
\* Created Fri Oct 21 06:36:45 PDT 2022 by lamport
