{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses #-}

module SMCDEL.Explicit.K where

import Control.Arrow ((&&&),second)
import Data.Containers.ListUtils (nubInt,nubOrd)
import Data.Dynamic
import Data.List (sort,(\\),delete,intercalate,intersect)
import qualified Data.Map.Strict as M
import Data.Map.Strict ((!))
import Data.Maybe (isJust,isNothing,fromJust)
import Test.QuickCheck

import SMCDEL.Language
import SMCDEL.Explicit.S5 (Action,Bisimulation,HasWorlds,World,worldsOf)
import SMCDEL.Internal.Help (alleqWith,lfp)
import SMCDEL.Internal.TexDisplay

newtype KripkeModel = KrM (M.Map World (M.Map Prp Bool, M.Map Agent [World]))
  deriving (KripkeModel -> KripkeModel -> Bool
(KripkeModel -> KripkeModel -> Bool)
-> (KripkeModel -> KripkeModel -> Bool) -> Eq KripkeModel
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: KripkeModel -> KripkeModel -> Bool
== :: KripkeModel -> KripkeModel -> Bool
$c/= :: KripkeModel -> KripkeModel -> Bool
/= :: KripkeModel -> KripkeModel -> Bool
Eq,Eq KripkeModel
Eq KripkeModel =>
(KripkeModel -> KripkeModel -> Ordering)
-> (KripkeModel -> KripkeModel -> Bool)
-> (KripkeModel -> KripkeModel -> Bool)
-> (KripkeModel -> KripkeModel -> Bool)
-> (KripkeModel -> KripkeModel -> Bool)
-> (KripkeModel -> KripkeModel -> KripkeModel)
-> (KripkeModel -> KripkeModel -> KripkeModel)
-> Ord KripkeModel
KripkeModel -> KripkeModel -> Bool
KripkeModel -> KripkeModel -> Ordering
KripkeModel -> KripkeModel -> KripkeModel
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
$ccompare :: KripkeModel -> KripkeModel -> Ordering
compare :: KripkeModel -> KripkeModel -> Ordering
$c< :: KripkeModel -> KripkeModel -> Bool
< :: KripkeModel -> KripkeModel -> Bool
$c<= :: KripkeModel -> KripkeModel -> Bool
<= :: KripkeModel -> KripkeModel -> Bool
$c> :: KripkeModel -> KripkeModel -> Bool
> :: KripkeModel -> KripkeModel -> Bool
$c>= :: KripkeModel -> KripkeModel -> Bool
>= :: KripkeModel -> KripkeModel -> Bool
$cmax :: KripkeModel -> KripkeModel -> KripkeModel
max :: KripkeModel -> KripkeModel -> KripkeModel
$cmin :: KripkeModel -> KripkeModel -> KripkeModel
min :: KripkeModel -> KripkeModel -> KripkeModel
Ord,World -> KripkeModel -> ShowS
[KripkeModel] -> ShowS
KripkeModel -> Agent
(World -> KripkeModel -> ShowS)
-> (KripkeModel -> Agent)
-> ([KripkeModel] -> ShowS)
-> Show KripkeModel
forall a.
(World -> a -> ShowS) -> (a -> Agent) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: World -> KripkeModel -> ShowS
showsPrec :: World -> KripkeModel -> ShowS
$cshow :: KripkeModel -> Agent
show :: KripkeModel -> Agent
$cshowList :: [KripkeModel] -> ShowS
showList :: [KripkeModel] -> ShowS
Show)

instance Pointed KripkeModel World
type PointedModel = (KripkeModel, World)

instance Pointed KripkeModel [World]
type MultipointedModel = (KripkeModel,[World])

distinctVal :: KripkeModel -> Bool
distinctVal :: KripkeModel -> Bool
distinctVal (KrM Map World (Map Prp Bool, Map Agent [World])
m) = Map World (Map Prp Bool, Map Agent [World]) -> World
forall k a. Map k a -> World
M.size Map World (Map Prp Bool, Map Agent [World])
m World -> World -> Bool
forall a. Eq a => a -> a -> Bool
== [Map Prp Bool] -> World
forall a. [a] -> World
forall (t :: * -> *) a. Foldable t => t a -> World
length ([Map Prp Bool] -> [Map Prp Bool]
forall a. Ord a => [a] -> [a]
nubOrd (((Map Prp Bool, Map Agent [World]) -> Map Prp Bool)
-> [(Map Prp Bool, Map Agent [World])] -> [Map Prp Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Map Prp Bool, Map Agent [World]) -> Map Prp Bool
forall a b. (a, b) -> a
fst (Map World (Map Prp Bool, Map Agent [World])
-> [(Map Prp Bool, Map Agent [World])]
forall k a. Map k a -> [a]
M.elems Map World (Map Prp Bool, Map Agent [World])
m)))

instance HasWorlds KripkeModel where
  worldsOf :: KripkeModel -> [World]
worldsOf (KrM Map World (Map Prp Bool, Map Agent [World])
m) = Map World (Map Prp Bool, Map Agent [World]) -> [World]
forall k a. Map k a -> [k]
M.keys Map World (Map Prp Bool, Map Agent [World])
m

instance HasVocab KripkeModel where
  vocabOf :: KripkeModel -> [Prp]
vocabOf (KrM Map World (Map Prp Bool, Map Agent [World])
m) = Map Prp Bool -> [Prp]
forall k a. Map k a -> [k]
M.keys (Map Prp Bool -> [Prp]) -> Map Prp Bool -> [Prp]
forall a b. (a -> b) -> a -> b
$ (Map Prp Bool, Map Agent [World]) -> Map Prp Bool
forall a b. (a, b) -> a
fst ([(Map Prp Bool, Map Agent [World])]
-> (Map Prp Bool, Map Agent [World])
forall a. HasCallStack => [a] -> a
head (Map World (Map Prp Bool, Map Agent [World])
-> [(Map Prp Bool, Map Agent [World])]
forall k a. Map k a -> [a]
M.elems Map World (Map Prp Bool, Map Agent [World])
m))

instance HasAgents KripkeModel where
  agentsOf :: KripkeModel -> [Agent]
agentsOf (KrM Map World (Map Prp Bool, Map Agent [World])
m) = Map Agent [World] -> [Agent]
forall k a. Map k a -> [k]
M.keys (Map Agent [World] -> [Agent]) -> Map Agent [World] -> [Agent]
forall a b. (a -> b) -> a -> b
$ (Map Prp Bool, Map Agent [World]) -> Map Agent [World]
forall a b. (a, b) -> b
snd ([(Map Prp Bool, Map Agent [World])]
-> (Map Prp Bool, Map Agent [World])
forall a. HasCallStack => [a] -> a
head (Map World (Map Prp Bool, Map Agent [World])
-> [(Map Prp Bool, Map Agent [World])]
forall k a. Map k a -> [a]
M.elems Map World (Map Prp Bool, Map Agent [World])
m))

relOfIn :: Agent -> KripkeModel -> M.Map World [World]
relOfIn :: Agent -> KripkeModel -> Map World [World]
relOfIn Agent
i (KrM Map World (Map Prp Bool, Map Agent [World])
m) = ((Map Prp Bool, Map Agent [World]) -> [World])
-> Map World (Map Prp Bool, Map Agent [World]) -> Map World [World]
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (\(Map Prp Bool, Map Agent [World])
x -> (Map Prp Bool, Map Agent [World]) -> Map Agent [World]
forall a b. (a, b) -> b
snd (Map Prp Bool, Map Agent [World])
x Map Agent [World] -> Agent -> [World]
forall k a. Ord k => Map k a -> k -> a
! Agent
i) Map World (Map Prp Bool, Map Agent [World])
m

truthsInAt :: KripkeModel -> World -> [Prp]
truthsInAt :: KripkeModel -> World -> [Prp]
truthsInAt (KrM Map World (Map Prp Bool, Map Agent [World])
m) World
w = Map Prp Bool -> [Prp]
forall k a. Map k a -> [k]
M.keys ((Bool -> Bool) -> Map Prp Bool -> Map Prp Bool
forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter Bool -> Bool
forall a. a -> a
id ((Map Prp Bool, Map Agent [World]) -> Map Prp Bool
forall a b. (a, b) -> a
fst (Map World (Map Prp Bool, Map Agent [World])
m Map World (Map Prp Bool, Map Agent [World])
-> World -> (Map Prp Bool, Map Agent [World])
forall k a. Ord k => Map k a -> k -> a
! World
w)))

instance KripkeLike KripkeModel where
  directed :: KripkeModel -> Bool
directed = Bool -> KripkeModel -> Bool
forall a b. a -> b -> a
const Bool
True
  getNodes :: KripkeModel -> [(Agent, Agent)]
getNodes KripkeModel
m = (World -> (Agent, Agent)) -> [World] -> [(Agent, Agent)]
forall a b. (a -> b) -> [a] -> [b]
map (World -> Agent
forall a. Show a => a -> Agent
show (World -> Agent) -> (World -> World) -> World -> Agent
forall b c a. (b -> c) -> (a -> b) -> a -> c
. World -> World
forall a. Enum a => a -> World
fromEnum (World -> Agent) -> (World -> Agent) -> World -> (Agent, Agent)
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& World -> Agent
labelOf) (KripkeModel -> [World]
forall a. HasWorlds a => a -> [World]
worldsOf KripkeModel
m) where
    labelOf :: World -> Agent
labelOf World
w = Agent
"$" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ [Prp] -> Agent
forall a. TexAble a => a -> Agent
tex (KripkeModel -> World -> [Prp]
truthsInAt KripkeModel
m World
w) Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
"$"
  getEdges :: KripkeModel -> [(Agent, Agent, Agent)]
getEdges KripkeModel
m =
    [[(Agent, Agent, Agent)]] -> [(Agent, Agent, Agent)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [ (Agent
a, World -> Agent
forall a. Show a => a -> Agent
show (World -> Agent) -> World -> Agent
forall a b. (a -> b) -> a -> b
$ World -> World
forall a. Enum a => a -> World
fromEnum World
w, World -> Agent
forall a. Show a => a -> Agent
show (World -> Agent) -> World -> Agent
forall a b. (a -> b) -> a -> b
$ World -> World
forall a. Enum a => a -> World
fromEnum World
v) | World
v <- Agent -> KripkeModel -> Map World [World]
relOfIn Agent
a KripkeModel
m Map World [World] -> World -> [World]
forall k a. Ord k => Map k a -> k -> a
! World
w ] | World
w <- KripkeModel -> [World]
forall a. HasWorlds a => a -> [World]
worldsOf KripkeModel
m, Agent
a <- KripkeModel -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf KripkeModel
m ]
  getActuals :: KripkeModel -> [Agent]
getActuals = [Agent] -> KripkeModel -> [Agent]
forall a b. a -> b -> a
const []

instance KripkeLike PointedModel where
  directed :: PointedModel -> Bool
directed = KripkeModel -> Bool
forall a. KripkeLike a => a -> Bool
directed (KripkeModel -> Bool)
-> (PointedModel -> KripkeModel) -> PointedModel -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PointedModel -> KripkeModel
forall a b. (a, b) -> a
fst
  getNodes :: PointedModel -> [(Agent, Agent)]
getNodes = KripkeModel -> [(Agent, Agent)]
forall a. KripkeLike a => a -> [(Agent, Agent)]
getNodes (KripkeModel -> [(Agent, Agent)])
-> (PointedModel -> KripkeModel)
-> PointedModel
-> [(Agent, Agent)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PointedModel -> KripkeModel
forall a b. (a, b) -> a
fst
  getEdges :: PointedModel -> [(Agent, Agent, Agent)]
getEdges = KripkeModel -> [(Agent, Agent, Agent)]
forall a. KripkeLike a => a -> [(Agent, Agent, Agent)]
getEdges (KripkeModel -> [(Agent, Agent, Agent)])
-> (PointedModel -> KripkeModel)
-> PointedModel
-> [(Agent, Agent, Agent)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PointedModel -> KripkeModel
forall a b. (a, b) -> a
fst
  getActuals :: PointedModel -> [Agent]
getActuals = Agent -> [Agent]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (Agent -> [Agent])
-> (PointedModel -> Agent) -> PointedModel -> [Agent]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. World -> Agent
forall a. Show a => a -> Agent
show (World -> Agent)
-> (PointedModel -> World) -> PointedModel -> Agent
forall b c a. (b -> c) -> (a -> b) -> a -> c
. World -> World
forall a. Enum a => a -> World
fromEnum (World -> World)
-> (PointedModel -> World) -> PointedModel -> World
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PointedModel -> World
forall a b. (a, b) -> b
snd

instance KripkeLike MultipointedModel where
  directed :: MultipointedModel -> Bool
directed = KripkeModel -> Bool
forall a. KripkeLike a => a -> Bool
directed (KripkeModel -> Bool)
-> (MultipointedModel -> KripkeModel) -> MultipointedModel -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MultipointedModel -> KripkeModel
forall a b. (a, b) -> a
fst
  getNodes :: MultipointedModel -> [(Agent, Agent)]
getNodes = KripkeModel -> [(Agent, Agent)]
forall a. KripkeLike a => a -> [(Agent, Agent)]
getNodes (KripkeModel -> [(Agent, Agent)])
-> (MultipointedModel -> KripkeModel)
-> MultipointedModel
-> [(Agent, Agent)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MultipointedModel -> KripkeModel
forall a b. (a, b) -> a
fst
  getEdges :: MultipointedModel -> [(Agent, Agent, Agent)]
getEdges = KripkeModel -> [(Agent, Agent, Agent)]
forall a. KripkeLike a => a -> [(Agent, Agent, Agent)]
getEdges (KripkeModel -> [(Agent, Agent, Agent)])
-> (MultipointedModel -> KripkeModel)
-> MultipointedModel
-> [(Agent, Agent, Agent)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MultipointedModel -> KripkeModel
forall a b. (a, b) -> a
fst
  getActuals :: MultipointedModel -> [Agent]
getActuals = (World -> Agent) -> [World] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map (World -> Agent
forall a. Show a => a -> Agent
show (World -> Agent) -> (World -> World) -> World -> Agent
forall b c a. (b -> c) -> (a -> b) -> a -> c
. World -> World
forall a. Enum a => a -> World
fromEnum) ([World] -> [Agent])
-> (MultipointedModel -> [World]) -> MultipointedModel -> [Agent]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MultipointedModel -> [World]
forall a b. (a, b) -> b
snd

instance TexAble KripkeModel       where
  tex :: KripkeModel -> Agent
tex           = ViaDot KripkeModel -> Agent
forall a. TexAble a => a -> Agent
tex(ViaDot KripkeModel -> Agent)
-> (KripkeModel -> ViaDot KripkeModel) -> KripkeModel -> Agent
forall b c a. (b -> c) -> (a -> b) -> a -> c
.KripkeModel -> ViaDot KripkeModel
forall a. a -> ViaDot a
ViaDot
  texTo :: KripkeModel -> Agent -> IO ()
texTo         = ViaDot KripkeModel -> Agent -> IO ()
forall a. TexAble a => a -> Agent -> IO ()
texTo(ViaDot KripkeModel -> Agent -> IO ())
-> (KripkeModel -> ViaDot KripkeModel)
-> KripkeModel
-> Agent
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.KripkeModel -> ViaDot KripkeModel
forall a. a -> ViaDot a
ViaDot
  texDocumentTo :: KripkeModel -> Agent -> IO ()
texDocumentTo = ViaDot KripkeModel -> Agent -> IO ()
forall a. TexAble a => a -> Agent -> IO ()
texDocumentTo(ViaDot KripkeModel -> Agent -> IO ())
-> (KripkeModel -> ViaDot KripkeModel)
-> KripkeModel
-> Agent
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.KripkeModel -> ViaDot KripkeModel
forall a. a -> ViaDot a
ViaDot

instance TexAble PointedModel      where
  tex :: PointedModel -> Agent
tex           = ViaDot PointedModel -> Agent
forall a. TexAble a => a -> Agent
tex(ViaDot PointedModel -> Agent)
-> (PointedModel -> ViaDot PointedModel) -> PointedModel -> Agent
forall b c a. (b -> c) -> (a -> b) -> a -> c
.PointedModel -> ViaDot PointedModel
forall a. a -> ViaDot a
ViaDot
  texTo :: PointedModel -> Agent -> IO ()
texTo         = ViaDot PointedModel -> Agent -> IO ()
forall a. TexAble a => a -> Agent -> IO ()
texTo(ViaDot PointedModel -> Agent -> IO ())
-> (PointedModel -> ViaDot PointedModel)
-> PointedModel
-> Agent
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.PointedModel -> ViaDot PointedModel
forall a. a -> ViaDot a
ViaDot
  texDocumentTo :: PointedModel -> Agent -> IO ()
texDocumentTo = ViaDot PointedModel -> Agent -> IO ()
forall a. TexAble a => a -> Agent -> IO ()
texDocumentTo(ViaDot PointedModel -> Agent -> IO ())
-> (PointedModel -> ViaDot PointedModel)
-> PointedModel
-> Agent
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.PointedModel -> ViaDot PointedModel
forall a. a -> ViaDot a
ViaDot

instance TexAble MultipointedModel where
  tex :: MultipointedModel -> Agent
tex           = ViaDot MultipointedModel -> Agent
forall a. TexAble a => a -> Agent
tex(ViaDot MultipointedModel -> Agent)
-> (MultipointedModel -> ViaDot MultipointedModel)
-> MultipointedModel
-> Agent
forall b c a. (b -> c) -> (a -> b) -> a -> c
.MultipointedModel -> ViaDot MultipointedModel
forall a. a -> ViaDot a
ViaDot
  texTo :: MultipointedModel -> Agent -> IO ()
texTo         = ViaDot MultipointedModel -> Agent -> IO ()
forall a. TexAble a => a -> Agent -> IO ()
texTo(ViaDot MultipointedModel -> Agent -> IO ())
-> (MultipointedModel -> ViaDot MultipointedModel)
-> MultipointedModel
-> Agent
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.MultipointedModel -> ViaDot MultipointedModel
forall a. a -> ViaDot a
ViaDot
  texDocumentTo :: MultipointedModel -> Agent -> IO ()
texDocumentTo = ViaDot MultipointedModel -> Agent -> IO ()
forall a. TexAble a => a -> Agent -> IO ()
texDocumentTo(ViaDot MultipointedModel -> Agent -> IO ())
-> (MultipointedModel -> ViaDot MultipointedModel)
-> MultipointedModel
-> Agent
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.MultipointedModel -> ViaDot MultipointedModel
forall a. a -> ViaDot a
ViaDot

instance Arbitrary KripkeModel where
  arbitrary :: Gen KripkeModel
arbitrary = do
    [World]
nonActualWorlds <- [World] -> Gen [World]
forall a. [a] -> Gen [a]
sublistOf [World
1..World
8]
    let worlds :: [World]
worlds = World
0 World -> [World] -> [World]
forall a. a -> [a] -> [a]
: [World]
nonActualWorlds
    [(World, (Map Prp Bool, Map Agent [World]))]
m <- (World -> Gen (World, (Map Prp Bool, Map Agent [World])))
-> [World] -> Gen [(World, (Map Prp Bool, Map Agent [World]))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\World
w -> do
      [(Prp, Bool)]
myAssignment <- [Prp] -> [Bool] -> [(Prp, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Prp]
defaultVocabulary ([Bool] -> [(Prp, Bool)]) -> Gen [Bool] -> Gen [(Prp, Bool)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Bool -> Gen [Bool]
forall a. Gen a -> Gen [a]
infiniteListOf ((Bool, Bool) -> Gen Bool
forall a. Random a => (a, a) -> Gen a
choose (Bool
True,Bool
False))
      [(Agent, [World])]
myRelations <- (Agent -> Gen (Agent, [World]))
-> [Agent] -> Gen [(Agent, [World])]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\Agent
a -> do
        [World]
reachables <- [World] -> Gen [World]
forall a. [a] -> Gen [a]
sublistOf [World]
worlds
        (Agent, [World]) -> Gen (Agent, [World])
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Agent
a,[World]
reachables)
        ) [Agent]
defaultAgents
      (World, (Map Prp Bool, Map Agent [World]))
-> Gen (World, (Map Prp Bool, Map Agent [World]))
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (World
w, ([(Prp, Bool)] -> Map Prp Bool
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Prp, Bool)]
myAssignment, [(Agent, [World])] -> Map Agent [World]
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Agent, [World])]
myRelations)) -- FIXME avoid fromList, build M.map directly?
      ) [World]
worlds
    KripkeModel -> Gen KripkeModel
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (KripkeModel -> Gen KripkeModel) -> KripkeModel -> Gen KripkeModel
forall a b. (a -> b) -> a -> b
$ Map World (Map Prp Bool, Map Agent [World]) -> KripkeModel
KrM (Map World (Map Prp Bool, Map Agent [World]) -> KripkeModel)
-> Map World (Map Prp Bool, Map Agent [World]) -> KripkeModel
forall a b. (a -> b) -> a -> b
$ [(World, (Map Prp Bool, Map Agent [World]))]
-> Map World (Map Prp Bool, Map Agent [World])
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(World, (Map Prp Bool, Map Agent [World]))]
m
  shrink :: KripkeModel -> [KripkeModel]
