---- MODULE ProjectDelivery ----
EXTENDS FiniteSets, Naturals

CONSTANTS Deliveries, Templates, Identities, Revisions, Others, InitialTemplateRef, InitialMode

Continuous == "Continuous"
Point == "Point"
Modes == {Continuous, Point}

Absent == "Absent"
Queued == "Queued"
Running == "Running"
Terminal == "Terminal"
Collected == "Collected"

\* Retry successors use fresh identities without consuming a source identity again.
Attempts == Deliveries \X Modes \X Identities
Slots == Attempts \cup Others
Phases == {Absent, Queued, Running, Terminal, Collected}

VARIABLES mode, templateRef, eligible, persisted, recorded, phase, attemptTemplate
VARIABLES wantedRev, templateRev, settled, attemptRev, availableRev
VARIABLES prepared, publishRev

vars == <<mode, templateRef, eligible, persisted, recorded, phase, attemptTemplate,
          wantedRev, templateRev, settled, attemptRev, availableRev, prepared, publishRev>>

ASSUME /\ Deliveries /= {}
       /\ Templates /= {}
       /\ Identities /= {}
       /\ Revisions /= {}
       /\ Attempts \cap Others = {}
       /\ InitialTemplateRef \in [Deliveries -> Templates]
       /\ InitialMode \in [Deliveries -> Modes]

DeliveryOf(attempt) == attempt[1]
ModeOf(attempt) == attempt[2]

RetryPairs ==
    {pair \in Attempts \X Attempts :
        /\ pair[1] /= pair[2]
        /\ DeliveryOf(pair[1]) = DeliveryOf(pair[2])
        /\ ModeOf(pair[1]) = ModeOf(pair[2])}

SelectedAttempt(delivery) ==
    <<delivery, mode[delivery], eligible[delivery][mode[delivery]]>>

RunningFor(template) ==
    {attempt \in Slots :
        /\ phase[attempt] = Running
        /\ attemptTemplate[attempt] = {template}}

ActiveFor(template) ==
    {attempt \in Slots :
        /\ phase[attempt] \in {Queued, Running}
        /\ attemptTemplate[attempt] = {template}}

TypeOK ==
    /\ mode \in [Deliveries -> Modes]
    /\ templateRef \in [Deliveries -> Templates]
    /\ eligible \in [Deliveries -> [Modes -> Identities]]
    /\ persisted \in SUBSET Attempts
    /\ recorded \in [Deliveries -> [Modes -> SUBSET Attempts]]
    /\ \A delivery \in Deliveries, sourceMode \in Modes :
        /\ Cardinality(recorded[delivery][sourceMode]) <= 1
        /\ \A attempt \in recorded[delivery][sourceMode] :
            /\ DeliveryOf(attempt) = delivery
            /\ ModeOf(attempt) = sourceMode
            /\ attempt \in persisted
    /\ phase \in [Slots -> Phases]
    /\ availableRev \in [Templates -> SUBSET Revisions]
    /\ wantedRev \in [Templates -> Revisions]
    /\ templateRev \in [Templates -> Revisions]
    /\ settled \in [Templates -> BOOLEAN]
    /\ attemptRev \in [Slots -> SUBSET Revisions]
    /\ attemptTemplate \in [Slots -> SUBSET Templates]
    /\ prepared \in [Slots -> SUBSET (Templates \X Revisions)]
    /\ publishRev \in [Templates -> SUBSET Revisions]
    /\ \A template \in Templates : Cardinality(publishRev[template]) <= 1
    /\ \A attempt \in Slots :
        /\ Cardinality(prepared[attempt]) <= 1
        /\ (phase[attempt] = Absent) = (attemptTemplate[attempt] = {})
        /\ phase[attempt] /= Absent => Cardinality(attemptTemplate[attempt]) = 1
        /\ (phase[attempt] = Absent) = (attemptRev[attempt] = {})
        /\ phase[attempt] /= Absent => Cardinality(attemptRev[attempt]) = 1

