A railroad crossing example

Below we present select benchmarks from the verification of a real-time rail-road crossing system. A full description of the rail-road crossing system as modeled and verified in STeP can be found in Nikolaj Bjørner, Zohar Manna, Henny B. Sipma and Tomás E. Uribe. Deductive Verification of Real-time Systems Using STeP.

The formulas below are generated by STeP as verification conditions from temporal proof-rules and are thus not directly user supplied.

This button will run our validity checking procedure on each of the formulas below:
The examples are established relative to the following background properties: 
local    T : rat
in       xsi1 : rat
in       xsi2 : rat
in       beta : rat
in       delta : rat
in       gamma_up : rat
in       gamma_down : rat
in       epsilon1 : rat
in       epsilon2 : rat
in       N : int
type     train_status == not_here | P | I
local    train_status : array [1..N] of train_status
local    last_enterI : array [1..N] of rat
local    first_enterI : array [1..N] of rat
type     gate_status == up | down | going_up | going_down
out      gate_status : gate_status
local    last_down : rat
local    last_up : rat
local    tick : rat
variable t0 : rat
variable t1 : rat
variable k : [1..N]

(0 < epsilon1 /\ 
  0 < epsilon2 /\ 
  0 < gamma_up /\ 
  0 < gamma_down /\ 
  0 < xsi1 /\ 0 < xsi2 /\ 0 < beta /\ 0 < delta)

/\
gamma_up <= xsi2

/\
gamma_down + beta + epsilon2 - epsilon1 <= xsi1

/\
gamma_down < epsilon1

/\
epsilon1 <= epsilon2

/\
(Forall i : [1..N] . 
   train_status[i] = not_here \/ 
   train_status[i] = P \/ train_status[i] = I)

/\
 (gate_status = up \/ 
  gate_status = going_up \/ 
  gate_status = going_down \/ gate_status = down)

Rail 1 
Forall i : [1..N] . 
 (Forall i : [1..N] . 
  T < first_enterI[i] --> ~(train_status[i] = I)) /\ 
 train_status[i] = P /\ first_enterI[i] <= T --> 
 (Forall i0 : [1..N] . 
  T < first_enterI[i0] --> 
  ~((update(train_status,I,i))[i0] = I))
Rail 2 
(Forall i : [1..N] . 
 (Forall i0 : [1..N] . 
  T < first_enterI[i0] --> 
  ~(i = i0 \/ I = train_status[i0])) \/ 
 ~(P = train_status[i]) \/ T < first_enterI[i]) \/ 
(1 <= N --> 
~(Forall i : [1..N] . 
  T < first_enterI[i] --> ~(I = train_status[i])))
Rail 3 
(Forall i : [1..N] . 
 (Forall i0 : [1..N] . 
  (if i = i0
      then 0 < epsilon1
      else T < first_enterI[i0]) --> 
  ~(if i = i0 then I = P else I = train_status[i0])) \/ 
 ~(train_status[i] = not_here)) \/ 
(1 <= N --> 
~(Forall i : [1..N] . 
  T < first_enterI[i] --> ~(I = train_status[i])))
Rail 4 
(Forall i : [1..N] . 
 T < first_enterI[i] --> ~(I = train_status[i])) /\ 
0 < tick /\ 
(Forall t : rat . 
 0 <= t /\ t <= tick --> 
 (gate_status = going_down --> T + t <= last_down) /\ 
 (gate_status = going_up --> T + t <= last_up) /\ 
 (Forall i : [1..N] . 
  P = train_status[i] --> T + t <= last_enterI[i]) /\ 
 (gate_status = up \/ gate_status = going_up --> 
 (Forall i : [1..N] . 
  train_status[i] = not_here \/ 
  T + gamma_down + t < first_enterI[i])) /\ 
 (gate_status = down \/ gate_status = going_down --> 
 (Exists i : [1..N] . 
  ~(train_status[i] = not_here) /\ 
  first_enterI[i] <= T + delta + gamma_down + gamma_up + 
                     t))) --> 
(Forall i : [1..N] . 
 T + tick < first_enterI[i] --> ~(I = train_status[i]))