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
$
[ [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 ]
[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 ]
[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
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] ]
changeLaw :: [(Prp, Bdd)]
changeLaw = [ (Int -> Prp
atP Int
i, Form -> Bdd
boolBddOf Form
Bot), (Int -> Prp
atP Int
j, Form -> Bdd
boolBddOf Form
Top) ]
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
$
[ [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 ]
[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 ]
[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] ]