Init ==
    /\ mode = InitialMode
    /\ templateRef = InitialTemplateRef
    /\ eligible =
        [delivery \in Deliveries |->
            [sourceMode \in Modes |-> CHOOSE identity \in Identities : TRUE]]
    /\ persisted = {}
    /\ recorded =
        [delivery \in Deliveries |-> [sourceMode \in Modes |-> {}]]
    /\ phase = [attempt \in Slots |-> Absent]
    /\ attemptTemplate = [attempt \in Slots |-> {}]
    /\ templateRev = [template \in Templates |-> CHOOSE revision \in Revisions : TRUE]
    /\ availableRev = [template \in Templates |-> {templateRev[template]}]
    /\ wantedRev = templateRev
    /\ settled = [template \in Templates |-> TRUE]
    /\ attemptRev = [attempt \in Slots |-> {}]
    /\ prepared = [attempt \in Slots |-> {}]
    /\ publishRev = [template \in Templates |-> {}]

ChangeEligibility(delivery, sourceMode, identity) ==
    /\ identity /= eligible[delivery][sourceMode]
    /\ eligible' =
        [eligible EXCEPT ![delivery][sourceMode] = identity]
    /\ UNCHANGED <<mode, templateRef, persisted, recorded, phase, attemptTemplate,
                   wantedRev, templateRev, settled, attemptRev, availableRev, prepared, publishRev>>

ChangeMode(delivery, sourceMode) ==
    /\ sourceMode /= mode[delivery]
    /\ mode' = [mode EXCEPT ![delivery] = sourceMode]
    /\ UNCHANGED <<templateRef, eligible, persisted, recorded, phase, attemptTemplate,
                   wantedRev, templateRev, settled, attemptRev, availableRev, prepared, publishRev>>

ChangeTemplateRef(delivery, template) ==
    /\ template /= templateRef[delivery]
    /\ templateRef' = [templateRef EXCEPT ![delivery] = template]
    /\ UNCHANGED <<mode, eligible, persisted, recorded, phase, attemptTemplate,
                   wantedRev, templateRev, settled, attemptRev, availableRev, prepared, publishRev>>

CreationEnabled(delivery) ==
    LET attempt == SelectedAttempt(delivery)
    IN  /\ recorded[delivery][mode[delivery]] = {}
        /\ attempt \notin persisted
        /\ phase[attempt] \in {Absent, Collected}
        /\ prepared[attempt] = {}
        /\ wantedRev[templateRef[delivery]] = templateRev[templateRef[delivery]]
        /\ settled[templateRef[delivery]]

Prepare(delivery) ==
    LET attempt == SelectedAttempt(delivery)
        template == templateRef[delivery]
    IN  /\ CreationEnabled(delivery)
        /\ prepared' =
            [prepared EXCEPT ![attempt] = {<<template, templateRev[template]>>}]
        /\ UNCHANGED <<mode, templateRef, eligible, persisted, recorded, phase,
                       attemptTemplate, wantedRev, templateRev, settled,
                       attemptRev, availableRev, publishRev>>

PrepareRetry(delivery, prior, attempt) ==
    LET template == templateRef[delivery]
    IN  /\ prior \in Attempts
        /\ attempt \in Attempts
        /\ DeliveryOf(prior) = delivery
        /\ DeliveryOf(attempt) = delivery
        /\ ModeOf(prior) = ModeOf(attempt)
        /\ prior \in persisted
        /\ phase[prior] \in {Terminal, Collected}
        /\ attempt \notin persisted
        /\ phase[attempt] \in {Absent, Collected}
        /\ prepared[attempt] = {}
        /\ \A sourceMode \in Modes : recorded[delivery][sourceMode] = {}
        /\ wantedRev[template] = templateRev[template]
        /\ settled[template]
        /\ prepared' =
            [prepared EXCEPT ![attempt] = {<<template, templateRev[template]>>}]
        /\ UNCHANGED <<mode, templateRef, eligible, persisted, recorded, phase,
                       attemptTemplate, wantedRev, templateRev, settled,
                       attemptRev, availableRev, publishRev>>

