Exercícios

1.

Escreva um ficheiro de especificação para o exemplo do controlador de um cruzamento que defina como objectivos de prova todas as fórmulas temporais exemplificadas na secção 2.3.

2.

Acrescente ao ficheiro definido na alínea anterior fórmulas temporais que especifiquem as seguintes propriedades (de acordo com a solução do problema apresentada):

• O primeiro comboio só aparece depois de aparecer o primeiro carro.
• Quando se aproxima um carro a cancela acabará por ficar aberta até o carro se afastar.
• Se um carro e um comboio chegarem simultameamente ao cruzamento, o comboio passa sempre primeiro que o carro.
• Sempre que um caro chega ao cruzamente a cancela abre-se logo no próximo estado.