module SMCDEL.Examples.GossipKw where
import SMCDEL.Language
import SMCDEL.Symbolic.S5 (boolBddOf)
import SMCDEL.Symbolic.K
import Control.Arrow ((&&&))
import Data.HasCacBDD hiding (Top)
import Data.Map.Strict (Map,fromList,empty)
import Data.List ((\\),sort)
n :: Int
n :: Int
n = Int
4
gossipInit :: BelScene
gossipInit :: BelScene
gossipInit = ([Prp] -> Bdd -> Map Agent RelBDD -> BelStruct
BlS [Prp]
vocab Bdd
law Map Agent RelBDD
obs, [Prp]
actual) where
vocab :: [Prp]
vocab = (Int -> Prp) -> [Int] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Prp
P [Int
1..Int
n]
law :: Bdd
law = Form -> Bdd
boolBddOf Form
Top
obs :: Map Agent RelBDD
obs = [(Agent, RelBDD)] -> Map Agent RelBDD
forall k a. Ord k => [(k, a)] -> Map k a
fromList [ (Int -> Agent
forall a. Show a => a -> Agent
show Int
i, [Prp] -> RelBDD
allsamebdd [Int -> Prp
P Int
i]) | Int
i <- [Int
1..Int
n] ]
actual :: [Prp]
actual = [Prp]
vocab
willExchangeT :: (Int,Int) -> Int -> Form
willExchangeT :: (Int, Int) -> Int -> Form
willExchangeT (Int
a,Int
b) Int
k | Int
k Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int
a,Int
b] = Prp -> Form
PrpF (Int -> Prp
P Int
k)
| Bool
otherwise = [Form] -> Form
Disj [ Agent -> Form -> Form
K (Int -> Agent
forall a. Show a => a -> Agent
show Int
i) (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Prp -> Form
PrpF (Int -> Prp
P Int
k) | Int
i <- [Int
a,Int
b] ]
inCall,inSecT :: Int -> Prp
inCall :: Int -> Prp
inCall Int
k = Int -> Prp
P (Int
100Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
k)
inSecT :: Int -> Prp
inSecT Int
k = Int -> Prp
P (Int
200Int -> Int -> Int
forall a. Num a => a -> a -> a
+(Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
*Int
2))
call :: (Int,Int) -> [Int] -> Event
call :: (Int, Int) -> [Int] -> Event
call (Int
a,Int
b) [Int]
secSetT = (Transformer
callTrf,[Prp]
actualSet) where
actualSet :: [Prp]
actualSet = [Int -> Prp
inCall Int
a, Int -> Prp
inCall Int
b] [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ (Int -> Prp) -> [Int] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Prp
inSecT [Int]
secSetT
callTrf :: Transformer
callTrf :: Transformer
callTrf = [Prp] -> Form -> Map Prp Bdd -> Map Agent RelBDD -> Transformer
Trf [Prp]
vocplus Form
lawplus Map Prp Bdd
forall k a. Map k a
empty Map Agent RelBDD
obsplus where
vocplus :: [Prp]
vocplus = [Prp] -> [Prp]
forall a. Ord a => [a] -> [a]
sort ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ (Int -> Prp) -> [Int] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Prp
inCall [Int
1..Int
n] [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ (Int -> Prp) -> [Int] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Prp
inSecT [Int
1..Int
n]
lawplus :: Form
lawplus = Form -> Form
simplify (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Disj [ [Form] -> Form
Conj [ Int -> Int -> Form
thisCallHappens Int
i Int
j, Int -> Int -> Form
theseSecretsAreExchanged Int
i Int
j ] | Int
i <- [Int
1..Int
n], Int
j <- [Int
1..Int
n], Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
j ] where
thisCallHappens :: Int -> Int -> Form
thisCallHappens Int
i Int
j = [Form] -> Form
Conj ([Form] -> Form) -> [Form] -> Form
forall a b. (a -> b) -> a -> b
$ (Int -> Form) -> [Int] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map (Prp -> Form
PrpF (Prp -> Form) -> (Int -> Prp) -> Int -> Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Prp
inCall) [Int
i,Int
j] [Form] -> [Form] -> [Form]
forall a. [a] -> [a] -> [a]
++ (Int -> Form) -> [Int] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map (Form -> Form
Neg (Form -> Form) -> (Int -> Form) -> Int -> Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prp -> Form
PrpF (Prp -> Form) -> (Int -> Prp) -> Int -> Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Prp
inCall) ([Int
1..Int
n] [Int] -> [Int] -> [Int]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Int
i,Int
j])
theseSecretsAreExchanged :: Int -> Int -> Form
theseSecretsAreExchanged Int
i Int
j = Form -> Form
simplify (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Conj
[ Prp -> Form
PrpF (Int -> Prp
inSecT Int
k) Form -> Form -> Form
`Equi` (Int, Int) -> Int -> Form
willExchangeT (Int
i,Int
j) Int
k | Int
k <- [Int
1..Int
n] ]
obsplus :: Map Agent RelBDD
obsplus :: Map Agent RelBDD
obsplus = [(Agent, RelBDD)] -> Map Agent RelBDD
forall k a. Ord k => [(k, a)] -> Map k a
fromList ([(Agent, RelBDD)] -> Map Agent RelBDD)
-> [(Agent, RelBDD)] -> Map Agent RelBDD
forall a b. (a -> b) -> a -> b
$ (Int -> (Agent, RelBDD)) -> [Int] -> [(Agent, RelBDD)]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Agent
forall a. Show a => a -> Agent
show (Int -> Agent) -> (Int -> RelBDD) -> Int -> (Agent, RelBDD)
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& Int -> RelBDD
obsfor) [Int
1..Int
n] where
obsfor :: Int -> RelBDD
obsfor Int
i = Bdd -> Bdd -> Bdd
con (Bdd -> Bdd -> Bdd) -> RelBDD -> Tagged Dubbel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Prp] -> RelBDD
allsamebdd [ Int -> Prp
inCall Int
i ]
Tagged Dubbel (Bdd -> Bdd) -> RelBDD -> RelBDD
forall a b.
Tagged Dubbel (a -> b) -> Tagged Dubbel a -> Tagged Dubbel b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Bdd -> Bdd -> Bdd
imp (Bdd -> Bdd -> Bdd) -> RelBDD -> Tagged Dubbel (Bdd -> Bdd)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Bdd -> RelBDD
mvBdd (Bdd -> RelBDD) -> (Prp -> Bdd) -> Prp -> RelBDD
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Form -> Bdd
boolBddOf (Form -> Bdd) -> (Prp -> Form) -> Prp -> Bdd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prp -> Form
PrpF (Prp -> RelBDD) -> Prp -> RelBDD
forall a b. (a -> b) -> a -> b
$ Int -> Prp
inCall Int
i)
Tagged Dubbel (Bdd -> Bdd) -> RelBDD -> RelBDD
forall a b.
Tagged Dubbel (a -> b) -> Tagged Dubbel a -> Tagged Dubbel b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Prp] -> RelBDD
allsamebdd ([Prp] -> [Prp]
forall a. Ord a => [a] -> [a]
sort ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ (Int -> Prp) -> [Int] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Prp
inCall [Int
1..Int
n] [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ (Int -> Prp) -> [Int] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Prp
inSecT [Int
1..Int
n]))
toBeExchangedT :: BelScene -> (Int,Int) -> [Int]
toBeExchangedT :: BelScene -> (Int, Int) -> [Int]
toBeExchangedT BelScene
scn (Int
a,Int
b) = (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (BelScene -> Form -> Bool
evalViaBdd BelScene
scn (Form -> Bool) -> (Int -> Form) -> Int -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, Int) -> Int -> Form
willExchangeT (Int
a,Int
b)) [Int
1..Int
n]
doCall :: BelScene -> (Int,Int) -> BelScene
doCall :: BelScene -> (Int, Int) -> BelScene
doCall BelScene
start (Int
a,Int
b) = BelScene -> BelScene
cleanupObsLaw (BelScene -> BelScene) -> BelScene -> BelScene
forall a b. (a -> b) -> a -> b
$ BelScene
start BelScene -> Event -> BelScene
forall a b. Update a b => a -> b -> a
`update` (Int, Int) -> [Int] -> Event
call (Int
a,Int
b) (BelScene -> (Int, Int) -> [Int]
toBeExchangedT BelScene
start (Int
a,Int
b))
doCalls :: BelScene -> [(Int,Int)] -> BelScene
doCalls :: BelScene -> [(Int, Int)] -> BelScene
doCalls = (BelScene -> (Int, Int) -> BelScene)
-> BelScene -> [(Int, Int)] -> BelScene
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl BelScene -> (Int, Int) -> BelScene
doCall
expert :: Int -> Form
expert :: Int -> Form
expert Int
k = [Form] -> Form
Conj [ Agent -> Form -> Form
K (Int -> Agent
forall a. Show a => a -> Agent
show Int
k) (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Prp -> Form
PrpF (Int -> Prp
P Int
i) | Int
i <- [Int
1..Int
n] ]
allExperts :: Form
allExperts :: Form
allExperts = [Form] -> Form
Conj ([Form] -> Form) -> [Form] -> Form
forall a b. (a -> b) -> a -> b
$ (Int -> Form) -> [Int] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Form
expert [Int
1..Int
n]
whoKnowsWhat :: BelScene -> [(Int,[Int])]
whoKnowsWhat :: BelScene -> [(Int, [Int])]
whoKnowsWhat BelScene
scn = [ (Int
k, (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> Int -> Bool
forall {a}. Show a => a -> Int -> Bool
knownBy Int
k) [Int
1..Int
n]) | Int
k <- [Int
1..Int
n] ] where
knownBy :: a -> Int -> Bool
knownBy a
k Int
i = BelScene -> Form -> Bool
evalViaBdd BelScene
scn (Agent -> Form -> Form
K (a -> Agent
forall a. Show a => a -> Agent
show a
k) (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Prp -> Form
PrpF (Int -> Prp
P Int
i))
whoKnowsMeta :: BelScene -> [(Int,[(Int,String)])]
whoKnowsMeta :: BelScene -> [(Int, [(Int, Agent)])]
whoKnowsMeta BelScene
scn = [ (Int
k, (Int -> (Int, Agent)) -> [Int] -> [(Int, Agent)]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Int -> (Int, Agent)
forall {a} {a}. (Show a, Show a) => a -> a -> (a, Agent)
meta Int
k) [Int
1..Int
n] ) | Int
k <- [Int
1..Int
n] ] where
meta :: a -> a -> (a, Agent)
meta a
x a
y = (a
y, (Int -> Char) -> [Int] -> Agent
forall a b. (a -> b) -> [a] -> [b]
map (a -> a -> Int -> Char
forall {a} {a}. (Show a, Show a) => a -> a -> Int -> Char
knowsAbout a
x a
y) [Int
1..Int
n])
knowsAbout :: a -> a -> Int -> Char
knowsAbout a
x a
y Int
i
| BelScene -> Form -> Bool
evalViaBdd BelScene
scn (Agent -> Form -> Form
K (a -> Agent
forall a. Show a => a -> Agent
show a
x) (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Prp -> Form
PrpF (Int -> Prp
P Int
i) Form -> Form -> Form
`Impl` Agent -> Form -> Form
K (a -> Agent
forall a. Show a => a -> Agent
show a
y) (Prp -> Form
PrpF (Int -> Prp
P Int
i))) = Char
'Y'
| BelScene -> Form -> Bool
evalViaBdd BelScene
scn (Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Agent -> Form -> Form
K (a -> Agent
forall a. Show a => a -> Agent
show a
x) (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Agent -> Form -> Form
K (a -> Agent
forall a. Show a => a -> Agent
show a
y) (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Prp -> Form
PrpF (Int -> Prp
P Int
i)) = Char
'?'
| BelScene -> Form -> Bool
evalViaBdd BelScene
scn (Agent -> Form -> Form
K (a -> Agent
forall a. Show a => a -> Agent
show a
x) (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Agent -> Form -> Form
K (a -> Agent
forall a. Show a => a -> Agent
show a
y) (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Prp -> Form
PrpF (Int -> Prp
P Int
i)) = Char
'_'
| Bool
otherwise = Char
'E'
after :: [(Int,Int)] -> BelScene
after :: [(Int, Int)] -> BelScene
after = BelScene -> [(Int, Int)] -> BelScene
doCalls BelScene
gossipInit
succeeds :: [(Int,Int)] -> Bool
succeeds :: [(Int, Int)] -> Bool
succeeds [(Int, Int)]
sequ = BelScene -> Form -> Bool
evalViaBdd ([(Int, Int)] -> BelScene
after [(Int, Int)]
sequ) Form
allExperts
allSequs :: Int -> [ [(Int,Int)] ]
allSequs :: Int -> [[(Int, Int)]]
allSequs Int
0 = [ [] ]
allSequs Int
l = [ (Int
i,Int
j)(Int, Int) -> [(Int, Int)] -> [(Int, Int)]
forall a. a -> [a] -> [a]
:[(Int, Int)]
rest | [(Int, Int)]
rest <- Int -> [[(Int, Int)]]
allSequs (Int
lInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1), Int
i <- [Int
1..Int
n], Int
j <- [Int
1..Int
n], Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
j ]