module CSPM.Evaluator.ProcessValues (
Event(..),
EventSet, eventSetFromList, EventMap,
Proc(..), UnCompiledProc, UnCompiledProcOperator, UnCompiledOperator,
CSPOperator(..),
ProcOperator(..),
ProcName(..),
operator, components,
splitProcIntoComponents,
trimProcess,
) where
import CSPM.Evaluator.Values
import qualified Data.Foldable as F
import qualified Data.Sequence as S
import Data.Hashable
import Util.Exception
import Util.Prelude
data Event =
Tau
| Tick
| UserEvent Value
deriving (Eq, Ord)
type EventMap = S.Seq (Event, Event)
type EventSet = S.Seq Event
eventSetFromList :: [Event] -> EventSet
eventSetFromList = S.fromList
instance Hashable Event where
hash Tau = 1
hash Tick = 2
hash (UserEvent vs) = combine 3 (hash vs)
newtype ProcName = ProcName (ScopeIdentifier) deriving (Eq, Hashable, Ord)
data ProcOperator seq evs =
Chase Bool
| Determinise
| Diamond
| Explicate Bool
| Normalize Bool
| ModelCompress
| Prioritise Bool (seq evs)
| StrongBisim
| TauLoopFactor
| WeakBisim
deriving (Eq, Ord)
instance Hashable (seq evs) => Hashable (ProcOperator seq evs) where
hash (Chase True) = 1
hash (Chase False) = 2
hash Diamond = 3
hash (Explicate True) = 4
hash (Explicate False) = 5
hash (Normalize True)= 6
hash (Normalize False)= 7
hash (Prioritise False evs) = combine 8 (hash evs)
hash (Prioritise True evs) = combine 9 (hash evs)
hash ModelCompress = 10
hash StrongBisim = 11
hash TauLoopFactor = 12
hash WeakBisim = 13
hash Determinise = 14
data CSPOperator seq ev evs evm =
PAlphaParallel (seq evs)
| PException evs
| PExternalChoice
| PGenParallel evs
| PHide evs
| PInternalChoice
| PInterrupt
| PInterleave
| PLinkParallel evm
| POperator (ProcOperator seq evs)
| PPrefix ev
| PRename evm
| PSequentialComp
| PSlidingChoice
| PSynchronisingExternalChoice evs
| PSynchronisingInterrupt evs
deriving (Eq, Ord)
instance (Hashable ev, Hashable evm, Hashable evs, Hashable (seq evs)) =>
Hashable (CSPOperator seq ev evs evm) where
hash (PAlphaParallel s) = combine 1 (hash s)
hash (PException s) = combine 2 (hash s)
hash PExternalChoice = 3
hash (PGenParallel evs) = combine 4 (hash evs)
hash (PHide evs) = combine 5 (hash evs)
hash PInternalChoice = 6
hash PInterrupt = 7
hash PInterleave = 8
hash (PLinkParallel s) = combine 9 (hash s)
hash (POperator op) = combine 11 (hash op)
hash (PPrefix ev) = combine 12 (hash ev)
hash (PRename evm) = combine 13 (hash evm)
hash PSequentialComp = 14
hash PSlidingChoice = 15
hash (PSynchronisingExternalChoice evs) = combine 16 (hash evs)
hash (PSynchronisingInterrupt evs) = combine 17 (hash evs)
errorThunk = panic "Trimmed process evaluated"
trimProcess :: UnCompiledProc -> UnCompiledProc
trimProcess (PUnaryOp op p1) =
PUnaryOp (trimOperator op) (trimProcess p1)
trimProcess (PBinaryOp op p1 p2) =
PBinaryOp (trimOperator op) (trimProcess p1) (trimProcess p2)
trimProcess (POp op ps) =
POp (trimOperator op) (fmap trimProcess ps)
trimProcess (PProcCall pn _) = PProcCall pn errorThunk
trimEvent :: Event -> Event
trimEvent Tau = Tau
trimEvent Tick = Tick
trimEvent (UserEvent v) = UserEvent (trimValueForProcessName v)
trimOperator :: UnCompiledOperator -> UnCompiledOperator
trimOperator (PAlphaParallel s) = PAlphaParallel (fmap (fmap trimEvent) s)
trimOperator (PException s) = PException (fmap trimEvent s)
trimOperator PExternalChoice = PExternalChoice
trimOperator (PGenParallel evs) = PGenParallel (fmap trimEvent evs)
trimOperator (PHide evs) = PHide (fmap trimEvent evs)
trimOperator PInternalChoice = PInternalChoice
trimOperator PInterrupt = PInterrupt
trimOperator PInterleave = PInterleave
trimOperator (PLinkParallel evm) =
PLinkParallel (fmap (\(ev,ev') -> (trimEvent ev, trimEvent ev')) evm)
trimOperator (POperator op) = POperator op
trimOperator (PPrefix ev) = PPrefix (trimEvent ev)
trimOperator (PRename evm) =
PRename (fmap (\(ev,ev') -> (trimEvent ev, trimEvent ev')) evm)
trimOperator PSequentialComp = PSequentialComp
trimOperator PSlidingChoice = PSlidingChoice
trimOperator (PSynchronisingExternalChoice evs) =
PSynchronisingExternalChoice (fmap trimEvent evs)
trimOperator (PSynchronisingInterrupt evs) =
PSynchronisingInterrupt (fmap trimEvent evs)
data Proc seq op pn ev evs evm =
PUnaryOp (op seq ev evs evm) (Proc seq op pn ev evs evm)
| PBinaryOp (op seq ev evs evm) (Proc seq op pn ev evs evm) (Proc seq op pn ev evs evm)
| POp (op seq ev evs evm) (seq (Proc seq op pn ev evs evm))
| PProcCall pn (Proc seq op pn ev evs evm)
instance (Eq pn, Eq (seq (Proc seq op pn ev evs evm)), Eq (op seq ev evs evm)) =>
Eq (Proc seq op pn ev evs evm) where
(PProcCall pn1 _) == (PProcCall pn2 _) = pn1 == pn2
(PUnaryOp op1 p1) == (PUnaryOp op2 p2) = op1 == op2 && p1 == p2
(PBinaryOp op1 p1 p2) == (PBinaryOp op2 r1 r2) =
op1 == op2 && p1 == r1 && p2 == r2
(POp op1 ps1) == (POp op2 ps2) = op1 == op2 && ps1 == ps2
_ == _ = False
instance (Hashable pn, Hashable (seq (Proc seq op pn ev evs evm)), Hashable (op seq ev evs evm)) =>
Hashable (Proc seq op pn ev evs evm) where
hash (PProcCall pn1 _) = combine 1 (hash pn1)
hash (PUnaryOp op1 p1) = combine 2 (combine (hash op1) (hash p1))
hash (PBinaryOp op1 p1 p2) = combine 3 (combine (hash op1) (combine (hash p1) (hash p2)))
hash (POp op ps) = combine 4 (combine (hash op) (hash ps))
instance (Ord pn, Ord (seq (Proc seq op pn ev evs evm)), Ord (op seq ev evs evm)) =>
Ord (Proc seq op pn ev evs evm) where
compare (PProcCall pn1 _) (PProcCall pn2 _) = compare pn1 pn2
compare (PProcCall _ _) _ = LT
compare _ (PProcCall _ _) = GT
compare (PUnaryOp op1 p1) (PUnaryOp op2 p2) =
compare op1 op2 `thenCmp` compare p1 p2
compare (PUnaryOp _ _) _ = LT
compare _ (PUnaryOp _ _) = GT
compare (PBinaryOp op1 p1 p2) (PBinaryOp op2 r1 r2) =
compare op1 op2 `thenCmp` compare p1 r1 `thenCmp` compare p2 r2
compare (PBinaryOp _ _ _) _ = LT
compare _ (PBinaryOp _ _ _) = GT
compare (POp op1 ps1) (POp op2 ps2) =
compare op1 op2 `thenCmp` compare ps1 ps2
type UnCompiledProc =
Proc S.Seq CSPOperator ProcName Event (S.Seq Event) (S.Seq (Event, Event))
type UnCompiledOperator =
CSPOperator S.Seq Event (S.Seq Event) (S.Seq (Event, Event))
type UnCompiledProcOperator =
ProcOperator S.Seq (S.Seq Event)
instance Hashable a => Hashable (S.Seq a) where
hash a = foldr combine 0 (F.toList (fmap hash a))
operator :: Proc seq op pn ev evs evm -> op seq ev evs evm
operator (PUnaryOp op _) = op
operator (PBinaryOp op _ _)= op
operator (POp op _) = op
components :: Proc S.Seq op pn ev evs evm -> S.Seq (Proc S.Seq op pn ev evs evm)
components (PBinaryOp _ p1 p2) = p1 S.<| p2 S.<| S.empty
components (POp _ ps) = ps
components (PUnaryOp _ p1) = S.singleton p1
splitProcIntoComponents :: (Eq pn, F.Foldable seq) => Proc seq op pn ev evs evm ->
(Proc seq op pn ev evs evm, [(pn, Proc seq op pn ev evs evm)])
splitProcIntoComponents p =
let
explored pns n = n `elem` (map fst pns)
exploreAll pns [] = pns
exploreAll pns (p:ps) = exploreAll (explore pns p) ps
explore pns (PUnaryOp _ p) = explore pns p
explore pns (PBinaryOp _ p1 p2) = exploreAll pns [p1,p2]
explore pns (POp _ ps) = exploreAll pns (F.toList ps)
explore pns (PProcCall n p) =
if explored pns n then pns
else explore ((n, p):pns) p
in (p, explore [] p)