FileSystem.als

module FileSystem

sig Time {}

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

sig Dir, File extends Object {}

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

sig Name {}

fact { all t : Time | all x : Object | all y : x.(parent.t).~(parent.t) - x | x.name not in y.name }

fact { all t : Time | all o : Object | o not in o.^(parent.t) }

fact { all t : Time | all fs : FileSystem | fs.(root+wd).t in fs.objects.t }

fact { all t : Time | all fs : FileSystem | all o : fs.objects.t | o.parent.t in fs.objects.t }

fact { all t : Time | all fs : FileSystem | fs.objects.t in *(parent.t).(fs.root.t) }


run {} for 4 but exactly 1 Time, exactly 1 FileSystem

fun ls [fs : FileSystem,t:Time] : set Object {
    (parent.t).(fs.wd.t) & fs.objects.t
}

pred rm [fs : FileSystem, f : File, t,t' : Time] {
    f in ls[fs,t]
    fs.objects.t' = fs.objects.t - f
    fs.root.t' = fs.root.t
    fs.wd.t' = fs.wd.t
}

pred cd [fs : FileSystem, d : Dir, t,t' : Time] {
    d in fs.objects.t
    fs.wd.t' = d
    fs.objects.t' = fs.objects.t
    fs.root.t' = fs.root.t
}

run rm for 4 but 1 FileSystem, 2 Time