wasm4pm_compat/
petri.rs

1pub use crate::models::{Arc, PetriNet, PetriNetRefusal, Place, Transition};
2use crate::law::SoundnessState;
3use std::fmt;
4use std::marker::PhantomData;
5
6// ── Marking ──────────────────────────────────────────────────────────────────
7
8/// A token distribution over places — the runtime state of a Petri net.
9#[derive(Debug, Clone, Default)]
10pub struct Marking {
11    tokens: Vec<(String, usize)>,
12}
13
14impl Marking {
15    pub fn new(tokens: impl IntoIterator<Item = (String, usize)>) -> Self {
16        Marking { tokens: tokens.into_iter().collect() }
17    }
18
19    pub fn empty() -> Self { Marking::default() }
20
21    pub fn is_empty(&self) -> bool { self.tokens.is_empty() }
22
23    pub fn tokens(&self) -> &[(String, usize)] { &self.tokens }
24}
25
26// ── PetriRefusal ─────────────────────────────────────────────────────────────
27
28/// Named refusal variants for Petri net validation laws.
29///
30/// Every variant names a specific law from van der Aalst's workflow net theory.
31#[derive(Debug, Clone, PartialEq, Eq)]
32pub enum PetriRefusal {
33    /// No final marking provided — a workflow net requires a defined sink state.
34    MissingFinalMarking,
35    /// An arc is typed but its object type is not declared in the net's type set.
36    ObjectTypeNotPreserved,
37}
38
39impl fmt::Display for PetriRefusal {
40    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
41        match self {
42            PetriRefusal::MissingFinalMarking => write!(f, "MissingFinalMarking"),
43            PetriRefusal::ObjectTypeNotPreserved => write!(f, "ObjectTypeNotPreserved"),
44        }
45    }
46}
47
48impl std::error::Error for PetriRefusal {}
49
50// ── WfNet typestate ───────────────────────────────────────────────────────────
51
52/// Typestate marker: soundness has been asserted (not verified by replay).
53pub struct SoundnessClaimed;
54
55/// Typestate marker: soundness has been witnessed by token replay.
56pub struct SoundnessWitnessed;
57
58/// Default typestate: no soundness claim has been made yet.
59///
60/// Users cannot construct `WfNet<Unchecked>` by naming the type parameter —
61/// they use `WfNet::new()` which returns `WfNet<Unchecked>` by inference.
62pub struct Unchecked;
63
64/// A workflow net — a Petri net with a designated final marking.
65///
66/// The typestate parameter `S` tracks soundness evidence:
67/// - `WfNet<Unchecked>` — no soundness claim made
68/// - `WfNet<SoundnessClaimed>` — caller asserted soundness via `claim_sound()`
69/// - `WfNet<SoundnessWitnessed>` — soundness verified by token replay
70pub struct WfNet<S = Unchecked> {
71    net: PetriNet,
72    final_marking: Marking,
73    _s: PhantomData<S>,
74}
75
76impl WfNet<Unchecked> {
77    pub fn new(net: PetriNet, final_marking: Marking) -> Self {
78        WfNet { net, final_marking, _s: PhantomData }
79    }
80
81    #[must_use]
82    pub fn claim_sound(self) -> WfNet<SoundnessClaimed> {
83        WfNet { net: self.net, final_marking: self.final_marking, _s: PhantomData }
84    }
85}
86
87impl<S> WfNet<S> {
88    #[must_use]
89    pub fn validate(&self) -> Result<(), PetriRefusal> {
90        if self.final_marking.is_empty() {
91            return Err(PetriRefusal::MissingFinalMarking);
92        }
93        Ok(())
94    }
95
96    #[must_use]
97    pub fn final_marking(&self) -> Option<&Marking> {
98        if self.final_marking.is_empty() { None } else { Some(&self.final_marking) }
99    }
100
101    pub fn net(&self) -> &PetriNet { &self.net }
102}
103
104// ── ObjectCentricPetriNet ─────────────────────────────────────────────────────
105
106/// A Petri net extended with object-type annotations on arcs,
107/// per the OCPN model from van der Aalst et al.
108#[derive(Debug, Clone)]
109pub struct ObjectCentricPetriNet {
110    net: PetriNet,
111    object_types: Vec<String>,
112}
113
114impl ObjectCentricPetriNet {
115    pub fn new(net: PetriNet, object_types: impl IntoIterator<Item = String>) -> Self {
116        ObjectCentricPetriNet { net, object_types: object_types.into_iter().collect() }
117    }
118
119    pub fn net(&self) -> &PetriNet { &self.net }
120    pub fn object_types(&self) -> &[String] { &self.object_types }
121
122    #[must_use]
123    pub fn validate(&self) -> Result<(), PetriRefusal> {
124        let type_set: std::collections::HashSet<&str> =
125            self.object_types.iter().map(|s| s.as_str()).collect();
126        for arc in &self.net.arcs {
127            if let Some((ref ot, _)) = arc.object_type {
128                if !type_set.contains(ot.as_str()) {
129                    return Err(PetriRefusal::ObjectTypeNotPreserved);
130                }
131            }
132        }
133        Ok(())
134    }
135}
136
137// ── PetriNet/Place/Transition accessor methods ────────────────────────────────
138
139impl Place {
140    pub fn id(&self) -> &str { &self.id }
141}
142
143impl Transition {
144    pub fn id(&self) -> &str { &self.id }
145}
146
147impl PetriNet {
148    pub fn places(&self) -> &[Place] { &self.places }
149    pub fn transitions(&self) -> &[Transition] { &self.transitions }
150    pub fn arcs(&self) -> &[Arc] { &self.arcs }
151    pub fn initial_marking(&self) -> RuntimeMarking<'_> { RuntimeMarking { net: self } }
152}
153
154/// Read-only view of the initial marking backed by the PetriNet's PackedKeyTable.
155pub struct RuntimeMarking<'a> {
156    net: &'a PetriNet,
157}
158
159impl<'a> RuntimeMarking<'a> {
160    /// Returns the token count on a named place, or 0 if not marked.
161    pub fn tokens_on(&self, place_id: &str) -> usize {
162        use crate::dense_kernel::fnv1a_64;
163        let hash = fnv1a_64(place_id.as_bytes());
164        *self.net.initial_marking.get(hash).unwrap_or(&0)
165    }
166}
167
168// ── Marking::tokens_on ───────────────────────────────────────────────────────
169
170impl Marking {
171    /// Returns the token count on a named place, or 0 if absent.
172    pub fn tokens_on(&self, place_id: &str) -> usize {
173        self.tokens.iter()
174            .find(|(id, _)| id == place_id)
175            .map(|(_, n)| *n)
176            .unwrap_or(0)
177    }
178}
179
180// ── ObjectChange builder ──────────────────────────────────────────────────────
181
182impl crate::ocel::ObjectChange {
183    /// Builder: add a timestamp to this change (no-op stub — ObjectChange is
184    /// currently structure-only; `at_ns` is reserved for future OCEL 2.0 typing).
185    #[must_use]
186    pub fn at_ns(self, _ns: u64) -> Self { self }
187}
188
189// ── Node-kind markers and typed arc structs ───────────────────────────────────
190
191/// Sealed marker: this type represents a place node.
192pub struct PlaceNodeMarker;
193
194/// Sealed marker: this type represents a transition node.
195pub struct TransitionNodeMarker;
196
197/// A pre-incidence (place → transition) arc carrying a typed weight.
198///
199/// The phantom types `P` and `T` name the place and transition namespaces;
200/// the weight type `W` names the arc multiplicity type (usually `u32`).
201pub struct PlaceToTransitionArc<P, T, W> {
202    w: W,
203    _p: PhantomData<(P, T)>,
204}
205
206impl<P, T, W: Copy> PlaceToTransitionArc<P, T, W> {
207    pub fn new(weight: W) -> Self {
208        PlaceToTransitionArc { w: weight, _p: PhantomData }
209    }
210    pub fn weight(&self) -> W { self.w }
211}
212
213/// A post-incidence (transition → place) arc carrying a typed weight.
214pub struct TransitionToPlaceArc<T, P, W> {
215    w: W,
216    _p: PhantomData<(T, P)>,
217}
218
219impl<T, P, W: Copy> TransitionToPlaceArc<T, P, W> {
220    pub fn new(weight: W) -> Self {
221        TransitionToPlaceArc { w: weight, _p: PhantomData }
222    }
223    pub fn weight(&self) -> W { self.w }
224}
225
226// ── WfNetConst — const-generic soundness typestate ────────────────────────────
227
228mod wfnet_seal {
229    pub(super) struct WfNetSeal;
230}
231
232/// Proof token that soundness has been verified (crate-internal only).
233pub struct SoundnessProof(wfnet_seal::WfNetSeal);
234
235impl SoundnessProof {
236    pub(crate) fn new() -> Self { SoundnessProof(wfnet_seal::WfNetSeal) }
237}
238
239/// A workflow net whose soundness state is embedded as a const generic parameter.
240///
241/// `SoundnessState::Unknown` is freely constructible.
242/// `SoundnessState::Claimed` is reachable via `.claim_sound()`.
243/// `SoundnessState::Witnessed` requires a `SoundnessProof` token — non-forgeable.
244pub struct WfNetConst<const SOUNDNESS: SoundnessState> {
245    _seal: (),
246}
247
248impl WfNetConst<{ SoundnessState::Unknown }> {
249    pub fn new() -> Self { WfNetConst { _seal: () } }
250
251    /// Advance: Unknown → Claimed (type-level re-tag, zero cost).
252    #[must_use]
253    pub fn claim_sound(self) -> WfNetConst<{ SoundnessState::Claimed }> {
254        WfNetConst { _seal: () }
255    }
256}
257
258impl WfNetConst<{ SoundnessState::Claimed }> {
259    /// Advance: Claimed → Witnessed, guarded by a `SoundnessProof` token.
260    ///
261    /// `SoundnessProof` is only constructible inside the petri module, making
262    /// this transition non-forgeable from external code.
263    #[must_use]
264    pub fn witness_soundness(self, _proof: SoundnessProof) -> WfNetConst<{ SoundnessState::Witnessed }> {
265        WfNetConst { _seal: () }
266    }
267}
268
269impl<const S: SoundnessState> WfNetConst<S> {
270    pub fn soundness_state(&self) -> SoundnessState { S }
271}
272
273// ── WfNetQuery ────────────────────────────────────────────────────────────────
274
275/// Query interface for WF-net structural properties (reserved for future use).
276pub struct WfNetQuery;
277
278#[cfg(test)]
279mod tests {
280    use super::*;
281    use crate::law::SoundnessState;
282
283    #[test]
284    fn soundness_proof_mints_and_advances_to_witnessed() {
285        // SoundnessProof::new() is pub(crate) — this test is the only caller,
286        // which is the point: it proves the sealed capability works end-to-end.
287        let proof = SoundnessProof::new();
288        let witnessed = WfNetConst::<{ SoundnessState::Unknown }>::new()
289            .claim_sound()
290            .witness_soundness(proof);
291        assert_eq!(witnessed.soundness_state(), SoundnessState::Witnessed);
292    }
293}
wasm4pm_compat/petri.rs

wasm4pm_compat/
petri.rs
