pyfcstm.verify.encoding

Verification encoding helpers for FCSTM runtime semantics.

The encoding package is an internal implementation layer used by pyfcstm.verify.algorithms. It translates FCSTM runtime semantics into Z3 expressions, operation environments, initial-entry contexts, and lifecycle condition points. Public callers should normally use the algorithm functions exported from pyfcstm.verify instead of importing these helpers.

Encoding map:

Module	Responsibility	Main consumers
pyfcstm.verify.encoding.expr	Expression translation with runtime-definedness constraints.	Guard, effect, and lifecycle algorithms.
pyfcstm.verify.encoding.guard	Transition guard translation and guard-domain extraction.	Guard and effect algorithms.
pyfcstm.verify.encoding.initial	Declaration initializer constraints and root initial path contexts.	Forced-guard, lifecycle, and composite-initial algorithms.
pyfcstm.verify.encoding.operation	Path-sensitive operation execution wrappers.	Effect and lifecycle algorithms.
pyfcstm.verify.encoding.trigger	Event and guard trigger encoding for transitions.	Transition-shadow and composite-initial algorithms.
pyfcstm.verify.encoding.lifecycle	First-cycle lifecycle operation and condition extraction.	Lifecycle algorithms.
pyfcstm.verify.encoding._core	Shared implementation details re-exported by the thin topic modules.	Maintainers only.

Example:

>>> from pyfcstm.verify.encoding import expr
>>> # Topic modules expose helpers, but public checks live in pyfcstm.verify.
>>> hasattr(expr, "_expr_z3_and_domains_or_result")
True

• pyfcstm.verify.encoding._core
  • is_sat
    • is_sat
• pyfcstm.verify.encoding.expr
  • __all__
    • __all__
• pyfcstm.verify.encoding.guard
  • __all__
    • __all__
• pyfcstm.verify.encoding.initial
  • __all__
    • __all__
• pyfcstm.verify.encoding.lifecycle
  • __all__
    • __all__
• pyfcstm.verify.encoding.operation
  • __all__
    • __all__
• pyfcstm.verify.encoding.trigger
  • __all__
    • __all__

__all__

pyfcstm.verify.encoding.__all__ = ['expr', 'guard', 'initial', 'lifecycle', 'operation', 'trigger']

Built-in mutable sequence.

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