Pequeno caso de estudo

Considere agora a especificação SPL apresentada na figura 2.2. Este programa é uma possível solução para o exercício 7 do capítulo anterior.

  

Figure 2.2: Possível solução para o controlador de um cruzamento

local aprox_carro, aprox_comboio : bool where 
      (aprox_carro, aprox_comboio ) = (false, false);
local cancela_aberta, sinal_verde : bool where 
      (cancela_aberta, sinal_verde) = (false, false);

Estrada :: [
        e0: loop forever do [
                e1: noncritical;
                e2: aprox_carro := true;
                e3: await cancela_aberta;
                e4: critical;
                e5: aprox_carro := false
        ]
]
||
Carril :: [
        c0: loop forever do [
                c1: noncritical;
                c2: aprox_comboio := true;
                c3: await sinal_verde;
                c4: critical;
                c5: aprox_comboio := false
        ]
]
||
Controlador :: [
        s0 : loop forever do [
                s1: when (aprox_carro) do [
                        s2:cancela_aberta := true; 
                        s3: await (!aprox_carro); 
                        s4: cancela_aberta := false
                ]
                or 
                s5: when (aprox_comboio) do [
                        s6:sinal_verde := true; 
                        s7: await (!aprox_comboio); 
                        s8: sinal_verde := false
                ]
        ]
]

Algumas das propriedades, e respectivas fórmulas temporais, que seria possível definir sobre esse programa são^2.2:

• A cancela nunca está aberta ao mesmo tempo que o sinal está verde.
  
  $$\Box \lnot(cancela\_aberta \land sinal\_verde)$$
  
  

• Nunca existem choques entre comboios e carros.
  
  $$\Box \lnot(at\_e4 \land at\_c4)$$
  
  

• Sempre que se aproxima um carro a cancela acabará por abrir.
  
  $$aprox\_carro \Rightarrow \Diamond cancela\_aberta$$
  
  

• Todos os comboios que se aproximam do cruzamento acabarão por passar.
  
  $$aprox\_comboio \Rightarrow \Diamond \lnot aprox\_comboio$$
  
  

• O valor da variável cancela_aberta segue sempre o valor de aprox_carro, i.é, sempre que se aproxima um carro a cancela abrirá e sempre que este se afasta ela volta a fechar.
  
  $$\forall u \cdot (aprox\_carro = u \Rightarrow \Diamond(cancela\_aberta = u))$$
  
  

• A cancela e o sinal estão, simultaneamente, fechada e vermelho um número infinito de vezes.
  
  $$\Box \Diamond (\lnot cancela\_aberta \land \lnot sinal\_verde)$$
  
  

• Sempre que se aproxima um comboio passará no máximo um carro até que o comboio passe.
  
  $$aprox\_comb \Rightarrow (\lnot at\_e4 \, \mathcal{W}\, at\_e4 \, \mathcal{W}\, \lnot at\_e4 \, \mathcal{W}\, at\_c4)$$