pyfcstm.bmc.domain

Domain numbering model for FCSTM bounded model checking.

The domain layer assigns stable integer identifiers to the model objects that a bounded trace formula needs before macro-step expansion or solver lowering. It is intentionally model-aware but query-independent: every state, event, and persistent variable in the pyfcstm.model.StateMachine receives a stable identifier, and later BMC layers decide which identifiers are relevant to a particular query.

Design contracts:

Normal model states use non-negative ids, while the terminal and cold-init sentinel states use fixed negative ids.
Frame references cover F_0..F_N and step references cover E_0..E_{N-1} for a positive bound N.
F_0 may be constrained by cold, hot, or terminated initial conditions, so its allowed-state set is broader than recurrence frames.
Step/event input slots are independent; the domain layer never adds implicit at-most-one event constraints.
to_canonical() returns only JSON-stable plain Python objects so domain dumps can be used directly as golden fixtures and preparation summaries.

The module contains:

STATE_INIT_ID and STATE_TERMINATE_ID - Fixed sentinel state identifiers.
StateDomainEntry - Stable state id metadata.
EventDomainEntry - Stable event id metadata.
VarDomainEntry - Stable persistent variable id metadata.
FrameRef, StepRef, and EventInputRef - Bounded trace reference objects.
BmcDomain - Complete domain snapshot with lookup helpers.
build_bmc_domain() - Construct a domain snapshot from a state machine.

Example:

>>> from pyfcstm.model import load_state_machine_from_text
>>> model = load_state_machine_from_text('state Root;')
>>> domain = build_bmc_domain(model, bound=1)
>>> domain.state_path_to_id('Root') >= 0
True
>>> domain.state_by_id(STATE_TERMINATE_ID).name
'STATE_TERMINATE'

STATE_INIT_ID

pyfcstm.bmc.domain.STATE_INIT_ID = -3

int([x]) -> integer int(x, base=10) -> integer

Convert a number or string to an integer, or return 0 if no arguments are given. If x is a number, return x.__int__(). For floating point numbers, this truncates towards zero.

If x is not a number or if base is given, then x must be a string, bytes, or bytearray instance representing an integer literal in the given base. The literal can be preceded by ‘+’ or ‘-’ and be surrounded by whitespace. The base defaults to 10. Valid bases are 0 and 2-36. Base 0 means to interpret the base from the string as an integer literal. >>> int(‘0b100’, base=0) 4

STATE_TERMINATE_ID

pyfcstm.bmc.domain.STATE_TERMINATE_ID = -1

int([x]) -> integer int(x, base=10) -> integer

Convert a number or string to an integer, or return 0 if no arguments are given. If x is a number, return x.__int__(). For floating point numbers, this truncates towards zero.

If x is not a number or if base is given, then x must be a string, bytes, or bytearray instance representing an integer literal in the given base. The literal can be preceded by ‘+’ or ‘-’ and be surrounded by whitespace. The base defaults to 10. Valid bases are 0 and 2-36. Base 0 means to interpret the base from the string as an integer literal. >>> int(‘0b100’, base=0) 4

all

pyfcstm.bmc.domain.__all__ = ['STATE_INIT_ID', 'STATE_TERMINATE_ID', 'StateDomainEntry', 'EventDomainEntry', 'VarDomainEntry', 'FrameRef', 'StepRef', 'EventInputRef', 'BmcDomain', 'build_bmc_domain']

Built-in mutable sequence.

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

StateDomainEntry

class pyfcstm.bmc.domain.StateDomainEntry(id: int, path: str, name: str, kind: str, parent_path: str | None = None, is_root: bool = False, is_stoppable: bool = False, is_sentinel: bool = False, is_generated_combo_pseudo: bool = False)[source]

Stable identifier metadata for a model state or sentinel state.

Parameters:

