-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Definition of a FDR-compatible CSP core-language.
--   
--   This package contains an interface for a CSP core-language. It defines
--   processes, events, event sets, a EDSL for process operations like
--   parallel or interleaving. This interface can be used to implement a
--   FDR-2.83 compatible CSPM animator. We use this interface in our tool
--   to connect the functional CSPM-sub-language with core CSP
--   functionality.
@package CSPM-CoreLanguage
@version 0.3.0.1


-- | 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 <a>Event</a>,
--   <a>EventSet</a>, <a>RenamingRelation</a> and the class <a>BE</a>
--   (<a>BE</a>== base event).
--   
--   For full CSPM support (channels with multiple fields, event closure
--   sets etc.) CSPM.CoreLanguage.Field is also needed.
module CSPM.CoreLanguage.Event

-- | Sigma is the set of all events that appear in a system.
type Sigma i = EventSet i

-- | The first argument of all functions in <a>BE</a> is a
--   phantom-type-argument, i.e. applications pass _|_ and implementations
--   must not use this value.
class BE i
eventEq :: BE i => i -> Event i -> Event i -> Bool
member :: BE i => i -> Event i -> EventSet i -> Bool
intersection :: BE i => i -> EventSet i -> EventSet i -> EventSet i
difference :: BE i => i -> EventSet i -> EventSet i -> EventSet i
union :: BE i => i -> EventSet i -> EventSet i -> EventSet i
null :: BE i => i -> EventSet i -> Bool
singleton :: BE i => i -> Event i -> EventSet i
insert :: BE i => i -> Event i -> EventSet i -> EventSet i
delete :: BE i => i -> Event i -> EventSet i -> EventSet i
eventSetToList :: BE i => i -> EventSet i -> [Event i]
allEvents :: BE i => i -> EventSet i
isInRenaming :: BE i => i -> RenamingRelation i -> Event i -> Event i -> Bool
imageRenaming :: BE i => i -> RenamingRelation i -> Event i -> [Event i]
preImageRenaming :: BE i => i -> RenamingRelation i -> Event i -> [Event i]
isInRenamingDomain :: BE i => i -> Event i -> RenamingRelation i -> Bool
isInRenamingRange :: BE i => i -> Event i -> RenamingRelation i -> Bool
getRenamingDomain :: BE i => i -> RenamingRelation i -> [Event i]
getRenamingRange :: BE i => i -> RenamingRelation i -> [Event i]
renamingFromList :: BE i => i -> [(Event i, Event i)] -> RenamingRelation i
renamingToList :: BE i => i -> RenamingRelation i -> [(Event i, Event i)]
singleEventToClosureSet :: BE i => i -> Event i -> EventSet i

-- | A wrapper for tick-events, tau-events and events from Sigma.
data TTE i
TickEvent :: TTE i
TauEvent :: TTE i
SEvent :: (Event i) -> TTE i
class ShowEvent i
showEvent :: ShowEvent i => i -> String
class ShowTTE i
showTTE :: ShowTTE i => i -> String
instance Typeable1 TTE


-- | This modules defines an FDR-compatible CSP core language. The core
--   language deals with CSP-related constructs like processes and events.
--   
--   The implementation of the underlying language must provide instances
--   for the type families <a>Prefix</a>, <a>ExtProcess</a> and class
--   <a>BL</a>.
module CSPM.CoreLanguage.Process

-- | A prefix expression.

-- | A process that has not yet been switched on.
class BE i => BL i
prefixNext :: BL i => Prefix i -> Event i -> Maybe (Process i)
switchOn :: BL i => ExtProcess i -> Process i

-- | A data type for CSPM processes. For efficiency, replicated
--   alphabetized parallel has an explicit constructor. Other replicated
--   operations get translated on the fly. For constructing processes one
--   should rather use the wrappers from CSPM.CoreLanguage.ProcessWrappers.
data Process i
Prefix :: (Prefix i) -> Process i
ExternalChoice :: (Process i) -> (Process i) -> Process i
InternalChoice :: (Process i) -> (Process i) -> Process i
Interleave :: (Process i) -> (Process i) -> Process i
Interrupt :: (Process i) -> (Process i) -> Process i
Timeout :: (Process i) -> (Process i) -> Process i
Sharing :: (Process i) -> (EventSet i) -> (Process i) -> Process i
AParallel :: (EventSet i) -> (EventSet i) -> (Process i) -> (Process i) -> Process i
RepAParallel :: [(EventSet i, Process i)] -> Process i
Seq :: (Process i) -> (Process i) -> Process i
Hide :: (EventSet i) -> (Process i) -> Process i
Stop :: Process i
Skip :: Process i
Omega :: Process i
Chaos :: (EventSet i) -> Process i

