Main Page | Class Hierarchy | Class List | Directories | File List | Class Members | File Members

checkpn Documentation

0.0b

Introduction

This document describes the implementation of a simple model checker called checkpn and based on the object-oriented model checking library Spot. It allows to check LTL formulae on ordinary Petri nets.

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.

Downloading and installation

The package can be download at http://spot.lip6.fr/wiki/CheckPn

Instructions for the installation are in the file named INSTALL.

Usage

The invocation command is of the form:

checkpn [OPTIONS...] petri_net_file

where OPTIONS are

Actions:

Options for the translation of the formula into an automaton (implies -f or -F):

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 Prod tool and composed by four places and three transitions follows:

#place A mk(2*<..>)
#place B
#place CS
#place EX mk(<..>)

#trans t1
in {A:<..>;}
out {B:<..>;}
#endtr

#trans t2
in {B:<..>;EX:<..>;}
out {CS:<..>;}
#endtr

#trans t3
in {CS:<..>;}
out {A:<..>;EX:<..>;}
#endtr

In this format, <..> designates an uncolored token. Here, all the tokens have to be uncolored as checkpn is restricted to ordinary nets. In the initial marking, place A contains two tokens, 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 G(B => F CS) 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 LTL parser documentation for more details about the LTL syntax.

> ./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>

As expected an example is found. At the opposite, the negation of the formula leads to an empty product automaton.

> ./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

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.

Firing rule implementation

Three classes form the firing rule module:

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:

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.

Interfacing Spot

The manual of Spot (see the page) explains how to interface it with a state space generator. The main goal is to masquerade the class petri_net as a TGBA. More precisely, three abstract classes of Spot have to be derivated:

In our model checker, the corresponding derivated classes are:

Based on this three new classes our model checker consists in the simple following function check(). Notice that this function is a simplified version of the one (model_check()) integrated in the model checker.

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;
}

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.

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 rg, visits all the reachable markings of a given Petri net and stores them in a hash table.

The performances of rg have been compared with the ones of checkpn using the option -c (the reachability graph is traversed and the number of states and edges are computed).

You can find here the table resulting of these experimentations.

The overhead induces by Spot seems to be very important (more than 30% with respect to rg for at least one example). Independently of the indirection implied by the derivation of abstract classes, the two implementations differ by:

This is only a first conclusion, the investigation is in progress...
Please comment this page and report errors about it on the RefDocComments page.
Generated on Mon Jan 31 15:17:13 2005 for checkpn by doxygen 1.4.0