diff --git a/CSPM-FiringRules.cabal b/CSPM-FiringRules.cabal
--- a/CSPM-FiringRules.cabal
+++ b/CSPM-FiringRules.cabal
@@ -1,7 +1,7 @@
-Name:                CSPM-FiringRules
-Version:             0.1.0.0
-Synopsis:            Firing rules semantic of CSPM
-Description:
+name:                CSPM-FiringRules
+version:             0.3.0.3
+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.)
@@ -12,37 +12,53 @@
   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
+category:            Language,Formal Methods,Concurrency
+build-type:          Simple
+license:             BSD3
+license-file:        LICENSE
+author:              2010 - 2011 Marc Fontaine
+maintainer:          Marc Fontaine <fontaine@cs.uni-duesseldorf.de>
+homepage:            http://www.stups.uni-duesseldorf.de/~fontaine/csp
+stability:           experimental
+tested-With:         GHC == 7.0.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
+cabal-Version:       >= 1.10
 
-build-type: Simple
-GHC-Options: -funbox-strict-fields -O2 -Wall
-Hs-Source-Dirs:         src
+flag QuickCheck
+  description: enable QuickCheck tests
+  default: True
 
-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
+library
+  build-Depends:
+     CSPM-CoreLanguage >= 0.2 && < 0.3
+    ,tree-monad >=0.3 && < 0.4
+    ,parallel-tree-search >=0.4 && < 0.5
+    ,base >= 4.0 && < 5.0
+    ,containers >= 0.4 && < 0.5
+    ,mtl (>= 2.0 && < 2.1 ) || (>= 1.1 && < 1.2)
+  
+  Default-Language: Haskell2010
+  ghc-options: -funbox-strict-fields -O2 -Wall
+  hs-source-dirs:         src
+
+  exposed-modules:
+    CSPM.FiringRules.Rules
+    CSPM.FiringRules.Verifier
+    CSPM.FiringRules.EnumerateEvents
+    CSPM.FiringRules.EnumerateEventsList
+    CSPM.FiringRules.FieldConstraints
+    CSPM.FiringRules.FieldConstraintsSearch
+    CSPM.FiringRules.Search
+    CSPM.FiringRules.Trace
+    CSPM.FiringRules.HelperClasses
+
+  if flag(QuickCheck)
+    build-depends:
+      QuickCheck >= 2.4 && < 2.5
+      ,random >= 1.0 && < 1.1
+    exposed-modules:
+      CSPM.FiringRules.Test.Test
+    other-modules:
+      CSPM.FiringRules.Test.Mock1
+      CSPM.FiringRules.Test.Mock2
+      CSPM.FiringRules.Test.Gen
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) Marc Fontaine 2007-2009
+Copyright (c) Marc Fontaine 2007-2011
 
 All rights reserved.
 
diff --git a/src/CSPM/FiringRules/EnumerateEvents.hs b/src/CSPM/FiringRules/EnumerateEvents.hs
--- a/src/CSPM/FiringRules/EnumerateEvents.hs
+++ b/src/CSPM/FiringRules/EnumerateEvents.hs
@@ -26,19 +26,19 @@
 import CSPM.CoreLanguage
 import CSPM.CoreLanguage.Event
 import CSPM.FiringRules.Rules
+import CSPM.FiringRules.Search
 
 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]
+  => Sigma i -> Process i -> Search (Rule i)
 computeTransitions events p
-  =  (liftM EventRule $ eventTransitions events p)
+  = (liftM EventRule $ eventTransitions events p)
          `mplus` (liftM TickRule $ tickTransitions p)
          `mplus` (liftM TauRule $ tauTransitions p)
 
@@ -46,18 +46,18 @@
      BL i
   => Sigma i
   -> Process i 
