Commit ab8cb01d authored by Stefan Jaax's avatar Stefan Jaax

Add polylog protocol

parent c0627874
......@@ -5,6 +5,7 @@ import ProtocolOutput
usageAction :: IO ()
usageAction = do
putStrLn "Usage: "
putStrLn "'./pp2petrinet effThresholdPP c' converts .. to PNet."
putStrLn "'./pp2petrinet majorityPP' converts Majority PP to PNet."
putStrLn "'./pp2petrinet broadCastPP' converts BroadCast PP to PNet."
putStrLn "'./pp2petrinet thresholdPP l c' converts threshold PP to PNet, where l and c are positive integers."
......@@ -32,6 +33,10 @@ newBirdsAction [x] = let pp = createNewBirdsProtocol (read x) in
putStr $ protocolToPetriNet pp ("New 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)
flockOfBirdsAction :: [String] -> IO ()
flockOfBirdsAction [x] = let pp = createFlockOfBirdsProtocol (read x) in
putStr $ protocolToPetriNet pp ("Flock of birds protocol with c = " ++ x)
......@@ -71,6 +76,7 @@ main = do
("oldThresholdPP":as) -> oldThresholdAction as
("moduloPP":as) -> moduloAction as
("flockOfBirdsPP":as) -> flockOfBirdsAction as
("effThresholdPP":as) -> effThresholdAction as
("newBirdsPP":as) -> newBirdsAction as
("verifiableFlockOfBirdsPP":as) -> verifiableFlockOfBirdsAction as
("simplePP":_) -> simpleAction
......
......@@ -8,6 +8,7 @@ module PopulationProtocol ( PopulationProtocol (..)
, createVerifiableFlockOfBirdsProtocol
, createNewBirdsProtocol
, createBroadcastProtocol
, createEfficientThresholdProtocol
, simpleProtocol
, MajorityState(..)
, createMLayerProtocol
......@@ -78,6 +79,53 @@ simpleProtocol = PopulationProtocol { states = [L 9, NL 2, NL 4, L 10, NL 1, NL
simpleTrans (q, r) = (q, r)
data THState = THVal (Int, Int) | Passivo | Eater deriving (Show, Eq, Ord)
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)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment