module SMCDEL.Examples.LetterPassing where

import Data.List (sort)

import SMCDEL.Language
import SMCDEL.Symbolic.S5 hiding (announce)
import SMCDEL.Translations.S5 (booloutof)
import SMCDEL.Other.Planning

explain :: Prp -> String
explain :: Prp -> String
explain (P Int
k) | Int -> Bool
forall a. Integral a => a -> Bool
odd Int
k     = String
"at " 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. Integral a => a -> a -> a
`div` Int
2)
              | Bool
otherwise = String
"for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
k Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2)

atP, forP :: Int -> Prp
atP :: Int -> Prp
atP  Int
k = Int -> Prp
P (Int -> Prp) -> Int -> Prp
forall a b. (a -> b) -> a -> b
$ Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
*Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
forP :: Int -> Prp
forP Int
k = Int -> Prp
P (Int -> Prp) -> Int -> Prp
forall a b. (a -> b) -> a -> b
$ Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
*Int
2

at, for :: Int -> Form
at :: Int -> Form
at  = Prp -> Form
PrpF (Prp -> Form) -> (Int -> Prp) -> Int -> Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Prp
atP
for :: Int -> Form
for = Prp -> Form
PrpF (Prp -> Form) -> (Int -> Prp) -> Int -> Form
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Prp
forP

letterStart :: MultipointedKnowScene
letterStart :: MultipointedKnowScene
letterStart = ([Prp] -> Bdd -> [(String, [Prp])] -> KnowStruct
KnS [Prp]
voc Bdd
law [(String, [Prp])]
obs, Bdd
cur) where
  voc :: [Prp]
