agenticraft_foundation.algebra.semantics

Operational semantics — LTS construction, trace extraction, deadlock detection, and liveness analysis.

Labeled Transition System (LTS) for CSP operational semantics.

This module provides: - LTS representation of process behavior - State space exploration - Trace generation - Deadlock detection

An LTS is a tuple (S, Act, →, s₀) where: - S: set of states - Act: set of actions/events - →: transition relation S × Act × S - s₀: initial state

Transition dataclass

A transition in an LTS: source ─event→ target.

LTSState dataclass

A state in the LTS, wrapping a process.

LTS dataclass

Labeled Transition System.

Represents the operational semantics of a CSP process as a graph.

ATTRIBUTE	DESCRIPTION
states	All states in the LTS TYPE: dict[int, LTSState]
transitions	All transitions TYPE: list[Transition]
initial_state	The starting state ID TYPE: int
alphabet	All events in the LTS TYPE: frozenset[Event]

num_states property

Number of states in the LTS.

num_transitions property

Number of transitions in the LTS.

add_state(state)

Add a state to the LTS.

add_transition(transition)

Add a transition to the LTS.

get_transitions_from(state_id)

Get all transitions from a state.

get_transitions_to(state_id)

Get all transitions to a state.

successors(state_id)

Yield (event, target_state) pairs for transitions from state.

predecessors(state_id)

Yield (event, source_state) pairs for transitions to state.

deadlock_states()

Return IDs of deadlock states.

terminal_states()

Return IDs of terminal (successfully terminated) states.

LTSBuilder

Builds an LTS from a CSP process through state space exploration.

Uses breadth-first exploration to discover all reachable states and transitions. State identity is determined by _state_key() of the process term -- structurally identical terms produce the same tuple key and map to the same state. This is conservative: semantically equivalent but structurally different terms may create duplicate states, which increases the state space but never misses behaviors.

Note: Processes containing callables (e.g., Guard) use object identity (id()) in their state key, so distinct Guard instances with equivalent conditions will be treated as different states.

__init__(max_states=10000, max_depth=1000)

Initialize the builder.

PARAMETER	DESCRIPTION
max_states	Maximum number of states to explore TYPE: int DEFAULT: 10000
max_depth	Maximum depth of exploration TYPE: int DEFAULT: 1000

build(process)

Build an LTS from a process.

PARAMETER	DESCRIPTION
process	The CSP process to analyze TYPE: Process

RETURNS	DESCRIPTION
LTS	The resulting LTS

DeadlockAnalysis dataclass

Result of deadlock analysis.

LivenessAnalysis dataclass

Result of liveness analysis.

traces(lts, max_length=100, include_tau=False)

Generate all traces of the LTS up to a maximum length.

A trace is a sequence of visible events (τ is typically hidden).

PARAMETER	DESCRIPTION
lts	The LTS to analyze TYPE: LTS
max_length	Maximum trace length TYPE: int DEFAULT: 100
include_tau	Whether to include τ (internal) events TYPE: bool DEFAULT: False

YIELDS	DESCRIPTION
Trace	Traces as tuples of events

maximal_traces(lts, max_length=100)

Generate maximal traces (traces that cannot be extended).

A maximal trace ends in either: - A deadlock state - A terminal state (successful termination) - Maximum length reached

PARAMETER	DESCRIPTION
lts	The LTS to analyze TYPE: LTS
max_length	Maximum trace length TYPE: int DEFAULT: 100

YIELDS	DESCRIPTION
Trace	Maximal traces

accepts(lts, trace)

Check if the LTS can perform the given trace.

PARAMETER	DESCRIPTION
lts	The LTS to check TYPE: LTS
trace	The trace to verify TYPE: Trace

RETURNS	DESCRIPTION
bool	True if the trace can be performed

detect_deadlock(lts, max_trace_length=50)

Detect deadlock states and find traces leading to them.

PARAMETER	DESCRIPTION
lts	The LTS to analyze TYPE: LTS
max_trace_length	Maximum trace length to consider TYPE: int DEFAULT: 50

RETURNS	DESCRIPTION
DeadlockAnalysis	DeadlockAnalysis with results

analyze_liveness(lts, events_of_interest=None)

Analyze liveness properties of the LTS.

PARAMETER	DESCRIPTION
lts	The LTS to analyze TYPE: LTS
events_of_interest	Events to check for liveness TYPE: set[Event] | None DEFAULT: None

RETURNS	DESCRIPTION
LivenessAnalysis	LivenessAnalysis with results

build_lts(process, max_states=10000)

Build an LTS from a process.

PARAMETER	DESCRIPTION
process	The CSP process TYPE: Process
max_states	Maximum states to explore TYPE: int DEFAULT: 10000

RETURNS	DESCRIPTION
LTS	The LTS representation

is_deadlock_free(process)

Check if a process is deadlock-free.

PARAMETER	DESCRIPTION
process	The CSP process to check TYPE: Process

RETURNS	DESCRIPTION
bool	True if the process cannot deadlock