CSPM.CoreLanguage.Event

This module 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, 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.

Documentation

type family Event i

type family EventSet i

type family RenamingRelation i

type Sigma i = EventSet i

Sigma is the set of all events that appear in a system.

class BE i where

The first argument of all functions in BE is a phantom-type-argument, i.e. applications pass _|_ and implementations must not use this value.

Minimal complete definition

eventEq, member, intersection, difference, union, null, singleton, insert, delete, eventSetToList, allEvents, isInRenaming, imageRenaming, preImageRenaming, isInRenamingDomain, isInRenamingRange, getRenamingDomain, getRenamingRange, renamingFromList, renamingToList, singleEventToClosureSet

Methods

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

A wrapper for tick-events, tau-events and events from Sigma.

Constructors

TickEvent

TauEvent

SEvent (Event i)

class ShowEvent i where

Minimal complete definition

showEvent

Methods

showEvent :: i -> String

class ShowTTE i where

Minimal complete definition

showTTE

Methods

showTTE :: i -> String