resources.als

one sig Person {
}

sig Resource {
  , access: set Person
  , parent: lone Resource
}

fact "No cycles" {
  no r: Resource |
		r in r.^parent
}

pred can_access[p: Person, r: Resource] {	
       p in (r.access + r.parent.access)
}


//if you can access the parent, you can access all its children
assert parent_implies_child {
	all p: Person, r: Resource |
		can_access[p, r] => all child: parent.r | can_access[p, child]
}


check parent_implies_child