-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathtest.maude
More file actions
154 lines (130 loc) · 9.71 KB
/
test.maude
File metadata and controls
154 lines (130 loc) · 9.71 KB
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
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
load ./actor.maude
--- This is used to make sure that counter increments everytime we call it
set clear rules off .
******* TEST COUNTER *******
--- rew counter . --- 0
--- rew counter . --- 1
--- rew counter . --- 2
--- rew counter counter . --- 3 4
******* TEST referenceList in ACTOR *******
--- red (0 :: 1 -> 2 ) , (3 :: 4 -> 5) , (6 :: 7 -> 8) .
******* TEST Msg in ACTOR *******
--- red @ A:MsgType :: B:ActorList :: C:ReferenceList :: D:MsgList @ .
--- red @ A:MsgType :: B:Actor C:ActorList :: D:ReferenceList :: E:Msg F:MsgList @ .
******* TEST updateInfo in ACTOR *******
--- testing releasing
--- --- remove from DR
--- red updateInfo(< i: 0 | sn: 0 | r: mtRefList | dr: (2 :: 3 -> 1), (3 :: 4 -> 5) | o: mtRefList | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | oa: empty >, 1) .
--- red updateInfo(< i: 0 | sn: 0 | r: mtRefList | dr: (2 :: 3 -> 0), (2 :: 3 -> 1) | o: mtRefList | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList |oa: empty >, 1) .
--- --- does not remove from DR
--- red updateInfo(< i: 0 | sn: 0 | r: mtRefList | dr: (2 :: 3 -> 0), (2 :: 3 -> 5) | o: mtRefList | ro: mtRefList | m: mtRefList | tr: mtRefList | owr: mtRefList | oa: empty >, 1) .
--- --- add to target releasing
--- red updateInfo(< i: 0 | sn: 0 | r: mtRefList | dr: mtRefList | o: mtRefList | ro: mtRefList | m: (2 :: 3 -> 1) | tr: mtRefList | owr: mtRefList | oa: empty >, 1) .
--- red updateInfo(< i: 0 | sn: 0 | r: mtRefList | dr: mtRefList | o: mtRefList | ro: mtRefList | m: (3 :: 4 -> 5), (2 :: 3 -> 1) | tr: mtRefList | owr: mtRefList | oa: empty >, 1) .
--- --- does not add to target releasing
--- red updateInfo(< i: 0 | sn: 0 | r: mtRefList | dr: mtRefList | o: mtRefList | ro: mtRefList | m: (2 :: 3 -> 2) | tr: mtRefList | owr: mtRefList | oa: empty >, 1) .
--- red updateInfo(< i: 0 | sn: 0 | r: mtRefList | dr: mtRefList | o: mtRefList | ro: mtRefList | m: (3 :: 4 -> 5), (2 :: 3 -> 3) | tr: mtRefList | owr: mtRefList | oa: empty >, 1) .
--- --- add to owner_releasing
--- red updateInfo(< i: 0 | sn: 0 | r: mtRefList | dr: mtRefList | o: mtRefList | ro: mtRefList | m: (2 :: 3 -> 1) | tr: mtRefList | owr: mtRefList | oa: empty >, 3) .
--- red updateInfo(< i: 0 | sn: 0 | r: mtRefList | dr: mtRefList | o: mtRefList | ro: mtRefList | m: (3 :: 4 -> 5), (2 :: 3 -> 1) | tr: mtRefList | owr: mtRefList | oa: empty >, 3) .
--- --- does not add to owner_releasing
--- red updateInfo(< i: 0 | sn: 0 | r: mtRefList | dr: mtRefList | o: mtRefList | ro: mtRefList | m: (2 :: 3 -> 2) | tr: mtRefList | owr: mtRefList | oa: empty >, 1) .
--- red updateInfo(< i: 0 | sn: 0 | r: mtRefList | dr: mtRefList | o: mtRefList | ro: mtRefList | m: (3 :: 4 -> 5), (2 :: 3 -> 3) | tr: mtRefList | owr: mtRefList | oa: empty >, 1) .
--- --- add to onAck from everything
--- --- TODO: NEEDS MORE TESTING
--- --- dr: should contain only 2 :: 2 -> 2
--- --- tr: should contain (3 :: 3 -> 1),(4 :: 4 -> 1)
--- --- owr: should contain (5 :: 1 -> 3)
--- --- sn: should be 1
--- --- oa: should contain (2 :: 2 -> 2),(3 :: 3 -> 1),(4 :: 4 -> 1),(5 :: 1 -> 3)
--- --- red updateInfo(< i: 0 | sn: 0 | r: mtRefList | dr: (0 :: 0 -> 1),(1 :: 1 -> 1),(2 :: 2 -> 2) | o: mtRefList | ro: mtRefList | m: (3 :: 3 -> 1),(4 :: 4 -> 1),(5 :: 1 -> 3),(6 :: 6 -> 7) | tr: mtRefList | owr: mtRefList | oa: empty >, 1) .
***(
ALL THE THINGS ABOVE ARE DEFUNCT UNTIL FURTHER NOTICE
THIS IS BECAUSE WE NEED TO NOT USE NAT BUT RATHER INAT
)
******* TEST newActor in ACTOR *******
--- red in ACTOR : newActor(0, mtRef) .
******* TEST spawn in ACTOR *******
--- red in ACTOR : spawn(s 0, mtRef) .
******* TEST createRef in ACTOR *******
--- red createRef(s s s s s s 0, (0 :: s 0 -> s s 0) , (s s s 0 :: s s s s 0 -> s s s s s 0) ) .
******* TEST receive in ACTOR *******
--- red receive(newActor(0, mtRef), (s s s s s 0 :: s s s s s s 0 -> s s s s s s s 0)) .
******* TEST release in ACTOR *******
--- remove from a reference list that is longer than 1
--- red release(< i: 0 | sn: 0 | r: (s s s 0 :: s s s s 0 -> s s s s s 0), (0 :: s 0 -> s s 0) | dr: mtRef | o: mtRef | ro: mtRef | m: mtRef | tr: mtRef | owr: mtRef | oa: empty >, 0 :: s 0 -> s s 0) .
--- --- remove from a reference list that is length 1
--- red release(< i: 0 | sn: 0 | r: (0 :: s 0 -> s s 0) | dr: mtRef | o: mtRef | ro: mtRef | m: mtRef | tr: mtRef | owr: mtRef | oa: empty >, 0 :: s 0 -> s s 0) .
******* TEST realeasingEquiv in ACTOR *******
--- --- should return ff
--- --- releasingEquiv(0, (1 :: 2 -> 3))
--- red in ACTOR : releasingEquiv(0, (s 0 :: s s 0 -> s s s 0)) .
--- --- should return tt
--- --- releasingEquiv(0, (1 :: 2 -> 0))
--- red in ACTOR : releasingEquiv(0, (s 0 :: s s 0 -> 0)) .
******* TEST releasingRefList in ACTOR *******
--- --- should return mtRefList
--- --- red in ACTOR : releasingRefList(0, mtRefList) .
--- --- releasingRefList(0, (1 :: 2 -> 3), (4 :: 5 -> 6))
--- red in ACTOR : releasingRefList(0, ((s 0 :: s s 0 -> s s s 0), (s s s s 0 :: s s s s s 0 -> s s s s s s 0))) .
--- --- should return a non-empty list
--- --- releasingRefList(0, (1 :: 2 -> 3), (4 :: 5 -> 0), (6 :: 7 -> 8)) = 4 :: 5 -> 0
--- red in ACTOR : releasingRefList(0, ((s 0 :: s s 0 -> s s s 0), (s s s s 0 :: s s s s s 0 -> 0), (s s s s s s 0 :: s s s s s s s 0 -> s s s s s s s s 0))) .
--- --- releasingRefList(0, (1 :: 2 -> 3), (4 :: 5 -> 0), (6 :: 7 -> 8), (9 :: 10 -> 0)) = 4 :: 5 -> 0, (9 :: 10 -> 0)
--- red in ACTOR : releasingRefList(0, ((s 0 :: s s 0 -> s s s 0), (s s s s 0 :: s s s s s 0 -> 0), (s s s s s s 0 :: s s s s s s s 0 -> s s s s s s s s 0), (s s s s s s s s s 0 :: s s s s s s s s s s 0 -> 0))) .
******* TEST createdRefList in ACTOR *******
--- --- should return mtRefList
--- red in ACTOR : createdRefList(0, mtRefList, mtRefList) .
--- red in ACTOR : createdRefList(0, mtRefList, 0 :: 0 -> 0) .
--- red in ACTOR : createdRefList(0, (s 0 :: s s 0 -> s s s 0), mtRefList) .
--- red in ACTOR : createdRefList(0, (s 0 :: s s 0 -> 0), (s 0 :: s s 0 -> 0)) .
--- red in ACTOR : createdRefList(0, (s 0 :: s s 0 -> s s s 0), (s 0 :: s s 0 -> s s s 0)) .
--- --- should return nonempty reflist
--- --- createRefList(0, 1 :: 2 -> 0, mtRefList) = 1 :: 2 -> 0
--- red in ACTOR : createdRefList(0, (s 0 :: s s 0 -> 0), mtRefList) .
--- --- createdRefList(0, (1 :: 2 -> 3, 4 :: 5 -> 0), (1 :: 2 -> 3)) = 4 :: 5 -> 0
--- red in ACTOR : createdRefList(0, ((s 0 :: s s 0 -> s s s 0), (s s s s 0 :: s s s s s 0 -> 0)), (s 0 :: s s 0 -> s s s 0)) .
--- --- createdRefList(0, (1 :: 2 -> 3, 4 :: 5 -> 0), (1 :: 2 -> 0)) = 4 :: 5 -> 0
--- red in ACTOR : createdRefList(0, ((s 0 :: s s 0 -> s s s 0), (s s s s 0 :: s s s s s 0 -> 0)), (s 0 :: s s 0 -> 0)) .
--- --- createdRefList(0, (1 :: 2 -> 0, 4 :: 5 -> 0, 6 :: 7 -> 0), (1 :: 2 -> 0)) = 4 :: 5 -> 0, 6 :: 7 -> 0
--- red in ACTOR : createdRefList(0, ((s 0 :: s s 0 -> 0), (s s s s 0 :: s s s s s 0 -> 0), (s s s s s s 0 :: s s s s s s s 0 -> 0)), (s 0 :: s s 0 -> 0)) .
******* TEST sentRefList in ACTOR *******
--- --- should return mtRefList
--- red in ACTOR : sentRefList(0, mtRefList, mtRefList) .
--- red in ACTOR : sentRefList(0, mtRefList, 0 :: 0 -> 0) .
--- red in ACTOR : sentRefList(0, (s 0 :: s s 0 -> s s s 0), mtRefList) .
--- red in ACTOR : sentRefList(0, (s 0 :: 0 -> 0), (s 0 :: 0 -> 0)) .
--- red in ACTOR : sentRefList(0, (s 0 :: s s 0 -> s s s 0), (s 0 :: s s 0 -> s s s 0)) .
--- --- should return nonempty reflist
--- --- sentRefList(0, 1 :: 0 -> 2, mtRefList) = 1 :: 0 -> 2
--- red in ACTOR : sentRefList(0, s 0 :: 0 -> s s 0, mtRefList) .
--- --- sentRefList(0, (1 :: 2 -> 3, 4 :: 0 -> 5), (1 :: 2 -> 3)) = 4 :: 0 -> 5
--- red in ACTOR : sentRefList(0, ((s 0 :: s s 0 -> s s s 0), (s s s s 0 :: 0 -> s s s s s 0)), (s 0 :: s s 0 -> s s s 0)) .
--- --- sentRefList(0, (1 :: 2 -> 3, 4 :: 0 -> 5), (1 :: 0 -> 2)) = 4 :: 0 -> 5
--- red in ACTOR : sentRefList(0, ((s 0 :: s s 0 -> s s s 0), (s s s s 0 :: 0 -> s s s s s 0)), (s 0 :: 0 -> s s 0)) .
--- --- sentRefList(0, (1 :: 0 -> 2, 4 :: 0 -> 5, 6 :: 0 -> 7), (1 :: 0 -> 2)) = 4 :: 0 -> 5, 6 :: 0 -> 7
--- red in ACTOR : sentRefList(0, ((s 0 :: 0 -> s s 0), (s s s s 0 :: 0 -> s s s s s 0), (s s s s s s 0 :: 0 -> s s s s s s s 0)), (s 0 :: 0 -> s s 0)) .
******* TEST updateInfo in ACTOR *******
--- --- add to onAck from everything
--- --- TODO: NEEDS MORE TESTING
--- --- dr: should contain only 2 :: 2 -> 2
--- --- tr: should contain (3 :: 3 -> 1),(4 :: 4 -> 1)
--- --- owr: should contain (5 :: 1 -> 3)
--- --- sn: should be 1
--- --- releasing: (0 :: 0 -> 1), (1 :: 1 -> 1)
--- --- created: (3 :: 3 -> 1), (4 :: 4 -> 1)
--- --- sent: (5 :: 1 -> 3)
--- --- oa: (0 :: 0 -> 1), (1 :: 1 -> 1) U (3 :: 3 -> 1), (4 :: 4 -> 1) U (5 :: 1 -> 3)
--- --- updateInfo(< i: 0 | sn: 0 | r: mtRefList | dr: (0 :: 0 -> 1),(1 :: 1 -> 1),(2 :: 2 -> 2) | o: mtRefList | ro: mtRefList | m: (3 :: 3 -> 1),(4 :: 4 -> 1),(5 :: 1 -> 3),(6 :: 6 -> 7) | tr: mtRefList | owr: mtRefList | oa: empty >, 1) .
--- --- < i: 0
--- --- | sn: s 0
--- --- | r: mtRefList
--- --- | dr: s s 0 :: s s 0 -> s s 0
--- --- | o: mtRefList | ro: mtRefList
--- --- | m: (s s s 0 :: s s s 0 -> s 0),(s s s s 0 :: s s s s 0 -> s 0),(s s s s s 0 :: s 0 -> s s s 0),s s s s s s 0 :: s s s s s s 0 -> s s s s s s s 0
--- --- | tr: (s s s 0 :: s s s 0 -> s 0),s s s s 0 :: s s s s 0 -> s 0
--- --- | owr: s s s s s 0 :: s 0 -> s s s 0
--- --- | oa: s 0 |-> (0 :: 0 -> s 0),(s 0 :: s 0 -> s 0),(s s s 0 :: s s s 0 -> s 0),(s s s s 0 :: s s s s 0 -> s 0),s s s s s 0 :: s 0 -> s s s 0
--- --- >
--- red updateInfo(< i: 0 | sn: 0 | r: mtRefList | dr: (0 :: 0 -> s 0),(s 0 :: s 0 -> s 0),(s s 0 :: s s 0 -> s s 0) | o: mtRefList | ro: mtRefList | m: (s s s 0 :: s s s 0 -> s 0),(s s s s 0 :: s s s s 0 -> s 0),(s s s s s 0 :: s 0 -> s s s 0),(s s s s s s 0 :: s s s s s s 0 -> s s s s s s s 0) | tr: mtRefList | owr: mtRefList | oa: empty >, s 0) .
--- red ((0 :: 0 -> s 0),s 0 :: s 0 -> s 0) U s s s s s 0 :: s 0 -> s s s 0 U (s s s 0 :: s s s 0 -> s 0) .