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