---- MODULE Qualification ----
EXTENDS Integers, FiniteSets

CONSTANTS Deliveries, MaxBuilds, MaxRequests, MaxTime, Interval, InitialPolicy

Policies == {"OnBuild", "ManualOnly"}
Keys == Deliveries \X {"Auto"} \X (1..MaxBuilds) \cup
        Deliveries \X {"Manual"} \X (1..MaxRequests)
Phases == {"Absent", "Pending", "Reserved", "Queued", "Running", "Terminal"}
ActivePhases == {"Reserved", "Queued", "Running"}

VARIABLES latest, policy, request, attempts, now, lastStart, covered

vars == <<latest, policy, request, attempts, now, lastStart, covered>>

ASSUME /\ Deliveries /= {}
       /\ MaxBuilds \in Nat \ {0}
       /\ MaxRequests \in Nat \ {0}
       /\ MaxTime \in Nat
       /\ Interval \in [Deliveries -> Nat]
       /\ InitialPolicy \in [Deliveries -> Policies]

Input(delivery, build) == <<delivery, build>>
Inputs == Deliveries \X (0..MaxBuilds)
EmptyRequest == [build |-> 0, nonce |-> 0]
EmptyAttempt(delivery) ==
    [phase |-> "Absent", build |-> 0, input |-> Input(delivery, 0),
     started |-> -1, prior |-> -1]

Active == {key \in Keys : attempts[key].phase \in ActivePhases}
Due(delivery) ==
    lastStart[delivery] = -1 \/ now >= lastStart[delivery] + Interval[delivery]

TypeOK ==
    /\ latest \in [Deliveries -> 0..MaxBuilds]
    /\ policy \in [Deliveries -> Policies]
    /\ request \in [Deliveries -> [build : 0..MaxBuilds, nonce : 0..MaxRequests]]
    /\ attempts \in [Keys -> [phase : Phases, build : 0..MaxBuilds,
                              input : Inputs, started : -1..MaxTime,
                              prior : -1..MaxTime]]
    /\ now \in 0..MaxTime
    /\ lastStart \in [Deliveries -> -1..MaxTime]
    /\ covered \in [Deliveries -> 0..MaxBuilds]

Init ==
    /\ latest = [delivery \in Deliveries |-> 0]
    /\ policy = InitialPolicy
    /\ request = [delivery \in Deliveries |-> EmptyRequest]
    /\ attempts = [key \in Keys |-> EmptyAttempt(key[1])]
    /\ now = 0
    /\ lastStart = [delivery \in Deliveries |-> -1]
    /\ covered = [delivery \in Deliveries |-> 0]

BuildSuccess(delivery) ==
    /\ latest[delivery] < MaxBuilds
    /\ latest' = [latest EXCEPT ![delivery] = @ + 1]
    /\ UNCHANGED <<policy, request, attempts, now, lastStart, covered>>

ChangePolicy(delivery, value) ==
    /\ policy[delivery] /= value
    /\ policy' = [policy EXCEPT ![delivery] = value]
    /\ UNCHANGED <<latest, request, attempts, now, lastStart, covered>>

Annotate(delivery, build, nonce) ==
    /\ build <= latest[delivery]
    /\ request' = [request EXCEPT ![delivery] = [build |-> build, nonce |-> nonce]]
    /\ UNCHANGED <<latest, policy, attempts, now, lastStart, covered>>

Accept(delivery) ==
    LET value == request[delivery]
        key == <<delivery, "Manual", value.nonce>>
    IN  /\ value.build > 0
        /\ value.nonce > 0
        /\ attempts[key].phase = "Absent"
        /\ attempts' = [attempts EXCEPT ![key] =
                [EmptyAttempt(delivery) EXCEPT
                    !.phase = "Pending", !.build = value.build,
                    !.input = Input(delivery, value.build)]]
        /\ UNCHANGED <<latest, policy, request, now, lastStart, covered>>

ReserveManual(key) ==
    /\ attempts[key].phase = "Pending"
    /\ Active = {}
    /\ attempts' = [attempts EXCEPT ![key].phase = "Reserved"]
    /\ UNCHANGED <<latest, policy, request, now, lastStart, covered>>

ReserveAuto(delivery) ==
    LET build == latest[delivery]
        key == <<delivery, "Auto", build>>
    IN  /\ policy[delivery] = "OnBuild"
        /\ build > covered[delivery]
        /\ Due(delivery)
        /\ Active = {}
        /\ attempts[key].phase = "Absent"
        /\ attempts' = [attempts EXCEPT ![key] =
                [EmptyAttempt(delivery) EXCEPT
                    !.phase = "Reserved", !.build = build,
                    !.input = Input(delivery, build)]]
        /\ UNCHANGED <<latest, policy, request, now, lastStart, covered>>

