RiSE4fun samples for CounterdogList of built-in samples for the Counterdog in RiSE4funen-US<a target='_blank' href='https://go.microsoft.com/?linkid=2028325'>Contact Us</a>| <a target='_blank' href='https://go.microsoft.com/fwlink/?LinkId=521839'>Privacy &amp; Cookies</a> | <a target='_blank' href='https://go.microsoft.com/fwlink/?LinkID=246338'>Terms of Use</a> | <a target='_blank' href='https://go.microsoft.com/fwlink/?LinkId=506942 '>Trademarks</a>| &copy; 2017 Microsofthttps://rise4fun.com//Images/Rise.gifRiSE4fun samples for Counterdoghttps://rise4fun.com/Counterdog/axiom_c1axiom_c1|- ! G : ^Program. [G]Ghttps://rise4fun.com/Counterdog/prop3prop3|- ! Phi : ^Property. Phi <--> [True] Phihttps://rise4fun.com/Counterdog/prop4prop4|- ! P : ^Property+. ! G : ^Program. P --> [G] Phttps://rise4fun.com/Counterdog/prop6prop6|- ! P : ^Property. q --> ([p] P <--> [p:-q] P)https://rise4fun.com/Counterdog/axiom_c2axiom_c2|- ! G : ^Program. ! P : ^Property. [G]P --> G --> Phttps://rise4fun.com/Counterdog/axiom_funaxiom_fun|- ! G : ^Program. ! P : ^Property. [G]~P <--> ~[G]Phttps://rise4fun.com/Counterdog/prop9prop9|- ! P : ^Property. ! G : ^Program. G --> (P <--> [G] P)https://rise4fun.com/Counterdog/axiom_permaxiom_perm|- ! G,G' : ^Program. ! P : ^Property. [G; G']~P <--> ~[G][G']Phttps://rise4fun.com/Counterdog/prop5prop5|- ! P : ^Property. ! G, G' : ^Program. [G] [G'] P <--> [G'] [G] Phttps://rise4fun.com/Counterdog/prop7prop7|- ! P : ^Property+. ! G1, G2 : ^Program. [G1] G2 & [G2] P --> [G1] Phttps://rise4fun.com/Counterdog/axiom_kaxiom_k|- ! G : ^Program. ! P, P' : ^Property. [G](P --> P') --> [G]P --> [G]P'https://rise4fun.com/Counterdog/prop2prop2|- ! P, P' : ^Property. ! G : ^Program. [G] (P | P') <--> [G] P | [G] P'https://rise4fun.com/Counterdog/prop1prop1|- ! P, P' : ^Property. ! G : ^Program. [G] (P & P') <--> [G] P & [G] P'https://rise4fun.com/Counterdog/axiom_dlogaxiom_dlog// PropertyC are all classical, i.e. box-free, properties |- ! P : ^PropertyC. [a:-b] P --> (b --> a) --> Phttps://rise4fun.com/Counterdog/testcase6testcase6|- [canRead(11,1,111); owns(2,11,111); isMember(2,11)] (canExecute(1,11,111) & ~isBanned(1,11)) & ~[owns(2,11,111); isMember(2,11)] (canExecute(1,11,111) & ~isBanned(1,11)) & ~[canRead(11,1,111) :- isMember(1,22); owns(2,11,111); isMember(2,11)] (canExecute(1,11,111) & ~isBanned(1,11)) --> ~isMember(1,22)https://rise4fun.com/Counterdog/testcase3testcase3|- {canRead(11,1,111) :- isMember(1,22);p1; p2; p3} [canRead(11,1,111); owns(2,11,111); isMember(2,11)] canExecute(1,11,111) & { owns(2,11,111); isMember(2,11); canRead(11,1,111) :- isMember(1,22);p1; p2; p3} ~ canExecute(1,11,111) & { canRead(11,1,111); isMember(2,11); canRead(11,1,111) :- isMember(1,22);p1; p2; p3} ~ canExecute(1,11,111) & { canRead(11,1,111); owns(2,11,111); canRead(11,1,111) :- isMember(1,22);p1; p2; p3} ~ canExecute(1,11,111) --> ~ isMember(1,22)https://rise4fun.com/Counterdog/testcase1testcase1|- [canRead(11,1,111); canRead(11,1,111) :- isMember(1,22); owns(2,11,111); isMember(2,11)] canExecute(1,11,111) & ~[canRead(11,1,111); canRead(11,1,111) :- isMember(1,22); owns(2,11,111)] canExecute(1,11,111) & ~[canRead(11,1,111); canRead(11,1,111) :- isMember(1,22); isMember(2,11)] canExecute(1,11,111) & ~[canRead(11,1,111); canRead(11,1,111) :- isMember(1,22)] canExecute(1,11,111) & [canRead(11,1,111); owns(2,11,111); isMember(2,11)] canExecute(1,11,111) & ~[canRead(11,1,111); owns(2,11,111)] canExecute(1,11,111) & ~[canRead(11,1,111); isMember(2,11)] canExecute(1,11,111) & ~[canRead(11,1,111)] canExecute(1,11,111) & ~[canRead(11,1,111) :- isMember(1,22); owns(2,11,111); isMember(2,11)] canExecute(1,11,111) & ~[canRead(11,1,111) :- isMember(1,22); owns(2,11,111)] canExecute(1,11,111) & ~[canRead(11,1,111) :- isMember(1,22); isMember(2,11)] canExecute(1,11,111) & ~[canRead(11,1,111) :- isMember(1,22)] canExecute(1,11,111) & ~[owns(2,11,111); isMember(2,11)] canExecute(1,11,111) & ~[owns(2,11,111)] canExecute(1,11,111) & ~[isMember(2,11)] canExecute(1,11,111) & ~canExecute(1,11,111) --> ~isMember(1,22)https://rise4fun.com/Counterdog/testcase2testcase2|- [canRead(11,1,111); canRead(11,1,111) :- isMember(1,22); owns(2,11,111); isMember(2,11)] canExecute(1,11,111) & ~[canRead(11,1,111); canRead(11,1,111) :- isMember(1,22); owns(2,11,111)] canExecute(1,11,111) & ~[canRead(11,1,111); canRead(11,1,111) :- isMember(1,22); isMember(2,11)] canExecute(1,11,111) & ~[canRead(11,1,111); canRead(11,1,111) :- isMember(1,22)] canExecute(1,11,111) & [canRead(11,1,111); owns(2,11,111); isMember(2,11)] canExecute(1,11,111) & ~[canRead(11,1,111); owns(2,11,111)] canExecute(1,11,111) & ~[canRead(11,1,111); isMember(2,11)] canExecute(1,11,111) & ~[canRead(11,1,111)] canExecute(1,11,111) & ~[canRead(11,1,111) :- isMember(1,22); owns(2,11,111); isMember(2,11)] canExecute(1,11,111) & ~[canRead(11,1,111) :- isMember(1,22); owns(2,11,111)] canExecute(1,11,111) & ~[canRead(11,1,111) :- isMember(1,22); isMember(2,11)] canExecute(1,11,111) & ~[canRead(11,1,111) :- isMember(1,22)] canExecute(1,11,111) & ~[owns(2,11,111); isMember(2,11)] canExecute(1,11,111) & ~[owns(2,11,111)] canExecute(1,11,111) & ~[isMember(2,11)] canExecute(1,11,111) & ~ canExecute(1,11,111) --> isMember(1,22)https://rise4fun.com/Counterdog/testcase5testcase5|- [canRead(11,1,111); canRead(11,1,111) :- isMember(1,22); owns(2,11,111); isMember(2,11)] (canExecute(1,11,111) & ~isBanned(1,11)) & ~[canRead(11,1,111); canRead(11,1,111) :- isMember(1,22); owns(2,11,111)] (canExecute(1,11,111) & ~isBanned(1,11)) & ~[canRead(11,1,111); canRead(11,1,111) :- isMember(1,22); isMember(2,11)] (canExecute(1,11,111) & ~isBanned(1,11)) & ~[canRead(11,1,111); canRead(11,1,111) :- isMember(1,22)] (canExecute(1,11,111) & ~isBanned(1,11)) & [canRead(11,1,111); owns(2,11,111); isMember(2,11)] (canExecute(1,11,111) & ~isBanned(1,11)) & ~[canRead(11,1,111); owns(2,11,111)] (canExecute(1,11,111) & ~isBanned(1,11)) & ~[canRead(11,1,111); isMember(2,11)] (canExecute(1,11,111) & ~isBanned(1,11)) & ~[canRead(11,1,111)] (canExecute(1,11,111) & ~isBanned(1,11)) & ~[canRead(11,1,111) :- isMember(1,22); owns(2,11,111); isMember(2,11)] (canExecute(1,11,111) & ~isBanned(1,11)) & ~[canRead(11,1,111) :- isMember(1,22); owns(2,11,111)] (canExecute(1,11,111) & ~isBanned(1,11)) & ~[canRead(11,1,111) :- isMember(1,22); isMember(2,11)] (canExecute(1,11,111) & ~isBanned(1,11)) & ~[canRead(11,1,111) :- isMember(1,22)] (canExecute(1,11,111) & ~isBanned(1,11)) & ~[owns(2,11,111); isMember(2,11)] (canExecute(1,11,111) & ~isBanned(1,11)) & ~[owns(2,11,111)] (canExecute(1,11,111) & ~isBanned(1,11)) & ~[isMember(2,11)] (canExecute(1,11,111) & ~isBanned(1,11)) & ~(canExecute(1,11,111) & ~isBanned(1,11)) --> ~isMember(1,22)