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

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

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


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)

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
74
                                    , predicate = Nothing
Stefan Jaax's avatar
Stefan Jaax committed
75
76
77
78
79
80
                                    } 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
81
82
data THState = THVal (Int, Int) | Passivo | Eater deriving (Show, Eq, Ord)

Stefan Jaax's avatar
Stefan Jaax committed
83
84
85
floorLog :: Int -> Int
floorLog = floor . logBase 2 . fromIntegral

86
87
88
89
genericFloorLog :: Integer -> Int
genericFloorLog = floor . logBase 2 . fromIntegral

g :: Int -> Int
Stefan Jaax's avatar
Stefan Jaax committed
90
91
92
93
94
95
96
97
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)

98
createLogFlockOfBirdsProtocol :: Integer -> PopulationProtocol Integer
Stefan Jaax's avatar
Stefan Jaax committed
99
100
101
102
103
createLogFlockOfBirdsProtocol c = PopulationProtocol{ states = nub logQ
                                                    , initial = [1, 0]
                                                    , opinion = (== c)
                                                    , trans = logTrans
                                                    , predicate = Just $ toVar 1 ++ " >= " ++ show c} where
104
  logQ = [2^i | i <- [0..(genericFloorLog c-1)]] ++ [c .&. (shift (complement 0) i) | i <- [0..(genericFloorLog c + 1)]]
Stefan Jaax's avatar
Stefan Jaax committed
105
106
  logTrans (x, y) | x + y >= c = (c, c)
                  | x == y && 2*x < c = (2*x, 0)
107
                  | y >= fromIntegral (genericFloorLog c) && y + x `elem` logQ = (x+y, 0)
Stefan Jaax's avatar
Stefan Jaax committed
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
                  | 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
128
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
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
173
174
175
176
177
createMLayerProtocol :: Int -> PopulationProtocol Int
createMLayerProtocol m = PopulationProtocol { states = [i | i <- [1..(2*m)]]
                                            , initial = states (createMLayerProtocol m)
                                            , trans = layerTrans
                                            , opinion = \x -> True
178
                                            , predicate = Nothing
Stefan Jaax's avatar
Stefan Jaax committed
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
                                            } 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)
198
199
200
                                             , opinion = \q -> q
                                             , predicate = Just (toVar True ++ " >= 1")
                                             }
Stefan Jaax's avatar
Stefan Jaax committed
201
202
203
204
205
206


createVerifiableFlockOfBirdsProtocol :: Int -> VerifiableFlockOfBirdsProtocol
createVerifiableFlockOfBirdsProtocol i = PopulationProtocol { states = [(b, j) | b <- [True, False], j <- [0..i]]
                                                            , initial = [((i == 1), 1)]
                                                            , trans = verifiableFlockOfBirdsTrans
207
208
209
                                                            , opinion = \(b, _) -> b
                                                            , predicate = Nothing
                                                            } where
Stefan Jaax's avatar
Stefan Jaax committed
210
211
212
213
214
215
216
217
218
219
220
  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
221
                                                  , predicate = Just flockOfBirdsPredicate
Stefan Jaax's avatar
Stefan Jaax committed
222
223
224
225
226
227
                                                  } where
  flockOfBirdsTrans (q1, q2) =  if q1 + q2 < i then
                                  (q1 + q2, 0)
                                else
                                  (i, i)
  flockOfBirdsOpinion x = (x == i)
228
  flockOfBirdsPredicate = (toVar 1) ++ " >= " ++ show i
Stefan Jaax's avatar
Stefan Jaax committed
229
230
231
232
233
234


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


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

Stefan Jaax's avatar
Stefan Jaax committed
255
256
257
258
259
260
261
  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))
262
263
264
265
  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
266
267
268
269
270
271
272


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
273
                                              , predicate = Just modPredicate
Stefan Jaax's avatar
Stefan Jaax committed
274
275
276
277
278
279
280
281
                                              } 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

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

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

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