------------------------------- MODULE ICen2 -------------------------------
(***************************************************************************)
(* The first part of this module defines the TLA+ representation of the    *)
(* abstract program ICen2 of Figure 7.5 of the book "A Science of Computer *)
(* Programs" by Leslie Lamport.  The second part defines a program ICen2_s *)
(* by adding a prophecy variable s to ICen2 as in Section 7.3.2, and it    *)
(* asserts that ICen2_s implements ICen1 under a suitable refinement       *)
(* mapping.  For that purpose, it instantiates module ICen1 that defines   *)
(* program ICen1.  That second part is commented out (by ending the module *)
(* before it) when this module is instantiated by ICen1, which is done     *)
(* when ICen1 is the root module.                                          *)
(***************************************************************************)
EXTENDS Integers, Sequences

CONSTANT Art, NotArt

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

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}
        
InputOrNot == /\ (inp = NotArt) /\ (aw = << >>)
              /\ inp' \in Art
              /\ \/ aw' = <<inp'>>
                 \/ aw' = aw
              /\ disp' = disp
         
Ack   == /\ (inp \in Art) /\ (aw = << >>)
         /\ inp' = NotArt
         /\ UNCHANGED <<aw, disp>>
       
Display   == /\ aw # << >>
             /\ disp' = <<aw[1], 1-disp[2]>>
             /\ aw' = << >>
             /\ UNCHANGED inp
           
Next2 == InputOrNot \/ Ack \/ Display

(***************************************************************************)
(* Although not done in the book, we now define a fairness requirement for *)
(* the ICen2 program.  It is weak fairness of all the actions except the   *)
(* InputOrNot action, since we don't want to require that the artist keep  *)
(* submitting works of art.                                                *)
(***************************************************************************)
Fairness2 == WF_vars(Ack \/ Display)

ICen2 == Init /\ [][Next2]_vars /\ Fairness2

(***************************************************************************)
(* When ICen2 is the root module, comment out the following line that ends *)
(* the module at this point.                                               *)
(***************************************************************************)
\*=============================================================================
(***************************************************************************)
(* Adding a stuttering variable s to show ICen2 => \EE aw : ICen1          *)
(***************************************************************************)
VARIABLE s

Init_s == Init /\ (s = 0)

Ack_s == (s=0) /\ Ack /\ (s'=0)

exp == IF aw' = << >> THEN 1 ELSE 0 

InputOrNot_s == \/ (s = 0) /\ InputOrNot  /\ (s' = exp)
                \/ (s > 0) /\ (s' = s-1) /\ UNCHANGED vars                
         
Display_s == (s = 0) /\ Display /\ (s' = 0)

Next2_s == InputOrNot_s \/ Ack_s \/ Display_s

ICen2_s == Init_s /\ [][Next2_s]_<<vars,s>> /\ Fairness2

awBar == IF s = 0 THEN aw ELSE <<inp>>

I == INSTANCE ICen1 WITH aw <- awBar
==============================================================================
\* Modification History
\* Last modified Wed Oct 16 16:02:05 CEST 2024 by lamport
\* Created Wed Nov 22 18:05:34 PST 2023 by lamport
