Railway capacity is complex to define and analyze, and existing tools and methods used in practice require comprehensive models of the railway network and its timetables. Design engineers working within the limited scope of construction projects report that only ad-hoc, experience-based methods of capacity analysis are available to them. Designs have subtle capacity pitfalls which are discovered too late, only when network-wide timetables are made -- there is a mismatch between the scope of construction projects and the scope of capacity analysis, as currently practiced.

We suggest a language for capacity specifications suited for construction projects, expressing properties such as running time, train frequency, overtaking and crossing. The planning problem arising from verification of these properties is constrained by discrete control system logic, network topology, laws of motion, and sparse communication. The second-order linear differential equations describing train motion can be solved analytically, but the resulting expressions contain multiplication of real variables.

We argue that reasoning over the whole discrete/continuous space of solutions is not efficient with current state-of-the-art solvers, and we present instead a special-purpose SAT-based dispatch planning tool which solves the discrete part of the problem. Continuous dynamics and timing constraints are evaluated using discrete event simulation, and the two components communicate in a CEGAR-loop (counterexample-guided abstraction refinement). We show that our method is fast enough at relevant scales to provide agile verification in a design setting, and we present case studies based on data from existing infrastructure and ongoing construction projects.