{-# OPTIONS_GHC -Wno-overlapping-patterns #-}
{-|
Module      : GossipState
Description : Implements the Gossip state, a slice in time denoting the state of a gossip graph and knowledge structure.
Copyright   : (c) Jesper Kuiper, 2021
                  Leander van Boven, 2021
                  Ramon Meffert, 2021
License     : BSD3
-}
module GossipState 
  ( -- * State type
    State ( State, stateGraph, stateKnowledgeStruct, stateCallSeq )
  , printState
  -- * Call validation and execution
  , validCalls
  , makeCall
  , executeCalls
  -- * Epistemic formula evaluation
  , evaluateGossipAtom
  , evaluateBddVar
  , evaluate
  , (|=)
  -- * Legacy
  , evaluate'
  )
where

import Data.Graph.Inductive
import Data.Graph.Inductive.Graph
--import Data.HasCacBDD hiding ( evaluate, Top )
import Data.Map.Strict ( (!) )
import Data.Set ( (\\) )
import System.Console.ANSI

import GossipGraph
import GossipKnowledge
import GossipTypes
import PrintableBdd hiding ( evaluate )

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

-- | The gossip state. 
data State = State {
  -- | The gossip graph of the current state.
  State -> GossipGraph
stateGraph :: GossipGraph,

  -- | The knowledge structure of the current state.
  State -> GossipKnowledgeStructure
stateKnowledgeStruct :: GossipKnowledgeStructure,

  -- | The call sequence of the current state. 
  State -> [Call]
stateCallSeq :: [Call]
}

-- | Prints the current state. 
printState :: State -> Bool -> IO ()
printState :: State -> Bool -> IO ()
printState (State GossipGraph
g GossipKnowledgeStructure
k [Call]
c) Bool
n = do
  [SGR] -> IO ()
setSGR [ConsoleLayer -> ColorIntensity -> Color -> SGR
SetColor ConsoleLayer
Foreground ColorIntensity
Vivid Color
Magenta]
  if Bool
n
    then String -> IO ()
putStrLn String
"\n=== UPDATED STATE ==="
    else String -> IO ()
putStrLn String
"\n=== CURRENT STATE ==="
  [SGR] -> IO ()
setSGR [ConsoleLayer -> ColorIntensity -> Color -> SGR
SetColor ConsoleLayer
Foreground ColorIntensity
Vivid Color
Cyan]
  String -> IO ()
putStrLn String
"= GossipGraph ="
  [SGR] -> IO ()
setSGR [SGR
Reset]
  GossipGraph -> IO ()
printGraph GossipGraph
g
  [SGR] -> IO ()
setSGR [ConsoleLayer -> ColorIntensity -> Color -> SGR
SetColor ConsoleLayer
Foreground ColorIntensity
Vivid Color
Cyan]
  String -> IO ()
putStrLn String
"\n= Knowledgestructure ="
  [SGR] -> IO ()
setSGR [SGR
Reset]
  GossipKnowledgeStructure -> IO ()
forall a. Show a => a -> IO ()
print GossipKnowledgeStructure
k
  [SGR] -> IO ()
setSGR [ConsoleLayer -> ColorIntensity -> Color -> SGR
SetColor ConsoleLayer
Foreground ColorIntensity
Vivid Color
Cyan]
  String -> IO ()
putStrLn String
"\n= Callsequence ="
  [SGR] -> IO ()
setSGR [SGR
Reset]
  [Call] -> IO ()
printCalls [Call]
c
  [SGR] -> IO ()
setSGR [ConsoleLayer -> ColorIntensity -> Color -> SGR
SetColor ConsoleLayer
Foreground ColorIntensity
Vivid Color
Magenta]
  String -> IO ()
putStrLn String
"\n====================="
  [SGR] -> IO ()
setSGR [SGR
Reset]

-- | Determines based on the current GossipGraph state which calls are actually allowed to be made. Note that no protocols are used for this, a call between a and b is valid iff a knows the number of b. 
validCalls :: GossipGraph -> ([Call], [GroupCall])
validCalls :: GossipGraph -> ([Call], [GroupCall])
validCalls GossipGraph
g = ([Call]
validDirectCalls, [GroupCall]
validGroupCalls)
  where
    validDirectCalls :: [Call]
    validDirectCalls :: [Call]
validDirectCalls = [ LNode AgentName
f LNode AgentName -> LNode AgentName -> Call
☎ LNode AgentName
t | f :: LNode AgentName
f@(Node
i, AgentName
_) <- GossipGraph -> [LNode AgentName]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes GossipGraph
g, t :: LNode AgentName
t@(Node
j, AgentName
_) <- GossipGraph -> [LNode AgentName]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes GossipGraph
g, Node
i Node -> Node -> Bool
forall a. Eq a => a -> a -> Bool
/= Node
j, GossipGraph -> LEdge Kind -> Bool
forall (gr :: * -> * -> *) b a.
(Graph gr, Eq b) =>
gr a b -> LEdge b -> Bool
hasLEdge GossipGraph
g (Node
i, Node
j, Kind
Number)]

    validGroupCalls :: [GroupCall]
    validGroupCalls :: [GroupCall]
validGroupCalls = [(LNode AgentName
f, LNode AgentName -> [LNode AgentName]
tos LNode AgentName
f) | f :: LNode AgentName
f@(Node
i, AgentName
_) <- GossipGraph -> [LNode AgentName]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes GossipGraph
g]

    tos :: Agent -> [Agent]
    tos :: LNode AgentName -> [LNode AgentName]
tos f :: LNode AgentName
f@(Node
i, AgentName
_) = [LNode AgentName
t | t :: LNode AgentName
t@(Node
j, AgentName
_) <- GossipGraph -> [LNode AgentName]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes GossipGraph
g, LNode AgentName
f LNode AgentName -> LNode AgentName -> Bool
forall a. Eq a => a -> a -> Bool
/= LNode AgentName
t, GossipGraph -> LEdge Kind -> Bool
forall (gr :: * -> * -> *) b a.
(Graph gr, Eq b) =>
gr a b -> LEdge b -> Bool
hasLEdge GossipGraph
g (Node
i,Node
j,Kind
Number)]

-- | Makes multiple calls by repeatedly invoking `makeCall`. 
executeCalls :: [Call] -> State -> IO State
executeCalls :: [Call] -> State -> IO State
executeCalls [] State
s = State -> IO State
forall (m :: * -> *) a. Monad m => a -> m a
return State
s
executeCalls (Call
c:[Call]
cs) State
s = do
  Call -> IO ()
printMakeCall Call
c
  let newState :: State
newState = Call -> State -> State
makeCall Call
c State
s
  State -> Bool -> IO ()
printState State
newState Bool
True
  [Call] -> State -> IO State
executeCalls [Call]
cs State
newState

-- | Makes a call and update the state. 
makeCall :: Call -> State -> State
makeCall :: Call -> State -> State
makeCall Call
c s :: State
s@(State GossipGraph
g GossipKnowledgeStructure
k [Call]
cs) =
  State -> [LEdge Kind] -> State
newState State
s ([LEdge Kind] -> State) -> [LEdge Kind] -> State
forall a b. (a -> b) -> a -> b
$ ((LEdge Kind -> Bool) -> [LEdge Kind] -> [LEdge Kind])
-> [LEdge Kind] -> (LEdge Kind -> Bool) -> [LEdge Kind]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (LEdge Kind -> Bool) -> [LEdge Kind] -> [LEdge Kind]
forall a. (a -> Bool) -> [a] -> [a]
filter (Call -> [LEdge Kind]
allEdges Call
c) ((LEdge Kind -> Bool) -> [LEdge Kind])
-> (LEdge Kind -> Bool) -> [LEdge Kind]
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> (LEdge Kind -> Bool) -> LEdge Kind -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GossipGraph -> LEdge Kind -> Bool
forall (gr :: * -> * -> *) b a.
(Graph gr, Eq b) =>
gr a b -> LEdge b -> Bool
hasLEdge GossipGraph
g
  where
    allEdges :: Call -> [Relation]
    allEdges :: Call -> [LEdge Kind]
allEdges ((Node
a, AgentName
_), (Node
b, AgentName
_)) =
      -- (a,x,Number) forall x s.t. N(b,x)
      [(Node
a, Node
x, Kind
Number) | (Node
x, AgentName
_) <- GossipGraph -> [LNode AgentName]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes GossipGraph
g, GossipGraph -> LEdge Kind -> Bool
forall (gr :: * -> * -> *) b a.
(Graph gr, Eq b) =>
gr a b -> LEdge b -> Bool
hasLEdge GossipGraph
g (Node
b, Node
x, Kind
Number)]
      [LEdge Kind] -> [LEdge Kind] -> [LEdge Kind]
forall a. [a] -> [a] -> [a]
++
      -- (a,x,Secret) forall x s.t. S(b,x)
      [(Node
a, Node
x, Kind
Secret) | (Node
x, AgentName
_) <- GossipGraph -> [LNode AgentName]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes GossipGraph
g, GossipGraph -> LEdge Kind -> Bool
forall (gr :: * -> * -> *) b a.
(Graph gr, Eq b) =>
gr a b -> LEdge b -> Bool
hasLEdge GossipGraph
g (Node
b, Node
x, Kind
Secret)]
      [LEdge Kind] -> [LEdge Kind] -> [LEdge Kind]
forall a. [a] -> [a] -> [a]
++
      -- (b,x,Number) forall x s.t. N(a,x)
      [(Node
b, Node
x, Kind
Number) | (Node
x, AgentName
_) <- GossipGraph -> [LNode AgentName]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes GossipGraph
g, GossipGraph -> LEdge Kind -> Bool
forall (gr :: * -> * -> *) b a.
(Graph gr, Eq b) =>
gr a b -> LEdge b -> Bool
hasLEdge GossipGraph
g (Node
a, Node
x, Kind
Number)]
      [LEdge Kind] -> [LEdge Kind] -> [LEdge Kind]
forall a. [a] -> [a] -> [a]
++
      -- (b,x,Secret) forall x s.t. S(a,x)
      [(Node
b, Node
x, Kind
Secret) | (Node
x, AgentName
_) <- GossipGraph -> [LNode AgentName]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes GossipGraph
g, GossipGraph -> LEdge Kind -> Bool
forall (gr :: * -> * -> *) b a.
(Graph gr, Eq b) =>
gr a b -> LEdge b -> Bool
hasLEdge GossipGraph
g (Node
a, Node
x, Kind
Secret)]

    newState :: State -> [Relation] -> State
    newState :: State -> [LEdge Kind] -> State
newState (State GossipGraph
g GossipKnowledgeStructure
k [Call]
cs) [LEdge Kind]
newEdges = GossipGraph -> GossipKnowledgeStructure -> [Call] -> State
State
      ([LEdge Kind] -> GossipGraph -> GossipGraph
forall (gr :: * -> * -> *) b a.
DynGraph gr =>
[LEdge b] -> gr a b -> gr a b
insEdges [LEdge Kind]
newEdges GossipGraph
g)
      (GossipKnowledgeStructure
-> Node -> Call -> GossipKnowledgeStructure
updateWithCall GossipKnowledgeStructure
k ([Call] -> Node
forall (t :: * -> *) a. Foldable t => t a -> Node
length [Call]
cs Node -> Node -> Node
forall a. Num a => a -> a -> a
+ Node
1) Call
c)
      ([Call]
cs [Call] -> [Call] -> [Call]
forall a. [a] -> [a] -> [a]
++ [Call
c])

-- | Evaluates a gossip atom (N(x,y), S(x,y) or C(x,y)), given the current state
evaluateGossipAtom :: State -> GossipAtom -> Bool
evaluateGossipAtom :: State -> GossipAtom -> Bool
evaluateGossipAtom (State GossipGraph
g GossipKnowledgeStructure
_ [Call]
_) (GAt Rel
N LNode AgentName
x LNode AgentName
y) = GossipGraph -> LNode AgentName -> Kind -> LNode AgentName -> Bool
hasRelationWith GossipGraph
g LNode AgentName
x Kind
Number LNode AgentName
y
evaluateGossipAtom (State GossipGraph
g GossipKnowledgeStructure
_ [Call]
_) (GAt Rel
S LNode AgentName
x LNode AgentName
y) = GossipGraph -> LNode AgentName -> Kind -> LNode AgentName -> Bool
hasRelationWith GossipGraph
g LNode AgentName
x Kind
Secret LNode AgentName
y
evaluateGossipAtom (State GossipGraph
_ GossipKnowledgeStructure
_ [Call]
s) (GAt Rel
C LNode AgentName
x LNode AgentName
y) = (LNode AgentName
x, LNode AgentName
y) Call -> [Call] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Call]
s

