module Control.Concurrent.CHP.Traces
(module Control.Concurrent.CHP.Traces.CSP
,module Control.Concurrent.CHP.Traces.Structural
,module Control.Concurrent.CHP.Traces.TraceOff
,module Control.Concurrent.CHP.Traces.VCR
,RecordedEvent
,ChannelLabels
,RecordedEventType(..)
,RecordedIndivEvent(..)
,recordedIndivEventLabel
,recordedIndivEventSeq
,Trace(..)
,vcrToCSP
,structuralToCSP
,structuralToVCR
) where
import Control.Arrow
import qualified Data.Foldable as F
import Data.List
import qualified Data.Map as Map
import Data.Monoid
import qualified Data.Set as Set
import Control.Concurrent.CHP.Base
import Control.Concurrent.CHP.Event
import Control.Concurrent.CHP.ProcessId
import Control.Concurrent.CHP.Traces.Base
import Control.Concurrent.CHP.Traces.CSP
import Control.Concurrent.CHP.Traces.Structural
import Control.Concurrent.CHP.Traces.TraceOff
import Control.Concurrent.CHP.Traces.VCR
vcrToCSP :: Eq u => VCRTrace u -> [CSPTrace u]
vcrToCSP (VCRTrace (ls, sets)) = [CSPTrace (ls, es) | es <- nub $ process sets]
where
process :: [Set.Set a] -> [[a]]
process [] = [[]]
process (s:ss)
| Set.null s = process ss
| otherwise = [a ++ b | a <- chp_permutations (Set.toList s), b <- process ss]
type EventMap eventId = Map.Map (RecordedIndivEvent eventId) (Set.Set ProcessId)
combine :: Ord u => [EventMap u] -> EventMap u
combine = foldl (Map.unionWith Set.union) Map.empty
participants :: Ord u => EventHierarchy (RecordedIndivEvent u)
-> Map.Map (RecordedIndivEvent u) Int
participants = F.foldr
(\e -> Map.insertWith (+) e 1)
Map.empty
single :: RecordedIndivEvent u -> ProcessId -> EventMap u
single k v = Map.singleton k (Set.singleton v)
data Cont u = Cont (EventMap u) ([RecordedIndivEvent u] -> Cont u)
| ContDone
instance Monoid (Cont u) where
mempty = ContDone
mappend ContDone r = r
mappend (Cont m f) r = Cont m (\e -> f e `mappend` r)
makeCont :: Ord u => EventHierarchy (RecordedIndivEvent u) -> ProcessId -> Cont u
makeCont (SingleEvent e) pid = c
where
c = Cont (single e pid) wait
wait e'
| e `elem` e' = ContDone
| otherwise = c
makeCont (StructuralSequence 0 _) _ = ContDone
makeCont (StructuralSequence n es) pid
= mconcat (map (uncurry makeCont) $ zip es pidsPlusOne)
`mappend` makeCont (StructuralSequence (n1) es) (last pidsPlusOne)
where
pidsPlusOne = take (1 + length es) $ iterate incPid pid
incPid (ProcessId ps) = ProcessId $ init ps ++ [ParSeq p (succ s)]
where
ParSeq p s = last ps
makeCont (StructuralParallel es) pid
= mergePar (map (uncurry makeCont) $ zip es (parPids pid))
where
parPids (ProcessId ps) = [ProcessId $ ps ++ [ParSeq i 0] | i <- [0..]]
mergePar :: Ord u => [Cont u] -> Cont u
mergePar cs = case [ m | Cont m _f <- cs] of
[] -> ContDone
ms -> Cont (combine ms) (\e -> mergePar [f e | Cont _m f <- cs])
structuralToVCR :: Ord u => StructuralTrace u -> [VCRTrace u]
structuralToVCR (StructuralTrace (ls, Nothing)) = [VCRTrace (ls, [])]
structuralToVCR (StructuralTrace (ls, Just str))
= nubBy eq [VCRTrace (ls, map (Set.map snd) $ reverse $ toVCR $ reverse tr) | tr <- flattenStructural str]
where
eq (VCRTrace (_, a)) (VCRTrace (_, b)) = a == b
toVCR :: Ord u => [(RecordedEvent u, Set.Set ProcessId)]
-> [(Set.Set (Set.Set ProcessId, RecordedEvent u))]
toVCR [] = []
toVCR ((e, pids) : rest)
= prependVCR (toVCR rest) pids [(pids, e)]
structuralToCSP :: Ord u => StructuralTrace u -> [CSPTrace u]
structuralToCSP (StructuralTrace (ls, Nothing)) = [CSPTrace (ls, [])]
structuralToCSP (StructuralTrace (ls, Just str))
= [CSPTrace (ls, map fst tr) | tr <- flattenStructural str]
flattenStructural :: forall u. Ord u => EventHierarchy (RecordedIndivEvent u) -> [[(RecordedEvent u, Set.Set ProcessId)]]
flattenStructural tr
= process $ makeCont tr rootProcessId
where
ps = participants tr
process :: Cont u -> [[(RecordedEvent u, Set.Set ProcessId)]]
process ContDone = [[]]
process (Cont m f)
= concat [map ((e, pids) :) $ process (f ie)
| (e,(ie,pids)) <- Map.toAscList eventsWithAllParticipants]
where
indivEventsWithAllParticipants :: Map.Map (RecordedIndivEvent u) (Set.Set ProcessId)
indivEventsWithAllParticipants = Map.map fst $ Map.filter (\(s, n) -> Set.size s == n) (Map.intersectionWith (,) m ps)
eventsWithAllParticipants :: Map.Map (RecordedEvent u) ([RecordedIndivEvent u], Set.Set ProcessId)
eventsWithAllParticipants
= Map.map snd $
Map.filterWithKey fixEvents $
Map.mapKeysWith mergeVals toWhole $
Map.map ((,) False . first (:[])) $
Map.mapWithKey (,) $
indivEventsWithAllParticipants
where
mergeVals :: (Bool, ([RecordedIndivEvent u], Set.Set ProcessId))
-> (Bool, ([RecordedIndivEvent u], Set.Set ProcessId))
-> (Bool, ([RecordedIndivEvent u], Set.Set ProcessId))
mergeVals (_, (es, pids)) (_, (es', pids'))
= (True, (es ++ es', Set.union pids pids'))
fixEvents :: RecordedEvent a -> (Bool, b) -> Bool
fixEvents (ChannelComm _, _) (b, _) = b
fixEvents _ _ = True
toWhole :: RecordedIndivEvent a -> RecordedEvent a
toWhole (ChannelWrite x _ s) = (ChannelComm s, x)
toWhole (ChannelRead x _ s) = (ChannelComm s, x)
toWhole (BarrierSyncIndiv x _ s) = (BarrierSync s, x)
toWhole (ClockSyncIndiv x _ t) = (ClockSync t, x)