source: examples/access_tests/creddy_prover/s5_result.save @ 11ca336

mei_rt2
Last change on this file since 11ca336 was 7f04233, checked in by Mei <mei@…>, 11 years ago

1) tweak examples
  • Property mode set to 100644
File size: 8.7 KB
Line 
1=====================s5_query.py==================
2keystore is not set, using current directory...
3
4===good============ SA.controlsQ('sliceA','info') <-?- lisa
5YAP query succeed
6pSA.controlsQ(S:pSA.standard,Priv:pPA.std_ops) <- pSA.controlsQ_(S,Priv).controlsQ(S,Priv)
7pSA.standard <- 'sliceA'
8pPA.std_ops <- 'info'
9pSA.controlsQ_(S:pSA.standard,Priv:pPA.std_ops) <- pSA.controls_(S)
10pSA.controls_(S:pSA.standard) <- pSA.owner(S)
11pSA.owner('sliceA') <- pDrd
12pDrd.controlsQ('sliceA','info') <- pLisa
13
14next proof:
15pSA.controlsQ(S:pSA.standard,Priv:pPA.std_ops) <- pSA.owner(S).controlsQ(S,Priv)
16pSA.standard <- 'sliceA'
17pPA.std_ops <- 'info'
18pSA.owner('sliceA') <- pDrd
19pDrd.controlsQ('sliceA','info') <- pLisa
20
21next proof:
22no more..
23
24
25===good============ SA.controlsQ_('sliceB','info') <-?- lisa
26YAP query succeed
27pSA.controlsQ_(S:pSA.standard,Priv:pPA.std_ops) <- pSA.delegate_controls_(S)
28pSA.standard <- 'sliceB'
29pPA.std_ops <- 'info'
30pSA.delegate_controls_('sliceB') <- pLisa
31
32===good============ SA.controlsQ_('sliceB','info') <-?- James
33YAP query succeed
34pSA.controlsQ_(S:pSA.standard,Priv:pPA.std_ops) <- pSA.delegate_controlsQ_(S,Priv).controlsQ_(S,Priv)
35pSA.standard <- 'sliceB'
36pPA.std_ops <- 'info'
37pSA.delegate_controlsQ_('sliceB','info') <- pJohn
38pJohn.controlsQ_('sliceB','info') <- pJames
39
40===good============ SA.controlsQ('sliceB','info') <-?- Dan
41YAP query succeed
42pSA.controlsQ(S:pSA.standard,Priv:pPA.std_ops) <- pSA.controls(S)
43pSA.standard <- 'sliceB'
44pPA.std_ops <- 'info'
45pSA.controls('sliceB') <- pDan
46
47===good============ SA.controlsQ('sliceA','info') <-?- John
48YAP query succeed
49pSA.controlsQ(S:pSA.standard,Priv:pPA.std_ops) <- pSA.controlsQ_(S,Priv)
50pSA.standard <- 'sliceA'
51pPA.std_ops <- 'info'
52pSA.controlsQ_(S:pSA.standard,Priv:pPA.std_ops) <- pSA.delegate_controlsQ_(S,Priv)
53pSA.delegate_controlsQ_(S:pSA.standard,Priv:pPA.std_ops) <- pSA.owner(S).delegate_controlsQ_(S,Priv)
54pSA.owner('sliceA') <- pDrd
55pDrd.delegate_controlsQ_('sliceA','info') <- pJohn
56
57===bad============ SA.controlsQ('sliceB','instantiate') <-?- John
58YAP query failed
59A partial proof(type:what)
60pSA.delegate_controlsQ_('sliceB','info') <- pJohn
61
62===bad============ SA.controlsQ('sliceB','instantiate') <-?- Tim
63YAP query failed
64A partial proof(type:what)
65pSA.controlsQ_(S:pSA.standard,Priv:pPA.std_ops) <- pSA.delegate_controlsQ_(S,Priv)
66pSA.standard <- 'sliceA'
67pPA.std_ops <- 'instantiate'
68pSA.delegate_controlsQ_(S:pSA.standard,Priv:pPA.std_ops) <- pSA.owner(S).delegate_controlsQ_(S,Priv)
69pSA.owner('sliceA') <- pDrd
70pDrd.delegate_controlsQ_('sliceA','instantiate') <- pTim
71
72===bad============ SA.controlsQ('sliceB','info') <-?- Tim
73YAP query failed
74A partial proof(type:what)
75pSA.controlsQ_(S:pSA.standard,Priv:pPA.std_ops) <- pSA.delegate_controlsQ_(S,Priv)
76pSA.standard <- 'sliceA'
77pPA.std_ops <- 'instantiate'
78pSA.delegate_controlsQ_(S:pSA.standard,Priv:pPA.std_ops) <- pSA.owner(S).delegate_controlsQ_(S,Priv)
79pSA.owner('sliceA') <- pDrd
80pDrd.delegate_controlsQ_('sliceA','instantiate') <- pTim
81
82===good============ SA.controlsQ('sliceB','info') <-?- Joe
83YAP query succeed
84pSA.controlsQ(S:pSA.standard,Priv:pPA.std_ops) <- pSA.controlsQ_(S,Priv)
85pSA.standard <- 'sliceB'
86pPA.std_ops <- 'info'
87pSA.controlsQ_(S:pSA.standard,Priv:pPA.std_ops) <- pSA.delegate_controlsQ_(S,Priv)
88pSA.delegate_controlsQ_('sliceB','info') <- pJohn
89
90
91
92=====================s5_run_query==================
93 
94===bad============ PA.controlsQ_(sliceA,'info')<-?-Dan
95YAP query failed
96prover failed!!
97 
98===good============ PA.controlsQ(sliceA,'info')<-?-Dan
99YAP query succeed
100prover success!!
101credentials needed :
102 pSA.controlsQ('sliceA','info')  <- pDan
103 
104===bad============ PA.controlsQ_(sliceA,'stop')<-?-Dan
105YAP query failed
106prover failed!!
107 
108===good============ PA.controlsQ(sliceA,'stop')<-?-Dan
109YAP query succeed
110prover success!!
111credentials needed :
112 pSA.controlsQ('sliceA','stop')  <- pDan
113 
114===good============ PA.controlsQ_(sliceA,'info')<-?-Frank
115YAP query succeed
116prover success!!
117credentials needed :
118 pSA.controlsQ_('sliceA','info')  <- pFrank
119 
120===good============ PA.controlsQ(sliceA,'info')<-?-Frank
121YAP query succeed
122prover success!!
123credentials needed :
124 pSA.controlsQ(S:pSA.standard,Priv:pPA.std_ops)  <- pSA.controlsQ_(S,Priv)
125 pSA.standard  <- 'sliceA'
126 pPA.std_ops  <- 'info'
127 pSA.controlsQ_('sliceA','info')  <- pFrank
128 
129===good============ PA.controlsQ_(sliceA,'stop')<-?-Frank
130YAP query succeed
131prover success!!
132credentials needed :
133 pSA.controlsQ_('sliceA','stop')  <- pFrank
134 
135===good============ PA.controlsQ(sliceA,'stop')<-?-Frank
136YAP query succeed
137prover success!!
138credentials needed :
139 pSA.controlsQ(S:pSA.standard,Priv:pPA.std_ops)  <- pSA.controlsQ_(S,Priv)
140 pSA.standard  <- 'sliceA'
141 pPA.std_ops  <- 'stop'
142 pSA.controlsQ_('sliceA','stop')  <- pFrank
143 
144===bad============ PA.controlsQ_(sliceA,'info')<-?-James
145YAP query succeed
146prover success!!
147credentials needed :
148 pSA.controlsQ_(S:pSA.standard,Priv:pPA.std_ops)  <- pSA.delegate_controlsQ_(S,Priv)
149 pSA.standard  <- 'sliceA'
150 pPA.std_ops  <- 'info'
151 pSA.delegate_controlsQ_('sliceA','info')  <- pJames
152 
153===good============ PA.controlsQ(sliceA,'info')<-?-James
154YAP query succeed
155prover success!!
156credentials needed :
157 pSA.controlsQ(S:pSA.standard,Priv:pPA.std_ops)  <- pSA.controlsQ_(S,Priv)
158 pSA.standard  <- 'sliceA'
159 pPA.std_ops  <- 'info'
160 pSA.controlsQ_(S:pSA.standard,Priv:pPA.std_ops)  <- pSA.delegate_controlsQ_(S,Priv)
161 pSA.delegate_controlsQ_('sliceA','info')  <- pJames
162 
163===bad============ PA.controlsQ_(sliceA,'stop')<-?-James
164YAP query failed
165prover failed!!
166 
167===good============ PA.controlsQ(sliceA,'stop')<-?-James
168YAP query succeed
169prover success!!
170credentials needed :
171 pSA.controlsQ(S:pSA.standard,Priv:pPA.std_ops)  <- pSA.controlsQ_(S,Priv).controlsQ(S,Priv)
172 pSA.standard  <- 'sliceA'
173 pPA.std_ops  <- 'stop'
174 pSA.controlsQ_(S:pSA.standard,Priv:pPA.std_ops)  <- pSA.controls_(S)
175 pSA.controls_(S:pSA.standard)  <- pSA.owner(S)
176 pSA.owner('sliceA')  <- pDrd
177 pDrd.controlsQ('sliceA','stop')  <- pJames
178 
179===bad============ PA.controlsQ_(sliceA,'info')<-?-Lisa
180YAP query failed
181prover failed!!
182 
183===good============ PA.controlsQ(sliceA,'info')<-?-Lisa
184YAP query succeed
185prover success!!
186credentials needed :
187 pSA.controlsQ(S:pSA.standard,Priv:pPA.std_ops)  <- pSA.controlsQ_(S,Priv).controlsQ(S,Priv)
188 pSA.standard  <- 'sliceA'
189 pPA.std_ops  <- 'info'
190 pSA.controlsQ_(S:pSA.standard,Priv:pPA.std_ops)  <- pSA.controls_(S)
191 pSA.controls_(S:pSA.standard)  <- pSA.owner(S)
192 pSA.owner('sliceA')  <- pDrd
193 pDrd.controlsQ('sliceA','info')  <- pLisa
194 
195===good============ PA.controlsQ_(sliceA,'stop')<-?-Lisa
196YAP query succeed
197prover success!!
198credentials needed :
199 pSA.controlsQ_(S:pSA.standard,Priv:pPA.std_ops)  <- pSA.delegate_controlsQ_(S,Priv)
200 pSA.standard  <- 'sliceA'
201 pPA.std_ops  <- 'stop'
202 pSA.delegate_controlsQ_('sliceA','stop')  <- pLisa
203 
204===good============ PA.controlsQ(sliceA,'stop')<-?-Lisa
205YAP query succeed
206prover success!!
207credentials needed :
208 pSA.controlsQ(S:pSA.standard,Priv:pPA.std_ops)  <- pSA.controlsQ_(S,Priv)
209 pSA.standard  <- 'sliceA'
210 pPA.std_ops  <- 'stop'
211 pSA.controlsQ_(S:pSA.standard,Priv:pPA.std_ops)  <- pSA.delegate_controlsQ_(S,Priv)
212 pSA.delegate_controlsQ_('sliceA','stop')  <- pLisa
213 
214===good============ PA.controlsQ_(sliceA,'info')<-?-Tim
215YAP query succeed
216prover success!!
217credentials needed :
218 pSA.controlsQ_(S:pSA.standard,Priv:pPA.std_ops)  <- pSA.owner(S).controlsQ_(S,Priv)
219 pSA.standard  <- 'sliceA'
220 pPA.std_ops  <- 'info'
221 pSA.owner('sliceA')  <- pDrd
222 pDrd.controlsQ_('sliceA','info')  <- pTim
223 
224===good============ PA.controlsQ(sliceA,'info')<-?-Tim
225YAP query succeed
226prover success!!
227credentials needed :
228 pSA.controlsQ(S:pSA.standard,Priv:pPA.std_ops)  <- pSA.controlsQ_(S,Priv)
229 pSA.standard  <- 'sliceA'
230 pPA.std_ops  <- 'info'
231 pSA.controlsQ_(S:pSA.standard,Priv:pPA.std_ops)  <- pSA.owner(S).controlsQ_(S,Priv)
232 pSA.owner('sliceA')  <- pDrd
233 pDrd.controlsQ_('sliceA','info')  <- pTim
234 
235===good============ PA.controlsQ_(sliceA,'stop')<-?-Tim
236YAP query succeed
237prover success!!
238credentials needed :
239 pSA.controlsQ_(S:pSA.standard,Priv:pPA.std_ops)  <- pSA.owner(S).controlsQ_(S,Priv)
240 pSA.standard  <- 'sliceA'
241 pPA.std_ops  <- 'stop'
242 pSA.owner('sliceA')  <- pDrd
243 pDrd.controlsQ_('sliceA','stop')  <- pTim
244 
245===good============ PA.controlsQ(sliceA,'stop')<-?-Tim
246YAP query succeed
247prover success!!
248credentials needed :
249 pSA.controlsQ(S:pSA.standard,Priv:pPA.std_ops)  <- pSA.controlsQ_(S,Priv)
250 pSA.standard  <- 'sliceA'
251 pPA.std_ops  <- 'stop'
252 pSA.controlsQ_(S:pSA.standard,Priv:pPA.std_ops)  <- pSA.owner(S).controlsQ_(S,Priv)
253 pSA.owner('sliceA')  <- pDrd
254 pDrd.controlsQ_('sliceA','stop')  <- pTim
255 
256===good============ John.controlsQ(sliceB,info)<-?-$ Joe
257YAP query succeed
258prover success!!
259credentials needed :
260 pJohn.controlsQ('sliceB','info')  <- pJoe
261
262
263
Note: See TracBrowser for help on using the repository browser.