wasm4pm-compat 26.6.23

//! Petri-net shapes — typed places/transitions/arcs and const-generic soundness.
//!
//! ## What this module IS
//!
//! - The structural shape of a (workflow) Petri net: bipartite typed arcs,
//!   `WfNetConst<SOUNDNESS>` carrying a non-forgeable soundness typestate, and
//!   `SeparableWfNet` whose private seal makes a separability claim unforgeable.
//!
//! ## What this module is **NOT**
//!
//! - **Not** a soundness checker or token-replay engine. The soundness *witness*
//!   is issued by a proof token; this crate never *computes* soundness, fires a
//!   transition, or explores a marking graph.
//!
//! Structure only. Graduate to `wasm4pm` to *decide* soundness or replay tokens.

use crate::law::SoundnessState;
pub use crate::models::{Arc, ArcDirection, PetriNet, PetriNetRefusal, Place, Transition};
use std::fmt;
use std::marker::PhantomData;

// ── Marking ──────────────────────────────────────────────────────────────────

/// A token distribution over places — the runtime state of a Petri net.
#[derive(Debug, Clone, Default)]
pub struct Marking {
    tokens: Vec<(String, usize)>,
}

impl Marking {
    pub fn new(tokens: impl IntoIterator<Item = (String, usize)>) -> Self {
        Marking {
            tokens: tokens.into_iter().collect(),
        }
    }

    pub fn empty() -> Self {
        Marking::default()
    }

    pub fn is_empty(&self) -> bool {
        self.tokens.is_empty()
    }

    pub fn tokens(&self) -> &[(String, usize)] {
        &self.tokens
    }
}

// ── PetriRefusal ─────────────────────────────────────────────────────────────

/// Named refusal variants for Petri net validation laws.
///
/// Every variant names a specific law from van der Aalst's workflow net theory.
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum PetriRefusal {
    MissingInitialMarking,
    MissingFinalMarking,
    DeadTransition,
    UnsafeNet,
    UnboundedNet,
    ObjectTypeNotPreserved,
    InvalidVariableArc,
    SoundnessNotWitnessed,
    InvalidCancellationRegion,
    InvalidInstanceBounds,
}

impl fmt::Display for PetriRefusal {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        let law = match self {
            PetriRefusal::MissingInitialMarking => "MissingInitialMarking",
            PetriRefusal::MissingFinalMarking => "MissingFinalMarking",
            PetriRefusal::DeadTransition => "DeadTransition",
            PetriRefusal::UnsafeNet => "UnsafeNet",
            PetriRefusal::UnboundedNet => "UnboundedNet",
            PetriRefusal::ObjectTypeNotPreserved => "ObjectTypeNotPreserved",
            PetriRefusal::InvalidVariableArc => "InvalidVariableArc",
            PetriRefusal::SoundnessNotWitnessed => "SoundnessNotWitnessed",
            PetriRefusal::InvalidCancellationRegion => "InvalidCancellationRegion",
            PetriRefusal::InvalidInstanceBounds => "InvalidInstanceBounds",
        };
        write!(f, "Petri-net refused by law: {law}")
    }
}

impl std::error::Error for PetriRefusal {}

// ── WfNet typestate ───────────────────────────────────────────────────────────

/// Typestate marker: soundness has been asserted (not verified by replay).
pub struct SoundnessClaimed;

/// Typestate marker: soundness has been witnessed by token replay.
pub struct SoundnessWitnessed;

/// Default typestate: no soundness claim has been made yet.
pub struct SoundnessUnknown;

/// Alias for compatibility.
pub type Unchecked = SoundnessUnknown;

/// A workflow net — a Petri net with a designated final marking.
///
/// The typestate parameter `S` tracks soundness evidence:
/// - `WfNet<SoundnessUnknown>` — no soundness claim made
/// - `WfNet<SoundnessClaimed>` — caller asserted soundness via `claim_sound()`
/// - `WfNet<SoundnessWitnessed>` — soundness verified by token replay
pub struct WfNet<S = SoundnessUnknown> {
    net: PetriNet,
    final_marking: Marking,
    _s: PhantomData<S>,
}

/// Phantom-typed proof carrier for workflow net soundness.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub struct WfNetSoundnessProofOf<Net> {
    _seal: (),
    _marker: std::marker::PhantomData<Net>,
}

