module SMCDEL.Examples.Toynabi where
import Data.List ((\\),sort)
import SMCDEL.Language
import SMCDEL.Symbolic.S5
import SMCDEL.Explicit.S5
import SMCDEL.Translations.S5
import SMCDEL.Other.Planning
cardIsAt :: Int -> Int -> Int -> Int -> Int -> Prp
cardIsAt :: Int -> Int -> Int -> Int -> Int -> Prp
cardIsAt Int
nPlayers Int
nCards Int
i Int
c Int
p = Int -> Prp
P ((Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
nCards Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
nPositions) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
nPositions) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
p) where
nPositions :: Int
nPositions = Double -> Int
forall b. Integral b => Double -> b
forall a b. (RealFrac a, Integral b) => a -> b
ceiling (Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
nCards Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
nPlayers :: Double)
toPlay :: Int -> Int -> Int -> Prp
toPlay :: Int -> Int -> Int -> Prp
toPlay Int
nPlayers Int
nCards Int
c = Int -> Prp
forall a. Enum a => Int -> a
toEnum (Int -> Prp) -> (Prp -> Int) -> Prp -> Prp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Int -> Int
forall a. Num a => a -> a -> a
+(Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
c)) (Int -> Int) -> (Prp -> Int) -> Prp -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Prp -> Int
forall a. Enum a => a -> Int
fromEnum (Prp -> Prp) -> Prp -> Prp
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Int -> Int -> Int -> Prp
cardIsAt Int
nPlayers Int
nCards Int
nPlayers (Int
nCardsInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (Int
nPositionsInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) where
nPositions :: Int
nPositions = Double -> Int
forall b. Integral b => Double -> b
forall a b. (RealFrac a, Integral b) => a -> b
ceiling (Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
nCards Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
nPlayers :: Double)
done :: Int -> Int -> Prp
done :: Int -> Int -> Prp
done Int
nPlayers Int
nCards = Int -> Int -> Int -> Prp
toPlay Int
nPlayers Int
nCards Int
nCards
vocab :: Int -> Int -> IO ()
vocab :: Int -> Int -> IO ()
vocab Int
nPlayers Int
nCards = do
(Prp -> IO ()) -> [Prp] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Prp -> IO ()
printExplain (MultipointedKnowScene -> [Prp]
forall a. HasVocab a => a -> [Prp]
vocabOf (MultipointedKnowScene -> [Prp]) -> MultipointedKnowScene -> [Prp]
forall a b. (a -> b) -> a -> b
$ Int -> Int -> MultipointedKnowScene
toynabiStartFor Int
nPlayers Int
nCards)
String -> IO ()
putStrLn String
"--"
(String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> IO ()
putStrLn [ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" has " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" @ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\t " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Prp -> String
forall a. Show a => a -> String
show (Int -> Int -> Int -> Int -> Int -> Prp
cardIsAt Int
nPlayers Int
nCards Int
i Int
c Int
p) | Int
i <- [Int]
players, Int
c <- [Int]
cards, Int
p <- [Int]
positions ]
(String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> IO ()
putStrLn [ String
"toPlay: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\t" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Prp -> String
forall a. Show a => a -> String
show (Int -> Int -> Int -> Prp
toPlay Int
nPlayers Int
nCards Int
c) | Int
c <- [Int]
cards ]
(String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> IO ()
putStrLn [ String
"done! \t" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Prp -> String
forall a. Show a => a -> String
show (Int -> Int -> Int -> Prp
toPlay Int
nPlayers Int
nCards Int
nCards) ]
where
printExplain :: Prp -> IO ()
printExplain Prp
p = String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ Prp -> String
forall a. Show a => a -> String
show Prp
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\t" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> Int -> Prp -> String
explain Int
nPlayers Int
nCards Prp
p
players :: [Int]
players = [Int
1..Int
nPlayers]
cards :: [Int]
cards = [Int
0..(Int
nCardsInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)]
nPositions :: Int
nPositions = Double -> Int
forall b. Integral b => Double -> b
forall a b. (RealFrac a, Integral b) => a -> b
ceiling (Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
nCards Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
nPlayers :: Double)
positions :: [Int]
positions = [Int
0..(Int
nPositionsInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)]
explain :: Int -> Int -> Prp -> String
explain :: Int -> Int -> Prp -> String
explain Int
nPlayers Int
nCards (P Int
k)
| Int -> Prp
P Int
k Prp -> Prp -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Int -> Int -> Prp
toPlay Int
nPlayers Int
nCards Int
nCards = String
"done!"
| Int -> Prp
P Int
k Prp -> Prp -> Bool
forall a. Ord a => a -> a -> Bool
>= Int -> Int -> Int -> Prp
toPlay Int
nPlayers Int
nCards Int
0 = String
"to play: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Prp -> Int
forall a. Enum a => a -> Int
fromEnum (Int -> Int -> Int -> Prp
toPlay Int
nPlayers Int
nCards Int
1))
| Bool
otherwise = Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" has " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" @ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
p where
nPositions :: Int
nPositions = Double -> Int
forall b. Integral b => Double -> b
forall a b. (RealFrac a, Integral b) => a -> b
ceiling (Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
nCards Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
nPlayers :: Double)
i :: Int
i = Int
k Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` (Int
nCards Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
nPositions)
c :: Int
c = (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
- (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
nCards Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
nPositions)) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
nPositions
p :: Int
p = Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
- (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
nCards Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
nPositions) Int -> Int -> Int
forall a. Num a => a -> a -> a
- (Int
c Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
nPositions)
explainState :: Int -> Int -> State -> String
explainState :: Int -> Int -> [Prp] -> String
explainState Int
nPlayers Int
nCards [Prp]
state = [[Int]] -> String
forall a. Show a => a -> String
show [ [ Int
c | Int
p <- [Int]
positions, Int
c <- [Int]
cards, Int -> Int -> Int -> Int -> Int -> Prp
cardIsAt Int
nPlayers Int
nCards Int
i Int
c Int
p Prp -> [Prp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Prp]
state ] | Int
i <- [Int]
players ] String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tP where
players :: [Int]
players = [Int
1..Int
nPlayers]
cards :: [Int]
cards = [Int
0..(Int
nCardsInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)]
nPositions :: Int
nPositions = Double -> Int
forall b. Integral b => Double -> b
forall a b. (RealFrac a, Integral b) => a -> b
ceiling (Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
nCards Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
nPlayers :: Double)
positions :: [Int]
positions = [Int
0..(Int
nPositionsInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)]
tP :: String
tP = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [ String
" to play: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
c | Int
c <- [Int]
cards, Int -> Int -> Int -> Prp
toPlay Int
nPlayers Int
nCards Int
c Prp -> [Prp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Prp]
state ]
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"done!" | Int -> Int -> Int -> Prp
toPlay Int
nPlayers Int
nCards Int
nCards Prp -> [Prp] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Prp]
state ]
toynabiStartFor :: Int -> Int -> MultipointedKnowScene
toynabiStartFor :: Int -> Int -> MultipointedKnowScene
toynabiStartFor Int
nPlayers Int
nCards = ([Prp] -> Bdd -> [(String, [Prp])] -> KnowStruct
KnS [Prp]
voc Bdd
law [(String, [Prp])]
obs, Bdd
cur) where
players :: [Int]
players = [Int
1..Int
nPlayers]
cards :: [Int]
cards = [Int
0..(Int
nCardsInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)]
nPositions :: Int
nPositions = Double -> Int
forall b. Integral b => Double -> b
forall a b. (RealFrac a, Integral b) => a -> b
ceiling (Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
nCards Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
nPlayers :: Double)
positions :: [Int]
positions = [Int
0..(Int
nPositionsInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)]
voc :: [Prp]
voc = [Prp] -> [Prp]
forall a. Ord a => [a] -> [a]
sort ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ [ Int -> Int -> Int -> Int -> Int -> Prp
cardIsAt Int
nPlayers Int
nCards Int
i Int
c Int
p | Int
i <- [Int]
players, Int
c <- [Int]
cards, Int
p <- [Int]
positions ]
[Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ [ Int -> Int -> Int -> Prp
toPlay Int
nPlayers Int
nCards Int
c | Int
c <- [Int]
cards ]
[Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ [ Int -> Int -> Prp
done Int
nPlayers Int
nCards ]
law :: Bdd
law = Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Conj ([Form] -> Form) -> [Form] -> Form
forall a b. (a -> b) -> a -> b
$
[ (if Int
cInt -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==Int
0 then Form -> Form
forall a. a -> a
id else 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
$ Int -> Int -> Int -> Prp
toPlay Int
nPlayers Int
nCards Int
c | Int
c <- [Int]
cards [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int
nCards] ]
[Form] -> [Form] -> [Form]
forall a. [a] -> [a] -> [a]
++ [ [Form] -> Form
Disj [ Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Int -> Int -> Int -> Prp
cardIsAt Int
nPlayers Int
nCards Int
i Int
c Int
p | Int
i <- [Int]
players, Int
p <- [Int]
positions ] | Int
c <- [Int]
cards ]
[Form] -> [Form] -> [Form]
forall a. [a] -> [a] -> [a]
++ [ Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Conj [ Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Int -> Int -> Int -> Prp
cardIsAt Int
nPlayers Int
nCards Int
i Int
c Int
p
, Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Int -> Int -> Int -> Prp
cardIsAt Int
nPlayers Int
nCards Int
j Int
c Int
q ] | Int
c <- [Int]
cards
, Int
i <- [Int]
players, Int
j <- [Int]
players
, Int
p <- [Int]
positions, Int
q <- [Int]
positions
, Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
j Bool -> Bool -> Bool
|| Int
p Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
q ]
[Form] -> [Form] -> [Form]
forall a. [a] -> [a] -> [a]
++ [ Form -> Form
Neg (Form -> Form) -> Form -> Form
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Conj [ Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Int -> Int -> Int -> Prp
cardIsAt Int
nPlayers Int
nCards Int
i Int
c Int
p
, Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Int -> Int -> Int -> Prp
cardIsAt Int
nPlayers Int
nCards Int
i Int
d Int
p ] | Int
c <- [Int]
cards, Int
d <- [Int]
cards
, Int
c Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
d
, Int
i <- [Int]
players
, Int
p <- [Int]
positions ]
[Form] -> [Form] -> [Form]
forall a. [a] -> [a] -> [a]
++ [ [Form] -> Form
Conj [ 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
$ Int -> Int -> Int -> Int -> Int -> Prp
cardIsAt Int
nPlayers Int
nCards Int
i Int
c Int
p ] | (Int
i,Int
p) <- Int -> [(Int, Int)] -> [(Int, Int)]
forall a. Int -> [a] -> [a]
drop Int
nCards [ (Int
i,Int
p) | Int
i <- [Int]
players, Int
p <- [Int]
positions ], Int
c <- [Int]
cards ]
obs :: [(String, [Prp])]
obs = [ (Int -> String
forall a. Show a => a -> String
show Int
i, [Prp]
voc [Prp] -> [Prp] -> [Prp]
forall a. Eq a => [a] -> [a] -> [a]
\\ [ Int -> Int -> Int -> Int -> Int -> Prp
cardIsAt Int
nPlayers Int
nCards Int
i Int
c Int
p | Int
c <- [Int]
cards, Int
p <- [Int]
positions ]) | Int
i <- [Int]
players ]
cur :: Bdd
cur = Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ [Form] -> Form
Conj ([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
$ Int -> Int -> Int -> Int -> Int -> Prp
cardIsAt Int
nPlayers Int
nCards Int
i Int
c Int
p | (Int
c,(Int
i,Int
p)) <- [Int] -> [(Int, Int)] -> [(Int, (Int, Int))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
cards [ (Int
i,Int
p) | Int
i <- [Int]
players, Int
p <- [Int]
positions ] ] [Form] -> [Form] -> [Form]
forall a. [a] -> [a] -> [a]
++
[ (if Int
c Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 then Form -> Form
forall a. a -> a
id else 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
$ Int -> Int -> Int -> Prp
toPlay Int
nPlayers Int
nCards Int
c | Int
c <- [Int]
cards ]
tell :: Int -> Int -> Int -> Int -> Int -> Labelled MultipointedEvent
tell :: Int -> Int -> Int -> Int -> Int -> Labelled MultipointedEvent
tell Int
nPlayers Int
nCards Int
i Int
c Int
p = (String
label, ([Prp]
-> Form -> [(Prp, Bdd)] -> [(String, [Prp])] -> KnowTransformer
KnTrf [Prp]
forall {a}. [a]
addprops Form
addlaw [(Prp, Bdd)]
forall {a}. [a]
changeLaw [(String, [Prp])]
forall {a}. [(String, [a])]
addObs, Form -> Bdd
boolBddOf Form
Top)) where
label :: String
label = String
"tell " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" card " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" @ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
p
addprops :: [a]
addprops = [ ]
addlaw :: Form
addlaw = Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Int -> Int -> Int -> Prp
cardIsAt Int
nPlayers Int
nCards Int
i Int
c Int
p
changeLaw :: [a]
changeLaw = [ ]
addObs :: [(String, [a])]
addObs = [ (Int -> String
forall a. Show a => a -> String
show Int
j, []) | Int
j <- [Int]
players ]
players :: [Int]
players = [Int
1..Int
nPlayers]
play :: Int -> Int -> Int -> Int -> Labelled MultipointedEvent
play :: Int -> Int -> Int -> Int -> Labelled MultipointedEvent
play Int
nPlayers Int
nCards Int
i Int
p = (String
label, ([Prp]
-> Form -> [(Prp, Bdd)] -> [(String, [Prp])] -> KnowTransformer
KnTrf [Prp]
forall {a}. [a]
addprops Form
addlaw [(Prp, Bdd)]
changeLaw [(String, [Prp])]
forall {a}. [(String, [a])]
addObs, Form -> Bdd
boolBddOf Form
Top)) where
label :: String
label = Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" plays position " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
p
addprops :: [a]
addprops = [ ]
addlaw :: Form
addlaw = [Form] -> Form
Disj [ [Form] -> Form
Conj [ Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Int -> Prp
toPlay Int
nPlayers Int
nCards Int
c
, Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Int -> Int -> Int -> Prp
cardIsAt Int
nPlayers Int
nCards Int
i Int
c Int
p ]
| Int
c <- [Int]
cards ]
changeLaw :: [(Prp, Bdd)]
changeLaw = [ (Int -> Int -> Int -> Int -> Int -> Prp
cardIsAt Int
nPlayers Int
nCards Int
i Int
c Int
p, Form -> Bdd
boolBddOf Form
Bot) | Int
c <- [Int]
cards ]
[(Prp, Bdd)] -> [(Prp, Bdd)] -> [(Prp, Bdd)]
forall a. [a] -> [a] -> [a]
++ [ ( Int -> Int -> Int -> Prp
toPlay Int
nPlayers Int
nCards Int
0, Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ Form -> Form -> Form -> Form
ite (Int -> Form
tP Int
0) Form
Bot (Int -> Form
tP Int
0) ) ]
[(Prp, Bdd)] -> [(Prp, Bdd)] -> [(Prp, Bdd)]
forall a. [a] -> [a] -> [a]
++ [ ( Int -> Int -> Int -> Prp
toPlay Int
nPlayers Int
nCards Int
c, Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ Form -> Form -> Form -> Form
ite (Int -> Form
tP Int
c) Form
Bot (Form -> Form -> Form -> Form
ite (Int -> Form
tP (Int
cInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)) Form
Top (Int -> Form
tP Int
c)) ) | Int
c <- [Int]
cards, Int
c Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 ]
[(Prp, Bdd)] -> [(Prp, Bdd)] -> [(Prp, Bdd)]
forall a. [a] -> [a] -> [a]
++ [ ( Int -> Int -> Int -> Prp
toPlay Int
nPlayers Int
nCards Int
nCards, Form -> Bdd
boolBddOf (Form -> Bdd) -> Form -> Bdd
forall a b. (a -> b) -> a -> b
$ Form -> Form -> Form -> Form
ite (Int -> Form
tP (Int
nCardsInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)) Form
Top Form
Bot ) | Int
c <- [Int]
cards, Int
c Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 ]
addObs :: [(String, [a])]
addObs = [ (Int -> String
forall a. Show a => a -> String
show Int
j, []) | Int
j <- [Int]
players ]
players :: [Int]
players = [Int
1..Int
nPlayers]
tP :: Int -> Form
tP Int
c = Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Int -> Prp
toPlay Int
nPlayers Int
nCards Int
c
cards :: [Int]
cards = [Int
0..(Int
nCardsInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)]
toynabiGoal :: Int -> Int -> Form
toynabiGoal :: Int -> Int -> Form
toynabiGoal Int
nPlayers Int
nCards = Prp -> Form
PrpF (Prp -> Form) -> Prp -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Prp
done Int
nPlayers Int
nCards
toynabi :: Int -> Int -> CoopTask MultipointedKnowScene MultipointedEvent
toynabi :: Int -> Int -> CoopTask MultipointedKnowScene MultipointedEvent
toynabi Int
nPlayers Int
nCards = MultipointedKnowScene
-> [Owned MultipointedEvent]
-> Form
-> CoopTask MultipointedKnowScene MultipointedEvent
forall state action.
state -> [Owned action] -> Form -> CoopTask state action
CoopTask (Int -> Int -> MultipointedKnowScene
toynabiStartFor Int
nPlayers Int
nCards) [Owned MultipointedEvent]
actions (Int -> Int -> Form
toynabiGoal Int
nPlayers Int
nCards) where
actions :: [Owned MultipointedEvent]
actions = [ (Int -> String
forall a. Show a => a -> String
show Int
i, Int -> Int -> Int -> Int -> Int -> Labelled MultipointedEvent
tell Int
nPlayers Int
nCards Int
j Int
c Int
p) | Int
i <- [Int]
players, Int
j <- [Int]
players, Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
j, Int
c <- [Int]
cards, Int
p <- [Int]
positions ] [Owned MultipointedEvent]
-> [Owned MultipointedEvent] -> [Owned MultipointedEvent]
forall a. [a] -> [a] -> [a]
++
[ (Int -> String
forall a. Show a => a -> String
show Int
i, Int -> Int -> Int -> Int -> Labelled MultipointedEvent
play Int
nPlayers Int
nCards Int
i Int
p) | Int
i <- [Int]
players, Int
p <- [Int]
positions ]
players :: [Int]
players = [Int
1..Int
nPlayers]
cards :: [Int]
cards = [Int
0..(Int
nCardsInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)]
nPositions :: Int
nPositions = Double -> Int
forall b. Integral b => Double -> b
forall a b. (RealFrac a, Integral b) => a -> b
ceiling (Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
nCards Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
nPlayers :: Double)
positions :: [Int]
positions = [Int
0..(Int
nPositionsInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)]
exampleResult :: PointedModelS5
exampleResult :: PointedModelS5
exampleResult = PointedModelS5 -> PointedModelS5
generatedSubmodel (PointedModelS5 -> PointedModelS5)
-> PointedModelS5 -> PointedModelS5
forall a b. (a -> b) -> a -> b
$ KnowScene -> PointedModelS5
knsToKripke (MultipointedKnowScene -> KnowStruct
forall a b. (a, b) -> a
fst MultipointedKnowScene
theKNS, [[Prp]] -> [Prp]
forall a. HasCallStack => [a] -> a
head ([[Prp]] -> [Prp]) -> [[Prp]] -> [Prp]
forall a b. (a -> b) -> a -> b
$ KnowStruct -> [[Prp]]
statesOf (KnowStruct -> [[Prp]]) -> KnowStruct -> [[Prp]]
forall a b. (a -> b) -> a -> b
$ MultipointedKnowScene -> KnowStruct
forall a b. (a, b) -> a
fst MultipointedKnowScene
theKNS) where
theKNS :: MultipointedKnowScene
theKNS = Int -> Int -> MultipointedKnowScene
toynabiStartFor Int
2 Int
4
MultipointedKnowScene -> MultipointedEvent -> MultipointedKnowScene
forall a b. Update a b => a -> b -> a
`update` Labelled MultipointedEvent -> MultipointedEvent
forall a b. (a, b) -> b
snd (Int -> Int -> Int -> Int -> Int -> Labelled MultipointedEvent
tell Int
2 Int
4 Int
1 Int
0 Int
0)
MultipointedKnowScene -> MultipointedEvent -> MultipointedKnowScene
forall a b. Update a b => a -> b -> a
`update` Labelled MultipointedEvent -> MultipointedEvent
forall a b. (a, b) -> b
snd (Int -> Int -> Int -> Int -> Labelled MultipointedEvent
play Int
2 Int
4 Int
1 Int
0)
MultipointedKnowScene -> MultipointedEvent -> MultipointedKnowScene
forall a b. Update a b => a -> b -> a
`update` Labelled MultipointedEvent -> MultipointedEvent
forall a b. (a, b) -> b
snd (Int -> Int -> Int -> Int -> Labelled MultipointedEvent
play Int
2 Int
4 Int
1 Int
1)