| Portability | GHC-only |
|---|---|
| Stability | experimental |
| Maintainer | fontaine@cs.uni-duesseldorf.de |
CSPM.CoreLanguage.Event
Description
This modules defines the event-related part of an interface between
the CSPM-CoreLanguage and the underlying implementation.
The underlying implementation has to instantiate the type-families Event, EventSet
and RenamingRelation and the class BE (BE== base event).
For full CSPM-support (channels with multiple fields, event closure sets etc.) CSPM.CoreLanguage.Field is also needed.
- type family Event i
- type family EventSet i
- type family RenamingRelation i
- type Sigma i = EventSet i
- class BE i where
- eventEq :: i -> Event i -> Event i -> Bool
- member :: i -> Event i -> EventSet i -> Bool
- intersection :: i -> EventSet i -> EventSet i -> EventSet i
- difference :: i -> EventSet i -> EventSet i -> EventSet i
- union :: i -> EventSet i -> EventSet i -> EventSet i
- null :: i -> EventSet i -> Bool
- singleton :: i -> Event i -> EventSet i
- insert :: i -> Event i -> EventSet i -> EventSet i
- delete :: i -> Event i -> EventSet i -> EventSet i
- eventSetToList :: i -> EventSet i -> [Event i]
- allEvents :: i -> EventSet i
- isInRenaming :: i -> RenamingRelation i -> Event i -> Event i -> Bool
- imageRenaming :: i -> RenamingRelation i -> Event i -> [Event i]
- preImageRenaming :: i -> RenamingRelation i -> Event i -> [Event i]
- isInRenamingDomain :: i -> Event i -> RenamingRelation i -> Bool
- isInRenamingRange :: i -> Event i -> RenamingRelation i -> Bool
- getRenamingDomain :: i -> RenamingRelation i -> [Event i]
- getRenamingRange :: i -> RenamingRelation i -> [Event i]
- renamingFromList :: i -> [(Event i, Event i)] -> RenamingRelation i
- renamingToList :: i -> RenamingRelation i -> [(Event i, Event i)]
- singleEventToClosureSet :: i -> Event i -> EventSet i
- data TTE i
- class ShowEvent i where
- class ShowTTE i where
Documentation
type family RenamingRelation i Source
The first argument of all function in BE is a phantom-type-argument, i.e.
applications pass _|_ and implementations must not use this value.
Methods
eventEq :: i -> Event i -> Event i -> BoolSource
member :: i -> Event i -> EventSet i -> BoolSource
intersection :: i -> EventSet i -> EventSet i -> EventSet iSource
difference :: i -> EventSet i -> EventSet i -> EventSet iSource
union :: i -> EventSet i -> EventSet i -> EventSet iSource
null :: i -> EventSet i -> BoolSource
singleton :: i -> Event i -> EventSet iSource
insert :: i -> Event i -> EventSet i -> EventSet iSource
delete :: i -> Event i -> EventSet i -> EventSet iSource
eventSetToList :: i -> EventSet i -> [Event i]Source
allEvents :: i -> EventSet iSource
isInRenaming :: i -> RenamingRelation i -> Event i -> Event i -> BoolSource
imageRenaming :: i -> RenamingRelation i -> Event i -> [Event i]Source
preImageRenaming :: i -> RenamingRelation i -> Event i -> [Event i]Source
isInRenamingDomain :: i -> Event i -> RenamingRelation i -> BoolSource
isInRenamingRange :: i -> Event i -> RenamingRelation i -> BoolSource
getRenamingDomain :: i -> RenamingRelation i -> [Event i]Source
getRenamingRange :: i -> RenamingRelation i -> [Event i]Source
renamingFromList :: i -> [(Event i, Event i)] -> RenamingRelation iSource
renamingToList :: i -> RenamingRelation i -> [(Event i, Event i)]Source
singleEventToClosureSet :: i -> Event i -> EventSet iSource
A wrapper for tick-events, tau-events and events from Sigma.