PopulationProtocol.hs 17.9 KB
Newer Older
Stefan Jaax's avatar
Stefan Jaax committed
1
2
3
4
5
6
7
8
9
10
module PopulationProtocol ( PopulationProtocol (..) 
                          , Population
                          , createModuloProtocol
                          , createThresholdProtocol
                          , createOldThresholdProtocol
                          , createMajorityProtocol
                          , createFlockOfBirdsProtocol
                          , createVerifiableFlockOfBirdsProtocol
                          , createNewBirdsProtocol
                          , createBroadcastProtocol
Stefan Jaax's avatar
Stefan Jaax committed
11
                          , createLogFlockOfBirdsProtocol
Stefan Jaax's avatar
Stefan Jaax committed
12
                          , createEfficientThresholdProtocol
Stefan Jaax's avatar
Stefan Jaax committed
13
14
15
                          , simpleProtocol
                          , MajorityState(..)
                          , createMLayerProtocol
Stefan Jaax's avatar
Stefan Jaax committed
16
                          , createPolyLogFlockOfBirdsProtocol
Stefan Jaax's avatar
Stefan Jaax committed
17
18
                          ) where

19
import Util
Stefan Jaax's avatar
Stefan Jaax committed
20
21
22
23
import qualified Data.Set as S
import qualified Data.MultiSet as MS
import qualified Data.Map.Strict as M
import Data.Tuple (swap)
Stefan Jaax's avatar
Stefan Jaax committed
24
import Data.List (intercalate, nub)
Stefan Jaax's avatar
Stefan Jaax committed
25
import Data.Maybe (catMaybes, fromMaybe)
Stefan Jaax's avatar
Stefan Jaax committed
26
import Data.Bits
Stefan Jaax's avatar
Stefan Jaax committed
27
28
29
30
31

data PopulationProtocol qs = PopulationProtocol { states :: [qs]
                                                , initial :: [qs]
                                                , trans :: (qs, qs) -> (qs, qs)
                                                , opinion :: qs -> Bool
32
                                                , predicate :: Maybe String
Stefan Jaax's avatar
Stefan Jaax committed
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
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
                                                }


type ThresholdProtocol = PopulationProtocol (ThresholdState)

type ModuloProtocol = PopulationProtocol (ModuloState)

type MajorityProtocol = PopulationProtocol (MajorityState)

type OldThresholdProtocol = PopulationProtocol (OldThresholdState)

type SimpleProtocol = PopulationProtocol (SimpleState)

type FlockOfBirdsProtocol = PopulationProtocol Int

type VerifiableFlockOfBirdsProtocol = PopulationProtocol (Bool, Int)

type Population qs = MS.MultiSet qs

data ThresholdState = Neg Int | Pos Int | BiasPos Int | Passive Bool deriving (Ord, Eq, Show)

data SimpleState = L Int | NL Int deriving (Ord, Eq, Show) 

data ModuloState = Mod Int | ModPassive Bool deriving (Ord, Eq, Show)

data MajorityState = A | B | Asmall | Bsmall deriving (Ord, Eq, Show)

data OldThresholdState = OldThresholdState { leaderBit :: Bool
                                           , outputBit :: Bool
                                           , numVal :: Int
                                           } deriving (Ord, Eq)

instance Show OldThresholdState where
  show q = let leaderStr = if leaderBit q then "L" else "NL"
               outputStr = "_" ++ show (outputBit q)
               numStr =  "_" ++ awkwardShowInt (numVal q)
           in
      leaderStr ++ outputStr ++ numStr


simpleProtocol :: SimpleProtocol
simpleProtocol = PopulationProtocol { states = [L 9, NL 2, NL 4, L 10, NL 1, NL 3]
                                    , initial = [L 9]
                                    , trans = simpleTrans
                                    , opinion = \x -> True
78
                                    , predicate = Nothing
Stefan Jaax's avatar
Stefan Jaax committed
79
80
81
82
83
84
                                    } where
  simpleTrans (L 9, NL 2) = (L 10, NL 1)
  simpleTrans (L 9, NL 4) = (L 10, NL 3)
  simpleTrans (q, r) = (q, r)


