diff --git a/CSPM-cspm.cabal b/CSPM-cspm.cabal --- a/CSPM-cspm.cabal +++ b/CSPM-cspm.cabal @@ -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 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 diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,4 +1,4 @@ -Copyright (c) Marc Fontaine 2007-2009 +Copyright (c) Marc Fontaine 2007-2011 All rights reserved. diff --git a/src/CSPM/Assert.hs b/src/CSPM/Assert.hs new file mode 100644 --- /dev/null +++ b/src/CSPM/Assert.hs @@ -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) diff --git a/src/CSPM/LTS/Deadlock.hs b/src/CSPM/LTS/Deadlock.hs new file mode 100644 --- /dev/null +++ b/src/CSPM/LTS/Deadlock.hs @@ -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 diff --git a/src/CSPM/LTS/LTS.hs b/src/CSPM/LTS/LTS.hs --- a/src/CSPM/LTS/LTS.hs +++ b/src/CSPM/LTS/LTS.hs @@ -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 diff --git a/src/CSPM/LTS/MkLtsPar.hs b/src/CSPM/LTS/MkLtsPar.hs --- a/src/CSPM/LTS/MkLtsPar.hs +++ b/src/CSPM/LTS/MkLtsPar.hs @@ -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 -} 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 @@ -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 diff --git a/src/CSPM/LTS/ToDot.hs b/src/CSPM/LTS/ToDot.hs --- a/src/CSPM/LTS/ToDot.hs +++ b/src/CSPM/LTS/ToDot.hs @@ -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 diff --git a/src/CSPM/LTS/Utils.hs b/src/CSPM/LTS/Utils.hs new file mode 100644 --- /dev/null +++ b/src/CSPM/LTS/Utils.hs @@ -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 diff --git a/src/Main.hs b/src/Main.hs --- a/src/Main.hs +++ b/src/Main.hs @@ -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 ()