ironstate 0.1.3

//! Declared invariants — properties that must hold after every transition.

use crate::machine::{EventKind, StateMachine};
use core::marker::PhantomData;

/// The assertion an invariant runs: `(before, event, after) -> holds?`, where
/// `after` is `Some` if the transition committed and `None` if it was rejected.
type Check<S, E> = Box<dyn Fn(&S, &E, &Option<S>) -> bool>;

/// A named property checked after each transition during `test!`.
///
/// The check receives the state before the event, the event, and the state
/// after — `Some` if the transition committed, `None` if it was rejected.
pub struct Invariant<S, E> {
    description: &'static str,
    check: Check<S, E>,
}

impl<S, E> Invariant<S, E> {
    /// Begin defining a custom invariant with a human-readable description.
    pub fn custom(description: &'static str) -> PartialInvariant<S, E> {
        PartialInvariant {
            description,
            _marker: PhantomData,
        }
    }

    /// The invariant's description, shown in failure output.
    pub fn description(&self) -> &'static str {
        self.description
    }

    /// Whether the property holds for this `(before, event, after)` step.
    pub fn holds(&self, before: &S, event: &E, after: &Option<S>) -> bool {
        (self.check)(before, event, after)
    }
}

/// A half-built [`Invariant`] awaiting its assertion closure.
pub struct PartialInvariant<S, E> {
    description: &'static str,
    _marker: PhantomData<fn(&S, &E)>,
}

impl<S, E> PartialInvariant<S, E> {
    /// Supply the property: return `true` when it holds, `false` when violated.
    pub fn assert(self, check: impl Fn(&S, &E, &Option<S>) -> bool + 'static) -> Invariant<S, E> {
        Invariant {
            description: self.description,
            check: Box::new(check),
        }
    }
}

/// Implemented by a machine that declares domain invariants.
///
/// Optional: a machine without an `Invariants` impl is still verified for its
/// structural properties by `test!`. Implement this to add domain-specific
/// checks on top.
///
/// Each invariant is a description paired with a closure over the step
/// `(before, event, after)`, where `after` is `Some(state)` when the transition
/// committed and `None` when it was rejected. Return `true` while the property
/// holds; `test!` reports the description and the shrunk event sequence when it
/// doesn't.
///
/// # Examples
///
/// An invariant is most useful for a property the structure can't express on its
/// own — a condition on the *data* a state carries. Here `Charging` holds a
/// charge level, and the property is a bound on that number rather than on which
/// variant we're in:
///
/// ```ignore
/// // enum Battery { Empty, Charging { percent: u8 }, Full }
///
/// impl Invariants for Battery {
///     fn invariants() -> Vec<Invariant<Self, Self::Event>> {
///         vec![
///             Invariant::custom("charge never exceeds 100%").assert(
///                 |_before, _event, after| match after {
///                     Some(Battery::Charging { percent }) => *percent <= 100,
///                     _ => true,
///                 },
///             ),
///         ]
///     }
/// }
/// ```
pub trait Invariants: StateMachine
where
    Self::Event: EventKind,
{
    /// The invariants to verify after every transition.
    fn invariants() -> Vec<Invariant<Self, Self::Event>>;
}