Stefan Jaax's avatar
Stefan Jaax committed
85
86
data THState = THVal (Int, Int) | Passivo | Eater deriving (Show, Eq, Ord)

Stefan Jaax's avatar
Stefan Jaax committed
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
floorLog :: Int -> Int
floorLog = floor . logBase 2 . fromIntegral

g :: Int -> Int 
g n = n - 2^(floorLog n)

maxLevel :: Int -> Int
maxLevel n | n == 0    = -1
           | otherwise = 1 + maxLevel (g n)

maxOnLevel i n = floorLog (iterate g n !! i)

createLogFlockOfBirdsProtocol :: Int -> PopulationProtocol Int
createLogFlockOfBirdsProtocol c = PopulationProtocol{ states = nub logQ
                                                    , initial = [1, 0]
                                                    , opinion = (== c)
                                                    , trans = logTrans
                                                    , predicate = Just $ toVar 1 ++ " >= " ++ show c} where
  logQ = [2^i | i <- [0..(floorLog c-1)]] ++ [c .&. (shift (complement 0) i) | i <- [0..(floorLog c + 1)]]
  logTrans (x, y) | x + y >= c = (c, c)
                  | x == y && 2*x < c = (2*x, 0)
                  | y >= floorLog c && y + x `elem` logQ = (x+y, 0)
                  | otherwise = (x, y)
createPolyLogFlockOfBirdsProtocol :: Int -> PopulationProtocol THState
createPolyLogFlockOfBirdsProtocol c = 
  PopulationProtocol{ states = logStates c ++ [Eater, Passivo]
                    , initial = [THVal(0, 0)]
                    , trans = logTrans
                    , opinion = \x -> x == Eater
                    , predicate = Just $ toVar (THVal (0, 0)) ++  ">= " ++ show c
                    } where
    logStates c = concat [[THVal (i, j) | j <- [0..maxOnLevel i c]] | i <- [0..maxLevel c]]
    logTrans (_, Eater) = (Eater, Eater)
    logTrans (THVal (i1, j1), THVal (i2, j2)) | i2 == maxLevel c && j2 == maxOnLevel (maxLevel c) c = (Eater, Eater)
                                              | i1 == i2 && j1 == j2 && j1 < maxOnLevel i1 c = (Passivo, THVal (i1, j1+1))
                                              | i1 == i2 && j2 == maxOnLevel i2 c = if j1 <= maxOnLevel (i1+1) c then
                                                                                      (THVal (i1+1, j1), THVal (i2, j2))
                                                                                    else
                                                                                      (Eater, Eater)
                                              | otherwise = (THVal (i1, j1), THVal (i2, j2))
    logTrans (a,b) = (a, b)

