PopulationProtocol.hs 9.38 KB
Newer Older
1 2 3 4
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
{-# OPTIONS_GHC -fno-warn-name-shadowing #-}

module PopulationProtocol
5 6
    (PopulationProtocol,State(..),Transition(..),
     Configuration,FlowVector,RConfiguration,RFlowVector,
7
     renameState,renameTransition,renameStatesAndTransitions,
8
     name,showNetName,states,transitions,initialStates,trueStates,falseStates,
9 10
     pre,lpre,post,lpost,mpre,mpost,context,
     makePopulationProtocol,makePopulationProtocolWithTrans,
11 12
     makePopulationProtocolFromStrings,makePopulationProtocolWithTransFromStrings,
     Trap,Siphon,Invariant(..))
13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57
where

import qualified Data.Map as M
import qualified Data.Set as S
import Control.Arrow (first,(***))
import Data.List (sort,(\\))

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

58
type Configuration = IVector State
59
type FlowVector = IVector Transition
60

61
type RConfiguration = RVector State
62
type RFlowVector = RVector Transition
63 64 65 66 67 68 69 70 71 72 73 74

type Trap = [State]
type Siphon = [State]

class Invariant a where
        invariantSize :: a -> Int

data PopulationProtocol = PopulationProtocol {
        name :: String,
        states :: [State],
        transitions :: [Transition],
        initialStates :: [State],
75 76
        trueStates :: [State],
        falseStates :: [State],
77 78 79 80 81 82 83 84 85 86
        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 ++
87 88 89 90 91 92
                   "\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
93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114
                        (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,
115 116 117 118
                trueStates =
                    listSet $ map (renameState f) $ trueStates pp,
                falseStates =
                    listSet $ map (renameState f) $ falseStates pp,
119 120 121 122 123 124 125 126 127 128 129 130 131
                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))

makePopulationProtocol :: String -> [State] -> [Transition] ->
        [State] -> [State] -> [State] ->
        [Either (Transition, State, Integer) (State, Transition, Integer)] ->
        PopulationProtocol
132
makePopulationProtocol name states transitions initialStates trueStates falseStates arcs =
133 134 135 136 137
            PopulationProtocol {
                name = name,
                states = listSet states,
                transitions = listSet transitions,
                initialStates = listSet initialStates,
138 139
                trueStates = listSet trueStates,
                falseStates = listSet falseStates,
140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162
                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
163
makePopulationProtocolFromStrings name states transitions initialStates trueStates falseStates arcs =
164 165 166 167 168
            makePopulationProtocol
                name
                (map State (S.toAscList stateSet))
                (map Transition (S.toAscList transitionSet))
                (map State initialStates)
169 170
                (map State trueStates)
                (map State falseStates)
171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196
                (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
197 198
makePopulationProtocolWithTrans name states initialStates trueStates falseStates ts =
            makePopulationProtocol name states (map fst ts) initialStates trueStates falseStates arcs
199 200 201 202 203 204 205
        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
206
makePopulationProtocolWithTransFromStrings name states initialStates trueStates falseStates arcs =
207 208 209 210
            makePopulationProtocolWithTrans
                name
                (map State states)
                (map State initialStates)
211 212
                (map State trueStates)
                (map State falseStates)
213 214 215 216
                (map toTArc arcs)
        where
            toTArc (t, (iq, oq)) =
                (Transition t, (map (first State) iq, map (first State) oq))