-
Notifications
You must be signed in to change notification settings - Fork 1
/
dataWire.tla
134 lines (104 loc) · 3.76 KB
/
dataWire.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
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
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
------------------------------ MODULE dataWire ------------------------------
EXTENDS Sequences, TLC, Naturals
CONSTANTS CORRUPT_DATA
(* --algorithm DataWire
variables
input = <<>>,
output = <<>>;
define
DropRandom(input1) == LET n == CHOOSE n \in 1..Len(input1) : TRUE
IN SubSeq(input1, 1, n) \o SubSeq(input1, n+2, Len(input1))
CorruptRandom(input2) == LET n == CHOOSE n \in 1..Len(input2) : TRUE
IN SubSeq(input2, 1, n) \o <<CORRUPT_DATA>> \o SubSeq(input2, n+2, Len(input2))
RECURSIVE CorruptLen2(_)
CorruptLen2(i) == IF i = 0 THEN <<>>
ELSE <<CORRUPT_DATA>> \o CorruptLen2(i-1)
CorruptLen(input3) == CorruptLen2(Len(input3))
end define;
fair+ process sendNormally = "Send"
begin A:
while TRUE do
await input # <<>> /\ output = <<>>;
output := input;
input := <<>>;
end while;
end process;
process dropRandomPacket = "Drop Rand"
begin A:
while TRUE do
await input # <<>> /\ output = <<>>;
output := DropRandom(input);
input := <<>>;
end while;
end process;
process dropAllPackets = "Drop All"
begin A:
while TRUE do
await input # <<>> /\ output = <<>>;
input := <<>>;
end while;
end process;
process corruptRandom = "corruptRandom"
begin A:
while TRUE do
await input # <<>> /\ output = <<>>;
output := CorruptRandom(input);
input := <<>>;
end while;
end process;
process corruptAllPackets = "corruptAll"
begin A:
while TRUE do
await input # <<>> /\ output = <<>>;
output := CorruptLen(input);
input := <<>>;
end while;
end process;
\* Shuffle was not attempted due to complexity, and corruption / dropping solves a similar problem
end algorithm;
*)
\* BEGIN TRANSLATION
\* Label A of process sendNormally at line 29 col 1 changed to A_
\* Label A of process dropRandomPacket at line 38 col 1 changed to A_d
\* Label A of process dropAllPackets at line 47 col 1 changed to A_dr
\* Label A of process corruptRandom at line 55 col 1 changed to A_c
VARIABLES input, output
(* define statement *)
DropRandom(input1) == LET n == CHOOSE n \in 1..Len(input1) : TRUE
IN SubSeq(input1, 1, n) \o SubSeq(input1, n+2, Len(input1))
CorruptRandom(input2) == LET n == CHOOSE n \in 1..Len(input2) : TRUE
IN SubSeq(input2, 1, n) \o <<CORRUPT_DATA>> \o SubSeq(input2, n+2, Len(input2))
RECURSIVE CorruptLen2(_)
CorruptLen2(i) == IF i = 0 THEN <<>>
ELSE <<CORRUPT_DATA>> \o CorruptLen2(i-1)
CorruptLen(input3) == CorruptLen2(Len(input3))
vars == << input, output >>
ProcSet == {"Send"} \cup {"Drop Rand"} \cup {"Drop All"} \cup {"corruptRandom"} \cup {"corruptAll"}
Init == (* Global variables *)
/\ input = <<>>
/\ output = <<>>
sendNormally == /\ input # <<>> /\ output = <<>>
/\ output' = input
/\ input' = <<>>
dropRandomPacket == /\ input # <<>> /\ output = <<>>
/\ output' = DropRandom(input)
/\ input' = <<>>
dropAllPackets == /\ input # <<>> /\ output = <<>>
/\ input' = <<>>
/\ UNCHANGED output
corruptRandom == /\ input # <<>> /\ output = <<>>
/\ output' = CorruptRandom(input)
/\ input' = <<>>
corruptAllPackets == /\ input # <<>> /\ output = <<>>
/\ output' = CorruptLen(input)
/\ input' = <<>>
Next == sendNormally \/ dropRandomPacket \/ dropAllPackets \/ corruptRandom
\/ corruptAllPackets
Spec == /\ Init /\ [][Next]_vars
/\ SF_vars(sendNormally)
\* END TRANSLATION
Fairness == /\ SF_vars(sendNormally)
=============================================================================
\* Modification History
\* Last modified Mon Jun 17 00:59:40 NZST 2019 by jb567
\* Created Sat Jun 01 15:52:42 NZST 2019 by jb567