cd2alloy < FileSystem.uml

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}

fun ls [self : FileSystem,t : Time] : set Object {none}

pred rm [self : FileSystem,a : File,t,t' : Time] {}

pred cd [self : FileSystem,a : Dir,t,t' : Time] {}

sig Name {}

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