------------------------- MODULE getCollectionPagev5 -------------------------

(* Traverses a relationship to the cache named statuses and updates the *)
(* array of pages to match. *)

EXTENDS Naturals, Integers, FiniteSets

CONSTANTS
  totalItems,
  pageSize,
  desired,
  next,
  maxFullPage,
  minFullPage,
  sentinelSize

VARIABLES
  statuses,
  pages,
  item,
  changes

additions == CHOOSE n \in 0..totalItems : TRUE
deletions == CHOOSE n \in 0..(totalItems-additions) : TRUE
netChanges == additions - deletions

(* Item numbers are monotonically increasing. *)
PossibleItems == 0..(totalItems-1)
ItemNat ==  CHOOSE x \in SUBSET PossibleItems : x /= {}
ItemStatus == { "new", "deleted", "unmodified" }

(* A dreaded magic number. *)
Sentinel == 9999

sentinelPageSize == (sentinelSize + additions) % pageSize
newlyFullPages == (sentinelSize + additions) \div pageSize 
pageBound == newlyFullPages + maxFullPage

PageNat == 1..pageBound
PageCount == PageNat \cup { Sentinel }

TypeOK ==
  /\ totalItems \in Nat
  /\ netChanges \in Int
  /\ pageSize \in Nat
  /\ desired \in PageCount
  /\ next \in PageCount  
  /\ statuses \in [ ItemNat -> ItemStatus ]
  /\ Cardinality({ x \in DOMAIN statuses: statuses[x] = "new" }) = additions
  /\ Cardinality({ x \in DOMAIN statuses: statuses[x] = "deleted" }) = deletions
  /\ pages \in [ PageCount -> SUBSET (DOMAIN statuses) ]
  /\ item \in DOMAIN statuses
  /\ changes \in -totalItems..totalItems

Max(set) ==
  CHOOSE x \in set : \A y \in set : x >= y

Cached(page1) == 
  \A item1 \in pages[page1] : item < item1

(* We count pages the newest of which is Sentinel then enumerate backwards *)
(* from the total pages minus one to one. *)
PageAtOrBefore(page1, page2) == 
  page1 >= page2

PageOfNewItem ==
  CHOOSE p \in PageCount :
    p \in 1..minFullPage \cup maxFullPage..pageBound \cup { Sentinel }
    /\ \/ p = Sentinel /\ sentinelPageSize /= Cardinality(pages[p])
       \/ p /= Sentinel /\ pageSize /= Cardinality(pages[p])

PageOfDeleteItem == 
  CHOOSE p \in PageCount : item \in pages[p] 

Iterate == 
  /\ item >= 1
  /\ item' = Max({ x \in DOMAIN statuses : x < item })
  /\ desired' = desired
  /\ statuses' = statuses

(* We assume that all new elements in the statuses are appended, *)
(* or prepended. *)
NewAtEndsOnly ==
 \A item1 \in DOMAIN statuses:
   \/ \A item2 \in DOMAIN statuses: 
        item1 >= item2 \/
        ~(statuses[item2] = "new" /\ statuses[item1] /= "new")
   \/ \A item2 \in DOMAIN statuses: 
        item1 <= item2 \/
        ~(statuses[item2] = "new" /\ statuses[item1] /= "new")

JumpToNext ==
  /\ item = next
  /\ statuses[Max(DOMAIN statuses)] /= "new"
  /\ netChanges = 0
  /\ PageAtOrBefore(minFullPage, desired)
  /\ PageAtOrBefore(desired, maxFullPage)

GoToStart ==
  /\ item = Max(DOMAIN statuses)

PageItemsMonotonicalIncreasing ==
  \A page1, page2 \in PageCount :
    ~PageAtOrBefore(page1, page2) =>
        \A item1 \in pages[page1] : \A item2 \in pages[page2] : 
            item2 > item1

PagesLessThanPageSize ==
  \A page1 \in PageCount : Cardinality(pages[page1]) <= pageSize

NewItemsNotInPages ==
  \A item1 \in DOMAIN statuses : statuses[item1] = "new" =>
    \A page1 \in PageCount : \A item2 \in pages[page1] : item2 /= item1

DeletedItemsInPages == 
  \A item1 \in DOMAIN statuses : statuses[item1] = "deleted" =>
     \E page1 \in PageCount : \E item2 \in pages[page1] : item2 = item1

UnmodifiedItemsInPages == 
  \A item1 \in DOMAIN statuses : statuses[item1] = "unmodified" =>
     \E page1 \in PageCount : \E item2 \in pages[page1] : item2 = item1

EmptyNewPages == 
  /\ \A page1 \in maxFullPage..pageBound \cup { Sentinel } :
    pages[page1] = {}
  /\ \A page1 \in 1..minFullPage :
    pages[page1] = {}

InitiallyNewPageOrNoAddition == 
  /\ \A page1 \in minFullPage..maxFullPage :
    \A item1 \in pages[page1] : statuses[item1] /= "new"

Init ==
  /\ TypeOK
  (* Insures "new" statuses are only in continuous ranges connected to the *)
  (* ends. *)
  /\ NewAtEndsOnly
  (* Set item and page to either jump to next or start at Sentinel *)
  /\ JumpToNext \/ GoToStart
  (* We do not assume a consistent pageSize for pages. *)
  (* We do not assume that pages are defragmented of a certain number *)
  /\ PageItemsMonotonicalIncreasing
  /\ PagesLessThanPageSize
  (* statuses is a record of the state with respect to the pages cache. *)
  /\ NewItemsNotInPages
  /\ DeletedItemsInPages
  /\ UnmodifiedItemsInPages
  /\ EmptyNewPages
  /\ changes = 0

Next == 
  \/ /\ statuses[item] = "new"
     (* If we've read all the changes needed we stop updating. *)
     /\ changes /= netChanges \/ ~Cached(desired)
     /\ pages' = [ pages EXCEPT ![PageOfNewItem] = pages[PageOfNewItem] \cup { item } ]
     /\ IF ~PageAtOrBefore(PageOfNewItem, minFullPage)
        THEN changes' = changes + 1 
        ELSE changes' = changes
     /\ Iterate
  \/ /\ statuses[item] = "deleted"
     /\ changes /= netChanges \/ ~Cached(desired)
     /\ pages' = [ pages EXCEPT ![PageOfDeleteItem] = pages[PageOfDeleteItem] \ { item } ]
     /\ IF ~PageAtOrBefore(PageOfDeleteItem, minFullPage)
        THEN changes' = changes - 1 
        ELSE changes' = changes
     /\ Iterate
  \/ /\ statuses[item] = "unmodified"
     /\ changes /= netChanges \/ ~Cached(desired)
     /\ pages' = pages
     /\ changes' = changes
     /\ Iterate

Inv == 
  (* Because ItemStatus is an enum its impossible to move an item. *)
  /\ PageItemsMonotonicalIncreasing
  /\ PagesLessThanPageSize
  (* This asserts our cache page boundarys' stability. *)
  /\ InitiallyNewPageOrNoAddition

Spec == Init /\ [][Next]_<<statuses, pages, item, changes>>

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