pyfcstm.bmc.macro

Macro-step case contracts for FCSTM bounded model checking.

The macro contract layer defines the solver-independent data objects exchanged between runtime-aligned macro-step expansion and later relation lowering. It records which flat control path a macro-step can take: source/target state ids, event/guard control atoms, priority exclusions expressed through accepted case labels, and the ordered model action blocks that would execute on that path. It deliberately does not lower operations into variable writeback expressions, split action-local if blocks, or construct Z3 implications.

Design contracts:

CycleCase.condition contains only control-path atoms. Valid atom prefixes are event:, guard:, and accepted:; action-local control flow and variable writeback constraints belong to later lowering.
GuardRequirement stores the raw model guard plus the action-block anchor at which that guard is checked. Later lowering interleaves action lowering and guard lowering instead of substituting guards in this layer.
ActionBlock preserves runtime action block boundaries and operation statement objects. A block may contain an pyfcstm.model.IfBlock, but that nested branch is not part of the case condition.
PriorityExclusion records declaration-order masks through accepted:<case_label> atoms. The accepted atom denotes the already lowered antecedent of a prior accepted path, not a raw event or guard trigger.
Partition verification is a build-time/test-time self-check. It first accepts structural accepted/fallback masks that are disjoint by construction, then falls back to a bounded truth-table checker for small non-canonical shapes. It never produces clauses for Core_N or Phi_N.

The module contains:

BoolTemplate - A small boolean recipe used by contract tests and partition self-checks.
EventUse, GuardRequirement, ActionBlock, and PriorityExclusion - Metadata for the flat macro-step path plan.
CycleCase - One macro-step relation case before solver lowering.
MacroStepFormal - Source-local buckets of success, delta, and build diagnostic conditions.
Helper constructors for absorb, fallback, semantic-delta, and partition checks.

Example:

>>> from pyfcstm.bmc.domain import build_bmc_domain
>>> from pyfcstm.bmc.macro import terminated_absorb_case
>>> from pyfcstm.model import load_state_machine_from_text
>>> domain = build_bmc_domain(load_state_machine_from_text('state Root;'), 1)
>>> terminated_absorb_case(domain).label
'__terminate__::absorb::__terminate__::0'

all

pyfcstm.bmc.macro.__all__ = ['BoolTemplate', 'EventUse', 'GuardRequirement', 'PriorityExclusion', 'ActionBlock', 'CycleCase', 'PartitionCheckResult', 'MacroStepFormal', 'case_path_condition', 'terminated_absorb_case', 'build_fallback_case', 'build_semantic_delta_case', 'verify_boolean_partition', 'verify_source_partition']

Built-in mutable sequence.

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

BoolTemplate

class pyfcstm.bmc.macro.BoolTemplate(kind: str, name: str | None = None, operands: Tuple[BoolTemplate, ...] = ())[source]

Solver-independent boolean condition recipe.

BoolTemplate intentionally supports only constants, atoms, not, and, and or. That is enough for macro contract checks while later solver lowering can map the recorded event, guard, and accepted atoms into Z3 formulas.

Parameters:

kind (str) – "true", "false", "atom", "not", "and", or "or".
name (str, optional) – Atom name for kind="atom", defaults to None.
operands (Tuple[BoolTemplate, ...], optional) – Child boolean templates for composite nodes, defaults to an empty tuple.

Example:

>>> gamma = BoolTemplate.atom('event:Root.Go')
>>> BoolTemplate.not_(gamma).evaluate({'event:Root.Go': False})
True

classmethod and_(*operands: BoolTemplate) → BoolTemplate[source]

Return logical conjunction of operands.

Parameters:: operands (BoolTemplate) – Operand conditions.
Returns:: Reduced conjunction, or constant true for an empty input.
Return type:: BoolTemplate

Example:

>>> BoolTemplate.and_().evaluate({})
True

classmethod atom(name: str) → BoolTemplate[source]

Return an atom condition.

Parameters:: name (str) – Atom name.
Returns:: Atom condition.
Return type:: BoolTemplate

Example:

>>> BoolTemplate.atom('guard:g0').variables
('guard:g0',)

evaluate(values: Mapping[str, bool]) → bool[source]

Evaluate this template on a boolean assignment.

