--------------------- MODULE mrwei ---------------------------

EXTENDS Integers

VARIABLES state, content, waker, mutWaker, mutContent, pollStep, promiseStep

ALL_STATES == { "IDLE", "SET", "SET_WAIT", "WAIT", "WAIT_REPLACE", "DRAIN", "WASTE" }

POSSIBLE_STATE == { "NotSet", "Set", "Taken", "InValid" }

ALL_POLL_STEPS == {  "Init", "RePoll", "ResumePollInit", "ResumeRePollReplace", "ResumeRePollSet", "ResumePollInitSet", "Finish", "ResumeDropFutureSet", "ResumeDropFutureWait" }
ALL_PROMISE_STEPS == { "Init", "ResumePromiseInit", "ResumePromiseWait", "DropPromise", "ResumeDropPromiseWait", "StopPromise" }

TypeInvarint == /\ state \in ALL_STATES
                /\ content \in POSSIBLE_STATE
                /\ waker \in POSSIBLE_STATE
                /\ mutWaker \in Nat
                /\ mutContent \in Nat

Init == /\ state = "IDLE"
        /\ content = "NotSet"
        /\ waker = "NotSet"
        /\ mutWaker = 0
        /\ mutContent = 0
        /\ pollStep = "Init"
        /\ promiseStep = "Init"

ReportWakerInvalid ==
    /\ waker' = "INVALID_STATE"
    /\ UNCHANGED <<state, content, mutContent, mutWaker, pollStep, promiseStep>>

ReportStateInvalid ==
    /\ state' = "INVALID_STATE"
    /\ UNCHANGED <<waker, content, mutContent, mutWaker, pollStep, promiseStep>>

ReportContentInvalid ==
    /\ content' = "INVALID_STATE"
    /\ UNCHANGED <<state, waker, mutContent, mutWaker, pollStep, promiseStep>>

AllUnchanged ==
    /\ UNCHANGED <<state, content, mutContent, waker, mutWaker, pollStep, promiseStep>>

PollInit == CASE state = "IDLE" ->
                IF waker = "NotSet" THEN
                    /\ mutWaker' = mutWaker + 1
                    /\ pollStep' = "ResumePollInit"
                    /\ UNCHANGED <<state, waker, content, mutContent, promiseStep>>
                ELSE ReportWakerInvalid
              [] OTHER -> ReportStateInvalid

ResumePollInit ==
    CASE state = "IDLE" ->
          IF waker = "NotSet" THEN
              /\ waker' = "Set"
              /\ UNCHANGED <<state, content, mutWaker, mutContent, pollStep, promiseStep>>
          ELSE IF waker = "Set" THEN 
              /\ mutWaker' = mutWaker - 1
              /\ state' = "WAIT"
              /\ pollStep = "RePoll"
              /\ UNCHANGED <<content, waker, mutContent, pollStep, promiseStep>>
          ELSE ReportWakerInvalid
      [] state = "SET" ->
          IF waker = "NotSet" THEN
              /\ mutContent' = mutContent + 1
              /\ pollStep' = "ResumePollInitSet"
              /\ UNCHANGED <<state, content, waker, mutWaker, promiseStep>>
          ELSE ReportWakerInvalid
      [] state = "WASTE" ->
           IF waker # "NotSet" THEN ReportWakerInvalid
           ELSE /\ pollStep' = "DropFuture"
                /\ UNCHANGED <<state, content, waker, mutContent, mutWaker, promiseStep>>
      [] OTHER -> ReportStateInvalid

ResumePollInitSet ==
    CASE state = "SET" ->
          IF waker = "NotSet" THEN
              /\ content' = "Taken"
              /\ waker' = "InValid"
              /\ UNCHANGED <<state, mutContent, mutWaker, pollStep, promiseStep>>
          ELSE IF waker = "InValid" THEN
              /\ mutContent' = mutContent - 1
              /\ mutWaker' = mutWaker - 1
              /\ state' = "DRAIN"
              /\ pollStep' = "Finish"
              /\ UNCHANGED <<content, waker, promiseStep>>
          ELSE ReportWakerInvalid
      [] OTHER -> ReportStateInvalid     

