module language/filesystem

abstract sig Object {}
--	{lone this.~@contents}

sig File extends Object {}
sig Dir extends Object {contents: set Object}
--	{this not in this.^@contents}

one sig Root extends Dir { }
--	{Object in this.*@contents}

fact {
--	no d: Dir | d in d.^contents
	Object in Root.*contents
--	all o: Object | lone o.~contents
	}

assert SomeDir {
	all o: Object - Root | some contents.o
	}
check SomeDir

assert RootTop {
	no o: Object | Root in o.contents
	}
check RootTop

assert FileInDir {
	all f: File | some contents.f
	}
check FileInDir