diff --git a/CSPM-cspm.cabal b/CSPM-cspm.cabal --- a/CSPM-cspm.cabal +++ b/CSPM-cspm.cabal @@ -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 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 diff --git a/src/CSPM/LTS/ToCsp.hs b/src/CSPM/LTS/ToCsp.hs --- a/src/CSPM/LTS/ToCsp.hs +++ b/src/CSPM/LTS/ToCsp.hs @@ -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 diff --git a/src/Main.hs b/src/Main.hs --- a/src/Main.hs +++ b/src/Main.hs @@ -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