CSPM-CoreLanguage-0.2.0.3: Definition of a FDR-compatible CSP core-language.

PortabilityGHC-only
Stabilityexperimental
Maintainerfontaine@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.

Synopsis

Documentation

type family Event i Source

type family EventSet i Source

type family RenamingRelation i Source

type Sigma i = EventSet iSource

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

class BE i whereSource

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

data TTE i Source

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

Constructors

TickEvent 
TauEvent 
SEvent (Event i) 

class ShowEvent i whereSource

Methods

showEvent :: i -> StringSource

class ShowTTE i whereSource

Methods

showTTE :: i -> StringSource