# Trying to model a Filesystem

**URL:** <https://alloytools.discourse.group/t/trying-to-model-a-filesystem/98>\
**Category:** Software Abstractions\
**Created:** [September 18, 2020, 6:57am UTC](https://alloytools.discourse.group/t/trying-to-model-a-filesystem/98 "2020-09-18T06:57:59Z")\
**Posts on this page:** 9\
**Page:** 1

<div class="post-metadata">

**Author:** ![Zenzi](https://avatars.discourse-cdn.com/v4/letter/z/e9a140/32.png) [@Zenzi](https://alloytools.discourse.group/u/Zenzi)\
**Post date:** [September 18, 2020, 6:57am UTC](https://alloytools.discourse.group/t/trying-to-model-a-filesystem/98/1 "2020-09-18T06:57:59Z")

</div>

Hi,

after reading chapter 2 and 3, I tried to practice Alloy a bit further. My goal is to model a simple filesystem and I started with creating a basic “structure” with files, folders and so on (based on [this](http://softwareabstractions.org/models/a4-models/chapter4/filesystem.als)).

```
/* ------------------------------------------------------ */
// Declarations:

abstract sig Object {}

one sig Root extends Container {} {
  not this in contains
}
abstract sig Container extends Object {
  contains: set Object
}

sig Folder extends Container {} {
  // a folder can not be part of itself
  not this in contains
  // root can not be part of a container
  not Root in contains
}

sig File extends Object {}

/* ------------------------------------------------------ */
fact {
  // every object is part of the file system
  Object in Root.*contains
  // every object except the Root is located in
  // exactly one container
  all o: Object - Root | lone contains.o
    
}

/* ------------------------------------------------------ */

assert NoRootParent {
  no contains.Root
}
// check NoRootParent for 5

assert HasParent {
  all o: Object - Root | lone contains.o 
}
// check HasParent for 5
/* ------------------------------------------------------ */
pred show { }

run show for 5 but exactly 1 Root

```

My questions:

1. I want to specify some operations like `addNewFile` and `removeFile`. However, I am struggling with adding a notion of “time” (i.e. for adding a new file: the new filesystem is the old one with the addition of a new element). I know that I have to create a new `sig` that relates different filesystems together but the result looks strange with the Alloy Analyzer. Do I need multiple Root objects then? What I would love to do is a projection over Time and visualize the effect of adding a new file to the system based on the predicate head `add_new_file(fs, fs': FileSystem, container: Container, newElement: Object)`. Can anyone show me an extension how to define operations that manipulate the filesystem? (\*)
2. Do I have to explicitly state that everything remains the same during an `addNewFile` or `removeFile` operation?
3. I have some `assert` statements and some `check` statements. Usually, I comment out the `check` statement when I want to run something different (and remove the comment if I want to check the assertion). Is there a smarter way to do that ? Can I run a whole bunch of checks at once?

Any other feedback is welcome.

(\*) Maybe, Electrum is the thing I should use but I would prefer doing it with Alloy itself and not rely on any extensions.

---

<div class="post-metadata">

**Author:** ![peter.kriens](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/peter.kriens/32/3_2.png) [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)\
**Post date:** [September 18, 2020, 7:43am UTC](https://alloytools.discourse.group/t/trying-to-model-a-filesystem/98/2 "2020-09-18T07:43:47Z")

</div>

> [@Zenzi](#):
>
> Maybe, Electrum is the thing I should use but I would prefer doing it with Alloy itself and not rely on any extensions.

The plan is that Alloy 6 will fully contain Electrum, it will not be an extension. It might take some time, but that is the current plan.

I highly recommend using Electrum for these state machines since I never got the hang of the Time concept.

> [@Zenzi](#):
>
> Do I have to explicitly state that everything remains the same during an `addNewFile` or `removeFile` operation?

Yes

> [@Zenzi](#):
>
> I have some `assert` statements and some `check` statements. Usually, I comment out the `check` statement when I want to run something different (and remove the comment if I want to check the assertion). Is there a smarter way to do that ? Can I run a whole bunch of checks at once?

You can have any number of check or run statements. They are listed in the Execute menu which also contains an entry to run them all.

---

<div class="post-metadata">

**Author:** ![steve.freeman](https://avatars.discourse-cdn.com/v4/letter/s/2acd7d/32.png) [@steve.freeman](https://alloytools.discourse.group/u/steve.freeman)\
**Post date:** [September 18, 2020, 7:54am UTC](https://alloytools.discourse.group/t/trying-to-model-a-filesystem/98/3 "2020-09-18T07:54:34Z")

</div>

I would also recommend Electrum. I managed to get the hang of the Ordered Time patterns but, frankly, it’s a waste of time. Electrum makes the result much easier to see, and it will be incorporated in the new version.

---

<div class="post-metadata">

**Author:** ![steve.freeman](https://avatars.discourse-cdn.com/v4/letter/s/2acd7d/32.png) [@steve.freeman](https://alloytools.discourse.group/u/steve.freeman)\
**Post date:** [September 18, 2020, 7:59am UTC](https://alloytools.discourse.group/t/trying-to-model-a-filesystem/98/4 "2020-09-18T07:59:36Z")

</div>

This [https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6](https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6) starts with an excellent description of how to model with state transitions in Electrum.

The point about asserting that everything else stays the same, is that Alloy will use any flexibility it is permitted to explore a model. This is good because we only specify what we care about. You might also check out this discussion which I found useful [https://alloytools.discourse.group/t/facts-vs-assertions](https://alloytools.discourse.group/t/facts-vs-assertions)

---

<div class="post-metadata">

**Author:** ![Zenzi](https://avatars.discourse-cdn.com/v4/letter/z/e9a140/32.png) [@Zenzi](https://alloytools.discourse.group/u/Zenzi)\
**Post date:** [September 18, 2020, 9:07am UTC](https://alloytools.discourse.group/t/trying-to-model-a-filesystem/98/5 "2020-09-18T09:07:03Z")

</div>

> [@peter.kriens](#):
>
> The plan is that Alloy 6 will fully contain Electrum, it will not be an extension. It might take some time, but that is the current plan.
> 
> I highly recommend using Electrum for these state machines since I never got the hang of the Time concept.

Ok thanks. I will check out Electrum at a later point in time and first try to understand modelling without it. Daniel Jackson wrote in the book that time and space can be modeled with relations and I want to get a deeper understanding with the basics - even if it takes some time. Additionally, the only source I have to learn is the book for now which does not cover Electrum (as far as I can tell).  
(I appreciate your tips on using Electrum and I guess that it makes life a lot easier. But I hope that my resistance for not using it right now is understandable 🙂 )

I tried to model it closely to the address book example in chapter 2. I think the main problem I have is to state the fact that everything remains the same (and the ordering of the assigned elements is weird, sometimes).

I tried the following extension to my model:

```
open util/ordering [FileSystem]
... /* other definitions */
sig FileSystem {
  root: lone Root
} {
  some root // ensure there is a root element
}

pred addNewElement(f, f': FileSystem, 
                   c: Container, 
                   o: Object)
{
  not f = f' and not f.root = f'.root and
    some c': Container |     
      c' in (f'.root).^contains and
      c'.contains = c.contains + o
}

```

This predicate (should) say something like: filesystem `f` and `f'` are related (but not the same) and there is a container `c'` in the new filesystem `f'` that contains the new element `o’. But I guess that I still have to state the fact that everything else remains the same.

One thing that is also a bit strange: Sometimes, `f` will be bound to `FileSystem$1` and I have to read the projection backwards. I added an ordering for `FileSystems`. Why is `f` bound to `FileSystem$1` and `f'` to `FileSystem$2` ?

I have not stated a fact `trace` yet (as sown in chapter 2 of the book), maybe that is my error at the moment.

> [@](#):
>
> > [@Zenzi](#):
> >
> > [Questions about running all checks and commands at once]
> 
> You can have any number of check or run statements. They are listed in the Execute menu which also contains an entry to run them all.

Thanks, exactly what I was looking for!

---

<div class="post-metadata">

**Author:** ![Zenzi](https://avatars.discourse-cdn.com/v4/letter/z/e9a140/32.png) [@Zenzi](https://alloytools.discourse.group/u/Zenzi)\
**Post date:** [September 18, 2020, 9:10am UTC](https://alloytools.discourse.group/t/trying-to-model-a-filesystem/98/6 "2020-09-18T09:10:03Z")

</div>

> [@steve.freeman](#):
>
> This [https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6](https://alloytools.discourse.group/t/modelling-a-state-machine-in-electrum-towards-alloy-6) starts with an excellent description of how to model with state transitions in Electrum.

Thanks, I will check out Electrum at a later point in time (please have a look at my previous posting for not doing it right now).

> [@](#):
>
> The point about asserting that everything else stays the same, is that Alloy will use any flexibility it is permitted to explore a model. This is good because we only specify what we care about. You might also check out this discussion which I found useful [https://alloytools.discourse.group/t/facts-vs-assertions](https://alloytools.discourse.group/t/facts-vs-assertions)

Yes 🙂 - it is strange when starting with Alloy but it makes sense and reveals potential errors. I definitely see the advantage of using every flexibility the Analyzer has.

---

<div class="post-metadata">

**Author:** ![peter.kriens](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/peter.kriens/32/3_2.png) [@peter.kriens](https://alloytools.discourse.group/u/peter.kriens)\
**Post date:** [September 18, 2020, 9:28am UTC](https://alloytools.discourse.group/t/trying-to-model-a-filesystem/98/7 "2020-09-18T09:28:08Z")

</div>

> [@Zenzi](#):
>
> But I hope that my resistance for not using it right now is understandable 🙂

Hey, it is your Time you’re wasting! 🙂 (Couldn’t resist the pun)

The thing is that the Time concept in Daniel’s book is probably the hardest part in the whole book. It is a tribute to Alloy that you can actually do time modelling in it without any special constructs. However, you could also do this modeling in assembly code …

You might want to checkout the [Electrum tutorial](https://haslab.github.io/TRUST/tutorial.html) before you dive deep into the Time examples so that you at least have some perspective of what’s coming.

But again, it is your Time …

---

<div class="post-metadata">

**Author:** ![steve.freeman](https://avatars.discourse-cdn.com/v4/letter/s/2acd7d/32.png) [@steve.freeman](https://alloytools.discourse.group/u/steve.freeman)\
**Post date:** [September 18, 2020, 10:00am UTC](https://alloytools.discourse.group/t/trying-to-model-a-filesystem/98/8 "2020-09-18T10:00:59Z")

</div>

> [@Zenzi](#):
>
> I have not stated a fact `trace` yet (as sown in chapter 2 of the book), maybe that is my error at the moment.

You do need to have the trace fact (or predicate called by a run) to force the sequence of transitions.

---

<div class="post-metadata">

**Author:** ![bch](https://avatars.discourse-cdn.com/v4/letter/b/f475e1/32.png) [@bch](https://alloytools.discourse.group/u/bch)\
**Post date:** [September 20, 2020, 7:10pm UTC](https://alloytools.discourse.group/t/trying-to-model-a-filesystem/98/9 "2020-09-20T19:10:32Z")

</div>

Steve Freeman via The Alloy Language and Tools  
[alloytools@discoursemail.com](mailto:alloytools@discoursemail.com) writes:

> > [Question about Filesystem operations]  
> > You do need to have the trace fact (or predicate called by a  
> > run) to force the sequence of transitions.

Yes, you need to build and maintain the time dependent component

The `Container` signature must be converted to something like  
that:

```
...
sig Time {}

abstract sig Container extends Object {
  contains: Object -> Time
}
... /* other definitions */

```

And the add operation might refer to a given time then:

```
...
  container.contains.t' = container.contains.t + object 
...

```

An ordering must be specified as well (see chapter 2.4).

It is also necessary to explicitly state what remains unchanged  
during a state transition.

I struggled with this a bit as well and as others already  
mentioned, Electrum simplifies this but isn’t explained in the  
book.

[Edit #1]: It looks like that replying by mail does not work as expected. I manually added the missing part of my mail.