impl<Net> WfNetSoundnessProofOf<Net> {
    #[allow(dead_code)]
    pub(crate) fn new() -> Self {
        WfNetSoundnessProofOf {
            _seal: (),
            _marker: std::marker::PhantomData,
        }
    }
}

impl WfNet<SoundnessUnknown> {
    pub fn new(net: PetriNet, final_marking: Marking) -> Self {
        WfNet {
            net,
            final_marking,
            _s: PhantomData,
        }
    }

    #[must_use]
    pub fn claim_sound(self) -> WfNet<SoundnessClaimed> {
        WfNet {
            net: self.net,
            final_marking: self.final_marking,
            _s: PhantomData,
        }
    }
}

impl<S> WfNet<S> {
    pub fn validate(&self) -> Result<(), PetriRefusal> {
        if self.final_marking.is_empty() {
            return Err(PetriRefusal::MissingFinalMarking);
        }
        Ok(())
    }

    #[must_use]
    pub fn final_marking(&self) -> Option<&Marking> {
        if self.final_marking.is_empty() {
            None
        } else {
            Some(&self.final_marking)
        }
    }

    pub fn net(&self) -> &PetriNet {
        &self.net
    }
}

// ── ObjectCentricPetriNet ─────────────────────────────────────────────────────

/// A Petri net extended with object-type annotations on arcs,
/// per the OCPN model from van der Aalst et al.
#[derive(Debug, Clone)]
pub struct ObjectCentricPetriNet {
    net: PetriNet,
    object_types: Vec<String>,
}

impl ObjectCentricPetriNet {
    pub fn new(net: PetriNet, object_types: impl IntoIterator<Item = String>) -> Self {
        ObjectCentricPetriNet {
            net,
            object_types: object_types.into_iter().collect(),
        }
    }

    pub fn net(&self) -> &PetriNet {
        &self.net
    }
    pub fn object_types(&self) -> &[String] {
        &self.object_types
    }

    pub fn validate(&self) -> Result<(), PetriRefusal> {
        let type_set: std::collections::HashSet<&str> =
            self.object_types.iter().map(|s| s.as_str()).collect();
        for arc in &self.net.arcs {
            if let Some((ref ot, _)) = arc.object_type {
                if !type_set.contains(ot.as_str()) {
                    return Err(PetriRefusal::ObjectTypeNotPreserved);
                }
            }
        }
        Ok(())
    }
}

// ── PetriNet/Place/Transition accessor methods ────────────────────────────────

impl Place {
    pub fn id(&self) -> &str {
        &self.id
    }
}

impl Transition {
    pub fn id(&self) -> &str {
        &self.id
    }
    pub fn label(&self) -> &str {
        &self.label
    }
    pub fn is_silent(&self) -> bool {
        self.is_invisible.unwrap_or(false)
    }
    pub fn silent(id: &str) -> Self {
        Transition {
            id: id.to_owned(),
            label: String::new(),
            is_invisible: Some(true),
        }
    }
}

impl PetriNet {
    pub fn places(&self) -> &[Place] {
        &self.places
    }
    pub fn transitions(&self) -> &[Transition] {
        &self.transitions
    }
    pub fn arcs(&self) -> &[Arc] {
        &self.arcs
    }
    /// The initial marking as a read-only, hash-backed view. Structure only:
    /// it reads token counts; it fires no transition.
    ///
    /// ```
    /// use wasm4pm_compat::petri::{PetriNet, Place, Transition, Arc, Marking};
    /// let net = PetriNet::new(
    ///     [Place::new("p0"), Place::new("p1")],
    ///     [Transition::new("t0", "fire")],
    ///     [Arc::place_to_transition("p0", "t0"), Arc::transition_to_place("t0", "p1")],
    ///     Marking::new([("p0".to_string(), 1)]),
    /// );
    /// let m = net.initial_marking();
    /// assert_eq!(m.tokens_on("p0"), 1);
    /// assert_eq!(m.tokens_on("p1"), 0); // unmarked place → 0
    /// ```
    pub fn initial_marking(&self) -> RuntimeMarking<'_> {
        RuntimeMarking { net: self }
    }
}

/// Read-only view of the initial marking backed by the PetriNet's PackedKeyTable.
pub struct RuntimeMarking<'a> {
    net: &'a PetriNet,
}

impl<'a> RuntimeMarking<'a> {
    /// Returns the token count on a named place, or 0 if not marked.
    pub fn tokens_on(&self, place_id: &str) -> usize {
        use crate::dense_kernel::fnv1a_64;
        let hash = fnv1a_64(place_id.as_bytes());
        *self.net.initial_marking.get(hash).unwrap_or(&0)
    }
}

// ── Marking::tokens_on ───────────────────────────────────────────────────────

impl Marking {
    /// Returns the token count on a named place, or 0 if absent.
    pub fn tokens_on(&self, place_id: &str) -> usize {
        self.tokens
            .iter()
            .find(|(id, _)| id == place_id)
            .map(|(_, n)| *n)
            .unwrap_or(0)
    }
}

// ── BipartiteArcConst ─────────────────────────────────────────────────────────

use crate::law::ArcDirectionConst;

pub struct BipartiteArcConst<const DIR: ArcDirectionConst, W> {
    place_id: String,
    transition_id: String,
    weight: W,
}

impl<const DIR: ArcDirectionConst, W: Copy> BipartiteArcConst<DIR, W> {
    pub fn new(place_id: &str, transition_id: &str, weight: W) -> Self {
        BipartiteArcConst {
            place_id: place_id.to_owned(),
            transition_id: transition_id.to_owned(),
            weight,
        }
    }
    pub fn place_id(&self) -> &str {
        &self.place_id
    }
    pub fn transition_id(&self) -> &str {
        &self.transition_id
    }
    pub fn weight(&self) -> W {
        self.weight
    }
    pub fn direction(&self) -> ArcDirectionConst {
        DIR
    }
}

// ── InitialFinalMarkingPair ───────────────────────────────────────────────────

pub struct InitialFinalMarkingPair {
    pub initial: Marking,
    pub final_marking: Marking,
}

impl InitialFinalMarkingPair {
    pub fn new(initial: Marking, final_marking: Marking) -> Self {
        InitialFinalMarkingPair {
            initial,
            final_marking,
        }
    }
    pub fn validate(&self) -> Result<(), PetriRefusal> {
        for (p_init, t_init) in self.initial.tokens() {
            if *t_init > 0 && self.final_marking.tokens_on(p_init) > 0 {
                return Err(PetriRefusal::UnsafeNet);
            }
        }
        Ok(())
    }
}

// ── Node-kind markers and typed arc structs ───────────────────────────────────

/// Sealed marker: this type represents a place node.
#[derive(Debug, Clone, Copy, Default, PartialEq, Eq, Hash)]
pub struct PlaceNodeMarker;

pub trait IsPlaceNode: Default + Clone + Copy {}
impl IsPlaceNode for PlaceNodeMarker {}

/// Sealed marker: this type represents a transition node.
#[derive(Debug, Clone, Copy, Default, PartialEq, Eq, Hash)]
pub struct TransitionNodeMarker;

pub trait IsTransitionNode: Default + Clone + Copy {}
impl IsTransitionNode for TransitionNodeMarker {}

pub trait IsValidArc {}

/// A pre-incidence (place → transition) arc carrying a typed weight.
///
/// The phantom types `P` and `T` name the place and transition namespaces;
/// the weight type `W` names the arc multiplicity type (usually `u32`).
pub struct PlaceToTransitionArc<P, T, W> {
    w: W,
    _p: PhantomData<(P, T)>,
}

impl<P, T, W: Copy> PlaceToTransitionArc<P, T, W> {
    pub fn new(weight: W) -> Self {
        PlaceToTransitionArc {
            w: weight,
            _p: PhantomData,
        }
    }
    pub fn weight(&self) -> W {
        self.w
    }
}

impl<P, T, W> IsValidArc for PlaceToTransitionArc<P, T, W> {}

/// A post-incidence (transition → place) arc carrying a typed weight.
pub struct TransitionToPlaceArc<T, P, W> {
    w: W,
    _p: PhantomData<(T, P)>,
}

impl<T, P, W: Copy> TransitionToPlaceArc<T, P, W> {
    pub fn new(weight: W) -> Self {
        TransitionToPlaceArc {
            w: weight,
            _p: PhantomData,
        }
    }
    pub fn weight(&self) -> W {
        self.w
    }
}

impl<T, P, W> IsValidArc for TransitionToPlaceArc<T, P, W> {}

