------------------------------ MODULE ICenSet2 ------------------------------
(***************************************************************************)
(* This specification describes a modification of ICenSq2 in which the     *)
(* censor maintains a set aw rather than a sequence of pictures, so        *)
(* pictures can be displayed in any order.  For simplicity, we disallow    *)
(* the artist from submitting the same painting twice by adding a variable *)
(* `old' that is the set of pictures the artist has already submitted.     *)
(***************************************************************************)
EXTENDS Integers, Sequences

CONSTANT Art, NotArt

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

TypeOKSet == /\ inp \in Art \cup {NotArt}
             /\ disp \in Art \X {0,1}
             /\ aw \subseteq Art
             /\ old \subseteq Art

InitSet == /\ inp = NotArt
           /\ aw = {}
           /\ disp \in Art \X {0,1}
           /\ old = {}
          
InpOrNotSet == /\ inp = NotArt 
               /\ inp' \in Art \ old
               /\ \/ aw' = aw \cup {inp'}
                  \/ aw' = aw
               /\ old' = old \cup {inp'}
               /\ disp' = disp
         
AckSet == /\ inp \in Art 
          /\ inp' = NotArt
          /\ UNCHANGED <<aw, disp, old>>
       
DisplaySet == \E w \in aw :
                /\ disp' = <<w, 1-disp[2]>>
                /\ aw' = aw \ {w}
                /\ UNCHANGED <<inp, old>>
           
NextSet2 == InpOrNotSet \/ AckSet \/ DisplaySet

\*ICenSet2 == InitSet /\ [][NextSet2]_v

(***************************************************************************)
(* 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_v(AckSet \/ DisplaySet)

ICenSet2 ==  InitSet /\ [][NextSet2]_v /\ Fairness2
=============================================================================
\* Modification History
\* Last modified Fri Oct 18 14:40:12 CEST 2024 by lamport
\* Created Sat Oct 22 07:58:56 PDT 2022 by lamport


=============================================================================
\* Modification History
\* Created Sat Oct 22 08:15:26 PDT 2022 by lamport
