packages feed

CSPM-cspm (empty) → 0.1.0.0

raw patch · 8 files changed

+546/−0 lines, 8 filesdep +CSPM-CoreLanguagedep +CSPM-FiringRulesdep +CSPM-Frontendsetup-changed

Dependencies added: CSPM-CoreLanguage, CSPM-FiringRules, CSPM-Frontend, CSPM-Interpreter, base, cmdargs, containers, parallel

Files

+ CSPM-cspm.cabal view
@@ -0,0 +1,50 @@+Name:                CSPM-cspm+Version:             0.1.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.+  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).+++License:             BSD3+category:            Language,Formal Methods,Concurrency+License-File:        LICENSE+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+build-type:          Simple++Executable cspm+  Build-Depends:+    CSPM-Frontend >= 0.3.0.0+    ,CSPM-CoreLanguage >= 0.1 && < 0.2+    ,CSPM-Interpreter >= 0.2 && < 0.3+    ,CSPM-FiringRules >= 0.1 && < 0.2+    ,cmdargs >= 0.1 && < 0.2+    ,containers >= 0.3 && < 0.4+    ,parallel >=2.2 && < 2.3+    ,base >= 4.0 && < 5.0++ +  GHC-Options: -threaded -funbox-strict-fields -O2 -Wall+  Extensions:+    DeriveDataTypeable, StandaloneDeriving, FlexibleInstances, FlexibleContexts+    TypeSynonymInstances+  Hs-Source-Dirs:      src+  Main-is:             Main.hs++  Other-modules:+    CSPM.LTS.LTS+    CSPM.LTS.MkLtsPar+    CSPM.LTS.ToCsp+    CSPM.LTS.ToDot
+ LICENSE view
@@ -0,0 +1,27 @@+Copyright (c) Marc Fontaine 2007-2009++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:+1. Redistributions of source code must retain the above copyright+   notice, this list of conditions and the following disclaimer.+2. Redistributions in binary form must reproduce the above copyright+   notice, this list of conditions and the following disclaimer in the+   documentation and/or other materials provided with the distribution.+3. Neither the name of the author nor the names of his contributors+   may be used to endorse or promote products derived from this software+   without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS ``AS IS'' AND+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE+ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY+OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF+SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,3 @@+#!/usr/bin/env runhaskell+import Distribution.Simple+main = defaultMain
+ src/CSPM/LTS/LTS.hs view
@@ -0,0 +1,38 @@+{-# LANGUAGE BangPatterns #-}+----------------------------------------------------------------------------+-- |+-- Module      :  CSPM.LTS.LTS+-- Copyright   :  (c) Fontaine 2009+-- License     :  BSD+-- +-- Maintainer  :  Fontaine@cs.uni-duesseldorf.de+-- Stability   :  experimental+-- Portability :  GHC-only+--+module CSPM.LTS.LTS+where+import CSPM.FiringRules.Rules+import CSPM.Interpreter as Interpreter+import CSPM.Interpreter.Hash++import Data.Map (Map)+import Data.Ord (comparing)+import Data.Function (on)++data LtsNode+  = LtsNode {+    nodeDigest :: ! Interpreter.Digest+   ,nodeProcess :: Interpreter.Process+   }++mkLtsNode :: Interpreter.Process -> LtsNode+mkLtsNode p = LtsNode {+   nodeDigest = hash p+  ,nodeProcess = p }++instance Ord  LtsNode where compare = comparing nodeDigest+instance Eq   LtsNode where (==) = on (==) nodeDigest+instance Show LtsNode where+  show f = "(LTSNode " ++ (show $ nodeDigest f) ++ ")"++type LTS = Map LtsNode [Rule INT]
+ src/CSPM/LTS/MkLtsPar.hs view
@@ -0,0 +1,78 @@+----------------------------------------------------------------------------+-- |+-- Module      :  CSPM.LTS.mkLtsPar+-- Copyright   :  (c) Fontaine 2010+-- License     :  BSD+-- +-- Maintainer  :  Fontaine@cs.uni-duesseldorf.de+-- Stability   :  experimental+-- Portability :  GHC-only+--+-- Compute the labled transition system of a process.+----------------------------------------------------------------------------+module CSPM.LTS.MkLtsPar+(+  mkLtsPar+)+where++import CSPM.CoreLanguage+import CSPM.FiringRules.Rules+import CSPM.FiringRules.Verifier (viewProcAfter)+import CSPM.FiringRules.FieldConstraints (computeTransitions)++--import CSPM.Interpreter as Interpreter+import CSPM.Interpreter (INT)++import CSPM.LTS.LTS++import Control.Parallel.Strategies+import qualified Data.Map as Map+import qualified Data.Set as Set+import Data.Set (Set)+import Data.List as List++-- | Compute the+mkLtsPar :: Sigma INT-> Process INT -> LTS+mkLtsPar events process+  = wave [mkLtsNode process] Map.empty+  where+    wave :: [LtsNode] -> LTS -> LTS+    wave [] lts = lts+    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)+          where rules =  computeTransitions events $ nodeProcess p+      +        !newLts = List.foldl' insertTransition lts transitions+          where+            insertTransition :: LTS -> (LtsNode, [Rule INT], [LtsNode]) -> LTS+            insertTransition l (p, rules, _) = Map.insert p rules l++        uniqueProcesses :: Set LtsNode+        !uniqueProcesses = List.foldl' insertProcess Set.empty processes+           where+             insertProcess :: Set LtsNode -> LtsNode -> Set LtsNode+             insertProcess s p = if Map.member p newLts+               then s+               else p `Set.insert` s++    parRules ::+          [(LtsNode, [Rule INT], [LtsNode ])]+       -> [(LtsNode, [Rule INT], [LtsNode ])]+    parRules = withStrategy $ parList $ seqTriple r0 (parList rwhnf) (parList rwhnf)+ {- +   semantic : parRules = id+ -}++{-+    parRules = withStrategy $ parList $ \(p,rl,pl) -> do+       p' <- rpar (p `using` r0)+       rl' <- rpar (rl `using` parList rwhnf)+       pl' <- rpar (pl `using` parList rwhnf)+       return (p',rl',pl')+-}
+ src/CSPM/LTS/ToCsp.hs view
@@ -0,0 +1,102 @@+----------------------------------------------------------------------------+-- |+-- Module      :  CSPM.LTS.ToCsp+-- Copyright   :  (c) Fontaine 2009+-- License     :  BSD+-- +-- Maintainer  :  Fontaine@cs.uni-duesseldorf.de+-- Stability   :  experimental+-- 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+  (+  ltsToCsp+  )+where++import CSPM.CoreLanguage hiding (Field)++import CSPM.Interpreter (INT, chanName, constrName, Value (..), Field )+import CSPM.FiringRules.Rules+import CSPM.FiringRules.Verifier (viewRule)++import CSPM.Interpreter.Hash++import CSPM.LTS.LTS++import System.IO+import qualified Data.Map as Map+import Data.List as List+import Control.Monad++ltsToCsp :: Process INT -> LTS -> String -> IO ()+ltsToCsp init 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}"+  forM_ (Map.assocs lts) $ dumpState file+  hClose file+  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++    showTrans :: Rule INT -> String+    showTrans r = eventToCsp trans ++ procToCsp to+       where+         (_from,trans,to) = viewRule r++    procToCsp :: Process INT -> String+    procToCsp p = "GP_" ++ (show $ hash p)+++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 ) ++ " -> "++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)
+ src/CSPM/LTS/ToDot.hs view
@@ -0,0 +1,96 @@+----------------------------------------------------------------------------+-- |+-- Module      :  CSPM.LTS.ToDot+-- Copyright   :  (c) Fontaine 2009+-- License     :  BSD+-- +-- Maintainer  :  Fontaine@cs.uni-duesseldorf.de+-- Stability   :  experimental+-- Portability :  GHC-only+--+-- dump a Lts as a Dot-file+-- todo : completely rewrite (use dot-library)+module CSPM.LTS.ToDot+(+  mkDotFile+)+where++import CSPM.CoreLanguage+import CSPM.FiringRules.Verifier+import CSPM.FiringRules.Rules++import CSPM.LTS.LTS++import CSPM.Interpreter (INT)+import qualified CSPM.Interpreter as Interpreter++import System.IO+import Data.Map as Map+import Data.List as List++import Control.Monad++-- todo : this is all pure no need for IO+-- todo : use dot-libray+mkDotFile :: FilePath -> LTS -> IO ()+mkDotFile filename lts = do+ file <- openFile filename WriteMode+ let dup = hPutStrLn file+ dup "digraph stateSpace {"+ dup "margin = \"0\""+-- dup "page = \"11.0,8.5\""+-- dup "size = \"11.0,8.5\""+ dup "rotate = \"0\""+ dup "ratio = \"fill\""+ forM_ (Map.assocs lts) $ \adj -> do+   dumpNode dup adj+ dup "}"+ hClose file+++dumpNode ::+     (String -> IO ())+  -> (LtsNode, [Rule INT])+  -> IO ()+dumpNode dup (proc,rules) = do+  dup $ dotNode proc+  forM_ rules $ \r -> dup $ dotEdge proc r++dotNode :: LtsNode -> String+dotNode proc = (showProc proc) ++ mkAttrib [mkLabel (show proc),color]+ where color = mkColor "black"++dotEdge :: LtsNode -> Rule INT-> String+dotEdge from rule+  = (showProc from) ++ " -> " ++ (showProc $ mkLtsNode to) ++ mkAttrib [label,color]+  where+{- _from is not equal to from, because some processes meight be switched off -}+    (_from,trans,to) = viewRule rule+    label = mkLabel $ eventToCsp trans+    color = mkColor "black" ++showProc :: LtsNode -> String+showProc x = "N"++ (show $ nodeDigest x)++mkAttrib :: [String] -> String+mkAttrib a = " [ " ++ (concat $ intersperse "," a) ++ " ]"++mkLabel :: String -> String+mkLabel l = "label = " ++ show l++mkColor :: String -> String+mkColor c = "color = " ++c++eventToCsp :: TTE INT -> String+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.VConstructor c -> Interpreter.constrName c+  _ -> error ("ToDot : fieldToCsp missing match" ++ show f)
+ src/Main.hs view
@@ -0,0 +1,152 @@+----------------------------------------------------------------------------+-- |+-- Module      :  Main+-- Copyright   :  (c) Fontaine 2010+-- License     :  BSD+-- +-- Maintainer  :  Fontaine@cs.uni-duesseldorf.de+-- Stability   :  experimental+-- Portability :  GHC-only+--+-- Comand line interface for the CSPM tools.+----------------------------------------------------------------------------+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE StandaloneDeriving #-}++module Main+where++import System.Console.CmdArgs hiding (args)+import CSPM.Interpreter+import CSPM.Interpreter.Test.CLI (evalEnv)+import CSPM.FiringRules.Trace (trace)+import CSPM.FiringRules.HelperClasses++import CSPM.LTS.MkLtsPar (mkLtsPar)+import CSPM.LTS.ToCsp (ltsToCsp)+import CSPM.LTS.ToDot (mkDotFile)+++instance EqOrd INT+instance CSP1 INT+instance CSP2 INT+instance FShow INT++-- | main-funtion for the command line.+main :: IO ()+main = cmdArgs "CSPM Tools V0.1" modes >>= execCommand+  where modes = [evalMode, traceMode, fdrMode, dotMode ]+data Args = +   Eval {+     evalContext :: FilePath+    ,evalExpr :: String+    }+  |Trace {+     src    :: FilePath+    ,entry  :: String+    }+  |FDR {+     src    :: FilePath+    ,entry  :: String+    ,out :: FilePath+    }+  |Dot {+     src    :: FilePath+    ,entry  :: String+    ,out :: 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 {+   evalContext = def+       &= text "optional: CSPM specification to load into context"+       & typFile +       & empty "" & explicit & flag "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"++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"++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"++myDefault :: String -> String -> String+myDefault a b = if null a then b else a++execCommand :: Args -> IO ()+execCommand args@Eval {} = do+  let context = if null $ evalContext args then Nothing else Just $ evalContext args+  isVerbose <- isLoud+  (val,_) <- evalEnv isVerbose context $ evalExpr args+  print val++execCommand args@Trace {} = do+  (proc,sigma) <- mkProcess (src args) (entry args)+  trace sigma proc++execCommand args@FDR {} = do+  (proc,sigma) <- mkProcess (src args) (entry args)+  let+    lts = mkLtsPar sigma proc+    outFile = myDefault (out args) (src args ++ ".fdr")+  ltsToCsp proc lts outFile+  return ()++execCommand args@Dot {} = do+  (proc,sigma) <- mkProcess (src args) (entry args)+  let+    lts = mkLtsPar sigma proc+    outFile = myDefault (out args) (src args ++ ".dot")+  mkDotFile outFile lts+  return ()++mkProcess :: FilePath -> String -> IO (Process, ClosureSet)+mkProcess file expr = do+  isVerbose <- isLoud+  (proc, env) <- evalEnv isVerbose (Just file) expr+  case proc of+    VProcess p -> return (p, getAllEvents env)+    _ -> error "type-error : entry-point is not a process"