------------------------------- MODULE ICen2 -------------------------------
(***************************************************************************)
(* The first part of this module defines the TLA+ representation of the    *)
(* abstract program ICen2 of Figure 7.4 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 and 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

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


(***************************************************************************)
(* We now define the 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.     *)
(***************************************************************************)
Fairness2 == WF_vars(Ack \/ Display)

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

(***************************************************************************)
(* To show that ICen2 => \EE aw : ICen1, comment out the following end of  *)
(* module line ===...===.                                                  *)
(***************************************************************************)
=============================================================================
(***************************************************************************)
(* 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>>

ICen2_sLive == ICen2_s /\ Fairness2

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

I == INSTANCE ICen1 WITH aw <- awBar


==============================================================================
\* Modification History
\* Last modified Wed Oct 16 15:12:01 CEST 2024 by lamport
\* Created Wed Nov 22 18:05:34 PST 2023 by lamport
