Hey folks. I’ve been learning a bit Alloy with the intention of using the linear temporal logic checking. I’ve had some experience with rewriting systems (most notably, Maude) and I’m really enjoying Alloy so far.
However, the fact that any (mutable) relation can change (if I don’t write x’ = x) in the predicate seems very inconvenient. I’ve already had many unexpected instances caused by forgetting to “lock” one relation. It also leads to a case where when I introduce a new relation, I’ll have to try remember to lock it in all of the time existing predicates - even if they are not related at all. Isn’t this quite fragile?
Am I doing something wrong? Is there another way of modeling such systems?
I once made a PlusCal like interpreter in the Alloy code base. There I analyzed the branches (implies) and made sure to add instructions when one branch set a var that was not set in the other branch. This seemed to work well but I have no idea how theoretically solid it was and nobody got excited … so it has been lingering since. From a user point of view I think it would be really a huge gain.
It is fragile indeed. It’s the other side of the coin of being so nicely declarative. When specifying an operational device with sort of a state machine, it can be cumbersome and error-prone.
But the freedom given by Alloy is also handy. For instance, you can specify a mutable relation by a global temporal fact rather than by what looks like an event (or an instruction in a PlusCal-like extension), and by no means do you want an implicit frame condition to fix its value because your spec might become inconsistent or implictly restrained.
With the next version of Alloy coming this fall, the combination of macros and meta (which should be fixed and extended to handle mutable stuff) may make it possible to get some shorter ways to handle FCs. Going further and creating an extension is of course possible (and was already prototyped, and is still researched by some of us) but it seems very difficult to come up with something the semantics of which is at the same time general enough and doesn’t put a burden on the user.
It’s not the most elegant solution, but a mutates “pragma” on predicate which “locks” every other relationwhich is not in the list (i.e. r' = r) would be “good enough” for me to feel more comfortable. And then maybe combined with a warning if you refer to r' in the predicate without it being part of the mutates list?
pred foo[] mutates(X, y, z) {
-- Now every relation _other_ than X, y, z will implicitly get `r' = r` added.
}
We did this in Electrum Action some years ago. As I said above, there are issues with this approach too, most notably with variables the value of which may be set outside of events, for instance using a global temporal fact. Also, there is an issue with the granularity of the pragma: you may want something less blunt than “mutated or unchanged”, depending on your time model (e.g. if you want to allow several events simultaneously).
My point is that choosing such an approach is easy but then it forces users to commit to one modeling approach that may not fit their problem domain. This goes against the generality of Alloy. So should we create another language, possibly losing some nice aspects of Alloy? Or is it possible to find an approach that has the wanted properties while keeping the good aspects of the language?
I also realize that I might need to change the way I’m thinking. I’m very used to thinking “start with an (specific) initial state” and then “define rules which iteratively change this”. However, Alloy is capable of creating interesting states without any rules being applied. This can also be considered a feature for actions as well: It’s valuable to let Alloy generate other interesting changes that runs “simultaneously” to our actions. And then instead we can add constraints with are more “fundamental” (e.g. fact { always … }).
I also realized that the way predicates interact with different parts can also be encode outside of the predicate itself:
fact {
-- Model the fact that we need to take out a lock on billing details whenever `upgradeProject` happens.
always (some p: Project | upgradeProject[p]) implies (billingDetails' = billingDetails)
}
This is actually very nice. You can start out without this constraint, and then Alloy can demonstrate a trace where someone is capable of upgrading their project while simultaneously removing their billing details (which leads to an invalid state of “upgraded project has no billing details”). Once we add this constraint we see that this is enough to make our model consistent.
Another modeling approach would be to add constraints the other way. Instead of restricting the different actions which can happen, you can restrict how the relations are allowed to change:
fact {
-- New projects can only be created or duplicated:
always all p: Project' - Project | createdProject[p] or (some other: Project | duplicatedProject[other, p])
-- Owner can only be changed if a project is transferred:
always all p: Project | p.owner' != p.owner implies transferProject[p, p.owner']
-- Projects can never be deleted:
always Project in Project'
}
And separately we could add other facts to make sure we’re getting an interesting trace (e.g. ensure that we actually do at least one of our actions in every step).