shrink KripkeModel
krm = [ KripkeModel
krm KripkeModel -> World -> KripkeModel
`withoutWorld` World
w | [World] -> World
forall a. [a] -> World
forall (t :: * -> *) a. Foldable t => t a -> World
length (KripkeModel -> [World]
forall a. HasWorlds a => a -> [World]
worldsOf KripkeModel
krm) World -> World -> Bool
forall a. Ord a => a -> a -> Bool
> World
1, World
w <- World -> [World] -> [World]
forall a. Eq a => a -> [a] -> [a]
delete World
0 (KripkeModel -> [World]
forall a. HasWorlds a => a -> [World]
worldsOf KripkeModel
krm) ]

withoutWorld :: KripkeModel -> World -> KripkeModel
withoutWorld :: KripkeModel -> World -> KripkeModel
withoutWorld (KrM Map World (Map Prp Bool, Map Agent [World])
m) World
w = Map World (Map Prp Bool, Map Agent [World]) -> KripkeModel
KrM (Map World (Map Prp Bool, Map Agent [World]) -> KripkeModel)
-> Map World (Map Prp Bool, Map Agent [World]) -> KripkeModel
forall a b. (a -> b) -> a -> b
$ ((Map Prp Bool, Map Agent [World])
 -> (Map Prp Bool, Map Agent [World]))
