{-|
Module      : GossipKnowledge
Description : Implements Knowledge Structures and Knowledge Transformers as defined in (Gattinger, 2018).
Copyright   : (c) Jesper Kuiper, 2021
                  Leander van Boven, 2021
                  Ramon Meffert, 2021
License     : BSD3
-}

module GossipKnowledge 
  ( -- * Atomic proposition for Dynamic Gossip
    GossipAtom ( GAt )
  , Rel( N, S, C )
  -- ** Conversion to and from BDDs
  , intToGAt
  , bddToGAt
  , gAtToInt
  , gAtToBdd
  -- ** Texification
  , texifyGAt
  , texifyBddVar
  -- * Epistemic formulae for Dyamic Gossip
  , Form ( Fact, K, M )
  , GossipForm (Top, Atom, Neg, Conj, Disj, Impl )
  -- * Knowledge Structures for Dynamic Gossip
  , GossipKnowledgeStructure ( GKS )
  -- ** Knowledge Structure fields
  , vocabulary
  , stateLaw
  , observables
  , nag
  -- ** Generation and validation
  , fromGossipGraph
  , validKS
  -- ** Transition from epistemic to boolean formulae
  , formToBdd
  , (<|>)
  -- * Knowledge Transformers for Dyamic Gossip
  , KnowledgeTransformer ( KT )
  -- ** Knowledge Transformer fields
  , addVocab
  , eventLaw
  , addObs
  -- ** Generation and validation
  , baseTransformer
  , validKT
  -- * Updating Knowledge Structures 
  , update
  , (|+|)
  , updateWithCall
  ) where

import Data.Graph.Inductive.Graph
--import Data.HasCacBDD
import Data.Map.Strict ( Map, unionWith, (!) )
import Data.Set ( Set, union, isSubsetOf, (\\) )
import System.IO

import qualified Data.List as List
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set

import GossipGraph
import GossipTypes
import PrintableBdd hiding ( var, forall, exists, forallSet, existsSet )
import Util


{- 
    Atomic propositions for gossip 
-}

-- | The relation type of a GossipAtom. 
data Rel = N  -- ^ Indicates that x knows the number of y.
         | S  -- ^ Indicates that x knows the secret of y.
         | C  -- ^ Indicates that x has called y.
         deriving (Int -> Rel -> ShowS
[Rel] -> ShowS
Rel -> String
(Int -> Rel -> ShowS)
-> (Rel -> String) -> ([Rel] -> ShowS) -> Show Rel
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Rel] -> ShowS
$cshowList :: [Rel] -> ShowS
show :: Rel -> String
$cshow :: Rel -> String
showsPrec :: Int -> Rel -> ShowS
$cshowsPrec :: Int -> Rel -> ShowS
Show, Eq Rel
Eq Rel
-> (Rel -> Rel -> Ordering)
-> (Rel -> Rel -> Bool)
-> (Rel -> Rel -> Bool)
-> (Rel -> Rel -> Bool)
-> (Rel -> Rel -> Bool)
-> (Rel -> Rel -> Rel)
-> (Rel -> Rel -> Rel)
-> Ord Rel
Rel -> Rel -> Bool
Rel -> Rel -> Ordering
Rel -> Rel -> Rel
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Rel -> Rel -> Rel
$cmin :: Rel -> Rel -> Rel
max :: Rel -> Rel -> Rel
$cmax :: Rel -> Rel -> Rel
>= :: Rel -> Rel -> Bool
$c>= :: Rel -> Rel -> Bool
> :: Rel -> Rel -> Bool
$c> :: Rel -> Rel -> Bool
<= :: Rel -> Rel -> Bool
$c<= :: Rel -> Rel -> Bool
< :: Rel -> Rel -> Bool
$c< :: Rel -> Rel -> Bool
compare :: Rel -> Rel -> Ordering
$ccompare :: Rel -> Rel -> Ordering
$cp1Ord :: Eq Rel
Ord, Rel -> Rel -> Bool
(Rel -> Rel -> Bool) -> (Rel -> Rel -> Bool) -> Eq Rel
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Rel -> Rel -> Bool
$c/= :: Rel -> Rel -> Bool
== :: Rel -> Rel -> Bool
$c== :: Rel -> Rel -> Bool
Eq, Int -> Rel
Rel -> Int
Rel -> [Rel]
Rel -> Rel
Rel -> Rel -> [Rel]
Rel -> Rel -> Rel -> [Rel]
(Rel -> Rel)
-> (Rel -> Rel)
-> (Int -> Rel)
-> (Rel -> Int)
-> (Rel -> [Rel])
-> (Rel -> Rel -> [Rel])
-> (Rel -> Rel -> [Rel])
-> (Rel -> Rel -> Rel -> [Rel])
-> Enum Rel
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: Rel -> Rel -> Rel -> [Rel]
$cenumFromThenTo :: Rel -> Rel -> Rel -> [Rel]
enumFromTo :: Rel -> Rel -> [Rel]
$cenumFromTo :: Rel -> Rel -> [Rel]
enumFromThen :: Rel -> Rel -> [Rel]
$cenumFromThen :: Rel -> Rel -> [Rel]
enumFrom :: Rel -> [Rel]
$cenumFrom :: Rel -> [Rel]
fromEnum :: Rel -> Int
$cfromEnum :: Rel -> Int
toEnum :: Int -> Rel
$ctoEnum :: Int -> Rel
pred :: Rel -> Rel
$cpred :: Rel -> Rel
succ :: Rel -> Rel
$csucc :: Rel -> Rel
Enum)