Submit(key) ==
    /\ attempts[key].phase = "Reserved"
    /\ attempts' = [attempts EXCEPT ![key].phase = "Queued"]
    /\ UNCHANGED <<latest, policy, request, now, lastStart, covered>>

Start(key) ==
    LET delivery == key[1]
        build == attempts[key].build
    IN  /\ attempts[key].phase = "Queued"
        /\ attempts' = [attempts EXCEPT ![key].phase = "Running",
                ![key].started = now, ![key].prior = lastStart[delivery]]
        /\ lastStart' = [lastStart EXCEPT ![delivery] = now]
        /\ covered' = [covered EXCEPT ![delivery] =
                IF build > @ THEN build ELSE @]
        /\ UNCHANGED <<latest, policy, request, now>>

Complete(key) ==
    /\ attempts[key].phase \in {"Queued", "Running"}
    /\ attempts' = [attempts EXCEPT ![key].phase = "Terminal"]
    /\ UNCHANGED <<latest, policy, request, now, lastStart, covered>>

Tick ==
    /\ now < MaxTime
    /\ now' = now + 1
    /\ UNCHANGED <<latest, policy, request, attempts, lastStart, covered>>

Next ==
    \/ \E delivery \in Deliveries : BuildSuccess(delivery)
    \/ \E delivery \in Deliveries, value \in Policies : ChangePolicy(delivery, value)
    \/ \E delivery \in Deliveries, build \in 1..MaxBuilds, nonce \in 1..MaxRequests :
        Annotate(delivery, build, nonce)
    \/ \E delivery \in Deliveries : Accept(delivery)
    \/ \E key \in Keys : ReserveManual(key)
    \/ \E delivery \in Deliveries : ReserveAuto(delivery)
    \/ \E key \in Keys : Submit(key)
    \/ \E key \in Keys : Start(key)
    \/ \E key \in Keys : Complete(key)
    \/ Tick

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

FairSpec ==
    /\ Spec
    /\ \A key \in Keys :
        /\ SF_vars(ReserveManual(key))
        /\ WF_vars(Submit(key))
        /\ WF_vars(Start(key))
        /\ WF_vars(Complete(key))
    /\ \A delivery \in Deliveries :
        /\ WF_vars(Accept(delivery))
        /\ SF_vars(ReserveAuto(delivery))
    /\ WF_vars(Tick)

ManualProgress ==
    \A key \in Keys :
        (attempts[key].phase = "Pending") ~> (attempts[key].phase = "Terminal")

Eligible(delivery, build) ==
    /\ policy[delivery] = "OnBuild"
    /\ latest[delivery] = build
    /\ build > covered[delivery]
    /\ Due(delivery)

AutoProgress ==
    \A delivery \in Deliveries, build \in 1..MaxBuilds :
        Eligible(delivery, build) ~>
            (attempts[<<delivery, "Auto", build>>].phase /= "Absent" \/
             ~Eligible(delivery, build))

GlobalCap == Cardinality(Active) <= 1

SuccessfulInputs ==
    \A key \in Keys : attempts[key].phase /= "Absent" =>
        /\ attempts[key].build \in 1..latest[key[1]]
        /\ attempts[key].input = Input(key[1], attempts[key].build)

AutoInterval ==
    \A key \in Keys :
        /\ key[2] = "Auto"
        /\ attempts[key].started >= 0
        /\ attempts[key].prior >= 0
        => attempts[key].started >= attempts[key].prior + Interval[key[1]]

InputsStable ==
    [][\A key \in Keys : attempts[key].phase /= "Absent" =>
        UNCHANGED <<attempts[key].build, attempts[key].input>>]_vars

AutoSelection ==
    [][\A key \in Keys :
        /\ key[2] = "Auto"
        /\ attempts[key].phase = "Absent"
        /\ attempts'[key].phase = "Reserved"
        => /\ policy[key[1]] = "OnBuild"
           /\ attempts'[key].build = latest[key[1]]
           /\ latest[key[1]] > covered[key[1]]
           /\ Due(key[1])]_vars

NoRestart ==
    [][\A key \in Keys : attempts[key].phase = "Terminal" =>
        attempts'[key].phase = "Terminal"]_vars

OnBuildPolicy == [delivery \in Deliveries |-> "OnBuild"]
TwoTicks == [delivery \in Deliveries |-> 2]

====