In this modality the system behaves mostly like the original CMU SMV. It performs some of the steps described previously in a fixed sequence. The sequence can be modified via command line options that enable different computations at fixed positions.
In the batch mode the system executes the first five steps previously described. The computation of the reachable states can be enabled before the computation of fairness constraints via the ``-f'' command line options. After the first five steps, the system looks for specifications in the source file, following the verification of CTL formulas, quantitative characteristics, LTL formulas and finally the invariants, if any. If the reordering of variables has been enabled via the -reorder command line option at the end of the computation, the reordering of variables starts and the generated ordering is saved into a file.
>