{- | This module shows how to use the SMCDEL model checker and the translations with some toy examples.

-}

{-# LANGUAGE FlexibleInstances #-}

module SMCDEL.Examples where

import Data.List ((\\),sort)

import SMCDEL.Explicit.S5
import SMCDEL.Internal.TaggedBDD
import SMCDEL.Language
import SMCDEL.Symbolic.S5
import SMCDEL.Translations.S5

-- * Knowledge and Meta-Knowledge

-- | A Kripke model with two states, where Bob knows that \(p\) is true and Alice does not.
-- Still, Alice knows that Bob knows whether \(p\).
-- This is because in all worlds that Alice confuses with the actual world Bob either knows that \(p\) or he knows that not \(p\).
modelA :: PointedModelS5
modelA :: PointedModelS5
modelA = ([World]
-> [(Agent, Partition)] -> [(World, Assignment)] -> KripkeModelS5
KrMS5 [World
0,World
1] [(Agent
alice,[[World
0,World
1]]),(Agent
bob,[[World
0],[World
1]])] [ (World
0,[(World -> Prp
P World
0,Bool
True)]), (World
1,[(World -> Prp
P World
0,Bool
False)]) ], World
0)

-- | A model with three states.
-- Bob knows that \(p\) is true and Alice does not.
-- Additionally here Alice does not even know whether Bob knows whether \(p\).
modelB :: PointedModelS5
modelB :: PointedModelS5
modelB =
  ([World]
-> [(Agent, Partition)] -> [(World, Assignment)] -> KripkeModelS5
KrMS5
    [World
0,World
1,World
2]
    [(Agent
alice,[[World
0,World
1,World
2]]),(Agent
bob,[[World
0],[World
1,World
2]])]
    [ (World
0,[(World -> Prp
P World
0,Bool
True)]), (World
1,[(World -> Prp
P World
0,Bool
True)]), (World
2,[(World -> Prp
P World
0,Bool
False)]) ]
  , World
0)

-- | The knowledge structure equivalent to `modelA`, obtained using `kripkeToKns`.
knsA :: KnowScene
knsA :: KnowScene
knsA = PointedModelS5 -> KnowScene
kripkeToKns PointedModelS5
modelA

-- | The knowledge structure equivalent to `modelB`, obtained using `kripkeToKns`.
knsB :: KnowScene
knsB :: KnowScene
knsB = PointedModelS5 -> KnowScene
kripkeToKns PointedModelS5
modelB

{- $
The only difference is in the state law of the knowledge structures.
Remember that this component determines which assignments are states of this knowledge structure.
In our implementation this is not a formula but a BDD, hence we show its graph here.
The BDD in `knsA` demands that the propositions \(p\) and \(p_2\) have the same value.
Hence knsA has just two states while `knsB` has three:

>>> let (structA,foo) = knsA in statesOf structA
[[P 0,P 2],[]]

>>> let (structB,foo) = knsB in statesOf structB
[[P 0],[P 0,P 2],[]]

-}

-- * Minimization via Translation

-- | A Kripke model with three states 0,1,2 where 0 and 1 are bisimilar --- it is redundant.
redundantModel :: PointedModelS5
redundantModel :: PointedModelS5
redundantModel = ([World]
-> [(Agent, Partition)] -> [(World, Assignment)] -> KripkeModelS5
KrMS5 [World
0,World
1,World
2] [(Agent
alice,[[World
0,World
1,World
2]]),(Agent
bob,[[World
0,World
1],[World
2]])] [ (World
0,[(World -> Prp
P World
0,Bool
True)]), (World
1,[(World -> Prp
P World
0,Bool
True)]), (World
2,[(World -> Prp
P World
0,Bool
False)]) ], World
0)

-- | The knowledge structure equivalent to `redundantModel`.
myKNS :: KnowScene
myKNS :: KnowScene
myKNS = PointedModelS5 -> KnowScene
kripkeToKns PointedModelS5
redundantModel

minimizedModel :: PointedModelS5
minimizedModel :: PointedModelS5
minimizedModel = KnowScene -> PointedModelS5
knsToKripke KnowScene
myKNS

minimizedKNS :: KnowScene
minimizedKNS :: KnowScene
minimizedKNS = PointedModelS5 -> KnowScene
kripkeToKns PointedModelS5
minimizedModel

-- | A propulation between `myKNS` and `minimizedKNS`.
myPropu :: Propulation
myPropu :: Propulation
myPropu = [Prp] -> Propulation
forall a. TagForBDDs a => [Prp] -> Tagged a Bdd
allsamebdd (KnowScene -> [Prp]
forall a. HasVocab a => a -> [Prp]
vocabOf KnowScene
myKNS)


-- * Different Announcements

-- | Public announcement as an action model.
pubAnnounceAction :: [Agent] -> Form -> PointedActionModelS5
pubAnnounceAction :: [Agent] -> Form -> PointedActionModelS5
pubAnnounceAction [Agent]
ags Form
f = ([(World, (Form, PostCondition))]
-> [(Agent, Partition)] -> ActionModelS5
ActMS5 [(World
0,(Form
f,[]))] [ (Agent
i,[[World
0]]) | Agent
i <- [Agent]
ags ], World
0)

examplePaAction :: PointedActionModelS5
examplePaAction :: PointedActionModelS5
examplePaAction = [Agent] -> Form -> PointedActionModelS5
pubAnnounceAction [Agent
alice,Agent
bob] (Prp -> Form
PrpF (World -> Prp
P World
0))

-- | Group announcement as an action model.
groupAnnounceAction :: [Agent] -> [Agent] -> Form -> PointedActionModelS5
groupAnnounceAction :: [Agent] -> [Agent] -> Form -> PointedActionModelS5
groupAnnounceAction [Agent]
everyone [Agent]
listeners Form
f = ([(World, (Form, PostCondition))]
-> [(Agent, Partition)] -> ActionModelS5
ActMS5 [(World
0,(Form
f,[])),(World
1,(Form -> Form
Neg Form
f,[]))] [(Agent, Partition)]
actrel, World
0)
  where actrel :: [(Agent, Partition)]
actrel = [(Agent, Partition)] -> [(Agent, Partition)]
forall a. Ord a => [a] -> [a]
sort ([(Agent, Partition)] -> [(Agent, Partition)])
-> [(Agent, Partition)] -> [(Agent, Partition)]
forall a b. (a -> b) -> a -> b
$ [ (Agent
i,[[World
0],[World
1]]) | Agent
i <- [Agent]
listeners ]
                     [(Agent, Partition)]
-> [(Agent, Partition)] -> [(Agent, Partition)]
forall a. [a] -> [a] -> [a]
++ [ (Agent
i,[[World
0 , World
1]]) | Agent
i <- [Agent]
everyone [Agent] -> [Agent] -> [Agent]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Agent]
listeners ]