id (int) – Stable state identifier. Normal model states use non-negative values; sentinel states use fixed negative values.
path (str) – Dot-separated full state path. Sentinel states use reserved $-prefixed paths such as "$STATE_TERMINATE".
name (str) – State name. Sentinel states use their reserved sentinel names.
kind (str) – "leaf", "composite", "pseudo", or "sentinel".
parent_path (str, optional) – Dot-separated parent state path, defaults to None.
is_root (bool, optional) – Whether this entry is the root model state, defaults to False.
is_stoppable (bool, optional) – Whether the state is a stoppable runtime leaf, defaults to False.
is_sentinel (bool, optional) – Whether this entry is a sentinel, defaults to False.
is_generated_combo_pseudo (bool, optional) – Whether the state is a trusted generated combo relay pseudo state, defaults to False.

Example:

>>> StateDomainEntry(0, 'Root', 'Root', 'leaf').to_canonical()['path']
'Root'

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

Return a JSON-stable state entry dictionary.

Returns:: Canonical state entry.
Return type:: Dict[str, object]

Example:

>>> StateDomainEntry(0, 'Root', 'Root', 'leaf').to_canonical()['node']
'state_domain_entry'

EventDomainEntry

class pyfcstm.bmc.domain.EventDomainEntry(id: int, path: str, name: str, owner_state_path: str, owner_state_id: int, owner_is_generated_combo_pseudo: bool = False)[source]

Stable identifier metadata for a model event.

Parameters:

id (int) – Stable event identifier.
path (str) – Dot-separated full event path.
name (str) – Event short name.
owner_state_path (str) – Dot-separated path of the declaring owner state.
owner_state_id (int) – State-domain id of the declaring owner state.
owner_is_generated_combo_pseudo (bool, optional) – Whether the owner is a generated combo pseudo state, defaults to False.

Example:

>>> EventDomainEntry(0, 'Root.Go', 'Go', 'Root', 0).owner_state_path
'Root'

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

Return a JSON-stable event entry dictionary.

Returns:: Canonical event entry.
Return type:: Dict[str, object]

Example:

>>> EventDomainEntry(0, 'Root.Go', 'Go', 'Root', 0).to_canonical()['node']
'event_domain_entry'

VarDomainEntry

class pyfcstm.bmc.domain.VarDomainEntry(id: int, name: str, declared_type: str)[source]

Stable identifier metadata for a persistent model variable.

Parameters:

id (int) – Stable variable identifier.
name (str) – Persistent variable name.
declared_type (str) – Declared FCSTM variable type.

Example:

>>> VarDomainEntry(0, 'counter', 'int').to_canonical()['declared_type']
'int'

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

Return a JSON-stable variable entry dictionary.

Returns:: Canonical variable entry.
Return type:: Dict[str, object]

Example:

>>> VarDomainEntry(0, 'x', 'int').to_canonical()['node']
'var_domain_entry'

FrameRef

class pyfcstm.bmc.domain.FrameRef(index: int, bound: int)[source]

Reference to a bounded trace frame F_i.

F_0 is the initial frame and can represent cold root, hot arbitrary state, or terminated initial conditions. Recurrence frames F_1..F_N are produced by macro-step transitions and are later constrained to stable leaf or sentinel states.

Parameters:

index (int) – Frame index.
bound (int) – Positive BMC bound.

Example:

>>> FrameRef(0, 2).role
'initial'
>>> FrameRef(2, 2).name
'F_2'

__str__() → str[source]

Return the canonical frame name.

Returns:: Frame name.
Return type:: str

Example:

>>> str(FrameRef(0, 1))
'F_0'

property name: str

Return the canonical frame name.

Returns:: Frame name such as "F_0".
Return type:: str

Example:

>>> FrameRef(1, 2).name
'F_1'

property role: str

Return the frame role.

Returns:: "initial" for F_0 and "transition" otherwise.
Return type:: str

Example:

>>> FrameRef(0, 1).role
'initial'

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

Return a JSON-stable frame dictionary.

Returns:: Canonical frame reference.
Return type:: Dict[str, object]

Example:

>>> FrameRef(1, 2).to_canonical()['name']
'F_1'

StepRef

class pyfcstm.bmc.domain.StepRef(index: int, bound: int)[source]

Reference to a bounded trace step input E_i.

Parameters:

index (int) – Step index.
bound (int) – Positive BMC bound.

Example:

>>> StepRef(0, 1).name
'E_0'

__str__() → str[source]

