diff --git a/CSPM-FiringRules.cabal b/CSPM-FiringRules.cabal
--- a/CSPM-FiringRules.cabal
+++ b/CSPM-FiringRules.cabal
@@ -1,5 +1,5 @@
 name:                CSPM-FiringRules
-version:             0.3.0.3
+version:             0.4.0.0
 synopsis:            Firing rules semantic of CSPM
 description:
   This package contains functions for computing the transitions of a CSP process
@@ -18,9 +18,8 @@
 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
+tested-With:         GHC == 7.0.3
 
 cabal-Version:       >= 1.10
 
@@ -30,7 +29,7 @@
 
 library
   build-Depends:
-     CSPM-CoreLanguage >= 0.2 && < 0.3
+     CSPM-CoreLanguage >= 0.3 && < 0.4
     ,tree-monad >=0.3 && < 0.4
     ,parallel-tree-search >=0.4 && < 0.5
     ,base >= 4.0 && < 5.0
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
@@ -111,6 +111,9 @@
       guard $ not $ isInRenamingRange ty event rel
       LinkEventR rel p <$> rp q
     )
+  Exception c p q -> if member ty event c
+    then ExceptionOccurs c p <$> rp q
+    else NoException c <$> rp p <*> pure q
   where
     rp = buildRuleEvent event
     ty = (undefined :: i)
@@ -183,6 +186,7 @@
       `mplus` (LinkTickL rel <$> tickTransitions p <*> pure q)
       `mplus` (LinkTickR rel p <$> tickTransitions q)
       `mplus` mkLinkedRules rel p q
+  Exception c p q -> mzero -- TODO
   where
     ty = (undefined :: i)
 
@@ -236,3 +240,4 @@
   Chaos _ -> mzero
   LinkParallel rel Omega Omega -> return $ LinkParallelTick rel
   LinkParallel _ _ _ -> mzero
+  Exception c p q -> mzero -- TODO
diff --git a/src/CSPM/FiringRules/FieldConstraintsSearch.hs b/src/CSPM/FiringRules/FieldConstraintsSearch.hs
--- a/src/CSPM/FiringRules/FieldConstraintsSearch.hs
+++ b/src/CSPM/FiringRules/FieldConstraintsSearch.hs
@@ -68,17 +68,18 @@
  | FChaos (ClosureState i)
  | FLinkEventL (Event.RenamingRelation i) (RuleField i) (Process i)
  | FLinkEventR (Event.RenamingRelation i) (Process i) (RuleField i)
+ | FNoException (ClosureState i) (RuleField i) (Process i)
+ | FExceptionOccurs (ClosureState i) (Process i) (RuleField i)
 
-rulePattern :: forall i. BF i => Event.EventSet i -> Process i -> Search (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)
+    -> joinRepExtChoiceParts
+         (initRepExtChoicePart events p)
+         (initRepExtChoicePart events q)
   InternalChoice _p _q -> mzero
   Interleave p q
     ->       (FInterleaveL <$> rp p <*> pure q)
@@ -106,7 +107,9 @@
   LinkParallel rel p q
     ->         (FLinkEventL rel <$> rp p <*> pure q)
        `mplus` (FLinkEventR rel p <$> rp q)
-
+  Exception c p q
+    ->         (FNoException (initClosure c) <$> rp p <*> pure q)
+       `mplus` (FExceptionOccurs (initClosure c) p <$> rp q)
   where
     ty = (undefined :: i)
     initClosure = closureStateInit ty
@@ -170,6 +173,12 @@
   FChaos c -> restrictField $ \e -> intersection ty e (closureFields c)
   FLinkEventL _ r _ -> propField r
   FLinkEventR _ _ r -> propField r
+  FNoException c r _ -> if closureState c == InClosure
+    then impossibleRule
+    else propField r
+  FExceptionOccurs c _ r -> if closureState c == NotInClosure
+    then impossibleRule
+    else propField r
   where
     restrictField :: (FieldSet i -> FieldSet i) -> PropM i ()
     restrictField fkt = do
@@ -205,7 +214,9 @@
   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)
+    -> 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
@@ -227,6 +238,8 @@
   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
+  FNoException c r q -> FNoException (fc c) <$> rec r <*> pure q
+  FExceptionOccurs c p r -> FExceptionOccurs (fc c) <$> pure p <*> rec r
   where
     rec r = nextField r field
     ty = (undefined :: i)
@@ -237,7 +250,8 @@
 convert RuleField to RuleEvent
 we must check all constraints here !
 -}
-lastField :: forall i. BF i => RuleField i -> Event.Event i -> Search (RuleEvent i)
+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
@@ -288,6 +302,12 @@
   FLinkEventR rel p r -> do
     guard $ not $ Event.isInRenamingRange ty event rel
     LinkEventR rel p <$> rec r