\* An API call can finish after a later observation without rereading admission gates.
Create(attempt) ==
    LET binding == CHOOSE value \in prepared[attempt] : TRUE
    IN  /\ attempt \in Slots
        /\ prepared[attempt] /= {}
        /\ IF attempt \in Attempts
              THEN /\ phase[attempt] \in {Absent, Collected}
                   /\ attempt \notin persisted
              ELSE phase[attempt] \in {Absent, Terminal, Collected}
        /\ phase' = [phase EXCEPT ![attempt] = Queued]
        /\ attemptTemplate' = [attemptTemplate EXCEPT ![attempt] = {binding[1]}]
        /\ attemptRev' = [attemptRev EXCEPT ![attempt] = {binding[2]}]
        /\ prepared' = [prepared EXCEPT ![attempt] = {}]
        /\ UNCHANGED <<mode, templateRef, eligible, persisted, recorded,
                       wantedRev, templateRev, settled, availableRev, publishRev>>

Start(attempt) ==
    /\ attempt \in Slots
    /\ phase[attempt] = Queued
    /\ \A template \in attemptTemplate[attempt] : RunningFor(template) = {}
    /\ phase' = [phase EXCEPT ![attempt] = Running]
    /\ UNCHANGED <<mode, templateRef, eligible, persisted, recorded, attemptTemplate,
                   wantedRev, templateRev, settled, attemptRev, availableRev, prepared, publishRev>>

Persist(delivery, attempt) ==
    /\ attempt \in Attempts
    /\ DeliveryOf(attempt) = delivery
    /\ attempt \notin persisted
    /\ phase[attempt] /= Absent
    /\ recorded[delivery][ModeOf(attempt)] = {}
    /\ persisted' = persisted \cup {attempt}
    /\ recorded' =
        [recorded EXCEPT ![delivery][ModeOf(attempt)] = {attempt}]
    /\ UNCHANGED <<mode, templateRef, eligible, phase, attemptTemplate,
                   wantedRev, templateRev, settled, attemptRev, availableRev, prepared, publishRev>>

Complete(attempt) ==
    /\ attempt \in Slots
    /\ phase[attempt] = Running
    /\ phase' = [phase EXCEPT ![attempt] = Terminal]
    /\ UNCHANGED <<mode, templateRef, eligible, persisted, recorded, attemptTemplate,
                   wantedRev, templateRev, settled, attemptRev, availableRev, prepared, publishRev>>

Reject(attempt) ==
    /\ attempt \in Slots
    /\ phase[attempt] = Queued
    /\ phase' = [phase EXCEPT ![attempt] = Terminal]
    /\ UNCHANGED <<mode, templateRef, eligible, persisted, recorded, attemptTemplate,
                   wantedRev, templateRev, settled, attemptRev, availableRev, prepared, publishRev>>

Release(delivery, sourceMode) ==
    /\ recorded[delivery][sourceMode] /= {}
    /\ \A attempt \in recorded[delivery][sourceMode] :
        phase[attempt] \in {Terminal, Collected}
    /\ recorded' = [recorded EXCEPT ![delivery][sourceMode] = {}]
    /\ UNCHANGED <<mode, templateRef, eligible, persisted, phase, attemptTemplate,
                   wantedRev, templateRev, settled, attemptRev, availableRev, prepared, publishRev>>

Collect(attempt) ==
    /\ attempt \in Attempts
    /\ phase[attempt] = Terminal
    /\ attempt \in persisted
    /\ phase' = [phase EXCEPT ![attempt] = Collected]
    /\ UNCHANGED <<mode, templateRef, eligible, persisted, recorded, attemptTemplate,
                   wantedRev, templateRev, settled, attemptRev, availableRev, prepared, publishRev>>

\* Other slots represent fresh workflow executions and can be reused after completion.
PrepareOther(attempt, template) ==
    /\ attempt \in Others
    /\ phase[attempt] \in {Absent, Terminal, Collected}
    /\ prepared[attempt] = {}
    /\ wantedRev[template] = templateRev[template]
    /\ settled[template]
    /\ prepared' = [prepared EXCEPT ![attempt] = {<<template, templateRev[template]>>}]
    /\ UNCHANGED <<mode, templateRef, eligible, persisted, recorded, phase,
                   attemptTemplate, wantedRev, templateRev, settled,
                   attemptRev, availableRev, publishRev>>