Return the canonical step name.

Returns:: Step name.
Return type:: str

Example:

>>> str(StepRef(0, 1))
'E_0'

property name: str

Return the canonical step name.

Returns:: Step name such as "E_0".
Return type:: str

Example:

>>> StepRef(0, 2).name
'E_0'

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

Return a JSON-stable step dictionary.

Returns:: Canonical step reference.
Return type:: Dict[str, object]

Example:

>>> StepRef(0, 2).to_canonical()['node']
'step_ref'

EventInputRef

class pyfcstm.bmc.domain.EventInputRef(step_index: int, event_id: int, event_path: str)[source]

Reference to one event input slot at one step.

Parameters:

step_index (int) – Step index.
event_id (int) – Event-domain id.
event_path (str) – Dot-separated event path used in the display name.

Example:

>>> EventInputRef(0, 2, 'Root.Go').name
'E_0[Root.Go]'

property name: str

Return the canonical event input display name.

Returns:: Input slot name such as "E_0[Root.Go]".
Return type:: str

Example:

>>> EventInputRef(0, 1, 'Root.Go').name
'E_0[Root.Go]'

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

Return a JSON-stable event input dictionary.

Returns:: Canonical event input reference.
Return type:: Dict[str, object]

Example:

>>> EventInputRef(0, 1, 'Root.Go').to_canonical()['event_id']
1

BmcDomain

class pyfcstm.bmc.domain.BmcDomain(bound: int, states: Tuple[StateDomainEntry, ...], events: Tuple[EventDomainEntry, ...], variables: Tuple[VarDomainEntry, ...], frames: Tuple[FrameRef, ...], steps: Tuple[StepRef, ...], event_inputs: Tuple[EventInputRef, ...], initial_state_ids: Tuple[int, ...], stable_state_ids: Tuple[int, ...], model: StateMachine | None = None)[source]

Complete bounded model checking domain snapshot.

Parameters:

bound (int) – Positive BMC bound.
states (Tuple[StateDomainEntry, ...]) – State-domain entries, including sentinel entries.
events (Tuple[EventDomainEntry, ...]) – Event-domain entries.
variables (Tuple[VarDomainEntry, ...]) – Persistent variable-domain entries.
frames (Tuple[FrameRef, ...]) – Frame references F_0..F_N.
steps (Tuple[StepRef, ...]) – Step references E_0..E_{N-1}.
event_inputs (Tuple[EventInputRef, ...]) – Step/event input slots. Domain snapshots require the full step-by-event Cartesian product; query and relation layers perform later pruning or cardinality constraints.
initial_state_ids (Tuple[int, ...]) – State ids allowed at F_0.
stable_state_ids (Tuple[int, ...]) – State ids allowed at recurrence frame boundaries.
model (StateMachine, optional) – Optional source model back-reference used by model-aware BMC layers, defaults to None. It is intentionally excluded from equality and canonical snapshots.

Example:

>>> from pyfcstm.model import load_state_machine_from_text
>>> domain = build_bmc_domain(load_state_machine_from_text('state Root;'), 1)
>>> domain.to_canonical()['node']
'bmc_domain'

event_by_id(event_id: int) → EventDomainEntry[source]

Return the event entry with event_id.

Parameters:: event_id (int) – Event id to look up.
Returns:: Matching event-domain entry.
Return type:: EventDomainEntry
Raises:: InvalidBmcDomain – If no event has event_id.

Example:

>>> from pyfcstm.model import load_state_machine_from_text
>>> model = load_state_machine_from_text('state Root { event Go; state A; [*] -> A; }')
>>> build_bmc_domain(model, 1).event_by_id(0).path
'Root.Go'

event_by_path(path: str) → EventDomainEntry[source]

Return the event entry with path.

Parameters:: path (str) – Dot-separated event path.
Returns:: Matching event-domain entry.
Return type:: EventDomainEntry
Raises:: InvalidBmcDomain – If path is unknown.

Example:

>>> from pyfcstm.model import load_state_machine_from_text
>>> model = load_state_machine_from_text('state Root { event Go; state A; [*] -> A; }')
>>> build_bmc_domain(model, 1).event_by_path('Root.Go').name
'Go'

