CSPM.Evaluator.ProcessValues

Events

data Event

Events, as represented in the LTS.

Constructors

Tau

The internal special event tau.

Tick

The internal event tick, representing termination.

UserEvent Value

Any event defined in a channel definition.

Instances

Eq Event

Ord Event

NFData UnCompiledProcOperator

NFData UnCompiledOperator

NFData Event

NFData UProc

Hashable Event

PrettyPrintable UnCompiledProc

PrettyPrintable Event

(Applicative m, Monad m, MonadicPrettyPrintable m Value) => MonadicPrettyPrintable m Event

Foldable f => MonadicPrettyPrintable Identity (f Event)

Foldable f => MonadicPrettyPrintable EvaluationMonad (f Event)

PrettyPrintable (Seq Event)

type EventSet = Seq Event

eventSetFromList :: [Event] -> EventSet

type EventMap = Seq (Event, Event)

Processes

data Proc seq op pn ev evs evm

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

Constructors

PUnaryOp (op seq ev evs evm) (Proc seq op pn ev evs evm)

PBinaryOp (op seq ev evs evm) (Proc seq op pn ev evs evm) (Proc seq op pn ev evs evm)

POp (op seq ev evs evm) (seq (Proc seq op pn ev evs evm))

PProcCall pn (Proc seq op pn ev evs evm)

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

Instances

NFData UProc

PrettyPrintable UnCompiledProc

(Foldable seq, Functor seq, MonadicPrettyPrintable m pn, MonadicPrettyPrintable m ev, MonadicPrettyPrintable m evs) => MonadicPrettyPrintable m (Proc seq CSPOperator pn ev evs (seq (ev, ev)))

(Eq pn, Eq (seq (Proc seq op pn ev evs evm)), Eq (op seq ev evs evm)) => Eq (Proc seq op pn ev evs evm)

(Ord pn, Ord (seq (Proc seq op pn ev evs evm)), Ord (op seq ev evs evm)) => Ord (Proc seq op pn ev evs evm)

(Hashable pn, Hashable (seq (Proc seq op pn ev evs evm)), Hashable (op seq ev evs evm)) => Hashable (Proc seq op pn ev evs evm)

Precedence (Proc seq CSPOperator pn ev evs (seq (ev, ev)))

type UnCompiledProc = Proc Seq CSPOperator ProcName Event (Seq Event) (Seq (Event, Event))

type UnCompiledProcOperator = ProcOperator Seq (Seq Event)

type UnCompiledOperator = CSPOperator Seq Event (Seq Event) (Seq (Event, Event))

data CSPOperator seq ev evs evm

Constructors

PAlphaParallel (seq evs)

PException evs

PExternalChoice

PGenParallel evs

PHide evs

PInternalChoice

PInterrupt

PInterleave

PLinkParallel evm

POperator (ProcOperator seq evs)

PPrefix ev

PRename evm

PSequentialComp

PSlidingChoice

PSynchronisingExternalChoice evs

PSynchronisingInterrupt evs

Instances

NFData UnCompiledOperator

NFData UProc

PrettyPrintable UnCompiledProc

(Applicative m, Foldable seq, Functor seq, Monad m, MonadicPrettyPrintable m ev, MonadicPrettyPrintable m evs) => MonadicPrettyPrintable m (CSPOperator seq ev evs (seq (ev, ev)))

(Foldable seq, Functor seq, MonadicPrettyPrintable m pn, MonadicPrettyPrintable m ev, MonadicPrettyPrintable m evs) => MonadicPrettyPrintable m (Proc seq CSPOperator pn ev evs (seq (ev, ev)))

(Eq ev, Eq evs, Eq evm, Eq (seq evs)) => Eq (CSPOperator seq ev evs evm)

(Ord ev, Ord evs, Ord evm, Ord (seq evs)) => Ord (CSPOperator seq ev evs evm)

(Hashable ev, Hashable evm, Hashable evs, Hashable (seq evs)) => Hashable (CSPOperator seq ev evs evm)

Precedence (Proc seq CSPOperator pn ev evs (seq (ev, ev)))

data ProcOperator seq evs

An operator that can be applied to processes.

Constructors

Chase Bool

Determinise

Diamond

Explicate Bool

Normalize Bool

ModelCompress

Prioritise Bool (seq evs)

StrongBisim

TauLoopFactor

WeakBisim

Instances

NFData UnCompiledProcOperator

(Applicative m, Foldable seq, Monad m, MonadicPrettyPrintable m evs) => MonadicPrettyPrintable m (ProcOperator seq evs)

Eq (seq evs) => Eq (ProcOperator seq evs)

Ord (seq evs) => Ord (ProcOperator seq evs)

Hashable (seq evs) => Hashable (ProcOperator seq evs)

(Foldable seq, MonadicPrettyPrintable Identity evs) => PrettyPrintable (ProcOperator seq evs)

newtype ProcName

ProcNames uniquely identify processes.

Constructors

ProcName ScopeIdentifier

Instances

Eq ProcName

Ord ProcName

NFData ProcName

NFData UProc

Hashable ProcName

PrettyPrintable UnCompiledProc

PrettyPrintable ProcName

(Applicative m, Monad m, MonadicPrettyPrintable m Value) => MonadicPrettyPrintable m ProcName

operator :: Proc seq op pn ev evs evm -> op seq ev evs evm

Gives the operator of a process. If the process is a ProcCall an error is thrown.

components :: Proc Seq op pn ev evs evm -> Seq (Proc Seq op pn ev evs evm)

Returns the components of a given process.

splitProcIntoComponents :: (Eq pn, Foldable seq) => Proc seq op pn ev evs evm -> (Proc seq op pn ev evs evm, [(pn, Proc seq op pn ev evs evm)])

Given a process, returns the initial process and all processes that it calls.

trimProcess :: UnCompiledProc -> UnCompiledProc