----------------------------------------------------------------------------------

-- ***   Web Service Algebra (based on traces): basic Haskell module ***

-- ***   (c) December 2007 by Peter Höfner and Florian Lautenbacher ***

----------------------------------------------------------------------------------
----------------------------------------------------------------------------------
module Traces where



-- Traces in Haskell

infixl 4  ??              -- subset-relation
infixl 5  \/ , /\ , !-    -- union, meet, set-difference
infixl 6  #               -- composition
infixl 7  ^^^, ^<=        -- power, limited iteration

--------------------------------------

type Trc a = [[[a]]]

--------------------------------------
empty = []

--------------------------------------

set s = deleteMultipleOccurences (qsort s)

-- Quicksort -------------------------

qsort [] = []

qsort (x:xs) = qsort begin ++ [x] ++ qsort end
  where begin = [ y | y <- xs, y <= x ]
        end = [ y | y <- xs, y >  x ]

-- sorted liste  (delete multiple occurences)---

deleteMultipleOccurences []  = []
deleteMultipleOccurences [x]  =  [x]
deleteMultipleOccurences (x:(y:s))  =
  if x == y then deleteMultipleOccurences (y:s)
            else x : deleteMultipleOccurences (y:s)

--------------------------------------

r \/ s  =  set (r ++ s)

--------------------------------------

s !- []  =  s
s !- (y:t)  =
  [x | x <- s, x /= y ] !- t
--------------------------------------


--------------------------------------

union :: [[a]] -> [a]
union  =  concat

--------------------------------------

(??) :: Eq a => a -> [a] -> Bool

x ?? s  =  any (==x) s

--------------------------------------

s /\ t  =  [ x | x <- s, x ?? t ]

-- euivalence (same elements) -----

equiv s t  =  (sub s t) && (sub t s)

-- inclusion -------------------------

sub s t    =  (s /\ t == s)

-- (co)domain -----------------------
dom r = set[[head(u)] | u <- r]
cod r = set[[last(u)] | u <- r]



-- negation of a test w.r.t. a knowledge power (skip) set
neg p = skip !- p


-- diamonds (no check if p is a test, ks = knowledge set)
fd r p = dom (r#p)
-- bd r p = cod (p#r)
--fb r p = neg (fd r (neg p))
-- bb r p ks = neg (bd r (neg p ks)) ks

--------------------------------------

-- calculate knowledge set ------------------------

knowledge r = set (defset r ++ valset r)

-- definition- and value set -----

defset  r  =  set (map head r)

valset r  =  set (map last r)

--------------------------------------
-- composition --------------

r # s = 
    set [x++tail(y)| x<-r, y<-s, last(x)==head(y)]


--powers ---------------------------

r^^^1      =  r
r^^^(n+1)  =  r # (r^^^n)

--------------------------------------

-- Iteration -------------------------

r^<=n  =  union [ r^^^i | i <- [1..n] ]

--------------------------------------

plus r  =  union [ r^^^i | i <- [1..] ]

--------------------------------------

------------Plus----------------------

pplus r = r \/ r # pplus r

--------------------------------------
--                                  --
--   Iteration mit Terminierung     --
--                                  --
--------------------------------------

ttplus r  =  it4 r (r # r) r empty

it4 r s t u =
  if sub t u then u
             else it4 r (s # r) (t \/ s) t

--ttstar r = idRel r \/ ttplus r

star r = skip \/ ttplus r 

--generating the powerset
powerset [] = [[]]
powerset (x:xs) = let p = powerset xs in p ++ map (x:) p

-- blow
add :: [String] -> [[String]] -> [[String]]
add x [] = []
add x (p:[]) = [x\/p]
add x (p:(a:xs)) = [p\/x,a]++(add x xs)
blow_single :: [[String]] -> Trc String
blow_single ws = set[add x ws | x<-powerset(k!-last(ws))]
blow :: Trc String -> Trc String
blow ws = set[add x y | y<-ws,x<-powerset(k!-last(y))]

buildplan :: String -> Trc String -> Trc String
buildplan str p = set[[set [],[str], x]| y<-p, x<-y]

----------------------------------------------------------------------------------
--PRINTING
----------------------------------------------------------------------------------

sep1 = "---------------------------------------------------------------------\n"
sep2 = "=====================================================================\n"

----------------------------------------------------------------------------------
--prn_hlp :: String -> [[String]] -> String
prn_hlp str (s:[]) = show s
prn_hlp str (s:trc) = show s ++ str ++ (prn_hlp str trc)  

printTRC1 trc = putStr (sep1 ++ foldl (++) "" (map (++"\n"++sep1) (map (prn_hlp "--") trc)))
printTRC2 trc = putStr (sep1 ++ foldl (++) "" (map (++"\n"++sep1) (map (prn_hlp "\n  --") trc)))

out trc = printTRC2 trc


-------------------------------------------------------------
-------------------------------------------------------------
-- Example: Web Services
-- Knowledge
d1     = "d1"
d2     = "d2"
dep    = "dep"
des    = "des"
cc     = "cc"
ff     = "ff"
etix1  = "etix1"
etix2  = "etix2"
resnrh = "resnrh"
cat    = "cat"
kind   = "kind"
smt    = "smt"
resnrc = "resnrc"

---------
--names
fli    = "flight"
hot    = "hotel"
ca     = "car"
fp     = "flightplan"
hp     = "hotelplan"

k = set [d1,d2,dep,des,cc,ff,etix1,etix2,resnrh,cat,kind,resnrc,smt]
names = set [fli,hot,ca,fp,hp]
powk = powerset k
-- assertions / tests
skip = [[x]|x<-powk]

flight_base :: Trc String
flight_base = set [[set [d1,dep,des,cc],[fli],set [d1,dep,des,cc,etix1]],
                   [set [d1,dep,des,ff],[fli],set [d1,dep,des,ff,etix1]],
                   [set [d2,dep,des,cc],[fli],set [d2,dep,des,cc,etix2]],
                   [set [d2,dep,des,ff],[fli],set [d2,dep,des,ff,etix2]]]
flight = blow flight_base

hotel_base :: Trc String
hotel_base = set [[set [d1,d2,des,kind,cat,cc],[hot],set [d1,d2,des,kind,cat,cc,resnrh]]]
hotel = blow hotel_base

car_base :: Trc String
car_base = set [[set [d1,d2,des,cc],[ca],set [d1,d2,des,cc,resnrc]]]
car = blow car_base

t1 = blow (set[[set[etix1]]])
t2 = blow (set[[set[etix2]]])
t3 = t1#t2 

flightplan_base = buildplan fp (((neg (t1\/t2))#(fd (star flight) (t1#t2))))
flightplan = blow flightplan_base

t4 = blow (set[[set[resnrh]]])
hotelplan_base = buildplan hp (((neg t4)#(fd (star hotel) t4)))
hotelplan = blow hotelplan_base

t5 = blow (set[[set[resnrc]]])

t6=t3#t4#t5
t7 = neg(t1\/t2\/t4\/t5)
choice = (flight \/ hotel \/ car)
tmp1 = t7#(star choice)
startparam = fd tmp1 t6