-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathNEWS
1728 lines (1228 loc) · 65.9 KB
/
NEWS
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
********************** NuSMV 2.6.0 (2015/10/14) **********************
This is a major release that comes after four years passed working
under the surface. The release provides some new features, many bug
fixes and optimizations, and substantial differences in the software
architecture and building system.
The main changes are:
o Splitting source code in two main components: the Core NuSMV library
and the NuSMV Shell. This split enables for a much easier
integration with other tools, and for a possible reorganization of
the shell in the future. This change breaks backward compatibility
of APIs and source code integration.
o Switch to cmake (http://cmake.org) for building source code. This
allows for a much faster build wrt previously used GNU Autotools,
higher portability, and lower maintenance costs.
The bug fixes and new features are described below.
Please consider switching to nuXmv (https://nuxmv.fbk.eu). nuXmv
extends NuSMV along two directions. For the verification of
finite-state synchronous designs, nuXmv features strong engines based
on state-of-the-art SAT-based algorithms (see the final results at the
Hardware Model Checking Competition 2015 at
http://fmv.jku.at/hwmcc15/). For the verification of infinite-state
synchronous designs, nuXmv features state-of-the-art SMT-based
verification techniques, implemented through a tight integration with
the MathSAT5 SMT solver (http://mathsat.fbk.eu). For details about
license terms see nuxmv's web pages.
----------------------------------------------------------------------
* New features
----------------------------------------------------------------------
o Language
- NuSMV language was extended to support the 'min', 'max', and 'abs'
operators.
o System commands
- Added four new commands 'check_pslspec_bmc',
'check_pslspec_bmc_inc', 'check_pslspec_sbmc',
'check_pslspec_sbmc_inc'. They handle the options -b (use bmc),
-s (use sbmc), -i (use incremental algorithms), -c and -N
previously handled by the single command 'check_pslspec', that
now is specific for bdd-based model checking.
- Added command 'convert_property_to_invar' which converts LTL
(CTL) properties in the form "G (AG) next-expr" to INVARSPEC.
- Command 'print_fair_transitions' now provides exact information
about the fair-transitions, and not about state-input pairs. The
command provides support also for dumping information in DOT and
CSV formats, which is useful to visually "inspect" the FSM.
o Command line options and system variables
- New variable 'boolean_conversion_uses_predicate_normalization':
When set to true, performs predicate normalization of any
expression before performing the booleanization. There are cases
where enabling this option pays off dramatically, however it
might be expensive on other cases since the normalization of the
predicates may blow up the formula. Set to false by default.
- New variable 'ltl2smv_single_justice': When set to true, the
tableau construction builds a degeneralized (single fairness)
symbolic encoding of the Buchi automaton within ltl2smv instead
of the default generalized (multiple fairness) one. Added
command line option -s to ltl2smv, to enable the emit of a
single justice tableau.
- New variables 'pp_cpp_path' and 'pp_m4_path' to allow users to
explicitly set the paths on the file system of 'cpp' and 'm4'
preprocessors.
o Improvements (internal)
- Introduced infinite-width words. In previous versione, maximum
width was limited to 64.
- RBC inlining now uses a LRU cache which always improves BMC
performances (up to 30% according to our experiments).
- Many functions were rewritten to avoid recursion. This allows
for a faster executions with more limited use of stack.
- Command 'help' no longer relies on external files for accessing
the commands' documentation. This simplify the usage.
----------------------------------------------------------------------
* Bug fixes
----------------------------------------------------------------------
There were about 270 bug fixes, most of them were minor, but some were
major issues. Here is the list of the most critical bug fixed:
* Fixes in type checker.
* Fixed some problems related to array handling appearing in some
corner case use.
* Fixed several issues with portability, in particular to allow
compilation of core libraray with msvc-2010.
----------------------------------------------------------------------
* Documentation
----------------------------------------------------------------------
Programmer's manual is now generated with doxygen
(http://www.doxygen.org). For this reason documentation of all
functions has been moved to the place of declaration (i.e. to header
files). Previous documentation system has been dropped.
----------------------------------------------------------------------
* Source Code
----------------------------------------------------------------------
Top level directory has been renamed from 'nusmv' to "NuSMV". Source
code is now located in "NuSMV/code/nusmv" with "NuSMV/code" in the
inclusion path to allow for explicit inclusion of header files in the
form "nusmv/..." which makes explicit where each header files is
imported from.
Core library and shell have been clearly split into
"NuSMV/code/nusmv/{core,shell}", and it is now possible to compile the
library standalone (option ENABLE_SHELL=OFF at configuration time).
********************** NuSMV 2.5.4 (2011/10/31) **********************
This is a minor release that provides some new features, some internal
improvements, and many bug fixes.
----------------------------------------------------------------------
* New features
----------------------------------------------------------------------
o System commands
- Added two new commands 'bmc_pick_state' and 'bmc_inc_simulate'
for interactive simulations using SAT;
- Added option "-n "name"" to command add_property to specify the name
- Removed unsupported options "-o" and "-1" from the documentation
command 'check_ltlspec_sbmc_inc';
o Command line options and system variables
- Added a new system boolean variable 'daggifier_enabled'
(Default set to 1), and a new relative command line option
"-disable_daggifier" to enable/disable the daggifier while
dumping SMV models.
o Improvements (internal)
- Performed several refactorings: added wff package and a few
basic data structures (e.g. utils/Pair.c, utils/Triple.c);
- The simplification of the expressions has been improved using
additional simplification rules, the local symbol tables and
pointers sorting;
- Improved iteration over the hash tables elements;
- Improved construction of static BDD var order.
----------------------------------------------------------------------
* Bug fixes
----------------------------------------------------------------------
We fixed about 15 bugs in this version. Many thanks to those users who
reported issues, and helped improving NuSMV.
Here is the list of the most critical bug fixed:
- Fixed a wrong simplification rule within the rbc package;
- Fixed a bug in condition simplification, which was not taking
into account context;
- Fixed a bug in prompt printing that was creating some syncronization
problem with external tools (thanks to Sylvain Soliman from INRIA for
the accurate bug report);
- Fixed a bug in the trace reader that caused seg-faults;
- Fixed an overflow in the operator swconst;
- Fixed a bug in the command add_property that was wrongly adding a
property P even if P was already used;
- Added some additional checks to trap uncorrect PSL formulae;
- Fixed a linking dependence about the library librbcdag.la in the
Makefile that prevented the creation of linkable library.
----------------------------------------------------------------------
* Documentation
----------------------------------------------------------------------
- The output of -h option for 'check_ltlspec_sbmc_inc',
'bmc_pick_state', 'bmc_inc_simulate', 'add_property',
'daggifier_enabled' commands, and the command line option
'-disable_daggifier' have been updated according to the recent
changes. The User Manual has been updated as well.
********************** NuSMV 2.5.3 (2011/06/16) **********************
This is a minor release that provides many bug fixes, some
internals improvement, and a few new features.
----------------------------------------------------------------------
* New features
----------------------------------------------------------------------
o System commands
- Command 'compute' has been renamed 'check_compute'. Old
command 'compute' is deprecated.
- Command 'clean_bdd_cache' has been renamed 'clean_sexp2bdd_cache'
- Added option -F <format> to command 'show_property', to print in
tabular or xml formats.
- Added options -t and -V to command 'show_vars', to print selected
information about the variables in the model.
- Added option -k <length> to command 'simulate', to make
uniform all simulation commands.
Old syntax 'simulate <length>' is now deprecated.
- Added options -r, -c <simp_constr> and -t <next_constr> to
SAT-based simulation commands, both incremental and non
incremental, in order to be more uniform with regard to the
BDD-based ones.
o Command line options and system variables
- Command line option and system variable 'disable_bdd_cache'
have been renamed to 'disable_sexp2bdd_caching'
- New command line option and system variable
'disable_syntactic_checks' which can improve performances by
skipping checks on input files which are assumed to be
syntactically correct by construction.
- New command line option and system variable
'keep_single_value_vars' to disable an optimization which by
default converts enumerative variables to constants when
their domain contains only a single element.
- New system variable 'default_simulation_steps' is used by
simulation commands. Command 'simulate' now considers it if
simulation steps are not specified; command 'bmc_simulate'
considers it instead of variable 'bmc_length'.
- New system variable 'parser_is_lax' can be used to force the
parser to try completing parsing even with syntactic errors,
reporting all found errors at the end.
- New system variable 'prop_print_method' can be used to select
how properties are printed out.
o Improvements (internals)
- New algorithms to compute COI (Cone of Influence) have been
implemented.
- Encoding of scalar variables have been improved to fit with
the BDD variable ordering. The new encoding proved to improve
performances in many general cases.
- Fixed BDD encoding of variables to trigger less re-orderings.
- Some RBC operations now use much less stack space.
- New Symbol Table implementation, with huge performances and
memory improvements.
- New system-widely-used NodeList implementation, which reduces
global NuSMV memory usage.
----------------------------------------------------------------------
* Bug fixes
----------------------------------------------------------------------
About 30 bugs were fixed in this version. Many thanks to those
users who reported issues, and helped improving NuSMV.
Here the most critical bug fixes are listed:
- Fixed a bug in CTL counter example generation, which was
surfacing in some cases.
- Fixed a bug which was triggered when adding incorrect properties
to the properties database.
- Fixed bug in command 'bmc_pick_state' when used with COI.
- Fixed compilation errors on recent GNU/Linux distributions
- Fixed compilation errors under Darwin.
- Fixed many memory leaks.
----------------------------------------------------------------------
* Documentation
----------------------------------------------------------------------
- Added a FAQ containing a set of most frequently asked questions
about NuSMV, and the SMV language.
- Added to the User Manual the description of some missing
operators like 'sizeof'
********************** NuSMV 2.5.2 (2010/10/29) **********************
This is a minor release that provides a few new features, and several
bug fixes.
----------------------------------------------------------------------
* New minor features
----------------------------------------------------------------------
o SMV grammar
- Array indices in PSL expressions can now be generic expressions,
like in normal SMV grammar. Previously, only constant numbers
were supported.
o Environment variables
- Some traces related environment variables have been renamed to
improve usability:
* counter_examples_hiding_prefix -> traces_hiding_prefix
* counter_examples_show_re -> traces_regexp
* show_defines_in_traces -> traces_show_defines
* trace_show_defines_with_next -> traces_show_defines_with_next
----------------------------------------------------------------------
* Bug fixes
----------------------------------------------------------------------
- Fixed a problem, causing segfault, in the way the COUNT operator
was handled. Thanks to Alexandre Arnold <a.arnold.fr AT gmail.com>
for reporing the issue.
- Fixed an assertion violation occuring in interactive simulation
when an incorrect constraint was given to restrict the number of
possible next states to be shown to the user.
- Fixed three problems in the trace visualization:
* Word constants in decimal format were not properly printed
under windows 32bit machines.
* In some cases the option specifiying the format for printing
word constants was ignored.
* In some cases the options specifying the filters over signals
were ignored.
- Fixed a problem of command execute_partial_traces that was not
reporting any message to the user for non re-executable traces.
- Fixed a bug in command write_coi_model which was generating
an incorrect model for properties with an empty coi.
- Fixed a problem of the "echo" command that was no longer
expanding references to environment variables.
- Fixed a problem that was causing NuSMV to crash when handling
command line options related to BMC and no SAT solver was
linked/detected at compile time.
- Fixed several other small bugs on internals not affecting the the
normal user interacting with NuSMV via the shell or in batch mode.
********************** NuSMV 2.5.1 (2010/10/01) **********************
This is a minor release that provides most notably a major change in
the language. It features also several bug fixes (more than 30), a few
new operators in the SMV language, some new command line options, a
few optimizations, and some fixes in the documentation.
The main changes are listed below. For details please refer to the
ChangeLog.
----------------------------------------------------------------------
* New features
----------------------------------------------------------------------
o SMV grammar
- The new version 2.5.1 makes a strong distinction between
integers and boolean types. This breaks backward compatibility,
since integers values cannot be used anymore where booleans are
used, and vice-versa.
To mitigate the problems that may arise from this change, new
operators have been introduced (e.g., the "count" operator), and
the signature of existing ones have been extended (e.g., the
"toint" operator) to allow to cope with no longer supported
expressions.
Thus, the following typical snipped of code are no longer
accepted:
1. Given N boolean expressions b1, ..., bN, to specify that at most
M out of N must be TRUE, before it was possible to write
(b1 + b2 + ... + bN) <= M.
From 2.5.1 on this condition has to be specified as
count(b1,b2,...,bN) <= M.
2. Constant "1" cannot be used anymore as default condition into
a "case" statement. Thus the following code snipped
case
b1 : e1;
...
bN : eN;
1 : eD; -- expression for default condition
esac
has to be rewritten as
case
b1 : e1;
...
bN : eN;
TRUE : eD; -- expression for default condition
esac
In this snippet b1, ..., bN are boolean expressions
representing the conditions, and e1, ..., eN, eD are the
expressions the case construct evaluates to when the
corresponding condition evaluates to TRUE.
- Added the count() operator, which takes a list of boolean
expressions and returns the number of expressions that evaluates
to TRUE.
- Operator toint() now supports word type expressions.
o System commands
- Command "show_vars" no longer prints by default all the
values of an enumerative variable, and truncates it if too
long to be printed, and reports the number of the remaining
elements. The new command line option "-v" for this command
enables the previous behavior.
- Command "set" now accepts "0" and "1" when setting values of
boolean system variables. Now "set <var> 0" has the same
effect as "unset <var>", and "set <var> 1" has the same
effect as "set <var>".
o Command line options
- The backward-compatibility option "-old" has been extended to
make NuSMV accept syntactical construct "1" in "case" conditions
to specify the default condition. This is intended to mitigate
the impact of the strong type distinction between integer and
boolean types, in existing SMV models. This feature will be
removed in future releases.
----------------------------------------------------------------------
* Bug fixes
----------------------------------------------------------------------
- Garbage in dimacs file under Windows platforms. Thanks to Luca
Zanetti <luzanetti AT fbk.eu> for repoting it.
- Standard output and error, and the shell's prompt are now in
sync under Windows. Thanks to Aleksey Nogin <anogin AT hrl.com>
for the report and for providing a patch.
- The parser can handle now comments with length greater than
16381 characters.
- The type checker can now successfully detect ambiguities in
identifiers which refer to both enumerative literals and
variable names.
- Fixed a crash which was in some cases occurring when extracting
the counter-example of a false property, with cone of influence
was enabled.
- Fixed some memory leaks.
- Fixed several portability issues.
********************** NuSMV 2.5.0 (2010/05/17) **********************
Version 2.5.0 is a major release which provides new features, many
optimizations and bug fixes, and an extensive reorganization of the
source code and API.
Many changes were driven by projects which involved
FBK, like:
- COCONUT, COrrect-by-CONstrUcTion Workbench for Design and
Verification of Embedded Systems
(http://www.coconut-project.eu/).
COCONUT was founded by EU FP7-2007-IST-1-217069.
- COMPASS, COrrectness, Modeling and Performance of
Aerospace SystemS (http://compass.informatik.rwth-aachen.de)
- EuRailCheck, European Railways Verification and Validation Tool
(http://es.fbk.eu/projects/eurailcheck).
In all these projects, the core of NuSMV has been improved to deal
with large scalability issues. Several bottlenecks were identified,
and fixed, with particular care about the memory usage.
The main changes are listed below. For details please refer to the
ChangeLog.
----------------------------------------------------------------------
* New features
----------------------------------------------------------------------
o Improvements
- New type "signed word" is introduced
- New type is added to allow signed arithmetic.
Also a few operations related to signed words are
introduced. They are "extend" and two casts - "signed" and
"unsigned". See user manual for more details.
- Added traces re-execution engine. Traces can now be executed
within the model, to check whether or not the trace contains
onlu valid assingments that are feasible in the model.
o SMV grammar
- Properties can now be named in the SMV model.
The syntax for property naming is "NAME pname := expr"
o PSL grammar
- The PSL grammar now supports word operations. All SMV word
operators are supported, made exception for the bit-selection
operator, which has a different syntax in PSL [select(w, h, l)].
See user manual for more details
o System commands
- Added the "bmc_pick_state" command. Similary to "pick_state",
chooses an element from the set of initial states, and makes it
the current state. This must be done in order to proceed with
BMC simulation
- Added the "bmc_inc_simulate" command. Does the same as
"bmc_simulate", but using incremental algorithms.
- Added the "bmc_simulate_check_feasible_constraints" command,
used to check whether or not a given constraint is feasible and
can thus be used as BMC simulation constraint.
- Added the "check_invar_bmc_inc" command, used for checking
invariant specifications using BMC incremental algorithms.
- Added the "check_ltlspec_bmc_inc" command, used for checking
LTL specifications using BMC incremental algorithms.
- Added the "clean_bdd_cache" command. Cleans the cached results
of evaluations of symbolic expressions to ADD and BDD
representations.
- Added the "execute_partial_traces" command, used for incomplete
trace execution
- Added the "execute_traces" command, used for complete trace
execution
- Added the "print_formula" command, which prints a formula in
canonical format.
- Added the "show_dependencies" command, which shows the
dependencies for the given expression
- Added the "write_coi_model" command, which reduces a model using
the Cone Of Influence over a given property and dumps it on a
file.
- Added the "write_flat_model_udg" command, which writes the input
given SMV model in the specified uDraw file
- Added the "write_pred_clusters_model" command, which writes flat
models corresponding to clusters of predicates to file.
- Added the "-P name" command option to all property-checking
commands (check_ctlspec, check_ltlspec, ...). When using this
option, only the property named "name" is checked.
- Added some new command options to the "check_invar" command:
* -s strategy : Force the analysis strategy (Overrides the
"check_invar_strategy" environment
variable). Possible values are {'forward',
'backward', 'forward-backward', 'bdd-bmc'}
* -e heuristic : Force the heuristic in case of
forward-backward strategy (Overrides the
"check_invar_forward_backward_heuristic"
environment variable). Possible values are
{'zigzag', 'smallest'}
* -t number : When using the mixed BDD and BMC approach
specify the heuristic threshold. Overrides
the "check_invar_bddbmc_threshold"
environment variable.
* -k number : When using the mixed BDD and BMC approach
specify the BMC max k. Overrides the
"bmc_length" environment variable
* -j heuristic : Specify the heuristic used to switch from BDD
to BMC (Overrides the
"check_invar_bddbmc_heuristic" environment
variable). Possible values are {'steps',
'size'}
- Added "-k number" options and "-t time" option to the
"compute_reachable" command, which respectively limit the
forward search in number of steps or in execution time.
- Added "-2" and "-n" options to the "echo" command. "-2" prints
the given string to stderr instead of stdout. "-n" does not add
a trailing newline to the printed string.
- Added the "-d" option to the "flatten_hierarchy" command. This
option delays the construction of vars constraints until needed
- Added the "-p" option to the "print_fsm_stats" command, which
prints out the normalized predicates the FSM consists of.
- Added a few command options to the "print_reachable_states"
command:
* -d : Prints the list of reachable states with defines
(Requires -v)
* -f : Prints the formula representing the reachable
states.
* -o filename : Prints the result on the specified filename
instead of on standard output
o Command line options
- Added option "-source sc_file": Executes NuSMV commands from
file sc_file
- Added option "-disable_bdd_cache" to disable bdd reachable
states caching.
- Added option "-bdd_soh heuristics" to set the heuristics to be
used to compute BDD ordering statically by analyzing the input
model.
- Added option "-ojeba alg" to set the algorthim used for
BDD-based language emptiness of Buchi fair transition systems.
o System variables
- System variables are now printed in a lexicographic order when
calling command "set"
- Added system variable "bdd_static_order_heuristics", which sets
the heuristics for guessing a good ordering by analyzing the
input model.
- Added system variable "bmc_inc_invar_alg", which sets the
default algorthim for BMC incremental invariants checking.
- Added system variable "check_invar_bddbmc_heuristic", which sets
the bdd-bmc heuristics to be used when using bdd-bmc BDD
invariants checking strategy
- Added system variable "check_invar_bddbmc_threshold", which sets
the threshold to be used when using bdd-bmc BDD invariants
checking strategy
- Added system variable "check_invar_forward_backward_heuristic",
which sets the heuristics used for forward-backward strategy
when checking invariants using BDD.
- Added system variable "check_invar_strategy", which sets the
strategy to be used for BDD based invariants specifications
checking.
- Added system variable "counter_examples_hiding_prefix". Symbols
names that match this string prefix will be not printed out when
showing a trace
- Addes system variable "counter_examples_show_re". Only symbols
whose names match this regular expression will be printed out
when showing a trace.
- Added system variable "daggifier_counter_threshold",
"daggifier_depth_threshold" and "daggifier_statistics", which
control the model dumper behavior.
- Added system variable "enable_bdd_cache", which determines if
during evaluation of symbolic expression to ADD and BDD
representations the obtained results are cached or not.
- Added system variable "oreg_justice_emptiness_bdd_algorithm",
which sets the algorithm used to determine language emptiness of
a Buchi fair transition system.
- Added system variable "rbc_rbc2cnf_algorithm", which defines the
algorithm used for conversion from RBC to CNF format.
- Added system variable "show_defines_in_traces", which controls
whether defines should be printed as part of a trace or be
skipped
- Added system variable "trace_show_defines_with_next", which
controls wheter defines containing next operator should be
printed as part of a trace or be skipped
- Added system variable "use_coi_size_sorting", which
enables/disables the use of the cone of influence variables set
size for properties sorting, before the verification step.
----------------------------------------------------------------------
* Bug fixes
----------------------------------------------------------------------
- Fixed the precedence of "mod" operator. Now it has the same
precedence as division instead of having precedence
between +/- and shift.
********************** NuSMV 2.4.3 (2007/05/22) **********************
This is a minor release that provides several bug fixes and
commands completion when interactive shell is used.
----------------------------------------------------------------------
* New features
----------------------------------------------------------------------
o User interaction
- Added commands completion functionality to the interactive shell
(requires readline library to be enabled and to be available at
compile time). Thanks to Tivadar Szemethy <tivadar.szemethy AT
vanderbilt.edu> who contributed the code for this feature.
----------------------------------------------------------------------
* Bug fixes
----------------------------------------------------------------------
- Fixed a failure that may occur when model checking LTL formulae
with defines referring directly or indirectly to input variables.
- Fixed a critical bug that made formula (AF p | AF q) being
rewritten as AF (p | q).
- Fixed a critical bug that made NuSMV fail when allocating more
than 4096 BDD variables.
- SBMC was not handling correctly past temporal operators.
- Operator unary minus (-) was not fully handled by type checker
and other components.
- Fixed a bug that allowed the properties database to contain
properties with problems (undefined symbols, type errors, ...).
- Use of keyword "self" as module's actual parameter has been
re-enabled.
- Fixed some memory leaks.
********************** NuSMV 2.4.2 (2007/04/06) **********************
This is a minor release that provides compatibility with 64-bit
architectures, speed improvements, a few extensions to the user
interface and many bug fixes. Latest versions of CUDD, Minisat and
Zchaff are also now used. Overall this release results on average
faster than previous ones.
----------------------------------------------------------------------
* New features
----------------------------------------------------------------------
o Improvements
- Specifications using words are bit-blasted using the circuits
corresponding to the functions occurring in the specification
when SAT based BMC is selected for verification. This enabled
the verification of models out of the scope of previous versions
of NuSMV.
- SAT based BMC encoding now features RBC inlining [ABE04] to
reduce problem size. With RBC inlining enabled, our experiments
showed on average a reduction of total model checking time.
RBC inlining has also been extended to symbolic SEXP encoding
to possibly benefit from its use in BDD based searches.
This inlining is not enabled by default since it does not
provide significant improvements on average, and in some cases
it results in degraded performance.
We remark that inlining might result in a dramatic degrade of
performances in some cases, depending on the nature and structure
of the problem.
[ABE04] P. A. Abdulla, P. Bjesse and N. Eén: Symbolic
Reachability Analysis Based on SAT-Solvers. In Proceedings of
Tools and Algorithms for Construction and Analysis of
Systems, 6th International Conference, TACAS 2000. Pages
411-425. Lecture Notes in Computer Science 1785. Springer.
- SAT based BMC uses an extended version of the efficient RBC to
CNF conversion described in [She04]. The new CNF conversion
leads to smaller CNF than previous one, and to an average
improvement in verification. Thanks to Daniel Sheridan for the
preliminary version of the CNF conversion, and to Gavin Keighren
for the preliminary porting to the new version of NuSMV.
[She04] D. Sheridan. The Optimality of a Fast CNF conversion and
its use with SAT. In Proceedings of the 7th International
Conference on Theory and Applications of Satisfiability
Testing (SAT'2004), 10-13 May 2004, Vancouver, BC, Canada.
- A patched version of CUDD-2.4.1 is now linked to NuSMV. Previous
version was a patched version of CUDD-2.3.0.
- Minisat2-061208 is now linked to NuSMV. Previous version was
Minisat-1.14. By default NuSMV now uses the MiniSAT extended
solver with simplification capabilities enabled.
- New version of Zchaff-2007.3.12 can now be optionally linked to
NuSMV. Previous version was zchaff-2003.12.04.
- NuSMV has been ported to 64-bit architectures. It can run and
compile smoothly on Intel Xeon(TM), AMD Opteron(TM), and Intel
IA64(TM) architectures.
We would like to thank Moshe Vardi, Kim Andrews, Franco M. Bladilo,
and Jan E. Odegard from Rice University for providing us with
cray facilities for testing the porting. The Cray computing
facility at Rice substantially contributed to the completion of
the 64-bit porting of NuSMV.
o User interaction
- Variable 'sexp_inlining' is used to enable/disable inlining
at sexp level. Sexp inlining at the moment is applied only
when BMC is performed. By default Sexp inlining is disabled.
- Option -sin on|off to control new system variable sexp_inlining.
- Variable 'rbc_inlining' is used to enable/disable RBC
inlining before committing a problem to any SAT solver. By
default RBC inlining is enabled.
- Option -rin on|off to control new system variable rbc_inlining.
----------------------------------------------------------------------
* Bug fixes:
----------------------------------------------------------------------
- Fixed a bug that led to cyclic assignments not being correctly
detected. Thanks to Michael Whalen <mwwhalen AT
rockwellcollins com> and Li Zhong <gravityzhong AT gmail
com> for reporting the bug.
- Fixed a critical bug that made the booleanizer cache not take
into account the contexts of booleanized formulae. Thanks
to Jori Dubrovin <jdubrovi AT circuit tcs hut fi>, Tommi
Junttila <Tommi.Junttila AT tkk fi> and Vesa Ojala <vojala
AT circuit tcs hut fi> for reporting the bug.
- Fixed a bug that made ltl2smv fail when expanding DEFINEs
containing input variables.
- Fixed a bug in Incremental SBMC that resulted in false
counterexamples in some cases if the property involved input
variables. Thanks to Tommi Junttila <Tommi.Junttila AT tkk fi>
for reporting the bug and also for providing a fix.
- Fixed associativity of some PSL operators that were not
consistent with the PSL LRM and with the core NuSMV
grammar. Thanks to Andrea Fedeli <andrea.fedeli AT st com> for
notifying us of the problem.
- Applied bug fixes and cleanups suggested by Felix Rauch Valenti
<frauch AT cse unsw edu au>. Valenti and others are working on a
research project in the area of static analysis, i.e. finding
problems (bugs) in C/C++ source code automatically. The research
project is called "Goanna" and uses NuSMV as backend. See
<http://www.ertos.nicta.com.au/research/goanna/>
- Fixed trace plugins that were not correctly working
when words variables were used. Thanks to Vincent Gourcuff
<vincent.gourcuff AT lurpa ens-cachan fr> for reporting the bug.
- Fixed a typo in configure.ac. Thanks to Mark Tuttle
<mark.r.tuttle AT intel com> for reporting the bug.
- Many other bug fixes (see Change Log)
********************** NuSMV 2.4.1 (2006/12/06) **********************
This is a minor release that provides to external contributions and
some extensions to the user interface. Moreover, it fixes many bugs.
----------------------------------------------------------------------
* New features
----------------------------------------------------------------------
o Improvements
- Optimized LTL tableau construction (contributed by Stefano
Tonetta's <tonettas_AT_lu.unisi.ch>) for LTL model checking via
BDDs. The optimization leads to an improvement of performance of
about 30% on average. Moreover, minor low-level optimizations
have been also integrated to the BDD-based LTL model checking,
e.g., it is now possible to reuse (default) previously
computated reachable states while combining the model and the
tableau FSMs.
- When building the scalar fsm, variable ordering is now taken
into account. This is an extension of the contribution by Wendy
Johnston <wendy_AT_itee.uq.edu.au> that initially extended NuSMV
to allow the user to specify a "transition relation ordering"
showing positive effects on the BDD conjunctive partioning. The
ordering is taken from the BDD variable ordering by default, or
it is taken from a specific "transition relation ordering"
provided explicitly by the user through an option.
o System commands
- Added options "-f" (force) to the commands
"build_boolean_model", "bmc_setup", "go", "go_bmc" and
"process_model". When specified, the new option forces the
corresponding model construction, even when COI is enabled.
- Command 'write_boolean_model' now dumps the "current variable"
ordering when the dynamic reordering had triggered.
- Added command 'check_ctlspec' as an alias of 'check_spec' (that
becomes deprecated)
- Command 'check_pslspec' supports SBMC through new options '-s',
'-c' and '-N'. See the user manual for further information.
o System variables
- Added system variable 'ltl_tableau_forward_search' to enable
calculation of reachable states set for the LTL tableau FSM.
- Added system variable 'trans_order_file' to specify an
alternative variable ordering to be used for the transition
relation clusterization.
- Renamed system variable 'program_name' to 'program_path' to hold
the complete path of the executable file that is being
executed when NuSMV is running.
- Added new system variable 'program_name' to hold the system
("NuSMV") name. The new variable may be used to create new
interactive programs derived from NuSMV.