ToCsp.hs

----------------------------------------------------------------------------
-- |
-- 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

-- | 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
--  dup $ "channel " ++ ( concat $ intersperse "," $ map showEvent $ getSigma trans)
--  let adjList = groupBy eqByFrom $ sortBy compareByFrom trans

--  dup $ "channel intTau,intTick"
  dup $ "GPINIT = " ++ procToCsp process  -- ++ "\\{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)