open util/ordering[FileSystem]

abstract sig FSObject {}

sig File, Dir extends FSObject {}

sig FileSystem {
  live: set FSObject,
  root: Dir & live,
  parent: (live - root) -> one (Dir & live),
  contents: (Dir & live) -> live
}

pred inv[ s: FileSystem ] {
  // A directory is the parent of its contents and vice versa
  s.contents = ~(s.parent)

  // File system is connected
  s.live in s.root.*(s.contents)
}

pred init[ s': FileSystem ] {
  #s'.live = 1
} 













// 1. check this (initialization)
/*
assert initEstablishes {
  all s': FileSystem | 
  init[s'] => inv[s']
}
check initEstablishes
*/

// 2. add to init: s'.contents[s'.root] = none

// 3. check this (preservation)
/*
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 removeAllPreserves {
  all s,s' : FileSystem, o: FSObject | inv[s] && removeAll [s,s',o] => inv[s']
}
check removeAllPreserves
*/
// 4. add to remove All: 
//   && s'.contents = s.contents :> s'.live


// 5. add further operation and execution fact
/*
pred add[ s, s': FileSystem, o: FSObject, d: Dir ] {
  !(o in s.live) && d in s.live &&
  s'.live = s.live + o
  s'.parent = s.parent + (o->d)
  s'.contents = s.contents ++ (d->(s.contents[d] + o))
} 

fact execution {
  init[first] &&
  all s: FileSystem - last | 
    (some o: FSObject | removeAll[s, s.next, o])  ||
    (some o: FSObject, d: Dir | add[s, s.next, o, d])
}
*/ 

// 6. add temporal invariant
/*
pred inv2[ s, s': FileSystem ] {
  s.root = s'.root
}

assert invtemp {
  all s, s': FileSystem | lte[s, s'] => inv2[s, s']
}

check invtemp 
*/

// 7. add global invariant
/*
assert invHolds {
  all s: FileSystem | inv[s]
}
check invHolds for 5 but exactly 1 FileSystem
*/