How to reduce temporal update boilerplate for state-rich models?

Questions
1

When creating models that track a lot of state, I generally create a main fact with the “trace” pattern or a “system” predicate that just has the chain of things that happen at every time step like:

pred system {
    always {
        some x: SigA | event1[a]
        or some y: SigB | event2[b]
        // ...
    }
}

Inside those event predicates though, if SigA/SigB … all have variable state, every predicate becomes kind of a mess because I have to specify in each one what DOESN’T change if that predicate is valid, like:

pred event1(x: SigA){
    x.temporalvar' = x.temporalvar + blah
    (SigA-x).temporalvars' = (SigA-x).temporalvars
    SigB.temporalvars' = SigB.temporalvars
    SigC.temporalvars' = SigC.temporalvars
    // ...
}

As otherwise those transitions will be left unspecified and Alloy just has freedom to break constraints, and I can’t (at least I think?) usually create a catch-all predicate that would specify all other state is to be left untouched given that the other state could have any signature type and there’s no generics in Alloy.

Is there some way to do the whole “all other state not specified here should just be x.y’ = x.y” without writing it out manually? or some more concise form? or am I using the “trace” style wrong and there’s some better way to encode this flow?

For me right now this is definitely the biggest pain point when writing state-rich models, I was thinking of writing a DSL to auto-generate a lot of this boilerplate but if there’s some way to leverage Alloy’s grammar to reduce the load here that’d be better.

1 Like
2

Hi Matthew,

This is a great question. Here are some strategies I’ve used for making frame conditions easier to express:

— Rather than expressing an update to a relation as

x.r’ = e and all x’: X - x | x.r’ = x.r`

use relational override and write

r’ = r ++ x -> e

— Organize events into a hierarchy using signature extension, and associate frame conditions with larger event classes. For example, in the hotel model in my book (p. 204), there’s a class of events called RoomKeyEvent which has a frame condition associated with it saying there is no change at the front desk.

— Separate frame conditions out into predicates that can be reused. The same example in my book uses a predicate noRoomChangeExcept [rs: set Room] which constrains there to be no change except possibly for the set of rooms rs. Such a predicate can also take a relation as an argument, although Alloy’s type system can get in the way a bit here (but can resolve overloaded predicate names with relations of different types).

— Use Reiter style frame conditions (my Alloy book, p203) in which you write a constraint that says that if a particular relation was modified, a certain event must have happened: eg, this constraint says that if the occupant of a room changed, then a checkin or a checkout must have happened:

occupant.t != occupant.t’ => e in Checkin + Checkout

— Not sure of the status of the implementation, but Alloy has a minimally documented metafacility (see http://alloytools.org/quickguide/meta.html) which allows you to quantify over fields, so you can say something like

all f: $Field | x.f = x.f’

Note that most of these strategies were developed prior to Alloy 6, which has made it more reasonable to use only predicates and not explicit event objects to define state transitions. Hopefully they can all be adopted in A6, maybe even in a better form, but I haven’t had a chance to look into that.

On a methodological note: Alloy’s declarative style, in which behavior is specified just by constraints, is what makes it powerful in many ways. Rather than saying everything at once, as you’d have to do in a program, you can say as little as possible and build a model up incrementally, adding more constraints to rule behaviors out, and discovering what is really needed to make a requirement true. This is also what lets you compose by conjunction, and makes it possible to model abstraction functions. It lets you define state components in terms of other state components, and also (most basically) define behavior by observation rather than construction (for example, saying that the value of a nonce is any value not used before).

But the flip side of this merit is frame conditions and the annoyance they cause. If I was designing Alloy again, especially given the advances of Alloy 6 which relies on embedding a particular model of dynamics (which basic Alloy does not do), I would include statement forms that include implicit frame conditions. I use such statements in modeling concepts in my recent book (Essence of Software, p227), writing things like

x.p += e

for

p’ = p + (x -> e)

I think there’s a great project to do in extending Alloy with such syntax!

Daniel

1 Like
3

You could use a macro. Off the top of my head, it might look something like

let unchanged[x] = x' = x
let also[x, y] = y' = y

Then you can do unchanged[(SigA-x).vars].also[SigB.vars].also[SigC.vars]... There’s probably a more elegant want to do this with macros, this is just my immediate idea.

2 Likes
4

In our extension to Alloy to model hierarchical, concurrent state transition systems (like Statecharts but with Alloy on the transitions) called Dash, the default behaviour is that a variable not mentioned in a transition action stays unchanged. A user can set an option to not add these constraints. Dash is best described in:

We have a beta-version of Dash (and its translation to Alloy) integrated into the Alloy Analyzer (version 6). Anyone who wants to try it out, please contact me at nday@uwaterloo.ca .

2 Likes
5

A few years ago I made an attempt to support a Pluscal like language in Alloy. One of the features was that it traversed all the logical paths and automatically ensured the non-used variables were kept constant if not mentioned in a branch.

PlusCal in Alloy

It never generated a lot of interest so I stopped pursuing it. I made a deplorable joke that seemed to have upset some sensitive souls and that dominated the discussion :slight_smile: but reviving the part that keeps unused variables constant might be an idea.

I agree that doing it manually is very error prone and tedious.

1 Like
6

Completing other answers, I wrote some months ago a post about how to model stateful models in our so called “reified event” style.

If you use the novel, built-in-temporal features of Alloy 6, I would advise against this style and would favor the reified event cited hereabove. The latter has all advantages of Daniel’s, while it doesn’t suffer from the tricky part, which is you don’t know how many atoms you may need in traces (you may miss some traces due to a bad scope specification for the event signature).

I’m using this, but I write it as follows to avoid bad surprises with the possible application of the prime symbol over a compound expression:

let unchanged[x] { (x)' = (x) }
2 Likes
7

Thanks for the answers everyone, I was able to make my model a little cleaner.

Out of curiosity, is there some way in Alloy to actually specify “nothing at all should change” between two time steps?

I noticed that if I wrote:

always univ' = univ

No variable-signature atoms are able to be created or destroyed, but the relations associated to fields are still able to change. The metafacility above doesn’t work on the univ object, it gives a grammar error, and actually I wasn’t able to get it to work at all with temporal specifiers, I just got Java runtime errors, so Alloy 6 might have broken it.

Is there any way to specify “the set of all relations” or “the set of all fields”?

8

Not that I am aware of…