CSPM-cspm 0.3.0.0 → 0.4.0.0
raw patch · 3 files changed
+164/−88 lines, 3 filesdep ~cmdargs
Dependency ranges changed: cmdargs
Files
- CSPM-cspm.cabal +25/−13
- src/CSPM/LTS/ToCsp.hs +4/−4
- src/Main.hs +135/−71
CSPM-cspm.cabal view
@@ -1,18 +1,28 @@ Name: CSPM-cspm-Version: 0.3.0.0+Version: 0.4.0.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:- 1) cspm eval -> evaluate an expression.- 2) cspm trace -> interactively trace a process.- 3) cspm dot -> compute the labeled transition system of a process and dump it as dot-file.- 4) cspm fdr -> compute the LTS and dump it a fdr script suitable for refinement checking.+ It supports four modes of operation ('eval', 'trace', 'dot' and 'fdr')+ and can be called for example as:+ .+ * 'cspm --help' -> print a help message.+ .+ * 'cspm eval '3+4'' -> evaluate an expression.+ .+ * 'cspm trace spec.csp' -> interactively trace a process.+ .+ * '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 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 (if the LTS- contains enough branching).+ LTS computation can demonstrate nice speed-ups on multi-core machines.+ Try for example 'cspm +RTS -N7 -RTS fdr spec.csp' to use 7 cores. License: BSD3@@ -21,8 +31,10 @@ Author: 2010 Marc Fontaine Maintainer: Marc Fontaine <fontaine@cs.uni-duesseldorf.de> Homepage: http://www.stups.uni-duesseldorf.de/~fontaine/csp-cabal-Version: >= 1.6+cabal-Version: >= 1.8 build-type: Simple+Tested-With: GHC == 6.12.3+Stability: unstable Executable cspm Build-Depends:@@ -30,16 +42,16 @@ ,CSPM-CoreLanguage >= 0.1 && < 0.2 ,CSPM-FiringRules >= 0.1 && < 0.2 ,CSPM-Interpreter >= 0.4 && < 0.5- ,cmdargs >= 0.1 && < 0.2+ ,cmdargs >= 0.3 && < 0.4 ,containers >= 0.3 && < 0.4 ,parallel >=2.2 && < 2.3 ,base >= 4.0 && < 5.0 - GHC-Options: -threaded -funbox-strict-fields -O2 -Wall+ GHC-Options: -threaded -funbox-strict-fields -O2 -Wall -fno-warn-orphans Extensions:- DeriveDataTypeable, StandaloneDeriving, FlexibleInstances, FlexibleContexts- TypeSynonymInstances+ DeriveDataTypeable, StandaloneDeriving+ TypeSynonymInstances, RecordWildCards Hs-Source-Dirs: src Main-is: Main.hs
src/CSPM/LTS/ToCsp.hs view
@@ -33,14 +33,14 @@ import Control.Monad ltsToCsp :: Process INT -> LTS -> String -> IO ()-ltsToCsp init lts fname = do+ltsToCsp process lts fname = do file <- openFile fname WriteMode let dup = hPutStrLn file -- dup $ "channel " ++ ( concat $ intersperse "," $ map showEvent $ getSigma trans) -- let adjList = groupBy eqByFrom $ sortBy compareByFrom trans -- dup $ "channel intTau,intTick"- dup $ "GPINIT = " ++ procToCsp init -- ++ "\\{intTau,intTick}"+ dup $ "GPINIT = " ++ procToCsp process -- ++ "\\{intTau,intTick}" forM_ (Map.assocs lts) $ dumpState file hClose file where@@ -66,8 +66,8 @@ dup ")" dup ")\n" - isTauRule (TauRule {}) = True- isTauRule _ = False+-- isTauRule (TauRule {}) = True+-- isTauRule _ = False showTrans :: Rule INT -> String showTrans r = eventToCsp trans ++ procToCsp to
src/Main.hs view
@@ -12,11 +12,11 @@ ---------------------------------------------------------------------------- {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE RecordWildCards #-} module Main where -import System.Console.CmdArgs hiding (args) import CSPM.Interpreter import CSPM.Interpreter.Test.CLI (evalEnv) import CSPM.FiringRules.Trace (trace)@@ -26,7 +26,13 @@ import CSPM.LTS.ToCsp (ltsToCsp) import CSPM.LTS.ToDot (mkDotFile) +import Language.CSPM.Frontend (LexError(..),ParseError(..),RenameError(..))+import Language.CSPM.Token (pprintAlexPosn, Token(..)) +import System.Console.CmdArgs+import Control.Exception+import System.Exit (exitSuccess, exitFailure)+ instance EqOrd INT instance CSP1 INT instance CSP2 INT@@ -34,11 +40,20 @@ -- | main-funtion for the command line. main :: IO ()-main = cmdArgs "CSPM Tools V0.1" modes >>= execCommand- where modes = [evalMode, traceMode, fdrMode, dotMode ]+main = do+ arguments <- cmdArgsRun argParser+ handleException $ execCommand arguments+ exitSuccess++-- definition of the command line parser+argParser :: Mode (CmdArgs Args)+argParser = cmdArgsMode $ modes [evalMode, traceMode, fdrMode, dotMode ]+ &= program "cspm"+ &= summary "cspm command line utility V0.4.0.0"+ data Args = Eval {- evalContext :: FilePath+ evalContext :: Maybe FilePath ,evalExpr :: String } |Trace {@@ -48,98 +63,98 @@ |FDR { src :: FilePath ,entry :: String- ,out :: FilePath+ ,out :: Maybe FilePath } |Dot { src :: FilePath ,entry :: String- ,out :: FilePath+ ,out :: Maybe FilePath } deriving (Data,Typeable,Show,Eq) -srcArg :: Attrib-srcArg- = text "CSPM specification"- & typFile- & empty "" - & argPos 0--mainArg :: Attrib-mainArg- = text "optional: the main process" - & typ "PROCESS"- & empty "MAIN"- & explicit & flag "main" & flag "m"--outArg :: Attrib-outArg- = text "optional: name of the output file"- & typFile- & explicit & flag "out" & flag "o"---evalMode :: Mode Args-evalMode = mode $ Eval {+evalMode :: Args+evalMode = Eval { evalContext = def- &= text "optional: CSPM specification to load into context"- & typFile - & empty "" & explicit & flag "src"+ &= help "optional: CSPM specification to load into context"+ &= typFile + &= explicit &= name "s" &= name "src" ,evalExpr = def - &= text "the expression to evaluate"- & typ "EXPR"- & argPos 0- } &= prog "eval"- & text "evaluate an expression"--traceMode :: Mode Args-traceMode = mode $ Trace {- src = def &= srcArg- ,entry = "MAIN" &= mainArg- } &= prog "trace"- & text "trace a process"+ &= help "the expression to evaluate"+ &= typ "EXPR"+ &= argPos 0+ } &= program "evaluate an expression" -fdrMode :: Mode Args-fdrMode = mode $ FDR {- src = def &= srcArg- ,entry = "MAIN" &= mainArg- ,out = def &= outArg- } &= prog "fdr"- & text "compute the LTS and dump it as fdr script"+traceMode :: Args+traceMode = Trace {+ src = def+ &= help "CSPM specification"+ &= typFile+ &= argPos 0+ ,entry = "MAIN"+ &= help "optional: the main process" + &= typ "PROCESS"+ &= explicit &= name "main" &= name "m"+ } &= program "trace a process" -dotMode :: Mode Args-dotMode = mode $ Dot {- src = def &= srcArg- ,entry = "MAIN" &= mainArg- ,out = def &= outArg- } &= prog "dot"- & text "compute the LTS and dump it as dot graph"+fdrMode :: Args+fdrMode = FDR {+ src = def+ &= help "CSPM specification"+ &= typFile+ &= argPos 0+ ,entry = "MAIN"+ &= help "optional: the main process" + &= typ "PROCESS"+ &= explicit &= name "main" &= name "m"+ ,out = def+ &= help "optional: name of the generated fdr file"+ &= typFile+ &= explicit &= name "out" &= name "o"+ } &= program "compute the LTS and dump it as fdr script" -myDefault :: String -> String -> String-myDefault a b = if null a then b else a+dotMode :: Args+dotMode = Dot {+ src = def+ &= help "CSPM specification"+ &= typFile+ &= argPos 0+ ,entry = "MAIN"+ &= help "optional: the main process" + &= typ "PROCESS"+ &= explicit &= name "main" &= name "m"+ ,out = def+ &= help "optional: name of the generated dot file"+ &= typFile+ &= explicit &= name "out" &= name "o"+ } &= program "compute the LTS and dump it as dot graph" +-- execute the command according to command line arguments execCommand :: Args -> IO ()-execCommand args@Eval {} = do- let context = if null $ evalContext args then Nothing else Just $ evalContext args+execCommand Eval {..} = do isVerbose <- isLoud- (val,_) <- evalEnv isVerbose context $ evalExpr args+ (val,_) <- evalEnv isVerbose evalContext evalExpr print val -execCommand args@Trace {} = do- (proc,sigma) <- mkProcess (src args) (entry args)+execCommand Trace {..} = do+ (proc,sigma) <- mkProcess src entry trace sigma proc -execCommand args@FDR {} = do- (proc,sigma) <- mkProcess (src args) (entry args)+execCommand FDR {..} = do+ (proc,sigma) <- mkProcess src entry let lts = mkLtsPar sigma proc- outFile = myDefault (out args) (src args ++ ".fdr")+ outFile = case out of+ Just f -> f+ Nothing -> src ++ ".fdr" ltsToCsp proc lts outFile return () -execCommand args@Dot {} = do- (proc,sigma) <- mkProcess (src args) (entry args)+execCommand Dot {..} = do+ (proc,sigma) <- mkProcess src entry let lts = mkLtsPar sigma proc- outFile = myDefault (out args) (src args ++ ".dot")+ outFile = case out of+ Just f -> f+ Nothing -> src ++ ".dot" mkDotFile outFile lts return () @@ -150,3 +165,52 @@ case proc of VProcess p -> return (p, getAllEvents env) _ -> error "type-error : entry-point is not a process"++-- example exception handler+handleException :: IO () -> IO ()+handleException x+ = x `catches` allHandler+ where+ allHandler = [+ Handler lexError, Handler parseError, Handler renameError+ ,Handler errCall+ ,Handler async -- pressing CTRL c+ ,Handler ioExc -- file not found etc+ ,Handler someExc ]+ lexError :: LexError -> IO ()+ lexError LexError {..} = do+ putStrLn "lexError"+ putStrLn $ pprintAlexPosn lexEPos+ putStrLn $ lexEMsg+ exitFailure+ parseError :: ParseError -> IO ()+ parseError ParseError {..} = do+ putStrLn "parseError"+ putStrLn $ parseErrorMsg+ putStrLn $ pprintAlexPosn parseErrorPos+ putStrLn $ "at token : " ++ (show $ tokenString parseErrorToken)+ exitFailure+ renameError :: RenameError -> IO ()+ renameError RenameError {..} = do+ putStrLn "renameError"+ putStrLn $ renameErrorMsg+ putStrLn $ show renameErrorLoc+ exitFailure+ ioExc :: IOException -> IO ()+ ioExc err = do+ putStrLn $ show err+ exitFailure+ errCall :: ErrorCall -> IO ()+ errCall err = flip catches allHandler $ do+ putStrLn "unexpected error call"+ putStrLn $ show err+ exitFailure+ async :: AsyncException -> IO ()+ async err = do+ putStrLn "AsyncException (Pressing CRTL C ?)"+ putStrLn $ show err+ exitFailure+ someExc :: SomeException -> IO ()+ someExc err = do+ putStrLn $ show err+ exitFailure