bmc_simulate_check_feasible_constraints - Performs a feasibility check on the list of given constraints. Constraints that are found to be feasible can be safely assumed not to cause deadlocks if used in the following step of incremental simulation.
bmc_simulate_check_feasible_constraints [-h | -q] [-c "formula"]*
This command generates feasibility problems for
each constraint. Every constraint is checked against current state
and FSM's transition relation, in order to exclude the possibility
of deadlocks. Constraints found to be feasible can be safely assumed
not to cause deadlocks if used in the following step of incremental
simulation.
Command options:
- -q
- Enables quiet mode. For each analyzed constraint "0" is
printed if the constraint is found to be unfeasible, "1" is
printed otherwise.
- -c "formula"
- Provide a constraint as a formula specified on
the command-line. This option can be specified multiple
times, in order to analyze a list of constraints.
Last updated on 2011/04/06 21h:12