-- | An atomic proposition in a gossip state: Rel(Agent, Agent).
data GossipAtom = GAt Rel Agent Agent deriving (Eq GossipAtom
Eq GossipAtom
-> (GossipAtom -> GossipAtom -> Ordering)
-> (GossipAtom -> GossipAtom -> Bool)
-> (GossipAtom -> GossipAtom -> Bool)
-> (GossipAtom -> GossipAtom -> Bool)
-> (GossipAtom -> GossipAtom -> Bool)
-> (GossipAtom -> GossipAtom -> GossipAtom)
-> (GossipAtom -> GossipAtom -> GossipAtom)
-> Ord GossipAtom
GossipAtom -> GossipAtom -> Bool
GossipAtom -> GossipAtom -> Ordering
GossipAtom -> GossipAtom -> GossipAtom
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: GossipAtom -> GossipAtom -> GossipAtom
$cmin :: GossipAtom -> GossipAtom -> GossipAtom
max :: GossipAtom -> GossipAtom -> GossipAtom
$cmax :: GossipAtom -> GossipAtom -> GossipAtom
>= :: GossipAtom -> GossipAtom -> Bool
$c>= :: GossipAtom -> GossipAtom -> Bool
> :: GossipAtom -> GossipAtom -> Bool
$c> :: GossipAtom -> GossipAtom -> Bool
<= :: GossipAtom -> GossipAtom -> Bool
$c<= :: GossipAtom -> GossipAtom -> Bool
< :: GossipAtom -> GossipAtom -> Bool
$c< :: GossipAtom -> GossipAtom -> Bool
compare :: GossipAtom -> GossipAtom -> Ordering
$ccompare :: GossipAtom -> GossipAtom -> Ordering
$cp1Ord :: Eq GossipAtom
Ord, GossipAtom -> GossipAtom -> Bool
(GossipAtom -> GossipAtom -> Bool)
-> (GossipAtom -> GossipAtom -> Bool) -> Eq GossipAtom
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GossipAtom -> GossipAtom -> Bool
$c/= :: GossipAtom -> GossipAtom -> Bool
== :: GossipAtom -> GossipAtom -> Bool
$c== :: GossipAtom -> GossipAtom -> Bool
Eq)

instance Show GossipAtom where
  show :: GossipAtom -> String
show (GAt Rel
rel Agent
a1 Agent
a2) = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Rel -> String
forall a. Show a => a -> String
show Rel
rel, Agent -> String
showAgent Agent
a1, Agent -> String
showAgent Agent
a2]

-- | Converts an atomic gossip proposition into a LaTeX string.
--
-- >>> texify (GAt N a b)
-- \texttt{N}ab
texifyGAt :: GossipAtom -> String
texifyGAt :: GossipAtom -> String
texifyGAt (GAt Rel
rel Agent
a1 Agent
a2) = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
List.concat [String
"\\texttt{", Rel -> String
forall a. Show a => a -> String
show Rel
rel, Agent -> String
showAgent Agent
a1, Agent -> String
showAgent Agent
a2, String
"}"]

-- | Converts a BDD formula to a list of GossipAtoms for all variables in the formula. Internally calls intToGAt.
--
-- >>> bddToGAt 3 ((var 0) `imp` (var 12))
-- >>> [Naa, Sba]
bddToGAt :: Int -> Bdd -> [GossipAtom]
bddToGAt :: Int -> Bdd -> [GossipAtom]
bddToGAt Int
n Bdd
bdd = (Int -> GossipAtom) -> [Int] -> [GossipAtom]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Int -> GossipAtom
intToGAt Int
n) (Bdd -> [Int]
allVarsOf Bdd
bdd)

-- | Converts a BDD variable index to a GossipAtom. Note that the first Int argument corresponds to the amount of agents present in the gossip graph. This is a bijective function to allow for unique indexing of atomic gossip propositions. 
--
-- >>> intToGAt 3 0
-- Naa
-- 
-- >>> intToGAt 3 12
-- Sba
intToGAt :: Int -> Int -> GossipAtom
intToGAt :: Int -> Int -> GossipAtom
intToGAt Int
n Int
v = Rel -> Agent -> Agent -> GossipAtom
GAt (Int -> Rel
forall a. Enum a => Int -> a
toEnum Int
rel) (Int
a1, Int -> Char
idToLab Int
a1) (Int
a2, Int -> Char
idToLab Int
a2)
  where rel :: Int
rel =  Int
v                   Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
nInt -> Integer -> Int
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
2
        a1 :: Int
a1  =  Int
v Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
nInt -> Integer -> Int
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
2         Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
n
        a2 :: Int
a2  =  Int
v Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
nInt -> Integer -> Int
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
2 Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
n

-- | Converts a BDD variable index to a GossipAtom, and converts that to a string.
--
-- >>> showBddVar 3 12
-- >>> "Sba"
showBddVar :: Int -> Int -> String
showBddVar :: Int -> Int -> String
showBddVar Int
n = GossipAtom -> String
forall a. Show a => a -> String
show (GossipAtom -> String) -> (Int -> GossipAtom) -> Int -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> GossipAtom
intToGAt Int
n

-- | Converts a BDD variable index to a GossipAtom, and converts that to a LaTeX string.
--
-- >>> texifyBddVar 3 12
-- "\texttt{S}ba"
texifyBddVar :: Int -> Int -> String
texifyBddVar :: Int -> Int -> String
texifyBddVar Int
n = GossipAtom -> String
texifyGAt (GossipAtom -> String) -> (Int -> GossipAtom) -> Int -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> GossipAtom
intToGAt Int
n

