ocl2alloy FileSystem.uml < FileSystem.ocl

module FileSystem
sig Time {}

sig Dir extends Object {}

sig File extends Object {}

sig FileSystem {objects : Object set -> Time,root : Dir one -> Time,wd : Dir one -> Time}

sig Name {}

abstract sig Object {name : one Name,parent : Dir lone -> Time}

fact {all t : Time | all self : Object | all y : Object | ((some v3 : Dir | (v3 in self.(parent.t)) && (v3 in y.(parent.t))) && (y != self)) => !(all v0 : Name | (v0 in self.name) => (v0 in y.name))}

fact {all t : Time | all self : Object | self not in self.^{v9 : univ,v0 : v9.(parent.t) | no none}}

fact {all t : Time | all self : FileSystem | all v12 : Dir | ((v12 in self.(root.t)) || (v12 in self.(wd.t))) => (v12 in self.(objects.t))}

fact {all t : Time | all self : FileSystem | all o : Object | (o in self.(objects.t)) => (all v17 : Dir | (v17 in o.(parent.t)) => (v17 in self.(objects.t)))}

fact {all t : Time | all self : FileSystem | all v24 : Object | (v24 in self.(objects.t)) => (some v27 : Dir | ((v24 = v27) || (v27 in v24.^{v28 : univ,v1 : v28.(parent.t) | no none})) && (v27 in self.(root.t)))}

fun ls [self : FileSystem,t : Time] : set Object {{v33 : Object | (some v34 : Dir | (v34 in v33.(parent.t)) && (v34 in self.(wd.t))) && (v33 in self.(objects.t))}}

pred rm [self : FileSystem,f : File,t,t' : Time] {f in ls[self,t]
                                                  (all v43 : Object | (v43 in self.(objects.t')) => ((v43 in self.(objects.t)) && (v43 != f))) && (all v48 : Object | ((v48 in self.(objects.t)) && (v48 != f)) => (v48 in self.(objects.t')))
                                                  (all v53 : Dir | (v53 in self.(root.t')) => (v53 in self.(root.t))) && (all v58 : Dir | (v58 in self.(root.t)) => (v58 in self.(root.t')))
                                                  (all v63 : Dir | (v63 in self.(wd.t')) => (v63 in self.(wd.t))) && (all v68 : Dir | (v68 in self.(wd.t)) => (v68 in self.(wd.t')))}

pred cd [self : FileSystem,d : Dir,t,t' : Time] {d in self.(objects.t)
                                                 (all v76 : Dir | (v76 in self.(wd.t')) => (v76 = d)) && (d in self.(wd.t'))
                                                 (all v82 : Object | (v82 in self.(objects.t')) => (v82 in self.(objects.t))) && (all v87 : Object | (v87 in self.(objects.t)) => (v87 in self.(objects.t')))
                                                 (all v92 : Dir | (v92 in self.(root.t')) => (v92 in self.(root.t))) && (all v97 : Dir | (v97 in self.(root.t)) => (v97 in self.(root.t')))}