Add benchmarks

benchmarks/pp2petrinet/PopulationProtocol.hs

+module PopulationProtocol ( PopulationProtocol (..) 
+                          , Population
+                          , createModuloProtocol
+                          , createThresholdProtocol
+                          , createOldThresholdProtocol
+                          , createMajorityProtocol
+                          , createFlockOfBirdsProtocol
+                          , createVerifiableFlockOfBirdsProtocol
+                          , createNewBirdsProtocol
+                          , createAVCProtocol
+                          , createBroadcastProtocol
+                          , simpleProtocol
+                          , MajorityState(..)
+                          , createMLayerProtocol
+                          ) where
+
+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.Maybe (catMaybes, fromMaybe)
+
+data PopulationProtocol qs = PopulationProtocol { states :: [qs]
+                                                , initial :: [qs]
+                                                , trans :: (qs, qs) -> (qs, qs)
+                                                , opinion :: qs -> Bool
+                                                }
+
+
+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 AVCProtocol = PopulationProtocol (AVCState)
+
+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 AVCState = AVCState { sgn :: Int 
+                         , weight :: Int
+                         } deriving (Ord, Eq)
+
+data OldThresholdState = OldThresholdState { leaderBit :: Bool
+                                           , outputBit :: Bool
+                                           , numVal :: Int
+                                           } deriving (Ord, Eq)
+
+instance Show AVCState where 
+  show q = awkwardShowInt (sgn q) ++ "_" ++ show (weight q)
+
+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
+                                    } where
+  simpleTrans (L 9, NL 2) = (L 10, NL 1)
+  simpleTrans (L 9, NL 4) = (L 10, NL 3)
+  simpleTrans (q, r) = (q, r)
+
+
+createMLayerProtocol :: Int -> PopulationProtocol Int
+createMLayerProtocol m = PopulationProtocol { states = [i | i <- [1..(2*m)]]
+                                            , initial = states (createMLayerProtocol m)
+                                            , trans = layerTrans
+                                            , opinion = \x -> True
+                                            } 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)
+
+
+createAVCProtocol :: Int -> Int -> AVCProtocol
+createAVCProtocol m d = PopulationProtocol { states = strongStates ++ intermdiateStates ++ weakStates
+                                           , trans = avcTrans
+                                           , initial = [AVCState (-1) m, AVCState 1 m]
+                                           , opinion = (== 1) . signum'} where 
+  strongStates = [AVCState (signum x) (abs x) | x <- [-m, -m + 2..m], (abs x) /= 1]
+  intermdiateStates = [AVCState d' 1 | d' <- [-d..d], d' /= 0]
+  weakStates = [AVCState (-1) 0, AVCState 1 0]
+  signum' q = signum (sgn q)
+  value q = (signum' q) * (weight q)
+  avcTrans (q1, q2) = if (weight q1 > 0 && weight q2 > 1) || (weight q2 > 0 && weight q1 > 1) then
+                         (down ((value q1 + value q2) `div` 2), up ((value q1 + value q2) `div` 2))
+                      else
+                        (if (weight q1)*(weight q2) == 0 && (weight q1 + weight q2) > 0 then
+                          (if weight q1 > 0 then
+                            (shiftToZero q1, signToZero q1)
+                           else
+                            (shiftToZero q2, signToZero q2))
+                        else
+                          (if (q1 `elem` [AVCState (-d) 1, AVCState d 1] && weight q2 == 1 && signum' q1 /= signum' q2) ||
+                             (q2 `elem` [AVCState (-d) 1, AVCState d 1] && weight q1 == 1 && signum' q1 /= signum' q2) then
+                                (AVCState (-1) 0, AVCState 1 0)
+                           else
+                             (shiftToZero q1, shiftToZero q2)))
+  phi k = case k of
+    (-1) -> AVCState (-1) 1
+    1 -> AVCState 1 1
+    x -> AVCState (signum x) (abs x)
+  down k = let k' = if even k then k - 1 else k in phi k'
+  up k = let k' = if even k then k + 1 else k in phi k'
+  shiftToZero q = case q of
+    AVCState s 1 -> if (abs s) < d then AVCState (s + signum s) 1 else AVCState s 1
+    x -> x
+  signToZero q = AVCState (signum' q) 0
+
+
+createBroadcastProtocol :: PopulationProtocol Bool
+createBroadcastProtocol = PopulationProtocol { states = [True, False]
+                                             , initial = states (createBroadcastProtocol)
+                                             , trans = \(q1, q2) -> (q1 || q2, q1 || q2)
+                                             , opinion = \q -> q}
+
+
+createVerifiableFlockOfBirdsProtocol :: Int -> VerifiableFlockOfBirdsProtocol
+createVerifiableFlockOfBirdsProtocol i = PopulationProtocol { states = [(b, j) | b <- [True, False], j <- [0..i]]
+                                                            , initial = [((i == 1), 1)]
+                                                            , trans = verifiableFlockOfBirdsTrans
+                                                            , opinion = \(b, _) -> b} 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
+                                                  } where
+  flockOfBirdsTrans (q1, q2) =  if q1 + q2 < i then
+                                  (q1 + q2, 0)
+                                else
+                                  (i, i)
+  flockOfBirdsOpinion x = (x == i)
+
+
+createNewBirdsProtocol :: Int -> PopulationProtocol Int
+createNewBirdsProtocol i = PopulationProtocol { states = [0..i]
+                                              , initial = [0, 1]
+                                              , trans = newBirdsTrans
+                                              , opinion = (== i)} where 
+  newBirdsTrans (q, q') | (q == q' && q > 0 && q < i) = (q, q + 1)
+                        | (q == i || q' == i) = (i, i)
+                        | otherwise = (q, q')
+
+
+createOldThresholdProtocol :: Int -> Int -> OldThresholdProtocol
+createOldThresholdProtocol lmax c = PopulationProtocol { states = [OldThresholdState b1 b2 s | b1 <- [True, False]
+                                                                                             , b2 <- [True, False]
+                                                                                             , s  <- [-lmax..lmax]]
+                                                       , initial = [q | q <- states (createOldThresholdProtocol lmax c) , leaderBit q]
+                                                       , trans = oldThresholdTrans
+                                                       , opinion = outputBit
+                                                       } where
+  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   
+
+
+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
+                                              } 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
+
+
+createMajorityProtocol :: MajorityProtocol
+createMajorityProtocol = PopulationProtocol { states = [A, B, Asmall, Bsmall]
+                                            , initial = [A, B]
+                                            , trans = majorityTrans
+                                            , opinion =  majorityOpinion
+                                            } 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
+                                                             }) 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]
+

benchmarks/pp2petrinet/ProtocolToPetrinet.hs

+module ProtocolToPetrinet where
+
+import PopulationProtocol
+import Data.Char (toLower)
+
+transToVar :: (Show qs) => (qs, qs) -> String
+transToVar (q1, q2) = "x_" ++ toVar q1 ++ "_" ++ toVar q2 
+ 
+
+toVar :: (Show a) => a -> String
+toVar = ('_':) . map toLower . filter (\x -> not (x  `elem` " ,()")) . show
+
+
+nonSilentActions :: (Ord qs) => PopulationProtocol qs -> [(qs, qs)]
+nonSilentActions pp = [(q1, q2) | q1 <- states pp
+                                , q2 <- states pp
+                                , q1 <= q2
+                                , (trans pp) (q1, q2) /= (q1, q2)
+				, (trans pp) (q1, q2) /= (q2, q1)]
+
+
+places :: (Show qs) => qs -> qs -> String
+places q1 q2 =  "{ " ++ toVar q1 ++ ", " ++ toVar q2 ++ " }"
+
+
+protocolToPetriNet :: (Show qs, Ord qs) => PopulationProtocol qs -> String -> String
+protocolToPetriNet pp name =  
+    "petri net " ++ show name ++ " {" ++ "\n" ++
+    "    places { " ++ unwords (toVar <$> states pp) ++ "}" ++ "\n" ++
+    "    transitions { " ++ unwords (transToVar <$> nonSilentActions pp) ++ " }" ++ "\n" ++
+    "    arcs {" ++ "\n" ++
+    unlines ["       " ++ places q1 q2 ++ " -> " ++ transToVar (q1, q2) ++ " -> " ++ places q1' q2' | 
+             (q1, q2) <- nonSilentActions pp, let (q1', q2') = (trans pp) (q1, q2)] ++
+    "    }\n" ++
+    "    initial {" ++ unwords (toVar <$> initial pp) ++ "}\n" ++
+    "    yes {" ++ unwords (toVar <$> [q | q <- states pp, (opinion pp) q]) ++ "}\n" ++
+    "    no {" ++ unwords (toVar <$> [q | q <- states pp, not ((opinion pp) q)]) ++ "}\n" ++
+    "}"

benchmarks/pp2petrinet/pp2petrinet.hs

+import System.Environment (getArgs)
+import PopulationProtocol
+import ProtocolToPetrinet
+
+usageAction :: IO ()
+usageAction = do 
+    putStrLn "Usage: "
+    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."
+    putStrLn "'./pp2petrinet moduloPP m c' converts Modulo PP to PNet, where m, c are positive integers."
+    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 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."
+
+
+majorityAction :: IO ()
+majorityAction = putStr $ protocolToPetriNet createMajorityProtocol "Majority Protocol"
+
+broadCastAction :: IO ()
+broadCastAction = putStr $ protocolToPetriNet createBroadcastProtocol "BroadCast Protocol"
+
+simpleAction :: IO ()
+simpleAction = putStr $ protocolToPetriNet simpleProtocol "Simple Protocol"
+
+
+newBirdsAction :: [String] -> IO ()
+newBirdsAction [x] = let pp = createNewBirdsProtocol (read x) in
+     putStr $ protocolToPetriNet  pp ("New 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)
+
+verifiableFlockOfBirdsAction :: [String] -> IO ()
+verifiableFlockOfBirdsAction [x] = let pp = createVerifiableFlockOfBirdsProtocol (read x) in
+     putStr $ protocolToPetriNet  pp ("Verifiable flock of birds protocol with c = " ++ x)
+
+oldThresholdAction :: [String] -> IO ()
+oldThresholdAction [x, y] = let  pp = createOldThresholdProtocol (read x) (read y) in
+    putStr $ protocolToPetriNet  pp ("Old Threshold Protocol with l = " ++ x ++ " and c = " ++ y)
+oldThresholdAction _ = usageAction
+
+
+thresholdAction :: [String] -> IO ()
+thresholdAction [x, y] = let (Just pp) = createThresholdProtocol (read x) (read y) in
+    putStr $ protocolToPetriNet  pp ("Threshold Protocol with l = " ++ x ++ " and c = " ++ y)
+thresholdAction _ = usageAction
+
+
+moduloAction :: [String] -> IO ()
+moduloAction [x, y] = let pp = createModuloProtocol (read x) (read y) in
+    putStr $ protocolToPetriNet  pp ("Modulo Protocol with m = " ++ x ++ " and c = " ++ y)
+moduloAction _ = usageAction
+
+fastMajorityAction :: [String] -> IO ()
+fastMajorityAction [m, d] = let pp = createAVCProtocol (read m) (read d) in
+    putStr $ protocolToPetriNet pp ("Fast majority with m = " ++ m ++ " and d = " ++ d)
+fastMajorityAction _ = usageAction
+
+
+layeredProtocolAction :: [String] -> IO ()
+layeredProtocolAction [m] = let pp = createMLayerProtocol (read m) in
+    putStr $ protocolToPetriNet pp ("Layered Protocol with m = " ++ m ++ " layers.")
+
+main = do
+    args <- getArgs
+    case args of
+        ("majorityPP":_) -> majorityAction
+        ("broadCastPP":_) -> broadCastAction
+        ("thresholdPP":as) -> thresholdAction as
+        ("oldThresholdPP":as) -> oldThresholdAction as
+        ("moduloPP":as) -> moduloAction as
+        ("flockOfBirdsPP":as) -> flockOfBirdsAction as
+        ("newBirdsPP":as) -> newBirdsAction as
+        ("verifiableFlockOfBirdsPP":as) -> verifiableFlockOfBirdsAction as
+        ("simplePP":_) -> simpleAction
+        ("fastMajorityPP":as) -> fastMajorityAction as
+        ("layeredProtocol":as) -> layeredProtocolAction as
+        _ -> usageAction