\* Requests record observed bundles; writes preceding observation leave wantedRev unchanged.
RequestTemplate(template, revision) ==
    /\ revision /= wantedRev[template]
    /\ wantedRev' = [wantedRev EXCEPT ![template] = revision]
    /\ settled' = [settled EXCEPT ![template] = FALSE]
    /\ publishRev' = [publishRev EXCEPT ![template] = {}]
    /\ UNCHANGED <<mode, templateRef, eligible, persisted, recorded, phase,
                   attemptTemplate, templateRev, attemptRev, availableRev, prepared>>

\* Settle abstracts expiration of the configured quiet interval after the latest change.
Settle(template) ==
    /\ ~settled[template]
    /\ settled' = [settled EXCEPT ![template] = TRUE]
    /\ UNCHANGED <<mode, templateRef, eligible, persisted, recorded, phase,
                   attemptTemplate, wantedRev, templateRev, attemptRev, availableRev, prepared, publishRev>>

PreparePublish(template) ==
    /\ wantedRev[template] /= templateRev[template]
    /\ settled[template]
    /\ ActiveFor(template) = {}
    /\ publishRev[template] = {}
    /\ publishRev' = [publishRev EXCEPT ![template] = {wantedRev[template]}]
    /\ UNCHANGED <<mode, templateRef, eligible, persisted, recorded, phase,
                   attemptTemplate, wantedRev, templateRev, settled,
                   attemptRev, availableRev, prepared>>

Publish(template) ==
    /\ wantedRev[template] /= templateRev[template]
    /\ settled[template]
    /\ publishRev[template] = {wantedRev[template]}
    /\ templateRev' = [templateRev EXCEPT ![template] = wantedRev[template]]
    /\ availableRev' =
        [availableRev EXCEPT ![template] = @ \cup {wantedRev[template]}]
    /\ publishRev' = [publishRev EXCEPT ![template] = {}]
    /\ UNCHANGED <<mode, templateRef, eligible, persisted, recorded, phase,
                   attemptTemplate, wantedRev, settled, attemptRev, prepared>>

Next ==
    \/ \E template \in Templates, revision \in Revisions :
        RequestTemplate(template, revision)
    \/ \E template \in Templates : Settle(template)
    \/ \E template \in Templates : PreparePublish(template)
    \/ \E template \in Templates : Publish(template)
    \/ \E delivery \in Deliveries, sourceMode \in Modes, identity \in Identities :
        ChangeEligibility(delivery, sourceMode, identity)
    \/ \E delivery \in Deliveries, sourceMode \in Modes :
        ChangeMode(delivery, sourceMode)
    \/ \E delivery \in Deliveries, template \in Templates :
        ChangeTemplateRef(delivery, template)
    \/ \E delivery \in Deliveries : Prepare(delivery)
    \/ \E pair \in RetryPairs :
        PrepareRetry(DeliveryOf(pair[1]), pair[1], pair[2])
    \/ \E attempt \in Others, template \in Templates : PrepareOther(attempt, template)
    \/ \E attempt \in Slots : Create(attempt)
    \/ \E attempt \in Slots : Start(attempt)
    \/ \E delivery \in Deliveries, attempt \in Attempts : Persist(delivery, attempt)
    \/ \E attempt \in Slots : Complete(attempt)
    \/ \E attempt \in Slots : Reject(attempt)
    \/ \E delivery \in Deliveries, sourceMode \in Modes : Release(delivery, sourceMode)
    \/ \E attempt \in Attempts : Collect(attempt)

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

\* Argo Secure mode also reads the captured specification during artifact cleanup.
TemplateAvailable ==
    \A attempt \in Slots : phase[attempt] \notin {Absent, Collected} =>
        \A template \in attemptTemplate[attempt] :
            attemptRev[attempt] \subseteq availableRev[template]

CollectedSaved ==
    \A attempt \in Attempts : phase[attempt] = Collected => attempt \in persisted

NoConcurrentRuns ==
    \A template \in Templates : Cardinality(RunningFor(template)) <= 1

TemplateStable ==
    [][\A attempt \in Slots : phase[attempt] \in {Queued, Running} =>
        UNCHANGED <<attemptTemplate[attempt], attemptRev[attempt]>>]_vars

PreparedAvailable ==
    \A attempt \in Slots : \A binding \in prepared[attempt] :
        binding[2] \in availableRev[binding[1]]

