a3/code/Gast/ESMSpec.dcl

   1 definition module ESMSpec
   2
   3 import StdClass, StdMaybe
   4 import gast //gen
   5
   6 ::      Traces             s i o :== [[SeenTrans s i o]]
   7 ::      ESM            s i o =   { s_0 :: s                                     // the initial state
   8                                                          , d_F :: Spec s i o            // the state transition function (\delta_F)
   9                                                          , out :: s i -> [[o]]          // outputs to be used if spec does not give them
  10                                                          , pred:: (SeenTrans s i o)->[[String]] // consitency issues
  11                                                          }
  12 ::      KnownAutomaton s i o =   {trans :: [SeenTrans s i o]
  13                                                          ,issues:: [(SeenTrans s i o,[String])]
  14                                                          }
  15 ::      SeenTrans      s i o :== (s,i,[o],s)
  16
  17 tupToSpec :: (state input -> [([output],state)]) -> Spec state input output // conversion for old specificaions
  18
  19 class render a :: !a -> String          // show a concise text representation for rendering purposes
  20
  21 enumerate               :: [a] | ggen{|*|} a
  22
  23 possibleInputs  :: (ESM s i o) [s] -> [i] | gEq{|*|} s & ggen{|*|}, gEq{|*|} i
  24 nextStates              :: (ESM s i o) i ![s] -> [s] | gEq{|*|} s
  25 addStep                 :: (ESM s i o) [s] i !(Traces s i o) -> Traces s i o | gEq{|*|} s
  26 narrowTraces    :: (Traces s i o) [s] -> Traces s i o | gEq{|*|} s
  27
  28 nodesOf                 :: !(KnownAutomaton s i o) -> [s] | gEq{|*|} s
  29 edgesFrom               :: s !(KnownAutomaton s i o) -> [SeenTrans s i o] | gEq{|*|} s
  30 edgesTo                 :: s !(KnownAutomaton s i o) -> [SeenTrans s i o] | gEq{|*|} s
  31
  32 startStates             :: ![SeenTrans s i o] -> [s] | gEq{|*|} s
  33 targetStates    :: ![SeenTrans s i o] -> [s] | gEq{|*|} s
  34
  35 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
  36
  37 nrOf                    :: !(KnownAutomaton s i o) s -> Int | gEq{|*|}, render s
  38
  39 gisMember  :: a ![a] -> Bool | gEq{|*|} a
  40 gremoveDup :: !.[a] -> .[a] | gEq{|*|} a
  41 gelemIndex :: a ![a] -> Maybe Int | gEq{|*|} a