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) -- k participates in the call
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)) -- secret k is being exchanged (as true)

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])
    -- lnsPreCondition i j = Neg $ K (show i) (PrpF $ P 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))

-- What do agents know, and what do they know about each others knowledge?
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 ]