{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, FlexibleContexts #-}

module SMCDEL.Explicit.S5 where

import Control.Arrow (second,(&&&))
import Data.Dynamic
import Data.GraphViz
import Data.List
import Data.Tuple (swap)
import Data.Maybe (fromMaybe)

import SMCDEL.Language
import SMCDEL.Internal.TexDisplay
import SMCDEL.Internal.Help (alleqWith,fusion,intersection,apply,(!),lfp)
import Test.QuickCheck

type World = Int

class HasWorlds a where
  worldsOf :: a -> [World]

instance (HasWorlds a, Pointed a b) => HasWorlds (a,b) where worldsOf :: (a, b) -> [Int]
worldsOf = a -> [Int]
forall a. HasWorlds a => a -> [Int]
worldsOf (a -> [Int]) -> ((a, b) -> a) -> (a, b) -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, b) -> a
forall a b. (a, b) -> a
fst

type Partition = [[World]]
type Assignment = [(Prp,Bool)]

data KripkeModelS5 = KrMS5 [World] [(Agent,Partition)] [(World,Assignment)] deriving (KripkeModelS5 -> KripkeModelS5 -> Bool
(KripkeModelS5 -> KripkeModelS5 -> Bool)
-> (KripkeModelS5 -> KripkeModelS5 -> Bool) -> Eq KripkeModelS5
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: KripkeModelS5 -> KripkeModelS5 -> Bool
== :: KripkeModelS5 -> KripkeModelS5 -> Bool
$c/= :: KripkeModelS5 -> KripkeModelS5 -> Bool
/= :: KripkeModelS5 -> KripkeModelS5 -> Bool
Eq,Eq KripkeModelS5
Eq KripkeModelS5 =>
(KripkeModelS5 -> KripkeModelS5 -> Ordering)
-> (KripkeModelS5 -> KripkeModelS5 -> Bool)
-> (KripkeModelS5 -> KripkeModelS5 -> Bool)
-> (KripkeModelS5 -> KripkeModelS5 -> Bool)
-> (KripkeModelS5 -> KripkeModelS5 -> Bool)
-> (KripkeModelS5 -> KripkeModelS5 -> KripkeModelS5)
-> (KripkeModelS5 -> KripkeModelS5 -> KripkeModelS5)
-> Ord KripkeModelS5
KripkeModelS5 -> KripkeModelS5 -> Bool
KripkeModelS5 -> KripkeModelS5 -> Ordering
KripkeModelS5 -> KripkeModelS5 -> KripkeModelS5
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 :: KripkeModelS5 -> KripkeModelS5 -> Ordering
compare :: KripkeModelS5 -> KripkeModelS5 -> Ordering
$c< :: KripkeModelS5 -> KripkeModelS5 -> Bool
< :: KripkeModelS5 -> KripkeModelS5 -> Bool
$c<= :: KripkeModelS5 -> KripkeModelS5 -> Bool
<= :: KripkeModelS5 -> KripkeModelS5 -> Bool
$c> :: KripkeModelS5 -> KripkeModelS5 -> Bool
> :: KripkeModelS5 -> KripkeModelS5 -> Bool
$c>= :: KripkeModelS5 -> KripkeModelS5 -> Bool
>= :: KripkeModelS5 -> KripkeModelS5 -> Bool
$cmax :: KripkeModelS5 -> KripkeModelS5 -> KripkeModelS5
max :: KripkeModelS5 -> KripkeModelS5 -> KripkeModelS5
$cmin :: KripkeModelS5 -> KripkeModelS5 -> KripkeModelS5
min :: KripkeModelS5 -> KripkeModelS5 -> KripkeModelS5
Ord,Int -> KripkeModelS5 -> ShowS
[KripkeModelS5] -> ShowS
KripkeModelS5 -> Agent
(Int -> KripkeModelS5 -> ShowS)
-> (KripkeModelS5 -> Agent)
-> ([KripkeModelS5] -> ShowS)
-> Show KripkeModelS5
forall a.
(Int -> a -> ShowS) -> (a -> Agent) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> KripkeModelS5 -> ShowS
showsPrec :: Int -> KripkeModelS5 -> ShowS
$cshow :: KripkeModelS5 -> Agent
show :: KripkeModelS5 -> Agent
$cshowList :: [KripkeModelS5] -> ShowS
showList :: [KripkeModelS5] -> ShowS
Show)

instance Pointed KripkeModelS5 World
type PointedModelS5 = (KripkeModelS5,World)

instance Pointed KripkeModelS5 [World]
type MultipointedModelS5 = (KripkeModelS5,[World])

instance HasAgents KripkeModelS5 where
  agentsOf :: KripkeModelS5 -> [Agent]
agentsOf (KrMS5 [Int]
_ [(Agent, [[Int]])]
rel [(Int, Assignment)]
_) = ((Agent, [[Int]]) -> Agent) -> [(Agent, [[Int]])] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map (Agent, [[Int]]) -> Agent
forall a b. (a, b) -> a
fst [(Agent, [[Int]])]
rel

instance HasVocab KripkeModelS5 where
  vocabOf :: KripkeModelS5 -> [Prp]
vocabOf (KrMS5 [Int]
_ [(Agent, [[Int]])]
_ [(Int, Assignment)]
val) = ((Prp, Bool) -> Prp) -> Assignment -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map (Prp, Bool) -> Prp
forall a b. (a, b) -> a
fst (Assignment -> [Prp]) -> Assignment -> [Prp]
forall a b. (a -> b) -> a -> b
$ (Int, Assignment) -> Assignment
forall a b. (a, b) -> b
snd ([(Int, Assignment)] -> (Int, Assignment)
forall a. HasCallStack => [a] -> a
head [(Int, Assignment)]
val)

instance HasWorlds KripkeModelS5 where
  worldsOf :: KripkeModelS5 -> [Int]
worldsOf (KrMS5 [Int]
ws [(Agent, [[Int]])]
_ [(Int, Assignment)]
_) = [Int]
ws

newtype PropList = PropList [Prp]

withoutWorld :: KripkeModelS5 -> World -> KripkeModelS5
withoutWorld :: KripkeModelS5 -> Int -> KripkeModelS5
withoutWorld (KrMS5 [Int]
worlds [(Agent, [[Int]])]
parts [(Int, Assignment)]
val) Int
w = [Int] -> [(Agent, [[Int]])] -> [(Int, Assignment)] -> KripkeModelS5
KrMS5
  (Int -> [Int] -> [Int]
forall a. Eq a => a -> [a] -> [a]
delete Int
w [Int]
worlds)
  (((Agent, [[Int]]) -> (Agent, [[Int]]))
-> [(Agent, [[Int]])] -> [(Agent, [[Int]])]
forall a b. (a -> b) -> [a] -> [b]
map (([[Int]] -> [[Int]]) -> (Agent, [[Int]]) -> (Agent, [[Int]])
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 (([Int] -> Bool) -> [[Int]] -> [[Int]]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Int] -> [Int] -> Bool
forall a. Eq a => a -> a -> Bool
/=[]) ([[Int]] -> [[Int]]) -> ([[Int]] -> [[Int]]) -> [[Int]] -> [[Int]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Int] -> [Int]) -> [[Int]] -> [[Int]]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> [Int] -> [Int]
forall a. Eq a => a -> [a] -> [a]
delete Int
w))) [(Agent, [[Int]])]
parts)
  (((Int, Assignment) -> Bool)
-> [(Int, Assignment)] -> [(Int, Assignment)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/=Int
w)(Int -> Bool)
-> ((Int, Assignment) -> Int) -> (Int, Assignment) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Int, Assignment) -> Int
forall a b. (a, b) -> a
fst) [(Int, Assignment)]
val)

withoutProps :: KripkeModelS5 -> [Prp] -> KripkeModelS5
withoutProps :: KripkeModelS5 -> [Prp] -> KripkeModelS5
withoutProps (KrMS5 [Int]
worlds [(Agent, [[Int]])]
parts [(Int, Assignment)]
val) [Prp]
dropProps = [Int] -> [(Agent, [[Int]])] -> [(Int, Assignment)] -> KripkeModelS5
KrMS5
  [Int]
worlds
  [(Agent, [[Int]])]
parts
  (((Int, Assignment) -> (Int, Assignment))
-> [(Int, Assignment)] -> [(Int, Assignment)]
forall a b. (a -> b) -> [a] -> [b]
map ((Assignment -> Assignment)
-> (Int, Assignment) -> (Int, Assignment)
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 ((Assignment -> Assignment)
 -> (Int, Assignment) -> (Int, Assignment))
-> (Assignment -> Assignment)
-> (Int, Assignment)
-> (Int, Assignment)
forall a b. (a -> b) -> a -> b
$ ((Prp, Bool) -> Bool) -> Assignment -> Assignment
forall a. (a -> Bool) -> [a] -> [a]
filter ((Prp -> [Prp] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Prp]
dropProps) (Prp -> Bool) -> ((Prp, Bool) -> Prp) -> (Prp, Bool) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Prp, Bool) -> Prp
forall a b. (a, b) -> a
fst)) [(Int, Assignment)]
val)

instance Arbitrary PropList where
  arbitrary :: Gen PropList
arbitrary = do
    [Prp]
moreprops <- [Prp] -> Gen [Prp]
forall a. [a] -> Gen [a]
sublistOf ((Int -> Prp) -> [Int] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Prp
P [Int
1..Int
10])
    PropList -> Gen PropList
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (PropList -> Gen PropList) -> PropList -> Gen PropList
forall a b. (a -> b) -> a -> b
$ [Prp] -> PropList
PropList ([Prp] -> PropList) -> [Prp] -> PropList
forall a b. (a -> b) -> a -> b
$ Int -> Prp
P Int
0 Prp -> [Prp] -> [Prp]
forall a. a -> [a] -> [a]
: [Prp]
moreprops

randomPartFor :: [World] -> Gen Partition
randomPartFor :: [Int] -> Gen [[Int]]
randomPartFor [Int]
worlds = do
  [Int]