ResumeRePollReplace ==
    CASE state = "WAIT_REPLACE" ->
          IF waker = "Set" THEN
              /\ state' = "WAIT"
              /\ mutWaker' = mutWaker - 1
              /\ pollStep' = "RePoll"
              /\ UNCHANGED <<content, mutContent, waker, promiseStep>>
          ELSE ReportWakerInvalid
      [] state = "SET_WAIT" ->
          IF waker = "Set" THEN
              /\ waker' = "Invalid"
              /\ mutContent' = content + 1
              /\ UNCHANGED <<state, content, mutWaker, pollStep, promiseStep>>
          ELSE IF content # "Taken" THEN
              /\ content' = "Taken"
              /\ UNCHANGED <<state, waker, mutWaker, mutContent, pollStep, promiseStep>>
          ELSE IF /\ waker = "Invalid" /\ content = "Taken" THEN
              /\ mutWaker' = mutWaker - 1
              /\ mutContent' = mutContent - 1
              /\ pollStep' = "Finish"
              /\ state' = "DRAIN"
              /\ UNCHANGED <<waker, promiseStep>>
          ELSE ReportWakerInvalid
      [] OTHER -> ReportStateInvalid

ResumeRePollSet ==
    CASE state = "SET_WAIT" ->
          IF content = "Set" THEN
              /\ content' = "Taken"
              /\ UNCHANGED <<state, waker, mutContent, mutWaker, pollStep, promiseStep>>
          ELSE IF content = "Taken" THEN
              /\ mutContent' = mutContent - 1
              /\ state' = "DRAIN"
              /\ pollStep' = "Finish"
              /\ UNCHANGED <<content, waker, mutWaker, promiseStep>>
          ELSE ReportContentInvalid
      [] OTHER -> ReportStateInvalid

RePoll == CASE state = "WAIT" ->
              /\ state' = "WAIT_REPLACE"
              /\ pollStep' = "ResumeRePollReplace"
              /\ mutWaker' = mutWaker + 1
              /\ UNCHANGED <<content, waker, mutContent, pollStep, promiseStep>>
            [] state = "SET_WAIT" ->
                IF content = "Set" THEN
                    /\ mutContent' = mutContent + 1
                    /\ pollStep' = "ResumeRePollSet"
                    /\ UNCHANGED <<state, waker, content, mutWaker, promiseStep>>
                ELSE ReportContentInvalid
            [] state = "DRAIN" -> AllUnchanged
            [] OTHER -> ReportStateInvalid

PollFinish == IF state = "DRAINED" THEN AllUnchanged
              ELSE ReportStateInvalid

Poll == CASE pollStep = "Init" -> PollInit
          [] pollStep = "RePoll" -> RePoll
          [] pollStep = "ResumePollInit" -> ResumePollInit
          [] pollStep = "ResumeRePollReplace" -> ResumeRePollReplace
          [] pollStep = "ResumeRePollSet" -> ResumeRePollSet
          [] pollStep = "ResumePollInitSet" -> ResumePollInitSet
          [] pollStep = "Finish" -> PollFinish
          [] OTHER -> AllUnchanged

ResumeDropFutureSet ==
    IF content = "Set" THEN
        /\ content' = "InValid"
        /\ waker' = "InValid"
        /\ UNCHANGED <<state, mutContent, mutWaker, pollStep, promiseStep>>
    ELSE IF content = "InValid" THEN
        /\ mutContent' = mutContent - 1
        /\ mutWaker' = mutWaker - 1
        /\ pollStep' = "StopFuture"
        /\ state' = "WASTE"
        /\ UNCHANGED <<waker, content, promiseStep>>
    ELSE ReportContentInvalid

