Add logarithmic protocol (08129a4e) · Commits · i7 / peregrine

benchmarks/pp-print/src/Main.hs

+7 −1

Original line number	Diff line number	Diff line
		@@ -13,6 +13,7 @@ usageAction = do
		putStrLn "'./pp2petrinet oldThresholdPP l c' converts Modulo PP to PNet, where l, c are positive integers."
		putStrLn "'./pp2petrinet flockOfBirdsPP c' converts FlockOfBirds PP to PNet, where c is a positive integer."
		putStrLn "'./pp2petrinet newBirdsPP c' converts NewBirds PP to PNet, where c is a positive integer."
		putStrLn "'./pp2petrinet polyLogFlockOfBirdsPP c' converts Polylog Flock-of-Birds PP to PNet, where c is a positive integer."
		putStrLn "'./pp2petrinet verifiableFlockOfBirdsPP c' converts VerifiableFlockOfBirds PP to PNet, where c is a positive integer."
		putStrLn "'./pp2petrinet fastMajorityPP m d' converts FastMajority PP to PNet, where m, d must be odd and positive integers."
		putStrLn "'./pp2petrinet layeredProtocol m' converts Protocol with m >= 1 termination layers to PNet."
		@@ -33,6 +34,10 @@ newBirdsAction [x] = let pp = createNewBirdsProtocol (read x) in
		putStr $ protocolToPetriNet pp ("New birds protocol with c = " ++ x)


		logFlockOfBirdsAction :: [String] -> IO ()
		logFlockOfBirdsAction [x] = let pp = createLogFlockOfBirdsProtocol (read x) in
		putStr $ protocolToPetriNet pp ("Log Flock of birds protocol with c = " ++ x)

		effThresholdAction :: [String] -> IO ()
		effThresholdAction [x] = let pp = createEfficientThresholdProtocol (read x) in
		putStr $ protocolToPetriNet pp ("Efficient Flock of birds protocol with c = " ++ x)
		@@ -79,6 +84,7 @@ main = do
		("effThresholdPP":as) -> effThresholdAction as
		("newBirdsPP":as) -> newBirdsAction as
		("verifiableFlockOfBirdsPP":as) -> verifiableFlockOfBirdsAction as
		("logFlockOfBirdsPP":as) -> logFlockOfBirdsAction as
		("simplePP":_) -> simpleAction
		("layeredProtocol":as) -> layeredProtocolAction as
		_ -> usageAction

benchmarks/pp-print/src/PopulationProtocol.hs

+46 −1

Original line number	Diff line number	Diff line
		@@ -8,10 +8,12 @@ module PopulationProtocol ( PopulationProtocol (..)
		, createVerifiableFlockOfBirdsProtocol
		, createNewBirdsProtocol
		, createBroadcastProtocol
		, createLogFlockOfBirdsProtocol
		, createEfficientThresholdProtocol
		, simpleProtocol
		, MajorityState(..)
		, createMLayerProtocol
		, createPolyLogFlockOfBirdsProtocol
		) where

		import Util
		@@ -19,8 +21,9 @@ import qualified Data.Set as S
		import qualified Data.MultiSet as MS
		import qualified Data.Map.Strict as M
		import Data.Tuple (swap)
		import Data.List (intercalate)
		import Data.List (intercalate, nub)
		import Data.Maybe (catMaybes, fromMaybe)
		import Data.Bits

		data PopulationProtocol qs = PopulationProtocol { states :: [qs]
		, initial :: [qs]
		@@ -81,6 +84,48 @@ simpleProtocol = PopulationProtocol { states = [L 9, NL 2, NL 4, L 10, NL 1, NL

		data THState = THVal (Int, Int) \| Passivo \| Eater deriving (Show, Eq, Ord)

		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 && 2x < c = (2x, 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)

		polylog :: Int -> Int
		polylog 1 = 0
		polylog n = let n' = 2^((floor . logBase 2 . fromIntegral) n) in