CSPM-cspm 0.5.6.0 → 0.6.0.4
raw patch · 11 files changed
+135/−162 lines, 11 filesdep +prettyclassdep ~CSPM-Frontenddep ~CSPM-Interpreterdep ~CSPM-ToPrologPVP ok
version bump matches the API change (PVP)
Dependencies added: prettyclass
Dependency ranges changed: CSPM-Frontend, CSPM-Interpreter, CSPM-ToProlog, cmdargs, hslua, parallel, pretty, transformers
API changes (from Hackage documentation)
+ CSPM.LTS.LTS: hashLTS :: LTS -> Digest
- CSPM.LTS.ToCsp: ltsToCsp :: Process INT -> LTS -> FilePath -> IO ()
+ CSPM.LTS.ToCsp: ltsToCsp :: Process INT -> LTS -> Doc
Files
- CSPM-cspm.cabal +22/−22
- src/CSPM/Assert.hs +12/−11
- src/CSPM/LTS/LTS.hs +19/−0
- src/CSPM/LTS/MkLtsDFS.hs +2/−1
- src/CSPM/LTS/MkLtsPar.hs +1/−0
- src/CSPM/LTS/ToCsp.hs +38/−69
- src/CSPM/LTS/ToDot.hs +3/−13
- src/CSPM/LTS/Utils.hs +0/−19
- src/CSPM/Lua.hs +6/−7
- src/Main/ExecCommand.hs +19/−8
- src/Scripting/LuaUtils.hs +13/−12
CSPM-cspm.cabal view
@@ -1,10 +1,10 @@ Name: CSPM-cspm-Version: 0.5.6.0+Version: 0.6.0.4 Synopsis: cspm command line tool for analyzing CSPM specifications. Description: cspm is a small command line tool for analyzing CSPM specifications.- It supports serveral modes of operation.+ It supports several modes of operation. For example as: . * 'cspm --help' -> print a help message.@@ -30,28 +30,29 @@ category: Language,Formal Methods,Concurrency License-File: LICENSE Author: Marc Fontaine-Maintainer: Marc Fontaine <fontaine@cs.uni-duesseldorf.de>+Maintainer: Marc Fontaine <Marc.Fontaine@gmx.de> cabal-Version: >= 1.10 build-type: Simple-Tested-With: GHC == 7.0.3+Tested-With: GHC == 7.4.1 Stability: experimental Executable cspm Build-Depends:- CSPM-Frontend >= 0.7 && < 0.8+ CSPM-Frontend >= 0.9 && < 0.10 ,CSPM-CoreLanguage >= 0.3 && < 0.4 ,CSPM-FiringRules >= 0.4 && < 0.5- ,CSPM-Interpreter >= 0.5 && < 0.6- ,CSPM-ToProlog >= 0.4 && < 0.5- ,cmdargs >= 0.7 && < 0.8+ ,CSPM-Interpreter >= 0.6 && < 0.7+ ,CSPM-ToProlog >= 0.5 && < 0.6+ ,cmdargs >= 0.9 && < 0.10 ,xml >= 1.3 && < 1.4 ,containers >= 0.4 && < 0.5- ,parallel >=3.1 && < 3.2+ ,parallel >= 3.2 && < 3.3 ,base >= 4.0 && < 5.0- ,pretty >=1.0 && <1.1- ,transformers >=0.2 && <0.3+ ,pretty >= 1.1 && < 1.2+ ,transformers >= 0.3 && < 0.4 ,syb >= 0.3 && <0.4- ,hslua == 0.3.3+ ,prettyclass >= 1.0 && < 1.1+ ,hslua == 0.3.4 GHC-Options: -threaded -funbox-strict-fields -O2 -Wall -fno-warn-orphans@@ -73,7 +74,6 @@ CSPM.LTS.MkLtsDFS CSPM.LTS.ToCsp CSPM.LTS.ToDot- CSPM.LTS.Utils CSPM.LTS.Deadlock CSPM.Lua Language.CSPM.AstToXML@@ -82,20 +82,21 @@ Library Build-Depends:- CSPM-Frontend >= 0.7 && < 0.8+ CSPM-Frontend >= 0.9 && < 0.10 ,CSPM-CoreLanguage >= 0.3 && < 0.4 ,CSPM-FiringRules >= 0.4 && < 0.5- ,CSPM-Interpreter >= 0.5 && < 0.6- ,CSPM-ToProlog >= 0.4 && < 0.5- ,cmdargs >= 0.7 && < 0.8+ ,CSPM-Interpreter >= 0.6 && < 0.7+ ,CSPM-ToProlog >= 0.5 && < 0.6+ ,cmdargs >= 0.9 && < 0.10 ,xml >= 1.3 && < 1.4 ,containers >= 0.4 && < 0.5- ,parallel >=3.1 && < 3.2+ ,parallel >= 3.2 && < 3.3 ,base >= 4.0 && < 5.0- ,pretty >=1.0 && <1.1- ,transformers >=0.2 && <0.3+ ,pretty >= 1.1 && < 1.2+ ,transformers >= 0.3 && < 0.4 ,syb >= 0.3 && <0.4- ,hslua == 0.3.3+ ,prettyclass >= 1.0 && < 1.1+ ,hslua == 0.3.4 GHC-Options: -funbox-strict-fields -O2 -Wall -fno-warn-orphans Default-Language: Haskell2010@@ -113,7 +114,6 @@ CSPM.LTS.MkLtsDFS CSPM.LTS.ToCsp CSPM.LTS.ToDot- CSPM.LTS.Utils CSPM.LTS.Deadlock CSPM.Lua Language.CSPM.AstToXML
src/CSPM/Assert.hs view
@@ -18,7 +18,7 @@ import Language.CSPM.AST as AST import Language.CSPM.AstUtils import Language.CSPM.Frontend-import Language.CSPM.PrettyPrinter (pp)+import Language.CSPM.PrettyPrinter () import CSPM.Interpreter.Eval import CSPM.Interpreter.Types (Env)@@ -28,7 +28,8 @@ import CSPM.LTS.Deadlock (findDeadlock) import Control.Exception.Base (evaluate)-import Text.PrettyPrint++import Text.PrettyPrint.HughesPJClass import Data.Either type AssertResult = Either Doc Doc@@ -62,14 +63,14 @@ 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+ then return $ Right $ text "pass :" <+> pPrint ass+ else return $ Left $ text "fail :" <+> pPrint ass AssertRefine {}- -> notSupported $ text "refinement not supported yet :" <+> pp ass+ -> notSupported $ text "refinement not supported yet :" <+> pPrint ass AssertTauPrio {}- -> notSupported $ text "tau priority assert not supported yet :" <+> pp ass+ -> notSupported $ text "tau priority assert not supported yet :" <+> pPrint ass AssertModelCheck _negated _expr _property (Just ext)- -> notSupported $ text "model checking fdr extensions :" <+> pp ass <+> pp ext+ -> notSupported $ text "model checking fdr extensions :" <+> pPrint ass <+> pPrint ext AssertModelCheck negated expr property Nothing -> do let sigma = getSigma env@@ -77,9 +78,9 @@ res <- case unLabel property of DeadlockFree -> checkDeadlockFree sigma proc Deterministic- -> notSupported (text "assert not supported yet :" <+> pp ass)+ -> notSupported (text "assert not supported yet :" <+> pPrint ass) LivelockFree- -> notSupported (text "assert not supported yet :" <+> pp ass)+ -> notSupported (text "assert not supported yet :" <+> pPrint ass) return $ if negated then either Right Left res else res@@ -91,7 +92,7 @@ putStrLn "running BFS for deadlock state" res <- evaluate $ findDeadlock sigma proc case res of- Nothing -> return $ Right $ pp ass <+> text " --- no deadlock found"+ Nothing -> return $ Right $ pPrint ass <+> text " --- no deadlock found" Just path- -> return $ Left $ pp ass <+> text " -- deadlock found: path-length :"+ -> return $ Left $ pPrint ass <+> text " -- deadlock found: path-length :" <+> (int $ length path)
src/CSPM/LTS/LTS.hs view
@@ -13,14 +13,17 @@ module CSPM.LTS.LTS where+import CSPM.CoreLanguage.Event import CSPM.FiringRules.Rules import CSPM.Interpreter as Interpreter import CSPM.Interpreter.Hash import Data.Typeable import Data.Map (Map)+import qualified Data.Map as Map import Data.Ord (comparing) import Data.Function (on)+import CSPM.FiringRules.Verifier (viewRule) data LtsNode = LtsNode {@@ -39,3 +42,19 @@ show f = "(LTSNode " ++ (show $ nodeDigest f) ++ ")" type LTS = Map LtsNode [Rule INT]++-- | Compute the hash value of an LTS. (Warning: This does not include entry process)+hashLTS :: LTS -> Interpreter.Digest+hashLTS = mix (hs "CSPM.LTS.LTS_salt0") . hash . map hashNode . Map.assocs+ where+ hashNode :: (LtsNode,[Rule INT]) -> Interpreter.Digest+ hashNode (node,transList)+ = mix3 (hs "transisition") (nodeDigest node) $ hash $ map hashTrans transList+ hashTrans :: Rule INT -> Interpreter.Digest+ hashTrans r = let (from,trans,to) = viewRule r+ in mix3 (hash from) (hashEvent trans) (hash to)++ hashEvent e = case e of+ TickEvent -> hs "tickEvent"+ TauEvent -> hs "tauEvent"+ SEvent l -> hash l
src/CSPM/LTS/MkLtsDFS.hs view
@@ -32,6 +32,7 @@ import System.Timeout as Timeout import Control.Exception+import Control.Monad import Data.IORef -- | Generate an LTS with a DFS@@ -57,7 +58,7 @@ where loop = do lts <- fmap snd $ readIORef ltsPtr- evaluate lts+ void $ evaluate lts finish <- atomicModifyIORef ltsPtr $ dfsStep sigma if finish then return () else loop
src/CSPM/LTS/MkLtsPar.hs view
@@ -10,6 +10,7 @@ -- -- Compute the labled transition system of a process. ----------------------------------------------------------------------------+{-# LANGUAGE BangPatterns #-} module CSPM.LTS.MkLtsPar ( mkLtsPar
src/CSPM/LTS/ToCsp.hs view
@@ -1,7 +1,7 @@ ---------------------------------------------------------------------------- -- | -- Module : CSPM.LTS.ToCsp--- Copyright : (c) Fontaine 2009+-- Copyright : (c) Fontaine 2009 - 2011 -- License : BSD -- -- Maintainer : Fontaine@cs.uni-duesseldorf.de@@ -9,7 +9,6 @@ -- Portability : GHC-only -- -- dump a Lts as Csp-Specifications suitable for FDR-refinementcheck--- todo :: make this a pure function (maybe serialize to a ByteString) module CSPM.LTS.ToCsp (@@ -19,89 +18,59 @@ import CSPM.CoreLanguage hiding (Field) -import CSPM.Interpreter (INT, chanName, constrName, Value (..), Field )+import CSPM.Interpreter (INT) -- todo : remove this dependency import CSPM.FiringRules.Rules import CSPM.FiringRules.Verifier (viewRule) -import CSPM.Interpreter.Hash+import CSPM.Interpreter.Hash -- todo : remove this depnedency import CSPM.LTS.LTS -import System.IO+import Text.PrettyPrint.HughesPJClass+ import qualified Data.Map as Map import Data.List as List-import Control.Monad --- | Dump an LTS to File in a format suitable for reloading it with FDR.+-- | Translate an LTS to a CSP specification 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--- dup $ "channel " ++ ( concat $ intersperse "," $ map showEvent $ getSigma trans)--- let adjList = groupBy eqByFrom $ sortBy compareByFrom trans+ -> Doc --- dup $ "channel intTau,intTick"- dup $ "GPINIT = " ++ procToCsp process -- ++ "\\{intTau,intTick}"- forM_ (Map.assocs lts) $ dumpState file- hClose file+ltsToCsp process lts+ = text "GPINIT = " <> procToCsp process+ $+$ (vcat $ map transToCsp $ Map.assocs lts) where- dumpState :: Handle -> (LtsNode, [Rule INT]) -> IO ()- dumpState file (n, transitions) = do- let- dup = hPutStr file- p = nodeProcess n- dup $ procToCsp p ++ " = (\n"- dup " "- if null transitions- then if p == Omega- then dup "SKIP"- else dup "STOP"- else case (List.partition isTauRule transitions) of- (tauRules,[]) -> dup $ concat $ intersperse "\n |~| " $ map showTrans tauRules- ([],nonTau) -> dup $ concat $ intersperse "\n [] " $ map showTrans nonTau- (tauRules,nonTau) -> do- dup "("- dup $ concat $ intersperse "\n [] " $ map showTrans nonTau- dup ") [> ("- dup $ concat $ intersperse "\n |~| " $ map showTrans tauRules- dup ")"- dup ")\n"---- isTauRule (TauRule {}) = True--- isTauRule _ = False+ procToCsp :: Process INT -> Doc+ procToCsp p = text "GP_" <> (text $ show $ hash p) - showTrans :: Rule INT -> String- showTrans r = eventToCsp trans ++ procToCsp to- where- (_from,trans,to) = viewRule r+ transToCsp :: (LtsNode, [Rule INT]) -> Doc+ transToCsp (p, transitions)+ = (procToCsp (nodeProcess p) <> text " = ")+ $+$ nest 4 (parens $ case (List.partition isTauRule transitions) of+ ([],[]) | nodeProcess p == Omega -> text "SKIP"+ ([],[]) -> text "STOP"+ (tauRules,[]) -> tauTransList tauRules+ ([], nonTau) -> eventTransList nonTau+ (tauRules,nonTau) -> vcat [+ parens $ eventTransList nonTau+ ,nest 4 $ text "[>"+ ,parens $ tauTransList tauRules+ ]) - procToCsp :: Process INT -> String- procToCsp p = "GP_" ++ (show $ hash p)+ tauTransList :: [Rule INT] -> Doc+ tauTransList = vcat . punctuate (text " |~| ") . map showTrans + eventTransList :: [Rule INT] -> Doc+ eventTransList = vcat . punctuate (text " [] ") . map showTrans -eventToCsp :: TTE INT -> String-eventToCsp e = case e of-{-- this breaks mydemos/SimpleSubsets.csp- todo: think about this- TickEvent -> "intTick -> "--}- TickEvent -> ""--- TauEvent -> "intTau -> "- TauEvent -> ""- SEvent l -> (concat $ intersperse "." $ List.map fieldToCsp l ) ++ " -> "+ showTrans :: Rule INT -> Doc+ showTrans r = eventToCsp trans <> procToCsp to+ where+ (_from,trans,to) = viewRule r -fieldToCsp :: Field -> String-fieldToCsp f = case f of- VChannel chan -> chanName chan- VInt i -> show i- VBool True -> "true"- VBool False -> "false"- VConstructor c -> constrName c- VTuple l -> "(" ++ (concat $ intersperse "," $ List.map fieldToCsp l) ++ ")"- VDotTuple l -> (concat $ intersperse "." $ List.map fieldToCsp l)- _ -> error ("ToCsp : fieldToCsp missing match" ++ show f)+ eventToCsp :: TTE INT -> Doc+ eventToCsp e = case e of+ TickEvent -> empty+ TauEvent -> empty+ SEvent l -> (hcat $ punctuate (text ".") $ List.map pPrint l) <> text "->"
src/CSPM/LTS/ToDot.hs view
@@ -23,8 +23,9 @@ import CSPM.LTS.LTS import CSPM.Interpreter (INT)-import qualified CSPM.Interpreter as Interpreter +import Text.PrettyPrint.HughesPJClass+ import System.IO import Data.Map as Map import Data.List as List@@ -88,15 +89,4 @@ eventToCsp e = case e of TickEvent -> "Tick" TauEvent -> "Tau"- SEvent l -> concat $ intersperse "." $ List.map fieldToCsp l--fieldToCsp :: Interpreter.Field -> String-fieldToCsp f = case f of- Interpreter.VChannel chan -> Interpreter.chanName chan- Interpreter.VInt i -> show i- Interpreter.VBool True -> "true"- Interpreter.VBool False -> "false"- Interpreter.VConstructor c -> Interpreter.constrName c- Interpreter.VTuple l -> "(" ++ (concat $ intersperse "," $ List.map fieldToCsp l) ++ ")"- Interpreter.VDotTuple l -> (concat $ intersperse "." $ List.map fieldToCsp l)- _ -> error ("ToDot : fieldToCsp missing match" ++ show f)+ SEvent l -> concat $ intersperse "." $ List.map prettyShow l
− src/CSPM/LTS/Utils.hs
@@ -1,19 +0,0 @@-------------------------------------------------------------------------------- |--- 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/CSPM/Lua.hs view
@@ -21,7 +21,6 @@ where import CSPM.Interpreter as Interpreter-import CSPM.Interpreter.Test.CLI (evalString) import CSPM.LTS.MkLtsPar (mkLtsPar) import CSPM.CoreLanguage.Event@@ -51,12 +50,12 @@ case err of Nothing -> throwIO $ ErrorFromLua loadRes "Lua.loadstring failed" Just msg -> throwIO $ ErrorFromLua loadRes msg- else do- Lua.push l $ LuaArray args- Lua.setglobal l "arg"- forM_ args $ Lua.push l- err <- call_debug l (length args) (Just 0)- maybe (return ()) throwIO err+ else do+ Lua.push l $ LuaArray args+ Lua.setglobal l "arg"+ forM_ args $ Lua.push l+ err <- call_debug l (length args) (Just 0)+ maybe (return ()) throwIO err exportList :: [Export] exportList =
src/Main/ExecCommand.hs view
@@ -21,6 +21,7 @@ import CSPM.Interpreter (INT,interpreterVersion,getSigma,Process,Sigma,Value(..),evalFile) import CSPM.FiringRules.Trace (trace) import CSPM.FiringRules.HelperClasses+import CSPM.FiringRules.Version(firingRulesVersion) import CSPM.CoreLanguage (coreLanguageVersion) import CSPM.LTS.MkLtsPar (mkLtsPar)@@ -34,16 +35,18 @@ (parseFile, frontendVersion ,eitherToExc, renameModule, castModule, lexInclude) import Language.CSPM.LexHelper (unicodeTokenString,asciiTokenString)-import Language.CSPM.PrettyPrinter (toPrettyString)+import Language.CSPM.PrettyPrinter () -import Language.CSPM.TranslateToProlog (translateToProlog)+import Language.CSPM.TranslateToProlog (translateToProlog,toPrologVersion) import Language.CSPM.AstToXML (moduleToXML, showTopElement) import System.Console.CmdArgs (isLoud) -- todo: fix this +import Text.PrettyPrint.HughesPJClass import qualified System.Timeout as Timeout import Control.Exception (evaluate) import System.Exit (exitSuccess)+import System.IO import Data.Version (showVersion) import Control.Monad import Data.Maybe@@ -63,14 +66,19 @@ ," cspm command line utility : ", showVersion version, nl ," CSPM-Frontend : ", showVersion frontendVersion, nl ," CSPM-CoreLanguage : ", showVersion coreLanguageVersion, nl- ," CSPM-FiringRules : ", nl+ ," CSPM-FiringRules : ", showVersion firingRulesVersion, nl ," CSPM-Interpreter : ", showVersion interpreterVersion, nl+ ," CSPM-ToProlog : ", showVersion toPrologVersion, nl ,nl ,"Usage examples:",nl ," cspm --help",nl ," cspm eval --help",nl ," cspm info",nl ," cspm eval '3+2'",nl+ ,nl+ ,"Copyright (c) Marc Fontaine 2007-2012",nl+ ,"Source code available at: http://hackage.haskell.org/package/CSPM-cspm",nl+ ,"Email : Marc.Fontaine@gmx.de",nl ] where nl = "\n" @@ -92,12 +100,15 @@ whenJust xmlOut $ \outFile -> do writeFile outFile $ showTopElement $ moduleToXML ast whenJust prettyOut $ \outFile -> do- writeFile outFile $ toPrettyString ast+ writeFile outFile $ prettyShow ast when (isJust addUnicode || isJust removeUnicode) $ do -- Token stream transformations tokens <- readFile src >>= lexInclude >>= eitherToExc- whenJust addUnicode $ \outFile -> do- writeFile outFile $ List.concatMap unicodeTokenString tokens+ whenJust addUnicode $ \outFile -> withFile outFile WriteMode+ $ \handle -> do+ hSetEncoding handle utf8+ hPutStr handle $ List.concatMap unicodeTokenString tokens+ hClose handle whenJust removeUnicode $ \outFile -> do writeFile outFile $ List.concatMap asciiTokenString tokens whenJust prologOut $ \outFile -> do@@ -110,7 +121,7 @@ execCommand Eval {..} = do (val,_) <- evalFile verbose evalContext evalExpr- print val+ putStrLn $ prettyShow val execCommand Trace {..} = do (proc,sigma) <- mkProcess src entry@@ -139,7 +150,7 @@ case fdrOut of Nothing -> return ()- Just outFile -> ltsToCsp proc lts outFile+ Just outFile -> writeFile outFile $ render $ ltsToCsp proc lts case dotOut of Nothing -> return () Just outFile -> mkDotFile outFile lts
src/Scripting/LuaUtils.hs view
@@ -8,6 +8,7 @@ {-# Language ViewPatterns, RecordWildCards #-} {-# Language ScopedTypeVariables, RankNTypes, GADTs, KindSignatures #-} {-# Language FlexibleInstances #-}+ module Scripting.LuaUtils where @@ -161,15 +162,15 @@ isString <- Lua.isstring l 1 if not isString then return 1 else do- Lua.getglobal l "debug"- isTable <- Lua.istable l (-1)- if not isTable then Lua.pop l 1 >> return 1- else do- Lua.getfield l (-1) "traceback"- isFunction <- Lua.isfunction l (-1)- if not isFunction then Lua.pop l 2 >> return 1- else do- Lua.pushvalue l 1- Lua.pushinteger l 2- void $ Lua.call l 2 1- return 1+ Lua.getglobal l "debug"+ isTable <- Lua.istable l (-1)+ if not isTable then Lua.pop l 1 >> return 1+ else do+ Lua.getfield l (-1) "traceback"+ isFunction <- Lua.isfunction l (-1)+ if not isFunction then Lua.pop l 2 >> return 1+ else do+ Lua.pushvalue l 1+ Lua.pushinteger l 2+ void $ Lua.call l 2 1+ return 1