Parameters:: values (Mapping[str, bool]) – Mapping from atom names to booleans.
Returns:: Evaluated boolean value.
Return type:: bool
Raises:: BmcBuildError – If an atom is missing or a value is not boolean.

Example:

>>> expr = BoolTemplate.and_(BoolTemplate.atom('a'), BoolTemplate.not_(BoolTemplate.atom('b')))
>>> expr.evaluate({'a': True, 'b': False})
True

classmethod false() → BoolTemplate[source]

Return the constant false condition.

Returns:: Constant false condition.
Return type:: BoolTemplate

Example:

>>> BoolTemplate.false().evaluate({})
False

classmethod not_(operand: BoolTemplate) → BoolTemplate[source]

Return logical negation of operand.

Parameters:: operand (BoolTemplate) – Operand condition.
Returns:: Negated condition with simple identities reduced.
Return type:: BoolTemplate

Example:

>>> BoolTemplate.not_(BoolTemplate.false()).evaluate({})
True

classmethod or_(*operands: BoolTemplate) → BoolTemplate[source]

Return logical disjunction of operands.

Parameters:: operands (BoolTemplate) – Operand conditions.
Returns:: Reduced disjunction, or constant false for an empty input.
Return type:: BoolTemplate

Example:

>>> BoolTemplate.or_().evaluate({})
False

to_canonical() → Dict[str, Any][source]

Return a JSON-stable condition recipe.

Returns:: Canonical condition dictionary.
Return type:: Dict[str, object]

Example:

>>> BoolTemplate.atom('guard:g0').to_canonical()['name']
'guard:g0'

classmethod true() → BoolTemplate[source]

Return the constant true condition.

Returns:: Constant true condition.
Return type:: BoolTemplate

Example:

>>> BoolTemplate.true().evaluate({})
True

property variables: Tuple[str, ...]

Return atom names referenced by this template.

Returns:: Sorted unique atom names.
Return type:: Tuple[str, …]

Example:

>>> BoolTemplate.or_(BoolTemplate.atom('b'), BoolTemplate.atom('a')).variables
('a', 'b')

EventUse

class pyfcstm.bmc.macro.EventUse(event_id: int, path: str, polarity: str, reason: str)[source]

Event input usage metadata for one case.

Parameters:

event_id (int) – Domain event id.
path (str) – Fully qualified event path.
polarity (str) – "positive" or "negative".
reason (str) – Usage reason such as "trigger" or "priority".

Example:

>>> EventUse(0, 'Root.Go', 'positive', 'trigger').polarity
'positive'

to_canonical() → Dict[str, Any][source]

Return a JSON-stable event-use dictionary.

Returns:: Canonical event-use metadata.
Return type:: Dict[str, object]

Example:

>>> EventUse(0, 'Root.Go', 'positive', 'trigger').to_canonical()['reason']
'trigger'

GuardRequirement

class pyfcstm.bmc.macro.GuardRequirement(requirement_id: str, owner_state_id: int, owner_state_path: str, transition_label: str, expr: Expr, polarity: str, reason: str, after_action_block_index: int)[source]

Raw transition guard requirement anchored to an action-block prefix.

Parameters:

requirement_id (str) – Stable per-formal guard requirement id.
owner_state_id (int) – Domain id of the state whose chooser owns the guard.
owner_state_path (str) – Dot-separated owner state path.
transition_label (str) – Human-readable transition label.
expr (pyfcstm.model.Expr) – Raw model expression evaluated by the runtime guard check.
polarity (str) – Guard polarity, normally "positive".
reason (str) – Guard-use reason such as "transition_guard".
after_action_block_index (int) – Number of action blocks that have executed before the guard is checked.

Example:

>>> from pyfcstm.model.expr import Boolean
>>> GuardRequirement('g0', 0, 'Root', 'Root -> A', Boolean(True), 'positive', 'transition_guard', 0).atom_name
'guard:g0'

property atom_name: str

Return the boolean atom name for this guard.

Returns:: Atom name in the guard:<id> namespace.
Return type:: str

Example:

>>> from pyfcstm.model.expr import Boolean
>>> GuardRequirement('g0', 0, 'Root', 't', Boolean(True), 'positive', 'transition_guard', 0).atom_name
'guard:g0'

to_canonical() → Dict[str, Any][source]

Return a JSON-stable guard requirement dictionary.

Returns:: Canonical guard requirement metadata.
Return type:: Dict[str, object]

