@keywords is, of, a.

@prefix log: <http://www.w3.org/2000/10/swap/log#> .
@prefix crypto: <http://www.w3.org/2000/10/swap/crypto#> .
@prefix str: <http://www.w3.org/2000/10/swap/string#> .

@prefix foaf: <http://xmlns.com/foaf/0.1/>.
@prefix session: <http://redfoot.net/2005/session#>.
@prefix rein: <http://dig.csail.mit.edu/2005/09/rein/network#> .
@prefix http: <http://dig.csail.mit.edu/2005/09/rein/examples/http-access#> .
@prefix t: <http://dig.csail.mit.edu/2005/09/rein/examples/troop#> .
@prefix : <http://dig.csail.mit.edu/2005/09/rein/examples/troop42#> .


# policy language used 
<> rein:policy-language <http://dig.csail.mit.edu/2005/09/rein/examples/http-access.rdf>. 

{ <http://dig.csail.mit.edu/2005/09/rein/examples/troop42.rdf> log:semantics ?F } => { ?F a TroopStuff }.


# Photos of the girls winning awards can be shared with anyone 
# currently in the troop, or who was ever a member. 
# These award photos can also be shared with the public 
# if, and only if, the girl's parents allow it.

# (i) shared with members of the troop

@forAll REQ, PHOTO, LOC, WHO, PG, X, TXT, PARENT.
{ REQ a rein:Request.
  REQ rein:resource PHOTO.
  ?F a TroopStuff; log:includes
        { PHOTO a t:AwardPhoto }.

  REQ rein:requester WHO.
  WHO session:secret ?S.
  ?S crypto:md5 TXT.

  ?F a TroopStuff; log:includes
        { [] t:member [ is foaf:maker of PG ] }.
  PG log:semantics [ log:includes
        { PG foaf:maker [ session:hexdigest TXT ] }
    ].

} => { WHO  http:can-get PHOTO }.



# These award photos can also be shared with the public 
# if, and only if, the girl's parents allow it.
# a member's parent's foaf page is listed on the member's foaf page
# the parent's foaf page describes whether or not the pic
# is accessible to the public

# (ii) parent can say which class of pics are publicly accessible
# either by stating it or using rules

@forAll REQ, PHOTO, WHO, PG, CHLD, PARENT, PCLASS, P, G.

{ REQ a rein:Request.
  REQ rein:resource PHOTO.
  ?F a TroopStuff; log:includes 
	{ PHOTO a t:AwardPhoto; picOf [ is foaf:maker of PG ]. }.

  REQ rein:requester WHO.

  ?F a TroopStuff; log:includes
    	{ [] t:member [ is foaf:maker of PG ]. }.

  PG log:semantics [ log:includes
        { PG foaf:maker [ child [ foaf:maker PARENT ] ] } 
     ].
 
  ( <http://dig.csail.mit.edu/2005/09/rein/examples/troop42.rdf>.log:semantics
    <http://dig.csail.mit.edu/2005/09/rein/examples/troop.rdf>.log:semantics
    <http://www.agfa.com/w3c/euler/rpo-rules.n3>.log:semantics
    PARENT.log:semantics
  ) log:conjunction P.
  P log:conclusion G.
  G log:includes { PARENT foaf:maker [ grantsPublicAccess PCLASS ]. PHOTO a PCLASS. }.

} => { WHO  http:can-get PHOTO }.


#(iii) parent can say which photos are publicly accessible
# either by stating each pic or using rules

@forAll REQ, PHOTO, WHO, PG, CHLD, PARENT, P, G.
{ REQ a rein:Request.
  REQ rein:resource PHOTO.
  ?F a TroopStuff; log:includes
        { PHOTO a t:AwardPhoto; picOf [ is foaf:maker of PG ]. }.

  REQ rein:requester WHO.

  ?F a TroopStuff; log:includes
        { [] t:member [ is foaf:maker of PG ]. }.

  PG log:semantics [ log:includes
        { PG foaf:maker [ child [ foaf:maker PARENT ] ] }
     ].

  ( <http://dig.csail.mit.edu/2005/09/rein/examples/troop42.rdf>.log:semantics
    <http://dig.csail.mit.edu/2005/09/rein/examples/troop.rdf>.log:semantics
    PARENT.log:semantics
  ) log:conjunction P.
  P log:conclusion G.
  G log:includes { PARENT foaf:maker [ grantsPublicAccess PHOTO ] }.

} => { PARENT a Parent. WHO  http:can-get PHOTO }.


#ends