View Source cure_fsm_verifier (cure v0.7.0)
Summary
Functions
Check for deadlocks using SMT A deadlock is a state with no outgoing transitions that is reachable
Check if the FSM has any deadlock states
Check liveness properties (system can always make progress)
Check if a target state is reachable from initial state
Check reachability using SMT (more precise than BFS for complex guards)
Check safety property (bad states are never reached)
Check if a state invariant holds in all reachable states Invariant is an expression that should be true in every state
Format verification results for display
Verify all properties and generate detailed report
Verify all properties of an FSM
Verify FSM properties using Z3 (bounded model checking)
Types
-type counterexample() :: #{state_name() => term()}.
-type property_result() :: {deadlock_free} | {has_deadlock, state_name()} | {reachable, state_name()} | {unreachable, state_name()} | {liveness_satisfied} | {liveness_violated, term()} | {safety_satisfied} | {safety_violated, counterexample()}.
-type state_name() :: atom().
-type verification_result() :: {ok, [property_result()]} | {error, term()}.
Functions
-spec check_deadlock_via_smt(FsmDef :: term()) -> {ok, deadlock_free} | {deadlock, state_name(), counterexample()} | {error, term()}.
Check for deadlocks using SMT A deadlock is a state with no outgoing transitions that is reachable
-spec check_deadlocks(FsmDef :: term()) -> [property_result()].
Check if the FSM has any deadlock states
-spec check_liveness(FsmDef :: term()) -> [property_result()].
Check liveness properties (system can always make progress)
-spec check_reachability(FsmDef :: term(), InitialState :: state_name(), TargetState :: state_name()) -> property_result().
Check if a target state is reachable from initial state
-spec check_reachability_via_smt(FsmDef :: term(), InitialState :: state_name(), TargetState :: state_name()) -> {reachable} | {unreachable} | {error, term()}.
Check reachability using SMT (more precise than BFS for complex guards)
-spec check_safety(FsmDef :: term(), BadStates :: [state_name()]) -> property_result().
Check safety property (bad states are never reached)
-spec check_state_invariant(FsmDef :: term(), Invariant :: term()) -> {ok, holds} | {violation, counterexample()} | {error, term()}.
Check if a state invariant holds in all reachable states Invariant is an expression that should be true in every state
-spec format_verification_result(verification_result()) -> binary().
Format verification results for display
-spec verify_all_properties(FsmDef :: term()) -> [property_result()].
Verify all properties and generate detailed report
-spec verify_fsm(FsmDef :: term()) -> verification_result().
Verify all properties of an FSM
Verify FSM properties using Z3 (bounded model checking)