CSPM.Evaluator.Values
- data Value
- data Proc
- = 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
- data ProcOperator
- = Chase
- | Diamond
- | Explicate
- | Normalize
- | ModelCompress
- | StrongBisim
- | TauLoopFactor
- | WeakBisim
- data Event
- compareValues :: Value -> Value -> Maybe Ordering
- procId :: Name -> [[Value]] -> ProcName
- valueEventToEvent :: Value -> Event
- combineDots :: Value -> Value -> EvaluationMonad Value
- extensions :: Value -> EvaluationMonad [Value]
- oneFieldExtensions :: Value -> EvaluationMonad [Value]
- productions :: Value -> EvaluationMonad [Value]
Documentation
Constructors
| VInt Int | |
| VBool Bool | |
| VTuple [Value] | |
| VDot [Value] | If A is a datatype clause that has 3 fields a b c then a runtime instantiation of this would be VDot [VDataType A, a, b, c] where a,b and c can contain other VDots. |
| VChannel Name | |
| VDataType Name | |
| VList [Value] | |
| VSet ValueSet | |
| VFunction ([Value] -> EvaluationMonad Value) | |
| VProc 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
data ProcOperator Source
An operator that can be applied to processes.
Constructors
| Chase | |
| Diamond | |
| Explicate | |
| Normalize | |
| ModelCompress | |
| StrongBisim | |
| TauLoopFactor | |
| WeakBisim |
Events, as represented in the LTS.
Constructors
| Tau | The internal special event tau. |
| Tick | The internal event tick, representing termination. |
| UserEvent String | Any event defined in a channel definition. |
Instances
compareValues :: Value -> Value -> Maybe OrderingSource
Implements CSPM comparisons (note that Ord Value does not).
valueEventToEvent :: Value -> EventSource
This assumes that the value is a VDot with the left is a VChannel
combineDots :: Value -> Value -> EvaluationMonad ValueSource
Takes two values and dots then together appropriately.
extensions :: Value -> EvaluationMonad [Value]Source
Takes a datatype or a channel value and then computes all x such that ev.x is a full datatype/event. Each of the returned values is guaranteed to be a VDot.
oneFieldExtensions :: Value -> EvaluationMonad [Value]Source
Returns an x such that ev.x has been extended by exactly one atomic field. This could be inside a subfield or elsewhere.
productions :: Value -> EvaluationMonad [Value]Source
Takes a datatype or a channel value and computes v.x for all x that complete the value.