6 Summary: New Symbolic Model Verifier
7 Summary(pl.UTF-8): Nowy weryfikator modeli symbolicznych
13 Source0: http://nusmv.irst.itc.it/distrib/%{name}-%{version}.tar.gz
14 # Source0-md5: cd1328fc70e9f48d2c4a96c0b8eb5a28
15 Patch0: %{name}-build.patch
16 URL: http://nusmv.irst.itc.it/
17 BuildRequires: autoconf
18 BuildRequires: automake
19 BuildRequires: expat-devel
20 BuildRequires: ghostscript
22 # alternative for lynx
24 BuildRequires: perl-base
25 BuildRequires: readline-devel
26 BuildRequires: tetex-dvips
27 BuildRequires: tetex-makeindex
28 BuildRequires: tetex-latex
29 BuildRoot: %{tmpdir}/%{name}-%{version}-root-%(id -u -n)
32 NuSMV is a reimplementation and extension of SMV, the first model
33 checker based on BDDs. NuSMV has been designed to be an open
34 architecture for model checking, which can be reliably used for the
35 verification of industrial designs, as a core for custom verification
36 tools, as a testbed for formal verification techniques, and applied
37 to other research areas.
39 NuSMV2, combines BDD-based model checking component that exploits the
40 CUDD library developed by Fabio Somenzi at Colorado University and
41 SAT-based model checking component that includes an RBC-based Bounded
42 Model Checker, connected to the SIM SAT library developed by the
45 %description -l pl.UTF-8
46 NuSVM to reimplementacja i rozszerzenie SMV - pierwszego weryfikatora
47 modeli opartego na BDD. NuSMV został zaprojektowany w otwartej
48 architekturze sprawdzania modeli, przez co może być niezawodnie
49 używany do weryfikacji projektów przemysłowych, jako podstawa własnych
50 narzędzi weryfikujących, jako poligon dla technik weryfikacji
51 formalnej oraz stosowany w innych obszarach badań.
53 NuSMV2 łączy komponent sprawdzający modele oparty na BDD,
54 wykorzystujący bibliotekę CUDD stworzoną przez Fabio Somenziniego w
55 Colorado University i komponent sprawdzający modele oparty na SAT
56 zawierający weryfikator modeli ograniczonych oparty na RBC, połączony
57 z biblioteką SIM SAT stworzoną przez University of Genova.
60 Summary: Header files for NuSMV
61 Summary(pl.UTF-8): Pliki nagłówkowe NuSMV
62 Group: Development/Libraries
63 Requires: %{name} = %{version}-%{release}
66 This is the package containing the header files for NuSMV.
68 %description devel -l pl.UTF-8
69 Ten pakiet zawiera pliki nagłówkowe NuSMV.
72 Summary: Static NuSMV library
73 Summary(pl.UTF-8): Statyczna biblioteka NuSMV
74 Group: Development/Libraries
75 Requires: %{name}-devel = %{version}-%{release}
80 %description static -l pl.UTF-8
81 Statyczna biblioteka NuSMV.
89 mkdir -p src/{sa/{fmea,stsa},mbp,mathsat}
90 touch src/sa/Makefile.in src/sa/fmea/Makefile.in src/sa/stsa/Makefile.in \
91 src/mbp/Makefile.in src/mathsat/Makefile.in
104 rm -rf $RPM_BUILD_ROOT
105 install -d $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version}
107 %{__make} -C nusmv install \
108 DESTDIR=$RPM_BUILD_ROOT
110 cp -a nusmv/examples/* $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version}
113 rm -rf $RPM_BUILD_ROOT
115 %post -p /sbin/ldconfig
116 %postun -p /sbin/ldconfig
119 %defattr(644,root,root,755)
120 %doc nusmv/{AUTHORS,ChangeLog,NEWS,README*}
121 %doc nusmv/doc/tutorial/tutorial.p*
122 %doc nusmv/doc/user-man/nusmv.p*
124 %attr(755,root,root) %{_bindir}/*
125 %attr(755,root,root) %{_libdir}/libnusmv*.so.*.*.*
126 %dir %{_datadir}/nusmv
127 %{_datadir}/nusmv/contrib
128 %{_datadir}/nusmv/help
129 %{_datadir}/nusmv/master.nusmvrc
130 %{_examplesdir}/%{name}-%{version}
133 %defattr(644,root,root,755)
134 %attr(755,root,root) %{_libdir}/libnusmv*.so
135 %{_libdir}/libnusmv*.la
141 %defattr(644,root,root,755)
142 %attr(755,root,root) %{_libdir}/libnusmv*.a