pyfcstm.verify.algorithms

Raw verification algorithm entry points.

This package groups raw verification algorithms by the model feature they analyze. Public callers should usually import the algorithms from pyfcstm.verify, while this package documents the implementation layout used by maintainers and by the registry.

Algorithm map:

Module	Algorithms	Checks
pyfcstm.verify.algorithms.guard	dead_guard(), guard_tautology(), forced_guard_unsat_under_init()	Guard satisfiability, guard validity, and forced guard feasibility under declaration initial values.
pyfcstm.verify.algorithms.effect	effect_no_op_under_guard(), effect_contradicts_guard()	Transition effect observability and post-effect guard consistency.
pyfcstm.verify.algorithms.transition	transition_shadowed_by_predecessor(), composite_init_guards_incomplete()	Declaration-order trigger coverage and composite initial-transition input coverage.
pyfcstm.verify.algorithms.lifecycle	enter_postcondition_implies_during_precondition()	First-cycle enter / during condition determinacy.

Example:

>>> from pyfcstm.verify import dead_guard
>>> from pyfcstm.verify.algorithms import dead_guard as grouped_dead_guard
>>> # The grouped package re-exports the same callable as the public API.
>>> grouped_dead_guard is dead_guard
True

• pyfcstm.verify.algorithms.effect
  • __all__
    • __all__
  • effect_no_op_under_guard
    • effect_no_op_under_guard()
  • effect_contradicts_guard
    • effect_contradicts_guard()
• pyfcstm.verify.algorithms.guard
  • __all__
    • __all__
  • dead_guard
    • dead_guard()
  • guard_tautology
    • guard_tautology()
  • forced_guard_unsat_under_init
    • forced_guard_unsat_under_init()
• pyfcstm.verify.algorithms.lifecycle
  • __all__
    • __all__
  • enter_postcondition_implies_during_precondition
    • enter_postcondition_implies_during_precondition()
• pyfcstm.verify.algorithms.transition
  • __all__
    • __all__
  • transition_shadowed_by_predecessor
    • transition_shadowed_by_predecessor()
  • composite_init_guards_incomplete
    • composite_init_guards_incomplete()

__all__

pyfcstm.verify.algorithms.__all__ = ['composite_init_guards_incomplete', 'dead_guard', 'effect_contradicts_guard', 'effect_no_op_under_guard', 'enter_postcondition_implies_during_precondition', 'forced_guard_unsat_under_init', 'guard_tautology', 'transition_shadowed_by_predecessor']

Built-in mutable sequence.

If no argument is given, the constructor creates a new empty list. The argument must be an iterable if specified.