pub struct SeparableWfNetMarker;

// The private `_seal` field is the non-forgeability mechanism, NOT an
// accidental near-`#[non_exhaustive]`. `#[non_exhaustive]` would not reproduce
// the "field `_seal` is private" compile error that the
// `wfnet_to_powl_nonseparable` type-law receipt asserts, and it permits
// struct-literal construction within this crate. Keep the private field.
#[allow(clippy::manual_non_exhaustive)]
pub struct SeparableWfNet<
    const S: SoundnessState,
    const FC: FreeChoiceMarker = { FreeChoiceMarker::General },
> {
    pub net: WfNetConst<S, FC>,
    /// Non-forgeable seal: this private field prevents constructing a
    /// separability claim via struct-literal syntax outside
    /// [`SeparableWfNet::declare_separable`] (Kourani, Park & van der Aalst
    /// 2026, Theorem 4.3). Without it, a non-separable WF-net could be forged
    /// into the POWL conversion path.
    _seal: (),
}

impl<const S: SoundnessState, const FC: FreeChoiceMarker> SeparableWfNet<S, FC> {
    pub fn declare_separable(net: WfNetConst<S, FC>) -> Self {
        SeparableWfNet { net, _seal: () }
    }

    pub fn into_powl(
        self,
        context_label: impl Into<String>,
    ) -> (crate::powl::Powl, crate::powl::WfNet2PowlWitness) {
        (
            crate::powl::Powl::new(),
            crate::powl::WfNet2PowlWitness::new_internal(context_label),
        )
    }
}

// ── WfNetConst — const-generic soundness typestate ────────────────────────────

mod wfnet_seal {
    pub(super) struct WfNetSeal;
}

/// Proof token that soundness has been verified (crate-internal only).
pub struct SoundnessProof(wfnet_seal::WfNetSeal);

#[allow(dead_code)] // reserved: issued by soundness-witnessing logic not yet in this crate
impl SoundnessProof {
    pub(crate) fn new() -> Self {
        SoundnessProof(wfnet_seal::WfNetSeal)
    }
}

/// The subclass marker for Free-Choice Petri Nets vs. General Workflow Nets.
///
/// Under Free-Choice nets (Desel 1995), soundness is decidable in polynomial time,
/// whereas general WF-nets require PSPACE-complete complexity.
#[derive(core::marker::ConstParamTy, PartialEq, Eq, Clone, Copy, Debug, Hash)]
pub enum FreeChoiceMarker {
    /// The net is structurally free-choice, enabling the polynomial-time soundness checking path.
    FreeChoice,
    /// The net is general, requiring the PSPACE-complete soundness checking path.
    General,
}

/// A workflow net whose soundness state and free-choice classification are embedded as const generic parameters.
///
/// `SoundnessState::Unknown` is freely constructible.
/// `SoundnessState::Claimed` is reachable via `.claim_sound()`.
/// `SoundnessState::Witnessed` requires a `SoundnessProof` token — non-forgeable.
///
/// The `FC` const-generic parameter allows distinguishing free-choice nets from general ones at the type level.
pub struct WfNetConst<
    const SOUNDNESS: SoundnessState,
    const FC: FreeChoiceMarker = { FreeChoiceMarker::General },
> {
    _seal: (),
}

impl WfNetConst<{ SoundnessState::Unknown }, { FreeChoiceMarker::General }> {
    pub fn new() -> Self {
        WfNetConst { _seal: () }
    }

    /// Advance: Unknown → Claimed (type-level re-tag, zero cost).
    #[must_use]
    pub fn claim_sound(
        self,
    ) -> WfNetConst<{ SoundnessState::Claimed }, { FreeChoiceMarker::General }> {
        WfNetConst { _seal: () }
    }
}

impl WfNetConst<{ SoundnessState::Unknown }, { FreeChoiceMarker::FreeChoice }> {
    pub fn new() -> Self {
        WfNetConst { _seal: () }
    }

    /// Advance: Unknown → Claimed (type-level re-tag, zero cost).
    #[must_use]
    pub fn claim_sound(
        self,
    ) -> WfNetConst<{ SoundnessState::Claimed }, { FreeChoiceMarker::FreeChoice }> {
        WfNetConst { _seal: () }
    }
}