-> Map World (Map Prp Bool, Map Agent [World])
-> Map World (Map Prp Bool, Map Agent [World])
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ((Map Agent [World] -> Map Agent [World])
-> (Map Prp Bool, Map Agent [World])
-> (Map Prp Bool, Map Agent [World])
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (([World] -> [World]) -> Map Agent [World] -> Map Agent [World]
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (World -> [World] -> [World]
forall a. Eq a => a -> [a] -> [a]
delete World
w))) (Map World (Map Prp Bool, Map Agent [World])
 -> Map World (Map Prp Bool, Map Agent [World]))
-> Map World (Map Prp Bool, Map Agent [World])
-> Map World (Map Prp Bool, Map Agent [World])
forall a b. (a -> b) -> a -> b
$ World
-> Map World (Map Prp Bool, Map Agent [World])
-> Map World (Map Prp Bool, Map Agent [World])
forall k a. Ord k => k -> Map k a -> Map k a
M.delete World
w Map World (Map Prp Bool, Map Agent [World])
m

eval :: PointedModel -> Form -> Bool
eval :: PointedModel -> Form -> Bool
eval PointedModel
_     Form
Top           = Bool
True
eval PointedModel
_     Form
Bot           = Bool
False
eval (KripkeModel
m,World
w) (PrpF Prp
p)      = Prp
p Prp -> [Prp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` KripkeModel -> World -> [Prp]
truthsInAt KripkeModel
m World
w
eval PointedModel
pm    (Neg Form
f)       = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ PointedModel -> Form -> Bool
eval PointedModel
pm Form
f
eval PointedModel
pm    (Conj [Form]
fs)     = (Form -> Bool) -> [Form] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (PointedModel -> Form -> Bool
eval PointedModel
pm) [Form]
fs
eval PointedModel
pm    (Disj [Form]
fs)     = (Form -> Bool) -> [Form] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (PointedModel -> Form -> Bool
eval PointedModel
pm) [Form]
fs
eval PointedModel
pm    (Xor  [Form]
fs)     = World -> Bool
forall a. Integral a => a -> Bool
odd (World -> Bool) -> World -> Bool
forall a b. (a -> b) -> a -> b
$ [Bool] -> World
forall a. [a] -> World
forall (t :: * -> *) a. Foldable t => t a -> World
length ((Bool -> Bool) -> [Bool] -> [Bool]
forall a. (a -> Bool) -> [a] -> [a]
filter Bool -> Bool
forall a. a -> a
id ([Bool] -> [Bool]) -> [Bool] -> [Bool]
forall a b. (a -> b) -> a -> b
$ (Form -> Bool) -> [Form] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (PointedModel -> Form -> Bool
eval PointedModel
pm) [Form]
fs)
eval PointedModel
pm    (Impl Form
f Form
g)    = Bool -> Bool
not (PointedModel -> Form -> Bool
eval PointedModel
pm Form
f) Bool -> Bool -> Bool
|| PointedModel -> Form -> Bool
eval PointedModel
pm Form
g
eval PointedModel
pm    (Equi Form
f Form
g)    = PointedModel -> Form -> Bool
eval PointedModel
pm Form
f Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== PointedModel -> Form -> Bool
eval PointedModel
pm Form
g
eval PointedModel
pm    (Forall [Prp]
ps Form
f) = PointedModel -> Form -> Bool
eval PointedModel
pm ((Form -> Prp -> Form) -> Form -> [Prp] -> Form
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Form -> Prp -> Form
singleForall Form
f [Prp]
ps) where
  singleForall :: Form -> Prp -> Form
singleForall Form
g Prp
p = [Form] -> Form
Conj [ Prp -> Form -> Form -> Form
substit Prp
p Form
Top Form
g, Prp -> Form -> Form -> Form
substit Prp
p Form
Bot Form
g ]
eval PointedModel
pm    (Exists [Prp]
ps Form
f) = PointedModel -> Form -> Bool
eval PointedModel
pm ((Form -> Prp -> Form) -> Form -> [Prp] -> Form
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Form -> Prp -> Form
singleExists Form
f [Prp]
ps) where
  singleExists :: Form -> Prp -> Form
singleExists Form
g Prp
p = [Form] -> Form
Disj [ Prp -> Form -> Form -> Form
substit Prp
p Form
Top Form
g, Prp -> Form -> Form -> Form
substit Prp
p Form
Bot Form
g ]
eval (KrM Map World (Map Prp Bool, Map Agent [World])
m,World
w) (K   Agent
i Form
f) = (World -> Bool) -> [World] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\World
w' -> PointedModel -> Form -> Bool
eval (Map World (Map Prp Bool, Map Agent [World]) -> KripkeModel
KrM Map World (Map Prp Bool, Map Agent [World])
m,World
w') Form
f) ((Map Prp Bool, Map Agent [World]) -> Map Agent [World]
forall a b. (a, b) -> b
snd (Map World (Map Prp Bool, Map Agent [World])
m Map World (Map Prp Bool, Map Agent [World])
-> World -> (Map Prp Bool, Map Agent [World])
forall k a. Ord k => Map k a -> k -> a
! World
w) Map Agent [World] -> Agent -> [World]
forall k a. Ord k => Map k a -> k -> a
! Agent
i)
eval (KrM Map World (Map Prp Bool, Map Agent [World])
m,World
w) (Kw  Agent
i Form
f) = (World -> Bool) -> [World] -> Bool
forall b a. Eq b => (a -> b) -> [a] -> Bool
alleqWith (\World
w' -> PointedModel -> Form -> Bool
eval (Map World (Map Prp Bool, Map Agent [World]) -> KripkeModel
KrM Map World (Map Prp Bool, Map Agent [World])
m,World
w') Form
f) ((Map Prp Bool, Map Agent [World]) -> Map Agent [World]
forall a b. (a, b) -> b
snd (Map World (Map Prp Bool, Map Agent [World])
m Map World (Map Prp Bool, Map Agent [World])
-> World -> (Map Prp Bool, Map Agent [World])
forall k a. Ord k => Map k a -> k -> a
! World
w) Map Agent [World] -> Agent -> [World]
forall k a. Ord k => Map k a -> k -> a
! Agent
i)
eval (KripkeModel
m,World
w) (Ck [Agent]
ags Form
form) = (World -> Bool) -> [World] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\World
w' -> PointedModel -> Form -> Bool
eval (KripkeModel
m,World
w') Form
form) (KripkeModel -> [Agent] -> World -> [World]
groupRel KripkeModel
m [Agent]
ags World
w)
eval (KripkeModel
m,World
w) (Ckw [Agent]
ags Form
form) = (World -> Bool) -> [World] -> Bool
forall b a. Eq b => (a -> b) -> [a] -> Bool
alleqWith (\World
w' -> PointedModel -> Form -> Bool
eval (KripkeModel
m,World
w') Form
form) (KripkeModel -> [Agent] -> World -> [World]
groupRel KripkeModel
m [Agent]
ags World
w)
eval (KripkeModel
m,World
w) (Dk [Agent]
ags Form
form) = (World -> Bool) -> [World] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\World
w' -> PointedModel -> Form -> Bool
eval (KripkeModel
m,World
w') Form
form) (KripkeModel -> [Agent] -> World -> [World]
distRel KripkeModel
m [Agent]
ags World
w)
eval (KripkeModel
m,World
w) (Dkw [Agent]
ags Form
form) = (World -> Bool) -> [World] -> Bool
forall b a. Eq b => (a -> b) -> [a] -> Bool
alleqWith (\World
w' -> PointedModel -> Form -> Bool
eval (KripkeModel
m,World
w') Form
form) (KripkeModel -> [Agent] -> World -> [World]
distRel KripkeModel
m [Agent]
ags World
w)
eval (KripkeModel
m,World
w) (PubAnnounce Form
f Form
g) = Bool -> Bool
not (PointedModel -> Form -> Bool
eval (KripkeModel
m,World
w) Form
f) Bool -> Bool -> Bool
|| PointedModel -> Form -> Bool
eval (PointedModel -> Form -> PointedModel
forall a b. Update a b => a -> b -> a
update (KripkeModel
m,World
w) Form
f) Form
g
eval (KripkeModel
m,World
w) (PubAnnounceW Form
f Form
g) = PointedModel -> Form -> Bool
eval (KripkeModel -> Form -> KripkeModel
forall a b. Update a b => a -> b -> a
update KripkeModel
m Form
aform, World
w) Form
g where
  aform :: Form
aform | PointedModel -> Form -> Bool
eval (KripkeModel
m,World
w) Form
f = Form
f
        | Bool
otherwise     = Form -> Form
Neg Form
f
eval (KripkeModel
m,World
w) (Announce [Agent]
listeners Form
f Form
g) = Bool -> Bool
not (PointedModel -> Form -> Bool
eval (KripkeModel
m,World
w) Form
f) Bool -> Bool -> Bool
|| PointedModel -> Form -> Bool
eval PointedModel
newm Form
g where
  newm :: PointedModel
newm = (KripkeModel
m,World
w) PointedModel -> PointedActionModel -> PointedModel
forall a b. Update a b => a -> b -> a
`update` [Agent] -> [Agent] -> Form -> PointedActionModel
announceAction (KripkeModel -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf KripkeModel
m) [Agent]
listeners Form
f
eval (KripkeModel
m,World
w) (AnnounceW [Agent]
listeners Form
f Form
g) = PointedModel -> Form -> Bool
eval PointedModel
newm Form
g where
  newm :: PointedModel
newm = (KripkeModel
m,World
w) PointedModel -> PointedActionModel -> PointedModel
forall a b. Update a b => a -> b -> a
`update` [Agent] -> [Agent] -> Form -> PointedActionModel
announceAction (KripkeModel -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf KripkeModel
m) [Agent]
listeners Form
aform
  aform :: Form
aform | PointedModel -> Form -> Bool
eval (KripkeModel
m,World
w) Form
f = Form
f
        | Bool
otherwise    = Form -> Form
Neg Form
f
eval PointedModel
pm (Dia (Dyn Agent
dynLabel Dynamic
d) Form
f) = case Dynamic -> Maybe PointedActionModel
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
d of
  Just PointedActionModel
pactm -> PointedModel -> Form -> Bool
eval PointedModel
pm (PointedActionModel -> Form
forall a. HasPrecondition a => a -> Form
preOf (PointedActionModel
pactm :: PointedActionModel)) Bool -> Bool -> Bool
&& PointedModel -> Form -> Bool
eval (PointedModel
pm PointedModel -> PointedActionModel -> PointedModel
forall a b. Update a b => a -> b -> a
`update` PointedActionModel
pactm) Form
f
  Maybe PointedActionModel
Nothing    -> Agent -> Bool
forall a. HasCallStack => Agent -> a
error (Agent -> Bool) -> Agent -> Bool
forall a b. (a -> b) -> a -> b
$ Agent
"cannot update Kripke model with '" Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
dynLabel Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
"':\n  " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Dynamic -> Agent
forall a. Show a => a -> Agent
show Dynamic
d

instance Semantics PointedModel where
  isTrue :: PointedModel -> Form -> Bool
isTrue = PointedModel -> Form -> Bool
eval

instance Semantics KripkeModel where
  isTrue :: KripkeModel -> Form -> Bool
isTrue KripkeModel
m = MultipointedModel -> Form -> Bool
forall a. Semantics a => a -> Form -> Bool
isTrue (KripkeModel
m, KripkeModel -> [World]
forall a. HasWorlds a => a -> [World]
worldsOf KripkeModel
m)

instance Semantics MultipointedModel where
  isTrue :: MultipointedModel -> Form -> Bool
isTrue (KripkeModel
m,[World]
ws) Form
f = (World -> Bool) -> [World] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\World
w -> PointedModel -> Form -> Bool
forall a. Semantics a => a -> Form -> Bool
isTrue (KripkeModel
m,World
w) Form
f) [World]
ws

-- | Transitive closure of the union of the relations of a group.
-- Note that this is not necessarily reflexive.
groupRel :: KripkeModel -> [Agent] -> World -> [World]
groupRel :: KripkeModel -> [Agent] -> World -> [World]
groupRel (KrM Map World (Map Prp Bool, Map Agent [World])
m) [Agent]
ags World
w = [World] -> [World]
forall a. Ord a => [a] -> [a]
sort ([World] -> [World]) -> [World] -> [World]
forall a b. (a -> b) -> a -> b
$ ([World] -> [World]) -> [World] -> [World]
forall a. Eq a => (a -> a) -> a -> a
lfp [World] -> [World]
extend (World -> [World]
oneStepReachFrom World
w) where
  oneStepReachFrom :: World -> [World]
oneStepReachFrom World
x = [[World]] -> [World]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ (Map Prp Bool, Map Agent [World]) -> Map Agent [World]
forall a b. (a, b) -> b
snd (Map World (Map Prp Bool, Map Agent [World])
m Map World (Map Prp Bool, Map Agent [World])
-> World -> (Map Prp Bool, Map Agent [World])
forall k a. Ord k => Map k a -> k -> a
! World
x) Map Agent [World] -> Agent -> [World]
forall k a. Ord k => Map k a -> k -> a
! Agent
a | Agent
a <- [Agent]
ags ]
  extend :: [World] -> [World]
extend [World]
xs = [World] -> [World]
nubInt ([World] -> [World]) -> [World] -> [World]
forall a b. (a -> b) -> a -> b
$ [World]
xs [World] -> [World] -> [World]
forall a. [a] -> [a] -> [a]
++ (World -> [World]) -> [World] -> [World]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap World -> [World]
oneStepReachFrom [World]
xs

distRel :: KripkeModel -> [Agent] -> World -> [World]
distRel :: KripkeModel -> [Agent] -> World -> [World]
distRel (KrM Map World (Map Prp Bool, Map Agent [World])
m) [Agent]
ags World
w = [World] -> [World]
forall a. Ord a => [a] -> [a]
sort ([World] -> [World]) -> [World] -> [World]
forall a b. (a -> b) -> a -> b
$ World -> [World]
oneStepReachFrom World
w where
  oneStepReachFrom :: World -> [World]
oneStepReachFrom World
x = ([World] -> [World] -> [World]) -> [[World]] -> [World]
forall a. (a -> a -> a) -> [a] -> a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 [World] -> [World] -> [World]
forall a. Eq a => [a] -> [a] -> [a]
intersect [ (Map Prp Bool, Map Agent [World]) -> Map Agent [World]
forall a b. (a, b) -> b
snd (Map World (Map Prp Bool, Map Agent [World])
m Map World (Map Prp Bool, Map Agent [World])
-> World -> (Map Prp Bool, Map Agent [World])
forall k a. Ord k => Map k a -> k -> a
! World
x) Map Agent [World] -> Agent -> [World]
forall k a. Ord k => Map k a -> k -> a
! Agent
a | Agent
a <- [Agent]
ags ]

instance Update KripkeModel Form where
  checks :: [KripkeModel -> Form -> Bool]
checks = [ ] -- unpointed models can always be updated with any formula
  unsafeUpdate :: KripkeModel -> Form -> KripkeModel
unsafeUpdate (KrM Map World (Map Prp Bool, Map Agent [World])
m) Form
f = Map World (Map Prp Bool, Map Agent [World]) -> KripkeModel
KrM Map World (Map Prp Bool, Map Agent [World])
newm where
    newm :: Map World (Map Prp Bool, Map Agent [World])
newm = (World
 -> (Map Prp Bool, Map Agent [World])
 -> Maybe (Map Prp Bool, Map Agent [World]))
-> Map World (Map Prp Bool, Map Agent [World])
-> Map World (Map Prp Bool, Map Agent [World])
forall k a b. (k -> a -> Maybe b) -> Map k a -> Map k b
M.mapMaybeWithKey World
-> (Map Prp Bool, Map Agent [World])
-> Maybe (Map Prp Bool, Map Agent [World])
isin Map World (Map Prp Bool, Map Agent [World])
m
    isin :: World
-> (Map Prp Bool, Map Agent [World])
-> Maybe (Map Prp Bool, Map Agent [World])
isin World
w' (Map Prp Bool
v,Map Agent [World]
rs) | PointedModel -> Form -> Bool
eval (Map World (Map Prp Bool, Map Agent [World]) -> KripkeModel
KrM Map World (Map Prp Bool, Map Agent [World])
m,World
w') Form
f = (Map Prp Bool, Map Agent [World])
-> Maybe (Map Prp Bool, Map Agent [World])
forall a. a -> Maybe a
Just (Map Prp Bool
v, ([World] -> [World]) -> Map Agent [World] -> Map Agent [World]
forall a b k. (a -> b) -> Map k a -> Map k b
M.map [World] -> [World]
newr Map Agent [World]
rs)
                   | Bool
otherwise         = Maybe (Map Prp Bool, Map Agent [World])
forall a. Maybe a
Nothing
    newr :: [World] -> [World]
newr = (World -> Bool) -> [World] -> [World]
forall a. (a -> Bool) -> [a] -> [a]
filter (World -> [World] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Map World (Map Prp Bool, Map Agent [World]) -> [World]
forall k a. Map k a -> [k]
M.keys Map World (Map Prp Bool, Map Agent [World])
newm)

instance Update PointedModel Form where
  unsafeUpdate :: PointedModel -> Form -> PointedModel
unsafeUpdate (KripkeModel
m,World
w) Form
f = (KripkeModel -> Form -> KripkeModel
forall a b. Update a b => a -> b -> a
unsafeUpdate KripkeModel
m Form
f, World
w)

instance Update MultipointedModel Form where
  unsafeUpdate :: MultipointedModel -> Form -> MultipointedModel
unsafeUpdate (KripkeModel
m,[World]
ws) Form
f =
    let newm :: KripkeModel
newm = KripkeModel -> Form -> KripkeModel
forall a b. Update a b => a -> b -> a
unsafeUpdate KripkeModel
m Form
f in (KripkeModel
newm, [World]
ws [World] -> [World] -> [World]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` KripkeModel -> [World]
forall a. HasWorlds a => a -> [World]
worldsOf KripkeModel
newm)

