Commit ba9defe3 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

initial version (0.0b)

parents
SUBDIRS= libpn src doc
EXTRA_DIST = \
samples/fms2.net \
samples/fms3.net \
samples/fms4.net \
samples/kanban2.net \
samples/kanban3.net \
samples/kanban4.net \
samples/philo5.net \
samples/philo6.net \
samples/philo7.net \
samples/philo8.net \
samples/philo9.net \
samples/ring5.net \
samples/ring6.net \
samples/simple.net
DISTCHECK_CONFIGURE_FLAGS=--with-spot=$(spot_prefix)
\ No newline at end of file
AC_INIT([checkpn], [0.0b])
AM_INIT_AUTOMAKE([-Wall -Werror foreign])
AC_ARG_WITH([spot], [prefix of the spot installation], [
AC_SUBST([spot_prefix], [$withval])
], [AC_MSG_ERROR([Please, use --with-spot=DIR.])])
AC_PROG_CXX
AC_PROG_RANLIB
AM_PROG_LEX
AC_PROG_YACC
AC_CONFIG_FILES([Makefile src/Makefile libpn/Makefile doc/Makefile
doc/Doxyfile])
AC_OUTPUT
This diff is collapsed.
DOXYGEN = doxygen
.PHONY: doc
all-local: $(srcdir)/stamp
doc:
rm -f $(srcdir)/stamp
$(MAKE) $(srcdir)/stamp
$(srcdir)/stamp: $(srcdir)/Doxyfile.in $(top_srcdir)/configure.ac
$(MAKE) Doxyfile
rm -rf checkpn.html checkpn.latex
$(DOXYGEN)
cp $(srcdir)/results.html checkpn.html
touch $@
$(srcdir)/checkpn.html: $(srcdir)/stamp
checkpn.latex: $(srcdir)/stamp
$(srcdir)/checkpn.pdf: $(srcdir)/stamp
cd checkpn.latex \
&& texi2dvi --pdf refman.tex \
&& cd .. && mv -f checkpn.latex/refman.pdf $@
EXTRA_DIST = \
footer.html \
mainpage.dox \
$(srcdir)/stamp \
$(srcdir)/checkpn.html \
$(srcdir)/checkpn.pdf
<hr size="1">
Please <b>comment</b> this page and <b>report errors</b> about it on
<a href="http://spot.lip6.fr/wiki/RefDocComments">the RefDocComments page</a>.
<br><address style="align: right;"><small>
Generated on $datetime for $projectname by <a href="http://www.doxygen.org/index.html"><img src="doxygen.png" alt="doxygen" align="middle" border=0></a> $doxygenversion</small></address>
</body>
</html>
/*!
\mainpage
\section intro_sec Introduction
This document describes the implementation of a simple model checker called
\c checkpn and based on the object-oriented model checking library
<a href="http://spot.lip6.fr/wiki/">Spot</a>. It allows to check
<a href="http://en.wikipedia.org/wiki/Linear_temporal_logic">LTL</a>
formulae on ordinary
<a href="http://en.wikipedia.org/wiki/Petri_net">Petri nets</a>.
\li The Petri net is given in a file respecting the syntax defined for the
<a href="http://www.tcs.hut.fi/Software/prod/">Prod</a> tool
(a basic example is given below).
\li The LTL formula must respect the syntax defined by the
<a href="http://spot.lip6.fr/wiki/LtlSyntax">LTL parser</a> of Spot.
\li The atomic propositions are simply the names of the Petri net places.
In a given reachable marking, a proposition is satisfied if the
corresponding place contains at least one token.
After a short description on how install the tool and use it, the main line
followed for the implementation of checkpn is discussed. A last section is
dedicated to an evaluation of the overhead induced by Spot.
\section install_sec Downloading and installation
The package can be download at http://spot.lip6.fr/wiki/CheckPn
Instructions for the installation are in the file named \c INSTALL.
\section usage_sec Usage
The invocation command is of the form:
<tt>checkpn [OPTIONS...] petri_net_file</tt>
where \c OPTIONS are
Actions:
\li \c -c display the number of states and edges of the reachability graph,
\li \c -e display a sequence (if any) of the net satisfying the formula (implies
\c -f or \c -F),
\li \c -fformula check the formula \c formula,
\li \c -Fformula_file check the formula read from \c formula_file,
\li \c -g display the reachability graph of the Petri net,
Options for the translation of the formula into an automaton (implies \c -f or
\c -F):
\li \c -b branching postponement (\c false by default)
\li \c -l fair-loop approximation (\c false by default)
\li \c -x try to produce a more deterministic automaton (\c false by default)
\li \c -y do not merge states with same symbolic representation (\c true by
default)
For more explanations on the four last options of the tool, see the
documentation of the parameters of spot::ltl_to_tgba_fm().
A basic Petri net expressed with the syntax of the
<a href="http://www.tcs.hut.fi/Software/prod/">Prod</a> tool and composed by
four places and three transitions follows:
\verbinclude simple.net
In this format, <tt>\<..\></tt> designates an uncolored token. Here, all
the tokens have to be uncolored as \c checkpn is restricted to ordinary nets.
In the initial marking, place \c A contains two tokens, \c EX only one and the
other places are empty. The syntax used for transitions and their connectives
is easy to deduce from this net description. As an example, the LTL formula <tt>
G(B => F CS)</tt> respects the syntax of Spot and is valid for this net. An
atomic proposition is statisfied in a given marking if the
corresponding place contains at least one token. See the
<a href="http://spot.lip6.fr/wiki/LtlSyntax">LTL parser</a> documentation for
more details about the LTL syntax.
\verbatim
> ./checkpn -e -f'G(B => F CS)' ../samples/simple.net
5 unique states visited
2 strongly connected components in search stack
automaton construction time: 0
checking time: 0
an accepting run exists
Prefix:
G(FCS | !B) * [2.A + 1.EX]
| <B:0, CS:0>
Cycle:
FCS & G(FCS | !B) * [1.A + 1.B + 1.EX]
| <B:1, CS:0>
FCS & G(FCS | !B) * [2.B + 1.EX]
| <B:1, CS:0>
FCS & G(FCS | !B) * [1.B + 1.CS]
| <B:1, CS:1> {Acc[CS]}
G(FCS | !B) * [1.A + 1.B + 1.EX]
| <B:1, CS:0>
FCS & G(FCS | !B) * [2.B + 1.EX]
| <B:1, CS:0>
FCS & G(FCS | !B) * [1.B + 1.CS]
| <B:1, CS:1>
\endverbatim
As expected an example is found. At the opposite, the negation of the
formula leads to an empty product automaton.
\verbatim
> ./checkpn -e -f'!G(B => F CS)' ../samples/simple.net
8 unique states visited
0 strongly connected components in search stack
automaton construction time: 0
checking time: 0
no accepting run found
\endverbatim
\section implem_sec Implementation
The implementation of the model checker has been realized in two steps. At
first, we have developped a set of classes corresponding to the firing rule
of the Petri net theory. Secondly, these classes have been interfaced with the
Spot library to produce the final model checker.
\subsection basic_class_subsec Firing rule implementation
Three classes form the firing rule module:
\li ::marking which encodes a Petri net state as an integer vector.
\li compressed_marking which encodes a Petri net state as a bit vector for
performance issues.
\li petri_net which implements the firing rule of a Petri net and
offers a parsing function.
These classes have been developped independently of Spot. The methods of the
class petri_net are sufficient to produce the reachability graph step by step.
The most important methods of this class are:
\li ::marking* petri_net::get_initial_marking() const;
\li std::list<int>* petri_net::firable(const marking& m) const;
\li ::marking* petri_net::successor(const marking& m, int t) const;
Moreover, the class function petri_net::parse() allows to create a
petri_net from a file description.
All this stuff has been grouped in a library called libpn.
\subsection interfacing_spot_subsec Interfacing Spot
The manual of Spot (see the
<a href="http://spot.lip6.fr/wiki/InterfacingSpot">page</a>) explains
how to interface it with a state space generator. The main goal is to
masquerade the class petri_net as a
<a href="http://spot.lip6.fr/wiki/TGBA">TGBA</a>. More precisely, three
abstract classes of Spot have to be derivated:
\li spot::state representing a state of a TGBA,
\li spot::tgba_succ_iterator allowing to iterate throw the successors of
a state,
\li and spot::tgba representing a TGBA.
In our model checker, the corresponding derivated classes are:
\li pn_state which implements a spot::state by encapsulation of a
compressed_marking,
\li pn_succ_iterator implementing a spot::tgba_succ_iterator,
\li pn_tgba which implements a spot::tgba by encapsulation of a petri_net.
Based on this three new classes our model checker consists in the simple
following function <tt>check()</tt>. Notice that this function is a simplified
version of the one (model_check()) integrated in the model checker.
\code
void check(const petri_net* n, const spot::ltl::formula* f) {
// n is a petri_net returned by petri_net::parse();
// f is a formula returned by spot::ltl::parse();
// ensure these atomic propositions correspond to place names
// here the test is done a posteriori, we could also have checked
// the validity of the AP during the parsing using a customized
// environment.
const string* s;
if ((s = check_at_prop(n, f))) {
std::cout << "the atomic proposition '" << *s
<< "' does not correspond to a place name" << std::endl;
return;
}
// roughly speaking, a bdd_dict object maps a BDD variable to an atomic
// proposition and vice-versa
spot::bdd_dict dict;
// collect atomic propositions used in f
spot::ltl::atomic_prop_set* sap = spot::ltl::atomic_prop_collect(f);
// p is the tgba view of n
// the atomic propositions of sap will be registered in dict by the
// constructor
pn_tgba p(n, sap, &dict);
// a is the tgba view of f
// a and p share the same dictionary
spot::tgba* a = spot::ltl_to_tgba_fm(f, &dict);
// prod is simply the product of a and p
spot::tgba_product prod(a, &p);
// construct an emptiness checker for prod
spot::emptiness_check *ec= new spot::couvreur99_check(&prod);
// check the emptiness
spot::emptiness_check_result* res = ec->check();
if (res) {
std::cout << "an accepting run exists" << std::endl;
// construct and print a counter-example
spot::tgba_run* run = res->accepting_run();
if (run) {
spot::print_tgba_run(std::cout, &prod, run);
delete run;
}
else {
std::cout << "an accepting run exists (use option '-e' to print it)"
<< std::endl;
}
delete res;
}
else {
std::cout << "no accepting run found" << std::endl;
}
// print some statistics
ec->print_stats(std::cout);
delete ec;
delete a;
delete sap;
return;
}
\endcode
Notice that a formula given as a string can be easily translated in a
spot::ltl::formula object by the function spot::ltl::parse().
Some other examples of Spot usages are presented in the program.
\li In count_markings(), the function spot::stats_reachable() is called to
display some statistics concerning the reachabilty graph of a Petri net.
\li The class spot::tgba_reachable_iterator_breadth_first has been derivated
in marking_graph_visitor. This last class implements a visitor displaying
the reachability graph of a Petri net and its usage is illustrated in
print_reachability_graph().
\section perf_sec Performance Issues
To evaluate the overhead induced by the Spot library, we have developped a
simple tool based on the three basic Petri net classes (::marking,
compressed_marking and petri_net) presented above. This last tool, called \c rg,
visits all the reachable markings of a given Petri net and stores them in a
hash table.
The performances of \c rg have been compared with the ones of \c checkpn
using the option \c -c (the reachability graph is traversed and the number of
states and edges are computed).
\htmlonly
You can find <a href="results.html">here</a> the table resulting of these
experimentations.
\endhtmlonly
\latexonly
\begin{table}
\label{tab-perf}
\centering
\begin{tabular}{|l||r|r|r|r|r|} \hline
& & & Time for & Time for & Cost of \\
Model & \# states & \# edges & \texttt{checkpn} (sec.) & \texttt{rg} (sec.) &
\texttt{spot} (\%) \\ \hline\hline
Fms2 & 3444 & 16311 & 0,06 & 0,05 & 16,66 \\
Fms3 & 48590 & 297382 & 1,13 & 0,97 & 14,15 \\
Fms4 & 438600 & 3166985 & 15,54 & 13,24 & 14,8 \\ \hline
Kanban2 & 4600 & 28120 & 0,07 & 0,05 & 28,57 \\
Kanban3 & 58400 & 446400 & 1,19 & 0,97 & 18,48 \\
Kanban4 & 454475 & 3979850 & 11,22 & 9,43 & 15,95 \\ \hline
Philo5 & 1364 & 6375 & 0,03 & 0,02 & 33,33 \\
Philo6 & 5778 & 32406 & 0,16 & 0,13 & 18,75 \\
Philo7 & 24476 & 160153 & 1,25 & 0,98 & 21,6 \\
Philo8 & 103682 & 775336 & 13,16 & 9,69 & 26,36 \\
Philo9 & 439204 & 3694923 & 172,19 & 116,58 & 32,29 \\ \hline
Ring5 & 53856 & 263040 & 2,18 & 1,8 & 17,43 \\
Ring6 & 575296 & 3341568 & 102,95 & 82,94 & 19,43 \\ \hline
Mutex8 & 17497 & 81664 & 0,57 & 0,44 & 22,80 \\
Mutex10 & 196831 & 1181000 & 27,36 & 19,18 & 29,89 \\ \hline
Nb-philo20 & 15127 & 167240 & 5,35 & 3,99 & 25,42 \\
Nb-philo25 & 167761 & 2318400 & 562,12 & 426,6 & 24,1 \\ \hline
\end{tabular}
\caption{Evaluation of the overhead induced by \texttt{checkpn}}
\end{table}
The table \ref{tab-perf} resumes these experimentations.
\endlatexonly
The overhead induces by Spot seems to be very important (more than 30% with
respect to \c rg for at least one example). Independently of the indirection
implied by the derivation of abstract classes, the two implementations differ
by:
\li The expansion of compressed marking (compressed_marking::expand()) is
necessary in \c checkpn due to the interface of spot::tgba. Indeed, the method
spot::tgba::succ_iter() takes a spot::state* as parameter. Because states
are stored in a compressed form, we have to expand them for the computation of
the firable transitions. In \c rg, this step is avoided. The stack contains
only ordinary markings and they are compressed before to be stored in the hash
table.
\li The interface of the class spot::state implied the implementation of a
method spot::state::compare(). This method has to define a total order relation
on states. In \c rg, such a method is not necessary. STL hash tables only
impose to define a key equality function. We can alleged that such a function
is less expansive that the previous one.
This is only a first conclusion, the investigation is in progress...
*/
noinst_LIBRARIES = libpn.a
libpn_a_SOURCES = \
compressedmarking.cpp \
compressedmarking.hh \
marking.cpp \
marking.hh \
petrinet.cpp \
petrinet.hh \
pnscan.ll \
pnparse.yy
AM_YFLAGS = -d
BUILT_SOURCES = pnparse.h
\ No newline at end of file
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// This file is part of the Spot tutorial. Spot is a model checking
// library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#include <cassert>
#include <vector>
#include <iterator>
#include <algorithm>
#include <iostream>
#include "compressedmarking.hh"
compressed_marking::compressed_marking(const compressed_marking& m) : mac(m.mac) {
}
compressed_marking::compressed_marking(const marking& m) : mac() {
int i, j, nbp = m.size();
for (i=0; i<nbp; ++i) {
int p = m.get(i);
if (p<8) { // insert p false following by 1 true
for (j=0; j<p; ++j)
mac.push_back(false);
mac.push_back(true);
}
else { // insert 8 false following by p in reverse order
for (j=0; j<8; ++j)
mac.push_back(false);
const int mask = 1;
const int si=8*sizeof(int);
for (j=0; j<si; ++j, p>>=1)
if (mask & p)
mac.push_back(true);
else
mac.push_back(false);
}
}
}
marking* compressed_marking::expand() const {
marking* res = new marking;
int p=0, v=0, cpt=0;
std::vector<bool>::const_iterator it = mac.begin();
while (it!=mac.end()) {
if (!*it) {
++cpt;
++it;
if (cpt==8) { // the value follows
const int si=8*sizeof(int);
int mask = 1;
v=0;
for (int j=0;j<si;++j,++it,mask<<=1) {
if (*it) v+=mask;
}
res->append(v);
++p;
cpt=0;
}
} else {
++it;
res->append(cpt);
++p;
cpt=0;
}
}
return res;
}
void compressed_marking::print(std::ostream& os) const {
std::copy(mac.begin(), mac.end(), std::ostream_iterator<bool>(os, " "));
}
const std::vector<bool>& compressed_marking::get_vector() const {
return mac;
}
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// This file is part of the Spot tutorial. Spot is a model checking
// library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#ifndef COMPRESSED_MARKING_HH
#define COMPRESSED_MARKING_HH
#include <vector>
#include <iostream>
#include "marking.hh"
/// \brief Implementation of a compressed ordinary Petri net state (a bit vector).
class compressed_marking {
public:
compressed_marking(const compressed_marking& m);
/// \brief Construct a compression of \a m.
compressed_marking(const marking& m);
/// Return the corresponding expanded marking.
marking* expand() const;
/// \brief Basic printing method (as a vector of bits).
void print(std::ostream& os) const;
/// \brief Return the std::vector<bool> coding the marking.
const std::vector<bool>& get_vector() const;
protected:
std::vector<bool> mac;
};
#endif
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// This file is part of the Spot tutorial. Spot is a model checking
// library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#include <cassert>
#include <vector>
#include <iostream>
#include <algorithm>
#include <functional>
#include "marking.hh"
marking::marking(const marking& m) : ma(m.ma) {
}
marking::marking(int size) : ma(size,0) {
assert(size>=0);
}
void marking::insert(int p, int n) {
assert(0<=p && p< (int)ma.size());
ma[p]=n;
}
void marking::append(int n) {
ma.push_back(n);
}
int marking::get(int p) const {
assert(0<=p && p<(int)ma.size());
return ma[p];
}
int marking::size() const {
return ma.size();
}
bool marking::operator<=(const marking& m) const {
assert(ma.size() == m.ma.size());
std::pair<std::vector<int>::const_iterator, std::vector<int>::const_iterator>
res = std::mismatch(
ma.begin(), ma.end(),
m.ma.begin(),std::less_equal<int>());
return res.first == ma.end();
}
bool marking::operator>=(const marking& m) const {
assert(ma.size() == m.ma.size());
std::pair<std::vector<int>::const_iterator, std::vector<int>::const_iterator>
res = std::mismatch(
ma.begin(), ma.end(),
m.ma.begin(),std::greater_equal<int>());
return res.first == ma.end();