impl WfNetConst<{ SoundnessState::Claimed }, { FreeChoiceMarker::General }> {
    /// Advance: Claimed → Witnessed, guarded by a `SoundnessProof` token.
    ///
    /// `SoundnessProof` is only constructible inside the petri module, making
    /// this transition non-forgeable from external code.
    #[must_use]
    pub fn witness_soundness(
        self,
        _proof: SoundnessProof,
    ) -> WfNetConst<{ SoundnessState::Witnessed }, { FreeChoiceMarker::General }> {
        WfNetConst { _seal: () }
    }
}

impl WfNetConst<{ SoundnessState::Claimed }, { FreeChoiceMarker::FreeChoice }> {
    /// Advance: Claimed → Witnessed, guarded by a `SoundnessProof` token.
    ///
    /// `SoundnessProof` is only constructible inside the petri module, making
    /// this transition non-forgeable from external code.
    #[must_use]
    pub fn witness_soundness(
        self,
        _proof: SoundnessProof,
    ) -> WfNetConst<{ SoundnessState::Witnessed }, { FreeChoiceMarker::FreeChoice }> {
        WfNetConst { _seal: () }
    }
}

impl<const S: SoundnessState, const FC: FreeChoiceMarker> WfNetConst<S, FC> {
    pub fn soundness_state(&self) -> SoundnessState {
        S
    }

    pub fn free_choice_state(&self) -> FreeChoiceMarker {
        FC
    }
}

impl WfNetConst<{ SoundnessState::Unknown }, { FreeChoiceMarker::General }> {
    /// Declare the net as Free-Choice after structural verification (re-tags at type level).
    #[must_use]
    pub fn into_free_choice(
        self,
    ) -> WfNetConst<{ SoundnessState::Unknown }, { FreeChoiceMarker::FreeChoice }> {
        WfNetConst { _seal: () }
    }
}

impl WfNetConst<{ SoundnessState::Claimed }, { FreeChoiceMarker::General }> {
    /// Declare the net as Free-Choice after structural verification (re-tags at type level).
    #[must_use]
    pub fn into_free_choice(
        self,
    ) -> WfNetConst<{ SoundnessState::Claimed }, { FreeChoiceMarker::FreeChoice }> {
        WfNetConst { _seal: () }
    }
}

impl WfNetConst<{ SoundnessState::Witnessed }, { FreeChoiceMarker::General }> {
    /// Declare the net as Free-Choice after structural verification (re-tags at type level).
    #[must_use]
    pub fn into_free_choice(
        self,
    ) -> WfNetConst<{ SoundnessState::Witnessed }, { FreeChoiceMarker::FreeChoice }> {
        WfNetConst { _seal: () }
    }
}

impl Default for WfNetConst<{ SoundnessState::Unknown }, { FreeChoiceMarker::General }> {
    fn default() -> Self {
        WfNetConst { _seal: () }
    }
}

impl Default for WfNetConst<{ SoundnessState::Unknown }, { FreeChoiceMarker::FreeChoice }> {
    fn default() -> Self {
        WfNetConst { _seal: () }
    }
}

// ── WfNetQuery ────────────────────────────────────────────────────────────────

/// Query interface for WF-net structural properties (reserved for future use).
pub trait WfNetQuery {
    /// The soundness state of this WF-net as a runtime value.
    fn soundness_state(&self) -> SoundnessState;
    /// The free-choice classification of this WF-net.
    fn free_choice_state(&self) -> FreeChoiceMarker;
}

impl<const S: SoundnessState, const FC: FreeChoiceMarker> WfNetQuery for WfNetConst<S, FC> {
    fn soundness_state(&self) -> SoundnessState {
        S
    }
    fn free_choice_state(&self) -> FreeChoiceMarker {
        FC
    }
}

// =============================================================================
// Stochastic Petri Nets
// =============================================================================

/// A stochastic weight representing a probability value `NUM / DEN` in `[0, 1]`.
///
/// Encodes the Leemans (2019) stochastic choice constraint: out-of-bounds weights
/// (e.g. numerator > denominator, or denominator == 0) are rejected at compile time.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct StochasticArcWeight<const NUM: u64, const DEN: u64>
where
    crate::law::Require<{ DEN > 0 }>: crate::law::IsTrue,
    crate::law::Require<{ NUM <= DEN }>: crate::law::IsTrue,
{
    _inner: crate::law::Between01<NUM, DEN>,
}

