forked from dmilstein/channels
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathtest_render_timeline.py
94 lines (85 loc) · 3.06 KB
/
test_render_timeline.py
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
from render_timeline import parse_states, extract_msg_steps, extract_clients
tlc_output = r'''
State 5: <client line 65, col 20 to line 69, col 40 of module two_client_reliable_channel>
/\ C = [ ClientInboxes |->
[ client1 |->
<< [ rawMsg |->
[ receiver |-> "client1",
sender |-> "client2",
msgLabel |-> "1",
senderState |-> 1,
receiverState |-> "",
sendAt |-> 2,
payload |-> 1,
recvAt |-> -1 ] ],
[ rawMsg |->
[ receiver |-> "client1",
sender |-> "client2",
msgLabel |-> "1",
senderState |-> 2,
receiverState |-> "",
sendAt |-> 3,
payload |-> 1,
recvAt |-> -1 ] ] >>,
client2 |-> <<>> ],
LogicalTime |-> 4,
MsgSteps |->
{ [ receiver |-> "client2",
sender |-> "client1",
msgLabel |-> "1",
senderState |-> 1,
receiverState |-> 3,
sendAt |-> 1,
payload |-> "",
recvAt |-> 4 ] },
NextMsgId |-> 3 ]
/\ GlobalCount = [client1 |-> 1, client2 |-> 3]
/\ MsgsSent = [client1 |-> 1, client2 |-> 2]
State 6: <client line 65, col 20 to line 69, col 40 of module two_client_reliable_channel>
/\ C = [ ClientInboxes |->
[ client1 |->
<< [ rawMsg |->
[ receiver |-> "client1",
sender |-> "client2",
msgLabel |-> "1",
senderState |-> 2,
receiverState |-> "",
sendAt |-> 3,
payload |-> 1,
recvAt |-> -1 ] ] >>,
client2 |-> <<>> ],
LogicalTime |-> 5,
MsgSteps |->
{ [ receiver |-> "client1",
sender |-> "client2",
msgLabel |-> "1",
senderState |-> 1,
receiverState |-> 2,
sendAt |-> 2,
payload |-> "",
recvAt |-> 5 ],
[ receiver |-> "client2",
sender |-> "client1",
msgLabel |-> "1",
senderState |-> 1,
receiverState |-> 3,
sendAt |-> 1,
payload |-> "",
recvAt |-> 4 ] },
NextMsgId |-> 3 ]
/\ GlobalCount = [client1 |-> 2, client2 |-> 3]
/\ MsgsSent = [client1 |-> 1, client2 |-> 2]
'''
def test_parse_states():
states = parse_states(tlc_output)
assert len(states) == 2
final_state = states[-1]
steps = extract_msg_steps(final_state)
assert len([ s.recvAt for s in steps if s.received ]) == 2
assert len([ s.recvAt for s in steps if not s.received ]) == 1
clients = extract_clients(final_state)
assert clients == ['client1', 'client2']
def test_parser_can_find_channels_under_any_name():
tlc_output_adjusted = tlc_output.replace(r'/\ C =', r'/\ OtherName =')
steps = extract_msg_steps(parse_states(tlc_output_adjusted)[-1])
assert len(steps) == 3