| Safe Haskell | None |
|---|
CSPM.Evaluator.ProcessValues
- data Event
- type EventSet = Seq Event
- eventSetFromList :: [Event] -> EventSet
- type EventMap = Seq (Event, Event)
- data Proc seq op pn ev evs evm
- 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
- = 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
- data ProcOperator seq evs
- = Chase Bool
- | Determinise
- | Diamond
- | Explicate Bool
- | Normalize Bool
- | ModelCompress
- | Prioritise Bool (seq evs)
- | StrongBisim
- | TauLoopFactor
- | WeakBisim
- newtype ProcName = ProcName ScopeIdentifier
- operator :: Proc seq op pn ev evs evm -> op seq ev evs evm
- components :: Proc Seq op pn ev evs evm -> Seq (Proc Seq op pn ev evs evm)
- 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)])
- trimProcess :: UnCompiledProc -> UnCompiledProc
Events
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
eventSetFromList :: [Event] -> EventSetSource
Processes
data Proc seq op pn ev evs evm Source
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 UnCompiledProcOperator = ProcOperator Seq (Seq Event)Source
type UnCompiledOperator = CSPOperator Seq Event (Seq Event) (Seq (Event, Event))Source
data CSPOperator seq ev evs evm Source
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 Source
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) |
ProcNames uniquely identify processes.
Constructors
| ProcName ScopeIdentifier |
operator :: Proc seq op pn ev evs evm -> op seq ev evs evmSource
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)Source
Returns the components of a given process.