`checkpn`

and based on the object-oriented model checking library Spot. It allows to check LTL formulae on ordinary Petri nets.

- The Petri net is given in a file respecting the syntax defined for the Prod tool (a basic example is given below).
- The LTL formula must respect the syntax defined by the LTL parser of Spot.
- 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.

Instructions for the installation are in the file named `INSTALL`

.

`checkpn [OPTIONS...] petri_net_file`

where `OPTIONS`

are

Actions:

`-c`

display the number of states and edges of the reachability graph,`-e`

display a sequence (if any) of the net satisfying the formula (implies`-f`

or`-F`

),`-fformula`

check the formula`formula`

,`-Fformula_file`

check the formula read from`formula_file`

,`-g`

display the reachability graph of the Petri net,

`-f`

or `-F`

):

`-b`

branching postponement (`false`

by default)`-l`

fair-loop approximation (`false`

by default)`-x`

try to produce a more deterministic automaton (`false`

by default)`-y`

do not merge states with same symbolic representation (`true`

by default)

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

- marking which encodes a Petri net state as an integer vector.
- compressed_marking which encodes a Petri net state as a bit vector for performance issues.
- petri_net which implements the firing rule of a Petri net and offers a parsing function.

- marking* petri_net::get_initial_marking() const;
- std::list<int>* petri_net::firable(const marking& m) const;
- marking* petri_net::successor(const marking& m, int t) const;

All this stuff has been grouped in a library called libpn.

- spot::state representing a state of a TGBA,
- spot::tgba_succ_iterator allowing to iterate throw the successors of a state,
- and spot::tgba representing a TGBA.

- pn_state which implements a spot::state by encapsulation of a compressed_marking,
- pn_succ_iterator implementing a spot::tgba_succ_iterator,
- pn_tgba which implements a spot::tgba by encapsulation of a petri_net.

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

- In count_markings(), the function spot::stats_reachable() is called to display some statistics concerning the reachabilty graph of a Petri net.
- 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().

`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:

- The expansion of compressed marking (compressed_marking::expand()) is necessary in
`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`rg`

, this step is avoided. The stack contains only ordinary markings and they are compressed before to be stored in the hash table.

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

Please

Generated on Mon Jan 31 15:17:13 2005 for checkpn by 1.4.0