Example:

>>> from pyfcstm.model.expr import Boolean
>>> GuardRequirement('g0', 0, 'Root', 't', Boolean(True), 'positive', 'transition_guard', 0).to_canonical()['atom']
'guard:g0'

PriorityExclusion

class pyfcstm.bmc.macro.PriorityExclusion(decision_id: str, reason: str, excluded_case_labels: Tuple[str, ...], excluded_condition: BoolTemplate, event_paths: Tuple[str, ...] = (), guard_requirement_ids: Tuple[str, ...] = ())[source]

Priority mask that excludes previously accepted control paths.

The event and guard-id fields are explanation metadata for the excluded accepted cases. They do not add conjuncts to the case condition. Lowering code must treat excluded_condition and CycleCase.condition as the truth sources and use the metadata only for witness/debug completeness.

Parameters:

decision_id (str) – Stable id for the chooser decision point.
reason (str) – Exclusion reason such as "transition_priority".
excluded_case_labels (Tuple[str, ...]) – Case labels excluded by this mask.
excluded_condition (BoolTemplate) – Boolean template over accepted: atoms.
event_paths (Tuple[str, ...], optional) – Event paths read by excluded cases, defaults to ().
guard_requirement_ids (Tuple[str, ...], optional) – Guard ids read by excluded cases, defaults to ().

Example:

>>> mask = PriorityExclusion('d0', 'transition_priority', ('c0',), BoolTemplate.atom('accepted:c0'))
>>> mask.excluded_case_labels
('c0',)

to_canonical() → Dict[str, Any][source]

Return a JSON-stable priority-exclusion dictionary.

Returns:: Canonical priority metadata.
Return type:: Dict[str, object]

Example:

>>> PriorityExclusion('d0', 'transition_priority', ('c0',), BoolTemplate.atom('accepted:c0')).to_canonical()['reason']
'transition_priority'

ActionBlock

class pyfcstm.bmc.macro.ActionBlock(block_kind: str, runtime_role: str, owner_state_id: int, owner_state_path: str, operations: Tuple[OperationStatement, ...], action_name: str | None = None, transition_label: str | None = None, is_abstract: bool = False, active_leaf_path: str | None = None, execution_state_path: str | None = None, named_ref: str | None = None)[source]

Runtime action block recorded for a macro-step path.

Parameters:

block_kind (str) – Public block kind: "state_action", "aspect_action", or "transition_effect".
runtime_role (str) – Runtime role explaining why the block executes, such as "state_enter", "leaf_during", "aspect_during_before", or "transition_effect".
owner_state_id (int) – Domain id of the state that owns the block.
owner_state_path (str) – Dot-separated owner state path.
operations (Tuple[pyfcstm.model.OperationStatement, ...]) – Ordered model statements in the block.
action_name (str, optional) – Optional model action function name, defaults to None.
transition_label (str, optional) – Optional transition label for effect blocks, defaults to None.
is_abstract (bool, optional) – Whether this block represents an abstract hook, defaults to False.
active_leaf_path (str, optional) – Runtime active leaf path when the block executes, defaults to None for legacy callers.
execution_state_path (str, optional) – Runtime public state path passed to abstract handler context, defaults to None and falls back to owner state.
named_ref (str, optional) – Named reference callsite path when this block was reached through ref, defaults to None.

Example:

>>> ActionBlock('state_action', 'leaf_during', 0, 'Root', ()).operations
()

to_canonical() → Dict[str, Any][source]

Return a JSON-stable action-block dictionary.

Returns:: Canonical action-block metadata.
Return type:: Dict[str, object]

Example:

>>> ActionBlock('state_action', 'leaf_during', 0, 'Root', ()).to_canonical()['block_kind']
'state_action'

CycleCase

class pyfcstm.bmc.macro.CycleCase(kind: str, source_state_id: int, source_state_path: str, target_state_id: int, target_state_path: str, label: str, condition: BoolTemplate, action_blocks: Tuple[ActionBlock, ...], used_events: Tuple[EventUse, ...] = (), guard_requirements: Tuple[GuardRequirement, ...] = (), priority_exclusions: Tuple[PriorityExclusion, ...] = (), failed_conditions: Tuple[BoolTemplate, ...] = (), consumed_events: Tuple[str, ...] = (), domain: BmcDomain | None = None)[source]

One macro-step relation case before solver lowering.

