In this lesson, we do not add any new features to the model, but instead we rewrite part of it to show you a different way to doing things. The resulting model is semantically equivalent, but is a bit more concise and arguably clearer.
Two of the four constraints which were in the
FileSystem appended fact have been removed:
contents in live->live
These constraints have been built into the other ones. First of
all, the line which used to read
root: Dir & live,
This defines the root of a FileSystem to be in the set of live objects of its FileSystem, and not just be any old directory. (since it is in the intersection of Dir and live).
Secondly, the lines which use to read
parent: FSObject ->lone Dir,
contents: Dir lone-> FSObject
parent: (live - root) ->one (Dir & live),
contents: Dir -> FSObject
This is the same trick, but a little bit messier because it has
been done to higher arity relations (relations with more than 2
entries in each row). The parent relation maps every live object (except the root)
to exactly one live Dir. The contents
relation can be relaxed to just say it
maps from Dir to FSObject
(since later we have
Also notice that the lone multiplicity markings have been replaced by one's. Where a lone indicated "0 or 1", a one indicates "exactly 1". Thus the first line makes sure that each live non-root object has exactly one parent.
In the next lesson, we add dynamic operations to the model, move and remove.