Process Calculus

Behavior expressions are the core of SPL. They describe process control flow using algebraic operators over actions and behavior names.

Terminals

Operators (by precedence, lowest to highest)

Prefix (sequential composition)

The dot . operator creates action-prefixed behaviors. a . P means "execute action a, then behave as P".

// Execute action a, then b, then terminate
P0 = a . b . done ;

When the left side of . is a named reference with arguments, it is parsed as an action prefix:

P0 = selectValidator(timeSlot) . P1 ;

Choice (nondeterministic)

The + operator models nondeterministic choice between alternatives:

// Either go left or go right
P0 = goLeft . P1 + goRight . P2 ;

N-ary choice is supported — multiple + alternatives are flattened:

P0 = action1 . P1
   + action2 . P2
   + action3 . P3 ;

Parallel composition

The || operator composes behaviors concurrently. Actions interleave nondeterministically:

// Two processes run concurrently
System = ProcessA || ProcessB ;

Guard

Square brackets [cond] create conditional guards:

Idle = [state == INVALID] HandleMiss
     + [state != INVALID] HandleHit ;

Guards are essential for modeling conditional branching.

Star (iteration)

The * postfix operator models repetition — zero or more executions:

P0 = (action . done) * ;

Recursion

Behavioral equations support mutual recursion through name references:

behavior {
    // P0 → P1 → P0 → P1 → ... (infinite loop)
    P0 = action1 . P1 ;
    P1 = action2 . P0 ;
}

A common pattern is looping back with a termination option:

behavior {
    P0 = processItem . P0    // loop
       + done ;              // or terminate
}

Parentheses

Use () to group sub-expressions:

P0 = a . (b . P1 + c . P2) ;

Algebraic laws

The substrate satisfies these laws (applied automatically during normalization):