Parameters:

kind (str) – Case kind such as "transition", "fallback", "absorb", or "delta".
source_state_id (int) – Domain state id of the source boundary.
source_state_path (str) – Source path used by the case label.
target_state_id (int) – Domain state id of the target boundary.
target_state_path (str) – Target path used by the case label.
label (str) – Stable label in source_path::case_kind::target_path::ordinal form.
condition (BoolTemplate) – Bare control-path condition without a source-state guard.
action_blocks (Tuple[ActionBlock, ...]) – Runtime action blocks executed by this path.
used_events (Tuple[EventUse, ...], optional) – Event inputs read by this case, defaults to ().
guard_requirements (Tuple[GuardRequirement, ...], optional) – Guard requirements read by this case, defaults to ().
priority_exclusions (Tuple[PriorityExclusion, ...], optional) – Priority masks applied by this case, defaults to ().
failed_conditions (Tuple[BoolTemplate, ...], optional) – Diagnostic-only failed candidate conditions, defaults to ().
consumed_events (Tuple[str, ...], optional) – Canonical event paths consumed by executed evented transitions in micro-step order. Paths may repeat when one Boolean event presence enables several transitions, defaults to ().
domain (BmcDomain, optional) – Optional domain used for eager validation, defaults to None.

Example:

>>> case = CycleCase('transition', 0, 'Root', 0, 'Root', 'Root::transition::Root::0', BoolTemplate.true(), ())
>>> case.condition.evaluate({})
True

to_canonical() → Dict[str, Any][source]

Return a JSON-stable case dictionary.

Returns:: Canonical cycle-case dictionary.
Return type:: Dict[str, object]

Example:

>>> case = CycleCase('transition', 0, 'Root', 0, 'Root', 'Root::transition::Root::0', BoolTemplate.true(), ())
>>> case.to_canonical()['kind']
'transition'

PartitionCheckResult

class pyfcstm.bmc.macro.PartitionCheckResult(variables: Tuple[str, ...], assignment_count: int, bucket_count: int)[source]

Summary of a source-local boolean partition self-check.

Parameters:

variables (Tuple[str, ...]) – Boolean atom names enumerated by the truth-table check.
assignment_count (int) – Number of assignments checked.
bucket_count (int) – Number of partition buckets.

Example:

>>> PartitionCheckResult(('event:Root.Go',), 2, 2).to_canonical()['assignment_count']
2

to_canonical() → Dict[str, Any][source]

Return a JSON-stable partition-check summary.

Returns:: Canonical self-check summary.
Return type:: Dict[str, object]

Example:

>>> PartitionCheckResult((), 1, 1).to_canonical()['node']
'partition_check_result'

MacroStepFormal

class pyfcstm.bmc.macro.MacroStepFormal(source: MacroStepSource, success_cases: Tuple[CycleCase, ...], delta_cases: Tuple[CycleCase, ...] = (), build_diagnostic_conditions: Tuple[BoolTemplate, ...] = ())[source]

Source-local macro-step case buckets.

Parameters:

source (MacroStepSource) – Source profile that produced these buckets.
success_cases (Tuple[CycleCase, ...]) – Ordinary relation cases such as transitions, fallbacks, and absorbs.
delta_cases (Tuple[CycleCase, ...], optional) – Semantic delta relation cases, defaults to ().
build_diagnostic_conditions (Tuple[BoolTemplate, ...], optional) – Build/encoder diagnostic conditions, defaults to ().

Example:

>>> from pyfcstm.bmc.domain import build_bmc_domain
>>> from pyfcstm.bmc.macro import MacroStepFormal, terminated_absorb_case
>>> from pyfcstm.bmc.source import terminated_source
>>> from pyfcstm.model import load_state_machine_from_text
>>> domain = build_bmc_domain(load_state_machine_from_text('state Root;'), 1)
>>> formal = MacroStepFormal(terminated_source(domain), (terminated_absorb_case(domain),))
>>> formal.cases[0].kind
'absorb'

property cases: Tuple[CycleCase, ...]

Return ordinary and delta relation cases in stable order.

Returns:: success_cases + delta_cases.
Return type:: Tuple[CycleCase, …]

Example:

