pyfcstm.verify.result

Raw verification result helpers.

This module defines the small result objects returned by raw verification algorithms. The payload deliberately stays below the diagnostics layer: algorithms return kind strings and plain dictionaries, while later integration can decide how those payloads become user-facing diagnostics.

Example:

>>> from pyfcstm.verify.result import make_diag, skip_result
>>> make_diag("W_DEAD_GUARD", "dead_guard", state="Root.A")["data"]
{'state': 'Root.A'}
>>> skip_result("unknown", "solver returned unknown").kind
'unknown'

ResultKind

pyfcstm.verify.result.ResultKind

alias of Literal[‘sat’, ‘unsat’, ‘unknown’, ‘timeout’, ‘undecidable_skip’]

__all__

pyfcstm.verify.result.__all__ = ['AlgorithmResult', 'ResultKind', 'make_diag', 'skip_result']

Built-in mutable sequence.

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

AlgorithmResult

class pyfcstm.verify.result.AlgorithmResult(kind: Literal['sat', 'unsat', 'unknown', 'timeout', 'undecidable_skip'], diagnostics: Tuple[dict, ...] = (), reason: str | None = None)[source]

Result returned by one raw verification algorithm.

Parameters:

  • kind (ResultKind) – Normalized solver or skip outcome.

  • diagnostics (Tuple[dict, ...]) – Raw diagnostic dictionaries produced by the algorithm. These stay diagnostics-layer independent.

  • reason (Optional[str], optional) – Optional reason for unknown / timeout / skip results, defaults to None.

Example:

>>> result = AlgorithmResult("sat", diagnostics=({"code": "W", "data": {}},))
>>> result.kind
'sat'
>>> len(result.diagnostics)
1

make_diag

pyfcstm.verify.result.make_diag(code: str, algorithm_name: str, **data) → dict[source]

Create a raw verify diagnostic payload.

Parameters:

  • code (str) – Future diagnostics code.

  • algorithm_name (str) – Algorithm that emitted the payload.

  • data (object) – Algorithm-specific payload fields.

Returns:

Raw diagnostic dictionary.

Return type:

dict

Example:

>>> make_diag("W_DEAD_GUARD", "dead_guard", state="Root.A")
{'code': 'W_DEAD_GUARD', 'algorithm_name': 'dead_guard', 'data': {'state': 'Root.A'}}

skip_result

pyfcstm.verify.result.skip_result(kind: Literal['sat', 'unsat', 'unknown', 'timeout', 'undecidable_skip'], reason: str | None) → AlgorithmResult[source]

Create a skip or indeterminate result.

Parameters:

  • kind (ResultKind) – Result kind.

  • reason (Optional[str]) – Optional reason text.

Returns:

Algorithm result.

Return type:

AlgorithmResult

Example:

>>> skip_result("undecidable_skip", "unsupported expression")
AlgorithmResult(kind='undecidable_skip', diagnostics=(), reason='unsupported expression')