_bmc_test_tableau - Generates a random formula to logically test the equivalent tableau


_bmc_test_tableau [-h] | [-n property_index] | [[ -d max_depth] [-c max_conns] [-o operator]]

Use this hidden command to generate random formulae and to test the equivalent tableau. The first time this command is called in the current NuSMV session it creates a new smv file with a model and generates a random ltl spec to test tableau. The following times it is called it appends a new formula to the file. The generated model contains the same number of non-deterministic variables the currently model loaded into NuSMV contains.
You cannot call this command if the bmc_loopback is set to '*' (all loops).


Last updated on 2011/04/06 21h:13