+  FNoException c r p -> do
+    guard_not_inClosure c
+    NoException (restoreClosure c) <$> rec r <*> pure p
+  FExceptionOccurs c p r -> do
+    guard_inClosure c
+    ExceptionOccurs (restoreClosure c) p <$> rec r
   where
     rec r = lastField r event
     ty = (undefined :: i)
@@ -306,14 +326,10 @@
 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)
+         (closureStateNext ty baseEvents chan)
          [chan] -- the accumulator for fields
          next
          (channelLen ty chan -1)
@@ -401,6 +417,7 @@
       `mplus` (LinkTickL rel <$> tickTransitions p <*> pure q)
       `mplus` (LinkTickR rel p <$> tickTransitions q)
       `mplus` mkLinkedRules rel p q
+  Exception c p q -> mzero -- TODO
 
 tickTransitions :: BL i => Process i -> Search (RuleTick i)
 tickTransitions proc = case proc of
@@ -431,6 +448,7 @@
   Chaos _ -> mzero
   LinkParallel rel Omega Omega -> return $ LinkParallelTick rel
   LinkParallel _ _ _ -> mzero
+  Exception c p q -> mzero -- TODO
 
 type RepAPProc i = (ClosureState i, Process i, [([Field.Field i], RuleEvent i)])
                                      -- why not do this field wise ^
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
@@ -15,26 +15,30 @@
 -- (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.
+-- We use three separate data types:
+-- 'RuleTau' stores a proof tree for a tau rule,
+-- 'RuleTick' stores a proof tree for a tick rule and
+-- 'RuleEvent' stores a proof tree for an event from Sigma.
 --
--- A list of the implemented firing rules (as pdf) is available via the package maintainer or
--- the web page.
+-- There is a one-to-one correspondence between
+-- each constructor of the data types 'RuleTau', 'RuleTick', 'RuleEvent'
+-- and one fireing rule.
 --
 -----------------------------------------------------------------------------
 
 {-# LANGUAGE FlexibleContexts, StandaloneDeriving, UndecidableInstances #-}
-module CSPM.FiringRules.Rules where
-
+{-# LANGUAGE DeriveDataTypeable #-}
+module CSPM.FiringRules.Rules
+where
 import CSPM.CoreLanguage
+import Data.Typeable
 
 -- | A sum-type for tau, tick and regular proof trees.
 data Rule i
   = TauRule (RuleTau i)
   | TickRule (RuleTick i)
   | EventRule (RuleEvent i)
+  deriving Typeable
 
 -- | Is this a proof tree for a tau-transition
 isTauRule :: Rule i -> Bool
@@ -75,6 +79,8 @@
   | LinkTauR (RenamingRelation i) (Process i) (RuleTau i)
   | LinkTickL (RenamingRelation i) (RuleTick i) (Process i)
   | LinkTickR (RenamingRelation i)  (Process i) (RuleTick i)
+  | ExceptionTauL (EventSet i) (RuleTau i) (Process i)
+  | ExceptionTauR (EventSet i) (Process i) (RuleTau i)
   | TraceSwitchOn (Process i) -- pseudo-tau for debugging
 
 -- | Representation of tick proof trees.
@@ -92,7 +98,7 @@
   | RenamingTick (RenamingRelation i) (RuleTick i)
   | LinkParallelTick (RenamingRelation i)
 
--- | Representation of regular proof trees (i.e. non-tau and non-tick transitions)
+-- | Representation of regular proof trees.
 data RuleEvent i
   = HPrefix (Event i) (Prefix i)
   | ExtChoiceL (RuleEvent i) (Process i)
@@ -133,12 +139,12 @@
   ,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 (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 (Event i), Ord (Prefix i), Ord (Process i), Ord (ExtProcess i)
+  ,Ord (EventSet i), Ord (RenamingRelation i) )
   => Ord (RuleEvent i)
 
 
diff --git a/src/CSPM/FiringRules/Test/Gen.hs b/src/CSPM/FiringRules/Test/Gen.hs
--- a/src/CSPM/FiringRules/Test/Gen.hs
+++ b/src/CSPM/FiringRules/Test/Gen.hs
@@ -69,6 +69,7 @@
   ,(10, binProc Seq)
   ,(10, liftM2 Hide (arbitraryEventSet ty) arbitrary)
   ,(30, genProcess 0)
+  ,(10, liftM3 Exception (arbitraryEventSet ty) subProcess subProcess)
   ]
   where
     binProc c = liftM2 c subProcess subProcess
@@ -208,6 +209,8 @@
          (allEvents ty)
          (delete ty event (allEvents ty))
        LinkEventR (renamingFromList ty rel) <$> p <*> r
+    ,f10 $ NoException <$> setWithoutEvent <*> r <*> p
+    ,f10 $ ExceptionOccurs <$> setWithEvent <*> p <*> r
     ]
   where
     p :: Gen (Process i)
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
@@ -8,9 +8,11 @@
 -- Stability   :  experimental
 -- Portability :  GHC-only
 --
--- QuickCheck tests for the modules CSPM.FiringRules.EnumerateEvents
+-- QuickCheck tests for the proof tree generators in
+-- module CSPM.FiringRules.EnumerateEvents and
 -- and CSPM.FiringRules.FieldConstraints.
--- We check for soundness, completeness and that both approaches yield the same result. 
+-- These QuickCheck properties check for soundness, completeness
+-- and that both proof tree generators yield the same result.
 --
 -----------------------------------------------------------------------------
 
@@ -78,12 +80,6 @@
     (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
@@ -106,13 +102,14 @@
     (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)
+    (computeNext_eq_EnumRuleEvent :: RuleEvent M2 -> Bool)
   quickCheck $ QC.label "enum Tau rules == symRuleTau"
-    (korrect_symTauRules :: RuleTau M2 -> Bool)
--}
+    (fieldTau :: RuleTau M2 -> Bool)
+  quickCheck $ QC.label "enum Tick rules == symRuleTick"
+    (fieldTick :: RuleTick M2 -> Bool)
 
+
 sound_EnumRuleTick :: CSP1 i => RuleTick i -> Bool
 sound_EnumRuleTick r
   = all (checkRule proc . TickRule) $ EnumNext.tickTransitions proc
@@ -149,21 +146,6 @@
   = 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"
@@ -180,8 +162,7 @@
     (fieldTau :: RuleTau M2 -> Bool)
 
   quickCheck $ QC.label "FieldNext.tickTransitions == EnumNext.tickTransitions"
-    (fieldTick :: RuleTau M2 -> Bool)
-
+    (fieldTick :: RuleTick M2 -> Bool)
 
 sound_computeNext :: forall i. CSP2 i => RuleEvent i -> Bool
 sound_computeNext r
@@ -211,9 +192,9 @@
     ruleSet2 = Set.fromList $ FieldNext.tauTransitions proc
     proc = viewProcBefore $ TauRule rule
 
-fieldTick :: forall i. CSP2 i => RuleTau i -> Bool
+fieldTick :: forall i. CSP2 i => RuleTick i -> Bool
 fieldTick rule = ruleSet1 == ruleSet2
   where
     ruleSet1 = Set.fromList $ EnumNext.tickTransitions proc
     ruleSet2 = Set.fromList $ FieldNext.tickTransitions proc
-    proc = viewProcBefore $ TauRule rule
+    proc = viewProcBefore $ TickRule rule
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
@@ -10,22 +10,18 @@
 --
 -- 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.
+-- 'viewRuleMaybe' checks that a proof tree is valid
+-- with respect to the firing rules semantics of CSPM.
+-- It checks, that the proof tree 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.
+-- 'viewRuleMaybe' construct an explicit representation of the transition.
 --
+-- 'viewRule' calls 'viewRuleMaybe' and throws an exception if
+-- the proof tree was not valid.
+-- The proof tree generators in this package only generate valid proof trees.
+-- 'viewRule' is used to check that assertion.
 -----------------------------------------------------------------------------
 {-# LANGUAGE ScopedTypeVariables #-}
 
@@ -51,8 +47,10 @@
 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').
+  This function constructs an explict representation of the transition
+  from the proof tree of the transition.
+  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)
@@ -85,7 +83,7 @@
     Just (p, e, p') -> Just (p, SEvent e, p')
     Nothing -> Nothing
 
--- | Used for testing.
+-- | Check a tau rule.
 viewRuleTau :: forall i. BL i => RuleTau i -> Maybe (Process i, Process i)
 viewRuleTau rule = case rule of
   ExtChoiceTauL pp q -> do
@@ -185,7 +183,7 @@
     return (LinkParallel rel p q, LinkParallel rel p' q')
   TraceSwitchOn p -> return (p, p)
 
--- | Used for testing.
+-- | Check a tick rule.
 viewRuleTick :: BL i => RuleTick i -> Maybe (Process i)
 viewRuleTick rule = case rule of
   InterleaveOmega -> return (Interleave Omega Omega)
@@ -215,8 +213,9 @@
   LinkParallelTick rel
     -> return $ LinkParallel rel Omega Omega
 
--- | Used for testing.
-viewRuleEvent :: forall i. BL i => RuleEvent i -> Maybe (Process i, Event i, Process i)
+-- | Check a regular rule
+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
@@ -313,7 +312,7 @@
     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 :: [EventRepAPart i] -> Maybe (Process i,Event i,Process i)
     checkRepAParallel l = do
       parts <- forM l $ \x -> case x of
         Left w -> return $ Left w