Rodin User’s Handbook v.2.8: Witnesses

2.8.5 Witnesses

The refinement of set_cars is more difficult since the event uses a parameter (the new value for cars_go). In order to refine it, we need a witness (3.2.4.4.4).

A witness is to an event’s parameter what a gluing invariant is to a variable: it is a mapping between the abstract parameter and the new parameter and allows the abstract parameter to disappear. In this example, the abstract parameter new_value is of type BOOL, and we introduce a new parameter new_value_colours of type COLOURS.

$\includegraphics[width=7mm]{img/warning_64.png}$
The naming of a witnesses’ label is extremely important. It must be the name of the abstract parameter. In our example, the label must be new_value

Let’s get started. We first provide the new variable, gluing invariant, typing invariant and initialisation as we have done before (at this point you can also rename the gluing invariant from the last section as gluing_peds in order to be able to determine between the two gluing invariants). Note that the traffic light for the cars can show more than one colour at a time. Therefore, the variable contains a set of colours instead of just one colour (as modelled for peds_colour):

$\includegraphics[width=7mm]{img/pencil_64.png}$

VARIABLES

$\tt cars\_ colours$

INVARIANTS

$\tt inv5 :$

$\it cars\_ colours \subseteq COLOURS$

$\tt gluing\_ cars :$

$\it cars\_ go = TRUE \mathbin \Leftrightarrow green \in cars\_ colours$

EVENTS

Initialisation

begin

$\tt init5 :$

$\it cars\_ colours := \{ red \}$

end

END

We also have to modify the guard on set_peds_green, which is something that you should now be able to figure out yourself (just replace cars_go = FALSE with green $\notin$ cars_colours).

The interesting piece is the last event, set_cars, which we rename as set_cars_colours. We change the parameter to new_value_colours and type it as a subset of COLOURS.

The witness appears in the with section of the event. The label must be new_value. The value itself must describe the relationship between the abstract parameter new_value and the new parameter new_value_colours. As we use the parameter as the new value for the variable cars_colours, the witness is an adaptation of the gluing invariant (we just replace cars_colours with new_value_colours).

$\includegraphics[width=7mm]{img/info_64.png}$
In most cases, the witness is a slightly modified gluing invariant.

Here is the resulting event:

$\includegraphics[width=7mm]{img/pencil_64.png}$

Event

set_cars_colours $\mathrel {\widehat=}$

refines

set_cars

any

$\it new\_ value\_ colours$

where

$\tt grd1 :$

$\it new\_ value\_ colours \subseteq COLOURS$

$\tt grd2 :$

$\it green \in new\_ value\_ colours \mathbin \Rightarrow peds\_ colour = red$

with

$\tt new\_ value :$

$\tt new\_ value = TRUE \mathbin \Leftrightarrow green \in new\_ value\_ colours$

then

$\tt act1 :$

$\it cars\_ colours := new\_ value\_ colours$

end

Now you can get rid of the variable cars_go and its initialisation clause, and there will not be any errors or warnings. But even though all proof obligations are now discharged, we’re not done yet. Even though the traffic light doesn’t violate the safety property from the abstract machine, it doesn’t behave the way described in Section 2.8.1. We still have to ensure that the lights are activated in the proper sequence. We can impose this behavior by adding four guards each of which define one transition:

$\includegraphics[width=7mm]{img/pencil_64.png}$

$\tt grd\_ y\_ r :$

$\it cars\_ colours = \{ yellow \} \mathbin \Rightarrow new\_ value\_ colours = \{ red \}$

$\tt grd\_ r\_ ry :$

$\it cars\_ colours = \{ red \} \mathbin \Rightarrow new\_ value\_ colours = \{ red, yellow \}$

$\tt grd\_ ry\_ g :$

$\it cars\_ colours = \{ red, yellow \} \mathbin \Rightarrow new\_ value\_ colours = \{ green \}$

$\tt grd\_ g\_ y :$

$\it cars\_ colours = \{ green \} \mathbin \Rightarrow new\_ value\_ colours = \{ yellow \}$

Rodin Handbook

2.8.5 Witnesses