module Scyther.Event (
Event(..)
, substEv
, substEvOrd
, evTIDs
, evOrdTIDs
, EventOrder
, cyclic
, before
, isaEvent
, isaEventOrd
, sptEvent
, sptRawEvent
, sptEventOrd
) where
import qualified Data.Set as S
import Data.Data
import Control.Arrow ( (***) )
import Control.Monad
import Text.Isar
import Scyther.Protocol
import Scyther.Message
import Scyther.Equalities
data Event =
Step TID RoleStep
| Learn Message
deriving( Eq, Ord, Show, Data, Typeable )
type EventOrder = S.Set (Event,Event)
cyclic :: EventOrder -> Bool
cyclic evord =
maybe True (const False) $ foldM visitForest S.empty (map fst evPairs)
where
evPairs = S.toList evord
visitForest visited x
| x `S.member` visited = return visited
| otherwise = findLoop S.empty visited x
findLoop parents visited x
| x `S.member` parents = mzero
| x `S.member` visited = return visited
| otherwise =
S.insert x `liftM` foldM (findLoop parents') visited next
where
next = [ e' | (e,e') <- evPairs, e == x ]
parents' = S.insert x parents
before :: EventOrder -> Event -> Event -> Bool
before evord from to = existsPath S.empty [from]
where
evPairs = S.toList evord
existsPath _ [] = False
existsPath visited (x:xs)
| x == to = True
| x `S.member` visited = existsPath visited xs
| otherwise =
existsPath (S.insert x visited) (next ++ xs)
where
next = [ e' | (e,e') <- evPairs, e == x ]
substEv :: Equalities -> Event -> Event
substEv eqs (Learn m) = Learn (substMsg eqs m)
substEv eqs (Step tid step) = Step (substTID eqs tid) step
substEvOrd :: Equalities -> (Event, Event) -> (Event, Event)
substEvOrd eqs = substEv eqs *** substEv eqs
evTIDs :: Event -> [TID]
evTIDs (Step tid _) = return tid
evTIDs (Learn m) = msgTIDs m
evOrdTIDs :: (Event, Event) -> [TID]
evOrdTIDs (e1, e2) = evTIDs e1 `mplus` evTIDs e2
eventTag :: (Event -> Doc)
-> (Doc -> Doc)
-> (Doc -> Doc)
-> Event -> Doc
eventTag pp ln _ ev@(Learn _) = ln (pp ev)
eventTag pp _ st ev@(Step _ _) = st (pp ev)
esplBefore :: IsarConf -> Doc -> Doc -> Doc
esplBefore conf e1 e2
| isPlainStyle conf = sep [text "predOrd t", nest 2 (parens e1), nest 2 (parens e2)]
| otherwise = sep [e1 <-> symbol "\\<prec>", e2]
isaRawEvent :: Bool -> IsarConf -> Mapping -> Event -> Doc
isaRawEvent addParens conf _ (Learn m) =
(if addParens then parens else id) $ isar conf m
isaRawEvent _ conf mapping (Step tid step) =
nestShort 2 lparen rparen (fsep [isar conf tid <> comma, ppStep])
where
ppStep = isaRoleStep conf (threadRole tid (getMappingEqs mapping)) step
isaEvent :: IsarConf
-> Mapping
-> Event -> Doc
isaEvent conf m =
eventTag (isaRawEvent False conf m) (inSet "knows t") (inSet "steps t")
where
inSet set d = d <-> isaIn conf <-> text set
isaEventOrd :: IsarConf -> Mapping -> (Event, Event) -> Doc
isaEventOrd conf m (e1, e2) =
esplBefore conf (ppEv e1) (ppEv e2)
where
ppEv = eventTag (isaRawEvent True conf m) (text "Ln" <>) (text "St" <>)
instance Isar Event where
isar conf = isaEvent conf (Mapping empty)
sptRawEvent :: Mapping -> Event -> Doc
sptRawEvent _ (Learn m) = sptMessage m
sptRawEvent mapping (Step tid step) =
parens $ fsep [sptTID tid <> comma, ppStep]
where
ppStep = sptRoleStep (threadRole tid (getMappingEqs mapping)) step
sptEvent :: Mapping -> Event -> Doc
sptEvent m = eventTag (sptRawEvent m) ((text "knows" <>) . parens) (text "step" <>)
sptEventOrd :: Mapping -> [Event] -> Doc
sptEventOrd m =
fcat . punctuate (text " < ") . map ppEv
where
ppEv = eventTag (sptRawEvent m) ((text "Ln" <>) . parens) (text "St" <>)