module Main where
import Data.Map
import Data.List
import Data.Char
import Test.QuickCheck
import SlicingX
import GuiModelFull
import GuiModel
type State = Map EventRef Bool
type StateRef = String
newtype N = N ([CondRef],[EventRef])
deriving (Eq,Show)
--res = [N (["c1,c2"],["e1","e2"]),N (["c3"],["e3"])]
instance Arbitrary N where
arbitrary = elements (ways 6) --res
coarbitrary s = variant (lengthHalf s)
lengthHalf (N s) = ((length (snd s)) `rem` 2)
-- Rules
-- quickCheck ruleX
-- deepCheck ruleX
-- verboseCheck ruleX
--
deepCheck p = check (defaultConfig { configMaxTest = 10000}) p
-- a sequência de eventos não pode ser vazia
rule1 (N (a,b)) =
classify ((length b)==2) "events sequence length: 1" $
classify ((length b)==3) "events sequence length: 2" $
classify ((length b)==4) "events sequence length: 3" $
classify ((length b)==5) "events sequence length: 4" $
classify ((length b)==6) "events sequence length: 5" $
classify ((length b)==7) "events sequence length: 6" $
classify ((length b)==8) "events sequence length: 7" $
classify ((length b)==9) "events sequence length: 8" $
classify ((length b)==10) "events sequence length: 9" $
classify ((length b)==11) "events sequence length: >10" $
length b /= 0
-- só é possível executar event5(sair) uma vez
rule2 (N (a,b)) =
classify ((length b)==2) "events sequence length: 1" $
classify ((length b)==3) "events sequence length: 2" $
classify ((length b)==4) "events sequence length: 3" $
classify ((length b)==5) "events sequence length: 4" $
classify ((length b)==6) "events sequence length: 5" $
classify ((length b)==7) "events sequence length: 6" $
classify ((length b)==8) "events sequence length: 7" $
classify ((length b)==9) "events sequence length: 8" $
classify ((length b)==10) "events sequence length: 9" $
classify ((length b)==11) "events sequence length: >10" $
length (Data.List.filter ((==) "event5") b) <= 1
-- se ocorrer event5(sair) então ocorre somente no fim
rule3 (N (a,b)) =
classify ((length b)==2) "events sequence length: 1" $
classify ((length b)==3) "events sequence length: 2" $
classify ((length b)==4) "events sequence length: 3" $
classify ((length b)==5) "events sequence length: 4" $
classify ((length b)==6) "events sequence length: 5" $
classify ((length b)==7) "events sequence length: 6" $
classify ((length b)==8) "events sequence length: 7" $
classify ((length b)==9) "events sequence length: 8" $
classify ((length b)==10) "events sequence length: 9" $
classify ((length b)==11) "events sequence length: >10" $
if (length (Data.List.filter ((==) "event5") b) == 1) then last b == "event5" else True
-- não pode remover mais do que insere
-- em cada instante nº remove com sucesso <= nº insere com sucesso
rule4Aux :: ([CondRef],[EventRef]) -> Int
rule4Aux ([],[]) = 0
rule4Aux ((h1:t1),(h:t))
| (h=="event1")&&(h1=="cond1") = 1+(rule4Aux (t1,t))
| (h=="event3")&&(h1=="cond7") = (-1)+(rule4Aux (t1,t))
| otherwise = (rule4Aux (t1,t))
rule4 (N (a,b)) =
classify ((length b)==2) "events sequence length: 1" $
classify ((length b)==3) "events sequence length: 2" $
classify ((length b)==4) "events sequence length: 3" $
classify ((length b)==5) "events sequence length: 4" $
classify ((length b)==6) "events sequence length: 5" $
classify ((length b)==7) "events sequence length: 6" $
classify ((length b)==8) "events sequence length: 7" $
classify ((length b)==9) "events sequence length: 8" $
classify ((length b)==10) "events sequence length: 9" $
classify ((length b)==11) "events sequence length: >10" $
all (((<=) 0).(rule4Aux)) (zip (inits a) (inits b))
-- só pode consultar se existir alunos (nº add > nº remove) e nº add >= 1
--rule5 :: N -> Bool
--rule5 (N (a,b)) = all (((<=) 1). (rule4Aux)) $ Data.List.filter (((==) "event2").last) (Data.List.filter ((/=) []) $ inits b)
rule5 (N (a,b)) = let res = zip (inits a) (inits b)
res1 = [(a,b)|(a,b)<-res,b/=[]]
res2 = [(a,b)|(a,b)<-res1,last b == "event2"]
in --collect ((length b)-1) $
classify ((length b)==2) "events sequence length: 1" $
classify ((length b)==3) "events sequence length: 2" $
classify ((length b)==4) "events sequence length: 3" $
classify ((length b)==5) "events sequence length: 4" $
classify ((length b)==6) "events sequence length: 5" $
classify ((length b)==7) "events sequence length: 6" $
classify ((length b)==8) "events sequence length: 7" $
classify ((length b)==9) "events sequence length: 8" $
classify ((length b)==10) "events sequence length: 9" $
classify ((length b)==11) "events sequence length: >10"
(all (((<=) 1). (rule4Aux)) res2 )
-- numero de condições igual ao numero de eventos
rule6 :: N -> Bool
rule6 (N (a,b)) = length a == length b
ruleX :: N -> N -> Bool
ruleX (N (a,b)) (N (c,d)) | (N (a,b)) /= (N (c,d)) = d /= b
| otherwise = True
validEvents :: [ExpRef] -> Pres -> [EventRef]
validEvents l p = keys ( Data.Map.filter (\v -> v==True) (validEventAux l p (Data.Map.map (\e -> True) events)))
validEventAux :: [ExpRef] -> Pres -> Map EventRef Bool -> Map EventRef Bool
validEventAux [] p validevents = validevents
validEventAux (h:t) p validevents | member h p = let res = p ! h in validEventAux t pres (Data.Map.insert (fst res) (snd res) validevents)
| otherwise = validEventAux t pres validevents
--ways :: Int -> [([CondRef],[EventRef])]
ways :: Int -> [N]
ways n = let l = waysAux guimodel n ["init"] [] [] [] (Data.List.union end close)
in [N (a,b)|(a,b) <- l]
waysAux :: GuiModel -> Int -> [EventRef] -> [EventRef] -> [CondRef] -> [ExpRef] -> End -> [([CondRef],[EventRef])]
waysAux _ 0 _ _ _ _ _ = []
waysAux gui n lEventRef1 lEventRef lCondRef lExpRef endlist =
concat [let lCondRefExpRef = toList (mapKeys (\k -> [snd k]) (filterWithKey (\k v -> fst k == e) gui))
lCondRefEventRef1 = [(lCondRef++lc,lEventRef++[e]) | (lc,le) <- lCondRefExpRef]
lCondRefEventRef2 =
-- if (not (elem e endlist)) then
concat [let ve = validEvents (lExpRef++le) pres in waysAux gui (n-1) ve (lEventRef++[e]) (lCondRef++lc) (lExpRef++le) endlist
| (lc,le) <- lCondRefExpRef, Data.List.intersect le (Data.List.union end close) == []
]
-- else []
in lCondRefEventRef1 ++ lCondRefEventRef2
| e <- lEventRef1
]
{--
--ways :: Int -> [([CondRef],[EventRef])]
ways1 :: Int -> [[(EventRef,CondRef)]]
ways1 n = let l = waysAux1 guimodel n ["init"] [] [] [] end
in [(a,b)|(a,b) <- l]
waysAux1 :: GuiModel -> Int -> [EventRef] -> [EventRef] -> [CondRef] -> [ExpRef] -> End -> [([CondRef],[EventRef])]
waysAux1 _ 0 _ _ _ _ _ = []
waysAux1 gui n lEventRef1 lEventRef lCondRef lExpRef endlist =
concat [let lCondRefExpRef = toList (mapKeys (\k -> [snd k]) (filterWithKey (\k v -> fst k == e) gui))
lCondRefEventRef1 = [(lCondRef++lc,lEventRef++[e]) | (lc,le) <- lCondRefExpRef]
lCondRefEventRef2 = if (not (elem e endlist)) then
concat [let ve = validEvents (lExpRef++le) pres in waysAux1 gui (n-1) ve (lEventRef++[e]) (lCondRef++lc) (lExpRef++le) endlist
| (lc,le) <- lCondRefExpRef
]
else []
in lCondRefEventRef1 ++ lCondRefEventRef2
| e <- lEventRef1
]
--}
eventsRefStatusApply :: State -> [ExpRef] -> State
eventsRefStatusApply m [] = m
eventsRefStatusApply m (h:t) | member h pres = let v = pres ! h
m1 = Data.Map.insert (fst v) (snd v) m
in eventsRefStatusApply m1 t
| otherwise = eventsRefStatusApply m t
guiGraph :: Int -> Map (State,EventRef,CondRef,[ExpRef]) State
guiGraph n =
let m = (Data.Map.map (\e -> True) events)
linit = toList (filterWithKey (\k v -> fst k == "init") guimodel)
gInit = fromList [((empty,fst a,snd a,b),eventsRefStatusApply m b)|(a,b) <- linit]
gRes = guiGraphAux gInit gInit n
in gRes
guiGraph1 :: State -> Map (State,EventRef,CondRef,[ExpRef]) State
guiGraph1 s =
let levent = keys (Data.Map.filter (\v -> v == True) s)
lmap = concat [toList (filterWithKey (\k v -> fst k == e) guimodel) | e <- levent]
-- gNext = fromList [if (not (Data.List.elem (fst a) end)) then ((s,fst a,snd a,b),eventsRefStatusApply s b)
gNext = fromList [if (Data.List.intersect b (Data.List.union end close) == []) then ((s,fst a,snd a,b),eventsRefStatusApply s b)
else ((s,fst a,snd a,b),empty)
|(a,b) <- lmap]
in gNext
guiGraphAux :: Map (State,EventRef,CondRef,[ExpRef]) State -> Map (State,EventRef,CondRef,[ExpRef]) State -> Int -> Map (State,EventRef,CondRef,[ExpRef]) State
guiGraphAux _ l 0 = l
guiGraphAux m l n = let res1 = [guiGraph1 s2 |((s1,e,c,le),s2) <- toList m,s2 /= empty]
res2 = foldl Data.Map.union empty res1
res3 = Data.Map.difference res2 l
res4 = if (res3 /= empty) then guiGraphAux res3 (Data.Map.union l res3) (n-1) else l
in res4
guiGraphRef :: Map (State,EventRef,CondRef,[ExpRef]) State -> (Map (StateRef,EventRef,CondRef,[ExpRef]) StateRef, Map StateRef State)
guiGraphRef m = let res = nub $ (Data.List.map (\(a,b,c,d) -> a) (keys m)) ++ (elems m)
res2 = fromList $ zip (Data.List.map (((++) "state").show) [0..((length res)-1)]) res
in guiGraphRefAux m res2
guiGraphRefAux :: Map (State,EventRef,CondRef,[ExpRef]) State -> (Map StateRef State) -> (Map (StateRef,EventRef,CondRef,[ExpRef]) StateRef, Map StateRef State)
guiGraphRefAux l n = let m = toList l
nn = toList n
f v = let r = [a| (a,b) <-nn, b == v]
in if r==[] then "" else head r
res = fromList [((f s1,e,c,le),f s2)| ((s1,e,c,le),s2) <- m]
in (res,n)
graphViz :: Map (StateRef,EventRef,CondRef,[ExpRef]) StateRef -> Map StateRef State -> String
graphViz m m1 =
let res = toList m
nodes = nub $ (Data.List.map (\(a,b,c,d) -> a) (keys m)) ++ (elems m)
res1 = "digraph gr { rankdir = TD;\n"++
"subgraph cluster {\n"++
"color=lightgrey;\n"++
"style=filled;\n"++
"label = \"New window actions:"++[e|e<-(show $ toList newWindow),e/='"']++"\";\n"++
concat [ e++ " [shape=box , fillcolor=royalblue, style=filled label=\"" ++ e ++ "\" ,color=royalblue];" ++ "\n" |e<-nodes,m1!e /= (fromList [])] ++
"init [shape=box , label=\"" ++ "state 0" ++ "\", color=green2];" ++ "\n" ++
(if (Data.List.null end == False)
then "end [shape=doublecircle , label=\"" ++ "end" ++ "\", color=red2];" ++ "\n"
else "") ++
(if (Data.List.null close == False)
then "close [shape=doublecircle , label=\"" ++ "close" ++ "\", color=red2];" ++ "\n"
else "") ++
"start [shape=point , fillcolor=gray, style=filled, color=gray];" ++ "\n" ++
concat ([if ((m1!a==(fromList []))&&(m1!e==(fromList [])))
then "init" ++" -> " ++ "end" ++ " [color=red2, label= \""++ b ++ "/" ++ c ++ "/" ++ (show d) ++"\"];\n"
else if (m1!a==empty)
then "init" ++" -> " ++ e ++ " [color=green2, label= \""++ b ++ "/" ++ c ++ "/" ++ (show d) ++"\"];\n"
else if (m1!e==empty)
then if (Data.List.intersect d end /= [])
then a ++" -> " ++ "end" ++ " [color=red2, label= \""++ b ++ "/" ++ c ++ "/" ++ (show d) ++"\"];\n"
else a ++" -> " ++ "close" ++ " [color=red2, label= \""++ b ++ "/" ++ c ++ "/" ++ (show d) ++"\"];\n"
else a ++" -> " ++ e ++ " [color=royalblue, label= \""++ b ++ "/" ++ c ++ "/" ++ (show d) ++"\"];\n"
|((a,b,c,d),e)<-res] ++ ["start" ++" -> " ++ "init" ++ " [color=gray];\n"]) ++
"}}"
in res1
graph :: Int -> IO ()
graph n = do let res = guiGraphRef $ guiGraph n
let res1 = graphViz (fst res) (snd res)
writeFile "states.txt" (show (snd res))
writeFile "graph.dot" res1
{--
runFile :: FilePath -> IO String
runFile f = putStrLn f >> readFile f
fff :: String -> [(Int,(String,[[String]],Int,Int,[(Int,Int)]))]
fff s = read s
actionsAnalyse :: IO ()
actionsAnalyse = do s <- runFile "actionsEnum.txt"
let act = [(a,concat c) | (a,(b,c,d,e,f)) <- fff s]
let act1 = [(a,slicen c "Ident",slicen c "Econst")| (a,c) <- act]
let act1a = [(a,[e | e <-(b!!0), e /= '"', e/= '\\'],c)| (a,b,c) <- act1,length b == 2,(b!!1)=="\"setEnabled\""]
let act2 = [(a,(b,True))|(a,b,c)<-act1a,(c==["Etrue"])]++[(a,b,False)|(a,b,c)<-act1a,(c==["Efalse"])]
writeFile "lixo.txt" (show act2)
--}
main :: IO ()
main = do putStrLn ""
graph 3
|