>>> source = MacroStepSource('entry', 'initial', 0, 'Root')
>>> case = CycleCase('delta', 0, 'Root', 0, 'Root', 'Root::delta::Root::0', BoolTemplate.true(), ())
>>> MacroStepFormal(source, (), (case,)).cases[0].kind
'delta'

to_canonical() → Dict[str, Any][source]

Return a JSON-stable formal dictionary.

Returns:: Canonical macro-step formal.
Return type:: Dict[str, object]

Example:

>>> source = MacroStepSource('entry', 'initial', 0, 'Root')
>>> case = CycleCase('delta', 0, 'Root', 0, 'Root', 'Root::delta::Root::0', BoolTemplate.true(), ())
>>> MacroStepFormal(source, (), (case,)).to_canonical()['source']['kind']
'entry'

verify_partition(max_assignments: int = 4096) → PartitionCheckResult[source]

Verify local case buckets with structural and truth-table self-checks.

Parameters:: max_assignments (int, optional) – Maximum assignments to enumerate, defaults to 4096.
Returns:: Partition self-check summary.
Return type:: PartitionCheckResult
Raises:: BmcBuildError – If the buckets overlap, leave a gap, or exceed the assignment budget for a non-structural shape.

Example:

>>> source = MacroStepSource('entry', 'initial', 0, 'Root')
>>> case = CycleCase('delta', 0, 'Root', 0, 'Root', 'Root::delta::Root::0', BoolTemplate.true(), ())
>>> MacroStepFormal(source, (), (case,)).verify_partition().bucket_count
1

case_path_condition

pyfcstm.bmc.macro.case_path_condition(case: CycleCase) → BoolTemplate[source]

Return the solver-independent control-path condition for case.

The helper intentionally returns CycleCase.condition without adding a source-state guard. Later relation builders are responsible for building the final antecedent and emitting Implies(A, R).

Parameters:: case (CycleCase) – Case whose control-path condition should be returned.
Returns:: Bare case condition.
Return type:: BoolTemplate
Raises:: InvalidBmcEncoding – If case is not a cycle case.

Example:

>>> case = CycleCase('transition', 0, 'Root', 0, 'Root', 'Root::transition::Root::0', BoolTemplate.true(), ())
>>> case_path_condition(case).evaluate({})
True

terminated_absorb_case

pyfcstm.bmc.macro.terminated_absorb_case(domain: BmcDomain) → CycleCase[source]

Build the terminate sentinel absorb case.

Parameters:: domain (BmcDomain) – Domain snapshot whose sentinel entries are used.
Returns:: Terminated self-loop absorb case.
Return type:: CycleCase

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)
>>> terminated_absorb_case(domain).kind
'absorb'

build_fallback_case

pyfcstm.bmc.macro.build_fallback_case(domain: BmcDomain, source: MacroStepSource, accepted_cases: Sequence[CycleCase], failed_conditions: Sequence[BoolTemplate] = (), ordinal: int = 0, guard_requirements: Sequence[GuardRequirement] = ()) → CycleCase[source]

Build a stable leaf fallback self-cycle.

The fallback condition negates accepted case labels rather than reusing raw trigger/guard predicates. Failed candidate conditions remain diagnostic metadata and do not shrink the fallback region.

Parameters:

domain (BmcDomain) – Domain snapshot whose event ids are used.
source (MacroStepSource) – Stable leaf source.
accepted_cases (Sequence[CycleCase]) – Accepted transition cases for the same stable leaf source.
failed_conditions (Sequence[BoolTemplate], optional) – Diagnostic-only failed conditions, defaults to ().
ordinal (int, optional) – Label ordinal, defaults to 0.
guard_requirements (Sequence[GuardRequirement], optional) – Guard metadata for atoms referenced by failed diagnostic conditions, defaults to ().

Returns:

Fallback case.

Return type:

CycleCase

Raises:

InvalidBmcEncoding – If source is not a stable leaf source.

Example:

>>> from pyfcstm.bmc.domain import build_bmc_domain
>>> from pyfcstm.bmc.source import stable_leaf_source
>>> from pyfcstm.model import load_state_machine_from_text
>>> domain = build_bmc_domain(load_state_machine_from_text('state Root;'), 1)
>>> source = stable_leaf_source(domain, 'Root')
>>> build_fallback_case(domain, source, ()).condition.evaluate({})
True

build_semantic_delta_case

