lang_empty - perform language emptiness check on a flattened network _________________________________________________________________ lang_empty [-b] [-d ] [-f ] [-h] [-i] [-s] [-t ] [-v ] [-A ] [-D ] [-S ] [-L ] Performs language emptiness check on a flattened network. The language is not empty when there is a fair path starting at an initial state. Before calling this command, the user should have initialized the design by calling the command [1]init_verify. A fairness constraint can be read in by calling the [2]read_fairness command; if none is specified, all paths are taken to be fair. The system is reduced automatically with respect to the set of fairness constraints. If the language is not empty, a proof of this fact is generated. A proof is a fair path starting at an initial state. This is represented by a finite sequence of states starting at an initial state (the stem) leading to a fair cycle, i.e., a cycle on which there lies a state from each fairness condition. Command options: -b Use backward analysis when performing debugging; the default is to use forward analysis. This should be tried when the debugger spends a large amount of time when creating a path to a fair cycle. -d Specify whether to demonstrate a proof of the language non-emptiness dbg_level must be one of the following: 0 : No debugging performed. This is the default. 1 : Generate a path to a fair cycle. -f Write the debugger output to dbg_file. -h Print the command usage. -m Pipe debugger output through the UNIX utility more. -i Print input values causing transitions between states during debugging. Both primary and pseudo inputs are printed. -s Print debug output in the format accepted by the [3]simulate command. -t Specify the time out period (in seconds) after which the command aborts. By default this option is set to infinity. -v Specify verbosity level. This sets the amount of feedback on CPU usage and code status. verbosity_level must be one of the following: 0 : No feedback provided. This is the default. 1 : Feedback on code location. 2 : Feedback on code location and CPU usage. -A Specify whether the compositional SCC analysis algorithm, Divide and Compose (DnC), is enabled for language emptiness checking. The DnC algorithm first enumerates fair SCCs in an over-approximated abstract model, and then successively refines them in the more concrete models. Since non-fair SCCs can be ignored in the more concrete models, a potentially large part of the state space are pruned away early on when the computations are cheap. le_method must be one of the following: 0 : no use of Divide and Compose (Default). 1 : use Divide and Compose. -D Specify extent to which don't cares are used to simplify MDDs. Don't cares are minterms on which the value taken by functions does not affect the computation; potentially, these minterms can be used to simplify MDDs and reduce time taken to perform MDD computations. dc_level must be one of the following: 0 : No don't cares are used. 1 : Use unreachable states as don't cares. This is the default. -S Specify schedule for GSH algorithm, which generalizes the Emerson-Lei algorithm and is used to compute greatest fixpoints. The choice of schedule affects the sequence in which EX and EU operators are applied. It makes a difference only when fairness constraints are specified. must be one of the following: EL : EU and EX operators strictly alternate. This is the default. EL1 : EX is applied once for every application of all EUs. EL2 : EX is applied repeatedly after each application of all EUs. budget : a hybrid of EL and EL2. random : enabled operators are applied in (pseudo-)random order. off : GSH is disabled, and the old algorithm is used instead. The old algorithm uses the EL , but the termination checks are less sophisticated than in GSH. -F Use forward analysis in the computation of the greatest fixpoint. This option is incompatible with -d 1 or higher and can only be used with -D 1. -L Use the lockstep algorithm, which is based on fair SCC enumeration. must be one of the following: off : Lockstep is disabled. This is the default. Language emptiness is checked by computing a hull of the fair SCCs. on : Lockstep is enabled. all : Lockstep is enabled; all fair SCCs are enumerated instead of terminating as soon as one is found. This can be used to study the SCCs of a graph, but it is slower than the default option. n : (n is a positive integer). Lockstep is enabled and up to n fair SCCs are enumerated. This is less expensive than all , but still less efficient than on , even when n = 1 . _________________________________________________________________ Last updated on 20100410 00h02 References 1. file://localhost/projects/development/hsv/vis/common/doc/html/init_verifyCmd.html 2. file://localhost/projects/development/hsv/vis/common/doc/html/read_fairnessCmd.html 3. file://localhost/projects/development/hsv/vis/common/doc/html/simulateCmd.html