A deadlock is when you reach a state from which no transition is possible: so imagine any UI where you reach a state where no action is possible anymore… clicking on a button has no effect, you can’t use a menu entry, or worse for critical systems…
Since @hwayne’s a heavy user of TLA+ and its TLC model-checker, he may be referring in part to the fact that the TLA+ toolbox has a handy builtin option to check for deadlocks. But that’s only a supposition.
Checking for the absence of deadlock is definitely possible in Alloy 6: however, since the Alloy 6 technique only considers infinite traces and a deadlock precisely induces a finite trace, deadlocks would be skipped if we didn’t model them differently. The classic approach, also recommended in TLA+, is to add a stuttering event to your spec. This way, a deadlock will now appear as an infinite trace ending in a state with a self-looping stuttering transition. Adding a stuttering event is worthwhile for several reasons so that’s not an issue. Now you may check that there is no trace such that you eventually stutter infinitely, i.e. in every trace, the state changes infinitely often (always eventually no stutter).
Not that I know.
I had the same kind of interest in FSMs as you but it’s not clear to me whether the operational nature of statecharts fits that well with the “declarative” nature of a specification language like Alloy. FSMs usually fix a lot of stuff (states, in particular) while, in Alloy, we usually want to leave the spec as open as possible.
Actually, I think the TLA+ definition of absence of deadlock is that some action is enabled. The advantage is that in TLA+ you have a keyword ENABLED that given an action (or disjunction of actions) determines the respective enabledness condition, so it is trivial to specify a property that can be used to check that there are no deadlocks. In Alloy 6 you can do the same but you have to specify the enabledness condition manually - most of the times it is trivial (it is just the disjunction of the guards of the actions), but in some cases it can be a bit tricky if there is some “interference” between the guards and other facts in the model.
In Alloy 6 you can do the same but you have to specify the enabledness condition manually - most of the times it is trivial (it is just the disjunction of the guards of the actions), but in some cases it can be a bit tricky if there is some “interference” between the guards and other facts in the model.
Could you provide an example of interference? There’s no change I could figure this out myself.
sig Person {
var friends : lone Person
}
fact NoSelfFriends {
always {
no p : Person | p in p.friends
}
}
pred add[a,b : Person] {
friends' = friends + a->b
}
pred stutter {
friends' = friends
}
fact Behavior {
no friends
always (stutter or some a,b : Person | add[a,b])
}
In this system, we have a single action which is to add a friend. That action has no explicit guard, only an effect saying what should be the value of friends in the next state.
In this system we have a deadlock, because we can reach a state where no action besides stutter is enabled. To check that there are no deadlocks we need to check that it is always the case that some action is enabled. However in this case, the enabledness condition of action add is not just its explicit guard (true in this case, since there is none specified). Due to the fact NoSelfFriends, parameters a and b cannot be the same person, and due to the multiplicity constraint lone in the declaration of friends we can only add a friend if none exists at the moment. So to check that there are no deadlocks we should use the following enabledness condition.
pred add_enabled[a,b : Person] {
a != b and no a.friends
}
check NoDeadlocks {
always (some a,b : Person | add_enabled[a,b])
}
This fact yields a counter-example, as expected, whatever the scope for Person.