module CSPM.LTS.ToCsp
(
ltsToCsp
)
where
import CSPM.CoreLanguage hiding (Field)
import CSPM.Interpreter (INT)
import CSPM.FiringRules.Rules
import CSPM.FiringRules.Verifier (viewRule)
import CSPM.Interpreter.Hash
import CSPM.LTS.LTS
import Text.PrettyPrint.HughesPJClass
import qualified Data.Map as Map
import Data.List as List
ltsToCsp ::
Process INT
-> LTS
-> Doc
ltsToCsp process lts
= text "GPINIT = " <> procToCsp process
$+$ (vcat $ map transToCsp $ Map.assocs lts)
where
procToCsp :: Process INT -> Doc
procToCsp p = text "GP_" <> (text $ show $ hash p)
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
])
tauTransList :: [Rule INT] -> Doc
tauTransList = vcat . punctuate (text " |~| ") . map showTrans
eventTransList :: [Rule INT] -> Doc
eventTransList = vcat . punctuate (text " [] ") . map showTrans
showTrans :: Rule INT -> Doc
showTrans r = eventToCsp trans <> procToCsp to
where
(_from,trans,to) = viewRule r
eventToCsp :: TTE INT -> Doc
eventToCsp e = case e of
TickEvent -> empty
TauEvent -> empty
SEvent l -> (hcat $ punctuate (text ".") $ List.map pPrint l) <> text "->"