abstract sig FSObject {
  parent: lone FSObject
}

sig File extends FSObject {}

sig Dir extends FSObject {
  contents: set FSObject
}

one sig Root extends Dir {}

pred isLeaf[f: FSObject] {
  f in File || no f.contents
}

// 1. run isLeaf: try to find an instance
// such that M (global constraints implied by signatures and facts) 
// and some f: FSObject | f in File | no f.contents 
run isLeaf

fun leaves[f: FSObject]: set FSObject {
  {x: f.*contents | isLeaf[x] } // comprehension!
}

// 2. run leaves: try to find an instance
// such that M (global constraints implied by signatures and facts) 
// and f: FSObject | set {x:  f.*contents | isLeaf[x]}
// note that it is possible that leaves delivers an empty result here. 
// If this must not be the case, "some" can be chosen instead of "set"
// also play with f.*contents (reflexive transitive closure) vs. f.^contents (transitive closure)
run leaves for 2 but exactly 2 File 

//3. try different runs of isLeaf:
/*
 run isLeaf
run isLeaf for 5
run isLeaf for 5 Dir, 2 File
run isLeaf for exactly 5 Dir
run isLeaf for 5 but 3 Dir
run isLeaf for 5 but exactly 3 Dir
*/

// 4. look at global models (search for model from slides in the output
// cardinalities of relations can also be restricted / constrained

pred show {}
run show for exactly 1 File, exactly 2 Dir

// problems identified:
// (a) root should not have a parent
// (b) contents and parent should be inverse relations
// (c) directory should not contain itself

// 5. add facts
// (a)
/*
fact noRootParent {
	no Root.parent
}
*/
// b()
/*
fact inverse1 {
	all d : Dir, o : d.contents | o.parent = d
}
*/
// (c)
/*
fact acyclic {
	no d: Dir | d in d.^contents
}
*/
// 6. exploring the model, we find out that we need the inverse for the second fact
assert inverse2 {  
	all o: FSObject | some o.parent => o in o.parent.contents 
}

// 7. we need that every object is reachable from the root
/*
fact {
	FSObject in Root.*contents
}
*/

// 7. and 5.b can be expressed as fact { contents = ~parent }

// 8. Finding a counterexample:
/*
assert nonEmptyRoot {
	!isLeaf [ Root ] 
}
check nonEmptyRoot for 3
*/

// 9. turn fact acyclic into an assertion, then check 
// check acyclic for 5

// 10. turn fact inverse2 into an assertion, then check 
// check inverse2

// 11. turn fact inverse1 into an assertion, then check
// check inverse1 

// 12. add the following fact and retry assertion inverse1 from above
/*
fact acyclic {
	no d: Dir | d in d.*contents
}
*/ 

// 13. check the following
/*
assert nonSense{
	0 = 1
}
check nonSense
*/

// 14. run show