3 %bcond_with zchaff # enable zChaff SAT Solver (zChaff is for non-commercial purposes only)
5 %define zchaff_ver 2008.10.12
6 %define minisat_ver 070721
8 Summary: New Symbolic Model Verifier
9 Summary(pl.UTF-8): Nowy weryfikator modeli symbolicznych
15 Source0: http://nusmv.irst.itc.it/distrib/%{name}-%{version}.tar.gz
16 # Source0-md5: 4d8ae6136fbd916d875cd48f82d5f327
17 Source1: http://minisat.se/downloads/minisat2-%{minisat_ver}.zip
18 # Source1-md5: fb12db9a13f86a2133758abfba239546
19 Source2: http://www.princeton.edu/~chaff/zchaff/zchaff.%{zchaff_ver}.zip
20 # Source2-md5: 7398b3e984a5046755cb3ef6b0e44d2e
21 Patch0: %{name}-build.patch
22 Patch1: %{name}-solvers.patch
23 Patch2: format-security.patch
24 URL: http://nusmv.irst.itc.it/
25 BuildRequires: autoconf
26 BuildRequires: automake
27 BuildRequires: expat-devel
28 BuildRequires: ghostscript
30 # alternative for lynx
32 BuildRequires: perl-base
33 BuildRequires: readline-devel
34 BuildRequires: texlive-dvips
35 BuildRequires: texlive-latex
36 BuildRequires: texlive-latex-bibtex
37 BuildRequires: texlive-latex-carlisle
38 BuildRequires: texlive-latex-extend
39 BuildRequires: texlive-latex-psnfss
40 BuildRequires: texlive-makeindex
42 BuildRoot: %{tmpdir}/%{name}-%{version}-root-%(id -u -n)
44 # a lot of inter-library deps confusing install_post_check_so
45 %define no_install_post_check_so 1
48 NuSMV is a reimplementation and extension of SMV, the first model
49 checker based on BDDs. NuSMV has been designed to be an open
50 architecture for model checking, which can be reliably used for the
51 verification of industrial designs, as a core for custom verification
52 tools, as a testbed for formal verification techniques, and applied
53 to other research areas.
55 NuSMV2, combines BDD-based model checking component that exploits the
56 CUDD library developed by Fabio Somenzi at Colorado University and
57 SAT-based model checking component that includes an RBC-based Bounded
58 Model Checker, connected to the SIM SAT library developed by the
61 %description -l pl.UTF-8
62 NuSVM to reimplementacja i rozszerzenie SMV - pierwszego weryfikatora
63 modeli opartego na BDD. NuSMV został zaprojektowany w otwartej
64 architekturze sprawdzania modeli, przez co może być niezawodnie
65 używany do weryfikacji projektów przemysłowych, jako podstawa własnych
66 narzędzi weryfikujących, jako poligon dla technik weryfikacji
67 formalnej oraz stosowany w innych obszarach badań.
69 NuSMV2 łączy komponent sprawdzający modele oparty na BDD,
70 wykorzystujący bibliotekę CUDD stworzoną przez Fabio Somenziniego w
71 Colorado University i komponent sprawdzający modele oparty na SAT
72 zawierający weryfikator modeli ograniczonych oparty na RBC, połączony
73 z biblioteką SIM SAT stworzoną przez University of Genova.
76 Summary: Header files for NuSMV
77 Summary(pl.UTF-8): Pliki nagłówkowe NuSMV
78 Group: Development/Libraries
79 Requires: %{name} = %{version}-%{release}
82 This is the package containing the header files for NuSMV.
84 %description devel -l pl.UTF-8
85 Ten pakiet zawiera pliki nagłówkowe NuSMV.
88 Summary: Static NuSMV library
89 Summary(pl.UTF-8): Statyczna biblioteka NuSMV
90 Group: Development/Libraries
91 Requires: %{name}-devel = %{version}-%{release}
96 %description static -l pl.UTF-8
97 Statyczna biblioteka NuSMV.
103 install %{SOURCE1} MiniSat/
104 install %{SOURCE2} zchaff/
110 ICFLAGS="%{rpmcflags} -fPIC"
114 OPTFLAGS="%{rpmcxxflags} -fPIC" COPTIMIZE="%{rpmcxxflags} -fPIC" ./build.sh
117 OPTFLAGS="%{rpmcxxflags} -fPIC" ./build.sh
121 cp -f Makefile Makefile_32bit
122 cp -f Makefile_64bit Makefile
135 %{?with_zchaff:--enable-zchaff} \
143 rm -rf $RPM_BUILD_ROOT
144 install -d $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version}
146 %{__make} -j1 -C nusmv install \
147 INSTALL_DATA="cp -a" \
148 INSTALL_HEADER="install -p" \
149 DESTDIR=$RPM_BUILD_ROOT
151 cp -a nusmv/examples/* $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version}
153 %{__rm} -r $RPM_BUILD_ROOT%{_datadir}/nusmv/{doc,examples,LGPL*,NEWS,README*}
154 %{__rm} -r $RPM_BUILD_ROOT%{_libdir}/*.la
157 rm -rf $RPM_BUILD_ROOT
159 %post -p /sbin/ldconfig
160 %postun -p /sbin/ldconfig
163 %defattr(644,root,root,755)
164 %doc nusmv/{AUTHORS,ChangeLog,NEWS,README*}
165 %doc nusmv/doc/tutorial/tutorial.p*
166 %doc nusmv/doc/user-man/nusmv.p*
168 %attr(755,root,root) %{_bindir}/*
169 %attr(755,root,root) %{_libdir}/lib*smv*.so.*.*.*
170 %attr(755,root,root) %ghost %{_libdir}/lib*smv*.so.0
171 %attr(755,root,root) %{_libdir}/librbcdag.so.*.*.*
172 %attr(755,root,root) %ghost %{_libdir}/librbcdag.so.0
173 %dir %{_datadir}/nusmv
174 %{_datadir}/nusmv/contrib
175 %{_datadir}/nusmv/help
176 %{_datadir}/nusmv/master.nusmvrc
177 %{_examplesdir}/%{name}-%{version}
180 %defattr(644,root,root,755)
181 %attr(755,root,root) %{_libdir}/lib*smv*.so
182 %attr(755,root,root) %{_libdir}/librbcdag.so
188 %defattr(644,root,root,755)
189 %attr(755,root,root) %{_libdir}/lib*smv*.a
190 %attr(755,root,root) %{_libdir}/librbcdag.a