exampleGroupAnnounceAction :: PointedActionModelS5
exampleGroupAnnounceAction :: PointedActionModelS5
exampleGroupAnnounceAction = [Agent] -> [Agent] -> Form -> PointedActionModelS5
groupAnnounceAction [Agent
alice, Agent
bob] [Agent
alice] (Prp -> Form
PrpF (World -> Prp
P World
0))

eGrAnLaw :: Form
exampleGrAnnEvent :: Event
exampleGrAnnEvent :: Event
exampleGrAnnEvent@(KnTrf [Prp]
_ Form
eGrAnLaw [(Prp, Bdd)]
_ [(Agent, [Prp])]
_, [Prp]
_) = PointedActionModelS5 -> Event
actionToEvent PointedActionModelS5
exampleGroupAnnounceAction

-- * Equivalent Action Models

-- | An action model.
actionOne :: PointedActionModelS5
actionOne :: PointedActionModelS5
actionOne = ([(World, (Form, PostCondition))]
-> [(Agent, Partition)] -> ActionModelS5
ActMS5 [(World
0,(Form
p,[])),(World
1, ([Form] -> Form
Disj [Form
q, Form -> Form
Neg Form
q],[]))] [(Agent
"Alice",[[World
0],[World
1]]), (Agent
"Bob",[[World
0,World
1]])], World
0) where (Form
p,Form
q) = (Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ World -> Prp
P World
0, Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ World -> Prp
P World
1)

-- | Another action model which has bisimilar (in fact identical!) effects as `actionOne` on any Kripke model.
actionTwo :: PointedActionModelS5
actionTwo :: PointedActionModelS5
actionTwo = ([(World, (Form, PostCondition))]
-> [(Agent, Partition)] -> ActionModelS5
ActMS5 [(World
0,(Form
p,[])),(World
1,(Form
q,[])),(World
2,(Form -> Form
Neg Form
q,[]))] [(Agent
"Alice",[[World
0],[World
1,World
2]]), (Agent
"Bob",[[World
0,World
1,World
2]]) ], World
0) where (Form
p,Form
q) = (Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ World -> Prp
P World
0, Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ World -> Prp
P World
1)