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