]>
Commit | Line | Data |
---|---|---|
5082b6a1 JR |
1 | # |
2 | # TODO: | |
3 | # - external cudd | |
4 | # - update all BRs | |
5 | # | |
6 | Summary: New Symbolic Model Verifier | |
d6427d08 | 7 | Summary(pl.UTF-8): Nowy weryfikator modeli symbolicznych |
5082b6a1 JR |
8 | Name: NuSMV |
9 | Version: 2.4.0 | |
10 | Release: 0.1 | |
11 | License: LGPL | |
12 | Group: Applications | |
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 | |
21 | BuildRequires: lynx | |
22 | # alternative for lynx | |
23 | #BuildRequires: links | |
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) | |
30 | ||
31 | %description | |
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. | |
38 | ||
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 | |
43 | University of Genova. | |
44 | ||
20305e49 | 45 | %description -l pl.UTF-8 |
6206e484 | 46 | NuSVM to reimplementacja i rozszerzenie SMV - pierwszego weryfikatora |
20305e49 JR |
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ń. | |
6206e484 | 52 | |
20305e49 JR |
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. | |
6206e484 | 58 | |
5082b6a1 JR |
59 | %package devel |
60 | Summary: Header files for NuSMV | |
d6427d08 | 61 | Summary(pl.UTF-8): Pliki nagłówkowe NuSMV |
5082b6a1 | 62 | Group: Development/Libraries |
6206e484 | 63 | Requires: %{name} = %{version}-%{release} |
5082b6a1 JR |
64 | |
65 | %description devel | |
66 | This is the package containing the header files for NuSMV. | |
67 | ||
20305e49 JR |
68 | %description devel -l pl.UTF-8 |
69 | Ten pakiet zawiera pliki nagłówkowe NuSMV. | |
5082b6a1 JR |
70 | |
71 | %package static | |
72 | Summary: Static NuSMV library | |
d6427d08 | 73 | Summary(pl.UTF-8): Statyczna biblioteka NuSMV |
5082b6a1 JR |
74 | Group: Development/Libraries |
75 | Requires: %{name}-devel = %{version}-%{release} | |
76 | ||
77 | %description static | |
78 | Static NuSMV library. | |
79 | ||
20305e49 | 80 | %description static -l pl.UTF-8 |
5082b6a1 JR |
81 | Statyczna biblioteka NuSMV. |
82 | ||
83 | %prep | |
84 | %setup -q | |
85 | %patch0 -p1 | |
86 | ||
87 | %build | |
88 | cd 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 | |
92 | ||
93 | %{__aclocal} | |
94 | %{__autoconf} | |
95 | %{__autoheader} | |
96 | %{__automake} | |
5082b6a1 JR |
97 | %configure \ |
98 | --enable-shared \ | |
99 | --enable-psl | |
100 | %{__make} | |
101 | %{__make} docs | |
102 | ||
103 | %install | |
104 | rm -rf $RPM_BUILD_ROOT | |
105 | install -d $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version} | |
106 | ||
107 | %{__make} -C nusmv install \ | |
108 | DESTDIR=$RPM_BUILD_ROOT | |
109 | ||
110 | cp -a nusmv/examples/* $RPM_BUILD_ROOT%{_examplesdir}/%{name}-%{version} | |
111 | ||
112 | %clean | |
113 | rm -rf $RPM_BUILD_ROOT | |
114 | ||
115 | %post -p /sbin/ldconfig | |
116 | %postun -p /sbin/ldconfig | |
117 | ||
118 | %files | |
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* | |
123 | %doc nusmv/doc/html | |
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} | |
131 | ||
132 | %files devel | |
133 | %defattr(644,root,root,755) | |
6206e484 JB |
134 | %attr(755,root,root) %{_libdir}/libnusmv*.so |
135 | %{_libdir}/libnusmv*.la | |
5082b6a1 JR |
136 | %{_includedir}/cudd* |
137 | %{_includedir}/nusmv | |
6206e484 | 138 | %{_pkgconfigdir}/* |
5082b6a1 JR |
139 | |
140 | %files static | |
141 | %defattr(644,root,root,755) | |
142 | %attr(755,root,root) %{_libdir}/libnusmv*.a |