Alloy File System Lesson I

filesystem1.als

sig FSObject {
  parent: lone Dir
}

sig Dir extends FSObject {
  contents: set FSObject
}

sig File extends FSObject {}

fact {
  all d: Dir, o: d.contents | o.parent = d
}

fact {
  File + Dir = FSObject
}

one sig Root extends Dir {} { no parent }

fact {
  FSObject in Root.*contents
}

assert acyclic {
  no d: Dir | d in d.^contents
}

check acyclic for 5

assert oneRoot {
  one d: Dir | no d.parent
}

check oneRoot for 5

assert oneLocation {
  all o: FSObject | lone d: Dir | o in d.contents
}

check oneLocation for 5

assert Wrong {
  all obj, p: (FSObject - Root) | obj.parent = p.parent
}

check Wrong for 15