1 implementation module ESMSpec
3 import StdBool, StdFunc, StdList, StdListExtensions, StdMaybe, StdMisc, StdString, StdTuple
7 tupToSpec :: (state input -> [([output],state)]) -> Spec state input output // conversion for old specificaions
8 tupToSpec fun = \s i = [Pt o t \\ (o,t) <- fun s i]
10 enumerate :: [a] | ggen{|*|} a
11 enumerate = generateAll aStream
13 possibleInputs :: (ESM s i o) [s] -> [i] | gEq{|*|} s & ggen{|*|}, gEq{|*|} i
14 possibleInputs esm states = gremoveDup (take 100 [i \\ s<-states, i<-enumerate | not (isEmpty (esm.d_F s i))])
16 nextStates :: (ESM s i o) i ![s] -> [s] | gEq{|*|} s
17 nextStates esm i states
20 , target <- esm.d_F s i
23 Ft f = [u \\ o<-esm.out s i, u<-f o]
26 narrowTraces :: (Traces s i o) [s] -> Traces s i o | gEq{|*|} s
27 narrowTraces trace states = fst (pruneTraces trace states)
29 pruneTraces :: (Traces s i o) [s] -> (Traces s i o,[s]) | gEq{|*|} s
30 pruneTraces [] states = ([],states)
31 pruneTraces [trans:rest] states
32 # (rest ,states) = pruneTraces rest states
33 # trans = [tr\\tr=:(s,i,o,t)<-trans|gisMember t states]
34 = ([trans:rest],startStates trans)
36 addStep :: (ESM s i o) [s] i !(Traces s i o) -> Traces s i o | gEq{|*|} s
37 addStep esm states i trace
38 = narrowTraces trace states ++
41 , target <- esm.d_F s i
42 , (o,t) <- case target of
43 Pt outs u = [(outs,u)];
44 Ft f = [ (o,u) \\ o<-esm.out s i, u<-f o]
47 nodesOf :: !(KnownAutomaton s i o) -> [s] | gEq{|*|} s
48 //nodesOf automaton = gremoveDup (flatten [[startnode,endnode] \\ (startnode,_,_,endnode) <- automaton.trans])
49 nodesOf automaton = gremoveDup ([s \\ (s,_,_,t) <- automaton.trans]++[t \\ (s,_,_,t) <- automaton.trans])
51 edgesFrom :: s !(KnownAutomaton s i o) -> [SeenTrans s i o] | gEq{|*|} s
52 edgesFrom startnode automaton = [edge \\ edge=:(s,i,o,t) <- automaton.trans | s===startnode]
54 edgesTo :: s !(KnownAutomaton s i o) -> [SeenTrans s i o] | gEq{|*|} s
55 edgesTo endnode automaton = [edge \\ edge=:(s,i,o,t) <- automaton.trans | t===endnode]
57 startStates :: ![SeenTrans s i o] -> [s] | gEq{|*|} s
58 startStates transitions = gremoveDup [ s \\ (s,i,o,t) <- transitions ]
60 targetStates :: ![SeenTrans s i o] -> [s] | gEq{|*|} s
61 targetStates transitions = gremoveDup [ t \\ (s,i,o,t) <- transitions ]
63 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
64 addTransitions n esm startstates is automaton
65 | n>0 && not (isEmpty startstates)
69 , i <- map snd (sortBy (\(a,_) (b,_).a<b) (map (\i.(render i,i)) is)) // is // sort inputs
70 , target <- esm.d_F s i
71 , (o,t) <- case target of
72 Pt outs u = [(outs,u)];
73 Ft f = [ (o,u) \\ o<-esm.out s i, u<-f o]
75 # newStates = targetStates newSeenTrans
76 # newTrans = [t \\ t <- newSeenTrans | not (gisMember t automaton.trans)]
77 # newIssues = [(t,e) \\ t<-newTrans, e <- esm.pred t | not (isEmpty e)]
78 = addTransitions (n-1) esm newStates (possibleInputs esm newStates) {trans=mix automaton.trans newTrans, issues=newIssues++automaton.issues}
79 | otherwise = automaton
81 mix :: [SeenTrans s i o] [SeenTrans s i o] -> [SeenTrans s i o] | render s & render i
82 mix known new = foldl (insertBy less) known new
84 insertBy :: (a a->Bool) [a] a -> [a]
85 insertBy le [] e = [e]
86 insertBy le l=:[a:x] e
91 less :: (SeenTrans s i o) (SeenTrans s i o) -> Bool | render s & render i
92 less (s1,i1,o1,t1) (s2,i2,o2,t2)
99 = rs1<rs2 || (rs1==rs2 && (ro1<ro2 || (ro1==ro2 && rt1<=rt2)))
101 nrOf :: !(KnownAutomaton s i o) s -> Int | gEq{|*|}, render s
103 = case gelemIndex s (nodesOf automaton) of
105 nothing = abort ("nrOf applied to unknown state: "+++render s+++"\n")
107 gisMember :: a ![a] -> Bool | gEq{|*|} a
108 gisMember x [hd:tl] = hd===x || gisMember x tl
109 gisMember _ _ = False
111 gremoveDup :: !.[a] -> .[a] | gEq{|*|} a
112 gremoveDup [x:xs] = [x:gremoveDup (filter ((=!=) x) xs)]
115 gelemIndex :: a ![a] -> Maybe Int | gEq{|*|} a
116 gelemIndex x l = scan 0 x l