-- | Just for debugging.
AProcess :: Int -> Process i
SwitchedOff :: (ExtProcess i) -> Process i
Renaming :: (RenamingRelation i) -> (Process i) -> Process i
LinkParallel :: (RenamingRelation i) -> (Process i) -> (Process i) -> Process i
Exception :: (EventSet i) -> (Process i) -> (Process i) -> Process i
isOmega :: Process i -> Bool
instance Typeable1 Process


-- | Wrappers for the constructors of data type <a>Process</a> and some
--   rewriting rules for replicated operations.
--   
--   This can also be used as EDSL for CSP.
module CSPM.CoreLanguage.ProcessWrapper
prefix :: Prefix i -> Process i
externalChoice :: Process i -> Process i -> Process i
internalChoice :: Process i -> Process i -> Process i
interleave :: Process i -> Process i -> Process i
interrupt :: Process i -> Process i -> Process i
timeout :: Process i -> Process i -> Process i
sharing :: Process i -> EventSet i -> Process i -> Process i
aparallel :: EventSet i -> EventSet i -> Process i -> Process i -> Process i
seq :: Process i -> Process i -> Process i
hide :: EventSet i -> Process i -> Process i
stop :: Process i
skip :: Process i
switchedOff :: ExtProcess i -> Process i
renaming :: RenamingRelation i -> Process i -> Process i
linkParallel :: RenamingRelation i -> Process i -> Process i -> Process i
repSeq :: [Process i] -> Process i
repInternalChoice :: [Process i] -> Process i
repExternalChoice :: [Process i] -> Process i
repInterleave :: [Process i] -> Process i
repAParallel :: [(EventSet i, Process i)] -> Process i
repSharing :: EventSet i -> [Process i] -> Process i
repLinkParallel :: RenamingRelation i -> [Process i] -> Process i
chaos :: EventSet i -> Process i


-- | This module defines the class <a>BF</a> for versions of CSP that also
--   support multi-field-events and event-closure sets.
module CSPM.CoreLanguage.Field
class BL i => BF i
fieldEq :: BF i => i -> Field i -> Field i -> Bool
member :: BF i => i -> Field i -> FieldSet i -> Bool
intersection :: BF i => i -> FieldSet i -> FieldSet i -> FieldSet i
difference :: BF i => i -> FieldSet i -> FieldSet i -> FieldSet i
union :: BF i => i -> FieldSet i -> FieldSet i -> FieldSet i
null :: BF i => i -> FieldSet i -> Bool
singleton :: BF i => i -> Field i -> FieldSet i
insert :: BF i => i -> Field i -> FieldSet i -> FieldSet i
delete :: BF i => i -> Field i -> FieldSet i -> FieldSet i
fieldSetToList :: BF i => i -> FieldSet i -> [Field i]
fieldSetFromList :: BF i => i -> [Field i] -> FieldSet i
joinFields :: BF i => i -> [Field i] -> Event i
splitFields :: BF i => i -> Event i -> [Field i]
channelLen :: BF i => i -> Field i -> Int
closureStateInit :: BF i => i -> EventSet i -> ClosureState i
closureStateNext :: BF i => i -> ClosureState i -> Field i -> ClosureState i
closureRestore :: BF i => i -> ClosureState i -> EventSet i
viewClosureState :: BF i => i -> ClosureState i -> ClosureView
viewClosureFields :: BF i => i -> ClosureState i -> FieldSet i
seenPrefixInClosure :: BF i => i -> ClosureState i -> Bool
prefixStateInit :: BF i => i -> Prefix i -> PrefixState i
prefixStateNext :: BF i => i -> PrefixState i -> Field i -> Maybe (PrefixState i)
prefixStateFinalize :: BF i => i -> PrefixState i -> Maybe (Prefix i)
viewPrefixState :: BF i => i -> PrefixState i -> PrefixFieldView i
data ClosureView
InClosure :: ClosureView
NotInClosure :: ClosureView
MaybeInClosure :: ClosureView
data PrefixFieldView i
FieldOut :: (Field i) -> PrefixFieldView i
FieldIn :: PrefixFieldView i
FieldGuard :: (FieldSet i) -> PrefixFieldView i
instance Show ClosureView
instance Eq ClosureView
instance Ord ClosureView


-- | Just re-exports.
module CSPM.CoreLanguage

-- | The version of the CSPM-CoreLangugage library
coreLanguageVersion :: Version