-  -> [RuleEvent i]
+  -> Search (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 :: forall i. BL i => i -> EventSet i -> Search (Event i)
 anyEvent ty sigma
-  = foldr (mplus . return)  mzero $ eventSetToList ty sigma
+  = anyOf $ eventSetToList ty sigma
 
-buildRuleEvent :: forall i. BL i => Event i -> Process i -> EnumM (RuleEvent i)
+buildRuleEvent :: forall i. BL i => Event i -> Process i -> Search (RuleEvent i)
 buildRuleEvent event proc = case proc of
   SwitchedOff p -> rp $ switchOn p
   Prefix p  -> case (prefixNext p event :: Maybe (Process i)) of
@@ -117,7 +117,7 @@
 
 buildRuleRepAParallel :: forall i. BL i
   => Event i 
-  -> [(EventSet i, Process i)] -> EnumM (RuleEvent i)
+  -> [(EventSet i, Process i)] -> Search (RuleEvent i)
 buildRuleRepAParallel event l = do
   l2 <- mapM parPart l
   if List.null $ Either.rights l2
@@ -131,7 +131,7 @@
       else return $ Left c
     ty = (undefined :: i)
 
-tauTransitions :: forall i. BL i => Process i -> EnumM (RuleTau i)
+tauTransitions :: forall i. BL i => Process i -> Search (RuleTau i)
 tauTransitions proc = case proc of
   SwitchedOff p -> tauTransitions $ switchOn p
   Prefix {} -> mzero
@@ -190,24 +190,24 @@
    => RenamingRelation i
    -> Process i
    -> Process i
-   -> EnumM (RuleTau i)
+   -> Search (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 :: Search (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 :: [Event i] -> Process i -> Search (Event i, RuleEvent i)
     rules s proc = do
-      e <- s
+      e <- anyOf s
       r <- buildRuleEvent e proc
       return (e,r)
     ty = (undefined :: i)
 
-tickTransitions :: BL i => Process i -> EnumM (RuleTick i)
+tickTransitions :: BL i => Process i -> Search (RuleTick i)
 tickTransitions proc = case proc of
   SwitchedOff p -> tickTransitions $ switchOn p
   Prefix {} -> mzero
@@ -226,7 +226,7 @@
   Seq _p _q -> mzero
   Hide c p -> HiddenTick c <$> tickTransitions p
   Stop -> mzero
-  Skip -> return $ SkipTick
+  Skip -> return SkipTick
   Omega -> mzero
   AProcess _n -> mzero
   RepAParallel l -> if all (isOmega . snd) l
diff --git a/src/CSPM/FiringRules/EnumerateEventsList.hs b/src/CSPM/FiringRules/EnumerateEventsList.hs
new file mode 100644
--- /dev/null
+++ b/src/CSPM/FiringRules/EnumerateEventsList.hs
@@ -0,0 +1,44 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  CSPM.FiringRules.EnumerateEventsList
+-- Copyright   :  (c) Fontaine 2010
+-- License     :  BSD
+-- 
+-- Maintainer  :  fontaine@cs.uni-duesseldorf.de
+-- Stability   :  experimental
+-- Portability :  GHC-only
+--
+-- Reexport of the functions from EnumerateEvents with a List interface.
+-----------------------------------------------------------------------------
+
+{-# LANGUAGE ScopedTypeVariables #-}
+module CSPM.FiringRules.EnumerateEventsList
+(
+  computeTransitions
+ ,eventTransitions
+ ,tauTransitions
+ ,tickTransitions
+)
+where
+
+import CSPM.CoreLanguage
+import CSPM.CoreLanguage.Event
+import CSPM.FiringRules.Rules
+import qualified CSPM.FiringRules.EnumerateEvents as EE
+import CSPM.FiringRules.Search (runSearch)
+
+-- | 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
+  = runSearch $ EE.computeTransitions events p
+
+eventTransitions :: forall i. BL i
+  => Sigma i -> Process i -> [RuleEvent i]
+eventTransitions sigma p = runSearch $ EE.eventTransitions sigma p
+
+tauTransitions :: forall i. BL i => Process i -> [RuleTau i]
+tauTransitions = runSearch . EE.tauTransitions
+
+tickTransitions :: BL i => Process i -> [RuleTick i]
+tickTransitions = runSearch . EE.tickTransitions
diff --git a/src/CSPM/FiringRules/FieldConstraints.hs b/src/CSPM/FiringRules/FieldConstraints.hs
--- a/src/CSPM/FiringRules/FieldConstraints.hs
+++ b/src/CSPM/FiringRules/FieldConstraints.hs
@@ -1,21 +1,17 @@
 -----------------------------------------------------------------------------
 -- |
--- Module      :  CSPM.FiringRules.FieldConstraints
--- Copyright   :  (c) Fontaine 2010
+-- Module      :  CSPM.FiringRules.FieldConstraintsList
+-- Copyright   :  (c) Fontaine 2010 - 2011
 -- 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.
---
+-- Reexport of the functions from FieldConstraintsSearch with a List interface.
 -----------------------------------------------------------------------------
 
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE ViewPatterns #-}
 module CSPM.FiringRules.FieldConstraints
 (
   computeTransitions
@@ -25,571 +21,26 @@
 )
 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
-
+import CSPM.CoreLanguage
+import CSPM.FiringRules.Rules
+import qualified CSPM.FiringRules.FieldConstraintsSearch as FC
+import CSPM.FiringRules.Search (runSearch)
 
+-- | Compute all possible transitions of the process.
 computeTransitions ::  forall i. BF i 
-  => Event.Sigma i -> Process i -> [Rule 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)
-
-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])
+  = runSearch $ FC.computeTransitions events p
 
-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
+-- | Compute all (event)- transitions of the process.
+eventTransitions :: forall i. BF i
+  => Sigma i -> Process i -> [RuleEvent i]
+eventTransitions sigma p = runSearch $ FC.eventTransitions sigma 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
+-- | Compute all tau-transitions of the process
+tauTransitions :: forall i. BF i => Process i -> [RuleTau i]
+tauTransitions = runSearch . FC.tauTransitions
 
-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
+-- | Compute all tick-transitions of the process
+tickTransitions :: BF i => Process i -> [RuleTick i]
+tickTransitions = runSearch . FC.tickTransitions
diff --git a/src/CSPM/FiringRules/FieldConstraintsSearch.hs b/src/CSPM/FiringRules/FieldConstraintsSearch.hs
new file mode 100644
--- /dev/null
+++ b/src/CSPM/FiringRules/FieldConstraintsSearch.hs
@@ -0,0 +1,592 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  CSPM.FiringRules.FieldConstraintsSearch
+-- Copyright   :  (c) Fontaine 2010 - 2011
+-- 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.FieldConstraintsSearch
+(
+  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 CSPM.FiringRules.Search
+
+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 -> Search (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)
+
+rulePattern :: forall i. BF i => Event.EventSet i -> Process i -> Search (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 -> Search (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 -> Search (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))
+    ->       (ExtChoiceL <$> (anyOf rp >>= rec) <*> pure q)
+    `mplus`  (ExtChoiceR p <$> (anyOf rq >>= rec) )
+  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 -> Search (RuleEvent i)
+eventTransitions events proc = liftM snd $ computeNextE events proc
+
+computeNextE :: BF i 
+  => Event.EventSet i -> Process i -> Search (Event.Event i, RuleEvent i)
+computeNextE events proc = rulePattern events proc >>= runFields events
+
+runFields :: forall i. BF i
+  => Event.EventSet i -> RuleField i -> Search (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 
+  -> Search ([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 -> Search (Field i, RuleField i)
+enumField top r = case execStateT (propField r) top of
+      Just s -> do
+        f <- anyOf $ fieldSetToList ty s
+        nr <- nextField r f
+        return (f ,nr )
+      Nothing -> mzero
+  where ty = (undefined :: i)
+
+tauTransitions :: forall i. BF i => Process i -> Search (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 -> Search (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)) $ runSearch $ 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 
+  -> Search (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)])
+      -> Search (EventRepAPart i)
+    mkPart (closure, origProc, []) = do
+      guard (not $ inClosure closure)
+      return $ Left (restoreClosure closure, origProc)
+    mkPart (closure, _origProc, (map snd -> rules)) = do
+      r <- anyOf 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
+  -> Search (RuleEvent i)
+renamingRules rel proc event = do
+    fromEvent <- anyOf $ 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
+   -> Search (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 :: Search (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 -> Search (Event.Event i, RuleEvent i)
+    rules s proc = do
+      e <- anyOf 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 = runSearch $ 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 = runSearch $ msum $ map (flip nextField field) rules
+
+joinRepExtChoiceParts :: forall i. BF i
+  => RepExtChoicePart i -> RepExtChoicePart i -> Search (RuleField i)
+joinRepExtChoiceParts l r = case (l,r) of
+  (Left _,Left _) -> mzero
+  (Right (_,rules), Left q) -> FExtChoiceL <$> anyOf rules <*> pure q
+  (Left p, Right (_,rules)) -> FExtChoiceR p <$> anyOf rules
+  (Right _,Right _) -> return $ FExtChoice l r
diff --git a/src/CSPM/FiringRules/HelperClasses.hs b/src/CSPM/FiringRules/HelperClasses.hs
--- a/src/CSPM/FiringRules/HelperClasses.hs
+++ b/src/CSPM/FiringRules/HelperClasses.hs
@@ -23,7 +23,10 @@
 -- | 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))
+  ,Eq (EventSet i), Eq (ExtProcess i), Eq (Prefix i), Eq (Event i), Eq (RenamingRelation i)
+  ,Ord (Process i), Ord (RuleTick i), Ord (RuleTau i) ,Ord (RuleEvent i)
+  ,Ord (EventSet i), Ord (ExtProcess i), Ord (Prefix i), Ord (Event i), Ord (RenamingRelation i))
+
   => EqOrd i
 
 -- | Implementation i supports 'Show'.
diff --git a/src/CSPM/FiringRules/Rules.hs b/src/CSPM/FiringRules/Rules.hs
--- a/src/CSPM/FiringRules/Rules.hs
+++ b/src/CSPM/FiringRules/Rules.hs
@@ -1,8 +1,8 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  CSPM.FiringRules.Rules
--- Copyright   :  (c) Fontaine 2010
--- License     :  BSD
+-- Copyright   :  (c) Fontaine 2010 - 2011
+-- License     :  BSD3
 -- 
 -- Maintainer  :  fontaine@cs.uni-duesseldorf.de
 -- Stability   :  experimental
@@ -30,16 +30,18 @@
 
 import CSPM.CoreLanguage
 
--- | A sum-type for tau, tick and regular rules.
+-- | A sum-type for tau, tick and regular proof trees.
 data Rule i
   = TauRule (RuleTau i)
   | TickRule (RuleTick i)
   | EventRule (RuleEvent i)
 
+-- | Is this a proof tree for a tau-transition
 isTauRule :: Rule i -> Bool
 isTauRule (TauRule {}) = True
 isTauRule _ = False
 
+-- | Representation of tau proof trees.
 data RuleTau i
   = Hidden (EventSet i) (RuleEvent i)
   | HideTau (EventSet i) (RuleTau i)
@@ -75,6 +77,7 @@
   | LinkTickR (RenamingRelation i)  (Process i) (RuleTick i)
   | TraceSwitchOn (Process i) -- pseudo-tau for debugging
 
+-- | Representation of tick proof trees.
 data RuleTick i
   = SkipTick
   | HiddenTick (EventSet i) (RuleTick i)
@@ -89,6 +92,7 @@
   | RenamingTick (RenamingRelation i) (RuleTick i)
   | LinkParallelTick (RenamingRelation i)
 
+-- | Representation of regular proof trees (i.e. non-tau and non-tick transitions)
 data RuleEvent i
   = HPrefix (Event i) (Prefix i)
   | ExtChoiceL (RuleEvent i) (Process i)
@@ -113,6 +117,8 @@
   | ChaosEvent (EventSet i) (Event i)
   | LinkEventL (RenamingRelation i) (RuleEvent i) (Process i)
   | LinkEventR (RenamingRelation i) (Process i) (RuleEvent i)
+  | NoException (EventSet i) (RuleEvent i)  (Process i)
+  | ExceptionOccurs (EventSet i) (Process i) (RuleEvent i)
 
 type EventRepAPart i
   = Either (EventSet i, Process i) (EventSet i, RuleEvent i)
diff --git a/src/CSPM/FiringRules/Search.hs b/src/CSPM/FiringRules/Search.hs
new file mode 100644
--- /dev/null
+++ b/src/CSPM/FiringRules/Search.hs
@@ -0,0 +1,36 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  CSPM.FiringRules.Search
+-- Copyright   :  (c) Fontaine 2010 - 2011
+-- License     :  BSD3
+-- 
+-- Maintainer  :  fontaine@cs.uni-duesseldorf.de
+-- Stability   :  experimental
+-- Portability :  GHC-only
+--
+-- Definition of the Search Monad.
+-- Currently just a small wrapper around the tree-monad package
+--
+-----------------------------------------------------------------------------
+
+module CSPM.FiringRules.Search
+(
+  Search
+ ,runSearch
+ ,anyOf
+)
+where
+
+import qualified Control.Monad.SearchTree as MS
+import Control.Parallel.TreeSearch (parSearch)
+import Control.Monad
+
+type Search a = MS.Search a
+
+-- | Run the search monad.
+runSearch :: Search a -> [a]
+runSearch = parSearch . MS.searchTree
+
+-- | Lift a list to the search monad.
+anyOf :: [a] -> Search a
+anyOf = msum . map return
diff --git a/src/CSPM/FiringRules/Test/Test.hs b/src/CSPM/FiringRules/Test/Test.hs
--- a/src/CSPM/FiringRules/Test/Test.hs
+++ b/src/CSPM/FiringRules/Test/Test.hs
@@ -29,7 +29,7 @@
 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.EnumerateEventsList as EnumNext
 import qualified CSPM.FiringRules.FieldConstraints as FieldNext
 import CSPM.FiringRules.HelperClasses
 
diff --git a/src/CSPM/FiringRules/Trace.hs b/src/CSPM/FiringRules/Trace.hs
--- a/src/CSPM/FiringRules/Trace.hs
+++ b/src/CSPM/FiringRules/Trace.hs
@@ -25,11 +25,14 @@
 import CSPM.FiringRules.FieldConstraints (computeTransitions)
 import CSPM.FiringRules.HelperClasses
 
+-- | A simplistic interactive CSP-M tracer.
+-- It prints all events offered by a Proccess to stdout and
+-- promts the user for the event to perform.
 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
+--  putStrLn "Process :"
+--  putStr $ show $ hash process
   let rules = computeTransitions events process
   if null rules
     then putStrLn "deadlock state"
@@ -42,7 +45,7 @@
     printTrans :: Int -> Rule i -> IO ()
     printTrans nr r = do
       putStr (show nr ++ " : ")
-      putStr $ showTTE $ viewEvent r
       putStrLn ""
---    putStrLn $ show r
+--      putStrLn $ show r  
+      putStr $ showTTE $ viewEvent r
       putStrLn ""
diff --git a/src/CSPM/FiringRules/Verifier.hs b/src/CSPM/FiringRules/Verifier.hs
--- a/src/CSPM/FiringRules/Verifier.hs
+++ b/src/CSPM/FiringRules/Verifier.hs
@@ -1,8 +1,8 @@
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  CSPM.FiringRules.Verifier
--- Copyright   :  (c) Fontaine 2010
--- License     :  BSD
+-- Copyright   :  (c) Fontaine 2010 - 2011
+-- License     :  BSD3
 -- 
 -- Maintainer  :  fontaine@cs.uni-duesseldorf.de
 -- Stability   :  experimental
@@ -72,9 +72,7 @@
 viewProcAfter :: BL i => Rule i  -> Process i
 viewProcAfter =  (\(_,_,p) -> p) . viewRule
 
-{-|
-  Like 'viewRule' but returns 'Nothing' in case of an invalid proof tree.
--}
+-- | 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
@@ -240,11 +238,11 @@
     return (Seq p q, e, Seq p' q)
   NotHidden c pp -> do
     (p, e, p') <- viewRuleEvent pp
-    guard $ not $ member ty e c
+    not_in_Closure 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
+    not_in_Closure e c
     return (Sharing p c q, e, Sharing p' c q)
   NotShareR c p qq -> do
     (q, e, q') <- viewRuleEvent qq
@@ -283,10 +281,10 @@
     (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')
+  Rename rel visibleEvent pp -> do
+    (p, internalEvent, p') <- viewRuleEvent pp
+    guard $ isInRenaming ty rel internalEvent visibleEvent
+    return (Renaming rel p, visibleEvent, Renaming rel p')
   RenameNotInDomain rel pp -> do
     (p, e, p') <- viewRuleEvent pp
     guard $ not $ isInRenamingDomain ty e rel
@@ -302,6 +300,14 @@
     (q, e, q') <- viewRuleEvent qq
     guard $ not $ isInRenamingRange ty e rel
     return (LinkParallel rel p q, e, LinkParallel rel p q')
+  NoException c pp q -> do
+    (p, e, p') <- viewRuleEvent pp
+    not_in_Closure e c
+    return (Exception c p q, e, Exception c p' q)
+  ExceptionOccurs c p qq -> do
+    (q, e, q') <- viewRuleEvent qq
+    in_Closure e c
+    return (Exception c p q, e, q')
   where
     ty = (undefined :: i)
     in_Closure e c = guard $ member ty e c