abstract sig FSObject { } // parent relationship has moved to global state FileSystem sig File, Dir extends FSObject {} // contents relationship has moved to global state FileSystem // facts from the static model: // one sig Root extends Dir {} // A fact rootIsTheRoot { no Root.parent } // B fact parentContentsSymmetry { contents = ~parent } // C fact reachability { all o: FSObject | o in Root.*contents } sig FileSystem { live: set FSObject, root: Dir & live, parent: (live - root) -> one (Dir & live), // implies no mapping root -> Dir possible (A) contents: (Dir & live) -> live } { // A directory is the parent of its contents and vice versa contents = ~parent // (B) // File system is connected live in root.*contents // (C) } pred show {} run show for 5 but 2 FileSystem pred init[ s': FileSystem ] { #s'.live = 1 } run init for 5 but 1 FileSystem pred removeAll[ s, s': FileSystem, o: FSObject ] { o in s.live - s.root && s'.live = s.live - o.*(s.contents) && s'.parent = s'.live <: s.parent } pred showRemove[ s, s': FileSystem, o: FSObject ] { s != s' && removeAll[s, s', o] } run showRemove for 7 but 2 FileSystem, 3 Dir, 2 File