CSPM-FiringRules 0.4.0.0 → 0.4.1.2

raw patch · 8 files changed

+54/−29 lines, 8 filesdep ~mtlPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: mtl

API changes (from Hackage documentation)

Files

• CSPM-FiringRules.cabal +7/−4
• src/CSPM/FiringRules/EnumerateEvents.hs +1/−1
• src/CSPM/FiringRules/FieldConstraintsSearch.hs +10/−10
• src/CSPM/FiringRules/Rules.hs +4/−4
• src/CSPM/FiringRules/Test/Test.hs +1/−1
• src/CSPM/FiringRules/Trace.hs +4/−4
• src/CSPM/FiringRules/Verifier.hs +5/−5
• src/CSPM/FiringRules/Version.hs +22/−0

@@ -1,5 +1,5 @@ name:                CSPM-FiringRules-version:             0.4.0.0+version:             0.4.1.2 synopsis:            Firing rules semantic of CSPM description:   This package contains functions for computing the transitions of a CSP process@@ -16,10 +16,10 @@ build-type:          Simple license:             BSD3 license-file:        LICENSE-author:              2010 - 2011 Marc Fontaine+author:              2010 - 2012 Marc Fontaine maintainer:          Marc Fontaine <fontaine@cs.uni-duesseldorf.de> stability:           experimental-tested-With:         GHC == 7.0.3+tested-With:         GHC == 7.4.1  cabal-Version:       >= 1.10 @@ -34,7 +34,7 @@     ,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)+    ,mtl >= 2.1 && < 2.2      Default-Language: Haskell2010   ghc-options: -funbox-strict-fields -O2 -Wall@@ -50,6 +50,9 @@     CSPM.FiringRules.Search     CSPM.FiringRules.Trace     CSPM.FiringRules.HelperClasses+    CSPM.FiringRules.Version+  Other-modules:+    Paths_CSPM_FiringRules    if flag(QuickCheck)     build-depends:

@@ -34,7 +34,7 @@ import Data.List as List  --- | Compute all possible transitions (via an event from Sigma) for a Process.+-- | Compute all possible transitions (via an event from Sigma) for a process. computeTransitions ::  forall i. BL i    => Sigma i -> Process i -> Search (Rule i) computeTransitions events p

@@ -204,7 +204,7 @@     ty = (undefined :: i)  {--fix one field in the event+Fix one field in the event. -} nextField :: forall i. BF i => RuleField i -> Field i -> Search (RuleField i) nextField rule field = case rule of@@ -246,9 +246,9 @@     fc c = closureStateNext ty c field  {--check constraints after last field and-convert RuleField to RuleEvent-we must check all constraints here !+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)@@ -549,8 +549,8 @@     ty = (undefined :: i)  {--we just enumerate everything-very inefficient !+We just enumerate everything,+very inefficient! -} mkLinkedRules :: forall i. BF i    => Event.RenamingRelation i@@ -569,7 +569,7 @@     rules :: [Event.Event i] -> Process i -> Search (Event.Event i, RuleEvent i)     rules s proc = do       e <- anyOf s-      -- use EnumNext instead!+      -- Use EnumNext instead!       computeNextE (Event.singleEventToClosureSet ty e) proc     ty = (undefined :: i) @@ -585,15 +585,15 @@   where rules = runSearch $ rulePattern events p  {--nextRepExtChoicePart may call nextField with invalid fields-nextRepExtChoicePart is only an approximation, it might return invalid rules+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+This is an error, we cannot rely on nextField to check the constraints nextField might return invalid rules -}   = if List.null newRules

@@ -8,8 +8,8 @@ -- Stability   :  experimental -- Portability :  GHC-only ----- This modules defines data types for (CSP) proof trees.--- A proof trees show that a particular transition is valid+-- This module defines data types for (CSP) proof trees.+-- A proof tree shows that a particular transition is valid -- with respect to the firing rules semantics. -- -- (For more info on the firing rule semantics @@ -40,7 +40,7 @@   | EventRule (RuleEvent i)   deriving Typeable --- | Is this a proof tree for a tau-transition+-- | Is this a proof tree for a tau-transition ? isTauRule :: Rule i -> Bool isTauRule (TauRule {}) = True isTauRule _ = False@@ -132,7 +132,7 @@ {- Not sure about this. Maybe this moves somewhere else or should be implemented differently.-This somehow complicated by the use of type-families +This is somehow complicated by the use of type families  -} deriving instance   (Show (Event i), Show (Prefix i), Show (Process i), Show (ExtProcess i)

@@ -10,7 +10,7 @@ -- -- QuickCheck tests for the proof tree generators in -- module CSPM.FiringRules.EnumerateEvents and--- and CSPM.FiringRules.FieldConstraints.+-- CSPM.FiringRules.FieldConstraints. -- These QuickCheck properties check for soundness, completeness -- and that both proof tree generators yield the same result. --

@@ -37,10 +37,10 @@   if null rules     then putStrLn "deadlock state"     else do-  sequence_ $ zipWith printTrans [0..] rules-  putStrLn "Select a Transition "-  i <- readLn-  trace events (viewProcAfter (rules !! i))+      sequence_ $ zipWith printTrans [0..] rules+      putStrLn "Select a Transition "+      i <- readLn+      trace events (viewProcAfter (rules !! i))   where     printTrans :: Int -> Rule i -> IO ()     printTrans nr r = do

@@ -12,11 +12,11 @@ -- -- '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+-- 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.--- 'viewRuleMaybe' construct an explicit representation of the transition.+-- 'viewRuleMaybe' constructs an explicit representation of the transition. -- -- 'viewRule' calls 'viewRuleMaybe' and throws an exception if -- the proof tree was not valid.@@ -317,15 +317,15 @@       parts <- forM l $ \x -> case x of         Left w -> return $ Left w         Right (c,r) -> do { v <- viewRuleEvent r; return $ Right (c,v) }---    check that all events are equal+--    Check that all events are equal.       let events = flip mapMaybe parts $ \x -> case x of             Left _ -> Nothing             Right (_,(_,e,_)) -> Just e       guard $ (not $ List.null events)           && (all (eventEq ty $ head events) $ tail events) {--check that if the event is in a closure set the corresponding process has-also taken part in the event+Check that if the event is in a closure set the corresponding process has+also taken part in the event. -}       let event = head events       guard $ flip all parts $ \x -> case x of

@@ -0,0 +1,22 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  CSPM.FiringRules.Version+-- Copyright   :  (c) Fontaine 2012+-- License     :  BSD3+--+-- Maintainer  :  fontaine@cs.uni-duesseldorf.de+-- Stability   :  experimental+-- Portability :  GHC-only+--+-- Reflect the version number of this library.+--+-----------------------------------------------------------------------------++module CSPM.FiringRules.Version+where+import Paths_CSPM_FiringRules+import Data.Version (Version)++-- | The version of the CSPM-FiringRules library.+firingRulesVersion :: Version+firingRulesVersion = version