# petrex v1.0.0 - Table of Contents

> Place/transition Petri nets for the BEAM: analysis first, PNML interchange, one OTP executor.

## Pages

- [Petrex](readme.md)
- [Design notes](notes.md)
- [Benchmarks](bench.md)
- [Changelog](changelog.md)

## Modules

- [Petrex](Petrex.md): Place/transition Petri nets for the BEAM, with analysis as the primary product.
- [Petrex.Analysis](Petrex.Analysis.md): Analysis of a net's skeleton.
- [Petrex.Analysis.CoverabilityTree](Petrex.Analysis.CoverabilityTree.md): A Karp–Miller coverability tree, as built by
`Petrex.Analysis.coverability/3`.
- [Petrex.Analysis.ReachabilityGraph](Petrex.Analysis.ReachabilityGraph.md): An explicit reachability graph, as built by `Petrex.Analysis.reachability/3`.
- [Petrex.Arc](Petrex.Arc.md): A weighted arc between a place and a transition.
- [Petrex.Marking](Petrex.Marking.md): Markings in their two representations.
- [Petrex.Net](Petrex.Net.md): A place/transition net with an initial token marking.
- [Petrex.PNML](Petrex.PNML.md): PNML (ISO/IEC 15909-2) interchange for place/transition nets.
- [Petrex.Place](Petrex.Place.md): A place of a Petri net.
- [Petrex.Runner](Petrex.Runner.md): Runs one net instance in a GenServer.
- [Petrex.Transition](Petrex.Transition.md): A transition of a Petri net.

- Exceptions
  - [Petrex.InconclusiveError](Petrex.InconclusiveError.md): Raised by the boolean analysis functions (`Petrex.Analysis.bounded?/3`,
`Petrex.Analysis.safe?/3`) when the exploration limit was reached before
the property was decided. A boolean cannot express "unknown", so they
raise rather than answer; the tuple-returning counterparts report the same
situation as `{:partial, result}`.
  - [Petrex.InvalidNetError](Petrex.InvalidNetError.md): Raised when a function that requires a well-formed net receives one that
fails `Petrex.Net.validate/1`. `errors` holds the validation errors.

