---------------------------- MODULE RoostSecrets ----------------------------
EXTENDS Naturals, Sequences

CONSTANTS
  Invocations,
  MaxVersion,
  ReadsPerInvocation,
  Snapshot

VARIABLES
  store,
  phase,
  snap,
  reads

vars == <<store, phase, snap, reads>>

Init ==
  /\ store = 1
  /\ phase = [i \in Invocations |-> "idle"]
  /\ snap = [i \in Invocations |-> 0]
  /\ reads = [i \in Invocations |-> <<>>]

Rotate ==
  /\ store < MaxVersion
  /\ store' = store + 1
  /\ UNCHANGED <<phase, snap, reads>>

Start(i) ==
  /\ phase[i] = "idle"
  /\ phase' = [phase EXCEPT ![i] = "running"]
  /\ snap' = [snap EXCEPT ![i] = store]
  /\ UNCHANGED <<store, reads>>

Read(i) ==
  /\ phase[i] = "running"
  /\ Len(reads[i]) < ReadsPerInvocation
  /\ reads' = [reads EXCEPT ![i] = Append(@, IF Snapshot THEN snap[i] ELSE store)]
  /\ UNCHANGED <<store, phase, snap>>

Finish(i) ==
  /\ phase[i] = "running"
  /\ Len(reads[i]) = ReadsPerInvocation
  /\ phase' = [phase EXCEPT ![i] = "done"]
  /\ UNCHANGED <<store, snap, reads>>

Next ==
  \/ Rotate
  \/ \E i \in Invocations : Start(i) \/ Read(i) \/ Finish(i)

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

TypeOK ==
  /\ store \in 1..MaxVersion
  /\ \A i \in Invocations : phase[i] \in {"idle", "running", "done"}
  /\ \A i \in Invocations : snap[i] \in 0..MaxVersion
  /\ \A i \in Invocations : \A k \in 1..Len(reads[i]) : reads[i][k] \in 1..MaxVersion

OneVersionPerInvocation ==
  \A i \in Invocations :
    \A a, b \in 1..Len(reads[i]) : reads[i][a] = reads[i][b]

CurrentAtStart ==
  \A i \in Invocations :
    \A k \in 1..Len(reads[i]) : reads[i][k] = snap[i]

=============================================================================