Stefan Jaax's avatar
Stefan Jaax committed
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
polylog :: Int -> Int
polylog 1 = 0
polylog n = let n' = 2^((floor . logBase 2 . fromIntegral) n) in
  if (n - n') == 0 then
    0
  else
    1 + polylog (n - n')

polyrange :: Int -> Int -> Int
polyrange i  n = if i == 0 then 
                  (floor . logBase 2 . fromIntegral) n 
                else
                  polyrange (i-1) (n - 2^((floor . logBase 2 . fromIntegral) n)) 

createEfficientThresholdProtocol :: Int -> PopulationProtocol THState
createEfficientThresholdProtocol c = let lg_bound = (floor . logBase 2 . fromIntegral) c in 
  PopulationProtocol { states = [THVal (i, 2^j) | i <- [0..polylog c], j <- [0..polyrange i c]] ++ [Passivo, Eater]
                     , initial = [THVal (0, 1)]
                     , trans = trans'
                     , opinion = \x -> x == Eater
         , predicate = Just $ toVar 1 ++  ">= " ++ show c
                     } where
  max_m i = maximum [m | THVal (x, m) <- states (createEfficientThresholdProtocol c), x == i]
  max_i = maximum [i | THVal(i, m) <- states (createEfficientThresholdProtocol c)]
  max_i_m = THVal (max_i, max_m max_i) 
  trans' (Eater, _) = (Eater, Eater)
  trans' (_, Eater) = (Eater, Eater)
  trans' (THVal (i1, m1), THVal (i2, m2)) =   if THVal (i2, m2) == max_i_m then
                                                (Eater, Eater)
                                              else
                                                if i1 == i2 then
                                                  if m1 == m2 && m2 /= max_m i2 then
                                                    (THVal (i2, 2*m2), Passivo)
                                                  else
                                                    if m2 == max_m i2 then
                                                      if m1 < m2 && (THVal (i2+1, m1) `elem` (states (createEfficientThresholdProtocol c))) then
                                                        (THVal (i2+1, m1), THVal(i2, m2))
                                                      else
                                                        (Eater, Eater)
                                                    else
                                                      (THVal (i1, m1), THVal (i2, m2))
                                                else
                                                  (THVal (i1, m1), THVal (i2, m2))
  trans' (a, b) = (a, b)

Stefan Jaax's avatar
Stefan Jaax committed
174
175
176
177
178
createMLayerProtocol :: Int -> PopulationProtocol Int
createMLayerProtocol m = PopulationProtocol { states = [i | i <- [1..(2*m)]]
                                            , initial = states (createMLayerProtocol m)
                                            , trans = layerTrans
                                            , opinion = \x -> True
179
                                            , predicate = Nothing
Stefan Jaax's avatar
Stefan Jaax committed
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
                                            } where
  layerTrans (q1, q2) = let boolToSign b = if b then 1 else -1
                            boolToVal b = if b then 1 else 0 in
    if odd q1 && q2 == (q1 + 1) then
      if q2 == (2*m) then
        (q2, q2)
      else 
        (q1+2, q2+2)
     else
      if q1 < q2 then
        (q1, q2 + (boolToSign (even q1))*(boolToVal (even q1 && odd q2 || odd q1 && even q2)))
      else
        (q1, q2)


createBroadcastProtocol :: PopulationProtocol Bool
createBroadcastProtocol = PopulationProtocol { states = [True, False]
                                             , initial = states (createBroadcastProtocol)
                                             , trans = \(q1, q2) -> (q1 || q2, q1 || q2)
199
200
201
                                             , opinion = \q -> q
                                             , predicate = Just (toVar True ++ " >= 1")
                                             }
Stefan Jaax's avatar
Stefan Jaax committed
202
203
204
205
206
207


createVerifiableFlockOfBirdsProtocol :: Int -> VerifiableFlockOfBirdsProtocol
createVerifiableFlockOfBirdsProtocol i = PopulationProtocol { states = [(b, j) | b <- [True, False], j <- [0..i]]
                                                            , initial = [((i == 1), 1)]
                                                            , trans = verifiableFlockOfBirdsTrans
208
209
210
                                                            , opinion = \(b, _) -> b
                                                            , predicate = Nothing
                                                            } where
Stefan Jaax's avatar
Stefan Jaax committed
211
212
213
214
215
216
217
218
219
220
221
  verifiableFlockOfBirdsTrans ((b1, n1), (b2, n2)) = if n1 + n2 < i then
                                                        ((b1, n1 + n2), (b2, 0))
                                                     else
                                                        ((True, i), (True, (n1+n2) - i))


createFlockOfBirdsProtocol :: Int -> FlockOfBirdsProtocol
createFlockOfBirdsProtocol i = PopulationProtocol { states = [0..i]
                                                  , initial = [0, 1]
                                                  , trans = flockOfBirdsTrans
                                                  , opinion = flockOfBirdsOpinion
222
                                                  , predicate = Just flockOfBirdsPredicate
Stefan Jaax's avatar
Stefan Jaax committed
223
224
225
226
227
228
                                                  } where
  flockOfBirdsTrans (q1, q2) =  if q1 + q2 < i then
                                  (q1 + q2, 0)
                                else
                                  (i, i)
  flockOfBirdsOpinion x = (x == i)
229
  flockOfBirdsPredicate = (toVar 1) ++ " >= " ++ show i
Stefan Jaax's avatar
Stefan Jaax committed
230
231
232
233
234
235


createNewBirdsProtocol :: Int -> PopulationProtocol Int
createNewBirdsProtocol i = PopulationProtocol { states = [0..i]
                                              , initial = [0, 1]
                                              , trans = newBirdsTrans
236
237
238
                                              , opinion = (== i)
                                              , predicate = Just newBirdsPredicate
                                              } where
Stefan Jaax's avatar
Stefan Jaax committed
239
240
241
  newBirdsTrans (q, q') | (q == q' && q > 0 && q < i) = (q, q + 1)
                        | (q == i || q' == i) = (i, i)
                        | otherwise = (q, q')
242
  newBirdsPredicate = (toVar 1) ++ " >= " ++ show i
Stefan Jaax's avatar
Stefan Jaax committed
243
244
245
246
247
248


createOldThresholdProtocol :: Int -> Int -> OldThresholdProtocol
createOldThresholdProtocol lmax c = PopulationProtocol { states = [OldThresholdState b1 b2 s | b1 <- [True, False]
                                                                                             , b2 <- [True, False]
                                                                                             , s  <- [-lmax..lmax]]
249
                                                       , initial = oldThresholdInitial
Stefan Jaax's avatar
Stefan Jaax committed
250
251
                                                       , trans = oldThresholdTrans
                                                       , opinion = outputBit
252
                                                       , predicate = Just oldThresholdPredicate
Stefan Jaax's avatar
Stefan Jaax committed
253
                                                       } where
254
255
  oldThresholdInitial = [q | q <- states (createOldThresholdProtocol lmax c) , leaderBit q]

Stefan Jaax's avatar
Stefan Jaax committed
256
257
258
259
260
261
262
  oldThresholdTrans (q1, q2) =  if leaderBit q1 || leaderBit q2 then 
                                  (OldThresholdState True (b q1 q2) (l q1 q2), 
                                   OldThresholdState False (b q1 q2) (r q1 q2))
                                else
                                  (q1, q2) where
  b q1 q2 = l q1 q2 < c
  l q1 q2 = max (-lmax) (min lmax (numVal q1 + numVal q2))
263
264
265
266
  r q1 q2 = numVal q1 + numVal q2 - l q1 q2

  oldThresholdPredicate = (intercalate " + " [ show (numVal q) ++ " * " ++ toVar q | q <- oldThresholdInitial ]) ++
                            " < " ++ (show c)
Stefan Jaax's avatar
Stefan Jaax committed
267
268
269
270
271
272
273


createModuloProtocol :: Int -> Int -> ModuloProtocol
createModuloProtocol n c = PopulationProtocol { states = [Mod i | i <- [0..(n-1)]] ++ [ModPassive True, ModPassive False]
                                              , initial = [Mod i | i <- [0..(n-1)]]
                                              , trans = modTrans
                                              , opinion = modOpinion
274
                                              , predicate = Just modPredicate
Stefan Jaax's avatar
Stefan Jaax committed
275
276
277
278
279
280
281
282
                                              } where
    modTrans (Mod a, Mod b) = let c' = (a + b) `mod` n in (Mod c', ModPassive (c' == c))
    modTrans (Mod a, ModPassive b) = (Mod a, ModPassive (a == c))
    modTrans (ModPassive b, Mod a) = modTrans (Mod a, ModPassive b)
    modTrans (a, b) = (a, b)
    modOpinion (Mod a) = a == c
    modOpinion (ModPassive b) = b

283
284
285
286
    modPredicate = "EXISTS k : " ++
                    (intercalate " + " [ show i ++ " * " ++ toVar (Mod i) | i <- [0..(n-1)] ]) ++
                    " = " ++ show c ++ " + " ++ show n ++ " * k"

Stefan Jaax's avatar
Stefan Jaax committed
287
288
289
290
291
292

createMajorityProtocol :: MajorityProtocol
createMajorityProtocol = PopulationProtocol { states = [A, B, Asmall, Bsmall]
                                            , initial = [A, B]
                                            , trans = majorityTrans
                                            , opinion =  majorityOpinion
293
                                            , predicate = Just (toVar A ++ " > " ++ toVar B)
Stefan Jaax's avatar
Stefan Jaax committed
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
                                            } where 
    majorityTrans (A, B) = (Asmall, Bsmall)
    majorityTrans (B, A) = (Bsmall, Asmall)
    majorityTrans (A, Bsmall) = (A, Asmall)
    majorityTrans (Bsmall, A) = (Asmall, A)
    majorityTrans (Asmall, Bsmall) = (Bsmall, Bsmall)
    majorityTrans (Bsmall, Asmall) = (Bsmall, Bsmall) 
    majorityTrans (B, Asmall) = (B, Bsmall)
    majorityTrans (Asmall, B) = (Bsmall, B)
    majorityTrans x = x

    majorityOpinion A = True
    majorityOpinion B = False
    majorityOpinion Asmall = True
    majorityOpinion Bsmall = False


createThresholdProtocol :: Int -> Int -> Maybe ThresholdProtocol
createThresholdProtocol n c' = if n < 0 || c' < 0 then
                                    Nothing
                               else
                                    Just (PopulationProtocol { states = thresholdStates
                                                             , initial = [Neg i | i <- [1..n]] ++ [Pos i | i <- [0..n]]
                                                             , trans = thresholdTrans
                                                             , opinion = thresholdOpinion
319
                                                             , predicate = Nothing
Stefan Jaax's avatar
Stefan Jaax committed
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
                                                             }) where
    thresholdStates = [Neg i | i <- [1..n]] ++ 
                      [Pos i | i <- [0..n]] ++
                      [BiasPos i | i <- [1..(n-1)]] ++
                      [Passive True, Passive False]

    thresholdTrans (Neg i, Neg j) | (i + j > n) = (Neg n, Neg (i + j - n))
                                  | otherwise = (Neg (i + j), Passive True)

    thresholdTrans (Pos i, Pos j) | (i + j > n && i + j < 2*n) = (Pos n, BiasPos (i + j - n))
                                  | (i + j == 2 * n) = (Pos n, Pos n)
                                  | otherwise = (Pos (i + j), Passive ((i + j) < c'))

    thresholdTrans (BiasPos i, BiasPos j) | (i + j < n) = (BiasPos (i + j), Passive ((i+j) < c'))
                                          | (i + j == n) =  (Pos (i + j), Passive False)
                                          | otherwise = (Pos n, Pos (i+j -n))

    thresholdTrans (Neg i, Pos j) = if i > j then 
                                        (Neg (i - j), Passive True) 
                                    else 
                                        (Pos (j - i), Passive ((j - i) < c'))
    thresholdTrans (Neg i, BiasPos j) = thresholdTrans (Neg i, Pos j)
    thresholdTrans (Pos i, BiasPos j) | (i + j <= n) = (Pos (i + j), Passive ((i+ j) < c'))
                                      | otherwise = (Pos n, BiasPos (i + j - n))
    thresholdTrans (Neg i, (Passive _ )) = (Neg i, Passive True)
    thresholdTrans (Pos i, Passive _) = (Pos i, Passive (i < c'))
    thresholdTrans (BiasPos i, Passive _) = (BiasPos i, Passive False)
    thresholdTrans (Passive a, Passive b) = (Passive a, Passive b)
    thresholdTrans (a, b) = swap $ thresholdTrans (b, a)

    thresholdOpinion (Neg _) = True
    thresholdOpinion (Pos j) = j < c'
    thresholdOpinion (BiasPos j) = False
    thresholdOpinion (Passive b) = b

awkwardShowInt :: Int -> String
awkwardShowInt i = head [str | (b, str) <- [(i > 0, "p" ++ show i),
                                            (i == 0, "0"),
                                            (i < 0, "m" ++ show (abs i))],
                                            b]