worldstore-loader-tla/RequestOperators.tla at master · bwzhang/worldstore-loader-tla · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
----------------------------- MODULE RequestOperators ----------------------------
EXTENDS Types

IdleRequestState == [type |-> IdleType]

StartedRequestState(key, requestVersion) ==
  [
    type |-> StartedType,
    key |-> key,
    requestVersion |-> requestVersion
  ]

CachesRequestedRequestState(requestState) ==
  [
    type |-> CachesRequestedType,
    key |-> requestState.key,
    requestVersion |-> requestState.requestVersion,
    maybeTopicVersionCacheResponse |-> NoneVal,
    maybeDataCacheResponse |-> NoneVal
  ]

CacheMissRequestState(requestState, maybeCacheVersion) ==
  [
    type |-> CacheMissType,
    key |-> requestState.key,
    requestVersion |-> requestState.requestVersion,
    maybeCacheVersion |-> maybeCacheVersion
  ]

DatabaseRespondedRequestState(requestState, databaseResponse) ==
  [
    type |-> DatabaseRespondedType,
    key |-> requestState.key,
    requestVersion |-> requestState.requestVersion,
    maybeCacheVersion |-> requestState.maybeCacheVersion,
    databaseResponse |-> databaseResponse
  ]

CompletedRequestState(requestState, response) ==
  [
    type |-> CompletedType,
    key |-> requestState.key,
    requestVersion |-> requestState.requestVersion,
    response |-> response
  ]
==================================================================================