CSPM-cspm 0.4.0.0 → 0.4.4.0
raw patch · 10 files changed
+319/−50 lines, 10 filesdep +CSPM-ToPrologdep +prettydep +transformersdep ~CSPM-CoreLanguagedep ~CSPM-FiringRulesdep ~CSPM-Frontend
Dependencies added: CSPM-ToProlog, pretty, transformers
Dependency ranges changed: CSPM-CoreLanguage, CSPM-FiringRules, CSPM-Frontend, cmdargs, containers, parallel
Files
- CSPM-cspm.cabal +30/−18
- LICENSE +1/−1
- src/CSPM/Assert.hs +97/−0
- src/CSPM/LTS/Deadlock.hs +69/−0
- src/CSPM/LTS/LTS.hs +2/−2
- src/CSPM/LTS/MkLtsPar.hs +7/−6
- src/CSPM/LTS/ToCsp.hs +6/−1
- src/CSPM/LTS/ToDot.hs +2/−0
- src/CSPM/LTS/Utils.hs +19/−0
- src/Main.hs +86/−22
CSPM-cspm.cabal view
@@ -1,11 +1,11 @@ Name: CSPM-cspm-Version: 0.4.0.0+Version: 0.4.4.0 Synopsis: cspm command line tool for analyzing CSPM specifications. Description: cspm is a small command line tool for analyzing CSPM specifications.- It supports four modes of operation ('eval', 'trace', 'dot' and 'fdr')- and can be called for example as:+ It supports serveral modes of operation.+ For example as: . * 'cspm --help' -> print a help message. .@@ -13,12 +13,16 @@ . * 'cspm trace spec.csp' -> interactively trace a process. .+ * 'cspm assert spec.csp' -> check the assertions of a specification.+ . * 'cspm dot spec.csp' -> compute the labeled transition system of a process and dump it as dot-file. . * 'cspm fdr spec.csp' -> compute the LTS and dump it a fdr script suitable for refinement checking. .+ * 'cspm toprolog spec.csp' -> generate prolog output for ProB+ . cspm is not a full featured FDR replacement. The main purpose of cspm is to show how the different CSPM-packages work together. LTS computation can demonstrate nice speed-ups on multi-core machines.@@ -28,35 +32,43 @@ License: BSD3 category: Language,Formal Methods,Concurrency License-File: LICENSE-Author: 2010 Marc Fontaine+Author: Marc Fontaine Maintainer: Marc Fontaine <fontaine@cs.uni-duesseldorf.de> Homepage: http://www.stups.uni-duesseldorf.de/~fontaine/csp-cabal-Version: >= 1.8+cabal-Version: >= 1.10 build-type: Simple-Tested-With: GHC == 6.12.3-Stability: unstable+Tested-With: GHC == 7.0.2+Stability: experimental Executable cspm Build-Depends:- CSPM-Frontend >= 0.4 && < 0.5- ,CSPM-CoreLanguage >= 0.1 && < 0.2- ,CSPM-FiringRules >= 0.1 && < 0.2+ CSPM-Frontend >= 0.6 && < 0.7+ ,CSPM-CoreLanguage >= 0.2 && < 0.3+ ,CSPM-FiringRules >= 0.3 && < 0.4 ,CSPM-Interpreter >= 0.4 && < 0.5- ,cmdargs >= 0.3 && < 0.4- ,containers >= 0.3 && < 0.4- ,parallel >=2.2 && < 2.3+ ,CSPM-ToProlog >= 0.3 && < 0.4+ ,cmdargs == 0.6.8+ ,containers >= 0.4 && < 0.5+ ,parallel >=3.1 && < 3.2 ,base >= 4.0 && < 5.0+ ,pretty >=1.0 && <1.1+ ,transformers >=0.2 && <0.3 - - GHC-Options: -threaded -funbox-strict-fields -O2 -Wall -fno-warn-orphans- Extensions:- DeriveDataTypeable, StandaloneDeriving- TypeSynonymInstances, RecordWildCards+ GHC-Options:+ -threaded -funbox-strict-fields -O2 -Wall -fno-warn-orphans +-- -funbox-strict-fields -O2 -Wall -fno-warn-orphans+ -rtsopts+ Default-Language: Haskell2010+ Other-Extensions:+ DeriveDataTypeable, StandaloneDeriving, TypeSynonymInstances, RecordWildCards Hs-Source-Dirs: src Main-is: Main.hs Other-modules:+ CSPM.Assert CSPM.LTS.LTS CSPM.LTS.MkLtsPar CSPM.LTS.ToCsp CSPM.LTS.ToDot+ CSPM.LTS.Utils+ CSPM.LTS.Deadlock
LICENSE view
@@ -1,4 +1,4 @@-Copyright (c) Marc Fontaine 2007-2009+Copyright (c) Marc Fontaine 2007-2011 All rights reserved.
+ src/CSPM/Assert.hs view
@@ -0,0 +1,97 @@+----------------------------------------------------------------------------+-- |+-- Module : CSPM.Assert+-- Copyright : (c) Fontaine 2011+-- License : BSD3+--+-- Maintainer : fontaine@cs.uni-duesseldorf.de+-- Stability : experimental+-- Portability : GHC-only+--+module CSPM.Assert+ (+ checkFileAsserts+ ,formatAssertResults+ )+where++import Language.CSPM.AST as AST+import Language.CSPM.AstUtils+import Language.CSPM.Frontend+import Language.CSPM.PrettyPrinter ()++import CSPM.Interpreter.Eval+import CSPM.Interpreter.Types (Env)+import CSPM.Interpreter (prepareAST)+import CSPM.Interpreter.CoreInstances ()++import CSPM.LTS.Deadlock (findDeadlock)++import Control.Exception.Base (evaluate)+import Text.PrettyPrint+import Data.Either++type AssertResult = Either Doc Doc++checkFileAsserts :: FilePath -> Bool -> IO [AssertResult]+checkFileAsserts src _verbose = do+ astRaw <- parseFile src+ (astR2,_) <- eitherToExc $ renameModule astRaw+ let+ astNew = prepareAST astR2+ env = evalModule $ astNew+ mapM (checkEnvAssert env) $ getModuleAsserts astNew++formatAssertResults :: [AssertResult] -> Doc+formatAssertResults results+ = vcat+ [+ text "Asserts pass :" <+> (int $ length passed)+ ,nest 4 $ vcat passed+ ,text "Asserts fail :" <+> (int $ length failed)+ ,nest 4 $ vcat failed+ ,case (length passed, length failed) of+ (0,0) -> text "No asserts found !"+ (_,0) -> text "All asserts pass !"+ (0,_) -> text "All asserts fail !"+ (_,_) -> text "Some asserts fail !"+ ]+ where+ (failed,passed) = partitionEithers results++checkEnvAssert :: Env -> LAssertDecl -> IO AssertResult+checkEnvAssert env ass = case unLabel ass of+ AssertBool expr -> if runEM (evalBool expr) env+ then return $ Right $ text "pass :" <+> pp ass+ else return $ Left $ text "fail :" <+> pp ass+ AssertRefine {}+ -> notSupported $ text "refinement not supported yet :" <+> pp ass+ AssertTauPrio {}+ -> notSupported $ text "tau priority assert not supported yet :" <+> pp ass+ AssertModelCheck _negated _expr _property (Just ext)+ -> notSupported $ text "model checking fdr extensions :" <+> pp ass <+> pp ext+ AssertModelCheck negated expr property Nothing -> do+ let+ sigma = getSigma env+ proc = runEM (evalProcess expr) env+ res <- case unLabel property of+ DeadlockFree -> checkDeadlockFree sigma proc+ Deterministic+ -> notSupported (text "assert not supported yet :" <+> pp ass)+ LivelockFree+ -> notSupported (text "assert not supported yet :" <+> pp ass)+ return $ if negated+ then either Right Left res+ else res++ where+ notSupported = return . Left++ checkDeadlockFree sigma proc = do+ putStrLn "running BFS for deadlock state"+ res <- evaluate $ findDeadlock sigma proc+ case res of+ Nothing -> return $ Right $ pp ass <+> text " --- no deadlock found"+ Just path+ -> return $ Left $ pp ass <+> text " -- deadlock found: path-length :"+ <+> (int $ length path)
+ src/CSPM/LTS/Deadlock.hs view
@@ -0,0 +1,69 @@+----------------------------------------------------------------------------+-- |+-- Module : CSPM.LTS.Deadlock+-- Copyright : (c) Fontaine 2011+-- License : BSD+--+-- Maintainer : Fontaine@cs.uni-duesseldorf.de+-- Stability : experimental+-- Portability : GHC-only+--+-- Search the state-space of a CSPM process for deadlock states+----------------------------------------------------------------------------+module CSPM.LTS.Deadlock+(+ findDeadlock+)+where++import CSPM.CoreLanguage+import CSPM.FiringRules.Rules+import CSPM.FiringRules.Verifier (viewProcAfter)+import CSPM.FiringRules.FieldConstraints (computeTransitions)++import CSPM.Interpreter (INT, Digest)+import CSPM.Interpreter.Hash++import Control.Monad+import Control.Monad.Trans.State+import Control.Monad.Trans.Class++import qualified Data.Set as Set+import Data.Set (Set)++type Path = ([Rule INT], Process INT)++type BM a = StateT (Set Digest) (Either [Rule INT]) a++-- | Search the statespace of a process for deadlock states.+-- returns the shortes trace to a deadlock.+findDeadlock ::+ Sigma INT -- ^ Sigma+ -> Process INT -- ^ the Process+ -> Maybe [Rule INT] -- a trace to a deadlock state (of Nothing)++findDeadlock sigma process+ = case evalStateT (wave [([],process)]) Set.empty of+ Right () -> Nothing+ Left p -> Just p+ where+ wave :: [Path] -> BM ()+ wave [] = return ()+ wave w = mapM expandPath w >>= wave . concat++ expandPath :: Path -> BM [Path]+ expandPath (path, node) = do+ t <- isOldNode node+ if t then return []+ else do+ let rules = computeTransitions sigma node+ when (null rules) $ lift $ Left $ reverse path+ return $ map (\r -> (r:path , viewProcAfter r)) rules++ isOldNode :: Process INT -> BM Bool+ isOldNode n = do+ let h = hash n+ s <- get+ let res = Set.member h s+ put $ Set.insert h s+ return res
src/CSPM/LTS/LTS.hs view
@@ -2,8 +2,8 @@ ---------------------------------------------------------------------------- -- | -- Module : CSPM.LTS.LTS--- Copyright : (c) Fontaine 2009--- License : BSD+-- Copyright : (c) Fontaine 2009 - 2011+-- License : BSD3 -- -- Maintainer : Fontaine@cs.uni-duesseldorf.de -- Stability : experimental
src/CSPM/LTS/MkLtsPar.hs view
@@ -1,7 +1,7 @@ ---------------------------------------------------------------------------- -- | -- Module : CSPM.LTS.mkLtsPar--- Copyright : (c) Fontaine 2010+-- Copyright : (c) Fontaine 2010 - 2011 -- License : BSD -- -- Maintainer : Fontaine@cs.uni-duesseldorf.de@@ -21,7 +21,6 @@ import CSPM.FiringRules.Verifier (viewProcAfter) import CSPM.FiringRules.FieldConstraints (computeTransitions) ---import CSPM.Interpreter as Interpreter import CSPM.Interpreter (INT) import CSPM.LTS.LTS@@ -32,8 +31,8 @@ import Data.Set (Set) import Data.List as List --- | Compute the-mkLtsPar :: Sigma INT-> Process INT -> LTS+-- | Compute the LTS of a Process.+mkLtsPar :: Sigma INT -> Process INT -> LTS mkLtsPar events process = wave [mkLtsNode process] Map.empty where@@ -42,7 +41,6 @@ wave w lts = wave (Set.toList uniqueProcesses) newLts where !transitions = parRules $ map processNext w- processes = concatMap (\(_,_,r) -> r) transitions processNext :: LtsNode -> (LtsNode, [Rule INT], [LtsNode]) processNext p = (p, rules, map (mkLtsNode . viewProcAfter) rules)@@ -61,10 +59,13 @@ then s else p `Set.insert` s + processes = concatMap (\(_,_,r) -> r) transitions++ parRules :: [(LtsNode, [Rule INT], [LtsNode ])] -> [(LtsNode, [Rule INT], [LtsNode ])]- parRules = withStrategy $ parList $ seqTriple r0 (parList rwhnf) (parList rwhnf)+ parRules = withStrategy $ parList $ evalTuple3 r0 (parList rseq) (parList rseq) {- semantic : parRules = id -}
src/CSPM/LTS/ToCsp.hs view
@@ -32,7 +32,12 @@ import Data.List as List import Control.Monad -ltsToCsp :: Process INT -> LTS -> String -> IO ()+-- | Dump an LTS to File in a format suitable for reloading it with FDR.+ltsToCsp ::+ Process INT -- ^ the intial process+ -> LTS -- ^ the LTS+ -> FilePath -- ^ output filename+ -> IO () ltsToCsp process lts fname = do file <- openFile fname WriteMode let dup = hPutStrLn file
src/CSPM/LTS/ToDot.hs view
@@ -33,6 +33,8 @@ -- todo : this is all pure no need for IO -- todo : use dot-libray++-- | Dump a LTS as a .dot-file. mkDotFile :: FilePath -> LTS -> IO () mkDotFile filename lts = do file <- openFile filename WriteMode
+ src/CSPM/LTS/Utils.hs view
@@ -0,0 +1,19 @@+----------------------------------------------------------------------------+-- |+-- Module : CSPM.LTS.Utils+-- Copyright : (c) Fontaine 2011+-- License : BSD3+-- +-- Maintainer : Fontaine@cs.uni-duesseldorf.de+-- Stability : experimental+-- Portability : GHC-only+--+-- Compute the labled transition system of a process.+----------------------------------------------------------------------------+module CSPM.LTS.Utils+where++import CSPM.LTS.LTS++import qualified Data.Map as Map+import Data.Maybe
src/Main.hs view
@@ -1,7 +1,7 @@ ---------------------------------------------------------------------------- -- | -- Module : Main--- Copyright : (c) Fontaine 2010+-- Copyright : (c) Fontaine 2010-2011 -- License : BSD -- -- Maintainer : Fontaine@cs.uni-duesseldorf.de@@ -13,6 +13,7 @@ {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE RecordWildCards #-}+{-# OPTIONS_GHC -fno-cse #-} module Main where@@ -25,10 +26,13 @@ import CSPM.LTS.MkLtsPar (mkLtsPar) import CSPM.LTS.ToCsp (ltsToCsp) import CSPM.LTS.ToDot (mkDotFile)+import CSPM.Assert (checkFileAsserts, formatAssertResults) import Language.CSPM.Frontend (LexError(..),ParseError(..),RenameError(..)) import Language.CSPM.Token (pprintAlexPosn, Token(..)) +import Language.CSPM.TranslateToProlog (translateToProlog)+ import System.Console.CmdArgs import Control.Exception import System.Exit (exitSuccess, exitFailure)@@ -47,30 +51,54 @@ -- definition of the command line parser argParser :: Mode (CmdArgs Args)-argParser = cmdArgsMode $ modes [evalMode, traceMode, fdrMode, dotMode ]+argParser = cmdArgsMode+ $ modes [evalMode, traceMode, assertMode, fdrMode, dotMode, toPrologMode] &= program "cspm"- &= summary "cspm command line utility V0.4.0.0"+ &= summary "cspm command line utility V0.4.3.0" -data Args = - Eval {+data Args =+ ToProlog {+ inFile :: FilePath+ ,outFile :: FilePath+ }+ |Eval { evalContext :: Maybe FilePath ,evalExpr :: String+ ,verbose :: Bool } |Trace { src :: FilePath ,entry :: String+ ,verbose :: Bool } |FDR { src :: FilePath ,entry :: String ,out :: Maybe FilePath+ ,verbose :: Bool } |Dot { src :: FilePath ,entry :: String ,out :: Maybe FilePath+ ,verbose :: Bool+ }+ |Assert {+ src :: FilePath+ ,verbose :: Bool } deriving (Data,Typeable,Show,Eq) ++toPrologMode :: Args+toPrologMode = ToProlog {+ inFile = def+ &= argPos 0+ &= typ "File"+ ,outFile = def+ &= argPos 1+ &= typ "File"+ } &= groupname "translate a CSP-M file to Prolog"+ evalMode :: Args evalMode = Eval { evalContext = def@@ -78,27 +106,33 @@ &= typFile &= explicit &= name "s" &= name "src" ,evalExpr = def - &= help "the expression to evaluate"- &= typ "EXPR" &= argPos 0- } &= program "evaluate an expression"+ &= typ "EXPR"+-- &= help "the expression to evaluate"+ ,verbose = def+ &= help "verbose"+ &= name "v" &= name "verbose"+ } &= groupname "evaluate an expression" traceMode :: Args traceMode = Trace { src = def- &= help "CSPM specification"- &= typFile &= argPos 0+ &= typFile+-- &= help "CSPM specification" ,entry = "MAIN" &= help "optional: the main process" &= typ "PROCESS" &= explicit &= name "main" &= name "m"- } &= program "trace a process"+ ,verbose = def+ &= help "verbose"+ &= name "v" &= name "verbose"+ } &= groupname "trace a process" fdrMode :: Args fdrMode = FDR { src = def- &= help "CSPM specification"+-- &= help "CSPM specification" &= typFile &= argPos 0 ,entry = "MAIN"@@ -109,12 +143,15 @@ &= help "optional: name of the generated fdr file" &= typFile &= explicit &= name "out" &= name "o"- } &= program "compute the LTS and dump it as fdr script"+ ,verbose = def+ &= help "verbose"+ &= name "v" &= name "verbose"+ } &= groupname "compute the LTS and dump it as fdr script" dotMode :: Args dotMode = Dot { src = def- &= help "CSPM specification"+-- &= help "CSPM specification" &= typFile &= argPos 0 ,entry = "MAIN"@@ -125,19 +162,37 @@ &= help "optional: name of the generated dot file" &= typFile &= explicit &= name "out" &= name "o"- } &= program "compute the LTS and dump it as dot graph"+ ,verbose = def+ &= help "verbose"+ &= name "v" &= name "verbose"+ } &= groupname "compute the LTS and dump it as dot graph" +assertMode :: Args+assertMode = Assert {+ src = def+ &= typFile+ &= argPos 0+ ,verbose = def+ &= help "verbose"+ &= name "v" &= name "verbose"+ } &= groupname "check the assert declarations of a specification"++ -- execute the command according to command line arguments execCommand :: Args -> IO ()+execCommand ToProlog {..} = translateToProlog inFile outFile execCommand Eval {..} = do- isVerbose <- isLoud- (val,_) <- evalEnv isVerbose evalContext evalExpr+ (val,_) <- evalEnv verbose evalContext evalExpr print val execCommand Trace {..} = do (proc,sigma) <- mkProcess src entry trace sigma proc +execCommand Assert {..} = do+ results <- checkFileAsserts src verbose+ putStrLn $ show $ formatAssertResults results+ execCommand FDR {..} = do (proc,sigma) <- mkProcess src entry let@@ -158,12 +213,12 @@ mkDotFile outFile lts return () -mkProcess :: FilePath -> String -> IO (Process, ClosureSet)+mkProcess :: FilePath -> String -> IO (Process, Sigma) mkProcess file expr = do isVerbose <- isLoud (proc, env) <- evalEnv isVerbose (Just file) expr case proc of- VProcess p -> return (p, getAllEvents env)+ VProcess p -> return (p, getSigma env) _ -> error "type-error : entry-point is not a process" -- example exception handler@@ -173,9 +228,10 @@ where allHandler = [ Handler lexError, Handler parseError, Handler renameError+ ,Handler interpreterError ,Handler errCall- ,Handler async -- pressing CTRL c- ,Handler ioExc -- file not found etc+ ,Handler async+ ,Handler ioExc ,Handler someExc ] lexError :: LexError -> IO () lexError LexError {..} = do@@ -196,6 +252,14 @@ putStrLn $ renameErrorMsg putStrLn $ show renameErrorLoc exitFailure+ interpreterError :: InterpreterError -> IO ()+ interpreterError err = do+ putStrLn "InterpreterError :"+ putStrLn $ errMsg err+ putStrLn $ show $ errLoc err+ putStrLn ""+ putStrLn $ show err+ exitFailure ioExc :: IOException -> IO () ioExc err = do putStrLn $ show err@@ -207,7 +271,7 @@ exitFailure async :: AsyncException -> IO () async err = do- putStrLn "AsyncException (Pressing CRTL C ?)"+ putStrLn "AsyncException (Pressing CRTL-C ?)" putStrLn $ show err exitFailure someExc :: SomeException -> IO ()