announceAction :: [Agent] -> [Agent] -> Form -> PointedActionModel
announceAction :: [Agent] -> [Agent] -> Form -> PointedActionModel
announceAction [Agent]
everyone [Agent]
listeners Form
f = (Map World Act -> ActionModel
ActM Map World Act
am, World
1) where
  am :: Map World Act
am = [(World, Act)] -> Map World Act
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
    [ (World
1, Act { pre :: Form
pre = Form
f,   post :: PostCondition
post = PostCondition
forall k a. Map k a
M.empty, rel :: Map Agent [World]
rel = [(Agent, [World])] -> Map Agent [World]
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Agent, [World])] -> Map Agent [World])
-> [(Agent, [World])] -> Map Agent [World]
forall a b. (a -> b) -> a -> b
$ [(Agent
i,[World
1]) | Agent
i <- [Agent]
listeners] [(Agent, [World])] -> [(Agent, [World])] -> [(Agent, [World])]
forall a. [a] -> [a] -> [a]
++ [(Agent
i,[World
2]) | Agent
i <- [Agent]
everyone [Agent] -> [Agent] -> [Agent]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Agent]
listeners] } )
    , (World
2, Act { pre :: Form
pre = Form
Top, post :: PostCondition
post = PostCondition
forall k a. Map k a
M.empty, rel :: Map Agent [World]
rel = [(Agent, [World])] -> Map Agent [World]
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Agent
i,[World
2]) | Agent
i <- [Agent]
everyone] } )
    ]

checkBisim :: Bisimulation -> KripkeModel -> KripkeModel -> Bool
checkBisim :: Bisimulation -> KripkeModel -> KripkeModel -> Bool
checkBisim [] KripkeModel
_  KripkeModel
_  = Bool
False
checkBisim Bisimulation
z  KripkeModel
m1 KripkeModel
m2 =
  ((World, World) -> Bool) -> Bisimulation -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(World
w1,World
w2) ->
        (KripkeModel -> World -> [Prp]
truthsInAt KripkeModel
m1 World
w1 [Prp] -> [Prp] -> Bool
forall a. Eq a => a -> a -> Bool
== KripkeModel -> World -> [Prp]
truthsInAt KripkeModel
m2 World
w2)  -- same valuation
    Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [ (World -> Bool) -> [World] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\World
v2 -> (World
v1,World
v2) (World, World) -> Bisimulation -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Bisimulation
z) (Agent -> KripkeModel -> Map World [World]
relOfIn Agent
ag KripkeModel
m2 Map World [World] -> World -> [World]
forall k a. Ord k => Map k a -> k -> a
! World
w2) -- forth
           | Agent
ag <- KripkeModel -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf KripkeModel
m1, World
v1 <- Agent -> KripkeModel -> Map World [World]
relOfIn Agent
ag KripkeModel
m1 Map World [World] -> World -> [World]
forall k a. Ord k => Map k a -> k -> a
! World
w1 ]
    Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [ (World -> Bool) -> [World] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\World
v1 -> (World
v1,World
v2) (World, World) -> Bisimulation -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Bisimulation
z) (Agent -> KripkeModel -> Map World [World]
relOfIn Agent
ag KripkeModel
m1 Map World [World] -> World -> [World]
forall k a. Ord k => Map k a -> k -> a
! World
w1) -- back
           | Agent
