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