10 lines
180 B
Promela
10 lines
180 B
Promela
/* safety: strict closing transitions */
|
|
ltl phi6 {
|
|
always (
|
|
(state[0] == ClosingState)
|
|
implies
|
|
(next (state[0] == ClosingState ||
|
|
state[0] == ClosedState))
|
|
)
|
|
}
|