Struct WfNet 

pub struct WfNet<S = SoundnessUnknown> { /* private fields */ }

A workflow net (WF-net): a Petri net with a single source and sink place and a soundness state tracked at the type level by the S typestate parameter.

The S parameter is one of SoundnessUnknown (default), SoundnessClaimed, or SoundnessWitnessed — empty-enum markers used via PhantomData. The field/parameter is a claim about soundness, never a computed proof: WfNet::validate checks only structural WF-net shape (initial and final markings present), and the soundness transition methods merely re-type the claim; they do not compute soundness.

Structure-only: actual soundness witnessing graduates to wasm4pm, which produces the witness that justifies moving to SoundnessWitnessed.

Implementations

impl WfNet<SoundnessUnknown>

pub fn new(net: PetriNet, final_marking: Marking) -> Self

Construct a WF-net in the SoundnessUnknown state from a Petri net and a final marking.

use wasm4pm_compat::petri::{WfNet, PetriNet, Place, Transition, Arc, Marking};
let net = PetriNet::new(
    [Place::new("src"), Place::new("snk")],
    [Transition::new("t", "a")],
    [Arc::place_to_transition("src", "t"), Arc::transition_to_place("t", "snk")],
    Marking::new([("src".to_string(), 1)]),
);
let wf = WfNet::new(net, Marking::new([("snk".to_string(), 1)]));
assert!(wf.validate().is_ok());

impl<S> WfNet<S>

pub fn net(&self) -> &PetriNet

The underlying Petri net.

pub fn final_marking(&self) -> Option<&Marking>

The final marking, if declared.

pub fn validate(&self) -> Result<(), PetriRefusal>

Structurally validate the WF-net shape.

Checks that the underlying net is structurally well-formed, that an initial marking places at least one token (PetriRefusal::MissingInitialMarking), and that a final marking is declared (PetriRefusal::MissingFinalMarking). It does not check soundness, safeness, or boundedness — those graduate to wasm4pm.

use wasm4pm_compat::petri::{WfNet, PetriNet, Place, Transition, Arc, Marking, PetriRefusal};
// Initial marking is empty -> MissingInitialMarking.
let net = PetriNet::new(
    [Place::new("src"), Place::new("snk")],
    [Transition::new("t", "a")],
    [Arc::place_to_transition("src", "t"), Arc::transition_to_place("t", "snk")],
    Marking::empty(),
);
let wf = WfNet::new(net, Marking::new([("snk".to_string(), 1)]));
assert_eq!(wf.validate(), Err(PetriRefusal::MissingInitialMarking));

pub fn claim_sound(self) -> WfNet<SoundnessClaimed>

Re-type this WF-net as carrying a soundness claim (unproven here).

This is a type-level re-tagging only — it computes nothing. Use it to record that an upstream source asserts soundness; discharge the claim by graduating to wasm4pm and witnessing it.

use wasm4pm_compat::petri::{WfNet, PetriNet, Marking, SoundnessClaimed};
let wf = WfNet::new(PetriNet::default(), Marking::new([("snk".to_string(), 1)]));
let _claimed: WfNet<SoundnessClaimed> = wf.claim_sound();

Trait Implementations

impl<S: Clone> Clone for WfNet<S>

fn clone(&self) -> WfNet<S>

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<S: Debug> Debug for WfNet<S>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<S: Eq> Eq for WfNet<S>

impl<S: PartialEq> PartialEq for WfNet<S>

fn eq(&self, other: &WfNet<S>) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl<S> StructuralPartialEq for WfNet<S>