-
Notifications
You must be signed in to change notification settings - Fork 0
/
t2.smv
187 lines (152 loc) · 7.75 KB
/
t2.smv
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
---------------------------------------------------------------------------
-- Trabalho 2 Metodos Formais. --
---------------------------------------------------------------------------
-- Nomes:
-- Arthur Sudbrack Ibarra
-- Felipe Grosze Nipper
-- Luiz Eduardo Mello dos Reis
-- Miguel Torres de Castro
-- Willian Magnum Albeche
---------------------------------------------------------------------------
-- TEMPORIZADOR. --
---------------------------------------------------------------------------
MODULE temporizador(reset)
VAR
tempo : 0 .. 3;
ASSIGN
init(tempo) := 0;
next(tempo) :=
case
reset : 0;
tempo = 3 : 3;
TRUE : tempo + 1;
esac;
DEFINE
timeout := tempo = 3;
---------------------------------------------------------------------------
-- CONTROLADOR --
---------------------------------------------------------------------------
MODULE main
VAR
veiculos_no_oeste : boolean;
veiculos_no_leste : boolean;
veiculos_sobre_ponte : boolean;
sinaleira_oeste : {verde, vermelho};
sinaleira_leste : {verde, vermelho};
vez_sinaleira : {oeste, leste};
temp : temporizador(temp.timeout);
ASSIGN
-- Inicialização.
init(veiculos_no_oeste) := FALSE;
init(veiculos_no_leste) := FALSE;
init(veiculos_sobre_ponte) := FALSE;
init(sinaleira_oeste) := vermelho;
init(sinaleira_leste) := vermelho;
init(vez_sinaleira) := oeste;
-- Transições de estado.
-- Regra que impede um veículos de estarem na ponte
-- se não havia veículos no oeste ou no leste no estado anterior.
next(veiculos_sobre_ponte) :=
case
!veiculos_no_oeste & !veiculos_no_leste : FALSE;
TRUE : {FALSE, TRUE};
esac;
-- Controla qual sinaleira tem direito de ficar verde.
next(vez_sinaleira) :=
case
-- Se ainda não deu timeout, mantém a vez da sinaleira atual.
!temp.timeout : vez_sinaleira;
-- Se deu timeout, passa a vez para a outra sinaleira.
vez_sinaleira = oeste : leste;
TRUE : oeste;
esac;
-- Controla a sinaleira oeste.
next(sinaleira_oeste) :=
case
-- Se deu timeout, fica vermelha.
temp.timeout : vermelho;
-- Se não tem veículos no oeste, fica vermelha.
!veiculos_no_oeste : vermelho;
-- Se tem veículos no oeste e nenhum sobre a ponte, fica verde.
-- Contanto que seja a vez dessa sinaleira.
vez_sinaleira = oeste & veiculos_no_oeste & !veiculos_sobre_ponte : verde;
-- Caso contrário, mantém a sinaleira no estado atual.
TRUE : sinaleira_oeste;
esac;
-- Controla a sinaleira leste.
next(sinaleira_leste) :=
case
-- Se deu timeout, fica vermelha.
temp.timeout : vermelho;
-- Se não tem veículos no leste, fica vermelha.
!veiculos_no_leste : vermelho;
-- Se tem veículos no leste e nenhum sobre a ponte, fica verde.
-- Contanto que seja a vez dessa sinaleira.
vez_sinaleira = leste & veiculos_no_leste & !veiculos_sobre_ponte : verde;
-- Caso contrário, mantém a sinaleira no estado atual.
TRUE : sinaleira_leste;
esac;
---------------------------------------------------------------------------
-- PROPRIEDADES --
---------------------------------------------------------------------------
---------------------------------------------------------------------------
-- LTL --
---------------------------------------------------------------------------
-- 1. Propriedade de segurança:
-- nunca é o caso que ambos os semáforos são "verde" ao mesmo tempo.
LTLSPEC G !(sinaleira_oeste = verde & sinaleira_leste = verde)
-- A fórmula acima é verdadeira e é desejada porque se ambos os semáforos
-- ficarem verdes ao mesmo tempo, pode ocorrer um acidente.
-- 2. Propriedade de vivacidade:
-- se um semáforo é "verde", então eventualmente ele será "vermelho".
LTLSPEC G ((sinaleira_oeste = verde) -> (F sinaleira_oeste = vermelho))
LTLSPEC G ((sinaleira_leste = verde) -> (F sinaleira_leste = vermelho))
-- As fórmulas acima são verdadeiras e são desejadas porque se um semáforo
-- ficar verde, ele deve ficar vermelho em algum momento, visto que se ele
-- ficar verde para sempre, os veículos do outro lado da ponte nunca poderão
-- atravessar.
-- 3. Sempre que existir um veículo na entrada do lado oeste da ponte, eventualmente o
-- semáforo do lado oeste será “verde”, dadas as seguintes suposições:
-- Se veículos estão sobre a ponte, eventualmente todos os veículos sairão da ponte;
-- Se um veículo está em um semáforo “vermelho”, ele permanece no semáforo
-- sob a luz “vermelha” até e incluindo o primeiro passo (se existir um) no qual o
-- semáforo muda para “verde”.
-- [OESTE]
-- Primeiro sub-item:
-- LTLSPEC (veiculos_sobre_ponte) -> (F !veiculos_sobre_ponte)
-- Segundo sub-item:
-- LTLSPEC (veiculos_no_oeste & sinaleira_oeste = vermelho) -> ((veiculos_no_oeste & sinaleira_oeste = vermelho) U (sinaleira_oeste = verde))
-- Item principal:
-- LTLSPEC (veiculos_no_oeste) -> (F sinaleira_oeste = verde)
-- Fórmula completa:
LTLSPEC G ((((veiculos_sobre_ponte) -> (F !veiculos_sobre_ponte)) & ((veiculos_no_oeste & sinaleira_oeste = vermelho) -> ((veiculos_no_oeste & sinaleira_oeste = vermelho) U (sinaleira_oeste = verde)))) -> ((veiculos_no_oeste) -> (F sinaleira_oeste = verde)))
-- [LESTE]
-- Primeiro sub-item:
-- LTLSPEC (veiculos_sobre_ponte) -> (F !veiculos_sobre_ponte)
-- Segundo sub-item:
-- LTLSPEC (veiculos_no_leste & sinaleira_leste = vermelho) -> ((veiculos_no_leste & sinaleira_leste = vermelho) U (sinaleira_leste = verde))
-- Item principal:
-- LTLSPEC (veiculos_no_leste) -> (F sinaleira_leste = verde)
-- Fórmula completa:
LTLSPEC G ((((veiculos_sobre_ponte) -> (F !veiculos_sobre_ponte)) & ((veiculos_no_leste & sinaleira_leste = vermelho) -> ((veiculos_no_leste & sinaleira_leste = vermelho) U (sinaleira_leste = verde)))) -> ((veiculos_no_leste) -> (F sinaleira_leste = verde)))
-- As fórmulas acima são verdadeiras e são desejadas, visto que as suposições
-- descrevem o comportamento esperado dos veículos e das sinaleiras. Se um
-- veículo está sobre a ponte, ele eventualmente sairá da ponte. Se um veículo
-- está em um semáforo vermelho, ele permanecerá no semáforo até que ele
-- fique verde. Se um veículo está na entrada do lado oeste, eventualmente o
-- semáforo do lado oeste ficará verde, e o mesmo vale para o lado leste.
---------------------------------------------------------------------------
-- CTL --
---------------------------------------------------------------------------
-- 1. Em algum momento o semáforo do lado oeste é
-- "verde" e em algum momento o semáforo do lado leste é “verde”.
CTLSPEC AG ((EF (sinaleira_oeste = verde)) & (EF (sinaleira_leste = verde)))
-- A fórmula acima é verdadeira e é desejada, visto que é desejado que ambos
-- os semáforos fiquem verdes em algum momento para que carros de ambos os
-- lados possam atravessar a ponte.
-- 2. Sempre que o semáforo do lado leste estiver "verde" e um veículo estiver
-- sobre a ponte, é possível que o semáforo do lado leste permaneça “verde” para sempre.
CTLSPEC AG ((sinaleira_leste = verde & veiculos_sobre_ponte) -> (EG sinaleira_leste = verde))
-- A fórmula acima é FALSA e realmente não é desejada, visto que se o semáforo do
-- lado leste ficar verde para sempre, os veículos do lado oeste nunca poderão
-- atravessar a ponte.