diff --git a/CSPM-cspm.cabal b/CSPM-cspm.cabal
new file mode 100644
--- /dev/null
+++ b/CSPM-cspm.cabal
@@ -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
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -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.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,3 @@
+#!/usr/bin/env runhaskell
+import Distribution.Simple
+main = defaultMain
diff --git a/src/CSPM/LTS/LTS.hs b/src/CSPM/LTS/LTS.hs
new file mode 100644
--- /dev/null
+++ b/src/CSPM/LTS/LTS.hs
@@ -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]
diff --git a/src/CSPM/LTS/MkLtsPar.hs b/src/CSPM/LTS/MkLtsPar.hs
new file mode 100644
--- /dev/null
+++ b/src/CSPM/LTS/MkLtsPar.hs
@@ -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')
+-}
diff --git a/src/CSPM/LTS/ToCsp.hs b/src/CSPM/LTS/ToCsp.hs
new file mode 100644
--- /dev/null
+++ b/src/CSPM/LTS/ToCsp.hs
@@ -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)
diff --git a/src/CSPM/LTS/ToDot.hs b/src/CSPM/LTS/ToDot.hs
new file mode 100644
--- /dev/null
+++ b/src/CSPM/LTS/ToDot.hs
@@ -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)
diff --git a/src/Main.hs b/src/Main.hs
new file mode 100644
--- /dev/null
+++ b/src/Main.hs
@@ -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"