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