{-|
Module      : GossipProtocol
Description : Implements different kinds of (epistemic) protocols for dynamic gossip.
Copyright   : (c) Jesper Kuiper, 2021
                  Leander van Boven, 2021
                  Ramon Meffert, 2021
License     : BSD3
-}
module GossipProtocol 
  ( -- * Protocol type
    GossipProtocol
  , showProtocol
    -- * Different protocols
  , callAny
  , learnNewSecrets
  , possibleInformationGrowth
    -- * Protocol evaluation
  , selectedCalls 
  )

where

import Data.Map (keys, (!))
import Data.Maybe
import Data.Set ((\\), toList)
import System.Console.ANSI

import GossipKnowledge
import GossipGraph
import GossipState
import GossipTypes
import PrintableBdd


-- | A protocol for dynamic gossip. Following (van Ditmarsch et al., 2017), a gossip protocol is defined as an epistemic formula using two agents. If this formula resolves to true, a call between these agents is allowed. If the formula resolves to false, such a call is not allowed. The first argument denotes the amount of agents, the second argument is the current knowledge structure, whereas the third argument denotes the call in question. 
type GossipProtocol = Int -> GossipKnowledgeStructure -> Call -> Form

-- | Converts a protocol to a string notation, as used in (van Ditmarsch et al., 2017). 
showProtocol :: State -> GossipProtocol -> String
showProtocol :: State -> GossipProtocol -> String
showProtocol (State GossipGraph
g GossipKnowledgeStructure
k [Call]
s) GossipProtocol
prot = String
"φ(x,y) = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Form -> String
forall a. Show a => a -> String
show (GossipProtocol
prot Int
26 GossipKnowledgeStructure
k (Char -> Agent
agentFromLab Char
'x',  Char -> Agent
agentFromLab Char
'y')) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ∀x,y"

-- | The most simple and naive protocol, it allows any call to be made. φ(a,b) = ⊤
callAny :: GossipProtocol
callAny :: GossipProtocol
callAny Int
_ GossipKnowledgeStructure
_ Call
_ = Bdd -> Form
Fact Bdd
top

-- | This protocol only allows a call if it leads to new secrets to be learned. φ(a,b) = ¬S(a,b)
learnNewSecrets :: GossipProtocol
learnNewSecrets :: GossipProtocol
learnNewSecrets Int
n GossipKnowledgeStructure
_ (Agent
x, Agent
y) = Bdd -> Form
Fact (Bdd -> Form) -> Bdd -> Form
forall a b. (a -> b) -> a -> b
$ Bdd -> Bdd
neg (Bdd -> Bdd) -> Bdd -> Bdd
forall a b. (a -> b) -> a -> b
$ Int -> GossipAtom -> Bdd
gAtToBdd Int
n (GossipAtom -> Bdd) -> GossipAtom -> Bdd
forall a b. (a -> b) -> a -> b
$ Rel -> Agent -> Agent -> GossipAtom
GAt Rel
S Agent
x Agent
y

-- | Introduced by (van Ditmarsch et al., 2017): "Call xy can be made if x knows y's number and if x considers it possible that there is a secret known by one of x,y but not the other." φ(a,b) = ⋁_{z ∈ A}( S(x, z) ↔︎ ¬S(y, z) )
possibleInformationGrowth :: GossipProtocol
possibleInformationGrowth :: GossipProtocol
possibleInformationGrowth Int
n (GKS Set Int
v Bdd
t Map Agent (Set Int)
o) (Agent
x, Agent
y) = Agent -> Form -> Form
M Agent
x (Bdd -> Form
Fact Bdd
fullCond)
    where
        allAgents :: [Agent]
allAgents = Map Agent (Set Int) -> [Agent]
forall k a. Map k a -> [k]
keys Map Agent (Set Int)
o
        -- | S(x, z)
        c1 :: Agent -> Bdd
