{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-} {-# OPTIONS_GHC -fno-warn-name-shadowing #-} module PopulationProtocol (PopulationProtocol,State(..),Transition(..), Configuration,FlowVector,RConfiguration,RFlowVector, renameState,renameTransition,renameStatesAndTransitions, invertPopulationProtocol, name,showNetName,states,transitions,initialStates,trueStates,falseStates, pre,lpre,post,lpost,mpre,mpost,context, makePopulationProtocol,makePopulationProtocolWithTrans, makePopulationProtocolFromStrings,makePopulationProtocolWithTransFromStrings, Trap,Siphon,Invariant(..)) where import qualified Data.Map as M import qualified Data.Set as S import Control.Arrow (first,(***)) import Data.List (sort,(\\)) import Data.Tuple (swap) import Util newtype State = State String deriving (Ord,Eq) newtype Transition = Transition String deriving (Ord,Eq) instance Show State where show (State q) = q instance Show Transition where show (Transition t) = t type ContextMap a b = M.Map a ([(b, Integer)],[(b, Integer)]) class (Ord a, Ord b) => Nodes a b | a -> b where lpre :: PopulationProtocol -> a -> [(b, Integer)] lpre pp = fst . context pp lpost :: PopulationProtocol -> a -> [(b, Integer)] lpost pp = snd . context pp pre :: PopulationProtocol -> a -> [b] pre pp = map fst . lpre pp post :: PopulationProtocol -> a -> [b] post pp = map fst . lpost pp lmpre :: PopulationProtocol -> [a] -> [(b, Integer)] lmpre pp = listMap . concatMap (lpre pp) lmpost :: PopulationProtocol -> [a] -> [(b, Integer)] lmpost pp = listMap . concatMap (lpost pp) mpre :: PopulationProtocol -> [a] -> [b] mpre pp = map fst . lmpre pp mpost :: PopulationProtocol -> [a] -> [b] mpost pp = map fst . lmpost pp context :: PopulationProtocol -> a -> ([(b, Integer)], [(b, Integer)]) context pp x = M.findWithDefault ([],[]) x (contextMap pp) contextMap :: PopulationProtocol -> ContextMap a b instance Nodes State Transition where contextMap = adjacencyQ instance Nodes Transition State where contextMap = adjacencyT type Configuration = IVector State type FlowVector = IVector Transition type RConfiguration = RVector State type RFlowVector = RVector Transition type Trap = [State] type Siphon = [State] class Invariant a where invariantSize :: a -> Int data PopulationProtocol = PopulationProtocol { name :: String, states :: [State], transitions :: [Transition], initialStates :: [State], trueStates :: [State], falseStates :: [State], adjacencyQ :: M.Map State ([(Transition,Integer)], [(Transition,Integer)]), adjacencyT :: M.Map Transition ([(State,Integer)], [(State,Integer)]) } showNetName :: PopulationProtocol -> String showNetName pp = "Population protocol" ++ (if null (name pp) then "" else " " ++ show (name pp)) instance Show PopulationProtocol where show pp = showNetName pp ++ "\nStates : " ++ show (states pp) ++ "\nTransitions : " ++ show (transitions pp) ++ "\nInitial states : " ++ show (initialStates pp) ++ "\nTrue states : " ++ show (trueStates pp) ++ "\nFalse states : " ++ show (falseStates pp) ++ "\nState arcs :\n" ++ unlines (map showContext (M.toList (adjacencyQ pp))) ++ "\nTransition arcs:\n" ++ unlines (map showContext (M.toList (adjacencyT pp))) where showContext (s,(l,r)) = show l ++ " -> " ++ show s ++ " -> " ++ show r renameState :: (String -> String) -> State -> State renameState f (State q) = State (f q) renameTransition :: (String -> String) -> Transition -> Transition renameTransition f (Transition t) = Transition (f t) renameStatesAndTransitions :: (String -> String) -> PopulationProtocol -> PopulationProtocol renameStatesAndTransitions f pp = PopulationProtocol { name = name pp, states = listSet $ map (renameState f) $ states pp, transitions = listSet $ map (renameTransition f) $ transitions pp, initialStates = listSet $ map (renameState f) $ initialStates pp, trueStates = listSet $ map (renameState f) $ trueStates pp, falseStates = listSet $ map (renameState f) $ falseStates pp, adjacencyQ = mapAdjacency (renameState f) (renameTransition f) $ adjacencyQ pp, adjacencyT = mapAdjacency (renameTransition f) (renameState f) $ adjacencyT pp } where mapAdjacency f g m = M.mapKeys f (M.map (mapContext g) m) mapContext f (pre, post) = (listMap (map (first f) pre), listMap (map (first f) post)) invertPopulationProtocol :: PopulationProtocol -> PopulationProtocol invertPopulationProtocol pp = PopulationProtocol { name = name pp, states = states pp, transitions = transitions pp, initialStates = initialStates pp, trueStates = trueStates pp, falseStates = falseStates pp, adjacencyQ = M.map swap $ adjacencyQ pp, adjacencyT = M.map swap $ adjacencyT pp } makePopulationProtocol :: String -> [State] -> [Transition] -> [State] -> [State] -> [State] -> [Either (Transition, State, Integer) (State, Transition, Integer)] -> PopulationProtocol makePopulationProtocol name states transitions initialStates trueStates falseStates arcs = PopulationProtocol { name = name, states = listSet states, transitions = listSet transitions, initialStates = listSet initialStates, trueStates = listSet trueStates, falseStates = listSet falseStates, adjacencyQ = M.map (listMap *** listMap) adQ, adjacencyT = M.map (listMap *** listMap) adT } where (adQ, adT) = foldl buildMaps (M.empty, M.empty) arcs buildMaps (mq,mt) (Left (_,_,0)) = (mq,mt) buildMaps (mq,mt) (Right (_,_,0)) = (mq,mt) buildMaps (mq,mt) (Right (q,t,w)) = let mq' = M.insertWith addArc q ([],[(t,w)]) mq mt' = M.insertWith addArc t ([(q,w)],[]) mt in (mq',mt') buildMaps (mq,mt) (Left (t,q,w)) = let mt' = M.insertWith addArc t ([],[(q,w)]) mt mq' = M.insertWith addArc q ([(t,w)],[]) mq in (mq',mt') addArc (lNew,rNew) (lOld,rOld) = (lNew ++ lOld,rNew ++ rOld) makePopulationProtocolFromStrings :: String -> [String] -> [String] -> [String] -> [String] -> [String] -> [(String, String, Integer)] -> PopulationProtocol makePopulationProtocolFromStrings name states transitions initialStates trueStates falseStates arcs = makePopulationProtocol name (map State (S.toAscList stateSet)) (map Transition (S.toAscList transitionSet)) (map State initialStates) (map State trueStates) (map State falseStates) (map toEitherArc arcs) where stateSet = S.fromList states transitionSet = S.fromList transitions toEitherArc (l,r,w) = let lq = l `S.member` stateSet lt = l `S.member` transitionSet rq = r `S.member` stateSet rt = r `S.member` transitionSet in case (lq,lt,rq,rt) of (True,False,False,True) -> Right (State l, Transition r, w) (False,True,True,False) -> Left (Transition l, State r, w) (False,False,_,_) -> error $ l ++ " not a declared state or transition " (_,_,False,False) -> error $ r ++ " not a declared state or transition " (True,_,True,_) -> error $ l ++ " and " ++ r ++ " both states" (_,True,_,True) -> error $ l ++ " and " ++ r ++ " both transitions" makePopulationProtocolWithTrans :: String -> [State] -> [State] -> [State] -> [State] -> [(Transition, ([(State, Integer)], [(State, Integer)]))] -> PopulationProtocol makePopulationProtocolWithTrans name states initialStates trueStates falseStates ts = makePopulationProtocol name states (map fst ts) initialStates trueStates falseStates arcs where arcs = [ Right (q,t,w) | (t,(is,_)) <- ts, (q,w) <- is ] ++ [ Left (t,q,w) | (t,(_,os)) <- ts, (q,w) <- os ] makePopulationProtocolWithTransFromStrings :: String -> [String] -> [String] -> [String] -> [String] -> [(String, ([(String, Integer)], [(String, Integer)]))] -> PopulationProtocol makePopulationProtocolWithTransFromStrings name states initialStates trueStates falseStates arcs = makePopulationProtocolWithTrans name (map State states) (map State initialStates) (map State trueStates) (map State falseStates) (map toTArc arcs) where toTArc (t, (iq, oq)) = (Transition t, (map (first State) iq, map (first State) oq))