]>
Commit | Line | Data |
---|---|---|
5082b6a1 JR |
1 | # |
2 | # TODO: | |
3 | # - external cudd | |
4 | # - update all BRs | |
5 | # | |
6 | Summary: New Symbolic Model Verifier | |
6206e484 | 7 | Summary(pl): Nowy weryfikator modeli symbolicznych |
5082b6a1 JR |
8 | Name: NuSMV |
9 | Version: 2.4.0 | |
10 | Release: 0.1 | |
11 | License: LGPL | |
12 | Group: Applications | |
13 | Source0: http://nusmv.irst.itc.it/distrib/%{name}-%{version}.tar.gz | |
14 | # Source0-md5: cd1328fc70e9f48d2c4a96c0b8eb5a28 | |
15 | Patch0: %{name}-build.patch | |
16 | URL: http://nusmv.irst.itc.it/ | |
17 | BuildRequires: autoconf | |
18 | BuildRequires: automake | |
19 | BuildRequires: expat-devel | |
20 | BuildRequires: ghostscript | |
21 | BuildRequires: lynx | |
22 | # alternative for lynx | |
23 | #BuildRequires: links | |
24 | BuildRequires: perl-base | |
25 | BuildRequires: readline-devel | |
26 | BuildRequires: tetex-dvips | |
27 | BuildRequires: tetex-makeindex | |
28 | BuildRequires: tetex-latex | |
29 | BuildRoot: %{tmpdir}/%{name}-%{version}-root-%(id -u -n) | |
30 | ||
31 | %description | |
32 | NuSMV is a reimplementation and extension of SMV, the first model | |
33 | checker based on BDDs. NuSMV has been designed to be an open | |
34 | architecture for model checking, which can be reliably used for the | |
35 | verification of industrial designs, as a core for custom verification | |
36 | tools, as a testbed for formal verification techniques, and applied | |
37 | to other research areas. | |
38 | ||
39 | NuSMV2, combines BDD-based model checking component that exploits the | |
40 | CUDD library developed by Fabio Somenzi at Colorado University and | |
41 | SAT-based model checking component that includes an RBC-based Bounded | |
42 | Model Checker, connected to the SIM SAT library developed by the | |
43 | University of Genova. | |
44 | ||
6206e484 JB |
45 | %description -l pl |
46 | NuSVM to reimplementacja i rozszerzenie SMV - pierwszego weryfikatora | |
47 |