-- | Converts a GossipAtom to a unique but labelled BDD variable. Note that the first argument corresponds to the amount of agents present in the gossip graph. 
--
-- >>> gAtToBdd 3 (GAt S b a)
-- Sba
--
-- Note that, while this function prints the normal gossip atom, the type that is returned is of BDD instead of GossipAtom. Internally, a unique variable index has been generated.
gAtToBdd :: Int -> GossipAtom -> Bdd
gAtToBdd :: Int -> GossipAtom -> Bdd
gAtToBdd Int
n GossipAtom
gat = Int -> Int -> Bdd
gvar Int
n (Int -> Bdd) -> Int -> Bdd
forall a b. (a -> b) -> a -> b
$ Int -> GossipAtom -> Int
gAtToInt Int
n GossipAtom
gat

-- | Converts a GossipAtom to a unique integer index that can be used for a BDD variable. 
--
-- >>> gAtToInt 3 (GAt S b a)
-- 12
gAtToInt :: Int -> GossipAtom -> Int
gAtToInt :: Int -> GossipAtom -> Int
gAtToInt Int
n (GAt Rel
rel (Int
a1,Char
_) (Int
a2,Char
_)) = Int
nInt -> Integer -> Int
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Rel -> Int
forall a. Enum a => a -> Int
fromEnum Rel
rel Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
a1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
a2


-- Local helper functions

-- | Generates a labelled BDD variable based on agent count and a variable index. 
gvar :: Int -> Int -> Bdd
gvar :: Int -> Int -> Bdd
gvar Int
n = (Int -> String) -> (Int -> String) -> Int -> Bdd
varl (Int -> Int -> String
showBddVar Int
n) (Int -> Int -> String
texifyBddVar Int
n)

-- | The labeller that is used to label variables in the BDD. 
strLabel :: Int -> VarLabeller
strLabel :: Int -> Int -> String
strLabel = Int -> Int -> String
showBddVar

-- | The labeller that is used to label variables in the LaTeX string of the BDD.
texLabel :: Int -> VarLabeller
texLabel :: Int -> Int -> String
texLabel = Int -> Int -> String
texifyBddVar


{- 
    Epistemic formulae for gossip
-}

-- | A recursively defined propositional formula build out of GossipAtoms.
data GossipForm
    = Top                           -- ^ Always true
    | Atom GossipAtom               -- ^ Atom
    | Neg GossipForm                -- ^ Negation
    | Conj [GossipForm]             -- ^ Conjunction
    | Disj [GossipForm]             -- ^ Disjunction   
    | Impl GossipForm GossipForm    -- ^ Implication
    deriving (Int -> GossipForm -> ShowS
[GossipForm] -> ShowS
GossipForm -> String
(Int -> GossipForm -> ShowS)
-> (GossipForm -> String)
-> ([GossipForm] -> ShowS)
-> Show GossipForm
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [GossipForm] -> ShowS
$cshowList :: [GossipForm] -> ShowS
show :: GossipForm -> String
$cshow :: GossipForm -> String
showsPrec :: Int -> GossipForm -> ShowS
$cshowsPrec :: Int -> GossipForm -> ShowS
Show)

-- | An epistemic formula, defined in terms of BDDs. This data structure allows for propositional formulae, as well as (higher-order) agent knowledge.  
data Form = Fact Bdd
          | K Agent Form
          | M Agent Form

instance Show Form where
  show :: Form -> String
show (Fact Bdd
bdd) = Bdd -> String
forall a. Show a => a -> String
show Bdd
bdd
  show (K Agent
ag Form
form) = String
"K" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent -> String
showAgent Agent
ag String -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> String
forall a. Show a => a -> String
show Form
form
  show (M Agent
ag Form
form) = String
"K̂" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent -> String
showAgent Agent
ag String -> ShowS
forall a. [a] -> [a] -> [a]
++ Form -> String
forall a. Show a => a -> String
show Form
form


{- 
    Knowledge Structures for gossip
-}

-- | A knowledge structure (Gattinger, 2018) which represents the knowledge of a Gossip State. 
data GossipKnowledgeStructure = GKS
  { -- | The set of propositional atoms available in the model. 
    GossipKnowledgeStructure -> Set Int
vocabulary :: Set Int,

    -- | A boolean formula representing the law that every state needs to adhere to. 
    GossipKnowledgeStructure -> Bdd
stateLaw :: Bdd,

    -- | The set of atoms seen by some agent. If an atom is observable for an agent, then they are certain as to whether this atom is true or false. 
    GossipKnowledgeStructure -> Map Agent (Set Int)
observables :: Map Agent (Set Int)
  } deriving ( GossipKnowledgeStructure -> GossipKnowledgeStructure -> Bool
(GossipKnowledgeStructure -> GossipKnowledgeStructure -> Bool)
-> (GossipKnowledgeStructure -> GossipKnowledgeStructure -> Bool)
-> Eq GossipKnowledgeStructure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GossipKnowledgeStructure -> GossipKnowledgeStructure -> Bool
$c/= :: GossipKnowledgeStructure -> GossipKnowledgeStructure -> Bool
== :: GossipKnowledgeStructure -> GossipKnowledgeStructure -> Bool
$c== :: GossipKnowledgeStructure -> GossipKnowledgeStructure -> Bool
Eq )

instance Show GossipKnowledgeStructure where
  show :: GossipKnowledgeStructure -> String
show (GKS Set Int
v Bdd
l Map Agent (Set Int)
o) = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ String
"vocabulary: { ", String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate String
",\n              "  [String]
vocab, String
" }"
    , String
"\nstate law: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bdd -> String
forall a. Show a => a -> String
show Bdd
l
    , String
