module PopulationProtocol ( PopulationProtocol (..) , createModuloProtocol , createThresholdProtocol , createOldThresholdProtocol , createMajorityProtocol , createFlockOfBirdsProtocol , createVerifiableFlockOfBirdsProtocol , createNewBirdsProtocol , createBroadcastProtocol , createLogFlockOfBirdsProtocol , createEfficientThresholdProtocol , simpleProtocol , MajorityState(..) , createMLayerProtocol , createPolyLogFlockOfBirdsProtocol ) where import Util import qualified Data.Set as S import qualified Data.Map.Strict as M import Data.Tuple (swap) import Data.List (intercalate, nub) import Data.Maybe (catMaybes, fromMaybe) import Data.Bits data PopulationProtocol qs = PopulationProtocol { states :: [qs] , initial :: [qs] , trans :: (qs, qs) -> (qs, qs) , opinion :: qs -> Bool , predicate :: Maybe String } 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 , predicate = Nothing } where simpleTrans (L 9, NL 2) = (L 10, NL 1) simpleTrans (L 9, NL 4) = (L 10, NL 3) simpleTrans (q, r) = (q, r) data THState = THVal (Int, Int) | Passivo | Eater deriving (Show, Eq, Ord) floorLog :: Int -> Int floorLog = floor . logBase 2 . fromIntegral genericFloorLog :: Integer -> Int genericFloorLog = 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 :: Integer -> PopulationProtocol Integer 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..(genericFloorLog c-1)]] ++ [c .&. (shift (complement 0) i) | i <- [0..(genericFloorLog c + 1)]] logTrans (x, y) | x + y >= c = (c, c) | x == y && 2*x < c = (2*x, 0) | y >= fromIntegral (genericFloorLog 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) 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) createMLayerProtocol :: Int -> PopulationProtocol Int createMLayerProtocol m = PopulationProtocol { states = [i | i <- [1..(2*m)]] , initial = states (createMLayerProtocol m) , trans = layerTrans , opinion = \x -> True , predicate = Nothing } 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) , opinion = \q -> q , predicate = Just (toVar True ++ " >= 1") } createVerifiableFlockOfBirdsProtocol :: Int -> VerifiableFlockOfBirdsProtocol createVerifiableFlockOfBirdsProtocol i = PopulationProtocol { states = [(b, j) | b <- [True, False], j <- [0..i]] , initial = [((i == 1), 1)] , trans = verifiableFlockOfBirdsTrans , opinion = \(b, _) -> b , predicate = Nothing } where 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 , predicate = Just flockOfBirdsPredicate } where flockOfBirdsTrans (q1, q2) = if q1 + q2 < i then (q1 + q2, 0) else (i, i) flockOfBirdsOpinion x = (x == i) flockOfBirdsPredicate = (toVar 1) ++ " >= " ++ show i createNewBirdsProtocol :: Int -> PopulationProtocol Int createNewBirdsProtocol i = PopulationProtocol { states = [0..i] , initial = [0, 1] , trans = newBirdsTrans , opinion = (== i) , predicate = Just newBirdsPredicate } where newBirdsTrans (q, q') | (q == q' && q > 0 && q < i) = (q, q + 1) | (q == i || q' == i) = (i, i) | otherwise = (q, q') newBirdsPredicate = (toVar 1) ++ " >= " ++ show i createOldThresholdProtocol :: Int -> Int -> OldThresholdProtocol createOldThresholdProtocol lmax c = PopulationProtocol { states = [OldThresholdState b1 b2 s | b1 <- [True, False] , b2 <- [True, False] , s <- [-lmax..lmax]] , initial = oldThresholdInitial , trans = oldThresholdTrans , opinion = outputBit , predicate = Just oldThresholdPredicate } where oldThresholdInitial = [q | q <- states (createOldThresholdProtocol lmax c) , leaderBit q] 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)) r q1 q2 = numVal q1 + numVal q2 - l q1 q2 oldThresholdPredicate = (intercalate " + " [ show (numVal q) ++ " * " ++ toVar q | q <- oldThresholdInitial ]) ++ " < " ++ (show c) 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 , predicate = Just modPredicate } 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 modPredicate = "( " ++ (intercalate " + " [ show i ++ " * " ++ toVar (Mod i) | i <- [0..(n-1)] ]) ++ " ) % " ++ show n ++ " = " ++ show c createMajorityProtocol :: MajorityProtocol createMajorityProtocol = PopulationProtocol { states = [A, B, Asmall, Bsmall] , initial = [A, B] , trans = majorityTrans , opinion = majorityOpinion , predicate = Just (toVar A ++ " > " ++ toVar B) } 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 , predicate = Nothing }) 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]