module SMCDEL.Examples.GossipS5 where

import SMCDEL.Language
import SMCDEL.Symbolic.S5
import Data.List ((\\))

gossipers :: Int -> [Int]
gossipers :: Int -> [Int]
gossipers Int
n = [Int
0..(Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)]

hasSof :: Int -> Int -> Int -> Prp
hasSof :: Int -> Int -> Int -> Prp
hasSof Int
n Int
a Int
b | Int
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
b    = [Char] -> Prp
forall a. HasCallStack => [Char] -> a
error [Char]
"Let's not even talk about that."
             | Bool
otherwise = Int -> Prp
forall a. Enum a => Int -> a
toEnum (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
b)

has :: Int -> Int -> Int -> Form
has :: Int -> Int -> Int -> Form
has Int
n Int
a Int
b = Prp -> Form
PrpF (Int -> Int -> Int -> Prp
hasSof Int
n Int
a Int
b)

expert :: Int -> Int -> Form
expert :: Int -> Int -> Form
expert Int
n Int
a = [Form] -> Form
Conj [ Prp -> Form
PrpF (Int -> Int -> Int -> Prp
hasSof Int
n Int
a Int
b) | Int
b <- Int -> [Int]
gossipers Int
n, Int
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
b ]

allExperts :: Int -> Form
allExperts :: Int -> Form
allExperts Int
n = [Form] -> Form
Conj [ Int -> Int -> Form
expert Int
n Int
a | Int
a <- Int -> [Int]
gossipers Int
n ]

gossipInit :: Int -> KnowScene
gossipInit :: Int -> KnowScene
gossipInit Int
n = ([Prp] -> Bdd -> [([Char], [Prp])] -> KnowStruct
KnS [Prp]
vocab Bdd
law [([Char], [Prp])]
forall {a}. [([Char], [a])]
obs, [Prp]
forall {a}. [a]
actual) where
  vocab :: [Prp]
vocab  = [ Int -> Int -> Int -> Prp
hasSof Int
n Int
i Int
j | Int
i <- Int -> [Int]
gossipers Int
n, Int
j <- Int -> [Int]
gossipers Int
n, Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
j ]
  law :: Bdd
law    = Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Conj [ Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Int -> Prp
hasSof Int
n Int
i Int
j
                            | Int
i <- Int -> [Int]
gossipers Int
n, Int
j <- Int -> [Int]
gossipers Int
n, Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
j]
  obs :: [([Char], [a])]
obs    = [ (Int -> [Char]
forall a. Show a => a -> [Char]
show Int
i, []) | Int
i <- Int -> [Int]
gossipers Int
n ]
  actual :: [a]
actual = [ ]

thisCallProp :: (Int,Int) -> Prp
thisCallProp :: (Int, Int) -> Prp
thisCallProp (Int
i,Int
j) | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
j     = Int -> Prp
P (Int
100 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
10Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
j)
                   | Bool
otherwise = [Char] -> Prp
forall a. HasCallStack => [Char] -> a
error ([Char] -> Prp) -> [Char] -> Prp
forall a b. (a -> b) -> a -> b
$ [Char]
"wrong call: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> [Char]
forall a. Show a => a -> [Char]
show (Int
i,Int
j)

call :: Int -> (Int,Int) -> Event
call :: Int -> (Int, Int) -> Event
call Int
n (Int
a,Int
b) = (Int -> KnowTransformer
callTrf Int
n, [(Int, Int) -> Prp
thisCallProp (Int
a,Int
b)])

callTrf :: Int -> KnowTransformer
callTrf :: Int -> KnowTransformer
callTrf Int
n = [Prp]
-> Form -> [(Prp, Bdd)] -> [([Char], [Prp])] -> KnowTransformer
KnTrf [Prp]
eventprops Form
eventlaw [(Prp, Bdd)]
changelaws [([Char], [Prp])]
eventobs where
  thisCallHappens :: (Int, Int) -> Form
thisCallHappens (Int
i,Int
j) = Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ (Int, Int) -> Prp
thisCallProp (Int
i,Int
j)
  isInCallForm :: Int -> Form