event_id_to_path(event_id: int) → str[source]

Return the path for an event id.

Parameters:: event_id (int) – Event id.
Returns:: Dot-separated event path.
Return type:: str
Raises:: InvalidBmcDomain – If event_id is unknown.

Example:

>>> from pyfcstm.model import load_state_machine_from_text
>>> model = load_state_machine_from_text('state Root { event Go; state A; [*] -> A; }')
>>> build_bmc_domain(model, 1).event_id_to_path(0)
'Root.Go'

event_input(step: StepRef, event_id: int) → EventInputRef[source]

Return the input slot for step and event_id.

Parameters:

step (StepRef) – Step reference.
event_id (int) – Event-domain id.

Returns:

Matching event input reference.

Return type:

EventInputRef

Raises:

InvalidBmcDomain – If the step or event id is outside this domain.

Example:

>>> from pyfcstm.model import load_state_machine_from_text
>>> model = load_state_machine_from_text('state Root { event Go; state A; [*] -> A; }')
>>> domain = build_bmc_domain(model, 1)
>>> domain.event_input(StepRef(0, 1), domain.event_path_to_id('Root.Go')).name
'E_0[Root.Go]'

event_path_to_id(path: str) → int[source]

Return the id for an event path.

Parameters:: path (str) – Dot-separated event path.
Returns:: Event id.
Return type:: int
Raises:: InvalidBmcDomain – If path is unknown.

Example:

>>> from pyfcstm.model import load_state_machine_from_text
>>> model = load_state_machine_from_text('state Root { event Go; state A; [*] -> A; }')
>>> build_bmc_domain(model, 1).event_path_to_id('Root.Go')
0

property frame0_state_ids: Tuple[int, ...]

Return state ids allowed in the initial frame.

Returns:: Initial-frame state ids.
Return type:: Tuple[int, …]

Example:

>>> from pyfcstm.model import load_state_machine_from_text
>>> domain = build_bmc_domain(load_state_machine_from_text('state Root;'), 1)
>>> domain.frame0_state_ids == domain.initial_state_ids
True

property recurrence_state_ids: Tuple[int, ...]

Return state ids allowed at recurrence frame boundaries.

Returns:: Recurrence-frame state ids.
Return type:: Tuple[int, …]

Example:

>>> from pyfcstm.model import load_state_machine_from_text
>>> domain = build_bmc_domain(load_state_machine_from_text('state Root;'), 1)
>>> domain.recurrence_state_ids == domain.stable_state_ids
True

state_by_id(state_id: int) → StateDomainEntry[source]

Return the state entry with state_id.

Parameters:: state_id (int) – State id to look up.
Returns:: Matching state-domain entry.
Return type:: StateDomainEntry
Raises:: InvalidBmcDomain – If no state has state_id.

Example:

>>> from pyfcstm.model import load_state_machine_from_text
>>> domain = build_bmc_domain(load_state_machine_from_text('state Root;'), 1)
>>> domain.state_by_id(domain.state_path_to_id('Root')).path
'Root'

state_by_path(path: str) → StateDomainEntry[source]

Return the state entry with path.

Parameters:: path (str) – Dot-separated state path. Sentinel states use reserved $-prefixed paths such as "$STATE_TERMINATE".
Returns:: Matching state-domain entry.
Return type:: StateDomainEntry
Raises:: InvalidBmcDomain – If no state has path.

Example:

>>> from pyfcstm.model import load_state_machine_from_text
>>> domain = build_bmc_domain(load_state_machine_from_text('state Root;'), 1)
>>> domain.state_by_path('$STATE_TERMINATE').name
'STATE_TERMINATE'

state_id_to_path(state_id: int) → str[source]

Return the path for a state id.

Parameters:: state_id (int) – State id.
Returns:: Dot-separated state path, or a reserved $-prefixed sentinel path.
Return type:: str
Raises:: InvalidBmcDomain – If state_id is unknown.

Example:

>>> from pyfcstm.model import load_state_machine_from_text
>>> domain = build_bmc_domain(load_state_machine_from_text('state Root;'), 1)
>>> domain.state_id_to_path(STATE_TERMINATE_ID)
'$STATE_TERMINATE'

