Is it possible in Alloy to predict the sequence of actions in order of priority of their implementation?

Question

I have an Alloy model describing lifts - there are many buildings B, which serves several lifters. Consider the situation of breakage elevators. Assume that simultaneously breaks several elevators in different homes and there are some reports of damage. The main issue is where should the lifter go first?

I describe this model and try to check the assertions in priority in order that where should go the lifter firstly:

sig Boolean {}
one sig True, False extends Boolean {}

sig Lift {broken:Boolean}

sig House {
  lift: set Lift,
  hospital:Boolean,
  alert:Boolean,
  people_hurt: Boolean
}

sig B1 extends House{}
fact {all b:B1|b.lift!=none}

sig P extends B1{}
fact {all b:P|b.people_hurt = True}

sig B2 extends P {}
fact {all b:B2| b.alert = True}

sig L extends House{}
fact {all b:L|b.alert = True}

sig B3 extends B1{}
fact{all b:B3|b.alert = True}

assert Priority1 {B3 = none}
assert Priority2 {B2 = none}

check Priority1 for 10 House, 10 Lift, 2 Boolean
check Priority2 for 10 House, 10 Lift, 2 Boolean

I used the Alloy Analyzer but didn't understand what it showed me. And the main question is - is it possible using this model about lifts predict the right sequence of evacuation of people?

Answer 1

Let us distinguish two questions here.

First, what is the Analyzer telling you?

Perhaps the easiest thing to do here is to talk you through a short session with the Analyzer.

When I load the model and ask the Analyzer to check the first assertion, it finds a counterexample. Since the instance has nine houses and eight lifts, it is kind of hard for me to see exactly what is going on, so one of the first things I do is to add a new command, check Priority1 for 3, to give me some instances that are smaller and quicker to understand.

The first counterexample for that request has three houses, one each of signatures B1, P, and B3, and one lift, which is broken. All three houses share the same lift. To make it easier to see how the houses differ, I customized the theme in the display of instances, to make all relations display as attributes (as well as arcs). So it's easy to see that the Analyzer has found a counterexample to the assertion, with

• a house named B1, with alert = False and people_hurt = True.
• a house named B3, with alert = True and people_hurt = False.
• a house named P, with alert = False and people_hurt = True.

The assertion being checked, Priority1, says that there will never be any instances of the model with any houses of signature B3 (which will all have at least one Lift and will all have alert set to True).

Since there don't seem to be any constraints that would prevent houses of signature B3 from existing, the fact that the Analyzer found a counter-example doesn't seem surprising.

The content of the model as I understand it is roughly this:

• There are lifts.
  (I'm not entirely certain what you mean by 'Lift' here; in British English the word 'lift' is used for what American English always calls an 'elevator'; from the wording of your note, I think you are regarding them as two different things. So I'm imagining a Lift as some kind of emergency equipment. [Otherwise, I don't see how different houses can share lifts.] From a formal point of view, of course, it doesn't matter; from a practical point of view, it means I don't understand very well what you're trying to say, and can only go by what you do say.)

• There are houses.
  Each house is associated with some set of Lifts, may have an alert, and may have people hurt.

• L is a subclass of houses. All houses in this subclass have an alert. (I'm not entirely certain what alert = True is intended to mean in the domain, so "have an alert" may not be the best way to describe this property; sorry.)

• B1 is a subclass of houses (disjoint from L). All houses in this subclass are associated with a non-empty set of lifts.

• B3 is a subclass of B1.
  All houses in this subclass have a non-empty set of lifts and have an alert.

• P is another subclass of B1 (disjoint from B3). All houses in this subclass have a non-empty set of lifts and have people hurt.

• B2 is a subclass of P.
  All houses in this subclass have a non-empty set of lifts, have people hurt, and have an alert.

(It is probably more convenient in the long run to restructure your signature hierarchy, but let's postpone that to the second question.)

The model also contains two assertions, both easily falsifiable:

• There will be no instances of signature B3.
• There will be no instances of signature B2.

Second, how can you use Alloy to model the problem of optimizing emergency response?

I won't try to answer this question in full; for one thing, I'm out of time, and for another, I'm not entirely certain I understand the requirements. So I'll limit myself to some general advice.

If you want to model a collection of houses, some of which have alarms and some of which don't, some which have people hurt and some which don't, it's probably more convenient to define signatures like

sig People_Hurt in House {}
sig Alert_Yes in House {}

Then your constraints can refer simply to the set of houses with people hurt by referring to People_Hurt and not by indirection over checking the value of a people_hurt relation which maps House to Boolean. (Your Boolean type is not bad, just unnecessary. If you want to keep it, make the Boolean sig abstract, then you don't need to single out "2 Boolean" in your scopes.) There's an example of what I mean in Jackson's book -- look for the model of traffic lights.

If you just want to be able to say, given a particular set of houses, with varying degrees of damage and injury, which houses should have top priority for first responders, you can probably just try to define a predicate that identifies the top-priority houses for the given model instance.

If you want to model a sequence of response: first this house, then this, then you have a more complex task because you'll need to model changes of state. It's worth doing, but my most important advice is: start small, and just work on getting the description of the situation right: write the rules for houses, damage, and injury, and keep generating instances until you are getting the kinds of instances you need. Then start worrying about identifying the top-priority houses. And only then start thinking about sequences of events. (Just my advice, of course; your mileage may vary.)