voc = [Prp] -> [Prp]
forall a. Ord a => [a] -> [a]
sort ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ (Int -> Prp) -> [Int] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Prp
atP [Int
1..Int
3] [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ (Int -> Prp) -> [Int] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Prp
forP [Int
1..Int
3]
  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
$
    -- letter must be at someone, but not two:
       [ [Form] -> Form
Disj ((Int -> Form) -> [Int] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Form
at [Int
1..Int
3]) ]
    [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 [Int -> Form
at Int
i, Int -> Form
at Int
j] | Int
i <- [Int
1..Int
3], Int
j <- [Int
1..Int
3], Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
j ]
    -- letter must be for someone, but not two:
    [Form] -> [Form] -> [Form]
forall a. [a] -> [a] -> [a]
++ [ [Form] -> Form
Disj ((Int -> Form) -> [Int] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Form
for [Int
1..Int
3]) ]
    [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 [Int -> Form
for Int
i, Int -> Form
for Int
j] | Int
i <- [Int
1..Int
3], Int
j <- [Int
1..Int
3], Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
j ]
    -- make it common knowledge that the letter is at 1, but not adressed to 1:
    [Form] -> [Form] -> [Form]
forall a. [a] -> [a] -> [a]
++ [ Int -> Form
at Int
1, Form -> Form
Neg (Int -> Form
for Int
1) ]
  obs :: [(String, [Prp])]
obs = [ (String
"1",[Int -> Prp
atP Int
1, Int -> Prp
forP Int
1, Int -> Prp
forP Int
2, Int -> Prp
forP Int
3])
        , (String
"2",[Int -> Prp
atP Int
2])
        , (String
"3",[Int -> Prp
atP Int
3]) ]
  cur :: Bdd
cur = [Prp] -> [Prp] -> Bdd
booloutof [Int -> Prp
atP Int
1, Int -> Prp
forP Int
3] [Prp]
voc

letterPass :: Int -> Int -> Int -> Labelled MultipointedEvent
letterPass :: Int -> Int -> Int -> Labelled MultipointedEvent
letterPass Int
n Int
i Int
j = (String
label, ([Prp]
-> Form -> [(Prp, Bdd)] -> [(String, [Prp])] -> KnowTransformer
KnTrf [Prp]
addprops Form
addlaw [(Prp, Bdd)]
changeLaw [(String, [Prp])]
addObs, Form -> Bdd
boolBddOf Form
Top)) where
  offset :: Int
offset      = Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
*Int
2 -- ensure addprops does not overlap with vocabOf (letterStartFor n)
  label :: String
label       = Int -> String
forall a. Show a => a -> String
show Int
i 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
j
  addprops :: [Prp]
addprops    = (Int -> Prp) -> [Int] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Prp
P [(Int
offset Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)..(Int
offset Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n)]
  addlaw :: Form
addlaw      = [Form] -> Form
Conj ([Form] -> Form) -> [Form] -> Form
forall a b. (a -> b) -> a -> b
$ Int -> Form
at Int
i Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
: [ Prp -> Form
PrpF (Int -> Prp
P (Int
offset Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
k)) Form -> Form -> Form
`Equi` Int -> Form
for Int
k | Int
k <- [Int
1..Int
n] ]
  -- publicly pass the letter from i to j:
  changeLaw :: [(Prp, Bdd)]
changeLaw   = [ (Int -> Prp
atP Int
i, Form -> Bdd
boolBddOf Form
Bot), (Int -> Prp
atP Int
j, Form -> Bdd
boolBddOf Form
Top) ]
  -- privately tell j who the receiver is:
  addObs :: [(String, [Prp])]
addObs      = [ (Int -> String
forall a. Show a => a -> String
show Int
k, if Int
k Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j then [Prp]
addprops else []) | Int
k <- [Int
1..Int
n] ]

letterGoal :: Form
letterGoal :: Form
letterGoal = [Form] -> Form
Conj [ Int -> Form
for Int
i Form -> Form -> Form
`Impl` Int -> Form
at Int
i | Int
i <- [Int
1,Int
2,Int
3] ]

letter :: CoopTask MultipointedKnowScene MultipointedEvent
letter :: CoopTask MultipointedKnowScene MultipointedEvent
letter = MultipointedKnowScene
-> [Owned MultipointedEvent]
-> Form
-> CoopTask MultipointedKnowScene MultipointedEvent
forall state action.
state -> [Owned action] -> Form -> CoopTask state action
CoopTask MultipointedKnowScene
letterStart [Owned MultipointedEvent]
actions Form
letterGoal where
  actions :: [Owned MultipointedEvent]
actions = [ (Int -> String
forall a. Show a => a -> String
show Int
i, Int -> Int -> Int -> Labelled MultipointedEvent
letterPass Int
3 Int
i Int
j) | (Int
i,Int
j) <- [(Int
1,Int
2),(Int
2,Int
1),(Int
2,Int
3),(Int
3,Int
2)] ]

letterStartFor :: Int -> MultipointedKnowScene
letterStartFor :: Int -> MultipointedKnowScene
letterStartFor Int
n = ([Prp] -> Bdd -> [(String, [Prp])] -> KnowStruct
KnS [Prp]
voc Bdd
law [(String, [Prp])]
obs, Bdd
cur) where
  voc :: [Prp]
voc = [Prp] -> [Prp]
forall a. Ord a => [a] -> [a]
sort ([Prp] -> [Prp]) -> [Prp] -> [Prp]
forall a b. (a -> b) -> a -> b
$ (Int -> Prp) -> [Int] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Prp
atP [Int
1..Int
n] [Prp] -> [Prp] -> [Prp]
forall a. [a] -> [a] -> [a]
++ (Int -> Prp) -> [Int] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Prp
forP [Int
1..Int
n]
  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
$
    -- letter must be at someone, but not two:
       [ [Form] -> Form
Disj ((Int -> Form) -> [Int] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Form
at [Int
1..Int
n]) ]
    [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 [Int -> Form
at Int
i, Int -> Form
at Int
j] | Int
i <-[Int
1..Int
n], Int
j <- [Int
1..Int
n], Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
j ]
    -- letter must be for someone, but not two:
    [Form] -> [Form] -> [Form]
forall a. [a] -> [a] -> [a]
++ [ [Form] -> Form
Disj ((Int -> Form) -> [Int] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Form
for [Int
1..Int
n]) ]
    [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 [Int -> Form
for Int
i, Int -> Form
for Int
j] | Int
i <-[Int
1..Int
n], Int
j <- [Int
1..Int
n], Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
j ]
    -- make it common knowledge that letter is at 1, but not adressed to 1:
    [Form] -> [Form] -> [Form]
forall a. [a] -> [a] -> [a]
++ [ Int -> Form
at Int
1, Form -> Form
Neg (Int -> Form
for Int
1) ]
  obs :: [(String, [Prp])]
obs = (String
"1", Int -> Prp
atP Int
1 Prp -> [Prp] -> [Prp]
forall a. a -> [a] -> [a]
: (Int -> Prp) -> [Int] -> [Prp]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Prp
forP [Int
1..Int
n]) (String, [Prp]) -> [(String, [Prp])] -> [(String, [Prp])]
forall a. a -> [a] -> [a]
: [ (Int -> String
forall a. Show a => a -> String
show Int
k, [Int -> Prp
atP Int
k]) | Int
k <- [Int
2..Int
n] ]
  cur :: Bdd
cur = [Prp] -> [Prp] -> Bdd
booloutof [Int -> Prp
atP Int
1, Int -> Prp
forP Int
n] [Prp]
voc

letterLine :: Int -> CoopTask MultipointedKnowScene MultipointedEvent
letterLine :: Int -> CoopTask MultipointedKnowScene MultipointedEvent
letterLine Int
n = MultipointedKnowScene
-> [Owned MultipointedEvent]
-> Form
-> CoopTask MultipointedKnowScene MultipointedEvent
forall state action.
state -> [Owned action] -> Form -> CoopTask state action
CoopTask (Int -> MultipointedKnowScene
letterStartFor Int
n) [Owned MultipointedEvent]
actions Form
goal where
  actions :: [Owned MultipointedEvent]
actions = [ (Int -> String
forall a. Show a => a -> String
show Int
i, Int -> Int -> Int -> Labelled MultipointedEvent
letterPass Int
n Int
i Int
j) | Int
i <- [Int
1..Int
n], Int
j <- [Int
1..Int
n], Int -> Int
forall a. Num a => a -> a
abs(Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
j) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 ]
  goal :: Form
goal = [Form] -> Form
Conj [ Int -> Form
for Int
i Form -> Form -> Form
`Impl` Int -> Form
at Int
i | Int
i <- [Int
1..Int
n] ]