packages feed

CSPM-FiringRules 0.3.0.3 → 0.4.0.0

raw patch · 7 files changed

+93/−82 lines, 7 filesdep ~CSPM-CoreLanguagePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: CSPM-CoreLanguage

API changes (from Hackage documentation)

+ CSPM.FiringRules.Rules: ExceptionTauL :: (EventSet i) -> (RuleTau i) -> (Process i) -> RuleTau i
+ CSPM.FiringRules.Rules: ExceptionTauR :: (EventSet i) -> (Process i) -> (RuleTau i) -> RuleTau i
+ CSPM.FiringRules.Rules: instance Typeable1 Rule

Files

CSPM-FiringRules.cabal view
@@ -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
src/CSPM/FiringRules/EnumerateEvents.hs view
@@ -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
src/CSPM/FiringRules/FieldConstraintsSearch.hs view
@@ -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 ^
src/CSPM/FiringRules/Rules.hs view
@@ -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)
src/CSPM/FiringRules/Test/Gen.hs view
@@ -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)
src/CSPM/FiringRules/Test/Test.hs view
@@ -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
src/CSPM/FiringRules/Verifier.hs view
@@ -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