indices <- Gen Int -> Gen [Int]
forall a. Gen a -> Gen [a]
infiniteListOf (Gen Int -> Gen [Int]) -> Gen Int -> Gen [Int]
forall a b. (a -> b) -> a -> b
$ (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
1, [Int] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
worlds)
  let pairs :: [(Int, Int)]
pairs = [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
worlds [Int]
indices
  let parts :: [[Int]]
parts = [ [Int] -> [Int]
forall a. Ord a => [a] -> [a]
sort ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ ((Int, Int) -> Int) -> [(Int, Int)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Int) -> Int
forall a b. (a, b) -> a
fst ([(Int, Int)] -> [Int]) -> [(Int, Int)] -> [Int]
forall a b. (a -> b) -> a -> b
$ ((Int, Int) -> Bool) -> [(Int, Int)] -> [(Int, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
k)(Int -> Bool) -> ((Int, Int) -> Int) -> (Int, Int) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Int, Int) -> Int
forall a b. (a, b) -> b
snd) [(Int, Int)]
pairs | Int
k <- [Int
1 .. ([Int] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
worlds)] ]
  [[Int]] -> Gen [[Int]]
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return ([[Int]] -> Gen [[Int]]) -> [[Int]] -> Gen [[Int]]
forall a b. (a -> b) -> a -> b
$ [[Int]] -> [[Int]]
forall a. Ord a => [a] -> [a]
sort ([[Int]] -> [[Int]]) -> [[Int]] -> [[Int]]
forall a b. (a -> b) -> a -> b
$ ([Int] -> Bool) -> [[Int]] -> [[Int]]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Int] -> [Int] -> Bool
forall a. Eq a => a -> a -> Bool
/=[]) [[Int]]
parts

instance Arbitrary KripkeModelS5 where
  arbitrary :: Gen KripkeModelS5
arbitrary = do
    [Int]
nonActualWorlds <- [Int] -> Gen [Int]
forall a. [a] -> Gen [a]
sublistOf [Int
1..Int
8]
    let worlds :: [Int]
worlds = Int
0 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
nonActualWorlds
    [(Int, Assignment)]
val <- (Int -> Gen (Int, Assignment)) -> [Int] -> Gen [(Int, Assignment)]
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 (\Int
w -> do
      Assignment
myAssignment <- [Prp] -> [Bool] -> Assignment
forall a b. [a] -> [b] -> [(a, b)]
zip [Prp]
defaultVocabulary ([Bool] -> Assignment) -> Gen [Bool] -> Gen Assignment
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))
      (Int, Assignment) -> Gen (Int, Assignment)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int
w,Assignment
myAssignment)
      ) [Int]
worlds
    [(Agent, [[Int]])]
parts <- (Agent -> Gen (Agent, [[Int]]))
-> [Agent] -> Gen [(Agent, [[Int]])]
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
i -> do
      [[Int]]
myPartition <- [Int] -> Gen [[Int]]
randomPartFor [Int]
worlds
      (Agent, [[Int]]) -> Gen (Agent, [[Int]])
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Agent
i,[[Int]]
myPartition)
      ) [Agent]
defaultAgents
    KripkeModelS5 -> Gen KripkeModelS5
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (KripkeModelS5 -> Gen KripkeModelS5)
-> KripkeModelS5 -> Gen KripkeModelS5
forall a b. (a -> b) -> a -> b
$ [Int] -> [(Agent, [[Int]])] -> [(Int, Assignment)] -> KripkeModelS5
KrMS5 [Int]
worlds [(Agent, [[Int]])]
parts [(Int, Assignment)]
val
  shrink :: KripkeModelS5 -> [KripkeModelS5]
shrink m :: KripkeModelS5
m@(KrMS5 [Int]
worlds [(Agent, [[Int]])]
_ [(Int, Assignment)]
_) =
    [ KripkeModelS5
m KripkeModelS5 -> Int -> KripkeModelS5
`withoutWorld` Int
w | Int
w <- [Int]
worlds, Bool -> Bool
not ([Int] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Int] -> Bool) -> [Int] -> Bool
forall a b. (a -> b) -> a -> b
$ Int -> [Int] -> [Int]
forall a. Eq a => a -> [a] -> [a]
delete Int
w [Int]
worlds) ]

eval :: PointedModelS5 -> Form -> Bool
eval :: PointedModelS5 -> Form -> Bool
eval PointedModelS5
_ Form
Top = Bool
True
eval PointedModelS5
_ Form
Bot = Bool
False
eval (KrMS5 [Int]
_ [(Agent, [[Int]])]
_ [(Int, Assignment)]
val, Int
cur) (PrpF Prp
p) = Assignment -> Prp -> Bool
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply ([(Int, Assignment)] -> Int -> Assignment
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [(Int, Assignment)]
val Int
cur) Prp
p
eval PointedModelS5
pm (Neg Form
form)    = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ PointedModelS5 -> Form -> Bool
eval PointedModelS5
pm Form
form
eval PointedModelS5
pm (Conj [Form]
forms)  = (Form -> Bool) -> [Form] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (PointedModelS5 -> Form -> Bool
eval PointedModelS5
pm) [Form]
forms
eval PointedModelS5
pm (Disj [Form]
forms)  = (Form -> Bool) -> [Form] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (PointedModelS5 -> Form -> Bool
eval PointedModelS5
pm) [Form]
forms
eval PointedModelS5
pm (Xor  [Form]
forms)  = Int -> Bool
forall a. Integral a => a -> Bool
odd (Int -> Bool) -> Int -> Bool
forall a b. (a -> b) -> a -> b
$ [Bool] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
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 (PointedModelS5 -> Form -> Bool
eval PointedModelS5
pm) [Form]
forms)
eval PointedModelS5
pm (Impl Form
f Form
g)    = Bool -> Bool
not (PointedModelS5 -> Form -> Bool
eval PointedModelS5
pm Form
f) Bool -> Bool -> Bool
|| PointedModelS5 -> Form -> Bool
eval PointedModelS5
pm Form
g
eval PointedModelS5
pm (Equi Form
f Form
g)    = PointedModelS5 -> Form -> Bool
eval PointedModelS5
pm Form
f Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== PointedModelS5 -> Form -> Bool
eval PointedModelS5
pm Form
g
eval PointedModelS5
pm (Forall [Prp]
ps Form
f) = PointedModelS5 -> Form -> Bool
eval PointedModelS5
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 PointedModelS5
pm (Exists [Prp]
ps Form
f) = PointedModelS5 -> Form -> Bool
eval PointedModelS5
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 (m :: KripkeModelS5
m@(KrMS5 [Int]
_ [(Agent, [[Int]])]
rel [(Int, Assignment)]
_),Int
w) (K Agent
ag Form
form) = (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Int
w' -> PointedModelS5 -> Form -> Bool
eval (KripkeModelS5
m,Int
w') Form
form) [Int]
vs where
  vs :: [Int]
vs = [[Int]] -> [Int]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Int]] -> [Int]) -> [[Int]] -> [Int]
forall a b. (a -> b) -> a -> b
$ ([Int] -> Bool) -> [[Int]] -> [[Int]]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Int
w) ([(Agent, [[Int]])] -> Agent -> [[Int]]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [(Agent, [[Int]])]
rel Agent
ag)
eval (m :: KripkeModelS5
m@(KrMS5 [Int]
_ [(Agent, [[Int]])]
rel [(Int, Assignment)]
_),Int
w) (Kw Agent
ag Form
form) = (Int -> Bool) -> [Int] -> Bool
forall b a. Eq b => (a -> b) -> [a] -> Bool
alleqWith (\Int
w' -> PointedModelS5 -> Form -> Bool
eval (KripkeModelS5
m,Int
w') Form
form) [Int]
vs where
  vs :: [Int]
vs = [[Int]] -> [Int]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Int]] -> [Int]) -> [[Int]] -> [Int]
forall a b. (a -> b) -> a -> b
$ ([Int] -> Bool) -> [[Int]] -> [[Int]]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Int
w) ([(Agent, [[Int]])] -> Agent -> [[Int]]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [(Agent, [[Int]])]
rel Agent
ag)
eval (m :: KripkeModelS5
m@(KrMS5 [Int]
_ [(Agent, [[Int]])]
rel [(Int, Assignment)]
_),Int
w) (Ck [Agent]
ags Form
form) = (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Int
w' -> PointedModelS5 -> Form -> Bool
eval (KripkeModelS5
m,Int
w') Form
form) [Int]
vs where
  vs :: [Int]
vs    = [[Int]] -> [Int]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Int]] -> [Int]) -> [[Int]] -> [Int]
forall a b. (a -> b) -> a -> b
$ ([Int] -> Bool) -> [[Int]] -> [[Int]]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Int
w) [[Int]]
ckrel
  ckrel :: [[Int]]
ckrel = [[Int]] -> [[Int]]
forall a. Ord a => [[a]] -> [[a]]
fusion ([[Int]] -> [[Int]]) -> [[Int]] -> [[Int]]
forall a b. (a -> b) -> a -> b
$ [[[Int]]] -> [[Int]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [(Agent, [[Int]])] -> Agent -> [[Int]]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [(Agent, [[Int]])]
rel Agent
i | Agent
i <- [Agent]
ags ]
eval (m :: KripkeModelS5
m@(KrMS5 [Int]
_ [(Agent, [[Int]])]
rel [(Int, Assignment)]
_),Int
w) (Ckw [Agent]
ags Form
form) = (Int -> Bool) -> [Int] -> Bool
forall b a. Eq b => (a -> b) -> [a] -> Bool
alleqWith (\Int
w' -> PointedModelS5 -> Form -> Bool
eval (KripkeModelS5
m,Int
w') Form
form) [Int]
vs where
  vs :: [Int]
vs    = [[Int]] -> [Int]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Int]] -> [Int]) -> [[Int]] -> [Int]
forall a b. (a -> b) -> a -> b
$ ([Int] -> Bool) -> [[Int]] -> [[Int]]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Int
w) [[Int]]
ckrel
  ckrel :: [[Int]]
