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 2012/11/18 14h:16