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).
/* ------------------------------------------------------ */
// 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:
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? (*)
Do I have to explicitly state that everything remains the same during an addNewFile or removeFile operation?
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.
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.
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
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.
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).
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.
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 before you dive deep into the Time examples so that you at least have some perspective of what’s coming.
)