abstract sig FSObject { parent: lone Dir } sig File extends FSObject {} sig Dir extends FSObject { contents: set FSObject } one sig Root extends Dir {} fact rootIsTheRoot { no Root.parent } fact parentContentsSymmetry { contents = ~parent } fact reachability { all o: FSObject | o in Root.*contents } pred show {} run show for 5 // facts from above seem to imply the following assertions assert dirIsParent { all d: Dir, o: d.contents | o.parent = d } check dirIsParent for 5 assert inverse1 { all o: FSObject | some o.parent => o in o.parent.contents } check inverse1 for 5 assert inverse2 { all o: FSObject | some o.parent => o in o.parent.contents } check inverse2 for 5 assert acyclic { no d: Dir | d in d.^contents } check acyclic for 5