Go to the first, previous, next, last section, table of contents.

4.1 Model Reading and Building

The following commands allow for the parsing and the compilation of the model into BDD.

Environment Variable: verbose_level

Controls the verbosity of the system. Possible values are integers from 0 (no messages) to 4 (full messages). The default value is 0.

Command: read_model [-h] [-i model-file]

Reads a NuSMV file. If the -i option is not specified, it reads from the file specified in the environment variable input_file.

-i model-file

Reads the model from file model-file, and sets the environment variable input_file to model-file.

Environment Variable: input_file

Stores the name of the input file containing the model. It can be set by the `set' command or by the command line option `-i'. There is no default value.

Command: flatten_hierarchy [-h]

Intantiates module declarations into the actual modules and processes. The instantiation substitutes the actual parameters for the formal parameters, and then prefixing the result by the instance name. This operation is performed on the textual representation, before any operation on decision diagrams is carried out.

Command: show_vars [-h] [-s] [-i] [-m | -o output-file]

Prints symbolic input and state variables of the model and their range of values (as defined in the input file).

-s

Prints only state variables.

-i

Prints only input variables.

-m

Pipes output through the program specified by the PAGER shell variable if defined, else through UNIX "more" command.

-o output-file

Writes the generated output to the file output-file.

Command: build_variables [-h] [-i order-file]

Generates the boolean BDD variables and the ADD (Algebraic Decision Diagrams) needed to encode propositionally the (symbolic) variables declared in the model.
order-file specifies the initial ordering of variables. By default the variables are created in the order in which they appear in a depth first traversal of the hierarchy.
The input order file can be partial and can contain variables not declared in the model. Variables not declared in the model are simply discarded. The variables declared in the model not listed in the input file are created at the end of the given ordering following the default ordering.

-i order-file

Sets the environment variable input_order_file to input-order-file, and reads the variable ordering to be used from file order-file. This can be combined with the write_order command. The variable ordering is written to a file, which can be inspected and reordered by the user, and then read back in.

Environment Variable: input_order_file

Indicates the file name containing the variable ordering to be used in building the model by the `build_variables' command. There is no default value.

Command: write_order [-h] | [-f order-file]

Writes the current order of BDD variables in the file specified in the environment variable output_order_file.

-f order-file

Sets the environment variable output_order_file to order-file and then writes the ordering into it.

Environment Variable: output_order_file

The file where the current variable ordering has to be written. The default value is `temp.ord'.

Command: build_model [-h] [-f] [-m method]

Compiles the flattened hierarchy into BDD (initial states, invariants, and transition relation) using the method specified in the environment variable partition_method for building the transition relation.

-m method

Sets the environment variable partition_method to the value method, and then builds the transition relation. Available methods are `Monolithic', `Disjunctive', `Conjunctive' and `Iwls95CP'.

-f

Forces the model construction using the specified method. By default, only one partition method is allowed. This option allows to overcome this default, and build the transition relation with different partitionings.

Environment Variable: partition_method

The method to be used in building the transition relation, and to compute images and preimages. Possible values are:

• Monolithic. No partitioning at all.
• Conjunctive. Conjunctive partitioning, with a simple threshold heuristic. Assignments are collected in a single cluster until its size grows over the value specified in the variable conj_part_threshold.
• Iwls95CP. Conjunctive partitioning, with clusters generated and ordered according to the heuristic described in [RAP+95]. Works in conjunction with the variables image_cluster_size, image_W1, image_W2, image_W3, image_W4.
• Disjunctive. Disjunctive partitioning. Available only for asynchronous models (i.e. if there are processes). A partition is built for each process in the model.

Environment Variable: conj_part_threshold

The limit of the size of clusters in conjunctive partitioning. The default value is 0 BDD nodes.

Environment Variables: image_cluster_size, image_W{1,2,3,4}

The parameters to configure the behavior of the Iwls95CP partitioning algorithm. image_cluster_size is used as threshold value for the clusters. The default value is 1000 BDD nodes. The other parameters attribute different weights to the different factors in the algorithm. The default values are 6, 1, 1, 2 respectively. (For a detailed description, please refer to [RAP+95].)

Command: print_iwls95info [-h] [-m | -o output-file]

This command prints out the information regarding each cluster. In particular for each cluster it prints out, the cluster number, the size of the cluster (in BDD nodes), the variables occurring in it, the size of the cube that has to be quantified out relative to the cluster, and the variables to be quantified out.

-m

Pipes the output generated by the command through the program specified by the PAGER shell variable if defined, or through the UNIX utility "more".

-o output-file

Writes the output produced to file output-file, rather than to the standard output.

Environment Variable: image_verbosity

Sets the verbosity for the image method Iwls95CP, possible values are 0 or 1. The default value is 0.

Command: print_iwls95options [-h]

This command prints out the configuration parameters of the IWLS95 clustering algorithm, i.e. image_verbosity, image_cluster_size and weights image_W{1,2,3,4}.

Command: compute_fairness [-h]

For each fairness constraint, computes the corresponding set of states.

Command: go [-h]

This command initializes the system for verification. It is equivalent to the command sequence read_model, flatten_hierarchy, build_variables, build_model, compute_fairness. If some commands have already been executed, then only the remaining ones will be invoked.

Command: process_model [-h] [-i model-file] [-m partition-method]

Reads the model, compiles it into BDD and performs the model checking of all the specification contained in it. If the environment variable forward_search has been set before, then the set of reachable states is computed. If the environment variables enable_reorder and reorder_method are set, then the reordering of variables is performed accordingly. This command simulates the batch behavior of NuSMV.

-i model-file

Sets the environment variable input_file to file model-file, and reads the model from file model-file.

-m partition-method

Sets the environment variable partition_method to partition-method and uses it as partitioning method.

Environment Variable: forward_search

Enables the computation of the reachable states during the process_model command and when used in conjunction with the ag_only_search environment variable enables the use of an ad hoc algorithm to verify invariants.

Command: check_trans [-h] [-m| -o output-file]

Checks if the transition relation is total. If the transition relation is not total then a potential deadlock state is showed out.

-m

Pipes the output generated by the command to the program specified by the PAGER shell variable if defined, else through the UNIX "more" command.

-o output-file

Writes the output generated by the command to the file output-file.

The reachable states are computed before in order to guarantee that deadlock states are actually reachable.

Environment Variable: check_trans

Controls the activation of the totality check of the transition relation during the process_model call. Possible values are 0 or 1. Default value is 0.