NuSMV.spec

   1 #
   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
   7 #
   8 Summary:        New Symbolic Model Verifier
   9 Summary(pl.UTF-8):      Nowy weryfikator modeli symbolicznych
  10 Name:           NuSMV
  11 Version:        2.5.4
  12 Release:        12
  13 License:        LGPL
  14 Group:          Applications
  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
  24 Patch3:         fork.patch
  25 Patch4:         cxx.patch
  26 URL:            http://nusmv.fbk.eu/
  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
  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
  43 BuildRequires:  unzip
  44 BuildRoot:      %{tmpdir}/%{name}-%{version}-root-%(id -u -n)
  45
  46 # a lot of inter-library deps confusing install_post_check_so
  47 %define         no_install_post_check_so        1
  48
  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
  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ń.
  70
  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.
  76
  77 %package devel
  78 Summary:        Header files for NuSMV
  79 Summary(pl.UTF-8):      Pliki nagłówkowe NuSMV
  80 Group:          Development/Libraries
  81 Requires:       %{name} = %{version}-%{release}
  82
  83 %description devel
  84 This is the package containing the header files for NuSMV.
  85
  86 %description devel -l pl.UTF-8
  87 Ten pakiet zawiera pliki nagłówkowe NuSMV.
  88
  89 %package static
  90 Summary:        Static NuSMV library
  91 Summary(pl.UTF-8):      Statyczna biblioteka NuSMV
  92 Group:          Development/Libraries
  93 Requires:       %{name}-devel = %{version}-%{release}
  94
  95 %description static
  96 Static NuSMV library.
  97
  98 %description static -l pl.UTF-8
  99 Statyczna biblioteka NuSMV.
 100
 101 %prep
 102 %setup -q
 103 install %{SOURCE1} MiniSat/
 104 cd MiniSat
 105 unzip -q *.zip
 106 cd ..
 107 install %{SOURCE2} zchaff/
 108
 109 %patch0 -p1
 110 %patch1 -p1
 111 %patch2 -p1
 112 %patch3 -p1
 113 %patch4 -p1
 114
 115 %build
 116 ICFLAGS="%{rpmcflags} -fPIC"
 117 export ICFLAGS
 118
 119 cd MiniSat/
 120 OPTFLAGS="%{rpmcxxflags} -fPIC" COPTIMIZE="%{rpmcxxflags} -fPIC" ./build.sh
 121 %if %{with zchaff}
 122 cd ../zchaff
 123 OPTFLAGS="%{rpmcxxflags} -fPIC" ./build.sh
 124 %endif
 125 cd ../cudd-*
 126 %ifarch %{x8664}
 127 cp -f Makefile Makefile_32bit
 128 cp -f Makefile_64bit Makefile
 129 %endif
 130 %{__make}
 131 cd ..
 132
 133 cd nusmv
 134
 135 %{__libtoolize}
 136 %{__aclocal} -I m4
 137 %{__autoconf}
 138 %{__automake}
 139 %configure \
 140         --enable-shared \
 141         %{?with_zchaff:--enable-zchaff} \
 142         --enable-minisat
 143
 144 %{__make}
 145
 146 %{__make} -j1 docs
 147
 148 %install
 149 rm -rf $RPM_BUILD_ROOT
 150 install -d $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version}
 151
 152 %{__make} -j1 -C nusmv install \
 153         INSTALL_DATA="cp -a" \
 154         INSTALL_HEADER="install -p" \
 155         DESTDIR=$RPM_BUILD_ROOT
 156
 157 cp -a nusmv/examples/* $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version}
 158
 159 %{__rm} -r $RPM_BUILD_ROOT%{_datadir}/nusmv/{doc,examples,LGPL*,NEWS,README*}
 160 %{__rm} -r $RPM_BUILD_ROOT%{_libdir}/*.la
 161
 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}/*
 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}
 184
 185 %files devel
 186 %defattr(644,root,root,755)
 187 %attr(755,root,root) %{_libdir}/lib*smv*.so
 188 %attr(755,root,root) %{_libdir}/librbcdag.so
 189 %{_includedir}/cudd*
 190 %{_includedir}/nusmv
 191 %{_pkgconfigdir}/*
 192
 193 %files static
 194 %defattr(644,root,root,755)
 195 %attr(755,root,root) %{_libdir}/lib*smv*.a
 196 %attr(755,root,root) %{_libdir}/librbcdag.a