ckrel = [[Int]] -> [[Int]]
forall a. Ord a => [[a]] -> [[a]]
fusion ([[Int]] -> [[Int]]) -> [[Int]] -> [[Int]]
forall a b. (a -> b) -> a -> b
$ [[[Int]]] -> [[Int]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [(Agent, [[Int]])] -> Agent -> [[Int]]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [(Agent, [[Int]])]
rel Agent
i | Agent
i <- [Agent]
ags ]
eval (m :: KripkeModelS5
m@(KrMS5 [Int]
worlds [(Agent, [[Int]])]
rel [(Int, Assignment)]
_),Int
w) (Dk [Agent]
ags Form
form) = (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Int
w' -> PointedModelS5 -> Form -> Bool
eval (KripkeModelS5
m,Int
w') Form
form) [Int]
vs where
  vs :: [Int]
vs    = [[Int]] -> [Int]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Int]] -> [Int]) -> [[Int]] -> [Int]
forall a b. (a -> b) -> a -> b
$ ([Int] -> Bool) -> [[Int]] -> [[Int]]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Int
w) [[Int]]
dkrel
  dkrel :: [[Int]]
dkrel = [Int] -> [[[Int]]] -> [[Int]]
forall a. Ord a => [a] -> [Erel a] -> Erel a
intersection [Int]
worlds [ [(Agent, [[Int]])] -> Agent -> [[Int]]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [(Agent, [[Int]])]
rel Agent
i | Agent
i <- [Agent]
ags ]
eval (m :: KripkeModelS5
m@(KrMS5 [Int]
worlds [(Agent, [[Int]])]
rel [(Int, Assignment)]
_),Int
w) (Dkw [Agent]
ags Form
form) = (Int -> Bool) -> [Int] -> Bool
forall b a. Eq b => (a -> b) -> [a] -> Bool
alleqWith (\Int
w' -> PointedModelS5 -> Form -> Bool
eval (KripkeModelS5
m,Int
w') Form
form) [Int]
vs where
  vs :: [Int]
vs    = [[Int]] -> [Int]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Int]] -> [Int]) -> [[Int]] -> [Int]
forall a b. (a -> b) -> a -> b
$ ([Int] -> Bool) -> [[Int]] -> [[Int]]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Int
w) [[Int]]
dkrel
  dkrel :: [[Int]]
dkrel = [Int] -> [[[Int]]] -> [[Int]]
forall a. Ord a => [a] -> [Erel a] -> Erel a
intersection [Int]
worlds [ [(Agent, [[Int]])] -> Agent -> [[Int]]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [(Agent, [[Int]])]
rel Agent
i | Agent
i <- [Agent]
ags ]
eval PointedModelS5
pm (PubAnnounce Form
form1 Form
form2) =
  Bool -> Bool
not (PointedModelS5 -> Form -> Bool
eval PointedModelS5
pm Form
form1) Bool -> Bool -> Bool
|| PointedModelS5 -> Form -> Bool
eval (PointedModelS5 -> Form -> PointedModelS5
forall a b. Update a b => a -> b -> a
update PointedModelS5
pm Form
form1) Form
form2
eval PointedModelS5
pm (PubAnnounceW Form
form1 Form
form2) =
  if PointedModelS5 -> Form -> Bool
eval PointedModelS5
pm Form
form1
    then PointedModelS5 -> Form -> Bool
eval (PointedModelS5 -> Form -> PointedModelS5
forall a b. Update a b => a -> b -> a
update PointedModelS5
pm Form
form1) Form
form2
    else PointedModelS5 -> Form -> Bool
eval (PointedModelS5 -> Form -> PointedModelS5
forall a b. Update a b => a -> b -> a
update PointedModelS5
pm (Form -> Form
Neg Form
form1)) Form
form2
eval PointedModelS5
pm (Announce [Agent]
ags Form
form1 Form
form2) =
  Bool -> Bool
not (PointedModelS5 -> Form -> Bool
eval PointedModelS5
pm Form
form1) Bool -> Bool -> Bool
|| PointedModelS5 -> Form -> Bool
eval (PointedModelS5 -> [Agent] -> Form -> PointedModelS5
announce PointedModelS5
pm [Agent]
ags Form
form1) Form
form2
eval PointedModelS5
pm (AnnounceW [Agent]
ags Form
form1 Form
form2) =
  if PointedModelS5 -> Form -> Bool
eval PointedModelS5
pm Form
form1
    then PointedModelS5 -> Form -> Bool
eval (PointedModelS5 -> [Agent] -> Form -> PointedModelS5
announce PointedModelS5
pm [Agent]
ags Form
form1) Form
form2
    else PointedModelS5 -> Form -> Bool
eval (PointedModelS5 -> [Agent] -> Form -> PointedModelS5
announce PointedModelS5
pm [Agent]
ags (Form -> Form
Neg Form
form1)) Form
form2
eval PointedModelS5
pm (Dia (Dyn Agent
dynLabel Dynamic
d) Form
f) = case Dynamic -> Maybe PointedActionModelS5
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
d of
  Just PointedActionModelS5
pactm -> PointedModelS5 -> Form -> Bool
eval PointedModelS5
pm (PointedActionModelS5 -> Form
forall a. HasPrecondition a => a -> Form
preOf (PointedActionModelS5
pactm :: PointedActionModelS5)) Bool -> Bool -> Bool
&& PointedModelS5 -> Form -> Bool
eval (PointedModelS5
pm PointedModelS5 -> PointedActionModelS5 -> PointedModelS5
forall a b. Update a b => a -> b -> a
`update` PointedActionModelS5
pactm) Form
f
  Maybe PointedActionModelS5
Nothing    -> case Dynamic -> Maybe MultipointedActionModelS5
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
d of
    Just MultipointedActionModelS5
mpactm -> PointedModelS5 -> Form -> Bool
eval PointedModelS5
pm (MultipointedActionModelS5 -> Form
forall a. HasPrecondition a => a -> Form
preOf (MultipointedActionModelS5
mpactm :: MultipointedActionModelS5)) Bool -> Bool -> Bool
&& PointedModelS5 -> Form -> Bool
eval (PointedModelS5
pm PointedModelS5 -> MultipointedActionModelS5 -> PointedModelS5
forall a b. Update a b => a -> b -> a
`update` MultipointedActionModelS5
mpactm) Form
f
    Maybe MultipointedActionModelS5
Nothing     -> Agent -> Bool
forall a. HasCallStack => Agent -> a
error (Agent -> Bool) -> Agent -> Bool
forall a b. (a -> b) -> a -> b
$ Agent
"cannot update S5 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

valid :: KripkeModelS5 -> Form -> Bool
valid :: KripkeModelS5 -> Form -> Bool
valid m :: KripkeModelS5
m@(KrMS5 [Int]
worlds [(Agent, [[Int]])]
_ [(Int, Assignment)]
_) Form
f = (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Int
w -> PointedModelS5 -> Form -> Bool
eval (KripkeModelS5
m,Int
w) Form
f) [Int]
worlds

instance Semantics KripkeModelS5 where
  isTrue :: KripkeModelS5 -> Form -> Bool
isTrue KripkeModelS5
m Form
f = (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Int
w -> PointedModelS5 -> Form -> Bool
forall a. Semantics a => a -> Form -> Bool
isTrue (KripkeModelS5
m,Int
w) Form
f) (KripkeModelS5 -> [Int]
forall a. HasWorlds a => a -> [Int]
worldsOf KripkeModelS5
m)

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

instance Semantics MultipointedModelS5 where
  isTrue :: MultipointedModelS5 -> Form -> Bool
isTrue (KripkeModelS5
m,[Int]
ws) Form
f = (Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Int
w -> PointedModelS5 -> Form -> Bool
forall a. Semantics a => a -> Form -> Bool
isTrue (KripkeModelS5
m,Int
w) Form
f) [Int]
ws

-- | Public announcements on Kripke models.
instance Update KripkeModelS5 Form where
  checks :: [KripkeModelS5 -> Form -> Bool]
checks = [] -- allow updating with formulas that are not globally true.
  unsafeUpdate :: KripkeModelS5 -> Form -> KripkeModelS5
unsafeUpdate m :: KripkeModelS5
m@(KrMS5 [Int]
sts [(Agent, [[Int]])]
rel [(Int, Assignment)]
val) Form
form = [Int] -> [(Agent, [[Int]])] -> [(Int, Assignment)] -> KripkeModelS5
KrMS5 [Int]
newsts [(Agent, [[Int]])]
newrel [(Int, Assignment)]
newval where
    newsts :: [Int]
newsts = (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (\Int
s -> PointedModelS5 -> Form -> Bool
eval (KripkeModelS5
m,Int
s) Form
form) [Int]
sts
    newrel :: [(Agent, [[Int]])]
newrel = ((Agent, [[Int]]) -> (Agent, [[Int]]))
-> [(Agent, [[Int]])] -> [(Agent, [[Int]])]
forall a b. (a -> b) -> [a] -> [b]
map (([[Int]] -> [[Int]]) -> (Agent, [[Int]]) -> (Agent, [[Int]])
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 [[Int]] -> [[Int]]
relfil) [(Agent, [[Int]])]
rel
    relfil :: [[Int]] -> [[Int]]
relfil = ([Int] -> Bool) -> [[Int]] -> [[Int]]
forall a. (a -> Bool) -> [a] -> [a]
filter ([][Int] -> [Int] -> Bool
forall a. Eq a => a -> a -> Bool
/=) ([[Int]] -> [[Int]]) -> ([[Int]] -> [[Int]]) -> [[Int]] -> [[Int]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Int] -> [Int]) -> [[Int]] -> [[Int]]
forall a b. (a -> b) -> [a] -> [b]
map ((Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
newsts))
    newval :: [(Int, Assignment)]
newval = ((Int, Assignment) -> Bool)
-> [(Int, Assignment)] -> [(Int, Assignment)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Int, Assignment)
p -> (Int, Assignment) -> Int
forall a b. (a, b) -> a
fst (Int, Assignment)
p Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
newsts) [(Int, Assignment)]
val