-- | Evaluates a Bdd variable as Int, given the current state
evaluateBddVar :: State -> Int -> Bool
evaluateBddVar :: State -> Node -> Bool
evaluateBddVar s :: State
s@(State GossipGraph
g GossipKnowledgeStructure
_ [Call]
_) = State -> GossipAtom -> Bool
evaluateGossipAtom State
s (GossipAtom -> Bool) -> (Node -> GossipAtom) -> Node -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Node -> Node -> GossipAtom
intToGAt (GossipGraph -> Node
noAgents GossipGraph
g)

-- | Evaluates an epistemic formula, given the current state
evaluate :: State -> Form -> Bool
evaluate :: State -> Form -> Bool
evaluate state :: State
state@(State GossipGraph
_ GossipKnowledgeStructure
k [Call]
_) Form
ϕ = Bdd -> (Node -> Bool) -> Bool
evaluateFun (GossipKnowledgeStructure
k GossipKnowledgeStructure -> Form -> Bdd
<|> Form
ϕ) (State -> Node -> Bool
evaluateBddVar State
state)

-- | An infix operator of the `evaluate` function. 
(|=) :: State -> Form -> Bool
State
state |= :: State -> Form -> Bool
|= Form
form = State -> Form -> Bool
evaluate State
state Form
form
infix 9 |=

