pyfcstm.bmc.source

Macro-step source profiles for FCSTM bounded model checking.

A macro-step source describes the state boundary from which one symbolic cycle starts before the later macro expander enumerates concrete pyfcstm.bmc.macro.CycleCase objects. The source layer is deliberately solver-independent: it consumes the numbered pyfcstm.bmc.domain.BmcDomain snapshot and records only stable ids, display paths, source kind, and origin. Initial where predicates stay outside this module and are compiled into the initial-frame formula by later query/binder layers.

Design contracts:

• init sources model cold entry through the internal cold-start sentinel.

• entry sources model hot non-stoppable states whose uncovered branch may become semantic delta.

• stable_leaf sources point at non-sentinel stoppable leaves and use the same macro-step semantics for initial hot starts and recurrence frames.

• terminated sources use a fixed sentinel id and reserved case-label path so user states with similar names cannot impersonate it.

• Constructors validate against pyfcstm.bmc.domain.BmcDomain eagerly; direct dataclass construction remains possible for tests but still performs the same validation when a domain is supplied.

The module contains:

• MacroStepSource - Immutable source profile consumed by macro-step case expansion.

• init_source(), entry_source(), stable_leaf_source(), and terminated_source() - Validated source constructors.

• source_from_initial_spec() - Convert query initial specifications into source profiles without reading the initial predicate.

Example:

>>> from pyfcstm.bmc.domain import build_bmc_domain
>>> from pyfcstm.bmc.query import InitialSpec
>>> from pyfcstm.bmc.source import source_from_initial_spec
>>> from pyfcstm.model import load_state_machine_from_text
>>> domain = build_bmc_domain(load_state_machine_from_text('state Root;'), 1)
>>> source = source_from_initial_spec(domain, InitialSpec())
>>> source.kind
'init'

INIT_CASE_PATH

pyfcstm.bmc.source.INIT_CASE_PATH = '__init__'

str(object=’’) -> str str(bytes_or_buffer[, encoding[, errors]]) -> str

Create a new string object from the given object. If encoding or errors is specified, then the object must expose a data buffer that will be decoded using the given encoding and error handler. Otherwise, returns the result of object.__str__() (if defined) or repr(object). encoding defaults to sys.getdefaultencoding(). errors defaults to ‘strict’.

TERMINATE_CASE_PATH

pyfcstm.bmc.source.TERMINATE_CASE_PATH = '__terminate__'

str(object=’’) -> str str(bytes_or_buffer[, encoding[, errors]]) -> str

Create a new string object from the given object. If encoding or errors is specified, then the object must expose a data buffer that will be decoded using the given encoding and error handler. Otherwise, returns the result of object.__str__() (if defined) or repr(object). encoding defaults to sys.getdefaultencoding(). errors defaults to ‘strict’.

__all__

pyfcstm.bmc.source.__all__ = ['INIT_CASE_PATH', 'TERMINATE_CASE_PATH', 'MacroStepSource', 'init_source', 'entry_source', 'stable_leaf_source', 'terminated_source', 'source_from_initial_spec']

Built-in mutable sequence.

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

MacroStepSource

class pyfcstm.bmc.source.MacroStepSource(kind: str, origin: str, source_state_id: int, source_state_path: str, domain: BmcDomain | None = None)

Source profile for one symbolic macro-step.

Parameters:

• kind (str) – Source kind: "init", "entry", "stable_leaf", or "terminated".

• origin (str) – "initial" for the F_0 -> F_1 source, or "recurrence" for recurrence-frame sources.

• source_state_id (int) – Domain state id for the source. Sentinel sources use the fixed negative sentinel ids.

• source_state_path (str) – Source path used by macro-case labels. Sentinel sources use reserved paths such as "__terminate__".

• domain (BmcDomain, optional) – Optional domain used for eager validation, defaults to None.

Variables:

• kind (str) – Source kind.

• origin (str) – Source origin.

• source_state_id (int) – Domain state id.

• source_state_path (str) – Macro-case source path.

Example:

>>> from pyfcstm.bmc.domain import build_bmc_domain
>>> from pyfcstm.bmc.source import entry_source
>>> from pyfcstm.model import load_state_machine_from_text
>>> domain = build_bmc_domain(load_state_machine_from_text('state Root;'), 1)
>>> entry_source(domain).allows_semantic_delta
True

property allows_semantic_delta: bool

Return whether this source may emit semantic delta cases.

Returns:

True for cold-init and entry sources.

Return type:

bool

Example:

>>> MacroStepSource('entry', 'recurrence', 0, 'Root').allows_semantic_delta
True

to_canonical() → Dict[str, Any]

Return a JSON-stable source dictionary.

Returns:

Canonical source profile.

Return type:

Dict[str, object]

Example:

>>> MacroStepSource('entry', 'initial', 0, 'Root').to_canonical()['kind']
'entry'

to_semantic_canonical(include_origin: bool = True) → Dict[str, Any]

Return canonical source semantics for equivalence checks.

Parameters:

include_origin (bool, optional) – Whether to include the origin field, defaults to True.

Returns:

Canonical semantic source profile.

Return type:

Dict[str, object]

Example:

>>> source = MacroStepSource('stable_leaf', 'initial', 1, 'Root.A')
>>> source.to_semantic_canonical(include_origin=False)['kind']
'stable_leaf'

