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.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 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: 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 @@ -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 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 @@ -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 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 @@ -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) 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 @@ -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. -- 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 @@ -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 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 @@ -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 diff --git a/src/CSPM/FiringRules/Version.hs b/src/CSPM/FiringRules/Version.hs new file mode 100644 --- /dev/null +++ b/src/CSPM/FiringRules/Version.hs @@ -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