ResumeDropFutureWait ==
    IF waker = "Set" THEN
        /\ waker' = "InValid"
        /\ UNCHANGED <<state, content, mutContent, mutWaker, pollStep, promiseStep>>
    ELSE IF waker = "InValid" THEN
        /\ mutWaker' = mutWaker - 1
        /\ pollStep' = "StopFuture"
        /\ UNCHANGED <<state, content, mutContent, waker, promiseStep>>
    ELSE ReportWakerInvalid

DropFutureInit ==
    CASE state = "IDLE" ->
          /\ state' = "WASTE"
          /\ pollStep' = "StopFuture"
          /\ UNCHANGED <<content, waker, mutContent, mutWaker, promiseStep>>
      [] state = "SET" ->
          /\ mutContent' = mutContent + 1
          /\ mutWaker' = mutWaker + 1
          /\ pollStep' = "ResumeDropFutureSet"
          /\ UNCHANGED <<state, content, waker, promiseStep>>
      [] state = "SET_WAIT" ->
          /\ mutContent' = mutContent + 1
          /\ mutWaker' = mutWaker + 1
          /\ pollStep' = "ResumeDropFutureSet"
          /\ UNCHANGED <<state, content, waker, mutWaker, promiseStep>>
      [] state = "WAIT" ->
          /\ state' = "WASTE"
          /\ mutWaker' = mutWaker + 1
          /\ pollStep' = "ResumeDropFutureWait"
          /\ UNCHANGED <<content, waker, mutContent, promiseStep>>
      [] state = "WASTE" ->
          /\ mutWaker' = mutWaker + 1
          /\ pollStep' = "ResumeDropFutureWait"
          /\ UNCHANGED <<state, content, waker, mutContent, promiseStep>>
      [] state = "DRAIN" ->
          /\ pollStep' = "StopFuture"
          /\ UNCHANGED <<state, content, waker, mutContent, mutWaker, promiseStep>>
      [] OTHER -> ReportStateInvalid


DropFuture == CASE pollStep = "Init" -> DropFutureInit
                [] pollStep = "RePoll" -> DropFutureInit
                [] pollStep = "Finish" -> DropFutureInit
                [] pollStep = "ResumeDropFutureSet" -> ResumeDropFutureSet
                [] pollStep = "ResumeDropFutureWait" -> ResumeDropFutureWait
                [] OTHER -> AllUnchanged

ResumePromiseInit ==
    CASE state = "IDLE" ->
          IF content = "NotSet" THEN
              /\ content' = "Set"
              /\ mutContent' = mutContent - 1
              /\ UNCHANGED <<state, waker, mutWaker, pollStep, promiseStep>>
          ELSE IF content = "Set" THEN
              /\ state' = "SET"
              /\ promiseStep' = "DropPromise"
              /\ UNCHANGED <<waker, mutWaker, content, mutContent, pollStep>>
          ELSE ReportContentInvalid
      [] state = "WAIT" ->
          /\ promiseStep' = "ResumePromiseWait"
          /\ UNCHANGED <<state, content, mutContent, waker, mutWaker, pollStep>>
       [] OTHER -> ReportStateInvalid

ResumePromiseWait ==
    CASE state = "WAIT" ->
          IF content = "NotSet" THEN
              /\ content' = "Set"
              /\ mutWaker' = mutWaker + 1
              /\ mutContent' = mutContent - 1
              /\ UNCHANGED <<state, waker, pollStep, promiseStep>>
          ELSE IF content = "Set" THEN
              /\ state' = "SET_WAIT"
              /\ waker' = "Taken"
              /\ mutWaker' = mutWaker - 1
              /\ promiseStep' = "DropPromise"
              /\ UNCHANGED <<content, mutContent, pollStep>>
          ELSE ReportContentInvalid
      [] state = "WAIT_REPLACE" ->
          IF content = "NotSet" THEN
              /\ content' = "Set"
              /\ mutContent' = mutContent - 1
              /\ UNCHANGED <<state, waker, mutWaker, pollStep, promiseStep>>
          ELSE IF content = "Set" THEN
              /\ state' = "SET_WAIT"
              /\ promiseStep' = "DropPromise"
              /\ UNCHANGED <<content, mutContent, waker, mutWaker, pollStep>>
          ELSE ReportContentInvalid
       [] OTHER -> ReportStateInvalid

