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:        2
  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 URL:            http://nusmv.irst.itc.it/
  24 BuildRequires:  autoconf
  25 BuildRequires:  automake
  26 BuildRequires:  expat-devel
  27 BuildRequires:  ghostscript
  28 BuildRequires:  lynx
  29 # alternative for lynx
  30 #BuildRequires: links
  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
  40 BuildRequires:  unzip
  41 BuildRoot:      %{tmpdir}/%{name}-%{version}-root-%(id -u -n)
  42
  43 # a lot of inter-library deps confusing install_post_check_so
  44 %define         no_install_post_check_so        1
  45
  46 %description
  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.
  53
  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
  58 University of Genova.
  59
  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ń.
  67
  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.
  73
  74 %package devel
  75 Summary:        Header files for NuSMV
  76 Summary(pl.UTF-8):      Pliki nagłówkowe NuSMV
  77 Group:          Development/Libraries
  78 Requires:       %{name} = %{version}-%{release}
  79
  80 %description devel
  81 This is the package containing the header files for NuSMV.
  82
  83 %description devel -l pl.UTF-8
  84 Ten pakiet zawiera pliki nagłówkowe NuSMV.
  85
  86 %package static
  87 Summary:        Static NuSMV library
  88 Summary(pl.UTF-8):      Statyczna biblioteka NuSMV
  89 Group:          Development/Libraries
  90 Requires:       %{name}-devel = %{version}-%{release}
  91
  92 %description static
  93 Static NuSMV library.
  94
  95 %description static -l pl.UTF-8
  96 Statyczna biblioteka NuSMV.
  97
  98 %prep
  99 %setup -q
 100 %patch0 -p1
 101
 102 install %{SOURCE1} MiniSat/
 103 install %{SOURCE2} zchaff/
 104
 105 %patch1 -p1
 106
 107 %build
 108 ICFLAGS="%{rpmcflags} -fPIC"
 109 export ICFLAGS
 110
 111 cd MiniSat/
 112 OPTFLAGS="%{rpmcxxflags} -fPIC" COPTIMIZE="%{rpmcxxflags} -fPIC" ./build.sh
 113 %if %{with zchaff}
 114 cd ../zchaff
 115 OPTFLAGS="%{rpmcxxflags} -fPIC" ./build.sh
 116 %endif
 117 cd ../cudd-*
 118 %ifarch %{x8664}
 119 cp -f Makefile Makefile_32bit
 120 cp -f Makefile_64bit Makefile
 121 %endif
 122 %{__make}
 123 cd ..
 124
 125 cd nusmv
 126
 127 %{__libtoolize}
 128 %{__aclocal} -I m4
 129 %{__autoconf}
 130 %{__automake}
 131 %configure \
 132         --enable-shared \
 133         %{?with_zchaff:--enable-zchaff} \
 134         --enable-minisat
 135
 136 %{__make}
 137
 138 %{__make} docs
 139
 140 %install
 141 rm -rf $RPM_BUILD_ROOT
 142 install -d $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version}
 143
 144 %{__make} -j1 -C nusmv install \
 145         INSTALL_DATA="cp -a" \
 146         INSTALL_HEADER="install -p" \
 147         DESTDIR=$RPM_BUILD_ROOT
 148
 149 cp -a nusmv/examples/* $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version}
 150
 151 %{__rm} -r $RPM_BUILD_ROOT%{_datadir}/nusmv/{doc,examples,LGPL*,NEWS,README*}
 152 %{__rm} -r $RPM_BUILD_ROOT%{_libdir}/*.la
 153
 154 %clean
 155 rm -rf $RPM_BUILD_ROOT
 156
 157 %post   -p /sbin/ldconfig
 158 %postun -p /sbin/ldconfig
 159
 160 %files
 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*
 165 %doc nusmv/doc/html
 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}
 176
 177 %files devel
 178 %defattr(644,root,root,755)
 179 %attr(755,root,root) %{_libdir}/lib*smv*.so
 180 %attr(755,root,root) %{_libdir}/librbcdag.so
 181 %{_includedir}/cudd*
 182 %{_includedir}/nusmv
 183 %{_pkgconfigdir}/*
 184
 185 %files static
 186 %defattr(644,root,root,755)
 187 %attr(755,root,root) %{_libdir}/lib*smv*.a
 188 %attr(755,root,root) %{_libdir}/librbcdag.a