source: examples/creddy_prover_tests/allout.save @ e97d2e2

mei_rt2_fix_1
Last change on this file since e97d2e2 was abf8d5d, checked in by Mei <mei@…>, 12 years ago

1) add backtrack/multiple solutions proof code changes and new

examples.
  • Property mode set to 100644
File size: 8.8 KB
RevLine 
[f0eb81d]1
[5110d42]2 ==> RUN on access_rt2
[f0eb81d]3 
[9502c50]4===good============ Alpha.access(Read,fileA)<-?-Bob
[f0eb81d]5YAP query succeed
6prover success!!
7credentials needed :
[7727f26]8 pAlpha.access('Read',F:pAlpha.documents(P))  <- pAlpha.team(P)
9 pAlpha.documents('proj1')  <- 'file//fileA'
10 pAlpha.team('proj1')  <- pBob
[f0eb81d]11 
[9502c50]12===bad============ Alpha.access(Read,fileA)<-?-Joe
[f0eb81d]13YAP query failed
14prover failed!!
15 
[9502c50]16===good============ Alpha.team(proj2)<-?-Joe
[f0eb81d]17YAP query succeed
18prover success!!
19credentials needed :
[7727f26]20 pAlpha.team('proj2')  <- pJoe
[f0eb81d]21
[5110d42]22 ==> RUN on acme_friend_rt1
[f0eb81d]23 
[9502c50]24===bad============ Acme.friendOf(Roadrunner) <- Coyote
[f0eb81d]25YAP query failed
26prover failed!!
27 
[9502c50]28===good============ Acme.friendOf(Roadrunner) <- Jackrabbit
[f0eb81d]29YAP query succeed
30prover success!!
31credentials needed :
[7727f26]32 pAcme.friendOf(pRoadrunner)  <- pJackrabbit
[f0eb81d]33 
[9502c50]34===good============ Acme.preferred_customer <- Jackrabbit
[f0eb81d]35YAP query succeed
36prover success!!
37credentials needed :
[7727f26]38 pAcme.preferred_customer  <- pAcme.friendOf(pRoadrunner)
39 pAcme.friendOf(pRoadrunner)  <- pJackrabbit
[f0eb81d]40 
[9502c50]41===good============ Acme.preferred_customer <- Coyote
[f0eb81d]42YAP query succeed
43prover success!!
44credentials needed :
[7727f26]45 pAcme.preferred_customer  <- pCoyote
[f0eb81d]46 
[9502c50]47===bad============ Acme.preferred_customer <- badCoyote
[d9c3886]48yyerror: encountered an invalid SHA id
[f0eb81d]49prover failed!!
50
[5110d42]51 ==> RUN on acme_rockets_intersection_rt0
[f0eb81d]52 
[9502c50]53===good============ Acme.buy_rockets <- Coyote
[f0eb81d]54YAP query succeed
55prover success!!
56credentials needed :
[7727f26]57 pAcme.buy_rockets  <- pAcme.preferred_customer & pWarnerBros.character
58 pAcme.preferred_customer  <- pCoyote
59 pWarnerBros.character  <- pCoyote
[f0eb81d]60 
[9502c50]61===bad============ Acme.bad_buy_rockets <- Coyote
[f0eb81d]62YAP query failed
63prover failed!!
64 
[9502c50]65===bad============ 99Acme.buy_rockets <- Coyote
[d9c3886]66yyerror: encountered an invalid SHA id
[f0eb81d]67prover failed!!
68 
[9502c50]69===bad=============== Acme.buy_rockets <- Batman
[f0eb81d]70YAP query failed
71prover failed!!
72
[5110d42]73 ==> RUN on acme_rockets_rt0
[f0eb81d]74 
[9502c50]75===good============ Acme.preferred_customer <- Coyote
[f0eb81d]76YAP query succeed
77prover success!!
78credentials needed :
[7727f26]79 pAcme.preferred_customer  <- pCoyote
[f0eb81d]80 
[9502c50]81===good=============== Acme.buy_rockets <- Coyote
[f0eb81d]82YAP query succeed
83prover success!!
84credentials needed :
[7727f26]85 pAcme.buy_rockets  <- pAcme.preferred_customer
86 pAcme.preferred_customer  <- pCoyote
[f0eb81d]87 
[9502c50]88===bad=============== Acme.buy_rockets <- Acme.preferred_customer
[8bd77b5]89fail, a.o <- b.o and a.r <- a.r query is not implemented yet !!!
[f0eb81d]90 
[9502c50]91===bad=============== Coyote.friend <- Acme
[f0eb81d]92YAP query failed
93prover failed!!
94
[5110d42]95 ==> RUN on alice_rt1
[f0eb81d]96 
[9502c50]97===good============ Party.guests <- dourmouse
[f0eb81d]98YAP query succeed
99prover success!!
100credentials needed :
[7727f26]101 pParty.guests  <- pParty.friendOf(pMarchHare)
102 pParty.friendOf(pMarchHare)  <- pDormouse
[f0eb81d]103 
[9502c50]104===bad============ Party.guests <- hatter
[f0eb81d]105YAP query failed
106prover failed!!
107
[5110d42]108 ==> RUN on alumni2_rt1
[f0eb81d]109 
[9502c50]110===good============ stateU.foundingAlumni <- Bob
[f0eb81d]111YAP query succeed
112prover success!!
113credentials needed :
[2efdff5]114 pStateU.foundingAlumni  <- pStateU.diploma(_,Year:[1960,1961,1963])
[7727f26]115 pStateU.diploma('mathmatics',1961)  <- pBob
[f0eb81d]116 
[9502c50]117===bad============ stateU.foundingAlumni <- Maryann
[f0eb81d]118YAP query failed
119prover failed!!
120 
[9502c50]121===bad============ stateU.foundingAlumni <- Joe
[f0eb81d]122YAP query failed
123prover failed!!
124
[5110d42]125 ==> RUN on alumni3_rt1
[f0eb81d]126 
[9502c50]127===good============ stateU.foundingAlumni <- Bob
[f0eb81d]128YAP query succeed
129prover success!!
130credentials needed :
[2efdff5]131 pStateU.foundingAlumni  <- pStateU.diploma(D:['mathmatics','psychology'],Year:[1960,1961,1963])
[7727f26]132 pStateU.diploma('mathmatics',1961)  <- pBob
[f0eb81d]133 
[9502c50]134===bad============ stateU.foundingAlumni <- Mark
[f0eb81d]135YAP query failed
136prover failed!!
137 
[9502c50]138===bad============ stateU.foundingAlumni <- Joe
[f0eb81d]139YAP query failed
140prover failed!!
141 
[9502c50]142===bad============ stateU.foundingAlumni <- Maryann
[f0eb81d]143YAP query failed
144prover failed!!
145 
[9502c50]146===good============ stateU.foundingAlumni <- Jan
[f0eb81d]147YAP query succeed
148prover success!!
149credentials needed :
[2efdff5]150 pStateU.foundingAlumni  <- pStateU.diploma(D:['mathmatics','psychology'],Year:[1960,1961,1963])
[7727f26]151 pStateU.diploma('psychology',1960)  <- pJan
[f0eb81d]152
[5110d42]153 ==> RUN on alumni_rt1
[f0eb81d]154 
[9502c50]155===bad============ stateU.foundingAlumni <- Bob
[f0eb81d]156YAP query failed
157prover failed!!
158 
[9502c50]159===good============ stateU.foundingAlumni <- Maryann
[f0eb81d]160YAP query succeed
161prover success!!
162credentials needed :
[2efdff5]163 pStateU.foundingAlumni  <- pStateU.diploma(_,Year:[1955..1958])
[7727f26]164 pStateU.diploma('psychology',1956)  <- pMaryann
[7b548fa]165 
[9502c50]166===good============ stateU.foundingAlumni <- Joe
[7b548fa]167YAP query succeed
168prover success!!
169credentials needed :
[2efdff5]170 pStateU.foundingAlumni  <- pStateU.diploma(_,Year:[1955..1958])
[7727f26]171 pStateU.diploma('zoology',1955)  <- pJoe
[7b548fa]172
[5110d42]173 ==> RUN on balltime_rt2
[7b548fa]174 
[9502c50]175===good============ league.stadium(access,true,20120128T130000)<-?-john
[7b548fa]176YAP query succeed
177prover success!!
178credentials needed :
[7727f26]179 pLeague.stadium('access',true,F:pLeague.gametime(T))  <- pLeague.players(T)
[2efdff5]180 pLeague.gametime('north')  <- 20120228T130000
[7727f26]181 pLeague.players('north')  <- pJohn
[7b548fa]182 
[9502c50]183===bad============ league.stadium(access,true,20120128T110000)<-?-mark
[7b548fa]184YAP query failed
185prover failed!!
186 
[9502c50]187===good============ league.stadium(access,true,20120128T080000)<-?-mark
[7b548fa]188YAP query succeed
189prover success!!
190credentials needed :
[2efdff5]191 pLeague.stadium('access',B:[true],F:[20120228T080000..20120228T090000])  <- pLeague.players(T)
[7727f26]192 pLeague.players('south')  <- pMark
[f0eb81d]193
[5110d42]194 ==> RUN on evaluator_rt1
[f0eb81d]195 
[9502c50]196===good============ USC.evaluatorOf(Maryann) <- John
[f0eb81d]197YAP query succeed
198prover success!!
199credentials needed :
[7727f26]200 pUSC.evaluatorOf(K)  <- pUSC.managerOf(K)
201 pUSC.managerOf(K)  <- pISI.managerOf(K)
202 pISI.managerOf(pMaryann)  <- pJohn
[f0eb81d]203 
[9502c50]204===good============ ISI.managerOf(Maryann) <- John
[f0eb81d]205YAP query succeed
206prover success!!
207credentials needed :
[7727f26]208 pISI.managerOf(pMaryann)  <- pJohn
[f0eb81d]209 
[9502c50]210===good============  USC.employee <-?- John
[f0eb81d]211YAP query succeed
212prover success!!
213credentials needed :
[7727f26]214 pUSC.employee  <- pISI.employee
215 pISI.employee  <- pJohn
[f0eb81d]216
[5110d42]217 ==> RUN on experiment_create_rt0
[f0eb81d]218 
[9502c50]219===good=============== Globotron.admin <- Alice
[f0eb81d]220YAP query succeed
221prover success!!
222credentials needed :
[7727f26]223 pGlobotron.admin  <- pAlice
[f0eb81d]224 
[9502c50]225===bad=============== Globotron.admin <- Bob
[f0eb81d]226YAP query failed
227prover failed!!
228 
[9502c50]229===good=============== Acme.experiment_create <- Bob
[f0eb81d]230YAP query succeed
231prover success!!
232credentials needed :
[7727f26]233 pAcme.experiment_create  <- pAcme.partner.experiment_create
234 pAcme.partner  <- pGlobotron
235 pGlobotron.experiment_create  <- pGlobotron.admin.power_user
236 pGlobotron.admin  <- pAlice
237 pAlice.power_user  <- pBob
[f0eb81d]238
[5110d42]239 ==> RUN on file_read_rt2
[f0eb81d]240 
[9502c50]241===good============ alpha.read(fileA) <- Bob
[f0eb81d]242YAP query succeed
243prover success!!
244credentials needed :
[7727f26]245 pAlpha.read(F)  <- pAlpha.managerOf(E:pAlpha.ownerOf(F))
246 pAlpha.ownerOf('file://fileA')  <- pJoe
247 pAlpha.managerOf(pJoe)  <- pBob
[f0eb81d]248 
[9502c50]249===bad============ alpha.read(fileA) <- Maryann
[f0eb81d]250YAP query failed
251prover failed!!
252
[5110d42]253 ==> RUN on fruits_rt2
[f0eb81d]254 
[9502c50]255===good============ mary.what2eat <- navel orange
[f0eb81d]256YAP query succeed
257prover success!!
258credentials needed :
[2efdff5]259 pMary.what2eat  <- pRalphs.fruitprice(P:[..2.00])
[7727f26]260 pRalphs.fruitprice(0.50)  <- 'navel orange'
[f0eb81d]261 
[9502c50]262===good============ mary.what2eat <- kiwi
[f0eb81d]263YAP query succeed
264prover success!!
265credentials needed :
[2efdff5]266 pMary.what2eat  <- pRalphs.fruitprice(P:[..2.00])
[7727f26]267 pRalphs.fruitprice(1.50)  <- 'kiwi'
[f0eb81d]268 
[9502c50]269===bad============ bob.what2eat <- navel orange
[f0eb81d]270YAP query failed
271prover failed!!
272 
[9502c50]273===good============ ralphs.fruitprice(1.50) <- apple
[f0eb81d]274YAP query succeed
275prover success!!
276credentials needed :
[7727f26]277 pRalphs.fruitprice(1.50)  <- 'apple'
[f0eb81d]278 
[9502c50]279===bad============ ralphs.fruitprice(1.50) <- green apple
[f0eb81d]280YAP query failed
281prover failed!!
[9335cfa]282
[5110d42]283 ==> RUN on leader_rt1
[8bd77b5]284 
285===yes============ geni.leader <- Bob
286YAP query succeed
287prover success!!
288credentials needed :
289 pGeni.leader  <- pBob
290 
291===no============ geni.leader <- Jack
292YAP query failed
293prover failed!!
294 
295===yes============ geni.leader <- Joe
296YAP query succeed
297prover success!!
298credentials needed :
299 pGeni.leader  <- pGeni.equivalent(P:pGeni.leader)
300 pGeni.leader  <- pBob
301 pGeni.equivalent(pBob)  <- pJoe
302
[5110d42]303 ==> RUN on payraise_rt1
[9335cfa]304 
305===bad============ alpha.payRaise <- Joe
306YAP query failed
307prover failed!!
308 
309===good============ alpha.payRaise <- Maryann
310YAP query succeed
311prover success!!
312credentials needed :
313 pAlpha.payRaise  <- pAlpha.evaluatorOf(This).goodPerformance & pAlpha.managerOf(This).niceCoworker
314 pAlpha.evaluatorOf(pMaryann)  <- pBob
315 pBob.goodPerformance  <- pMaryann
316 pAlpha.managerOf(Z)  <- pAlpha.evaluatorOf(Z)
317 pBob.niceCoworker  <- pMaryann
[abf8d5d]318
319 ==> RUN on acme_multi_rt0
320 
321===good============ Acme.preferred_customer <- Coyote
322YAP query succeed
323prover success!!
324credentials needed :
325 pAcme.preferred_customer  <- pCoyote
326 
327===good=============== Acme.buy_rockets <- Coyote
328YAP query succeed
329prover success!!
330credentials needed :
331 pAcme.buy_rockets  <- pAcme.preferred_customer
332 pAcme.preferred_customer  <- pCoyote
333another proof!!
334credentials needed :
335 pAcme.buy_rockets  <- pAcme.worst_lucked
336 pAcme.worst_lucked  <- pCoyote
337no more!!
338 
339===bad=============== Acme.buy_rockets <- Acme.preferred_customer
340fail, a.o <- b.o and a.r <- a.r query is not implemented yet !!!
341 
342===bad=============== Coyote.friend <- Acme
343YAP query failed
344prover failed!!
Note: See TracBrowser for help on using the repository browser.