diff --git a/CSPM-FiringRules.cabal b/CSPM-FiringRules.cabal
new file mode 100644
--- /dev/null
+++ b/CSPM-FiringRules.cabal
@@ -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
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -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.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,3 @@
+#!/usr/bin/env runhaskell
+import Distribution.Simple
+main = defaultMain
diff --git a/src/CSPM/FiringRules/EnumerateEvents.hs b/src/CSPM/FiringRules/EnumerateEvents.hs
new file mode 100644
--- /dev/null
+++ b/src/CSPM/FiringRules/EnumerateEvents.hs
@@ -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
diff --git a/src/CSPM/FiringRules/FieldConstraints.hs b/src/CSPM/FiringRules/FieldConstraints.hs
new file mode 100644
--- /dev/null
+++ b/src/CSPM/FiringRules/FieldConstraints.hs
@@ -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
diff --git a/src/CSPM/FiringRules/HelperClasses.hs b/src/CSPM/FiringRules/HelperClasses.hs
new file mode 100644
--- /dev/null
+++ b/src/CSPM/FiringRules/HelperClasses.hs
@@ -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
+
diff --git a/src/CSPM/FiringRules/Rules.hs b/src/CSPM/FiringRules/Rules.hs
new file mode 100644
--- /dev/null
+++ b/src/CSPM/FiringRules/Rules.hs
@@ -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)
diff --git a/src/CSPM/FiringRules/Test/Gen.hs b/src/CSPM/FiringRules/Test/Gen.hs
new file mode 100644
--- /dev/null
+++ b/src/CSPM/FiringRules/Test/Gen.hs
@@ -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
diff --git a/src/CSPM/FiringRules/Test/Mock1.hs b/src/CSPM/FiringRules/Test/Mock1.hs
new file mode 100644
--- /dev/null
+++ b/src/CSPM/FiringRules/Test/Mock1.hs
@@ -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)
diff --git a/src/CSPM/FiringRules/Test/Mock2.hs b/src/CSPM/FiringRules/Test/Mock2.hs
new file mode 100644
--- /dev/null
+++ b/src/CSPM/FiringRules/Test/Mock2.hs
@@ -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
diff --git a/src/CSPM/FiringRules/Test/Test.hs b/src/CSPM/FiringRules/Test/Test.hs
new file mode 100644
--- /dev/null
+++ b/src/CSPM/FiringRules/Test/Test.hs
@@ -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
diff --git a/src/CSPM/FiringRules/Trace.hs b/src/CSPM/FiringRules/Trace.hs
new file mode 100644
--- /dev/null
+++ b/src/CSPM/FiringRules/Trace.hs
@@ -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 ""
diff --git a/src/CSPM/FiringRules/Verifier.hs b/src/CSPM/FiringRules/Verifier.hs
new file mode 100644
--- /dev/null
+++ b/src/CSPM/FiringRules/Verifier.hs
@@ -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')