pyfcstm.bmc.errors

Exception hierarchy for FCSTM bounded model checking queries.

The BMC package keeps query, encoding, and construction failures separate from parser, solver, and verification-registry concerns. These exceptions are plain Python errors with stable names so later parser, binder, engine, and adapter layers can raise structured failures without importing pyfcstm.verify.

Design contracts:

  • Error classes are intentionally thin and stable so parser, binder, engine, and adapter layers can share them without coupling to each other.

  • BmcQueryParseError is reserved for syntax-facing failures before a well-formed query object exists. InvalidBmcQuery remains the structural query-model validation error after AST objects are being built.

  • Query data-model validation uses these BMC-specific exceptions for structural failures, while expression category mix-ups still use normal Python type errors where that is more precise.

The module contains:

Example:

>>> from pyfcstm.bmc.errors import BmcError, InvalidBmcQuery
>>> try:
...     raise InvalidBmcQuery("bad bound")
... except BmcError as err:
...     str(err)
'bad bound'

__all__

pyfcstm.bmc.errors.__all__ = ['BmcError', 'BmcQueryParseError', 'InvalidBmcQuery', 'UnsupportedBmcQuery', 'InvalidBmcEncoding', 'InvalidBmcDomain', 'BmcBuildError']

Built-in mutable sequence.

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

BmcError

class pyfcstm.bmc.errors.BmcError[source]

Base class for FCSTM BMC failures.

Parameters:

message (str) – Human-readable error message.

Example:

>>> err = BmcError("query failed")
>>> str(err)
'query failed'

BmcQueryParseError

class pyfcstm.bmc.errors.BmcQueryParseError[source]

Raised when .fbmcq text or parse trees cannot build BMC AST nodes.

This exception covers lexical syntax diagnostics, parser syntax diagnostics, unfinished parsing, unknown text entry points, and parse-tree roots that the listener did not map to a BMC AST object. It deliberately does not cover model-aware validation or query structural validation, which use InvalidBmcQuery.

Parameters:

message (str) – Human-readable parse failure message.

Example:

>>> err = BmcQueryParseError("syntax error")
>>> isinstance(err, BmcError)
True

InvalidBmcQuery

class pyfcstm.bmc.errors.InvalidBmcQuery[source]

Raised when a BMC query model is structurally invalid.

Parameters:

message (str) – Human-readable validation message.

Example:

>>> err = InvalidBmcQuery("mode must be cold")
>>> isinstance(err, BmcError)
True

UnsupportedBmcQuery

class pyfcstm.bmc.errors.UnsupportedBmcQuery[source]

Raised when a valid BMC query requests unsupported behavior.

Parameters:

message (str) – Human-readable unsupported-feature message.

Example:

>>> err = UnsupportedBmcQuery("called() is not lowered yet")
>>> isinstance(err, BmcError)
True

InvalidBmcEncoding

class pyfcstm.bmc.errors.InvalidBmcEncoding[source]

Raised when symbolic BMC encoding data is internally inconsistent.

Parameters:

message (str) – Human-readable encoding message.

Example:

>>> err = InvalidBmcEncoding("missing frame")
>>> isinstance(err, BmcError)
True

InvalidBmcDomain

class pyfcstm.bmc.errors.InvalidBmcDomain[source]

Raised when BMC domain construction receives invalid data.

Parameters:

message (str) – Human-readable domain message.

Example:

>>> err = InvalidBmcDomain("unknown state")
>>> isinstance(err, BmcError)
True

BmcBuildError

class pyfcstm.bmc.errors.BmcBuildError[source]

Raised when BMC preparation cannot build a usable context.

Parameters:

message (str) – Human-readable build message.

Example:

>>> err = BmcBuildError("model binding failed")
>>> isinstance(err, BmcError)
True