PopulationProtocol.hs 10.5 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
     invertPopulationProtocol,
9
     name,showNetName,states,transitions,initialStates,trueStates,falseStates,predicate,
10
11
     pre,lpre,post,lpost,mpre,mpost,context,
     makePopulationProtocol,makePopulationProtocolWithTrans,
12
13
     makePopulationProtocolFromStrings,makePopulationProtocolWithTransFromStrings,
     Trap,Siphon,Invariant(..))
14
15
16
17
18
19
where

import qualified Data.Map as M
import qualified Data.Set as S
import Control.Arrow (first,(***))
import Data.List (sort,(\\))
20
import Data.Tuple (swap)
21
22

import Util
23
import Property
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
58
59
60

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

61
type Configuration = IVector State
62
type FlowVector = IVector Transition
63

64
type RConfiguration = RVector State
65
type RFlowVector = RVector Transition
66
67
68
69
70
71
72
73
74
75
76
77

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

class Invariant a where
        invariantSize :: a -> Int

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

135
136
137
138
139
140
141
142
143
invertPopulationProtocol :: PopulationProtocol -> PopulationProtocol
invertPopulationProtocol pp =
            PopulationProtocol {
                name             = name pp,
                states           = states pp,
                transitions      = transitions pp,
                initialStates    = initialStates pp,
                trueStates       = trueStates pp,
                falseStates      = falseStates pp,
144
                predicate        = predicate pp,
145
146
147
148
149
150
                adjacencyQ       = M.map swap $ adjacencyQ pp,
                adjacencyT       = M.map swap $ adjacencyT pp
            }



151
makePopulationProtocol :: String -> [State] -> [Transition] ->
152
        [State] -> [State] -> [State] -> QuantFormula State ->
153
154
        [Either (Transition, State, Integer) (State, Transition, Integer)] ->
        PopulationProtocol
155
makePopulationProtocol name states transitions initialStates trueStates falseStates predicate arcs =
156
157
158
159
160
            PopulationProtocol {
                name = name,
                states = listSet states,
                transitions = listSet transitions,
                initialStates = listSet initialStates,
161
162
                trueStates = listSet trueStates,
                falseStates = listSet falseStates,
163
                predicate = predicate,
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
                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] ->
186
        QuantFormula String -> [(String, String, Integer)] -> PopulationProtocol
187
makePopulationProtocolFromStrings name states transitions initialStates trueStates falseStates predicate arcs =
188
189
190
191
192
            makePopulationProtocol
                name
                (map State (S.toAscList stateSet))
                (map Transition (S.toAscList transitionSet))
                (map State initialStates)
193
194
                (map State trueStates)
                (map State falseStates)
195
                (fmap State predicate)
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
                (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] ->
220
        QuantFormula State -> [(Transition, ([(State, Integer)], [(State, Integer)]))] ->
221
        PopulationProtocol
222
223
makePopulationProtocolWithTrans name states initialStates trueStates falseStates predicate ts =
            makePopulationProtocol name states (map fst ts) initialStates trueStates falseStates predicate arcs
224
225
226
227
228
        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] ->
229
        QuantFormula String -> [(String, ([(String, Integer)], [(String, Integer)]))] ->
230
        PopulationProtocol
231
makePopulationProtocolWithTransFromStrings name states initialStates trueStates falseStates predicate arcs =
232
233
234
235
            makePopulationProtocolWithTrans
                name
                (map State states)
                (map State initialStates)
236
237
                (map State trueStates)
                (map State falseStates)
238
                (fmap State predicate)
239
240
241
242
                (map toTArc arcs)
        where
            toTArc (t, (iq, oq)) =
                (Transition t, (map (first State) iq, map (first State) oq))