Skip to main content

Crate libpetri

Crate libpetri 

Source
Expand description

§libpetri — Coloured Time Petri Net Engine

A high-performance Petri net engine with formal verification support.

§Quick Start

use libpetri::*;

let p1 = Place::<i32>::new("input");
let p2 = Place::<i32>::new("output");

let t = Transition::builder("process")
    .input(one(&p1))
    .output(out_place(&p2))
    .action(fork())
    .build();

let net = PetriNet::builder("example").transition(t).build();

let mut marking = Marking::new();
marking.add(&p1, Token::at(42, 0));

let mut executor = BitmapNetExecutor::<NoopEventStore>::new(
    &net, marking, ExecutorOptions::default(),
);
executor.run_sync();

assert_eq!(*executor.marking().peek(&p2).unwrap(), 42);

§Example: Basic Chain

basic_chain p_p2 p2 t_t2 t2 p_p2->t_t2 p_p3 p3 p_p1 p1 t_t1 t1 p_p1->t_t1 t_t1->p_p2 t_t2->p_p3

§Example: Order Processing Pipeline

A showcase net demonstrating all arc types (input, output, read, inhibitor, reset), both place types (regular + environment), all timing modes (immediate, deadline, delayed, window, exact), and patterns (AND-fork, AND-join, XOR, priority).

OrderProcessingPipeline p_Ready Ready t_Ship Ship p_Ready->t_Ship p_CancelRequest CancelRequest t_Cancel Cancel p_CancelRequest->t_Cancel p_PaymentFailed PaymentFailed t_RetryPayment RetryPayment [1000, ∞) p_PaymentFailed->t_RetryPayment t_Reject Reject p_PaymentFailed->t_Reject p_Overdue Overdue p_Overdue->t_RetryPayment p_Overdue->t_Reject t_Monitor Monitor [10000, 10000] p_Overdue->t_Monitor p_Active Active p_Active->t_Ship p_Active->t_Monitor p_PaymentOk PaymentOk t_Approve Approve [0, 2000] p_PaymentOk->t_Approve p_Validating Validating t_Authorize Authorize [200, 5000] p_Validating->t_Authorize p_Shipped Shipped p_Shipped->t_Cancel p_Shipped->t_Monitor p_Cancelled Cancelled p_Cancelled->t_Ship p_Cancelled->t_Monitor p_Rejected Rejected p_Rejected->t_Cancel p_Rejected->t_Monitor p_Order Order t_Receive Receive P=10 p_Order->t_Receive p_InStock InStock p_InStock->t_Approve t_Receive->p_Active t_Receive->p_Validating t_Receive->p_InStock t_Authorize->p_PaymentFailed PaymentFailed t_Authorize->p_PaymentOk PaymentOk t_RetryPayment->p_PaymentFailed PaymentFailed t_RetryPayment->p_PaymentOk PaymentOk t_Approve->p_Ready t_Ship->p_Shipped t_Reject->p_Rejected t_Reject->p_InStock t_Cancel->p_Cancelled t_Monitor->p_Overdue

§Crate Structure

  • core — Places, tokens, transitions, timing, actions
  • event — Event store for recording execution events
  • runtime — Bitmap-based executor (sync + async)
  • export — DOT/Graphviz export pipeline
  • verification — Formal verification (P-invariants, state class graphs, SMT)

Re-exports§

pub use libpetri_core as core;
pub use libpetri_event as event;
pub use libpetri_export as export;
pub use libpetri_runtime as runtime;
pub use libpetri_verification as verification;

Structs§

ActionError
Error returned by transition actions.
BitmapNetExecutor
Bitmap-based executor for Coloured Time Petri Nets.
CompiledNet
Integer-indexed, precomputed representation of a PetriNet for bitmap-based execution.
EnvironmentPlace
An environment place that accepts external token injection. Wraps a regular Place and marks it for external event injection.
ExecutorOptions
Options for constructing a BitmapNetExecutor.
InMemoryEventStore
In-memory event store for debugging and testing.
Inhibitor
Inhibitor arc: blocks transition if place has tokens.
Marking
Mutable token state of a Petri net during execution.
NoopEventStore
No-op event store for production use.
PetriNet
Immutable definition of a Time Petri Net structure.
Place
A typed place in the Petri Net that holds tokens of a specific type.
PlaceRef
Type-erased reference to a place, used internally for arc storage.
PrecompiledExecutorBuilder
Builder for PrecompiledNetExecutor.
PrecompiledNet
Precompiled flat-array net representation for the super::precompiled_executor::PrecompiledNetExecutor.
PrecompiledNetExecutor
High-performance precompiled flat-array Petri net executor.
Read
Read arc: requires token without consuming.
Reset
Reset arc: removes all tokens from place when firing.
Token
An immutable token carrying a typed value through the Petri net.
Transition
A transition in the Time Petri Net that transforms tokens.
TransitionContext
Context provided to transition actions.

Enums§

In
Input specification with cardinality and optional guard predicate.
NetEvent
All observable events during Petri net execution.
Out
Output specification with explicit split semantics.
Timing
Firing timing specification for transitions.

Traits§

EventStore
Trait for event storage during Petri net execution.

Functions§

all
Consume all available tokens (must be 1+).
and
AND-split: all children must receive tokens.
and_places
AND-split from places: all places must receive tokens.
async_action
Creates an action from an async closure.
at_least
Wait for N+ tokens, consume all when enabled.
deadline
Immediate with deadline: can fire immediately, must fire by deadline.
delayed
Delayed firing: must wait, then can fire anytime.
dot_export
Convenience function: maps a PetriNet to DOT format string.
exact
Exact timing: fires at precisely the specified time.
exactly
Consume exactly N tokens from the place.
fork
Fork action: copies single input token to all outputs.
forward_input
Forward consumed input value to output place on timeout.
immediate
Immediate firing: can fire as soon as enabled, no deadline.
inhibitor
Creates an inhibitor arc for the given place.
one
Consume exactly 1 token from the place.
out_place
Leaf output spec for a single place.
passthrough
Identity action: produces no outputs. Executes synchronously.
produce
Produce action: produces a single token with the given value to the specified place.
read
Creates a read arc for the given place.
reset
Creates a reset arc for the given place.
sync_action
Creates an action from a synchronous closure.
timeout
Timeout output: activates if action exceeds duration.
timeout_place
Timeout output pointing to a single place.
transform
Transform action: applies function to context, copies result to ALL output places.
window
Time window: can fire within [earliest, latest].
xor
XOR-split: exactly one child receives token.
xor_places
XOR-split from places: exactly one place receives token.

Type Aliases§

BoxedAction
Type alias for boxed transition actions.