The method used for image computation is displayed by the option -v 1. To change the image computation method, use the command set image_method, and then start again with the command flatten_hierarchy. The reachability computation makes extensive use of image computation. There are several user-settable options that can be used to affect the performance of image computation. See the documentation for the set command for these options.
Command options:
hints_file> hints_file contains a series of hints. A hint is
a formula that does not contain any temporal operators, so
hints_file has the same syntax as a file of invariants
used for check_invariant. The hints are used in the order given to
change the transition relation. The transition relation is
conjoined with the hint to yield an underapproximation of the
transition relation. If the hints are cleverly chosen, this may
speed up the computation considerably, because a search with the
changed transition relation may be much simpler than one with the
original transition relation, and results obtained can be reused, so
that we may never have to do an expensive search with the original
relation. See also: Ravi and Somenzi, Hints to accelerate symbolic
traversal. CHARME'99; Bloem, Ravi, and Somenzi, Efficient Decision
Procedures for Model Checking of Linear Time Logic Properties,
CAV'99; Bloem, Ravi, and Somenzi, Symbolic Guided Search for CTL
Model Checking, DAC'00. Not allowed with -A 2 or -i, and will only
work with iwls95 or monolithic image methods. The description of
some options for guided search can be found in the help page for
print_guided_search_options.
1: Print a summary of reachability analysis and some information about the image computation method (see print_img_info) and summarizes results of reachability:
2: Prints the detailed information about reachability analysis. For each printStep, it prints the MDD size of the reachable state set and the number of states in the set.
0: (default) Breadth First Search. No approximate reachability computation.
1: High Density Reachability Analysis (HD). Computes reachable states in a
manner that keeps BDD sizes under control. May be faster than BFS in some
cases. For larger circuits, this option should compute more reachable
states. For help on controlling options for HD, look up help on the command:
print_hd_options
print_hd_options. Refer to Ravi and Somenzi, ICCAD95. This
option is available only when VIS is linked with the CUDD package.
2. Approximate Reachability Don't Cares(ARDC). Computes over-approximate
reachable states. For help on controlling options for ARDC, look up help on
the command: print_ardc_options
print_ardc_options. Refer Moon's paper, ICCAD98 and 2
papers by Cho et al, December TCAD96: one is for State Space Decomposition
and the other is for Approximate FSM Traversal. The options -d, -g and -f are
not compatible with this option.
set. This option is incompatible with -i.
]
SideEffects [The reachable states, depth, initial states of the FSM are
stored.]
******************************************************************************/
static int
CommandComputeReach(
Hrc_Manager_t ** hmgr,
int argc,
char ** argv)
{
int c;
mdd_t *reachableStates = NIL(mdd_t);
mdd_t *initialStates;
long initialTime;
long finalTime;
static int verbosityLevel;
static int printStep;
static int timeOutPeriod;
Fsm_Fsm_t *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
static int reorderFlag;
static int reorderThreshold;
static int shellFlag;
static int depthValue;
static int incrementalFlag;
static int approxFlag;
static int ardc;
static int recompute;
Fsm_RchType_t rchType;
FILE *guideFile = NIL(FILE); /* file of hints for guided search */
array_t *guideArray = NIL(array_t);
Img_MethodType imgMethod;
/*
* These are the default values. These variables must be declared static
* to avoid lint warnings. Since they are static, we must reinitialize
* them outside of the variable declarations.
*/
verbosityLevel = 0;
printStep = 0;
timeOutPeriod = 0;
shellFlag = 0;
depthValue = 0;
incrementalFlag = 0;
rchType = Fsm_Rch_Default_c;
approxFlag = 0;
ardc = 0;
recompute = 0;
/*
* Parse command line options.
*/
util_getopt_reset();
while ((c = util_getopt(argc, argv, "d:fg:hir:s:t:v:A:DF")) != EOF) {
switch(c) {
case 'd':
depthValue = atoi(util_optarg);
break;
case 'f':
shellFlag = 1;
break;
case 'g':
guideFile = Cmd_FileOpen(util_optarg, "r", NIL(char *), 0);
if (guideFile == NIL(FILE)) {
fprintf(vis_stdout,
"** rch error: Guide file cannot be read. Check permissions and path\n");
goto usage;
}
break;
case 'h':
goto usage;
case 'i':
incrementalFlag = 1;
break;
case 'r':
reorderFlag = 1;
reorderThreshold = atoi(util_optarg);
break;
case 's':
printStep = atoi(util_optarg);
break;
case 't':
timeOutPeriod = atoi(util_optarg);
break;
case 'v':
verbosityLevel = atoi(util_optarg);
break;
case 'A' :
approxFlag = atoi(util_optarg);
if ((approxFlag > 2) || (approxFlag < 0)) {
goto usage;
}
break;
case 'D':
ardc = 1;
break;
case 'F':
recompute = 1;
break;
default:
goto usage;
}
}
if (c == EOF && argc != util_optind)
goto usage;
imgMethod = Img_UserSpecifiedMethod();
if ((approxFlag == 1) && (bdd_get_package_name() != CUDD)) {
fprintf(vis_stderr, "** rch error: compute_reach with -A 1 option is currently supported only by CUDD.\n");
return 1;
}
if (fsm == NIL(Fsm_Fsm_t)) {
return 1;
}
if (incrementalFlag && approxFlag) {
fprintf(vis_stdout,
"** rch error: Incremental flag and approx flag are incompatible.\n");
goto usage;
}
if (incrementalFlag && ardc) {
fprintf(vis_stdout,
"** rch error: The -i and -D flags are incompatible.\n");
goto usage;
}
if (depthValue && approxFlag == 2) {
fprintf(vis_stdout,
"** rch error: Depth value and over-approx flag are incompatible.\n");
goto usage;
}
if (shellFlag && approxFlag == 2) {
fprintf(vis_stdout,
"** rch error: Shell flag and over-approx flag are incompatible.\n");
goto usage;
}
if (guideFile != NIL(FILE)){
if(incrementalFlag) {
fprintf(vis_stdout, "** rch error: Guided search is not compatible with the -i flag\n");
goto usage;
}
if(approxFlag == 2){
fprintf(vis_stdout, "** rch error: Guided search is not compatible with Over-approx flag\n");
goto usage;
}
if(imgMethod != Img_Iwls95_c && imgMethod != Img_Monolithic_c &&
imgMethod != Img_Mlp_c){
fprintf(vis_stdout, "** rch error: Guided search can only be performed\n");
fprintf(vis_stdout, "with IWLS95, MLP, or Monolithic image methods.\n");
goto usage;
}
}/* if guided search requested */
/* Start the timeOut timer. */
if (timeOutPeriod > 0){
(void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
(void) alarm(timeOutPeriod);
if (setjmp(timeOutEnv) > 0) {
(void) fprintf(vis_stdout, "** rch info: Timeout occurred after %d seconds.\n",
timeOutPeriod);
(void) fprintf(vis_stdout, "** rch warning: The time out may have "
"corrupted the data.\n");
alarm(0);
return 1;
}
}
/* Make sure that the initial states can be computed without a problem. */
error_init();
initialStates = Fsm_FsmComputeInitialStates(fsm);
if (initialStates == NIL(mdd_t)) {
(void) fprintf(vis_stderr, "** rch error: Latch initialization function depends on another latch:\n");
(void) fprintf(vis_stderr, "%s", error_string());
(void) fprintf(vis_stderr, "\n");
(void) fprintf(vis_stderr, "** rch error: Initial states cannot be computed.\n");
return (1);
}
else {
mdd_free(initialStates);
}
/* translate approx flag */
switch(approxFlag) {
case 0: rchType = Fsm_Rch_Bfs_c; break;
case 1: rchType = Fsm_Rch_Hd_c; break;
case 2: rchType = Fsm_Rch_Oa_c; break;
default: rchType = Fsm_Rch_Default_c; break;
}
if (guideFile != NIL(FILE)) {
guideArray = Mc_ComputeGuideArray(fsm, guideFile);
if(guideArray == NIL(array_t))
return(1);
}
if (rchType == Fsm_Rch_Oa_c) {
array_t *apprReachableStates;
initialTime = util_cpu_time();
apprReachableStates = Fsm_FsmComputeOverApproximateReachableStates(fsm,
incrementalFlag, verbosityLevel, printStep, depthValue, shellFlag,
reorderFlag, reorderThreshold, recompute);
finalTime = util_cpu_time();
if (apprReachableStates == NIL(array_t)) {
(void)fprintf(vis_stdout,
"** rch error: Reachability computation failed, no rechable states\n");
return 1;
}
if (verbosityLevel > 0)
Fsm_ArdcPrintReachabilityResults(fsm, finalTime-initialTime);
alarm(0);
return(0);
}
/* Compute the reachable states. */
initialTime = util_cpu_time();
reachableStates = Fsm_FsmComputeReachableStates(
fsm, incrementalFlag, verbosityLevel, printStep, depthValue, shellFlag,
reorderFlag, reorderThreshold, rchType, ardc, recompute, NIL(array_t),
(verbosityLevel > 0), guideArray);
finalTime = util_cpu_time();
mdd_array_free(guideArray);
if (reachableStates == NIL(mdd_t)) {
(void)fprintf(vis_stdout, "** rch error: Reachability computation failed, no rechable states\n");
return 1;
}
if (verbosityLevel > 0){
if (fsm->imageInfo){
char *methodType =
Img_ImageInfoObtainMethodTypeAsString(fsm->imageInfo);
(void) fprintf(vis_stdout, "** rch info: Computing reachable states using the ");
(void) fprintf(vis_stdout, "%s image computation method.\n", methodType);
FREE(methodType);
(void)Img_ImageInfoPrintMethodParams(fsm->imageInfo,
vis_stdout);
if (Img_ImageInfoObtainMethodType(fsm->imageInfo) == Img_Tfm_c ||
Img_ImageInfoObtainMethodType(fsm->imageInfo) == Img_Hybrid_c) {
Img_TfmPrintStatistics(fsm->imageInfo, Img_Forward_c);
}
}
Fsm_FsmReachabilityPrintResults(fsm, finalTime-initialTime, approxFlag);
}
mdd_free(reachableStates);
alarm(0);
return (0);
usage:
(void) fprintf(vis_stderr, "usage: compute_reach [-d depthValue] [-h] [-f] [-i] [-g
Currently, only Buchi constraints are supported. A Buchi fairness constraint
is given by a list of individual Buchi conditions, B1, B2, ..., Bk, where Bi
is a set of FSM states. A state is fair if there exists an infinite path
from that state that intersects each Bi infinitely often.
The conditions are specified by a file containing at least one CTL formula
(see the VIS CTL and LTL syntax manual). In
particular, Bi is defined by a CTL formula, which represents the set of
states that makes the formula true (in the absence of any fairness
constraint). References to signal names in the network should be made using
the full hierarchical names. Note that the support of any wire referred to
in a formula should consist only of latches. Each CTL formula is terminated
by a semicolon.
Example: In the three conditions below, B1 contains those states that have a
next state where cntr.out is RED, B2 contains those where timer.active is 1,
and B3 contains those states for which every path from the state has
tlc.request=1 until tlc.acknowledge=1.
Command options:
Command options:
Command options:
Command options:
EX(cntr.out=RED);
(timer.active=1);
A(tlc.request=1 U tlc.acknowledge=1);
Command options:
]
SideEffects []
******************************************************************************/
static int
CommandReadFairness(
Hrc_Manager_t ** hmgr,
int argc,
char ** argv)
{
int c;
FILE *fp;
array_t *formulaArray;
Fsm_Fsm_t *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
/*
* Parse command line options.
*/
util_getopt_reset();
while ((c = util_getopt(argc, argv, "h")) != EOF) {
switch(c) {
case 'h':
goto usage;
default:
goto usage;
}
/* NOT REACHED */
}
if (fsm == NIL(Fsm_Fsm_t)) {
(void) fprintf(vis_stderr, "** fair error: Fairness constraint not recorded.\n");
return 1;
}
/*
* Open the fairness file.
*/
if (argc - util_optind == 0) {
(void) fprintf(vis_stderr, "** fair error: fairness file not provided\n");
goto usage;
}
else if (argc - util_optind > 1) {
(void) fprintf(vis_stderr, "** fair error: too many arguments\n");
goto usage;
}
fp = Cmd_FileOpen(argv[util_optind], "r", NIL(char *), 0);
if (fp == NIL(FILE)) {
return 1;
}
/*
* Parse the formulas in the file.
*/
formulaArray = Ctlp_FileParseFormulaArray(fp);
(void) fclose(fp);
if (formulaArray == NIL(array_t)) {
(void) fprintf(vis_stderr, "** fair error: error reading fairness conditions.\n");
return 1;
}
else if (array_n(formulaArray) == 0) {
(void) fprintf(vis_stderr, "** fair error: fairness file is empty.\n");
(void) fprintf(vis_stderr, "** fair error: Use reset_fairness to reset the fairness constraint.");
return 1;
}
else {
int j;
Fsm_Fairness_t *fairness;
Ntk_Network_t *network = Fsm_FsmReadNetwork(fsm);
/*
* First check that each formula is semantically correct wrt the network.
*/
error_init();
for (j = 0; j < array_n(formulaArray); j++) {
Ctlp_Formula_t *formula;
boolean status;
formula = array_fetch(Ctlp_Formula_t *, formulaArray, j);
status = Mc_FormulaStaticSemanticCheckOnNetwork(formula, network, FALSE);
if (status == FALSE) {
(void) fprintf(vis_stderr,
"** fair error: error reading fairness constraint ");
Ctlp_FormulaPrint(vis_stderr, formula);
(void) fprintf(vis_stderr, ":\n");
(void) fprintf(vis_stderr, "%s", error_string());
(void) fprintf(vis_stderr, "\n");
return 1;
}
}
/*
* Interpret the array of CTL formulas as a set of Buchi conditions.
* Hence, create a single disjunct, consisting of k conjuncts, where k is
* the number of CTL formulas read in. The jth conjunct has the jth
* formula as its finallyInf component, and NULL as its globallyInf
* component.
*/
fairness = FsmFairnessAlloc(fsm);
for (j = 0; j < array_n(formulaArray); j++) {
Ctlp_Formula_t *formula = array_fetch(Ctlp_Formula_t *, formulaArray, j);
FsmFairnessAddConjunct(fairness, formula, NIL(Ctlp_Formula_t), 0, j);
}
array_free(formulaArray); /* Don't free the formulas themselves. */
/*
* Remove any existing fairnessInfo associated with the FSM, and update
* the fairnessInfo.constraint with the new fairness just read.
*/
FsmFsmFairnessInfoUpdate(fsm, NIL(mdd_t), fairness, NIL(array_t));
return 0;
}
usage:
(void) fprintf(vis_stderr, "usage: read_fairness [-h] file\n");
(void) fprintf(vis_stderr, " -h print the command usage\n");
(void) fprintf(vis_stderr, " file file containing the list of conditions\n");
return 1;
}
/**Function********************************************************************
Synopsis [Implements the reset_fairness command.]
Description [If no network or FSM exists, does nothing. Otherwise, resets
the fairnessInfo associated with the FSM to the default case.]
CommandName [reset_fairness]
CommandSynopsis [reset the fairness constraint]
CommandArguments [\[-h\]]
CommandDescription [Remove any existing fairness constraint associated with
the FSM of the flattened network, and impose a single constraint, TRUE,
indicating that all states are "accepting".
]
SideEffects []
******************************************************************************/
static int
CommandResetFairness(
Hrc_Manager_t ** hmgr,
int argc,
char ** argv)
{
int c;
Fsm_Fsm_t *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
/*
* Parse command line options.
*/
util_getopt_reset();
while ((c = util_getopt(argc, argv, "h")) != EOF) {
switch(c) {
case 'h':
goto usage;
default:
goto usage;
}
/* NOT REACHED */
}
if (fsm == NIL(Fsm_Fsm_t)) {
return 1;
}
/*
* Remove any existing fairnessInfo associated with the FSM, and add back
* the default constraint.
*/
FsmFsmFairnessInfoUpdate(fsm, NIL(mdd_t), NIL(Fsm_Fairness_t), NIL(array_t));
fsm->fairnessInfo.constraint = FsmFsmCreateDefaultFairnessConstraint(fsm);
return 0;
usage:
(void) fprintf(vis_stderr, "usage: reset_fairness [-h]\n");
(void) fprintf(vis_stderr, " -h print the command usage\n");
return 1;
}
/**Function********************************************************************
Synopsis [Implements the print_fairness command.]
Description [If no network or FSM exists, does nothing. Otherwise, prints
the fairness constraint associated with the FSM. If no fairness
constraint exists, then prints a message to that affect.]
CommandName [print_fairness]
CommandSynopsis [print the fairness constraint of the flattened network]
CommandArguments [\[-h\]]
CommandDescription [Print the fairness constraint (i.e the set of Buchi
conditions) associated with the FSM of the flattened network. By default,
the flattened network has the single constraint TRUE, indicating that all
paths are fair.
]
SideEffects []
******************************************************************************/
static int
CommandPrintFairness(
Hrc_Manager_t ** hmgr,
int argc,
char ** argv)
{
int c;
Fsm_Fairness_t *constraint;
int numDisjuncts;
Fsm_Fsm_t *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
/*
* Parse command line options.
*/
util_getopt_reset();
while ((c = util_getopt(argc, argv, "h")) != EOF) {
switch(c) {
case 'h':
goto usage;
default:
goto usage;
}
/* NOT REACHED */
}
if (fsm == NIL(Fsm_Fsm_t)) {
return 1;
}
/*
* Print the fairness constraint. It is assumed that there is at least one
* disjunct present. Currently, only Buchi constraints can be printed out.
*/
constraint = Fsm_FsmReadFairnessConstraint(fsm);
assert(constraint != NIL(Fsm_Fairness_t));
numDisjuncts = Fsm_FairnessReadNumDisjuncts(constraint);
assert(numDisjuncts != 0);
if (numDisjuncts > 1) {
(void) fprintf(vis_stdout, "Fairness constraint not Buchi...");
(void) fprintf(vis_stdout, "don't know how to print.\n");
}
else {
int i;
int numConjuncts = Fsm_FairnessReadNumConjunctsOfDisjunct(constraint, 0);
(void) fprintf(vis_stdout, "Fairness constraint:\n");
for (i = 0; i < numConjuncts; i++) {
if (Fsm_FairnessReadGloballyInfFormula(constraint, 0, i) !=
NIL(Ctlp_Formula_t)) {
(void) fprintf(vis_stdout, "Fairness constraint not Buchi...");
(void) fprintf(vis_stdout, "don't know how to print.\n");
}
Ctlp_FormulaPrint(vis_stdout,
Fsm_FairnessReadFinallyInfFormula(constraint, 0, i));
(void) fprintf(vis_stdout, ";\n");
}
}
return 0;
usage:
(void) fprintf(vis_stderr, "usage: print_fairness [-h]\n");
(void) fprintf(vis_stderr, " -h print the command usage\n");
return 1;
}
/**Function********************************************************************
Synopsis [Implements the print_img_info command.]
CommandName [print_img_info]
CommandSynopsis [print information about the image method currently
in use]
CommandArguments [\[-b\] \[-f\] \[-h\] ]
CommandDescription [Prints information about the image computation method
currently being used by the FSM. This includes the particular values of
parameters used by the method for initialization. If the image information
does not exist, then this command forces the information to be
computed. If none of the flags (-b or -f) is set, forward
transition relation is computed.
]
SideEffects []
******************************************************************************/
static int
CommandPrintImageInfo(Hrc_Manager_t ** hmgr, int argc, char ** argv)
{
int c;
Img_ImageInfo_t *imageInfo;
Fsm_Fsm_t *fsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
int bwdImgFlag = 0;
int fwdImgFlag = 0;
util_getopt_reset();
while ((c = util_getopt(argc, argv, "bfh")) != EOF) {
switch(c) {
case 'b':
bwdImgFlag = 1;
break;
case 'f':
fwdImgFlag = 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if (fsm == NIL(Fsm_Fsm_t)) {
return 1;
}
if (!(bwdImgFlag || fwdImgFlag)){
fwdImgFlag = 1;
}
imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm, bwdImgFlag, fwdImgFlag);
Img_ImageInfoPrintMethodParams(imageInfo, vis_stdout);
return 0;
usage:
(void) fprintf(vis_stderr,"usage: print_image_method [-b] [-f] [-h]\n");
(void) fprintf(vis_stderr, " -b create the backward transition relation\n");
(void) fprintf(vis_stderr, " -f create the forward transition relation\n");
(void) fprintf(vis_stderr, " -h print the command usage\n");
return 1;
}
/**Function********************************************************************
Synopsis [Implements the print_hd_options command.]
CommandName [print_hd_options]
CommandSynopsis [print information about the HD options currently
in use]
CommandArguments [\[-h\] ]
CommandDescription [Prints information about the current HD options.
The HD method is an alternate method to compute a least fixpoint and
is provided with the compute_reach and check_invariant commands.
The method is described in Ravi and Somenzi, ICCAD95. The command
can be used only when compiled with the CUDD package.
Methods:
remap_ua : (Default) The BDD approximation method of DAC98 Ravi, Shiple, McMillan, Somenzi.
biased_rua : Approximation method similar to remap_ua, but uses a bias function. The bias function is set appropriate to the context.
under_approx : The BDD approximation method of Shiple's thesis.
heavy_branch : The BDD approximation method of ICCAD95 Ravi, Somenzi.
short_paths : The BDD approximation method of ICCAD95 Ravi, Somenzi.
compress : An approximation method that runs short_paths first and then remap_ua.
Methods:
brute_force : Computes the image of the entire reached set. May be fatal if the reached set is very large.
conjuncts : (Default) Computes the image of reached by decomposing into parts.
hybrid : Computes the image of a subset of reached. If no new states, then the reaminder is decomposed in parts.
For methods, refer hd_frontier_approx_method methods. Default is remap_ua.
Methods:
approx : (Default) Computes a partial image by under-approximating the intermediate products of image computation.
clipping : Computes a partial image by "clipping" the depth of recursion of the and-abstract computations during image computation.
For methods, refer hd_frontier_approx_method methods. Default is remap_ua.
Command options:
<method>
method must be one of the following:
0 : MBM (machine by machine).
1 : RFBF(reached frame by frame).
2 : TFBF(to frame by frame).
3 : TMBM(combination of MBM and TFBF).
4 : LMBM(least fixpoint MBM, default).
5 : TLMBM(combination of LMBM and TFBF).
<size>
size must be a positive integer (default = 8).
<affinity>
affinity must be a positive real (default = 0.5).
<iteration>
iteration must be a positive integer or zero.
<target>
target must be one of the following:
0 : constrain transition relation (default).
1 : constrain initial states.
2 : constrain both.
<method>
method must be one of the following:
0 : restrict (default).
1 : constrain
2 : compact (currently supported by only CUDD)
3 : squeeze (currently supported by only CUDD)
<method>
method must be one of the following:
yes : allow variable reorderings during consecutive image
constraining operations (default)
no : don't allow variable reorderings during consecutive
image constraining operations
<method>
method must be one of the following:
0 : do not abstract pseudo input variables
1 : abstract pseudo inputs before image computation (default)
2 : abstract pseudo inputs at every end of image computation
3 : abstract pseudo inputs at the end of approximate traversal
<method>
method must be one of the following:
yes : keep decomposed reachable stateses (default)
no : make a conjunction of reachable states of all submachines
<method>
method must be one of the following:
yes : use projected initial states for submachine (default)
no : use original initial states for submachine
<method>
method must be one of the following:
monolithic : use monolithic image computation
iwls95 : use iwls95 image computation (default)
mlp : use mlp image computation
tfm : use tfm image computation
hybrid : use hybrid image computation
<method>
method must be one of the following:
yes : use High Density for reachable states of submachines
no : use BFS for reachable states of submachines (default)
<method>
method must be one of the following:
yes : whenever partitioned transition relation changes,
reorders partitioned transition relation
no : no reordering of partitioned transition relation (default)
<method>
method must be one of the following:
0 : constrain w.r.t. the reachable states of fanin submachines
(default)
1 : constrain w.r.t. the reachable states of both fanin
submachines and itself
<method>
method must be one of the following:
0 : makes pseudo input variables with exact support
(default)
1 : makes pseudo input variables from all state
variables of the other submachines
2 : makes pseudo input variables from all state
variables of fanin submachines
<method>
method must be one of the following:
0 : use given initial states all the time
1 : use current reached states as initial states (default)
2 : use current frontier as initial states
<method>
method must be one of the following:
yes : use constrained transition relation for next iteration
no : use original transition relation for next iteration
(default)
<filename>
filename containing grouping information
<filename>
filename to write grouping information
<verbosity>
verbosity must be 0 - 3 (default = 0).
Command options:
<method>
method must be one of the following:
0 : input splitting (default)
1 : output splitting
2 : mixed (input split + output split)
<method>
method must be one of the following:
0 : support before splitting (default)
1 : support after splitting
2 : estimate BDD size after splitting
3 : top variable
<method>
method must be one of the following:
yes : choose either state or input variable as splitting
variable (default)
no : choose only state variable as splitting variable
<method>
method must be one of the following:
0 : do not convert to range computation
1 : convert image to range computation (default)
2 : use a threshold (tfm_range_threshold, default for
hybrid)
<method>
method must be one of the following:
yes : force to reorder before checking tfm_range_threshold
no : do not reorder (default)
<method>
method must be one of the following:
0 : the closest variable to top (default)
1 : the smallest BDD size after splitting
<method>
method must be one of the following:
0 : smallest BDD size (default)
1 : largest BDD size
2 : top variable
<method>
method must be one of the following:
yes : try to find a decomposable variable (articulation point)
no : do not try (default)
<method>
method must be one of the following:
yes : sort function vectors (default for tfm)
no : do not sort (default for hybrid)
<method>
method must be one of the following:
yes : print statistics
no : do not print (default)
<method>
method must be one of the following:
yes : print BDD size
no : do not print (default)
<method>
method must be one of the following:
yes : try cube splitting
no : do not try (default)
<method>
method must be one of the following:
0 : do not try (default)
1 : try to find essential variables
2 : on and off dynamically
<method>
method must be one of the following:
0 : do not print (default)
1 : print only at end
2 : print at every image computation
<method>
method must be one of the following:
0 : do not use cache (default for hybrid)
1 : use cache (default)
2 : store all intermediate results
<method>
method must be one of the following:
yes : use only one global cache (default)
no : use one cache per machine
<method>
method must be one of the following:
0 : flush cache only when requested
1 : flush cache at the end of image computation (default)
2 : flush cache before reordering
<method>
method must be one of the following:
yes : compose all
no : do not compose (default)
<method>
method must be one of the following:
0 : input splitting (domain cofactoring, default)
1 : output splitting (constraint cofactoring)
2 : mixed (input split + output split)
3 : substitution
<method>
method must be one of the following:
0 : support before splitting (default)
1 : support after splitting
2 : estimate BDD size after splitting
3 : top variable
<method>
method must be one of the following:
0 : smallest BDD size (default)
1 : largest BDD size
2 : top variable
<method>
method must be one of the following:
0 : substitution (default)
1 : constraint cofactoring
2 : hybrid
<method>
method must be one of the following:
yes : minimize function vector w.r.t. a chosen function
in constraint cofactoring
no : do not minimize (default)
<verbosity>
verbosity must be 0 - 2 (default = 0).
Command options:
<mode>
mode must be one of the following:
0 : start with only transition function and build transition
relation on demand
1 : start with both transition function and relation (default)
2 : start with only transition relation. Only this mode
can deal with nondeterminism.
<method>
method must be one of the following:
0 : use support (default)
1 : use estimate BDD size
<method>
method must be one of the following:
yes : build partial transition relation
no : build full transition relation (default)
<method>
method must be one of the following:
0 : use BDD size (default)
1 : use support
<method>
method must be one of the following:
yes : apply splitting to transition relation at once
no : do not apply (default)
<method>
method must be one of the following:
0 : use only lambda
1 : use lambda and also special checks to conjoin
2 : use lambda and also improvement
3 : use all (default)
<method>
method must be one of the following:
yes : reorder relation array with from to conjoin (default)
no : reorder relation array without from to conjoin
<method>
method must be one of the following:
yes : reorder relation array with from to conjoin
no : reorder relation array without from to conjoin (default)
<method>
method must be one of the following:
0 : total lifetime with ps/pi variables (default)
1 : active lifetime with ps/pi variables
2 : total lifetime with ps/ns/pi variables
<method>
method must be one of the following:
0 : total lifetime with ns/pi variables
1 : active lifetime with ps/pi variables
2 : total lifetime with ps/ns/pi variables (default)
3 : total lifetime with ps/pi variables
<method>
method must be one of the following:
yes : include from set in lambda computation (default)
no : do not include
<method>
method must be one of the following:
yes : use transition relation (default)
no : use transition function vector
<method>
method must be one of the following:
yes : compute lambda after clustering
no : do not cluster (default)
<method>
method must be one of the following:
yes : rebuild transition relation from function vector
whenever the function vector changes
no : do not rebuild (default)
<method>
method must be one of the following:
yes : keep all primary input variables in forward transition
relation.
no : quantify out local primary input variables from the
transition relation. (default)
<method>
method must be one of the following:
yes : keep all primary input variables in backward transition
relation and preimages.
no : quantify out local primary input variables from the
transition relation. (default)
<method>
method must be one of the following:
yes : canonicalize the function vector
no : do not canonicalize (default)
lt;methodgt;
method must be one of the following:
iwls95 (default) mlp
Command options:
<method>
method must be one of the following:
0 : linear clustering
1 : affinity based tree clustering (default)
<method>
method must be one of the following:
0 : no reordering after clustering (default)
1 : reorder using MLP after clustering (inside)
2 : reorder using MLP after clustering (outside)
3 : reorder using IWLS95 after clustering
<method>
method must be one of the following:
0 : no reordering after clustering (default)
1 : reorder using MLP after clustering (inside)
2 : reorder using MLP after clustering (outside)
3 : reorder using IWLS95 after clustering
<method>
method must be one of the following:
0 : no postprocessing (default)
1 : do postprocesing after ordering
2 : do postprocesing after clustering or reordering
3 : do both 1 and 2
Command options:
i1,i2,...,in, with n at
most the number of hints that you specify . The k'th hint will
be used for ik iterations (images). A value of 0
causes the hint to be applied to convergence. Not setting this option is
like setting it to 0,0,...,0. If length of the specified
sequence is less than the number of hints, the sequence is padded with
zeroes.