Skip to main content

Crate libpetri_runtime

Crate libpetri_runtime 

Source
Expand description

§libpetri-runtime — Petri Net Executors

Provides two executors for running Coloured Time Petri Nets defined with libpetri-core.

§BitmapNetExecutor

The general-purpose executor. Single-threaded orchestrator with concurrent async actions.

ExecutorExample p_start start t_fork fork prio=5 p_start->t_fork p_branch_b branch_b t_process_b process_b [0, 5000]ms p_branch_b->t_process_b p_branch_a branch_a t_process_a process_a [100, ∞)ms p_branch_a->t_process_a p_join join t_complete complete p_join->t_complete ×2 p_done done t_fork->p_branch_b t_fork->p_branch_a t_process_a->p_join t_process_b->p_join t_complete->p_done

§Execution Loop (5 phases per cycle)

  1. Process completed — collect outputs from finished async actions
  2. Process events — inject tokens from environment places
  3. Update dirty — re-evaluate enablement via bitmap masks (O(W) where W = ceil(places/64))
  4. Fire ready — sorted by priority, then FIFO by enablement time
  5. Await work — sleep until action completes, timer fires, or event arrives

§Key types

§PrecompiledNetExecutor

A high-performance alternative optimized for throughput-critical workloads.

PrecompiledExample p_p4 p4 t_step_5 step_5 p_p4->t_step_5 p_p5 p5 p_p3 p3 t_step_4 step_4 p_p3->t_step_4 p_p1 p1 t_step_2 step_2 p_p1->t_step_2 p_p0 p0 t_step_1 step_1 p_p0->t_step_1 p_p2 p2 t_step_3 step_3 p_p2->t_step_3 t_step_1->p_p1 t_step_2->p_p2 t_step_3->p_p3 t_step_4->p_p4 t_step_5->p_p5

Additional optimizations over BitmapNetExecutor:

  • Ring buffer token storage (flat Vec<Option<ErasedToken>> pool)
  • Opcode-based consume dispatch (CONSUME_ONE, CONSUME_N, CONSUME_ALL, RESET)
  • Two-level summary bitmaps for dirty/enabled iteration
  • Reusable HashMap buffers reclaimed via take_inputs()/take_reads()
  • Priority-partitioned ready queues

§Key types

§Compilation Pipeline

PetriNet ──► CompiledNet ──► PrecompiledNet (optional)
             (bitmap masks)   (ring buffers, opcodes)

§Marking

Marking holds the mutable token state — type-erased FIFO queues per place, with typed access via Place<T> references.

§Async Support

Enable the tokio feature for run_async() on both executors. This allows transition actions to be async (CompletableFuture-style) with external event injection via environment places.

Modules§

bitmap
compiled_net
environment
executor
marking
precompiled_executor
precompiled_net