packages feed

CSPM-CoreLanguage (empty) → 0.1.0.0

raw patch · 8 files changed

+393/−0 lines, 8 filesdep +basesetup-changed

Dependencies added: base

Files

+ CSPM-CoreLanguage.cabal view
@@ -0,0 +1,35 @@+Name:                CSPM-CoreLanguage+Version:             0.1.0.0+Synopsis:            Definition of a FDR-compatible CSP core-language. +Description:+  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.+++Category:            Language,Formal Methods,Concurrency+License:             BSD3+License-File:        LICENSE+Author:              2010 Marc Fontaine+Maintainer:          Marc Fontaine <fontaine@cs.uni-duesseldorf.de>+Homepage:            http://www.stups.uni-duesseldorf.de/~fontaine/csp+Bug-reports:         http://asap0.cs.uni-duesseldorf.de/trac/prob/newticket+Stability:           experimental+Tested-With:         GHC == 6.12.2++cabal-Version:       >= 1.6+Build-Depends: base >= 4.0 && < 5.0++build-type: Simple+GHC-Options: -funbox-strict-fields -O2 -Wall+Hs-Source-Dirs:         src++Exposed-modules:+  CSPM.CoreLanguage+  CSPM.CoreLanguage.Event+  CSPM.CoreLanguage.Process+  CSPM.CoreLanguage.ProcessWrapper+  CSPM.CoreLanguage.Field
+ LICENSE view
@@ -0,0 +1,27 @@+Copyright (c) Marc Fontaine 2007-2009++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:+1. Redistributions of source code must retain the above copyright+   notice, this list of conditions and the following disclaimer.+2. Redistributions in binary form must reproduce the above copyright+   notice, this list of conditions and the following disclaimer in the+   documentation and/or other materials provided with the distribution.+3. Neither the name of the author nor the names of his contributors+   may be used to endorse or promote products derived from this software+   without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS ``AS IS'' AND+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE+ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY+OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF+SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,3 @@+#!/usr/bin/env runhaskell+import Distribution.Simple+main = defaultMain
+ src/CSPM/CoreLanguage.hs view
@@ -0,0 +1,28 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  CSPM.CoreLanguage+-- Copyright   :  (c) Fontaine 2010+-- License     :  BSD+-- +-- Maintainer  :  fontaine@cs.uni-duesseldorf.de+-- Stability   :  experimental+-- Portability :  GHC-only+--+-- Just re-exports.+--+-----------------------------------------------------------------------------+module CSPM.CoreLanguage+(+  module CSPM.CoreLanguage.Process+ ,module CSPM.CoreLanguage.ProcessWrapper+ ,module CSPM.CoreLanguage.Event+ ,module CSPM.CoreLanguage.Field+)+where++import CSPM.CoreLanguage.Process+import CSPM.CoreLanguage.ProcessWrapper+import CSPM.CoreLanguage.Event hiding (BE (..))+import CSPM.CoreLanguage.Event (BE)+import CSPM.CoreLanguage.Field hiding (BF (..))+import CSPM.CoreLanguage.Field (BF)
+ src/CSPM/CoreLanguage/Event.hs view
@@ -0,0 +1,63 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  CSPM.CoreLanguage.Event+-- Copyright   :  (c) Fontaine 2010+-- License     :  BSD+-- +-- Maintainer  :  fontaine@cs.uni-duesseldorf.de+-- Stability   :  experimental+-- Portability :  GHC-only+--+-- 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.+-----------------------------------------------------------------------------+{-# LANGUAGE TypeFamilies #-}++module CSPM.CoreLanguage.Event+where++type family Event i+type family EventSet i+type family RenamingRelation i++-- | Sigma is the set of all events that appear in a system.+type Sigma i = EventSet i++-- | The first argument of all function in 'BE' is a phantom-type-argument, i.e.+-- applications pass _|_ and implementations must not use this value.+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++-- | A wrapper for tick-events, tau-events and events from Sigma.+data TTE i+  = TickEvent+  | TauEvent+  | SEvent (Event i)++class ShowEvent i where showEvent :: i -> String+class ShowTTE i where showTTE :: i -> String
+ src/CSPM/CoreLanguage/Field.hs view
@@ -0,0 +1,65 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  CSPM.CoreLanguage.Field+-- Copyright   :  (c) Fontaine 2010+-- License     :  BSD+-- +-- Maintainer  :  fontaine@cs.uni-duesseldorf.de+-- Stability   :  experimental+-- Portability :  GHC-only+--+-- This modules extends 'BE' for languages that also support multi-field-events and+-- event-closure sets.+-----------------------------------------------------------------------------+{-# LANGUAGE TypeFamilies #-}++module CSPM.CoreLanguage.Field+where++import CSPM.CoreLanguage.Event+import CSPM.CoreLanguage.Process++type family Field i+type family FieldSet i+type family ClosureState i+type family PrefixState i++class BL i => BF i where+  fieldEq :: i -> Field i -> Field i -> Bool+  member :: i -> Field i -> FieldSet i -> Bool+  intersection :: i -> FieldSet i -> FieldSet i -> FieldSet i+  difference :: i -> FieldSet i -> FieldSet i -> FieldSet i+  union :: i -> FieldSet i -> FieldSet i -> FieldSet i+  null :: i -> FieldSet i -> Bool+  singleton :: i -> Field i -> FieldSet i+  insert :: i -> Field i -> FieldSet i -> FieldSet i+  delete :: i -> Field i -> FieldSet i -> FieldSet i+  fieldSetToList :: i -> FieldSet i -> [Field i]+  fieldSetFromList :: i -> [Field i] -> FieldSet i++  joinFields :: i -> [Field i] -> Event i+  splitFields :: i -> Event i -> [Field i]+  channelLen :: i -> Field i -> Int++  closureStateInit :: i -> EventSet i -> ClosureState i+  closureStateNext :: i -> ClosureState i -> Field i -> ClosureState i+  closureRestore   :: i -> ClosureState i -> EventSet i+  viewClosureState :: i -> ClosureState i -> ClosureView+  viewClosureFields :: i -> ClosureState i -> FieldSet i+  seenPrefixInClosure :: i -> ClosureState i -> Bool++  prefixStateInit :: i -> Prefix i -> PrefixState i+  prefixStateNext :: i -> PrefixState i -> Field i -> Maybe (PrefixState i)+  prefixStateFinalize :: i -> PrefixState i -> Maybe (Prefix i)+  viewPrefixState :: i -> PrefixState i -> PrefixFieldView i++data ClosureView+  = InClosure+  | NotInClosure+  | MaybeInClosure+  deriving (Show,Eq,Ord)++data PrefixFieldView i+  = FieldOut (Field i)+  | FieldIn+  | FieldGuard (FieldSet i)
+ src/CSPM/CoreLanguage/Process.hs view
@@ -0,0 +1,66 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  CSPM.CoreLanguage.Process+-- Copyright   :  (c) Fontaine 2010+-- License     :  BSD+-- +-- Maintainer  :  fontaine@cs.uni-duesseldorf.de+-- Stability   :  experimental+-- Portability :  GHC-only+--+-- This modules defines a FDR-compatible CSP core language.+-- The core language deals with CSP related constructs like processes and events,+-- but abstracts, e.g. from the underlying functional programming language.+--+-- The implementation of the underlying language+-- must provide instances for the type families 'Prefix' and 'ExtProcess' and class 'BL'.+-----------------------------------------------------------------------------+{-# LANGUAGE TypeFamilies #-}++module CSPM.CoreLanguage.Process where++import CSPM.CoreLanguage.Event++-- | A prefix expression.+type family Prefix i++-- | A proccess that has not yet been switched on.+type family ExtProcess i++class (BE i) => BL i where+  -- | Try to perform an 'Event' return the successor 'Process' or Nothing if the event is+  -- not possible.+  prefixNext :: Prefix i -> Event i -> Maybe (Process i)+  switchOn :: ExtProcess i -> Process i++{-|+  A data type for CSPM processes.+  For efficency, replicated alphabetized parallel has an explicit constructor.+  Other replicated operations get translated on the fly.+  For constructing processes one should rather uses the wrappers from +  CSPM.CoreLanguage.ProcessWrappers.+-}+data Process i+  = Prefix (Prefix i)+  | ExternalChoice (Process i) (Process i)+  | InternalChoice (Process i) (Process i)+  | Interleave  (Process i) (Process i)+  | Interrupt (Process i) (Process i)+  | Timeout (Process i) (Process i)+  | Sharing (Process i) (EventSet i) (Process i)+  | AParallel (EventSet i) (EventSet i) (Process i) (Process i) +  | RepAParallel [(EventSet i,Process i)]+  | Seq (Process i) (Process i)+  | Hide (EventSet i) (Process i)+  | Stop+  | Skip+  | Omega+  | Chaos (EventSet i)+  | AProcess Int -- ^ Just for debugging.+  | SwitchedOff  (ExtProcess i)+  | Renaming (RenamingRelation i) (Process i)+  | LinkParallel (RenamingRelation i) (Process i) (Process i)++isOmega :: Process i -> Bool+isOmega Omega = True+isOmega _ = False
+ src/CSPM/CoreLanguage/ProcessWrapper.hs view
@@ -0,0 +1,106 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  CSPM.CoreLanguage.Process+-- Copyright   :  (c) Fontaine 2010+-- License     :  BSD+-- +-- Maintainer  :  fontaine@cs.uni-duesseldorf.de+-- Stability   :  experimental+-- Portability :  GHC-only+--+-- Wrappers for the constructors of data type 'Process' and some+-- rewriting rules for replicated operations.+--+-- This can also be used an EDSL for CSP.+--+-----------------------------------------------------------------------------++module CSPM.CoreLanguage.ProcessWrapper+where++import CSPM.CoreLanguage.Process+import CSPM.CoreLanguage.Event++prefix :: Prefix i -> Process i+prefix = Prefix++externalChoice :: Process i -> Process i -> Process i+externalChoice = ExternalChoice++internalChoice :: Process i -> Process i -> Process i+internalChoice = InternalChoice++interleave :: Process i -> Process i -> Process i+interleave = Interleave++interrupt :: Process i -> Process i -> Process i+interrupt = Interrupt++timeout :: Process i -> Process i -> Process i+timeout = Timeout++sharing :: Process i -> EventSet i -> Process i -> Process i+sharing = Sharing++aparallel ::+     EventSet i -> EventSet i +  -> Process i -> Process i+  -> Process i+aparallel = AParallel+--aparallel a1 a2 p1 p2 = RepAParallel [(a1,p1),(a2,p2)]++seq :: Process i -> Process i -> Process i+seq = Seq++hide :: EventSet i -> Process i -> Process i+hide = Hide++stop :: Process i+stop = Stop++skip :: Process i+skip = Skip++switchedOff  :: ExtProcess i -> Process i+switchedOff = SwitchedOff++renaming :: RenamingRelation i -> Process i -> Process i+renaming = Renaming++linkParallel :: RenamingRelation i -> Process i -> Process i -> Process i+linkParallel = LinkParallel++repSeq :: [Process i] -> Process i+repSeq = foldr CSPM.CoreLanguage.ProcessWrapper.seq  skip++{- todo: create balanced trees of operators instead of list -}+repInternalChoice :: [Process i] -> Process i+repInternalChoice [] = stop+repInternalChoice l = foldr1 internalChoice l++repExternalChoice :: [Process i] -> Process i+repExternalChoice [] = stop+repExternalChoice l = foldr1 externalChoice l++repInterleave :: [Process i] -> Process i+repInterleave = foldr interleave skip++repAParallel :: [(EventSet i,Process i)] -> Process i+repAParallel l = case l of+  [] -> error "ProcessWrapper : empty repAParallel"+  [(_,p)] -> p+--  [(c1,p1),(c2,p2)] -> aparallel c1 c2 p1 p2 -- takes longer than generic version ?+  _ -> RepAParallel l++repSharing :: EventSet i -> [Process i] -> Process i+repSharing _ [] = error "ProcessWrapper.hs : empty repSharing"+repSharing _ [p] = p+repSharing c l = foldr1 (\a b -> sharing a c b) l++repLinkParallel :: RenamingRelation i -> [Process i] -> Process i+repLinkParallel _ [] = error "ProcessWrapper.hs : empty repLinkParallel"+repLinkParallel _ [_] = error "ProcessWrapper.hs : repLinkParallel over one process"+repLinkParallel rel l = foldr1 (\a b -> linkParallel rel a b) l++chaos :: EventSet i -> Process i+chaos = Chaos