instance Update PointedModelS5 Form where
  unsafeUpdate :: PointedModelS5 -> Form -> PointedModelS5
unsafeUpdate (KripkeModelS5
m,Int
w) Form
f = (KripkeModelS5 -> Form -> KripkeModelS5
forall a b. Update a b => a -> b -> a
unsafeUpdate KripkeModelS5
m Form
f, Int
w)

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

announce :: PointedModelS5 -> [Agent] -> Form -> PointedModelS5
announce :: PointedModelS5 -> [Agent] -> Form -> PointedModelS5
announce pm :: PointedModelS5
pm@(m :: KripkeModelS5
m@(KrMS5 [Int]
sts [(Agent, [[Int]])]
rel [(Int, Assignment)]
val), Int
cur) [Agent]
ags Form
form =
  if PointedModelS5 -> Form -> Bool
eval PointedModelS5
pm Form
form then ([Int] -> [(Agent, [[Int]])] -> [(Int, Assignment)] -> KripkeModelS5
KrMS5 [Int]
sts [(Agent, [[Int]])]
newrel [(Int, Assignment)]
val, Int
cur)
                  else Agent -> PointedModelS5
forall a. HasCallStack => Agent -> a
error Agent
"announce failed: Liar!"
  where
    split :: [Int] -> [[Int]]
split [Int]
ws = ([Int] -> [Int]) -> [[Int]] -> [[Int]]
forall a b. (a -> b) -> [a] -> [b]
map [Int] -> [Int]
forall a. Ord a => [a] -> [a]
sort([[Int]] -> [[Int]])
-> (([Int], [Int]) -> [[Int]]) -> ([Int], [Int]) -> [[Int]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(\([Int]
x,[Int]
y) -> [[Int]
x,[Int]
y]) (([Int], [Int]) -> [[Int]]) -> ([Int], [Int]) -> [[Int]]
forall a b. (a -> b) -> a -> b
$ (Int -> Bool) -> [Int] -> ([Int], [Int])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\Int
s -> PointedModelS5 -> Form -> Bool
eval (KripkeModelS5
m,Int
s) Form
form) [Int]
ws
    newrel :: [(Agent, [[Int]])]
newrel = ((Agent, [[Int]]) -> (Agent, [[Int]]))
-> [(Agent, [[Int]])] -> [(Agent, [[Int]])]
forall a b. (a -> b) -> [a] -> [b]
map (Agent, [[Int]]) -> (Agent, [[Int]])
nrel [(Agent, [[Int]])]
rel
    nrel :: (Agent, [[Int]]) -> (Agent, [[Int]])
nrel (Agent
i,[[Int]]
ri) | Agent
i Agent -> [Agent] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Agent]
ags = (Agent
i, ([Int] -> [[Int]]) -> [[Int]] -> [[Int]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (([Int] -> Bool) -> [[Int]] -> [[Int]]
forall a. (a -> Bool) -> [a] -> [a]
filter ([][Int] -> [Int] -> Bool
forall a. Eq a => a -> a -> Bool
/=) ([[Int]] -> [[Int]]) -> ([Int] -> [[Int]]) -> [Int] -> [[Int]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> [[Int]]
split) [[Int]]
ri)
                | Bool
otherwise    = (Agent
i,[[Int]]
ri)

announceAction :: [Agent] -> [Agent] -> Form -> PointedActionModelS5
announceAction :: [Agent] -> [Agent] -> Form -> PointedActionModelS5
announceAction [Agent]
everyone [Agent]
listeners Form
f = (ActionModelS5
am, Int
1) where
  am :: ActionModelS5
am = [(Int, (Form, PostCondition))]
-> [(Agent, [[Int]])] -> ActionModelS5
ActMS5 -- [(Action,(Form,PostCondition))] [(Agent,Partition)]
    [ (Int
1, (Form
f, [])), (Int
2, (Form
Top, [])) ]
    [ (Agent
i, if Agent
i Agent -> [Agent] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Agent]
listeners then [[Int
1],[Int
2]] else [[Int
1,Int
2]] ) | Agent
i <- [Agent]
everyone ]

instance KripkeLike KripkeModelS5 where
  directed :: KripkeModelS5 -> Bool
directed = Bool -> KripkeModelS5 -> Bool
forall a b. a -> b -> a
const Bool
False
  getNodes :: KripkeModelS5 -> [(Agent, Agent)]
getNodes (KrMS5 [Int]
ws [(Agent, [[Int]])]
_ [(Int, Assignment)]
val) = (Int -> (Agent, Agent)) -> [Int] -> [(Agent, Agent)]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Agent
forall a. Show a => a -> Agent
show (Int -> Agent) -> (Int -> Agent) -> Int -> (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')
&&& Int -> Agent
labelOf) [Int]
ws where
    labelOf :: Int -> Agent
labelOf Int
w = Assignment -> Agent
forall a. TexAble a => a -> Agent
tex (Assignment -> Agent) -> Assignment -> Agent
forall a b. (a -> b) -> a -> b
$ [(Int, Assignment)] -> Int -> Assignment
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [(Int, Assignment)]
val Int
w
  getEdges :: KripkeModelS5 -> [(Agent, Agent, Agent)]
getEdges (KrMS5 [Int]
_ [(Agent, [[Int]])]
rel [(Int, Assignment)]
_) =
    [(Agent, Agent, Agent)] -> [(Agent, Agent, Agent)]
forall a. Eq a => [a] -> [a]
nub [ (Agent
a,Int -> Agent
forall a. Show a => a -> Agent
show Int
x,Int -> Agent
forall a. Show a => a -> Agent
show Int
y) | Agent
a <- ((Agent, [[Int]]) -> Agent) -> [(Agent, [[Int]])] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map (Agent, [[Int]]) -> Agent
forall a b. (a, b) -> a
fst [(Agent, [[Int]])]
rel, [Int]
part <- [(Agent, [[Int]])] -> Agent -> [[Int]]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [(Agent, [[Int]])]
rel Agent
a, Int
x <- [Int]
part, Int
y <- [Int]
part, Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
y ]

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

instance KripkeLike PointedModelS5 where
  directed :: PointedModelS5 -> Bool
directed = KripkeModelS5 -> Bool
forall a. KripkeLike a => a -> Bool
directed (KripkeModelS5 -> Bool)
-> (PointedModelS5 -> KripkeModelS5) -> PointedModelS5 -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PointedModelS5 -> KripkeModelS5
forall a b. (a, b) -> a
fst
  getNodes :: PointedModelS5 -> [(Agent, Agent)]
getNodes = KripkeModelS5 -> [(Agent, Agent)]
forall a. KripkeLike a => a -> [(Agent, Agent)]
getNodes (KripkeModelS5 -> [(Agent, Agent)])
-> (PointedModelS5 -> KripkeModelS5)
-> PointedModelS5
-> [(Agent, Agent)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PointedModelS5 -> KripkeModelS5
forall a b. (a, b) -> a
fst
  getEdges :: PointedModelS5 -> [(Agent, Agent, Agent)]
getEdges = KripkeModelS5 -> [(Agent, Agent, Agent)]
forall a. KripkeLike a => a -> [(Agent, Agent, Agent)]
getEdges (KripkeModelS5 -> [(Agent, Agent, Agent)])
-> (PointedModelS5 -> KripkeModelS5)
-> PointedModelS5
-> [(Agent, Agent, Agent)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PointedModelS5 -> KripkeModelS5
forall a b. (a, b) -> a
fst
  getActuals :: PointedModelS5 -> [Agent]
getActuals (KripkeModelS5
_, Int
cur) = [Int -> Agent
forall a. Show a => a -> Agent
show Int
cur]

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

instance KripkeLike MultipointedModelS5 where
  directed :: MultipointedModelS5 -> Bool
directed = KripkeModelS5 -> Bool
forall a. KripkeLike a => a -> Bool
directed (KripkeModelS5 -> Bool)
-> (MultipointedModelS5 -> KripkeModelS5)
-> MultipointedModelS5
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MultipointedModelS5 -> KripkeModelS5
forall a b. (a, b) -> a
fst
  getNodes :: MultipointedModelS5 -> [(Agent, Agent)]
getNodes = KripkeModelS5 -> [(Agent, Agent)]
forall a. KripkeLike a => a -> [(Agent, Agent)]
getNodes (KripkeModelS5 -> [(Agent, Agent)])
-> (MultipointedModelS5 -> KripkeModelS5)
-> MultipointedModelS5
-> [(Agent, Agent)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MultipointedModelS5 -> KripkeModelS5
forall a b. (a, b) -> a
fst
  getEdges :: MultipointedModelS5 -> [(Agent, Agent, Agent)]
getEdges = KripkeModelS5 -> [(Agent, Agent, Agent)]
forall a. KripkeLike a => a -> [(Agent, Agent, Agent)]
getEdges (KripkeModelS5 -> [(Agent, Agent, Agent)])
-> (MultipointedModelS5 -> KripkeModelS5)
-> MultipointedModelS5
-> [(Agent, Agent, Agent)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MultipointedModelS5 -> KripkeModelS5
forall a b. (a, b) -> a
fst
  getActuals :: MultipointedModelS5 -> [Agent]
getActuals (KripkeModelS5
_, [Int]
curs) = (Int -> Agent) -> [Int] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Agent
forall a. Show a => a -> Agent
show [Int]
curs

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

type Bisimulation = [(World,World)]

checkBisim :: Bisimulation -> KripkeModelS5 -> KripkeModelS5 -> Bool
checkBisim :: [(Int, Int)] -> KripkeModelS5 -> KripkeModelS5 -> Bool
checkBisim [] KripkeModelS5
_                   KripkeModelS5
_                     = Bool
False
checkBisim [(Int, Int)]
z  m1 :: KripkeModelS5
m1@(KrMS5 [Int]
_ [(Agent, [[Int]])]
rel1 [(Int, Assignment)]
val1) m2 :: KripkeModelS5
m2@(KrMS5 [Int]
_ [(Agent, [[Int]])]
rel2 [(Int, Assignment)]
val2) =
  ((Int, Int) -> Bool) -> [(Int, Int)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\(Int
w1,Int
w2) ->
        ([(Int, Assignment)]
val1 [(Int, Assignment)] -> Int -> Assignment
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Int
w1 Assignment -> Assignment -> Bool
forall a. Eq a => a -> a -> Bool
== [(Int, Assignment)]
val2 [(Int, Assignment)] -> Int -> Assignment
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Int
w2)  -- same valuation
    Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [ ([Int] -> Bool) -> [[Int]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Int
v2 -> (Int
v1,Int
v2) (Int, Int) -> [(Int, Int)] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [(Int, Int)]
z)) (([Int] -> Bool) -> [[Int]] -> [[Int]]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Int
w2) ([(Agent, [[Int]])]
rel2 [(Agent, [[Int]])] -> Agent -> [[Int]]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Agent
ag)) -- forth
           | Agent
ag <- KripkeModelS5 -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf KripkeModelS5
m1, Int
v1 <- [[Int]] -> [Int]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Int]] -> [Int]) -> [[Int]] -> [Int]
forall a b. (a -> b) -> a -> b
$ ([Int] -> Bool) -> [[Int]] -> [[Int]]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Int
w1) ([(Agent, [[Int]])]
rel1 [(Agent, [[Int]])] -> Agent -> [[Int]]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Agent
ag) ]
    Bool -> Bool -> Bool
