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
-> FilePath
-> IO ()
ltsToCsp process lts fname = do
file <- openFile fname WriteMode
let dup = hPutStrLn file
dup $ "GPINIT = " ++ procToCsp process
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"
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
TickEvent -> ""
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)