------------------------------ MODULE ICenSet1 ------------------------------
(***************************************************************************)
(* This specification describes a modification of ICenSq1 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 = {}
          
InputSet == /\ inp = NotArt 
            /\ inp' \in Art \ old
            /\ aw' = aw \cup {inp'}
            /\ old' = old \cup {inp'}
            /\ disp' = disp
         
AckSet == /\ inp \in Art 
          /\ inp' = NotArt
          /\ UNCHANGED <<aw, disp, old>>

DispOrNotSet == \E w \in aw : 
                   /\ \/ disp' = <<w, 1-disp[2]>>
                      \/ disp' = disp
                   /\ aw' = aw \ {w}
                   /\ UNCHANGED <<inp, old>>
                  
           
NextSet1 == InputSet \/ AckSet \/ DispOrNotSet

ICenSet1 == InitSet /\ [][NextSet1]_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.     *)
(***************************************************************************)
Fairness1 == WF_v(AckSet \/ DispOrNotSet)

ICensSet1Live == ICenSet1 /\ Fairness1
-----------------------------------------------------------------------------
(***************************************************************************)
(* Adding the prophecy set variable p.                                     *)
(***************************************************************************)
CONSTANTS Yes, No
Pi == {Yes, No}
ASSUME /\ Yes # No
       /\ Pi \cap Art = {}

FcnPlus(f, w, d) == 
   [x \in {w} \cup DOMAIN f |-> IF x = w THEN d ELSE f[x]]

FcnMinus(f, w) == [x \in (DOMAIN f) \ {w} |-> f[x]]

VARIABLE p
v_p ==  <<inp, aw, disp, old, p>>

TypeOKSet_p == TypeOKSet /\ (p \in [aw -> Pi])

InitSet_p == InitSet /\ (p = << >>)
 
InputSet_p == InputSet /\ (\E i \in Pi : p' = FcnPlus(p, inp', i))  

AckSet_p == AckSet /\ (p'=p)

DorNSet(w, i) ==  /\ \/ (i = Yes) /\ (disp' = <<w, 1-disp[2]>>)
                     \/ (i = No)  /\ (disp' = disp)
                  /\ aw' = aw \ {w}
                  /\ UNCHANGED <<inp, old>>

DispOrNotSet_p ==\E w \in aw :
                     /\ DorNSet(w, p[w])
                     /\ p' = FcnMinus(p, w)

NextSet1_p == InputSet_p \/ AckSet_p \/ DispOrNotSet_p

\*ICenSet1_p == InitSet_p /\ [][NextSet1_p]_v_p

ICenSet1_p ==  InitSet_p /\ [][NextSet1_p]_v_p /\ Fairness1
-----------------------------------------------------------------------------
awBar == {w \in aw : p[w] = Yes}

IC2 == INSTANCE ICenSet2 WITH aw <- awBar

=============================================================================
\* Modification History
\* Last modified Fri Oct 18 14:41:31 CEST 2024 by lamport
\* Created Sat Oct 22 07:58:56 PDT 2022 by lamport
