------------------------------ MODULE ICenSeq2 ------------------------------
(***************************************************************************)
(* This module defines the TLA+ representation of the abstract program     *)
(* ICenSeq2 of Figure 7.7 of the book "A Science of Concurrent Programs"   *)
(* by Leslie Lamport.  The module is instantiated by the root module       *)
(* ICenSeq1.                                                               *)
(***************************************************************************)
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}
        
InpOrNotSeq == /\ inp = NotArt
               /\ inp' \in Art
               /\ \/ aw' = Append(aw, inp')
                  \/ aw' = aw
               /\ disp' = disp
         
AckSeq == /\ inp \in Art 
          /\ inp' = NotArt
          /\ UNCHANGED <<aw, disp>>
       
DisplaySeq == /\ aw # << >>
              /\ disp' = <<aw[1], 1-disp[2]>>
              /\ aw' = Tail(aw)
              /\ UNCHANGED inp
           
NextSeq2 == InpOrNotSeq \/ AckSeq \/ DisplaySeq

(***************************************************************************)
(* Although not done in the book, we define a fairness requirement for the *)
(* ICenSeq2 program.  It is weak fairness of all the actions except the    *)
(* InpOrNotSeq action, since we don't want to require that the artist keep *)
(* submitting works of art.                                                *)
(***************************************************************************)
FairnessSeq2 == WF_vars(AckSeq \/ DisplaySeq)

ICenSeq2 == InitSeq /\ [][NextSeq2]_vars /\ FairnessSeq2
=============================================================================
\* Modification History
\* Last modified Fri Oct 18 15:26:15 CEST 2024 by lamport
\* Created Fri Oct 21 06:53:24 PDT 2022 by lamport