pyfcstm.bmc.macro.build_semantic_delta_case(domain: BmcDomain, source: MacroStepSource, accepted_cases: Sequence[CycleCase], build_diagnostic_conditions: Sequence[BoolTemplate] = (), failed_conditions: Sequence[BoolTemplate] = (), ordinal: int = 0, guard_requirements: Sequence[GuardRequirement] = ()) → CycleCase[source]

Build a non-stoppable entry uncovered-region delta case.

The delta condition negates accepted case labels and build-diagnostic conditions. Failed candidate conditions remain diagnostic metadata only.

Parameters:

domain (BmcDomain) – Domain snapshot whose event ids are used.
source (MacroStepSource) – Initial entry source.
accepted_cases (Sequence[CycleCase]) – Accepted transition or initial success cases.
build_diagnostic_conditions (Sequence[BoolTemplate], optional) – Build diagnostic conditions excluded from semantic delta, defaults to ().
failed_conditions (Sequence[BoolTemplate], optional) – Diagnostic-only failed candidate conditions, defaults to ().
ordinal (int, optional) – Label ordinal, defaults to 0.
guard_requirements (Sequence[GuardRequirement], optional) – Guard metadata for atoms referenced by failed diagnostic conditions, defaults to ().

Returns:

Semantic delta case that self-loops the source.

Return type:

CycleCase

Raises:

InvalidBmcEncoding – If source does not allow semantic delta.

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)
>>> case = build_semantic_delta_case(domain, entry_source(domain), ())
>>> case.target_state_id == case.source_state_id
True

verify_boolean_partition

pyfcstm.bmc.macro.verify_boolean_partition(buckets: Sequence[BoolTemplate], variables: Sequence[str] | None = None, max_assignments: int = 4096) → PartitionCheckResult[source]

Verify that boolean buckets are complete and pairwise disjoint.

Parameters:

buckets (Sequence[BoolTemplate]) – Boolean bucket conditions.
variables (Sequence[str], optional) – Optional explicit universe variables, defaults to the union of bucket atoms.
max_assignments (int, optional) – Maximum truth-table assignments, defaults to 4096.

Returns:

Partition self-check summary.

Return type:

PartitionCheckResult

Raises:

BmcBuildError – If the partition is not exactly one or cannot be checked.

Example:

>>> a = BoolTemplate.atom('event:Root.Go')
>>> verify_boolean_partition((a, BoolTemplate.not_(a))).assignment_count
2

verify_source_partition

pyfcstm.bmc.macro.verify_source_partition(source: MacroStepSource, success_cases: Sequence[CycleCase], delta_cases: Sequence[CycleCase] = (), build_diagnostic_conditions: Sequence[BoolTemplate] = (), max_assignments: int = 4096) → PartitionCheckResult[source]

Verify one source’s local case partition.

Canonical accepted/fallback masks are verified structurally to avoid rejecting large declaration-priority partitions merely because their event or guard atom count exceeds the fallback truth-table budget. Non-canonical shapes are resolved through the source-local accepted-case registry and then checked by bounded truth-table enumeration.

Parameters:

source (MacroStepSource) – Macro-step source profile.
success_cases (Sequence[CycleCase]) – Ordinary success cases.
delta_cases (Sequence[CycleCase], optional) – Semantic delta cases, defaults to ().
build_diagnostic_conditions (Sequence[BoolTemplate], optional) – Build diagnostic conditions, defaults to ().
max_assignments (int, optional) – Maximum truth-table assignments, defaults to 4096.

Returns:

Partition self-check summary.

Return type:

PartitionCheckResult

Raises:

BmcBuildError – If the buckets are not complete and disjoint.
InvalidBmcEncoding – If the source/case buckets have an invalid shape, including unsupported delta buckets or malformed sentinel absorb partitions.

Example:

>>> source = MacroStepSource('entry', 'initial', 0, 'Root')
>>> case = CycleCase('delta', 0, 'Root', 0, 'Root', 'Root::delta::Root::0', BoolTemplate.true(), ())
>>> verify_source_partition(source, (), (case,)).bucket_count
1

pyfcstm.bmc.macro

__all__

BoolTemplate

EventUse

GuardRequirement

PriorityExclusion

ActionBlock

CycleCase

PartitionCheckResult

MacroStepFormal

case_path_condition

terminated_absorb_case

build_fallback_case

build_semantic_delta_case

verify_boolean_partition

verify_source_partition

all