"\nobservables: ", String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate String
"\n             " ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ ((Agent, Set Int) -> String) -> [(Agent, Set Int)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Agent, Set Int) -> String
shObs (Map Agent (Set Int) -> [(Agent, Set Int)]
forall k a. Map k a -> [(k, a)]
Map.assocs Map Agent (Set Int)
o)
    ] where

      vocab :: [String]
vocab = ([String] -> String) -> [[String]] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate String
", ") ([[String]] -> [String]) -> [[String]] -> [String]
forall a b. (a -> b) -> a -> b
$ Int -> [String] -> [[String]]
forall e. Int -> [e] -> [[e]]
chunksOf Int
9 ([String] -> [[String]]) -> [String] -> [[String]]
forall a b. (a -> b) -> a -> b
$ (Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
gat (Set Int -> [Int]
forall a. Set a -> [a]
Set.toList Set Int
v)

      gat :: Int -> String
      gat :: Int -> String
gat = GossipAtom -> String
forall a. Show a => a -> String
show (GossipAtom -> String) -> (Int -> GossipAtom) -> Int -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> GossipAtom
intToGAt (Map Agent (Set Int) -> Int
forall k a. Map k a -> Int
Map.size Map Agent (Set Int)
o)

      shObs :: (Agent, Set Int) -> String
      shObs :: (Agent, Set Int) -> String
shObs (Agent
a, Set Int
s) =  [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
        [ Agent -> String
showAgent Agent
a, String
" -> "
        , String
"{ ", String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
List.intercalate String
", " ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
gat (Set Int -> [Int]
forall a. Set a -> [a]
Set.toList Set Int
s), String
" }"
        ]

      -- The following two functions were taken from the source code of Data.List.Split, so that we don't have to 
      -- import the entire module. 
      -- Source: https://hackage.haskell.org/package/split-0.2.3.4/docs/src/Data.List.Split.Internals.html#build
      build :: ((a -> [a] -> [a]) -> [a] -> [a]) -> [a]
      build :: ((a -> [a] -> [a]) -> [a] -> [a]) -> [a]
build (a -> [a] -> [a]) -> [a] -> [a]
g = (a -> [a] -> [a]) -> [a] -> [a]
g (:) []

      chunksOf :: Int -> [e] -> [[e]]
      chunksOf :: Int -> [e] -> [[e]]
chunksOf Int
i [e]
ls = ([e] -> [e]) -> [[e]] -> [[e]]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> [e] -> [e]
forall a. Int -> [a] -> [a]
take Int
i) ((([e] -> [[e]] -> [[e]]) -> [[e]] -> [[e]]) -> [[e]]
forall a. ((a -> [a] -> [a]) -> [a] -> [a]) -> [a]
build ([e] -> ([e] -> [[e]] -> [[e]]) -> [[e]] -> [[e]]
forall e a. [e] -> ([e] -> a -> a) -> a -> a
splitter [e]
ls)) where
        splitter :: [e] -> ([e] -> a -> a) -> a -> a
        splitter :: [e] -> ([e] -> a -> a) -> a -> a
splitter [] [e] -> a -> a
_ a
n = a
n
        splitter [e]
l [e] -> a -> a
c a
n  = [e]
l [e] -> a -> a
`c` [e] -> ([e] -> a -> a) -> a -> a
forall e a. [e] -> ([e] -> a -> a) -> a -> a
splitter (Int -> [e] -> [e]
forall a. Int -> [a] -> [a]
drop Int
i [e]
l) [e] -> a -> a
c a
n
      -- End of copy

-- | Checks if a given Knowledge Structure is valid. It checks whether the variables found in both the state law and the observable sets are present in the vocabulary. 
validKS :: GossipKnowledgeStructure -> Bool
validKS :: GossipKnowledgeStructure -> Bool
validKS (GKS Set Int
vocab Bdd
law Map Agent (Set Int)
obs) =
  let lawCheck :: Bool
lawCheck = [Int] -> Set Int
forall a. Ord a => [a] -> Set a
Set.fromList (Bdd -> [Int]
allVarsOf Bdd
law) Set Int -> Set Int -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`isSubsetOf` Set Int
vocab
      obsCheck :: Bool
obsCheck = (Set Int -> Bool -> Bool) -> Bool -> Map Agent (Set Int) -> Bool
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr (Bool -> Bool -> Bool
(&&) (Bool -> Bool -> Bool)
-> (Set Int -> Bool) -> Set Int -> Bool -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set Int -> Set Int -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`isSubsetOf` Set Int
vocab)) Bool
True Map Agent (Set Int)
obs
   in Bool
lawCheck Bool -> Bool -> Bool
&& Bool
obsCheck

-- | Converts a gossip graph to its corresponding knowledge structure. 
--   Note that this doesn't convert a gossip state, i.e. no call sequence is encoded.
--   This is meant for the conversion of the _initial_ gossip state, (G, ε) 
--   (van Ditmarsch et al., 2017)
fromGossipGraph :: GossipGraph -> GossipKnowledgeStructure
fromGossipGraph :: GossipGraph -> GossipKnowledgeStructure
fromGossipGraph GossipGraph
graph =
  let agents :: [Agent]
agents = GossipGraph -> [Agent]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes GossipGraph
graph
      n :: Int
n = [Agent] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Agent]
agents

      gvar :: GossipAtom -> Bdd
gvar = Int -> GossipAtom -> Bdd
gAtToBdd Int
n
      gint :: GossipAtom -> Int
gint = Int -> GossipAtom -> Int
gAtToInt Int
n

      -- vocabulary
      agentCombs :: [(Agent, Agent)]