AdmissionReady ==
    [][\A attempt \in Slots : \A binding \in prepared'[attempt] \ prepared[attempt] :
        /\ settled[binding[1]]
        /\ binding[2] = wantedRev[binding[1]]
        /\ binding[2] = templateRev[binding[1]]]_vars

PublishDrained ==
    [][\A template \in Templates : publishRev'[template] \ publishRev[template] /= {} =>
        /\ settled[template]
        /\ ActiveFor(template) = {}
        /\ publishRev'[template] = {wantedRev[template]}]_vars

PublishLatest ==
    [][\A template \in Templates : templateRev'[template] /= templateRev[template] =>
        /\ settled[template]
        /\ publishRev[template] = {wantedRev[template]}
        /\ templateRev'[template] = wantedRev[template]]_vars

ProgressFair ==
    /\ Spec
    /\ \A template \in Templates :
        /\ WF_vars(Settle(template))
        /\ WF_vars(PreparePublish(template))
        /\ WF_vars(Publish(template))
    /\ \A attempt \in Slots :
        /\ WF_vars(Create(attempt))
        /\ WF_vars(Complete(attempt))

FairSpec ==
    /\ ProgressFair
    /\ \A attempt \in Slots : WF_vars(Start(attempt))

PublishProgress ==
    \A template \in Templates, revision \in Revisions :
        (<>[](wantedRev[template] = revision)) =>
            <>[](templateRev[template] = revision)

\* Strong fairness abstracts Argo's equal-priority mutex queue, ordered by creation time.
LiveSpec ==
    /\ ProgressFair
    /\ \A attempt \in Slots : SF_vars(Start(attempt))
    /\ \A delivery \in Deliveries : WF_vars(Prepare(delivery))
    /\ \A delivery \in Deliveries, attempt \in Attempts :
        WF_vars(Persist(delivery, attempt))
    /\ \A delivery \in Deliveries, sourceMode \in Modes :
        WF_vars(Release(delivery, sourceMode))

DebounceProgress ==
    \A template \in Templates, revision \in Revisions :
        (<>[](wantedRev[template] = revision)) => <>[]settled[template]

DrainProgress ==
    \A template \in Templates :
        (wantedRev[template] /= templateRev[template]) ~>
            (ActiveFor(template) = {} \/ wantedRev[template] = templateRev[template])

AttemptProgress ==
    \A attempt \in Slots :
        (phase[attempt] \in {Queued, Running}) ~>
            (phase[attempt] \in {Terminal, Collected})

ReleaseProgress ==
    \A delivery \in Deliveries, sourceMode \in Modes :
        (/\ recorded[delivery][sourceMode] /= {}
         /\ \A attempt \in recorded[delivery][sourceMode] :
                phase[attempt] \in {Terminal, Collected}) ~>
            (recorded[delivery][sourceMode] = {})

RecordOnce ==
    [][\A delivery \in Deliveries, sourceMode \in Modes :
        (recorded'[delivery][sourceMode] \ recorded[delivery][sourceMode])
            \subseteq (persisted' \ persisted)]_vars

RecordProgress ==
    \A attempt \in Attempts :
        (phase[attempt] /= Absent) ~> (attempt \in persisted)

SelectedFor(delivery, attempt, template, revision) ==
    /\ SelectedAttempt(delivery) = attempt
    /\ templateRef[delivery] = template
    /\ wantedRev[template] = revision

DeliveryProgress ==
    \A delivery \in Deliveries, attempt \in Attempts,
       template \in Templates, revision \in Revisions :
        (<>[]SelectedFor(delivery, attempt, template, revision)) =>
            <>(attempt \in persisted /\ phase[attempt] \in {Terminal, Collected})

ContinuousOnly == \A delivery \in Deliveries : mode[delivery] = Continuous

LiveDomain ==
    /\ ContinuousOnly
    /\ \A delivery \in Deliveries :
        eligible[delivery][Point] = CHOOSE identity \in Identities : TRUE

SharedTemplateRef ==
    [delivery \in Deliveries |-> CHOOSE template \in Templates : TRUE]

ContinuousMode == [delivery \in Deliveries |-> Continuous]

====