Using the two track bidirectional station from previous examples, we now turn to verifying the running time for a single train across the station.

The properties to be verified are summarized in the usage file:

vehicle passengertrain length 150.0 accel 1.0 brake 0.9 maxspeed 20.0

movement passengertrain {
  visit #start [b1]
  visit #end [b2]
}

timing start end 150.0

Running the railperfcheck program on this usage gives success, and outputs the following dispatch plan:

route ra2
route rexita2
train t1 l=150.0 a=1.0 b=0.9 v=20.0 rentrya

The plan represents a witness for the satisfaction of the properties given in the usage file, and the results can be inspected as usual.