agenticraft_foundation.mpst.checker

Well-formedness checking for session types — validates protocol structure and properties.

Session type checker with runtime verification.

This module provides type checking for MPST sessions, integrating with the InvariantRegistry for runtime verification of session properties.

Key Features: - Well-formedness checking for global types - Session conformance checking against local types - Runtime monitoring with StateTransitionMonitor - Integration with InvariantRegistry for property verification

References: - Honda, Yoshida, Carbone (2008) - Multiparty Session Types

WellFormednessResult dataclass

Result of well-formedness checking.

ATTRIBUTE	DESCRIPTION
is_well_formed	Whether the type is well-formed TYPE: bool
errors	List of errors found TYPE: list[str]
warnings	List of warnings TYPE: list[str]
participants	Set of participants in the type TYPE: set[ParticipantId]

WellFormednessChecker

Checks well-formedness of global session types.

A global type G is well-formed if: 1. All participants are reachable from the initial state 2. No orphan messages (every send has a matching receive) 3. Choice consistency (sender/receiver are distinct) 4. Recursion is guarded (no unguarded recursive calls) 5. Projection is defined for all participants

check(global_type)

Check if a global type is well-formed.

PARAMETER	DESCRIPTION
global_type	Global session type to check TYPE: SessionType

RETURNS	DESCRIPTION
WellFormednessResult	WellFormednessResult with details

SessionMonitor dataclass

Monitors a session's conformance to its local type.

Tracks message exchanges and verifies they conform to the expected local type for each participant.

Integrates with StateTransitionMonitor for transition tracking.

on_send(receiver, payload)

Handle a send action.

PARAMETER	DESCRIPTION
receiver	Target participant TYPE: ParticipantId
payload	Message payload TYPE: MessagePayload

RETURNS	DESCRIPTION
bool	True if send conforms to local type

RAISES	DESCRIPTION
TypeCheckError	If strict and send doesn't conform

on_receive(sender, payload)

Handle a receive action.

PARAMETER	DESCRIPTION
sender	Source participant TYPE: ParticipantId
payload	Message payload TYPE: MessagePayload

RETURNS	DESCRIPTION
bool	True if receive conforms to local type

is_complete()

Check if session has completed successfully.

can_send()

Check if next action is a send.

can_receive()

Check if next action is a receive.

get_violations()

Get all recorded violations.

get_state()

Get current monitor state.

MPSTInvariantRegistry

Registry of MPST-specific invariants.

Provides standard session type invariants for runtime verification.

__init__(registry=None)

Initialize with optional parent registry.

PARAMETER	DESCRIPTION
registry	Parent InvariantRegistry to use TYPE: InvariantRegistry | None DEFAULT: None

check_all(monitors)

Check all MPST invariants.

PARAMETER	DESCRIPTION
monitors	Dictionary of session monitors TYPE: dict[ParticipantId, SessionMonitor]

RETURNS	DESCRIPTION
list[str]	List of violated invariant names

SessionTypeChecker

Complete session type checker with runtime monitoring.

Provides: - Well-formedness checking of global types - Local type projection - Runtime session monitoring - Invariant verification

__init__(registry=None)

Initialize type checker.

PARAMETER	DESCRIPTION
registry	Optional InvariantRegistry for invariants TYPE: InvariantRegistry | None DEFAULT: None

check_well_formed(global_type)

Check if a global type is well-formed.

PARAMETER	DESCRIPTION
global_type	Global session type TYPE: SessionType

RETURNS	DESCRIPTION
WellFormednessResult	WellFormednessResult with details

project(global_type, participant)

Project global type to local type.

PARAMETER	DESCRIPTION
global_type	Global session type TYPE: SessionType
participant	Participant to project for TYPE: ParticipantId

RETURNS	DESCRIPTION
SessionType	Local session type

create_session(session_id, global_type, strict=True)

Create monitors for a new session.

PARAMETER	DESCRIPTION
session_id	Unique session identifier TYPE: str
global_type	Global session type TYPE: SessionType
strict	If True, raise on type violations TYPE: bool DEFAULT: True

RETURNS	DESCRIPTION
dict[ParticipantId, SessionMonitor]	Dictionary of monitors per participant

get_session(session_id)

Get monitors for an active session.

PARAMETER	DESCRIPTION
session_id	Session identifier TYPE: str

RETURNS	DESCRIPTION
dict[ParticipantId, SessionMonitor] | None	Dictionary of monitors or None if not found

close_session(session_id)

Close and remove a session.

PARAMETER	DESCRIPTION
session_id	Session to close TYPE: str

RETURNS	DESCRIPTION
bool	True if session was active and closed

check_invariants(session_id)

Check MPST invariants for a session.

PARAMETER	DESCRIPTION
session_id	Session to check TYPE: str

RETURNS	DESCRIPTION
list[str]	List of violated invariant names

get_statistics()

Get checker statistics.

RETURNS	DESCRIPTION
dict[str, Any]	Dictionary with statistics