state_path_to_id(path: str) → int[source]

Return the id for a state path.

Parameters:: path (str) – Dot-separated state path. Sentinel states use reserved $-prefixed paths such as "$STATE_TERMINATE".
Returns:: State id.
Return type:: int
Raises:: InvalidBmcDomain – If path is unknown.

Example:

>>> from pyfcstm.model import load_state_machine_from_text
>>> domain = build_bmc_domain(load_state_machine_from_text('state Root;'), 1)
>>> domain.state_path_to_id('$STATE_INIT')
-3

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

Return a JSON-stable domain dictionary.

Returns:: Canonical domain snapshot.
Return type:: Dict[str, object]

Example:

>>> from pyfcstm.model import load_state_machine_from_text
>>> domain = build_bmc_domain(load_state_machine_from_text('state Root;'), 1)
>>> domain.to_canonical()['sentinels']['terminate']
-1

variable_by_id(variable_id: int) → VarDomainEntry[source]

Return the variable entry with variable_id.

Parameters:: variable_id (int) – Variable id.
Returns:: Matching variable-domain entry.
Return type:: VarDomainEntry
Raises:: InvalidBmcDomain – If variable_id is unknown.

Example:

>>> from pyfcstm.model import load_state_machine_from_text
>>> model = load_state_machine_from_text('def int x = 0; state Root;')
>>> build_bmc_domain(model, 1).variable_by_id(0).name
'x'

variable_by_name(name: str) → VarDomainEntry[source]

Return the variable entry with name.

Parameters:: name (str) – Persistent variable name.
Returns:: Matching variable-domain entry.
Return type:: VarDomainEntry
Raises:: InvalidBmcDomain – If name is unknown.

Example:

>>> from pyfcstm.model import load_state_machine_from_text
>>> model = load_state_machine_from_text('def int x = 0; state Root;')
>>> build_bmc_domain(model, 1).variable_by_name('x').declared_type
'int'

variable_id_to_name(variable_id: int) → str[source]

Return the name for a variable id.

Parameters:: variable_id (int) – Variable id.
Returns:: Variable name.
Return type:: str
Raises:: InvalidBmcDomain – If variable_id is unknown.

Example:

>>> from pyfcstm.model import load_state_machine_from_text
>>> model = load_state_machine_from_text('def int x = 0; state Root;')
>>> build_bmc_domain(model, 1).variable_id_to_name(0)
'x'

variable_name_to_id(name: str) → int[source]

Return the id for a persistent variable name.

Parameters:: name (str) – Persistent variable name.
Returns:: Variable id.
Return type:: int
Raises:: InvalidBmcDomain – If name is unknown.

Example:

>>> from pyfcstm.model import load_state_machine_from_text
>>> model = load_state_machine_from_text('def int x = 0; state Root;')
>>> build_bmc_domain(model, 1).variable_name_to_id('x')
0

build_bmc_domain

pyfcstm.bmc.domain.build_bmc_domain(model: StateMachine, bound: int) → BmcDomain[source]

Build a BMC domain snapshot from a state machine and bound.

The domain contains all model states, all resolved model events, all persistent variable declarations, fixed sentinel states, frame references, step references, and independent step/event input slots. It does not bind a query, build macro-step cases, or allocate solver symbols.

Parameters:

model (StateMachine) – State machine to number.
bound (int) – Positive BMC bound.

Returns:

Complete BMC domain snapshot.

Return type:

BmcDomain

Raises:

InvalidBmcDomain – If model is not a state machine or bound is not positive.

Example:

>>> from pyfcstm.model import load_state_machine_from_text
>>> model = load_state_machine_from_text('state Root { event Go; state A; [*] -> A; }')
>>> domain = build_bmc_domain(model, 1)
>>> domain.event_path_to_id('Root.Go')
0

pyfcstm.bmc.domain

STATE_INIT_ID

STATE_TERMINATE_ID

__all__

StateDomainEntry

EventDomainEntry

VarDomainEntry

FrameRef

StepRef

EventInputRef

BmcDomain

build_bmc_domain

all