source: examples/python_tests/acme_multi_rt0/multi.save @ 646e57e

mei_rt2mei_rt2_fix_1
Last change on this file since 646e57e was 646e57e, checked in by Mei <mei@…>, 12 years ago

1) add partial proof

  • Property mode set to 100644
File size: 723 bytes
Line 
1
2...final principal set...
3(pAcme,keyid,y)
4(pCoyote,keyid,y)
5
6...final policy attribute set...
7pAcme.buy_rockets <- pAcme.preferred_customer
8pAcme.buy_rockets <- pAcme.worst_lucked
9pAcme.preferred_customer <- pCoyote
10pAcme.worst_lucked <- pCoyote
11
12===good============ Acme.buy_rockets <- Coyote
13YAP query succeed
14pAcme.buy_rockets <- pAcme.preferred_customer
15pAcme.preferred_customer <- pCoyote
16
17next proof:
18pAcme.buy_rockets <- pAcme.worst_lucked
19pAcme.worst_lucked <- pCoyote
20
21next proof:
22no more..
23
24
25===good============ Acme.preferred_customer <- Coyote
26YAP query succeed
27pAcme.preferred_customer <- pCoyote
28
29next proof:
30no more..
31
32
33===bad=============== Coyote.friend <- Acme
34YAP query failed
35
36next proof:
37no more..
38
Note: See TracBrowser for help on using the repository browser.