agentCombs = [(Agent
x,Agent
y) | Agent
x <- [Agent]
agents, Agent
y <- [Agent]
agents]
      vocabAtoms :: [GossipAtom]
vocabAtoms = ((Agent, Agent) -> [GossipAtom] -> [GossipAtom])
-> [GossipAtom] -> [(Agent, Agent)] -> [GossipAtom]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Agent
x,Agent
y) -> [GossipAtom] -> [GossipAtom] -> [GossipAtom]
forall a. [a] -> [a] -> [a]
(++) [Rel -> Agent -> Agent -> GossipAtom
GAt Rel
N Agent
x Agent
y, Rel -> Agent -> Agent -> GossipAtom
GAt Rel
S Agent
x Agent
y, Rel -> Agent -> Agent -> GossipAtom
GAt Rel
C Agent
x Agent
y]) [] [(Agent, Agent)]
agentCombs
      vocabulary :: [Int]
vocabulary = (GossipAtom -> Int) -> [GossipAtom] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map GossipAtom -> Int
gint [GossipAtom]
vocabAtoms

      -- state law
      stateLaw :: Bdd
stateLaw = [Bdd] -> Bdd
conSet ((Agent -> [Bdd] -> [Bdd]) -> [Bdd] -> [Agent] -> [Bdd]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ Agent
x -> [Bdd] -> [Bdd] -> [Bdd]
forall a. [a] -> [a] -> [a]
(++) [GossipAtom -> Bdd
gvar (Rel -> Agent -> Agent -> GossipAtom
GAt Rel
N Agent
x Agent
x), GossipAtom -> Bdd
gvar (Rel -> Agent -> Agent -> GossipAtom
GAt Rel
S Agent
x Agent
x)]) [] [Agent]
agents)
        Bdd -> Bdd -> Bdd
`con` [Bdd] -> Bdd
conSet (
          [ GossipAtom -> Bdd
gvar (Rel -> Agent -> Agent -> GossipAtom
GAt Rel
C Agent
x Agent
y) Bdd -> Bdd -> Bdd
`imp` [Bdd] -> Bdd
conSet             --  if x has called y;
            [ GossipAtom -> Bdd
gvar (Rel -> Agent -> Agent -> GossipAtom
GAt Rel
N Agent
x Agent
y)                        --  then x knows y's number;
            , GossipAtom -> Bdd
gvar (Rel -> Agent -> Agent -> GossipAtom
GAt Rel
N Agent
y Agent
x)                        --  and y knows x's number;
            , GossipAtom -> Bdd
gvar (Rel -> Agent -> Agent -> GossipAtom
GAt Rel
S Agent
x Agent
y)                        --  and x knows y's secret;
            , GossipAtom -> Bdd
gvar (Rel -> Agent -> Agent -> GossipAtom
GAt Rel
S Agent
y Agent
x)                        --  and y knows x's secret;
            ] | Agent
x <- [Agent]
agents, Agent
y <- [Agent]
agents, Agent
x Agent -> Agent -> Bool
forall a. Eq a => a -> a -> Bool
/= Agent
y] [Bdd] -> [Bdd] -> [Bdd]
forall a. [a] -> [a] -> [a]
++ 
          [ GossipAtom -> Bdd
gvar (Rel -> Agent -> Agent -> GossipAtom
GAt Rel
C Agent
x Agent
y) Bdd -> Bdd -> Bdd
`imp` [Bdd] -> Bdd
conSet         
            [ GossipAtom -> Bdd
gvar (Rel -> Agent -> Agent -> GossipAtom
GAt Rel
N Agent
x Agent
z) Bdd -> Bdd -> Bdd
`equ` GossipAtom -> Bdd
gvar (Rel -> Agent -> Agent -> GossipAtom
GAt Rel
N Agent
y Agent
z) -- and if x knows the number of some z, then y does so as well (and vice versa);
            , GossipAtom -> Bdd
gvar (Rel -> Agent -> Agent -> GossipAtom
GAt Rel
S Agent
x Agent
z) Bdd -> Bdd -> Bdd
`equ` GossipAtom -> Bdd
gvar (Rel -> Agent -> Agent -> GossipAtom
GAt Rel
S Agent
y Agent
z) -- and if x knows the secret of some z, then y does so as well (and vice versa).
            ] | Agent
x <- [Agent]
agents, Agent
y <- [Agent]
agents, Agent
x Agent -> Agent -> Bool
forall a. Eq a => a -> a -> Bool
/= Agent
y, Agent
z <- [Agent]
agents, Agent
x Agent -> Agent -> Bool
forall a. Eq a => a -> a -> Bool
/= Agent
z, Agent
y Agent -> Agent -> Bool
forall a. Eq a => a -> a -> Bool
/= Agent
z
          ])

      -- observables
      initials :: [GossipAtom]
initials = (Agent -> [GossipAtom] -> [GossipAtom])
-> [GossipAtom] -> [Agent] -> [GossipAtom]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ Agent
x -> [GossipAtom] -> [GossipAtom] -> [GossipAtom]
forall a. [a] -> [a] -> [a]
(++) [Rel -> Agent -> Agent -> GossipAtom
GAt Rel
N Agent
x Agent
x, Rel -> Agent -> Agent -> GossipAtom
GAt Rel
S Agent
x Agent
x]) [] [Agent]
agents
      numbersOf :: Agent -> [GossipAtom]
numbersOf Agent
ag = [Rel -> Agent -> Agent -> GossipAtom
GAt Rel
N Agent
ag Agent
x | Agent
x <- GossipGraph -> Agent -> [Agent]
numbersKnownBy GossipGraph
graph Agent
ag]

      observablesOf :: Agent -> [Int]