impl<const NUM: u64, const DEN: u64> StochasticArcWeight<NUM, DEN>
where
    crate::law::Require<{ DEN > 0 }>: crate::law::IsTrue,
    crate::law::Require<{ NUM <= DEN }>: crate::law::IsTrue,
{
    /// Construct a new compile-time stochastic weight.
    pub const fn new() -> Self {
        Self {
            _inner: crate::law::Between01::new(),
        }
    }

    /// Returns the numerator of the weight.
    pub const fn num(&self) -> u64 {
        NUM
    }

    /// Returns the denominator of the weight.
    pub const fn den(&self) -> u64 {
        DEN
    }
}

impl<const NUM: u64, const DEN: u64> Default for StochasticArcWeight<NUM, DEN>
where
    crate::law::Require<{ DEN > 0 }>: crate::law::IsTrue,
    crate::law::Require<{ NUM <= DEN }>: crate::law::IsTrue,
{
    fn default() -> Self {
        Self::new()
    }
}

/// Unit-struct marker representing an immediate transition.
/// Fired instantly when enabled; conflicts are resolved using relative probability weights.
#[derive(Debug, Clone, Copy, Default, PartialEq, Eq, Hash)]
pub struct ImmediateTransition;

/// Unit-struct marker representing a timed transition.
/// Fired stochastically after a delay determined by its firing rate.
#[derive(Debug, Clone, Copy, Default, PartialEq, Eq, Hash)]
pub struct TimedTransition;

mod private {
    pub trait Sealed {}
    impl Sealed for super::ImmediateTransition {}
    impl Sealed for super::TimedTransition {}
}

/// Trait implemented by valid stochastic transition kind markers.
///
/// This trait is sealed to prevent users from implementing it for arbitrary types.
pub trait IsStochasticTransitionKind: private::Sealed + Default + Copy {}

impl IsStochasticTransitionKind for ImmediateTransition {}
impl IsStochasticTransitionKind for TimedTransition {}

/// A transition in a stochastic Petri net, type-stamped with its structural kind.
///
/// This is a zero-cost wrapper around a transition identifier.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct StochasticTransition<KIND: IsStochasticTransitionKind> {
    pub id: String,
    _kind: PhantomData<KIND>,
}

impl<KIND: IsStochasticTransitionKind> StochasticTransition<KIND> {
    /// Construct a new typed stochastic transition.
    pub fn new(id: &str) -> Self {
        Self {
            id: id.to_string(),
            _kind: PhantomData,
        }
    }

    /// The transition's identifier.
    pub fn id(&self) -> &str {
        &self.id
    }
}

// =============================================================================
// Petri Net Unfoldings
// =============================================================================

/// A Condition in a branching process / occurrence net, corresponding to a place instance.
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub struct Condition {
    /// Unique identifier of this condition in the unfolding.
    pub id: String,
    /// Reference to the place ID in the original net.
    pub place_id: String,
}

impl Condition {
    pub fn new(id: impl Into<String>, place_id: impl Into<String>) -> Self {
        Condition {
            id: id.into(),
            place_id: place_id.into(),
        }
    }
}

/// An Event in a branching process / occurrence net, corresponding to a transition firing.
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub struct Event {
    /// Unique identifier of this event in the unfolding.
    pub id: String,
    /// Reference to the transition ID in the original net.
    pub transition_id: String,
}

impl Event {
    pub fn new(id: impl Into<String>, transition_id: impl Into<String>) -> Self {
        Event {
            id: id.into(),
            transition_id: transition_id.into(),
        }
    }
}

/// A Branching Process (occurrence net) of a Petri net.
///
/// Under Murata 1989, the branching process is acyclic, and every condition
/// has at most one incoming event. The type parameter `Net` binds the branching
/// process to the original Petri net type, enforcing type safety.
#[derive(Debug, Clone, PartialEq)]
pub struct BranchingProcess<Net = PetriNet> {
    pub conditions: Vec<Condition>,
    pub events: Vec<Event>,
    pub arcs: Vec<Arc>,
    _marker: std::marker::PhantomData<Net>,
}

impl<Net> BranchingProcess<Net> {
    pub fn new(conditions: Vec<Condition>, events: Vec<Event>, arcs: Vec<Arc>) -> Self {
        BranchingProcess {
            conditions,
            events,
            arcs,
            _marker: std::marker::PhantomData,
        }
    }

