+++ /dev/null
-implementation module ESMSpec\r
-\r
-import StdBool, StdFunc, StdList, StdListExtensions, StdMaybe, StdMisc, StdString, StdTuple\r
-import GenPrint, GenEq\r
-import gast\r
-\r
-tupToSpec :: (state input -> [([output],state)]) -> Spec state input output // conversion for old specificaions\r
-tupToSpec fun = \s i = [Pt o t \\ (o,t) <- fun s i]\r
-\r
-enumerate :: [a] | ggen{|*|} a\r
-enumerate = generateAll aStream\r
-\r
-possibleInputs :: (ESM s i o) [s] -> [i] | gEq{|*|} s & ggen{|*|}, gEq{|*|} i\r
-possibleInputs esm states = gremoveDup (take 100 [i \\ s<-states, i<-enumerate | not (isEmpty (esm.d_F s i))])\r
-\r
-nextStates :: (ESM s i o) i ![s] -> [s] | gEq{|*|} s\r
-nextStates esm i states\r
- = gremoveDup [ t\r
- \\ s <- states\r
- , target <- esm.d_F s i\r
- , t <- case target of\r
- Pt outs u = [u];\r
- Ft f = [u \\ o<-esm.out s i, u<-f o]\r
- ]\r
-\r
-narrowTraces :: (Traces s i o) [s] -> Traces s i o | gEq{|*|} s\r
-narrowTraces trace states = fst (pruneTraces trace states)\r
-\r
-pruneTraces :: (Traces s i o) [s] -> (Traces s i o,[s]) | gEq{|*|} s\r
-pruneTraces [] states = ([],states)\r
-pruneTraces [trans:rest] states\r
- # (rest ,states) = pruneTraces rest states\r
- # trans = [tr\\tr=:(s,i,o,t)<-trans|gisMember t states]\r
- = ([trans:rest],startStates trans)\r
-\r
-addStep :: (ESM s i o) [s] i !(Traces s i o) -> Traces s i o | gEq{|*|} s\r
-addStep esm states i trace\r
- = narrowTraces trace states ++\r
- [[ (s,i,o,t)\r
- \\ s <- states\r
- , target <- esm.d_F s i\r
- , (o,t) <- case target of\r
- Pt outs u = [(outs,u)];\r
- Ft f = [ (o,u) \\ o<-esm.out s i, u<-f o]\r
- ]]\r
-\r
-nodesOf :: !(KnownAutomaton s i o) -> [s] | gEq{|*|} s\r
-//nodesOf automaton = gremoveDup (flatten [[startnode,endnode] \\ (startnode,_,_,endnode) <- automaton.trans])\r
-nodesOf automaton = gremoveDup ([s \\ (s,_,_,t) <- automaton.trans]++[t \\ (s,_,_,t) <- automaton.trans])\r
-\r
-edgesFrom :: s !(KnownAutomaton s i o) -> [SeenTrans s i o] | gEq{|*|} s\r
-edgesFrom startnode automaton = [edge \\ edge=:(s,i,o,t) <- automaton.trans | s===startnode]\r
-\r
-edgesTo :: s !(KnownAutomaton s i o) -> [SeenTrans s i o] | gEq{|*|} s\r
-edgesTo endnode automaton = [edge \\ edge=:(s,i,o,t) <- automaton.trans | t===endnode]\r
-\r
-startStates :: ![SeenTrans s i o] -> [s] | gEq{|*|} s\r
-startStates transitions = gremoveDup [ s \\ (s,i,o,t) <- transitions ]\r
-\r
-targetStates :: ![SeenTrans s i o] -> [s] | gEq{|*|} s\r
-targetStates transitions = gremoveDup [ t \\ (s,i,o,t) <- transitions ]\r
-\r
-addTransitions :: !Int (ESM s i o) [s] [i] !(KnownAutomaton s i o) -> KnownAutomaton s i o | gEq{|*|}, render s & render, ggen{|*|}, gEq{|*|} i & gEq{|*|} o\r
-addTransitions n esm startstates is automaton\r
- | n>0 && not (isEmpty startstates)\r
- # newSeenTrans\r
- = [ (s,i,o,t)\r
- \\ s <- startstates\r
- , i <- map snd (sortBy (\(a,_) (b,_).a<b) (map (\i.(render i,i)) is)) // is // sort inputs\r
- , target <- esm.d_F s i\r
- , (o,t) <- case target of\r
- Pt outs u = [(outs,u)];\r
- Ft f = [ (o,u) \\ o<-esm.out s i, u<-f o]\r
- ]\r
- # newStates = targetStates newSeenTrans\r
- # newTrans = [t \\ t <- newSeenTrans | not (gisMember t automaton.trans)]\r
- # newIssues = [(t,e) \\ t<-newTrans, e <- esm.pred t | not (isEmpty e)]\r
- = addTransitions (n-1) esm newStates (possibleInputs esm newStates) {trans=mix automaton.trans newTrans, issues=newIssues++automaton.issues}\r
- | otherwise = automaton\r
-\r
-mix :: [SeenTrans s i o] [SeenTrans s i o] -> [SeenTrans s i o] | render s & render i\r
-mix known new = foldl (insertBy less) known new\r
-\r
-insertBy :: (a a->Bool) [a] a -> [a]\r
-insertBy le [] e = [e]\r
-insertBy le l=:[a:x] e\r
- | le e a\r
- = [e:l]\r
- = [a:insertBy le x e]\r
-\r
-less :: (SeenTrans s i o) (SeenTrans s i o) -> Bool | render s & render i\r
-less (s1,i1,o1,t1) (s2,i2,o2,t2)\r
- # rs1 = render s1\r
- # rs2 = render s2\r
- # ro1 = render i1\r
- # ro2 = render i2\r
- # rt1 = render t1\r
- # rt2 = render t2\r
- = rs1<rs2 || (rs1==rs2 && (ro1<ro2 || (ro1==ro2 && rt1<=rt2)))\r
-\r
-nrOf :: !(KnownAutomaton s i o) s -> Int | gEq{|*|}, render s\r
-nrOf automaton s\r
- = case gelemIndex s (nodesOf automaton) of\r
- Just i = i\r
- nothing = abort ("nrOf applied to unknown state: "+++render s+++"\n")\r
-\r
-gisMember :: a ![a] -> Bool | gEq{|*|} a\r
-gisMember x [hd:tl] = hd===x || gisMember x tl\r
-gisMember _ _ = False\r
-\r
-gremoveDup :: !.[a] -> .[a] | gEq{|*|} a\r
-gremoveDup [x:xs] = [x:gremoveDup (filter ((=!=) x) xs)]\r
-gremoveDup _ = []\r
-\r
-gelemIndex :: a ![a] -> Maybe Int | gEq{|*|} a\r
-gelemIndex x l = scan 0 x l\r
-where\r
- scan i x [a:r]\r
- | x===a = Just i\r
- = scan (i+1) x r\r
- scan i x _ = Nothing\r
-\r
repositories / tt2015.git / blobdiff