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

-- | Given nPlayers and nCards in total, this proposition encodes that player i has card c in position p.
-- Note that we start counting players with 1, but cards and positions with 0.
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)

-- | A proposition to say that the card c should be played next.
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)

-- | This proposition says that the game has ended.
done :: Int -> Int -> Prp
done :: Int -> Int -> Prp
done Int
nPlayers Int
nCards = Int -> Int -> Int -> Prp
toPlay Int
nPlayers Int
nCards Int
nCards

-- | Print and translate the vocabulary in both directions, just for debugging.
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)) -- TODO test and check this!
  | 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 ]

-- | The starting knowledge structure.
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
$
    -- The next card to be played is 0:
       [ (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] ]
    -- Each card must be at someone in some position, but not two:
    [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 ]
    -- For each player each position can only hold one card:
    [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 ]
    -- If nPlayers * nPositions > nCards then there are empty 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
$
          -- distribute all the cards:
          [ 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]
++
          -- set toPlay to 0:
          [ (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 agent i that they have card c at position p.
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]

-- | Let agent i play the card at position p.
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 ] -- remove card from that position
                [(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) ) ] -- if first card is played
                [(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 ] -- increase toPlay
                [(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 ] -- set done

  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)]

-- | The goal.
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

-- | The whole cooperative planning task.
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)]

-- | An example result to test whether updating works, translated to a Kripke model.
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)