Macro funfsm::invariant

macro_rules! invariant {
    ($c:ident, $p:expr) => { ... };
}

Pre/Postconditions are only checked in specific states. Invariants are checked in every state.