a3/code/Gast/ESMSpec.icl

   1 implementation module ESMSpec
   2
   3 import StdBool, StdFunc, StdList, StdListExtensions, StdMaybe, StdMisc, StdString, StdTuple
   4 import GenPrint, GenEq
   5 import gast
   6
   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]
   9
  10 enumerate :: [a] | ggen{|*|} a
  11 enumerate = generateAll aStream
  12
  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))])
  15
  16 nextStates :: (ESM s i o) i ![s] -> [s] | gEq{|*|} s
  17 nextStates esm i states
  18         = gremoveDup    [ t
  19                                 \\      s <- states
  20                                 ,       target <- esm.d_F s i
  21                                 ,       t <- case target of
  22                                                         Pt outs u = [u];
  23                                                         Ft f = [u \\ o<-esm.out s i, u<-f o]
  24                                 ]
  25
  26 narrowTraces :: (Traces s i o) [s] -> Traces s i o | gEq{|*|} s
  27 narrowTraces trace states = fst (pruneTraces trace states)
  28
  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)
  35
  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 ++
  39                 [[      (s,i,o,t)
  40                  \\ s <- 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]
  45                 ]]
  46
  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])
  50
  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]
  53
  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]
  56
  57 startStates :: ![SeenTrans s i o] -> [s] | gEq{|*|} s
  58 startStates transitions                 = gremoveDup [ s \\ (s,i,o,t) <- transitions ]
  59
  60 targetStates :: ![SeenTrans s i o] -> [s] | gEq{|*|} s
  61 targetStates transitions                = gremoveDup [ t \\ (s,i,o,t) <- transitions ]
  62
  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)
  66                 # newSeenTrans
  67                         =       [       (s,i,o,t)
  68                                 \\      s <- 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]
  74                                 ]
  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
  80
  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
  83
  84 insertBy :: (a a->Bool) [a] a -> [a]
  85 insertBy le [] e = [e]
  86 insertBy le l=:[a:x] e
  87         | le e a
  88                 = [e:l]
  89                 = [a:insertBy le x e]
  90
  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)
  93         # rs1 = render s1
  94         # rs2 = render s2
  95         # ro1 = render i1
  96         # ro2 = render i2
  97         # rt1 = render t1
  98         # rt2 = render t2
  99         = rs1<rs2 || (rs1==rs2 && (ro1<ro2 || (ro1==ro2 && rt1<=rt2)))
 100
 101 nrOf :: !(KnownAutomaton s i o) s -> Int | gEq{|*|}, render s
 102 nrOf automaton s
 103         = case gelemIndex s (nodesOf automaton) of
 104                 Just i                                  = i
 105                 nothing                                 = abort ("nrOf applied to unknown state: "+++render s+++"\n")
 106
 107 gisMember :: a ![a] -> Bool | gEq{|*|} a
 108 gisMember x [hd:tl] = hd===x || gisMember x tl
 109 gisMember _ _       = False
 110
 111 gremoveDup :: !.[a] -> .[a] | gEq{|*|} a
 112 gremoveDup [x:xs] = [x:gremoveDup (filter ((=!=) x) xs)]
 113 gremoveDup _      = []
 114
 115 gelemIndex :: a ![a] -> Maybe Int | gEq{|*|} a
 116 gelemIndex x l = scan 0 x l
 117 where
 118         scan i x [a:r]
 119                 | x===a = Just i
 120                                 = scan (i+1) x r
 121         scan i x _ = Nothing
 122