blob: 80d0358e4a0e0ec41fca76203ce9d7c0bea004a5 (
plain)
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
|
\* Config file to run the TLC model-checker on MultiTenantMigrations.tla.
\* See MultiTenantMigrations.tla for instructions.
CONSTANTS DonorStartMigrationRequest = DonorStartMigrationRequest
CONSTANTS DonorStartMigrationResponse = DonorStartMigrationResponse
CONSTANTS RecipientSyncData1Request = RecipientSyncData1Request
CONSTANTS RecipientSyncData1Response = RecipientSyncData1Response
CONSTANTS RecipientSyncData2Request = RecipientSyncData2Request
CONSTANTS RecipientSyncData2Response = RecipientSyncData2Response
CONSTANTS DonorForgetMigrationRequest = DonorForgetMigrationRequest
CONSTANTS DonorForgetMigrationResponse = DonorForgetMigrationResponse
CONSTANTS RecipientForgetMigrationRequest = RecipientForgetMigrationRequest
CONSTANTS RecipientForgetMigrationResponse = RecipientForgetMigrationResponse
CONSTANTS RecUnstarted = RecUnstarted
CONSTANTS RecInconsistent = RecInconsistent
CONSTANTS RecConsistent = RecConsistent
CONSTANTS RecLagged = RecLagged
CONSTANTS RecReady = RecReady
CONSTANTS RecAborted = RecAborted
CONSTANTS RecTerminalState = RecTerminalState
CONSTANTS DonUnstarted = DonUnstarted
CONSTANTS DonDataSync = DonDataSync
CONSTANTS DonBlocking = DonBlocking
CONSTANTS DonCommitted = DonCommitted
CONSTANTS DonAborted = DonAborted
CONSTANTS DonTerminalState = DonTerminalState
CONSTANTS CloudUnknown = CloudUnknown
CONSTANTS CloudCommitted = CloudCommitted
CONSTANTS CloudAborted = CloudAborted
CONSTANTS CloudTerminalState = CloudTerminalState
CONSTANTS MigrationNone = MigrationNone
CONSTANTS MigrationCommitted = MigrationCommitted
CONSTANTS MigrationAborted = MigrationAborted
CONSTANTS SyncOK = SyncOK
CONSTANTS SyncAborted = SyncAborted
CONSTANT MaxRequests = 8
INVARIANT StateMachinesConsistent
PROPERTY MigrationEventuallyCompletes
PROPERTY MessageBagEventuallyEmpties
PROPERTY EachRequestHasAResponse
\* Not configurable.
CONSTRAINT StateConstraint
SPECIFICATION Spec
\* The spec can terminate without a deadlock. The liveness properties are present to ensure the
\* termination states are correct.
CHECK_DEADLOCK FALSE
|
