Commit 1683cbb1 authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Add predicate to generated protocols

parent b0578845
...@@ -13,16 +13,19 @@ module PopulationProtocol ( PopulationProtocol (..) ...@@ -13,16 +13,19 @@ module PopulationProtocol ( PopulationProtocol (..)
, createMLayerProtocol , createMLayerProtocol
) where ) where
import Util
import qualified Data.Set as S import qualified Data.Set as S
import qualified Data.MultiSet as MS import qualified Data.MultiSet as MS
import qualified Data.Map.Strict as M import qualified Data.Map.Strict as M
import Data.Tuple (swap) import Data.Tuple (swap)
import Data.List (intercalate)
import Data.Maybe (catMaybes, fromMaybe) import Data.Maybe (catMaybes, fromMaybe)
data PopulationProtocol qs = PopulationProtocol { states :: [qs] data PopulationProtocol qs = PopulationProtocol { states :: [qs]
, initial :: [qs] , initial :: [qs]
, trans :: (qs, qs) -> (qs, qs) , trans :: (qs, qs) -> (qs, qs)
, opinion :: qs -> Bool , opinion :: qs -> Bool
, predicate :: Maybe String
} }
...@@ -68,6 +71,7 @@ simpleProtocol = PopulationProtocol { states = [L 9, NL 2, NL 4, L 10, NL 1, NL ...@@ -68,6 +71,7 @@ simpleProtocol = PopulationProtocol { states = [L 9, NL 2, NL 4, L 10, NL 1, NL
, initial = [L 9] , initial = [L 9]
, trans = simpleTrans , trans = simpleTrans
, opinion = \x -> True , opinion = \x -> True
, predicate = Nothing
} where } where
simpleTrans (L 9, NL 2) = (L 10, NL 1) simpleTrans (L 9, NL 2) = (L 10, NL 1)
simpleTrans (L 9, NL 4) = (L 10, NL 3) simpleTrans (L 9, NL 4) = (L 10, NL 3)
...@@ -79,6 +83,7 @@ createMLayerProtocol m = PopulationProtocol { states = [i | i <- [1..(2*m)]] ...@@ -79,6 +83,7 @@ createMLayerProtocol m = PopulationProtocol { states = [i | i <- [1..(2*m)]]
, initial = states (createMLayerProtocol m) , initial = states (createMLayerProtocol m)
, trans = layerTrans , trans = layerTrans
, opinion = \x -> True , opinion = \x -> True
, predicate = Nothing
} where } where
layerTrans (q1, q2) = let boolToSign b = if b then 1 else -1 layerTrans (q1, q2) = let boolToSign b = if b then 1 else -1
boolToVal b = if b then 1 else 0 in boolToVal b = if b then 1 else 0 in
...@@ -98,14 +103,18 @@ createBroadcastProtocol :: PopulationProtocol Bool ...@@ -98,14 +103,18 @@ createBroadcastProtocol :: PopulationProtocol Bool
createBroadcastProtocol = PopulationProtocol { states = [True, False] createBroadcastProtocol = PopulationProtocol { states = [True, False]
, initial = states (createBroadcastProtocol) , initial = states (createBroadcastProtocol)
, trans = \(q1, q2) -> (q1 || q2, q1 || q2) , trans = \(q1, q2) -> (q1 || q2, q1 || q2)
, opinion = \q -> q} , opinion = \q -> q
, predicate = Just (toVar True ++ " >= 1")
}
createVerifiableFlockOfBirdsProtocol :: Int -> VerifiableFlockOfBirdsProtocol createVerifiableFlockOfBirdsProtocol :: Int -> VerifiableFlockOfBirdsProtocol
createVerifiableFlockOfBirdsProtocol i = PopulationProtocol { states = [(b, j) | b <- [True, False], j <- [0..i]] createVerifiableFlockOfBirdsProtocol i = PopulationProtocol { states = [(b, j) | b <- [True, False], j <- [0..i]]
, initial = [((i == 1), 1)] , initial = [((i == 1), 1)]
, trans = verifiableFlockOfBirdsTrans , trans = verifiableFlockOfBirdsTrans
, opinion = \(b, _) -> b} where , opinion = \(b, _) -> b
, predicate = Nothing
} where
verifiableFlockOfBirdsTrans ((b1, n1), (b2, n2)) = if n1 + n2 < i then verifiableFlockOfBirdsTrans ((b1, n1), (b2, n2)) = if n1 + n2 < i then
((b1, n1 + n2), (b2, 0)) ((b1, n1 + n2), (b2, 0))
else else
...@@ -117,32 +126,40 @@ createFlockOfBirdsProtocol i = PopulationProtocol { states = [0..i] ...@@ -117,32 +126,40 @@ createFlockOfBirdsProtocol i = PopulationProtocol { states = [0..i]
, initial = [0, 1] , initial = [0, 1]
, trans = flockOfBirdsTrans , trans = flockOfBirdsTrans
, opinion = flockOfBirdsOpinion , opinion = flockOfBirdsOpinion
, predicate = Just flockOfBirdsPredicate
} where } where
flockOfBirdsTrans (q1, q2) = if q1 + q2 < i then flockOfBirdsTrans (q1, q2) = if q1 + q2 < i then
(q1 + q2, 0) (q1 + q2, 0)
else else
(i, i) (i, i)
flockOfBirdsOpinion x = (x == i) flockOfBirdsOpinion x = (x == i)
flockOfBirdsPredicate = (toVar 1) ++ " >= " ++ show i
createNewBirdsProtocol :: Int -> PopulationProtocol Int createNewBirdsProtocol :: Int -> PopulationProtocol Int
createNewBirdsProtocol i = PopulationProtocol { states = [0..i] createNewBirdsProtocol i = PopulationProtocol { states = [0..i]
, initial = [0, 1] , initial = [0, 1]
, trans = newBirdsTrans , trans = newBirdsTrans
, opinion = (== i)} where , opinion = (== i)
, predicate = Just newBirdsPredicate
} where
newBirdsTrans (q, q') | (q == q' && q > 0 && q < i) = (q, q + 1) newBirdsTrans (q, q') | (q == q' && q > 0 && q < i) = (q, q + 1)
| (q == i || q' == i) = (i, i) | (q == i || q' == i) = (i, i)
| otherwise = (q, q') | otherwise = (q, q')
newBirdsPredicate = (toVar 1) ++ " >= " ++ show i
createOldThresholdProtocol :: Int -> Int -> OldThresholdProtocol createOldThresholdProtocol :: Int -> Int -> OldThresholdProtocol
createOldThresholdProtocol lmax c = PopulationProtocol { states = [OldThresholdState b1 b2 s | b1 <- [True, False] createOldThresholdProtocol lmax c = PopulationProtocol { states = [OldThresholdState b1 b2 s | b1 <- [True, False]
, b2 <- [True, False] , b2 <- [True, False]
, s <- [-lmax..lmax]] , s <- [-lmax..lmax]]
, initial = [q | q <- states (createOldThresholdProtocol lmax c) , leaderBit q] , initial = oldThresholdInitial
, trans = oldThresholdTrans , trans = oldThresholdTrans
, opinion = outputBit , opinion = outputBit
, predicate = Just oldThresholdPredicate
} where } where
oldThresholdInitial = [q | q <- states (createOldThresholdProtocol lmax c) , leaderBit q]
oldThresholdTrans (q1, q2) = if leaderBit q1 || leaderBit q2 then oldThresholdTrans (q1, q2) = if leaderBit q1 || leaderBit q2 then
(OldThresholdState True (b q1 q2) (l q1 q2), (OldThresholdState True (b q1 q2) (l q1 q2),
OldThresholdState False (b q1 q2) (r q1 q2)) OldThresholdState False (b q1 q2) (r q1 q2))
...@@ -150,7 +167,10 @@ createOldThresholdProtocol lmax c = PopulationProtocol { states = [OldThresholdS ...@@ -150,7 +167,10 @@ createOldThresholdProtocol lmax c = PopulationProtocol { states = [OldThresholdS
(q1, q2) where (q1, q2) where
b q1 q2 = l q1 q2 < c b q1 q2 = l q1 q2 < c
l q1 q2 = max (-lmax) (min lmax (numVal q1 + numVal q2)) l q1 q2 = max (-lmax) (min lmax (numVal q1 + numVal q2))
r q1 q2 = numVal q1 + numVal q2 - l q1 q2 r q1 q2 = numVal q1 + numVal q2 - l q1 q2
oldThresholdPredicate = (intercalate " + " [ show (numVal q) ++ " * " ++ toVar q | q <- oldThresholdInitial ]) ++
" < " ++ (show c)
createModuloProtocol :: Int -> Int -> ModuloProtocol createModuloProtocol :: Int -> Int -> ModuloProtocol
...@@ -158,6 +178,7 @@ createModuloProtocol n c = PopulationProtocol { states = [Mod i | i <- [0..(n-1) ...@@ -158,6 +178,7 @@ createModuloProtocol n c = PopulationProtocol { states = [Mod i | i <- [0..(n-1)
, initial = [Mod i | i <- [0..(n-1)]] , initial = [Mod i | i <- [0..(n-1)]]
, trans = modTrans , trans = modTrans
, opinion = modOpinion , opinion = modOpinion
, predicate = Just modPredicate
} where } where
modTrans (Mod a, Mod b) = let c' = (a + b) `mod` n in (Mod c', ModPassive (c' == c)) 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 (Mod a, ModPassive b) = (Mod a, ModPassive (a == c))
...@@ -166,12 +187,17 @@ createModuloProtocol n c = PopulationProtocol { states = [Mod i | i <- [0..(n-1) ...@@ -166,12 +187,17 @@ createModuloProtocol n c = PopulationProtocol { states = [Mod i | i <- [0..(n-1)
modOpinion (Mod a) = a == c modOpinion (Mod a) = a == c
modOpinion (ModPassive b) = b modOpinion (ModPassive b) = b
modPredicate = "EXISTS k : " ++
(intercalate " + " [ show i ++ " * " ++ toVar (Mod i) | i <- [0..(n-1)] ]) ++
" = " ++ show c ++ " + " ++ show n ++ " * k"
createMajorityProtocol :: MajorityProtocol createMajorityProtocol :: MajorityProtocol
createMajorityProtocol = PopulationProtocol { states = [A, B, Asmall, Bsmall] createMajorityProtocol = PopulationProtocol { states = [A, B, Asmall, Bsmall]
, initial = [A, B] , initial = [A, B]
, trans = majorityTrans , trans = majorityTrans
, opinion = majorityOpinion , opinion = majorityOpinion
, predicate = Just (toVar A ++ " > " ++ toVar B)
} where } where
majorityTrans (A, B) = (Asmall, Bsmall) majorityTrans (A, B) = (Asmall, Bsmall)
majorityTrans (B, A) = (Bsmall, Asmall) majorityTrans (B, A) = (Bsmall, Asmall)
...@@ -197,6 +223,7 @@ createThresholdProtocol n c' = if n < 0 || c' < 0 then ...@@ -197,6 +223,7 @@ createThresholdProtocol n c' = if n < 0 || c' < 0 then
, initial = [Neg i | i <- [1..n]] ++ [Pos i | i <- [0..n]] , initial = [Neg i | i <- [1..n]] ++ [Pos i | i <- [0..n]]
, trans = thresholdTrans , trans = thresholdTrans
, opinion = thresholdOpinion , opinion = thresholdOpinion
, predicate = Nothing
}) where }) where
thresholdStates = [Neg i | i <- [1..n]] ++ thresholdStates = [Neg i | i <- [1..n]] ++
[Pos i | i <- [0..n]] ++ [Pos i | i <- [0..n]] ++
......
module ProtocolOutput where module ProtocolOutput where
import Util
import PopulationProtocol 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 :: (Ord qs) => PopulationProtocol qs -> [(qs, qs)]
nonSilentActions pp = [(q1, q2) | q1 <- states pp nonSilentActions pp = [(q1, q2) | q1 <- states pp
, q2 <- states pp , q2 <- states pp
, q1 <= q2 , q1 <= q2
, (trans pp) (q1, q2) /= (q1, q2) , (trans pp) (q1, q2) /= (q1, q2)
, (trans pp) (q1, q2) /= (q2, q1)] , (trans pp) (q1, q2) /= (q2, q1)]
places :: (Show qs) => qs -> qs -> String places :: (Show qs) => qs -> qs -> String
...@@ -24,15 +16,19 @@ places q1 q2 = "{ " ++ toVar q1 ++ ", " ++ toVar q2 ++ " }" ...@@ -24,15 +16,19 @@ places q1 q2 = "{ " ++ toVar q1 ++ ", " ++ toVar q2 ++ " }"
protocolToPetriNet :: (Show qs, Ord qs) => PopulationProtocol qs -> String -> String protocolToPetriNet :: (Show qs, Ord qs) => PopulationProtocol qs -> String -> String
protocolToPetriNet pp name = protocolToPetriNet pp name =
"population protocol " ++ show name ++ " {" ++ "\n" ++ "population protocol " ++ show name ++ " {" ++ "\n" ++
" states { " ++ unwords (toVar <$> states pp) ++ "}" ++ "\n" ++ " states { " ++ unwords (toVar <$> states pp) ++ "}" ++ "\n" ++
" transitions { " ++ unwords (transToVar <$> nonSilentActions pp) ++ " }" ++ "\n" ++ " transitions { " ++ unwords (transToVar <$> nonSilentActions pp) ++ " }" ++ "\n" ++
" arcs {" ++ "\n" ++ " arcs {" ++ "\n" ++
unlines [" " ++ places q1 q2 ++ " -> " ++ transToVar (q1, q2) ++ " -> " ++ places q1' q2' | unlines [" " ++ places q1 q2 ++ " -> " ++ transToVar (q1, q2) ++ " -> " ++ places q1' q2' |
(q1, q2) <- nonSilentActions pp, let (q1', q2') = (trans pp) (q1, q2)] ++ (q1, q2) <- nonSilentActions pp, let (q1', q2') = (trans pp) (q1, q2)] ++
" }\n" ++ " }\n" ++
" initial {" ++ unwords (toVar <$> initial pp) ++ "}\n" ++ " initial {" ++ unwords (toVar <$> initial pp) ++ "}\n" ++
" true {" ++ unwords (toVar <$> [q | q <- states pp, (opinion pp) q]) ++ "}\n" ++ " true {" ++ unwords (toVar <$> [q | q <- states pp, (opinion pp) q]) ++ "}\n" ++
" false {" ++ unwords (toVar <$> [q | q <- states pp, not ((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"
) ++
"}" "}"
module Util (transToVar, toVar) where
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
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