This my first post, so thanks for the AMAZING tool that is Alloy. In our times, people sometimes feel entitled to the good stuff. But we know it takes a lot of effort. Alloy is an incredible contribution to the community!
I am trying to model a Virtual Machine with Services that are spawned, acquiring a PID.
I designed the spawn predicate to avoid two services being assigned the same PID.
Then I wrote run to init, run spawn a couple times and assert that two services share a PID.
But unfortunately I get examples, which means my model is not correct.
Could someone help with the basics?
Why can it find a model if the spawn predicate
requires that a new pid is not used by any service?
This should make for fresh pids.
Why there are conditions with more than
one new pid? There is a framing condition to say
that all other services remain the same…
Is this style of quantification correct the problem? I tried to avoid one s : Service, p : Pid | spawn[s,p] to make it more succint.
sig Service {
var pid : lone Pid
}
sig Pid {}
pred spawn {
one s : Service, p : Pid {
no s.pid
p not in Service.pid
s.pid' = p
(Service - s).pid' = (Service - s).pid
p in Service.pid'
}
}
fun online : set Pid {
{ p : Pid | p in Service.pid }
}
pred init {
no Service.pid
}
pred stutter {
Service.pid' = Service.pid
}
pred sharing {
some s : Service |
some t : Service |
s != t and s.pid = t.pid and some s.pid
}
run {
init
and after spawn
and after after spawn
and after after after sharing
}
Actually no: if you look at at states 2 and 3 of the trace, you’ll see that in both cases you indeed have (Service - Service$1).pid' = (Service - Service$1).pid (you can see this in going to state 2 and then use the Evaluator), while there was a change for Service$2.
This is because the frame condition is too lax: you don’t say that pid shouldn’t change for each service (except s) but that pid shouldn’t change for the union of all services other than s. You could then rather write all s2: Service - s | s2.pid' = s2.pid.
In general, I see two issues with this sort of quantification:
one is a treacherous quantifier, because saying one a:A, b: B| ... is different than one a:A | one b:B | .... some, all and no do not suffer from this source of confusion.
for events, you usually expect other stuff to be unchanged due to frame conditions, so the fact that there is exactly one pair of service and pid that changes should often be a property of your model rather than something you enforce.
All in all, I rewrote your model in what I think is a bit more idiomatic. Observe how spawn states that pid changes in s->p but remains otherwise the same.
sig Service {
var pid : lone Pid
}
sig Pid {}
pred init {
no pid
}
pred spawn[s: Service, p: Pid] {
no s.pid
p not in Service.pid
pid' = pid + s->p
}
pred stutter {
pid' = pid
}
fact traces {
init
always some s: Service, p: Pid | spawn[s, p] or stutter
}
pred sharing {
some disj s, t : Service | s.pid = t.pid and some s.pid
}
run {}
check {
always not sharing
}