isInCallForm Int
k = [Form] -> Form
Disj ([Form] -> Form) -> [Form] -> Form
forall a b. (a -> b) -> a -> b
$ [ (Int, Int) -> Form
thisCallHappens (Int
i,Int
k) | Int
i <- Int -> [Int]
gossipers Int
n [Int] -> [Int] -> [Int]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Int
k], Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
k ]
                       [Form] -> [Form] -> [Form]
forall a. [a] -> [a] -> [a]
++ [ (Int, Int) -> Form
thisCallHappens (Int
k,Int
j) | Int
j <- Int -> [Int]
gossipers Int
n [Int] -> [Int] -> [Int]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Int
k], Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
j ]
  allCalls :: [(Int, Int)]
allCalls = [ (Int
i,Int
j) | Int
i <- Int -> [Int]
gossipers Int
n, Int
j <- Int -> [Int]
gossipers Int
n, Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
j ]
  eventprops :: [Prp]
eventprops = ((Int, Int) -> Prp) -> [(Int, Int)] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Int) -> Prp
thisCallProp [(Int, Int)]
allCalls
  eventlaw :: Form
eventlaw = Form -> Form
simplify (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$
    [Form] -> Form
Conj [ [Form] -> Form
Disj (((Int, Int) -> Form) -> [(Int, Int)] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Int) -> Form
thisCallHappens [(Int, Int)]
allCalls)
         -- some call must happen, but never two at the same time:
         , Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Disj [ [Form] -> Form
Conj [(Int, Int) -> Form
thisCallHappens (Int, Int)
c1, (Int, Int) -> Form
thisCallHappens (Int, Int)
c2]
                      | (Int, Int)
c1 <- [(Int, Int)]
allCalls, (Int, Int)
c2 <- [(Int, Int)]
allCalls [(Int, Int)] -> [(Int, Int)] -> [(Int, Int)]
forall a. Eq a => [a] -> [a] -> [a]
\\ [(Int, Int)
c1] ] ]
  callPropsWith :: Int -> [Prp]
callPropsWith Int
k = [ (Int, Int) -> Prp
thisCallProp (Int
i,Int
k) | Int
i <- Int -> [Int]
gossipers Int
n, Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
k ]
                 [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ [ (Int, Int) -> Prp
thisCallProp (Int
k,Int
j) | Int
j <- Int -> [Int]
gossipers Int
n, Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
j ]
  eventobs :: [([Char], [Prp])]
eventobs = [(Int -> [Char]
forall a. Show a => a -> [Char]
show Int
k, Int -> [Prp]
callPropsWith Int
k) | Int
k <- Int -> [Int]
gossipers Int
n]
  changelaws :: [(Prp, Bdd)]
changelaws =
    [(Int -> Int -> Int -> Prp
hasSof Int
n Int
i Int
j, Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$              -- after a call, i has the secret of j iff
        [Form] -> Form
Disj [ Int -> Int -> Int -> Form
has Int
n Int
i Int
j                     -- i already knew j, or
             , [Form] -> Form
Conj ((Int -> Form) -> [Int] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Form
isInCallForm [Int
i,Int
j]) -- i and j are both in the call or
             , [Form] -> Form
Conj [ Int -> Form
isInCallForm Int
i         -- i is in the call and there is some k in
                    , [Form] -> Form
Disj [ [Form] -> Form
Conj [ Int -> Form
isInCallForm Int
k, Int -> Int -> Int -> Form
has Int
n Int
k Int
j ] -- the call who knew j
                           | Int
k <- Int -> [Int]
gossipers Int
n [Int] -> [Int] -> [Int]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Int
j] ] ]
             ])
    | Int
i <- Int -> [Int]
gossipers Int
n, Int
j <- Int -> [Int]
gossipers Int
n, Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
j ]