    pub fn conditions(&self) -> &[Condition] {
        &self.conditions
    }

    pub fn events(&self) -> &[Event] {
        &self.events
    }

    pub fn arcs(&self) -> &[Arc] {
        &self.arcs
    }
}

impl<Net> Default for BranchingProcess<Net> {
    fn default() -> Self {
        BranchingProcess {
            conditions: Vec::new(),
            events: Vec::new(),
            arcs: Vec::new(),
            _marker: std::marker::PhantomData,
        }
    }
}

/// An Unfolding Prefix of a branching process.
///
/// Under Murata 1989 and McMillan 1992, the unfolding prefix is a finite complete prefix
/// containing cut-off event designations that truncates infinite execution sequences.
#[derive(Debug, Clone, PartialEq)]
pub struct UnfoldingPrefix<Net = PetriNet> {
    pub process: BranchingProcess<Net>,
    pub cutoff_events: Vec<String>,
}

impl<Net> UnfoldingPrefix<Net> {
    pub fn new(process: BranchingProcess<Net>, cutoff_events: Vec<String>) -> Self {
        UnfoldingPrefix {
            process,
            cutoff_events,
        }
    }

    pub fn process(&self) -> &BranchingProcess<Net> {
        &self.process
    }

    pub fn cutoff_events(&self) -> &[String] {
        &self.cutoff_events
    }

    pub fn is_cutoff(&self, event_id: &str) -> bool {
        self.cutoff_events.iter().any(|id| id == event_id)
    }
}

impl<Net> Default for UnfoldingPrefix<Net> {
    fn default() -> Self {
        UnfoldingPrefix {
            process: BranchingProcess::default(),
            cutoff_events: Vec::new(),
        }
    }
}

/// `rem: T ⇸ P(T ∪ C \ {i, o})` — each task optionally names a cancellation
/// region. This struct carries the *shape* of that region: a named set of node
/// ids. Token-removal execution (the actual vacuuming) graduates to `wasm4pm`.
///
/// The `#[repr(transparent)]` newtype prevents a bare `Vec<String>` from being
/// accidentally passed where a `CancellationRegion` is required. It is zero-cost
/// to hold and clone.
///
/// Structure-only: carries ids, never fires.
#[repr(transparent)]
#[derive(Clone, Debug, PartialEq, Eq, Default)]
pub struct CancellationRegion {
    /// The ids of nodes (places, conditions, tasks) in this cancellation region,
    /// excluding the initial and final place of the net (i, o).
    pub members: Vec<String>,
}

impl CancellationRegion {
    /// Construct a cancellation region from an iterator of node ids.
    ///
    /// ```
    /// use wasm4pm_compat::petri::CancellationRegion;
    /// let region = CancellationRegion::new(["t1", "t2", "c3"]);
    /// assert_eq!(region.members(), &["t1", "t2", "c3"]);
    /// ```
    pub fn new<I, S>(members: I) -> Self
    where
        I: IntoIterator<Item = S>,
        S: Into<String>,
    {
        CancellationRegion {
            members: members.into_iter().map(Into::into).collect(),
        }
    }

    /// The node ids in this cancellation region.
    pub fn members(&self) -> &[String] {
        &self.members
    }
}

// ── YAWL multiple-instance bounds ───────────────────────────────────────────

#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)]
pub enum InstanceCreationKind {
    /// All child instances are created at the moment the task fires.
    Static,
    /// Child instances may be created incrementally during the task's lifetime.
    Dynamic,
}

/// A YAWL multiple-instance task specification: the four-tuple
/// `(min_instances, max_instances, threshold, creation_kind)`.
#[derive(Clone, Debug, PartialEq, Eq)]
pub struct MultipleInstanceSpec {
    /// Minimum number of instances that must complete.
    pub min: u32,
    /// Maximum number of instances (`None` = unbounded / ∞).
    pub max: Option<u32>,
    /// Threshold for collective completion (`None` = all instances).
    pub threshold: Option<u32>,
    /// Whether child instances are created statically or dynamically.
    pub creation: InstanceCreationKind,
}

