SMV in this directory is standard SMV r2.4 with the added features: - Dynamic variable reordering - Quantitative property computing. COMPUTE MIN[start, event] gives the length of the minimum path from start to event. COMPUTE MAX[start, event] gives the length of the maximum path from start to event. See examples/periodic.smv for an example of usage of the features above. *** Important *** To compute quantitative properties, smv *must* be used with the -f option (compute the reachable set of states beforehand). If this option is not used, the results will be wrong. Notice that these added features are still experimental code. The SMV code is stable, but the newly added features may be not.