Skip to content

GitLab

Commit a58acf69 authored by Stefan Jaax's avatar Stefan Jaax
Browse files
Options

Change benchmarks to JSON

parent e3bce867
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 1910 additions and 342 deletions
benchmarks/pp-print/pp-print.cabal
View file @ a58acf69
......@@ -21,6 +21,6 @@ executable pp-print
main-is: Main.hs
other-modules:
-- other-extensions:
build-depends: multiset, base >= 4.8, containers
build-depends: multiset, base >= 4.8, containers, aeson, aeson-pretty, bytestring
hs-source-dirs: src
default-language: Haskell2010
benchmarks/pp-print/src/Main.hs
View file @ a58acf69
import System.Environment (getArgs)
import PopulationProtocol
import ProtocolOutput
import qualified Data.ByteString.Lazy as BS
usageAction :: IO ()
usageAction = do
......@@ -20,57 +21,57 @@ usageAction = do
majorityAction :: IO ()
majorityAction = putStr $ protocolToPetriNet createMajorityProtocol "Majority Protocol"
majorityAction = BS.putStr $ pp2JSON createMajorityProtocol "Majority Protocol"
broadCastAction :: IO ()
broadCastAction = putStr $ protocolToPetriNet createBroadcastProtocol "BroadCast Protocol"
broadCastAction = BS.putStr $ pp2JSON createBroadcastProtocol "BroadCast Protocol"
simpleAction :: IO ()
simpleAction = putStr $ protocolToPetriNet simpleProtocol "Simple Protocol"
simpleAction = BS.putStr $ pp2JSON simpleProtocol "Simple Protocol"
newBirdsAction :: [String] -> IO ()
newBirdsAction [x] = let pp = createNewBirdsProtocol (read x) in
putStr $ protocolToPetriNet pp ("New birds protocol with c = " ++ x)
BS.putStr $ pp2JSON 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)
BS.putStr $ pp2JSON 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)
BS.putStr $ pp2JSON 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)
BS.putStr $ pp2JSON 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)
BS.putStr $ pp2JSON 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)
BS.putStr $ pp2JSON 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)
BS.putStr $ pp2JSON 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)
BS.putStr $ pp2JSON pp ("Modulo Protocol with m = " ++ x ++ " and c = " ++ y)
moduloAction _ = usageAction
layeredProtocolAction :: [String] -> IO ()
layeredProtocolAction [m] = let pp = createMLayerProtocol (read m) in
putStr $ protocolToPetriNet pp ("Layered Protocol with m = " ++ m ++ " layers.")
BS.putStr $ pp2JSON pp ("Layered Protocol with m = " ++ m ++ " layers.")
main = do
args <- getArgs
......
benchmarks/pp-print/src/ProtocolOutput.hs
View file @ a58acf69
{-# LANGUAGE DeriveGeneric #-}
module ProtocolOutput where
import Util
import PopulationProtocol
import qualified PopulationProtocol as P
import Data.Aeson
import Data.Aeson.Encode.Pretty
import qualified Data.ByteString.Lazy as BS
import GHC.Generics (Generic)
nonSilentActions :: (Ord qs) => PopulationProtocol qs -> [(qs, qs)]
nonSilentActions pp = [(q1, q2) | q1 <- states pp
, q2 <- states pp
nonSilentActions :: (Ord qs) => P.PopulationProtocol qs -> [(qs, qs)]
nonSilentActions pp = [(q1, q2) | q1 <- P.states pp
, q2 <- P.states pp
, q1 <= q2
, (trans pp) (q1, q2) /= (q1, q2)
, (trans pp) (q1, q2) /= (q2, q1)]
, (P.trans pp) (q1, q2) /= (q1, q2)
, (P.trans pp) (q1, q2) /= (q2, q1)]
places :: (Show qs) => qs -> qs -> String
places q1 q2 = "{ " ++ toVar q1 ++ ", " ++ toVar q2 ++ " }"
data TransStruct = TransStruct { name :: String
, pre :: [String]
, post :: [String]
} deriving (Eq, Ord, Show, Generic)
data PPStruct = PPStruct { title :: String
, states :: [String]
, transitions :: [TransStruct]
, initialStates :: [String]
, trueStates :: [String]
, predicate :: Maybe String
} deriving (Eq, Ord, Show, Generic)
instance ToJSON TransStruct
instance ToJSON PPStruct
protocolToPetriNet :: (Show qs, Ord qs) => PopulationProtocol qs -> String -> String
protocolToPetriNet pp name =
"population protocol " ++ show name ++ " {" ++ "\n" ++
" states { " ++ 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" ++
" true {" ++ unwords (toVar <$> [q | q <- states pp, (opinion pp) q]) ++ "}\n" ++
" false {" ++ unwords (toVar <$> [q | q <- states pp, not ((opinion pp) q)]) ++ "}\n" ++
(case (predicate pp) of
Nothing -> ""
Just p -> " predicate { " ++ p ++ " }\n"
) ++
"}"
pp2JSON :: (Show qs, Ord qs) => P.PopulationProtocol qs -> String -> BS.ByteString
pp2JSON pp str = encodePretty $
PPStruct { title = str
, states = toVar <$> P.states pp
, transitions = [ TransStruct { name = transToVar (q1, q2)
, pre = toVar <$> [q1, q2]
, post = toVar <$> [q1', q2']
}
| (q1, q2) <- nonSilentActions pp
, let (q1', q2') = (P.trans pp) (q1, q2)
]
, initialStates = toVar <$> P.initial pp
, trueStates = toVar <$> [q | q <- P.states pp, (P.opinion pp) q]
, predicate = P.predicate pp
}
examples/broadcast.pp
View file @ a58acf69
population protocol "Broadcast Protocol" {
states { _true _false }
transitions { x_false_true }
arcs {
{ _false, _true } -> x_false_true -> { _true, _true }
}
initial { _true _false }
true { _true }
false { _false }
predicate { _true >= 1 }
{ "title": "Broadcast Protocol",
"states": ["true", "false"],
"transitions": [{ "name": "true,false->true,true",
"pre": ["true", "false"],
"post": ["true", "true"]
}
],
"initialStates": ["true", "false"],
"trueStates": ["true"],
"predicate": "true >= 1"
}
examples/flockofbirds_v1_c4.pp deleted 100644 → 0
View file @ e3bce867
population protocol "Flock of Birds Protocol (variant 1) with c = 4" {
states { _0 _1 _2 _3 _4 }
transitions { x_0_4 x_1_1 x_1_2 x_1_3 x_1_4 x_2_2 x_2_3 x_2_4 x_3_3 x_3_4 }
arcs {
{ _0, _4 } -> x_0_4 -> { _4, _4 }
{ _1, _1 } -> x_1_1 -> { _2, _0 }
{ _1, _2 } -> x_1_2 -> { _3, _0 }
{ _1, _3 } -> x_1_3 -> { _4, _4 }
{ _1, _4 } -> x_1_4 -> { _4, _4 }
{ _2, _2 } -> x_2_2 -> { _4, _4 }
{ _2, _3 } -> x_2_3 -> { _4, _4 }
{ _2, _4 } -> x_2_4 -> { _4, _4 }
{ _3, _3 } -> x_3_3 -> { _4, _4 }
{ _3, _4 } -> x_3_4 -> { _4, _4 }
}
initial { _0 _1 }
true { _4 }
false { _0 _1 _2 _3 }
predicate { _1 >= 4 }
}
examples/flockofbirds_v2_c4.pp deleted 100644 → 0
View file @ e3bce867
population protocol "Flock of Birds Protocol (variant 2) with c = 4" {
states { _0 _1 _2 _3 _4 }
transitions { x_0_4 x_1_1 x_1_4 x_2_2 x_2_4 x_3_3 x_3_4 }
arcs {
{ _0, _4 } -> x_0_4 -> { _4, _4 }
{ _1, _1 } -> x_1_1 -> { _1, _2 }
{ _1, _4 } -> x_1_4 -> { _4, _4 }
{ _2, _2 } -> x_2_2 -> { _2, _3 }
{ _2, _4 } -> x_2_4 -> { _4, _4 }
{ _3, _3 } -> x_3_3 -> { _3, _4 }
{ _3, _4 } -> x_3_4 -> { _4, _4 }
}
initial { _0 _1 }
true { _4 }
false { _0 _1 _2 _3 }
predicate { _1 >= 4 }
}
examples/majority.pp
View file @ a58acf69
population protocol "Majority Protocol" {
states { good bad neutral mildlybad }
transitions { x_good_bad x_good_mildlybad x_bad_neutral x_neutral_mildlybad }
arcs {
{ good, bad } -> x_good_bad -> { neutral, mildlybad }
{ good, mildlybad } -> x_good_mildlybad -> { good, neutral }
{ bad, neutral } -> x_bad_neutral -> { bad, mildlybad }
{ neutral, mildlybad } -> x_neutral_mildlybad -> { mildlybad, mildlybad }
}
initial { good bad }
true { good neutral }
false { bad mildlybad }
predicate { good > bad }
}
{
"transitions": [
{
"pre": [
"_a",
"_b"
],
"post": [
"_asmall",
"_bsmall"
],
"name": "x__a__b"
},
{
"pre": [
"_a",
"_bsmall"
],
"post": [
"_a",
"_asmall"
],
"name": "x__a__bsmall"
},
{
"pre": [
"_b",
"_asmall"
],
"post": [
"_b",
"_bsmall"
],
"name": "x__b__asmall"
},
{
"pre": [
"_asmall",
"_bsmall"
],
"post": [
"_bsmall",
"_bsmall"
],
"name": "x__asmall__bsmall"
}
],
"states": [
"_a",
"_b",
"_asmall",
"_bsmall"
],
"initialStates": [
"_a",
"_b"
],
"predicate": "_a > _b",
"trueStates": [
"_a",
"_asmall"
],
"title": "Majority Protocol"
}
\ No newline at end of file
examples/remainder_m3_c1.pp
View file @ a58acf69
population protocol "Remainder Protocol with m = 3 and c = 1" {
states { _0 _1 _2 _true _false }
transitions { x_0_0 x_0_1 x_0_2 x_0_true x_1_1 x_1_2 x_1_false x_2_2 x_2_true }
arcs {
{ _0, _0 } -> x_0_0 -> { _0, _false }
{ _0, _1 } -> x_0_1 -> { _1, _true }
{ _0, _2 } -> x_0_2 -> { _2, _false }
{ _0, _true } -> x_0_true -> { _0, _false }
{ _1, _1 } -> x_1_1 -> { _2, _false }
{ _1, _2 } -> x_1_2 -> { _0, _false }
{ _1, _false } -> x_1_false -> { _1, _true }
{ _2, _2 } -> x_2_2 -> { _1, _true }
{ _2, _true } -> x_2_true -> { _2, _false }
}
initial { _0 _1 _2 }
true { _1 _true }
false { _0 _2 _false }
predicate {
EXISTS k : _1 + 2 * _2 = 1 + 3*k
}
}
{
"transitions": [
{
"pre": [
"_mod0",
"_mod0"
],
"post": [
"_mod0",
"_modpassivefalse"
],
"name": "x__mod0__mod0"
},
{
"pre": [
"_mod0",
"_mod1"
],
"post": [
"_mod1",
"_modpassivetrue"
],
"name": "x__mod0__mod1"
},
{
"pre": [
"_mod0",
"_mod2"
],
"post": [
"_mod2",
"_modpassivefalse"
],
"name": "x__mod0__mod2"
},
{
"pre": [
"_mod0",
"_modpassivetrue"
],
"post": [
"_mod0",
"_modpassivefalse"
],
"name": "x__mod0__modpassivetrue"
},
{
"pre": [
"_mod1",
"_mod1"
],
"post": [
"_mod2",
"_modpassivefalse"
],
"name": "x__mod1__mod1"
},
{
"pre": [
"_mod1",
"_mod2"
],
"post": [
"_mod0",
"_modpassivefalse"
],
"name": "x__mod1__mod2"
},
{
"pre": [
"_mod1",
"_modpassivefalse"
],
"post": [
"_mod1",
"_modpassivetrue"
],
"name": "x__mod1__modpassivefalse"
},
{
"pre": [
"_mod2",
"_mod2"
],
"post": [
"_mod1",
"_modpassivetrue"
],
"name": "x__mod2__mod2"
},
{
"pre": [
"_mod2",
"_modpassivetrue"
],
"post": [
"_mod2",
"_modpassivefalse"
],
"name": "x__mod2__modpassivetrue"
}
],
"states": [
"_mod0",
"_mod1",
"_mod2",
"_modpassivetrue",
"_modpassivefalse"
],
"initialStates": [
"_mod0",
"_mod1",
"_mod2"
],
"predicate": "EXISTS k : 0 * _mod0 + 1 * _mod1 + 2 * _mod2 = 1 + 3 * k",
"trueStates": [
"_mod1",
"_modpassivetrue"
],
"title": "Modulo Protocol with m = 3 and c = 1"
}
\ No newline at end of file
examples/threshold_l2_c1.pp
View file @ a58acf69
This diff is collapsed.
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