observablesOf Agent
ag = (GossipAtom -> Int) -> [GossipAtom] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map GossipAtom -> Int
gint ([GossipAtom] -> [Int]) -> [GossipAtom] -> [Int]
forall a b. (a -> b) -> a -> b
$ [GossipAtom]
initials [GossipAtom] -> [GossipAtom] -> [GossipAtom]
forall a. [a] -> [a] -> [a]
++ Agent -> [GossipAtom]
numbersOf Agent
ag
      observables :: Map Agent (Set Int)
observables = [(Agent, Set Int)] -> Map Agent (Set Int)
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Agent
a, [Int] -> Set Int
forall a. Ord a => [a] -> Set a
Set.fromList ([Int] -> Set Int) -> [Int] -> Set Int
forall a b. (a -> b) -> a -> b
$ Agent -> [Int]
observablesOf Agent
a) | Agent
a <- [Agent]
agents]

   in Set Int -> Bdd -> Map Agent (Set Int) -> GossipKnowledgeStructure
GKS ([Int] -> Set Int
forall a. Ord a => [a] -> Set a
Set.fromList [Int]
vocabulary) Bdd
stateLaw Map Agent (Set Int)
observables

-- | Converts an epistemic formula to a boolean formula, given a knowledge structure
--   in Gattinger (2018), `fromToBdd k ϕ` is denoted by ||ϕ||_k.
formToBdd :: GossipKnowledgeStructure -> Form -> Bdd
formToBdd :: GossipKnowledgeStructure -> Form -> Bdd
formToBdd GossipKnowledgeStructure
k Form
form =
  case Form
form of
    Fact Bdd
bdd -> Bdd
bdd
    K Agent
ag Form
f -> GossipKnowledgeStructure -> Agent -> Form -> Bdd
knowledgeToBdd GossipKnowledgeStructure
k Agent
ag Form
f
    M Agent
ag Form
f -> Bdd -> Bdd
neg (Bdd -> Bdd) -> Bdd -> Bdd
forall a b. (a -> b) -> a -> b
$ GossipKnowledgeStructure -> Agent -> Form -> Bdd
knowledgeToBdd GossipKnowledgeStructure
k Agent
ag Form
f
  where
    knowledgeToBdd :: GossipKnowledgeStructure -> Agent -> Form -> Bdd
knowledgeToBdd GossipKnowledgeStructure
k Agent
ag Form
f =
      let universe :: [Int]
universe = Set Int -> [Int]
forall a. Set a -> [a]
Set.toList (Set Int -> [Int]) -> Set Int -> [Int]
forall a b. (a -> b) -> a -> b
$ GossipKnowledgeStructure -> Set Int
vocabulary GossipKnowledgeStructure
k Set Int -> Set Int -> Set Int
forall a. Ord a => Set a -> Set a -> Set a
\\ (GossipKnowledgeStructure -> Map Agent (Set Int)
observables GossipKnowledgeStructure
k Map Agent (Set Int) -> Agent -> Set Int
forall k a. Ord k => Map k a -> k -> a
! Agent
ag)
          formula :: Bdd
formula = case Form
f of
            Fact bdd -> GossipKnowledgeStructure -> Bdd
stateLaw GossipKnowledgeStructure
k Bdd -> Bdd -> Bdd
`imp` Bdd
bdd
            K a f -> GossipKnowledgeStructure -> Bdd
stateLaw GossipKnowledgeStructure
k Bdd -> Bdd -> Bdd
`imp` GossipKnowledgeStructure -> Agent -> Form -> Bdd
knowledgeToBdd GossipKnowledgeStructure
k Agent
a Form
f
            M a f -> Bdd -> Bdd
neg (Bdd -> Bdd) -> Bdd -> Bdd
forall a b. (a -> b) -> a -> b
$ GossipKnowledgeStructure -> Bdd
stateLaw GossipKnowledgeStructure
k Bdd -> Bdd -> Bdd
`imp` Bdd -> Bdd
neg (GossipKnowledgeStructure -> Agent -> Form -> Bdd
knowledgeToBdd GossipKnowledgeStructure
k Agent
a Form
f)
      in GossipKnowledgeStructure -> [Int] -> Bdd -> Bdd
gforallSet GossipKnowledgeStructure
k [Int]
universe Bdd
formula


-- | An infix operator for the formToBdd function. 
(<|>) :: GossipKnowledgeStructure -> Form -> Bdd
GossipKnowledgeStructure
k <|> :: GossipKnowledgeStructure -> Form -> Bdd
<|> Form
ϕ = GossipKnowledgeStructure -> Form -> Bdd
formToBdd GossipKnowledgeStructure
k Form
ϕ
infix 9 <|>


-- Private helper functions for Knowledge Structures

-- | Extracts the number of agents from the Knowledge Structure. 
nag :: GossipKnowledgeStructure -> Int
nag :: GossipKnowledgeStructure -> Int
nag (GKS Set Int
_ Bdd
_ Map Agent (Set Int)
o) = Map Agent (Set Int) -> Int
forall k a. Map k a -> Int
Map.size Map Agent (Set Int)
o

gforall :: GossipKnowledgeStructure -> Int -> Bdd -> Bdd
gforall :: GossipKnowledgeStructure -> Int -> Bdd -> Bdd
gforall GossipKnowledgeStructure
k = (Int -> String) -> (Int -> String) -> Int -> Bdd -> Bdd
foralll (Int -> Int -> String
strLabel (Int -> Int -> String) -> Int -> Int -> String
forall a b. (a -> b) -> a -> b
$ GossipKnowledgeStructure -> Int
nag GossipKnowledgeStructure
k) (Int -> Int -> String
texLabel (Int -> Int -> String) -> Int -> Int -> String
forall a b. (a -> b) -> a -> b
$ GossipKnowledgeStructure -> Int
nag GossipKnowledgeStructure
k)