property uses_stable_fallback: bool

Return whether this source must use stable leaf fallback.

Returns:

True for "stable_leaf" sources.

Return type:

bool

Example:

>>> MacroStepSource('stable_leaf', 'recurrence', 1, 'Root.A').uses_stable_fallback
True

init_source

pyfcstm.bmc.source.init_source(domain: BmcDomain, origin: str = 'initial') → MacroStepSource

Construct the internal cold-start source.

Parameters:

• domain (BmcDomain) – Domain snapshot containing the fixed init sentinel.

• origin (str, optional) – Source origin, defaults to "initial".

Returns:

Validated init source.

Return type:

MacroStepSource

Raises:

InvalidBmcEncoding – If the domain sentinel metadata is missing.

Example:

>>> from pyfcstm.bmc.domain import build_bmc_domain, STATE_INIT_ID
>>> from pyfcstm.model import load_state_machine_from_text
>>> domain = build_bmc_domain(load_state_machine_from_text('state Root;'), 1)
>>> init_source(domain).source_state_id == STATE_INIT_ID
True

entry_source

pyfcstm.bmc.source.entry_source(domain: BmcDomain, state: int | str | StateDomainEntry | None = None, origin: str = 'initial') → MacroStepSource

Construct a hot-entry source for a root or non-stoppable model state.

state defaults to the model root for callers that need an already-entered root boundary, such as recurrence from a query-local non-stoppable source. Cold starts use init_source() instead. Explicit non-root stoppable leaves should be constructed through stable_leaf_source().

Parameters:

• domain (BmcDomain) – Domain snapshot that owns the source state.

• state (int or str or StateDomainEntry, optional) – Source state id, path, or entry, defaults to the root state.

• origin (str, optional) – Source origin, defaults to "initial".

Returns:

Validated entry source.

Return type:

MacroStepSource

Raises:

InvalidBmcEncoding – If the source is not the root or a non-stoppable model state in domain.

Example:

>>> from pyfcstm.bmc.domain import build_bmc_domain
>>> from pyfcstm.model import load_state_machine_from_text
>>> domain = build_bmc_domain(load_state_machine_from_text('state Root;'), 1)
>>> entry_source(domain).kind
'entry'

stable_leaf_source

pyfcstm.bmc.source.stable_leaf_source(domain: BmcDomain, state: int | str | StateDomainEntry, origin: str = 'recurrence') → MacroStepSource

Construct a stable leaf source.

Parameters:

• domain (BmcDomain) – Domain snapshot that owns the source state.

• state (int or str or StateDomainEntry) – Stoppable leaf state id, path, or entry.

• origin (str, optional) – Source origin, defaults to "recurrence".

Returns:

Validated stable leaf source.

Return type:

MacroStepSource

Raises:

InvalidBmcEncoding – If state is not a non-sentinel stoppable leaf in domain.

Example:

>>> from pyfcstm.bmc.domain import build_bmc_domain
>>> from pyfcstm.model import load_state_machine_from_text
>>> domain = build_bmc_domain(load_state_machine_from_text('state Root;'), 1)
>>> stable_leaf_source(domain, 'Root').uses_stable_fallback
True

terminated_source

pyfcstm.bmc.source.terminated_source(domain: BmcDomain, origin: str = 'recurrence') → MacroStepSource

Construct a terminated sentinel absorb source.

Parameters:

• domain (BmcDomain) – Domain snapshot containing the fixed terminate sentinel.

• origin (str, optional) – Source origin, defaults to "recurrence".

Returns:

Validated terminated source.

Return type:

MacroStepSource

Raises:

InvalidBmcEncoding – If the domain sentinel metadata is missing.

Example:

>>> from pyfcstm.bmc.domain import build_bmc_domain, STATE_TERMINATE_ID
>>> from pyfcstm.model import load_state_machine_from_text
>>> domain = build_bmc_domain(load_state_machine_from_text('state Root;'), 1)
>>> terminated_source(domain).source_state_id == STATE_TERMINATE_ID
True

source_from_initial_spec

pyfcstm.bmc.source.source_from_initial_spec(domain: BmcDomain, initial_spec: InitialSpec) → MacroStepSource

Build the initial macro-step source for an initial specification.

The optional InitialSpec.predicate is intentionally ignored here. It belongs to the initial-frame condition I_0 and must not affect source kind, fallback partition, or any future pyfcstm.bmc.macro.CycleCase condition.

Parameters:

• domain (BmcDomain) – Domain snapshot used to resolve initial state paths.

• initial_spec (InitialSpec) – Parser-independent initial specification.

Returns:

Initial macro-step source.

Return type:

MacroStepSource

Raises:

• InvalidBmcQuery – If initial_spec has an unsupported mode.

• InvalidBmcEncoding – If the referenced state cannot be used as a source profile.

Example:

>>> from pyfcstm.bmc.domain import build_bmc_domain
>>> from pyfcstm.bmc.query import InitialSpec
>>> from pyfcstm.model import load_state_machine_from_text
>>> domain = build_bmc_domain(load_state_machine_from_text('state Root;'), 1)
>>> source_from_initial_spec(
...     domain, InitialSpec(mode='state', state_path='Root')
... ).kind
'stable_leaf'