Damn, that’s subtle. The commands function introduces new instances of the Command sig into the “environment”, which have to be matched.
And the name of the function and the leading underbars are just conventions that have no significance.
I’m not sure to understand what’s meant by “wiring up” here.
You don’t need the “commands” function to make the model work. You need it to be able to easily say which commands should be displayed in the Visualizer. Indeed, in Alloy, every function without parameters yields a set that can be themed in the Visualizer.
Here, “commands” returns the set of commands that are “fired”: the Visualizer evaluates it in every state. This way, you can theme your visualization by (1) saying you don’t want to display all commands (sig Command: Show = Off) but (2) only those that are fired in the current state (set $commands: Show = On).
Notice this is plain Alloy, but I’ll admit it’s subtle at first. And yes, underscores are only a convention.
That’s my understanding. The revelatory thing here is that a fun isn’t a delayed expression (there’s a let form for that), it’s a set of tuples of a certain shape. A fun seems to be more concrete than a sig.
That’s what I mean by wiring up. The model worked as well as ever it did without the Commands.
A fun is simply an expression with a name and, possibly, parameters. Similarly a pred is simply a constraint with a name and, possibly, parameters. So to speak, both are parametrized shortcuts.
A sig represents a set (of atoms). But if you think of funs without parameters, it also represents a set. Therefore, as the Visualizer knows how to theme sets, it can theme sigs as muchs as parameter-less funs.
Also, as Electrum instances are traces (= sequences of states), the value of any set (except those known to be constant) may change in every state.
Now, in the Visualizer, you don’t want to represent the set of all possible commands, in general. You only want to represent the set of commands that happen in a given state that you’re currently displaying. Which is what commands yields.
Yes.
No, I see that now, although the predicates do seem to. And the reason I think that is that I’ve never seen an instance where the rule doesn’t hold.
So, while this:
can create a counter-example, if I include it in the trace the run is fine. Which is interesting.
However, my misunderstanding about the use of disj is the reason that models with multiple vehicles don’t work, so thanks for explaining that.
Yes, but given the way they behave, it doesn’t seem to be delayed, hanging around unevaluated, waiting to be instantiated as a stack frame or activation record in the way that a function in a functional language or a procedure in a procedural language are.
This is the head-banging bit for us old-school coders.
My next thought is that, in our world, repeated patterns like this are often a hint of missing features.
Well I think it’s pretty normal. As you said, this is subtle. I should add however that Daniel’s book, even if on Alloy 4 only, is very helpful to understand a lot of this. There is also some work coming for Alloy 6/Electrum.
Absolutely.
We had a prototype for this for a former version of Electrum but it was too limited and a bit bogus. More importantly, we decided to retain the freedom and “declarativeness” of Alloy on purpose, when we submitted Electrum.
We will propose an extension for state machine modelling in the future and it will, in particular, handle these patterns automatically.
Here’s my new version of the cards problem. It seems to be getting more compact, which is nice.
I used the guard clause in cancel to make sure I have the right cards, rather than filtering up front (counterintuitive to me). In principle, I could have just passed in the target card to cancel, but I wanted the visualiser to show me its replacement as well. I might change my mind on this.
enum Status { unissued, issued, cancelled }
sig Card {
var status : Status
}
sig Customer {
var cards: disj some Card
}
// ---- events ----
pred cancel[toCancel, replacement: Card] {
toCancel in Customer.cards
replacement in status.unissued
let customer = cards.toCancel {
status' = (status ++ toCancel->cancelled) ++ replacement->issued
cards' = cards - customer->toCancel + customer->replacement
}
}
pred skip {
status' = status
cards' = cards
}
// ---- reification ----
enum Event { Cancel, Skip }
fun _cancel : Event -> Card -> Card {
Cancel -> { card, replacement: Card | cancel[card, replacement] }
}
fun _skip : Event {
{event : Skip | skip}
}
fun events : set Event {
_cancel.Card.Card + _skip
}
// ---- behaviours ----
pred init {
no status.cancelled
#status.unissued > 1
all customer: Customer | some customer.cards
status.issued = Customer.cards
}
fact traces {
init
always (skip or some toCancel, replacement: Card | cancel[toCancel, replacement])
}
pred example { eventually no status.unissued }
assert card_lifecycle {
always all card : Card | card.status' = card.status or card.status' = card.status.next
}
check card_lifecycle for 6 but exactly 2 Customer, 4 steps
run { example } for 6 but exactly 2 Customer, 4 stepsand it turns out that fun and pred do not share a namespace, so can name both cancel, which reads better in the visualiser. Is your experience that this causes problems?
I hid this fact because I feared it would be even more mind-boggling 
I seem to recall I had one issue some time but I haven’t kept a record so I’m not sure. As far as I’m concerned, I use the same name.
Looks good to me.
Remark: cards' = cards - customer->toCancel + customer->replacement could be simplified as:
cards' = cards ++ customer->replacement.
except that cards is one customer to many cards, whereas status is one card to one status.
Oops, right, you cancel one card but keep the others, of course.
1 Like
Ah, ok, that’s an interesting tip.
As to {z}, that’s because I haven’t full internalised that Alloy doesn’t have atoms, only singleton sets.
This is a great example,
in the text mode one can see the used event and the arguments.
…
skolem $_cancel={Cancel$0->Card$2->Card$3}
skolem $_skip={}
skolem $events={Cancel$0}
But, when I run this model with kodkod, these skolems aren’t available there.
Any idea why?
The kodkod output is the same with Alloy Analyzer text output, but the skolems _cancel and _skip are missing.
This is because predicates and functions do not exist at the Kodkod level. When the compilation to Kodkod happens, all calls to predicates and functions are unfolded away.
(PS: in traces, you could even have written always some events instead of always (skip or some toCancel, replacement: Card | cancel[toCancel, replacement])).