&& [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [ ([Int] -> Bool) -> [[Int]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Int
v1 -> (Int
v1,Int
v2) (Int, Int) -> [(Int, Int)] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [(Int, Int)]
z)) (([Int] -> Bool) -> [[Int]] -> [[Int]]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Int
w1) ([(Agent, [[Int]])]
rel1 [(Agent, [[Int]])] -> Agent -> [[Int]]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Agent
ag)) -- back
           | Agent
ag <- KripkeModelS5 -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf KripkeModelS5
m2, Int
v2 <- [[Int]] -> [Int]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Int]] -> [Int]) -> [[Int]] -> [Int]
forall a b. (a -> b) -> a -> b
$ ([Int] -> Bool) -> [[Int]] -> [[Int]]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Int
w2) ([(Agent, [[Int]])]
rel2 [(Agent, [[Int]])] -> Agent -> [[Int]]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Agent
ag) ]
      ) [(Int, Int)]
z

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

generatedSubmodel :: PointedModelS5 -> PointedModelS5
generatedSubmodel :: PointedModelS5 -> PointedModelS5
generatedSubmodel (KrMS5 [Int]
oldWorlds [(Agent, [[Int]])]
rel [(Int, Assignment)]
val, Int
cur) =
  if Int
cur Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [Int]
oldWorlds
    then Agent -> PointedModelS5
forall a. HasCallStack => Agent -> a
error Agent
"Actual world is not in the model!"
    else ([Int] -> [(Agent, [[Int]])] -> [(Int, Assignment)] -> KripkeModelS5
KrMS5 [Int]
newWorlds [(Agent, [[Int]])]
newrel [(Int, Assignment)]
newval, Int
cur) where
      newWorlds :: [World]
      newWorlds :: [Int]
newWorlds = ([Int] -> [Int]) -> [Int] -> [Int]
forall a. Eq a => (a -> a) -> a -> a
lfp [Int] -> [Int]
forall {t :: * -> *}. Foldable t => t Int -> [Int]
follow [Int
cur] where
        follow :: t Int -> [Int]
follow t Int
xs = [Int] -> [Int]
forall a. Ord a => [a] -> [a]
sort ([Int] -> [Int]) -> ([Int] -> [Int]) -> [Int] -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> [Int]
forall a. Eq a => [a] -> [a]
nub ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ [[Int]] -> [Int]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Int]
part | (Agent
_,[[Int]]
parts) <- [(Agent, [[Int]])]
rel, [Int]
part <- [[Int]]
parts, (Int -> Bool) -> t Int -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
part) t Int
xs ]
      newrel :: [(Agent, [[Int]])]
newrel = ((Agent, [[Int]]) -> (Agent, [[Int]]))
-> [(Agent, [[Int]])] -> [(Agent, [[Int]])]
forall a b. (a -> b) -> [a] -> [b]
map (([[Int]] -> [[Int]]) -> (Agent, [[Int]]) -> (Agent, [[Int]])
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 (([[Int]] -> [[Int]]) -> (Agent, [[Int]]) -> (Agent, [[Int]]))
-> ([[Int]] -> [[Int]]) -> (Agent, [[Int]]) -> (Agent, [[Int]])
forall a b. (a -> b) -> a -> b
$ ([Int] -> Bool) -> [[Int]] -> [[Int]]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Int -> Bool) -> [Int] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
newWorlds))) [(Agent, [[Int]])]
rel
      newval :: [(Int, Assignment)]
newval = ((Int, Assignment) -> Bool)
-> [(Int, Assignment)] -> [(Int, Assignment)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Int, Assignment)
p -> (Int, Assignment) -> Int
forall a b. (a, b) -> a
fst (Int, Assignment)
p Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
newWorlds) [(Int, Assignment)]
val

bisimClasses :: KripkeModelS5 -> [[World]]
bisimClasses :: KripkeModelS5 -> [[Int]]
bisimClasses m :: KripkeModelS5
m@(KrMS5 [Int]
_ [(Agent, [[Int]])]
rel [(Int, Assignment)]
val) = [[Int]] -> [[Int]]
refine [[Int]]
sameAssignmentPartition where
  sameAssignmentPartition :: [[Int]]
sameAssignmentPartition =
    ([(Assignment, Int)] -> [Int]) -> [[(Assignment, Int)]] -> [[Int]]
forall a b. (a -> b) -> [a] -> [b]
map (((Assignment, Int) -> Int) -> [(Assignment, Int)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Assignment, Int) -> Int
forall a b. (a, b) -> b
snd)
      ([[(Assignment, Int)]] -> [[Int]])
