accounts.als

sig Account {
  resources: set Resource,
  users: set User
}

sig User {
  canAccess: some Resource
}

sig Resource {
  parent: lone Resource
}

run {} for 2 but exactly 2 Account

fact "no shared users or resources" {
  all u: User | one a: Account | u in a.users

  all r: Resource | one a: Account | r in a.resources
}

fact "parent resource in same account" {
  all r: Resource | 
	some r.parent implies
		 (one a: Account | r in a.resources and r.parent in a.resources)
}

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

pred can_access(u: User, r: Resource) {	
       r in u.canAccess or r.parent in u.canAccess
}

run {
  some u: User, r: Resource | can_access[u, r]
}




//if you can access the parent, you can access all its children
assert parent_implies_child {
	all u: User, r: Resource |
		can_access[u, r] implies 
                    all child: parent.r | can_access[u, child]
}


check parent_implies_child