gexists :: GossipKnowledgeStructure -> Int -> Bdd -> Bdd
gexists :: GossipKnowledgeStructure -> Int -> Bdd -> Bdd
gexists GossipKnowledgeStructure
k = (Int -> String) -> (Int -> String) -> Int -> Bdd -> Bdd
existsl (Int -> Int -> String
strLabel (Int -> Int -> String) -> Int -> Int -> String
forall a b. (a -> b) -> a -> b
$ GossipKnowledgeStructure -> Int
nag GossipKnowledgeStructure
k) (Int -> Int -> String
texLabel (Int -> Int -> String) -> Int -> Int -> String
forall a b. (a -> b) -> a -> b
$ GossipKnowledgeStructure -> Int
nag GossipKnowledgeStructure
k)

gforallSet :: GossipKnowledgeStructure -> [Int] -> Bdd -> Bdd
gforallSet :: GossipKnowledgeStructure -> [Int] -> Bdd -> Bdd
gforallSet GossipKnowledgeStructure
k = (Int -> String) -> (Int -> String) -> [Int] -> Bdd -> Bdd
forallSetl (Int -> Int -> String
strLabel (Int -> Int -> String) -> Int -> Int -> String
forall a b. (a -> b) -> a -> b
$ GossipKnowledgeStructure -> Int
nag GossipKnowledgeStructure
k) (Int -> Int -> String
texLabel (Int -> Int -> String) -> Int -> Int -> String
forall a b. (a -> b) -> a -> b
$ GossipKnowledgeStructure -> Int
nag GossipKnowledgeStructure
k)

gexistsSet :: GossipKnowledgeStructure -> [Int] -> Bdd -> Bdd
gexistsSet :: GossipKnowledgeStructure -> [Int] -> Bdd -> Bdd
gexistsSet GossipKnowledgeStructure
k = (Int -> String) -> (Int -> String) -> [Int] -> Bdd -> Bdd
existsSetl (Int -> Int -> String
strLabel (Int -> Int -> String) -> Int -> Int -> String
forall a b. (a -> b) -> a -> b
$ GossipKnowledgeStructure -> Int
nag GossipKnowledgeStructure
k) (Int -> Int -> String
texLabel (Int -> Int -> String) -> Int -> Int -> String
forall a b. (a -> b) -> a -> b
$ GossipKnowledgeStructure -> Int
nag GossipKnowledgeStructure
k)

{- 
    Knowledge transformer for gossip 
-}

-- | The Knowledge Transformer data structure, as defined in (Gattinger, 2018).
data KnowledgeTransformer = KT
  { -- | Additional vocabulary.
    KnowledgeTransformer -> Set Int
addVocab :: Set Int,

    -- | The event law.
    KnowledgeTransformer -> Bdd
eventLaw :: Bdd,

    -- | Additional observables.
    KnowledgeTransformer -> Map Agent (Set Int)
addObs :: Map Agent (Set Int)
  }

-- | A base Knowledge Transformer structure, which will not change the Knowledge Structure.
baseTransformer :: KnowledgeTransformer
baseTransformer :: KnowledgeTransformer
baseTransformer = Set Int -> Bdd -> Map Agent (Set Int) -> KnowledgeTransformer
KT Set Int
forall a. Set a
Set.empty Bdd
top Map Agent (Set Int)
forall k a. Map k a
Map.empty

