-
Notifications
You must be signed in to change notification settings - Fork 0
/
reference.maude
145 lines (127 loc) · 6.69 KB
/
reference.maude
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
set include BOOL off .
load util.maude
fmod REFERENCE is protecting INAT .
--- ########## SORTS ##########
sorts Reference NeReferenceList ReferenceList ReferenceListUnion .
--- ########## SUBSORTS ##########
subsorts Reference < NeReferenceList < ReferenceList .
--- ########## OPS ##########
op mtRefListUnion : -> ReferenceListUnion [ctor] .
op mtRefList : -> ReferenceList [ctor] .
--- References
--- x : A -> B, where x is a reference ID and A,B are actor IDs
op _::_->_ : iNat iNat iNat -> Reference [ctor] .
--- op __ : Reference Reference -> ReferenceList [ctor] .
--- TODO: Should this check for uniqueness (set) for each reference?
op _,_ : ReferenceList ReferenceList -> ReferenceList [ctor comm assoc id: mtRefList] .
op _,_ : NeReferenceList ReferenceList -> NeReferenceList [ctor ditto] .
op _,_ : ReferenceList NeReferenceList -> NeReferenceList [ctor ditto] .
--- This removes the references in the first reference list from the second reference list
op remList(_,_) : ReferenceList ReferenceList -> ReferenceList .
--- This operate denotes the 3 possible things we have in on ack
--- releasing U created U sent
op _U_U_ : ReferenceList ReferenceList ReferenceList -> ReferenceListUnion [ctor] .
--- This returns the length of a reference list
op lenRL(_) : ReferenceList -> iNat .
--- Given two ReferenceLists A, B check that B's destinations are a subset of
--- A's destinations
op checkSubsetRefApp(_,_) : ReferenceList ReferenceList -> Pred .
op checkSubsetRefAppHelper(_,_) : ReferenceList Reference -> Pred .
--- checks if a reference is in a reference list
op _in_ : Reference ReferenceList -> Pred .
--- checks if two reference lists are equal
op _~RL_ : ReferenceList ReferenceList -> Pred .
--- ########## VARS ##########
vars x A B C D E F : iNat .
vars RefA RefB : Reference .
vars RefLiA RefLiB RefLiC RefLiD RefLiE RefLiF RefLiG RefLiH : ReferenceList .
--- ########## EQS ##########
--- Uniqueness equation
--- NOTE: THIS CHECKS A REFERENCE AS A WHOLE AND NOT JUST THE REFERENCE NUMBER
--- eq (RefLiA, RefA, RefLiB), (RefLiC, RefA, RefLiD) = RefLiA, RefA, RefLiB, RefLiC, RefLiD .
--- NOTE: THIS CHECKS A REFERENCE NUMBER SPECIFICALLY
--- eq mtRef, mtRef = mtRef .
--- eq mtRef, RefLiA = RefLiA .
eq (RefLiA, (x :: A -> B), RefLiB), (RefLiC, (x :: C -> D), RefLiD) = RefLiA, (x :: A -> B), RefLiB, RefLiC, RefLiD .
eq remList(mtRefList, RefLiA) = RefLiA . --- termination
eq remList((RefA, RefLiA), (RefLiB, RefA, RefLiC)) = remList(RefLiA, (RefLiB, RefLiC)) . --- remove case
eq remList((RefA, RefLiA), (RefLiB, RefB, RefLiC)) = RefB, remList(RefLiA, (RefLiB, RefLiC)) . --- doesn't exist recreate
--- eq mtRefList U mtRefList = mtRefList .
--- eq RefLiA U mtRefList = RefLiA .
--- eq mtRefList U RefLiA = RefLiA .
--- eq (RefA, RefLiA) U (RefA, RefLiB) = RefA, (RefLiA U RefLiB) .
--- eq (RefA, RefLiA) U (RefB, RefLiB) = RefA, RefB, (RefLiA U RefLiB) .
eq lenRL(mtRefList) = 0 .
eq lenRL(RefA, RefLiA) = s lenRL(RefLiA) .
eq checkSubsetRefApp(mtRefList, mtRefList) = tt .
eq checkSubsetRefApp(RefLiA, mtRefList) = tt .
eq checkSubsetRefApp(mtRefList, RefLiB) = ff .
eq checkSubsetRefApp(RefLiA, (RefA , RefLiB)) =
checkSubsetRefAppHelper(RefLiA, RefA) and checkSubsetRefApp(RefLiA, RefLiB) .
eq checkSubsetRefAppHelper(mtRefList, RefA) = ff .
eq checkSubsetRefAppHelper( ( (A :: B -> C), RefLiA ) , (D :: E -> F) ) =
(C ~iN F) or checkSubsetRefAppHelper(RefLiA, (D :: E -> F) ) .
eq RefA in mtRefList = ff .
eq RefA in (RefLiB, RefA, RefLiC) = tt .
eq RefA in (RefLiB, RefB, RefLiC) = ff .
eq mtRefList ~RL mtRefList = tt .
eq mtRefList ~RL RefLiA = ff .
eq RefLiA ~RL mtRefList = ff .
eq ((A :: B -> C) , RefLiA) ~RL ((D :: E -> F) , RefLiB) = ((A ~iN D) and ((B ~iN E) and (C ~iN F))) and (RefLiA ~RL RefLiB) .
endfm
--- red mtRefList, (0 :: 0 -> 0) .
--- red (0 :: 0 -> 0), mtRefList .
--- red 0 :: 0 -> 0 .
--- red (0 :: 0 -> 0), (0 :: 0 -> 0) .
--- red (0 :: 0 -> 0), (s 0 :: 0 -> 0), (s 0 :: 0 -> 0), (0 :: 0 -> 0) .
--- red (0 :: 0 -> s 0), (s 0 :: 0 -> 0), (s s 0 :: 0 -> 0), (0 :: 0 -> 0), (s s s 0 :: 0 -> 0), (s 0 :: 0 -> 0), (0 :: 0 -> 0), (s s s s 0 :: 0 -> 0), (0 :: 0 -> 0) .
--- return mt list
--- red remList(mtRefList, mtRefList) .
--- red remList(mtRefList, 0 :: s 0 -> s s 0) .
--- return non-empty list
--- red remList((0 :: s 0 -> s s 0), ((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 :: s s s s s s s 0 -> s s s s s s s s 0))) .
--- red remList(((s s s s s s 0 :: s s s s s s s 0 -> s s s s s s s s 0), (0 :: s 0 -> s s 0)), ((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 :: s s s s s s s 0 -> s s s s s s s s 0))) .
--- --- union 2 mts should still be mt
--- red mtRefList U mtRefList .
--- --- union of mt and non empty should be non-empty
--- red mtRefList U 0 :: s 0 -> s s 0 .
--- red 0 :: s 0 -> s s 0 U mtRefList .
--- --- below case covers duplicates
--- red ((0 :: 0 -> 0),(s 0 :: 0 -> 0)) U ((s s 0 :: 0 -> 0),(s s s 0 :: 0 -> 0)) .
--- red ((0 :: 0 -> 0),mtRefList,(s 0 :: 0 -> 0)) U ((s 0 :: 0 -> 0),(s s s 0 :: 0 -> 0)) .
--- red lenRL(mtRefList) .
--- red lenRL(0 :: 0 -> 0) .
--- red lenRL(mtRefList, (0 :: 0 -> 0)) .
--- red lenRL((0 :: 0 -> 0), mtRefList, (s 0 :: s 0 -> s 0)) .
--- --- tt
--- red checkSubsetRefApp(mtRefList, mtRefList) .
--- --- tt
--- red checkSubsetRefApp((0 :: 0 -> 0), mtRefList) .
--- --- ff
--- red checkSubsetRefApp(mtRefList, (0 :: 0 -> 0)) .
--- --- tt
--- red checkSubsetRefApp( ( (0 :: 0 -> 0), (s 0 :: s 0 -> s 0), (s s 0 :: s s 0 -> s s 0) ) , mtRefList) .
--- --- ff
--- red checkSubsetRefApp(mtRefList, ( (0 :: 0 -> 0), (s 0 :: s 0 -> s 0), (s s 0 :: s s 0 -> s s 0) ) ) .
--- --- tt
--- red checkSubsetRefApp( ( (0 :: 0 -> 0), (s 0 :: s 0 -> s 0), (s s 0 :: s s 0 -> s s 0) ) , (s s s 0 :: s 0 -> 0) ) .
--- --- ff
--- red checkSubsetRefApp( ( (0 :: 0 -> 0), (s 0 :: s 0 -> s 0), (s s 0 :: s s 0 -> s s 0) ) , ((s s s s 0 :: s 0 -> s s s 0) , (s s s 0 :: s 0 -> 0)) ) .
--- --- tt
--- red checkSubsetRefApp( ( (0 :: 0 -> 0), (s 0 :: s 0 -> s 0), (s s 0 :: s s 0 -> s s 0) ) , ((s s s 0 :: s 0 -> 0), (s s s s 0 :: s s s s 0 -> s s 0)) ) .
--- --- ff
--- red (0 :: 0 -> 0) in mtRefList .
--- --- ff
--- red (0 :: 0 -> 0) in ((s 0 :: s 0 -> s 0) , (s s 0 :: s s 0 -> s s 0)) .
--- red (0 :: 0 -> 0) in (s 0 :: s 0 -> s 0) .
--- --- tt
--- red (0 :: 0 -> 0) in ( (0 :: 0 -> 0) , (s s 0 :: s s 0 -> s s 0)) .
--- red (0 :: 0 -> 0) in ( (s s 0 :: s s 0 -> s s 0), (0 :: 0 -> 0) ) .
--- --- tt
--- red mtRefList ~RL mtRefList .
--- red (0 :: 0 -> 0) ~RL (0 :: 0 -> 0) .
--- red (s 0 :: 0 -> 0) , (0 :: 0 -> 0) ~RL (0 :: 0 -> 0) , (s 0 :: 0 -> 0) .
--- --- ff
--- red (0 :: 0 -> 0) , (s 0 :: 0 -> 0) ~RL (0 :: 0 -> 0) .
--- red A:Reference ~RL mtRefList .
--- red mtRefList ~RL A:Reference .