CSPM.Compiler.Processes

This module provides the input data structure to the compiler.

Documentation

data Proc

A compiled process. Note this is an infinite data structure (due to PProcCall) as this makes compilation easy (we can easily chase dependencies).

Constructors

PAlphaParallel [(Set Event, Proc)]

PException Proc (Set Event) Proc

PExternalChoice [Proc]

PGenParallel (Set Event) [Proc]

PHide Proc (Set Event)

PInternalChoice [Proc]

PInterrupt Proc Proc

PInterleave [Proc]

PLinkParallel Proc (Map Event Event) Proc

POperator ProcOperator Proc

PPrefix Event Proc

PRename (Relation Event Event) Proc

PSequentialComp Proc Proc

PSlidingChoice Proc Proc

PProcCall ProcName Proc

Labels the process this contains. This allows infinite loops to be spotted.

Instances

Show Proc

PrettyPrintable Proc

data ProcOperator

An operator that can be applied to processes.

Constructors

Chase

Diamond

Explicate

Normalize

ModelCompress

StrongBisim

TauLoopFactor

WeakBisim

Instances

Eq ProcOperator

Show ProcOperator

PrettyPrintable ProcOperator

data ProcName

ProcNames uniquely identify processes.

Constructors

ProcName

Fields

name :: Name

The name of this process (recal Name s are unique).

arguments :: [[Value]]

The arguments applied to this process, in case it was a function call.

Instances

Eq ProcName

Show ProcName

PrettyPrintable ProcName

prettyPrintAllRequiredProcesses :: Proc -> Doc

Pretty prints the given process and all processes that it depends upon.