ts

This module provides the framework for easily defining transition systems and transition-system (parameteric) terms/formulas.

A transition-system term (TSTerm) can be thought of as a term (or formula) with "holes" for transition-system symbols (constants, functions, relations) and free variables.

class BaseTransitionSystem(abc.ABC):

Abstract base class for all transition-system implementation: user-defined (via TransitionSystem) or programmatically built (like timers.TimerTransitionSystem). The fields of a BaseTransitionSystem represent a state in the system.

next: Self

Get the post-state version of the transition system.

Returns

A transition system with suffix "'" representing the next state.

def sanity_check(self) -> bool:

Provides a simple sanity check for the system:

Checking the initial state is satisfiable
Checking every transition is satisfiable
Checking the initial state & disjunction of all transitions is satisfiable

Returns

whether the system is sane

class Params(typing.Protocol):

A protocol representing parameters (free variables) of a parametric term. Can be thought of as a mapping of names (str) to Z3 expressions (z3.ExprRef).

class ParamSpec(dict[str, Sort]):

A specification of parameters: a mapping of names (str) to sorts (typed_z3.Sort, classes derived from typed_z3.Expr).

@dataclass(frozen=True)

class TSTerm(typing.Generic[T]):

A transition-system term. Given a transition system state (instance of BaseTransitionSystem) and values for its parameters (see spec), produces a term of type T.

spec: ParamSpec

The specification for the parameters (free variables) of the term.

type TSFormula = TSTerm[z3.z3.BoolRef]

Shorthand for a TSTerm the returns a formula (z3.BoolRef).

type Immutable = Annotated[T, 'immutable']

Annotation for immutable symbols in a user-defined transition system (see TransitionSystem).

class TransitionSystem(BaseTransitionSystem, abc.ABC):

User-defined transition system. A transition system is defined by subclassing this class, declaring the signature using fields, and annotating methods as conjuncts of the initial state (@init), transitions (@transition), or axioms (@axiom).

Symbols (constants, functions, relations) in the vocabulary of the transition system's state are declared with fields, annotated with their sort:

class Thread(Finite): ...

class TerminationSystem(TransitionSystem):
    # A mutable constant of sort Thread
    running: Thread

    # An immutable constant of sort Thread
    first: Immutable[Thread]

    # A mutable unary relation over threads
    on: Rel[Thread]

    # An immutable binary relation
    gt: Immutable[Rel[Thread, Thread]]

    # An immutable binary relation, declared to be well-founded
    lt: Immutable[WFRel[Thread]]

    # An immutable function from threads to threads
    prev: Immutable[Fun[Thread, Thread]]

See also: typed_z3.Expr, typed_z3.Fun, typed_z3.Rel, typed_z3.WFRel, axiom, init, transition.

Inherited Members

BaseTransitionSystem: next; sanity_check

def init( fun: TypedFormula[T, typing.Unpack[Ts]]) -> TypedFormula[T, typing.Unpack[Ts]]:

Decorator for defining an initial-state conjunct. Should only be used inside a subclass of TransitionSystem. Parameters to the decorated method are implicitly universally quantified.

Parameters

fun: The formula function to mark as an initial state condition.

Returns

The decorated function.

Example:

class TerminationSystem(TransitionSystem):
    # snip...

    @init
    def initially_all_on(T: Thread) -> BoolRef:
        return self.on(T)

def transition( fun: TypedFormula[T, typing.Unpack[Ts]]) -> TypedFormula[T, typing.Unpack[Ts]]:

Decorator for defining a transition. Should only be used inside a subclass of TransitionSystem. Parameters to the decorated method are implicitly existentially quantified.

Parameters

fun: The formula function to mark as a transition.

Returns

The decorated function.

Example:

class TerminationSystem(TransitionSystem):
    # snip...

    @transition
    def turn_off(t: Thread) -> BoolRef:
        return self.on.update({(t,): false})

def axiom( fun: TypedFormula[T, typing.Unpack[Ts]]) -> TypedFormula[T, typing.Unpack[Ts]]:

Decorator for defining an axiom. Should only be used inside a subclass of TransitionSystem. Parameters to the decorated method are implicitly universally quantified.

Parameters

fun: The formula function to mark as an axiom.

Returns

The decorated function.

Example:

class TerminationSystem(TransitionSystem):
    # snip...

    @axiom
    def first_is_minimal(T: Thread) -> BoolRef:
        return Or(self.first == X, self.lt(self.first, X))

type TermLike = Union[TSTerm[E], Callable[..., E], E]

Any value that can be converted to a TSTerm. Usually not used directly, but as input for different objects that expect terms and formulas that are parametric by the transition system state and free variables (like orders and ranks).

Examples

A Z3 term with no free variables:

class Thread(Expr): ...
class MyTS(TransitionSystem):
    c: Thread
    f: Fun[Thread, Thread, Thread]

ts = MyTS()
example1: TermLike[Thread] = ts.f(ts.c, ts.c)

Free functions that explicitly receive a transition system and parameters:

def example2(ts: MyTS, x: Thread) -> Thread:
    return ts.f(ts.c, x)

Bound methods on transition systems:

class MyTS(TransitionSystem):
    # snip...

    def example3(self, x: Thread) -> Thread:
        return self.f(self.c, x)

See additional examples in ranks.

type FormulaLike = TermLike[z3.z3.BoolRef]

Any value that can be converted to a TSFormula, shorthand for TermLike for formulas (z3.BoolRef).