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:        10
  13 License:        LGPL
  14 Group:          Applications
  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 Patch3:         fork.patch
  25 URL:            http://nusmv.irst.itc.it/
  26 BuildRequires:  autoconf
  27 BuildRequires:  automake
  28 BuildRequires:  expat-devel
  29 BuildRequires:  ghostscript
  30 BuildRequires:  lynx
  31 # alternative for lynx
  32 #BuildRequires: links
  33 BuildRequires:  perl-base
  34 BuildRequires:  readline-devel
  35 BuildRequires:  texlive-dvips
  36 BuildRequires:  texlive-latex
  37 BuildRequires:  texlive-latex-bibtex
  38 BuildRequires:  texlive-latex-carlisle
  39 BuildRequires:  texlive-latex-extend
  40 BuildRequires:  texlive-latex-psnfss
  41 BuildRequires:  texlive-makeindex
  42 BuildRequires:  unzip
  43 BuildRoot:      %{tmpdir}/%{name}-%{version}-root-%(id -u -n)
  44
  45 # a lot of inter-library deps confusing install_post_check_so
  46 %define         no_install_post_check_so        1
  47
  48 %description
  49 NuSMV is a reimplementation and extension of SMV, the first model
  50 checker based on BDDs. NuSMV has been designed to be an open
  51 architecture for model checking, which can be reliably used for the
  52 verification of industrial designs, as a core for custom verification
  53 tools, as a testbed for formal verification techniques, and applied
  54 to other research areas.
  55
  56 NuSMV2, combines BDD-based model checking component that exploits the
  57 CUDD library developed by Fabio Somenzi at Colorado University and
  58 SAT-based model checking component that includes an RBC-based Bounded
  59 Model Checker, connected to the SIM SAT library developed by the
  60 University of Genova.
  61
  62 %description -l pl.UTF-8
  63 NuSVM to reimplementacja i rozszerzenie SMV - pierwszego weryfikatora
  64 modeli opartego na BDD. NuSMV został zaprojektowany w otwartej
  65 architekturze sprawdzania modeli, przez co może być niezawodnie
  66 używany do weryfikacji projektów przemysłowych, jako podstawa własnych
  67 narzędzi weryfikujących, jako poligon dla technik weryfikacji
  68 formalnej oraz stosowany w innych obszarach badań.
  69
  70 NuSMV2 łączy komponent sprawdzający modele oparty na BDD,
  71 wykorzystujący bibliotekę CUDD stworzoną przez Fabio Somenziniego w
  72 Colorado University i komponent sprawdzający modele oparty na SAT
  73 zawierający weryfikator modeli ograniczonych oparty na RBC, połączony
  74 z biblioteką SIM SAT stworzoną przez University of Genova.
  75
  76 %package devel
  77 Summary:        Header files for NuSMV
  78 Summary(pl.UTF-8):      Pliki nagłówkowe NuSMV
  79 Group:          Development/Libraries
  80 Requires:       %{name} = %{version}-%{release}
  81
  82 %description devel
  83 This is the package containing the header files for NuSMV.
  84
  85 %description devel -l pl.UTF-8
  86 Ten pakiet zawiera pliki nagłówkowe NuSMV.
  87
  88 %package static
  89 Summary:        Static NuSMV library
  90 Summary(pl.UTF-8):      Statyczna biblioteka NuSMV
  91 Group:          Development/Libraries
  92 Requires:       %{name}-devel = %{version}-%{release}
  93
  94 %description static
  95 Static NuSMV library.
  96
  97 %description static -l pl.UTF-8
  98 Statyczna biblioteka NuSMV.
  99
 100 %prep
 101 %setup -q
 102 install %{SOURCE1} MiniSat/
 103 cd MiniSat
 104 unzip -q *.zip
 105 cd ..
 106 install %{SOURCE2} zchaff/
 107
 108 %patch0 -p1
 109 %patch1 -p1
 110 %patch2 -p1
 111 %patch3 -p1
 112
 113 %build
 114 ICFLAGS="%{rpmcflags} -fPIC"
 115 export ICFLAGS
 116
 117 cd MiniSat/
 118 OPTFLAGS="%{rpmcxxflags} -fPIC" COPTIMIZE="%{rpmcxxflags} -fPIC" ./build.sh
 119 %if %{with zchaff}
 120 cd ../zchaff
 121 OPTFLAGS="%{rpmcxxflags} -fPIC" ./build.sh
 122 %endif
 123 cd ../cudd-*
 124 %ifarch %{x8664}
 125 cp -f Makefile Makefile_32bit
 126 cp -f Makefile_64bit Makefile
 127 %endif
 128 %{__make}
 129 cd ..
 130
 131 cd nusmv
 132
 133 %{__libtoolize}
 134 %{__aclocal} -I m4
 135 %{__autoconf}
 136 %{__automake}
 137 %configure \
 138         --enable-shared \
 139         %{?with_zchaff:--enable-zchaff} \
 140         --enable-minisat
 141
 142 %{__make}
 143
 144 %{__make} -j1 docs
 145
 146 %install
 147 rm -rf $RPM_BUILD_ROOT
 148 install -d $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version}
 149
 150 %{__make} -j1 -C nusmv install \
 151         INSTALL_DATA="cp -a" \
 152         INSTALL_HEADER="install -p" \
 153         DESTDIR=$RPM_BUILD_ROOT
 154
 155 cp -a nusmv/examples/* $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version}
 156
 157 %{__rm} -r $RPM_BUILD_ROOT%{_datadir}/nusmv/{doc,examples,LGPL*,NEWS,README*}
 158 %{__rm} -r $RPM_BUILD_ROOT%{_libdir}/*.la
 159
 160 %clean
 161 rm -rf $RPM_BUILD_ROOT
 162
 163 %post   -p /sbin/ldconfig
 164 %postun -p /sbin/ldconfig
 165
 166 %files
 167 %defattr(644,root,root,755)
 168 %doc nusmv/{AUTHORS,ChangeLog,NEWS,README*}
 169 %doc nusmv/doc/tutorial/tutorial.p*
 170 %doc nusmv/doc/user-man/nusmv.p*
 171 %doc nusmv/doc/html
 172 %attr(755,root,root) %{_bindir}/*
 173 %attr(755,root,root) %{_libdir}/lib*smv*.so.*.*.*
 174 %attr(755,root,root) %ghost %{_libdir}/lib*smv*.so.0
 175 %attr(755,root,root) %{_libdir}/librbcdag.so.*.*.*
 176 %attr(755,root,root) %ghost %{_libdir}/librbcdag.so.0
 177 %dir %{_datadir}/nusmv
 178 %{_datadir}/nusmv/contrib
 179 %{_datadir}/nusmv/help
 180 %{_datadir}/nusmv/master.nusmvrc
 181 %{_examplesdir}/%{name}-%{version}
 182
 183 %files devel
 184 %defattr(644,root,root,755)
 185 %attr(755,root,root) %{_libdir}/lib*smv*.so
 186 %attr(755,root,root) %{_libdir}/librbcdag.so
 187 %{_includedir}/cudd*
 188 %{_includedir}/nusmv
 189 %{_pkgconfigdir}/*
 190
 191 %files static
 192 %defattr(644,root,root,755)
 193 %attr(755,root,root) %{_libdir}/lib*smv*.a
 194 %attr(755,root,root) %{_libdir}/librbcdag.a