agenticraft_foundation.algebra.csp¶
CSP process definitions — 13 operators implementing the full Process contract.
CSP (Communicating Sequential Processes) implementation.
Based on Hoare (1985) - Communicating Sequential Processes.
This module provides: - Core process primitives (STOP, SKIP, Prefix) - Choice operators (external □, internal ⊓) - Parallel composition (interleaving ||, synchronized |[A]|) - Sequential composition (;) - Hiding (P \ H)
Key Concepts: - Process: Entity that can engage in events - Event: Atomic unit of communication/action - Alphabet: Set of events a process can engage in - Trace: Sequence of events performed by a process
Event
¶
Bases: str
An event in CSP.
Events are atomic units of communication or action. The special event "✓" (TICK) indicates successful termination.
ProcessKind
¶
Bases: Enum
Classification of process types.
Process
¶
Bases: ABC
Abstract base class for CSP processes.
A process is characterized by: - alphabet: The set of events it can engage in - initials: The initial events it can perform - after(e): The process after performing event e
kind
abstractmethod
property
¶
Process classification.
alphabet()
abstractmethod
¶
Return the alphabet (set of events) this process can engage in.
initials()
abstractmethod
¶
Return the set of initial events the process can perform.
after(event)
abstractmethod
¶
can_perform(event)
¶
Check if the process can perform the given event.
is_deadlocked()
¶
Check if the process is deadlocked (no possible events).
is_terminated()
¶
Check if the process has successfully terminated.
Stop
dataclass
¶
Bases: Process
STOP - The deadlocked process.
STOP cannot perform any events. It represents deadlock.
Properties: - alphabet(STOP) = {} - initials(STOP) = {} - traces(STOP) = {⟨⟩}
Skip
dataclass
¶
Bases: Process
SKIP - Successful termination.
SKIP can only perform the tick event (✓) and then becomes STOP.
Properties: - alphabet(SKIP) = {✓} - initials(SKIP) = {✓} - traces(SKIP) = {⟨⟩, ⟨✓⟩}
Prefix
dataclass
¶
Bases: Process
a → P (Prefix/Guarding).
Prefix performs event 'a' and then behaves as process P.
Properties: - alphabet(a → P) = {a} ∪ alphabet(P) - initials(a → P) = {a} - (a → P) ─a→ P
ExternalChoice
dataclass
¶
Bases: Process
P □ Q (External Choice).
The environment chooses between P and Q based on the initial event.
Properties: - alphabet(P □ Q) = alphabet(P) ∪ alphabet(Q) - initials(P □ Q) = initials(P) ∪ initials(Q) - P □ Q ─a→ P' if P ─a→ P' and a ∉ initials(Q) - P □ Q ─a→ Q' if Q ─a→ Q' and a ∉ initials(P) - P □ Q ─a→ P' ⊓ Q' if a ∈ initials(P) ∩ initials(Q) (nondeterministic)
after(event)
¶
Resolve external choice by performing an event.
When both branches offer the event, the result is an internal (nondeterministic) choice between the two continuations, per Roscoe (1998) §3.3.
| PARAMETER | DESCRIPTION |
|---|---|
event
|
The event to perform.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
Process
|
Continuation process after performing the event. |
| RAISES | DESCRIPTION |
|---|---|
ValueError
|
If neither branch can perform the event. |
InternalChoice
dataclass
¶
Bases: Process
P ⊓ Q (Internal/Nondeterministic Choice).
The process internally chooses between P and Q. The environment has no control over which branch is taken.
Properties: - alphabet(P ⊓ Q) = alphabet(P) ∪ alphabet(Q) - initials(P ⊓ Q) = initials(P) ∪ initials(Q) - P ⊓ Q ─τ→ P (internal transition to P) - P ⊓ Q ─τ→ Q (internal transition to Q)
Parallel
dataclass
¶
Bases: Process
P |[A]| Q (Generalized Parallel Composition).
P and Q run in parallel, synchronizing on events in A. - Events in A require both processes to participate - Events not in A can be performed independently
Special cases: - P ||| Q (A = {}) : Interleaving (no synchronization) - P || Q (A = alphabet(P) ∩ alphabet(Q)) : Alphabetized parallel
Properties: - alphabet(P |[A]| Q) = alphabet(P) ∪ alphabet(Q) - For a ∈ A: P |[A]| Q ─a→ P' |[A]| Q' iff P ─a→ P' and Q ─a→ Q' - For a ∉ A: P |[A]| Q ─a→ P' |[A]| Q iff P ─a→ P'
Sequential
dataclass
¶
Bases: Process
P ; Q (Sequential Composition).
P runs first, and when it terminates (performs ✓), Q starts.
Properties: - alphabet(P ; Q) = (alphabet(P) - {✓}) ∪ alphabet(Q) - initials(P ; Q) = initials(P) - {✓} if ✓ ∉ initials(P) = (initials(P) - {✓}) ∪ initials(Q) if ✓ ∈ initials(P) - P ; Q ─a→ P' ; Q if P ─a→ P' and a ≠ ✓ - P ; Q ─τ→ Q if P ─✓→ (starts Q after P terminates)
Hiding
dataclass
¶
Bases: Process
P \ H (Hiding).
Events in H are hidden (become internal τ actions).
Properties: - alphabet(P \ H) = alphabet(P) - H - P \ H ─a→ P' \ H if P ─a→ P' and a ∉ H - P \ H ─τ→ P' \ H if P ─a→ P' and a ∈ H
Recursion
dataclass
¶
Variable
dataclass
¶
substitute(process, var_name, replacement)
¶
Substitute all occurrences of a named variable with a process.
Recursively traverses the process tree, replacing each Variable
node whose name matches var_name with replacement. Respects
variable shadowing in Recursion nodes.
| PARAMETER | DESCRIPTION |
|---|---|
process
|
The process tree to transform.
TYPE:
|
var_name
|
Name of the variable to replace.
TYPE:
|
replacement
|
Process to substitute in place of the variable.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
Process
|
A new process tree with all matching variables replaced. |
stop()
¶
Create STOP process.
skip()
¶
Create SKIP process.
prefix(event, continuation)
¶
Create prefix process: event → continuation.
choice(left, right)
¶
Create external choice: left □ right.
internal_choice(left, right)
¶
Create internal choice: left ⊓ right.
parallel(left, right, sync=None)
¶
Create parallel composition: left |[sync]| right.
interleave(left, right)
¶
Create interleaving: left ||| right.
sequential(first, second)
¶
Create sequential composition: first ; second.
hide(process, hidden)
¶
Create hiding: process \ hidden.
rec(variable, body)
¶
Create recursion: μvariable.body.
var(name)
¶
Create recursion variable.