module CSPM.LTS.LTS
where
import CSPM.CoreLanguage.Event
import CSPM.FiringRules.Rules
import CSPM.Interpreter as Interpreter
import CSPM.Interpreter.Hash
import Data.Typeable
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Ord (comparing)
import Data.Function (on)
import CSPM.FiringRules.Verifier (viewRule)
data LtsNode
= LtsNode {
nodeDigest :: ! Interpreter.Digest
,nodeProcess :: Interpreter.Process
} deriving Typeable
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]
hashLTS :: LTS -> Interpreter.Digest
hashLTS = mix (hs "CSPM.LTS.LTS_salt0") . hash . map hashNode . Map.assocs
where
hashNode :: (LtsNode,[Rule INT]) -> Interpreter.Digest
hashNode (node,transList)
= mix3 (hs "transisition") (nodeDigest node) $ hash $ map hashTrans transList
hashTrans :: Rule INT -> Interpreter.Digest
hashTrans r = let (from,trans,to) = viewRule r
in mix3 (hash from) (hashEvent trans) (hash to)
hashEvent e = case e of
TickEvent -> hs "tickEvent"
TauEvent -> hs "tauEvent"
SEvent l -> hash l