Home

NuSMV 2.5 User Manual

1. E E F F F E FI FI next_a range FL_property next_a range FL_property next_e range FL_property next_e range FL_property next_event psl_bexpr FL_property next_event psl_bexpr FL_property next_event psl_bexpr number FL_property next_event psl_bexpr number FL_property next_event_a psl_bexpr psl_expr FL_property next_event_a psl_bexpr psl_expr FL_property next_event_e psl_bexpr psl_expr FL_property next_event_e psl_bexpr psl_expr FL_property OPERATORS ON SERES sequence FL_property sequence gt sequence sequence gt sequence always sequence G sequence never sequence eventually sequence within sequence_or_psl_bexpr psl_bexpr sequence within sequence_or_psl_bexpr psl_bexpr sequence within sequence_or_psl_bexpr psl_bexpr sequence 43 within_ sequence_or_psl_bexpr psl_bexpr sequence vr whilenot psl_bexpr sequence whilenot psl_bexpr sequence whilenot psl_bexpr sequence whilenot_ psl_bexpr sequence sequence_or_psl_bexpr sequence psl_bexpr Sequences i e istances of class sequence are defined as follows sequence SERE SER sequence psl_bexpr 7 COMPOSITION OPERATORS ERE SERE ERE SE RE ERE amp SE RE ERE amp amp SERE ER
2. 0004 2 3 13 Processes 2 3 16 Context 2 3 12 References to Module Components Variables and Defines 2 3 14 A Program and the main Module 2 3 15 Namespaces and Constraints on Declarations 2 3 17 ISA Declarations 0 00002 ee eee 2 4 Specifications 2 4 2 2 4 1 CTL Specifications Invariant Specifications A VO 0 0 0O NNNNA 2 4 3 LTL Specifications 2 4 4 Real Time CTL Specifications and Computations 2 4 5 PSL Specifications 2 5 Variable Order Input 0 2 5 1 Input File Syntax 2 00 2 5 2 Scalar Variablesl 2 4 2 5 3 Array Variables 00 2 6 Clusters Ordering 000 3 Running NuSMV interactively 3 1 Model Reading and Building o ooa 3 2 Commands for Checking Specifications 3 3 Commands for Bounded Model Checking 3 5 Simulation Commands o a 3 6 Execution Commands o oao aa a BET ATACES ns e e Hes ee ke a E cee E E Ae 3 7 1 Inspecting Traces 3 7 2 Displaying Traces 3 7 3 Trace Plugin Commands 3 8 Trace Plugins 3 8 1 Basic Trace Explainer 3 8 3 XML Format Printer 3 8 4 XML Format Reader 3 9 Interface to the DD Package 3 10 AdministrationCommands 3 11 Other Environment Variables
3. psl_expr psl_expr psl_expr psl_expr psl_expr psl_unary_expr psl_primary_expr psl_primary_expr psl_primary_expr psl_binary_expr psl_expr psl_expr psl_expr union psl_expr psl_expr in psl_expr psl_expr psl_expr psl_expr psl_expr psl_expr psl_expr psl_expr psl_expr psl_expr psl_expr psl_expr psl_expr psl_expr lt psl_expr psl_expr lt psl_expr psl_expr gt psl_expr psl_expr gt psl_expr psl_expr amp psl_expr psl_expr psl_expr psl_expr xor psl_expr psl_conditional_expr psl_expr psl_expr psl_expr psl_case_expr case psl_expr psl_expr psl_expr psl_expr endcase Among the subclasses of psl_expr we depict the class ps1_bexpr that will be used in the following to identify purely boolean i e not temporal expressions psl_property replicator psl_expr a replicated property FL_property abort psl_bexpr psl_expr lt gt psl_expr psl_expr gt psl_expr FL_property OBE_property replicator forall var_id index_range in value_set index_range 131 range range low_bound high_bound low_bound number identifier high_bound number identifier inf inifite high bound value_set value_range value_range boolean value_range psl_expr range FL_property PRIMITIVE LTL OPERATORS X FL_property FL_property L_property L_property L_property U FL_property L_property W FL_property 7 SIMPLE T
4. n number Computes only the property with index number P name Checks the COMPUTE property named name in the prop erty database check_property Checks a property into the current list of proper Command ties or a newly specified property check_property h n number P name c 1 i s q p formula IN context Checks the specified property taken from the property list or adds the new specified prop erty and checks it It is possible to check LTL CTL INVAR PSL and quantitative COMPUTE properties Every newly inserted property is inserted and checked See variable use_coi_size_sorting for changing properties verification order Command Options n number Checks the property stored at the given index P name Checks the property named name in the property database E Checks all the CTL properties not already checked If p is used the given formula is expected to be a CTL formula 1 Checks all the LTL properties not already checked If p is used the given formula is expected to be a LTL formula i Checks all the INVAR properties not already checked If p is used the given formula is expected to be a INVAR formula s Checks all the PSL properties not already checked If p is used the given formula is expected to be a PSL formula q Checks all the COMPUTE properties not already checked If p is used the given formula is expected to be a COMPUTE formul
5. shell_command Command 99 ey executes a shell command The shell_command is executed by calling bin sh c shell command If the command does not exists or you have not the right to execute it then an error message is printed alias Provides an alias for a command Command alias h lt name gt lt string gt The alias command if given no arguments will print the definition of all current aliases Given a single argument it will print the definition of that alias if any Given two arguments the keyword lt name gt becomes an alias for the command string lt string gt replacing any other alias with the same name Command Options lt name gt Alias lt string gt Command string It is possible to create aliases that take arguments by using the history substitution mechanism To protect the history substitution character 3 from immediate expansion it must be preceded by a when entering the alias For example uSMV gt alias read read_model i 1 smv set input_order_file l ord uSMV gt read short will create an alias read execute read model i short smv set input_order_file short ord And again uSMV gt alias echo2 echo Hi echo uSMV gt echo2 happy birthday will print Hi happy birthday CAVEAT Currently there is no check to see if there is a circular dependency in the alias definition e g uSMV gt alias foo echo
6. A variable identifier and define identifier are expressions which identify a variable or a define respectively Their syntax rules are define_identifier complex_identifier variable_identifier complex_identifier 13 toint basic_expr word and boolean to integer constant conversion integer to unsigned word constant conversion The syntax and semantics of complex_identifiers are explained in Section 2 3 12 Ref erences to Module Components page 32 All defines and variables referenced in expressions should be declared All identifiers variables defines symbolic constants etc can be used prior to their definition i e there is no constraint on order such as in C where a declaration of a vari able should always be placed in text above the variable use See more information about define and variable declarations in Section 2 3 2 DEFINE Declarations page 26 and Section 2 3 1 Variable Declarations page 23 A define is a kind of macro Every time a define is met in expressions it is substituted by the expression associated with this define Therefore the type of a define is the type of the associated expression in the current context Define expressions may contain next operators Normal rules apply No nested next operators variable_identifier represents state input and frozen variables The type of a variable is specified in its declaration For more information about variables see Sec tion Defi
7. NuSMV h help v vl int source script_file load script_file s old old_div_op smv_old disable_syntactic_checks dcx cpp pre pps ofm fm file obm bm file lp n idx is ic ils ips ii 0tt f r df flt AG coi i ivfile o ov file t tv file reorder dynamic m method disable_sexp2bdd_caching bdd_soh heuristics mono thresh cp_t cp cp t iwls95 cp_t noaffinity iwls95preorder bmc bmc_length k sat solver name sin onloff rin onl off ojeba algorithm input file where the meaning of the options is described below If input file is not provided in batch mode then the model is read from standard input help h Prints the command line help v _ verbose level Enables printing of additional information on the internal operations of NUSMV Setting verbose level to 1 gives the basic information Using this option makes you feel better since otherwise the program prints nothing until it finishes and there is no evidence that it is doing anything at all Set ting the verbose level higher than 1 enables printing of much extra information 109 keep_single_ve int source sc_file load sc_file S old old_div_op disable_syntactic checks keep_single value_vars dcx cpp pre pps Enables interactive mode Executes NuSMV commands from file sc_file same as source deprecated
8. cpp 110 cp cp t 113 oe aA acx 110 disable_sexp2bdd_caching 112 disable_ syntactic_checks I10 dynamic 112 f1t 0 s 1 hel1p 109 n 109 ic M1 ii 1 ils H1 is M1 iwls95preorder I13 iwls95 cp t 113 oe iv file 112 keep_single_value_vars 110 lp 111 mono 113 m method 112 noaffinity 113 n idx 111 obm bm file 0 T ojeba algorithm iapa eor ee o1d 110 o ov file pre pps reorder rin on off 113 r 11 sat_solver name 113 sin on off 113 source cmd file thresh cp t 113 t tv file v verbose level ASSIG constraint 28 FAIRNESS constraints B0 FROZENVAR declaration 25 IVAR declaration 24 26 VAR declaration 24 26 running temp ord 5 17 lt lt gt gt gt lt gt lt 1 107 107 mod 16 7 nusmvre 110 A administration commands 99 AND logical and bitwise array define declarations array type 8 Array Variables 46 B basic next expression Basic Trace Explainer batch running NUSMV bit selection operator boolean type bool operator C case expressions Commands for Bounded Model Checking 68 Commands for checking PSL specifications comments in NUSMV language 6 137 compassion constraints concatenation operator constant expressions CONSTANTS declarations 27 context CTL specificatio
9. flatten_hierarchy show_plugins encode variables show_property E show_traces show_vars write_flat_model write_reduced_model write_simplified_model build_flat_model build_model check_ctlspec check_invar check_Itispec check_property check_pslspec compute check_ItIlspec_simp check_fsm compute_reachable print_fsm_stats print_fair_states print_fair_transitions print_reachable_states build_boolean_model write_boolean_model goto_state pick_state simulate write_order bmc_simulate check_invar_bmc check_invar_bmc_inc check_Itispec_bmc check _Itlspec_bmc_inc check_ItIlspec_bmc_onepb check_ItIlspec_sbmc check_Itlspec_sbmc_inc check_pslspec gen_invar_bmc gen_Itispec_bmc gen_Itispec_bmc_onepb gen_Itlspec_sbmc Figure 3 1 The dependency among NUSMV commands 108 Chapter 4 Running NuSMV batch When the int option is not specified NUSMV runs as a batch program in the style of SMV performing some of the steps described in previous section in a fixed sequence system_prompt gt NuSMV command line options input file lt RET gt The program described in input file is processed and the corresponding finite state machine is built Then if input file contains formulas to verify their truth in the specified structure is evaluated For each formula which is not true a counterexample is printed The batch mode can be controlled with the following command line options
10. set command Environment variables can be either logical or utility autoexec Environment Variable Defines a command string to be automatically executed after every command processed by the command interpreter This may be useful for timing commands or tracing the progress of optimization on_failure_script_quits Environment Variable When a non fatal error occurs during the interactive mode the interactive interpreter sim ply stops the currently executed command prints the reason of the problem and prompts for a new command When set this variables makes the command interpreter quit when an error occur and then quit NUSMV This behaviour might be useful when the command source is controlled by either a system pipe or a shell script Under these conditions a mistake within the script interpreted by source or any unexpected error might hang the controlling script or pipe as by default the interpreter would simply give up the current execution and wait for further commands The default value of this environment variable is 0 106 filec Environment Variable Enables file completion a la csh If the system has been compiled with the readline library the user is able to perform file completion by typing the lt TAB gt key in a way similar to the file completion inside the bash shell If the system has not been compiled with the readline library a built in method to perform file completion a la
11. n number Checks the CTL property with index number in the prop erty database P name Checks the CTL property named name in the property database If the ag only search environment variable has been set then a specialized algorithm to check AG formulas is used instead of the standard model checking algorithms Since version 2 4 1 this command substitutes check spec that is deprecated check_spec Performs fair CTL model checking Command check_spec h m o output file n number p ctl expr IN context Performs fair CTL model checking Since version 2 4 1 this command is deprecated but still provided for backward compati bility reasons Use check_ct 1spec instead ag_only_search Environment Variable Enables the use of an ad hoc algorithm for checking AG formulas Given a formula of the form AG alpha the algorithm computes the set of states satisfying alpha and checks whether it contains the set of reachable states If this is not the case the formula is proved to be false forward_search Environment Variable 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 Since version 2 4 0 this option is set by default 60 Itl_tableau_forward_search Environment Variable Forces the computation of the set of reachable states for the tabl
12. puted reachable states incrementally using this option t seconds If specified forces the computation of reachable states to end after seconds seconds This limit could not be precise since the if the computation of a step is running when the limit occurs the computation is not interrupted until the end of the step print_reachable_states Prints out the number of reachable states Command print_reachable_states h v d f o filename Prints the number of reachable states of the given model In verbose mode prints also the list of all reachable states The reachable states are computed if needed Command Options v Prints the list of reachable states d Prints the list of reachable states with defines Requires v f Prints the formula representing the reachable states o filename Prints the result on the specified filename instead of on standard output check_fsm Checks the transition relation for totality Command check_fsm h m 0o output file 58 Checks if the transition relation is total If the transition relation is not total then a potential deadlock state is shown Command Options m Pipes the output generated by the command to the pro gram specified by the PAGER shell variable if defined else through the UNIX command more o output file Writes the output generated by the command to the file output file At the beginning reachable states are computed in order
13. _ word_value word_sign_specifier one of us word_width integer_number a number greater than zero word_base b Bio oj d ovDiffhi H word_value hex_digit word_value hex_digit word_value _ hex_digit one of 012345678 9abcde FABCDEF Note that e The width of a word must be a number strictly greater than 0 e Decimal word constants must be declared with the width specifier since the number of bits needed for an expression like 0d_0149 is unclear e Digits are restricted depending on the base the constant is given in 3999 e Digits can be separated by the underscore character _ to aid clarity for example 0b_0101_1111_1100 which is equivalent to 0b_010111111100 11 e For a given width N the value of a constant has to be in range 0 2 1 For decimal signed words both s and d are provided the value of a constant has to be in range Oise 2 e The number of bits in word constant has an implementation limit which for most systems is 64 bits Range Constant A range constant specifies a set of consecutive integer numbers For example a con stant 1 5 indicates the set of numbers 1 0 1 2 3 4 and 5 Other examples of range constant canbe 1 10 10 10 1 300 The syntactic rule of the range constant is the following range_constant integer_number integer_number with an additional constraint that the first integer number must be less than or equal to the second intege
14. and 1 has to be written as TRUE instead For backward compatibility options please see page 50 If Then Else expressions In certain cases the syntax described above may look a bit awkard In simpler cases it is possible to use the alternative terser e e e expression This construct is defined as follows cond_expr basic_exprl basic_expr2 This expression evaluates to basic_expr1 if the condition in cond_expr evaluates to true and to basic_expr2 otherwise Therefore the expressions condl expl exp2andcase cond1l expl TRUE expr2 esac are equivalent Basic Next Expression Next expressions refer to the values of variables in the next state For example if a variable v is a state variable then next v refers to that variable v in the next time step A next applied to a complex expression is a shorthand method of applying next to all the variables in the expressions recursively Example next 1 a b is equivalent to 1 next a next b Note that the next operator cannot be applied twice i e next next a is not allowed The syntactic rule is 5See 2 1 6 for information on set types and their counterpart types See Section Type Order page 9 for the information on the order of types 20 basic_next_expr next basic_expr Anext expression does not change the type Count Operator The count operator counts the number of expressions which are true The count operator is a synt
15. csh can be used This method is enabled with the set filec command The csh file comple tion method can be also enabled if the readline library has been used In this case the features offered by readline will be disabled shell_char Environment Variable shell_char specifies a character to be used as shell escape The default value of this environment variable is history_char Environment Variable history char specifies a character to be used in history substitutions The default value of this environment variable is open_path Environment Variable open_path in analogy to the shell variable PATH is a list of colon separated strings giving directories to be searched whenever a file is opened for read Typically the current directory is first in this list The standard system library NUuSMV_LIBRARY_PATH is always implicitly appended to the current path This provides a convenient short hand mechanism for reaching standard library files nusmvy_stderr Environment Variable Standard error normally stderr can be re directed to a file by setting the variable nusmv_stderr nusmy_stdout Environment Variable Standard output normally stdout can be re directed to a file by setting the internal variable nusmv_stdout nusmy_stdin Environment Variable Standard input normally st din can be re directed to a file by setting the internal variable nusmv_stdin 107
16. signed word N signed word N amp gt lt gt xor xnor boolean boolean boolean unsigned word N unsigned word N unsigned word N signed word N signed word N signed word N boolean boolean boolean integer integer boolean symbolic enum symbolic enum boolean integers and symbolic enum integers and symbolic enum boolean unsigned word N unsigned word N boolean signed word N signed word N boolean Index Subscript Operator exp exp2 array N M of subtype word N subtype array N M of subtype integer subtype the value of exp has to be in range N M Bit Wise Operators concatenation word N word M unsigned word N M where word e can be any of unsigned word e or signed word e expi lexp2 exp3 unsigned word N integer integer unsigned word exp3 exp2 1 signed word N integer integer unsigned word exp3 exp2 1 exressions exp2 and exp3 must be integers such that 0 lt expg lt exp3 lt N lt lt gt gt shift unsigned word N integer unsigned word N unsigned word N unsigned word e unsigned word N signed word N integer signed word N signed word N unsigned word e signed word N 121 Set Operators exp1 exp2 expn equivalent to consecutive union operations union boolean set boolean set boolean set integer set
17. the variable whose declaration declares the symbolic constants also has a full identifier Symbolic constants have a separate namespace so their identifiers may potentially be equal for example variable identifiers It is an error if the same identifier in an expression can simultaneously refer toa symbolic constant anda variable or a define A symbolic constant may be declared an arbitrary number of times but it must be declared at least once if it is used in an expression 2 3 16 Context Every module instance has its own context in which all expressions are analyzed The context can be defined as the full identifiers of variables declared in the module without their simple identifiers Let us consider the following example 35 MODULE main VAR a foo VAR b moo MODULE foo VAR c moo MODULE moo VAR d boolean The context of the module mainis emptyf the context of the module instance a and inside the module foo is a the contexts of module moo may be b if the module instance b is analyzed and a c if the module instance a c is analyzed 2 3 17 ISA Declarations There are cases in which some parts of a module could be shared among different modules or could be used as a module themselves In NUSMV it is possible to declare the common parts as separate modules and then use the ISA declaration to import the common parts inside a module declaration The syntax of an i
18. toint wordl signed unsigned extend next init unsigned word 1 boolean integer boolean boolean integer unsigned word N constant integer signed word N constant integer boolean unsigned word 1 unsigned word N signed word N signed word N unsigned word N unsigned word e integer unsigned word N integer signed word e integer signed word N integer any type the same type any type the same type boolean boolean no type integer integer no type integer integer set no type symbolic enum symbolic enum no type symbolic enum symbolic set no type integers and symbolic enum integers and symbolic enum no type integers and symbolic enum integers and symbolic set no type unsigned word N unsigned word N no type signed word N signed word N no type Implicit type conversion is performed on the right operand only 123 Appendix C Production Rules This appendix contains the syntactic production rules for writing a NUSMV program Identifiers identifier identifier _first_character identifier identifier_consecutive_character identifier _first_character one of ABCDEFGHIJIJKLUMNOPQRSTUVWXYZ abcdefghigjgkimnopqrstuvwxyz identifier _consecutive_character identifier _first_character digit one of digit one of 0123456789 Note th
19. 1 IVAR c TRUE FALSE The variable a is a state variable b is a frozen variable and c is an input variable In the following examples VAR d stopped running waiting finished VAR e 2 4 2 O VAR f 1 a 3 d q 4 the variables d e and f are of enumeration types and all their possible values are specified in the type specifiers oftheir declarations VAR g unsigned word 3 VAR h word 3 VAR i signed word 4 The variables g and h are of 3 bits wide unsigned word type i e unsigned word 3 and i is of 4 bits wide signed word type i e signed word 4 VAR j array 1 1 of boolean The variable j is an array of boolean elements with indexes 1 0 and 1 2 3 2 DEFINE Declarations In order to make descriptions more concise a symbol can be associated with a common expres sion and a DEFINE declaration introduces such a symbol The syntax for this kind of declaration is define_declaration DEFINE define_body define_body identifier simple_expr define_body identifier simple_expr DEFINE associates an identifier on the left hand side of the with an expression on the right side A define statement can be considered as a macro Whenever a define 26 identifier occurs in an expression the identifier is syntactically replaced by the ex pression it is associated with The associated expression is always evaluated in the context of the statement where the iden
20. 1 6 for more information about the set types and their counterpart types 4See 2 1 6 for more information about the set types and their counterpart types 19 basic_expr basic_expr case_body basic_expr basic_expr A case_expr returns the value of the first expression on the right hand side of such that the corresponding condition on the left hand side evaluates to TRUE For example the result of the expression case left_expression_1l right_expression_l left_expression_2 right_expression_2 left_expression_N right_expression_N esac is right_expression_k such that for all from 0 to k 1 left_expression_i is FALSE and left_expression_k is TRUE It is an error if all expressions on the left hand side evalu ate to FALSE The type of expressions on the left hand side must be boolean If one of the expression on the right is of a set type then if it is possible all remaining expressions on the right are converted to their counterpart set types The type of the whole expression is such a minimal typq that all of the expressions on the right after possible convertion to Set types can be implicitly converted to this type If this is not possible NUSMV throws an error Note Prior to version 2 5 1 using 1 as left_expression_N was pretty common e g case condl exprl cond2 expr2 1 exprN otherwis esac Since version 2 5 1 integer values are no longer implicitly casted to boolean
21. Assignments describe a system of equations that say how the FSM evolves through time With an arbitrary set of equations there is no guarantee that a solution exists or that it is unique We tackle this problem by placing certain restrictive syntactic rules on the structure of assignments thus guaranteeing that the program is implementable The restriction rules for assignments are e The single assignment rule each variable may be assigned only once e The circular dependency rule a set of equations must not have cycles in its depen dency graph not broken by delays The single assignment rule disregards conflicting definitions and can be formulated as one may either assign a value to a variable x or to next x and init x but not both For instance the following are legal assignments Example 1 x expri Example 2 init x expri Example 3 next x expri Example 4 init x expri next x exproa while the following are illegal assignments Example 1 x expri X 1 expra Example 2 init x expri init x expro Example 3 x expri init x expr2 Example 4 x expri next x expr2 29 If we have an assignment like x y then we say that x depends on y A combinatorial loop is a cycle of dependencies not broken by delays For instance the assignments x I Yi y i x form a combinat
22. Avoids to load the NUSMV_ commands con tained in nusmvre or in nusmvrce or in S NuSMV_LIBRARY_PATH master nusmvrc Keeps backward compatibility with older versions of NuSMV This option disables some new features like type checking and dumping of new extension to SMV files In ad dition if enabled case conditions also accepts 1 which is semantically equivalent to the truth value TRUE This backward compatibility feature has been added in NUSMV 2 5 1 in order to help porting of old SMV models Infact in versions older than 2 5 1 it was pretty common to use 1 in case conditions expressions For an example please see ea dae Enables the old semantics of and mod operations from NUSMV 2 3 0 instead of ANSI C semantics Disables all syntactic checks that will be performed when flattening the input model Warning If the model is not well formed NUSMV may result in unpredictable results use this option at your own risk Does not convert variables that have only one single possible value into constant DEFINEs Disables the generation of counter examples for prop erties that are proved to be false See also variable counter_examples Runs pre processor on SMV files before any of those speci fied with the pre option Specifies a list of pre processors to run in the order given on the input file before it is parsed by NUSMV Note that if the cpp command is used then the pre processors speci fie
23. PREDICATES process array of boolean integer real word wordl bool signed unsigned extend resize sizeof uwconst swconst EX AX EF AF EG AG E F O G H X Y Z A U S V T BU EBF ABF EBG ABG case esac mod next init union in xor xnor self TRUE FALSE count To represent various values we will use integer numbers which are any non empty sequence of decimal digits preceded by an optional unary minus integer_number digit digit integer_number digit and symbolic constants which are identifiers symbolic_constant identifier Examples of integer numbers and symbolic constants are 3 14 007 OK FAIL waiting stop The values of symbolic constants and integer numbers do not intersect 2 1 Types Overview This section provides an overview of the types that are recognised by NUSMV 2 1 1 Boolean The boolean type comprises symbolic values FALSE and TRUE 2 1 2 Integer The domain of the integer type is simply any whole number positive or negative At the mo ment there are implementation dependent constraints on the this type and integer numbers can only be in the range 2 1 to 231 1 more accurately these values are equivalent to the C C macros INT_MIN 1 and INT_MAX 2 1 3 Enumeration Types An enumeration type is a type specified by full enumerations of all the values that the type com prises For example the enumeration of values may be stopped running waiting
24. ables otherwise it prints out only the label t 1 of the state chosen where t is the number of the new trace that is the number of traces so far generated plus one Randomly picks a state from the set of initial states Enables the user to interactively pick up an initial state The user is requested to choose a state from a list of possible items every item in the list doesn t show frozen and state variables unchanged with respect to a previous item If the number of possible states is too high then the user has to specify some further constraints as simple expression Displays all state and frozen variables changed and un changed with respect to a previous item in an interactive picking This option works only if the i options has been specified Uses constraints to restrict the set of initial states in which the state has to be picked constraints must be enclosed between double quotes Picks state from trace state label A new simulation trace will be created by copying prefix of the source trace up to specified state 85 simulate Performs a simulation from the current selected state Command simulat h t constraints v r i a c constraints k steps Generates a sequence of at most steps states representing a possible execution of the model starting from the current state The current state must be set via the pick_state or goto_state commands It is possible to
25. alias Command unalias h lt alias names gt Removes the definition of an alias specified via the alias command Command Options lt alias names gt Aliases to be removed 105 unset Unsets an environment variable Command unset h lt variables gt A variable environment is maintained by the command interpreter The set command sets a variable to a particular value and the unset command removes the definition of a variable Command Options lt variables gt Variables to be unset usage Provides a dump of process statistics Command usage h Prints a formatted dump of processor specific usage statistics For Berkeley Unix this includes all of the information in the getrusage structure which Looks for a file called file name Command which h lt file_name gt Looks for a file in a set of directories which includes the current directory as well as those in the NUSMV path If it finds the specified file it reports the found file s path The searching path is specified through the set open_path command in nusmvrc Command Options lt file_name gt File to be searched 3 11 Other Environment Variables The behavior of the system depends on the value of some environment variables For instance an environment variable specifies the partitioning method to be used in building the transition rela tion The value of environment variables can be inspected and modified with the
26. and intended semantics check _Itlspec Performs LTL model checking Command check_ltlspec h m o output file n number p Itl expr IN context P name Performs model checking of LTL formulas LTL model checking is reduced to CTL model checking as described in the paper by CGH97 A 1tl expr to be checked can be specified at command line using option p Alterna tively option n can be used for checking a particular formula in the property database If neither n nor p are used all the LTLSPEC formulas in the database are checked See variable use_coi_size_sorting for changing properties verification order Command Options m Pipes the output generated by the command in process ing LTLSPECs to the program specified by the PAGER shell variable if defined else through the UNIX command more o output file Writes the output generated by the command in processing LTLSPECs to the file output file p ltl expr IN An LTL formula to be checked context is the module context instance name which the variables in 1tl expr must be evaluated in P name Checks the LTL property named name n number Checks the LTL property with index number in the prop erty database check_compute Performs computation of quantitative character Command istics check_comput h m o output file n number p compute expr IN context P name This command deals with the computati
27. annealing This method is an implementation of simu lated annealing for variable ordering This method is po tentially very slow e genetic This method is an implementation of a genetic algorithm for variable ordering This method is potentially very slow e exact This method implements a dynamic programming approach to exact reordering It only stores a BDD at a time Therefore it is relatively efficient in terms of mem ory Compared to other reordering strategies it is very slow and is not recommended for more than 16 boolean variables _ N Pe a e linear This method is a combination of sifting and linear transformations vo e linear_converge The linear method is iterated until no further improvement is obtained f lt method gt Force dynamic ordering to be invoked immediately The val ues for lt method gt are the same as in option e clean_sexp2bdd_cache Cleans the cached results of evaluations Command of symbolic expressions to ADD and BDD representations clean_sexp2bdd_cache h During conversion of symbolic expressions to ADD and BDD representations the re sults of evaluations are normally cached see additionally the environment variable enable_sexp2bdd_caching This allows to save time by avoid the construction of BDD for the same symbolic expression several time In some situations it may be preferable to clean the cache and free collected ADD and BDD This operation can be done for ex
28. can contain next operators and is NOT automatically shifted by one state as done with option c k steps Maximum length of the path according to the constraints The length of a trace could contain less than steps states this is the case in which simulation stops in an intermedi ate step because it may not exist any future state satisfying those constraints The default value is determined by the default_simulation_steps environment variable default_simulation_steps Environment Variable Controls the default number of steps performed by all simulation commands The default is 10 shown _states Environment Variable Controls the maximum number of states tail will be shown during an interactive simulation session Possible values are integers from 1 to 100 The default value is 25 traces_hiding_prefix Environment Variable see section for a detailed description traces_regexp Environment Variable see section for a detailed description 3 6 Execution Commands In this section we describe the commands that allow to perform trace re execution on a given model See also the section Section 3 7 Traces page 89 that describes the commands available for manipulating traces 87 execute_traces Executes complete traces on the model FSM Command xecute_traces h trace_number v m o output file ngin a Executes traces stored in the Trace Manager If no trace is specified last registered trac
29. context P name k max_length o filename N c This command generates one or more problems and calls SAT solver for each one The In cremental BMC encoding used is the one by of Heljanko Junttila and Latvala as described in KHLO5 For each problem this command incrementally generates many satisfiability subproblems and calls the SAT solver on each one of them Each problem is related to a specific problem bound which increases from zero 0 to the given maximum problem length Here max_length is the bound of the problem that system is going to generate and solve In this context the maximum problem bound is represented by the k command parameter or by its default value stored in the environment variable bmc_length The property to be checked may be specified using the n idx the p formula or the P name options See variable use_coi_size_sorting for changing properties verification order 75 Command Options n index index is the numeric index of a valid LTL specification for mula actually located in the properties database p formula IN Checks the formula specified on the command line context context is the module instance name which the variables in formula must be evaluated in P name Checks the LTL property named name in the property database k max_ength max _length is the maximum problem bound to be checked Only natural numbers are valid values for this option If no value is giv
30. database max _length is the maximum problem bound to be checked Only natural numbers are valid values for this option If no value is given the environment variable bmc_length is con sidered instead The loopback value may be e a natural number in 0 max_length 1 A positive sign can be also used as prefix of the number Any in valid combination of length and loopback will be skipped during the generation solving process a negative number in 1 bmc_length In this case loop back is considered a value relative to max_length Any in valid combination of length and loopback will be skipped during the generation solving process e the symbol X which means no loopback e the symbol which means all possible loopbacks from zero to length 1 filename is the name of the dumped dimacs file It may con tain special symbols which will be macro expanded to form the real file name Possible symbols are e F model name with path part e f model name without path part e k current problem bound e I current loopback value e n index of the currently processed formula in the prop erty database e the character check _Itlspec_sbmc_ine Checks the given LTL specification or Command all LTL specifications if no formula is given Checking parameters are the maximum length and the loopback value check_ltlspec_sbmc_inc h n idx p formula IN
31. elements can themselves be arrays The two bound expressions have to be statically evaluable to constant integer numbers and may contain names of defines and module formal parameters State Variables A state of the model is an assignment of values to a set of state and frozen variables State variables and also instances of modules are declared by the notation var_declaration VAR var_list var_list identifier type_specifier var_list identifier type_specifier A variable declaration specifies the identifier of the variables and its type A variable can take the values only from the domain of its type In particular a variable of a enumeration type may take only the values enumerated in the type specifier of the declaration Input Variables IVAR s input variables are used to label transitions of the Finite State Machine The difference between the syntax for the input and state variables declarations is the keyword indicating the beginning of a declaration ivar_declaration IVAR simple_var_list simple_var_list identifier simple_type_specifier simple_var_list identifier simple_type_specifier Another difference between input and state variables is that input variables cannot be instances of modules The usage of input variables is more limited than the usage of state variables which can occur everywhere both in the model and specifications Namely input variables cannot occur in e Left side of as
32. execu tion process_model Performs the batch steps and then returns control Command to the interactive shell 55 process_model h f r i model file m Method Reads the model compiles it into BDD and performs the model checking of all the specifi cation contained in it If the environment variable orward_search has been set before then the set of reachable states is computed If the option r is specified the reordering of variables is performed and a dump of the variable ordering is performed accordingly This command simulates the batch behavior of NUSMV and then returns the control to the interactive shell Command Options f Forces the model construction even when Cone Of Influence is enabled f Forces a variable reordering at the end of the computation and dumps the new variables ordering to the default order ing file This options acts like the command line option reorder i model file Sets the environment variable input_file to file model file and reads the model from file model file m Method Sets the environment variable partition method to Method and uses it as partitioning method build_flat_model Compiles the flattened hierarchy into a Scalar Command FSM build_flat_model h Compiles the flattened hierarchy into SEXP initial states invariants and transition rela tion build_boolean_model Compiles the flattened hierarchy into Command boolean Scalar FSM bui
33. followed by a possible empty sequence of characters from the set A Za z0 9_ An integer is any whole number positive or negative B 1 Types The main types recognised by NUSMV are as follows boolean integer symbolic enum integers and symbolic enum boolean set integer set symbolic set integers and symbolic set unsigned word N where N is any whole number gt 1 signed word N where N is any whole number gt 1 For more detalied description of existing types see Section 2 1 Types page 7 B 2 Implicit Conversion There is only one kind of implicit convertion For more information on type ordering see Sec tion Implicit Type Conversion page I0 Implicit type convertions changes the type of an expression to its counterpart set type The Figure B 2 shows the direction of such convertions For more information on set types and their counterpart types see Section Set Types page 119 unsigned word 1 integer symbolic enum boolean ii l integers and symbolic enum unsigned word 3 unsigned word 2 signed word 1 integer set symbolic set boolean set l integers and symbolic set signed word 3 signed word 2 Figure B 1 The ordering on the types in NUSMV boolean boolean set integer integer set symbolic enum symbolic set integers and symbolic enum integers and symbolic set Figure B 2 Implicit convertion to counterpart set types B 3 Type Rules The type rules are presented b
34. generated trace all variables Picks a state from a set of possible future states in a random way Performs a simulation in which computation is restricted to states satisfying those constraints The desired se quence of states could not exist if such constraints were too strong or it may happen that at some point of the simulation a future state satisfying those constraints doesn t exist in that case a trace with a number of states less than steps trace is obtained Note constraints must be enclosed between double quotes The expression cannot contain next operators and is automatically shifted by one state in order to constraint only the next steps 81 t constraints k steps Performs a simulation in which computation is restricted to states satisfying those constraints The desired se quence of states could not exist if such constraints were too strong or it may happen that at some point of the simulation a future state satisfying those constraints doesn t exist in that case a trace with a number of states less than steps trace is obtained Note constraints must be enclosed between double quotes The expression can contain next operators and is NOT automatically shifted by one state as done with option c Maximum length of the path according to the constraints The length of a trace could contain less than steps states this is the case in which simulation stops in an intermedi ate step because it may not e
35. h n idx p formula IN context P name k length 1 loopback o filename As the gen_1t 1spec_bmc command but it generates and dumps only one problem given its bound and loopback Command Options 72 n index index is the numeric index of a valid LTL specification for mula actually located in the properties database The valid ity of index value is checked out by the system p formula IN Checks the formula specified on the command line context context is the module instance name which the variables in formula must be evaluated in P name Checks the LTL property named name in the property database k length length is the single problem bound used to generate and dump it Only natural numbers are valid values for this option If no value is given the environment variable bmc_length is considered instead 1 loopback The loopback value may be e a natural number in 0 ength 1 A positive sign C can be also used as prefix of the number Any invalid combi nation of length and loopback will be skipped during the generation and dumping process e negative number in 1 ength Any invalid combination of length and loopback will be skipped during the genera tion process e the symbol X which means no loopback e the symbol x which means all possible loopback from zero to length 1 o filename filename is the name of the dumped dimacs file If this op tion
36. has some other options explained below See variable use_coi_size_sorting for changing properties verification order 61 Command Options atl o output file p invar expr context P name s strategy Pipes the output generated by the program in processing INVARSPEC s to the program specified by the PAGER shell variable if defined else through the UNIX command more Writes the output generated by the command in processing INVARSPEC s to the file output file The command line specified invariant formula to be verified context is the module instance name which the variables in invar expr must be evaluated in Checks the INVAR property named name in the property database Chooses the strategy to use while performing reachability analysis Possible strategies are e forward Explore the search space from initial states and try to reach bad states e backward Explore the search space from bad states and try to reach initial states e forward backward Explore the search space using a heuristic to decide at each step whether to move from bad states or from reachable states e bdd bmc Explore the search space using BDD with forward backward strategy and use a heuris tic specified with j option to decide if to switch from BDD technology to BMC The idea is to expand the sets of states reachable from both bad and initial states eventually stop and search for a pat
37. holds in a future time instant i with m lt i lt n e EBG m n p requires that there exists a path starting from a state such that property p holds in all future time instants i with m lt i lt n e ABG m n p requires that for all paths starting from a state property p holds in all future time instants i with m lt i lt n e E p BU m n q requires that there exists a path starting from a state such that property q holds in a future time instant i with m lt i lt n and property p holds in all future time instants j with m lt j lt i e A p BU m n q J requires that for all paths starting from a state property q holds in a future time instant i with m lt i lt n and property p holds in all future time instants j with mm lt j lt it Real time CTL specifications can be defined with the following syntax which extends the syntax for CTL specifications keyword SPEC is deprecated rtctl_specification CTLSPEC rtctl_expr SPEC rtctl_expr CTLSPEC NAME name rtctl_expr SPEC NAME name rtctl_expr With the COMPUTE statement it is also possible to compute quantitative information on the FSM In particular it is possible to compute the exact bound on the delay between two specified events expressed as CTL formulas The syntax is the following compute_specification COMPUTE compute_expr COMPUTE NAME name compute_expr where compute_expr MIN rtctl_expr rtctl_
38. inclusion 19 index subscript inequality NOT 14 OR 14 precedence rental AE shift 16 union 18 word concatenation 17 XNOR 14 XOR 14 options 109 138 OR logical and bitwise P parentheses process processes process keyword PSL Specifications type specifiers 23 U unsigned operator uwconst operator Vv variable declarations 23 variables W Real Time CTL Specifications and Computa word1 operator 22 R tions resize operator 18 S Scalar Variables 45 self set expressions 18 set types 8 Shell configuration Variables 106 Shift Operator signed operator simple expressions 21 Simulation Commands 85 sizeof operator I8 States Variables Table state variables 24 state variables syntax 26 swconst operator 22 syntax rules complex identifiers 32 identifiers 6 main program 34 module declarations 80 symbolic constants 7 type specifiers 23 T toint operator 21 Trace Plugin Commands 91 Trace Plugins Traces 89 TRANS constraint 28 Type conversion operators 21 type order 9 types 7 array boolean enumerations implicit conversion 10 integer ordering 9 set 8 word word type 8 X XML Format Printer 94 XML Format Reader 95 XNOR logical and bitwise 14 XOR logical and bitwise 14 139
39. is considered t threshold When using bdd bmc strategy specify the threshold for the chosen heuristic If this option is not specified the value of the environment variable check_invar_bddbmc_threshold is considered k length When using bdd bmc strategy specify the maximum length of the path to search for during BMC search If this option is not specified the value of the environment variable bmc_length is considered check _invar strategy Environment Variable Determines default search strategy to be used when using command check_invar See the documentation of check_invar for a detailed description of possible values and intended semantics check_invar_forward_backward_heuristic Environment Variable Determines default forward backward heuristic to be used when using command check_invar See the documentation of check_invar for a detailed description of possible values and intended semantics check_invar_bdd_bmc_heuristic Environment Variable Determines default bdd bmc heuristic to be used when using command check_invar See the documentation of check_invar for a detailed description of possible values and intended semantics check_invar_bdd_bmc_threshold Environment Variable 63 Determines default bdd bmc threshold to be used when using command check_invar See the documentation of check_invar for a detailed description of possible values
40. is provided since NuSMV 2 4 0 to prevent the com putation of reachable states that are otherwise computed by default Forces the computation of the set of reachable states for the tableau resulting from BDD based LTL model check ing command check_ltlspec If the option flt is not specified default the resulting tableau will inherit the computation of the reachable states from the model if en abled If the option f1t is specified the reachable states set will be calculated for the model and for the tableau resulting from LTL model checking This might improve performances of the command check_1t1spec but may also lead to a dramatic slowing down This options has ef fect only when the calculation of reachable states is enabled see f 111 AG CoL We remark that when cone of influence reduc tion is enabled a counter example trace for a prop erty that does not hold may not be a valid counter example trace for the orig inal model We refer the reader to the Fre quently Asked Questions FAQ FAQ i iv file o ov file t tv file reorder dynamic m method disable_sexp2bdd_cacfietmg the bdd_soh heuristics Verifies only AG formulas using an ad hoc algorithm see documentation for the ag_only_search environment variable Sets to 1 the cone_of_influence environment variable Enables cone of influence reduction Reads the variable ordering from file iv_file Writes the
41. may con tain special symbols which will be macro expanded to form the real file name Possible symbols are e F model name with path part e f model name without path part e k current problem bound e I current loopback value e n index of the currently processed formula in the prop erty database e the character check _Itlspec_bmc_onepb Checks the given LTL specification or Command all LTL specifications if no formula is given Checking parameters are the single problem bound and the loopback value check_ltlspec_bmc_onepb h n idx p formula IN context P name k length 1 loopback o filename As command check_1tlspec_bmc but it produces only one single problem with fixed bound and loopback values with no iteration of the problem bound from zero to max_length Command Options n index index is the numeric index of a valid LTL specification for mula actually located in the properties database The valid ity of index value is checked out by the system 70 p formula IN Checks the formula specified on the command line context context is the module instance name which the variables in formula must be evaluated in P name Checks the LTL property named name in the property database k length length is the problem bound used when generating the sin gle problem Only natural numbers are valid values for this option If no value is given the environment var
42. name of the array The reason for this is that the actual definition of an array in the model file is essentially a shorthand method of defining a list of variables that all have the same type Nothing is gained by declaring it as an array over declaring each of the elements individually and there is no difference in terms of the internal representation of the variables 2 6 Clusters Ordering When NUSMV builds a clusterized BDD based FSM during model construction an initial sim ple clusters list is roughly constructed by iterating through a list of variables and by constructing 46 the clusters by picking the transition relation associated to each variable in the list Later the clusters list will be refined and improved by applying the clustering alghorithm that the user previoulsy selected see partitioning methods at page 3 1 for further information In WJKWLvdBRO06 Wendy Johnston and others from University of Queensland showed that choosing a good ordering for the initial list of variables that is used to build the clusters list may lead to a dramatic improvement of performances They did experiments in a modified version of NUSMV by allowing the user to specify a variable ordering to be used when con structing the initial clusters list The prototype code has been included in version 2 4 1 that offers the new option trans_order_file to specify a file containing a variable ordering see at page 53 for further information Grammar
43. of symmetric sifting It is similar to sifting with one addition Variables that be come adjacent during sifting are tested for symmetry If they are symmetric they are linked in a group Sifting then continues with a group being moved instead of a sin gle variable The symmetry_sift method is iterated until no further improvement is obtained Permutes the variables within windows of n adjacent vari ables where n can be either 2 3 or 4 so as to minimize the overall BDD size The window 2 3 4 method is iterated until no further improvement is obtained This method is similar to symmetry_sift but uses more general criteria to create groups The group_sift method is iterated until no further im provement is obtained This method is an implementation of simulated annealing for variable ordering This method is potentially very slow This method is an implementation of a genetic algorithm for variable ordering This method is potentially very slow This method implements a dynamic programming ap proach to exact reordering It only stores one BDD at a time Therefore it is relatively efficient in terms of mem ory Compared to other reordering strategies it is very slow and is not recommended for more than 16 boolean variables 96 linear linear_conv This method is a combination of sifting and linear transformations The linear method is iterated until no further improve ment is obtained dynamic
44. of the clusters ordering file is the same of variable ordering file presented in section 2 5 at page 45 47 Chapter 3 Running NuSMV interactively The main interaction mode of NUSMV is through an interactive shell In this mode NUSMV enters a read eval print loop The user can activate the various NUSMV computation steps as system commands with different options These steps can therefore be invoked separately possibly undone or repeated under different modalities These steps include the construction of the model under different partitioning techniques model checking of specifications and the configuration of the BDD package The interactive shell of NUSMV is activated from the system prompt as follows NuSMV gt is the default NUSMV shell prompt system_prompt gt NuSMV int lt RET gt NuSMVv gt When running interactively NUSMV first tries to read and execute commands from an initialization file if such file can be found and is readable unless s is passed on the command line First file masternusmvrce is looked for in directory defined in environment variable NUSMV_LIBRARY PATH or in default library path if no such variable is defined If no such file exists file nusmvrc is looked for in user s home directory and as a last attemp nusmvre is looked for in current directory Commands in the initialization file if any are executed consec utively When initialization phase is completed the NUSMV shell is displayed and
45. pslspec h m o output file n number p psl expr IN context P name b i g 1 k bmc lenght 1 loopback Depending on the characteristics of the PSL property and on the options the commands applies CTL based model checking or LTL based possibily bounded model checking A psl expr to be checked can be specified at command line using option p Alterna tively option n can be used for checking a particular formula in the property database If neither n nor p are used all the PSLSPEC formulas in the database are checked If option b is used LTL bounded model checking is applied otherwise bdd based model checking is applied For LTL bounded model checking options k and 1 can be used to define the maximum problem bound and the value of the loopback for the single generated problems respectively their values can be stored in the environment variables bmc_lenght and bmc_loopback Single problems can be generated by using option 1 By using op tion i the incremental version of bounded model checking is activated Bounded model checking problems can be generated and dumped in a file by using option g 83 See variable use_coi_size_sorting for changing properties verification order Command Options m o output file p psl expr context n number P name b k bmc_length 1 loopback IN Pipes the output generated by the command in process ing PSLSPECs to the pro
46. reordering methods available with the CUDD pack age are listed below The default value is sift sift Moves each variable throughout the order to find an opti mal position for that variable assuming all other variables are fixed This generally achieves greater size reductions than the window method but is slower random Pairs of variables are randomly chosen and swapped in the order The swap is performed by a series of swaps of adjacent variables The best order among those obtained by the series of swaps is retained The number of pairs chosen for swapping equals the number of variables in the diagram To be exact M C Mo where M is the model from which the trace was generated and Mo is the currently loaded and built model Note however that this may mean that the trace is not valid for the model Mo 95 random_pivot sift_converge symmetry_sift symmetry_sift_converge window2 window3 window4 window2_converge window3_converge window4_converge group_sift group_sift_converge annealing genetic exact Same as random but the two variables are chosen so that the first is above the variable with the largest num ber of nodes and the second is below that variable In case there are several variables tied for the maximum number of nodes the one closest to the root is used The sift method is iterated until no further improvement is obtained This method is an implementation
47. s p is true ins EF pis true in a state so if there exists a series of transitions So S1 S1 S2 Sn 1 Sn such that p is true in sn AF pis true in a state so if for all series of transitions So 1 S1 S2 8n 1 Sn p is true in Sn EG pis true ina state so if there exists an infinite series of transitions So gt s1 1 gt Se such that p is true in every si AG pis true ina state so if for all infinite series of transitions So 1 1 S2 p is true in every s E p U q is true ina state so if there exists a series of transitions So 51 S1 S2 Sn 1 Sn Such that p is true in every state from so to s _ and q is true in state sn A p U q is true in a state so if for all series of transitions So s1 1 2 Sn 1 Sn p is true in every state from so to 1 and q is true in state Sn A CTL formula is true if it is true in all initial states For a detailed description about the semantics of PSL operators please see psl03 2 4 2 Invariant Specifications It is also possible to specify invariant specifications with special constructs Invariants are propo sitional formulas which must hold invariantly in the model The corresponding command is INVARSPEC with syntax invar_specification INVARSPEC next_expr INVARSPEC NAME name next_expr This statement is intuitively equivalent to 37 SPEC AG simple_expr but can be c
48. successive input combinatorial section Such a way if a variable in a model was input and became state or vice versa the existing traces still can be read and executed 92 Loads a trace which has been previously output to a file with the XML Format Output plugin The model from which the trace was originally generated must be loaded and built using the command go first Please note that this command is only available on systems that have the Expat XML parser library installed 3 8 Trace Plugins NUSMV comes with three plugins which can be used to display a trace that has been generated Basic Trace Explainer States Variables Table XML Format Printer There is also an xml loader which can read in any trace which has been output to a file by the XML Format Printer Note however that this loader is only available on systems that have the Expat XML parser library installed Once a trace has been generated it is output to stdout using the currently selected plu gin The command show_t races can be used to output any previuosly generated or loaded trace to a specific file 3 8 1 Basic Trace Explainer This plugin prints out each state the current values of the variables in the trace one after the other The initial state contains all the state and frozen variables and their initial values States are numbered in the following fashion trace_number state_number There is the option of printing out the value of every variabl
49. to guarantee that deadlock states are actually reachable check_fsm Environment Variable 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 print_fsm_stats Prints out information about the fsm and cluster Command ing print_fsm_stats h m p o output file This command prints out information regarding the fsm and 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 Also the command can print all the normalized predicates the FMS consists of A normalized predicate is a boolean expression which does not have other boolean sub expressions For example expression b lt O0 a b 0 cis normalized into o lt 0 a b c O c which has 3 normalized predicates inside b lt 0 a b c O c Command Options h Prints the command usage m Pipes the output generated by the command to the pro gram specified by the PAGER shell variable if defined else through the UNIX command more p Prints out the normalized predicates the FSM consists of Expressions in properties are ignored o output file Writes the output generated by the command to the file output file print_fair_states Prints ou
50. word N unsigned word N boolean signed word N signed word N boolean Arithmetic Operators x The arithmetic operators addition unary negation or binary subtraction multiplica tion and division have the following signature x integer integer integer unsigned word N unsigned word N unsigned word N signed word N signed word N signed word N unary integer integer unsigned word N unsigned word N signed word N signed word N Before checking the expression for being correctly typed the implicit type conversion can be applied to one of the operands If the operators are applied to unsigned word N or signed word N type then the operations are performed modulo 2 The result of the operator is the quotient from the division of the first operand by the second The result of the operator is the algebraic quotient with any fractional part discarded this is often called truncation towards zero If the quotient a b is representable the expres sion a b b a mod b shall equal a If the value of the second operand is zero the behavior is undefined and an error is thrown by NUSMV The semantics is equivalent to the corresponding one of C C languages In the versions of NUSMV prior to 2 4 0 the semantics of division was different See page 16 for more detail 15 Remainder Operator mod The result of the mod operator i
51. 4 Running NuSMV batch Bibliography A Compatibility with CMU SMV B Typing Rules 2 Implicit Conversion B 3 Type Rules o o sa corect amea meaa C Production Rules w ndex ndex ndex apres wee Sis 46 109 114 116 119 Sack a amp 119 ob Bak bd 119 sori ce bie iia 120 124 135 136 137 Chapter 1 Introduction NuSMV is a symbolic model checker originated from the reengineering reimplemen tation and extension of CMU SMV the original BDD based model checker developed at CMU McM93 The NUSMV project aims at the development of a state of the art symbolic model checker designed to be applicable in technology transfer projects it is a well structured open flexible and documented platform for model checking and is robust and close to industrial systems standards CCGROOJ Version 1 of NUSMV basically implements BDD based symbolic model check ing Version 2 of NUSMV NUSM V2 in the following inherits all the functionalities of the previous version and extends them in several directions CCG 02 The main novelty in NUSM V2 is the integration of model checking techniques based on proposi tional satisfiability SAT BCCZ99 SAT based model checking is currently enjoying a substantial success in several industrial fields and opens up new research directions BDD based and SAT based model checking are often able to solve different classes of problems and can therefore be seen as complementary tech
52. C Lei Efficient model checking in fragments of the propo sitional mu calculus extended abstract In LICS pages 267 278 IEEE Computer Society 1986 E Allen Emerson A K Mok A Prasad Sistla and Jai Srinivasan Quan titative temporal reasoning In Edmund M Clarke and Robert P Krushan editors Proceedings of Computer Aided Verification CAV 90 volume 531 of LNCS pages 136 145 Berlin Germany June 1991 Niklas E n and Niklas S rensson Temporal induction by incremental sat solving In Ofer Strichman and Armin Biere editors Electronic Notes in Theoretical Computer Science volume 89 Elsevier 2004 114 FAQ HKQ03 KHLOS5 LBHJ05 Mar85 McM92 McM93 MHS00 PSL psl03 RAPT 95 sfVS96 She04 Som98 WJKWLvdBRO6 Frequently Asked Questions FAQ Available at jeu faq htmljor within the NUSMV distribution package T A Henzinger O Kupferman and S Qadeer From Pre historic to Post modern symbolic model checking Formal Methods in System Design 23 3 303 327 2003 T Junttila K Heljanko and T Latvala Incremental and complete bounded model checking for full PLTL In K Etessami and S K Rajamani ed itors Computer Aided Verification 17 International Conference CAV 2005 number 3576 in Lecture Notes in Computer Science pages 98 111 Springer 2005 T Latvala A Biere K Heljanko and T Junttila Simple is better Efficient bounded model chec
53. E SERE RegExp QUALIFIERS NDNNNnNnNN SERE count x count SERE i psl_bexpr count psl_bexpr gt count count number range Istances of OBE_property are CTL properties in the PSL style and are defined as follows OBE_property AX OBE_property AG OBE_property AF OBE A OBE_property U OBE_property EX OBE_property EG OBE_property EF OBE_property E OBE_property U OBE_property The NUSMV parser allows to input any specification based on the grammar above but currently verification of PSL specifications is supported only for the OBE subset and for a subset of PSL for which it is possible to define a translation into LTL For the specifications that belong to these subsets it is possible to apply all the verification techniques that can be applied to LTL and CTL Specifications 44 2 5 Variable Order Input It is possible to specify the order in which variables should appear in the BDD s generated by NUSMV The file which gives the desired order can be read in using the i option in batch mode or by setting the input_order_file environment variable in interactive mode 2 5 1 Input File Syntax The syntax for input files describing the desired variable ordering is as follows where the file can be considered as a list of variable names each of which must be on a separate line vars
54. EMPORAL OPERATORS always FL_property never FL property next FL property next FL_property eventually FL_property L_ property until FL_property L property until FL_property L property until FL_property L_ property until_ FL_property L_ property before FL_property L_ property before FL_property L_property before _ FL_property L_ property before_ FL_property EXTENDED NEXT OPERATORS X number FL_property X number FL_property next number FL_property next number FL_property F EF E F F F FI El next_a range FL_property next_a range FL_property next_e range FL_property next_e range FL_property next_event psl_bexpr FL_property next_event psl_bexpr FL_property next_event psl_bexpr number FL_property next_event psl_bexpr numker FL_property 132 next_event_a psl_bexpr psl_expr FL_property next_event_a psl_bexpr psl_expr FL_property next_event_e psl_bexpr psl_expr FL_property next_event_e psl_bexpr psl_expr FL_property 7 OPERATORS ON SERES sequence FL_property sequence gt sequence sequence gt sequence always sequence G sequence never sequence eventually sequence within sequence_or_psl_bexpr psl_bexpr sequence within sequence_or_psl_bexpr psl_bexpr sequenc
55. NuSMV 2 5 User Manual Roberto Cavada Alessandro Cimatti Charles Arthur Jochim Gavin Keighren Emanuele Olivetti Marco Pistore Marco Roveri and Andrei Tchaltsev FBK irst Via Sommarive 18 38055 Povo Trento Italy Email This document is part of the distribution package of the NUSMV model checker available athttp nusmv fbk eu Parts of this documents have been taken from The SMV System Draft by K McMillan available at sdfdsf http www cs cmu edu modelcheck smv smvmanual r2 2 ps Copyright 1998 2005 by CMU and ITC irst Copyright 2010 by FBK irst Contents 1 Introduction 2 Input Language 2 1 Types Overview 2 1 1 Boolean 2 1 7 Type Order 2 2 Expressions NI 2 2 1 Implicit Type Conversion 2 2 2 Constant Expressions 2 00 2 2 3 Basic Expressions 2 2 4 Simple and Next Expressions 2 5 Type conversion operators 2 3 Definition of the FSM 2 3 1 Variable Declarations 5 20004 2 3 2 DEFINE Declarations 2 000500 4 2 3 3 Array Define Declarations 0 2 3 4 CONSTANTS Declarations 004 4 2 3 INIT Constraint s sss 2 ee ee 2 3 6 INVAR Constraint 2 a 2 3 7 TRANS Constraint 2 ee ee Se Mat et ek pa ada EE 2 3 9 FAIRNESS Constraints 0 002000 4 2 3 10 MODULE Declarations 2 0020 004 2 3 11 MODULE Instantiations
56. SMV have been isolated and separated in mod ules Interfaces between modules have been provided This reduces the effort needed to modify and extend NUSMV Quality of the implementation NUS MV is written in ANSI C is POSIX com pliant and has been debugged with Purify in order to detect memory leaks Fur thermore the system code is thoroughly commented NUSMV uses the state of the art BDD package developed at Colorado University and provides a gen eral interface for linking with state of the art SAT solvers This makes NUSMV very robust portable efficient and easy to understand by people other than the developers This document is structured as follows e In Chapter 2 Input Language page 6 we define the syntax of the input language of NUSMV e In Chapter 3 Running NuSMV interactively page the commands of the interaction shell are described e In Chapter 4 Running NuSMV batch page we define the batch mode of NuUSMV NUSMV is available athttp nusmv fbk eu Chapter 2 Input Language In this chapter we present the syntax and semantics of the input language of NUSMV Before going into the details of the language let us give a few general notes about the syntax In the syntax notations used below syntactic categories non terminals are indicated by monospace font and tokens and character set members terminals by bold font Grammar productions enclosed in square brackets are optional while a vertica
57. The property to be checked may be specified using the n idx or the p formula options If you need to generate a DIMACS dump file of all generated problems you must use the option o filename 69 Command Options n index index is the numeric index of a valid LTL specification for mula actually located in the properties database p formula IN Checks the formula specified on the command line context context is the module instance name which the variables in formula must be evaluated in P name Checks the LTL property named name in the property database k max_length max_length is the maximum problem bound to be checked Only natural numbers are valid values for this option If no value is given the environment variable bmc_length is con sidered instead 1 loopback The loopback value may be e a natural number in 0 max_length 1 A positive sign can be also used as prefix of the number Any in valid combination of length and loopback will be skipped during the generation solving process e a negative number in 1 bmc_length In this case loop back is considered a value relative to max_length Any in valid combination of length and loopback will be skipped during the generation solving process e the symbol X which means no loopback e the symbol which means all possible loopbacks from zero to length 1 o filename filename is the name of the dumped dimacs file It
58. W3 image_W4 It is possible default to use affinity clustering to improve model checking performance See affinity variable It is also possible to avoid default preordering of clusters see RAP 95 by setting the iwls95preorder variable appropriately conj_part_threshold Environment Variable The limit of the size of clusters in conjunctive partitioning The default value is 0 BDD nodes affinity Environment Variable Enables affinity clustering heuristic described in MHSO0 possible values are 0 or 1 The default value is 1 trans_order_file Environment Variable Reads the a variables list from file tv_file to be used when clustering the transition rela tion This feature has been provided by Wendy Johnston University of Queensland The results of Johnston s research have been presented at FM 2006 in Hamilton Canada See WJKWLvdBRO6 image_cluster_size Environment Variable One of the parameters to configure the behaviour of the w s95CP partitioning algorithm image_cluster_size is used as threshold value for the clusters The default value is 1000 BDD nodes 54 image_W 1 2 3 4 Environment Variable The other parameters for the Jw s95CP partitioning algorithm These attribute different weights to the different factors in the algorithm The default values are 6 1 1 6 respec tively For a detailed description please refer to JRAP 95 iwls95preorder Environment Variable Enables clus
59. _dimacs_filename will be considered Command Options n index index is the numeric index of a valid LTL specification for mula actually located in the properties database p formula IN Dumps the formula specified on the command line context context is the module instance name which the variables in formula must be evaluated in P name Checks the LTL property named name k max_length max_length is the maximum problem bound to be generated Only natural numbers are valid values for this option If no value is given the environment variable bmc_length is con sidered instead 76 1 loopback The loopback value may be e a natural number in 0 max_length 1 A positive sign can be also used as prefix of the number Any in valid combination of length and loopback will be skipped during the generation solving process e a negative number in 1 bmc_length In this case loop back is considered a value relative to max_length Any in valid combination of length and loopback will be skipped during the generation solving process e the symbol X which means no loopback e the symbol which means all possible loopbacks from zero to length 1 o filename filename is the name of the dumped dimacs file It may con tain special symbols which will be macro expanded to form the real file name Possible symbols are e F model name with path part e f model name without path pa
60. _list EMPTY var_list_item vars_list var_list_item complex_identifier complex_identifier integer_number Where EMPTY means parsing nothing This grammar allows for parsing a list of variable names of the following forms Complete_Var_Name to specify an ordinary variable Complete_Var_Name index to specify an array variable element Complete_Var_Name NUMBER to specify a specific bit of a scalar variable where Complete_Var_Name is just the name of the variable if it appears in the module MAIN otherwise it has the module name s prepended to the start for example modl mod2 modN varname where varname is a variable in modN and modN varname is a variable in modN 1 and so on Note that the module name main is implicitely prepended to every variable name and therefore must not be included in their declarations Any variable which appears in the model file but not the ordering file is placed after all the others in the ordering Variables which appear in the ordering file but not the model file are ignored In both cases NUSMV displays a warning message stating these actions Comments can be included by using the same syntax as regular NUSMV files That is by starting the line with 2 5 2 Scalar Variables A variable which has a finite range of values that it can take is encoded as a set of boolean variables i e bits These boolean variables represent the binary equivalents of all the possible v
61. _var_ordering Deals with the dynamic variable order Command ing dynamic_var_ordering d I lt method gt f lt method gt h Controls the application and the modalities of dynamic variable ordering Dynamic ordering is a technique to reorder the BDD variables to reduce the size of the existing BDDs When no options are specified the current status of dynamic ordering is displayed At most one of the options e f and d should be specified Dynamic ordering may be time consuming but can often reduce the size of the BDDs dramatically A good point to invoke dynamic ordering explicitly using the f option is after the commands build_model once the transition relation has been built It is possible to save the ordering found using write_order in order to reuse it using buildmodel i order file in the future Command Options d e lt method gt Disable dynamic ordering from triggering automatically Enable dynamic ordering to trigger automatically whenever a certain threshold on the overall BDD size is reached lt method gt must be one of the following e sift Moves each variable throughout the order to find an optimal position for that variable assuming all other vari ables are fixed This generally achieves greater size re ductions than the window method but is slower random Pairs of variables are randomly chosen and swapped in the order The swap is performed by a series of swaps of ad
62. a p formula IN Checks the formula specified on the command line context context is the module instance name which the variables in formula must be evaluated in add_property Adds a property to the list of properties Command add_property h c aus 2 q s p formula IN context Adds a property in the list of properties It is possible to insert LTL CTL INVAR PSL and quantitative COMPUTE properties Every newly inserted property is initialized to unchecked A type option must be given to properly execute the command 65 Command Options c Adds a CTL property 1 Adds an LTL property i Adds an INVAR property s Adds a PSL property q Adds a quantitative COMPUTE property p formula IN Adds the formula specified on the command line context context is the module instance name which the variables in formula must be evaluated in show property Shows the currently stored properties Command show_property h n idx P name c 1 isl Se q f v u m o F format Shows the properties currently stored in the list of properties This list is initialized with the properties CTL LTL INVAR COMPUTE present in the input file if any then all of the properties added by the user with the relative check_property or add_property commands are appended to this list For every property the following informations are displayed e the identifie
63. a UNIX like history mechanism inside the NUSMV shell Command Options lt num gt Lists the last lt num gt events Lists the last 30 events if lt num gt is not specified History Substitution The history substitution mechanism is a simpler version of the csh history substitution mechanism It enables you to reuse words from previously typed commands The default history substitution character is the is default for shell escapes and marks the beginning of a comment This can be changed using the set command In this description is used as the history_char The can appear anywhere in a line A line containing a history substitution is echoed to the screen after the substitution takes place can be preceded by a in order to escape the substitution for example to enter a into an alias or to set the prompt Each valid line typed at the prompt is saved If the history variable is set see help page for set each line is also echoed to the history file You can use the history command to list the previously typed commands Substitutions At any point in a line these history substitutions are available Command Options 0 Initial word of last command Sin n th argument of last command amp S Last argument of last command Sx All but initial word of last command BS Last command Sstuf Last command beginning with stuf n Repeat the n th command 101 S n Rep
64. abel the current state This command is used to navigate along traces produced by NUSMV During the navigation there is a current state and the current trace is the trace the current state belongs to 89 state_label is in the form trace state where trace is the index of the trace which the state has to be taken from state is the index of the state within the given trace If st ate is a negative number then the state index is intended to be relative to the length of the given trace For example 2 1 means the last state of the trace 2 2 2 is the state before the last state etc print_current_state Prints out the current state Command print current _state h v Prints the name of the current state if defined Command Options v Prints the value of all the state and frozen variables of the current state 3 7 2 Displaying Traces NUSMV comes with three trace plugins see Section 3 8 Trace Plugins page 93 which can be used to display traces in the system Once a trace has been generated by NUSMYV it is printed to stdout using the trace explanation plugin which has been set as the current default The command show_t races see Section 5 Simulation Commands page 85 can then be used to print out one or more traces using a different trace plugin as well as allowing for output to a file Generation and displaying of traces can be enabled disabled by setting variable counter_examples Some filtering of symbols that are
65. actic sugar for toint bool_exprl toint bool_expr2 toint bool_exprN This operator has been introduced in version 2 5 1 to simplify the porting of those models which exploited the implicit casting of integer to boolean to encoding e g predicates like bO bl BN lt 3 at most two bits are enabled Since version 2 5 1 this expression can be written as count b0 b1 bN lt 3 2 2 4 Simple and Next Expressions Simple_expressions are expressions built only from the values of variables in the current state Therefore the simple_expression cannot have a next operation inside and the syntax of simple_expressions is as follows simple_expr basic_expr with the alternative basic_next_expr not allowed Simple_expressions can be used to specify sets of states for example the initial set of states The next_expression relates current and next state variables to express transitions in the FSM The next_expression can have next operation inside i e next_expr basic_expr with the alternative basic_next_expr allowed 2 2 5 Type conversion operators Integer conversion operator toint converts an unsigned word e constant or a signed word e constant or a boolean expression to an integer representing its value Also integer expressions are allowed but no action is performed The signature of this conversion operator is toint integer integer toint boolean integer toint u
66. ailable 90 show_defines_in_traces Environment Variable Controls whether defines should be printed as part of a trace or be skipped Skipping printing of the defines can help in reducing time and memory usage required to build very big traces traces_show_defines_with_next Environment Variable Controls whether defines containing next operators should be printed as part of a trace or be skipped 3 7 3 Trace Plugin Commands The following commands relate to the plugins which are available in NUSMV show_plugins Shows the available trace explanation plugins Command show plugins h n plugin no a Command Options n plugin no Shows the plugin with the index number equal to plugin no Shows all the available plugins Shows the available plugins that can be used to display a trace which has been generated by NUSMYV or that has been loaded with the read_t race command The plugin that is used to read in a trace is also shown The current default plugin is marked with D All the available plugins are displayed by default if no command options are given default_trace_plugin Environment Variable This determines which trace plugin will be used by default when traces that are generated by NUSMV are to be shown The values that this variable can take depend on which trace plugins are installed Use the command show_plugins to see which ones are available The default value is 0 show trac
67. al and can contain variables not declared in the model Variables listed in the ordering file but not declared in the model are simply discarded The variables declared in the model but not listed in the variable file provided in input are created at the end of the given ordering following the default ordering All the ordering files generated by CMU SMV are accepted in input from NUSMV but the ordering files generated by NUSMV may be not accepted by CMU SMV Notice that there is no guarantee that a good ordering for CMU SMV is also a good ordering for NUSMV In the ordering files for NUSMYV identifier process_selector_can be used to control the position of the variable that encodes process selection In CMU SMV it is not possible to control the position of this variable in the ordering it is hard coded at the top of the ordering A further difference about variable ordering consists in the fact that in NUSMV it is allowed to specify single bits of scalar variables In the example 117 VARS 03 73 NUSMV will create three variables x 0 x 1 and x 2 that can be explicitly mentioned in the variable ordering file to fine control their ordering 118 Appendix B Typing Rules This appendix gives the explicit formal typing rules for NUSMV s input language as well as notes on implicit conversion and casting In the following an atomic constant is defined as being any sequence of characters starting with a character in the set A Za z_ and
68. alues for the scalar variable Thus a scalar variable that can take values from 0 to 7 would require three boolean variables to represent it It is possible not only to declare the position of a scalar variable in the ordering file but each of the boolean variables which represent it If only the scalar variable itself is named then all the boolean variables which are actually used to encode it are grouped together in the BDD package Variables which are grouped together will always remain next to each other in the BDD package and in the same order When dynamic variable re ordering is carried out the group of variables are treated as one entity and moved as such 0Note that if the ordering is not provided by a user then NUSMV decides by itself how to order the vari ables Two shell variables bdd_static_order_heuristics see page 53 and vars_order_type see page 53 allow to control the ordering creation 45 If a scalar variable is omitted from the ordering file then it will be added at the end of the variable order and the specific bit variables that represent it will be grouped together However if any specific bit variables have been declared in the ordering file see below then these will not be grouped with the remaining ones It is also possible to specify the location of specific bit variables anywhere in the ordering This is achieved by first specifying the scalar variable name in the desired location then simply spec ifying C
69. ame Checks the INVARSPEC property named name k maxJength max_length is the maximum problem bound that can be reached Only natural numbers are valid values for this option If no value is given the environment variable bmc_length is considered instead a alg alg specifies the algorithm to use The value can be dual or zigzag If no value is given the environment variable bmc_inc_invar_alg is considered instead bmc _invar_alg Environment Variable Sets the default algorithm used by the command check_invar_bmc Possible values are classic and een sorensson The default value is classic bmc_inc_invar_alg Environment Variable Sets the default algorithm used by the command check_invar_bmc_inc Possible val ues are dual and zigzag The default value is dual bmc_invar_dimacs_filename Environment Variable This is the default file name used when generating DIMACS invar dumps This variable may be taken into account by the command gen_invar_bmc DIMACS file name can contain special symbols which will be expanded to represent the actual file name Possible symbols are e F The currently loaded model name with full path e f The currently loaded model name without path part e n The numerical index of the currently processed formula in the properties database 80 e The character The default value is f_invar_n n sat_solver 3 Environment Variable The SAT solver s name actually to be u
70. ample to free some memory Another possible reason is that dynamic reordering may modify all existing BDDs and cleaning the cache thereby freeing the BDD may speed up the reordering This command is designed specifically to free the internal cache of evaluated expressions and their ADDs and BDDs Note that only the cache of symbolic expression to bdd eval uator is freed BDDs of variables constants and expressions collected in BDD FSM or anywhere else are not freed print_formula Prints a formula in canonical format Command print_formula h v f expression Prints the number of satsfying assignments for the given formula In verbose mode prints also the list of such assigments In formula mode a canonical representation of the formula is printed 98 Command Options v Prints explicit models of the formula f Prints the simplified and canonical formula enable_sexp2bdd_caching Environment Variable This variable determines if during evaluation of symbolic expression to ADD and BDD representations the obtained results are cached or not Note that if the variable is set down consequently computed results are not cached but the previously cached data remain un modified and will be used during later evaluations The default value of this variable is 1 which can be changed by a command line option disable_sexp2bdd_caching For more information about the reasons of why BDD cache should be disabled in some situatio
71. and does the same thing as check_invar_bmc see the description on page but uses an incremental algorithm and therefore usually runs considerably quicker The incremental algorithms exploit the fact that satisfiability problems generated for a particular invariant have common subparts so information obtained during solving of one problem can be used in solving another one A SAT solver with an incremental interface is required by this command If no such SAT solver is provided then this command will be unavailable There are two incremental algorithms which can be used Dual and ZigZag Both algorithms are equally powerful but may show different performance depending on a SAT solver used and an invariant being proved At the moment the Dual algorithm cannot be used if there are input variables in a given model For additional information about algorithms consider ES04 Also notice that during checking of invariants all the fairness conditions associated with the model are ignored See variable use_coi_size_sorting for changing properties verification order Command Options n index index is the numeric index of a valid INVAR specification formula actually located in the property database The va lidity of index value is checked out by the system p formula IN Checks the formula specified on the command line context context is the module instance name which the variables in formula must be evaluated in P n
72. and next value set in an ASSIGN statement i e statements such as ASSIGN next a expr and ASSIGN a expr are illegal Apart from that frozen variables may occur in the definition of the FSM in any place in which a state variable may occur Some examples are as follows e Left side current and next state assignments are illegal while init state assignments are allowed FROZENVAR a boolean FROZENVAR b boolean FROZENVAR c boolean VAR d boolean FROZENVAR e boolean ASSIGN init a d legal next b d illegal c d illegal e a also illegal e INIT TRANS INVAR FAIRNESS JUSTICE and COMPASSION statements are all legal So is the scope of a next expression For example the following has an empty state space FROZENVAR a boolean INIT a INVAR a alternatively this has two initial states deadlocking FROZENVAR b boolean TRANS next b lt gt b and that s just unfair FROZENVAR c boolean FAIRNESS c FAIRNESS c 25 e All kinds of specifications involving frozen variables are allowed e g FROZENVAR c boolean True by definition SPEC AG c gt AG c amp c gt AG c Here neither is true INVARSPEC c INVARSPE c False as above LTLSPEC G F c amp GF c Examples Below are examples of state frozen and input variable declarations VAR a boolean FROZENVAR b 0
73. ariable bmc_length value is consid ered instead 1 loopback The loopback value may be e a natural number in 0 max_length 1 A positive sign C can be also used as prefix of the number Any in valid combination of bound and loopback will be skipped during the generation and dumping process e a negative number in 1 bmc_length In this case loop back is considered a value relative to max_length Any in valid combination of bound and loopback will be skipped during the generation process e the symbol X which means no loopback e the symbol which means all possible loopback from zero to length 1 o filename filename is the name of dumped dimacs files If this options is not specified variable bmc_dimacs_filename will be con sidered The file name string may contain special symbols which will be macro expanded to form the real file name Possible symbols are e F model name with path part e f model name without path part e k current problem bound e 1 current loopback value e n index of the currently processed formula in the prop erty database e the character gen_Itlspec_bmc_onepb Dumps into one dimacs file the problem Command generated for the given LTL specification or for all LTL specifi cations if no formula is explicitly given Generation and dumping parameters are the problem bound and the loopback value gen_ltlspec_bmc_onepb
74. ariables FROZENVAR It is used to introduce frozen variables JUSTICE It is used to introduce justice fairness constraints COMPASSION It is used to introduce compassion fairness constraints CONSTANTS It is used to force declaration of constants word It is used to declare word type variables wordl It is used to cast boolean expressions to word type bool It is used to cast word expressions to boolean type unsigned It is used to cast signed words to unsigned ones signed It is used to cast unsigned words to signed ones extend It is used to increase the width of words The IMPLEMENTS INPUT OUTPUT statements are not no longer supported by NUSMV NuSMV differs from CMU SMV also in the controls that are performed on the input for mulas Several formulas that are valid for CMU SMV but that have no clear semantics are not accepted by NUSMV In particular e Itis no longer possible to write formulas containing nested next TRANS next alpha amp next beta next gamma gt delta 116 e It is no longer possible to write formulas containing next in the right hand side of normal and init assignments they are allowed in the right hand side of next assign ments and with the statements INVAR and INIT INVAR next alpha amp beta INIT next beta gt alpha ASSIG delta alpha amp next gamma normal assignments init gamma alpha a
75. asic_expr basic_expr word concatenation wordl basic_expr boolean to unsigned word 1 conversion bool basic_expr unsigned word 1 and int to boolean conversion 12 count basic_expr_list count of true boolean expressions swconst basic_expr basic_expr integer to signed word constant conversion uwconst basic_expr basic_expr signed basic_expr unsigned word to signed word conversion unsigned basic_expr signed word to unsigned word conversion sizeof basic_expr word size as an integer extend basic_expr basic_expr word width extension resize basic_expr basic_expr word width resize basic_expr union basic_expr union of set expressions set_body_expr set expression basic_expr in basic_expr inclusion in a set expression basic_expr basic_expr basic_expr if then els xpression case_expr case expression basic_next_expr next expression basic_expr_list basic_expr basic_expr_list basic_expr The order of parsing precedence for operators from high to low is 1 unary minus mod lt lt gt gt union in ta lt gt lt gt amp xor xnor e Pe e lt gt gt Operators of equal precedence associate to the left except gt that associates to the right The constants and their types are explained in Section Constant Expressions page I0 Variables and Defines
76. at there are certain reserved keyword which cannot be used as identifiers see page 6 Variable and DEFINE Identifiers define_identifier complex_identifier variable_identifier complex_identifier Complex Identifiers complex_identifier identifier complex_identifier identifier complex_identifier simple_expression self Integer Numbers integer_number 124 digit digit integer_number digit Constants constant boolean_constant integer_constant symbolic_constant word_constant range_constant one of FALSE TRUE boolean_constant integer_constant integer_number symbolic_constant identifier word_constant 0 word_sign_specifier one of us gt 0 word_width integer_number word_base b B ol lOjdj D word_value hex_digit word_value hex_digit word_value _ hex_digit one of word_sign_specifier h word_base word_width 012345678 9abcde fABCDEF Note that there are some additional restrictions on the exact format of word constants see page I Ip range_constant integer_number Basic Expressions basic_expr constant se variable_identifier define_identifier basic_expr basic_expr amp basic_expr basic_expr basic_expr basic_expr xor basic_expr basic_expr xnor basic_expr basic_expr gt basic_expr basic_expr lt gt basic_expr 125 basic_expr integer_number a constant a variable identif
77. ation This option is incompatible with t v Prints verbosely Scalar variable s values are not truncated if too long for printing m Pipes the output to the program specified by the PAGER shell variable if defined else through the UNIX command more o output file Writes the output generated by the command to output file show_dependencies Shows the dependencies for the given expres Command sion show dependencies h k bound e expression Prints the set of variables that are in the dependency set of the given expression If the bound is specified using the k argument then the computation of the dependencies is done until the bound has been reached If not specified the computation is performed until no new dependencies are found Command Options Shows the command usage k bound Sets the bound limit for the dependencies computation e expr The expression on which the dependencies are computed encode_variables Builds the BDD variables necessary to compile Command the model into a BDD encode_variables h i order file Generates the boolean BDD variables and the ADD needed to encode propositionally the symbolic variables declared in the model The variables are created as default 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 sim
78. cated keyword SPEC can be used instead The syntax of this specification is ctl_specification CTLSPEC ctl_expr SPEC ctl_expr CTLSPEC NAME name ctl_expr SPEC NAME name ctl_expr The module main is instantiated with the so called empty identifier which cannot be referenced in a program 36 The syntax of CTL formulas recognized by NUSMV is as follows etli Since expr simple_expr a simple boolean expression ctl_expr ctl_expr logical not ctl_expr amp ctl_expr logical and ctl_expr ctl_expr logical or ctl_expr xor ctl_expr logical exclusive or ctl_expr xnor ctl_expr logical NOT exclusive or ctl_expr gt ctl_expr logical implies ctl_expr lt gt ctl_expr logical equivalence EG ctl_expr exists globally EX ctl_expr exists next state EF ctl_expr exists finally AG ctl_expr forall globally AX ctl_expr forall next state AF ctl_expr forall finally E ctl_expr U ctl_expr exists until A ctl_expr U ctl_expr forall until simple_expr cannot contain the next operator ct 1_expr cannot contain it either The ct 1_expr should also be a boolean expression Intuitively the semantics of CTL operators is as follows EX pis true ina state s if there exists a state s such that a transition goes from s to s and p is true in s AX pis true ina state s if for all states s where there is a transition from s to
79. d Options autoexec Defines a command string to be automatically executed af ter every command processed by the command interpreter This is useful for things like timing commands or tracing the progress of optimization open_path open_path in analogy to the shell variable PATH is a list of colon separated strings giving directories to be searched whenever a file is opened for read Typically the current di rectory is the first item in this list The standard system library typically NUuSMV_LIBRARY_PATH is always im plicitly appended to the current path This provides a con venient short hand mechanism for reaching standard library files nusmv_stderr Standard error normally stderr can be re directed to a file by setting the variable nusmv_stderr nusmv_stdout Standard output normally stdout can be re directed to a source Execut file by setting the variable nusmv_stdout es a sequence of commands from a file Command sourc h p s x lt file gt lt args gt Reads and executes commands from a file Command Options P Prints a prompt before reading each command 103 s Silently ignores an attempt to execute commands from a nonexistent file x Echoes each command before it is executed lt file gt File name Arguments on the command line after the filename are remembered but not evaluated Commands in the script file can then refer to these arguments usi
80. d by this command will be run after the input file has been pre processed by that pre processor pps is either one sin gle pre processor name with or without double quotes or it is a space separated list of pre processor names contained within double quotes 110 ofm fm file obm bm_file lp n idx is ic ils ips i CE dft SECRE prints flattened model to file fn_file Prints boolean model to file bn_file Lists all properties in SMV model Specifies which property of SMV model should be checked Does not check SPEC properties Sets to 1 the ignore_spec environment variable Does not check COMPUTE properties Sets to 1 the ignore_compute environment variable Does not check LTLSPEC properties Sets to 1 the ignore_lt1lspec environment variable Does not check PSLSPEC properties Sets to 1 the ignore_pslspec environment variable Does not check INVARSPEC properties Sets to 1 the ignore_invariant environment variable Checks whether the transition relation is total Computes the set of reachable states before evaluating CTL expressions Since NuSMV 2 4 0 this option is set by de fault and it is provided for backward compatibility only See also option df Prints the number of reachable states before exiting If the f option is not used the set of reachable states is computed Disable the computation of the set of reachable states This option
81. e PAGER shell variable if defined else through the UNIX more command write_coi_model Writes a restricted flat model to a file Command write_coi_model h n idx p expr P name c 1 i s q C I g Writes the currently loaded SMV model in the specified file after having flattened it If a property is specified the dumped model is the result of applying the Cone Of Influence over that property otherwise a restricted SMV model is dumped for each property in the property database Processes are eliminated and a corresponding equivalent model is printed out If no file is specified stderr is used for output Command Options o filename Attempts to write the flat SMV model in filename p expr Applies COI for the given expression expression Notice that also the property type has to be specified P name Applies COI for property named name n idx Applies COI for property stored with index idx e Dumps COI model for all CTL properties 1 Dumps COI model for all LTL properties i Dumps COI model for all INVAR properties S Dumps COI model for all PSL properties q Dumps COI model for all COMPUTE properties gt Only prints the list of variables that are in the COI of properties g Dumps the COI model that represents the union of all COI properties cone_of_influence Environment Variable Uses the cone of influence reduction when checking properties When cone of influence
82. e is executed Traces must be complete in order to perform execution Command Options v a m o output file e engine trace number Verbosely prints traces execution steps Prints all the currently stored traces Pipes the output through the program specified by the PAGER shell variable if defined else through the UNIX command more Writes the output generated by the command to output file Selects an engine for trace re execution It must be one of bdg sat or smt The ordinal identifier number of the trace to be printed This must be the last argument of the command Omitting the trace number causes the most recently generated trace to be executed execute_partial_traces Executes partial traces on the model FSM Command execute_partial_traces e engine a trace h v r m o output file number Executes traces stored in the Trace Manager If no trace is specified last registered trace is executed Traces are not required to be complete Upon succesful termination a new complete trace is registered in the Trace Manager Command Options v a D o output file e engine Verbosely prints traces execution steps Prints all the currently stored traces Performs restart on complete states When a complete state i e a state which is non ambiguosly determined by a com plete assignment to state variables is encountered the re execution al
83. e within sequence_or_psl_bexpr psl_bexpr sequence within_ sequence_or_psl_bexpr psl_bexpr sequence whilenot psl_bexpr sequence whilenot psl_bexpr sequence whilenot psl_bexpr sequence whilenot_ psl_bexpr sequence sequence_or_psl_bexpr sequence psl_bexpr sequence SERE SERE sequence psl_bexpr 7 COMPOSITION OPERATORS SERE SERE SERE SERE SERE amp SERE SERE amp amp SERE SERE SERE RegExp QUALIFIERS SERE count count SERE i psl_bexpr count psl_bexpr gt count count number range OBE_property AX OBE_property AG OBE_property AF OBE_property A OBE_property U OBE_property 133 fex Q O ive Hw m E_property E_property E_property E_property U OB FE property 134 Index see bang 99 go_bmc 63 got o state 89 Po go0 55 add_property 65 help 101 alias 100 history 101 bmc_inc_simulate 82 pick_state 85 bmc_pick_state 8 print_bdd_stats 99 bmc_set up 68 print_current _state 90 bmc_simulate_check_feasibl _const rq imins fair_states 9 print fair_transitions 9 bmc_simulate 8 print_formula 93 build_boolean_model 56 print_fsm_stats 59 build_flat_model 56 print_iwls95options 55 buildmodel 53 print_reachable_states 8 check_compu
84. e Command write_boolean_model h o filename Writes the currently loaded SMV model in the specified file after having flattened and booleanized it Processes are eliminated and a corresponding equivalent model is printed out If no file is specified the file specified via the environment variable output_boolean_model_file is used if any otherwise standard output is used Command Options 0o filename Attempts to write the flat and boolean SMV model in filename In NuSMV 2 5 scalar variables are dumped as DEFINEs whose body is their boolean encoding This allows the user to still express and see parts of the generated boolean model in terms of the original model s scalar variables names and values and still keeping the generated model purely boolean Also symbolic constants are dumped within a CONSTANTS statement to declare the values of the original scalar variables for future reading of the generated file When NUSMV detects that there were triggered one or more dynamic reorderings in the BDD engine the command write_boolean_model also dumps the current variables ordering if the option out put_order _file is set The dumped variables ordering will contain single bits or scalar variables depending on the current value of the option write_order_dumps_bits See command write_order for further information about variables ordering output_boolean_model_file Environment Variable The file where the flattened and bool
85. e in each state or just those which have changed from the previous one The one that is used can be chosen by selecting the appropriate trace plugin The values of any constants which depend on both input and state or frozen variables are printed next It then prints the set of inputs which cause the transition to a new state if the model contains inputs before actually printing the new state itself The set of inputs and the subsequent state have the same number associated to them In the case of a looping trace if the next state to be printed is the same as the last state in the trace a line is printed stating that this is the point where the loop begins With the exception of the initial state for which no input values are printed the output syntax for each state is as follows gt Input RACE_NO STATE_NO lt x for each input var being printed i INPUT_VARi VALUI gt State TRACE_NO STATE_NO lt x for each state and frozen var being printed j x STATE_VARJ VALUE x for each combinatorial constant being printed k CONSTANTk VALUE Gl where INPUT_VAR STATE_VAR and CONSTANT have the relevant module names prepended to them seperated by a period with the exception of the module main The version of this plugin which only prints out those variables whose values have changed is the initial default plugin used by NUSMV 93 3 8 2 States Variables Table This trace
86. e required by operations over BDDs Reordering methods can be activated to determine better variable orders in order to reduce the size of the existing BDDs Reordering of the variables can be triggered in two ways by the user or by the BDD package In the first way reordering is triggered by the interactive shell command dynamic_var_ordering with the f option Reordering is triggered by the BDD package when the number of nodes reaches a given threshold The threshold is initialized and automatically adjusted after each reordering by the package This is called dynamic reordering and can be enabled or disabled by the user Dynamic reordering is enabled with the shell command dynamic_var_ordering with the option e and disabled with the d option Variable dynamic_reorder can also be used to determine whether dynamic reordering is active If dynamic reordering is enabled it may be beneficial also to disable BDD caching by unsetting variable enable_sexp2bdd_caching dynamic_reorder Environment Variable Determines whether dynamic reordering is active If this variable is set dynamic reorder ing will take place as described above If not set default no dynamic reordering will occur This variable can also be set by passing dynamic command line option when invoking NUSMV reorder_method Environment Variable Specifies the ordering method to be used when dynamic variable reordering is fired The possible values corresponding to the
87. e variable use_coi_size_sorting for changing properties verification order Command Options n index index is the numeric index of a valid INVAR specification formula actually located in the property database The va lidity of index value is checked out by the system p formula IN Checks the formula specified on the command line context context is the module instance name which the variables in formula must be evaluated in P name Checks the INVAR property named name in the property database k max_length max_length is the maximum problem bound that can be reached Only natural numbers are valid values for this op tion Use this option only if the een sorensson algorithm is selected If no value is given the environment variable bmc_length is considered instead 78 e Performs an extra induction step for finding a proof Can be used only with the een sorensson algorithm a alg alg specifies the algorithm The value can be classic or een sorensson If no value is given the environment variable bmc_invar_alg is considered instead o filename filename is the name of the dumped dimacs file It may con tain special symbols which will be macro expanded to form the real file name Possible symbols are e F model name with path part e f model name without path part e n index of the currently processed formula in the prop erties database e the character gen_invar bmc Generates the given
88. each partition set to cp_t DEFAULT with cp_t 1000 DEPRECATED use thresh instead Enables Iwls95 conjunctive partitioning and sets the thresh old of each partition to cp_t Disables affinity clustering Enables Jw ls95CP preordering Enables BMC instead of BDD model checking works only for LTL properties and PSL properties that can be translated into LTL Sets bmc_length variable used by BMC Sets sat_solver variable used by BMC so select the sat solver to be used Enables on or disables off Sexp inlining by setting sys tem variable sexp_inlining Default value is of f Enables on or disables off RBC inlining by setting sys tem variable rbc_inlining Default value is on The idea about inlining was taken from ABE0O by Parosh Aziz Abdulla Per Bjesse and Niklas E n Sets the algorthim used for BDD based language emptiness of Biichi fair transition systems by setting system variable oreg_justice_emptiness_bdd_algorithm de fault is EL_bwd The available algorithms are EL_bwd EL_fwd 113 Bibliography ABE00 BCCZ99 BCLt 94 CBM90 CCG 02 CCGR00 CGH97 Dil88 EL86 EMSS91 ES04 P A Abdulla P Bjesse and N E n Symbolic reachability analysis based on sat solvers In Proceedings of Tools and Algorithms for Construction and Analysis of Systems 6th International Conference TACAS 2000 volume 1785 of Lecture Notes in Computer Science pages 411 425 S
89. eanized model has to be written The default value is stdout 57 output_word format Environment Variable This variable sets in which base unsigned word e and signed word e constants are outputted during traces counterexamples etc printing Possible values are 2 8 10 and 16 Note that if a part of an input file is outputted for example if a specification expression is outputted then the unsigned word e and signed word e constants remain in same format as they were written in the input file 3 2 Commands for Checking Specifications The following commands allow for the BDD based model checking of a NUSMV model compute_reachable Computes the set of reachable states Command compute_reachable h k number t seconds Computes the set of reachable states The result is then used to simplify image and preim age computations This can result in improved performances for models with sparse state spaces Sometimes the execution of this command can take much time because the compu tation of reachable states may be very expensive Use the k option to limit the number of forward step to perform If the reachable states has been already computed the command returns immediately since there is nothing more to compute Command Options k number If specified limits the computation of reachable states to perform number steps forward starting from the last com puted frontier This means that you can expand the com
90. eat the n th previous command old new Replace old with new in previous command Trailing spaces are significant during substitution Initial spaces are not significant print_usage Prints processor and BDD statistics Command print_usage h Prints a formatted dump of processor specific usage statistics and BDD usage statistics For Berkeley Unix this includes all of the information in the get rusage structure quit exits NuSMV Command quit h s x Stops the program Does not save the current network before exiting Command Options s Frees all the used memory before quitting This is slower and it is used for finding memory leaks X Leaves immediately Skip all the cleanup code leaving it to the OS This can save quite a long time reset Resets the whole system Command reset h Resets the whole system in order to read in another model and to perform verification on it set Sets an environment variable Command set h lt name gt lt value gt A variable environment is maintained by the command interpreter The set command sets a variable to a particular value and the unset command removes the definition of a variable If set is given no arguments it prints the current value of all variables Command Options lt name gt Variable name lt value gt Value to be assigned to the variable Using the set command to set a variable without giving any explicit
91. eau resulting from BDD based LTL model checking performed by command check_1t1spec If the variable 1tl_tableau_forward_search is not set default the resulting tableau will inherit the computation of the reachable states from the model if enabled If the variable is set the reachable states set will be calculated for the model and for the tableau resulting from LTL model checking This might improve performances of the command check_1tlspec but may also lead to a dramatic slowing down This variable has effect only when the calculation of reachable states for the model is enabled see forward_search oreg_justice_ emptiness_bdd_algorithm Environment Variable The algorithm used to determine language emptiness of a Biichi fair transition sys tem The algorithm may be used from the following commands check 1tlspec check_pslspec Possible values are e EL bwd The default value The Emerson Lei algorithm EL86 in its usual back wards direction i e using backward image computations e EL fwd A variant of the Emerson Lei algorithm that uses only for ward image computations see e g HKQO3 This variant requires the variables forward_search ltl_tableau_forward_search use_reachable_states to be set Furthermore counterexample compu tation is not yet implemented i e counter_examples should not be set When invoking one of the commands mentioned above all required settings are performed automatically if not already found as n
92. eeded and are restored after execution of the command check_invar Performs model checking of invariants Command check_invar h m o output file n number invar expr IN context P name s strategy e forward backward heuristic j bdd bmc heuristic t threshold k length Performs invariant checking on the given model An invariant is a set of states Checking the invariant is the process of determining that all states reachable from the initial states lie in the invariant Invariants to be verified can be provided as simple formulas without any temporal operators in the input file via the INVARSPEC keyword or directly at command line using the option p Option n can be used for checking a particular invariant of the model If neither n nor p are used all the invariants are checked During checking of invariants all the fairness conditions associated with the model are ignored If an invariant does not hold a proof of failure is demonstrated This consists of a path starting from an initial state to a state lying outside the invariant This path has the property that it is the shortest path leading to a state outside the invariant A search strategy can be specified with s option This is useful to speed up the check in some situations If forward backward or bdd bmc strategy is specified then it is possible to choose a search heuristic with e option bdd bmc strategy
93. elow with the operators on the left and the signatures of the rules on the right To save space more than one operator may be on the left hand side and it is also the case that an individual operator may have more than one signature For more information on these expressions and their type rules see Section 2 2 Expressions page 9 Constants boolean_constant boolean integer_constant integer symbolic_constant symbolic enum word_constant unsigned word N or signed word N where N is the number of bits required range_constant integer set Variable and Define variable_identifier Type where Type is the type of the variable define_identifier Type where Type is the type of the define s expression 120 Arithmetic Operators integer integer unsigned word N unsigned word N signed word N signed word N integer integer integer unsigned word N unsigned word N unsigned word N signed word N signed word N signed word N mod integer integer integer unsigned word N unsigned word N unsigned word N signed word N signed word N signed word N For operations on words the result is taken modulo Qn gt lt integer integer boolean unsigned word N unsigned word N boolean signed word N signed word N boolean Logic Operators negation boolean boolean unsigned word N unsigned word N
94. em into a dimacs file Each problem is related to a specific problem bound which increases from zero 0 to the given maximum problem bound In this short description length is the bound of the problem that system is going to dump out In this context the maximum problem bound is represented by the max_length parameter or by its default value stored in the environment variable bmc_length Each dumped problem also depends on the loopback you can explicitly specify by the 1 option or by its default value stored in the environment variable bmc_loopback The property to be checked may be specified using the n idxorthe p formula options You may specify dimacs file name by using the option o filename otherwise the default value stored in the environment variable bmc_dimacs_filename will be con sidered 71 Command Options n index index is the numeric index of a valid LTL specification for mula actually located in the properties database The valid ity of index value is checked out by the system p formula IN Checks the formula specified on the command line context context is the module instance name which the variables in formula must be evaluated in P name Checks the LTL property named name in the property database k max_tlength max_length is the maximum problem bound used when in creasing problem bound starting from zero Only natural numbers are valid values for this option If no value is given the environment v
95. emental algorithms bmc_setup Builds the model in a Boolean Epression format Command bmc_setup h You must call this command before use any other bmc related command Only one call per session is required go_bmce Initializes the system for the BMC verification Command go_bmc h f This command initializes the system for verification It is equivalent to the command sequence read_model flatten_hierarchy encode_variables build_boolean_model bmc_setup If some commands have already been executed then only the remaining ones will be invoked Command Options f Forces model construction even when Cone Of Influence is enabled 68 sexp_inlining Environment Variable This variable enables the Sexp inlining when the boolean model is built Sexp inlining is performed in a similar way to RBC inlining see system variable rbc_inlining but the underlying structures and kind of problem are different because inlining is applied at the Sexp level instead of the RBC level Inlining is applied to initial states invariants and transition relations By default Sexp inlining is disabled rbe_inlining Environment Variable When set this variable makes BMC perform the RBC inlining before committing any problem to the SAT solver Depending on the problem structure and length the inlining may either make SAT solving much faster or slow it down dramatically Experiments showed an average improvement in time of SAT so
96. en the environment variable bmc_length is con sidered instead N Does not perform virtual unrolling e Performs completeness check gen_Itlspec_sbme Dumps into one or more dimacs files the given Command LTL specification or all LTL specifications if no formula is given Generation and dumping parameters are the maximum bound and the loopback values gen_ltlspec_sbmc h n idx p formula IN context P name k max_length 1l loopback o filename This command generates one or more problems and dumps each problem into a dimacs file The BMC encoding used is the one by of Latvala Biere Heljanko and Junttila as de scribed in Each problem is related to a specific problem bound which increases from zero 0 to the given maximum problem length Here max_length is the bound of the problem that system is going to generate and dump In this context the maximum prob lem bound is represented by the k command parameter or by its default value stored in the environment variable bmc_length The single generated problem also depends on the Loopback parameter you can explicitly specify by the 1 option or by its default value stored in the environment variable bmc_loopback The property to be used for tghe problem dumping may be specified using the n idx or the p formula options You may specify dimacs file name by using the op tion o filename otherwise the default value stored in the environment variable bmc
97. ength 1 loopback o filename This command generates one or more problems and calls SAT solver for each one The BMC encoding used is the one by of Latvala Biere Heljanko and Junttila as described in LBHJ05 Each problem is related to a specific problem bound which increases from zero 0 to the given maximum problem length Here max_length is the bound of the problem that system is going to generate and solve In this context the maximum problem bound is represented by the k command parameter or by its default value stored in the environment variable bmc_length The single generated problem also depends on the Loopback parameter you can explicitly specify by the 1 option or by its default value stored in the environment variable bmc_loopback The property to be checked may be specified using the n idx or the p formula options If you need to generate a DIMACS dump file of all generated problems you must use the option o filename See variable use_coi_size_sorting for changing properties verification order Command Options n index index is the numeric index of a valid LTL specification for mula actually located in the properties database 74 p formula IN context P name k max_length 1 loopback o filename Checks the formula specified on the command line context is the module instance name which the variables in formula must be evaluated in Checks the LTL property named name in the property
98. ently loaded model name with full path e f The currently loaded model name without path part e n The numerical index of the currently processed formula in the property database e k The currently generated problem length e I The currently generated problem loopback value e The character The default value is _k k_1 1_n n bmc_sbmc_gf_fg_opt Environment Variable Controls whether the system exploits an optimization when performing SBMC on formu lae in the form F Gp or GFp The default value is 1 active check_invar_bme Generates and solves the given invariant or all Command invariants if no formula is given check_invar_bmc h n idx p formula IN context P name a alg e k bmc_bound o filename In Bounded Model Checking invariants are proved using induction For this satisfiability problems for the base and induction step are generated and a SAT solver is invoked on each of them At the moment two algorithms can be used to prove invariants In one algorithm which we call classic the base and induction steps are built on one state and one transition respectively Another algorithm which we call een sorensson ESO4 can build the base and induction steps on many states and transitions As a result the second algorithm is more powerful Also notice that during checking of invariants all the fairness conditions associated with the model are ignored Se
99. erands can be of boolean unsigned word e or signed word e type and the type of the whole expression is the type of the operands Note that both word operands should have the same width Equality and Inequality The operators equality and inequality have the following signature 14 boolean boolean boolean integer integer boolean symbolic enum symbolic enum boolean integers and symbolic enum integers and symbolic enum boolean unsigned word N unsigned word N boolean signed word N signed word N boolean No implicit type conversion is performed For example in the expression TRUE 5 the left operand is of type boolean and the right one is of type integer Though the signature of the operation does not have a boolean integer rule the expression is not correct because no implicit type conversion will be performed One can use the toint or the bool for explicit casts For example toint TRUE 5 or TRUE bool 5 This is also true if one of the operands is of type unsigned word 1 and the other one is of the type boolean Explicit cast must be used e g using word1 or bool Relational Operators gt lt gt lt The relational operators gt greater than lt less than gt greater than or equal to and lt less than or equal to have the following signature gt lt gt lt integer integer boolean unsigned
100. erences a variable define or a module in stance from inside the main module Let us consider the following MODULE main VAR a boolean VAR b foo VAR c moo MODULE foo VAR q boolean e moo MODULE moo DEFINE f 0 lt 1 MODULE not_used VAR n boolean VAR t used MODULE used VAR k boolean The full identifier of the variable a is a the full identifier of the variable q from the module foo is b q the full identifier of the module instance e from the module foo is b e the full identifiers of the define f from the module moo are b e f and c f because two module instances contain this define Notice that the variables n and k as well as the module instance t do not have full identifiers because they cannot be accessed from main since the module not_used is not instantiated In the NUSMV language variable define and module instances belong to one namespace and no two full identifiers of different variable define or module instances should be equal Also none of them can be redefined A symbolic constant can be introduced by a variable declaration if its type specifier enumerates the symbolic constant For example the variable declaration VAR a OK FAIL waiting declares the variable a as well as the symbolic constants OK FAIL and waiting The full identifiers of the symbolic constants are equal to their simple identifiers with the additional condition
101. es Shows the traces generated in a NuSMV session Command show_traces h v t A m o output file p plugin no a trace_number from_state to_state Command Options v Verbosely prints traces content all state and frozen vari ables otherwise it prints out only those variables that have changed their value from previous state This option only applies when the Basic Trace Explainer plugin is used to display the trace 91 o output file p plugin no trace_number from_step to step Prints only the total number of currently stored traces Prints all the currently stored traces Pipes the output through the program specified by the PAGER shell variable if defined else through the UNIX command more Writes the output generated by the command to output file Uses the specified trace plugin to display the trace The ordinal identifier number of the trace to be printed Omitting the trace number causes the most recently gener ated trace to be printed The number of the first step of the trace to be printed Nega tive numbers can be used to denote right to left indexes from the last step The number of the trace to be printed Negative numbers can be used to denote right to left indexes from the last step Omitting this parameter causes the entire suffix of the trace to be printed Prints the trace s using a rewriting mapping for all symbols The rewriting is the same used i
102. expr MAX rtctl_expr rtctl_expr MIN start final returns the length of the shortest path from a state in start to a state in final For this the set of states reachable from start is computed If at any point we encounter a state satisfying final we return the number of steps taken to reach the state If a fixed point is reached and no computed states intersect final then infinity is returned MAX start final returns the length of the longest path from a state in start to a state in final If there exists an infinite path beginning in a state in start that never reaches a state in final then infinity is returned If any of the initial or final states is empty then undefined is returned It is important to remark here that if the FSM is not total i e it contains deadlock states COMPUTE may produce wrong results It is possible to check the FSM against deadlock states by calling the command check_fsm 40 2 4 5 PSL Specifications NUSMV allows for PSL specifications as from version 1 01 of PSL Language Reference Manual psl03 PSL specifications are introduced by the keyword PSLSPEC The syntax of this declaration as from the PSL parsers distributed by IBM PSL is pslspec_declaration PSLSPEC psl_expr PSLSPEC NAME name psl_expr where psl_expr psl_primary_expr psl_unary_expr psl_binary_expr psl_conditional_expr psl_case_expr psl_property The first five classes define the build
103. finished 2 4 2 O FAIL 1 3 7 OK etc All elements of an enumer ation have to be unique although the order of elements is not important However in the NUSMV type system expressions cannot be of actual enumeration types but of their simplified and generalised versions only Such generalised enumeration types do not contain information about the exact values constituting the types but only the flag whether all values are integer numbers symbolic constants or both Below only generalised versions of enumeration types are explained The symbolic enum type covers enumerations containing only symbolic constants For example the enumerations stopped running waiting and FAIL OK be long to the symbolic enum type There is also a integers and symbolic enum type This type comprises enumerations which contain both integer numbers and symbolic constants for example 1 1 waiting 0 1 OK running stopped waiting 0 Another enumeration type is integer enum Example of enumerations of integers are 2 4 2 O and 1 1 In the NUSMV type system an expression of the type integer enum is always converted to the type integer Explaining the type of expression we will always use the type integer instead of integer enum Enumerations cannot contain any boolean value i c FALSE TRUE boolean type must be declared as boolean To summarise we actually deal only with two enumeration types symbolic enum and integers and symbo
104. g syntax type_specifier simple_type_specifier module_type_specifier simple_type_specifier boolean word basic_expr unsigned word basic_expr signed word basic_expr enumeration_type_body basic_expr basic_expr array basic_expr basic_expr of simple_type_specifier enumeration_type_body enumeration_type_value enumeration_type_body enumeration_type_value enumeration_type_value symbolic_constant integer_number There are two kinds of type specifier asimple type specifier andamodule type specifier The module type specifier is explained later in Section 2 3 11 MODULE Instantiations page 31 The simple type specifier comprises boolean type integer type enumeration types unsigned word e signed word e and arrays types The boolean type is specified by the keyword boolean A enumeration type is specified by full enumeration of all the values the type comprises For example possible enumeration type specifiers are 0 2 3 1 1 0 OK OK FAIL running FALSE and TRUE values cannot be used as enumeration type speci fiers The values in the list are enclosed in curly brackets and separated by commas The values may be integer numbers symbolic constants or both All values in the list should be distinct from each other although the order of values is not important Note expressions cannot be of the actual enumeration types but only the simplified ver sions of enumeratio
105. gical not ltl_expr amp ltl_expr logical and ltl_expr ltl_expr logical or ltl_expr xor ltl_expr logical exclusive or ltl_expr xnor l1tl_expr logical NOT exclusive or itl_expr gt 1ltl_expr logical implies ltl_expr lt gt ltl_expr logical equivalence gt FUTURE X 1ltl_expr next state G ltl_expr globally F ltl_expr finally ltl_expr U ltl_expr until ltl_expr V l1tl_expr releases PAST Y 1ltl_expr previous state Z 1ltl_expr not previous state not H 1tl_expr historically O ltl_expr once ltl_expr S ltl_expr since ltl_expr T ltl_expr triggered Real Time CTL Specification rtctl_specification SPEC rtctl_expr rtctl_expr ctl_expr EBF range rtctl_expr ABF range rtctl_expr EBG range rtctl_expr ABG range rtctl_expr A rtctl_expr BU range rtctl_expr E rtctl_expr BU range rtctl_expr range integer_number integer_number It is also possible to compute quantative information for the FSM compute_specification COMPUTE compute_expr compute_expr MIN rtctl_expr rtctl_expr MAX rtctl_expr rtctl_expr PSL Specification pslspec_declaration PSLSPEC psl_expr psl_expr psl_primary_expr psl_unary_expr 130 psl_binary_expr psl_conditional_expr psl_case_expr psl_property psl_primary_expr number 7 a numeric constant boolean 7 a boolean constant var_id a variable identifier psl_expr
106. gorithm is re initialized thus reducing compu tation time Pipes the output through the program specified by the PAGER shell variable if defined else through the UNIX command more Writes the output generated by the command to output file Selects an engine for trace re execution It must be one of bdd sat or smt 88 trace_number The ordinal identifier number of the trace to be printed This must be the last argument of the command Omitting the trace number causes the most recently generated trace to be executed 3 7 Traces A trace consists of an initial state optionally followed by a sequence of states inputs pairs corresponding to a possible execution of the model Apart from the initial state each pair contains the inputs that caused the transition to the new state and the new state itself The initial state has no such input values defined as it does not depend on the values of any of the inputs The values of any constants declared in DEFINE sections are also part of a trace If the value of a constant depends only on state and frozen variables then it will be treated as if it is a state variable too If it depends only on input variables then it will be treated as if it is an input variable If however a constant depends upon both input and state frozen variables and or NEXTed state variables then it gets displayed in a separate combinatorial section Since the values of any such consta
107. gram specified by the PAGER shell variable if defined else through the UNIX command more Writes the output generated by the command in processing PSLSPEC s to the file output file A PSL formula to be checked context is the module instance name which the variables in psl expr must be evaluated in Checks the PSL property with index number in the prop erty database Checks the PSL property named name in the property database Applies SAT based bounded model checking The SAT solver to be used will be chosen according to the current value of the system variable sat_solver Applies incremental SAT bounded model checking if avail able i e if an incremental SAT solver has been linked to NuSMV This option can be used only in combination with the option b Dumps DIMACS version of bounded model checking prob lem into a file whose name depends on the system variable bmc_dimacs_filename This feature is not allowed in combination of the option i Generates a single bounded model checking problem with fixed bound and loopback values it does not iterate incre menting the value of the problem bound bmc_length is the maximum problem bound to be checked Only natural numbers are valid values for this option If no value is given the environment variable bmc_length is con sidered instead The loopback value may be e a natural number in 0 max_length 1 A positive sign can be also used as prefix
108. h between frontiers using BMC technology Options j t and k are enabled only when using this strategy Note that the algorithm used for the BMC approach is the one specified in the variable bmc_invar_alg If this option is not specified the value of the environment variable check_invar_strategy is considered 62 e f b heuristic Specify the heuristic that decides at each step if we must ex pand reachable states or bad states This option is enabled only when using forward backward or bdd bmc strate gies Possible values are zigzag and smallest zigzag forces to perform a step forward and the next step backward an so on while smallest performs a step from the frontier with the BDD representing the state is smaller If this op tion is not specified the value of the environment variable check_invar_forward_backward_heuristic is considered j bdd bmc heuristic When using bdd bmc strategy specify the heuristic that decides at which step we must switch from BDD to BMC technolgy You should use the option t to specify the threshold for the chosen heuristic Possible heuristics are steps and size steps forces to switch after a num ber of steps equal to the threshold while size switch when BDDs are bigger in the number of nodes than the threshold If this option is not specified the value of the environment variable check_invar_bddbmc_heuristic
109. he main Module The syntax of a NUSMV program is program module_list module_list module module_list module There must be one module with the name main and no formal parameters The module main is the one evaluated by the interpreter 2 3 15 Namespaces and Constraints on Declarations Identifiers in the NUSMV input language may reference five different entities modules vari ables defines module instances and symbolic constants Module identifiers have their own separate namespace Module identifiers can be used in module type specifiers only and no other kind of identifiers can be used there see Section 2 3 11 MODULE Instantiations page Bip Thus module identifiers may be equal to other kinds of identifiers without making the program ambiguous However no two modules should be declared with the same identifier Modules cannot be declared in other modules therefore they are always referenced by simple identifiers Variable define and module instance identifiers are introduced in a program when the mod ule containing their declarations is instantiated Inside this module the variables defines and 34 module instances may be referenced by the simple identifiers Inside other modules their simple identifiers should be preceded by the identifier of the module instance containing their declaration and lt DOT gt Such identifiers are called complex identifier The full identifier is a complex identifier which ref
110. hecked by a specialised algorithm during reachability analysis and Invariant Spec ifications can contain next operators Fairness constraints are not taken into account during invariant checking 2 4 3 LTL Specifications LTL specifications are introduced by the keyword LTLSPEC The syntax of this specification is ltl_specification LTLSPEC ltl_expr LTLSPEC NAME name ltl_expr The syntax of LTL formulas recognized by NUSMV is as follows ltl_expr simple_expr a simple boolean expression ltl_expr ltl_expr logical not ltl_expr amp ltl_expr logical and ltl_expr ltl_expr logical or ltl_expr xor ltl_expr logical exclusive or ltl_expr xnor l1tl_expr logical NOT exclusive or itl_expr gt 1ltl_expr logical implies ltl_expr lt gt ltl_expr logical equivalence FUTURE X 1ltl_expr next state G ltl_expr globally F ltl_expr finally ltl_expr U ltl_expr until ltl_expr V l1tl_expr releases PAST Y 1ltl_expr previous state Z 1ltl_expr not previous state not H 1tl_expr historically O 1tl_expr once ltl_expr S ltl_expr since ltl_expr T ltl_expr triggered Intuitively the semantics of LTL operators is as follows e X pis true at time t if p is true at time t 1 e F pis true at time t if p is true at some time t gt t e G pis true at time t if p is true at all times t gt t e p U gis true at time t if q is true at some time t gt
111. hold 1tl_tableau_forward_search 60 nusmv_stderr 107 nusmv_st din 107 nusmv_st dout 107 on_failure_script_quit s 106 open_path 107 oreg_justice_emptiness_bdd_algorithm output boolean model_file 57 output flatten model_file 57 output order_file 52 output_word_format partition_method pp list 49 prop _print_method 68 rbc_inlining 69 rbc_rbc2cnf_algorithm 69 reorder_method check_invar_forward_backward_heuri staitcsolver 81 check_invar_strategy 63 cone _of_influence 67 conj _part_threshold 54 counter_examples 90 daggifier_counter_threshold 57 daggifier_depth_threshold 57 daggifier_statistics 57 default simulation steps 87 default trace_ plugin 1 disable_syntact ic_checks 50 dynamic _reorder 95 enable_sexp2bdd_caching 99 filec 107 forward_search 60 history char I07 image_W 1 2 3 4 55 image_cluster size 54 image_verbosity 55 input _file 49 input_order_file 52 iwls95preorder 55 keep_single_value_vars 50 sexp_inlining 69 shell _char 107 show defines_in _traces 9 shown_states 87 traces_hiding_prefix 87 90 traces _regexp 87 90 traces_show_defines_with_next 9 trans_order_file 54 type _check ing_warning _on 0 use_coi_size_sorting vars_order_type gt 3 verbose_level write_order_dumps_bit s 2 136 Index Symbols snusmvre 110 AG 112 bdd_soh 112 bmc_length k 13 bmc 13 coi 112
112. iable bmc_length is considered instead 1 loopback The loopback value may be e a natural number in 0 max_length 1 A positive sign C can be also used as prefix of the number Any in valid combination of length and loopback will be skipped during the generation solving process e a negative number in 1 bmc_length In this case loop back is considered a value relative to length Any invalid combination of length and loopback will be skipped during the generation solving process e the symbol X which means no loopback e the symbol which means all possible loopback from zero to length 1 o filename filename is the name of the dumped dimacs file It may con tain special symbols which will be macro expanded to form the real file name Possible symbols are e F model name with path part e f model name without path part e k current problem bound e I1 current loopback value e n index of the currently processed formula in the prop erty database e the character gen_Itlspec_bme Dumps into one or more dimacs files the given Command LTL specification or all LTL specifications if no formula is given Generation and dumping parameters are the maximum bound and the loopback value gen_ltlspec_bmc h n idx p formula IN context P name k max_length 1 loopback o filename This command generates one or more problems and dumps each probl
113. ier complex_identifier simple_expression self Every variable and define used in an expression should be declared It is possible to have forward references when a variable or define identifier is used textually before the corresponding declaration Notations with lt DOT gt are used to access the components of modules For example if m is an instance of a module see Section 2 3 11 MODULE Instantiations page 3 I for information 8This also means that the actual parameters are analyzed in the context of the variable declaration where the module is instantiated not in the context of the expression where the formal parameter occurs 32 about instances of modules then the expression m c identifies the component c of the module instance m This is precisely analogous to accessing a component of a structured data type Note that actual parameters of a module can potentially be instances of other modules Therefore parameters of modules allow access to the components of other module instances as in the following example MODULE main x VAR a bar m foo a MODULE bar VAR q boolean p boolean MODULE foo c DEFINE flag c q c p Here the value of m flag is the logical OR of a p and a q Individual elements of an array are accessed in the typical fashion with the index given in square brackets See for more information It is possible to refer to the name tha
114. ier a define identifier logical bitwise logical bitwise logical bitwise logical bitwise logical bitwise logical bitwise logical bitwise NOT AND OR exclusive OR NOT xor implication equivalence _ word_value basic_expr basic_expr equality basic_expr basic_expr inequality basic_expr lt basic_expr less than basic_expr gt basic_expr greater than basic_expr lt basic_expr less than or equal basic_expr gt basic_expr greater than or equal basic_expr unary minus basic_expr basic_expr integer addition basic_expr basic_expr integer subtraction basic_expr basic_expr integer multiplication basic_expr basic_expr integer division basic_expr mod basic_expr integer remainder basic_expr gt gt basic_expr bit shift right basic_expr lt lt basic_expr bit shift left basic_expr index index subscript basic_expr integer_number integer_number word bits selection basic_expr basic_expr word concatenation wordl basic_expr boolean to word 1 convertion bool basic_expr toint basic_expr signed basic_expr unsigned to signed word convertion unsigned basic_expr signed to unsigned word convertion extend basic_expr basic_expr word width increase resize basic_expr basic_expr word width resizing basic_expr union basic_expr union of set expressions set_body_expr set expression basic_expr i
115. ier and indicates a unique value symbolic_constant identifier The type of a symbolic constant is symbolic enum See Section 2 3 15 Namespaces page 34 for more information about how symbolic constants are distinguished from other identifiers ie variables defines etc 10 Word Constant Word constant begins with digit 0 followed by optional character u unsigned or s signed and one of the characters b B binary 0 O octal d D decimal or h H hexadeci mal which gives the base that the actual constant is in Next comes an optional decimal integer giving the number of bits then the character _ and lastly the constant value itself Assuming N is the width of the constant the type of a word constant is signed word N if character s is provided and unsigned word N otherwise For example 0sb5_10111 has type signed word 5 0uo06_37 has type unsigned word 6 0d11_9 has type unsigned word 1 1 Osh12_a9 has type signed word 12 The number of bits can be skipped in which case the width is automatically calculated from the number of digits in the constant and its base It may be necessary to explicitly give leading zeroes to make the type correct the following are all equivalent declarations of the integer constant 11 as a word of type unsigned word 8 Oud8_11 Oub8_1011 0b_00001011 Oh_O0b Oh8_b The syntactic rule of the word constant is the following word_constant 0 word_sign_specifier word_base word_width
116. ing blocks for ps1_property and provide means of com bining instances of that class they are defined as follows psl_primary_expr number a numeric constant boolean 7 a boolean constant word j a word constant var_id 7 a variable identifier psl_expr psl_expr psl_expr psl_expr psl_expr psl_expr psl_unary_expr psl_primary_expr psl_primary_expr psl_primary_expr bool psl_expr wordl psl_expr uwconst psl_expr psl_expr sweonst psl_expr psl_expr sizeof psl_expr toint psl_expr signed psl_expr unsigned psl_expr extend psl_expr psl_primary_expr resize psl_expr psl_primary_expr select psl_expr psl_expr psl_expr psl_binary_expr psl_expr psl_expr psl_expr union psl_expr psl_expr in psl_expr psl_expr psl_expr psl_expr psl_expr psl_expr psl_expr psl_expr psl_expr psl_expr psl_expr 41 psl_expr psl_expr psl_expr lt psl_expr psl_expr lt psl_expr psl_expr gt psl_expr psl_expr gt psl_expr psl_expr amp psl_expr psl_expr psl_expr psl_expr xor psl_expr psl_expr xnor psl_expr psl_expr lt lt psl_expr psl_expr gt gt psl_expr psl_expr psl_expr psl_conditional_expr psl_expr psl_expr psl_expr psl_case_expr case psl_expr psl_expr psl_expr psl_expr endcase Among the subclasses of psl_expr we depict the class ps1_bexpr that will be used in the foll
117. integer set integer set symbolic set symbolic set symbolic set integers and symbolic set integers and symbolic set integers and symbolic set At first if it is possible the operands are converted to their set counterpart types then both operands are implicitly converted to a minimal common type in boolean set boolean set boolean set integer set integer set integer set symbolic set symbolic set symbolic set integers and symbolic set integers and symbolic set integers and symbolic set At first if it is possible the operands are converted to their set counterpart types then implicit convertion is performed on one of the operands Case and If Then Else Expression case cond resulti conda results cond resultn esac cond resulti resulta cond must be of type boolean If one of result is of a set type then all other result are converted to their counterpart set types The overall type of the expression is such a minimal type that each result can be implicitly converted to Formula Operators EX AX EF AF EG AG X Y Z G H F O boolean boolean A U E U U S boolean boolean boolean A BU E BU boolean integer integer boolean boolean EBF ABF EBG ABG integer integer boolean boolean 122 Miscellaneous Operators Integer Integer integer_number integer_number integer bool
118. invariant or all invariants if Command no formula is given gen_invar_bmc h n idx p formula IN context P name o filename At the moment the invariants are generated using classic algorithm only see the de scription of check_invar_bmc on page 78 Command Options n index index is the numeric index of a valid INVAR specification formula actually located in the property database The va lidity of index value is checked out by the system p formula IN Checks the formula specified on the command line context context is the module instance name which the variables in formula must be evaluated in P name Checks the INVAR property named name in the property database o filename filename is the name of the dumped dimacs file If you do not use this option the dimacs file name is taken from the environment variable bmc_invar_dimacs_filename File name may contain special symbols which will be macro expanded to form the real dimacs file name Possi ble symbols are e F model name with path part e f model name without path part e n index of the currently processed formula in the prop erties database e the character check_invar_bmc_ine Generates and solves the given invariant Command or all invariants if no formula is given using incremental algo rithms check_invar_bmc_inc h n idx p formula IN context P name a algorithm 79 This comm
119. is attempted that does not satisfy this restriction Index Subscript Operator The index subscript operator extracts one element of an array in the typical fashion On the left of there has to be an expression of array type The index expression in the brackets has to be an expression of integer or word e type with value greater or equal to lower bound and less or equal to the upper bound of the array The signature of the index subscript operator is array N M of subtype word N subtype array N M of subtype integer subtype For example for below declarations MODULE main VAR a array 1 4 of array 1 2 of boolean DEFINE d 12 4 1 2 VAR r O 1 expressions a 1 a 0 r 1 and d r 1 are valid whereas a 0 a 0 r and d 0 r 1 will cause out of bound error Bit Selection Operator The bit selection operator extracts consecutive bits from a unsigned word e or signed word e expression resulting in a new unsigned word e expression This operation always decreases the width of a word or leaves it intact The expressions in the brackets have to be integer constants which specify the high and low bound The high bound must be greater than or equal to the low bound The bits count from 0 The result of the operations is unsigned word e value consisting of the consecutive bits beginning from the high bound of the operand down to and including the low bound bit F
120. its value in the next state If the expression on the right hand side evaluates to a not set expres sion such as integer number or symbolic constant the assignment simply means that the left hand side is equal to the right hand side On the other hand if the expression eval uates to a set then the assignment means that the left hand side is contained in that set It is an error if the value of the expression is not contained in the range of the variable on the left hand side Semantically assignments can be expressed using other kinds of constraints 28 ASSIGN a exp is equivalent to INVAR a in exp ASSIGN init a exp is equivalentto INIT a in exp ASSIGN next a exp is equivalent to TRANS next a in exp Notice that an additional constraint is forced when assignments are used with respect to their corresponding constraints counterpart when a variable is assigned a value that it is not an ele ment of its declared type an error is raised The allowed types of the assignment operator are integer integer integer integer set symbolic enum symbolic enum symbolic enum symbolic set integers and symbolic enum integers and symbolic enum integers and symbolic enum integers and symbolic set unsigned word N unsigned word N signed word N signed word N Before checking the assignment for being correctly typed the implicit type conversion can be applied to the right operand Rules for assignments
121. j lt value variable j gt VALUE lt value gt lt state gt lt combinatorial id i l gt x for each combinatorial constant k lt value variable k gt VALUE lt value gt lt combinatorial gt lt input id 1i 1 gt for each input var 1 lt value variable 1 gt VALUE lt value gt lt input gt lt node gt lt counter example gt Note that for the last state in the trace there is no input section in the node tags This is because the inputs section gives the new input values which cause the transition to the next state in the trace There is also no combinatorial section as this depends on the values of the inputs and are therefore undefined when there are no inputs 94 3 8 4 XML Format Reader This plugin makes use of the Expat XML parser library and as such can only be used on systems where this library is available Previously generated traces for a given model can be loaded using this plugin provided that the original model fild has been loaded and built using the command go When a trace is loaded it is given the smallest available trace number to identify it It can then be manipulated in the same way as any generated trace 3 9 Interface to the DD Package NUSMV uses the state of the art BDD package CUDD Som98 Control over the BDD package can be very important to tune the performance of the system In particular the order of variables is critical to control the memory and the tim
122. jacent variables The best order among those obtained by the series of swaps is retained The number of pairs chosen for swapping equals the number of variables in the diagram random_pivot Same as random but the two variables are chosen so that the first is above the variable with the largest number of nodes and the second is below that vari able In case there are several variables tied for the maxi mum number of nodes the one closest to the root is used sift_converge The sift method is iterated until no further improvement is obtained symmetry sift This method is an implementation of sym metric sifting It is similar to sifting with one addition Variables that become adjacent during sifting are tested for symmetry If they are symmetric they are linked in a group Sifting then continues with a group being moved instead of a single variable 97 e symmetry sift converge The symmetry sift method is iterated until no further improvement is obtained e window 2 3 4 Permutes the variables within windows of n adjacent variables where n can be either 2 3 or 4 so as to minimize the overall BDD size e window 2 3 4 _ converge The window 2 3 4 method is iterated until no further improvement is obtained e group sift This method is similar to symmetry sift but uses more general criteria to create groups e group sift_converge The group sift method is iterated until no further improvement is obtained e
123. king for past LTL In R Cousot editor Verification Model Checking and Abstract Interpretation 6th International Conference VMCAI 2005 number 3385 in Lecture Notes in Computer Science pages 380 395 Springer 2005 A J Martin The design of a self timed circuit for distributed mutual exclu sion In In H Fuchs and W H Freeman editors Proceedings of the 1985 Chapel Hill Conference on VLSI pages 245 260 New York 1985 K L McMillan The smv system draft In Available at http www cs cmu edu modelcheck smv smvmanual r2 2 ps 1992 K L McMillan Symbolic model checking In Kluwer Academic Publ 1993 Moon Hachtel and Somenzi Border block tringular form and conjunction schedule in image computation In FMCAD 2000 Language Front End for Sugar Foundation Language http www haifa il ibm com projects Vverification sugar parser html Accellera Property Specification Language Reference Manual Version 1 01 http www eda org vfv docs psl_Irm 1 01 pdf April 2003 R K Ranjan A Aziz B Plessier C Pixley and R K Brayton Effi cient bdd algorithms for fsm synthesis and verification In In IEEE ACM Proceedings International Workshop on Logic Synthesis Lake Tahoe NV May 1995 VIS A system for Verification and The VIS Group Synthesis Proceed ings of the 8th international conference on computer aided verification p428 432 In Springer Lecture Notes in Computer Science 1102 Edited by R Al
124. l bar is used to separate alternatives in the syntax rules Sometimes one of is used at the beginning of a rule as a shorthand for choosing among several alternatives If the characters and are in bold font they lose their special meaning and become regular tokens In the following an identifier may be any sequence of characters starting with a character in the set A Za z_ and followed by a possibly empty sequence of char acters belonging to the set A Za z0 9_ All characters and case in an identifier are significant Whitespace characters are space lt SPACE gt tab lt TAB gt and new line lt RET gt Any string starting with two dashes and ending with a newline is a comment and ignored by the parser The syntax rule for an identifier is identifier identifier _first_character identifier identifier_consecutive_character identifier _first_character one of ABCDEFGHIJIKLUMNOPQRS TUVWXYZ abcdefghigjgkimnopqrstuvwxyz identifier _consecutive_character identifier _first_character digit one of digit one of 0123456789 An identifier is always distinct from the NUSMV language reserved keywords which are MODULE DEFINE MDEFINE CONSTANTS VAR IVAR FROZENVAR INIT TRANS INVAR SPEC CTLSPEC LTLSPEC PSLSPEC COMPUTE NAME INVARSPEC FAIRNESS JUSTICE COMPASSION ISA ASSIGN CONSTRAINT SIMPWFF CTLWFF LTLWFF PSLWFF COMPWFF IN MIN MAX MIRROR PRED
125. l be considered If the variable output_order_file is unset or set to an empty value then standard output will be used By default the bits constituting the scalar variables encoding are not dumped When a variable bit should be dumped the scalar variable which the bit belongs to is dumped instead if not previously dumped The result is a variable ordering containing only scalar and boolean model variables To dump single bits instead of the corresponding scalar variables either the option b can be specified or the environment variable write order_dumps _bits must be previ ously set When the boolean variable dumping is enabled the single bits will occur within the result ing ordering file in the same position that they occur at BDD level Command Options bp Dumps bits of scalar variables instead of the single scalar variables See also the variable write_order_dumps_bits o order file Sets the environment variable output_order_file to order file and then dumps the ordering list into that file f order file Alias for the o option Supplied for backward compatibility output_order_file Environment Variable The file where the current variable ordering has to be written A value for this variable can also be provided with command line option o The default value is temp ord vars_order_type Environment Variable 52 Controls the manner variables are ordered by default when a variable ordering is no
126. ld_boolean_model h f Compiles the flattened hierarchy into boolean SEXP initial states invariants and transi tion relation Command Options f Forces the boolean model construction write_flat_model Writes a flat model to a file Command write_flat_model h A o filename Writes the currently loaded SMV model in the specified file after having flattened it Processes are eliminated and a corresponding equivalent model is printed out If no file is specified the file specified via the environment variable output flatten_model_file is used if any otherwise standard output is used Command Options 0o filename Attempts to write the flat SMV model in filename 56 A Writes the flat SMV model using a renaming map to anon imize the model All the symbols except numerical con stanst will be renamed output flatten model file Environment Variable The file where the flattened model has to be written The default value is stdout daggifier_depth_threshold Environment Variable Sets the minimum threshold for expressions depth to be daggified daggifier_counter_threshold Environment Variable Sets the minimum threshold for expressions count to be daggified i e expression must show at least Number time to be daggified daggifier_statistics Environment Variable Prints daggifier statistics after model dumping write_boolean_model Writes a flat and boolean model to a fil
127. lexp1 exp2 expNcan be converted to it It is not possible to declare asymmetrical arrays This means that it is forbidden to declare an array with a different number of elements in a dimension For example the following code will result in an error DEFINE x r 1 2 3 1 21 2 3 4 CONSTANTS Declarations CONSTANTS declarations allow the user to explicitly declare symbolic constants that might oc cur or not within the FSM that is being defined CONSTANTS declarations are expecially useful in those conditions that require symbolic constants to occur only in DEFINEs body e g in gen erated models For an example of usage see also the command write_ boolean_model A constant is allowed to be declared multiple times as after the first declaration any further decla ration will be ignored CONSTANTS declarations are an extension of the original SMV grammar and they are supported since NuSMV 2 5 The syntax for this kind of declaration is constants_declaration CONSTANTS constants_body constants_body identifier constants_body identifier 27 2 3 5 INIT Constraint The set of initial states of the model is determined by a boolean expression under the INIT keyword The syntax of an INIT constraint is init_constrain INIT simple_expr Since the expression in the INIT constraint is a simple_expression it cannot contain the next operator The expression also has to be of type boolean If there is mo
128. lic enum These types are distinguishable and have different operations allowed on them 2 1 4 Word The unsigned word e and signed word e types are used to model vector of bits booleans which allow bitwise logical and arithmetic operations unsigned and signed respectively These types are distinguishable by their width For example type unsigned word 3 represents vector of three bits which allows unsigned operations and type signed word 7 represents vector of seven bits which allows signed operations When values of unsigned word N are interpreted as integer numbers the bit representation used is the most popular one i e each bit represents a successive power of 2 between 0 bit number 0 and 2 1 bit number N 1 Thus unsigned word N is able to represent values from 0 to 2 1 The bit representation of signed word N type is two s complement i e it is the same as for unsigned word N except that the highest bit number N 1 has value 2 Thus the possible value for signed word N are from 2 to 2 1 1 2 1 5 Array Arrays are declared with a lower and upper bound for the index and the type of the elements in the array For example array 0 3 of boolean array 10 20 of OK y z array 1 8 of array 1 2 of unsigned word 5 The type array 1 8 of array 1 2 of unsigned word 5 means an array of 8 elements from 1 to 8 each of which is an array of 4 elements from 1 t
129. lving when RBC inlining is enabled RBC inlining is enabled by default The idea about inlining was taken from by Parosh Aziz Abdulla Per Bjesse and Niklas E n rbc_rbe2cnf_algorithm Environment Variable This variable defines the algorithm used for conversion from RBC to CNF format in which a problem is supplied to a SAT solver The default value sheridan refers to She04 algorithm which allows to obtain a more compact CNF formulas The other value tseitin refers to a standard Tseiting transformation algorithm check _Itlspec_bme Checks the given LTL specification or all LTL Command specifications if no formula is given Checking parameters are the maximum length and the loopback value check_ltlspec_bmc h n idx p formula IN context P name k max_length 1 loopback o filename This command generates one or more problems and calls SAT solver for each one Each problem is related to a specific problem bound which increases from zero 0 to the given maximum problem length Here max_length is the bound of the problem that system is going to generate and solve In this context the maximum problem bound is represented by the k command parameter or by its default value stored in the environment variable bmc_length The single generated problem also depends on the loopback parameter you can explicitly specify by the 1 option or by its default value stored in the environ ment variable bmc_loopback
130. mmand Options n index index is the numeric index of a valid LTL specification for mula actually located in the properties database p formula IN Checks the formula specified on the command line context context is the module instance name which the variables in formula must be evaluated in P name Checks the LTL property named name in the property database k max_ength max_length is the maximum problem bound must be reached Only natural numbers are valid values for this option If no value is given the environment variable bmc_length is considered instead 1 loopback The loopback value may be e a natural number in 0 max_length 1 A positive sign can be also used as prefix of the number Any in valid combination of length and loopback will be skipped during the generation solving process e a negative number in 1 bmc_length In this case loop back is considered a value relative to max_length Any in valid combination of length and loopback will be skipped during the generation solving process e the symbol X which means no loopback e the symbol x which means all possible loopback from zero to length 1 check_Itlspec_sbme Checks the given LTL specification or all Command LTL specifications if no formula is given Checking parameters are the maximum length and the loopback value check_ltlspec_sbmc h n idx p formula IN context P name k max_l
131. mp next delta init assignments e Itis no longer possible to write SPEC FAIRNESS statements containing next FAIRNESS next running SPEC next x amp y e The check for circular dependencies among variables has been done more restrictive We say that variable x depends on variable y if x f y We say that there is a circular dependency in the definition of x if x depends on itself e g x f x y x depends on y and y depends on x e g x f y and y f x or x f z z fly and y f x In the case of circular dependencies among variables there is no fixed order in which we can compute the involved variables Avoiding circular dependencies among variables guarantee that there exists an order in which the variables can be computed In NUSMV circular dependencies are not allowed In CMU SMV the test for circular dependencies is able to detect circular dependencies only in normal assignments and not in next assignments The circular dependencies check of NUSMV has been extended to detect circularities also in next assignments For instance the following fragment of code is accepted by CMU SMV but discarded by NUSMV MODULE main VAR y boolean x boolean ASSIGN next x x amp next y next y y amp next x Another difference between NUSMV and CMU SMV is in the variable order file The vari able ordering file accepted by NUSMV can be parti
132. n basic_expr inclusion expression basic_expr basic_expr basic_expr if then else expression count basic_expr_list count of TRUE boolean expressions case_expr case expression next basic_expr next expression basic_expr_list basic_expr basic_expr_list basic_expr set_body_expr basic_expr set_body_expr basic_expr Case Expression and If Then Else Expression case_expr case case_body esac case_body basic_expr basic_expr case_body basic_expr basic_expr basic_expr basic_expr basic_expr 126 word 1 and integer to boolean convertion word N and boolean to integer convertion Simple Expression simple_expr basic_expr Note that simple expressions cannot contain next operators Next Expression next_expr basic_expr Type Specifier type_specifier simple_type_specifier module_type_spicifier simple_type_specifier boolean word integer_number unsigned word integer_number signed word integer_number enumeration_type_body integer_number integer_number array integer_number integer_number of simple_type_specifier enumeration_type_body enumeration_type_value enumeration_type_body enumeration_type_value enumeration_type_value symbolic_constant integer_number Module Type Specifier module_type_specifier identifier parameter_list process identifier parameter_lis
133. n the fair path In NUSMV compassion constraints are identified by keyword COMPASS ton If compassion constraints are used then the model must not con tain any input variables Currently NUSMV does not enforce this so it is the responsibility of the user to make sure that this is the case Fairness constraints are declared using the following syntax all expressions are expected to be boolean fairness_constraint FAIRNESS simple_expr JUSTICE simple_expr COMPASSION simple_expr simple_expr A path is considered fair if and only if it satisfies all the constraints declared in this manner 2 3 10 MODULE Declarations A module declaration is an encapsulated collection of declarations constraints and specifica tions A module declaration also opens a new identifier scope Once defined a module can be reused as many times as necessary Modules are used in such a way that each instance of a mod ule refers to different data structures A module can contain instances of other modules allowing a structural hierarchy to be built The syntax of a module declaration is as follows TIn the current version of NUSMV compassion constraints are supported only for BDD based LTL model checking We plan to add support for compassion constraints also for CTL specifications and in Bounded Model Checking in the next releases of NUSMV 30 module MODULE identifier module_parameters module_body module_parameters iden
134. n types such as symbolic enum and integers and symbolic enum A type specifier can be given by two expressions separated by lt TWO DOTS gt The two expressions have both to evaluate to constants integer numbers and may contain names of defines and module formal parameters For example 1 P1 5 D1 where P1 refers to a module formal parameter and D1 refers to a define Both P1 and D1 have to be statically evaluable to integer constants This is just a shorthand for a enumeration type containing the list of integer numbers from the range given in type specifier For example the type specifiers 1 5 23 and 1 0 1 2 3 4 5 are equivalent Note that the evaluated number on the left from the two dots must be less than or equal to the evaluated number on the right The unsigned word e type is specified by the keywords unsigned word where unsigned may be skipped with a basic_expr supplied in square brackets The expres sion must be statically evaluable to a constant integer number whose value must be greater than zero The signed word e type is specified in a similar way with the keywords signed word The purpose of the word types is to offer integer and bitwise arithmetic An array type is denoted by a sequence of the keyword array a basic_expr specifying the lower bound of the array index two dots a basic_expr specifying the upper bound of the array index the keyword of and the type of array s elements The
135. n write_flat_model with option A Shows the traces currently stored in system memory if any By default it shows the last generated trace if any Optional trace number can be followed by two indexes from_state to_state denoting a trace slice Thus it is possible to require printout only of an arbitrary fragment of the trace this can be helpful when inspecting very big traces If the XML Format Output plugin is being used to save generated traces to a file with the intent of reading them back in again at a later date then only one trace should be saved per file This is because the trace reader does not currently support multiple traces in one file read_trace Loads a previously saved trace Command read_trace h Command Options i filename i filename u s filename Reads in a trace from the specified file Note that the file must only contain one trace This option has been depre cated Use the explicit filename argument instead Turns undefined symbol error into a warning The loader will ignore assignments to undefined symbols Turns wrong section error into a warning The loader will accept symbol assignment even if they are in a different section than expected Assignments will be silently moved to appropriate section i e misplaced assignments to state symbols will be moved back to previous state section and assignments to input combinatorial symbols will be moved forward to
136. nd booleanized SMV files and promotion of boolean constants to their integer counterpart If set to 0 then the type checking is turned on and whenever a type error is encountered while compiling a NUSMV program the user is informed and the execution stopped Since NUSMV 2 5 1 backward compatibility mode introduces a porting feature from old models which use constant 1 as case conditions instead of forcing the use of TRUE The option by default it set to 0 type_checking warning on Environment Variable Enables notification of warning messages generated by the type checking If set to 0 then messages are disregarded otherwise if set to 1 they are notified to the user As default it set to 1 show_vars Shows model s symbolic variables and their values Command show vars h s f i t v v m o output file Prints a summary of the variables declared in the input file Moreover it prints also the list of symbolic input frozen and state variables of the model with their range of values as defined in the input file if the proper command option is specified Command Options s Prints only state variables f Prints only frozen variables i Prints only input variables t Prints only the number of variables among selected kinds grouped by type This option is incompatible with V 50 V Prints only the list of variables with their types among se lected kinds with no summary inform
137. ned word N to an unsigned word N while signed performs the opposite operation and converts an unsigned word N to a signed word N Both operations do not change the bit representation of a provided word The signatures of these conversion operators are unsigned signed word N unsigned word N signed unsigned word N signed word N For example signed Oub_101 Osb_101 signed 0ud3_5 0sd3_3 unsigned 0sb_101 Ousb_101 unsigned 0sd3_3 Oud3_5 2 3 Definition of the FSM We consider a Finite State Machine FSM described in terms of state variables input variables and frozen variables which may assume different values in different states of a transition rela tion describing how inputs leads from one state to possibly many different states and of Fairness conditions that describe constraints on the valid paths of the execution of the FSM In this docu ment we distinguish among constraints used to constrain the behavior of a FSM e g a modulo 22 4 counter increments its value modulo 4 and specifications used to express properties to verify on the FSM e g the counter reaches value 3 In the following it is described how these concepts can be declared in the NUS MV language 2 3 1 Variable Declarations A variable can be an input a frozen or a state variable The declaration of a variable specifies the variable s type with the help of type specifier Type Specifiers Atype specifier has the followin
138. ned word integer signed word e integer signed word integer Set Expressions The set expression is an expression defining a set of boolean integer and symbolic enum values A set expression can be created with the union operator For example 1 union 0 specifies the set of values 1 and 0 One or both of the operands of union can be sets In this 18 case union returns a union of these sets For example expression 1 union 0 union 3 specifies the set of values 1 0 and 3 Note that there cannot be a set of sets in NuSMV Sets can contain only singleton values but not other sets The signature of the union operator is union _ boolean set boolean set boolean set integer set integer set integer set symbolic set symbolic set symbolic set integers and symbolic set integers and symbolic set integers and symbolic set Before checking the expression for being correctly typed if it is possible both operands are converted to their counterpart set types which virtually means converting individual values to singleton sets Then both operands are implicitly converted to a minimal type that covers both operands If after these manipulations the operands do not satisfy the signature of union operator an error is raised by NUSMV There is also another way to write a set expression by enumerating all its values between curly brackets The syntactic rule for the values in curly brackets is set_body_exp
139. ng the history substitution mechanism EXAMPLE Contents of test scr read model i 3 2 flatten hierarchy build variables buildmodel compute_fairness Typing source test scr short smv on the command line will execute the sequence read_model i short smv flatten_hierarchy build_variables buildmodel compute_fairness In this case 0 gets source 1 gets test scr and 2 gets short smv If you type alias st source test scr and then type st short smv bozo you will execute readmodel i bozo flatten_hierarchy build_variables buildmodel compute_fairness because bozo was the second argument on the last command line typed In other words command substitution in a script file depends on how the script file was invoked Switches passed to a command are also counted as positional parameters Therefore if you type st x short smv bozo you will execute read model i short smv flatten_hierarchy build_variables build_model compute_fairness To pass the x switch or any other switch to source when the script uses posi tional parameters you may define an alias For instance alias srcx source x See the variable on_failure_script_quits for further information time Provides a simple CPU elapsed time value Command 104 time h Prints the processor time used since the last invocation of the t ime command and the total processor time used since NUSMV was started unalias Removes the definition of an
140. niques Starting from NUSMV2 we are also adopting a new development and license model NUSMV2 is distributed with an OpenSource licensd that allows anyone interested to freely use the tool and to participate in its development The aim of the NUSMV OpenSource project is to provide to the model checking community a common platform for the research the implementation and the comparison of new symbolic model checking techniques Since the release of NUSMV2 the NUSMV team has received code contributions for different parts of the system Several research institutes and commercial companies have expressed interest in collaborating to the development of NUSMV The main features of NUSMV are the following e Functionalities NUSMV allows for the representation of synchronous and asynchronous finite state system and for the analysis of specifications ex pressed in Computation Tree Logic CTL and Linear Temporal Logic LTL using BDD based and SAT based model checking techniques Heuristics are available for achieving efficiency and partially controlling the state explosion The interaction with the user can be carried on with a textual interface as well as in batch mode 1 see http www opensource org However asynchronous processes are deprecated in version 2 5 0 and later and may be no longer sup ported in future versions e Architecture A software architecture has been defined The different compo nents and functionalities of NU
141. nition of the FSM page Section State Variables page Sec tion Input Variables page 24 and Section eaten Variables page Bef Snes a symbolic constant is syntactically indistinguishable from variable_identifiers and define_identifiers a symbol table is used to distinguish them from each other Parentheses Parentheses may be used to group expressions The type of the whole expression is the same as the type of the expression in the parentheses Logical and Bitwise The signature of the logical and bitwise NOT operator is boolean boolean unsigned word N unsigned word N signed word N signed word N This means that the operation can be applied to boolean unsigned word e and signed word e operands The type of the whole expression is the same as the type of the operand If the operand is not boolean unsigned word e or signed word e then the expression violates the type system and NUSMV will throw an error Logical and Bitwise amp xor xnor gt lt gt Logical and bitwise binary operators amp AND OR xor exclusive OR xnor negated exclusive OR gt implies and lt gt if and only if are similar to the unary operator except that they take two operands Their signature is amp xor xnor gt lt gt boolean boolean boolean unsigned word N unsigned word N unsigned word N signed word N signed word N signed word N the op
142. ns 36 D DD package interface declarations 34 DEFINE array DEFINE declarations 26 defines definition of the FSM 22 Displaying Traces 90 E enumeration types 7 Execution Commands expressions 9 basic expressions 12 basic next case constants next sets simple extend operator F fair execution paths fairness BLE Ey fair paths frozen variables syntax 25 I identifiers 32 if then else expressions IFF logical and bitwise implicit type conversion IMPLIES logical and bitwise 14 Important Difference Between BDD and SAT Based LTL Model Checking inclusion operator 19 index subscript operator 17 infinity 40 INIT constraint Input File Syntax 45 input variables syntax 24 26 Inspecting Traces 89 integer type 7 interactive running NuSMV 48 interactive shell 48 interface to DD Package 95 INVAR constraint 28 Invariant Specifications INVARSPEC Specifications 37 ISA declarations 36 J justice constraints 30 K keywords 6 L LTL Specifications 38 M main module 34 master nusmvrc 110 model compiling model parsing model reading MODULE declarations 30 MODULE instantiations N namespaces next expressions 21 NOT logical and bitwise O operator mod 16 operators AND 14 arithmetic bit selection 17 cast count equality IFF 14 IMPLIES 14
143. ns see command clean_sexp2bdd_cache print_bdd_stats Prints out the BDD statistics and parameters Command print_bdd_stats h Prints the statistics for the BDD package The amount of information depends on the BDD package configuration established at compilation time The configurtion parameters are printed out too More information about statistics and parameters can be found in the documentation of the CUDD Decision Diagram package set_bdd_parameters Creates a table with the value of all cur Command rently active NuSMV flags and change accordingly the configurable parameters of the BDD package set_bdd_parameters h s Applies the variables table of the NUSMV environnement to the BDD package so the user can set specific BDD parameters to the given value This command works in con junction with the print_bdd_stats and set commands print _bdd_stats first prints a report of the parameters and statistics of the current bdd_manager By using the command set the user may modify the value of any of the parameters of the underlying BDD package The way to do it is by setting a value in the variable BDD parameter name where parameter name is the name of the parameter exactly as printed by the print_bdd_stats command Command Options s Prints the BDD parameter and statistics after the modification 3 10 Administration Commands This section describes the administrative commands offered by the interactive shell of NUSMV
144. nsigned word e integer toint signed word e integer Warning using the toint operator with word variables may cause bad performances of the system Performances may degrade with the increase of the number of bits of the word expression 21 Boolean conversion operator bool converts unsigned word 1 and integer expressions to boolean Also boolean expres sions are allowed but no action is perfomed In case of integer expression the result of the conversion is FALSE if the expression resolves to 0 TRUE otherwise In case of unsigned word 1 expression the conversion obeys the following table boo1 0ub1_0 FALSE bool Oub1_1 TRUE Integer to Word Constants Conversion swceonst uwconst convert an integer constant into a signed word e constant or unsigned word e constant of given size respectively The signature of these conversion operator is swceonst integer integer signed word e uwconst integer integer unsigned word e Where the left integer parameter is the value and the right integer parameter is the size in bits of the generated unsigned word e or signed word e constant Word1 Explicit Conversions word1 converts a boolean to a unsigned word 1 The signature of this conversion operator is word1 boolean unsigned word 1 The conversion obeys the following table word1 FALSE Oub1_0 word1 TRUE Oub1_1 Unsigned and Signed Explicit Conversions unsigned converts a sig
145. nsisting of just one state s FALSE violates the specification G s TRUE and is still consistent with the FSM as the transition relation is not taken ever and there is not initial condition to violate Note however that this state is a deadlock and cannot have consecutive states In order to make SAT based bound model checking ignore finite paths it is enough to add a fairness condition to the main module JUSTICE TRUE Being limited to fair paths SAT based bounded model checking cannot find a finite counter example and results of model checking become consistent with BDD based model checking 2 4 4 Real Time CTL Specifications and Computations NUSMV allows for Real Time CTL specifications EMSS91 NUSMV assumes that each transition takes unit time for execution RTCTL extends the syntax of CTL path expressions with the following bounded modalities rtctl_expr ctl_expr 39 EBF range rtctl_expr ABF range rtctl_expr EBG range rtctl_expr ABG range rtctl_expr A rtctl_expr BU range rtctl_expr E rtctl_expr BU range rtctl_expr range integer_number integer_number Given ranges must be non negative Intuitively the semantics of the RTCTL operators is as follows e EBF m n p requires that there exists a path starting from a state such that property p holds in a future time instant i with m lt i lt n e ABF m n prequires that for all paths starting from a state property p
146. nstants_declaration assign_constraint trans_constraint init_constraint invar_constraint fairness_constraint ctl_specification invar_specification ltl_specification compute_specification isa_declaration ISA Declaration isa_declaration ISA identifier Warning this is a deprecated feature and will eventually be removed from NUSMV Use module instances instead CTL Specification ctl_specification ctl_expr simple_expr ctl_expr E ctl_expr U ctl_expr A ctl_expr U ctl_expr ctl_expr ctl_expr amp ctl_expr ctl_expr ctl_expr 7 ctl_expr xor ctl_expr ctl_expr xnor ctl_expr ctl_expr gt ctl_expr ctl_expr lt gt ctl_expr EG ctl_expr EX ctl_expr 5 EF ctl_expr AG ctl_expr AX ctl_expr AF ctl_expr z INVAR Specification invar_specification This is equivalent to SPEC AG simple_expr SPEC ctl_expr a simp logical logical logica logica logical logica logica exists exists exists forall forall forall exists forall boolean expression not and or exclusive or NOT exclusive or implies equivalence globally next state finally globally next state finally until until INVARSPEC simple_expr but is checked by a specialised algorithm during reachability analysis 129 LTL Specification ltl_specification LTLSPEC 1tl_expr ltl_expr simple_expr a simple boolean expression ltl_expr ltl_expr lo
147. nts depend on one or more inputs the initial state does not contain this section either Traces are created by NUSMV when a formula is found to be false they are also generated as a result of a simulation Section Simulation Commands page or partial trace re execution Section 3 6 Execution Commands page 87 Each trace has a number and the states inputs pairs are numbered within the trace Trace n has states inputs n 1 n 2 n 3 where n 1 represents the initial state When Cone of Influence COD is enabled when generating a trace e g when performing model checking the generated trace will contain only the relevant symbols variables and DE FINEs which are in the COI projected by the variables occurring in the property which is being checked The symbols which are left out of the COI will be not visible in the generated trace as they do not occur in the problem encoded in the solving engine Notice that when COI is enabled the generated trace may or may not be a valid counter example trace for the original model 3 7 1 Inspecting Traces The trace inspection commands of NUSMV allow for navigation along the labelled states inputs pairs of the traces produced During the navigation there is a current state and the current trace is the trace the current state belongs to The commands are the following goto_state Goes to a given state of a trace Command goto_state h state_label Makes state_l
148. ny position build_model Compiles the flattened hierarchy into a BDD Command buildmodel h f m Method 53 Compiles the flattened hierarchy into a BDD initial states invariants and transition relation using the method specified in the environment variable part ition_method for building the transition relation Command Options m Method Sets the environment variable partition_method to the value Method and then builds the transition relation Available methods are Monolithic Threshold and Iwls95CP E Forces model construction By default only one partition method is allowed This option allows to overcome this de fault and to build the transition relation with different parti tioning methods partition method Environment Variable The method to be used in building the transition relation and to compute images and preimages Possible values are e Monolithic No partitioning at all e Threshold Conjunctive partitioning with a simple threshold heuristic Assign ments are collected in a single cluster until its size grows over the value specified in the variable conj part threshold It is possible default to use affinity clustering to improve model checking performance See affinity variable e 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_
149. o 2 that are 5 bit long unsigned words Array subtype is the immediate subtype of an array type For example subtype of array 1 8 of array 1 2 of unsigned word 5 is array 1 2 of unsigned word 5 which has its own subtype unsigned word 5 array types are incompatible with set type i e array elements cannot be of set type Expression of array type can be constructed with array DEFINE see 2 3 3 or variables of array type see 2 3 1 2 1 6 Set Types set types are used to identify expressions representing a set of values There are four set types boolean set integer set symbolic set integers and symbolic set The set types can be used in a very limited number of ways In particular a variable cannot be of a set type Only range constant and union operator can be used to create an expression of a set type and only in case e e and assignmenf expressions can have imediate operands of a set type Every set type has a counterpart among other types In particular the counterpart of a boolean set type is boolean the counterpart of a integer set type is integer the counterpart of a symbolic set type is symbolic enum the counterpart of a integers and symbolic set type is integers and symbolic enum Some types such as unsigned word e and signed word e do not have a set type counterpart 2 1 7 Type Order Figure 2 I depicts the order existing between types in NUSMV unsigned word 1 integer symbolic enum bo
150. of modulo operator can be obtained from the remainder operator by exploit ing the equivalence n modulo M n mod M M mod M Where mod is the remainder operator Shift Operators lt lt gt gt The signature of the shift operators is lt lt gt gt unsigned word N integer unsigned word N signed word N integer signed word N unsigned word N unsigned word M unsigned word N signed word N unsigned word M signed word N Before checking the expression for being correctly typed the right operand can be implicitly converted from boolean to integer type Left shift lt lt right shift gt gt operation shifts to the left right the bits of the left operand by the number specified in the right operand A shift by N bits is equivalent to N shifts by 1 bit A bit shifted behind the word bound is lost During shifting a word is padded with zeros with the exception of the right shift for signed word e in which case a word is padded with its highest bit For instance 16 OQub4_0101 lt lt 2 is equal to Osb3_1011 gt gt 2 is equal to Oub4_0100 lt lt 1 is equal to Osb3_1110 gt gt 1 is equal to Oub4_1000 lt lt 0 is equal to Osb3_1111 gt gt 0 is equal to Oub4_1000 and Osb3_1111 It has to be remarked that the shifting requires the right operand to be greater or equal to zero and less then or equal to the width of the word it is applied to NUSMV raises an error if a shift
151. of the number Any in valid combination of length and loopback will be skipped during the generation solving process e a negative number in 1 bmc_length In this case loop back is considered a value relative to max_length Any in valid combination of length and loopback will be skipped during the generation solving process 84 e the symbol X which means no loopback e the symbol which means all possible loopbacks from zero to length 1 If no value is given the environment vari able bmc_loopback is considered instead 3 5 Simulation Commands In this section we describe the commands that allow to simulate a NUSMV specification See also the section SectionB 7 Traces page 89 that describes the commands available for manip ulating traces pick_state Picks a state from the set of initial states Command pick_state h trace state r i a e constraints s Chooses an element from the set of initial states and makes it the current state replacing the old one The chosen state is stored as the first state of a new trace ready to be lengthened by steps states by the simulate command The state can be chosen according to different policies which can be specified via command line options By default the state is chosen in a deterministic way Command Options mi i c constraints s trace stat Verbosely prints out chosen state all state and frozen vari
152. olean l P integers and symbolic enum unsigned word 3 unsigned word 2 signed word 1 integer set symbolic set signed word 2 boolean set I l integers and symbolic set signed word 3 array N1 M1 of subtypel N1 N2 subtypel i M1 M2 and l array N2 M2 of subtype2 en at subtype2 Figure 2 1 The ordering on the types in NUSMV It means for example that integer is less than integers and symbolic enum symbolic enum is less than integers and symbolic enum etc The unsigned word e and signed word e any other type or between each other Any type is equal to itself Note that enumerations containing only integer numbers have the type integer For 2 arrays types array N1 M1 of subtypel and array N2 M2 of subtype2 the first type is less then the second one if and only if N1 N2 M1 M2 and type subtype is less than subtype2 2 2 Expressions The previous versions of NuSMV prior to 2 4 0 did not have the type system and as such ex pressions were untyped In the current version all expressions are typed and there are constraints on the type of operands Therefore an expression may now potentially violate the type system i e be erroneous For more information on these operators see pages 12 18 19 19 ana respectively To maintain backward compatibility there is a new system variable called backward_compatibility and a correponding old command line option that disables a few new features of version 2 4 to keep backwa
153. omplete_Var_Name i at the position where you want that bit variable to appear Complete_Var_Name Complete_Var_Name i The result of doing this is that the variable representing the it bit is located in a different position to the remainder of the variables representing the rest of the bits The specific bit variables varname 0 varname i 1 varname i 1 varname N are grouped together as before If any one bit occurs before the variable it belongs to the remaining specific bit variables are not grouped together Complete _Var_Name i Complete_Var_Name The variable representing the it bit is located at the position given in the variable ordering and the remainder are located where the scalar variable name is declared In this case the remaining bit variables will not be grouped together This is just a short hand way of writing each individual specific bit variable in the ordering file The following are equivalent Complete_Var_Name 0 Complete_Var_Name 0 Complete_Var_Name 1 Complete_Var_Name Complete_Var_Name N 1 where the scalar variable Complet e_Var_Name requires N boolean variables to encode all the possible values that it may take It is still possible to then specify other specific bit variables at later points in the ordering file as before 2 5 3 Array Variables When declaring array variables in the ordering file each individual element must be specified separately It is not permitted to specify just the
154. on 2 2 4 Simple and Next Expressions page 21 It is an error if the number of actual parameters is different from the number of formal parameters Whenever formal parameters occur in expressions within the module they are replaced by the actual parameters The semantic of module instantiation is 31 similar to call by reference Here are examples MODULE main VAR a boolean b foole MODULE foo x ASSIGN x TRUE the variable a is assigned the value TRUE This distinguishes the call by reference mechanism from a call by value scheme Now consider the following program MODULE main DEFINE b bar a MODULE bar x DEFINE a 1 y i x In this program the value of y is 0 On the other hand using a call by name mechanism the value of y would be 1 since a would be substituted as an expression for x Forward references to module names are allowed but circular references are not and result in an error The keyword process is explained in Section 2 3 13 Processes page 33 2 3 12 References to Module Components Variables and Defines As described in Section Variables and Defines page defines and variables can be referenced in expressions as variable_identifiers and define_identifiers respectively both of which are complex identifiers The syntax of a complex identifier is complex_identifier identifier complex_identifier identif
155. on of quantitative characteristics of real time sys tems Itis able to compute the length of the shortest longest path from two given set of states MAX alpha beta MIN alpha beta eal Properties of the above form can be specified in the input file via the keyword COMPUT or directly at command line using option p If there exists an infinite path beginning in a state in start that never reaches a state in final then infinity is returned If any of the initial or final states is empty then undefined is returned Option n can be used for computing a particular expression in the model If neither n nor p are used all the COMPUTE specifications are computed It is important to remark here that if the FSM is not total i e it contains deadlock states COMPUTE may produce wrong results It is possible to check the FSM against deadlock states by calling the command check_fsm See variable use_coi_size_sorting for changing properties verification order 64 Command Options m Pipes the output generated by the command in process ing COMPUTEs to the program specified by the PAGER shell variable if defined else through the UNIX command more o output file Writes the output generated by the command in processing COMPUTES to the file output file p compute expr IM COMPUTE formula to be checked context context is the module instance name which the variables in compute expr must be evaluated in
156. or example 0sb7_1011001 4 1 extracts bits 1 through 4 including Ist and 4th bits and is equal to Qub4_1100 Oub3_101 0 0 extracts bit number 0 and is equal to Oub1_1 The signature of the bit selection operator is unsigned word N integer integer unsigned word integer integer 1 signed word N integer integer unsigned word integer integer 1 where 0 lt integer lt integer lt N Word Concatenation Operator The concatenation operator joins two words unsigned word e or signed word e or both together to create a larger unsigned word e type The operator itself is two colons and its signature is as follows word M word N unsigned word M N See for array defines and for array variables 17 where word N is unsigned word N or signed word N The left hand operand will make up the upper bits of the new word and the right hand operand will make up the lower bits The result is always unsigned word e For example given the two words w1 Oub4_1101 andw2 Osb2_00 the result of w1 w2 is Oub6_110100 Word sizeof Operator sizeof operator provides a very simple way for retrieving the width of a word The behavior of this operator can be described as follows let w be a word N sizeof w returns N The signature of the operator is sizeof unsigned word e integer signed word e integer Extend Word Conversions extend o
157. orial loop Indeed there is no fixed order in which we can compute x and y since at each time instant the value of x depends on the value of y and vice versa We can introduce a unit delay dependency using the next operator x i yi next y X In this case there is a unit delay dependency between x and y A combinatorial loop is a cycle of dependencies whose total delay is zero In NUSMV combinatorial loops are illegal This guarantees that for any set of equations describing the behavior of variable there is at least one solution There might be multiple solutions in the case of unassigned variables or in the case of non deterministic assignments such as in the following example next x case x 1 TRUE 0 1 esac 2 3 9 FAIRNESS Constraints A fairness constraint restricts the attention only to fair execution paths When evaluating speci fications the model checker considers path quantifiers to apply only to fair paths NUSMV supports two types of fairness constraints namely justice constraints and com passion constraints A justice constraint consists of a formula f which is assumed to be true infinitely often in all the fair paths In NUSMYV justice constraints are identified by keywords JUSTICE and for backward compatibility FAIRNESS A compassion constraint consists of a pair of formulas p q if property p is true infinitely often in a fair path then also formula q has to be true infinitely often i
158. owing to identify purely boolean i e not temporal expressions The class of PSL properties psl_property is defined as follows psl_property replicator psl_expr a replicated property FL_property abort psl_bexpr psl_expr lt gt psl_expr psl_expr gt psl_expr FL property OBE_property replicator forall var_id index_range in value_set index_range range range low_bound high_bound low_bound number identifier high_bound number identifier inf inifite high bound value_set value_range value_range boolean value_range psl_expr range The instances of FL property are temporal properties built using LTL operators and SEREs operators and are defined as follows FL property 42 E r PRIMITIVE LTL OPERATORS X FL_property X FL_property F FL_property G FL_property F L_property U FL_property FL_property W FL_property SIMPLE TEMPORAL OPERATORS always FL_property never FL_ property next FL property next FL_property eventually FL_property L_ property until FL_property L_ property until FL_property L property until FL_property L_ property until_ FL_property L_ property before FL_property L_ property before FL_property L_property before FL_property L_ property before_ FL_property EXTENDED NEXT OPERATORS X number FL_property X number FL_property next number FL_property next number FL_property
159. perator increases the width of a word by attaching additional bits on the left If the provided word is unsigned then zeros are added otherwise if the word is signed the highest sing bit is repeated corresponding number of times The signature of the operator is extend unsigned word N integer unsigned word N integer signed word N integer signed word N integer For example extend 0ub3_101 2 Oub5_00101 extend 0sb3_101 2 Osb5_11101 extend 0sb3_011 2 Osb5_00011 Note that the right operand of extend has to be an integer constant greater or equal to zero Resize Word Conversions resize operator provides a more comfortable way of changing the width of a word The behavior of this operator can be described as follows let w be a M bits unsigned word e and N be the required width if M N w is returned unmodified if N is less than M bits in the range N 1 0 are extracted from w if N is greater than M w is extended of N M bits up to required width padding with zeroes let w be aM bits signed word e and N be the required width if M N w is returned unmodified if N is less than M bits in the range N 2 0 are extracted from w while N 1 ith bit is forced to preserve the value of the original sign bit of w M 1 ith bit if N is greater than M w is extended of N M bits up to required width extending sign bit The signature of the operator is resize unsigned word e integer unsig
160. plugin prints out the trace as a table either with the states on each row or in each column The entries along the state axis are SL C25 T2 S2 ato Ch ln Sn where S1 is the initial state and J gives the values of the input variables which caused the transition from state S _1 to state S C gives the values of any combinatorial constants where the value depends on the values of the state or frozen variables in state S _1 and the values of input variables in state S The variables in the model are placed along the other axis Only the values of state and frozen variables are displayed in the State row column only the values of input variables are displayed in the Input row column and only the values of combinatorial constants are displayed in the Constants row column All remaining cells have displayed 3 8 3 XML Format Printer This plugin prints out the trace either to stdout or to a specified file using the command show_traces If traces are to be output to a file with the intention of them being loaded again at a later date then each trace must be saved in a separate file This is because the XML Reader plugin does not currently support multiple traces per file The format of a dumped XML trace file is as follows lt XML_VERSION_STRING gt lt counter example type TRACE_TYPE desc TRACE_DESC gt x for each state i x lt node gt lt state id i gt x for each state and frozen var
161. ply discarded Variables declared in the model which are not listed in the ordering input file will be created and appended at the end of the given ordering list according to the default ordering Command Options i order file Sets the environment variable input_order_file to 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 51 input_order file Environment Variable Indicates the file name containing the variable ordering to be used in building the model by the encode_variables command A value for this variable can also be provided with command line option i There is no default value write_order_dumps_bits Environment Variable Changes the behaviour of the command write_order When this variable is set write_order will dump the bits constituting the boolean en coding of each scalar variable instead of the scalar variable itself This helps to work at bits level in the variable ordering file See the command write_order for further information The default value is 1 write_order Writes variable order to file Command write_order h b o fy order file Writes the current order of BDD variables in the file specified via the o option If no option is specified the environment variable out put order_file wil
162. presented when showing traces can be controlled by variables traces_hiding_prefix and traces_regexp counter_examples Environment Variable This determines whether traces are generated when needed See also command line option dcx traces_hiding_prefix Environment Variable Symbols names that match this string prefix will be not printed out when showing a trace This variable may be used to avoid displaying symbols that are expected to be not visible to the user For example this variable is exploited when dumping booleanized models as NUSMV may introduce hidden placeholding symbols as DEFINES that do not carry any useful information for the user and that would make traces hardly readable if printed Default is __ traces_regexp Environment Variable Only symbols whose names match this regular expression will be printed out when show ing a trace This option might be used by users that are interested in showing only some symbol names Names are first filtered out by applying matching of the dual vari able traces_hiding prefix and then filtered names are checked against content of traces_regexp Given regular expression can be a Posix Basic Regular Expression Matching is carried out on symbol names without any contextual information like module hierarchy For example in m1 m2 name only name is checked for filtering Notice that depending on the underlaying platform and operating system this variable might be not av
163. pringer 2000 A Biere A Cimatti E Clarke and Y Zhu Symbolic model checking without bdds In Tools and Algorithms for Construction and Analysis of Systems In TACAS 99 March 1999 J R Burch E M Clarke D E Long K L McMillan and D L Dill Sym bolic model checking for sequential circuit verification In JEEE Trans actions on Computer Aided Design of Integrated Circuits and Systems 13 4 401 424 April 1994 O Coudert C Berthet and J C Madre Verification of synchronous se quential machines based on symbolic execution In In J Sifakis editor Proceedings of the International Workshop on Automatic Verification Meth ods for Finite State Systems volume 407 of LNCS pages 365 373 Berlin June 1990 A Cimatti E Clarke E Giunchiglia F Giunchiglia M Pistore M Roveri R Sebastiani and A Tacchella Nusmv 2 An opensource tool for symbolic model checking In Proceedings of Computer Aided Verification CAV 02 2002 A Cimatti E Clarke F Giunchiglia and M Roveri Nusmv a new sym bolic model checker In International Journal on Software Tools for Tech nology Transfer STTT 2 4 March 2000 E Clarke O Grumberg and K Hamaguchi Another look at ltl model checking In Formal Methods in System Design 10 1 57 71 February 1997 D Dill Trace theory for automatic hierarchical verification of speed independent circuits In ACM Distinguished Dissertations MIT Press 1988 E Emerson and
164. print_bdd_stats foo creates an alias which refers to itself Executing the command foo will result an infinite loop during which the command print_bdd_stats will be executed echo Merely echoes the arguments Command cho h 2 n o filename a lt string gt Echoes the specified string either to standard output or to filename if the option o is specified Command Options 2 Redirects output to the standard error instead of the standard output This cannot be used in combination with the option n Does not output the trailing newline 0o filename Echoes to the specified filename instead of to standard out put If the option a is not specified the file filename will be overwritten if it already exists a Appends the output to the file specified by option o in stead of overwritting it Use only with the option o 100 help Provides on line information on commands Command help a h lt command gt If invoked with no arguments he 1p prints the list of all commands known to the command interpreter If a command name is given detailed information for that command will be provided Command Options a Provides a list of all internal commands whose names begin with the underscore character _ by convention history list previous commands and their event numbers Command history h lt num gt Lists previous commands and their event numbers This is
165. put state and frozen variables are ordered as they are declared in the input smv file e lexicographic This is deprecated value topological has to be used instead bdd_static_order_heuristics Environment Variable When a variable ordering is not specified see variable input_order_fileon page 52 NUSMV can try to guess a good ordering by analyzing the input model Possible values are e none No heuristics are applied e basic This heuristics creates some initial ordering and then moves scalar and word variables in this ordering to form groups Groups go one after another and every group contains variables which interact with each other in the model For example having variables a b c d e f and a single model constraint TRANS next a b 1 gt next c d e amp next f a will results in 2 groups of variables a b f and c d e Shell variable vars_order_type page 53 provides additional control over the heuristics In particular it allows to put input state variables in the initial ordering at the begin the end or in topological order Moreover if the value of this variable is ending in _bi then in very individual group the bits of variables are additionally interleaved Note that variable groups created by the heuristics has nothing to do with BDD package groups which disallow dynamic reordering of variables in one group After the heuristics is applied the dynamic reordering may move any bit of any variable at a
166. r basic_expr set_body_expr basic_expr Enumerating values in curly brackets is semantically equivalent to writing them connected by union operators For example expression exp1 exp2 exp3 is equivalent to exp1 union exp2 union exp3 Note that according to the semantics of union operator ex pression 1 2 3 4 isequivalentto 1 2 3 4 i e there is no actually set of sets Set expressions can be used only as operands of union and in operations as the right operand of case and as the second and the third operand of e e e expressions and assignments In all other places the use of set expressions is prohibited Inclusion Operator in The inclusion operator in tests the left operand for being a subset of the right operand If either operand is a number or a symbolic value instead of a set it is coerced to a singleton set The signature of the in operator is in boolean set boolean set boolean integer set integer set boolean symbolic set symbolic set boolean integers and symbolic set integers and symbolic set boolean Similar to union operation before checking the expression for being correctly typed if it is possible both operands are converted to their counterpart set types Then if required implicit type conversion is carried out on one of the operands Case Expressions A case expression has the following syntax case_expr case case_body esac case_body 3See 2
167. r instance it is not possible to evaluate CTL expressions before the model is built A number of commands and environment variables like those dealing with file names accept arbitrary strings There are a few reserved characters which must be escaped if they are to be used literally in such situations See the section describing the history command on page I01 for more information The verbosity of NUSMV is controlled by the following environment variable verbose level Environment Variable Controls the verbosity of the system Possible values are integers from 0 no messages to 4 full messages The default value is 0 3 1 Model Reading and Building The following commands allow for the parsing and compilation of the model into a BDD read_model Reads a NuSMV file into NuSMV 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 Command Options i model file Sets the environment variable input_ file to model file and reads the model from the specified file input_file Environment Variable 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 pp_list Environment Variable Stores the list of pre processors to be run on the input file before it is parsed by NUSMV The pre proces
168. r number The type of arange constant is integer set 2 2 3 Basic Expressions A basic expression is the most common kind of expression used in NUSMV basic_expr constant 4 Constant variable_identifier a variable identifier define_identifier a define identifier basic_expr basic_expr logical or bitwise NOT basic_expr amp basic_expr logical or bitwise AND basic_expr basic_expr logical or bitwise OR basic_expr xor basic_expr logical or bitwise exclusive OR basic_expr xnor basic_expr logical or bitwise NOT exclusive OR basic_expr gt basic_expr logical or bitwise implication basic_expr lt gt basic_expr logical or bitwise equivalence basic_expr basic_expr equality basic_expr basic_expr inequality basic_expr lt basic_expr less than basic_expr gt basic_expr greater than basic_expr lt basic_expr less than or equal basic_expr gt basic_expr greater than or equal basic_expr integer unary minus basic_expr basic_expr integer addition basic_expr basic_expr integer subtraction basic_expr basic_expr integer multiplication basic_expr basic_expr integer division basic_expr mod basic_expr integer remainder basic_expr gt gt basic_expr bit shift right basic_expr lt lt basic_expr bit shift left basic_expr index index subscript basic_expr basic_expr basic_expr word bits selection b
169. r of the property a progressive number e the property name if available e the property formula e the type CTL LTL INVAR PSL COMPUTE e the status of the formula Unchecked True False or the result of the quantitative expression if any it can be infinite e if the formula has been found to be false the index number of the corresponding counterexample trace By default all the properties currently stored in the list of properties are shown Specifying the suitable options properties with a certain status Unchecked True False and or of a certain type e g CTL LTL or with a given identifier it is possible to let the system show a restricted set of properties It is allowed to insert only one option per status and one option per type Command Options P name Prints out the property named name n idx Prints out the property numbered idx Prints only CTL properties I Prints only LTL properties i Prints only INVAR properties q Prints only COMPUTE properties u Prints only unchecked properties t Prints only those properties found to be true f Prints only those properties found to be false 66 s Prints the number of stored properties o filename Writes the output generated by the command to filename F format Prints with the specified format tabular and xml are com mon formats however use F help to see all available formats m Pipes the output through the program specified by th
170. rated NUSMV internally calls a propositional SAT solver in order to find an assignment which satisfies the problem Currently NUSMV supplies two SAT solvers Zchaff and MiniSat If none of the two is enabled all Bounded Model Checking part in NUSMV will not be available Notice that Zchaff and MiniSat are for non commercial purposes only They are therefore not included in the source code distribution or in some of the binary distributions of NUSMV Some commands for Bounded Model Checking use incremental algorithms These algo rithms exploit the fact that satisfiability problems generated for a particular bounded model checking problem often share common subparts So information obtained during solving of one satisfiability problem can be used in solving of another one The incremental algorithms usually run quicker then non incremental ones but require a SAT solver with incremental inter face At the moment only Zchaff and MiniSat offer such an interface If none of these solvers are linked to NUSMV then the commands which make use of the incremental algorithms will not be available It is also possible to generate the satisfiability problem without calling the SAT solver Each generated problem is dumped in DIMACS format to a file DIMACS is the standard format used as input by most SAT solvers so it is possible to use NUSMV with a separate external SAT solver At the moment the DIMACS files can be generated only by commands which do not use incr
171. rd compatibility with old version of NuUSMV In particular if this system variable is set then type violations caused by expressions of old types i e enumeration type boolean and integer will be ignored by the type checker instead warnings will be printed out See description at page 50 for further information If additionally the system variable type_checking_warning_on is unset then even these warnings will not be printed out 2 2 1 Implicit Type Conversion In some expressions operands may be converted from one type to its set type counterpart see 2 1 6 For example integer can be converted to integer set type Note Prior to version 2 5 1 implicit type conversion from integer to boolean and vicev ersa was performed Since version 2 5 1 implicit integer boolean type conversion is no longer supported and explicit cast operators have to be used 2 2 2 Constant Expressions A constant can be a boolean integer symbolic word or range constant constant boolean_constant integer_constant symbolic_constant word_constant rvange_constant Boolean Constant A boolean constant is one of the symbolic values FALSE and TRUE The type of a boolean constant is boolean boolean_constant one of FALSE TRUE Integer Constant An integer constant isan integer number The type of an integer constant is integer integer_constant integer_number Symbolic Constant A symbolic constant is syntactically an identif
172. re than one INIT constraint the initial set is the conjunction of all of the INIT constraints 2 3 6 INVAR Constraint The set of invariant states can be specified using a boolean expression under the INVAR key word The syntax of an INVAR constraint is invar_constraint INVAR simple_expr Since the expression in the INVAR constraint is a simple_expression it cannot contain the next operator If there is more than one INVAR constraint the invariant set is the conjunction of all of the INVAR constraints 2 3 7 TRANS Constraint The transition relation of the model is a set of current state next state pairs Whether or not a given pair is in this set is determined by a boolean expression introduced by the TRANS keyword The syntax of a TRANS constraint is trans_constraint TRANS next_expr It is an error for the expression to be not of the boolean type If there is more than one TRANS constraint the transition relation is the conjunction of all of TRANS constraints 2 3 8 ASSIGN Constraint An assignment has the form assign_constraint ASSIGN assign_list assign_list assign assign_list assign assign complex_identifier init complex_identifier next complex_identifier simple_expr simple_expr next_expr On the left hand side of the assignment identifier denotes the current value of a vari able init identifier denotes its initial value and next identifier denotes
173. reatment of past temporal operators Note that the counterexample is generated in such a way to show that the falsity of a LTL specification may contain state variables which have been introduced by the tableau construction procedure In the case of SAT based reasoning a similar tableau construction is carried out to encode the paths of limited length violating the property NUSMV generates a propositional satisfiability problem that is then tackled by means of an efficient SAT solver BCCZ99 In both cases the tableau constructions are completely transparent to the user Important Difference Between BDD and SAT Based LTL Model Checking If a FSM to be checked it not total i e has deadlock state the model checking may return different results for the same LTL specification depending on the verification engine used For example for below model MODULE main VAR s boolean TRANS s TRUE TLSPEC G s TRUE the LTL specification is proved valid by BDD based model checking but is violated by SAT based bounded model checking The counter example found consists of one state s FALSE This difference between the results is caused by the fact that BDD model checking investi gates only infinite paths whereas SAT based model checking is able to deal also with finite paths Apparently infinite paths cannot ever have s FALSE as then the transition relation will not hold between the consecutive states in the path A finite path co
174. reduction is active the problem encoded in the solving engine consists only of the relevant parts of the model for the property being checked This can greatly help in reducing solving time and memory usage Note however that a COI counter example trace may or may not be a valid counter example trace for the original model use_coi_size_sorting Environment Variable Uses the cone of influence variables set size for properties sorting before the verification step If set to 1 properties are verified starting with the one that has the smallest COI set ending with the property with the biggest COI set If set to 0 properties are verified according to the declaration order in the input file 67 prop_print_method Environment Variable Determines how properties are printed The following methods are available name Prints the property name If not available defaults to method index index Prints the property index If not available defaults to method truncated truncated Prints the formula of the property If the formula is longer than 40 characters it is truncated formula The default method simply prints the formula 3 3 Commands for Bounded Model Checking In this section we describe in detail the commands for doing and controlling Bounded Model Checking in NUSMV Bounded Model Checking is based on the reduction of the bounded model checking problem to a propositional satisfiability problem After the problem is gen e
175. rt e k current problem bound e I current loopback value e n index of the currently processed formula in the prop erty database e the character bmc_length Environment Variable Sets the generated problem bound Possible values are any natural number but must be compatible with the current value held by the variable bmc_loopback The default value is WO bmc_loopback Environment Variable Sets the generated problem loop Possible values are e Any natural number but less than the current value of the variable bmc_length In this case the loop point is absolute e Any negative number but greater than or equal to bmc _length In this case specified loop is the loop length e The symbol X which means no loopback e The symbol which means any possible loopbacks The default value is bmc_optimized_tableau Environment Variable Uses depth optimization for LTL Tableau construction in BMC bmc_force_pltl_tableau Environment Variable Forces to use PLTL instead of LTL for BMC tableau construction bmc_dimacs_filename Environment Variable This is the default file name used when generating DIMACS problem dumps This variable may be taken into account by all commands which belong to the gen_Itlspec_bmc family DIMACS file name can contain special symbols which will be expanded to represent the actual file name Possible symbols are 77 e F The curr
176. run the simulation in three ways according to different command line policies deterministic the default mode random and interactive The resulting sequence is stored in a trace indexed with an integer number taking into account the total number of traces stored in the system There is a different behavior in the way traces are built according to how current state is set current state is always put at the beginning of a new trace so it will contain at most steps 1 states except when it is the last state of an existent old trace In this case the old trace is lengthened by at most steps states Command Options P Prints current generated trace only those variables whose value changed from the previous state Verbosely prints current generated trace changed and un changed state and frozen variables Picks a state from a set of possible future states in a random way Enables the user to interactively choose every state of the trace step by step If the number of possible states is too high then the user has to specify some constraints as simple expression These constraints are used only for a single sim ulation step and are forgotten in the following ones They are to be intended in an opposite way with respect to those constraints eventually entered with the pick_state com mand or during an interactive simulation session when the number of future states to be displayed is too high that are local only to a single
177. s is not specified variable bmc_dimacs_filename will be considered The file name string may contain spe cial symbols which will be macro expanded to form the real file name Possible symbols are e F model name with path part e f model name without path part e k current problem bound e I1 current loopback value e n index of the currently processed formula in the prop erty database e the character check_Itlspec_bme_ine Checks the given LTL specification or all Command LTL specifications if no formula is given using an incremental al gorithm Checking parameters are the maximum length and the loopback value check_ltlspec_bmc_inc h n idx p formula IN context P name k max_length 1 loopback For each problem this command incrementally generates many satisfiability subproblems and calls the SAT solver on each one of them The incremental algorithm exploits the fact that subproblems have common subparts so information obtained during a previous call to the SAT solver can be used in the consecutive ones Logically this command does the same thing as check_1t1lspec_bmc see the description on page 69 but usually runs considerably quicker A SAT solver with an incremental interface is required by this command therefore if no such SAT solver is provided then this command will be unavailable See variable use_coi_size_sorting for changing properties verification order 73 Co
178. s the algebraic remainder of the division If the value of the second operand is zero the behavior is undefined and an error is thrown by NUSMV The signature of the remainder operator is mod integer integer integer unsigned word N unsigned word N unsigned word N signed word N signed word N signed word N The semantics of mod operator is equivalent to the corresponding operator of C C lan guages Thus if the quotient a b is representable the expression a b b a mod b shall equal a Note in older versions of NUSMV priori 2 4 0 the semantics of quotient and remainder were different Having the division and remainder operators and mod be of the current i e C C s semantics the older semantics of division was given by the formula IF a mod b lt 0 THEN a b 1 ELSE a b and the semantics of remainder operator was given by the formula IF a mod b lt 0 THEN a mod b b ELSE a mod b Note that in both versions the equation a b b a mod b a holds For example in the current version of NuSMV the following holds 7 5 1 7 mod 5 2 7 5 7 mod 5 2 7 5 1 7 mod 5 2 7 5 1 7 mod 5 2 whereas in the older versions on NuSMV the equations were 7 5 1 7 mod 5 2 7 5 2 7mod5 3 7 5 1 7 mod 5 2 7 5 0 7 mod 5 7 When supplied the command line option old_div_op switches the semantics of division and remainder to the old one Note semantics
179. sa_declaration is as follows isa_declaration ISA identifier where identifier must be the name of a declared module The ISA_declaration can be thought as a simple macro expansion command because the body of the module referenced by an ISA command is replaced to the ISA declaration Warning ISA is a deprecated feature and will be removed from future versions of NuSMV Therefore avoid the use of ISA_declarations Use module instances instead 2 4 Specifications The specifications to be checked on the FSM can be expressed in temporal logics like Compu tation Tree Logic CTL Linear Temporal Logic LTL extended with Past Operators and Property Specification Language PSL that includes CTL and LTL with Sequencial Extended Regular Expressions SERE a variant of classical regular expressions It is also possible to an alyze quantitative characteristics of the FSM by specifying real time CTL specifications Spec ifications can be positioned within modules in which case they are preprocessed to rename the variables according to their context CTL and LTL specifications are evaluated by NUSMV in order to determine their truth or falsity in the FSM When a specification is discovered to be false NUSMV constructs and prints a counterexample i e a trace of the FSM that falsifies the property 2 4 1 CTL Specifications A CTL specification is given as a formula in the temporal logic CTL introduced by the keyword CTLSPEC however depre
180. sed Default SAT solver is MiniSat Depending on the NUSMV configuration also the Zchaff SAT solver can be available or not Notice that Zchaff and MiniSat are for non commercial purposes only If no SAT solver has been configured BMC commands and environment variables will not be available bmc_pick state Picks a state from the set of initial states Command bmc_pick_state Fr h Ivi c constraint s trace state Chooses an element from the set of initial states and makes it the current state replacing the old one The chosen state is stored as the rst state of a new trace ready to be lengthened by steps states by the bmc_simulate command or the bmc_inc_simulate command Command Options v c constraint Verbosely prints the generated trace Set a constraint to narrow initial states s state Picks state from trace state label E Randomly picks a state from the set of initial states bmc_simulate Generates a trace of the model from 0 zero to k Command bmc_simulate constraints Command Options c constraint h p v r c constraints t k steps bmc_simulate does not require a specification to build the problem because only the model is used to build it The problem length is represented by the k command parameter or by its default value stored in the environment variable bmc_length Prints the generated trace only changed variables Prints the
181. signments For example all these assignments are not allowed IVAR i boolean ASSIGN init i TRUE next i FALSE e INIT statements For example IVAR i boolean VAR s boolean INIT i s e Scope of next expressions For example IVAR i boolean VAR s boolean TRANS i gt s this is allowed TRANS next i gt s this is NOT allowed 24 e Some specification kinds CTLSPEC SPEC INVARSPEC COMPUTE PSLSPEC For example IVAR i boolean VAR s boolean SPEC AF i gt s this is NOT allowed LTLSPEC F X i gt s this is allowed e Anywhere in the FSM when checking invariants with BMC and the DUAL algorithm See at page 80 for further information Frozen Variables FROZENVAR s frozen variables are variables that retain their initial value throughout the evo lution of the state machine this initial value can be constrained in the same ways as for normal state variables Similar to input variables the difference between the syntax for the frozen and state variables declarations is the keyword indicating the beginning of a declaration frozenvar_declaration FROZENVAR simple _var_list The semantics of some frozen variable a is that of a state variable accompanied by an assignment that keeps its value constant it is handled more efficiently though ASSIGN next a a As a consequence frozen variables may not have their current
182. sors are executed in the order specified by this variable The argument must either be the empty string specifying that no pre processors are to be run on the input file one single pre processor name or a space seperated list of pre processor names inside double quotes Any invalid names are ignored The default is none flatten_hierarchy Flattens the hierarchy of modules Command flatten_hierarchy h d 49 This command is responsible of the instantiation of modules and processes The instantia tion is performed by substituting the actual parameters for the formal parameters and then by prefixing the result via the instance name Command Options q Delays the construction of vars constraints until needed disable_syntactic_checks Environment Variable Enables or disables the syntactic checks that are performed by the flatten_hierarchy com mand Warning If the model is not well formed NUSMV may result in unpredictable results use this option at your own risk keep _single_value_vars Environment Variable Enables or disables the conversion of variables that can assume only one single possible value into constant DEFINEs backward_compatibility Environment Variable It is used to enable or disable type checking and other features provided by NuSMV 2 5 If set to 1 then the type checking is turned off and NUSMV behaves as the old versions w r t type checking and other features like writing of flattened a
183. step of the simulation and are forgotten in the next one To improve readability of the list of the states which the user must pick one from each state is presented in terms of dif ference with respect of the previous one 86 a Displays all the state and frozen variables changed and un changed during every step of an interactive session This option works only if the i option has been specified c constraints Performs a simulation in which computation is restricted to states satisfying those constraints The desired se quence of states could not exist if such constraints were too strong or it may happen that at some point of the simulation a future state satisfying those constraints doesn t exist in that case a trace with a number of states less than steps trace is obtained Note constraints must be enclosed between double quotes The expression cannot contain next operators and is automatically shifted by one state in order to constraint only the next steps t constraints Performs a simulation in which computation is restricted to states satisfying those constraints The desired se quence of states could not exist if such constraints were too strong or it may happen that at some point of the simulation a future state satisfying those constraints doesn t exist in that case a trace with a number of states less than steps trace is obtained Note constraints must be enclosed between double quotes The expression
184. t parameter_list simple_expr parameter_list simple_expr State Input and Frozen Variables var_declaration VAR var_list ivar_declaration IVAR simple_var_list frozenvar_declaration FROZENVAR simple _var_list var_list identifier type_specifier var_list identifier type_specifier 127 simple_var_list identifier simple_type_specifier simple_var_list identifier simple_type_specifier DEFINE Declaration define_declaration DEFINE define_body define_body identifier simple_expr define_body identifier simple_expr CONSTANTS Declaration constants_declaration CONSTANTS constants_body constants_body identifier constants_body identifier ASSIGN Declaration assign_constraint ASSIGN assign_list assign_list assign assign_list assign assign complex_identifier init complex_identifier next complex_identifier simple_expr simple_expr next_expr TRANS Statement trans_constraint TRANS next_expr INIT Statement init_constrain INIT simple_expr INVAR Statement invar_constraint INVAR simple_expr Module Declarations module MODULE identifier module_parameters module_body module_parameters identifier module_parameters identifier module_body module_element module_body module_element module_element var_declaration 128 ivar_declaration frozenvar_declaration define_declaration co
185. t and for all time t such that t lt t lt t pis true e p V qgistrue at time t if q holds at all time steps t gt t up to and including the time step t where p also holds Alternatively it may be the case that p never holds in which case q must hold in all time steps t gt t e Y pistrue at time t gt to if p holds at time t 1 Y pis false at time to e Z pis equivalent to Y p with the exception that the expression is true at time to e H pis true at time t if p holds in all previous time steps t lt t e O pis true at time t if p held in at least one of the previous time steps t lt t 38 e p S qis true at time t if q held at time t lt t and p holds in all time steps t such that t tO SF e p T qis true at time t if p held at time t lt t and q holds in all time steps t such that t lt t lt t Alternatively if p has never been true then q must hold in all time steps t such that to lt t lt t An LTL formula is true if it is true at the initial time to In NUSMV LTL specifications can be analyzed both by means of BDD based reasoning or by means of SAT based bounded model checking In the case of BDD based reasoning NUSMV proceeds according to For each LTL specification a tableau of the behaviors falsifying the property is constructed and then synchronously composed with the model With respect to CGH97 the approach is fully integrated within NUSMV and allows full t
186. t specified by a user and not computed statically by heuristics see variables input_order_fileon page 52Jand bdd_static_order_heuristics on page 53p The individual bits of variables may or may not be interleaved When bits interleaving is not used then bits belonging to one variable are grouped together in the ordering Other wise the bits interleaving is applied and all higher bits of all variables are ordered before all the lower bits i e N th bits of all variables go before N 1 th bits The exception is boolean variables which are ordered before variables of any other type though boolean variables consist of only 0 th bit The value of vars_order_type may be e inputs_before Input variables are forced to be ordered before state and frozen vari ables default No bits interleaving is done e inputs_after Input variables are forced to be ordered after state and frozen vari ables No bits interleaving is done e topological Input state and frozen variables are ordered as they are declared in the input smv file No bits interleaving is done e inputs_before_bi Bits are interleaved and in every group of N th bits input variables are forced to be ordered before state and frozen variables This is the default value e inputs_after_bi Bits are interleaved and in every group of N th bits input variables are forced to be ordered after state and frozen variables e topological_bi Bits are interleaved and in every group of N th bits in
187. t the current module has been instantiated to by using the self built in identifier MODULE container init_valuel init_value2 VAR cl counter init_valuel self VAR c2 counter init_value2 self MODULE counter init_value my_container VAR v 1 100 ASSIGN init v init_value DEF INE greatestCounterInContainer v gt my_container cl v amp v gt my_container c2 v MODULE main VAR c container 14 7 SPEC c cl greatestCounterInContainer In this example an instance of the module container is passed to the sub module counter In the main module c is declared to be an instance of the module container which de clares two instances of the module counter Every instance of the counter module has a define greatestCounterInContainer which specifies the condition when this particular counter has the greatest value in the container it belongs to So a counter needs access to the parent container to access all the counters in the container 2 3 13 Processes Important Since NUSMV version 2 5 0 processes are deprecated In future versions of NUSMV processes may be no longer supported and only synchronous FSM will be supported by the input language Modeling of asynchronous processes will have to be resolved at higher level 33 Processes are used to model interleaving concurrency A process is a module which is instan tiated using the keyword process see Sec
188. t the number of fair states Command print_fair_states h v Prints the number of fair states of the given model In verbose mode prints also the list of all fair states print_fair_transitions Prints out the number of fair states Command print_fair_transitions h v 59 Prints the number of fair transitions of the given model In verbose mode prints also the list of all fair transitions The transitions are displayed as state input pairs check_ctlspec Performs fair CTL model checking Command check_ctlspec h m o output file n number p ctl expr IN context P name Performs fair CTL model checking A ctl expr to be checked can be specified at command line using option p Alterna tively option n can be used for checking a particular formula in the property database If neither n nor p nor P are used all the SPEC formulas in the database are checked See variable use_coi size_sorting for changing properties verification order Command Options m Pipes the output generated by the command in processing SPEC s to the program specified by the PAGER shell vari able if defined else through the UNIX command more 0o output file Writes the output generated by the command in processing SPEC s to the file output file p ctl expr IN A CTL formula to be checked context is the module context instance name which the variables in ctl expr must be evaluated in
189. te 64 print_usage 102 check_ct 1spec 59 process _mode1 55 check_fsm 58 quit 102 check_invar_bmc_inc 79 read_model 49 check_invar_bmc 78 read_trace 92 check_invar 6 reset 102 check_1t1lspec_bmc_inc 73 set _bdd_parameters 99 check_1t 1spec_bmc_onepb 70 set 102 check_l1t 1spec_bmc 69 show_ dependencies 5 check_1t1spec_sbmc_inc 75 show plugins 9 check_l1t l1spec _sbmc 74 show property 66 check_l1t 1 spec 64 show _traces 9 check _property 65 show_vars 50 check_ps1spec 83 simulate 84 check_spec 60 source 103 clean_sexp2bdd_cache 98 time 104 comput e_reachable 58 unalias 105 dynamic_var_ordering 97 unset 106 echo 100 usage 106 encode variables 51 which 106 execute_partial traces 88 write_boolean_model 57 execute_traces 88 write_coi_model 67 flatten_hierarchy 49 write_flat_model 56 gen_invar_bmc 79 write_order 52 gen_ltlspec_bmc_onepb gen_lt lspec_bmc 7 gen_ltlspec_sbmc get_internal_status 55 135 Index NuSMV_LIBRARY PATH 107 110 affinity ag only_search 60 autoexec 106 backward_compatibility bdd_static_order_heuristics 53 bmc_dimacs_filename 77 bmc_force_pltl_tableau 77 bmc_inc_invar_alg 80 bmc_invar_alg 80 bmc_invar_dimacs_filename 80 bmc_length 77 bmc_loopback 77 bmc_optimized_t ableau 77 bmc sbmc gf fg opt 78 check fsm 59 check_invar_bdd_bmc_heuristic 63 check_invar_bdd_bmc_thres
190. ter preordering following heuristic described in RAPT 95 possible values are 0 or 1 The default value is 0 Preordering can be very slow image_verbosity Environment Variable Sets the verbosity for the image method Jw s95CP possible values are 0 or 1 The default value is 0 print_iwls95options Prints the Iwls95 Options Command print_iwls95options h This command prints out the configuration parameters of the IWLS95 clustering algorithm ie image_verbosity image_cluster_size and image W 1 2 37 4 go Initializes the system for the verification Command go h f This command initializes the system for verification It is equivalent to the command sequence read_model flatten_hierarchy encode_variables build_flat_model build_model If some commands have already been executed then only the remaining ones will be in voked Command Options f Forces model construction even when Cone Of Influence is enabled get_internal_status Prints out the internal status of the system Command get_internal_status h Prints out the internal status of the system i e e 1 read_model1 has not yet been executed or an error occurred during its execu tion e 0 flatten_hierarchy has not yet been executed or an error occurred during its execution e 1 encode_variables has not yet been executed or an error occurred during its execution e 2 build_model has not yet been executed or an error occurred during its
191. the system is now ready to execute user commands A NUSMV command is a sequence of words The first word specifies the command to be executed The remaining words are arguments to the invoked command Commands separated by a are executed sequentially the NUSMV shell waits for each command to terminate in turn The behavior of commands can depend on environment variables similar to csh environment variables It is also possible to make NUSMV read and execute a sequence of commands from a file through the command line option source system_prompt gt NuSMV source cimd_file lt RET gt source cmd file Starts the interactive shell and then executes NUSMV com mands from file cmd file If an error occurs during a com mand execution commands that follow will not be executed See also the variable on_failure_script_quits The option source implies int 48 In the following we present the possible commands followed by the related environment vari ables classified in different categories Every command answers to the option h by printing out the command usage When output is paged for some commands option m it is piped through the program specified by the UNIX PAGER shell variable if defined or through the UNIX com mand more Environment variables can be assigned a value with the set command Com mand sequences to NUSMV must obey the partial order specified in the Figure 3 11 depicted at page 108 Fo
192. tifier module_parameters identifier module_body module_element module_body module_element module_element var_declaration ivar_declaration frozenvar_declaration define_declaration constants_declaration assign_constraint trans_constraint init_constraint invar_constraint fairness_constraint ctl_specification invar_specification ltl_specification compute_specification isa_declaration The identifier immediately following the keyword MODULE is the name associated with the module Module names have a separate name space in the program and hence may clash with names of variables and definitions The optional list of identifiers in parentheses are the formal parameters of the module 2 3 11 MODULE Instantiations An instance of a module is created using the VAR declaration see Section 2 3 1 State Variables page 24 with a module type specifier see Section Type Specifiers page 23 The syntax ofa module type specifier is module_type_specifier identifier parameter_list process identifier parameter_list parameter_list next_expr parameter_list next_expr A variable declaration with a module type specifier introduces a name for the module instance The module type specifier provides the name of the instantiating module and also a list of actual parameters which are assigned to the formal parameters of the module An actual parameter can be any legal next expression see Secti
193. tifier is declared see Section 2 3 16 Context page 35 for an explanation of contexts Forward references to defined symbols are allowed but circular defini tions are not and result in an error The difference between defined symbols and variables is that while variables are statically typed definitions are not 2 3 3 Array Define Declarations It is possible to specify an array expressions This feature is experimental and currently available only through DEFINE declaration The syntax for this kind of declaration is array_define_declaration DEFINE identifier array_expression array_expression array_contents array_expression_list array_expression_list array_expression array_expression array_expression_list array_contents it next_expr array_contents next_expr Array DEFINE associates an identifier on the left hand side of the with an array expression As a normal DEFINE statement an array define is considered as a macro Whenever an array identifier occurs in an expression the identifier is syntactically replaced by the array expression it is associated with As with normal DEFINE an array DEFINE expression is always evaluated in the context of the statement where the identifier is declared and forward references to defined symbols are allowed but circular definitions are not The type of an array expression expl exp2 expN is array 0 N 1 of type where type is the least type such that al
194. tion 2 3 11 MODULE Instantiations page 3 Ip The program executes a step by non deterministically choosing a process then executing all of the assignment statements in that process in parallel It is implicit that if a given variable is not assigned by the process then its value remains unchanged Note that only assignments of the form ASSIGN next var_name are influenced by processes All other kinds of assignments and all constraints such as TRANS INVAR etc are always in force independent of which process is selected for execution Each instance of a process has a special boolean variable associated with it called running The value of this variable is TRUE if and only if the process instance is currently selected for execution No two processes may be running at the same time Note that only in the presence of processes NuSMV internally declares special variables running and _process_selector _ These names should NOT be used in user s own dec larations when processes are used but they can be referenced for example in the transition relation of a module Furthermore if the user declares N processes there will be N 1 processes allocated as the module main has always its own process associated In the following example there are three process p1 p2 and main MODULE my_module my module definition MODULE main VAR pl process my_module p2 process my_module 2 3 14 A Program and t
195. to states satisfying those constraints The desired se quence of states could not exist if such constraints were too strong or it may happen that at some point of the simulation a future state satisfying those constraints doesn t exist in that case a trace with a number of states less than steps trace is obtained Note constraints must be enclosed between double quotes The expression can contain next operators and is NOT automatically shifted by one state as done with option c k steps Maximum length of the path according to the constraints The length of a trace could contain less than steps states this is the case in which simulation stops in an intermedi ate step because it may not exist any future state satisfying those constraints The default value is determined by the default_simulation_steps environment variable bmc simulate_check_feasible_constraints Checks feasability for Command the given constraints bmc_simulate_check_feasible_constraints h q c constr Checks if the given constraints are feasible for BMC simulation Command Options q Prints the output in compact form c constr Specify one constraint whose feasability has to be checked can be used multiple times order is important to read the result 3 4 Commands for checking PSL specifications The following command allow for model checking of PSL specifications check_pslspec Performs PSL model checking Command check
196. ur and T Henzinger New Brunswick NJ 1996 Daniel Sheridan The optimality of a fast cnf conversion and its use with sat In SAT 2004 F Somenzi Cudd Cu decision diagram package release 2 2 0 In De partment of Electrical and Computer Engineering University of Colorado at Boulder May 1998 P A Strooper W Johnston K Winter L van den Berg and P Robinson Model based variable and transition orderings for efficient symbolic model checking In FM 2006 Formal Methods number 4085 in Lecture Notes in Computer Science pages 524 540 Springer Berlin 2006 115 Appendix A Compatibility with CMU SMV The NUSMV language is mostly source compatible with the original version of SMV distributed at Carnegie Mellon University from which we started In this appendix we describe the most common problems that can be encountered when trying to use old CMU SMV programs with NUSMV The main problem is variable names in old programs that conflicts with new reserved key words The list of the new reserved keywords of NUSMV w r t CMU SMV is the following F G X U V These names are reserved for the LTL temporal operators W H O Y Z S Ta B CTLSPEC It is used to introduce CTL specifications LTLSPEC It is used to introduce LTL specifications INVARSPEC It is used to introduce invariant specifications PSLSPEC It is used to introduce PSL specifications IVAR It is used to introduce input v
197. value is allowed and sets the variable to 1 NuSMV gt set foo will set the variable foo to 1 Interpolation of variables is allowed when using the set command The variables are referred to with the prefix of So for example what follows can be done to check the value of a set variable NuSMV gt set foo bar NuSMV gt echo foo bar 102 The last line bar will be the output produced by NUSMV Variables can be extended by using the character to concatenate values For example NuSMV gt se NuSMV gt se NuSMV gt ec bar fooba The variable be present w characters interpolation NuSMV gt se NuSMV gt ec this t foo bar t foo Sfoo foobar ho Sfoo r foo is extended with the value foobar Whitespace characters may ithin quotes However variable interpolation lays the restriction that the and may not be used within quotes This is to allow for recursive So for example the following is allowed t foo bar this ho foo bar The last line will be the output produced by NUSMV But in the following the value of the variable foo bar_ will not be interpreted correctly NuSMV gt se NuSMV gt ec foo bar If a variable t foo bar this ho foo bar is not set by the set command then the variable is returned unchanged Different commands use environment information for different purposes The command interpreter makes use of the following parameters Comman
198. variable ordering to file ov_file Reads a variable list from file tv _file This list defines the order for clustering the transition relation This fea ture has been provided by Wendy Johnston University of Queensland The results of Johnston s et al research have been presented at FM 2006 in Hamilton Canada See WJKWLvdBRO6 Enables variable reordering after having checked all the specification if any Enables dynamic reordering of variables Uses method when variable ordering is enabled Pos sible values for method are those allowed for the reorder_method environment variable see Section 3 9 Interface to DD package pe default value of environment variable enable bdd cache to 0 i e the evaluation of symbolic expression to ADD and BDD representations are not cached See command clean sexp2bdd cache for reasons of why BDD cache should be disabled sometimes Sets the default bdd_static_order_heuristics to heuristics i e the option sets up the heuristics to be used to compute BDD ordering statically by analyzing the input model See the documentation about variable bdd_static_order_heuristics on page 53 for more details value of environment variable 112 mono thresh cpt cp cp t iwls95 cpt noaffinity iwls95preoder bmc bmc length k sat_solver name sin on off rin on off ojeba algorithm Enables monolithic transition relation conjunctive partitioning with threshold of
199. xist any future state satisfying those constraints The default value is determined by the default_simulation_steps environment variable bmc_inc_simulate Generates a trace of the model from 0 zero to Command k bmc_inc_simulat t constraints p v r c constraints k steps Performs incremental simulation of the model bmc_inc_simulate does not require a specification to build the problem because only the model is used to build it The problem length is represented by the k command parameter or by its default value stored in the environment variable bmc_length Command Options c constraint Prints the generated trace only changed variables Prints the generated trace all variables Picks a state from a set of possible future states in a random way Performs a simulation in which computation is restricted to states satisfying those constraints The desired se quence of states could not exist if such constraints were too strong or it may happen that at some point of the simulation a future state satisfying those constraints doesn t exist in that case a trace with a number of states less than steps trace is obtained Note constraints must be enclosed between double quotes The expression cannot contain next operators and is automatically shifted by one state in order to constraint only the next steps 82 t constraints Performs a simulation in which computation is restricted

NuSMV 2.5 User Manual

Contents

Download Pdf Manuals

Related Search

Related Contents