doCall :: KnowScene -> (Int,Int) -> KnowScene
doCall :: KnowScene -> (Int, Int) -> KnowScene
doCall KnowScene
start (Int
a,Int
b) = KnowScene
start KnowScene -> Event -> KnowScene
forall a b. Update a b => a -> b -> a
`update` Int -> (Int, Int) -> Event
call ([[Char]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([[Char]] -> Int) -> [[Char]] -> Int
forall a b. (a -> b) -> a -> b
$ KnowScene -> [[Char]]
forall a. HasAgents a => a -> [[Char]]
agentsOf KnowScene
start) (Int
a,Int
b)

after :: Int -> [(Int,Int)] -> KnowScene
after :: Int -> [(Int, Int)] -> KnowScene
after Int
n = (KnowScene -> (Int, Int) -> KnowScene)
-> KnowScene -> [(Int, Int)] -> KnowScene
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl KnowScene -> (Int, Int) -> KnowScene
doCall (Int -> KnowScene
gossipInit Int
n)

isSuccess :: Int -> [(Int,Int)] -> Bool
isSuccess :: Int -> [(Int, Int)] -> Bool
isSuccess Int
n [(Int, Int)]
cs = KnowScene -> Form -> Bool
evalViaBdd (Int -> [(Int, Int)] -> KnowScene
after Int
n [(Int, Int)]
cs) (Int -> Form
allExperts Int
n)

whoKnowsMeta :: KnowScene -> [(Int,[(Int,String)])]
whoKnowsMeta :: KnowScene -> [(Int, [(Int, [Char])])]
whoKnowsMeta KnowScene
scn = [ (Int
k, (Int -> (Int, [Char])) -> [Int] -> [(Int, [Char])]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Int -> (Int, [Char])
forall {a}. Show a => a -> Int -> (Int, [Char])
meta Int
k) [Int
0..Int
maxid] ) | Int
k <- [Int
0..Int
maxid] ] where
  n :: Int
n = [[Char]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (KnowScene -> [[Char]]
forall a. HasAgents a => a -> [[Char]]
agentsOf KnowScene
scn)
  maxid :: Int
maxid = Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
  meta :: a -> Int -> (Int, [Char])
meta a
x Int
y = (Int
y, (Int -> Char) -> [Int] -> [Char]
forall a b. (a -> b) -> [a] -> [b]
map (a -> Int -> Int -> Char
forall {a}. Show a => a -> Int -> Int -> Char
knowsAbout a
x Int
y) [Int
0..Int
maxid])
  knowsAbout :: a -> Int -> Int -> Char
knowsAbout a
x Int
y Int
i
    | Int
y Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
i = Char
'X'
    | KnowScene -> Form -> Bool
evalViaBdd KnowScene
scn (      [Char] -> Form -> Form
K (a -> [Char]
forall a. Show a => a -> [Char]
show a
x) (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$       Prp -> Form
PrpF (Int -> Int -> Int -> Prp
hasSof Int
n Int
y Int
i)) = Char
'Y'
    | KnowScene -> Form -> Bool
evalViaBdd KnowScene
scn (Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ [Char] -> Form -> Form
K (a -> [Char]
forall a. Show a => a -> [Char]
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
$ Prp -> Form
PrpF (Int -> Int -> Int -> Prp
hasSof Int
n Int
y Int
i)) = Char
'?'
    | KnowScene -> Form -> Bool
evalViaBdd KnowScene
scn (      [Char] -> Form -> Form
K (a -> [Char]
forall a. Show a => a -> [Char]
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
$ Prp -> Form
PrpF (Int -> Int -> Int -> Prp
hasSof Int
n Int
y Int
i)) = Char
'_'
    | Bool
otherwise                                                     = Char
'E'

allSequs :: Int -> Int -> [ [(Int,Int)] ]
allSequs :: Int -> Int -> [[(Int, Int)]]
allSequs Int
_ Int
0 = [ [] ]
allSequs Int
n 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, Int)]]
allSequs Int
n (Int
lInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1), Int
i <- Int -> [Int]
gossipers Int
n, Int
j <- Int -> [Int]
gossipers Int
n, Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
j ]