mxcl/homebrew — pull request #22649 by nlohmann (2013-09-18 10:35:46+00:00)
Title: Sara: 1.0 - Deciding reachability for Petri nets

Sara is a tool for solving the reachability problem for Petri nets. Given a
low-level Petri net, i.e. sets of places and transitions with weighted arcs
between them, and an initial and a final marking, Sara tries to determine
whether the final marking can be reached from the initial marking by firing a
sequence of transitions in the Petri net. While the initial marking must be a
map from the places to non-negative integers, that means one single marking,
the final marking can be somewhat generalized. It is possible -- for each place
on its own -- to declare that the given number must be reached exactly (as for
the initial marking), covered (a higher value is allowed), or bounded (a lower
value is permissible). In addition, more general constraints may be formulated
which the final marking must fulfill. Such a constraint can be any linear
(in)equation built from places and transitions.

As a by-product, also problems of form ``given a Petri net, an initial marking,
and a transition multiset, is the multiset realizable?'' can be solved.
Realizable means that there is a firing sequence in the Petri net that contains
each transition exactly as often as the transition multiset dictates.

If Sara can compute the problem given, it should either tell the user that
there is a solution and present a firing sequence proving this, or it should
tell that the problem is infeasible. In the latter case, Sara might provide
additional information that gives some insight into why the problem is
infeasible.