Publish bug

publish.tla

------------------------------ MODULE publish ------------------------------
EXTENDS TLC, Sequences, Integers


(* --algorithm publish
variable draft_course = {1,2,3,4,5}, published_course \in SUBSET {1,2,3,4}; 
 

process modify \in {1, 2} \* two possibilities
variables local_draft = draft_course;
begin Modify:
    while TRUE do
        either
            Create:
                with x = CHOOSE x \in ((1..200) \ draft_course):TRUE do
                    local_draft := {x} \union local_draft;
                    draft_course := {x} \union draft_course;
                end with;
        or
            Publish:
                with x \in local_draft do
                    published_course := {x} \union published_course;
                end with;
        or
            Delete:
                with  x \in local_draft do
                    local_draft := local_draft \ {x};
                    draft_course := draft_course \ {x};
                    published_course := published_course \ {x};
                end with;
        end either;
    end while;
end process;
end algorithm; *)


\* BEGIN TRANSLATION
VARIABLES draft_course, published_course, pc, local_draft

vars == << draft_course, published_course, pc, local_draft >>

ProcSet == ({1, 2})

Init == (* Global variables *)
        /\ draft_course = {1,2,3,4,5}
        /\ published_course = {1,2,3,4}
        (* Process modify *)
        /\ local_draft = [self \in {1, 2} |-> draft_course]
        /\ pc = [self \in ProcSet |-> "Modify"]

Modify(self) == /\ pc[self] = "Modify"
                /\ \/ /\ pc' = [pc EXCEPT ![self] = "Create"]
                   \/ /\ pc' = [pc EXCEPT ![self] = "Publish"]
                   \/ /\ pc' = [pc EXCEPT ![self] = "Delete"]
                /\ UNCHANGED << draft_course, published_course, local_draft >>

Create(self) == /\ pc[self] = "Create"
                /\ LET x == CHOOSE x \in ((1..200) \ draft_course):TRUE IN
                     /\ local_draft' = [local_draft EXCEPT ![self] = {x} \union local_draft[self]]
                     /\ draft_course' = ({x} \union draft_course)
                /\ pc' = [pc EXCEPT ![self] = "Modify"]
                /\ UNCHANGED published_course

Publish(self) == /\ pc[self] = "Publish"
                 /\ \E x \in local_draft[self]:
                      published_course' = ({x} \union published_course)
                 /\ pc' = [pc EXCEPT ![self] = "Modify"]
                 /\ UNCHANGED << draft_course, local_draft >>

Delete(self) == /\ pc[self] = "Delete"
                /\ \E x \in local_draft[self]:
                     /\ local_draft' = [local_draft EXCEPT ![self] = local_draft[self] \ {x}]
                     /\ draft_course' = draft_course \ {x}
                     /\ published_course' = published_course \ {x}
                /\ pc' = [pc EXCEPT ![self] = "Modify"]

modify(self) == Modify(self) \/ Create(self) \/ Publish(self)
                   \/ Delete(self)

Next == (\E self \in {1, 2}: modify(self))

Spec == Init /\ [][Next]_vars

\* END TRANSLATION

SubsetInvariant == published_course \subseteq draft_course


=============================================================================
\* Modification History
\* Last modified Fri May 18 12:32:28 EDT 2018 by adampalay
\* Created Fri May 18 11:11:14 EDT 2018 by adampalay