-> [[(Assignment, Int)]] -> [[Int]]
forall a b. (a -> b) -> a -> b
$ ((Assignment, Int) -> (Assignment, Int) -> Bool)
-> [(Assignment, Int)] -> [[(Assignment, Int)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (\(Assignment, Int)
x (Assignment, Int)
y -> (Assignment, Int) -> Assignment
forall a b. (a, b) -> a
fst (Assignment, Int)
x Assignment -> Assignment -> Bool
forall a. Eq a => a -> a -> Bool
== (Assignment, Int) -> Assignment
forall a b. (a, b) -> a
fst (Assignment, Int)
y)
        ([(Assignment, Int)] -> [[(Assignment, Int)]])
-> [(Assignment, Int)] -> [[(Assignment, Int)]]
forall a b. (a -> b) -> a -> b
$ [(Assignment, Int)] -> [(Assignment, Int)]
forall a. Ord a => [a] -> [a]
sort (((Int, Assignment) -> (Assignment, Int))
-> [(Int, Assignment)] -> [(Assignment, Int)]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Assignment) -> (Assignment, Int)
forall a b. (a, b) -> (b, a)
swap [(Int, Assignment)]
val)
  refine :: [[Int]] -> [[Int]]
refine [[Int]]
parts = [[Int]] -> [[Int]]
forall a. Ord a => [a] -> [a]
sort ([[Int]] -> [[Int]]) -> [[Int]] -> [[Int]]
forall a b. (a -> b) -> a -> b
$ ([Int] -> [Int]) -> [[Int]] -> [[Int]]
forall a b. (a -> b) -> [a] -> [b]
map [Int] -> [Int]
forall a. Ord a => [a] -> [a]
sort ([[Int]] -> [[Int]]) -> [[Int]] -> [[Int]]
forall a b. (a -> b) -> a -> b
$ ([[Int]] -> Agent -> [[Int]]) -> [[Int]] -> [Agent] -> [[Int]]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl [[Int]] -> Agent -> [[Int]]
splitByAgent [[Int]]
parts (KripkeModelS5 -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf KripkeModelS5
m)
  splitByAgent :: [[Int]] -> Agent -> [[Int]]
splitByAgent [[Int]]
parts Agent
a =
    [[[Int]]] -> [[Int]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ ([Int] -> Bool) -> [[Int]] -> [[Int]]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> ([Int] -> Bool) -> [Int] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [ [Int]
ws [Int] -> [Int] -> [Int]
forall a. Eq a => [a] -> [a] -> [a]
`intersect` [Int]
aPart | [Int]
aPart <- [(Agent, [[Int]])]
rel [(Agent, [[Int]])] -> Agent -> [[Int]]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Agent
a ] | [Int]
ws <- [[Int]]
parts ]

checkBisimClasses :: KripkeModelS5 -> Bool
checkBisimClasses :: KripkeModelS5 -> Bool
checkBisimClasses KripkeModelS5
m =
  [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [ [(Int, Int)] -> PointedModelS5 -> PointedModelS5 -> Bool
checkBisimPointed (Int -> Int -> [(Int, Int)]
swapZ Int
w1 Int
w2) (KripkeModelS5
m,Int
w1) (KripkeModelS5
m,Int
w2)
      | [Int]
part <- KripkeModelS5 -> [[Int]]
bisimClasses KripkeModelS5
m, Int
w1 <- [Int]
part, Int
w2 <-[Int]
part, Int
w1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
w2 ] where
    swapZ :: Int -> Int -> [(Int, Int)]
swapZ Int
w1 Int
w2 = [(Int, Int)] -> [(Int, Int)]
forall a. Ord a => [a] -> [a]
sort ([(Int, Int)] -> [(Int, Int)]) -> [(Int, Int)] -> [(Int, Int)]
forall a b. (a -> b) -> a -> b
$ [(Int
w1,Int
w2),(Int
w2,Int
w1)] [(Int, Int)] -> [(Int, Int)] -> [(Int, Int)]
forall a. [a] -> [a] -> [a]
++ [ (Int
w,Int
w) | Int
w <- KripkeModelS5 -> [Int]
forall a. HasWorlds a => a -> [Int]
worldsOf KripkeModelS5
m [Int] -> [Int] -> [Int]
forall a. Eq a => [a] -> [a] -> [a]
\\ [Int
w1,Int
w2] ]

bisiminimize :: PointedModelS5 -> PointedModelS5
bisiminimize :: PointedModelS5 -> PointedModelS5
bisiminimize (KripkeModelS5
m,Int
w) =
  if ([Int] -> Bool) -> [[Int]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
1) (Int -> Bool) -> ([Int] -> Int) -> [Int] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length) (KripkeModelS5 -> [[Int]]
bisimClasses KripkeModelS5
m)
    then (KripkeModelS5
m,Int
w) -- nothing to minimize
    else ([Int] -> [(Agent, [[Int]])] -> [(Int, Assignment)] -> KripkeModelS5
KrMS5 [Int]
newWorlds [(Agent, [[Int]])]
newRel [(Int, Assignment)]
newVal, Int -> Int
copyFct Int
w) where
      KrMS5 [Int]
_ [(Agent, [[Int]])]
oldRel [(Int, Assignment)]
oldVal = KripkeModelS5
m
      copyRel :: [([Int], Int)]
copyRel      = [[Int]] -> [Int] -> [([Int], Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (KripkeModelS5 -> [[Int]]
bisimClasses KripkeModelS5
m) [Int
1..]
      copyFct :: Int -> Int
copyFct Int
wOld = ([Int], Int) -> Int
forall a b. (a, b) -> b
snd (([Int], Int) -> Int) -> ([Int], Int) -> Int
forall a b. (a -> b) -> a -> b
$ [([Int], Int)] -> ([Int], Int)
forall a. HasCallStack => [a] -> a
head ([([Int], Int)] -> ([Int], Int)) -> [([Int], Int)] -> ([Int], Int)
forall a b. (a -> b) -> a -> b
$ (([Int], Int) -> Bool) -> [([Int], Int)] -> [([Int], Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Int
wOld Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem`) ([Int] -> Bool) -> (([Int], Int) -> [Int]) -> ([Int], Int) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Int], Int) -> [Int]
forall a b. (a, b) -> a
fst) [([Int], Int)]
copyRel
      newWorlds :: [Int]
newWorlds    = (([Int], Int) -> Int) -> [([Int], Int)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map ([Int], Int) -> Int
forall a b. (a, b) -> b
snd [([Int], Int)]
copyRel
      newRel :: [(Agent, [[Int]])]
newRel       = [ (Agent
a,Agent -> [[Int]]
newRelFor Agent
a) | Agent
a <- KripkeModelS5 -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf KripkeModelS5
m ]
      newRelFor :: Agent -> [[Int]]
newRelFor Agent
a  = [ [Int] -> [Int]
forall a. Eq a => [a] -> [a]
nub [ Int -> Int
copyFct Int
wOld | Int
wOld <- [Int]
part ] |  [Int]
part <- [(Agent, [[Int]])]
oldRel [(Agent, [[Int]])] -> Agent -> [[Int]]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Agent
a ]
      newVal :: [(Int, Assignment)]
newVal       = [ (Int
wNew, [(Int, Assignment)]
oldVal [(Int, Assignment)] -> Int -> Assignment
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Int
wOld) | (Int
wOld:[Int]
_,Int
wNew) <- [([Int], Int)]
copyRel ]

instance Optimizable PointedModelS5 where
  optimize :: [Prp] -> PointedModelS5 -> PointedModelS5
optimize [Prp]
_ = PointedModelS5 -> PointedModelS5
bisiminimize (PointedModelS5 -> PointedModelS5)
-> (PointedModelS5 -> PointedModelS5)
-> PointedModelS5
-> PointedModelS5
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PointedModelS5 -> PointedModelS5
generatedSubmodel

type Action = Int
type PostCondition = [(Prp,Form)]

data ActionModelS5 = ActMS5 [(Action,(Form,PostCondition))] [(Agent,Partition)]
  deriving (ActionModelS5 -> ActionModelS5 -> Bool
(ActionModelS5 -> ActionModelS5 -> Bool)
-> (ActionModelS5 -> ActionModelS5 -> Bool) -> Eq ActionModelS5
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ActionModelS5 -> ActionModelS5 -> Bool
== :: ActionModelS5 -> ActionModelS5 -> Bool
$c/= :: ActionModelS5 -> ActionModelS5 -> Bool
/= :: ActionModelS5 -> ActionModelS5 -> Bool
Eq,Eq ActionModelS5
Eq ActionModelS5 =>
(ActionModelS5 -> ActionModelS5 -> Ordering)
-> (ActionModelS5 -> ActionModelS5 -> Bool)
-> (ActionModelS5 -> ActionModelS5 -> Bool)
-> (ActionModelS5 -> ActionModelS5 -> Bool)
-> (ActionModelS5 -> ActionModelS5 -> Bool)
-> (ActionModelS5 -> ActionModelS5 -> ActionModelS5)
-> (ActionModelS5 -> ActionModelS5 -> ActionModelS5)
-> Ord ActionModelS5
ActionModelS5 -> ActionModelS5 -> Bool
ActionModelS5 -> ActionModelS5 -> Ordering
ActionModelS5 -> ActionModelS5 -> ActionModelS5
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 :: ActionModelS5 -> ActionModelS5 -> Ordering
compare :: ActionModelS5 -> ActionModelS5 -> Ordering
$c< :: ActionModelS5 -> ActionModelS5 -> Bool
< :: ActionModelS5 -> ActionModelS5 -> Bool
$c<= :: ActionModelS5 -> ActionModelS5 -> Bool
<= :: ActionModelS5 -> ActionModelS5 -> Bool
$c> :: ActionModelS5 -> ActionModelS5 -> Bool
> :: ActionModelS5 -> ActionModelS5 -> Bool
$c>= :: ActionModelS5 -> ActionModelS5 -> Bool
>= :: ActionModelS5 -> ActionModelS5 -> Bool
$cmax :: ActionModelS5 -> ActionModelS5 -> ActionModelS5
max :: ActionModelS5 -> ActionModelS5 -> ActionModelS5
$cmin :: ActionModelS5 -> ActionModelS5 -> ActionModelS5
min :: ActionModelS5 -> ActionModelS5 -> ActionModelS5
Ord,Int -> ActionModelS5 -> ShowS
[ActionModelS5] -> ShowS
ActionModelS5 -> Agent
(Int -> ActionModelS5 -> ShowS)
-> (ActionModelS5 -> Agent)
-> ([ActionModelS5] -> ShowS)
-> Show ActionModelS5
forall a.
(Int -> a -> ShowS) -> (a -> Agent) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ActionModelS5 -> ShowS
showsPrec :: Int -> ActionModelS5 -> ShowS
$cshow :: ActionModelS5 -> Agent
show :: ActionModelS5 -> Agent
$cshowList :: [ActionModelS5] -> ShowS
showList :: [ActionModelS5] -> ShowS
Show)

instance HasAgents ActionModelS5 where
  agentsOf :: ActionModelS5 -> [Agent]
agentsOf (ActMS5 [(Int, (Form, PostCondition))]
_ [(Agent, [[Int]])]
rel) = ((Agent, [[Int]]) -> Agent) -> [(Agent, [[Int]])] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map (Agent, [[Int]]) -> Agent
forall a b. (a, b) -> a
fst [(Agent, [[Int]])]
rel

-- | A safe way to `lookup` all postconditions
safepost :: PostCondition -> Prp -> Form
safepost :: PostCondition -> Prp -> Form
safepost PostCondition
posts Prp
p = Form -> Maybe Form -> Form
forall a. a -> Maybe a -> a
fromMaybe (Prp -> Form
PrpF Prp
p) (Prp -> PostCondition -> Maybe Form
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Prp
p PostCondition
posts)

instance Pointed ActionModelS5 Action
type PointedActionModelS5 = (ActionModelS5, Action)

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

instance HasPrecondition PointedActionModelS5 where
  preOf :: PointedActionModelS5 -> Form
preOf (ActMS5 [(Int, (Form, PostCondition))]
acts [(Agent, [[Int]])]
_, Int
actual) = (Form, PostCondition) -> Form
forall a b. (a, b) -> a
fst ([(Int, (Form, PostCondition))]
acts [(Int, (Form, PostCondition))] -> Int -> (Form, PostCondition)
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Int
actual)

instance Pointed ActionModelS5 [Action]
type MultipointedActionModelS5 = (ActionModelS5,[Action])

instance HasPrecondition MultipointedActionModelS5 where
  preOf :: MultipointedActionModelS5 -> Form
preOf (ActionModelS5
am, [Int]
actuals) = [Form] -> Form
Disj [ PointedActionModelS5 -> Form
forall a. HasPrecondition a => a -> Form
preOf (ActionModelS5
am, Int
a) | Int
a <- [Int]
actuals ]

instance KripkeLike ActionModelS5 where
  directed :: ActionModelS5 -> Bool
directed = Bool -> ActionModelS5 -> Bool
forall a b. a -> b -> a
const Bool
False
  getNodes :: ActionModelS5 -> [(Agent, Agent)]
getNodes (ActMS5 [(Int, (Form, PostCondition))]
acts [(Agent, [[Int]])]
_) = ((Int, (Form, PostCondition)) -> (Agent, Agent))
-> [(Int, (Form, PostCondition))] -> [(Agent, Agent)]
forall a b. (a -> b) -> [a] -> [b]
map (Int, (Form, PostCondition)) -> (Agent, Agent)
forall {a} {a} {a} {a}.
(Show a, TexAble a, TexAble a, TexAble a) =>
(a, (a, [(a, a)])) -> (Agent, Agent)
labelOf [(Int, (Form, PostCondition))]
acts where
    labelOf :: (a, (a, [(a, a)])) -> (Agent, Agent)
labelOf (a
a,(a
pre,[(a, a)]
posts)) = (a -> Agent
forall a. Show a => a -> Agent
show a
a, [Agent] -> Agent
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
      [ Agent
"$\\begin{array}{c} ? " , a -> Agent
forall a. TexAble a => a -> Agent
tex a
pre, Agent
"\\\\"
      , Agent -> [Agent] -> Agent
forall a. [a] -> [[a]] -> [a]
intercalate Agent
"\\\\" (((a, a) -> Agent) -> [(a, a)] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map (a, a) -> Agent
forall {a} {a}. (TexAble a, TexAble a) => (a, a) -> Agent
showPost [(a, a)]
posts)
      , 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 :: ActionModelS5 -> [(Agent, Agent, Agent)]
getEdges am :: ActionModelS5
am@(ActMS5 [(Int, (Form, PostCondition))]
_ [(Agent, [[Int]])]
rel) =
    [(Agent, Agent, Agent)] -> [(Agent, Agent, Agent)]
forall a. Eq a => [a] -> [a]
nub [ (Agent
a, Int -> Agent
forall a. Show a => a -> Agent
show Int
x, Int -> Agent
forall a. Show a => a -> Agent
show Int
y) | Agent
a <- ActionModelS5 -> [Agent]
forall a. HasAgents a => a -> [Agent]
agentsOf ActionModelS5
am, [Int]
part <- [(Agent, [[Int]])]
rel [(Agent, [[Int]])] -> Agent -> [[Int]]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Agent
a, Int
x <- [Int]
part, Int
y <- [Int]
part, Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
y ]
  getActuals :: ActionModelS5 -> [Agent]
getActuals ActionModelS5
_ = [ ]
  nodeAts :: ActionModelS5 -> Bool -> Attributes
nodeAts ActionModelS5
_ Bool
True  = [Shape -> Attribute
shape Shape
BoxShape, Style -> Attribute
style Style
solid]
  nodeAts ActionModelS5
_ Bool
False = [Shape -> Attribute
shape Shape
BoxShape, Style -> Attribute
style Style
dashed]

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

instance KripkeLike PointedActionModelS5 where
  directed :: PointedActionModelS5 -> Bool
directed = ActionModelS5 -> Bool
forall a. KripkeLike a => a -> Bool
directed (ActionModelS5 -> Bool)
-> (PointedActionModelS5 -> ActionModelS5)
-> PointedActionModelS5
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PointedActionModelS5 -> ActionModelS5
forall a b. (a, b) -> a
fst
  getNodes :: PointedActionModelS5 -> [(Agent, Agent)]
getNodes = ActionModelS5 -> [(Agent, Agent)]
forall a. KripkeLike a => a -> [(Agent, Agent)]
getNodes (ActionModelS5 -> [(Agent, Agent)])
-> (PointedActionModelS5 -> ActionModelS5)
-> PointedActionModelS5
-> [(Agent, Agent)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PointedActionModelS5 -> ActionModelS5
forall a b. (a, b) -> a
fst
  getEdges :: PointedActionModelS5 -> [(Agent, Agent, Agent)]
getEdges = ActionModelS5 -> [(Agent, Agent, Agent)]
forall a. KripkeLike a => a -> [(Agent, Agent, Agent)]
getEdges (ActionModelS5 -> [(Agent, Agent, Agent)])
-> (PointedActionModelS5 -> ActionModelS5)
-> PointedActionModelS5
-> [(Agent, Agent, Agent)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PointedActionModelS5 -> ActionModelS5
forall a b. (a, b) -> a
fst
  getActuals :: PointedActionModelS5 -> [Agent]
getActuals (ActionModelS5
_, Int
cur) = [Int -> Agent
forall a. Show a => a -> Agent
show Int
cur]

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

instance KripkeLike MultipointedActionModelS5 where
  directed :: MultipointedActionModelS5 -> Bool
directed = ActionModelS5 -> Bool
forall a. KripkeLike a => a -> Bool
directed (ActionModelS5 -> Bool)
-> (MultipointedActionModelS5 -> ActionModelS5)
-> MultipointedActionModelS5
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MultipointedActionModelS5 -> ActionModelS5
forall a b. (a, b) -> a
fst
  getNodes :: MultipointedActionModelS5 -> [(Agent, Agent)]
getNodes = ActionModelS5 -> [(Agent, Agent)]
forall a. KripkeLike a => a -> [(Agent, Agent)]
getNodes (ActionModelS5 -> [(Agent, Agent)])
-> (MultipointedActionModelS5 -> ActionModelS5)
-> MultipointedActionModelS5
-> [(Agent, Agent)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MultipointedActionModelS5 -> ActionModelS5
forall a b. (a, b) -> a
fst
  getEdges :: MultipointedActionModelS5 -> [(Agent, Agent, Agent)]
getEdges = ActionModelS5 -> [(Agent, Agent, Agent)]
forall a. KripkeLike a => a -> [(Agent, Agent, Agent)]
getEdges (ActionModelS5 -> [(Agent, Agent, Agent)])
-> (MultipointedActionModelS5 -> ActionModelS5)
-> MultipointedActionModelS5
-> [(Agent, Agent, Agent)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MultipointedActionModelS5 -> ActionModelS5
forall a b. (a, b) -> a
fst
  getActuals :: MultipointedActionModelS5 -> [Agent]
getActuals (ActionModelS5
_, [Int]
curs) = (Int -> Agent) -> [Int] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Agent
forall a. Show a => a -> Agent
show [Int]
curs

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

instance Arbitrary ActionModelS5 where
  arbitrary :: Gen ActionModelS5
arbitrary = do
    BF Form
f <- (Int -> Gen BF) -> Gen BF
forall a. (Int -> Gen a) -> Gen a
sized ((Int -> Gen BF) -> Gen BF) -> (Int -> Gen BF) -> Gen BF
forall a b. (a -> b) -> a -> b
$ [Prp] -> Int -> Gen BF
randomboolformWith [Int -> Prp
P Int
0 .. Int -> Prp
P Int
4]
    BF Form
g <- (Int -> Gen BF) -> Gen BF
forall a. (Int -> Gen a) -> Gen a
sized ((Int -> Gen BF) -> Gen BF) -> (Int -> Gen BF) -> Gen BF
forall a b. (a -> b) -> a -> b
$ [Prp] -> Int -> Gen BF
randomboolformWith [Int -> Prp
P Int
0 .. Int -> Prp
P Int
4]
    BF Form
h <- (Int -> Gen BF) -> Gen BF
forall a. (Int -> Gen a) -> Gen a
sized ((Int -> Gen BF) -> Gen BF) -> (Int -> Gen BF) -> Gen BF
forall a b. (a -> b) -> a -> b
$ [Prp] -> Int -> Gen BF
randomboolformWith [Int -> Prp
P Int
0 .. Int -> Prp
P Int
4]
    PostCondition
myPost <- (\Int
_ -> do
      Prp
proptochange <- [Prp] -> Gen Prp
forall a. [a] -> Gen a
elements [Int -> Prp
P Int
0 .. Int -> Prp
P Int
4]
      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 [Int -> Prp
P Int
0 .. Int -> Prp
P Int
4]
      PostCondition -> Gen PostCondition
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return [ (Prp
proptochange, Form
postconcon) ]
      ) (Int
0::Action)
    ActionModelS5 -> Gen ActionModelS5
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (ActionModelS5 -> Gen ActionModelS5)
-> ActionModelS5 -> Gen ActionModelS5
forall a b. (a -> b) -> a -> b
$
      [(Int, (Form, PostCondition))]
-> [(Agent, [[Int]])] -> ActionModelS5
ActMS5
        [ (Int
0,(Form
Top,[]))
        , (Int
1,(Form
f  ,[]))
        , (Int
2,(Form
g  ,PostCondition
myPost))
        , (Int
3,(Form
h  ,[]))     ]
        ( (Agent
"0",[[Int
0],[Int
1],[Int
2],[Int
3]])(Agent, [[Int]]) -> [(Agent, [[Int]])] -> [(Agent, [[Int]])]
forall a. a -> [a] -> [a]
:[(Int -> Agent
forall a. Show a => a -> Agent
show Int
k,[[Int
0..Int
3::Int]]) | Int
k<-[Int
1..Int
5::Int] ])

instance Update KripkeModelS5 ActionModelS5 where
  checks :: [KripkeModelS5 -> ActionModelS5 -> Bool]
checks = [KripkeModelS5 -> ActionModelS5 -> Bool
forall a b. (HasAgents a, HasAgents b) => a -> b -> Bool
haveSameAgents]
  unsafeUpdate :: KripkeModelS5 -> ActionModelS5 -> KripkeModelS5
unsafeUpdate KripkeModelS5
m am :: ActionModelS5
am@(ActMS5 [(Int, (Form, PostCondition))]
acts [(Agent, [[Int]])]
_) =
    let (KripkeModelS5
newModel,[Int]
_) = MultipointedModelS5
-> MultipointedActionModelS5 -> MultipointedModelS5
forall a b. Update a b => a -> b -> a
unsafeUpdate (KripkeModelS5
m, KripkeModelS5 -> [Int]
forall a. HasWorlds a => a -> [Int]
worldsOf KripkeModelS5
m) (ActionModelS5
am, ((Int, (Form, PostCondition)) -> Int)
-> [(Int, (Form, PostCondition))] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, (Form, PostCondition)) -> Int
forall a b. (a, b) -> a
fst [(Int, (Form, PostCondition))]
acts) in KripkeModelS5
newModel

instance Update PointedModelS5 PointedActionModelS5 where
  checks :: [PointedModelS5 -> PointedActionModelS5 -> Bool]
checks = [PointedModelS5 -> PointedActionModelS5 -> Bool
forall a b. (HasAgents a, HasAgents b) => a -> b -> Bool
haveSameAgents,PointedModelS5 -> PointedActionModelS5 -> Bool
forall a b. Update a b => a -> b -> Bool
preCheck]
  unsafeUpdate :: PointedModelS5 -> PointedActionModelS5 -> PointedModelS5
unsafeUpdate (KripkeModelS5
m, Int
w) (ActionModelS5
actm, Int
a) = [Int] -> Int
forall a. HasCallStack => [a] -> a
head ([Int] -> Int) -> MultipointedModelS5 -> PointedModelS5
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MultipointedModelS5
-> MultipointedActionModelS5 -> MultipointedModelS5
forall a b. Update a b => a -> b -> a
unsafeUpdate (KripkeModelS5
m, [Int
w]) (ActionModelS5
actm, [Int
a])

instance Update PointedModelS5 MultipointedActionModelS5 where
  checks :: [PointedModelS5 -> MultipointedActionModelS5 -> Bool]
checks = [PointedModelS5 -> MultipointedActionModelS5 -> Bool
forall a b. (HasAgents a, HasAgents b) => a -> b -> Bool
haveSameAgents,PointedModelS5 -> MultipointedActionModelS5 -> Bool
forall a b. Update a b => a -> b -> Bool
preCheck]
  unsafeUpdate :: PointedModelS5 -> MultipointedActionModelS5 -> PointedModelS5
unsafeUpdate (KripkeModelS5
m, Int
w) MultipointedActionModelS5
mpactm = [Int] -> Int
forall a. HasCallStack => [a] -> a
head ([Int] -> Int) -> MultipointedModelS5 -> PointedModelS5
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MultipointedModelS5
-> MultipointedActionModelS5 -> MultipointedModelS5
forall a b. Update a b => a -> b -> a
unsafeUpdate (KripkeModelS5
m, [Int
w]) MultipointedActionModelS5
mpactm

instance Update MultipointedModelS5 PointedActionModelS5 where
  checks :: [MultipointedModelS5 -> PointedActionModelS5 -> Bool]
checks = [MultipointedModelS5 -> PointedActionModelS5 -> Bool
forall a b. (HasAgents a, HasAgents b) => a -> b -> Bool
haveSameAgents] -- do not check precondition!
  unsafeUpdate :: MultipointedModelS5 -> PointedActionModelS5 -> MultipointedModelS5
unsafeUpdate MultipointedModelS5
mpm (ActionModelS5
actm, Int
a) = MultipointedModelS5
-> MultipointedActionModelS5 -> MultipointedModelS5
forall a b. Update a b => a -> b -> a
unsafeUpdate MultipointedModelS5
mpm (ActionModelS5
actm, [Int
a])

instance Update MultipointedModelS5 MultipointedActionModelS5 where
  checks :: [MultipointedModelS5 -> MultipointedActionModelS5 -> Bool]
checks = [MultipointedModelS5 -> MultipointedActionModelS5 -> Bool
forall a b. (HasAgents a, HasAgents b) => a -> b -> Bool
haveSameAgents] -- do not check precondition!
  unsafeUpdate :: MultipointedModelS5
-> MultipointedActionModelS5 -> MultipointedModelS5
unsafeUpdate (m :: KripkeModelS5
m@(KrMS5 [Int]
oldWorlds [(Agent, [[Int]])]
oldrel [(Int, Assignment)]
oldval), [Int]
oldcurs) (ActMS5 [(Int, (Form, PostCondition))]
acts [(Agent, [[Int]])]
actrel, [Int]
factions) =
    ([Int] -> [(Agent, [[Int]])] -> [(Int, Assignment)] -> KripkeModelS5
KrMS5 [Int]
newWorlds [(Agent, [[Int]])]
newrel [(Int, Assignment)]
newval, [Int]
newcurs) where
      startcount :: Int
startcount        = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [Int]
oldWorlds Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
      copiesOf :: (Int, Int) -> [(Int, Int, Int)]
copiesOf (Int
s,Int
a)    = [ (Int
s, Int
a, Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
startcount Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
s) | PointedModelS5 -> Form -> Bool
eval (KripkeModelS5
m, Int
s) ((Form, PostCondition) -> Form
forall a b. (a, b) -> a
fst ((Form, PostCondition) -> Form) -> (Form, PostCondition) -> Form
forall a b. (a -> b) -> a -> b
$ [(Int, (Form, PostCondition))]
acts [(Int, (Form, PostCondition))] -> Int -> (Form, PostCondition)
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Int
a) ]
      newWorldsTriples :: [(Int, Int, Int)]
newWorldsTriples  = [[(Int, Int, Int)]] -> [(Int, Int, Int)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ (Int, Int) -> [(Int, Int, Int)]
copiesOf (Int
s,Int
a) | Int
s <- [Int]
oldWorlds, (Int
a,(Form, PostCondition)
_) <- [(Int, (Form, PostCondition))]
acts ]
      newWorlds :: [Int]
newWorlds         = ((Int, Int, Int) -> Int) -> [(Int, Int, Int)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (\(Int
_,Int
_,Int
x) -> Int
x) [(Int, Int, Int)]
newWorldsTriples
      newval :: [(Int, Assignment)]
newval            = ((Int, Int, Int) -> (Int, Assignment))
-> [(Int, Int, Int)] -> [(Int, Assignment)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Int
s,Int
a,Int
t) -> (Int
t, (Int, Int) -> Assignment
newValAt (Int
s,Int
a))) [(Int, Int, Int)]
newWorldsTriples where
        newValAt :: (Int, Int) -> Assignment
newValAt (Int, Int)
sa = [ (Prp
p, (Int, Int) -> Prp -> Bool
newValAtFor (Int, Int)
sa Prp
p) | Prp
p <- KripkeModelS5 -> [Prp]
forall a. HasVocab a => a -> [Prp]
vocabOf KripkeModelS5
m ]
        newValAtFor :: (Int, Int) -> Prp -> Bool
newValAtFor (Int
s,Int
a) Prp
p = case Prp -> PostCondition -> Maybe Form
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Prp
p ((Form, PostCondition) -> PostCondition
forall a b. (a, b) -> b
snd ([(Int, (Form, PostCondition))]
acts [(Int, (Form, PostCondition))] -> Int -> (Form, PostCondition)
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Int
a)) of
          Just Form
postOfP -> PointedModelS5 -> Form -> Bool
eval (KripkeModelS5
m, Int
s) Form
postOfP
          Maybe Form
Nothing      -> ([(Int, Assignment)]
oldval [(Int, Assignment)] -> Int -> Assignment
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Int
s) Assignment -> Prp -> Bool
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
! Prp
p
      listFor :: Agent -> [([Int], [Int])]
listFor Agent
ag        = [[Int]] -> [[Int]] -> [([Int], [Int])]
forall a b. [a] -> [b] -> [(a, b)]
cartProd ([(Agent, [[Int]])] -> Agent -> [[Int]]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [(Agent, [[Int]])]
oldrel Agent
ag) ([(Agent, [[Int]])] -> Agent -> [[Int]]
forall a b. (Show a, Show b, Eq a) => Rel a b -> a -> b
apply [(Agent, [[Int]])]
actrel Agent
ag)
      newPartsFor :: Agent -> [[(Int, Int)]]
newPartsFor Agent
ag    = [ [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
cartProd [Int]
as [Int]
bs | ([Int]
as,[Int]
bs) <- Agent -> [([Int], [Int])]
listFor Agent
ag ]
      translSingle :: (Int, Int) -> [Int]
translSingle (Int, Int)
pair = (Int -> Bool) -> [Int] -> [Int]
forall a. (a -> Bool) -> [a] -> [a]
filter (Int -> [Int] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Int]
newWorlds) ([Int] -> [Int]) -> [Int] -> [Int]
forall a b. (a -> b) -> a -> b
$ ((Int, Int, Int) -> Int) -> [(Int, Int, Int)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (\(Int
_,Int
_,Int
x) -> Int
x) ([(Int, Int, Int)] -> [Int]) -> [(Int, Int, Int)] -> [Int]
forall a b. (a -> b) -> a -> b
$ (Int, Int) -> [(Int, Int, Int)]
copiesOf (Int, Int)
pair
      transEqClass :: [(Int, Int)] -> [Int]
transEqClass      = ((Int, Int) -> [Int]) -> [(Int, Int)] -> [Int]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Int, Int) -> [Int]
translSingle
      nTransPartsFor :: Agent -> [[Int]]
nTransPartsFor Agent
ag = ([Int] -> Bool) -> [[Int]] -> [[Int]]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Int] -> [Int] -> Bool
forall a. Eq a => a -> a -> Bool
/= []) ([[Int]] -> [[Int]]) -> [[Int]] -> [[Int]]
forall a b. (a -> b) -> a -> b
$ ([(Int, Int)] -> [Int]) -> [[(Int, Int)]] -> [[Int]]
forall a b. (a -> b) -> [a] -> [b]
map [(Int, Int)] -> [Int]
transEqClass (Agent -> [[(Int, Int)]]
newPartsFor Agent
ag)
      newrel :: [(Agent, [[Int]])]
newrel            = [ (Agent
a, Agent -> [[Int]]
nTransPartsFor Agent
a)  | Agent
a <- ((Agent, [[Int]]) -> Agent) -> [(Agent, [[Int]])] -> [Agent]
forall a b. (a -> b) -> [a] -> [b]
map (Agent, [[Int]]) -> Agent
forall a b. (a, b) -> a
fst [(Agent, [[Int]])]
oldrel ]
      newcurs :: [Int]
newcurs           = [[Int]] -> [Int]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ ((Int, Int, Int) -> Int) -> [(Int, Int, Int)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (\(Int
_,Int
_,Int
x) -> Int
x) ([(Int, Int, Int)] -> [Int]) -> [(Int, Int, Int)] -> [Int]
forall a b. (a -> b) -> a -> b
$ (Int, Int) -> [(Int, Int, Int)]
copiesOf (Int
s,Int
a) | Int
s <- [Int]
oldcurs, Int
a <- [Int]
factions ]
      cartProd :: [a] -> [b] -> [(a, b)]
cartProd [a]
xs [b]
ys    = [ (a
x,b
y) | a
x <- [a]
xs, b
y <- [b]
ys ]