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.fbk.eu/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
26 URL: http://nusmv.fbk.eu/
27 BuildRequires: autoconf
28 BuildRequires: automake
29 BuildRequires: expat-devel
30 BuildRequires: ghostscript
32 # alternative for lynx
34 BuildRequires: perl-base
35 BuildRequires: readline-devel
36 BuildRequires: texlive-dvips
37 BuildRequires: texlive-latex
38 BuildRequires: texlive-latex-bibtex
39 BuildRequires: texlive-latex-carlisle
40 BuildRequires: texlive-latex-extend
41 BuildRequires: texlive-latex-psnfss
42 BuildRequires: texlive-makeindex
44 BuildRoot: %{tmpdir}/%{name}-%{version}-root-%(id -u -n)
46 # a lot of inter-library deps confusing install_post_check_so
47 %define no_install_post_check_so 1
50 NuSMV is a reimplementation and extension of SMV, the first model
51 checker based on BDDs. NuSMV has been designed to be an open
52 architecture for model checking, which can be reliably used for the
53 verification of industrial designs, as a core for custom verification
54 tools, as a testbed for formal verification techniques, and applied
55 to other research areas.
57 NuSMV2, combines BDD-based model checking component that exploits the
58 CUDD library developed by Fabio Somenzi at Colorado University and
59 SAT-based model checking component that includes an RBC-based Bounded
60 Model Checker, connected to the SIM SAT library developed by the
63 %description -l pl.UTF-8
64 NuSVM to reimplementacja i rozszerzenie SMV - pierwszego weryfikatora
65 modeli opartego na BDD. NuSMV został zaprojektowany w otwartej
66 architekturze sprawdzania modeli, przez co może być niezawodnie
67 używany do weryfikacji projektów przemysłowych, jako podstawa własnych
68 narzędzi weryfikujących, jako poligon dla technik weryfikacji
69 formalnej oraz stosowany w innych obszarach badań.
71 NuSMV2 łączy komponent sprawdzający modele oparty na BDD,
72 wykorzystujący bibliotekę CUDD stworzoną przez Fabio Somenziniego w
73 Colorado University i komponent sprawdzający modele oparty na SAT
74 zawierający weryfikator modeli ograniczonych oparty na RBC, połączony
75 z biblioteką SIM SAT stworzoną przez University of Genova.
78 Summary: Header files for NuSMV
79 Summary(pl.UTF-8): Pliki nagłówkowe NuSMV
80 Group: Development/Libraries
81 Requires: %{name} = %{version}-%{release}
84 This is the package containing the header files for NuSMV.
86 %description devel -l pl.UTF-8
87 Ten pakiet zawiera pliki nagłówkowe NuSMV.
90 Summary: Static NuSMV library
91 Summary(pl.UTF-8): Statyczna biblioteka NuSMV
92 Group: Development/Libraries
93 Requires: %{name}-devel = %{version}-%{release}
98 %description static -l pl.UTF-8
99 Statyczna biblioteka NuSMV.
103 install %{SOURCE1} MiniSat/
107 install %{SOURCE2} zchaff/
116 ICFLAGS="%{rpmcflags} -fPIC"
120 OPTFLAGS="%{rpmcxxflags} -fPIC" COPTIMIZE="%{rpmcxxflags} -fPIC" ./build.sh
123 OPTFLAGS="%{rpmcxxflags} -fPIC" ./build.sh
127 cp -f Makefile Makefile_32bit
128 cp -f Makefile_64bit Makefile
141 %{?with_zchaff:--enable-zchaff} \
149 rm -rf $RPM_BUILD_ROOT
150 install -d $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version}
152 %{__make} -j1 -C nusmv install \
153 INSTALL_DATA="cp -a" \
154 INSTALL_HEADER="install -p" \
155 DESTDIR=$RPM_BUILD_ROOT
157 cp -a nusmv/examples/* $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version}
159 %{__rm} -r $RPM_BUILD_ROOT%{_datadir}/nusmv/{doc,examples,LGPL*,NEWS,README*}
160 %{__rm} -r $RPM_BUILD_ROOT%{_libdir}/*.la
163 rm -rf $RPM_BUILD_ROOT
165 %post -p /sbin/ldconfig
166 %postun -p /sbin/ldconfig
169 %defattr(644,root,root,755)
170 %doc nusmv/{AUTHORS,ChangeLog,NEWS,README*}
171 %doc nusmv/doc/tutorial/tutorial.p*
172 %doc nusmv/doc/user-man/nusmv.p*
174 %attr(755,root,root) %{_bindir}/*
175 %attr(755,root,root) %{_libdir}/lib*smv*.so.*.*.*
176 %attr(755,root,root) %ghost %{_libdir}/lib*smv*.so.0
177 %attr(755,root,root) %{_libdir}/librbcdag.so.*.*.*
178 %attr(755,root,root) %ghost %{_libdir}/librbcdag.so.0
179 %dir %{_datadir}/nusmv
180 %{_datadir}/nusmv/contrib
181 %{_datadir}/nusmv/help
182 %{_datadir}/nusmv/master.nusmvrc
183 %{_examplesdir}/%{name}-%{version}
186 %defattr(644,root,root,755)
187 %attr(755,root,root) %{_libdir}/lib*smv*.so
188 %attr(755,root,root) %{_libdir}/librbcdag.so
194 %defattr(644,root,root,755)
195 %attr(755,root,root) %{_libdir}/lib*smv*.a
196 %attr(755,root,root) %{_libdir}/librbcdag.a