PromiseInit ==
    CASE state = "IDLE" ->
          /\ mutContent' = mutContent + 1
          /\ promiseStep' = "ResumePromiseInit"
          /\ UNCHANGED <<state, content, waker, mutWaker, pollStep>>
      [] state = "WAIT" ->
          /\ mutContent' = mutContent + 1
          /\ promiseStep' = "ResumePromiseWait"
          /\ UNCHANGED <<state, content, waker, mutWaker, pollStep>>
      [] state = "WASTE" ->
          /\ promiseStep' = "DropPromise"
          /\ UNCHANGED <<state, content, waker, mutContent, mutWaker, pollStep>>
      [] OTHER -> ReportStateInvalid

DropPromiseDirectly ==
    /\ state' = "WASTE"
    /\ promiseStep' = "StopPromise"
    /\ UNCHANGED <<content, waker, mutContent, mutWaker, pollStep>>

ResumeDropPromiseWait ==
    IF waker = "Set" THEN
        /\ waker' = "Taken"
        /\ UNCHANGED <<state, content, mutContent, mutWaker, pollStep, promiseStep>>
    ELSE IF waker = "Taken" THEN
        /\ mutWaker' = mutWaker - 1
        /\ promiseStep' = "StopPromise"
        /\ UNCHANGED <<state, content, mutContent, waker, pollStep>>
    ELSE ReportWakerInvalid

DropPromiseInit ==
    CASE state = "IDLE" -> DropPromiseDirectly
      [] state = "WAIT" ->
          /\ state' = "WASTE"
          /\ mutWaker' = mutWaker + 1
          /\ promiseStep' = "ResumeDropPromiseWait"
          /\ UNCHANGED <<content, waker, mutContent, pollStep>>
      [] state = "WAIT_REPLACE" -> DropPromiseDirectly
      [] state \in { "SET", "SET_WAIT", "DRAIN", "WASTE" } ->
          /\ promiseStep' = "StopPromise"
          /\ UNCHANGED <<state, content, mutContent, waker, mutWaker, pollStep>>
      [] OTHER -> ReportStateInvalid

DropPromise ==
    CASE promiseStep = "Init" -> DropPromiseInit
      [] promiseStep = "DropPromise" -> DropPromiseInit
      [] promiseStep = "ResumeDropPromiseWait" -> ResumeDropPromiseWait
      [] OTHER -> AllUnchanged

Promise ==
    CASE promiseStep = "Init" -> PromiseInit
      [] promiseStep = "ResumePromiseInit" -> ResumePromiseInit
      [] promiseStep = "ResumePromiseWait" -> ResumePromiseWait
      [] OTHER -> AllUnchanged

Next == \/ Poll
        \/ DropFuture
        \/ Promise
        \/ DropPromise

UnreachableState == /\ \/ state \notin { "SET", "SET_WAIT" }
                       \/ content # "NotSet"
                    /\ \/ state \notin { "WAIT", "WAIT_REPLACE" }
                       \/ waker = "Set"
                    /\ mutContent \in { 0, 1 }
                    /\ mutWaker \in { 0, 1 }

ResourceDrop ==
    \/ pollStep # "StopFuture"
    \/ promiseStep # "StopPromise"
    \/ /\ content \in {"InValid", "NotSet", "Taken"}
       /\ waker \in {"InValid", "NotSet", "Taken"}
       /\ state \in { "WASTE", "DRAIN" }
       /\ mutContent = 0
       /\ mutWaker = 0
===================================================================================================