ag <- KripkeModel -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf KripkeModel
m2, World
v2 <- Agent -> KripkeModel -> Map World [World]
relOfIn Agent
ag KripkeModel
m2 Map World [World] -> World -> [World]
forall k a. Ord k => Map k a -> k -> a
! World
w2 ]
      ) Bisimulation
z

checkBisimPointed :: Bisimulation -> PointedModel -> PointedModel -> Bool
checkBisimPointed :: Bisimulation -> PointedModel -> PointedModel -> Bool
checkBisimPointed Bisimulation
z (KripkeModel
m1,World
w1) (KripkeModel
m2,World
w2) = (World
w1,World
w2) (World, World) -> Bisimulation -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Bisimulation
z Bool -> Bool -> Bool
&& Bisimulation -> KripkeModel -> KripkeModel -> Bool
checkBisim Bisimulation
z KripkeModel
m1 KripkeModel
m2

type Status = Maybe Form
type StatusMap = M.Map (World,World) Status

diff :: KripkeModel -> KripkeModel -> StatusMap
diff :: KripkeModel -> KripkeModel -> StatusMap
diff KripkeModel
m1 KripkeModel
m2 = (StatusMap -> StatusMap) -> StatusMap -> StatusMap
forall a. Eq a => (a -> a) -> a -> a
lfp StatusMap -> StatusMap
step StatusMap
start where
  -- initialize using differences in atomic propositions given by valuation
  start :: StatusMap
start = [((World, World), Maybe Form)] -> StatusMap
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [ ((World
w1,World
w2), [Prp] -> [Prp] -> Maybe Form
propDiff (KripkeModel -> World -> [Prp]
truthsInAt KripkeModel
m1 World
w1) (KripkeModel -> World -> [Prp]
truthsInAt KripkeModel
m2 World
w2))
                     |  World
w1 <- KripkeModel -> [World]
forall a. HasWorlds a => a -> [World]
worldsOf KripkeModel
m1, World
w2 <- KripkeModel -> [World]
forall a. HasWorlds a => a -> [World]
worldsOf KripkeModel
m2 ]
  propDiff :: [Prp] -> [Prp] -> Maybe Form
propDiff [Prp]
ps [Prp]
qs | [Prp]
ps [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Prp]
qs [Prp] -> [Prp] -> Bool
forall a. Eq a => a -> a -> Bool
/= []  = Form -> Maybe Form
forall a. a -> Maybe a
Just (Form -> Maybe Form) -> Form -> Maybe Form
forall a b. (a -> b) -> a -> b
$       Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ [Prp] -> Prp
forall a. HasCallStack => [a] -> a
head ([Prp]
ps [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Prp]
qs)
                 | [Prp]
