module Scyther.Formula (
Atom(..)
, Formula(..)
, substAtom
, relabelTIDs
, hasQuantifiers
, conjuncts
, conjunctionToAtoms
, isTypingFormula
, destTypingFormula
, atomTIDs
, findRole
, isaCompr
, isaUncompr
, sptAtom
, isaAtom
, isaFormula
, sptFormula
) where
import Data.Maybe
import Data.Data
import Control.Applicative as App
import Control.Monad
import Control.Monad.State
import Control.Monad.Reader
import Text.Isar
import Scyther.Protocol
import Scyther.Message
import Scyther.Equalities as E
import Scyther.Event
import Scyther.Typing
data Atom =
AFalse
| AEq AnyEq
| AEv Event
| AEvOrd (Event, Event)
| ACompr Message
| AUncompr Message
| AHasType MVar (Maybe Type)
| ATyping Typing
| AReachable Protocol
deriving( Eq, Show, Ord, Data, Typeable )
data Formula =
FAtom Atom
| FConj Formula Formula
| FExists (Either TID AgentId) Formula
deriving( Eq, Show, Ord, Data, Typeable )
isTypingFormula :: Formula -> Bool
isTypingFormula = isJust . destTypingFormula
destTypingFormula :: Formula -> Maybe Typing
destTypingFormula (FAtom (ATyping typ)) = return typ
destTypingFormula _ = mzero
relabelTIDs :: [TID] -> Formula -> Formula
relabelTIDs tids0 formula =
runReader (evalStateT (go formula) tids0) (Mapping E.empty)
where
go (FAtom atom) = FAtom <$> ((substAtom . getMappingEqs) <$> ask <*> pure atom)
go (FConj l r) = FConj <$> go l <*> go r
go (FExists (Left tid) inner) = do
tids <- get
case tids of
[] -> error "relabelTIDs: out of labels"
tid':tids' -> do
put tids'
FExists (Left tid') <$> local (addTIDMapping tid tid') (go inner)
go (FExists q@(Right _) inner) = FExists q <$> go inner
atomTIDs :: Atom -> [TID]
atomTIDs AFalse = mzero
atomTIDs (ATyping _) = mzero
atomTIDs (AReachable _) = mzero
atomTIDs (AEv e) = evTIDs e
atomTIDs (AEvOrd ord) = evOrdTIDs ord
atomTIDs (ACompr m) = msgTIDs m
atomTIDs (AUncompr m) = msgTIDs m
atomTIDs (AHasType v _) = return $ mvarTID v
atomTIDs (AEq eq) = anyEqTIDs eq
substAtom :: Equalities -> Atom -> Atom
substAtom eqs atom = case atom of
AFalse -> atom
AEq eq -> AEq $ substAnyEq eqs eq
AEv ev -> AEv $ substEv eqs ev
AEvOrd ord -> AEvOrd $ substEvOrd eqs ord
ACompr m -> ACompr $ substMsg eqs m
AUncompr m -> AUncompr $ substMsg eqs m
AHasType mv ty -> AHasType (mapMVar (substLocalId eqs) mv) ty
ATyping _ -> atom
AReachable _ -> atom
hasQuantifiers :: Formula -> Bool
hasQuantifiers = isNothing . conjunctionToAtoms
conjunctionToAtoms :: MonadPlus m => Formula -> m [Atom]
conjunctionToAtoms (FAtom a) = return [a]
conjunctionToAtoms (FConj f1 f2) =
(++) `liftM` conjunctionToAtoms f1 `ap` conjunctionToAtoms f2
conjunctionToAtoms _ =
fail "conjunctionToAtoms: existential quantifier encountered."
conjuncts :: Formula -> [Formula]
conjuncts (FConj f1 f2) = conjuncts f1 ++ conjuncts f2
conjuncts f = pure f
findRole :: TID -> Formula -> Maybe Role
findRole tid = go
where
go (FAtom (AEq (TIDRoleEq (tid', role))))
| tid == tid' = return role
| otherwise = mzero
go (FAtom _) = mzero
go (FConj f1 f2) = go f1 `mplus` go f2
go (FExists v f)
| Left tid == v = mzero
| otherwise = go f
isaCompr :: IsarConf -> Message -> Doc
isaCompr conf m = text "RLKR" <> parens (isar conf m) <-> isaIn conf <-> text "reveals t"
isaUncompr :: IsarConf -> Message -> Doc
isaUncompr conf m = text "RLKR" <> parens (isar conf m) <-> isaNotIn conf <-> text "reveals t"
sptCompr :: Message -> Doc
sptCompr m = text "compromised" <> parens (sptMessage m)
sptUncompr :: Message -> Doc
sptUncompr m = text "uncompromised" <> parens (sptMessage m)
isaAtom :: IsarConf -> Mapping -> Atom -> Doc
isaAtom conf mapping atom = case atom of
AFalse -> text "False"
AEq eq -> ppIsar eq
AEv ev -> isaEvent conf mapping ev
AEvOrd ord -> isaEventOrd conf mapping ord
ACompr av -> isaCompr conf av
AUncompr av -> isaUncompr conf av
AHasType mv ty -> let tid = mvarTID mv
optRole = threadRole tid (getMappingEqs mapping)
in ppIsar mv <-> isaIn conf <->
isaOptType conf optRole ty <-> ppIsar (mvarTID mv) <->
isaExecutionSystemState conf
ATyping _ -> text "well-typed"
AReachable p ->
text "(t,r,s)" <-> isaIn conf <-> text "reachable" <-> text (protoName p)
where
ppIsar :: Isar a => a -> Doc
ppIsar = isar conf
sptAtom :: Mapping -> Atom -> Doc
sptAtom mapping atom = case atom of
AFalse -> text "False"
AEq eq -> sptAnyEq eq
AEv ev -> sptEvent mapping ev
AEvOrd (e1,e2) -> sptEventOrd mapping [e1,e2]
ACompr av -> sptCompr av
AUncompr av -> sptUncompr av
AHasType mv ty -> let optRole = threadRole (mvarTID mv) (getMappingEqs mapping)
in sptMVar mv <-> text "::" <-> sptOptType optRole ty
ATyping WeaklyAtomic -> text "weakly-atomic"
ATyping typ -> sptTyping typ
AReachable p -> text "reachable" <-> text (protoName p)
isaFormula :: IsarConf -> Mapping -> Formula -> Doc
isaFormula conf = pp
where
ppIsar :: Isar a => a -> Doc
ppIsar = isar conf
pp m (FAtom atom) = isaAtom conf m atom
pp m (FConj f1 f2) = sep [pp m f1 <-> isaAnd conf, pp m f2]
pp m (FExists v f) = parens $
sep [ isaExists conf <-> (either ppIsar ppIsar v) <> char '.'
, nest 2 $ pp m' f
]
where
m' = case v of
Left tid -> maybe id (addTIDRoleMapping tid) (findRole tid f) m
Right _ -> m
sptFormula :: Mapping -> Formula -> Doc
sptFormula = pp
where
pp m (FAtom atom) = sptAtom m atom
pp m (FConj f1 f2) = sep [pp m f1 <-> char '&', pp m f2]
pp m (FExists v f) = parens $
sep [ char '?' <-> (either sptTID sptAgentId v) <> char '.'
, nest 2 $ pp m' f
]
where
m' = case v of
Left tid -> maybe id (addTIDRoleMapping tid) (findRole tid f) m
Right _ -> m