-- | Checks if a Knowledge Transformer is valid. Checks whether all atoms in the additional vocabulary are actually new, whether the event law only uses variables that are contained in either the original vocabulary or the additional vocabulary, and whether the additional observables are items from the additional vocabulary.
validKT :: GossipKnowledgeStructure -> KnowledgeTransformer -> Bool
validKT :: GossipKnowledgeStructure -> KnowledgeTransformer -> Bool
validKT (GKS Set Int
v Bdd
_ Map Agent (Set Int)
o) (KT Set Int
v' Bdd
l' Map Agent (Set Int)
o') =
  let vocabCheck :: Bool
vocabCheck = Set Int -> Set Int -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.disjoint Set Int
v Set Int
v'
      lawCheck :: Bool
lawCheck = [Int] -> Set Int
forall a. Ord a => [a] -> Set a
Set.fromList (Bdd -> [Int]
allVarsOf Bdd
l') Set Int -> Set Int -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`isSubsetOf` (Set Int
v Set Int -> Set Int -> Set Int
forall a. Ord a => Set a -> Set a -> Set a
`union` Set Int
v')
      obsCheck :: Bool
obsCheck = (Set Int -> Bool -> Bool) -> Bool -> Map Agent (Set Int) -> Bool
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr (Bool -> Bool -> Bool
(&&) (Bool -> Bool -> Bool)
-> (Set Int -> Bool) -> Set Int -> Bool -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set Int -> Set Int -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`isSubsetOf` Set Int
v')) Bool
True Map Agent (Set Int)
o'
   in Bool
vocabCheck Bool -> Bool -> Bool
&& Bool
lawCheck Bool -> Bool -> Bool
&& Bool
obsCheck

-- | Updates a Knowledge Structure, given a Knowledge Transformer. 
update :: GossipKnowledgeStructure -> KnowledgeTransformer -> GossipKnowledgeStructure
update :: GossipKnowledgeStructure
-> KnowledgeTransformer -> GossipKnowledgeStructure
update (GKS Set Int
v Bdd
l Map Agent (Set Int)
o) (KT Set Int
v' Bdd
l' Map Agent (Set Int)
o') = GKS :: Set Int -> Bdd -> Map Agent (Set Int) -> GossipKnowledgeStructure
GKS
  { vocabulary :: Set Int
vocabulary = Set Int
v Set Int -> Set Int -> Set Int
forall a. Ord a => Set a -> Set a -> Set a
`union` Set Int
v',
    stateLaw :: Bdd
stateLaw = Bdd
l Bdd -> Bdd -> Bdd
`con` Bdd
l',
    observables :: Map Agent (Set Int)
observables = (Set Int -> Set Int -> Set Int)
-> Map Agent (Set Int)
-> Map Agent (Set Int)
-> Map Agent (Set Int)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
unionWith Set Int -> Set Int -> Set Int
forall a. Ord a => Set a -> Set a -> Set a
union Map Agent (Set Int)
o Map Agent (Set Int)
o'
  }

-- | An infix operator for the `update` function. 
(|+|) :: GossipKnowledgeStructure -> KnowledgeTransformer -> GossipKnowledgeStructure
GossipKnowledgeStructure
f |+| :: GossipKnowledgeStructure
-> KnowledgeTransformer -> GossipKnowledgeStructure
|+| KnowledgeTransformer
x = GossipKnowledgeStructure
-> KnowledgeTransformer -> GossipKnowledgeStructure
update GossipKnowledgeStructure
f KnowledgeTransformer
x
infixl 9 |+|


{- 
    Update schemes for gossip calls
-}

-- | Updates a Knowledge Structure for a given call made between two agents. The integer argument denotes the tick counter. 
updateWithCall :: GossipKnowledgeStructure -> Int -> Call -> GossipKnowledgeStructure
updateWithCall :: GossipKnowledgeStructure
-> Int -> (Agent, Agent) -> GossipKnowledgeStructure
updateWithCall GossipKnowledgeStructure
gks Int
ticks (Agent
a, Agent
b) = GossipKnowledgeStructure
gks GossipKnowledgeStructure
-> KnowledgeTransformer -> GossipKnowledgeStructure
|+| KnowledgeTransformer
transformer
  where
        transformer :: KnowledgeTransformer
transformer = KnowledgeTransformer
baseTransformer
          { addObs :: Map Agent (Set Int)
addObs = (Agent -> Set Int -> Map Agent (Set Int) -> Map Agent (Set Int)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Agent
a Set Int
oa (Map Agent (Set Int) -> Map Agent (Set Int))
-> (Map Agent (Set Int) -> Map Agent (Set Int))
-> Map Agent (Set Int)
-> Map Agent (Set Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Agent -> Set Int -> Map Agent (Set Int) -> Map Agent (Set Int)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Agent
b Set Int
ob) Map Agent (Set Int)
forall k a. Map k a
Map.empty
          --, eventLaw = xorSet $ map conSet allCallCombinations
          }

        agents :: [Agent]
agents = Map Agent (Set Int) -> [Agent]
forall k a. Map k a -> [k]
Map.keys (Map Agent (Set Int) -> [Agent]) -> Map Agent (Set Int) -> [Agent]
forall a b. (a -> b) -> a -> b
$ GossipKnowledgeStructure -> Map Agent (Set Int)
observables GossipKnowledgeStructure
gks
        --combinations = (. List.subsequences) . filter . (. length) . (==)
        --allCallCombinations = combinations ticks [gAtToBdd (nag gks) (GAt C x y) | x <- agents, y <- agents]

        oa :: Set Int
oa = [Int] -> Set Int
forall a. Ord a => [a] -> Set a
Set.fromList ([Int] -> Set Int) -> [Int] -> Set Int
forall a b. (a -> b) -> a -> b
$ (GossipAtom -> Int) -> [GossipAtom] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> GossipAtom -> Int
gAtToInt (Int -> GossipAtom -> Int) -> Int -> GossipAtom -> Int
forall a b. (a -> b) -> a -> b
$ GossipKnowledgeStructure -> Int
nag GossipKnowledgeStructure
gks)
          [ Rel -> Agent -> Agent -> GossipAtom
GAt Rel
C Agent
a Agent
b
          , Rel -> Agent -> Agent -> GossipAtom
GAt Rel
S Agent
a Agent
b
          , Rel -> Agent -> Agent -> GossipAtom
GAt Rel
S Agent
b Agent
a
          , Rel -> Agent -> Agent -> GossipAtom
GAt Rel
N Agent
b Agent
a
          ]

        ob :: Set Int
ob = [Int] -> Set Int
forall a. Ord a => [a] -> Set a
Set.fromList ([Int] -> Set Int) -> [Int] -> Set Int
forall a b. (a -> b) -> a -> b
$ (GossipAtom -> Int) -> [GossipAtom] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> GossipAtom -> Int
gAtToInt (Int -> GossipAtom -> Int) -> Int -> GossipAtom -> Int
forall a b. (a -> b) -> a -> b
$ GossipKnowledgeStructure -> Int
nag GossipKnowledgeStructure
gks)
          [ Rel -> Agent -> Agent -> GossipAtom
GAt Rel
C Agent
a Agent
b
          , Rel -> Agent -> Agent -> GossipAtom
GAt Rel
S Agent
a Agent
b
          , Rel -> Agent -> Agent -> GossipAtom
GAt Rel
S Agent
b Agent
a
          , Rel -> Agent -> Agent -> GossipAtom
GAt Rel
N Agent
a Agent
b
          , Rel -> Agent -> Agent -> GossipAtom
GAt Rel
N Agent
b Agent
a
          ]