CSPM-FiringRules (empty) → 0.1.0.0

raw patch · 13 files changed

+2317/−0 lines, 13 filesdep +CSPM-CoreLanguagedep +QuickCheckdep +basesetup-changed

Dependencies added: CSPM-CoreLanguage, QuickCheck, base, containers, mtl, random

Files

• CSPM-FiringRules.cabal +48/−0
• LICENSE +27/−0
• Setup.hs +3/−0
• src/CSPM/FiringRules/EnumerateEvents.hs +238/−0
• src/CSPM/FiringRules/FieldConstraints.hs +595/−0
• src/CSPM/FiringRules/HelperClasses.hs +40/−0
• src/CSPM/FiringRules/Rules.hs +172/−0
• src/CSPM/FiringRules/Test/Gen.hs +237/−0
• src/CSPM/FiringRules/Test/Mock1.hs +103/−0
• src/CSPM/FiringRules/Test/Mock2.hs +251/−0
• src/CSPM/FiringRules/Test/Test.hs +219/−0
• src/CSPM/FiringRules/Trace.hs +48/−0
• src/CSPM/FiringRules/Verifier.hs +336/−0

@@ -0,0 +1,48 @@+Name:                CSPM-FiringRules+Version:             0.1.0.0+Synopsis:            Firing rules semantic of CSPM+Description:+  This package contains functions for computing the transitions of a CSP process+  based on the standard CSP firing rule semantic+  (see The Theory and Practice of Concurrency A.W. Roscoe 1999.)+  It also contains a rudimentary tracer for executing transitions,+  some QuickCheck tests, and a data type for proof trees.+  To use this package one has to provide instances for the classes and type families,+  defined in the CSPM-CoreLanguage package.+  The package contains two mock-implementations that provide these instances.+  The CSPM-Interpreter package contains an other implementation.++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+Stability:           experimental+Tested-With:         GHC == 6.12.2++cabal-Version:       >= 1.6+Build-Depends:+   CSPM-CoreLanguage >= 0.1 && < 0.2+  ,base >= 4.0 && < 5.0+  ,containers >= 0.3 && < 0.4+  ,mtl >= 1.1 && < 1.2+  ,QuickCheck >= 2.1 && < 2.2+  ,random >= 1.0 && < 1.1++build-type: Simple+GHC-Options: -funbox-strict-fields -O2 -Wall+Hs-Source-Dirs:         src++Exposed-modules:+  CSPM.FiringRules.Rules+  CSPM.FiringRules.Verifier+  CSPM.FiringRules.EnumerateEvents+  CSPM.FiringRules.FieldConstraints+  CSPM.FiringRules.Trace+  CSPM.FiringRules.Test.Test+  CSPM.FiringRules.HelperClasses+Other-modules:+  CSPM.FiringRules.Test.Mock1+  CSPM.FiringRules.Test.Mock2+  CSPM.FiringRules.Test.Gen

@@ -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.

@@ -0,0 +1,3 @@+#!/usr/bin/env runhaskell+import Distribution.Simple+main = defaultMain

