-
Notifications
You must be signed in to change notification settings - Fork 0
/
fn.tla
57 lines (42 loc) · 1.48 KB
/
fn.tla
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
--------------------------------- MODULE fn ---------------------------------
EXTENDS Naturals, TLC
----
(* Debugging helpers *)
PrintVal(id, exp) == PrintT(<<id, exp>>)
----
VARIABLES slots
----
NumSlots == 2
Caps == {"Null", "Mem"}
Cores == {0,1}
NoOwner == CHOOSE v : v \notin Cores
Slots == [cap: Caps, owner: (Cores \union {NoOwner}), location: Cores, locked: BOOLEAN]
IsCopy(a, b) ==
a = b
SlotWithNull(slot) ==
[ slot EXCEPT !.cap = "Null", !.owner = NoOwner, !.locked = FALSE ]
Init ==
slots = [s \in 0..(NumSlots-1) |->
IF s = 0
THEN [cap |-> "Mem",
owner |-> 0,
location |-> s % 2,
locked |-> TRUE]
ELSE [cap |-> "Null",
owner |-> NoOwner,
location |-> s % 2,
locked |-> FALSE]]
Next ==
/\ PrintVal("slots:", slots)
/\ slots' = [ s \in DOMAIN slots |->
CASE s = 0
-> [ slots[s] EXCEPT !.locked = FALSE ]
[] IsCopy(slots[s], slots[0])
-> SlotWithNull(slots[s])
[] OTHER
-> slots[s]]
/\ PrintVal("slots'", slots')
=============================================================================
\* Modification History
\* Last modified Thu May 18 10:42:22 CEST 2017 by gerbesim
\* Created Thu May 18 10:23:43 CEST 2017 by gerbesim