-- | Legacy method, evalute a GossipFormula (note, without knowledge) by naive recursion
evaluate' :: State -> GossipForm -> Bool
evaluate' :: State -> GossipForm -> Bool
evaluate' State
_ GossipForm
Top                            = Bool
True
evaluate' (State GossipGraph
g GossipKnowledgeStructure
_ [Call]
_) (Atom (GAt Rel
N LNode AgentName
x LNode AgentName
y)) = GossipGraph -> LNode AgentName -> Kind -> LNode AgentName -> Bool
hasRelationWith GossipGraph
g LNode AgentName
x Kind
Number LNode AgentName
y
evaluate' (State GossipGraph
g GossipKnowledgeStructure
_ [Call]
_) (Atom (GAt Rel
S LNode AgentName
x LNode AgentName
y)) = GossipGraph -> LNode AgentName -> Kind -> LNode AgentName -> Bool
hasRelationWith GossipGraph
g LNode AgentName
x Kind
Secret LNode AgentName
y
evaluate' (State GossipGraph
_ GossipKnowledgeStructure
_ [Call]
s) (Atom (GAt Rel
C LNode AgentName
x LNode AgentName
y)) = (LNode AgentName
x, LNode AgentName
y) Call -> [Call] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Call]
s
evaluate' State
s (Neg GossipForm
form)                     = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ State -> GossipForm -> Bool
evaluate' State
s GossipForm
form
evaluate' State
s (Conj (GossipForm
form:[GossipForm]
rest))             = State -> GossipForm -> Bool
evaluate' State
s GossipForm
form Bool -> Bool -> Bool
&& State -> GossipForm -> Bool
evaluate' State
s ([GossipForm] -> GossipForm
Conj [GossipForm]
rest)
evaluate' State
s (Disj (GossipForm
form:[GossipForm]
rest))             = State -> GossipForm -> Bool
evaluate' State
s GossipForm
form Bool -> Bool -> Bool
|| State -> GossipForm -> Bool
evaluate' State
s ([GossipForm] -> GossipForm
Disj [GossipForm]
rest)
evaluate' State
s (Impl GossipForm
prem GossipForm
conc)               = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ State -> GossipForm -> Bool
evaluate' State
s GossipForm
prem Bool -> Bool -> Bool
|| State -> GossipForm -> Bool
evaluate' State
s GossipForm
conc