@@ -0,0 +1,238 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  CSPM.FiringRules.EnumerateEvents+-- Copyright   :  (c) Fontaine 2010+-- License     :  BSD+-- +-- Maintainer  :  fontaine@cs.uni-duesseldorf.de+-- Stability   :  experimental+-- Portability :  GHC-only+--+-- Brute-force computation of all possible transitions of a process.+-- Enumerates all events in 'Sigma'.+--+-----------------------------------------------------------------------------++{-# LANGUAGE ScopedTypeVariables #-}+module CSPM.FiringRules.EnumerateEvents+(+  computeTransitions+ ,eventTransitions+ ,tauTransitions+ ,tickTransitions+)+where++import CSPM.CoreLanguage+import CSPM.CoreLanguage.Event+import CSPM.FiringRules.Rules++import Control.Monad+import Control.Applicative+import Data.Either as Either+import Data.List as List++type EnumM a = [a]++-- | Compute all possible transitions (via an event from Sigma) for a Process.+computeTransitions ::  forall i. BL i +  => Sigma i -> Process i -> [Rule i]+computeTransitions events p+  =  (liftM EventRule $ eventTransitions events p)+         `mplus` (liftM TickRule $ tickTransitions p)+         `mplus` (liftM TauRule $ tauTransitions p)++eventTransitions :: forall i.+     BL i+  => Sigma i+  -> Process i +  -> [RuleEvent i]+eventTransitions sigma p = do+  e <- anyEvent ty sigma+  buildRuleEvent e p+  where+    ty = (undefined :: i)++anyEvent :: forall i. BL i => i -> EventSet i -> EnumM (Event i)+anyEvent ty sigma+  = foldr (mplus . return)  mzero $ eventSetToList ty sigma++buildRuleEvent :: forall i. BL i => Event i -> Process i -> EnumM (RuleEvent i)+buildRuleEvent event proc = case proc of+  SwitchedOff p -> rp $ switchOn p+  Prefix p  -> case (prefixNext p event :: Maybe (Process i)) of+    Nothing -> mzero+    Just _ -> return $ HPrefix event p+  ExternalChoice p q+    ->       (ExtChoiceL <$> rp p <*> pure q)+     `mplus` (ExtChoiceR p <$> rp q) +  InternalChoice _ _ -> mzero+  Interleave p q+    ->       (InterleaveL <$> rp p <*> pure q)+     `mplus` (InterleaveR p <$> rp q)+  Interrupt p q -> (NoInterrupt <$> rp p <*> pure q)+     `mplus` (InterruptOccurs p <$> rp q)+  Timeout p q -> TimeoutNo <$> rp p <*> pure q+  Sharing p c q -> if member ty event c+      then Shared c <$> rp p <*> rp q+      else (NotShareL c <$> rp p <*> pure q)+           `mplus` (NotShareR c p <$> rp q)+  Seq p q -> SeqNormal <$> rp p <*> pure q+  AParallel x y p q -> case (member ty event x, member ty event y) of+    (True, True) ->  AParallelBoth x y <$> rp p <*> rp q+    (True, False) -> AParallelL x y <$> rp p <*> pure q+    (False, True) -> AParallelR x y p <$> rp q+    (False,False) -> mzero+  RepAParallel l -> buildRuleRepAParallel event l+  Hide c p -> if member ty event c+      then mzero+      else NotHidden c <$> rp p+  Stop -> mzero+  Skip -> mzero+  Omega -> mzero+  AProcess _n -> mzero+  Renaming rel p -> (do+    e2 <- anyEvent ty (allEvents ty)+    guard $ isInRenaming ty rel e2 event+    rule <- buildRuleEvent e2 p+    return $ Rename rel event rule+    )+    `mplus` (do+       guard $ not $ isInRenamingDomain ty event rel+       RenameNotInDomain rel <$> rp p+       )+  Chaos c -> if member ty event c+    then return $ ChaosEvent c event+    else mzero+  LinkParallel rel p q -> (do+      guard $ not $ isInRenamingDomain ty event rel+      LinkEventL rel <$> rp p <*> pure q+    ) `mplus` (do+      guard $ not $ isInRenamingRange ty event rel+      LinkEventR rel p <$> rp q+    )+  where+    rp = buildRuleEvent event+    ty = (undefined :: i)++buildRuleRepAParallel :: forall i. BL i+  => Event i +  -> [(EventSet i, Process i)] -> EnumM (RuleEvent i)+buildRuleRepAParallel event l = do+  l2 <- mapM parPart l+  if List.null $ Either.rights l2+    then mzero+    else return $ RepAParallelEvent l2+  where+    parPart c@(alpha, p) = if member ty event alpha+      then do+        r <- buildRuleEvent event p+        return $ Right (alpha, r)+      else return $ Left c+    ty = (undefined :: i)++tauTransitions :: forall i. BL i => Process i -> EnumM (RuleTau i)+tauTransitions proc = case proc of+  SwitchedOff p -> tauTransitions $ switchOn p+  Prefix {} -> mzero+  ExternalChoice p q+    ->       (ExtChoiceTauL <$> tauTransitions p <*> pure q)+     `mplus` (ExtChoiceTauR p <$> tauTransitions q)+  InternalChoice p q+    ->       (return $ InternalChoiceL p q)+     `mplus` (return $ InternalChoiceR p q)+  Interleave p q+    ->       (InterleaveTauL <$> tauTransitions p <*> pure q)+     `mplus` (InterleaveTauR p <$> tauTransitions q)+     `mplus` (InterleaveTickL <$> tickTransitions p <*> pure q)+     `mplus` (InterleaveTickR p <$> tickTransitions q)+  Interrupt p q+    ->       (InterruptTauL <$> tauTransitions p <*> pure q)+     `mplus` (InterruptTauR p <$> tauTransitions q)+  Timeout p q+    ->       (TimeoutTauR <$> tauTransitions p <*> pure q)+     `mplus` (return $ TimeoutOccurs p q)+  Sharing p c q+    ->       (ShareTauL c <$> tauTransitions p <*> pure q)+     `mplus` (ShareTauR c p <$> tauTransitions q)+     `mplus` (ShareTickL c <$> tickTransitions p <*> pure q)+     `mplus` (ShareTickR c p <$> tickTransitions q)+  AParallel pc qc p q+    ->       (AParallelTauL pc qc <$> tauTransitions p <*> pure q)+     `mplus` (AParallelTauR pc qc p <$> tauTransitions q)+     `mplus` (AParallelTickL pc qc <$> tickTransitions p <*> pure q)+     `mplus` (AParallelTickR pc qc p <$> tickTransitions q)+  Seq p q+    ->        (SeqTau <$> tauTransitions p <*> pure q)+      `mplus` (SeqTick <$> tickTransitions p <*> pure q)+  Hide hidden p -> (do+    e <- anyEvent ty hidden+    rule <- buildRuleEvent e p+    return $ Hidden hidden rule)+   `mplus` (HideTau hidden <$> tauTransitions p)+  Stop -> mzero+  Skip -> mzero+  Omega -> mzero+  AProcess _n -> mzero+  RepAParallel l -> mzero -- TODO ! tau for replicated AParallel+  Renaming rel p -> RenamingTau rel <$> tauTransitions p+  Chaos c -> return $ ChaosStop c+  LinkParallel rel p q+    ->        (LinkTauL rel <$> tauTransitions p <*> pure q)+      `mplus` (LinkTauR rel p <$> tauTransitions q)+      `mplus` (LinkTickL rel <$> tickTransitions p <*> pure q)+      `mplus` (LinkTickR rel p <$> tickTransitions q)+      `mplus` mkLinkedRules rel p q+  where+    ty = (undefined :: i)++mkLinkedRules :: forall i. BL i+   => RenamingRelation i+   -> Process i+   -> Process i+   -> EnumM (RuleTau i)+mkLinkedRules rel p q = do+  (e1, r1) <- rules1+  (e2, r2) <- rules2+  guard $ isInRenaming ty rel e1 e2+  return $ LinkLinked rel r1 r2+  where+    rules1 :: EnumM (Event i, RuleEvent i)+    rules1 = rules (getRenamingDomain ty rel) p+    rules2 = rules (getRenamingRange ty rel) q+    rules :: [Event i] -> Process i -> EnumM (Event i, RuleEvent i)+    rules s proc = do+      e <- s+      r <- buildRuleEvent e proc+      return (e,r)+    ty = (undefined :: i)++tickTransitions :: BL i => Process i -> EnumM (RuleTick i)+tickTransitions proc = case proc of+  SwitchedOff p -> tickTransitions $ switchOn p+  Prefix {} -> mzero+  ExternalChoice p q+    ->       (ExtChoiceTickL <$> tickTransitions p <*> pure q)+     `mplus` (ExtChoiceTickR p <$> tickTransitions q)+  InternalChoice _p _q -> mzero+  Interleave Omega Omega -> return $ InterleaveOmega+  Interleave _ _ -> mzero+  Interrupt p q -> InterruptTick <$> tickTransitions p <*> pure q+  Timeout p q -> TimeoutTick <$> tickTransitions p <*> pure q+  Sharing Omega c Omega -> return $ ShareOmega c+  Sharing _ _ _ -> mzero+  AParallel c1 c2 Omega Omega -> return $ AParallelOmega c1 c2+  AParallel _ _ _ _ -> mzero+  Seq _p _q -> mzero+  Hide c p -> HiddenTick c <$> tickTransitions p+  Stop -> mzero+  Skip -> return $ SkipTick+  Omega -> mzero+  AProcess _n -> mzero+  RepAParallel l -> if all (isOmega . snd) l+    then return $ RepAParallelOmega $ map fst l+    else mzero+  Renaming rel p -> RenamingTick rel <$> tickTransitions p+  Chaos _ -> mzero+  LinkParallel rel Omega Omega -> return $ LinkParallelTick rel+  LinkParallel _ _ _ -> mzero

@@ -0,0 +1,595 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  CSPM.FiringRules.FieldConstraints+-- Copyright   :  (c) Fontaine 2010+-- License     :  BSD+-- +-- Maintainer  :  fontaine@cs.uni-duesseldorf.de+-- Stability   :  experimental+-- Portability :  GHC-only+--+-- Field-wise generation of transitions.+-- Uses some kind of abstract interpretation/constraint propagation to avoid+-- enumeration of 'Sigma' in some cases.+--+-----------------------------------------------------------------------------++{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE ViewPatterns #-}+module CSPM.FiringRules.FieldConstraints+(+  computeTransitions+ ,eventTransitions+ ,tauTransitions+ ,tickTransitions+)+where++import CSPM.CoreLanguage.Process+import qualified CSPM.CoreLanguage.Event as Event+import CSPM.CoreLanguage.Field as Field+import CSPM.FiringRules.Rules as Rules++import Control.Arrow+import Control.Monad.State+import Control.Applicative+import Data.Maybe+import qualified Data.List as List+++computeTransitions ::  forall i. BF i +  => Event.Sigma i -> Process i -> [Rule i]+computeTransitions events p+  =  (liftM EventRule $ eventTransitions events p)+         `mplus` (liftM TickRule $ tickTransitions p)+         `mplus` (liftM TauRule $ tauTransitions p)++data RuleField i+ = FPrefix (PrefixState i)+ | FExtChoiceL (RuleField i) (Process i)+ | FExtChoiceR (Process i) (RuleField i)+ | FExtChoice (RepExtChoicePart i) (RepExtChoicePart i)+ | FInterleaveL (RuleField i) (Process i)+ | FInterleaveR (Process i) (RuleField i)+ | FSeqNormal (RuleField i) (Process i)+ | FNotHidden (ClosureState i) (RuleField i)+ | FNotShareL (ClosureState i) (RuleField i) (Process i)+ | FNotShareR (ClosureState i) (Process i) (RuleField i)+ | FShared (ClosureState i) (RuleField i) (RuleField i)+ | FAParallelL (ClosureState i) (ClosureState i) (RuleField i) (Process i)+ | FAParallelR (ClosureState i) (ClosureState i) (Process i) (RuleField i)+ | FAParallelBoth (ClosureState i) (ClosureState i) (RuleField i) (RuleField i)+ | FNoInterrupt (RuleField i) (Process i)+ | FInterrupt (Process i) (RuleField i)+ | FTimeout (RuleField i) (Process i)+ | FRepAParallel (RepAP i)+ | FRenaming (Event.RenamingRelation i) (Process i)+ | FChaos (ClosureState i)+ | FLinkEventL (Event.RenamingRelation i) (RuleField i) (Process i)+ | FLinkEventR (Event.RenamingRelation i) (Process i) (RuleField i)+type EnumM a = [a]++rulePattern :: forall i. BF i => Event.EventSet i -> Process i -> EnumM (RuleField i)+rulePattern events proc = case proc of+  SwitchedOff p -> rp $ switchOn p+--  SwitchedOff p -> mzero+  Prefix p -> return $ FPrefix $ prefixStateInit ty p+  ExternalChoice p q+    -> joinRepExtChoiceParts (initRepExtChoicePart events p) (initRepExtChoicePart events q)++--    ->            (FExtChoiceL <$> rp p <*> pure q)+--                 `mplus` (FExtChoiceR p <$> rp q)+  InternalChoice _p _q -> mzero+  Interleave p q+    ->       (FInterleaveL <$> rp p <*> pure q)+     `mplus` (FInterleaveR p <$> rp q)+  Interrupt p q -> (FNoInterrupt <$> rp p <*> pure q)+     `mplus` (FInterrupt p <$> rp q)+  Timeout p q -> FTimeout <$> rp p <*> pure q+  Sharing p c q+    ->       (FShared (initClosure c) <$> rp p <*> rp q)+     `mplus` (FNotShareL (initClosure c) <$> rp p <*> pure q)+     `mplus` (FNotShareR (initClosure c) p <$> rp q)+  AParallel pc qc p q+    ->       (FAParallelL (initClosure pc) (initClosure qc) <$> rp p <*> pure q)+     `mplus` (FAParallelR (initClosure pc) (initClosure qc) <$> pure p <*> rp q)+     `mplus` (FAParallelBoth (initClosure pc) (initClosure qc) <$> rp p <*> rp q)+  Seq p q -> FSeqNormal <$> rp p <*> pure q+  Hide c p -> FNotHidden (initClosure c) <$> rp p+  Stop -> mzero+  Skip -> mzero+  Omega -> mzero+  AProcess _n -> mzero+  RepAParallel l -> return $ FRepAParallel $ initRepAParallel l+  Renaming rel p -> return $ FRenaming rel p+  Chaos c -> return $ FChaos $ initClosure c+  LinkParallel rel p q+    ->         (FLinkEventL rel <$> rp p <*> pure q)+       `mplus` (FLinkEventR rel p <$> rp q)++  where+    ty = (undefined :: i)+    initClosure = closureStateInit ty+    rp = rulePattern events    ++type PropM i a = StateT (FieldSet i) Maybe a++propField :: forall i. BF i => RuleField i -> PropM i ()+propField rule = case rule of+  FPrefix p -> case viewPrefixState ty p of+    FieldOut f -> fixField f+    FieldIn -> return ()+    FieldGuard g -> restrictField $ \e -> intersection ty e g+  FExtChoiceL r _ -> propField r+  FExtChoiceR _ r -> propField r+  FExtChoice _p _q -> return ()+  FInterleaveL r _ -> propField r+  FInterleaveR _ r -> propField r+  FSeqNormal r _ -> propField r+  FNotHidden hidden r -> if closureState hidden == InClosure+    then impossibleRule+    else propField r+  FNotShareL c r _ -> if closureState c == InClosure+    then impossibleRule+    else propField r+  FNotShareR c _ r -> if closureState c == InClosure+    then impossibleRule+    else propField r+  FShared c r1 r2 -> if closureState c == NotInClosure+    then impossibleRule+    else do+      restrictField $ \e -> intersection ty e (closureFields c)+      propField r1+      propField r2+  FAParallelL c1 c2 r _ -> case (closureState c1,closureState c2) of+    (NotInClosure,_) -> impossibleRule+    (_,InClosure) -> impossibleRule+    _ -> do+      restrictField $ \e -> intersection ty e (closureFields c1)+      propField r+  FAParallelR c1 c2 _ r -> case (closureState c1,closureState c2) of+    (_,NotInClosure) -> impossibleRule+    (InClosure,_) -> impossibleRule+    _ -> do+      restrictField $ \e -> intersection ty e (closureFields c2)+      propField r+  FAParallelBoth c1 c2 r1 r2 -> case (closureState c1,closureState c2) of+    (NotInClosure,_) -> impossibleRule+    (_,NotInClosure) -> impossibleRule+    _ -> do+      restrictField $ \e -> intersection ty e (closureFields c1)+      restrictField $ \e -> intersection ty e (closureFields c2)+      propField r1+      propField r2+  FNoInterrupt r _ -> propField r+  FInterrupt _ r -> propField r+  FTimeout r _ -> propField r+  FRepAParallel RepAPFailed -> impossibleRule+  FRepAParallel x -> restrictField $ \e -> intersection ty e (repInitials x)+  FRenaming _ _  -> return () -- todo: some properagtion for renaming +  FChaos c -> restrictField $ \e -> intersection ty e (closureFields c)+  FLinkEventL _ r _ -> propField r+  FLinkEventR _ _ r -> propField r+  where+    restrictField :: (FieldSet i -> FieldSet i) -> PropM i ()+    restrictField fkt = do+      possible <- get+      let restricted = fkt possible+      if Field.null ty restricted+        then impossibleRule+        else put restricted++    fixField :: Field i -> PropM i ()+    fixField e = do+      possible <- get+      if member ty e possible+        then put $ singleton ty e+        else impossibleRule++    impossibleRule :: PropM i ()+    impossibleRule = mzero+    closureState :: ClosureState i -> ClosureView+    closureState = viewClosureState ty+    closureFields :: ClosureState i -> FieldSet i+    closureFields = viewClosureFields ty+    ty = (undefined :: i)++{-+fix one field in the event+-}+nextField :: forall i. BF i => RuleField i -> Field i -> EnumM (RuleField i)+nextField rule field = case rule of+  FPrefix p -> case prefixStateNext ty p field of+    Just a -> return $ FPrefix a+    Nothing -> mzero+  FExtChoiceL r p -> FExtChoiceL <$> rec r <*> pure p+  FExtChoiceR p r -> FExtChoiceR p <$> rec r+  FExtChoice p q+    -> joinRepExtChoiceParts (nextRepExtChoicePart p field) (nextRepExtChoicePart q field)+  FInterleaveL r p -> FInterleaveL <$> rec r <*> pure p+  FInterleaveR p r -> FInterleaveR p <$> rec r+  FSeqNormal r p -> FSeqNormal <$> rec r <*> pure p+  FNotHidden c r -> FNotHidden (fc c) <$> rec r+  FNotShareL c r p -> FNotShareL (fc c) <$> rec r <*> pure p+  FNotShareR c p r -> FNotShareR (fc c) p <$> rec r+  FShared c r1 r2 -> FShared (fc c) <$> rec r1 <*> rec r2+  FAParallelL c1 c2 r q+    -> FAParallelL (fc c1) (fc c2) <$> rec r <*> pure q+  FAParallelR c1 c2 p r+    -> FAParallelR (fc c1) (fc c2) p <$> rec r+  FAParallelBoth c1 c2 r1 r2+    -> FAParallelBoth (fc c1) (fc c2) <$> rec r1 <*> rec r2+  FNoInterrupt r q -> FNoInterrupt <$> rec r <*> pure q+  FInterrupt p r -> FInterrupt p <$> rec r+  FTimeout r q -> FTimeout <$> rec r <*> pure q+  FRepAParallel x -> return $ FRepAParallel $ repNextField field x+  FRenaming rel p -> return $ FRenaming rel p+  FChaos c -> return $ FChaos (fc c)+  FLinkEventL rel r q -> FLinkEventL rel <$> rec r <*> pure q+  FLinkEventR rel p r -> FLinkEventR rel p <$> rec r+  where+    rec r = nextField r field+    ty = (undefined :: i)+    fc c = closureStateNext ty c field++{-+check constraints after last field and+convert RuleField to RuleEvent+we must check all constraints here !+-}+lastField :: forall i. BF i => RuleField i -> Event.Event i -> EnumM (RuleEvent i)+lastField rule event = case rule of+  FPrefix p -> case prefixStateFinalize ty p of+    Nothing -> mzero+    Just x -> return $ HPrefix event x+  FExtChoiceL r p -> ExtChoiceL <$> rec r <*> pure p+  FExtChoiceR p r -> ExtChoiceR p <$> rec r+  FExtChoice (Right (p,rp)) (Right (q,rq)) -> (do+    r <- rp >>= rec+    return $ ExtChoiceL r q)+    `mplus` (do+       r <- rq >>= rec+       return $ ExtChoiceR p r)+  FExtChoice _ _ -> error "unreachable: this case is handled by nextField"+  FInterleaveL r p -> InterleaveL <$> rec r <*> pure p+  FInterleaveR p r -> InterleaveR p <$> rec r+  FSeqNormal r p -> SeqNormal <$> rec r <*> pure p+  FNotHidden hidden r -> do+    guard_not_inClosure hidden+    NotHidden (restoreClosure hidden) <$> rec r+  FNotShareL c r p -> do+    guard_not_inClosure c+    NotShareL (restoreClosure c) <$> rec r <*> pure p+  FNotShareR c p r -> do+    guard_not_inClosure c+    NotShareR (restoreClosure c) p <$> rec r+  FShared c r1 r2 -> do+    guard_inClosure c+    Shared (restoreClosure c) <$> rec r1 <*> rec r2+  FAParallelL c1 c2 r q -> case (inClosure c1,inClosure c2) of+    (True,False) -> AParallelL (restoreClosure c1) (restoreClosure c2) <$> rec r <*> pure q+    _ -> mzero+  FAParallelR c1 c2 p r -> case (inClosure c1,inClosure c2) of+    (False,True) -> AParallelR (restoreClosure c1) (restoreClosure c2) <$> pure p <*> rec r+    _ -> mzero+  FAParallelBoth c1 c2 r1 r2 ->  case (inClosure c1,inClosure c2) of+    (True,True) -> AParallelBoth (restoreClosure c1) (restoreClosure c2) +                    <$> rec r1 <*> rec r2+    _ -> mzero+  FNoInterrupt r q -> NoInterrupt <$> rec r <*> pure q+  FInterrupt p r -> InterruptOccurs p <$> rec r+  FTimeout r q -> TimeoutNo <$> rec r <*> pure q+  FRepAParallel RepAPFailed -> mzero+  FRepAParallel x -> repToRules event x+  FRenaming rel p -> renamingRules rel p event+  FChaos c -> if inClosure c+    then return $ ChaosEvent (restoreClosure c) event+    else mzero+  FLinkEventL rel r q -> do+    guard $ not $ Event.isInRenamingDomain ty event rel+    LinkEventL rel <$> rec r <*> pure q+  FLinkEventR rel p r -> do+    guard $ not $ Event.isInRenamingRange ty event rel+    LinkEventR rel p <$> rec r+  where+    rec r = lastField r event+    ty = (undefined :: i)+    restoreClosure = closureRestore ty+    inClosure = seenPrefixInClosure ty+    guard_inClosure = guard . seenPrefixInClosure ty+    guard_not_inClosure = guard . not . seenPrefixInClosure ty++eventTransitions :: BF i => Event.EventSet i -> Process i -> EnumM (RuleEvent i)+eventTransitions events proc = liftM snd $ computeNextE events proc++computeNextE :: BF i +  => Event.EventSet i -> Process i -> EnumM (Event.Event i, RuleEvent i)+computeNextE events proc = rulePattern events proc >>= runFields events++runFields :: forall i. BF i+  => Event.EventSet i -> RuleField i -> EnumM (Event.Event i, RuleEvent i)+runFields events r = do+{- acctually chanels are allways output fields and they are allways+fixed so there should be no need to enumerate here+also opportunity for optimizations+-}+      let baseEvents = closureStateInit ty events+      (chan,next) <- enumField (viewClosureFields ty baseEvents ) r+      (e,final) <- loopFields+         (closureStateNext ty baseEvents chan) -- the allEvents set(after fixing the channel)+         [chan] -- the accumulator for fields+         next+         (channelLen ty chan -1)+      let event = joinFields ty $ reverse e+      rule <- lastField final event+      return (event,rule)+   where ty = (undefined :: i)++loopFields :: forall i.+  BF i =>+     ClosureState i   -- the universe for events+  -> [Field i]        -- accumulator for fields+  -> RuleField i      -- current rule+  -> Int              -- number fields left in prefix +  -> EnumM ([Field i], RuleField i)+loopFields _ eventAcc rule 0 = return (eventAcc, rule)+loopFields closureState eventAcc rule n = do+      (f,next) <- enumField (viewClosureFields ty closureState) rule+      loopFields +        (closureStateNext ty closureState f)+        (f:eventAcc)+        next+        (n-1)+   where ty = (undefined :: i)++enumField :: forall i. BF i => FieldSet i -> RuleField i -> EnumM (Field i, RuleField i)+enumField top r = case execStateT (propField r) top of+      Just s -> do+        f <- fieldSetToList ty s+        nr <- nextField r f+        return (f ,nr )+      Nothing -> mzero+  where ty = (undefined :: i)++tauTransitions :: forall i. BF i => Process i -> EnumM (RuleTau i)+tauTransitions proc = case proc of+  SwitchedOff p -> tauTransitions $ switchOn p+--  SwitchedOff p -> mzero+--  SwitchedOff p -> return $ TraceSwitchOn $ switchOn p+  Prefix {} -> mzero+  ExternalChoice p q+    ->       (ExtChoiceTauL <$> tauTransitions p <*> pure q)+     `mplus` (ExtChoiceTauR p <$> tauTransitions q)+  InternalChoice p q+    ->       (return $ InternalChoiceL p q)+     `mplus` (return $ InternalChoiceR p q)+  Interleave p q+    ->       (InterleaveTauL <$> tauTransitions p <*> pure q)+     `mplus` (InterleaveTauR p <$> tauTransitions q)+     `mplus` (InterleaveTickL <$> tickTransitions p <*> pure q)+     `mplus` (InterleaveTickR p <$> tickTransitions q)+  Interrupt p q+    ->       (InterruptTauL <$> tauTransitions p <*> pure q)+     `mplus` (InterruptTauR p <$> tauTransitions q)+  Timeout p q+    ->       (TimeoutTauR <$> tauTransitions p <*> pure q)+     `mplus` (return $ TimeoutOccurs p q)+  Sharing p c q+    ->       (ShareTauL c <$> tauTransitions p <*> pure q)+     `mplus` (ShareTauR c p <$> tauTransitions q)+     `mplus` (ShareTickL c <$> tickTransitions p <*> pure q)+     `mplus` (ShareTickR c p <$> tickTransitions q)+  AParallel pc qc p q+    ->       (AParallelTauL pc qc <$> tauTransitions p <*> pure q)+     `mplus` (AParallelTauR pc qc p <$> tauTransitions q)+     `mplus` (AParallelTickL pc qc <$> tickTransitions p <*> pure q)+     `mplus` (AParallelTickR pc qc p <$> tickTransitions q)+  Seq p q+    ->        (SeqTau <$> tauTransitions p <*> pure q)+      `mplus` (SeqTick <$> tickTransitions p <*> pure q)+  Hide hidden p -> (do+    rule <- (eventTransitions hidden p)+    return $ Hidden hidden rule)+   `mplus` (HideTau hidden <$> tauTransitions p)+  Stop -> mzero+  Skip -> mzero+  Omega -> mzero+  AProcess _n -> mzero+  RepAParallel _ -> mzero -- TODO ! tau for replicated AParallel+  Renaming rel p -> RenamingTau rel <$> tauTransitions p+  Chaos c -> return $ ChaosStop c+  LinkParallel rel p q+    ->        (LinkTauL rel <$> tauTransitions p <*> pure q)+      `mplus` (LinkTauR rel p <$> tauTransitions q)+      `mplus` (LinkTickL rel <$> tickTransitions p <*> pure q)+      `mplus` (LinkTickR rel p <$> tickTransitions q)+      `mplus` mkLinkedRules rel p q++tickTransitions :: BL i => Process i -> EnumM (RuleTick i)+tickTransitions proc = case proc of+  SwitchedOff p -> tickTransitions $ switchOn p+  Prefix {} -> mzero+  ExternalChoice p q+    ->       (ExtChoiceTickL <$> tickTransitions p <*> pure q)+     `mplus` (ExtChoiceTickR p <$> tickTransitions q)+  InternalChoice _p _q -> mzero+  Interleave Omega Omega -> return $ InterleaveOmega+  Interleave _ _ -> mzero+  Interrupt p q -> InterruptTick <$> tickTransitions p <*> pure q+  Timeout p q -> TimeoutTick <$> tickTransitions p <*> pure q+  Sharing Omega c Omega -> return $ ShareOmega c+  Sharing _ _ _ -> mzero+  AParallel c1 c2 Omega Omega -> return $ AParallelOmega c1 c2+  AParallel _ _ _ _ -> mzero+  RepAParallel l -> if all (isOmega . snd) l+    then return $ RepAParallelOmega $ map fst l+    else mzero+  Seq _p _q -> mzero+  Hide c p -> HiddenTick c <$> tickTransitions p+  Stop -> mzero+  Skip -> return $ SkipTick+  Omega -> mzero+  AProcess _n -> mzero+  Renaming rel p -> RenamingTick rel <$> tickTransitions p+  Chaos _ -> mzero+  LinkParallel rel Omega Omega -> return $ LinkParallelTick rel+  LinkParallel _ _ _ -> mzero++type RepAPProc i = (ClosureState i, Process i, [([Field.Field i], RuleEvent i)])+                                     -- why not do this field wise ^+data RepAP i+  = RepAP {+      repInitials :: FieldSet i+     ,repProcs :: [RepAPProc i]+     }+  | RepAPFailed++instance Show (RepAP i) where show _ = "RepAP"++initRepAParallel :: forall i. BF i+  => [(Event.EventSet i, Process i)]+  -> RepAP i+initRepAParallel l = RepAP {+   repInitials = joinInitials ln+  ,repProcs = ln+  }+  where+    ty = (undefined :: i)+    ln = map mkLn l+    mkLn :: (Event.EventSet i, Process i) -> RepAPProc i+    mkLn (closure,p)+      = (closureStateInit ty closure+        ,p+        ,map (first (splitFields ty)) $ computeNextE closure p)    ++joinInitials :: forall i. BF i+  => [RepAPProc i]+  -> FieldSet i+joinInitials l= fieldSetFromList ty $ concatMap jf l where+  jf (_,_,a) = mapMaybe il a+  il ([],_) = Nothing+  il (h:_,_) = Just h+  ty = (undefined :: i)++repNextField :: forall i. BF i+  => Field i -> RepAP i -> RepAP i+repNextField _ RepAPFailed = RepAPFailed+repNextField field x = RepAP {+   repInitials = joinInitials newProcs+  ,repProcs = newProcs+  }+  where+    ty = (undefined :: i)+    newProcs :: [RepAPProc i]+    newProcs = map filterRules $ repProcs x+    filterRules :: RepAPProc i -> RepAPProc i+    filterRules (closure, p, rules) +      = (closureStateNext ty closure field, p, mapMaybe nextR rules )+    nextR ([], _r) = Nothing+    nextR (h:t, r) | fieldEq ty field h = Just (t,r)+    nextR _ = Nothing++repToRules :: forall i. BF i +  => Event.Event i+  -> RepAP i +  -> EnumM (RuleEvent i)+repToRules event ra = do+  parts <- mapM mkPart $ repProcs ra+  if all isLeft parts+    then mzero+    else return $ RepAParallelEvent parts+  where+    mkPart :: (ClosureState i, Process i, [([Field.Field i], RuleEvent i)])+      -> EnumM (EventRepAPart i)+    mkPart (closure, origProc, []) = do+      guard (not $ inClosure closure)+      return $ Left (restoreClosure closure, origProc)+    mkPart (closure, _origProc, (map snd -> rules)) = do+      r <- rules+      return $ Right (restoreClosure closure, r)+    restoreClosure = closureRestore ty+    inClosure = seenPrefixInClosure ty   +    ty = (undefined :: i)+    isLeft (Left _) = True+    isLeft _ = False++{-+  todo : special cases for injective and relational renamings+-}    +renamingRules :: forall i. BF i+  => Event.RenamingRelation i+  -> Process i+  -> Event.Event i+  -> EnumM (RuleEvent i)+renamingRules rel proc event = do+    fromEvent <- Event.preImageRenaming ty rel event+    rule <- eventTransitions (Event.singleEventToClosureSet ty fromEvent) proc+    return $ Rename rel event rule    +  `mplus` (do+    guard $ not $ Event.isInRenamingDomain ty event rel+    -- here we could callback on enumNext !+    rule <- eventTransitions (Event.singleEventToClosureSet ty event) proc+    return $ RenameNotInDomain rel rule)+  where+    ty = (undefined :: i)++{-+we just enumerate everything+very inefficient !+-}+mkLinkedRules :: forall i. BF i+   => Event.RenamingRelation i+   -> Process i+   -> Process i+   -> EnumM (RuleTau i)+mkLinkedRules rel p q = do+  (e1, r1) <- rules1+  (e2, r2) <- rules2+  guard $ Event.isInRenaming ty rel e1 e2+  return $ LinkLinked rel r1 r2+  where+    rules1 :: EnumM (Event.Event i, RuleEvent i)+    rules1 = rules (Event.getRenamingDomain ty rel) p+    rules2 = rules (Event.getRenamingRange ty rel) q+    rules :: [Event.Event i] -> Process i -> EnumM (Event.Event i, RuleEvent i)+    rules s proc = do+      e <- s+      -- use EnumNext instead!+      computeNextE (Event.singleEventToClosureSet ty e) proc+    ty = (undefined :: i)+++type RepExtChoicePart i = Either (Process i) (Process i,[RuleField i])++initRepExtChoicePart :: forall i. BF i+  => Event.EventSet i -> Process i -> RepExtChoicePart i+initRepExtChoicePart events p+  = if List.null rules+    then Left p+    else Right (p,rules)+  where rules = rulePattern events p++{-+nextRepExtChoicePart may call nextField with invalid fields+nextRepExtChoicePart is only an approximation, it might return invalid rules+-}+nextRepExtChoicePart :: forall i. BF i+  => RepExtChoicePart i -> Field i -> RepExtChoicePart i+nextRepExtChoicePart (Left p) _ = (Left p)+nextRepExtChoicePart (Right (p,rules)) field+{-+this is an error, we cannot rely on nextField to check the constraints+nextField might return invalid rules+-}+  = if List.null newRules+    then Left p+    else Right (p,newRules)+  where newRules = concatMap (flip nextField field) rules++joinRepExtChoiceParts :: forall i. BF i+  => RepExtChoicePart i -> RepExtChoicePart i -> EnumM (RuleField i)+joinRepExtChoiceParts l r = case (l,r) of+  (Left _,Left _) -> mzero+  (Right (_,rules), Left q) -> FExtChoiceL <$> rules <*> pure q+  (Left p, Right (_,rules)) -> FExtChoiceR p <$> rules+  (Right _,Right _) -> return $ FExtChoice l r

@@ -0,0 +1,40 @@+{-# LANGUAGE FlexibleContexts, TypeFamilies #-}+-----------------------------------------------------------------------------+-- |+-- Module      :  CSPM.FiringRules.HelperClasses+-- Copyright   :  (c) Fontaine 2010+-- License     :  BSD+-- +-- Maintainer  :  fontaine@cs.uni-duesseldorf.de+-- Stability   :  experimental+-- Portability :  GHC-only+--+-- Some helper classes.+-- (Might be deleted or moved somewhere else some time.)+--+-----------------------------------------------------------------------------++module CSPM.FiringRules.HelperClasses+where++import CSPM.CoreLanguage+import CSPM.FiringRules.Rules++-- | Implementation i supports 'Eq' and 'Ord'.+class+  (Eq (Process i), Eq (RuleTick i), Eq (RuleTau i), Eq (RuleEvent i)+  ,Ord (Process i), Ord (RuleTick i), Ord (RuleTau i) ,Ord (RuleEvent i))+  => EqOrd i++-- | Implementation i supports 'Show'.+class+  (Show (TTE i), Show (Rule i), Show (Process i), Show (RuleTick i)+  , Show (RuleTau i), Show (RuleEvent i))+  => FShow i++-- | 'CSP1' means that implementation i supports the base language.+class (EqOrd i,BL i) => CSP1 i++-- | 'CSP2' means that implementation i supports the base language and multi-field events.+class (EqOrd i,BF i,CSP1 i) => CSP2 i+

@@ -0,0 +1,172 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  CSPM.FiringRules.Rules+-- Copyright   :  (c) Fontaine 2010+-- License     :  BSD+-- +-- Maintainer  :  fontaine@cs.uni-duesseldorf.de+-- Stability   :  experimental+-- Portability :  GHC-only+--+-- This modules defines data types for (CSP) proof trees.+-- A proof trees show that a particular transition is valid+-- with respect to the firing rules semantics.+--+-- (For more info on the firing rule semantics +-- see: The Theory and Practice of Concurrency A.W. Roscoe 1999.)+-- +-- We use three separate data types for tau rules, tick rules and regular rules.+--+-- There is a one-to-one correspondence between each constructor of the data types+-- 'RuleTau', 'RuleTick', 'RuleEvent' and one fireing rule.+--+-- A list of the implemented firing rules (as pdf) is available via the package maintainer or+-- the web page.+--+-----------------------------------------------------------------------------++{-# LANGUAGE FlexibleContexts, StandaloneDeriving, UndecidableInstances #-}+module CSPM.FiringRules.Rules where++import CSPM.CoreLanguage++-- | A sum-type for tau, tick and regular rules.+data Rule i+  = TauRule (RuleTau i)+  | TickRule (RuleTick i)+  | EventRule (RuleEvent i)++isTauRule :: Rule i -> Bool+isTauRule (TauRule {}) = True+isTauRule _ = False++data RuleTau i+  = Hidden (EventSet i) (RuleEvent i)+  | HideTau (EventSet i) (RuleTau i)+  | SeqTau (RuleTau i) (Process i)+  | SeqTick (RuleTick i) (Process i)+  | InternalChoiceL (Process i) (Process i)+  | InternalChoiceR (Process i) (Process i)+  | ChaosStop (EventSet i)+  | TimeoutOccurs (Process i) (Process i)+  | TimeoutTauR (RuleTau i) (Process i)+  | ExtChoiceTauL (RuleTau i) (Process i)+  | ExtChoiceTauR (Process i) (RuleTau i)+  | InterleaveTauL (RuleTau i) (Process i)+  | InterleaveTauR (Process i) (RuleTau i)+  | InterleaveTickL (RuleTick i) (Process i)+  | InterleaveTickR (Process i) (RuleTick i)+  | ShareTauL (EventSet i) (RuleTau i) (Process i)+  | ShareTauR (EventSet i) (Process i) (RuleTau i)+  | ShareTickL (EventSet i) (RuleTick i) (Process i)+  | ShareTickR (EventSet i) (Process i) (RuleTick i)+  | AParallelTauL (EventSet i) (EventSet i) (RuleTau i) (Process i)+  | AParallelTauR (EventSet i) (EventSet i) (Process i) (RuleTau i)+  | AParallelTickL (EventSet i) (EventSet i) (RuleTick i) (Process i)+  | AParallelTickR (EventSet i) (EventSet i) (Process i) (RuleTick i)+  | InterruptTauL (RuleTau i) (Process i)+  | InterruptTauR (Process i) (RuleTau i)+  | TauRepAParallel [Either (EventSet i,Process i) (EventSet i,RuleTau i)]+  | RenamingTau (RenamingRelation i) (RuleTau i)+  | LinkLinked (RenamingRelation i) (RuleEvent i) (RuleEvent i)+  | LinkTauL (RenamingRelation i) (RuleTau i) (Process i)+  | LinkTauR (RenamingRelation i) (Process i) (RuleTau i)+  | LinkTickL (RenamingRelation i) (RuleTick i) (Process i)+  | LinkTickR (RenamingRelation i)  (Process i) (RuleTick i)+  | TraceSwitchOn (Process i) -- pseudo-tau for debugging++data RuleTick i+  = SkipTick+  | HiddenTick (EventSet i) (RuleTick i)+  | InterruptTick (RuleTick i) (Process i)+  | TimeoutTick (RuleTick i) (Process i)+  | ShareOmega (EventSet i)+  | AParallelOmega (EventSet i) (EventSet i)+  | RepAParallelOmega [EventSet i]+  | InterleaveOmega+  | ExtChoiceTickL (RuleTick i) (Process i)+  | ExtChoiceTickR (Process i) (RuleTick i)+  | RenamingTick (RenamingRelation i) (RuleTick i)+  | LinkParallelTick (RenamingRelation i)++data RuleEvent i+  = HPrefix (Event i) (Prefix i)+  | ExtChoiceL (RuleEvent i) (Process i)+  | ExtChoiceR (Process i) (RuleEvent i)+  | InterleaveL (RuleEvent i) (Process i)+  | InterleaveR (Process i) (RuleEvent i)+  | SeqNormal (RuleEvent i) (Process i)+  | NotHidden (EventSet i) (RuleEvent i)+  | NotShareL (EventSet i) (RuleEvent i) (Process i)+  | NotShareR (EventSet i) (Process i) (RuleEvent i)+  | Shared (EventSet i) (RuleEvent i) (RuleEvent i)+  | AParallelL (EventSet i) (EventSet i) (RuleEvent i) (Process i)+  | AParallelR (EventSet i) (EventSet i) (Process i) (RuleEvent i)+  | AParallelBoth (EventSet i) (EventSet i) (RuleEvent i) (RuleEvent i)+  | RepAParallelEvent [EventRepAPart i]+  | NoInterrupt (RuleEvent i) (Process i)+  | InterruptOccurs (Process i) (RuleEvent i)+  | TimeoutNo (RuleEvent i) (Process i)+  | Rename (RenamingRelation i) (Event i) (RuleEvent i)+-- todo make special cases for Rename injective and rename relational+  | RenameNotInDomain (RenamingRelation i) (RuleEvent i)+  | ChaosEvent (EventSet i) (Event i)+  | LinkEventL (RenamingRelation i) (RuleEvent i) (Process i)+  | LinkEventR (RenamingRelation i) (Process i) (RuleEvent i)++type EventRepAPart i+  = Either (EventSet i, Process i) (EventSet i, RuleEvent i)++{-+Not sure about this.+Maybe this moves somewhere else or should be implemented differently.+This somehow complicated by the use of type-families +-}+deriving instance+  (Show (Event i), Show (Prefix i), Show (Process i), Show (ExtProcess i)+  ,Show (EventSet i), Show (RenamingRelation i))+  => Show (RuleEvent i)+deriving instance+  (Eq (Event i), Eq (Prefix i), Eq (Process i), Eq (ExtProcess i), Eq (EventSet i)+  ,Eq (RenamingRelation i) )+  => Eq (RuleEvent i)+deriving instance+  (Ord (Event i), Ord (Prefix i), Ord (Process i), Ord (ExtProcess i), Ord (EventSet i)+  ,Ord (RenamingRelation i) )+  => Ord (RuleEvent i)+++deriving instance+  (Show (Process i), Show (EventSet i), Show (Prefix i), Show (ExtProcess i)+  ,Show (RenamingRelation i))+  => Show (RuleTick i)+deriving instance+  (Eq (Process i), Eq (EventSet i), Eq (Prefix i), Eq (ExtProcess i)+  ,Eq (RenamingRelation i))+  => Eq (RuleTick i)+deriving instance+  (Ord (Process i), Ord (EventSet i), Ord (Prefix i), Ord (ExtProcess i)+  ,Ord (RenamingRelation i))+   => Ord (RuleTick i)+++deriving instance+  (Show (RuleEvent i), Show (RuleTick i), Show (Process i)+  ,Show (EventSet i), Show (RenamingRelation i))+  => Show (RuleTau i)+deriving instance+  (Eq (RuleEvent i), Eq (RuleTick i), Eq (Process i)+  ,Eq (EventSet i), Eq (RenamingRelation i))+  => Eq (RuleTau i)+deriving instance+  (Ord (RuleEvent i), Ord (RuleTick i), Ord (Process i), Ord (EventSet i)+  ,Ord (ExtProcess i), Ord (Prefix i), Ord (Event i),Ord (RenamingRelation i) )+  => Ord (RuleTau i)++deriving instance+  (Show (RuleEvent i), Show (RuleTick i), Show (RuleTau i))+  => Show (Rule i)++deriving instance+  (Eq (RuleEvent i), Eq (RuleTick i), Eq (RuleTau i))+  => Eq (Rule i)

@@ -0,0 +1,237 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  CSPM.CoreLanguage.FiringRules.Gen+-- Copyright   :  (c) Fontaine 2010+-- License     :  BSD+-- +-- Maintainer  :  fontaine@cs.uni-duesseldorf.de+-- Stability   :  experimental+-- Portability :  GHC-only+--+-- Generation of arbitrary processes and proof trees for QuickCheck-testing.+--+-----------------------------------------------------------------------------++{-# LANGUAGE FlexibleInstances,TypeSynonymInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}+module CSPM.FiringRules.Test.Gen where++import CSPM.CoreLanguage+import CSPM.CoreLanguage.Event+import CSPM.FiringRules.Rules++import Test.QuickCheck.Arbitrary+import Test.QuickCheck.Gen+import Control.Monad+import Control.Applicative+import qualified Data.List as List++class (BL i) => Arb i where+  genPrefix :: i -> Event i -> Gen (Prefix i)+  arbitraryEvent :: i -> Gen (Event i)+  arbitraryEventSet :: i -> Gen (EventSet i)+  arbitraryRenaming :: i -> Gen (RenamingRelation i)+  arbitraryRenaming ty = liftM (renamingFromList ty) $ arbitraryRenamingDR ty e e+    where e = allEvents ty+  arbitraryRenamingDR :: i -> EventSet i -> EventSet i -> Gen [(Event i, Event i)]+  arbitraryRenamingDR ty domain range+    = listOf1 $ liftM2 (,)+        (elements $ eventSetToList ty domain)+        (elements $ eventSetToList ty range)++mkArb :: Arbitrary a => (a -> t) -> Gen t+mkArb f = fmap f arbitrary++mkArb2 :: (Arbitrary a,Arbitrary b) => (a -> b -> t) -> Gen t+mkArb2 f = liftM2 f arbitrary arbitrary++mkArb3 ::+  (Arbitrary a, Arbitrary b, Arbitrary c) => +  (a -> b -> c-> t) -> Gen t+mkArb3 f = liftM3 f arbitrary arbitrary arbitrary++instance Arb i => Arbitrary (Process i) where arbitrary = sized genProcess++arbitraryPrefix :: forall i. Arb i => i -> Gen (Prefix i)+arbitraryPrefix i = do+  arbitraryEvent i >>= genPrefix i++genProcess :: forall i. Arb i => Int -> Gen (Process i)+genProcess 0 = elements $ [Stop,Skip,Omega] ++ atomicProcesses+  where atomicProcesses = map AProcess [1..5]+genProcess n = frequency [+   (10, liftM Prefix $ arbitraryPrefix ty)+  ,(10, binProc ExternalChoice)+  ,(10, binProc InternalChoice)+  ,(10, binProc Interleave)+  ,(10, binProc Interrupt)+  ,(10, liftM3 Sharing subProcess (arbitraryEventSet ty) subProcess)+  ,(10, binProc Seq)+  ,(10, liftM2 Hide (arbitraryEventSet ty) arbitrary)+  ,(30, genProcess 0)+  ]+  where+    binProc c = liftM2 c subProcess subProcess+    subProcess = resize (n `div` 2) arbitrary+    ty = (undefined :: i)++instance Arb i => Arbitrary (RuleEvent i) where arbitrary = arbitraryRE++arbitraryRE :: forall i. Arb i => Gen (RuleEvent i)+arbitraryRE = sized $ \size -> do+    arbitraryEvent (undefined :: i) >>= genRule size++instance Arb i => Arbitrary (RuleTau i) where+  arbitrary = sized genRuleTau++genRuleTau :: forall i. Arb i => Int -> Gen (RuleTau i)+genRuleTau 0 = oneof [ mkArb2 InternalChoiceL, mkArb2 InternalChoiceR ]+genRuleTau n = frequency [+     f10 $ do+        h <- arbSet+        hiddenEvent <- elements $ (eventSetToList ty) (allEvents ty)+        r <- genRule n hiddenEvent+        return $ Hidden (insert ty hiddenEvent h) r+    ,f10 $ ExtChoiceTauL <$> subRule <*> p+    ,f10 $ ExtChoiceTauR <$> p <*> subRule+    ,f10 $ SeqTick <$> subRuleTick <*> p+    ,f10 $ SeqTau <$> subRule <*> p+    ,f10 $ ShareTauL <$> arbSet <*> subRule <*> p+    ,f10 $ ShareTauR <$> arbSet <*> p <*> subRule+    ,f10 $ ShareTickL <$> arbSet <*> subRuleTick <*> p+    ,f10 $ ShareTickR <$> arbSet <*> p <*> subRuleTick+    ,f10 $ AParallelTauL <$> arbSet <*> arbSet <*> subRule <*> p+    ,f10 $ AParallelTauR <$> arbSet <*> arbSet <*> p <*> subRule+    ,f10 $ AParallelTickL <$> arbSet <*> arbSet <*> subRuleTick <*> p+    ,f10 $ AParallelTickR <$> arbSet <*> arbSet <*> p <*> subRuleTick+    ,f10 $ InterleaveTauL <$> subRule <*> p+    ,f10 $ InterleaveTauR <$> p <*> subRule+    ,f10 $ InterleaveTickL <$> subRuleTick <*> p+    ,f10 $ InterleaveTickR <$> p <*> subRuleTick+    ,f10 $ InterruptTauL <$> subRule <*> p+    ,f10 $ InterruptTauR <$> p <*> subRule+    ,f10 $ TimeoutTauR <$> subRule <*> p+    ,f10 $ TimeoutOccurs <$> p <*> p+    ,f10 $ ChaosStop <$> arbSet+    ,f10 $ LinkTauL <$> arbitraryRenaming ty <*> subRule <*> p+    ,f10 $ LinkTauR <$> arbitraryRenaming ty <*> p <*> subRule+    ,f10 $ LinkTickL <$> arbitraryRenaming ty <*> subRuleTick <*> p+    ,f10 $ LinkTickR <$> arbitraryRenaming ty <*> p <*> subRuleTick+    ,f10 $ do+       rel <- arbitraryRenaming ty+       (e1,e2) <- elements (renamingToList ty rel)+       LinkLinked rel <$> subRuleEvent e1 <*> subRuleEvent e2+    ]+  where+    subRule :: Gen (RuleTau i)+    subRule = genRuleTau $ n `div` 2+    subRuleTick :: Gen (RuleTick i)+    subRuleTick = genRuleTick $ n `div` 2+    subRuleEvent :: Event i -> Gen (RuleEvent i)+    subRuleEvent e = genRule (n `div` 2) e+    ty = (undefined :: i)+    p :: Gen (Process i)+    p = arbitrary+    f10 x = (10,x)+    arbSet = arbitraryEventSet ty++instance Arb i => Arbitrary (RuleTick i) where+  arbitrary = sized genRuleTick++genRuleTick :: forall i. Arb i => Int -> Gen (RuleTick i)+genRuleTick 0 = oneof+  [ liftM ShareOmega $ arbitraryEventSet (undefined :: i)+  , return InterleaveOmega ]++genRuleTick n = frequency [+     f10 $ return SkipTick+    ,f10 $ HiddenTick <$> arbSet <*> r+    ,f10 $ ShareOmega <$> arbSet+    ,f10 $ return InterleaveOmega+    ,f10 $ ExtChoiceTickL <$> r <*> p+    ,f10 $ ExtChoiceTickR <$> p <*> r+    ,f10 $ InterruptTick <$> r <*> p+    ,f10 $ TimeoutTick <$> r <*> p+    ,f10 $ RenamingTick <$> arbitraryRenaming ty <*> r+    ,f10 $ LinkParallelTick <$> arbitraryRenaming ty+    ,f10 $ AParallelOmega <$> arbSet <*> arbSet+    ,f10 $ RepAParallelOmega <$> (resize 4 $ listOf1 arbSet)+    ]+  where+    r :: Gen (RuleTick i)+    r = genRuleTick $ n `div` 2+    p :: Gen (Process i)+    p = arbitrary++    f10 x = (10,x)+    arbSet = arbitraryEventSet ty+    ty = (undefined :: i)++genRule :: forall i. Arb i => Int -> Event i -> Gen (RuleEvent i)+genRule 0 event = HPrefix event <$> genPrefix (undefined :: i) event+genRule n event = frequency [+     f10 $ ExtChoiceL <$> r <*> p+    ,f10 $ ExtChoiceR <$> p <*> r+    ,f10 $ InterleaveL <$> r <*> p+    ,f10 $ InterleaveR <$> p <*> r+    ,f10 $ SeqNormal <$> r <*> p+    ,f10 $ NotHidden <$> setWithoutEvent <*> genRule n event+    ,f10 $ NotShareL <$> setWithoutEvent <*> r <*> p+    ,f10 $ NotShareR <$> setWithoutEvent <*> p <*> r+    ,f10 $ Shared <$> setWithEvent <*> r <*> r+    ,f10 $ ChaosEvent <$> setWithEvent <*> pure event+    ,f10 $ AParallelL <$> setWithEvent <*> setWithoutEvent <*> r <*> p+    ,f10 $ AParallelR <$> setWithoutEvent <*> setWithEvent <*> p <*> r+    ,f10 $ AParallelBoth <$> setWithEvent <*> setWithEvent <*> r <*> r+    ,f10 $ arbitraryRepAParallelEvent+    ,f10 $ NoInterrupt <$> r <*> p+    ,f10 $ InterruptOccurs <$> p <*> r+    ,f10 $ TimeoutNo <$> r <*> p+    ,f10 $ do+       t <- arbitraryRenamingDR ty (allEvents ty) (allEvents ty)+       newEvent <- arbitraryEvent ty+       let rel = renamingFromList ty ((newEvent, event) : t)+       Rename rel event <$> genRule (n `div` 2) newEvent+    ,f10 $ do+       rel <- arbitraryRenamingDR ty+         (delete ty event (allEvents ty))+         (allEvents ty)+       RenameNotInDomain (renamingFromList ty rel) <$> r+    ,(30, genRule 0 event)+    ,f10 $ do+       rel <- arbitraryRenamingDR ty+         (delete ty event (allEvents ty))+         (allEvents ty)+       LinkEventL (renamingFromList ty rel) <$> r <*> p+    ,f10 $ do+       rel <- arbitraryRenamingDR ty+         (allEvents ty)+         (delete ty event (allEvents ty))+       LinkEventR (renamingFromList ty rel) <$> p <*> r+    ]+  where+    p :: Gen (Process i)+    p = arbitrary+    r :: Gen (RuleEvent i)+    r = genRule (n `div` 2) event++    f10 x = (10,x)+    arbSet = arbitraryEventSet ty+    setWithEvent :: Gen (EventSet i)+    setWithEvent = do+      x <- arbSet+      return $ insert ty event x+    setWithoutEvent :: Gen (EventSet i)+    setWithoutEvent = do+      x <- arbSet+      return $ delete ty event x+    ty = (undefined :: i)++    arbitraryRepAParallelEvent :: Gen (RuleEvent i)+    arbitraryRepAParallelEvent = do+      flags <- (resize 4 $ listOf1 arbitrary) -- hardcoded max 4 processes+            `suchThat` List.or+      RepAParallelEvent <$> mapM repAPart flags+    repAPart :: Bool -> Gen (EventRepAPart i)+    repAPart True  = Right <$> liftM2 (,) setWithEvent r+    repAPart False = Left <$> liftM2 (,) setWithoutEvent p

@@ -0,0 +1,103 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  CSPM.FiringRules.Test.Mock1+-- Copyright   :  (c) Fontaine 2010+-- License     :  BSD+-- +-- Maintainer  :  fontaine@cs.uni-duesseldorf.de+-- Stability   :  experimental+-- Portability :  GHC-only+--+-- A mock implementation of CSP-Processes.+--+-----------------------------------------------------------------------------++{-# LANGUAGE EmptyDataDecls, TypeFamilies #-}+{-# LANGUAGE StandaloneDeriving, FlexibleInstances #-} ++module CSPM.FiringRules.Test.Mock1+where++import CSPM.CoreLanguage+import CSPM.CoreLanguage.Event++import CSPM.FiringRules.Test.Gen+import CSPM.FiringRules.HelperClasses++import Data.Set (Set)+import qualified Data.Set as Set+import Data.Map (Map)+import qualified Data.Map as Map+import qualified Data.List as List+import Test.QuickCheck.Arbitrary+import Test.QuickCheck.Gen+import Control.Monad+import Control.Applicative++data M1++m1 :: M1+m1 = undefined++type instance Prefix M1 = PrefixM1 +data PrefixM1 = PrefixM1 (Map Int (Process M1))+  deriving (Show,Eq,Ord)++type instance ExtProcess M1 = Process M1++deriving instance Show (Process M1)+deriving instance Eq (Process M1)+deriving instance Ord (Process M1)++instance EqOrd M1+instance CSP1 M1+++type instance Event M1 = Int+type instance EventSet M1 = Set Int+type instance RenamingRelation M1 = Set (Int,Int)++instance BE M1 where+  eventEq _ty = (==)+  member _ty = Set.member+  intersection _ty = Set.intersection+  difference _ty = Set.difference +  union = error "BE M1 union undefined"+  null _ty = Set.null+  singleton _ty = Set.singleton+  insert _ty = Set.insert+  delete _ty = Set.delete+  eventSetToList _ty = Set.toList+  allEvents _ty = Set.fromList [1..5]+  isInRenaming _ty rel a b = (a,b) `Set.member` rel+  imageRenaming _ty rel e = Set.toList $ Set.map snd $ Set.filter ((==) e . fst) rel+  preImageRenaming _ty rel e = Set.toList $  Set.map fst $ Set.filter ((==) e . snd) rel+  isInRenamingDomain _ty e rel = any ((==) e . fst) $ Set.toList rel+  isInRenamingRange _ty e rel = any ((==) e . snd) $ Set.toList rel+  getRenamingDomain _ty = Set.toList . Set.map fst+  getRenamingRange _ty = Set.toList . Set.map snd+  renamingFromList _ty = Set.fromList+  renamingToList _ty = Set.toList+  singleEventToClosureSet = error "BE M1 singleEventToClosureSet undefined (Mock1)"+++instance BL M1 where+  switchOn = id+  prefixNext (PrefixM1 m) e = Map.lookup e m++instance Arb M1 where+  genPrefix _ty = genPrefixM1+  arbitraryEvent _ty = elements $ eventSetToList m1 $ allEvents m1+  arbitraryEventSet _ty = arbitraryEventSetM1++arbitraryEventSetM1 :: Gen (EventSet M1)+arbitraryEventSetM1 = elements $ map Set.fromList+    $ List.subsequences $ eventSetToList m1 $ allEvents m1++genPrefixM1 :: Event M1 -> Gen (Prefix M1)+genPrefixM1 event = do+  proc <- arbitrary+  transCount <- elements [1..5]+  extraTransitions <- replicateM transCount+    ((,) <$> arbitraryEvent m1 <*> arbitrary)+  return $ PrefixM1 $ Map.fromList ((event,proc) : extraTransitions)

@@ -0,0 +1,251 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  CSPM.CoreLanguage.FiringRules.Mock2+-- Copyright   :  (c) Fontaine 2010+-- License     :  BSD+-- +-- Maintainer  :  fontaine@cs.uni-duesseldorf.de+-- Stability   :  experimental+-- Portability :  GHC-only+--+-- A mock implementation of CSP-Processes.+--+-----------------------------------------------------------------------------++{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE EmptyDataDecls, TypeFamilies #-}+{-# LANGUAGE StandaloneDeriving, FlexibleInstances, FlexibleContexts,TypeSynonymInstances #-}+module CSPM.FiringRules.Test.Mock2+where++import CSPM.CoreLanguage+import CSPM.CoreLanguage.Event as Event+import CSPM.CoreLanguage.Field as Field++import CSPM.FiringRules.Test.Gen+import CSPM.FiringRules.HelperClasses++import Test.QuickCheck.Arbitrary+import Test.QuickCheck.Gen+import Data.Set (Set)+import qualified Data.Set as Set+import qualified Data.List as List+import Control.Monad+import Control.Applicative++data M2+m2 :: M2+m2 = undefined++type ProcessM2 = Process M2+type ClosureViewM2 = ClosureView++instance EqOrd M2+instance CSP2 M2+instance CSP1 M2++type instance Field M2 = FieldM2+data FieldM2+  = Chan Int+  | Field Int+  deriving (Show,Eq,Ord)++type instance FieldSet M2 = FieldSetM2+newtype FieldSetM2 = FieldSet {unFieldSet :: (Set FieldM2)}+  deriving (Show,Eq,Ord)++type instance Event M2 = EventM2+newtype EventM2 = Event {unEvent :: [FieldM2]}+  deriving (Show,Eq,Ord)++type instance EventSet M2 = EventSetM2+newtype EventSetM2 = EventSet {unEventSet :: (Set EventM2)}+  deriving (Show,Eq,Ord)++type instance Prefix M2 = PrefixM2+newtype PrefixM2 = PrefixM2 {unPrefixM2 :: InternalPrefix}+  deriving (Show,Eq,Ord)++type instance ExtProcess M2 = ExtProcessM2+newtype ExtProcessM2 = ExtProcess (Process M2)+  deriving (Show,Eq,Ord)++type instance ClosureState M2 = ClosureStateM2+data ClosureStateM2 = ClosureState Int [Field M2] EventSetM2+  deriving (Show)++type instance PrefixState M2 = PrefixStateM2+data PrefixStateM2 = PrefixState Int [Field M2] InternalPrefix+  deriving (Show)++type instance RenamingRelation M2 = RenamingRelationM2+data RenamingRelationM2 = RenamingRelation {unRenamingRelation :: Set (EventM2, EventM2)}+  deriving (Show, Eq, Ord)++deriving instance Show (Process M2)+deriving instance Eq (Process M2)+deriving instance Ord (Process M2)+++instance BL M2 where+  prefixNext (PrefixM2 c) event = if Event.member m2 event (allPrefixes c)+    then Just (error "M2 prefixNext p' undefined")+    else Nothing+  switchOn (ExtProcess x) = x++instance BE M2 where+  eventEq _ty a b = a == b+  member _ty a (EventSet s) = a `Set.member` s+  intersection _ty (EventSet a) (EventSet b) = EventSet $ a `Set.intersection` b+  difference _ty (EventSet a) (EventSet b) = EventSet $ a `Set.difference` b+  null _ty (EventSet a) = Set.null a+  singleton _ty a = EventSet $ Set.singleton a+  union = error "BE M2 union undefined (Mock2)"+  insert _ty a (EventSet s) = EventSet $ a `Set.insert` s+  delete _ty a (EventSet s) = EventSet $ a `Set.delete` s+  eventSetToList _ty (EventSet s) = Set.toList s+  allEvents _ty = EventSet $ Set.fromList allEventsList+  isInRenaming _ty (RenamingRelation r) e1 e2 = (e1,e2) `Set.member` r+  imageRenaming _ty (RenamingRelation r) e+    = Set.toList $ Set.map snd $ Set.filter ((==) e . fst) r+  preImageRenaming _ty (RenamingRelation r) e+    = Set.toList $ Set.map fst $ Set.filter ((==) e . snd) r+  isInRenamingDomain _ty e (RenamingRelation r)+    = not $ Set.null $ Set.filter ((==) e . fst) r+  isInRenamingRange _ty e (RenamingRelation r)+    = not $ Set.null $ Set.filter ((==) e . snd) r+  getRenamingDomain _ty = Set.toList . Set.map fst . unRenamingRelation+  getRenamingRange _ty = Set.toList . Set.map snd . unRenamingRelation+  renamingFromList _ty = RenamingRelation . Set.fromList+  renamingToList _ty = Set.toList . unRenamingRelation+  singleEventToClosureSet _ty = EventSet . Set.singleton+++allEventsList :: [Event M2]+allEventsList = List.concat [+     Event <$> [[Chan 1]]+    ,Event <$> sequence [[Chan 2],map Field [1,2,3]]+    ,Event <$> sequence [[Chan 3],map Field [1,2,3],map Field [1,2,3]]+    ]++instance Arb M2 where+  genPrefix _ty = genPrefixM2+  arbitraryEvent _ty = elements $ allEventsList+  arbitraryEventSet _ty = elements $ map (EventSet . Set.fromList)+    $ List.subsequences $ allEventsList++genPrefixM2 :: Arbitrary ProcessM2 => EventM2-> Gen (Prefix M2)+genPrefixM2 event = liftM PrefixM2 (genInternalPrefix event)++data InternalPrefix = InternalPrefix {internalPrefixFields :: [MField]}+  deriving (Show,Eq,Ord)++data MField+  = MOut (Field M2)+  | MIn+  | MGuard (FieldSet M2)+  deriving (Show,Eq,Ord)++allPrefixes :: InternalPrefix -> EventSetM2+allPrefixes p+  = EventSet $ Set.fromList $ map (joinFields m2)+     $ mapM enumField $ internalPrefixFields p+  where+    enumField :: MField -> [FieldM2]+    enumField (MOut f) = [f]+    enumField MIn = map Field [1,2,3]+    enumField (MGuard f) = fieldSetToList m2 f++genInternalPrefix :: Event M2 -> Gen InternalPrefix+genInternalPrefix e = do+  f <- genMFields e+  return $ InternalPrefix f++{- generate fields that at least contain the given event -}+genMFields :: Event M2 -> Gen [MField]+genMFields (Event []) = error "Mock2.hs genMFields : empty event"+genMFields (Event (chan:rest)) = do+  l <- mapM genf rest+  return (MOut chan : l)+  where+    genf f = frequency [+       (10,return $ MOut f)+      ,(10,return MIn)+      ,(10,return $ MGuard $ FieldSet $ Set.singleton f) -- todo more interesting guards+      ]++instance BF M2 where+  fieldEq _ty a b = a == b+  member _ty e (FieldSet s) = e `Set.member` s+  intersection _ty (FieldSet a) (FieldSet b) = FieldSet $ a `Set.intersection` b+  difference _ty (FieldSet a) (FieldSet b) = FieldSet $ a `Set.difference` b+  null _ty (FieldSet a) = Set.null a+  singleton _ty a = FieldSet $ Set.singleton a+  union = error "BF M2 union undefined"+  insert _ty a (FieldSet s) = FieldSet $ a `Set.insert` s+  delete _ty a (FieldSet s) = FieldSet $ a `Set.delete` s+  fieldSetToList _ty (FieldSet s) = Set.toList s++  joinFields _ty = Event+  splitFields _ty (Event l) = l+  channelLen _ty (Chan i) = i+  channelLen _ty _ = error "MockM2 channelLen : not a channel field"++  closureStateInit _ty s = ClosureState 0 [] s++  closureStateNext _ty (ClosureState i l s) f = ClosureState (i+1) (l++[f]) s+  closureRestore   _ty (ClosureState _ _ s) = s++  viewClosureState _ty = viewClosureStateM2+  viewClosureFields _ty = viewClosureFieldsM2+  seenPrefixInClosure ty (ClosureState _i l s) = Event.member ty (Event l) s++  prefixStateInit _ty p = PrefixState 0 [] $ unPrefixM2 p+{-+  prefixStateNext _ty (PrefixState i l p) f = Just $ PrefixState (i+1) (l++[f]) p++this assumes that computeNext allways passes valid fields+(this is not the case, but why ?)++-}+  prefixStateNext _ty (PrefixState i l p) field+    = if checkField (internalPrefixFields p !!i) field+        then Just $ PrefixState (i+1) (l++[field]) p+        else Nothing+    where+      checkField :: MField -> Field M2 -> Bool+      checkField f v = case f of+        MOut v2 -> v == v2+        MIn -> True+        MGuard s -> Field.member m2 v s  ++  prefixStateFinalize _ty (PrefixState _ _ p)+     = Just $ PrefixM2 p -- just return the original process+  viewPrefixState _ty  (PrefixState i _ (InternalPrefix l)) = case ( l !! i) of+    MOut val -> FieldOut val+    MIn -> FieldIn+    MGuard s -> FieldGuard s  +  fieldSetFromList _ty = FieldSet . Set.fromList+++viewClosureStateM2 :: ClosureStateM2 -> ClosureViewM2+viewClosureStateM2 (ClosureState _i p s)+  = if List.null possiblePrefixes+      then NotInClosure+      else MaybeInClosure+  where +    l :: [Event M2]+    l = eventSetToList m2 s+    possiblePrefixes :: [[Field M2]]+    possiblePrefixes = filter (List.isPrefixOf p) $ map (splitFields m2) l+++viewClosureFieldsM2 :: ClosureStateM2 -> FieldSetM2+viewClosureFieldsM2 (ClosureState i p s)+  = FieldSet $ Set.fromList $ map head rests    +  where+    l :: [Event M2]+    l = eventSetToList m2 s+    possiblePrefixes :: [[Field M2]]+    possiblePrefixes = filter (List.isPrefixOf p) $ map (splitFields m2) l+    rests = map (drop i) possiblePrefixes

@@ -0,0 +1,219 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  CSPM.FiringRules.Test.Test+-- Copyright   :  (c) Fontaine 2010+-- License     :  BSD+-- +-- Maintainer  :  fontaine@cs.uni-duesseldorf.de+-- Stability   :  experimental+-- Portability :  GHC-only+--+-- QuickCheck tests for the modules CSPM.FiringRules.EnumerateEvents+-- and CSPM.FiringRules.FieldConstraints.+-- We check for soundness, completeness and that both approaches yield the same result. +--+-----------------------------------------------------------------------------++{-# LANGUAGE StandaloneDeriving,FlexibleInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}+module CSPM.FiringRules.Test.Test+(+  main+)+where++import CSPM.CoreLanguage+import CSPM.CoreLanguage.Event (allEvents)++import CSPM.FiringRules.Rules+import CSPM.FiringRules.Verifier+import CSPM.FiringRules.Test.Mock1+import CSPM.FiringRules.Test.Mock2+import qualified CSPM.FiringRules.EnumerateEvents as EnumNext+import qualified CSPM.FiringRules.FieldConstraints as FieldNext+import CSPM.FiringRules.HelperClasses++import System.Random+import Test.QuickCheck as QC+import Data.Maybe+import qualified Data.List as List+import qualified Data.Set as Set+import Control.Monad++-- | Run a number of QuickCheck tests (with fixed seed).+main :: IO ()+main = forM_ [1,2,3,4] $ \seed -> do+  putStrLn $ "\n\n\nSeed " ++ show seed+  mainDet seed++mainDet :: Int -> IO ()+mainDet i = do+  setStdGen $ mkStdGen i+  testAll++testAll :: IO ()+testAll = do+  testMock1+  testMock2+  testFields++testMock1 :: IO ()+testMock1 = do+  putStrLn "testing Mock1"+  quickCheck $ QC.label "generator Tau rules" +    ((isJust . viewRuleTau) :: RuleTau M1 -> Bool)+  quickCheck $ QC.label "generator Tick rules"+    ((isJust . viewRuleTick) :: RuleTick M1 -> Bool)+  quickCheck $ QC.label "generator Event rules"+    ((isJust . viewRuleEvent) :: RuleEvent M1 -> Bool)+  quickCheck $ QC.label "sound enum Tick rules" +    (sound_EnumRuleTick :: RuleTick M1 -> Bool)+  quickCheck $ QC.label "sound enum Tau rules"+    (sound_EnumRuleTau :: RuleTau M1 -> Bool)+  quickCheck $ QC.label "sound enum Event rules"+    (sound_EnumRuleEvent :: RuleEvent M1 -> Bool)+  quickCheck $ QC.label "complete enum Tick rules"+    (complete_enumTickRules :: RuleTick M1 -> Bool)+  quickCheck $ QC.label "complete enum Tau rules"+    (complete_enumTauRules :: RuleTau M1 -> Bool)+  quickCheck $ QC.label "complete enum Event rules"+    (complete_enumEventRules :: RuleEvent M1 -> Bool)+{-+  quickCheck $ QC.label "enum Event rules == evalEventRules"+    (korrect_evalEventRules :: RuleEvent M1 -> Bool)+  quickCheck $ QC.label "enum Tau rules == symRuleTau"+    (korrect_symTauRules :: RuleTau M1 -> Bool)+-}++testMock2 :: IO ()+testMock2 = do+  putStrLn "\n\ntesting Mock2\n\n"+  quickCheck $ QC.label "generator Tau rules" +    ((isJust . viewRuleTau) :: RuleTau M2 -> Bool)+  quickCheck $ QC.label "generator Tick rules"+    ((isJust . viewRuleTick) :: RuleTick M2 -> Bool)+  quickCheck $ QC.label "generator Event rules"+    ((isJust . viewRuleEvent) :: RuleEvent M2 -> Bool)+  quickCheck $ QC.label "sound enum Tick rules" +    (sound_EnumRuleTick :: RuleTick M2 -> Bool)+  quickCheck $ QC.label "sound enum Tau rules"+    (sound_EnumRuleTau :: RuleTau M2 -> Bool)+  quickCheck $ QC.label "sound enum Event rules"+    (sound_EnumRuleEvent :: RuleEvent M2 -> Bool)+  quickCheck $ QC.label "complete enum Tick rules"+    (complete_enumTickRules :: RuleTick M2 -> Bool)+  quickCheck $ QC.label "complete enum Tau rules"+    (complete_enumTauRules :: RuleTau M2 -> Bool)+  quickCheck $ QC.label "complete enum Event rules"+    (complete_enumEventRules :: RuleEvent M2 -> Bool)+{-+  quickCheck $ QC.label "enum Event rules == evalEventRules"+    (korrect_evalEventRules :: RuleEvent M2 -> Bool)+  quickCheck $ QC.label "enum Tau rules == symRuleTau"+    (korrect_symTauRules :: RuleTau M2 -> Bool)+-}++sound_EnumRuleTick :: CSP1 i => RuleTick i -> Bool+sound_EnumRuleTick r+  = all (checkRule proc . TickRule) $ EnumNext.tickTransitions proc+  where proc = viewProcBefore $ TickRule r++sound_EnumRuleTau :: CSP1 i => RuleTau i -> Bool+sound_EnumRuleTau r+  = all (checkRule proc . TauRule) $ EnumNext.tauTransitions proc+  where proc = viewProcBefore $ TauRule r++sound_EnumRuleEvent :: forall i. CSP1 i => RuleEvent i -> Bool+sound_EnumRuleEvent r+  = all (checkRule proc . EventRule) $ EnumNext.eventTransitions sigma proc+  where+    proc = viewProcBefore $ EventRule r+    sigma = allEvents (undefined :: i)++checkRule :: CSP1 i => Process i -> Rule i -> Bool+checkRule proc r+  = case viewRuleMaybe r of+      Nothing -> False+      Just (p,_,_) -> p == proc++complete_enumTickRules :: CSP1 i => RuleTick i -> Bool+complete_enumTickRules r+  = r `List.elem` (EnumNext.tickTransitions $ viewProcBefore $ TickRule r)++complete_enumTauRules :: CSP1 i => RuleTau i -> Bool+complete_enumTauRules r+  = r `List.elem` (EnumNext.tauTransitions $ viewProcBefore $ TauRule r)++complete_enumEventRules :: forall i. CSP1 i => RuleEvent i -> Bool+complete_enumEventRules r+  = r `List.elem` (EnumNext.eventTransitions sigma $ viewProcBefore $ EventRule r)+  where sigma = allEvents (undefined :: i)++{-+korrect_evalEventRules :: forall i. CSP1 i => RuleEvent i -> Bool+korrect_evalEventRules rule = ruleSet1 == ruleSet2 where+  ruleSet1 = Set.fromList $ enumRuleEvent sigma proc+  ruleSet2 = Set.fromList $ evalRuleEvents proc+  proc = viewProcBefore $ EventRule rule+  sigma = allEvents (undefined :: i)++korrect_symTauRules :: CSP1 i => RuleTau i -> Bool+korrect_symTauRules rule = ruleSet1 == ruleSet2 where+  ruleSet1 = Set.fromList $ buildRuleTau proc+  ruleSet2 = Set.fromList $ symRuleTau proc+  proc = viewProcBefore $ TauRule rule+-}++testFields :: IO ()+testFields = do+  putStrLn "\n\nTesting computeNext"+  quickCheck $ QC.label "sound_computeNext" +    (sound_computeNext :: RuleEvent M2 -> Bool)++  quickCheck $ QC.label "complete_computeNext" +    (complete_computeNext :: RuleEvent M2 -> Bool)++  quickCheck $ QC.label "FieldNext.eventTransitions == EnumNext.eventTransitions"+    (computeNext_eq_EnumRuleEvent :: RuleEvent M2 -> Bool)++  quickCheck $ QC.label "FieldNext.tauTransitions == EnumNext.tauTransitions"+    (fieldTau :: RuleTau M2 -> Bool)++  quickCheck $ QC.label "FieldNext.tickTransitions == EnumNext.tickTransitions"+    (fieldTick :: RuleTau M2 -> Bool)+++sound_computeNext :: forall i. CSP2 i => RuleEvent i -> Bool+sound_computeNext r+  = all (checkRule proc . EventRule) $ FieldNext.eventTransitions sigma proc+  where+    proc = viewProcBefore $ EventRule r+    sigma = allEvents (undefined :: i)++complete_computeNext :: forall i. CSP2 i => RuleEvent i -> Bool+complete_computeNext r+  = r `List.elem` (FieldNext.eventTransitions sigma $ viewProcBefore $ EventRule r)+  where+    sigma = allEvents (undefined :: i)++computeNext_eq_EnumRuleEvent :: forall i. CSP2 i => RuleEvent i -> Bool+computeNext_eq_EnumRuleEvent rule = ruleSet1 == ruleSet2+  where+    ruleSet1 = Set.fromList $ FieldNext.eventTransitions sigma proc+    ruleSet2 = Set.fromList $ EnumNext.eventTransitions sigma proc+    proc = viewProcBefore $ EventRule rule+    sigma = allEvents (undefined :: i)++fieldTau :: forall i. CSP2 i => RuleTau i -> Bool+fieldTau rule = ruleSet1 == ruleSet2+  where+    ruleSet1 = Set.fromList $ EnumNext.tauTransitions proc+    ruleSet2 = Set.fromList $ FieldNext.tauTransitions proc+    proc = viewProcBefore $ TauRule rule++fieldTick :: forall i. CSP2 i => RuleTau i -> Bool+fieldTick rule = ruleSet1 == ruleSet2+  where+    ruleSet1 = Set.fromList $ EnumNext.tickTransitions proc+    ruleSet2 = Set.fromList $ FieldNext.tickTransitions proc+    proc = viewProcBefore $ TauRule rule

@@ -0,0 +1,48 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  CSPM.FiringRules.Trace+-- Copyright   :  (c) Fontaine 2010+-- License     :  BSD+-- +-- Maintainer  :  fontaine@cs.uni-duesseldorf.de+-- Stability   :  experimental+-- Portability :  GHC-only+--+-- A very rudimentary process tracer for debugging and testing.+-- Prints the current process and the possible transitions to stdout+-- and lets the user select a transition by typing to stdin.+--+-----------------------------------------------------------------------------++{-# LANGUAGE ScopedTypeVariables, TypeFamilies #-}+module CSPM.FiringRules.Trace+where++import CSPM.CoreLanguage++import CSPM.FiringRules.Rules+import CSPM.FiringRules.Verifier  (viewProcAfter,viewEvent)+import CSPM.FiringRules.FieldConstraints (computeTransitions)+import CSPM.FiringRules.HelperClasses++trace :: forall i e. (FShow i, ShowTTE e , CSP2 i, e ~ TTE i)+  => Sigma i -> Process i -> IO ()+trace events process = do+  putStrLn "\n\n\nProcess :"+  putStrLn $ show process+  let rules = computeTransitions events process+  if null rules+    then putStrLn "deadlock state"+    else do+  sequence_ $ zipWith printTrans [0..] rules+  putStrLn "Select a Transition "+  i <- readLn+  trace events (viewProcAfter (rules !! i))+  where+    printTrans :: Int -> Rule i -> IO ()+    printTrans nr r = do+      putStr (show nr ++ " : ")+      putStr $ showTTE $ viewEvent r+      putStrLn ""+--    putStrLn $ show r+      putStrLn ""

@@ -0,0 +1,336 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  CSPM.FiringRules.Verifier+-- Copyright   :  (c) Fontaine 2010+-- License     :  BSD+-- +-- Maintainer  :  fontaine@cs.uni-duesseldorf.de+-- Stability   :  experimental+-- Portability :  GHC-only+--+-- A checker for the firing rules semantics of CSPM.+--+-- It checks that a transition proof tree is valid with respect to the firing rules+-- semantics of CSPM.+-- In particular, it checks, that it is syntactically valid and that all side conditions hold.+-- +-- The 'Rule' data type stores proof trees in a compressed form.+-- These functions are also used to reconstruct an explicit representation of the transition.+--+-- Note :+-- In our use-case for this module, it is an assertions that the proof tree generator+-- only constructs valid proof trees,+-- i.e. an invalid proof tree always means a bug in the proof tree generator.+-- We use 'viewRule' to reconstruct the transition and at the same time check that assertion.+-- If one knows for sure that all proof trees are correct,+-- it is possible to use a faster version of 'viewRule',+-- which reconstructs the transition without checking the side conditions.+--+-----------------------------------------------------------------------------+{-# LANGUAGE ScopedTypeVariables #-}++module CSPM.FiringRules.Verifier+  (+   viewRule+  ,viewProcBefore+  ,viewEvent+  ,viewProcAfter+  ,viewRuleMaybe+  ,viewRuleTau+  ,viewRuleTick+  ,viewRuleEvent+  )+where++import CSPM.CoreLanguage+import CSPM.CoreLanguage.Event+import CSPM.FiringRules.Rules++import Control.Monad+import Data.Maybe+import qualified Data.List as List++{-|+  This function reconstructs the transition that is actually proven by the proof tree.+  It returns the transition as a triple (predecessor 'Process', Event, successor 'Process').+  If the proof tree is invalid it throws an exception.+-}+viewRule :: BL i => Rule i -> (Process i, TTE i, Process i)+viewRule proofTree = case viewRuleMaybe proofTree of+  Nothing -> error "viewRule : internal error malformed Rule"+  Just v -> v++-- | Like 'viewRule' but just return the predecessor process.+viewProcBefore :: BL i => Rule i -> Process i+viewProcBefore = (\(p,_,_) -> p) . viewRule++-- | Like 'viewRule' but just return the event.+viewEvent :: BL i => Rule i -> TTE i+viewEvent =  (\(_,e,_) -> e) . viewRule++-- | Like 'viewRule' but just return the successor process.+viewProcAfter :: BL i => Rule i  -> Process i+viewProcAfter =  (\(_,_,p) -> p) . viewRule++{-|+  Like 'viewRule' but returns 'Nothing' in case of an invalid proof tree.+-}+viewRuleMaybe :: BL i => Rule i -> Maybe (Process i, TTE i, Process i)+viewRuleMaybe proofTree = case proofTree of+  TauRule r -> case viewRuleTau r of+    Just (p, p') -> Just (p, TauEvent, p')+    Nothing     -> Nothing+  TickRule r -> case viewRuleTick r of+    Just p  -> Just (p, TickEvent, Omega)+    Nothing -> Nothing+  EventRule r -> case viewRuleEvent r of+    Just (p, e, p') -> Just (p, SEvent e, p')+    Nothing -> Nothing++-- | Used for testing.+viewRuleTau :: forall i. BL i => RuleTau i -> Maybe (Process i, Process i)+viewRuleTau rule = case rule of+  ExtChoiceTauL pp q -> do+    (p, p') <- viewRuleTau pp+    return (ExternalChoice p q, ExternalChoice p' q)+  ExtChoiceTauR p qq -> do+    (q, q') <- viewRuleTau qq+    return (ExternalChoice p q, ExternalChoice p q')+  InternalChoiceL p q -> return (InternalChoice p q,p)+  InternalChoiceR p q -> return (InternalChoice p q,q)+  InterleaveTauL pp q -> do+    (p, p') <- viewRuleTau pp+    return (Interleave p q, Interleave p' q)+  InterleaveTauR p qq -> do+    (q, q') <- viewRuleTau qq+    return (Interleave p q, Interleave p q')+  InterleaveTickL pp q -> do+    p <- viewRuleTick pp+    return (Interleave p q, Interleave Omega q)+  InterleaveTickR p qq -> do+    q <- viewRuleTick qq+    return (Interleave p q, Interleave p Omega)+  SeqTau pp q -> do+    (p, p') <- viewRuleTau pp+    return (Seq p q, Seq p' q)+  SeqTick pp q -> do+    p <- viewRuleTick pp+    return (Seq p q, q)+  Hidden c pp -> do+    (p, e, p') <- viewRuleEvent pp+    guard $ member (undefined :: i) e c+    return (Hide c p, Hide c p')+  HideTau c pp -> do+    (p, p') <- viewRuleTau pp+    return (Hide c p, Hide c p')+  ShareTauL c pp q -> do+    (p, p') <- viewRuleTau pp+    return (Sharing p c q, Sharing p' c q)+  ShareTauR c p qq -> do+    (q, q') <- viewRuleTau qq+    return (Sharing p c q, Sharing p c q')+  ShareTickL c pp q -> do+    p <- viewRuleTick pp+    return (Sharing p c q, Sharing Omega c q)+  ShareTickR c p qq -> do+    q <- viewRuleTick qq+    return (Sharing p c q, Sharing p c Omega)+  AParallelTauL pc qc r q -> do+    (p, p') <- viewRuleTau r+    return (AParallel pc qc p q, AParallel pc qc p' q)+  AParallelTauR pc qc p r -> do+    (q, q') <- viewRuleTau r+    return (AParallel pc qc p q, AParallel pc qc p q')    +  AParallelTickL pc qc r q -> do+    p <- viewRuleTick r+    return (AParallel pc qc p q, AParallel pc qc Omega q)    +  AParallelTickR pc qc p r -> do+    q <- viewRuleTick r+    return (AParallel pc qc p q, AParallel pc qc p Omega)    +  InterruptTauL r q -> do+    (p, p') <- viewRuleTau r+    return (Interrupt p q, Interrupt p' q)+  InterruptTauR p r -> do+    (q, q') <- viewRuleTau r+    return (Interrupt p q, Interrupt p q')+  TauRepAParallel l -> do+    parts <- forM l $ \x -> case x of+      Left a -> return (a, a)+      Right (c, r) -> do +        (p, p') <- viewRuleTau r+        return ((c,p), (c,p'))+    return (RepAParallel $ map fst parts, RepAParallel $ map snd parts)+  TimeoutTauR r q -> do+    (p, p') <- viewRuleTau r+    return (Timeout p q, Timeout p' q)+  TimeoutOccurs p q -> return (Timeout p q, q)+  RenamingTau rel pp -> do+    (p, p') <- viewRuleTau pp+    return (Renaming rel p, Renaming rel p')+  ChaosStop e -> return (Chaos e, Stop)+  LinkTauL rel pp q -> do+    (p, p') <- viewRuleTau pp+    return (LinkParallel rel p q, LinkParallel rel p' q)+  LinkTauR rel p qq -> do+    (q, q') <- viewRuleTau qq+    return (LinkParallel rel p q, LinkParallel rel p q')+  LinkTickL rel pp q -> do+    p <- viewRuleTick pp+    return (LinkParallel rel p q, LinkParallel rel Omega q)+  LinkTickR rel p qq -> do+    q <- viewRuleTick qq+    return (LinkParallel rel p q, LinkParallel rel p Omega)+  LinkLinked rel pp qq -> do+    (p, e1, p') <- viewRuleEvent pp+    (q, e2, q') <- viewRuleEvent qq+    guard $ isInRenaming (undefined :: i) rel e1 e2+    return (LinkParallel rel p q, LinkParallel rel p' q')+  TraceSwitchOn p -> return (p, p)++-- | Used for testing.+viewRuleTick :: BL i => RuleTick i -> Maybe (Process i)+viewRuleTick rule = case rule of+  InterleaveOmega -> return (Interleave Omega Omega)+  HiddenTick c pp -> do+    p <- viewRuleTick pp+    return $ Hide c p+  ShareOmega c -> return $ Sharing Omega c Omega+  AParallelOmega c1 c2 -> return $ AParallel c1 c2 Omega Omega+  SkipTick -> return Skip+  ExtChoiceTickL pp q -> do+    p <- viewRuleTick pp+    return $ ExternalChoice p q+  ExtChoiceTickR p qq -> do+    q <- viewRuleTick qq+    return $ ExternalChoice p q+  InterruptTick pp q -> do+    p <- viewRuleTick pp+    return $ Interrupt p q+  TimeoutTick pp q -> do+    p <- viewRuleTick pp+    return $ Timeout p q+  RepAParallelOmega l+    -> return $ RepAParallel $ zip l $ repeat Omega+  RenamingTick rel pp -> do+    p <- viewRuleTick pp+    return $ Renaming rel p+  LinkParallelTick rel+    -> return $ LinkParallel rel Omega Omega++-- | Used for testing.+viewRuleEvent :: forall i. BL i => RuleEvent i -> Maybe (Process i, Event i, Process i)+viewRuleEvent rule = case rule of+  HPrefix e p -> do+    p' <- prefixNext p e+    return (Prefix p, e, p')+  ExtChoiceL pp q -> do+    (p, e, p') <- viewRuleEvent pp+    return (ExternalChoice p q, e, p')+  ExtChoiceR p qq -> do+    (q, e, q') <- viewRuleEvent qq+    return (ExternalChoice p q, e, q')+  InterleaveL pp q -> do+    (p, e, p') <- viewRuleEvent pp+    return (Interleave p q, e, Interleave p' q)+  InterleaveR p qq -> do+    (q, e, q') <- viewRuleEvent qq+    return (Interleave p q, e, Interleave p q')+  SeqNormal pp q -> do+    (p, e, p') <- viewRuleEvent pp+    return (Seq p q, e, Seq p' q)+  NotHidden c pp -> do+    (p, e, p') <- viewRuleEvent pp+    guard $ not $ member ty e c+    return (Hide c p, e, Hide c p')+  NotShareL c pp q -> do+    (p, e, p') <- viewRuleEvent pp+    guard $ not $ member ty e c+    return (Sharing p c q, e, Sharing p' c q)+  NotShareR c p qq -> do+    (q, e, q') <- viewRuleEvent qq+    not_in_Closure e c+    return (Sharing p c q, e, Sharing p c q')+  Shared c pp qq -> do+    (p, e1, p') <- viewRuleEvent pp+    (q, e2, q') <- viewRuleEvent qq+    guard $ eventEq ty e1 e2+    in_Closure e1 c+    return (Sharing p c q, e1, Sharing p' c q')+  AParallelL c1 c2 pp q -> do+    (p, e, p') <- viewRuleEvent pp+    in_Closure e c1+    not_in_Closure e c2+    return (AParallel c1 c2 p q, e, AParallel c1 c2 p' q)+  AParallelR c1 c2 p qq -> do+    (q, e, q') <- viewRuleEvent qq+    not_in_Closure e c1+    in_Closure e c2+    return (AParallel c1 c2 p q, e, AParallel c1 c2 p q')+  AParallelBoth c1 c2 pp qq -> do+    (p, e2, p') <- viewRuleEvent pp+    (q, e1, q') <- viewRuleEvent qq+    guard $ eventEq ty e1 e2+    in_Closure e1 c1+    in_Closure e1 c2+    return (AParallel c1 c2 p q, e1, AParallel c1 c2 p' q')+  NoInterrupt pp q -> do+    (p, e, p') <- viewRuleEvent pp+    return (Interrupt p q, e, Interrupt p' q)+  InterruptOccurs p qq -> do+    (q, e, q') <- viewRuleEvent qq+    return (Interrupt p q, e, q')+  TimeoutNo pp q -> do+    (p, e, p') <- viewRuleEvent pp+    return (Timeout p q, e, p')+  RepAParallelEvent l -> checkRepAParallel l+  Rename rel event pp -> do+    (p, e, p') <- viewRuleEvent pp+    guard $ isInRenaming ty rel e event+    return (Renaming rel p, event, Renaming rel p')+  RenameNotInDomain rel pp -> do+    (p, e, p') <- viewRuleEvent pp+    guard $ not $ isInRenamingDomain ty e rel+    return (Renaming rel p, e, Renaming rel p')+  ChaosEvent c e -> do+    in_Closure e c+    return (Chaos c, e, Chaos c)+  LinkEventL rel pp q -> do+    (p, e, p') <- viewRuleEvent pp+    guard $ not $ isInRenamingDomain ty e rel+    return (LinkParallel rel p q, e, LinkParallel rel p' q)+  LinkEventR rel p qq -> do+    (q, e, q') <- viewRuleEvent qq+    guard $ not $ isInRenamingRange ty e rel+    return (LinkParallel rel p q, e, LinkParallel rel p q')+  where+    ty = (undefined :: i)+    in_Closure e c = guard $ member ty e c+    not_in_Closure e c = guard $ not $ member ty e c++    checkRepAParallel :: [EventRepAPart i] -> Maybe (Process i, Event i, Process i)+    checkRepAParallel l = do+      parts <- forM l $ \x -> case x of+        Left w -> return $ Left w+        Right (c,r) -> do { v <- viewRuleEvent r; return $ Right (c,v) }+--    check that all events are equal+      let events = flip mapMaybe parts $ \x -> case x of+            Left _ -> Nothing+            Right (_,(_,e,_)) -> Just e+      guard $ (not $ List.null events) +         && (all (eventEq ty $ head events) $ tail events)+{-+check that if the event is in a closure set the corresponding process has+also taken part in the event+-}+      let event = head events+      guard $ flip all parts $ \x -> case x of+            Left (closure,_) -> not $ member ty event closure+            Right (closure,_) -> member ty event closure+      let+        procs = flip map parts $ \x -> case x of+          Left pair -> pair+          Right (c,(p,_,_)) -> (c,p)+        procs' = flip map parts $ \x -> case x of+          Left pair -> pair+          Right (c,(_,_,p')) -> (c,p')+      return (RepAParallel procs, event, RepAParallel procs')