qs [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Prp]
ps [Prp] -> [Prp] -> Bool
forall a. Eq a => a -> a -> Bool
/= []  = Form -> Maybe Form
forall a. a -> Maybe a
Just (Form -> Maybe Form) -> Form -> Maybe 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 (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ [Prp] -> Prp
forall a. HasCallStack => [a] -> a
head ([Prp]
qs [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Prp]
ps)
                 | Bool
otherwise       = Maybe Form
forall a. Maybe a
Nothing
  -- until a fixpoint is reached, update the map using all relations
  step :: StatusMap -> StatusMap
step StatusMap
curMap = ((World, World) -> Maybe Form -> Maybe Form)
-> StatusMap -> StatusMap
forall k a b. (k -> a -> b) -> Map k a -> Map k b
M.mapWithKey (StatusMap -> (World, World) -> Maybe Form -> Maybe Form
updateAt StatusMap
curMap) StatusMap
curMap
  updateAt :: StatusMap -> (World, World) -> Maybe Form -> Maybe Form
updateAt StatusMap
_      (World, World)
_       (Just Form
f) = Form -> Maybe Form
forall a. a -> Maybe a
Just Form
f
  updateAt StatusMap
curMap (World
w1,World
w2) Maybe Form
Nothing  = case
    -- forth
    [ Form -> Form
Neg (Form -> Form) -> ([Form] -> Form) -> [Form] -> Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Agent -> Form -> Form
K Agent
i (Form -> Form) -> ([Form] -> Form) -> [Form] -> Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Form -> Form
Neg (Form -> Form) -> ([Form] -> Form) -> [Form] -> Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Form] -> Form
Conj ([Form] -> Form) -> [Form] -> Form
forall a b. (a -> b) -> a -> b
$ [ Form
f | World
w2' <- [World]
w2's, let f :: Form
f = Maybe Form -> Form
forall a. HasCallStack => Maybe a -> a
fromJust (StatusMap
curMap StatusMap -> (World, World) -> Maybe Form
forall k a. Ord k => Map k a -> k -> a
! (World
w1',World
w2')) ]
    | Agent
i <- KripkeModel -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf KripkeModel
m1
    , let w2's :: [World]
w2's = Agent -> KripkeModel -> Map World [World]
relOfIn Agent
i KripkeModel
m2 Map World [World] -> World -> [World]
forall k a. Ord k => Map k a -> k -> a
! World
w2
    , World
w1' <- Agent -> KripkeModel -> Map World [World]
relOfIn Agent
i KripkeModel
m1 Map World [World] -> World -> [World]
forall k a. Ord k => Map k a -> k -> a
! World
w1
    , (World -> Bool) -> [World] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\World
w2' -> Maybe Form -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Form -> Bool) -> Maybe Form -> Bool
forall a b. (a -> b) -> a -> b
$ StatusMap
curMap StatusMap -> (World, World) -> Maybe Form
forall k a. Ord k => Map k a -> k -> a
! (World
w1',World
w2')) [World]
w2's
    ]
    [Form] -> [Form] -> [Form]
forall a. [a] -> [a] -> [a]
++
    -- back
    [ Agent -> Form -> Form
K Agent
i (Form -> Form) -> ([Form] -> Form) -> [Form] -> Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Form] -> Form
Disj ([Form] -> Form) -> [Form] -> Form
forall a b. (a -> b) -> a -> b
$ [ Form
f | World
w1' <- [World]
w1's, let f :: Form
f = Maybe Form -> Form
forall a. HasCallStack => Maybe a -> a
fromJust (StatusMap
curMap StatusMap -> (World, World) -> Maybe Form
forall k a. Ord k => Map k a -> k -> a
! (World
w1',World
w2')) ]
    | Agent
i <- KripkeModel -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf KripkeModel
m1
    , let w1's :: [World]
w1's = Agent -> KripkeModel -> Map World [World]
relOfIn Agent
i KripkeModel
m1 Map World [World] -> World -> [World]
forall k a. Ord k => Map k a -> k -> a
! World
w1
    , World
w2' <- Agent -> KripkeModel -> Map World [World]
relOfIn Agent
i KripkeModel
m2 Map World [World] -> World -> [World]
forall k a. Ord k => Map k a -> k -> a
! World
w2
    , (World -> Bool) -> [World] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\World
w1' -> Maybe Form -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Form -> Bool) -> Maybe Form -> Bool
forall a b. (a -> b) -> a -> b
$ StatusMap
curMap StatusMap -> (World, World) -> Maybe Form
forall k a. Ord k => Map k a -> k -> a
! (World
w1',World
w2')) [World]
w1's
    ]
    of
      [] -> Maybe Form
forall a. Maybe a
Nothing
      (Form
f:[Form]
_) -> Form -> Maybe Form
forall a. a -> Maybe a
Just Form
f

diffPointed :: PointedModel -> PointedModel -> Either Bisimulation Form
diffPointed :: PointedModel -> PointedModel -> Either Bisimulation Form
diffPointed (KripkeModel
m1,World
w1) (KripkeModel
m2,World
w2) =
  case KripkeModel -> KripkeModel -> StatusMap
diff KripkeModel
m1 KripkeModel
m2 StatusMap -> (World, World) -> Maybe Form
forall k a. Ord k => Map k a -> k -> a
! (World
w1,World
w2) of
    Maybe Form
Nothing -> Bisimulation -> Either Bisimulation Form
forall a b. a -> Either a b
Left (Bisimulation -> Either Bisimulation Form)
-> Bisimulation -> Either Bisimulation Form
forall a b. (a -> b) -> a -> b
$ StatusMap -> Bisimulation
forall k a. Map k a -> [k]
M.keys (StatusMap -> Bisimulation) -> StatusMap -> Bisimulation
forall a b. (a -> b) -> a -> b
$ (Maybe Form -> Bool) -> StatusMap -> StatusMap
forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter Maybe Form -> Bool
forall a. Maybe a -> Bool
isNothing (KripkeModel -> KripkeModel -> StatusMap
diff KripkeModel
m1 KripkeModel
m2)
    Just Form
f -> Form -> Either Bisimulation Form
forall a b. b -> Either a b
Right Form
f

generatedSubmodel :: PointedModel -> PointedModel
generatedSubmodel :: PointedModel -> PointedModel
generatedSubmodel (KrM Map World (Map Prp Bool, Map Agent [World])
m, World
cur) = (Map World (Map Prp Bool, Map Agent [World]) -> KripkeModel
KrM Map World (Map Prp Bool, Map Agent [World])
newm, World
cur) where
  newm :: Map World (Map Prp Bool, Map Agent [World])
newm = (World
 -> (Map Prp Bool, Map Agent [World])
 -> Maybe (Map Prp Bool, Map Agent [World]))
-> Map World (Map Prp Bool, Map Agent [World])
-> Map World (Map Prp Bool, Map Agent [World])
forall k a b. (k -> a -> Maybe b) -> Map k a -> Map k b
M.mapMaybeWithKey World
-> (Map Prp Bool, Map Agent [World])
-> Maybe (Map Prp Bool, Map Agent [World])
isin Map World (Map Prp Bool, Map Agent [World])
m
  isin :: World
-> (Map Prp Bool, Map Agent [World])
-> Maybe (Map Prp Bool, Map Agent [World])
isin World
w' (Map Prp Bool
v,Map Agent [World]
rs) | World
w' World -> [World] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [World]
reachable = (Map Prp Bool, Map Agent [World])
-> Maybe (Map Prp Bool, Map Agent [World])
forall a. a -> Maybe a
Just (Map Prp Bool
v, ([World] -> [World]) -> Map Agent [World] -> Map Agent [World]
forall a b k. (a -> b) -> Map k a -> Map k b
M.map [World] -> [World]
newr Map Agent [World]
rs)
                 | Bool
otherwise           = Maybe (Map Prp Bool, Map Agent [World])
forall a. Maybe a
Nothing
  newr :: [World] -> [World]
newr = (World -> Bool) -> [World] -> [World]
forall a. (a -> Bool) -> [a] -> [a]
filter (World -> [World] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Map World (Map Prp Bool, Map Agent [World]) -> [World]
forall k a. Map k a -> [k]
M.keys Map World (Map Prp Bool, Map Agent [World])
newm)
  reachable :: [World]
reachable = ([World] -> [World]) -> [World] -> [World]
forall a. Eq a => (a -> a) -> a -> a
lfp [World] -> [World]
follow [World
cur] where
    follow :: [World] -> [World]
follow [World]
xs = [World] -> [World]
forall a. Ord a => [a] -> [a]
sort ([World] -> [World]) -> ([World] -> [World]) -> [World] -> [World]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [World] -> [World]
nubInt ([World] -> [World]) -> [World] -> [World]
forall a b. (a -> b) -> a -> b
$ [[World]] -> [World]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ (Map Prp Bool, Map Agent [World]) -> Map Agent [World]
forall a b. (a, b) -> b
snd (Map World (Map Prp Bool, Map Agent [World])
m Map World (Map Prp Bool, Map Agent [World])
-> World -> (Map Prp Bool, Map Agent [World])
forall k a. Ord k => Map k a -> k -> a
! World
x) Map Agent [World] -> Agent -> [World]
forall k a. Ord k => Map k a -> k -> a
! Agent
a | World
x <- [World]
xs, Agent
a <- KripkeModel -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf (Map World (Map Prp Bool, Map Agent [World]) -> KripkeModel
KrM Map World (Map Prp Bool, Map Agent [World])
m) ]

type PostCondition = M.Map Prp Form

data Act = Act {Act -> Form
pre :: Form, Act -> PostCondition
post :: PostCondition, Act -> Map Agent [World]
rel :: M.Map Agent [Action]}
  deriving (Act -> Act -> Bool
(Act -> Act -> Bool) -> (Act -> Act -> Bool) -> Eq Act
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Act -> Act -> Bool
== :: Act -> Act -> Bool
$c/= :: Act -> Act -> Bool
/= :: Act -> Act -> Bool
Eq,Eq Act
Eq Act =>
(Act -> Act -> Ordering)
-> (Act -> Act -> Bool)
-> (Act -> Act -> Bool)
-> (Act -> Act -> Bool)
-> (Act -> Act -> Bool)
-> (Act -> Act -> Act)
-> (Act -> Act -> Act)
-> Ord Act
Act -> Act -> Bool
Act -> Act -> Ordering
Act -> Act -> Act
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
$ccompare :: Act -> Act -> Ordering
compare :: Act -> Act -> Ordering
$c< :: Act -> Act -> Bool
< :: Act -> Act -> Bool
$c<= :: Act -> Act -> Bool
<= :: Act -> Act -> Bool
$c> :: Act -> Act -> Bool
> :: Act -> Act -> Bool
$c>= :: Act -> Act -> Bool
>= :: Act -> Act -> Bool
$cmax :: Act -> Act -> Act
max :: Act -> Act -> Act
$cmin :: Act -> Act -> Act
min :: Act -> Act -> Act
Ord,World -> Act -> ShowS
[Act] -> ShowS
Act -> Agent
(World -> Act -> ShowS)
-> (Act -> Agent) -> ([Act] -> ShowS) -> Show Act
forall a.
(World -> a -> ShowS) -> (a -> Agent) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: World -> Act -> ShowS
showsPrec :: World -> Act -> ShowS
$cshow :: Act -> Agent
show :: Act -> Agent
$cshowList :: [Act] -> ShowS
showList :: [Act] -> ShowS
Show)

-- | Extend `post` to all propositions
safepost :: Act -> Prp -> Form
safepost :: Act -> Prp -> Form
safepost Act
ch Prp
p | Prp
p Prp -> [Prp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` PostCondition -> [Prp]
forall k a. Map k a -> [k]
M.keys (Act -> PostCondition
post Act
ch) = Act -> PostCondition
post Act
ch PostCondition -> Prp -> Form
forall k a. Ord k => Map k a -> k -> a
! Prp
p
              | Bool
otherwise = Prp -> Form
PrpF Prp
p

newtype ActionModel = ActM (M.Map Action Act)
  deriving (ActionModel -> ActionModel -> Bool
(ActionModel -> ActionModel -> Bool)
-> (ActionModel -> ActionModel -> Bool) -> Eq ActionModel
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ActionModel -> ActionModel -> Bool
== :: ActionModel -> ActionModel -> Bool
$c/= :: ActionModel -> ActionModel -> Bool
/= :: ActionModel -> ActionModel -> Bool
Eq,Eq ActionModel
Eq ActionModel =>
(ActionModel -> ActionModel -> Ordering)
-> (ActionModel -> ActionModel -> Bool)
-> (ActionModel -> ActionModel -> Bool)
-> (ActionModel -> ActionModel -> Bool)
-> (ActionModel -> ActionModel -> Bool)
-> (ActionModel -> ActionModel -> ActionModel)
-> (ActionModel -> ActionModel -> ActionModel)
-> Ord ActionModel
ActionModel -> ActionModel -> Bool
ActionModel -> ActionModel -> Ordering
ActionModel -> ActionModel -> ActionModel
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
$ccompare :: ActionModel -> ActionModel -> Ordering
compare :: ActionModel -> ActionModel -> Ordering
$c< :: ActionModel -> ActionModel -> Bool
< :: ActionModel -> ActionModel -> Bool
$c<= :: ActionModel -> ActionModel -> Bool
<= :: ActionModel -> ActionModel -> Bool
$c> :: ActionModel -> ActionModel -> Bool
> :: ActionModel -> ActionModel -> Bool
$c>= :: ActionModel -> ActionModel -> Bool
>= :: ActionModel -> ActionModel -> Bool
$cmax :: ActionModel -> ActionModel -> ActionModel
max :: ActionModel -> ActionModel -> ActionModel
$cmin :: ActionModel -> ActionModel -> ActionModel
min :: ActionModel -> ActionModel -> ActionModel
Ord,World -> ActionModel -> ShowS
[ActionModel] -> ShowS
ActionModel -> Agent
(World -> ActionModel -> ShowS)
-> (ActionModel -> Agent)
-> ([ActionModel] -> ShowS)
-> Show ActionModel
forall a.
(World -> a -> ShowS) -> (a -> Agent) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: World -> ActionModel -> ShowS
showsPrec :: World -> ActionModel -> ShowS
$cshow :: ActionModel -> Agent
show :: ActionModel -> Agent
$cshowList :: [ActionModel] -> ShowS
showList :: [ActionModel] -> ShowS
Show)

instance HasAgents ActionModel where
  agentsOf :: ActionModel -> [Agent]
agentsOf (ActM Map World Act
am) = Map Agent [World] -> [Agent]
forall k a. Map k a -> [k]
M.keys (Map Agent [World] -> [Agent]) -> Map Agent [World] -> [Agent]
forall a b. (a -> b) -> a -> b
$ Act -> Map Agent [World]
rel ([Act] -> Act
forall a. HasCallStack => [a] -> a
head (Map World Act -> [Act]
forall k a. Map k a -> [a]
M.elems Map World Act
am))

instance HasPrecondition ActionModel where
  preOf :: ActionModel -> Form
preOf ActionModel
_ = Form
Top

instance Pointed ActionModel Action
type PointedActionModel = (ActionModel, Action)

instance HasPrecondition PointedActionModel where
  preOf :: PointedActionModel -> Form
preOf (ActM Map World Act
am, World
actual) = Act -> Form
pre (Map World Act
am Map World Act -> World -> Act
forall k a. Ord k => Map k a -> k -> a
! World
actual)

instance Pointed ActionModel [Action]
type MultipointedActionModel = (ActionModel, [Action])

instance HasPrecondition MultipointedActionModel where
  preOf :: MultipointedActionModel -> Form
preOf (ActM Map World Act
am, [World]
as) = [Form] -> Form
Disj [ Act -> Form
pre (Map World Act
am Map World Act -> World -> Act
forall k a. Ord k => Map k a -> k -> a
! World
a) | World
a <- [World]
as ]

instance Update KripkeModel ActionModel where
  checks :: [KripkeModel -> ActionModel -> Bool]
checks = [KripkeModel -> ActionModel -> Bool
forall a b. (HasAgents a, HasAgents b) => a -> b -> Bool
haveSameAgents]
  unsafeUpdate :: KripkeModel -> ActionModel -> KripkeModel
unsafeUpdate KripkeModel
m (ActM Map World Act
am) =
    let (KripkeModel
newModel,[World]
_) = MultipointedModel -> MultipointedActionModel -> MultipointedModel
forall a b. Update a b => a -> b -> a
unsafeUpdate (KripkeModel
m, KripkeModel -> [World]
forall a. HasWorlds a => a -> [World]
worldsOf KripkeModel
m) (Map World Act -> ActionModel
ActM Map World Act
am, Map World Act -> [World]
forall k a. Map k a -> [k]
M.keys Map World Act
am) in KripkeModel
newModel

instance Update PointedModel PointedActionModel where
  checks :: [PointedModel -> PointedActionModel -> Bool]
checks = [PointedModel -> PointedActionModel -> Bool
forall a b. (HasAgents a, HasAgents b) => a -> b -> Bool
haveSameAgents,PointedModel -> PointedActionModel -> Bool
forall a b. Update a b => a -> b -> Bool
preCheck]
  unsafeUpdate :: PointedModel -> PointedActionModel -> PointedModel
unsafeUpdate (KripkeModel
m, World
w) (ActionModel
actm, World
a) = [World] -> World
forall a. HasCallStack => [a] -> a
head ([World] -> World) -> MultipointedModel -> PointedModel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MultipointedModel -> MultipointedActionModel -> MultipointedModel
forall a b. Update a b => a -> b -> a
unsafeUpdate (KripkeModel
m, [World
w]) (ActionModel
actm, [World
a])

instance Update PointedModel MultipointedActionModel where
  checks :: [PointedModel -> MultipointedActionModel -> Bool]
checks = [PointedModel -> MultipointedActionModel -> Bool
forall a b. (HasAgents a, HasAgents b) => a -> b -> Bool
haveSameAgents,PointedModel -> MultipointedActionModel -> Bool
forall a b. Update a b => a -> b -> Bool
preCheck]
  unsafeUpdate :: PointedModel -> MultipointedActionModel -> PointedModel
unsafeUpdate (KripkeModel
m, World
w) MultipointedActionModel
mpactm = [World] -> World
forall a. HasCallStack => [a] -> a
head ([World] -> World) -> MultipointedModel -> PointedModel
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MultipointedModel -> MultipointedActionModel -> MultipointedModel
forall a b. Update a b => a -> b -> a
unsafeUpdate (KripkeModel
m, [World
w]) MultipointedActionModel
mpactm

instance Update MultipointedModel PointedActionModel where
  checks :: [MultipointedModel -> PointedActionModel -> Bool]
checks = [MultipointedModel -> PointedActionModel -> Bool
forall a b. (HasAgents a, HasAgents b) => a -> b -> Bool
haveSameAgents] -- do not check precondition!
  unsafeUpdate :: MultipointedModel -> PointedActionModel -> MultipointedModel
unsafeUpdate MultipointedModel
mpm (ActionModel
actm, World
a) = MultipointedModel -> MultipointedActionModel -> MultipointedModel
forall a b. Update a b => a -> b -> a
unsafeUpdate MultipointedModel
mpm (ActionModel
actm, [World
a])

instance Update MultipointedModel MultipointedActionModel where
  checks :: [MultipointedModel -> MultipointedActionModel -> Bool]
checks = [MultipointedModel -> MultipointedActionModel -> Bool
forall a b. (HasAgents a, HasAgents b) => a -> b -> Bool
haveSameAgents]
  unsafeUpdate :: MultipointedModel -> MultipointedActionModel -> MultipointedModel
unsafeUpdate (KrM Map World (Map Prp Bool, Map Agent [World])
m, [World]
ws) (ActM Map World Act
am, [World]
facts) =
    (Map World (Map Prp Bool, Map Agent [World]) -> KripkeModel
KrM (Map World (Map Prp Bool, Map Agent [World]) -> KripkeModel)
-> Map World (Map Prp Bool, Map Agent [World]) -> KripkeModel
forall a b. (a -> b) -> a -> b
$ [(World, (Map Prp Bool, Map Agent [World]))]
-> Map World (Map Prp Bool, Map Agent [World])
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ((((World, World), World)
 -> (World, (Map Prp Bool, Map Agent [World])))
-> [((World, World), World)]
-> [(World, (Map Prp Bool, Map Agent [World]))]
forall a b. (a -> b) -> [a] -> [b]
map ((World, World), World)
-> (World, (Map Prp Bool, Map Agent [World]))
forall {a}.
((World, World), a) -> (a, (Map Prp Bool, Map Agent [World]))
annotate [((World, World), World)]
worldPairs), [World]
newActualWorlds) where
      worldPairs :: [((World, World), World)]
worldPairs = Bisimulation -> [World] -> [((World, World), World)]
forall a b. [a] -> [b] -> [(a, b)]
zip ([Bisimulation] -> Bisimulation
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [ (World
s, World
a) | PointedModel -> Form -> Bool
eval (Map World (Map Prp Bool, Map Agent [World]) -> KripkeModel
KrM Map World (Map Prp Bool, Map Agent [World])
m, World
s) (Act -> Form
pre (Act -> Form) -> Act -> Form
forall a b. (a -> b) -> a -> b
$ Map World Act
am Map World Act -> World -> Act
forall k a. Ord k => Map k a -> k -> a
! World
a) ] | World
s <- Map World (Map Prp Bool, Map Agent [World]) -> [World]
forall k a. Map k a -> [k]
M.keys Map World (Map Prp Bool, Map Agent [World])
m, World
a <- Map World Act -> [World]
forall k a. Map k a -> [k]
M.keys Map World Act
am ]) [World
0..]
      newActualWorlds :: [World]
newActualWorlds = [ World
k | ((World
w,World
a),World
k) <- [((World, World), World)]
worldPairs, World
w World -> [World] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [World]
ws, World
a World -> [World] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [World]
facts ]
      annotate :: ((World, World), a) -> (a, (Map Prp Bool, Map Agent [World]))
annotate ((World
s,World
a),a
news) = (a
news , (Map Prp Bool
newval, [(Agent, [World])] -> Map Agent [World]
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ((Agent -> (Agent, [World])) -> [Agent] -> [(Agent, [World])]
forall a b. (a -> b) -> [a] -> [b]
map Agent -> (Agent, [World])
reachFor (KripkeModel -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf (Map World (Map Prp Bool, Map Agent [World]) -> KripkeModel
KrM Map World (Map Prp Bool, Map Agent [World])
m))))) where
        newval :: Map Prp Bool
newval = (Prp -> Bool -> Bool) -> Map Prp Bool -> Map Prp Bool
forall k a b. (k -> a -> b) -> Map k a -> Map k b
M.mapWithKey Prp -> Bool -> Bool
applyPC ((Map Prp Bool, Map Agent [World]) -> Map Prp Bool
forall a b. (a, b) -> a
fst ((Map Prp Bool, Map Agent [World]) -> Map Prp Bool)
-> (Map Prp Bool, Map Agent [World]) -> Map Prp Bool
forall a b. (a -> b) -> a -> b
$ Map World (Map Prp Bool, Map Agent [World])
m Map World (Map Prp Bool, Map Agent [World])
-> World -> (Map Prp Bool, Map Agent [World])
forall k a. Ord k => Map k a -> k -> a
! World
s)
        applyPC :: Prp -> Bool -> Bool
applyPC Prp
p Bool
oldbit
          | Prp
p Prp -> [Prp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` PostCondition -> [Prp]
forall k a. Map k a -> [k]
M.keys (Act -> PostCondition
post (Map World Act
am Map World Act -> World -> Act
forall k a. Ord k => Map k a -> k -> a
! World
a)) = PointedModel -> Form -> Bool
eval (Map World (Map Prp Bool, Map Agent [World]) -> KripkeModel
KrM Map World (Map Prp Bool, Map Agent [World])
m,World
s) (Act -> PostCondition
post (Map World Act
am Map World Act -> World -> Act
forall k a. Ord k => Map k a -> k -> a
! World
a) PostCondition -> Prp -> Form
forall k a. Ord k => Map k a -> k -> a
! Prp
p)
          | Bool
otherwise = Bool
oldbit
        reachFor :: Agent -> (Agent, [World])
reachFor Agent
i = (Agent
i, [ World
news' | ((World
s',World
a'),World
news') <- [((World, World), World)]
worldPairs, World
s' World -> [World] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (Map Prp Bool, Map Agent [World]) -> Map Agent [World]
forall a b. (a, b) -> b
snd (Map World (Map Prp Bool, Map Agent [World])
m Map World (Map Prp Bool, Map Agent [World])
-> World -> (Map Prp Bool, Map Agent [World])
forall k a. Ord k => Map k a -> k -> a
!  World
s) Map Agent [World] -> Agent -> [World]
forall k a. Ord k => Map k a -> k -> a
! Agent
i, World
a' World -> [World] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Act -> Map Agent [World]
rel (Map World Act
am Map World Act -> World -> Act
forall k a. Ord k => Map k a -> k -> a
! World
a) Map Agent [World] -> Agent -> [World]
forall k a. Ord k => Map k a -> k -> a
! Agent
i ])

instance Arbitrary ActionModel where
  arbitrary :: Gen ActionModel
arbitrary = do
    let allactions :: [World]
allactions = [World
0..World
3]
    BF Form
f <- (World -> Gen BF) -> Gen BF
forall a. (World -> Gen a) -> Gen a
sized ((World -> Gen BF) -> Gen BF) -> (World -> Gen BF) -> Gen BF
forall a b. (a -> b) -> a -> b
$ [Prp] -> World -> Gen BF
randomboolformWith [Prp]
defaultVocabulary
    BF Form
g <- (World -> Gen BF) -> Gen BF
forall a. (World -> Gen a) -> Gen a
sized ((World -> Gen BF) -> Gen BF) -> (World -> Gen BF) -> Gen BF
forall a b. (a -> b) -> a -> b
$ [Prp] -> World -> Gen BF
randomboolformWith [Prp]
defaultVocabulary
    BF Form
h <- (World -> Gen BF) -> Gen BF
forall a. (World -> Gen a) -> Gen a
sized ((World -> Gen BF) -> Gen BF) -> (World -> Gen BF) -> Gen BF
forall a b. (a -> b) -> a -> b
$ [Prp] -> World -> Gen BF
randomboolformWith [Prp]
defaultVocabulary
    let myPres :: [Form]
myPres  = Form
Top Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: (Form -> Form) -> [Form] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map Form -> Form
simplify [Form
f,Form
g,Form
h]
    [PostCondition]
myPosts <- (World -> Gen PostCondition) -> [World] -> Gen [PostCondition]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\World
_ -> do
      Prp
proptochange <- [Prp] -> Gen Prp
forall a. [a] -> Gen a
elements [Prp]
defaultVocabulary
      Form
postconcon <- [Form] -> Gen Form
forall a. [a] -> Gen a
elements ([Form] -> Gen Form) -> [Form] -> Gen Form
forall a b. (a -> b) -> a -> b
$ [Form
Top,Form
Bot] [Form] -> [Form] -> [Form]
forall a. [a] -> [a] -> [a]
++ (Prp -> Form) -> [Prp] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map Prp -> Form
PrpF [Prp]
defaultVocabulary
      PostCondition -> Gen PostCondition
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (PostCondition -> Gen PostCondition)
-> PostCondition -> Gen PostCondition
forall a b. (a -> b) -> a -> b
$ [(Prp, Form)] -> PostCondition
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [ (Prp
proptochange, Form
postconcon) ]
      ) [World]
allactions
    [Map Agent [World]]
myRels <- (World -> Gen (Map Agent [World]))
-> [World] -> Gen [Map Agent [World]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\World
k -> do
      [World]
reachList <- [World] -> Gen [World]
forall a. [a] -> Gen [a]
sublistOf [World]
allactions
      Map Agent [World] -> Gen (Map Agent [World])
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Agent [World] -> Gen (Map Agent [World]))
-> Map Agent [World] -> Gen (Map Agent [World])
forall a b. (a -> b) -> a -> b
$ [(Agent, [World])] -> Map Agent [World]
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(Agent, [World])] -> Map Agent [World])
-> [(Agent, [World])] -> Map Agent [World]
forall a b. (a -> b) -> a -> b
$ (Agent
"1",[World
k]) (Agent, [World]) -> [(Agent, [World])] -> [(Agent, [World])]
forall a. a -> [a] -> [a]
: [ (Agent
ag,[World]
reachList) | Agent
ag <- [Agent] -> [Agent]
forall a. HasCallStack => [a] -> [a]
tail [Agent]
defaultAgents ]
      ) [World]
allactions
    ActionModel -> Gen ActionModel
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (ActionModel -> Gen ActionModel) -> ActionModel -> Gen ActionModel
forall a b. (a -> b) -> a -> b
$ Map World Act -> ActionModel
ActM (Map World Act -> ActionModel) -> Map World Act -> ActionModel
forall a b. (a -> b) -> a -> b
$ [(World, Act)] -> Map World Act
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
      [ (World
k::Action, Form -> PostCondition -> Map Agent [World] -> Act
Act ([Form]
myPres [Form] -> World -> Form
forall a. HasCallStack => [a] -> World -> a
!! World
k) ([PostCondition]
myPosts [PostCondition] -> World -> PostCondition
forall a. HasCallStack => [a] -> World -> a
!! World
k) ([Map Agent [World]]
myRels [Map Agent [World]] -> World -> Map Agent [World]
forall a. HasCallStack => [a] -> World -> a
!! World
k)) | World
k <- [World]
allactions ]
  shrink :: ActionModel -> [ActionModel]
shrink (ActM Map World Act
am) = [ Map World Act -> ActionModel
ActM (Map World Act -> ActionModel) -> Map World Act -> ActionModel
forall a b. (a -> b) -> a -> b
$ World -> Map World Act -> Map World Act
forall {k}. World -> Map k Act -> Map k Act
removeFromRels World
k (Map World Act -> Map World Act) -> Map World Act -> Map World Act
forall a b. (a -> b) -> a -> b
$ World -> Map World Act -> Map World Act
forall k a. Ord k => k -> Map k a -> Map k a
M.delete World
k Map World Act
am | World
k <- Map World Act -> [World]
forall k a. Map k a -> [k]
M.keys Map World Act
am, World
k World -> World -> Bool
forall a. Eq a => a -> a -> Bool
/= World
0 ] where
    removeFromRels :: World -> Map k Act -> Map k Act
removeFromRels = (Act -> Act) -> Map k Act -> Map k Act
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ((Act -> Act) -> Map k Act -> Map k Act)
-> (World -> Act -> Act) -> World -> Map k Act -> Map k Act
forall b c a. (b -> c) -> (a -> b) -> a -> c
. World -> Act -> Act
removeFrom where
      removeFrom :: World -> Act -> Act
removeFrom World
k Act
c = Act
c { rel = M.map (delete k) (rel c) }

instance KripkeLike ActionModel where
  directed :: ActionModel -> Bool
directed = Bool -> ActionModel -> Bool
forall a b. a -> b -> a
const Bool
True
  getNodes :: ActionModel -> [(Agent, Agent)]
getNodes (ActM Map World Act
am) = (World -> (Agent, Agent)) -> [World] -> [(Agent, Agent)]
forall a b. (a -> b) -> [a] -> [b]
map (World -> Agent
forall a. Show a => a -> Agent
show (World -> Agent) -> (World -> Agent) -> World -> (Agent, Agent)
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& World -> Agent
labelOf) (Map World Act -> [World]
forall k a. Map k a -> [k]
M.keys Map World Act
am) where
    labelOf :: World -> Agent
labelOf World
a = [Agent] -> Agent
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ Agent
"$\\begin{array}{c} ? " , Form -> Agent
forall a. TexAble a => a -> Agent
tex (Act -> Form
pre (Map World Act
am Map World Act -> World -> Act
forall k a. Ord k => Map k a -> k -> a
! World
a)) , Agent
"\\\\"
      , Agent -> [Agent] -> Agent
forall a. [a] -> [[a]] -> [a]
intercalate Agent
"\\\\" (((Prp, Form) -> Agent) -> [(Prp, Form)] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map (Prp, Form) -> Agent
forall {a} {a}. (TexAble a, TexAble a) => (a, a) -> Agent
showPost (PostCondition -> [(Prp, Form)]
forall k a. Map k a -> [(k, a)]
M.toList (PostCondition -> [(Prp, Form)]) -> PostCondition -> [(Prp, Form)]
forall a b. (a -> b) -> a -> b
$ Act -> PostCondition
post (Map World Act
am Map World Act -> World -> Act
forall k a. Ord k => Map k a -> k -> a
! World
a)))
      , Agent
"\\end{array}$" ]
    showPost :: (a, a) -> Agent
showPost (a
p,a
f) = a -> Agent
forall a. TexAble a => a -> Agent
tex a
p Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ Agent
" := " Agent -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> Agent
forall a. TexAble a => a -> Agent
tex a
f
  getEdges :: ActionModel -> [(Agent, Agent, Agent)]
getEdges (ActM Map World Act
am) =
    [[(Agent, Agent, Agent)]] -> [(Agent, Agent, Agent)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [ (Agent
i, World -> Agent
forall a. Show a => a -> Agent
show World
a, World -> Agent
forall a. Show a => a -> Agent
show World
b) | World
b <- Act -> Map Agent [World]
rel (Map World Act
am Map World Act -> World -> Act
forall k a. Ord k => Map k a -> k -> a
! World
a) Map Agent [World] -> Agent -> [World]
forall k a. Ord k => Map k a -> k -> a
! Agent
i ] | World
a <- Map World Act -> [World]
forall k a. Map k a -> [k]
M.keys Map World Act
am, Agent
i <- ActionModel -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf (Map World Act -> ActionModel
ActM Map World Act
am) ]
  getActuals :: ActionModel -> [Agent]
getActuals = [Agent] -> ActionModel -> [Agent]
forall a b. a -> b -> a
const [ ]

instance TexAble ActionModel where
  tex :: ActionModel -> Agent
tex = ViaDot ActionModel -> Agent
forall a. TexAble a => a -> Agent
tex(ViaDot ActionModel -> Agent)
-> (ActionModel -> ViaDot ActionModel) -> ActionModel -> Agent
forall b c a. (b -> c) -> (a -> b) -> a -> c
.ActionModel -> ViaDot ActionModel
forall a. a -> ViaDot a
ViaDot
  texTo :: ActionModel -> Agent -> IO ()
texTo = ViaDot ActionModel -> Agent -> IO ()
forall a. TexAble a => a -> Agent -> IO ()
texTo(ViaDot ActionModel -> Agent -> IO ())
-> (ActionModel -> ViaDot ActionModel)
-> ActionModel
-> Agent
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.ActionModel -> ViaDot ActionModel
forall a. a -> ViaDot a
ViaDot
  texDocumentTo :: ActionModel -> Agent -> IO ()
texDocumentTo = ViaDot ActionModel -> Agent -> IO ()
forall a. TexAble a => a -> Agent -> IO ()
texDocumentTo(ViaDot ActionModel -> Agent -> IO ())
-> (ActionModel -> ViaDot ActionModel)
-> ActionModel
-> Agent
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.ActionModel -> ViaDot ActionModel
forall a. a -> ViaDot a
ViaDot

instance KripkeLike PointedActionModel where
  directed :: PointedActionModel -> Bool
directed = ActionModel -> Bool
forall a. KripkeLike a => a -> Bool
directed (ActionModel -> Bool)
-> (PointedActionModel -> ActionModel)
-> PointedActionModel
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PointedActionModel -> ActionModel
forall a b. (a, b) -> a
fst
  getNodes :: PointedActionModel -> [(Agent, Agent)]
getNodes = ActionModel -> [(Agent, Agent)]
forall a. KripkeLike a => a -> [(Agent, Agent)]
getNodes (ActionModel -> [(Agent, Agent)])
-> (PointedActionModel -> ActionModel)
-> PointedActionModel
-> [(Agent, Agent)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PointedActionModel -> ActionModel
forall a b. (a, b) -> a
fst
  getEdges :: PointedActionModel -> [(Agent, Agent, Agent)]
getEdges = ActionModel -> [(Agent, Agent, Agent)]
forall a. KripkeLike a => a -> [(Agent, Agent, Agent)]
getEdges (ActionModel -> [(Agent, Agent, Agent)])
-> (PointedActionModel -> ActionModel)
-> PointedActionModel
-> [(Agent, Agent, Agent)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PointedActionModel -> ActionModel
forall a b. (a, b) -> a
fst
  getActuals :: PointedActionModel -> [Agent]
getActuals (ActionModel
_, World
a) = [World -> Agent
forall a. Show a => a -> Agent
show World
a]

instance TexAble PointedActionModel where
  tex :: PointedActionModel -> Agent
tex = ViaDot PointedActionModel -> Agent
forall a. TexAble a => a -> Agent
tex(ViaDot PointedActionModel -> Agent)
-> (PointedActionModel -> ViaDot PointedActionModel)
-> PointedActionModel
-> Agent
forall b c a. (b -> c) -> (a -> b) -> a -> c
.PointedActionModel -> ViaDot PointedActionModel
forall a. a -> ViaDot a
ViaDot
  texTo :: PointedActionModel -> Agent -> IO ()
texTo = ViaDot PointedActionModel -> Agent -> IO ()
forall a. TexAble a => a -> Agent -> IO ()
texTo(ViaDot PointedActionModel -> Agent -> IO ())
-> (PointedActionModel -> ViaDot PointedActionModel)
-> PointedActionModel
-> Agent
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.PointedActionModel -> ViaDot PointedActionModel
forall a. a -> ViaDot a
ViaDot
  texDocumentTo :: PointedActionModel -> Agent -> IO ()
texDocumentTo = ViaDot PointedActionModel -> Agent -> IO ()
forall a. TexAble a => a -> Agent -> IO ()
texDocumentTo(ViaDot PointedActionModel -> Agent -> IO ())
-> (PointedActionModel -> ViaDot PointedActionModel)
-> PointedActionModel
-> Agent
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.PointedActionModel -> ViaDot PointedActionModel
forall a. a -> ViaDot a
ViaDot

instance KripkeLike MultipointedActionModel where
  directed :: MultipointedActionModel -> Bool
directed = ActionModel -> Bool
forall a. KripkeLike a => a -> Bool
directed (ActionModel -> Bool)
-> (MultipointedActionModel -> ActionModel)
-> MultipointedActionModel
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MultipointedActionModel -> ActionModel
forall a b. (a, b) -> a
fst
  getNodes :: MultipointedActionModel -> [(Agent, Agent)]
getNodes = ActionModel -> [(Agent, Agent)]
forall a. KripkeLike a => a -> [(Agent, Agent)]
getNodes (ActionModel -> [(Agent, Agent)])
-> (MultipointedActionModel -> ActionModel)
-> MultipointedActionModel
-> [(Agent, Agent)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MultipointedActionModel -> ActionModel
forall a b. (a, b) -> a
fst
  getEdges :: MultipointedActionModel -> [(Agent, Agent, Agent)]
getEdges = ActionModel -> [(Agent, Agent, Agent)]
forall a. KripkeLike a => a -> [(Agent, Agent, Agent)]
getEdges (ActionModel -> [(Agent, Agent, Agent)])
-> (MultipointedActionModel -> ActionModel)
-> MultipointedActionModel
-> [(Agent, Agent, Agent)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MultipointedActionModel -> ActionModel
forall a b. (a, b) -> a
fst
  getActuals :: MultipointedActionModel -> [Agent]
getActuals (ActionModel
_, [World]
as) = (World -> Agent) -> [World] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map World -> Agent
forall a. Show a => a -> Agent
show [World]
as

instance TexAble MultipointedActionModel where
  tex :: MultipointedActionModel -> Agent
tex = ViaDot MultipointedActionModel -> Agent
forall a. TexAble a => a -> Agent
tex(ViaDot MultipointedActionModel -> Agent)
-> (MultipointedActionModel -> ViaDot MultipointedActionModel)
-> MultipointedActionModel
-> Agent
forall b c a. (b -> c) -> (a -> b) -> a -> c
.MultipointedActionModel -> ViaDot MultipointedActionModel
forall a. a -> ViaDot a
ViaDot
  texTo :: MultipointedActionModel -> Agent -> IO ()
texTo = ViaDot MultipointedActionModel -> Agent -> IO ()
forall a. TexAble a => a -> Agent -> IO ()
texTo(ViaDot MultipointedActionModel -> Agent -> IO ())
-> (MultipointedActionModel -> ViaDot MultipointedActionModel)
-> MultipointedActionModel
-> Agent
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.MultipointedActionModel -> ViaDot MultipointedActionModel
forall a. a -> ViaDot a
ViaDot
  texDocumentTo :: MultipointedActionModel -> Agent -> IO ()
texDocumentTo = ViaDot MultipointedActionModel -> Agent -> IO ()
forall a. TexAble a => a -> Agent -> IO ()
texDocumentTo(ViaDot MultipointedActionModel -> Agent -> IO ())
-> (MultipointedActionModel -> ViaDot MultipointedActionModel)
-> MultipointedActionModel
-> Agent
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
.MultipointedActionModel -> ViaDot MultipointedActionModel
forall a. a -> ViaDot a
ViaDot