--- /dev/null
+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
--- /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
--- /dev/null
+// Péter Diviánszky, 2007\r
+// Code extended and adapted by Peter Achten, 2007\r
+\r
+definition module Graphviz\r
+\r
+//from StdOverloaded import class ==, class toString\r
+from StdOverloaded import class toString\r
+import StdMaybe\r
+import ESMSpec\r
+import GenEq\r
+\r
+// A digraph contains a title and a list of node definitions\r
+:: Digraph \r
+ = Digraph String [GraphAttribute] [NodeDef] (Maybe SelectedItem)\r
+:: SelectedItem\r
+ = Node Int\r
+\r
+digraphTitle :: !Digraph -> String\r
+digraphAtts :: !Digraph -> [GraphAttribute]\r
+digraphNodes :: !Digraph -> [NodeDef]\r
+digraphSelectedItem :: !Digraph -> Maybe SelectedItem\r
+\r
+// A node definition contains a unique identifier (an integer), a list of node attributes and a list of edge definitions.\r
+// An edge definition contains an identifier (the id of the end node and edge attributes).\r
+:: NodeDef \r
+ = NodeDef !Int ![NodeState] ![NodeAttribute] [EdgeDef]\r
+:: EdgeDef\r
+ :== (!Int,![EdgeAttribute])\r
+:: NodeState\r
+ = NStAllEdgesFound !Bool // all edges of this node are known\r
+\r
+// Convert digraph into list of strings.\r
+// The strings are lines of the graphviz representation of the graph.\r
+printDigraph :: !Digraph -> [String]\r
+\r
+:: GraphAttribute\r
+ = GAtt_Damping Real\r
+ | GAtt_K Real\r
+ | GAtt_URL String\r
+ | GAtt_bb Rect\r
+ | GAtt_bgcolor Color\r
+ | GAtt_center Bool\r
+ | GAtt_charset String\r
+ | GAtt_clusterrank ClusterMode\r
+ | GAtt_colorscheme String\r
+ | GAtt_comment String\r
+ | GAtt_compound Bool\r
+ | GAtt_concentrate Bool\r
+ | GAtt_defaultdist Real\r
+ | GAtt_dim Int\r
+// | GAtt_diredgeconstraints ... PA: ignored, neato only\r
+ | GAtt_dpi Real\r
+ | GAtt_epsilon Real\r
+ | GAtt_esep Real\r
+ | GAtt_fontcolor Color\r
+ | GAtt_fontname String\r
+ | GAtt_fontnames String\r
+ | GAtt_fontpath String\r
+ | GAtt_fontsize Real\r
+ | GAtt_label String\r
+ | GAtt_labeljust String\r
+ | GAtt_labelloc String\r
+ | GAtt_landscape Bool\r
+ | GAtt_layers LayerList\r
+ | GAtt_layersep String\r
+ | GAtt_levelsgap Real\r
+ | GAtt_lp DotPoint\r
+ | GAtt_margin Margin\r
+ | GAtt_maxiter Int\r
+ | GAtt_mclimit Real\r
+ | GAtt_mindist Real\r
+ | GAtt_mode String\r
+ | GAtt_model String\r
+ | GAtt_mosek Bool\r
+ | GAtt_nodesep Real\r
+ | GAtt_nojustify Bool\r
+ | GAtt_normalize Bool\r
+ | GAtt_nslimit Real\r
+ | GAtt_nslimit1 Real\r
+ | GAtt_ordering String\r
+ | GAtt_orientation String\r
+ | GAtt_outputorder OutputMode\r
+ | GAtt_pad Pad\r
+ | GAtt_page Pointf\r
+ | GAtt_pagedir PageDir\r
+ | GAtt_quantum Real\r
+ | GAtt_rank RankType\r
+ | GAtt_rankdir RankDir\r
+ | GAtt_ranksep Real\r
+ | GAtt_ratio Ratio\r
+ | GAtt_remincross Bool\r
+ | GAtt_resolution Real\r
+ | GAtt_root String\r
+ | GAtt_rotate Int\r
+ | GAtt_searchsize Int\r
+ | GAtt_showboxes Int\r
+ | GAtt_size Sizef //Pointf // PA++\r
+// | GAtt_splines PA: skipped for the time being\r
+ | GAtt_start StartType\r
+ | GAtt_stylesheet String\r
+ | GAtt_target String\r
+ | GAtt_truecolor Bool\r
+ | GAtt_viewport ViewPort\r
+ | GAtt_voro_margin Real\r
+:: NodeAttribute\r
+ = NAtt_URL String\r
+ | NAtt_color Color\r
+ | NAtt_colorscheme String\r
+ | NAtt_comment String\r
+ | NAtt_distortion Real\r
+ | NAtt_fillcolor Color\r
+ | NAtt_fixedsize Bool\r
+ | NAtt_fontcolor Color\r
+ | NAtt_fontname String\r
+ | NAtt_fontsize Real\r
+ | NAtt_group String\r
+ | NAtt_height Real\r
+ | NAtt_label String\r
+ | NAtt_layer LayerRange\r
+ | NAtt_margin Margin\r
+ | NAtt_nojustify Bool\r
+ | NAtt_orientation Real\r
+ | NAtt_peripheries Int\r
+ | NAtt_pin Bool\r
+// | NAtt_pos ... PA: ignored for the time being\r
+ | NAtt_rects Rect\r
+ | NAtt_regular Bool\r
+ | NAtt_samplepoints Int\r
+ | NAtt_shape NodeShape\r
+ | NAtt_shapefile String\r
+ | NAtt_showboxes Int\r
+ | NAtt_sides Int\r
+ | NAtt_skew Real\r
+ | NAtt_style NodeStyle\r
+ | NAtt_target String\r
+ | NAtt_tooltip String\r
+ | NAtt_width Real\r
+ | NAtt_z Real\r
+:: EdgeAttribute\r
+ = EAtt_URL String\r
+ | EAtt_arrowhead ArrowType\r
+ | EAtt_arrowsize Real\r
+ | EAtt_arrowtail ArrowType\r
+ | EAtt_color Color\r
+ | EAtt_colorscheme String\r
+ | EAtt_comment String\r
+ | EAtt_constraint Bool\r
+ | EAtt_decorate Bool\r
+ | EAtt_dir DirType\r
+ | EAtt_edgeURL String\r
+ | EAtt_edgehref String\r
+ | EAtt_edgetarget String\r
+ | EAtt_edgetooltip String\r
+ | EAtt_fontcolor Color\r
+ | EAtt_fontname String\r
+ | EAtt_fontsize Real\r
+ | EAtt_headURL String\r
+ | EAtt_headclip Bool\r
+ | EAtt_headhref String\r
+ | EAtt_headlabel String\r
+ | EAtt_headport PortPos\r
+ | EAtt_headtarget String\r
+ | EAtt_headtooltip String\r
+ | EAtt_href String\r
+ | EAtt_label String\r
+ | EAtt_labelURL String\r
+ | EAtt_labelangle Real\r
+ | EAtt_labeldistance Real\r
+ | EAtt_labelfloat Bool\r
+ | EAtt_labelfontcolor Color\r
+ | EAtt_labelfontname String\r
+ | EAtt_labelfontsize Real\r
+ | EAtt_labelhref String\r
+ | EAtt_labeltarget String\r
+ | EAtt_labeltooltip String\r
+ | EAtt_layer LayerRange\r
+ | EAtt_len Real\r
+ | EAtt_lhead String\r
+ | EAtt_lp DotPoint\r
+ | EAtt_ltail String\r
+ | EAtt_minlen Int\r
+ | EAtt_nojustify Bool\r
+// | EAtt_pos PA: ignored for the time being\r
+ | EAtt_samehead String\r
+ | EAtt_sametail String\r
+ | EAtt_showboxes Int\r
+ | EAtt_style EdgeStyle\r
+ | EAtt_tailURL String\r
+ | EAtt_tailclip Bool\r
+ | EAtt_tailhref String\r
+ | EAtt_taillabel String\r
+ | EAtt_tailport PortPos\r
+ | EAtt_tailtarget String\r
+ | EAtt_tailtooltip String\r
+ | EAtt_target String\r
+ | EAtt_tooltip String\r
+ | EAtt_weight Real\r
+:: ClusterMode\r
+ = CM_local | CM_global | CM_none\r
+:: CompassPoint\r
+ = CP_n | CP_ne | CP_e | CP_se | CP_s | CP_sw | CP_w | CP_nw\r
+:: DotPoint\r
+ = DotPoint Real Real Bool\r
+:: LayerId\r
+ = LayerAll\r
+ | LayerNr Int\r
+ | LayerName String\r
+:: LayerList\r
+ = LayerList [String]\r
+:: LayerRange\r
+ = LayerRange LayerId [LayerId]\r
+:: Margin\r
+ = SingleMargin Real\r
+ | DoubleMargin Real Real\r
+:: OutputMode\r
+ = OM_breadthfirst | OM_nodesfirst | OM_edgesfirst\r
+:: Pad\r
+ = SinglePad Real\r
+ | DoublePad Real Real\r
+:: PageDir\r
+ = PD_BL | PD_BR | PD_TL | PD_TR | PD_RB | PD_RT | PD_LB | PD_LT\r
+:: Pointf\r
+ = Pointf Real Real\r
+:: PortPos // PA: for now only compass points are supported\r
+ :== CompassPoint\r
+:: RankDir\r
+ = RD_TB | RD_LR | RD_BT | RD_RL\r
+:: RankType\r
+ = RT_same | RT_min | RT_source | RT_max | RT_sink\r
+:: Ratio\r
+ = AspectRatio Real\r
+ | R_fill\r
+ | R_compress\r
+ | R_expand\r
+ | R_auto\r
+:: Rect\r
+ = {llx :: Int,lly :: Int, urx :: Int, ury :: Int}\r
+:: Sizef // PA++\r
+ = Sizef Real Real Bool\r
+:: StartStyle\r
+ = SS_regular | SS_self | SS_random\r
+:: StartType\r
+ = { startStyle :: Maybe StartStyle\r
+ , startSeed :: Maybe Int\r
+ }\r
+:: ViewPort\r
+ = { vp_W :: Real\r
+ , vp_H :: Real\r
+ , vp_Z :: Maybe Real\r
+ , vp_xy :: Maybe Pointf\r
+ }\r
+\r
+pointNode :: [NodeAttribute] // attributes of a point-shaped node\r
+hiddenNode :: [NodeAttribute] // attributes of a hidden node\r
+\r
+\r
+:: NodeShape \r
+ = NShape_box\r
+ | NShape_circle \r
+ | NShape_diamond\r
+ | NShape_doublecircle\r
+ | NShape_doubleoctagon\r
+ | NShape_egg\r
+ | NShape_ellipse \r
+ | NShape_hexagon\r
+ | NShape_house\r
+ | NShape_invtriangle\r
+ | NShape_invtrapezium\r
+ | NShape_invhouse\r
+ | NShape_octagon\r
+ | NShape_Mdiamond\r
+ | NShape_Msquare\r
+ | NShape_Mcircle\r
+ | NShape_parallelogram \r
+ | NShape_pentagon\r
+ | NShape_plainText\r
+ | NShape_polygon\r
+ | NShape_point \r
+ | NShape_rect\r
+ | NShape_rectangle\r
+ | NShape_septagon\r
+ | NShape_trapezium\r
+ | NShape_triangle\r
+ | NShape_tripleoctagon\r
+ | NShape_none\r
+instance toString NodeShape\r
+instance == NodeShape\r
+derive gEq NodeShape // PK++\r
+\r
+:: NodeStyle\r
+ = NStyle_filled\r
+ | NStyle_invis\r
+ | NStyle_diagonals\r
+ | NStyle_rounded\r
+ | NStyle_dashed\r
+ | NStyle_dotted\r
+ | NStyle_solid\r
+ | NStyle_bold\r
+instance toString NodeStyle\r
+instance == NodeStyle\r
+derive gEq NodeStyle // PK++\r
+\r
+:: EdgeStyle \r
+ = EStyle_solid \r
+ | EStyle_bold\r
+ | EStyle_dashed\r
+ | EStyle_dotted\r
+ | EStyle_invis\r
+instance toString EdgeStyle\r
+instance == EdgeStyle\r
+derive gEq EdgeStyle // PK++\r
+\r
+:: Color \r
+ = RGB Int Int Int\r
+ | HSV Real Real Real\r
+ | Color String // X11 1.2 color names; see rgb.txt\r
+\r
+C_black :== Color "black"\r
+C_white :== Color "white"\r
+C_gray :== Color "gray"\r
+C_red :== Color "red"\r
+C_green :== Color "green"\r
+C_blue :== Color "blue"\r
+C_yellow :== Color "yellow"\r
+\r
+instance toString Color\r
+instance == Color\r
+derive gEq Color // PK++\r
+\r
+:: ArrowType =\r
+ { closest :: Arrow\r
+ , furthest :: Maybe Arrow\r
+ }\r
+:: Arrow =\r
+ { open :: Bool\r
+ , side :: Maybe Side\r
+ , shape :: ArrowShape\r
+ }\r
+:: Side\r
+ = Side_l\r
+ | Side_r\r
+:: ArrowShape\r
+ = AShape_box\r
+ | AShape_crow\r
+ | AShape_diamond\r
+ | AShape_dot\r
+ | AShape_inv\r
+ | AShape_none\r
+ | AShape_normal\r
+ | AShape_tee\r
+ | AShape_vee\r
+instance toString ArrowType\r
+instance == ArrowType\r
+derive gEq ArrowType // PK++\r
+\r
+\r
+// direction of the edge\r
+:: DirType\r
+ = DT_forward \r
+ | DT_back \r
+ | DT_both \r
+ | DT_none\r
+instance toString DirType\r
+instance == DirType\r
+derive gEq DirType // PK++\r
+\r
+layersep :== ":\t"\r
+\r
+mkDigraph :: String (KnownAutomaton s i o,s,[s],[s],[SeenTrans s i o],[SeenTrans s i o]) -> Digraph | render, gEq{|*|} s \r
+ & render, gEq{|*|} i \r
+ & render, gEq{|*|} o\r
--- /dev/null
+// Péter Diviánszky, 2007\r
+// Code extended and adapted for using generics by Peter Achten, 2007\r
+\r
+implementation module Graphviz\r
+\r
+import StdArray, StdOverloaded, StdList, StdOrdList, StdTuple, StdString, StdBool, StdMisc\r
+import StdMaybe, StdListExtensions\r
+import GenLib\r
+import ESMSpec\r
+\r
+derive gEq EdgeStyle, NodeStyle, DirType, NodeShape, Side, ArrowShape, Maybe, ArrowType, Arrow, Color\r
+derive gPrint EdgeStyle, NodeStyle, DirType, NodeShape, Side, ArrowShape, Maybe, CompassPoint, StartStyle,\r
+ ClusterMode, OutputMode, PageDir, RankDir, RankType\r
+derive printNameValuePair GraphAttribute, NodeAttribute, EdgeAttribute\r
+\r
+// Almost regular toString instances:\r
+instance toString EdgeStyle where toString es = /*quote*/ (skipXXX_InConstructorName (printToString es))\r
+instance toString NodeStyle where toString ns = quote (skipXXX_InConstructorName (printToString ns))\r
+instance toString DirType where toString dir = quote (skipXXX_InConstructorName (printToString dir))\r
+instance toString NodeShape where toString ns = skipXXX_InConstructorName (printToString ns)\r
+instance toString Side where toString s = skipXXX_InConstructorName (printToString s)\r
+instance toString ArrowShape where toString s = skipXXX_InConstructorName (printToString s)\r
+instance toString CompassPoint where toString cp = quote (skipXXX_InConstructorName (printToString cp))\r
+instance toString ClusterMode where toString cm = quote (skipXXX_InConstructorName (printToString cm))\r
+instance toString OutputMode where toString om = quote (skipXXX_InConstructorName (printToString om))\r
+instance toString PageDir where toString pd = skipXXX_InConstructorName (printToString pd)\r
+instance toString RankDir where toString rd = skipXXX_InConstructorName (printToString rd)\r
+instance toString RankType where toString rt = skipXXX_InConstructorName (printToString rt)\r
+instance toString StartStyle where toString ss = skipXXX_InConstructorName (printToString ss)\r
+instance toString NodeAttribute where toString na = printNameValuePair{|*|} na\r
+instance toString EdgeAttribute where toString ea = printNameValuePair{|*|} ea\r
+instance toString GraphAttribute where toString ga = printNameValuePair{|*|} ga\r
+// Less regular toString instances:\r
+instance toString Arrow where\r
+ toString {open,side,shape} = if open "o" "" +++ if (isJust side) (toString (fromJust side)) "" +++ toString shape\r
+instance toString ArrowType where\r
+ toString {closest,furthest} = quote (toString closest +++ if (isJust furthest) (toString (fromJust furthest)) "")\r
+instance toString Color where\r
+ toString (Color name) = name\r
+\r
+ toString (HSV h s v) = "\"" $> toS h $> " " $> toS s $> " " $> toS v $> "\""\r
+ where\r
+ toS x\r
+ | x<0.0 || x>1.0 = abort "HSV value out of range.\n" \r
+ | otherwise = toString (toReal (toInt (1000.0*x)) / 1000.0)\r
+\r
+ toString (RGB r g b) = "\"#" $> toS r $> toS g $> toS b $> "\""\r
+ where\r
+ toS x \r
+ | x<0 || x>255 = abort "RGB value out of range.\n" \r
+ | otherwise = toString [toC (x/16), toC (x rem 16)] \r
+ toC x \r
+ | x < 10 = toChar (x + fromChar '0')\r
+ | otherwise = toChar (x - 10 + fromChar 'A')\r
+instance toString DotPoint where\r
+ toString (DotPoint x y fix) = x >$ "," >$ y >$ if fix "!" ""\r
+instance toString LayerId where\r
+ toString layerid = case layerid of\r
+ LayerAll = "all"\r
+ LayerNr nr = toString nr\r
+ LayerName str = str\r
+instance toString LayerList where\r
+ toString (LayerList names) = foldr (\next before -> before $> layersep $> next) "" names\r
+instance toString LayerRange where\r
+ toString (LayerRange id ids)= foldr (\next before -> before $> layersep $> next) (toString id) ids\r
+instance toString Margin where\r
+ toString margin = case margin of\r
+ SingleMargin a = toString a\r
+ DoubleMargin a b = a >$ "," $> b\r
+instance toString Pad where\r
+ toString pad = case pad of\r
+ SinglePad a = toString a\r
+ DoublePad a b = a >$ "," $> b\r
+instance toString Pointf where\r
+ toString (Pointf x y) = quote (x >$ "," $> y)\r
+instance toString Ratio where\r
+ toString ratio = case ratio of\r
+ AspectRatio r = quote (toString r)\r
+ R_fill = quote "fill"\r
+ R_compress = quote "compress"\r
+ R_expand = quote "expand"\r
+ R_auto = quote "auto"\r
+instance toString Rect where\r
+ toString {llx,lly,urx,ury} = llx >$ "," $> lly >$ "," $> urx >$ "," $> ury\r
+instance toString Sizef where // PA++\r
+ toString (Sizef x y True) = "\"" +++ toString x +++ "," +++ toString y +++ "!\""\r
+ toString (Sizef x y False) = "\"" +++ toString x +++ "," +++ toString y +++ "\""\r
+instance toString StartType where\r
+ toString {startStyle,startSeed}\r
+ = if (isJust startStyle) (toString (fromJust startStyle)) "" +++ \r
+ if (isJust startSeed) (toString (fromJust startSeed )) ""\r
+instance toString ViewPort where\r
+ toString {vp_W,vp_H,vp_Z,vp_xy}\r
+ = (vp_W >$ "," $> vp_H) +++ \r
+ if (isJust vp_Z ) ("," $> (fromJust vp_Z )) "" +++\r
+ if (isJust vp_xy) ("," $> (fromJust vp_xy)) ""\r
+\r
+// Print name=value pairs for algebraic data types with unary data constructors in XXX_name constructor name format.\r
+generic printNameValuePair a :: a -> String\r
+printNameValuePair{|Int|} x = toString x\r
+printNameValuePair{|Real|} x = toString x\r
+printNameValuePair{|Char|} x = toString x\r
+printNameValuePair{|String|} x = quote x\r
+printNameValuePair{|Bool|} x = firstCharLowerCase (toString x)\r
+printNameValuePair{|UNIT|} x = ""\r
+printNameValuePair{|PAIR|} px py (PAIR x y) = px x +++ " " +++ py y\r
+printNameValuePair{|EITHER|} pl pr (LEFT x) = pl x\r
+printNameValuePair{|EITHER|} pl pr (RIGHT y) = pr y\r
+printNameValuePair{|OBJECT|} px (OBJECT x) = px x\r
+printNameValuePair{|CONS of d|} px (CONS x) = skipXXX_InConstructorName d.gcd_name +++ "=" +++ px x\r
+// Specializations of printNameValuePair:\r
+printNameValuePair{|ArrowType|} x = toString x\r
+printNameValuePair{|Color|} x = toString x\r
+printNameValuePair{|ClusterMode|} x = toString x\r
+printNameValuePair{|CompassPoint|} x = toString x\r
+printNameValuePair{|DirType|} x = toString x\r
+printNameValuePair{|DotPoint|} x = toString x\r
+printNameValuePair{|EdgeStyle|} x = toString x\r
+printNameValuePair{|LayerList|} x = toString x\r
+printNameValuePair{|LayerRange|} x = toString x\r
+printNameValuePair{|Margin|} x = toString x\r
+printNameValuePair{|NodeShape|} x = toString x\r
+printNameValuePair{|NodeStyle|} x = toString x\r
+printNameValuePair{|OutputMode|} x = toString x\r
+printNameValuePair{|Pad|} x = toString x\r
+printNameValuePair{|PageDir|} x = toString x\r
+printNameValuePair{|Pointf|} x = toString x\r
+printNameValuePair{|RankDir|} x = toString x\r
+printNameValuePair{|RankType|} x = toString x\r
+printNameValuePair{|Ratio|} x = toString x\r
+printNameValuePair{|Rect|} x = toString x\r
+printNameValuePair{|Sizef|} x = toString x // PA++\r
+printNameValuePair{|StartType|} x = toString x\r
+printNameValuePair{|ViewPort|} x = toString x\r
+\r
+instance == EdgeStyle where (==) a b = gEq{|*|} a b\r
+instance == NodeStyle where (==) a b = gEq{|*|} a b\r
+instance == DirType where (==) a b = gEq{|*|} a b\r
+instance == NodeShape where (==) a b = gEq{|*|} a b\r
+instance == ArrowType where (==) a b = gEq{|*|} a b\r
+instance == Color where (==) a b = gEq{|*|} a b\r
+\r
+\r
+digraphTitle :: !Digraph -> String\r
+digraphTitle (Digraph title _ _ _) = title\r
+\r
+digraphAtts :: !Digraph -> [GraphAttribute]\r
+digraphAtts (Digraph _ atts _ _) = atts\r
+\r
+digraphNodes :: !Digraph -> [NodeDef]\r
+digraphNodes (Digraph _ _ nodes _) = nodes\r
+\r
+digraphSelectedItem :: !Digraph -> Maybe SelectedItem\r
+digraphSelectedItem (Digraph _ _ _ selected) = selected\r
+\r
+pointNode :: [NodeAttribute]\r
+pointNode =: [NAtt_shape NShape_point]\r
+\r
+hiddenNode :: [NodeAttribute]\r
+hiddenNode =: [NAtt_shape NShape_point,NAtt_style NStyle_invis]\r
+\r
+commaseparatedlist :: [String] -> String\r
+commaseparatedlist [] = ""\r
+commaseparatedlist l = "[" +++ (foldr (+++) "" (intersperse "," l)) +++ "]"\r
+\r
+printDigraph :: !Digraph -> [String]\r
+//printDigraph (Digraph title atts nodes _) = map (\x->x+++"\n") (prelude title (graphAtts atts) (contents nodes))\r
+printDigraph digraph = case includeChanges digraph of\r
+ Digraph title atts nodes _ -> map (\x->x+++"\n") (prelude title (graphAtts atts) (contents nodes))\r
+\r
+includeChanges :: !Digraph -> Digraph\r
+includeChanges dg=:(Digraph _ _ _ Nothing) = dg\r
+includeChanges (Digraph title atts nodes change)= Digraph title atts (map includeNodeChange nodes) Nothing\r
+where\r
+ (Node nr`) = fromJust change\r
+ \r
+ includeNodeChange :: !NodeDef -> NodeDef\r
+ includeNodeChange (NodeDef nr st atts edges)\r
+ | nr==nr` = NodeDef nr st (map replaceNodeAtt atts) edges\r
+ | otherwise = NodeDef nr st (map defaultNodeAtt atts) edges\r
+ where\r
+ all_edges_found = not (isEmpty [s \\ s=:(NStAllEdgesFound True) <- st])\r
+ \r
+ replaceNodeAtt (NAtt_fillcolor _) = NAtt_fillcolor (fst (active_state_color 1))\r
+ replaceNodeAtt (NAtt_fontcolor _) = NAtt_fontcolor (snd (active_state_color 1))\r
+ replaceNodeAtt att = att\r
+ \r
+ defaultNodeAtt (NAtt_fillcolor c) = NAtt_fillcolor (if all_edges_found (fst finished_state_color) (fst default_state_color))\r
+ defaultNodeAtt (NAtt_fontcolor c) = NAtt_fontcolor (if all_edges_found (snd finished_state_color) (snd default_state_color))\r
+ defaultNodeAtt att = att\r
+\r
+createGraphName :: !String -> String\r
+createGraphName "" = "G"\r
+createGraphName x = x\r
+\r
+prelude :: !String ![String] ![String] -> [String]\r
+prelude title graphAtts contents = [ "digraph " +++ createGraphName title +++ " {"\r
+ , "label=" +++ quote title \r
+ ] ++ \r
+ graphAtts ++ \r
+ contents ++ \r
+ [ "}" ]\r
+\r
+graphAtts :: ![GraphAttribute] -> [String]\r
+graphAtts graphAtts = map printNameValuePair{|*|} graphAtts\r
+\r
+contents :: ![NodeDef] -> [String]\r
+contents nodeDefs = map snd (mergeBy (\(x,_) (y,_)= x<y) nodes` edges`)\r
+where\r
+ (nodes,edges) = unzip (mapSt f nodeDefs 1)\r
+ where\r
+ f (NodeDef id st na edges) num = ( ((num,id,na)\r
+ ,[(n,id,id`,ea) \\ (id`,ea)<- edges & n<-[num+1..]]\r
+ )\r
+ , num + 1 + length edges\r
+ )\r
+ \r
+ nodes` = map (\(num, id, atts) = (num, id >$ commaseparatedlist (map toString atts))) nodes\r
+ edges` = map (\(num,source,target,atts) = (num,source >$ "->" $> target >$ commaseparatedlist (map toString atts))) (flatten edges)\r
+\r
+\r
+mkDigraph :: String (KnownAutomaton s i o,s,[s],[s],[SeenTrans s i o],[SeenTrans s i o]) -> Digraph | render, gEq{|*|} s & render, gEq{|*|} i & render, gEq{|*|} o\r
+mkDigraph name (automaton,s_0,init_states,finished,issues,trace)\r
+ = Digraph\r
+ (remove_spaces name)\r
+ graphAttributes\r
+ (if (isEmpty automaton.trans)\r
+ [NodeDef 0 [NStAllEdgesFound (gisMember s_0 finished)] (nodeAttributes s_0 init_states (gisMember s_0 finished)) []]\r
+ [NodeDef (nrOf automaton n) [NStAllEdgesFound (gisMember n finished)] (nodeAttributes n init_states (gisMember n finished))\r
+ [ let (s,i,o,t) = trans in\r
+ (nrOf automaton t , [ EAtt_label (render i+++"/"+++showList ("[","]",",") o)\r
+ , EAtt_fontname "Helvetica"\r
+ , EAtt_fontsize fontsize\r
+ , EAtt_labelfontname "Helvetica"\r
+ , EAtt_labelfontsize fontsize\r
+ , EAtt_color\r
+ (if (gisMember trans issues)\r
+ (Color "red")\r
+ (if (gisMember trans trace)\r
+ (Color "blue")\r
+ (Color "black")))\r
+ , EAtt_arrowsize (if (gisMember trans trace) 2.0 1.2)\r
+ // , EAtt_style (if (isMember trans trace) EStyle_bold EStyle_solid)\r
+ ])\r
+ \\ trans <- edgesFrom n automaton\r
+ ]\r
+ \\ n <- let nodes = nodesOf automaton in if (gisMember s_0 nodes && hd nodes =!= s_0) [s_0:filter ((=!=) s_0) nodes] nodes\r
+ ]\r
+ ) Nothing\r
+where\r
+ graphAttributes = [ GAtt_rankdir RD_LR\r
+ , GAtt_size (Sizef 10.0 6.0 True)\r
+ , GAtt_bgcolor (Color "lightsteelblue")\r
+ , GAtt_ordering "out"\r
+ , GAtt_outputorder OM_nodesfirst // OM_edgesfirst // PK\r
+ ]\r
+ nodeAttributes n init_states finished\r
+ = (if (gisMember n init_states) [ NAtt_fillcolor act_backgr, NAtt_fontcolor act_txt ]\r
+ (if finished [ NAtt_fillcolor done_backgr,NAtt_fontcolor done_txt]\r
+ [ NAtt_fillcolor def_backgr, NAtt_fontcolor def_txt ]\r
+ )) ++\r
+ [ NAtt_label (render n)\r
+ , NAtt_style NStyle_filled\r
+ , NAtt_shape (if (n === s_0) NShape_doublecircle NShape_circle)\r
+ , NAtt_fontname "Helvetica"\r
+ , NAtt_fontsize fontsize\r
+ , NAtt_fixedsize True\r
+ , NAtt_width 1.0, NAtt_height 1.0\r
+ ]\r
+ where\r
+ ( act_backgr, act_txt) = active_state_color (length init_states)\r
+ (done_backgr,done_txt) = finished_state_color\r
+ ( def_backgr, def_txt) = default_state_color\r
+\r
+active_state_color :: !Int -> (!Color,!Color)\r
+active_state_color nr = (RGB 255 dim dim,Color "white")\r
+where\r
+ dim = min 250 (255 - 255 / nr)\r
+\r
+finished_state_color :: (!Color,!Color)\r
+finished_state_color = (Color "blue", Color "white")\r
+\r
+default_state_color :: (!Color,!Color)\r
+default_state_color = (Color "grey90",Color "black")\r
+\r
+fontsize = 11.0\r
+\r
+// Utility functions:\r
+\r
+mapSt :: (a b -> (c,b)) [a] b -> [c]\r
+mapSt f [] st = []\r
+mapSt f [h:t] st \r
+ #! (x, st) = f h st\r
+ = [x : mapSt f t st]\r
+\r
+quote :: !String -> String\r
+quote a = "\"" $> (flatten (map f (fromString a))) >$ "\""\r
+where\r
+ f '\"' = ['\\\"']\r
+ f x = [x]\r
+\r
+skipXXX_InConstructorName :: !String -> String\r
+skipXXX_InConstructorName str\r
+ = case dropWhile ((<>) '_') [c \\ c<-:str] of\r
+ [] = str\r
+ underscoreName = str % (n-length underscoreName+1,n-1)\r
+where\r
+ n = size str\r
+\r
+firstCharLowerCase :: !String -> String\r
+firstCharLowerCase str\r
+ | size str > 0 = str := (0,toLower str.[0])\r
+ | otherwise = str\r
+\r
+($>) infixr 5 :: !String !a -> String | toString a\r
+($>) str arg = str +++ toString arg\r
+\r
+(>$) infixr 5 :: !a !String -> String | toString a\r
+(>$) arg str = toString arg +++ str\r
+\r
+showList :: !(!String,!String,!String) ![a] -> String | render a\r
+showList (open,close,delimit) [] = open +++ close\r
+showList (open,close,delimit) [x] = open +++ render x +++ close\r
+showList (open,close,delimit) xs = open +++ foldr (\x str->render x+++delimit+++str) "" (init xs) +++ render (last xs) +++ close\r
+\r
+remove_spaces :: !String -> String\r
+remove_spaces str = {c \\ c<-:str | not (isSpace c)}\r
--- /dev/null
+definition module confSM\r
+\r
+/*\r
+ GAST: A Generic Automatic Software Test-system\r
+ \r
+ ioco: Input Output COnformance of reactive systems\r
+\r
+ Pieter Koopman, 2004-2008\r
+ Radboud Universty, Nijmegen\r
+ The Netherlands\r
+ pieter@cs.ru.nl\r
+*/\r
+\r
+import StdEnv, MersenneTwister, gen, genLibTest, testable, StdMaybe\r
+\r
+:: Spec state input output :== state input -> [Trans output state]\r
+:: Trans output state = Pt [output] state | Ft ([output]->[state])\r
+derive genShow Trans\r
+\r
+:: TestOption s i o\r
+ = Ntests Int\r
+ | Nsequences Int\r
+ | Seed Int\r
+ | Randoms [Int]\r
+ | FixedInputs [[i]]\r
+ | InputFun (RandomStream s -> [i])\r
+ | OnPath Int\r
+ | FSM [i] (s->[i]) // inputs state_identification\r
+ | MkTrace Bool\r
+ | OnTheFly\r
+ | SwitchSpec (Spec s i o)\r
+ | OnAndOffPath\r
+ | ErrorFile String\r
+ | Stop ([s] -> Bool)\r
+ | Inconsistent ([o] [s] -> Maybe [String])\r
+\r
+:: IUTstep t i o :== t -> .(i -> .([o],t))\r
+SpectoIUTstep :: (Spec t i o) (t i -> [[o]]) -> IUTstep (t,RandomStream) i o | genShow{|*|} t & genShow{|*|} i & genShow{|*|} o\r
+\r
+toSpec :: (state input -> [(state,[output])]) -> Spec state input output\r
+\r
+genLongInputs :: s (Spec s i o) [i] Int [Int] -> [[i]]\r
+generateFSMpaths :: s (Spec s i o) [i] (s->[i]) -> [[i]] | gEq{|*|} s\r
+\r
+//testConfSM :: [TestOption s i o] (Spec s i o) s (IUTstep .t i o) .t (.t->.t) *d -> (.t,*d)\r
+// | FileSystem d & ggen{|*|} i & gEq{|*|} s & gEq{|*|} o & genShow{|*|} s & genShow{|*|} i & genShow{|*|} o\r
+testConfSM :: [TestOption s i o] (Spec s i o) s (IUTstep .t i o) .t (.t->.t) *File *File -> (.t,*File,*File)\r
+ | ggen{|*|} i & gEq{|*|} s & gEq{|*|} o & genShow{|*|} s & genShow{|*|} i & genShow{|*|} o\r
+\r
+(after) infix 0 :: [s] (Spec s i o) -> ([i] -> [s])\r
+\r
+propDeterministic :: (Spec s i o) s i -> Bool\r
+propTotal :: (Spec s i o) s i -> Bool\r
+//propComplete :: (Spec s i o) s i -> Bool // equal to propTotal\r
+propComplete spec s i :== propTotal spec s i\r
--- /dev/null
+implementation module confSM\r
+\r
+/*\r
+ GAST: A Generic Automatic Software Test-system\r
+ \r
+ ioco: Input Output COnformance of reactive systems\r
+\r
+ Pieter Koopman, 2004, 2005\r
+ Radboud Universty, Nijmegen\r
+ The Netherlands\r
+ pieter@cs.ru.nl\r
+*/\r
+\r
+import StdEnv, MersenneTwister, gen, GenEq, genLibTest, testable, StdLib\r
+\r
+toSpec :: (state input -> [(state,[output])]) -> Spec state input output // conversion for old specificaions\r
+toSpec fun = \s i = [Pt o t \\ (t,o) <- fun s i]\r
+\r
+SpectoIUTstep :: (Spec t i o) (t i -> [[o]]) -> IUTstep (t,RandomStream) i o | genShow{|*|} t & genShow{|*|} i & genShow{|*|} o\r
+SpectoIUTstep spec outputGen = selectTrans\r
+where\r
+ selectTrans (t,[r,r2,r3:rnd]) i\r
+ # tuples = spec t i\r
+ len = lengthN 353 0 tuples\r
+ | len == 0\r
+ = abort ("\n\nIUT is not input enabled in state "+show1 t+" for input "+show1 i+"\n")\r
+ = case tuples !! ((abs r) rem len) of\r
+ Pt o t = (o,(t,rnd))\r
+ Ft f # outputs = outputGen t i\r
+ leno = lengthN 31 0 outputs\r
+ | leno == 0\r
+ = abort ("\n\nOutput function yields no output in state "+show1 t+" for input "+show1 i+"\n")\r
+ # output = outputs !! ((abs r2) rem leno)\r
+ states = f output\r
+ lens = lengthN 37 0 states\r
+ | lens == 0\r
+ = abort ("\n\nIUT is not input enabled in state "+show1 t+" for input "+show1 i+" output "+show1 output+"\n")\r
+ = (output,(states !! ((abs r3) rem lens),rnd))\r
+ \r
+ // =abort "toUIT"\r
+\r
+:: NewInput i = NewInput i | Reset | End\r
+\r
+:: *TestState s i o\r
+ = !{ spec :: !Spec s i o\r
+// , specW :: !SpecWorld s i\r
+ , iniState:: !s\r
+ , curState:: ![s]\r
+ , nRej :: !Int\r
+ , nTrun :: !Int\r
+ , nPath :: !Int\r
+ , nStep :: !Int\r
+ , nTotal :: !Int\r
+ , maxPath :: !Int\r
+ , maxLen :: !Int\r
+ , nOnPath :: !Int\r
+ , inputs :: (RandomStream s -> [i])\r
+ , input :: !((TestState s i o) -> *(NewInput i, TestState s i o))\r
+ , n :: !Int\r
+ , rnd :: RandomStream\r
+ , h_in :: [i]\r
+ , h_out :: [[o]]\r
+ , h_state :: [[s]]\r
+ , fileName:: String\r
+ , errFile :: !*File\r
+ , mesFile :: !*File\r
+ , trace :: !Bool\r
+ , incons :: [o] [s] -> Maybe [String]\r
+ , stop :: [s] -> Bool\r
+ }\r
+/*\r
+apply :: i (IUT s i o) -> ([o],IUT s i o) | genShow{|*|} s & genShow{|*|} i\r
+apply i (IUT f s [r:rnd])\r
+ = case f s i of\r
+ [] = abort ("IUT is not input enabled! State: "+++show1 s+++", input: "+++show1 i)\r
+ list\r
+ # n = length list\r
+ (t,o) = list !! ((abs r) rem n)\r
+ = (o,IUT f t rnd)\r
+*/\r
+ \r
+switchSpec :: (Spec s i o) (TestState s i o) -> *(NewInput i, TestState s i o) | ggen{|*|} i\r
+switchSpec spec ts=:{nOnPath} = newSpec spec nOnPath ts\r
+\r
+newSpec :: (Spec s i o) !Int (TestState s i o) -> *(NewInput i, TestState s i o) | ggen{|*|} i\r
+newSpec spec2 0 ts=:{spec} = oldSpec spec {ts & spec = spec2}\r
+newSpec spec2 n ts\r
+ # (i,ts) = onTheFly ts\r
+ = case i of\r
+ Reset = (i,{ ts & input = newSpec spec2 ts.nOnPath })\r
+ NewInput _ = (i,{ ts & input = newSpec spec2 (n-1)})\r
+ _ = (i,ts)\r
+\r
+oldSpec :: (Spec s i o) (TestState s i o) -> *(NewInput i, TestState s i o) | ggen{|*|} i\r
+oldSpec spec2 ts\r
+ # (i,ts) = onTheFly ts\r
+ = case i of\r
+ Reset = (i,{ ts & input = newSpec spec2 ts.nOnPath })\r
+ _ = (i,ts)\r
+\r
+onAndOff :: (TestState s i o) -> *(NewInput i, TestState s i o) | ggen{|*|} i\r
+onAndOff ts=:{nOnPath} = onPath nOnPath ts\r
+\r
+onPath :: Int (TestState s i o) -> *(NewInput i, TestState s i o) | ggen{|*|} i\r
+onPath 0 ts=:{spec}\r
+ # (rnd1,rnd2) = split ts.rnd\r
+ = offPath spec (ggen{|*|} 2 rnd1) {ts & spec = mkComplete spec, rnd = rnd2} \r
+onPath n ts\r
+ # (i,ts) = onTheFly ts\r
+ = case i of\r
+ Reset = (i,{ ts & input = onPath ts.nOnPath })\r
+ NewInput _ = (i,{ ts & input = onPath (n-1)})\r
+ _ = (i,ts)\r
+\r
+mkComplete spec s i\r
+ = case spec s i of\r
+ [] = [Pt [] s]\r
+ r = r\r
+\r
+offPath :: (Spec s i o) [i] (TestState s i o) -> *(NewInput i, TestState s i o) | ggen{|*|} i\r
+offPath spec [] ts = (Reset,{ ts & input = onPath ts.nOnPath })\r
+offPath spec [i:r] ts\r
+ | ts.nStep >= ts.maxLen-1 || ts.nRej >= ts.maxLen-1\r
+ = (Reset,{ ts & input = onPath ts.nOnPath })\r
+ = (NewInput i,{ts & input = offPath spec r})\r
+\r
+onTheFly :: (TestState s i o) -> *(NewInput i, TestState s i o)\r
+onTheFly ts=:{curState,inputs,rnd,spec}\r
+ # [r1,r2:rnd] = rnd\r
+ = case [ i \\ s <- randomize curState (genRandInt r1) 2 (\_=[])\r
+ , i <- inputs (genRandInt r2) s\r
+ | not (isEmpty (spec s i))\r
+ ] of\r
+ [] = (Reset, {ts & rnd=rnd})\r
+ is # max = 157 // the maximum number of outputs to consider\r
+ n = lengthN max 0 is // the number of the selected input\r
+ [r:rnd] = rnd\r
+ i = is !! ((abs r) rem n)\r
+ = (NewInput i,{ts & rnd = rnd})\r
+\r
+lengthN :: !Int !Int ![a] -> Int\r
+lengthN m n [] = n\r
+lengthN m n [a:x]\r
+ | n<m\r
+ = lengthN m (n+1) x\r
+ = m\r
+\r
+fixedInputs [] ts = (End, ts)\r
+fixedInputs [[] :r] ts = (Reset, { ts & input = fixedInputs r })\r
+fixedInputs [[a:x]:r] ts=:{curState,spec} \r
+ | isEmpty [t \\ s<- curState, t<-spec s a]\r
+ = (Reset, { ts & input = fixedInputs r , nTrun = ts.nTrun+1})\r
+ = (NewInput a, {ts & input = fixedInputs [x:r]})\r
+\r
+genLongInput :: s Int (Spec s i o) [i] [Int] -> [i]\r
+genLongInput s 0 spec inputs [r:x] = randomize inputs x 7 (\_.[])\r
+genLongInput s n spec inputs [r,r2:x]\r
+ = case [ i \\ i <- inputs | not (isEmpty (spec s i)) ] of\r
+ [] = []\r
+ l # i = l !! ((abs r) rem (length l))\r
+ = case spec s i of\r
+ [] = abort "\n\nError in genLongInput, please report.\n\n"\r
+ list # len = length list\r
+ s = case list !! ((abs r2) rem len) of\r
+ Pt o s = s\r
+ Ft f = abort "genLongInput Ft f"\r
+ = [ i : genLongInput s (n-1) spec inputs x ] \r
+\r
+genLongInputs :: s (Spec s i o) [i] Int [Int] -> [[i]]\r
+genLongInputs s spec inputs n [r:x] = [genLongInput s n spec inputs (genRandInt r): genLongInputs s spec inputs n x]\r
+\r
+testConfSM :: [TestOption s i o] (Spec s i o) s (IUTstep .t i o) .t (.t->.t) *File *File -> (.t,*File,*File)\r
+ | ggen{|*|} i & gEq{|*|} s & gEq{|*|} o & genShow{|*|} s & genShow{|*|} i & genShow{|*|} o\r
+testConfSM opts spec s0 iut t reset console file\r
+ # ts=:{fileName} = initState file console\r
+ # (t,ts) = doTest ts iut t reset\r
+ {mesFile,errFile} = ts\r
+ = (t, mesFile, errFile)\r
+where\r
+ initState file console\r
+ = handleOptions opts\r
+ { spec = spec\r
+ // , specW = \s i.[]\r
+ , iniState= s0\r
+ , curState= [s0]\r
+ , nRej = 0\r
+ , nTrun = 0\r
+ , nPath = 0\r
+ , nStep = 0\r
+ , nTotal = 0\r
+ , maxPath = 100\r
+ , maxLen = 1000\r
+ , nOnPath = 50\r
+ , inputs = (\rnd s -> ggen {|*|} 2 rnd)\r
+ , input = onTheFly \r
+ , n = 0\r
+ , h_in = []\r
+ , h_out = []\r
+ , h_state = []\r
+ , rnd = aStream\r
+ , errFile = file\r
+ , fileName= outputFile\r
+ , mesFile = console <<< "Gast starts testing.\n"\r
+ , trace = False\r
+ , incons = \o ss -> Nothing\r
+ , stop = (\states = False)\r
+ }\r
+\r
+findFileName [] name = name\r
+findFileName [ErrorFile s:r] name = findFileName r s\r
+findFileName [_:r] name = findFileName r name\r
+\r
+doTest :: (TestState s i o) (IUTstep .t i o) .t (.t->.t) -> (.t,TestState s i o)\r
+ | gEq{|*|} s & gEq{|*|} o & genShow{|*|} s & genShow{|*|} i & genShow{|*|} o\r
+doTest ts=:{input,curState,spec,incons} step t reset\r
+ | isEmpty ts.curState\r
+ = (t, errorFound ts)\r
+ | ts.nStep >= ts.maxLen || ts.nRej >= ts.maxLen\r
+ = doTest (resetState ts) step (reset t) reset\r
+ | ts.nPath >= ts.maxPath\r
+ | ts.nRej == 0 && ts.nTrun == 0\r
+ = (t,{ts & mesFile = ts.mesFile <<< "\nEnd of testing, maximum paths used. \n"\r
+ <<< ts.nPath\r
+ <<< " test paths executed successful, in total "\r
+ <<< ts.nTotal <<< " transitions.\n"})\r
+ = (t,{ts & mesFile = ts.mesFile <<< "\nEnd of testing, maximum paths used. \n"\r
+ <<< ts.nPath\r
+ <<< " test paths executed successful, "\r
+ <<< ts.nTrun <<< " paths truncated, "\r
+ <<< " in total "\r
+ <<< ts.nTotal <<< " transitions.\n"})\r
+ # (inp,ts) = input ts\r
+ = case inp of\r
+ Reset = doTest (resetState ts) step (reset t) reset\r
+ End | ts.nRej == 0 && ts.nTrun == 0\r
+ = (t,{ts & mesFile = ts.mesFile <<< "\nAll input paths tested successfully.\n"\r
+ <<< "All " <<< ts.nPath\r
+ <<< " executed test paths successful (Proof), in total "\r
+ <<< ts.nTotal <<< " transitions.\n"})\r
+ = (t,{ts & mesFile = ts.mesFile <<< "\nAll inputs tested successfully.\n"\r
+ <<< (ts.nPath-ts.nRej)\r
+ <<< "test path executed successful (Proof), " <<< ts.nRej\r
+ <<< " paths rejected " <<< ts.nTrun\r
+ <<< " paths truncated, "\r
+ <<< "in total " <<< ts.nTotal <<< " transitions.\n"})\r
+ NewInput i // assumption: only inputs allowed by spec will be generated:\r
+ #! (iut_o,t) = step t i\r
+ tuples = [tup \\ s<-curState, tup<-spec s i]\r
+ states = mkset (newStates tuples iut_o)\r
+ | isEmpty states\r
+ #! errFile = ts.errFile <<< "Issue found! Trace:\n"\r
+ <<< "SpecificationStates Input -> ObservedOutput\n"\r
+ errFile = showError (ts.nStep+1) [curState:ts.h_state] [i:ts.h_in] [iut_o:ts.h_out] errFile\r
+ errFile = errorInfo ts.nPath ts.nRej ts.nTrun (ts.nTotal+1) (errFile <<< "\n")\r
+ mesFile = errorInfo ts.nPath ts.nRej ts.nTrun (ts.nTotal+1) ts.mesFile\r
+ mesFile = mesFile <<< "See file \"" <<< ts.fileName <<< "\" for details about the issue.\n"\r
+ = (t,{ts & mesFile = mesFile\r
+ , errFile = errFile\r
+ , curState = []\r
+ })\r
+ = case incons iut_o states of\r
+ Nothing\r
+ # mesFile = ts.mesFile <<< "paths: " <<< ts.nPath <<< ", rejected: " <<< ts.nRej <<< ", truncated: " <<< ts.nTrun <<< "...\r"\r
+ = doTest {ts & curState = states\r
+ , nStep = ts.nStep+1\r
+ , nTotal =ts.nTotal+1\r
+ , h_in = [i:ts.h_in]\r
+ , h_out = [iut_o:ts.h_out]\r
+ , h_state = [curState:ts.h_state]\r
+ , mesFile = if ts.trace (mesFile <<< ts.nPath <<< "," <<< ts.nStep <<< ": " <<< show1 ts.curState <<< " " <<< show1 i <<< " " <<< show1 iut_o <<< "\n") mesFile\r
+ }\r
+ step t reset\r
+ Just errors \r
+ #! errFile = ts.errFile <<< "Inconsistency! Trace:\n"\r
+ <<< "SpecificationStates Input -> ObservedOutput\n"\r
+ errFile = showError (ts.nStep+1) [curState:ts.h_state] [i:ts.h_in] [iut_o:ts.h_out] errFile\r
+ errFile = errFile <<< "Inconsistency info:\n" <<< errors <<< "\n"\r
+ errFile = errorInfo ts.nPath ts.nRej ts.nTrun (ts.nTotal+1) (errFile <<< "\n")\r
+ mesFile = ts.mesFile <<< "Inconsistency found!\n" <<< errors <<< "\n\n"\r
+ mesFile = errorInfo ts.nPath ts.nRej ts.nTrun (ts.nTotal+1) mesFile\r
+ mesFile = mesFile <<< "See file \"" <<< ts.fileName <<< "\" for details.\n"\r
+ = (t,{ts & mesFile = mesFile\r
+ , errFile = errFile\r
+ , curState = []\r
+ })\r
+where\r
+ errorInfo :: !Int !Int !Int !Int *File -> *File\r
+ errorInfo nPath nRej nTrun nTotal file\r
+ = file <<< "Issue found in path " <<< (nPath+1) <<< ", "\r
+ <<< (nPath-nRej) <<< " paths executed, "\r
+ <<< nTrun <<< " tests truncated, in total "\r
+ <<< nTotal <<< " transitions.\n"\r
+\r
+outputFile = "testOut.txt"\r
+\r
+newStates [] iut_o = []\r
+newStates [Pt o s:r] iut_o\r
+ | o === iut_o\r
+ = [s:newStates r iut_o]\r
+ = newStates r iut_o\r
+newStates [Ft f:r] iut_o = f iut_o ++ newStates r iut_o\r
+\r
+resetState ts\r
+ = {ts & curState = [ts.iniState]\r
+ , nPath = ts.nPath+1\r
+ , nStep = 0\r
+ , h_in = []\r
+ , h_out = []\r
+ , h_state = []\r
+ , mesFile = if ts.trace (ts.mesFile <<< "End of path reached: reset.\n") ts.mesFile\r
+ }\r
+\r
+errorFound ts=:{errFile,mesFile}\r
+ # errFile = errFile <<< "Issue Found!\n"\r
+ # mesFile = mesFile <<< "Issue Found!\n"\r
+ = {ts & errFile = errFile,mesFile=mesFile}\r
+\r
+restart testState = { testState & h_in = [], h_out = [], h_state = [] }\r
+ /*\r
+testConfSM :: [TestOption s i o] (Spec s i o) s (IUTstep .t i o) .t (.t->.t) *d -> (.t,*d)\r
+ | FileSystem d & ggen{|*|} i & gEq{|*|} s & gEq{|*|} o & genShow{|*|} s & genShow{|*|} i & genShow{|*|} o\r
+testConfSM opts spec s0 iut t reset world\r
+ # (console,world) = stdio world\r
+ filename = findFileName opts outputFile\r
+ # (ok,file,world) = fopen filename FWriteText world\r
+ | not ok\r
+ # console = console <<< "Cannot open output file "<<< filename\r
+ = (t, snd (fclose console world))\r
+ # //console = console <<< ".\n"\r
+ ts=:{fileName} = initState file console\r
+ # (t,ts) = doTest ts iut t reset\r
+ {mesFile,errFile} = ts\r
+ = (t, snd (fclose mesFile (snd (fclose errFile world))))\r
+where\r
+ initState file console\r
+ = handleOptions opts\r
+ { spec = spec\r
+ , iniState= s0\r
+ , curState= [s0]\r
+ , nRej = 0\r
+ , nTrun = 0\r
+ , nPath = 0\r
+ , nStep = 0\r
+ , nTotal = 0\r
+ , maxPath = 100\r
+ , maxLen = 1000\r
+ , nOnPath = 50\r
+ , inputs = (\rnd s -> ggen {|*|} 2 rnd)\r
+ , input = onTheFly \r
+ , n = 0\r
+ , h_in = []\r
+ , h_out = []\r
+ , h_state = []\r
+ , rnd = aStream\r
+ , errFile = file\r
+ , fileName= outputFile\r
+ , mesFile = console <<< "Gast starts testing.\n"\r
+ , trace = False\r
+ , incons = \o ss -> Nothing\r
+ , stop = (\states = False)\r
+ }\r
+\r
+findFileName [] name = name\r
+findFileName [ErrorFile s:r] name = findFileName r s\r
+findFileName [_:r] name = findFileName r name\r
+\r
+doTest :: (TestState s i o) (IUTstep .t i o) .t (.t->.t) -> (.t,TestState s i o)\r
+ | gEq{|*|} s & gEq{|*|} o & genShow{|*|} s & genShow{|*|} i & genShow{|*|} o\r
+doTest ts=:{input,curState,spec,stop} step t reset\r
+ | isEmpty ts.curState\r
+ = (t, errorFound ts)\r
+ | ts.nStep >= ts.maxLen || ts.nRej >= ts.maxLen || stop curState\r
+ = doTest (resetState ts) step (reset t) reset\r
+ | ts.nPath >= ts.maxPath\r
+ | ts.nRej == 0 && ts.nTrun == 0\r
+ = (t,{ts & mesFile = ts.mesFile <<< "\nEnd of testing, maximum paths used. \n"\r
+ <<< ts.nPath\r
+ <<< " test paths executed successful, in total "\r
+ <<< ts.nTotal <<< " transitions.\n"})\r
+ = (t,{ts & mesFile = ts.mesFile <<< "\nEnd of testing, maximum paths used. \n"\r
+ <<< ts.nPath\r
+ <<< " test paths executed successful, "\r
+ <<< ts.nTrun <<< " paths truncated, "\r
+ <<< " in total "\r
+ <<< ts.nTotal <<< " transitions.\n"})\r
+ # (inp,ts) = input ts\r
+ = case inp of\r
+ Reset = doTest (resetState ts) step (reset t) reset\r
+ End | ts.nRej == 0 && ts.nTrun == 0\r
+ = (t,{ts & mesFile = ts.mesFile <<< "\nAll input paths tested successfully.\n"\r
+ <<< "All " <<< ts.nPath\r
+ <<< " executed test paths successful (Proof), in total "\r
+ <<< ts.nTotal <<< " transitions.\n"})\r
+ = (t,{ts & mesFile = ts.mesFile <<< "\nAll inputs tested successfully.\n"\r
+ <<< (ts.nPath-ts.nRej)\r
+ <<< "test path executed successful (Proof), " <<< ts.nRej\r
+ <<< " paths rejected " <<< ts.nTrun\r
+ <<< " paths truncated, "\r
+ <<< "in total " <<< ts.nTotal <<< " transitions.\n"})\r
+// Input i // assumption: only inputs allowed by spec will be generated:\r
+ NewInput i // assumption: only inputs allowed by spec will be generated:\r
+ #! (iut_o,t) = step t i\r
+ tuples = [tup \\ s<-curState, tup<-spec s i]\r
+ = case mkset (newStates tuples iut_o) of\r
+ [] #! errFile = ts.errFile <<< "Issue found! Trace:\n"\r
+ <<< "SpecificationStates Input -> ObservedOutput\n"\r
+ errFile = showError (ts.nStep+1) [curState:ts.h_state] [i:ts.h_in] [iut_o:ts.h_out] errFile\r
+ errFile = errFile <<< "\nAllowed outputs and target states: " <<< show tuples <<< "\n"\r
+ errFile = errorInfo ts.nPath ts.nRej ts.nTrun (ts.nTotal+1) (errFile <<< "\n")\r
+ mesFile = errorInfo ts.nPath ts.nRej ts.nTrun (ts.nTotal+1) ts.mesFile\r
+ mesFile = mesFile <<< "See file \"" <<< ts.fileName <<< "\" for details about the issue.\n"\r
+\r
+ = (t,{ts & mesFile = mesFile\r
+ , errFile = errFile\r
+ , curState = []\r
+ })\r
+ states #! mesFile = ts.mesFile <<< "paths: " <<< ts.nPath <<< ", rejected: " <<< ts.nRej <<< ", truncated: " <<< ts.nTrun <<< "...\r"\r
+ = doTest {ts & curState = states\r
+ , nStep = ts.nStep+1\r
+ , nTotal =ts.nTotal+1\r
+ , h_in = [i:ts.h_in]\r
+ , h_out = [iut_o:ts.h_out]\r
+ , h_state = [curState:ts.h_state]\r
+ , mesFile = if ts.trace (mesFile <<< ts.nPath <<< "," <<< ts.nStep <<< ": " <<< show1 ts.curState <<< " " <<< show1 i <<< " " <<< show1 iut_o <<< "\n") mesFile\r
+ }\r
+ step t reset\r
+ where\r
+ errorInfo :: !Int !Int !Int !Int *File -> *File\r
+ errorInfo nPath nRej nTrun nTotal file\r
+ = file <<< "Issue found in path " <<< (nPath+1) <<< ", "\r
+ <<< (nPath-nRej) <<< " paths executed to bound or end, "\r
+ <<< nTrun <<< " paths truncated, in total "\r
+ <<< nTotal <<< " transitions.\n"\r
+\r
+ // = (t,{ts & mesFile = ts.mesFile <<< "\nAll inputs tested successfully\n"})\r
+\r
+outputFile = "testOut.txt"\r
+\r
+newStates [] iut_o = []\r
+newStates [Pt o s:r] iut_o\r
+ | o === iut_o\r
+ = [s:newStates r iut_o]\r
+ = newStates r iut_o\r
+newStates [Ft f:r] iut_o = f iut_o ++ newStates r iut_o\r
+\r
+resetState ts\r
+ = {ts & curState = [ts.iniState]\r
+ , nPath = ts.nPath+1\r
+ , nStep = 0\r
+ , h_in = []\r
+ , h_out = []\r
+ , h_state = []\r
+ , mesFile = if ts.trace (ts.mesFile <<< "End of path reached: reset.\n") ts.mesFile\r
+ }\r
+\r
+errorFound ts=:{errFile,mesFile}\r
+ # errFile = errFile <<< "Issue Found!\n"\r
+ # mesFile = mesFile <<< "Issue Found!\n"\r
+ = {ts & errFile = errFile,mesFile=mesFile}\r
+\r
+restart testState = { testState & h_in = [], h_out = [], h_state = [] }\r
+*/\r
+handleOptions [] ts = ts\r
+handleOptions [o:r] ts=:{mesFile}\r
+ # ts = case o of\r
+ Ntests n = {ts & maxLen = n}\r
+ Nsequences n = {ts & maxPath = n}\r
+ Seed n = {ts & rnd = genRandInt n}\r
+ Randoms rnd = {ts & rnd = rnd }\r
+ FixedInputs ll_input = {ts & input = fixedInputs ll_input }\r
+ InputFun f = {ts & inputs = f }\r
+ // OutputFun f = {test & } //([s] i -> o)\r
+ FSM inp identify = {ts & input = fixedInputs (generateFSMpaths ts.iniState ts.spec inp identify) }\r
+ MkTrace b = { ts & trace = b }\r
+ OnPath n = { ts & nOnPath = n }\r
+ OnAndOffPath = { ts & input = onAndOff }\r
+ SwitchSpec spec = { ts & input = switchSpec spec }\r
+ OnTheFly = { ts & input = onTheFly }\r
+ ErrorFile f = { ts & fileName = f }\r
+ Stop pred = { ts & stop = pred }\r
+ = handleOptions r ts\r
+\r
+showError :: Int [a] [b] [c] !*File -> *File | genShow{|*|} a & genShow{|*|} b & genShow{|*|} c\r
+showError n [a:x] [b:y] [c:z] file = showError (n-1) x y z file <<< " " <<< n <<< ": " <<< show a <<< " " <<< show1 b <<< " -> " <<< show c <<< "\n"\r
+showError _ [] [] [] file = file\r
+showError _ _ _ _ file = file <<< "\n\n\tInternal error in \"showError\", please report to pieter@cs.ru.nl!\n\n"\r
+\r
+/*\r
+testConf :: Int (Spec s i o) (Spec t i o) s t ([s] -> Bool) [[i]] *d -> *d \r
+ | FileSystem d & gEq{|*|} s & gEq{|*|} o & genShow{|*|} s & genShow{|*|} t & genShow{|*|} i & genShow{|*|} o //& <<< o\r
+testConf max spec imp state stateIUT stop paths world\r
+ # (console,world) = stdio world\r
+ # (ok,file,world) = fopen outputFile FWriteText world\r
+ | not ok\r
+ = abort ("Cannot open output file "+++outputFile)\r
+ # (file,console) = test 0 0 0 1 paths file console\r
+ = snd (fclose console (snd (fclose file world)))\r
+where\r
+ outputFile = "testOut.txt"\r
+ test s t r n [] file console\r
+ = (file\r
+ ,console <<< "All (" <<< (n-r-1) <<< ") executed test paths successful (Proof), " <<< ", rejected " <<< r\r
+ <<< ", tests truncated " <<< t <<< ", in total " <<< s <<< " transitions.\n"\r
+ )\r
+ test s t r n l file console\r
+ | n > max\r
+ = (file\r
+ ,console <<< max <<< " test paths used, testing terminated, " <<< r <<< " rejected, " <<< t <<< " tests truncated, in total "\r
+ <<< (n-r-1) <<< " paths executed, " <<< s <<< " transitions.\n"\r
+ )\r
+ test s t r n [path:paths] file console\r
+ // | cbc spec [state] path\r
+ #!console = if ((n - r) bitand /*1023*/ /*31*/ 7 == 0)\r
+ (console <<< "paths: " <<< (n-1) <<< ", rejected: " <<< r <<< " paths executed: " <<< (n-r-1) <<< ", truncated: " <<< t <<< "...\r")\r
+ console\r
+ # iut = IUT imp stateIUT (genRandInt 195773)\r
+ #! (ok, skipped, steps, file) = conf 0 [state] iut path [] [] [] [] file\r
+ #! file = file\r
+ s = s+steps\r
+ | ok\r
+ | skipped = test s (t + 1) r (n + 1) paths file console\r
+ = test s t r (n + 1) paths file console\r
+ # console = console <<< "Issue found after " <<< n <<< " paths, " <<< (n-r) <<< " paths executed, " <<< t <<< " tests truncated, in total " <<< s <<< " transitions.\n" <<< "See \"" <<< outputFile <<< "\" for details about the issue.\n"\r
+ = (file,console)\r
+ // = test s t (r+1) (n+1) paths file\r
+ \r
+ conf s [] iut path out this sts ex file\r
+ #! file = file <<< "ERROR: output to last input was wrong!\n"\r
+ <<< "Expected outputs: " <<< show1 ex <<< "\n"\r
+ file = showError (length this) this out sts file\r
+ = (False, False, s, file)\r
+ conf s states iut path out this sts ex file\r
+ | stop states\r
+ = (True, True, s, file)\r
+ conf s states iut [] out this sts ex file = (True, False, s, file)\r
+ conf s states iut [i:path] out this sts ex file\r
+ # (iutout,iut) = apply i iut\r
+ specifiedResp = [ tup \\ s1 <- states, tup <- spec s1 i ]\r
+ = case specifiedResp of\r
+ [] = (True, True, s, file)\r
+ _ # states2 = mkset [ s2 \\ (s2,specout) <- specifiedResp | specout === iutout ]\r
+ = conf (s+1) states2 iut path [iutout:out] [i:this] [states:sts] (map snd specifiedResp) file\r
+\r
+ showError :: Int [a] [b] [s] !*File -> *File | genShow{|*|} a & genShow{|*|} b & genShow{|*|} s\r
+ showError n [a:x] [b:y] [s:z] file = showError (n-1) x y z file <<< " " <<< n <<< ": " <<< show s <<< " " <<< show1 a <<< " -> " <<< show b <<< "\n"\r
+ showError _ [] [] [] file = file\r
+ showError _ _ _ _ file = file <<< "\n\n\tInternal error in \"showError\", please report!\n\n"\r
+*/\r
+mkset [a:xs] = [a:[x\\x<-xs|not (x===a)]]\r
+mkset [] = []\r
+\r
+instance <<< [a] | <<< a\r
+where\r
+ (<<<) file [] = file\r
+ (<<<) file [a:x] = file <<< a <<< x\r
+\r
+derive genShow Trans\r
+\r
+// ----------------------------------------------\r
+\r
+:: Transition state input output :== (state,input,[output],state)\r
+\r
+:: LTS state input output // Labelled Transition System\r
+ = { trans :: [Transition state input output]\r
+ , initial :: state\r
+ // set of states and labels are not needed, this is determined by the type state.\r
+ }\r
+\r
+generateLTS :: (Spec s i o) s (s->[i]) -> LTS s i o | gEq{|*|} s\r
+generateLTS spec s i = generateLTSpred (\_=True) spec s i\r
+\r
+generateLTSpred :: (s->Bool) (Spec s i o) s (s->[i]) -> LTS s i o | gEq{|*|} s\r
+generateLTSpred p spec s inputs\r
+ = { trans = generateTrans [] [s] spec inputs\r
+ , initial = s\r
+ }\r
+where\r
+// generateTrans :: [s] [s] (Spec s i o) (s->[i]) -> [(s,i,[o],s)] | gEq{|*|} s\r
+ generateTrans seen [] spec inputs = []\r
+ generateTrans seen [s:todo] spec inputs\r
+ | not (isEmpty [f \\ i <- inputs s, Ft f <- spec s i ])\r
+ = abort "Cannot handle (Ft f) transitions in FSM"\r
+ # trans = [ (s,i,o,t) \\ i <- inputs s, Pt o t <- spec s i ]\r
+ seen = [ s:seen ]\r
+ new = [ t \\ (_,_,_,t) <- trans | isNew seen t && p t ]\r
+ = trans ++ generateTrans seen (removeDup (todo++new)) spec inputs\r
+// isNew :: [s] s -> Bool | gEq{|*|} s\r
+ isNew [] t = True\r
+ isNew [s:seen] t\r
+ | s===t\r
+ = False\r
+ = isNew seen t\r
+// removeDup :: !.[a] -> .[a] | gEq{|*|} a\r
+ removeDup [x:xs] = [x:removeDup (filter ((=!=) x) xs)]\r
+ removeDup _ = []\r
+\r
+A4 :: (LTS state input output) (state -> [input]) -> [[input]] | gEq{|*|} state\r
+A4 lts stateIdent = gen [([],lts.initial)] lts.trans []\r
+where\r
+ gen _ [] _ = []\r
+ gen [(input,state):tups] trans next\r
+ = step input trans state [] tups next False False\r
+ gen [] t [] = []\r
+ gen [] t l = gen (reverse l) t []\r
+ \r
+ step input [trans=:(s1, toki, toko,s2):r] state seentrans tups next ever now\r
+ | s1 === state\r
+ = step [toki:input] (revApp seentrans r) s2 [] tups [(input,state):next] True True\r
+ = step input r state [trans:seentrans] tups next ever now\r
+ step input [] state seentrans tups next ever now \r
+ | now = step input seentrans state [] tups next True False // input is extended\r
+ | ever = [revApp input (stateIdent state): gen tups seentrans next]\r
+ = gen tups seentrans next\r
+ \r
+ revApp [] acc = acc\r
+ revApp [a:x] acc = revApp x [a:acc]\r
+\r
+generateFSMpaths :: s (Spec s i o) [i] (s->[i]) -> [[i]] | gEq{|*|} s\r
+generateFSMpaths start spec inputs identify = A4 (generateLTS spec start (\_=inputs)) identify\r
+\r
+//----------------- the after operator from ioco theory -----------------//\r
+//----------------- yields the possible states after an input sequence --//\r
+\r
+(after) infix 0 :: [s] (Spec s i o) -> ([i] -> [s])\r
+(after) s spec // = apply s\r
+ = \i = case i of\r
+ [] = s\r
+ [i:r]\r
+ | not (isEmpty [f \\ u<-s, Ft f <- spec u i ])\r
+ = abort "Cannot handle (Ft f) transitions in (after)"\r
+ = ([t \\ u<-s, Pt o t <- spec u i] after spec) r\r
+/*where\r
+ apply [] i = []\r
+ apply s [] = s\r
+ apply s [i:r] = apply [t \\ u<-s, (t,o) <- spec u i] r\r
+*/\r
+//----------------- properties of specifications -----------------//\r
+\r
+propDeterministic :: (Spec s i o) s i -> Bool\r
+propDeterministic m s i = length (m s i) <= 1\r
+\r
+propTotal :: (Spec s i o) s i -> Bool\r
+propTotal m s i = not (isEmpty (m s i))\r
--- /dev/null
+definition module gast\r
+\r
+/*\r
+ GAST: A Generic Automatic Software Test-system\r
+\r
+ Pieter Koopman, 2004-2010\r
+ Radboud Universty, Nijmegen\r
+ The Netherlands\r
+ pieter@cs.ru.nl\r
+*/\r
+\r
+import MersenneTwister, gen, GenEq, genLibTest, testable, confSM, stdProperty
\ No newline at end of file
--- /dev/null
+implementation module gast\r
+\r
+/*\r
+ GAST: A Generic Automatic Software Test-system\r
+\r
+ Pieter Koopman, 2004-2010\r
+ Radboud Universty, Nijmegen\r
+ The Netherlands\r
+ pieter@cs.ru.nl\r
+*/\r
+
\ No newline at end of file
--- /dev/null
+definition module gen\r
+\r
+/*\r
+ GAST: A Generic Automatic Software Test-system\r
+ \r
+ gen: generic generation of values of a type\r
+\r
+ Pieter Koopman, 2004\r
+ Radboud Universty, Nijmegen\r
+ The Netherlands\r
+ pieter@cs.ru.nl\r
+*/\r
+\r
+import StdGeneric\r
+\r
+randomize :: [a] [Int] Int ([Int] -> [a]) -> [a]\r
+\r
+generic ggen a :: Int [Int] -> [a]\r
+\r
+derive ggen Int, Bool, Real, Char, UNIT, PAIR, EITHER, CONS, OBJECT, FIELD, (,), (,,), (,,,), [], String\r
+\r
+maxint :: Int\r
+minint :: Int\r
+StrLen :== 80\r
--- /dev/null
+implementation module gen\r
+\r
+/*\r
+ GAST: A Generic Automatic Software Test-system\r
+ \r
+ gen: generic generation of values of a type\r
+\r
+ Pieter Koopman, 2004\r
+ Radboud Universty, Nijmegen\r
+ The Netherlands\r
+ pieter@cs.ru.nl\r
+*/\r
+\r
+import StdEnv, StdGeneric, MersenneTwister\r
+\r
+// -------\r
+:: RandomStream :== [Int]\r
+\r
+aStream :: RandomStream\r
+aStream = genRandInt 42\r
+\r
+split :: RandomStream -> (RandomStream,RandomStream)\r
+split [r,s:rnd]\r
+ # seed = r*s\r
+ | seed==0\r
+ = split rnd\r
+ = (genRandInt seed, rnd)\r
+split _ = abort "gen.icl: the increadable has been done, you have used all random values!"\r
+// -------\r
+\r
+randomize :: [a] [Int] Int ([Int] -> [a]) -> [a]\r
+randomize list rnd n c = rand list rnd n []\r
+where\r
+ rand [] rnd m [] = c rnd\r
+ rand [] rnd m [x] = [x:c rnd]\r
+ rand [] rnd m l = rand l rnd n []\r
+ rand [a:x] [i:rnd] m l\r
+ | m==0 || (i rem m) == 0\r
+ = [a:rand x rnd (m-1) l]\r
+ = rand x rnd m [a:l]\r
+// -------\r
+\r
+generic ggen a :: Int [Int] -> [a]\r
+\r
+maxint :: Int\r
+maxint = 2147483647\r
+\r
+minint :: Int\r
+minint = -2147483648\r
+\r
+ggen{|Int|} n rnd = randomize [0,1,-1,maxint,minint] rnd 5 id\r
+ggen{|Bool|} n rnd = randomize [False,True] rnd 2 \_.[]\r
+ggen{|Char|} n rnd = randomize (map toChar [32..126] ++ ['\t\n\r']) rnd 98 (\_.[])\r
+ggen{|Real|} n rnd = randomize [0.0,1.0,-1.0] rnd 3 (\[s:x] -> f x (genRandReal s))\r
+where f [i,j:x] [r:s]\r
+ | r==0.0\r
+ = [r:f x s]\r
+ # r = if (isOdd i) r (~r)\r
+ r = if (isOdd j) r (1.0/r)\r
+ = [r:f x s]\r
+\r
+bias :== 1024\r
+\r
+ggen{|UNIT|} n rnd = [UNIT]\r
+ggen{|PAIR|} f g n rnd\r
+ # (rn2,rnd) = split rnd\r
+ = map (\(a,b)=PAIR a b) (diag2 (f n rnd) (g n rn2)) // inlinen !?\r
+ggen{|EITHER|} f g n rnd\r
+ # (r1,rnd) = split rnd\r
+ (r2,rnd) = split rnd\r
+ = Merge n rnd (f n r1) (g (n+1) r2)\r
+where\r
+ Merge :: Int RandomStream [a] [b] -> [EITHER a b] // Correct, strict in none of the lists!\r
+ Merge n [i:r] as bs\r
+ | (i rem n) <> 0\r
+// | (i rem bias) > n+(bias/2)\r
+ = case as of\r
+ [] = map RIGHT bs\r
+ [a:as] = [LEFT a: Merge n r as bs]\r
+ = case bs of\r
+ [] = map LEFT as\r
+ [b:bs] = [RIGHT b: Merge n r as bs]\r
+/* Merge :: RandomStream [a] [b] -> [EITHER a b] // Wrong, strict in both lists\r
+ Merge r [] bs = map RIGHT bs\r
+ Merge r as [] = map LEFT as\r
+ Merge [i:r] [a:as] [b:bs]\r
+ | isOdd i\r
+ = [LEFT a, RIGHT b:Merge r as bs]\r
+ = [RIGHT b, LEFT a:Merge r as bs]\r
+*//* = Merge (isOdd (hd rnd)) (f r1) (g r2)\r
+where\r
+ Merge :: Bool [a] [b] -> [EITHER a b]\r
+ Merge r as bs\r
+ | r\r
+ = case as of\r
+ [] = map RIGHT bs\r
+ [a:as] = [LEFT a: Merge (not r) as bs]\r
+ = case bs of\r
+ [] = map LEFT as\r
+ [b:bs] = [RIGHT b: Merge (not r) as bs]\r
+*/\r
+ggen{|CONS|} f n rnd = map CONS (f n rnd)\r
+ggen{|OBJECT|} f n rnd = map OBJECT (f n rnd)\r
+ggen{|FIELD|} f n rnd = map FIELD (f n rnd)\r
+ggen{|String|} n rnd = ["hello world!","Tested with GAST!": rndStrings 0 rnd]\r
+where\r
+ rndStrings 0 rnd = ["": rndStrings 1 rnd]\r
+ rndStrings len [r,s:rnd] \r
+ # (chars,rnd) = seqList (repeatn ((abs r) rem len) genElem) rnd\r
+ string = {c \\ c<-chars}\r
+ = [string:rndStrings ((len rem StrLen)+1) rnd]\r
+\r
+class genElem a where genElem :: RandomStream -> .(a,RandomStream)\r
+\r
+instance genElem Int where genElem [r:rnd] = (r,rnd)\r
+instance genElem Char where genElem [r:rnd] = (toChar (32+((abs r) rem 94)),rnd)\r
+instance genElem Bool where genElem [r:rnd] = (isOdd r,rnd)\r
+instance genElem Real where genElem [r,s,t:rnd] = ((toReal r/toReal s)*toReal t,rnd)\r
+\r
+derive ggen (,), (,,), (,,,), []\r
+derive bimap []\r
--- /dev/null
+definition module genLibTest\r
+\r
+/*\r
+ GAST: A Generic Automatic Software Test-system\r
+ \r
+ genLibtest: library for generic testing: showing and comparing values\r
+\r
+ Pieter Koopman, 2004\r
+ Radboud Universty, Nijmegen\r
+ The Netherlands\r
+ pieter@cs.ru.nl\r
+*/\r
+\r
+import StdGeneric, GenEq\r
+\r
+import StdClass\r
+instance + String\r
+\r
+(@) infixl 2 :: (a->b) a -> b\r
+(@!)infixl 2 :: (a->b) !a -> b\r
+\r
+generic genShow a :: String Bool a [String] -> [String]\r
+generic gLess a :: a a -> Bool\r
+\r
+derive genShow Int, Char, Bool, Real, String, UNIT, PAIR, EITHER, OBJECT, CONS, FIELD, [], (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,), (,,,,,,,,), (,,,,,,,,,), (->), {}, {!}\r
+derive gLess Int, Char, Bool, Real, String, UNIT, PAIR, EITHER, OBJECT, CONS, FIELD, [], (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,), (,,,,,,,,), (,,,,,,,,,) \r
+\r
+show :: !a -> [String] | genShow{|*|} a\r
+show1 :: !a -> String | genShow{|*|} a\r
+\r
+(-<-) infix 4 :: !a !a -> Bool | gLess{|*|} a\r
+(->-) infix 4 :: !a !a -> Bool | gLess{|*|} a\r
+(-<=) infix 4 :: !a !a -> Bool | gLess{|*|} a\r
+(=>-) infix 4 :: !a !a -> Bool | gLess{|*|} a\r
+\r
--- /dev/null
+implementation module genLibTest\r
+\r
+/*\r
+ GAST: A Generic Automatic Software Test-system\r
+ \r
+ genLibtest: library for generic testing: showing and comparing values\r
+\r
+ Pieter Koopman, 2004\r
+ Radboud Universty, Nijmegen\r
+ The Netherlands\r
+ pieter@cs.ru.nl\r
+*/\r
+\r
+import StdEnv, StdGeneric, GenEq\r
+\r
+instance + String where (+) s t = s +++ t\r
+\r
+(@)infixl 2 :: (a->b) a -> b\r
+(@) f x = f x\r
+\r
+(@!)infixl 2 :: (a->b) !a -> b\r
+(@!) f x = f x\r
+\r
+//--- show ---//\r
+generic genShow a :: String Bool a [String] -> [String]\r
+\r
+genShow{|Int|} sep p x rest = [toString x: rest]\r
+genShow{|Char|} sep p x rest = ["'",showChar x,"'": rest]\r
+genShow{|Bool|} sep p x rest = [toString x: rest]\r
+genShow{|Real|} sep p x rest = [toString x: rest]\r
+genShow{|String|} sep p s rest = ["\"",s,"\"":rest] \r
+genShow{|UNIT|} sep p _ rest = rest\r
+genShow{|PAIR|} fx fy sep p (PAIR x y) rest\r
+// | p\r
+// = ["(":fx sep p x [sep: fy sep p y [")":rest]]]\r
+ = fx sep p x [sep: fy sep p y rest]\r
+//genShow{|PAIR|} fx fy sep p (PAIR x y) rest = fx sep True x [sep: fy sep True y rest]\r
+genShow{|EITHER|} fl fr sep p (LEFT x) rest = fl sep p x rest\r
+genShow{|EITHER|} fl fr sep p (RIGHT x) rest = fr sep p x rest\r
+genShow{|OBJECT|} f sep p (OBJECT x) rest = f sep p x rest\r
+genShow{|(->)|} fa fr sep p f rest = ["<function>": rest]\r
+genShow{|{}|} fx sep p xs rest = ["{" :showList fx [x\\x<-:xs] ["}":rest]]\r
+genShow{|{!}|} fx sep p xs rest = ["{!":showList fx [x\\x<-:xs] ["}":rest]]\r
+//genShow{|{#}|} fx sep p xs rest = ["{#":showList fx [x\\x<-:xs] ["}":rest]]\r
+genShow{|[]|} f sep p xs rest = ["[" :showList f xs ["]":rest]]\r
+genShow{|(,)|} f1 f2 sep p (x1,x2) rest = ["(":f1 sep False x1 [",":f2 sep False x2 [")":rest]]]\r
+genShow{|(,,)|} f1 f2 f3 sep p (x1,x2,x3) rest = ["(":f1 sep False x1 [",":f2 sep False x2 [",":f3 sep False x3 [")":rest]]]]\r
+genShow{|(,,,)|} f1 f2 f3 f4 sep p (x1,x2,x3,x4) rest\r
+ = ["(":f1 sep False x1 [",":f2 sep False x2 [",":f3 sep False x3 [",":f4 sep False x4 [")":rest]]]]]\r
+genShow{|(,,,,)|} f1 f2 f3 f4 f5 sep p (x1,x2,x3,x4,x5) rest\r
+ = ["(":f1 sep False x1 [",":f2 sep False x2 [",":f3 sep False x3 [",":f4 sep False x4 [",":f5 sep False x5 [")":rest]]]]]]\r
+genShow{|(,,,,,)|} f1 f2 f3 f4 f5 f6 sep p (x1,x2,x3,x4,x5, x6) rest = ["(":f1 sep False x1 [",":f2 sep False x2 [",":f3 sep False x3 [",":f4 sep False x4 [",":f5 sep False x5 [",":f6 sep False x6 [")":rest]]]]]]]\r
+genShow{|(,,,,,,)|}f1 f2 f3 f4 f5 f6 f7 sep p (x1,x2,x3,x4,x5,x6,x7) rest\r
+ = ["(":f1 sep False x1 [",":f2 sep False x2 [",":f3 sep False x3 [",":f4 sep False x4 [",":f5 sep False x5 [",":f6 sep False x6 [",":f7 sep False x7 [")":rest]]]]]]]]\r
+genShow{|(,,,,,,,)|}f1 f2 f3 f4 f5 f6 f7 f8 sep p (x1,x2,x3,x4,x5,x6,x7,x8) rest\r
+ = ["(":f1 sep False x1 [",":f2 sep False x2 [",":f3 sep False x3 [",":f4 sep False x4 [",":f5 sep False x5 [",":f6 sep False x6 [",":f7 sep False x7 [",":f8 sep False x8 [")":rest]]]]]]]]]\r
+genShow{|(,,,,,,,,)|}f1 f2 f3 f4 f5 f6 f7 f8 f9 sep p (x1,x2,x3,x4,x5,x6,x7,x8,x9) rest\r
+ = ["(":f1 sep False x1 [",":f2 sep False x2 [",":f3 sep False x3 [",":f4 sep False x4 [",":f5 sep False x5 [",":f6 sep False x6 [",":f7 sep False x7 [",":f8 sep False x8 [",":f9 sep False x9 [")":rest]]]]]]]]]]\r
+genShow{|(,,,,,,,,,)|}f1 f2 f3 f4 f5 f6 f7 f8 f9 f0 sep p (x1,x2,x3,x4,x5,x6,x7,x8,x9,x0) rest\r
+ = ["(":f1 sep False x1 [",":f2 sep False x2 [",":f3 sep False x3 [",":f4 sep False x4 [",":f5 sep False x5 [",":f6 sep False x6 [",":f7 sep False x7 [",":f8 sep False x8 [",":f9 sep False x9 [",":f0 sep False x0 [")":rest]]]]]]]]]]]\r
+genShow{|CONS of {gcd_name, gcd_arity, gcd_fields}|} fx sep p (CONS x) rest\r
+ | gcd_arity == 0\r
+ = [gcd_name: rest]\r
+ | isEmpty gcd_fields // ordinary constructor\r
+ | p // parentheses needed\r
+// = ["(",gcd_name," ":fx " " False x [")":rest]]\r
+// = [gcd_name," ":fx " " False x rest]\r
+ = ["(",gcd_name," ":fx " " True x [")":rest]]\r
+ = [gcd_name," ":fx " " True x rest]\r
+ | otherwise // record\r
+ = ["{",{gcd_name.[i]\\i<-[1..size gcd_name-1]},"|":fx "," False x ["}":rest]]\r
+genShow{|FIELD of {gfd_name}|} fx sep p (FIELD x) rest\r
+ = [gfd_name,"=":fx sep False x rest]\r
+\r
+showChar :: Char -> String\r
+showChar c\r
+ = case c of\r
+ '\n' = "\\n"\r
+ '\t' = "\\t"\r
+ '\r' = "\\r"\r
+ '\b' = "\\b"\r
+ '\'' = "\\'"\r
+ c = toString c\r
+\r
+showList :: (.String -> .(.Bool -> .(.a -> .(u:[v:String] -> w:[x:String])))) ![.a] z:[u0:String] -> w0:[x0:String], [w0 <= u,x0 <= v,z w <= w0,u0 x <= x0]\r
+showList f [] rest = rest\r
+showList f [x] rest = f "" False x rest\r
+showList f [x:xs] rest = f "" False x [",":showList f xs rest]\r
+\r
+show :: !a -> [String] | genShow{|*|} a\r
+show x = genShow{|*|} "" False x []\r
+\r
+show1 :: !a -> String | genShow{|*|} a\r
+show1 x = glue (genShow{|*|} "" True x [])\r
+where\r
+ glue :: [String] -> String\r
+ glue [] = ""\r
+ glue [x:xs]\r
+ = case xs of\r
+ [] = x\r
+ = x+glue xs\r
+\r
+//--- comparision ---//\r
+/*\r
+instance < Bool\r
+where\r
+ (<) True b = not b\r
+ (<) False _ = False\r
+*/\r
+generic gLess a :: a a -> Bool\r
+\r
+gLess{|UNIT|} _ _ = False\r
+gLess{|PAIR|} fx fy (PAIR x1 y1) (PAIR x2 y2) = fx x1 x2 || (not (fx x2 x1) && fy y1 y2) // x1<x2 || (x1==x2) && y1<y2\r
+gLess{|EITHER|} fl fr (LEFT x) (LEFT y) = fl x y\r
+gLess{|EITHER|} fl fr (RIGHT x) (RIGHT y) = fr x y\r
+gLess{|EITHER|} fl fr (LEFT x) (RIGHT y) = True\r
+gLess{|EITHER|} fl fr (RIGHT x) (LEFT y) = False\r
+gLess{|CONS|} f (CONS x) (CONS y) = f x y\r
+gLess{|OBJECT|} f (OBJECT x) (OBJECT y) = f x y\r
+gLess{|FIELD|} f (FIELD x) (FIELD y) = f x y\r
+gLess{|Int|} x y = x < y\r
+gLess{|Char|} x y = x < y\r
+gLess{|Bool|} False y = y\r
+gLess{|Bool|} x y = False\r
+gLess{|Real|} x y = x < y\r
+gLess{|String|} x y = x < y\r
+\r
+derive gLess [], (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,), (,,,,,,,,), (,,,,,,,,,)\r
+\r
+(-<-) infix 4 :: !a !a -> Bool | gLess{|*|} a\r
+(-<-) x y = gLess{|*|} x y\r
+\r
+(->-) infix 4 :: !a !a -> Bool | gLess{|*|} a\r
+(->-) x y = gLess{|*|} y x\r
+\r
+(-<=) infix 4 :: !a !a -> Bool | gLess{|*|} a\r
+(-<=) x y = not (gLess{|*|} y x)\r
+\r
+(=>-) infix 4 :: !a !a -> Bool | gLess{|*|} a\r
+(=>-) x y = not (gLess{|*|} x y)\r
+\r
--- /dev/null
+% Configuration file for iDataGraphvizForm.\r
+% Comment lines start with % and run to the entire line or end of file.\r
+% Content should consist of name value pairs.\r
+% Syntactic restrictions:\r
+% name must not contain whitespace and do not start with %;\r
+% name and value are separated by a non-zero number of whitespace characters; \r
+% value is interpreted up until, but excluding next newline character;\r
+% values must terminate with a newline character.\r
+% current names:\r
+% DOT_PATH: the full path name to the dot.exe application of the graphviz package.\r
+%\r
+DOT_PATH C:\Program Files\ATT\Graphviz\bin\dot.exe\r
--- /dev/null
+definition module iDataGraphvizForm\r
+\r
+import StdiData\r
+import Graphviz\r
+\r
+derive gForm Digraph\r
+derive gUpd Digraph\r
+derive gPrint Digraph\r
+derive gParse Digraph\r
+derive gerda Digraph\r
+derive read Digraph\r
+derive write Digraph\r
+\r
--- /dev/null
+implementation module iDataGraphvizForm\r
+\r
+import StdEnv\r
+import StdiData, iDataHandler\r
+import Graphviz\r
+import launch\r
+import Directory\r
+\r
+derive gUpd [], Maybe, NodeState, //Digraph, \r
+ Arrow, ArrowShape, ArrowType, ClusterMode, Color, CompassPoint, DirType, DotPoint, \r
+ EdgeAttribute, EdgeStyle, GraphAttribute, LayerId, LayerList, LayerRange, Margin, \r
+ NodeAttribute, NodeDef, NodeShape, NodeStyle, OutputMode, Pad, PageDir, Pointf, \r
+ RankDir, RankType, Ratio, Rect, SelectedItem, Side, Sizef, StartStyle, StartType, ViewPort\r
+derive gPrint Maybe, Digraph, NodeState,\r
+ Arrow, ArrowShape, ArrowType, ClusterMode, Color, CompassPoint, DirType, DotPoint, \r
+ EdgeAttribute, EdgeStyle, GraphAttribute, LayerId, LayerList, LayerRange, Margin, \r
+ NodeAttribute, NodeDef, NodeShape, NodeStyle, OutputMode, Pad, PageDir, Pointf, \r
+ RankDir, RankType, Ratio, Rect, SelectedItem, Side, Sizef, StartStyle, StartType, ViewPort\r
+derive gParse Maybe, Digraph, NodeState,\r
+ Arrow, ArrowShape, ArrowType, ClusterMode, Color, CompassPoint, DirType, DotPoint, \r
+ EdgeAttribute, EdgeStyle, GraphAttribute, LayerId, LayerList, LayerRange, Margin, \r
+ NodeAttribute, NodeDef, NodeShape, NodeStyle, OutputMode, Pad, PageDir, Pointf, \r
+ RankDir, RankType, Ratio, Rect, SelectedItem, Side, Sizef, StartStyle, StartType, ViewPort\r
+derive gerda Digraph, NodeState, \r
+ Arrow, ArrowShape, ArrowType, ClusterMode, Color, CompassPoint, DirType, DotPoint, \r
+ EdgeAttribute, EdgeStyle, GraphAttribute, LayerId, LayerList, LayerRange, Margin, \r
+ NodeAttribute, NodeDef, NodeShape, NodeStyle, OutputMode, Pad, PageDir, Pointf, \r
+ RankDir, RankType, Ratio, Rect, SelectedItem, Side, Sizef, StartStyle, StartType, ViewPort\r
+derive read Maybe, Digraph, NodeState, \r
+ Arrow, ArrowShape, ArrowType, ClusterMode, Color, CompassPoint, DirType, DotPoint, \r
+ EdgeAttribute, EdgeStyle, GraphAttribute, LayerId, LayerList, LayerRange, Margin, \r
+ NodeAttribute, NodeDef, NodeShape, NodeStyle, OutputMode, Pad, PageDir, Pointf, \r
+ RankDir, RankType, Ratio, Rect, SelectedItem, Side, Sizef, StartStyle, StartType, ViewPort\r
+derive write Maybe, Digraph, NodeState, \r
+ Arrow, ArrowShape, ArrowType, ClusterMode, Color, CompassPoint, DirType, DotPoint, \r
+ EdgeAttribute, EdgeStyle, GraphAttribute, LayerId, LayerList, LayerRange, Margin, \r
+ NodeAttribute, NodeDef, NodeShape, NodeStyle, OutputMode, Pad, PageDir, Pointf, \r
+ RankDir, RankType, Ratio, Rect, SelectedItem, Side, Sizef, StartStyle, StartType, ViewPort\r
+\r
+// Specialization of iData for Digraph values:\r
+gUpd {|Digraph|} (UpdSearch (UpdC node) 0) (Digraph name graphAtts nodeDefs _)\r
+ = (UpdDone, Digraph name graphAtts nodeDefs nodeNr)\r
+where\r
+ nodeNr = case [nr \\ NodeDef nr _ nodeAtts _ <- nodeDefs | not (isEmpty (filter (isNAtt_label node) nodeAtts))] of\r
+ [nr:_] = Just (Node nr)\r
+ _ = Nothing\r
+ isNAtt_label l (NAtt_label l`)\r
+ = l==l`\r
+ isNAtt_label _ _ = False\r
+gUpd {|Digraph|} (UpdSearch other cnt) g\r
+ = (UpdSearch other (cnt-1),g)\r
+gUpd {|Digraph|} (UpdCreate l) _\r
+ = (UpdCreate l,Digraph "" [] [] Nothing)\r
+gUpd {|Digraph|} mode g = (mode,g)\r
+\r
+gForm {|Digraph|} (init,formid) hst\r
+ # (value,hst) = accWorldHSt (obtainValueFromConfig dot_exe_path_name) hst\r
+ | isNothing value = (result [ Txt ("Could not obtain "+++dot_exe_path_name+++" from "+++config_file_name+++".") ],hst)\r
+ # exe = fromJust value\r
+ # hst = appWorldHSt (ensureDirectory (target "")) hst // PA++\r
+ # (ok,hst) = accWorldHSt (writefile (target (dotext name)) (printDigraph (enhanceDigraphWithLinks digraph))) hst\r
+ | not ok = (result [ Txt ("Could not write Digraph to "+++target (dotext name)+++".") ],hst)\r
+ # ((ok,exit),hst) = accWorldHSt (collect3 (launch exe (toGIF (target name)))) hst\r
+ | not ok = (result [ Txt ("Creation of "+++gifext (target name)+++" failed. Exit code = "+++toString exit+++".") ],hst)\r
+ # ((ok,exit),hst) = accWorldHSt (collect3 (launch exe (toMAP (target name) name))) hst\r
+ | not ok = (result [ Txt ("Creation of "+++mapext (target name)+++" failed. Exit code = "+++toString exit+++".") ],hst)\r
+ # ((ok,lines),hst) = accWorldHSt (collect3 (readfile (mapext map_source_name))) hst\r
+ | not ok = (result [ Txt ("Reading of "+++mapext (target name)+++" failed.") ],hst)\r
+ # (cntr,hst) = CntrHSt hst\r
+ # lines = map (enhanceMAPlineWithOnClickEvent cntr) lines\r
+ | otherwise = (result [ \r
+ Img [ Img_Src (gifext img_source_name)\r
+ , Img_Usemap ("#"+++name)\r
+// , Img_Width (Percent 100)\r
+ , Img_Height (Percent 60)\r
+ ]\r
+ : map InlineCode lines\r
+ ],incrHSt 1 hst)\r
+where\r
+ digraph = formid.ival\r
+ name = formid.id\r
+ clean_name = clean_up name\r
+ result html = {changed=False,value=digraph,form=html}\r
+ img_source_name = ThisExe+++"/"+++name\r
+ map_source_name = ThisExe+++"/"+++name\r
+\r
+ \r
+ clean_up :: !String -> String\r
+// clean_up name = name\r
+ clean_up name = {clean_char c \\ c<-: name}\r
+ clean_char '.' = 'x'\r
+ clean_char '+' = 'p'\r
+ clean_char '-' = 'm'\r
+ clean_char c = c\r
+\r
+ enhanceMAPlineWithOnClickEvent :: !Int !String -> String\r
+ enhanceMAPlineWithOnClickEvent cntr line\r
+ | line%(0,5) == "<area "\r
+ | size line <= 6 || isNothing href_bounds //|| isNothing title_bounds\r
+ = line\r
+ | otherwise = line%(0,fst href-1) +++ \r
+ "onclick=\"toClean(this,'" +++ encodeTriplet(name,cntr,UpdC titletext) +++ "',true,false,false);\" " +++ \r
+ "id=\""+++ encodeInputId(name,cntr,UpdC titletext) +++ "\"" +++\r
+ line%(snd href+1,size line-1)\r
+ | line%(0,4) == "<map "\r
+ = "<map id=\"" +++ name +++ "\" name=\"" +++ name +++ "\">\n"\r
+ | otherwise\r
+ = line\r
+ where\r
+ href_bounds = boundsOfKeyValue "href=" line\r
+ title_bounds = boundsOfKeyValue "title=" line\r
+ href = fromJust href_bounds\r
+ title = fromJust title_bounds\r
+ titletext = line%(fst title+7,snd title-1)\r
+\r
+boundsOfKeyValue :: !String !String -> Maybe (!Int,!Int)\r
+boundsOfKeyValue key str\r
+ = case [i \\ i<-[0..size str-size key] | str%(i,i+size key-1) == key] of\r
+ [i : _] = case [j \\ j<-[i..size str-1] | str.[j]=='\"'] of\r
+ [_,close:_] = Just (i,close)\r
+ otherwise = Nothing\r
+ otherwise = Nothing\r
+\r
+enhanceDigraphWithLinks :: !Digraph -> Digraph\r
+enhanceDigraphWithLinks (Digraph name graphAtts nodeDefs selected)\r
+ = Digraph name graphAtts \r
+ [ NodeDef nr st [ NAtt_URL ("http://localhost/"+++ThisExe) : nodeAtts ] edges \r
+ \\ NodeDef nr st nodeAtts edges <- nodeDefs\r
+ ] selected\r
+\r
+obtainValueFromConfig :: !String !*env -> (!Maybe String,!*env) | FileSystem env\r
+obtainValueFromConfig name env\r
+ # (ok,file,env) = fopen config_file_name FReadText env\r
+ | not ok = (Nothing,env)\r
+ # (value,file) = obtainValueFromFile name file\r
+ # (ok,env) = fclose file env\r
+ | not ok = (Nothing,env)\r
+ | otherwise = (value, env)\r
+where\r
+ obtainValueFromFile :: !String !*File -> (!Maybe String,!*File)\r
+ obtainValueFromFile name file\r
+ # (lines,file) = readlines file\r
+ # value = case [ skipSpace (line%(name_length,size line-2)) \\ line<-lines\r
+ | line.[0] <> commentsymbol \r
+ && size line > name_length\r
+ && line%(0,name_length-1) == name\r
+ ] of [v:_] = Just v\r
+ _ = Nothing\r
+ = (value,file)\r
+ where\r
+ name_length = size name\r
+\r
+config_file_name :== "iDataGraphvizForm.config"\r
+commentsymbol :== '%'\r
+dot_exe_path_name :== "DOT_PATH"\r
+target file = MyAbsDir +++ ThisExe +++ "\\" +++ file\r
+toGIF file = "-Tgif -o " +++ "\"" +++ gifext file +++ "\" \"" +++ dotext file +++ "\""\r
+//toMAP file = "-Tcmapx -o " +++ "\"" +++ mapext file +++ "\" \"" +++ dotext file +++ "\""\r
+toMAP file name = "-Tcmapx" +++ " -Glabel=" +++ name +++ " -o " +++ "\"" +++ mapext file +++ "\" \"" +++ dotext file +++ "\""\r
+gifext file = file +++ ".gif"\r
+mapext file = file +++ ".map"\r
+dotext file = file +++ ".dot"\r
+\r
+// Utility functions:\r
+/* ensureDirectory path env\r
+ checks whether the directory at path exists. If so, no further actions are taken.\r
+ If not, the directory is created.\r
+*/\r
+import StdDebug\r
+\r
+ensureDirectory :: !String !*env -> *env | FileSystem env // PA++\r
+ensureDirectory pathname env\r
+ # ((ok,path), env) = pd_StringToPath pathname env\r
+ | not ok = env\r
+ # ((err,info),env) = getFileInfo path env\r
+ | err<>NoDirError = snd (createDirectory path env)\r
+ | otherwise = env\r
+\r
+writefile :: !String ![String] !*env -> (!Bool,!*env) | FileSystem env\r
+writefile fileName content env\r
+ # (ok,file,env) = fopen fileName FWriteText env\r
+ | not ok = (False,env)\r
+ # file = foldl (<<<) file content\r
+ = fclose file env\r
+\r
+readfile :: !String !*env -> (!Bool,![String],!*env) | FileSystem env\r
+readfile fileName env\r
+ # (ok,file,env) = fopen fileName FReadText env\r
+ | not ok = (False,[],env)\r
+ # (content,file) = readlines file\r
+ # (ok,env) = fclose file env\r
+ = (ok,content,env)\r
+\r
+readlines :: !*File -> (![String],!*File)\r
+readlines file\r
+ # (end,file) = fend file\r
+ | end = ([],file)\r
+ # (line, file) = freadline file\r
+ # (lines,file) = readlines file\r
+ = ([line:lines],file)\r
+\r
+collect3 :: (.s -> (.a,.b,.s)) .s -> (.(.a,.b),.s)\r
+collect3 f st\r
+ # (a,b,st) = f st\r
+ = ((a,b),st)\r
+\r
+skipSpace :: !String -> String\r
+skipSpace str = toString (dropWhile isSpace (fromString str))\r
--- /dev/null
+definition module launch\r
+\r
+:: PathAndApplication :== String\r
+:: CommandlineArgs :== String\r
+\r
+launch :: !PathAndApplication !CommandlineArgs !*World -> (!Bool,!Int,!*World)\r
--- /dev/null
+implementation module launch\r
+\r
+import StdEnv\r
+import /*StdIO,*/ostoolbox, clCCall_12\r
+\r
+//Start = launch (applicationpath "hello.exe") 42\r
+/*Start\r
+ # (ok1,exit1,tb) = launch exe (toGIF "test") 42\r
+ # (ok2,exit2,tb) = launch exe (toMAP "test") tb\r
+ = (ok1 && ok2, (exit1,exit2),tb)*/\r
+//Start = launch exe arg 42\r
+\r
+/*\r
+exe = "C:\\Program Files\\ATT\\Graphviz\\bin\\dot.exe"\r
+toGIF dot = "-Tgif -o " +++ dot +++ ".gif " +++ dot +++ ".dot"\r
+toMAP dot = "-Tcmapx -o " +++ dot +++ ".map " +++ dot +++ ".dot"\r
+\r
+exe = "D:\\Peter\\Projecten\\SpecificationVerification\\LaunchExternalApplication\\showCmndlineArgs.exe"\r
+arg = "one two three four"\r
+*/\r
+\r
+launch :: !PathAndApplication !CommandlineArgs !*World -> (!Bool,!Int,!*World)\r
+launch command cmndline world\r
+ # (tb,world) = worldGetToolbox world\r
+ # (commandptr,tb) = winMakeCString (command+++" "+++cmndline) tb\r
+ # (success,exitcode,tb) = winCallProcess commandptr 0 0 0 0 0 tb\r
+ # tb = winReleaseCString commandptr tb\r
+ # world = worldSetToolbox tb world\r
+ = (success,exitcode,world)\r
--- /dev/null
+definition module stdProperty\r
+\r
+/*\r
+ GAST: A Generic Automatic Software Test-system\r
+ \r
+ stdProperty: opertors on logical properties\r
+\r
+ Pieter Koopman, 2004\r
+ Radboud Universty, Nijmegen\r
+ The Netherlands\r
+ pieter@cs.ru.nl\r
+*/\r
+\r
+import genLibTest\r
+import testable\r
+\r
+class (\/) infixr 2 a b :: !a b -> Property // Conditional or of arg1 and arg2\r
+class (/\) infixr 3 a b :: !a b -> Property // Conditional and of arg1 and arg2\r
+\r
+instance /\ Bool Bool\r
+instance /\ Property Bool\r
+instance /\ Bool Property\r
+instance /\ Property Property\r
+\r
+instance \/ Bool Bool\r
+instance \/ Property Bool\r
+instance \/ Bool Property\r
+instance \/ Property Property\r
+\r
+class (==>) infixr 1 b :: b p -> Property | Testable p\r
+\r
+instance ==> Bool\r
+instance ==> Property\r
+\r
+(<==>) infix 4 :: !a !b -> Property | Testable a & Testable b // True if properties are equivalent\r
+\r
+ExistsIn :: (x->p) [x] -> Property | Testable p & TestArg x // type is too restricive\r
+Exists :: (x->p) -> Property | Testable p & TestArg x\r
+ForAll :: !(x->p) -> Property | Testable p & TestArg x\r
+\r
+ForEach :: ![x] !(x->p) -> Property | Testable p & TestArg x\r
+(For) infixl 0 :: !(x->p) ![x] -> Property | Testable p & TestArg x\r
+(ForAndGen) infixl 0 :: !(x->p) ![x] -> Property | Testable p & TestArg x\r
+\r
+classify :: !Bool l !p -> Property | Testable p & genShow{|*|} l\r
+label :: !l !p -> Property | Testable p & genShow{|*|} l\r
+name :: !n !p -> Property | Testable p & genShow{|*|} n\r
+\r
+instance ~ Bool\r
+instance ~ Property\r
--- /dev/null
+implementation module stdProperty\r
+\r
+/*\r
+ GAST: A Generic Automatic Software Test-system\r
+ \r
+ stdProperty: opertors on logical properties\r
+\r
+ Pieter Koopman, 2004..2008\r
+ Radboud Universty, Nijmegen\r
+ The Netherlands\r
+ pieter@cs.ru.nl\r
+*/\r
+\r
+import testable, StdEnv\r
+from MersenneTwister import genRandInt\r
+\r
+class (==>) infixr 1 b :: b p -> Property | Testable p\r
+\r
+instance ==> Bool\r
+where\r
+ (==>) c p\r
+ | c = Prop (evaluate p)\r
+ = Prop (\rs r = [{r & res = Rej}])\r
+\r
+instance ==> Property\r
+where\r
+ (==>) c p = Prop imp\r
+ where\r
+ imp rs r\r
+ # r1 = testAnalysis r (evaluate c rs r)\r
+ = case r1.res of\r
+ OK = evaluate p rs r1\r
+ = [{r & res = Rej}]\r
+\r
+class (\/) infixr 2 a b :: !a b -> Property // Conditional or of arg1 and arg2\r
+class (/\) infixr 3 a b :: !a b -> Property // Conditional and of arg1 and arg2\r
+\r
+instance /\ Bool Bool where (/\) x y = prop (x && y)\r
+instance /\ Property Bool where (/\) x y = x /\ prop y\r
+instance /\ Bool Property where (/\) x y = prop x /\ y\r
+instance /\ Property Property\r
+where (/\) x y = Prop (and x y)\r
+ where\r
+ and x y rs r \r
+ # (rs2,rs) = split rs\r
+ r1 = testAnalysis r (evaluate x rs r)\r
+ r2 = testAnalysis r (evaluate y rs2 r)\r
+ = case (r1.res,r2.res) of // collect labels !! \r
+ (CE ,_ ) = [r1] // to fix the evaluation order\r
+ (_ ,CE ) = [r2]\r
+ (Undef,_ ) = [r2]\r
+ (Rej ,OK ) = [r2]\r
+ = [r1]\r
+/*\r
+ (OK ,OK ) = [r1]\r
+ (OK ,Rej ) = [r1]\r
+ (OK ,Undef) = [r1]\r
+ (OK ,CE ) = [r2]\r
+ (Rej ,OK ) = [r2]\r
+ (Rej ,Rej ) = [r1]\r
+ (Rej ,Undef) = [r1]\r
+ (Pass ,CE ) = [r2]\r
+ (Pass ,OK ) = [r1]\r
+ (Pass ,Rej ) = [r1]\r
+ (Pass ,Undef) = [r1]\r
+ (Pass ,CE ) = [r2]\r
+ (Undef,OK ) = [r2]\r
+ (Undef,Rej ) = [r2]\r
+ (Undef,Undef) = [r2]\r
+ (Undef,CE ) = [r2]\r
+ (CE ,OK ) = [r1]\r
+ (CE ,Rej ) = [r1]\r
+ (CE ,Undef) = [r1]\r
+ (CE ,CE ) = [r1]\r
+*/\r
+instance \/ Bool Bool where (\/) x y = prop (x || y)\r
+instance \/ Property Bool where (\/) x y = x \/ prop y\r
+instance \/ Bool Property where (\/) x y = prop x \/ y\r
+instance \/ Property Property\r
+where (\/) x y = Prop (or x y)\r
+ where\r
+ or x y rs r \r
+ # (rs2,rs) = split rs\r
+ = case testAnalysis r (evaluate x rs r) of\r
+ r=:{res=OK} = [r]\r
+ r=:{res=Pass} = case testAnalysis r (evaluate y rs2 r) of\r
+ r2=:{res=OK} = [r2]\r
+ = [r]\r
+ = evaluate y rs2 r\r
+\r
+(<==>) infix 4 :: !a !b -> Property | Testable a & Testable b // True if properties are equivalent\r
+(<==>) p q \r
+ # rs = genRandInt 42\r
+ r = {res=Undef, labels=[], args=[], name=[]}\r
+ b = testAnalysis r (evaluate p rs r)\r
+ c = testAnalysis r (evaluate q rs r)\r
+ = prop (b.res == c.res) // can this be improved?\r
+\r
+(===>) infix 1 :: Bool Bool -> Bool\r
+(===>) p q = (not p) || q \r
+\r
+ExistsIn :: (x->p) [x] -> Property | Testable p & TestArg x\r
+ExistsIn f l = Prop p\r
+where p rs r = [exists r [testAnalysis r (evaluate (f a) rs r)\\a <- l] MaxExists]\r
+\r
+Exists :: (x->p) -> Property | Testable p & TestArg x\r
+Exists f = Prop p\r
+where p rs r\r
+ # (rs,rs2) = split rs\r
+ = [exists r [testAnalysis r (evaluate (f a) rs2 r)\\a <- generateAll rs] MaxExists]\r
+exists r [] n = {r & res = CE}\r
+exists r _ 0 = {r & res = Undef}\r
+exists _ [r=:{res}:x] n = case res of\r
+ OK = r\r
+ Pass = r\r
+ = exists r x (n-1)\r
+\r
+noCE r [] n = {r & res = OK}\r
+noCE r _ 0 = {r & res = Pass}\r
+noCE _ [r=:{res=CE}:x] n = r\r
+noCE _ [r=:{res=OK}:x] n = noCE {r&res=Pass} x (n-1)\r
+noCE r [_:x] n = noCE r x (n-1)\r
+\r
+testAnalysis :: Admin [Admin] -> Admin // maakt van een lijst resultaten een enkel resultaat\r
+testAnalysis r l = analysis l MaxExists Undef OK\r
+where\r
+ analysis [] n min max = {r & res = max}\r
+ analysis _ 0 min max = {r & res = min}\r
+ analysis [s:x] n min max\r
+ = case s.res of\r
+ CE = s\r
+ OK = analysis x (n-1) Pass max\r
+ Pass = analysis x (n-1) Pass Pass\r
+ Undef = analysis x (n-1) min max\r
+ Rej = case min of\r
+ OK = analysis x (n-1) OK max\r
+ Pass = analysis x (n-1) Pass max\r
+ = analysis x (n-1) Rej max\r
+ = abort "Unknow result in testAnalysis"\r
+\r
+ForAll :: !(x->p) -> Property | Testable p & TestArg x\r
+ForAll f = Prop (evaluate f)\r
+\r
+ForEach :: ![x] !(x->p) -> Property | Testable p & TestArg x\r
+ForEach list f = Prop (forAll f list)\r
+\r
+(For) infixl 0 :: !(x->p) ![x] -> Property | Testable p & TestArg x\r
+(For) p list = ForEach list p\r
+\r
+// XXXXXXXXXXXXXXXXXXXXXXXXXX\r
+\r
+class (VOOR) infixl 0 t :: (t a b) [a] -> [b]\r
+instance VOOR (->)\r
+where VOOR f l = map f l\r
+\r
+:: PL a b = PL [a->b]\r
+instance VOOR PL\r
+where VOOR (PL fl) l = diagonal [map f l\\f<-fl] //[f x \\ f<-fl, x<-l]\r
+\r
+//| Testable p & TestArg x\r
+\r
+// XXXXXXXXXXXXXXXXXXXXXXXXXX\r
+\r
+(ForAndGen) infixl 0 :: !(x->p) ![x] -> Property | Testable p & TestArg x\r
+(ForAndGen) p list = Prop (evaluate p)\r
+where evaluate f rs result\r
+ # (rs,rs2) = split rs\r
+ = forAll f (list++generateAll rs) rs2 result\r
+\r
+classify :: !Bool l !p -> Property | Testable p & genShow{|*|} l\r
+classify c l p\r
+ | c = Prop (\rs r = evaluate p rs {r & labels = [show1 l:r.labels]})\r
+ = Prop (evaluate p)\r
+\r
+label :: !l !p -> Property | Testable p & genShow{|*|} l\r
+label l p = Prop (\rs r = evaluate p rs {r & labels = [show1 l:r.labels]})\r
+\r
+name :: !n !p -> Property | Testable p & genShow{|*|} n\r
+name n p = Prop (\rs r = evaluate p rs {r & name = [show1 n:r.name]})\r
+\r
+instance ~ Bool where ~ b = not b\r
+\r
+instance ~ Result\r
+where\r
+ ~ CE = OK\r
+ ~ OK = CE\r
+ ~ Pass = CE\r
+ ~ Rej = Rej\r
+ ~ Undef = Undef\r
+\r
+instance ~ Property\r
+where ~ (Prop p) = Prop (\rs r = let r` = testAnalysis r (p rs r) in [{r` & res = ~r`.res}])\r
+\r
--- /dev/null
+definition module testOption\r
+\r
+/*\r
+ Pieter Koopman, 2010\r
+ Radboud Universty, Nijmegen\r
+ The Netherlands\r
+ pieter@cs.ru.nl\r
+*/\r
+\r
+import MersenneTwister, confSM, StdMaybe\r
+\r
+:: TestOption s i o\r
+ = Ntests Int\r
+ | Nsequences Int\r
+ | Seed Int\r
+ | Randoms [Int]\r
+ | FixedInputs [[i]]\r
+ | InputFun (RandomStream s -> [i])\r
+ | OnPath Int\r
+ | FSM [i] (s->[i]) // inputs state_identification\r
+ | MkTrace Bool\r
+ | OnTheFly\r
+ | SwitchSpec (Spec s i o)\r
+ | OnAndOffPath\r
+ | ErrorFile String\r
+ | Stop ([s] -> Bool)\r
+ | Inconsistent ([o] [s] -> Maybe [String])
\ No newline at end of file
--- /dev/null
+implementation module testOption\r
+\r
+/*\r
+ Pieter Koopman 2010\r
+ pieter@cs.ru.nl\r
+*/
\ No newline at end of file
--- /dev/null
+definition module testable\r
+\r
+/*\r
+ GAST: A Generic Automatic Software Test-system\r
+ \r
+ testable: the test algorithm for logical properties\r
+\r
+ Pieter Koopman, 2002-2010\r
+ Radboud Universty, Nijmegen\r
+ The Netherlands\r
+ pieter@cs.ru.nl\r
+*/\r
+\r
+import genLibTest\r
+from stdProperty import ::Property // for instance of testable\r
+import gen\r
+\r
+//--- basics --//\r
+\r
+:: Admin = {labels::![String], args::![String], name::![String], res::Result}\r
+:: Result = Undef | Rej | Pass | OK | CE\r
+:: RandomStream :== [Int]\r
+\r
+derive gLess Result\r
+instance == Result\r
+\r
+:: Property = Prop (RandomStream Admin -> [Admin])\r
+\r
+prop :: a -> Property | Testable a\r
+\r
+class TestArg a | genShow{|*|}, ggen{|*|} a\r
+class Testable a where evaluate :: a RandomStream !Admin -> [Admin]\r
+\r
+instance Testable Bool\r
+instance Testable Result\r
+instance Testable Property\r
+instance Testable (a->b) | Testable b & TestArg a \r
+instance Testable [a] | Testable a \r
+\r
+//derive bimap [], (,), (,,), (,,,), (,,,,), (,,,,,)\r
+\r
+MaxExists :== 1000\r
+NrOfTest :== 1000\r
+\r
+//--- for generating lists of elements ---//\r
+\r
+aStream :: RandomStream\r
+\r
+//--- for implementation of properties ---//\r
+\r
+diagonal :: [[a]] -> [a]\r
+forAll :: !(a->b) ![a] RandomStream !Admin -> [Admin] | Testable b & TestArg a\r
+split :: !RandomStream -> (RandomStream,RandomStream)\r
+generateAll :: !RandomStream -> [a] | ggen{|*|} a\r
+\r
+//--- testing --//\r
+\r
+:: Testoption\r
+ = Tests Int\r
+ | Fails Int\r
+ | Args Int\r
+ | RandomSeed Int\r
+ | RandomList [Int]\r
+ | Verbose\r
+ | Concise\r
+ | Quiet\r
+\r
+Test :: [Testoption] !p -> [String] | Testable p\r
+TestList :: [Testoption] ![p] -> [String] | Testable p\r
+\r
+verbose :: !RandomStream !p -> [String] | Testable p\r
+verbosen :: !Int !RandomStream !p -> [String] | Testable p\r
+concise :: !RandomStream !p -> [String] | Testable p\r
+concisen :: !Int !RandomStream !p -> [String] | Testable p\r
+quiet :: !RandomStream !p -> [String] | Testable p\r
+quietn :: !Int !RandomStream !p -> [String] | Testable p\r
+quietnm :: !Int !Int !RandomStream !p -> [String] | Testable p\r
+\r
+test :: !p -> [String] | Testable p // test p NrOfTest times\r
+testn :: !Int !p -> [String] | Testable p // maxnumber of tests\r
+ttestn :: !Int !p -> [String] | Testable p // maxnumber of tests, trace all arguments\r
+testnm :: !Int !Int !p -> [String] | Testable p // maxnumber of tests, max number of errors\r
+ttestnm :: !Int !Int !p -> [String] | Testable p // maxnumber of tests, max number of errors\r
--- /dev/null
+implementation module testable\r
+\r
+/*\r
+ GAST: A Generic Automatic Software Test-system\r
+ \r
+ testable: the test algorithm for logical properties\r
+\r
+ Pieter Koopman, 2002-2010\r
+ Radboud Universty, Nijmegen\r
+ The Netherlands\r
+ pieter@cs.ru.nl\r
+*/\r
+\r
+import StdEnv, MersenneTwister, genLibTest /*, StdTime*/ , gen\r
+\r
+derive gLess Result\r
+instance == Result where (==) x y = x===y\r
+\r
+newAdmin :: Admin\r
+newAdmin = {res=Undef, labels=[], args=[], name=[]}\r
+\r
+class TestArg a | genShow{|*|}, ggen{|*|} a\r
+\r
+//class Testable a where evaluate :: a RandomStream Admin -> [Admin]\r
+\r
+//instance Testable Bool where evaluate b rs result = [{result & res = if b OK CE, args = reverse result.args}]\r
+instance Testable Bool where evaluate b rs result=:{args} = [{result & args = reverse args, res = if b OK CE}]\r
+\r
+instance Testable Result where evaluate r rs result=:{args} = [{result & args = reverse args, res = r}]\r
+\r
+instance Testable Property\r
+where evaluate (Prop p) rs result = p rs result\r
+\r
+instance Testable (a->b) | Testable b & TestArg a \r
+where evaluate f rs admin\r
+ # (rs,rs2) = split rs\r
+ = forAll f (generateAll rs) rs2 admin\r
+\r
+instance Testable [a] | Testable a \r
+where\r
+// evaluate [] rs admin=:{args} = [{admin & args = reverse args, res = OK}] \r
+ evaluate list rs admin = diagonal [ evaluate x (genRandInt seed) admin \\ x<-list & seed<-rs ]\r
+// evaluate list rs admin = flatten [ evaluate x (genRandInt seed) admin \\ x<-list & seed<-rs ]\r
+\r
+:: Property = Prop (RandomStream Admin -> [Admin])\r
+\r
+prop :: a -> Property | Testable a\r
+prop p = Prop (evaluate p)\r
+\r
+forAll :: !(a->b) ![a] RandomStream !Admin -> [Admin] | Testable b & TestArg a\r
+forAll f [] rs r=:{args} = [{r & args = reverse args, res = OK}] // to handle empty sets of values\r
+forAll f list rs r = diagonal [apply f a (genRandInt seed) r \\ a<-list & seed<-rs ]\r
+\r
+apply :: !(a->b) a RandomStream !Admin -> [Admin] | Testable b & TestArg a\r
+apply f a rs r = evaluate (f a) rs {r & args = [show1 a:r.args]}\r
+\r
+diagonal :: [[a]] -> [a]\r
+diagonal list = f 1 2 list []\r
+where\r
+ f n m [] [] = []\r
+ f 0 m xs ys = f m (m+1) (rev ys xs) []\r
+ f n m [] ys = f m (m+1) (rev ys []) []\r
+ f n m [[x:r]:xs] ys = [x: f (n-1) m xs [r:ys]]\r
+ f n m [[]:xs] ys = f (n-1) m xs ys\r
+ \r
+ rev [] accu = accu\r
+ rev [x:r] accu = rev r [x:accu]\r
+\r
+generateAll :: !RandomStream -> [a] | ggen{|*|} a\r
+generateAll rnd = ggen{|*|} 2 rnd\r
+\r
+derive gEq Result\r
+derive bimap [], (,), (,,), (,,,), (,,,,), (,,,,,)\r
+\r
+//--- Random ---//\r
+\r
+split :: !RandomStream -> (RandomStream,RandomStream)\r
+split [r,s:rnd]\r
+ # seed = r*s\r
+ | seed==0\r
+ = split rnd\r
+ = (rnd, genRandInt seed)\r
+\r
+(>>=) infix 0 :: (a -> (b,a)) (b a -> d) -> a -> d\r
+(>>=) f g = \st = let (r,st1) = f st in g r st1\r
+\r
+result :: b -> a -> (b,a)\r
+result b = \a = (b,a)\r
+\r
+//--- testing ---//\r
+\r
+:: Config\r
+ = { maxTests :: Int\r
+ , maxArgs :: Int\r
+ , every :: Int Admin [String] -> [String]\r
+ , fails :: Int\r
+ , randoms :: [Int]\r
+ }\r
+\r
+verboseConfig\r
+ = { maxTests = NrOfTest\r
+ , maxArgs = 2*NrOfTest\r
+ , every = verboseEvery\r
+ , fails = 1\r
+ , randoms = aStream\r
+ }\r
+verboseEvery n r c = [blank,toString n,":":showArgs r.args c]\r
+\r
+traceConfig\r
+ = { maxTests = 100\r
+ , maxArgs = 1000\r
+ , every = traceEvery\r
+ , fails = 1\r
+ , randoms = aStream\r
+ }\r
+traceEvery n r c = ["\n",toString n,":":showArgs r.args c]\r
+\r
+blank :: String\r
+blank =: { createArray len ' ' & [0] = '\r', [len-1] = '\r' } where len = 81\r
+\r
+countConfig\r
+ = { maxTests = 100\r
+ , maxArgs = 10000\r
+ , every = countEvery\r
+ , fails = 1\r
+ , randoms = aStream\r
+ }\r
+countEvery n r c = [toString n,"\r": c]\r
+\r
+quietConfig\r
+ = { maxTests = 1000\r
+ , maxArgs = 10000\r
+ , every = animate2 // \n r c = if (n rem 10000 == 0) [".":c] c\r
+ , fails = 1\r
+ , randoms = aStream\r
+ }\r
+\r
+animate n r c\r
+ | n rem Steps == 0\r
+ = case (n/Steps) rem 4 of\r
+ 0 = ["\r|":c]\r
+ 1 = ["\r/":c]\r
+ 2 = ["\r-":c]\r
+ 3 = ["\r\\":c]\r
+ = ["??":c]\r
+ = c\r
+\r
+Steps =: 1000\r
+\r
+animate2 n r c\r
+ | n rem Steps == 0\r
+ = ["\r \r",toString n," ":c]\r
+ = c\r
+\r
+Test :: [Testoption] !p -> [String] | Testable p\r
+Test options p = (\config.testConfig config.randoms {config & randoms = []} p) (foldl handleOption verboseConfig options)\r
+where\r
+ handleOption c (Tests i) = {c & maxTests = i, maxArgs = 2*i}\r
+ handleOption c (Fails i) = {c & fails = i}\r
+ handleOption c (Args i) = {c & maxArgs = i}\r
+ handleOption c (RandomSeed i) = {c & randoms = genRandInt i}\r
+ handleOption c (RandomList r) = {c & randoms = r}\r
+ handleOption c Verbose = {c & every = verboseEvery}\r
+ handleOption c Concise = {c & every = countEvery}\r
+ handleOption c Quiet = {c & every = animate2}\r
+\r
+TestList :: [Testoption] ![p] -> [String] | Testable p\r
+TestList options ps = flatten (map (Test options) ps)\r
+\r
+test :: !p -> [String] | Testable p\r
+test p = testn NrOfTest p\r
+\r
+testn :: !Int !p -> [String] | Testable p\r
+testn n p = verbosen n aStream p\r
+\r
+testnm :: !Int !Int !p -> [String] | Testable p\r
+testnm n m p = testConfig aStream { verboseConfig & maxTests = n, maxArgs = 100*n, fails = m } p\r
+\r
+ttestn :: !Int !p -> [String] | Testable p\r
+ttestn n p = testConfig aStream { traceConfig & maxTests = n, maxArgs = 100*n } p\r
+\r
+ttestnm :: !Int !Int !p -> [String] | Testable p\r
+ttestnm n m p = testConfig aStream { traceConfig & maxTests = n, maxArgs = 100*n, fails = m } p\r
+\r
+verbose :: !RandomStream !p -> [String] | Testable p\r
+verbose rs p = testConfig rs verboseConfig p\r
+\r
+verbosen :: !Int !RandomStream !p -> [String] | Testable p\r
+verbosen n rs p = testConfig rs { verboseConfig & maxTests = n, maxArgs = 100*n } p\r
+\r
+concise :: !RandomStream !p -> [String] | Testable p\r
+concise rs p = testConfig rs countConfig p\r
+\r
+concisen :: !Int !RandomStream !p -> [String] | Testable p\r
+concisen n rs p = testConfig rs { countConfig & maxTests = n, maxArgs = 100*n } p\r
+\r
+quiet :: !RandomStream !p -> [String] | Testable p\r
+quiet rs p = testConfig rs quietConfig p\r
+\r
+quietn :: !Int !RandomStream !p -> [String] | Testable p\r
+quietn n rs p = testConfig rs { quietConfig & maxTests = n, maxArgs = 100*n } p\r
+\r
+quietnm :: !Int !Int !RandomStream !p -> [String] | Testable p\r
+quietnm n m rs p = testConfig rs { quietConfig & maxTests = n, maxArgs = 100*n, fails = m } p\r
+\r
+aStream :: RandomStream\r
+aStream = genRandInt 1957 //1964\r
+\r
+gather :: [Admin] -> [[String]]\r
+gather list = [r.args \\ r<- list]\r
+\r
+testConfig :: RandomStream Config p -> [String] | Testable p\r
+testConfig rs {maxTests,maxArgs,every,fails} p = analyse (evaluate p rs newAdmin) maxTests maxArgs 0 0 0 [] []\r
+where\r
+ analyse :: ![.Admin] !Int !Int !Int !Int !Int ![(String,Int)] ![String] -> [String]\r
+ analyse [] ntests nargs 0 0 0 labels name = [blank:showName name [" Proof: success for all arguments": conclude ntests nargs 0 0 labels]]\r
+ analyse [] ntests nargs nrej 0 0 labels name = [blank:showName name [" Proof: Success for all not rejected arguments,": conclude ntests nargs nrej 0 labels]]\r
+ analyse [] ntests nargs nrej nund 0 labels name \r
+ | ntests==maxTests = [blank:showName name [" Undefined: no success nor counter example found, all tests rejected or undefined ": conclude ntests nargs nrej nund labels]]\r
+ = [blank:showName name [" Success for arguments, ": conclude ntests nargs nrej nund labels]]\r
+ analyse [] ntests nargs nrej nund ne labels name = [blank:showName name [toString ne," counterexamples found,": conclude ntests nargs nrej nund labels]]\r
+ analyse _ 0 nargs nrej nund 0 labels name = [blank:showName name [" Passed": conclude 0 nargs nrej nund labels]]\r
+ analyse _ 0 nargs nrej nund ne labels name = [blank:showName name [toString ne," counterexamples found,": conclude 0 nargs nrej nund labels]]\r
+ analyse _ ntests 0 nrej nund 0 labels name \r
+ | ntests==maxTests = [blank:showName name [" No tests performed, maximum number of arguments (",toString maxArgs,") generated": conclude ntests 0 nrej nund labels]]\r
+ = [blank:showName name [" Passed: maximum number of arguments (",toString maxArgs,") generated": conclude ntests 0 nrej nund labels]]\r
+ analyse _ ntests 0 nrej nund ne labels name = [blank:showName name [toString ne," counterexamples found,": conclude 0 0 nrej nund labels]]\r
+ analyse [res:rest] ntests nargs nrej nund ne labels name \r
+ = every (maxTests-ntests+1) res\r
+ ( case res.res of\r
+ OK = analyse rest (ntests-1) (nargs-1) nrej nund ne (admin res.labels labels) res.name\r
+ Pass = analyse rest (ntests-1) (nargs-1) nrej nund ne (admin res.labels labels) res.name // NOT YET CORRECT ?\r
+ CE = ["\r":showName res.name ["Counterexample ",toString (ne+1)," found after ",toString (maxTests-ntests+1)," tests:":showArgs res.args ["\n":more]]]\r
+ where\r
+ more | ne+1<fails\r
+ = analyse rest (ntests-1) (nargs-1) nrej nund (ne+1) labels res.name\r
+ = showName res.name [toString (ne+1)," counterexamples found,": conclude (ntests-1) nargs nrej nund labels]\r
+ Rej = analyse rest ntests (nargs-1) (nrej+1) nund ne labels res.name\r
+ Undef = analyse rest ntests (nargs-1) nrej (nund+1) ne labels res.name\r
+ = abort "Error in Gast: analyse; missing case for result\n"\r
+ )\r
+\r
+ conclude ntests nargs nrej nund labels\r
+ # n = maxTests-ntests\r
+ rest = showLabels n (sort labels)\r
+ rest = case nrej of\r
+ 0 = rest\r
+ 1 = [" one case rejected":rest]\r
+ = [" ",toString nrej," cases rejected":rest]\r
+ rest = case nund of\r
+ 0 = rest\r
+ 1 = [" one case undefined":rest]\r
+ = [" ",toString nund," cases undefined":rest]\r
+ | n==0\r
+ = rest\r
+ = [" after ",toString n," tests":rest]\r
+\r
+ admin :: ![String] ![(String,Int)] -> [(String,Int)]\r
+ admin [] accu = accu\r
+ admin [label:rest] accu = admin rest (insert label accu)\r
+\r
+ insert :: !String ![(String,Int)] -> [(String,Int)]\r
+ insert label [] = [(label,1)]\r
+ insert label [this=:(old,n):rest]\r
+ | label==old\r
+ = [(old,n+1):rest]\r
+ = [this:insert label rest]\r
+\r
+ showLabels :: !Int ![(String,Int)] -> [String]\r
+ showLabels ntests [] = ["\n"]\r
+ showLabels 0 [(lab,n):rest] = ["\n",lab,": ",toString n:showLabels 0 rest]\r
+ showLabels ntests [(lab,n):rest] = ["\n",lab,": ",toString n," (",toString (toReal (n*100)/toReal ntests),"%)":showLabels ntests rest]\r
+\r
+ showName l c = s (reverse l) c\r
+ where\r
+ s [] c = c\r
+ s [l] c = [l," ":c]\r
+ s [a:x] c = [a,".":s x c]\r
+\r
+cr :== "\r"\r
+\r
+showArgs :: ![String] [String] -> [String]\r
+showArgs [] c = c // ["\n":c] // c\r
+showArgs [a:rest] c = [" ",a: showArgs rest c]\r
repositories / tt2015.git / commitdiff