worldstore-loader-tla/Types.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
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
----------------------------- MODULE Types ----------------------------
EXTENDS Integers

CONSTANT Request,
         Version,
         Key,
         Topic,
         TopicsForKey,
         TopicVersionCacheInstance,
         DataCacheInstance,
         CacheInvalidator

ASSUME
  /\ Version \subseteq Nat
  /\ \A v \in Version: v \geq 0
  /\ (\A v \in Version: v = 0 \/ (v - 1) \in Version)

ASSUME
  /\ TopicsForKey \in [Key -> SUBSET Topic]
  /\ \A k \in Key: TopicsForKey[k] /= {}

\* We pretend the data contains the version associated with its latest
\* update. This is only used by the safety invariant.
Data == [lastUpdateVersion: Version]

NoneVal == [type |-> "None"]
SomeVal(value) == [type |-> "Some", value |-> value]
Maybe(valueSet) == [type: {"None"}] \cup [type: {"Some"}, value: valueSet]

TopicVersionCacheResponse == Maybe([maxTopicVersion: Version, cacheVersion: Version])
TopicVersionCacheState == [maybeVersionForTopic: [Topic -> Maybe(Version)], maybeVersion: Maybe(Version)]

DataCacheResponse == Maybe([data: Data, version: Version])
DataCacheState == [Key -> DataCacheResponse]

DatabaseResponse == Data
DatabaseSnapshot == [Key -> DatabaseResponse]
DatabaseState == [maybeSnapshotForVersion: [Version -> Maybe(DatabaseSnapshot)], version: Version]

IdleType == "Idle"
StartedType == "Started"
CachesRequestedType == "CachesRequested"
CacheMissType == "CacheMiss"
DatabaseRespondedType == "DatabaseResponded"
CompletedType == "Complete"

RequestState ==
  [type: {IdleType}]
      \cup
  [
    type: {StartedType},
    key: Key,
    requestVersion: Version
  ]
      \cup
  [
    type: {CachesRequestedType},
    key: Key,
    requestVersion: Version,
    maybeTopicVersionCacheResponse: Maybe(TopicVersionCacheResponse),
    maybeDataCacheResponse: Maybe(DataCacheResponse)
  ]
      \cup
  [
    type: {CacheMissType},
    key: Key,
    requestVersion: Version,
    maybeCacheVersion: Maybe(Version)
  ]
      \cup
  [
    type: {DatabaseRespondedType},
    key: Key,
    requestVersion: Version,
    maybeCacheVersion: Maybe(Version),
    databaseResponse: DatabaseResponse
  ]
      \cup
  [type: {CompletedType}, key: Key, requestVersion: Version, response: Data]

MaximumVersion(versions) ==
  IF versions = {} THEN -1 ELSE CHOOSE n \in versions : \A m \in versions : n \geq m
==================================================================================