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