Home

NuSMV 2.2 User Manual

Contents

1. h n idx p formula IN context This command does the same thing as check_invar_bmc see the description on page 38 but uses an incremental algorithm and therefore usually runs con siderably quicker The incremental algorithms exploit the fact that satisfiability problems generated for a particular invariant have common subparts so informa tion 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 39 There are two incremental algorithms which can be used Dual and ZigZag Both algorithms are equally powerful but may show different performance de pending 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 Command Options n index p formula context k max _length a alg bmc_invar_alg IN 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 Checks the formula specified on the command line context is the module instance name which the variables in formula must be evaluated in maxtength is the maximum problem bound that can be reached Only natural numb
2. 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 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 generated NUSMV internally calls a propositional SAT solver in or der to find an assignment which satisfies the problem Currently NUSMV supplies three SAT solvers SIM Zchaff and MiniSat 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 algorithms exploit the fact that satisfiability problems generated for a particular bounded model checking problem often share common subparts So information obtained dur ing 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 interface 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 n
3. self id atom id simple_expr J An atom identifies the object of that name as defined in a VAR or DEF INE declaration If a identifies an instance of a module then the expression a b identifies the com ponent object named b of instance a This is precisely analogous to accessing a component of a structured data type Note that an actual parameter of module a can identify another module instance b allowing a to access components of p as in the following example MODULE main cs VAR a foo b D bar a MODULI E foo x DEF INE G r X p lx q MODULE bar x VAR p boolean a boolean Here the value of c is the logical or of p and q If a identifies an array the expression a b identifies element p of array a It is an error for the expression b to evaluate to a number outside the subscript bounds of array a or to a symbolic value It is possible to refer the name the current module has been instantiated to by using the self builtin identifier MODULE element above below token VAR 13 Token boolean ASSIG init Token token next Token token in DEFINE above token in Token grant out below grant out MODULE cell VAR 2 element self Dep O bts lement e1 self 1 DEFINE 2 token in token in gra
4. 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 informati on 63 int load cmd file Cpp pre pps ofm fm file obm bm_file 1p n idx siS SIC ils STi Ett AG Col i ivfile o ov file reorder dynamic Starts interactive shell 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 Avoids to load the NUSMV commands con tained in nusmvre or in nusmvre or in NuSMV_LIBRARY_PATH master nusmvrc Runs preprocessor 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 fied 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 seperated list of pre processor names contained within double quotes prints flattened model to file fn_file Prints boolean model to file bn file Lists all properties in SMV model
5. during every step of an interactive session This option works only if the i option has been specified 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 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 intermediate step because it may not exist any future state satisfying those constraints A trace is a sequence of states inputs pairs corresponding to a possible execution of the model 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 D EF INE sections are also part of a trace If the value of a constant depends only on state 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 con stant depends upon both input and
6. n can be used for checking a particular formula in the property database If neither n nor p are used all the SPEC formulas in the database are checked Command Options m Pipes the output generated by the command in processing SPEC s 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 SPEC s to the file output file p ctl expr A CTL formula to be checked context is the module IN context instance name which the variables in ct l expr must be evaluated in n number Checks the CTL property with index number in the prop erty 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 ag_only_search Environment Variable Enables the use of an ad hoc algorithm for checking AG formulas Given a for mula 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 28 Enables the computation of the reachable states during the process_model command and when used in conjunction with the ag only_search environ ment variable enables the use of an ad hoc algorithm to verify invariants check_invar Perfor
7. 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 li brary typically NuSMV_LIBRARY_PATH is always implic itly appended to the current path This provides a convenient 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 file by setting the variable nusmv_stdout source Executes a sequence of commands from a file Command source 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 s Silently ignores an attempt to execute commands from a nonexistent file 2x Echoes each command before it is executed lt file gt File name Arguments on the command line after the filename are remembered but not eval uated Commands in the script file can then refer to these arguments using the history substitution mechanism EXAMPLE Contents of test scr o readmodel i 2 flatten _hierarchy build variables buildmodel compute fairness Typing source test scr short smv on the command line will execute the sequence 57 readmodel i
8. or in each column The entries along the state axis are SO CL ET St 2 Cn Tn Sn where SO is the initial state and J gives the values of the input variables which caused the transition from state S _ to state S C gives the values of any combina torial constants where the value depends on the values of the state 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 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 6 3 XML Format Printer This plugin prints out the trace either to st dout or to a specified file using the com mand 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 47 E lt XML_VERSION_STRING gt lt counter example type TRACE_TYPE desc TRACE_DESC gt for each state i lt node gt lt state id i gt for each state var j lt value variable j gt VALUE lt value gt lt state gt lt combinatorial id i
9. 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 Typ ically the current directory is first in this list The standard system library NuSMV_LIBRARY_PATH is always implicitly appended to the current path This provides a convenient short hand mechanism for reaching standard library files nusmy _stderr Environment Variable Standard error normally st derr can be re directed to a file by setting the vari able nusmv_stderr nusmv_stdout Environment Variable 61 reset read_model flatten_hierarchy encode_variables build_model compute_reachable LE k check_spec check_Itlspec_bmc check_ltlspec gen_Itlspec_bmc check_invar check_invar_bmc check_trans gen_invar_bmc compute_reachable bmc_simulate simulate Figure 3 1 The dependency among NUSMV commands Standard output normally stdout can be re directed to a file by setting the internal variable nusmv_stdout nusmyv_stdin Environment Variable Stan
10. 1 gt for each combinatorial constant k lt value variable k gt VALUE lt value gt lt combinatorial gt lt input id i 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 3 6 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 file 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 7 Interface to the DD Package NUS MV uses the state of the art BDD package CUDD Som98 Control over the BDD package can very important to tune the performance of the system In particular the order of variables is critical to control the memory and the time required by operations To be exact Mi C Mo where M is the model from which the trace was
11. 2 3 2 LTL Specifications o e 2 3 3 Real Time CTL Specifications and Computations 2 4 Variable Order Input 2 4 1 InputFile Syntax o 2 4 2 Scalar Variables Z243 Array Variables gardos d So ee ed 3 Running NuSMV interactively 3 1 Model Reading and Building o 3 2 Commands for Checking Specifications 3 3 Commands for Bounded Model Checking 3 4 Simulation Commands 0 0 000 eee ene Bed O te ee DAADA We ae ek tee 3 5 1 Inspecting Traces ss ag or a ee eS 3 5 2 Displaying Trac s 00 aaa eet E ass 3 5 3 Trace Plugin Commands 0 3 6 Trace PLODIOS hoi er rr a SE oa ECS 46 3 6 1 Basic Trace Explainer o a 46 3 6 2 States Variables Table 47 3 6 3 XML Format Printer 47 3 6 4 XML Format Reader 48 3 7 Interface to the DD Package o 48 3 8 Administration Commands 0 000084 52 3 9 Other Environment Variables 60 4 Running NuSMV batch 63 A Compatibility with CMU SMV 68 Chapter 1 Introduction NUS MV 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 th
12. 6 we define the syntax of the input language of NuUSMV e In Chapter 3 Running NuSMV interactively page 21 the commands of the interaction shell are described e In Chapter 4 Running NuSMV batch page 63 we define the batch mode of NuUSMV NUSMV is available at http nusmv irst itc it Chapter 2 Syntax We present now the complete syntax of the input language of NUSMV In the follow ing an atom may be any sequence of characters starting with a character in the set A Za z_ and followed by a possibly empty sequence of characters belonging to the set A Za z0 9_S A number is any sequence of digits A digit belongs to the set 0 9 All characters and case in a name are significant Whitespace characters are space lt SPACE gt tab lt TAB gt and newline lt RET gt Any string starting with two dashes and ending with a newline is a comment Any other tokens recognized by the parser are enclosed in quotes in the syntax expressions below Grammar productions enclosed in square brackets are optional 2 1 Expressions Expressions are constructed from variables constants and a collection of operators including boolean connectives integer arithmetic operators case expressions and set expressions 2 1 1 Simple Expressions Simple expressions are expressions built only from current state variables Simple expressions can be used to specify sets of states e g the initial set of states
13. The syntax of simple expressions is as follows simple_expr atom 5 a symbolic constant number j a numeric constant TRUE The boolean constant FALSE The boolean constant var_id j a Variable identifier simple_expr I simple_expr 7 logical not simple_expr amp simple_expr 7 logical and simple_expr simple_expr 77 Logical or simple_expr xor simple_expr logical exclusive or simple_expr gt simple_expr 7 logical implication simple_expr lt gt simple_expr logical equivalence J 0 simple_expr simple_expr 7 equality simple_expr simple_expr 7 inequality simple_expr lt simple_expr 7 less than simple_expr gt simple_expr 7 greater than simple_expr lt simple_expr 7 less than or equal simple_expr gt simple_expr 77 Greater than or equal simple_expr simple_expr 7 integer addition simple_expr simple _ expr 7 integer subtraction simple_expr simple_expr 7 integer multiplication simple_expr simple_expr 7 integer division simple_expr mod simple_expr integer remainder set_simple_expr 7 a set simple_expression case_Simple_expr 7 a case expression A var_id see Section 2 2 10 Identifiers page 13 or identifier is a symbol or expres sion which identifies an object such as a variable or a defined symbol Since a var_id can be an atom there is a possible ambiguity if a variable or defined symbol has the same na
14. and commercial companies have express interest in collaborating to the de velopment of NUSMV The main features of NUSMV are the following e Functionalities NUSMV allows for the representation of synchronous and asynchronous finite state systems and for the analysis of specifications expressed in Computation Tree Logic CTL and Linear Temporal Logic LTL using BDD based and SAT based model checking techniques Heuristics are avail able 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 Architecture A software architecture has been defined The different compo nents and functionalities of NUSMV have been isolated and separated in mod 1 see http www opensource org ules Interfaces between modules have been provided This reduces the effort needed to modify and extend NUSMV Quality of the implementation NUSMV 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 other people than the developers This document is structured as follows e In Chapter 2 Syntax page
15. are both assigned in the pro gram e the current value and the next value of a variable are both assigned in the program 2 2 4 TRANS declarations The transition relation R 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 valued expression T intro duced by the TRANS keyword The syntax of a TRANS declaration is trans_declaration TRANS trans_expr trans_expr 24 Next expr It is an error for the expression to yield any value other than 0 or 1 If there is more than one TRANS declaration the transition relation is the conjunction of all of TRANS declarations 2 2 5 INIT declarations The set of initial states of the model is determined by a boolean expression under the INIT keyword The syntax of a INIT declaration is 10 init_declaration INIT init_expr init_expr simple_expr It is an error for the expression to contain the next operator or to yield any value other than 0 or 1 If there is more than one INIT declaration the initial set is the conjunction of all of the INIT declarations 2 2 6 INVAR declarations The set of invariant states i e the analogous of normal assignments as described in Section 2 2 3 ASSIGN declarations page 10 can be specified using a boolean expression under the INVAR keyword The syntax of a INVAR declaration is invar_declaration INVAR invar_expr invar_exp
16. 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 de pendencies only in normal assignments and not in next assignments The circular dependencies check of NUSMV has been extended to detect circulari ties 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 next y next y y next x Another difference between NUSMV and CMU SMV is in the variable order file The variable ordering file accepted by NUSMV can be partial and can contain vari ables 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 follow ing 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 ac cepted 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 NUSMV iden tifier process_selector can be used to control the position of the variable that encodes proces
17. different factors in the algorithm The default values are 6 1 1 6 respectively For a detailed description please refer to RAPT 95 iwls95preorder Environment Variable 25 Enables cluster preordering following heuristic described in RAP 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 w s95CP possible values are 0 or 1 The default value is 0 print_iwls95options Prints the Iwls95 Options Command print_iwls9 5options h This command prints out the configuration parameters of the IWLS9S clustering algorithm i e image_verbosity image_cluster_sizeand image W 1 2 3 4 go Initializes the system for the verification Command go h This command initializes the system for verification It is equivalent to the com mand sequence read_model flatten_hierarchy encode_variables buildmodel build_flat_model build_boolean_model If some com mands have already been executed then only the remaining ones will be invoked process_model Performs the batch steps and then returns Command control to the interactive shell process model h i model file m Method Reads the model compiles it into BDD and performs the model checking of all the specification contained in it If the environment variable forward_search has been set before then the set of reachable states is computed If the envi r
18. 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 Jength 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_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 ltlspec_ bmc family DIMACS file name can contain special symbols which will be expanded to represent the actual file name Possible symbols are 37 e F The currently loaded model name with full path e Cf The currently loaded model name without path part e On The numerical index of the currently processed formula in the property database e k The currently generated problem length e The currently generated problem loopback value e The character The default value is _k k_1 1_n n check_invar_bmc Generates and solves the given invari Command ant or all invariants if no formula is given check_invarbme h n idx p formula IN context a alg 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 i
19. from zero to length 1 o filename filename is the name of the dumped dimacs file If this op tions 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 f model name without path part k current problem bound 21 current loopback value erty database e 00 the E character check_ltlspec_bmc_inc Checks the given LTL specification or all LTL specifications if no formula is given using an in cremental algorithm Checking parameters are the maximum length and the loopback value check_1t1spec bmc inc h n idx p formula k max_length 1 loopback On index of the currently processed formula in the prop Command IN context For each problem this command incrementally generates many satisfiability sub problems and calls the SAT solver on each one of them The incremental algo rithm 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_1t 1spec_bmc see the description on page 32 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 unavail
20. generated and Ma is the currently loaded and built model Note however that this may mean that the trace is not valid for the model Mo 48 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 re ordering by the package This is called dynamic reordering and can be enabled or dis abled by the user Dynamic reordering is enabled with the shell command dynamic var_ordering with the option e and disabled with the d option enable_reorder Environment Variable Specifies whether dynamic reordering is enabled when value is 0 or disabled when value is 1 reorder_method Environment Variable Specifies the ordering method to be used when dynamic variable reordering is fired The possible values corresponding to the reordering methods available with the CUDD package are listed below The default value is sift Site Moves each variable throughout the order to find an optimal position for that variable assuming all other variables are fixed This generally achieves greater size r
21. ltl_expr Z ltl_expr H ltl_expr o Etl exp ltl_expr S 1t1_expr ltl_expr T ltl_expr EC 1t1l_expr a simple boolean expression logical not logical and logical or logical exclusive or logical implies logical equivalence next state globally finally until releases previous state not previous state not historically once since triggered In NUSMV LTL specifications can be analyzed both by means of BDD based reason ing or by means of SAT based bounded model checking In the first case NUSMV proceeds along the lines described in CGH97 For each LTL specification a tableau able to recognize the behaviors falsifying the property is constructed and then syn chronously composed with the model With respect to CGH97 the approach is fully integrated within NUSMV and allows for full treatment of past temporal operators In the case of BDD based reasoning the counterexample generated to show the fal sity of a LTL specification may contain state variables which have been introduced by the tableau construction procedure In the second case a similar tableau construction is carried out to encode the existence of a path of limited length violating the prop erty 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 2 3 3 Real Time CTL Specificat
22. name Command Options i file name Reads in a trace from the specified file Note that the file must only contain one trace 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 6 Trace Plugins NUSMV comes with three plugins which can be used to diaplay a trace that has been generated Basic Trace Explainer States Variables Table XML Format Printer There is also a plugin which can read in any trace which has been output to a file by the XML Format Printer Note however that this reader 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 plugin The command show_traces can be used to output any previuosly generated or loaded trace to a specific file 3 6 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 variables and their initial values States are numbered in the following fasion trace_number state_number 46 There is the option of printing out the value of every variable in each state or just those which have changed from the
23. 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 Disable dynamic ordering from triggering automatically e lt method gt 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 50 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 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 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 impleme
24. ordering to be used in building the model by the encode_variables command 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 encoding 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 0 write_order Writes variable order to file Command 23 write_order h b o f 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 output_order_file will 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 previously set When the boolean variable dumping is enabled the single bits will occur within the resulting orderin
25. 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 42 Command Options C constraints steps 3 5 Traces Prints current generated trace only those variables whose value changed from the previous state Verbosely prints current generated trace changed and un changed state 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 step of the simulation and are forgotten in the next one Displays all the state variables changed and unchanged
26. the FSM can be expressed in two different tem poral logics the Computation Tree Logic CTL and the Linear Temporal Logic LTL extended with Past Operators It is also possible to analyze quantitative characteristics of the FSM by specifying real time CTL specifications Specifications can be posi tioned within modules in which case they are preprocessed to rename the variables according to the containing 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 prop erty 2 3 1 CTL Specifications A CTL specification is given as a formula in the temporal logic CTL introduced by the keyword SPEC The syntax of this declaration is spec_declaration SPEC spec_expr spec_expr ctl_expr The syntax of CTL formulas recognized by the NUSMV parser is as follows ctl_expr simple_expr 7 a Simple boolean expression MeT ere Le eis mjt ctl_expr 7 Logical not ctl_expr amp ctl_expr logical and ctl_expr ctl_expr 7 Logical or In 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 specifi cations and in Bounded Model Checking in the next releases of NUSMV 15 ctl_expr xor ctl
27. 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 The last line bar will be the output produced by NUSMV Variables can be ex tended by using the character to concatenate values For example NuSMV gt set foo bar NuSMV gt set foo foo foobar NuSMV gt echo foo bar foobar The variable foo is extended with the value foobar Whitespace characters may be present within quotes However variable interpolation lays the restriction that the characters and may not be used within quotes This is to allow for recursive interpolation So for example the following is allowed NuSMV gt set foo bar this NuSMV gt echo foo bar this 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 set foo bar this NuSMV gt echo foo bar foo bar If a variable is not set by the set command then the variable is returned un changed Different commands use environment information for different pur poses The command interpreter makes use of the following parameters 56 Command 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
28. NuSMV 2 2 User Manual Roberto Cavada Alessandro Cimatti Emanuele Olivetti Gavin Keighren Marco Pistore and Marco Roveri IRST Via Sommarive 18 38055 Povo Trento Italy Email nusmv irst itc it This document is part of the distribution package of the NUSMV model checker avail able at http nusmv irst itc it Parts of this documents have been taken from The SMV System Draft by K McMillan available at http www cs cmu edu modelcheck smv smvmanual r2 2 ps Copyright 1998 2005 by CMU and ITC irst Contents 1 Introduction 2 Syntax Qel A EXPTESSIONS 5 ii a was he as AG OE A a 2 1 1 Simple Expressions 0 2 12 Next Expressions s i a ad aS 2 2 Definition of the FSM 0 e 2 2 1 State Variables 22 2 Input Variables spore rre a la 2 2 3 ASSIGN declarations 2 2 4 TRANS declarations e 2 2 5 INIT declarations is coeno e 2 2 6 INVAR declarations 2 2 7 DEFINE declarations 2 2 8 TSA declarations 2 2 9 MODULE declarations 2 2 AQ Identifiers oia a a lp aa 2 2 11 Themainmodule DDD SPIOCESSES 3 AA Sy Be eo Be ee he ete BS 2 2 13 FAIRNESS declarations 02004 2 3 Specifications sosen e 5 jb ee ee ee ee ee ec 2 3 1 CTL Specifications o es pessa
29. Specifies which property of SMV model should be checked Does not check SPEC Does not check COMPUTE Does not check LTLSP 5a Q Does not check INVARSPEC Checks whether the transition relation is total Computes the set of reachable states before evaluating CTL expressions Prints the number of reachable states before exiting If the f option is not used the set of reachable states is computed Verifies only AG formulas using an ad hoc algorithm see documentation for the ag only search environment variable Enables cone of influence reduction Reads the variable ordering from file iv file Reads the variable ordering from file ov_file Enables variable reordering after having checked all the specification if any Enables ayia reordering of variables m method mono thresh cpt cp cpt iwls95 cpt noaffinity iwls95preoder bmc bmc k Uses method when variable ordering is enabled Pos sible values for method are those allowed for the reorder_method environment variable see Section 3 7 Interface to DD package page 48 Enables monolithic transition relation conjunctive partitioning with threshold of each partition set to cp DEFAULT with cp_t 1000 DEPRECATED use thresh instead Enables Iwls95 conjunctive partitioning and sets the thresh old of each partition to cpt Disables affinity clustering Enables w s95CP preordering Enables BMC instead of BDD model checkin
30. _expr 7 logical exclusive or ctl_expr gt ctl_expr 7 logical implies ctl_expr lt gt ctl_expr 7 Logical equivalence EG ctl_expr 7 exists globally EX ctl_expr exists next state EF ctl_expr 7 exists finally AG ctl_expr 7 forall globally AX ctl_expr forall next state AF ctl_expr forall finally E ctl_expr UT ctl_expr exists until A ctl expr U ctl_ expr forall until It is an error for an expressions in a CTL formula to contain a next operator or to have non boolean components i e subformulas which evaluate to a value other than 0 or 1 It is also possible to specify invariants i e propositional formulas which must hold invariantly in the model The corresponding command is INVARSPEC with syntax checkinvar_declaration This statement corresponds to SPEC AG simple_expr INVARSPE E simple_expr but can be checked by a specialized algorithm during reachability analysis 2 3 2 LTL Specifications LTL specifications are introduced by the keyword LTLSPEC The syntax of this declaration is ltlspec_declaration LTLSP where 1t1_expr simple_expr CM LELexpr Mm Ii Tel expr ltl_expr amp ltl_expr ltl_expr ltl_expr ltl_expr xor ltl_expr ltl_expr gt l1tl_expr 1t1_expr lt gt ltl_expr FUTURE Xx 1 t1_expr G 1 t1_expr E Etl cexpr ltl_expr U 1t1_expr ltl_expr V ltl_expr 77 PAST Y
31. _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 idxorthe p formula options If you need to generate a DIMACS dump file of all generated problems you must use the option o filename Command Options n index p formula IN context k max_length 1 loopback index is the numeric index of a valid LTL specification for mula actually located in the properties database Checks the formula specified on the command line context is the module instance name which the variables in formula must be evaluated in 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 e anegative number in 1 bmc length In this ca
32. able 36 Command Options n index p formula IN context k max _length 1 loopback bmc_length index is the numeric index of a valid LTL specification for mula actually located in the properties database Checks the formula specified on the command line context is the module instance name which the variables in formula must be evaluated in maxtength 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 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 anegative 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 loopback from zero to length 1 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_oopback The default value is 10 bmc_loopback Environment Variable Sets the generated problem loop Possible values are
33. and linear transformations a f 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 print_bdd_stats Prints out the BDD statistics and parame Command ters 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 Command currently 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 pack age so the user can set specific BDD parameters to the given value This com mand works in conjunction 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_sta
34. ant i with m lt 1 lt n and property p holds in all future time instants j with m lt j lt i Real time CTL specifications can be defined with the following syntax which extends the syntax for CTL specifications 17 spec_declaration SPEC rtctl_expr With the COMPUTE statement it is also possible to compute quantitative informa tion 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_declaration COMPUTE compute_expr where compute_expr MIN rtctl_expr rtctl_expr MAX rtctl_expr rtctl_expr MIN start final computes the set of states reachable from start 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 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 2 4 Variable Order Input It is possible to specify the order in which variables should appear in the BDD s gen erated 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 v
35. ariable in interactive mode 2 4 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_list EMPTY var_list_item vars_list var_list_item var_main_id Fi yo var_main_id NUMB var_main_id ATOM var_main_id NUMBER var_main_id var_id var_id ATOM var_id NUMBER var_id var_id That is 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 an encoded scalar variable 18 where Complete_Var_Name is just the name of the variable if it appears in the mod ule 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 i
36. at the n th command n Repeat 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 oe Ur 50 ct E Hh o0 de AP P AP X oP X 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 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 reset Resets the whole system Command reset h Resets the whole system in order to read in another model and to perform verifi cation 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 com mand 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 55 Command Options lt name gt Variable name lt value gt Value to be assigned to the variable Interpolation of variables is allowed when using the set command The vari ables are referred
37. bles similar to csh environment variables In the following we present the possible commands followed by the related envi ronment variables classified in different categories Every command answers to the option h by printing out the command usage When output is paged for some com mands option m it is piped through the program specified by the UNIX PAGER shell variable if defined or through the UNIX command more Environment variables can be assigned a value with the set command Command sequences to NUSMV must obey the partial order specified in the figure depicted on page 62 For 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 54 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 21 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 readmodel h i mode
38. body assign_body atom simple_expr 7 normal assignment init atom simple expr 7 init assignment next atom next_expr 7 next assignment On the left hand side of the assignment atom denotes the current value of a variable init atom denotes its initial value and next atom denotes its value in the next state If the expression on the right hand side evaluates to an integer 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 evaluates 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 In order for a program to be implementable there must be some order in which the assignments can be executed such that no variable is assigned after its value is referenced This is not the case if there is a circular dependency among the assignments in any given process Hence such a condition is an error It is also an error for a variable to be assigned more than once at any given time More precisely it is an error if any of the following occur e the next or current value of a variable is assigned more than once in a given process e the initial value of a variable is assigned more than once in the program e the current value and the initial value of a variable
39. cation then simply specifying Complete_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 l 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 Complete_Var_Name requires N boolean variables to en code all the possible values that it may take It is still possible to then specify other specific bit variables at later points in the or dering file as before 2 4 3 Array Variables When declaring array variables in the ordering file each individual element must be specified separately I
40. dard input normally st din can be re directed to a file by setting the inter nal variable nusmv_stdin 62 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 The program described in input file is proc ET gt input file lt RI essed and the corresponding finite state ma chine 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 NuSMV h help v vl int load scriptfile s cpp pre pps ofm fmfile obm bm file lp n idx is ic ils ii ctt f r AG coi i ivfile o ovfile reorder dynamic m method mono thresh cp t cp cp t iwls95 cp t noaffinity iwls95preorder bmc bmc length k 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 A 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
41. dition no two processes with the same parents may be running at the same time 2 2 13 FAIRNESS declarations A fairness constraint restricts the attention only to fair execution paths When evalu ating specifications the model checker considers path quantifiers to apply only to fair paths 14 NUSMV supports two types of fairness constraints namely justice constraints and compassion constraints A justice constraint consists of a formula f which is assumed to be true infinitely often in all the fair paths In NUSMV justice constraints are iden tified by keywords JUSTICE and for backward compatibility FAIRNESS A com passion 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 in the fair path In NuSMV compassion constraints are identified by keyword COMPASSION If com passion constraints are used then the model must not contain any input variables Cur rently 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 fairness declaration 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 Specifications The specifications to be checked on
42. e command line context is the module instance name which the variables 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 variable context in formula must be evaluated in k length bmc_length is considered instead 1 loopback The loopback value may be e a natural number in 0 maxJength 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 anegative 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 dur ing the generation solving process 33 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 l current loopback value e On index of the currently processed formula in the prop erty database e 00 the character gen ltlspec_bme Dumps into one or more dimacs files the Command given LTL specification or all LTL specifica
43. e 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 CCGROO Version 1 of NUSMV basically implements BDD based symbolic model check ing Version 2 of NUSMV NUSMV2 in the following inherits all the functionalities of the previous version and extend them in several directions CCGt02 The main novelty in NUSMV2 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 techniques Starting from NUSMV2 we are also adopting a new development and license model NUSMV2 is distributed with an OpenSource license 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
44. eductions 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 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 maximum number of nodes the one closest to the root is used sift_converge The sift method is iterated until no further im provement is obtained symmetry sift This method is an implementation of symmetric sift ing It is similar to sifting with one addition Vari ables 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 49 symmetry sift_convEhesymmetry_sift method is iterated until no further improvement is obtained 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 window 2 3 4 convEhegeindow 2 3 4 method is iterated until no further improvement is obtained group sift This method is similar to symmetry_sift but use
45. en LTL specification or for all LTL specifications if no formula is explicitly given Genera tion and dumping parameters are the problem bound and the loopback value gen 1t1spec bmc onepb h n idx p formula IN context k length 1 loopback o filename As the gen_1t 1spec_bmc command but it generates and dumps only one prob lem given its bound and loopback Command Options n index index is the numeric index of a valid LTL specification for mula actually located in the properties database The validity of index value is checked out by the system 35 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 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 anatural number in 0 length 1 A positive sign 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 negative number in 1 length Any invalid combination of length and loopback will be skipped during the gener ation process e the symbol X which means no loopback e the symbol which means all possible loopback
46. eory for automatic hierarchical verification of speed independent circuits In ACM Distinguished Dissertations MIT Press 1988 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 66 Mar85 A J Martin The design of a self timed circuit for distributed mutual ex clusion In In H Fuchs and W H Freeman editors Proceedings of the 1985 Chapel Hill Conference on VLSI pages 245 260 New York 1985 McM92 K L McMillan The smv system draft In Available at http www cs cmu edu modelcheck smv smvmanual r2 2 ps 1992 McM93 K L McMillan Symbolic model checking In Kluwer Academic Publ 1993 MHS00 Moon Hachtel and Somenzi Border block tringular form and conjunc tion schedule in image computation In FMCAD 2000 RAP 95 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 sfVS96 VIS A system for Verification and The VIS G
47. ers are valid values for this option If no value is given the environment variable bmc_length is considered instead 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 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 Pos sible values 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 e The character The default value is f_invar_n n sat_solver Environment Variable 40 The SAT solver s name actually to be used Default SAT solver is SIM De pending on the NUSMV configuration also the Zchaff and MiniSat SAT solvers can be available or not Notice that Zchaff and MiniSat are
48. es in invar expr must be evaluated in check_ltlspec Performs LTL model checking Command check_ltlspec h m o output file n number p ltl expr IN context Performs model checking of LTL formulas LTL model checking is reduced to CTL model checking as described in the paper by CGH97 A ltl expr to be checked can be specified at command line using option p Alternatively 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 Command Options 29 m Pipes the output generated by the command in process ing LTLSPECs to the program specified by the PAG ER shell variable 1f 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 An LTL formula to be checked context is the module IN context instance name which the variables in 1t1 expr must be evaluated in n number Checks the LTL property with index number in the property database compute Performs computation of quantitative character Command istics compute h m o output file n number p compute expr IN context This command deals with the computation of quantitative characteristics of real time systems It is able to compute the length of the shortest longest path fro
49. ex of the currently processed formula in the prop erties database 38 e 00 the character gen invar_bmc Generates the given invariant or all in Command variants ifno formula is given gen invar bmc h o filename n idx p formula IN context At the moment the invariants are generated using classic algorithm only see the description of check_ Command Options n index p formula IN context o filename invar_bmc on page 38 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 Checks the formula specified on the command line context is the module instance name which the variables in formula must be evaluated in 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 Possible sym bols are e F model name with path part e f model name without path part e On index of the currently processed formula in the prop erties database e 00 the character check_invar_bmc_inc Generates and solves the given in Command variant or all invariants if n mental algorithms check_invar bmc inc Ta algorithm o formula is given using incre
50. for non commercial purposes only bmc_simulate Generates a trace of the model from 0 zero Command to k bmc_simulate h k 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 Command Options k length length is the length of the generated simulation 3 4 Simulation Commands In this section we describe the commands that allow to simulate a NUSMV specifica tion See also the section Section 3 5 Traces page 43 that describes the commands available for manipulating traces pick_state Picks a state from the set of initial states Command pick state h v r i al c constraints 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 v Verbosely prints out chosen state all state variables oth erwise 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 r Rand
51. g Sets bmc_length variable used by BMC 65 Bibliography BCCZ99 BCL 94 CBM90 CCG 02 CCGROO CGH97 Dil88 EMSS91 ES04 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 IEEE 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 sequential machines based on symbolic execution In In J Sifakis edi tor Proceedings of the International Workshop on Automatic Verification Methods 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 Ver ification CAV 02 2002 A Cimatti E Clarke F Giunchiglia and M Roveri Nusmv a new symbolic model checker In International Journal on Software Tools for Technology 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 th
52. g at all e Threshold Conjunctive partitioning with a simple threshold heuristic Assignments are collected in a single cluster until its size grows over the value specified in the variable conj_part_threshold It is possible default to use affinity clustering to improve model checking performance See affinity variable Iwls95CP Conjunctive partitioning with clusters generated and ordered ac cording to the heuristic described in RAP 95 Works in conjunction with the variables image_cluster _size image_W1 image_W2 image_W3 image_W4 It is possible default to use affinity clustering to improve model checking performance See affinity variable It is also possi ble 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 MHS00 possible values are 0 or 1 The default value is 1 image_cluster_size Environment Variable One of the parameters to configure the behaviour of the Jw s95CP partitioning algorithm image_cluster _size is used as threshold value for the clusters The default value is 1000 BDD nodes image_W 1 2 3 4 Environment Variable The other parameters for the Jw s95CP partitioning algorithm These attribute different weights to the
53. g file in the same position that they occur at BDD level Command Options b Dumps bits of scalar variables instead of the single scalar variables See also the variable write_order_dumps_bits o order fil Sets the environment variable output _order_file to order file and then dumps the ordering list into that file f order fil Alias for the o option Supplied for backward compatibil 1ty output_order file Environment Variable The file where the current variable ordering has to be written The default value is temp ord build_model Compiles the flattened hierarchy into a BDD Command buildmodel h 1 m Method Compiles the flattened hierarchy into a BDD initial states invariants and transi tion relation using the method specified in the environment variable part it ion_method for building the transition relation Command Options m Method Sets the environment variable partitionmethod to the value Method and then builds the transition relation Available methods are Monolithic Threshold and Iwls95CP 24 f 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 partitionin
54. gin 45 nable_reorder 49 filec 61 forward_search 29 history _char 61 image_W 1 2 3 4 25 image cluster size 25 image_verbosity 26 input file 22 input_order_file 23 iwls95preorder 26 nusmv _stderr 6l nusmv _stdin 62 nusmv_st dout 62 on_failure_script_quits 61 open path 61 output_order_file 24 partition method 25 pp list 22 reorder_method 49 sat solver 41 shell _char 61 showed_states 42 verbose level 21 write_order_dumps_bits 23 71 Index Symbols nusmvrc 64 AG 64 bmc 65 bmc k 65 coi 64 cpp 64 cp cp t 65 ctt 64 dynamic 64 f 64 he lp 63 h 63 ic 64 ii 64 ils 64 int 64 is 64 iwls95preorder 65 iwls95 cpt 65 i iv file 64 load cmd file 64 1p 64 mono 65 m method 65 noaffinity 65 n idx 64 obm bmile 64 ofmfm_file 64 o ov file 64 pre pps 64 reorder 64 r 64 thresh cp t 65 v verbose level 63 FAIRNESS declarations 14 IVAR declaration 9 VAR declaration 9 running 14 temp ord 24 72 7 nusmvre 64 A administration commands 52 Array Variables 20 B Basic Trace Explainer 46 batch running NUSMV 63 C case expressions 7 Commands for Bounded Model Check ing 31 comments in NUSMV language 6 compassion constraints 14 CTL Specifications 15 D DD package interface 48 DEFINE declarations 11 Displaying Traces 44 E expressions 6 F fair e
55. ile 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 to guarantee that dead lock 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_fair_states Prints out the number of fair states Command print fair_states h v 27 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 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_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 A ctl expr to be checked can be specified at command line using option p Alternatively option
56. ion takes the union of two sets If either argument is a number or a symbolic value instead of a set it is coerced to a singleton set 2 1 2 Next Expressions While simple expressions can represent sets of states next expressions relate current and next state variables to express transitions in the FSM The structure of next ex pressions is similar to the structure of simple expressions See Section 2 1 1 simple expressions page 6 The difference is that next expression allow to refer to next state variables The grammar is depicted below next_expr atom 5 a symbolic constant number 7 a numeric constant TRUE The boolean constant 1 FALSE The boolean constant 0 var_id a Variable identifier next_expr next simple_expr next value of an expression I next_expr 7 logical not next_expr amp next_expr 7 logical and next_expr next_expr 7 logical or next_expr xor next_expr 7 logical exclusive or next_expr gt next_expr 7 logical implication next_expr lt gt next_expr 7 logical equivalence next_expr next_expr 7 equality next_expr next_expr 7 inequality next_expr lt next_expr 7 less than next_expr gt next_expr 7 Greater than next_expr lt next_expr less than or equal next_expr gt next_expr 7 greater than or equal next_expr next_expr 7 integer addition next_expr next_expr 7 integer subtrac
57. ions 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 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 J range number number 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 p requires that for all paths starting from a state property p 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 eE 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 eA p BU m n q requires that for all paths starting from a state prop erty q holds in a future time inst
58. l 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 fil Sets the environment variable input _file to model fi le 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 processors 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 This command is responsible of the instantiation of modules and processes The instantiation is performed by substituting the actual parameters for the formal parameters and then by prefixing the result via the instance name show_vars Shows model s symbolic variables and their val Command ues show vars h s i m o output file Prints symbolic input and state variables of the model with their range of values as defi
59. les gt A variable environment is maintained by the command interpreter The set com mand 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 filename 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 NUSMVEC Command Options lt file_name gt File to be searched 3 9 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 build ing the transition relation The value of environment variables can be inspected and modified with the set command Environment variables can be either logical or util ity 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 pr
60. lugins page 46 which can be used to display traces in the system Once a trace has been generated by NUSMV it is printed to stdout using the trace explanation plugin which has been set as the current default The command show_traces see Section 3 4 Simulation Commands page 41 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 3 5 3 Trace Plugin Commands The following commands relate to the plugins which are available in NUSMV show_plugins Shows the available trace explanation plug Command ins show plugins h n plugin no a 44 Command Options n plugin no Shows the plugin with the index number equal to plugin no a Shows all the available plugins Shows the available plugins that can be used to display a trace which has been generated by NUSMV 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 O show_traces Shows the
61. m two given set of states MAX alpha beta MIN alpha beta Properties of the above form can be specified in the input file via the keyword COMPUTE or directly at command line using option p 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 Command Options m Pipes the output generated by the command in process ing COMPUTEs to the program specified by the PAG ER shell variable 1f defined else through the UNIX command more 0o output file Writes the output generated by the command in processing COMPUTEs to the file output file p A COMPUTE formula to be checked context is the mod compute expr ule instance name which the variables in compute expr IN context must be evaluated in n number Computes only the property with index number add_property Adds a property to the list of properties add property i t c 1 1 i 9 IN context 30 P Command formula Adds a property in the list of properties It is possible to insert LTL CTL INVAR and quantitative COMPUTE properties Every newly inserted property is initialized to unchecked A type option must be given to properly execute the command Command Options Adds a CTL property I Adds an LTL property i Adds an INVAR property q Adds a quantitative COMPUTE property
62. me as a symbolic constant Such an ambiguity is flagged by the interpreter as an error The order of parsing precedence for operators from high to low is Operators of equal precedence associate to the left except gt that associates to the right Parentheses may be used to group expressions Case Expressions A case expression has the following syntax case_simple_expr case simple_expr simple_expr simple_expr simple_expr simple_expr simple_expr esac A case_simple_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 1 Thus if simple_expr on the left side is true then the result is the corresponding simple_expr on the right side If none of the expressions on the left hand side evaluates to 1 the result of the case_expression is the numeric value 1 It is an error for any expression on the left hand side to return a value other than the truth values 0 or 1 Set Expressions A set expression has the following syntax set_expr set_elem set_elem set definition simple_expr in simple_expr set inclusion test simple _expr union simple_expr 77 set union set_elem simple_expr A set can be defined by enumerating its elements inside curly braces The inclusion operator in tests a value for membership in a set The union operator un
63. ms model checking of invariants Command check_invar h m o output file n number p invar expr IN context 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 invariant 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 Command Options m 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 o output file Writes the output generated by the command in processing INVARSPEC s to the file output file p invar expr The command line specified invariant formula to be verified IN context context is the module instance name which the variabl
64. ncluded by using the same syntax as regular NUSMV files That is by starting the line with 2 4 2 Scalar Variables A variable which has a finite range of values that it can take is encoded as a set of boolean variables These boolean variables represent the binary equivalents of all the possible values 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 to not only 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 actu ally used to encode it are grouped together in the BDD Variables which are grouped together will always remain next to each other in the BDD 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 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 that specific bit variables are placed elsewhere in the order ing This is achieved by first specifying the scalar variable name in the desired lo
65. ned in the input file 22 Command Options 8 Prints only state variables i Prints only input variables 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 encode_variables Builds the BDD variables necessary to Command compile the model into a BDD encode variables h i order file Generates the boolean BDD variables and the ADD needed to encode proposi tionally 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 hierar chy The input order file can be partial and can contain variables not declared in the model Variables not declared in the model are simply discarded Variables de clared 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 order ing Command Options i order fil 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 input_order file Environment Variable Indicates the file name containing the variable
66. nt out grant in amp el grant out MODULE main VAR cl cell In this example the name the ce11 module has been instantiated to is passed to the submodule element In the main module declaring c1 to be an instance of mod ule cell and defining above token in in module e2 really amounts to defin ing the symbol c1 token in When you in the ce11 module declare el to be an instance of module element and you define grant out in module el to be below grant out you are really defining it to be the symbol c1 grant out 2 2 11 The main module The syntax of a NUSMV program is program module_1 module_2 module_n There must be one module with the name main and no formal parameters The module main is the one evaluated by the interpreter 2 2 12 Processes Processes are used to model interleaving concurrency A process is a module which is instantiated using the keyword process see Section 2 2 1 state variables page 9 The program executes a step by non deterministically choosing a process then execut ing 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 Each instance of a process has a special boolean variable associated with it called running The value of this variable is 1 if and only if the process instance is currently selected for execution A process may run only when its parent is running In ad
67. ntation of symmetric sifting It is similar to sifting with one ad dition 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 symmetry_sift_converge The symmetry_sift method is iterated until no further improvement is obtained 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 window 2 3 4 converge The window 2 3 4 method is iterated until no further improvement is obtained group sift This method is similar to symmetry sift but uses more general criteria to create groups group sift_converge The group sift method is iterated until no further improvement is obtained annealing This method is an implementation of simu lated annealing for variable ordering This method is po tentially very slow genetic This method is an implementation of a genetic al gorithm for variable ordering This method is potentially very slow 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 51 e linear This method is a combination of sifting
68. o2 echo Hi echo NuSMV 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 NuSMV gt alias foo echo print_bddistats 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 o filename a lt string gt Echoes the specified string either to standard output or to filename if the op tion o is specified Command Options 53 o 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 instead of overwritting it Use only with the option o help Provides on line information on commands Command help a h lt command gt If invoked with no arguments help 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 previou
69. ogress of optimization on_failure_script_quits Environment Variable 60 When a non fatal error occurs during the interactive mode the interactive in terpreter simply 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 be haviour 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 seript 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 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 csh can be used This method is enabled with the set filec command The csh file completion 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
70. omly picks a state from the set of initial states F 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 state variables un changed 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 41 a Displays all state variables changed and unchanged with re spect to a previous item in an interactive picking This op tion works only if the 1 options has been specified C Uses constraints to restrict the set of initial states in constraints which the state has to be picked constraints must be enclosed between double quotes showed_states Environment Variable Controls the maximum number of states showed during an interactive simulation session Possible values are integers from 1 to 100 The default value is 25 simulate Performs a simulation from the current selected Command State simulate h p v r i a c constraints steps Generates a sequence of at most st eps 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 run the simulation in three ways according to different command line policies deterministic the default mode random and interactive The
71. onment variables enable_reorder and reorder_method are set then the reordering of variables is performed accordingly This command simulates the batch behavior of NUSMV and then returns the control to the interactive shell Command Options i model fil Sets the environment variable input_file to file model file and reads the model from file model file m Method Sets the environment variable partitionmethod to Method and uses it as partitioning method 3 2 Commands for Checking Specifications The following commands allow for the BDD based model checking of a NUSMV model 26 compute_reachable Computes the set of reachable states Command compute reachable h Computes the set of reachable states The result is then used to simplify im age and preimage computations This can result in improved performances for models with sparse state spaces Sometimes this option may slow down the per formances because the computation of reachable states may be very expensive The environment variable forward_search is set during the execution of this command print_reachable_states Prints out the number of reachable Command states print_ reachable states h v 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 check_fsm Checks the transition relation for totality Command check_fsm h m o output f
72. ort the common parts inside a module declaration The syntax of an ISA declaration is as follows isa_declaration ISA atom where atom 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 refer enced by an ISA command is replaced to the ISA declaration 11 2 2 9 MODULE declarations A module is an encapsulated collection of declarations Once defined a module can be reused as many times as necessary Modules can also be so that each instance of a module can refer to different data values A module can contain instances of other modules allowing a structural hierarchy to be built The syntax of a module declaration is as follows module MODULE atom atom atom atom var_declaration ivar_declaration assign_declaration trans_declaration init_declaration invar_declaration spec_declaration checkinvar_declaration ltlspec_declaration compute_declaration fairness declaration define_declaration isa_declaration The atom immediately following the keyword MODULE is the name associated with the module Module names are drawn from a separate name space from other names in the program and hence may clash with names of variables and definitions The optional list of atoms in parentheses are the formal parameters of the module Whenever these parameters occur in expressions within the module they are replaced b
73. ot 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 gener ated only by commands which do not use incremental algorithms bmc_setup Builds the model in a Boolean Epression for Command mat bmc setup h You must call this command before use any other bmc related command Only one call per session is required go_bmc Initializes the system for the BMC verification Command 31 go_bmc h This command initializes the system for verification It is equivalent to the com mand 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 check_ItIlspec_bme Checks the given LTL specification or Command all LTL specifications if no formula is given Checking pa rameters are the maximum length and the loopback value check_ltlspec bmc h n idx p formula IN context 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
74. 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 variables are printed next It then prints the set of inputs which cause the transition to a new state 1f 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 for each input var being printed i INPUT_VARi VALUE gt State RACE_NO STATE_NO lt for each state var being printed j STATE_VARj VALUE for each combinatorial constant being printed k CONSTANTk VALUE 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 3 6 2 States Variables Table This trace plugin prints out the trace as a table either with the states on each row
75. r simple_expr It is an error for the expression to contain the next operator or to yield any value other than 0 or 1 If there is more than one INVAR declaration the invariant set is the conjunction of all of the INVAR declarations 2 2 7 DEFINE declarations In order to make descriptions more concise a symbol can be associated with a com monly expression The syntax for this kind of declaration is define_declaration DEFINE atom simple_expr atom simple_expr atom simple_expr Whenever an identifier referring to the symbol on the left hand side of the in a DEFINE occurs in an expression it is replaced by the expression on the right hand side The expression on the right hand side is always evaluated in its context see Sec tion 2 2 9 MODULE declarations page 12 for an explanation of contexts Forward references to defined symbols are allowed but circular definitions are not allowed and result in an error Itis not possible to assign values to defined symbols non deterministically Another difference between defined symbols and variables is that while variables are statically typed definitions are not 2 2 8 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 imp
76. roup 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 Alur and T Henzinger New Brunswick NJ 1996 Som98 F Somenzi Cudd Cu decision diagram package release 2 2 0 In Department of Electrical and Computer Engineering University of Col orado at Boulder May 1998 67 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 re served words The list of the new reserved words 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 T B LTLSPEC It is used to introduce LTL specifications INVARSPEC It is used to introduce invariant specifications IVAR It is used to introduce input variables JUSTICE It is used to introduce justice fairness constraints COMPASSION It is used to introduce compassion fairness constraints The IMPLEMENTS INPUT OUTPUT statements are not supported by NUSMV They are parsed from the input file but are internally ignored NuSMV differ
77. s commands and their event numbers This is 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 sub stitution mechanism It enables you to reuse words from previously typed com mands The default history substitution character is the is default for shell es capes 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 54 Command Options vO Initial word of last command in n th argument of last command Last argument of last command All but initial word of last command Last command Last command beginning with stuf Repe
78. s from CMU SMV also in the controls that are performed on the input formulas Several formulas that are valid for CMU SMV but that have no clear semantics are not accepted by NUSMV In particular e It is no longer possible to write formulas containing nested next TRANS next alpha next beta next gamma gt delta e Itis 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 assignments and with the statements INVAR and INIT INVAR next alpha amp beta INIT next beta gt alpha 68 ASSIGN delta alpha amp next gamma normal assignments init gamma alpha amp next delta init assignments It is no longer possible to write SPEC FAIRNESS statements containing next FAIRNESS next running SPEC next x amp y The check for circular dependencies among variables has been done more re strictive 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 f y 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
79. s 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 ES04 can build the base and induction steps on many states and transitions As a result the second algorithm is more powerful 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 k max _length maxtength 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 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 On ind
80. s more general criteria to create groups group _sift_convergEhe group_sift method is iterated until no further improvement is obtained annealing This method is an implementation of simulated an nealing for variable ordering This method is poten tially very slow genetic This method is an implementation of a genetic algo rithm for variable ordering This method is poten tially very slow exact This method implements a dynamic programming approach to exact reordering It only stores one BDD at a time Therefore it is relatively efficient in terms of memory Compared to other reordering strategies itis very slow and is not recommended for more than 16 boolean variables linear This method is a combination of sifting and linear transformations linear_conv The linear method is iterated until no further im provement is obtained dynamic_var_ordering Deals with the dynamic variable Command ordering dynamic_var_ordering d e lt method gt f lt method gt h Controls the application and the modalities of dynamic variable ordering Dy namic 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 dy namic ordering is displayed At most one of the options e 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
81. s 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 69 Command Index see bang 52 32 add_property 30 alias 53 bmc_setup 31 bmc_simulate 41 build_model 24 check_fsm 27 check_invar bmc inc 39 check_invar_bmc 38 check_invar 29 check_1tlspec_bmc_inc 36 c c g Cc heck_1t1spec_bmc_onephb 33 heck 1t1spec bmc 32 heck_1t1spec 29 heck_spec 28 compute_reachable 27 compute 30 dynamic_var_ordering 50 echo 53 encode_variables 23 flatten _hierarchy 22 gen_invar_bmc 39 gen_lt1lspec_bmc_onepb 35 gen_ltlspec_bmc 34 go_bme 31 goto state 44 go 26 help 54 history 54 pick_state 41 print_bdd_stats 52 print_current state 44 print_fair_states 27 print_fair_transitions 28 print_iwls95options 26 print_reachable_states 27 print_usage 55 process _model 26 70 quit 55 read_model 22 read_t race 46 reset 55 set_bdd_parameters 52 set 55 show _plugins 44 show_t races 45 show_vars 22 simulate 42 source 57 time 58 unalias 58 unset 60 usage 60 which 60 write_order 23 Variable Index NuSMV_LIBRARY_PATH 61 64 affinity 25 ag only search 28 autoexec 60 bmc_dimacs_filename 37 bmc_inc_invar _alg 40 bmc_invar_alg 40 bmc_invar_dimacs_filename 40 bmc_length 37 bmc_loopback 37 check_fsm 27 conj_part_threshold 25 default_trace_plu
82. se 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 32 o filename e the symbol X which means no loopback e thesymbol 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 f model name without path part k current problem bound 21 current loopback value On index of the currently processed formula in the prop erty database e 00 the character check_Itlspec_bmc_onepb Checks the given LTL specifica Command tion or all LTL specifications if no formula is given Check ing parameters are the single problem bound and the loop back value check_1t1spec bmc onepb h n idx p formula k length 1 loopback o filename IN context As command check_1t1spec_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 p formula IN index is the numeric index of a valid LTL specification for mula actually located in the properties database The validity of index value is checked out by the system Checks the formula specified on th
83. short smv flatten_hierarchy build variables buildmodel compute_fairness In this case O gets source 3 1 getstest 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 parame ters Therefore if you type st x short smv bozo you will execute readmodel i short smv flatten_hierarchy build variables buildmodel compute_fairness To pass the x switch or any other switch to source when the script uses positional 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 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 alias Command unalias h lt alias names gt Removes the definition of an alias specified via the alias command Command Options 58 lt alias names gt Aliases to be removed 59 unset Unsets an environment variable Command unset h lt variab
84. simple_expr simple_expr Mt y process atom simple_expr simple_expr val atom number A variable of type boolean can take on the numerical values 0 and 1 representing false and true respectively In the case of a list of values enclosed in quotes where atoms are taken to be symbolic constants the variable is a scalar which take any of these values In the case of an array declaration the first simple_expr is the lower bound on the subscript and the second simple _expr is the upper bound Both of these expressions must evaluate to integer constants Finally an atom optionally followed by a list of expressions in parentheses indicates an instance of module atom see Section 2 2 9 MODULE declarations page 12 The keyword causes the module to be instantiated as an asynchronous process see Section 2 2 12 processes page 14 2 2 2 Input Variables IVAR input variables are used to label transitions of the Finite State Machine The syntax for the declaration of input variables is the following ivar_declaration IVAR at om type 7 at om type The type associated with a variable declaration can be either a boolean a scalar a user defined module or an array of any of these including arrays of arrays see Sec tion 2 2 1 state variables page 9 2 2 3 ASSIGN declarations An assignment has the form assign_declaration ASSIGN assign_body assign_
85. state variables then it gets displayed in a seperate combinatorial section Since the values of any such constants depend on one or more inputs the initial state does not contain this section either 43 Traces are created by NUSMV when a formula is found to be false they are also generated as a result of a simulation Section 3 4 Simulation Commands page 41 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 3 5 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 st ate_label 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 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 variables of the current state 3 5 2 Displaying Traces NUSMV comes with three trace plugins see Section 3 6 Trace P
86. t is not permitted to specify just the 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 20 Chapter 3 Running NuSMV interactively The main interaction mode of NUSMV is through an interactive shell In this mode NUS MV enters a read eval print loop The user can activate the various NUSMV com putation 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 in teractive 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 NuSMV gt A NUSMV command is a sequence of words The first word specifies the com mand 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 envi ronment varia
87. ted in 34 k max _length 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 variable bmc_length value is considered in stead 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 anegative 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 f model name without path part k current problem bound 21 current loopback value On index of the currently processed formula in the prop erty database e 00 the character gen_Itlspec_bmc_onepb Dumps into one dimacs file the Command problem generated for the giv
88. tion next_expr next_expr 7 integer multiplication next_expr next_expr 7 integer division next_expr mod next_expr 7 integer remainder set_next_expr 7 a set next_expression case_next_expr 7 a case expression set_next_expr and case_next expr are the same as set_simple _expr see Section 2 1 1 set expressions page 7 and case_simple_expr see Section 2 1 1 case expressions page 7 respectively with the replacement of simple with next The only additional production is next simple expr which allows to shift all the variables in simple_expr to the next state The next operator distributes on every operator For instance the formula next A B C is a shorthand for the formula next A amp next B next C Itis an error if in the scope of the next operator occurs another next operator 2 2 Definition of the FSM 2 2 1 State Variables A state of the model is an assignment of values to a set of state variables These variables and also instances of modules are declared by the notation var_declaration VAR at om type at om type The type associated with a variable declaration can be either a boolean a scalar a user defined module or an array of any of these including arrays of arrays Type Specifiers A type specifier has the syntax type boolean MAO Fa AA ss VAL TN number number array number number of type atom
89. tions if no for mula is given Generation and dumping parameters are the maximum bound and the loopback value gen 1t1spec ome h n idx p formula IN context k max_length 1 loopback o filename This command generates one or more problems and dumps each problem 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 maxJength pa rameter or by its default value stored in the environment variable bmc_length Each dumped problem also depends on the loopback you can explicitly spec ify 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 other wise the default value stored in the environment variable bmc_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 The validity 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 evalua
90. traces generated in a NuSMV ses Command sion show traces h v t m o output filel p plugin no Ta trace number Shows the traces currently stored in system memory if any By default 1t shows the last generated trace if any Command Options v Verbosely prints traces content all state variables 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 E Prints only the total number of currently stored traces a Prints all the currently stored traces m Pipes the output through 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 p plugin no Uses the specified trace plugin to display the trace 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 printed 45 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_trac h i file
91. ts command Command Options s Prints the BDD parameter and statistics after the modifica tion 3 8 Administration Commands This section describes the administrative commands offered by the interactive shell of NUSMV shelllcommand Command 52 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 cur rent 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 com mand 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 from immediate ex pansion it must be preceded by a when entering the alias For example NuSMV gt alias read readmodel i l smv set input order file S l ord NuSMV gt read short will create an alias read execute read_model i short smv set input_order file short ord And again NuSMV gt alias ech
92. xecution paths 14 fairness constraints 14 fairness constraints declaration 14 fair paths 14 I Identifiers 13 infinity 18 INIT declaration 10 Input File Syntax 18 input variables syntax 9 Inspecting Traces 44 interactive running NUSMV 21 interactive shell 21 interface to DD Package 48 Vv INVAR declaration 11 var_id 7 ISA declarations 11 X J XML Format Printer 47 justice constraints 14 XML Format Reader 48 L LTL Specifications 16 M main module 14 master nusmvrc 64 model compiling 22 model parsing 22 model reading 22 MODULE declarations 12 N Next Expressions 8 next expressions 8 O options 63 P process 14 processes 14 process keyword 14 R Real Time CTL Specifications and Com putations 17 S Scalar Variables 19 self 13 set expressions 7 Shell configuration Variables 60 simple expressions 6 Simulation Commands 41 States Variables Table 47 state variables syntax 9 T Trace Plugin Commands 44 Trace Plugins 46 Traces 43 TRANS declarations 10 type declaration 9 type specifiers 9 73
93. y the actual parameters which are supplied when the module is instantiated see below An instance of a module is created using the VAR declaration see Section 2 2 1 state variables page 9 This declaration supplies a name for the instance and also a list of actual parameters which are assigned to the formal parameters in the module definition An actual parameter can be any legal expression It is an error if the number of actual parameters is different from the number of formal parameters The semantic of module instantiation is similar to call by reference For example in the following program fragment MODULE main VAR a boolean b foe lays MODULE foo x ASSIGN x 1 the variable a is assigned the value 1 This distinguishes the call by reference mecha nism from a call by value scheme Now consider the following program MODULE main DEFINE 12 MODULE bar x DEFINE a 1 Y Xi In this program the value of y is 0 On the other hand using a call by name mech anism the value of y would be 1 since a would be substituted as an expression for Xx Forward references to module names are allowed but circular references are not and result in an error 2 2 10 Identifiers An id or identifier is an expression which references an object Objects are instances of modules variables and defined symbols The syntax of an identifier is as follows id atom

Download Pdf Manuals

Related Search

Related Contents

HP Imaging and Printing Security Center White Paper    American Power Conversion 240-320kW 480V User's Manual  Guía del usuario de la impresora láser Phaser 5500  Ug Manuel d`utilisation    

Copyright © All rights reserved. Failed to retrieve file