To sum things up, the example is about a radiotherapy control device and is explained with more details in the aforementioned article. The authors give a characterization of the unsafe property as follow:
The machine is unsafe when the electron beam is fired at high intensity and the shield is in low position.
There exists a trace that ends with theThis can be expressed by the goalfireaction, contains thehbaction and doesn't include anyhsaction.
[hb, fire] \\ [hs]
. The first list is an ordered list of actions that must appear in the final trace and the second is a list of gates that must not appear in it.
Trying this goal returns as first trace:That's exactly what we wanted and we can conclude that the machine is not safe. However, the attentive reader probably noticed that we cheated. Indeed, theoretically a trace including alb line(s): [7] ls line(s): [7] i/exit line(s): [7,7] xr line(s): [11] hb line(s): [7] el line(s): [12] fire line(s): [17]
lb
between the hb
and the fire
action also satisfies the goal above. So, if we want to avoid it, we have to put it in the list of excluded gates. The new goal is [hb, fire] \\
[hs, lb]
which lamentably fails to find any trace for the very simple reason that the initialization is then impossible (first lb
in our trace). The real goal should be: Find a trace that includesThat's not what was specified by the original goal. Right now, this kind of goal cannot be used. However, we can find a goal that is more strict. Indeed, if we consider two goalshband ends byfireso that there is nolband nohsbetween them.
G1
and G2
so that G1
is stricter than G2
, then each trace satisfying G1
also satisfies G2
. That's exactly what we did with the goal [hb, fire] \\ [hs, lb]
. And indeed it was stricter (we didn't find any trace although the trace found satisfies the real goal). So, let's try to solve the problem we had
with this goal where the first lb
was causing troubles. To do so, let's use one of the features of goal:If an action is in the goal and its gate is in the list of gates to avoid, then the action will be accepted.Now, let's consider the new goal
[lb, hb, fire] \\ [lb, hs]
. It is obviously stricter than the real one and if we try it we get a trace (the same as previously). The fact that we have a trace is enough to
conclude that the machine is unsafe. If we were to consider the very first goal, the existence is not enough, we have to check that there is
nolb
between the hb
and the fire
.
If we look more closely at the specification, we can see that we cannot have a lb
between a hb
and a fire
. The only place (except for the initialization) where we have a setup[lb, ls]
is at the following line:
setup[hb, hs] >> (fire; setup[lb, ls])
The consequence of this is that the very first goal was not that bad. That's why it gave a good trace...fire
action it also provides as experiments the status of the shield and of the beam. Therefore, the original property can be transformed as:
There exists a trace ending with the action fire !high !down
Those traces are exactly the ones the goal fire !high !down
will look for. And if we try it we get: And the mere existence of this trace allows us to conclude that the machine is not safe. That's much easier than with the basic LOTOS specification.lb line(s): [41] ls line(s): [41] xr line(s): [47] hb line(s): [61] el line(s): [48] fire !high:beam !down:shield line(s): [81]