impl MultipleInstanceSpec {
    /// Construct a multiple-instance spec.
    pub fn new(
        min: u32,
        max: Option<u32>,
        threshold: Option<u32>,
        creation: InstanceCreationKind,
    ) -> Self {
        MultipleInstanceSpec {
            min,
            max,
            threshold,
            creation,
        }
    }

    /// Structurally validate the instance bounds.
    #[must_use = "check the shape-check result"]
    pub fn validate(&self) -> Result<(), PetriRefusal> {
        if self.min == 0 {
            return Err(PetriRefusal::InvalidInstanceBounds);
        }
        if let Some(max) = self.max {
            if self.min > max {
                return Err(PetriRefusal::InvalidInstanceBounds);
            }
        }
        Ok(())
    }
}

// ── YAWL multiple-instance bounds — compile-time law surface ────────────────

/// A YAWL multiple-instance spec with bounds enforced **at compile time**.
///
/// `MultipleInstanceSpecConst<MIN, MAX>` encodes the YAWL Definition 1 `nofi`
/// invariant `1 ≤ MIN ≤ MAX` as const-generic where-bounds so that a violation
/// is a **compile error**, not a runtime refusal.
///
/// Law: YAWL Definition 1 nofi — `min: N`, `max: N^∞`, `1 ≤ min ≤ max`.
pub struct MultipleInstanceSpecConst<const MIN: u32, const MAX: u32>
where
    crate::law::Require<{ MIN >= 1 }>: crate::law::IsTrue,
    crate::law::Require<{ MIN <= MAX }>: crate::law::IsTrue,
{
    _private: (),
}

impl<const MIN: u32, const MAX: u32> MultipleInstanceSpecConst<MIN, MAX>
where
    crate::law::Require<{ MIN >= 1 }>: crate::law::IsTrue,
    crate::law::Require<{ MIN <= MAX }>: crate::law::IsTrue,
{
    /// Construct a `MultipleInstanceSpecConst<MIN, MAX>` — only possible when
    /// `MIN >= 1` and `MIN <= MAX`.
    pub const fn new() -> Self {
        MultipleInstanceSpecConst { _private: () }
    }

    /// The minimum instance count encoded in the type.
    pub const fn min(&self) -> u32 {
        MIN
    }

    /// The maximum instance count encoded in the type.
    pub const fn max(&self) -> u32 {
        MAX
    }
}

impl<const MIN: u32, const MAX: u32> Default for MultipleInstanceSpecConst<MIN, MAX>
where
    crate::law::Require<{ MIN >= 1 }>: crate::law::IsTrue,
    crate::law::Require<{ MIN <= MAX }>: crate::law::IsTrue,
{
    fn default() -> Self {
        Self::new()
    }
}

/// A standalone, named error type for the *missing final marking* law.
#[derive(Clone, Copy, Debug, Default, PartialEq, Eq, Hash)]
pub struct MissingFinalMarkingError;

impl core::fmt::Display for MissingFinalMarkingError {
    fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
        write!(f, "WF-net refused by law: MissingFinalMarking")
    }
}

impl From<MissingFinalMarkingError> for PetriRefusal {
    fn from(_: MissingFinalMarkingError) -> Self {
        PetriRefusal::MissingFinalMarking
    }
}

pub struct BoundedWfNet<const PLACES: usize, const TRANSITIONS: usize>
where
    [(); PLACES + TRANSITIONS]:,
{
    pub places: [String; PLACES],
    pub transitions: [String; TRANSITIONS],
}

impl<const PLACES: usize, const TRANSITIONS: usize> BoundedWfNet<PLACES, TRANSITIONS>
where
    [(); PLACES + TRANSITIONS]:,
    crate::law::Require<{ PLACES + TRANSITIONS <= 4096 }>: crate::law::IsTrue,
{
    pub fn new(places: [String; PLACES], transitions: [String; TRANSITIONS]) -> Self {
        Self {
            places,
            transitions,
        }
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::law::SoundnessState;

    #[test]
    fn soundness_proof_mints_and_advances_to_witnessed() {
        // SoundnessProof::new() is pub(crate) — this test is the only caller,
        // which is the point: it proves the sealed capability works end-to-end.
        let proof = SoundnessProof::new();
        let witnessed = WfNetConst::<{ SoundnessState::Unknown }>::new()
            .claim_sound()
            .witness_soundness(proof);
        assert_eq!(witnessed.soundness_state(), SoundnessState::Witnessed);
    }
}