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