]>
Commit | Line | Data |
---|---|---|
5082b6a1 | 1 | # |
6641397e JR |
2 | # Conditional build: |
3 | %bcond_with zchaff # enable zChaff SAT Solver (zChaff is for non-commercial purposes only) | |
4 | # | |
5 | %define zchaff_ver 2008.10.12 | |
6 | %define minisat_ver 070721 | |
5082b6a1 JR |
7 | # |
8 | Summary: New Symbolic Model Verifier | |
d6427d08 | 9 | Summary(pl.UTF-8): Nowy weryfikator modeli symbolicznych |
5082b6a1 | 10 | Name: NuSMV |
cefc5ce4 | 11 | Version: 2.5.4 |
8c1f86cf | 12 | Release: 12 |
5082b6a1 JR |
13 | License: LGPL |
14 | Group: Applications | |
e2c66126 | 15 | Source0: http://nusmv.fbk.eu/distrib/%{name}-%{version}.tar.gz |
cefc5ce4 | 16 | # Source0-md5: 4d8ae6136fbd916d875cd48f82d5f327 |
6641397e JR |
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 | |
5082b6a1 | 21 | Patch0: %{name}-build.patch |
6641397e | 22 | Patch1: %{name}-solvers.patch |
cf278024 | 23 | Patch2: format-security.patch |
09aa6f55 | 24 | Patch3: fork.patch |
8c1f86cf | 25 | Patch4: cxx.patch |
e2c66126 | 26 | URL: http://nusmv.fbk.eu/ |
5082b6a1 JR |
27 | BuildRequires: autoconf |
28 | BuildRequires: automake | |
29 | BuildRequires: expat-devel | |
30 | BuildRequires: ghostscript | |
31 | BuildRequires: lynx | |
32 | # alternative for lynx | |
33 | #BuildRequires: links | |
34 | BuildRequires: perl-base | |
35 | BuildRequires: readline-devel | |
6641397e JR |
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 | |
69f6bee2 | 43 | BuildRequires: unzip |
5082b6a1 JR |
44 | BuildRoot: %{tmpdir}/%{name}-%{version}-root-%(id -u -n) |
45 | ||
1cbb4be0 JR |
46 | # a lot of inter-library deps confusing install_post_check_so |
47 | %define no_install_post_check_so 1 | |
48 | ||
5082b6a1 JR |
49 | %description |
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. | |
56 | ||
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 | |
61 | University of Genova. | |
62 | ||
20305e49 | 63 | %description -l pl.UTF-8 |
6206e484 | 64 | NuSVM to reimplementacja i rozszerzenie SMV - pierwszego weryfikatora |
20305e49 JR |
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ń. | |
6206e484 | 70 | |
20305e49 JR |
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. | |
6206e484 | 76 | |
5082b6a1 JR |
77 | %package devel |
78 | Summary: Header files for NuSMV | |
d6427d08 | 79 | Summary(pl.UTF-8): Pliki nagłówkowe NuSMV |
5082b6a1 | 80 | Group: Development/Libraries |
6206e484 | 81 | Requires: %{name} = %{version}-%{release} |
5082b6a1 JR |
82 | |
83 | %description devel | |
84 | This is the package containing the header files for NuSMV. | |
85 | ||
20305e49 JR |
86 | %description devel -l pl.UTF-8 |
87 | Ten pakiet zawiera pliki nagłówkowe NuSMV. | |
5082b6a1 JR |
88 | |
89 | %package static | |
90 | Summary: Static NuSMV library | |
d6427d08 | 91 | Summary(pl.UTF-8): Statyczna biblioteka NuSMV |
5082b6a1 JR |
92 | Group: Development/Libraries |
93 | Requires: %{name}-devel = %{version}-%{release} | |
94 | ||
95 | %description static | |
96 | Static NuSMV library. | |
97 | ||
20305e49 | 98 | %description static -l pl.UTF-8 |
5082b6a1 JR |
99 | Statyczna biblioteka NuSMV. |
100 | ||
101 | %prep | |
102 | %setup -q | |
6641397e | 103 | install %{SOURCE1} MiniSat/ |
17427a19 AM |
104 | cd MiniSat |
105 | unzip -q *.zip | |
106 | cd .. | |
6641397e JR |
107 | install %{SOURCE2} zchaff/ |
108 | ||
17427a19 | 109 | %patch0 -p1 |
6641397e | 110 | %patch1 -p1 |
cf278024 | 111 | %patch2 -p1 |
09aa6f55 | 112 | %patch3 -p1 |
8c1f86cf | 113 | %patch4 -p1 |
6641397e | 114 | |
5082b6a1 | 115 | %build |
1cbb4be0 | 116 | ICFLAGS="%{rpmcflags} -fPIC" |
d8d91413 | 117 | export ICFLAGS |
5082b6a1 | 118 | |
6641397e | 119 | cd MiniSat/ |
1cbb4be0 | 120 | OPTFLAGS="%{rpmcxxflags} -fPIC" COPTIMIZE="%{rpmcxxflags} -fPIC" ./build.sh |
6641397e JR |
121 | %if %{with zchaff} |
122 | cd ../zchaff | |
1cbb4be0 | 123 | OPTFLAGS="%{rpmcxxflags} -fPIC" ./build.sh |
6641397e JR |
124 | %endif |
125 | cd ../cudd-* | |
25a3234b | 126 | %ifarch %{x8664} |
74c2172a JR |
127 | cp -f Makefile Makefile_32bit |
128 | cp -f Makefile_64bit Makefile | |
25a3234b | 129 | %endif |
6641397e JR |
130 | %{__make} |
131 | cd .. | |
25a3234b | 132 | |
74c2172a JR |
133 | cd nusmv |
134 | ||
1cbb4be0 JR |
135 | %{__libtoolize} |
136 | %{__aclocal} -I m4 | |
137 | %{__autoconf} | |
138 | %{__automake} | |
139 | %configure \ | |
5082b6a1 | 140 | --enable-shared \ |
6641397e JR |
141 | %{?with_zchaff:--enable-zchaff} \ |
142 | --enable-minisat | |
143 | ||
5082b6a1 | 144 | %{__make} |
1cbb4be0 | 145 | |
34c4f2ed | 146 | %{__make} -j1 docs |
5082b6a1 JR |
147 | |
148 | %install | |
149 | rm -rf $RPM_BUILD_ROOT | |
150 | install -d $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version} | |
151 | ||
306c78b8 | 152 | %{__make} -j1 -C nusmv install \ |
1cbb4be0 JR |
153 | INSTALL_DATA="cp -a" \ |
154 | INSTALL_HEADER="install -p" \ | |
5082b6a1 JR |
155 | DESTDIR=$RPM_BUILD_ROOT |
156 | ||
157 | cp -a nusmv/examples/* $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version} | |
158 | ||
1cbb4be0 JR |
159 | %{__rm} -r $RPM_BUILD_ROOT%{_datadir}/nusmv/{doc,examples,LGPL*,NEWS,README*} |
160 | %{__rm} -r $RPM_BUILD_ROOT%{_libdir}/*.la | |
6641397e | 161 | |
5082b6a1 JR |
162 | %clean |
163 | rm -rf $RPM_BUILD_ROOT | |
164 | ||
165 | %post -p /sbin/ldconfig | |
166 | %postun -p /sbin/ldconfig | |
167 | ||
168 | %files | |
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* | |
173 | %doc nusmv/doc/html | |
174 | %attr(755,root,root) %{_bindir}/* | |
65c2d833 | 175 | %attr(755,root,root) %{_libdir}/lib*smv*.so.*.*.* |
2ef2bad5 JR |
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 | |
5082b6a1 JR |
179 | %dir %{_datadir}/nusmv |
180 | %{_datadir}/nusmv/contrib | |
181 | %{_datadir}/nusmv/help | |
182 | %{_datadir}/nusmv/master.nusmvrc | |
183 | %{_examplesdir}/%{name}-%{version} | |
184 | ||
185 | %files devel | |
186 | %defattr(644,root,root,755) | |
65c2d833 | 187 | %attr(755,root,root) %{_libdir}/lib*smv*.so |
2ef2bad5 | 188 | %attr(755,root,root) %{_libdir}/librbcdag.so |
5082b6a1 JR |
189 | %{_includedir}/cudd* |
190 | %{_includedir}/nusmv | |
6206e484 | 191 | %{_pkgconfigdir}/* |
5082b6a1 JR |
192 | |
193 | %files static | |
194 | %defattr(644,root,root,755) | |
65c2d833 | 195 | %attr(755,root,root) %{_libdir}/lib*smv*.a |
2ef2bad5 | 196 | %attr(755,root,root) %{_libdir}/librbcdag.a |