reset a3, kut Charlie ;)

[tt2015.git] / a3 / code / Gast / ESMSpec.dcl

diff --git a/a3/code/Gast/ESMSpec.dcl b/a3/code/Gast/ESMSpec.dcl
new file mode 100644 (file)
index 0000000..2737b29
--- /dev/null
+++ b/a3/code/Gast/ESMSpec.dcl
@@ -0,0 +1,41 @@
+definition module ESMSpec\r
+\r
+import StdClass, StdMaybe\r
+import gast //gen\r
+\r
+::     Traces             s i o :== [[SeenTrans s i o]]\r
+::     ESM            s i o =   { s_0 :: s                                     // the initial state\r
+                                                        , d_F :: Spec s i o            // the state transition function (\delta_F)\r
+                                                        , out :: s i -> [[o]]          // outputs to be used if spec does not give them\r
+                                                        , pred:: (SeenTrans s i o)->[[String]] // consitency issues\r
+                                                        }\r
+::     KnownAutomaton s i o =   {trans :: [SeenTrans s i o]\r
+                                                        ,issues:: [(SeenTrans s i o,[String])]\r
+                                                        }\r
+::     SeenTrans      s i o :== (s,i,[o],s)\r
+\r
+tupToSpec :: (state input -> [([output],state)]) -> Spec state input output // conversion for old specificaions\r
+\r
+class render a :: !a -> String         // show a concise text representation for rendering purposes\r
+\r
+enumerate              :: [a] | ggen{|*|} a\r
+\r
+possibleInputs :: (ESM s i o) [s] -> [i] | gEq{|*|} s & ggen{|*|}, gEq{|*|} i\r
+nextStates             :: (ESM s i o) i ![s] -> [s] | gEq{|*|} s\r
+addStep                        :: (ESM s i o) [s] i !(Traces s i o) -> Traces s i o | gEq{|*|} s\r
+narrowTraces   :: (Traces s i o) [s] -> Traces s i o | gEq{|*|} s\r
+\r
+nodesOf                        :: !(KnownAutomaton s i o) -> [s] | gEq{|*|} s\r
+edgesFrom              :: s !(KnownAutomaton s i o) -> [SeenTrans s i o] | gEq{|*|} s\r
+edgesTo                        :: s !(KnownAutomaton s i o) -> [SeenTrans s i o] | gEq{|*|} s\r
+\r
+startStates            :: ![SeenTrans s i o] -> [s] | gEq{|*|} s\r
+targetStates   :: ![SeenTrans s i o] -> [s] | gEq{|*|} s\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
+\r
+nrOf                   :: !(KnownAutomaton s i o) s -> Int | gEq{|*|}, render s\r
+\r
+gisMember  :: a ![a] -> Bool | gEq{|*|} a\r
+gremoveDup :: !.[a] -> .[a] | gEq{|*|} a\r
+gelemIndex :: a ![a] -> Maybe Int | gEq{|*|} a\r