Skip to content

peregrine
peregrine
Commit c61e5ef7 authored by Stefan Jaax's avatar Stefan Jaax
Browse files
Options

Merge branch 'json' into 'master' 

Json

See merge request i7/peregrine!1
parents cb83555d c1c7e6b2
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 1999 additions and 466 deletions
README.md
View file @ c61e5ef7
......@@ -16,47 +16,39 @@ and the build system [cabal >= 1.22](https://www.haskell.org/cabal/).
Input
------
Peregrine takes a single population protocol as input.
The following example shows how a protocol is encoded:
Peregrine takes a single population protocol as JSON-encoded input.
The following example shows the input format:
```
population protocol "Majority Protocol" {
states { a b a_small b_small}
transitions { t1 t2 t3 t4 }
arcs { { a, b } -> t1 -> { a_small, b_small }
{ b, a_small } -> t2 -> { b, b_small }
{ a, b_small } -> t3 -> { a, a_small }
{ a_small, b_small } -> t4 -> { a_small, a_small }
}
initial { a b }
true { a a_small }
false { b b_small }
{
"title": "Majority Protocol",
"states": ["A", "a", "B", "b"],
"transitions": [
{ "name": "t1",
"pre": ["A", "B"],
"post": ["a", "b"]
},
{ "name": "t2",
"pre": ["B", "a"],
"post": ["B", "b"]
},
{ "name": "t3",
"pre": ["A", "b"],
"post": ["A", "a"]
},
{ "name": "t4",
"pre": ["a", "b"],
"post": ["a", "a"]
}
],
initialStates: ["A", "B"],
trueStates: ["A", "a"],
predicate: "A >= B",
description: "This protocol computes whether there are more B-states than A-states"
}
```
* After the keyword *population protocol* the name of the protocol is given in
quotes.
* Finite sets are specified in braces
through space- or comma-separated lists of names.
Names consist of alphanumerical characters or underscores.
* The set of states is given after the identifier *states*.
* In order to make transitions identifiable,
each transition must be given a name after the keyword *transitions*.
* Transitions are defined after the keyword *arcs*; there must be one definition
for each transition name.
* The set following the keyword *initial* specifies states that can
belong to an initial population.
* The sets following the keywords *true* and *false* identify the states
that map to true and false, respectively.
Usage
-------
......
benchmarks/pp-print/pp-print.cabal
View file @ c61e5ef7
......@@ -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 @ c61e5ef7
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 @ c61e5ef7
{-# 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 @ c61e5ef7
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 @ cb83555d
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 @ cb83555d
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 @ c61e5ef7
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 @ c61e5ef7
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 @ c61e5ef7
This diff is collapsed.
peregrine.cabal
View file @ c61e5ef7
......@@ -22,8 +22,8 @@ executable peregrine
main-is: Main.hs
other-modules:
-- other-extensions:
build-depends: base >=4 && <5, sbv, parsec, containers, transformers,
bytestring, mtl, stm, async, parallel-io
build-depends: base >=4 && <5, sbv, parsec >= 3.1, containers, transformers,
bytestring, mtl, stm, async, parallel-io, text, aeson
hs-source-dirs: src
default-language: Haskell2010
ghc-options: -fsimpl-tick-factor=1000 -threaded -rtsopts -with-rtsopts=-N
src/Parser.hs
View file @ c61e5ef7
......@@ -3,6 +3,8 @@ module Parser
where
import Text.Parsec
import qualified Data.Text as T
import qualified Data.Text.IO as TIO
type Parser a = Parsec String () a
......@@ -14,7 +16,7 @@ parseString p str =
parseFile :: Parser a -> String -> IO a
parseFile p file = do
contents <- readFile file
case parse p file contents of
contents <- T.unpack <$> TIO.readFile file
case parse p file contents of
Left e -> print e >> fail "parse error"
Right r -> return r
src/Parser/PP.hs
View file @ c61e5ef7
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
module Parser.PP
(parseContent)
where
import Data.Aeson
import Data.Aeson.TH (deriveJSON, defaultOptions)
import Control.Applicative ((<*),(*>),(<$>))
import Data.Functor.Identity
import Text.Parsec
import qualified Data.Set as S
import qualified Data.ByteString.Lazy.Char8 as BS
import qualified Data.Text as T
import Text.Parsec.Expr
import Text.Parsec.Language (LanguageDef, emptyDef)
import qualified Text.Parsec.Token as Token
import Parser
import PopulationProtocol (PopulationProtocol,makePopulationProtocolFromStrings,State(..),Transition(..))
import Property
......@@ -25,7 +33,7 @@ languageDef =
Token.reservedOpNames = ["->", "<", "<=", "=", "!=", ">=", ">",
"+", "-", "*", "&&", "||", "!", ":"]
}
lexer :: Token.TokenParser ()
lexer = Token.makeTokenParser languageDef
......@@ -68,78 +76,6 @@ ident = (identifier <|> stringLiteral) <?> "identifier"
identList :: Parser [String]
identList = singleOrList ident
states :: Parser [String]
states = reserved "states" *> identList
transitions :: Parser [String]
transitions = reserved "transitions" *> identList
initial :: Parser [String]
initial = reserved "initial" *> identList
trueStates :: Parser [String]
trueStates = reserved "true" *> identList
falseStates :: Parser [String]
falseStates = reserved "false" *> identList
arc :: Parser [(String,String,Integer)]
arc = do
lhs <- identList
rhsList <- many1 (do
reservedOp "->"
w <- numberOption
ids <- identList
return (ids,w)
)
return $ fst $ foldl makeArc ([],lhs) rhsList
where
makeArc (as,lhs) (rhs,w) = ([(l,r,w) | l <- lhs, r <- rhs] ++ as, rhs)
arcs :: Parser [(String,String,Integer)]
arcs = do
reserved "arcs"
as <- singleOrList arc
return $ concat as
data Statement = States [String]
| Transitions [String]
| Initial [String]
| TrueStatement [String]
| FalseStatement [String]
| PredicateStatement (QuantFormula String)
| Arcs [(String,String,Integer)]
statement :: Parser Statement
statement = States <$> states <|>
Transitions <$> transitions <|>
Arcs <$> arcs <|>
Initial <$> initial <|>
TrueStatement <$> trueStates <|>
FalseStatement <$> falseStates <|>
PredicateStatement <$> predicate
populationProtocol :: Parser PopulationProtocol
populationProtocol = do
reserved "population"
reserved "protocol"
name <- option "" ident
statements <- braces (many statement)
let (qs,ts,qinitial,qtrue,qfalse,ps,as) = foldl splitStatement ([],[],[],[],[],Nothing,[]) statements
let predicate = case ps of
Nothing -> ExQuantFormula [] FTrue
Just p -> p
return $ makePopulationProtocolFromStrings name qs ts qinitial qtrue qfalse predicate as
where
splitStatement (qs,ts,qinitial,qtrue,qfalse,ps,as) stmnt = case stmnt of
States q -> (q ++ qs,ts,qinitial,qtrue,qfalse,ps,as)
Transitions t -> (qs,t ++ ts,qinitial,qtrue,qfalse,ps,as)
Initial q -> (qs,ts,q ++ qinitial,qtrue,qfalse,ps,as)
TrueStatement q -> (qs,ts,qinitial,q ++ qtrue,qfalse,ps,as)
FalseStatement q -> (qs,ts,qinitial,qtrue,q ++ qfalse,ps,as)
PredicateStatement p -> (qs,ts,qinitial,qtrue,qfalse,Just p,as)
Arcs a -> (qs,ts,qinitial,qtrue,qfalse,ps,a ++ as)
binary :: String -> (a -> a -> a) -> Assoc -> Operator String () Identity a
binary name fun = Infix ( reservedOp name *> return fun )
prefix :: String -> (a -> a) -> Operator String () Identity a
......@@ -205,16 +141,51 @@ quantFormula =
<|>
(ExQuantFormula [] <$> formula)
predicate :: Parser (QuantFormula String)
predicate = do
reserved "predicate"
form <- braces quantFormula
return form
instance FromJSON (QuantFormula String) where
parseJSON (String v) = do
let formula = parse quantFormula "" (T.unpack v)
case formula of
Left e -> fail "Predicate formula not well-formed."
Right r -> return r
parseJSON _ = fail "Expect string for predicate."
instance ToJSON (QuantFormula String) where
toJSON x = String ""
data RecordTransition = RecordTransition {
name :: String,
pre :: [String],
post :: [String]
} deriving (Show)
data RecordPP = RecordPP {
title :: String,
states :: [String],
transitions :: [RecordTransition],
initialStates :: [String],
trueStates :: [String],
predicate :: Maybe (QuantFormula String),
description :: Maybe String
} deriving (Show)
$(deriveJSON defaultOptions ''RecordTransition)
$(deriveJSON defaultOptions ''RecordPP)
recordPP2PopulationProtocol :: RecordPP -> PopulationProtocol
recordPP2PopulationProtocol r =
makePopulationProtocolFromStrings (title r) (states r) (map name (transitions r)) (initialStates r) (trueStates r) falseStates p arcs where