blob: 707e2c36930042e3d8b78dad23488a9d16029c2f (
plain)
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
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
|
; EXPECT: unsat
; COMMAND-LINE: --sygus-out=status --lang=sygus2
(set-logic ALL)
(declare-datatype Packet ((P1) (P2)))
(declare-datatype Node ((A) (B) (C)))
(declare-datatype SPair ((mkPair (pnode Node) (ppacket Packet))))
(declare-datatype State ((mkState (rcv (Array SPair Bool)))))
(declare-datatype StateList ((consSL (headSL State) (tailSL StateList)) (nilSL)))
; C is destination of P1 and P2
(define-fun h_State ((s State)) Real
(+
(ite (select (rcv s) (mkPair C P1)) 1.0 0.0)
(ite (select (rcv s) (mkPair C P2)) 1.0 0.0)
)
)
; reliability
(define-fun rel () Real 0.7)
; new chance of success
(define-fun updateReal ((addP Real) (currP Real)) Real
(+ currP (* (- 1.0 currP) addP))
)
; Actions and how they are interpreted
(declare-datatype Action (
(sleep)
(pushPck (push_dst Node) (push_pck Packet))
(pullPck (pull_src Node) (pull_pck Packet))
))
(declare-datatype ActionList ((consAL (headA Action) (tailA ActionList)) (nilAL)))
;; returns true if action is valid for actor in state s
(define-fun preconditionAction ((actor Node) (a Action) (s State)) Bool
(let ((rcv (rcv s)))
(ite ((_ is pullPck) a)
(let ((pck (pull_pck a)))
; don't pull if already recieved the packet
(not (select rcv (mkPair actor pck)))
)
true
)
)
)
; which action fires in state s?
(define-fun-rec actionListToAction ((actor Node) (al ActionList) (s State)) Action
(ite ((_ is consAL) al)
(let ((a (headA al)))
(ite (preconditionAction actor a s)
a
(actionListToAction actor (tailA al) s)
)
)
sleep
)
)
(declare-datatype PState ((mkPState (states StateList) (prob (Array State Real)))))
(define-fun-rec h_PState_rec ((pssl StateList) (pspb (Array State Real))) Real
(ite ((_ is consSL) pssl)
(let ((s (headSL pssl)))
(+ (* (select pspb s) (h_State s)) (h_PState_rec (tailSL pssl) pspb))
)
0.0)
)
(define-fun h_PState ((ps PState)) Real
(h_PState_rec (states ps) (prob ps))
)
(define-fun nilPState () PState
(mkPState nilSL ((as const (Array State Real)) 0))
)
(define-fun-rec appendStateToPState ((s State) (r Real) (p PState)) PState
(let ((pstates (states p)))
(let ((pprob (prob p)))
(let ((pr (select pprob s)))
(mkPState
; add to list if not there already
(ite (= pr 0.0)
(consSL s pstates)
pstates
)
(store
pprob
s (+ r pr)
)
)
)))
)
(define-fun transNode ((actor Node) (a Action) (r Real) (s State) (psp PState)) PState
(let ((prevRcv (rcv s)))
(ite ((_ is pushPck) a)
(let ((dst (push_dst a)))
(let ((pck (push_pck a)))
(let ((dst_pair (mkPair dst pck)))
(let ((src_pair (mkPair actor pck)))
(let ((chSuccess (ite (select prevRcv src_pair) rel 0.0)))
; success and failure
(appendStateToPState
(mkState (store prevRcv dst_pair true))
(* r chSuccess)
(appendStateToPState
s
(* r (- 1.0 chSuccess))
psp
))
)))))
(ite ((_ is pullPck) a)
(let ((src (pull_src a)))
(let ((pck (pull_pck a)))
(let ((dst_pair (mkPair actor pck)))
(let ((src_pair (mkPair src pck)))
(let ((chSuccess (ite (select prevRcv src_pair) rel 0.0)))
; success and failure
(appendStateToPState
(mkState (store prevRcv dst_pair true))
(* r chSuccess)
(appendStateToPState
s
(* r (- 1.0 chSuccess))
psp
))
)))))
(appendStateToPState
s
r
psp)
))
)
)
(define-fun-rec transNodeListRec ((actor Node) (al ActionList) (ps PState) (pssl StateList) (psp PState)) PState
; if more states to consider in s
(ite ((_ is consSL) pssl)
(let ((s (headSL pssl)))
(let ((r (select (prob ps) s)))
(transNode actor (actionListToAction actor al s) r s
(transNodeListRec actor al ps (tailSL pssl) psp))
))
psp)
)
(define-fun-rec transNodeList ((actor Node) (al ActionList) (ps PState) (psp PState)) PState
(transNodeListRec actor al ps (states ps) psp)
)
(define-fun trans ((aa ActionList) (ab ActionList) (ac ActionList) (ps PState)) PState
;(transNodeList A aa ps
;(transNodeList B ab ps
(transNodeList C ac ps
nilPState);))
)
(synth-fun actionA () ActionList
((GAL ActionList) (GA Action) (GN Node) (GP Packet))
(
(GAL ActionList (nilAL))
(GA Action ((pushPck GN GP) (pullPck GN GP)))
(GN Node (B C))
(GP Packet (P1 P2))
)
)
(synth-fun actionB () ActionList
((GAL ActionList) (GA Action) (GN Node) (GP Packet))
(
(GAL ActionList (nilAL))
(GA Action ((pushPck GN GP) (pullPck GN GP)))
(GN Node (A C))
(GP Packet (P1 P2))
)
)
(synth-fun actionC () ActionList
((GAL ActionList) (GA Action) (GN Node) (GP Packet))
(
(GAL ActionList ((consAL GA GAL) nilAL))
(GA Action ((pushPck GN GP) (pullPck GN GP)))
(GN Node (A B))
(GP Packet (P1 P2))
)
)
; A and B initially have packets P1 and P2
(define-fun init-state () State
(mkState
(store
(store
((as const (Array SPair Bool)) false)
(mkPair B P2) true
)
(mkPair A P1) true
)
)
)
(define-fun init-pstate () PState
(appendStateToPState init-state 1.0 nilPState)
)
; expected value of packets is greater than 1.0 after 2 time steps.
(constraint
(< 1.0 (h_PState
(trans actionA actionB actionC (trans actionA actionB actionC init-pstate))
))
)
(check-synth)
|
