Next dumb question. I had assumed that in code like the following, inP would only be applied to a P, even though it’s “called” with a Base. As far as I can tell, the only place a status can be set to In is in the inP predicate, but I still managed to have a Q set to In.
Guidance?
enum State { Out, In }
abstract sig Base { var state : one State }
sig P, Q extends Base {}
pred inP[p: P] {
p.state = Out
state' = state ++ p->In
}
pred skip { state' = state }
pred init { Base.state = Out }
fact traces {
init
always (some b: Base| inP[b] or skip[])
}
check {
always Q.state != In
} for 5 but 2 Q
Yes, this can be confusing. This is explained in Sect. B.6.4 of Daniel’s book:
Invocations of functions and predicates are type-checked by ensuring that the actual argument expressions are not disjoint from the formal arguments. Functions and predicates, like fields, may be overloaded, so long as all usages can be unambiguously resolved by the type checker.
The constraints implicit in the declarations of arguments of functions and predicates are conjoined to the body constraint when a function or predicate is run. When a function or predicate is invoked (that is, used within another function or predicate but not run directly), however, these implicit constraints are ignored. You should therefore not rely on such declaration constraints to have a semantic effect; they are intended as redundant documentation. A future version of Alloy may include a checking scheme that determines whether actual expressions have values compatible with the declaration constraints of formals.
TL;DR: if you want to enforce some constraints on parameters of a fun/pred, it’s usually better to add them to its body.
I agree it may be error-prone but I’m not sure it’s completely trivial to come up with a satisfying solution so easily. In any case, please file the issue on the Alloy repo (it’s already present in plain Alloy, and Electrum will soon join the Alloy repo).
Not before now. That I’m discovering the same problem rather makes my case, although it’s disconcerting that there’s no solution. If it can’t be fixed in the language, perhaps there should be a warning if people don’t add the extra type check.
I see that you are using this idiom for updating state:
state' = state ++ p->In
which I think has been recommended to me, too, and I don’t understand why, since this
p.state' = In
seems to have the same effect and, to me, reads better and has clearer intent.
demo:
enum State { Out, In, Fish}
abstract sig Base { var state : one State }
pred inB[p: Base] {
p.state' = In
}
pred fish[p: Base]{
p.state' in Fish
}
pred skip { state' = state }
pred init { Base.state = Out }
fact traces {
init
always (some b: Base| inB[b] or fish[b] or skip[])
}
run {
eventually Base.state in In
Base.state in Fish releases Base.state not in In
} for 5 but 2 Base
It’s not quite the same as the relational version ensures that none of the other values in the relationship change. The other version requires that I also say that
(Base - p).state' = (Base - p).state
I’m finding that I like the relational version now I’ve got used to it, not least because it reinforces the relational core to the language, and it makes common patterns easy to see.
This constraint still allows the states of other bases to change somehow (for example two different bases swapping their states). To ensure they do not change you could use the following constraint.
all b : Base - p | b.state' = b.state
Or, using the domain restriction operator, the following constraint.
(Base - p) <: state' = (Base - p) <: state
But I just prefer to specify the operation using the “relational version” state' = state ++ p->In and avoid the need for these frame conditions.
But it also suggests that there’s a huge training issue here as most of the introductory material starts with the ‘.’ notation, making it difficult for newbies to avoid bugs.
Yes. I have those stong frame conditons in my models, actually abstracted like allThingsUnchangedExceptFor. I can see now that the relational form obviates the need for them, and that this is very non-obvious to smart, motivated neophites (cough! cough!) but very obvious to experts. So, that’s a candidate Pattern.
Certainly. Now, there’s nothing wrong with using the allButFoo approach for some time. Once you’re used to always (cough) think of frame conditions, you’re good for the yellow belt. The aforementioned relational approach to frame conditions is for the orange belt (note: I’m not an expert in Karate belts) And there’s also the so-called Reiter approach (see Daniel’s book).
Where in Daniel’s book? It’s not the easiest to navigate for thematic content.
Meanwhile, how would one apply the pattern in a conext like this:
abstract sig Zone{}
one sig People extends Zone{}
one sig Cargo extends Zone{}
abstract sig Vehicle{
//structural relations
,zones: some Zone
//state
,var disj locked, unlocked: set zones //is this disfavoured?
}{
//facts about state
zones = locked + unlocked
//facts about structure
zones = People + Cargo
}
pred Vehicle::unlock[z: Zone]{
this.unlocked' = this.unlocked + z
this.locked' = this.locked - z
this.zonesOtherThanUnchanged[z]
this.otherVehiclesUnchanged
}
pred Vehicle::lock[z: Zone]{
this.locked' = this.locked + z
this.unlocked' = this.unlocked - z
this.zonesOtherThanUnchanged[z]
this.otherVehiclesUnchanged
}
pred Vehicle::zoneUnchanged[z: Zone]{
z & this.locked = z & this.locked'
z & this.unlocked = z & this.unlocked'
}
pred Vehicle::zonesOtherThanUnchanged[z: Zone]{
all z: this.zones - z | this.zoneUnchanged[z]
}
pred Vehicle::otherVehiclesUnchanged{
all v: Vehicle - this | v.unchanged
}
pred Vehicle::unchanged{
this.locked' = this.locked
this.unlocked' = this.unlocked
}
Where there may be mulitple vehicles and in the absence of a -- relation? Does the desirability of the “relational” form for representing state changes with implied frame conditions mean that this apporach to state is disfavoured?
I don’t have the book with me. IIRC it’s in the section on the Hotel example.
As explained above, you must think in relational terms, meaning a field is a relation the first column of which is the enclosing signature. Then you must ask yourself on which tuple(s) this relation changes when a given event is fired.
You can then read ++ as “except” (this is TLA+ parlance): r' = r ++ (x->t->u) means "I’m no changing rexcept that x->t->u will replace every tuple in r which starts with (the value denoted by) x.
I don’t think there is a need for a -- operator: what would be its meaning w.r.t. -?
Now, I think your model is a bit too complex. Is it because it’s a simplification of a real model? E.g. you have many ...unchanged... predicates, featuring & in particular, and it seems it’s due to this non-essential complexity. So I’d first simplify the domain, before trying to fix the behavioral part of the specification (incl. frame conditions). I’m not exactly sure (perhaps I don’t understand your model well) because I’m very busy these days, but:
I guess People and Cargo shouldn’t be one. Why not put an exact bound of 1 in commands, if you want to study simple models first? You may add a some multiplicity if you want to avoid models without people or cargo.
Similarly, why equate Zone and zones? If it’s only to avoid superfluous zones (i.e. unattached to a car), I think it’s better to handle this in another way.
Also, it seems locked and unlocked partition zones at each step. The problem with having 3 relations is that you’ll have to somehow handle their consistency. I think this may be disfavoured. OTOH, if you only use 2 relations and compute the third out of the others, with a fun say, then some properties you try to ensure will be ensured by construction.
Isn’t this enough (notice the unlock method which I apply on purpose to theunlocked fun):
abstract sig Zone{}
some sig People extends Zone{}
some sig Cargo extends Zone{}
abstract sig Vehicle{
zones: disj some Zone,
var locked: set zones,
}
fun unlocked : Vehicle -> Zone {
zones - locked
}
pred Vehicle::unlock[z: Zone]{
unlocked' = unlocked + this->z
}
pred Vehicle::lock[z: Zone]{
locked' = locked + this->z
}
run {} for 3 but exactly 1 People, exactly 1 Cargo
And there’s also the so-called Reiter approach (see Daniel’s book).