c1 Agent
z = Int -> GossipAtom -> Bdd
gAtToBdd Int
n (GossipAtom -> Bdd) -> GossipAtom -> Bdd
forall a b. (a -> b) -> a -> b
$ Rel -> Agent -> Agent -> GossipAtom
GAt Rel
S Agent
x Agent
z
        -- | ¬S(y, z)
        c2 :: Agent -> Bdd
c2 Agent
z = Bdd -> Bdd
neg (Bdd -> Bdd) -> Bdd -> Bdd
forall a b. (a -> b) -> a -> b
$ Int -> GossipAtom -> Bdd
gAtToBdd Int
n (GossipAtom -> Bdd) -> GossipAtom -> Bdd
forall a b. (a -> b) -> a -> b
$ Rel -> Agent -> Agent -> GossipAtom
GAt Rel
S Agent
y Agent
z
        -- | S(x, z) ↔︎ ¬S(y, z)
        cond :: Agent -> Bdd
cond Agent
z = Agent -> Bdd
c1 Agent
z Bdd -> Bdd -> Bdd
`equ` Agent -> Bdd
c2 Agent
z
        -- | θ → ⋁_{z \in A}( S(x, z) ↔︎ ¬S(y, z) )
        fullCond :: Bdd
fullCond = [Bdd] -> Bdd
disSet ([Bdd] -> Bdd) -> [Bdd] -> Bdd
forall a b. (a -> b) -> a -> b
$ (Agent -> Bdd) -> [Agent] -> [Bdd]
forall a b. (a -> b) -> [a] -> [b]
map Agent -> Bdd
cond [Agent]
allAgents

-- | Selects all calls that are allowed by the given gossip protocol. Note that there could also be no calls allowed. 
selectedCalls :: GossipProtocol -> State -> ([Call], [GroupCall])
selectedCalls :: GossipProtocol -> State -> ([Call], [GroupCall])
selectedCalls GossipProtocol
prot s :: State
s@(State GossipGraph
g GossipKnowledgeStructure
k [Call]
c) =
  let valid :: ([Call], [GroupCall])
valid = GossipGraph -> ([Call], [GroupCall])
validCalls GossipGraph
g
      direct :: [Call]
direct = (Call -> Bool) -> [Call] -> [Call]
forall a. (a -> Bool) -> [a] -> [a]
filter Call -> Bool
isSelected ([Call] -> [Call]) -> [Call] -> [Call]
forall a b. (a -> b) -> a -> b
$ ([Call], [GroupCall]) -> [Call]
forall a b. (a, b) -> a
fst ([Call], [GroupCall])
valid
      group :: [GroupCall]
group = (GroupCall -> Bool) -> [GroupCall] -> [GroupCall]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ GroupCall
g -> GroupCall -> Bool
isGroupCallSelected GroupCall
g Bool -> Bool -> Bool
&& GroupCall -> Bool
isActualGroup GroupCall
g) (([Call], [GroupCall]) -> [GroupCall]
forall a b. (a, b) -> b
snd ([Call], [GroupCall])
valid)
  in ([Call]
direct, [GroupCall]
group)
  where
    isSelected :: Call -> Bool
    isSelected :: Call -> Bool
isSelected Call
c = State
s State -> Form -> Bool
|= GossipProtocol
prot (GossipGraph -> Int
noAgents GossipGraph
g) GossipKnowledgeStructure
k Call
c

    isGroupCallSelected :: GroupCall -> Bool
    isGroupCallSelected :: GroupCall -> Bool
isGroupCallSelected GroupCall
g = (Call -> Bool) -> [Call] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Call -> Bool
isSelected ([Call] -> Bool) -> [Call] -> Bool
forall a b. (a -> b) -> a -> b
$ GroupCall -> [Call]
toCalls GroupCall
g

    isActualGroup :: GroupCall -> Bool
    isActualGroup :: GroupCall -> Bool
isActualGroup (Agent
_, []) = Bool
False
    isActualGroup (Agent
_, Agent
h:[Agent]
t) = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Agent] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Agent]
t