From 81d74e891ca9c02ef58f59cc7102bc8e2c73a0b5 Mon Sep 17 00:00:00 2001 From: Steffen Michels Date: Wed, 14 Feb 2018 15:37:22 +0100 Subject: [PATCH] include counter examples in json end event messages --- Libraries/Gast/Testable.icl | 103 ++++++++++++++++++++++-------------- 1 file changed, 62 insertions(+), 41 deletions(-) diff --git a/Libraries/Gast/Testable.icl b/Libraries/Gast/Testable.icl index da50c49..ad0d3f1 100644 --- a/Libraries/Gast/Testable.icl +++ b/Libraries/Gast/Testable.icl @@ -22,9 +22,11 @@ instance == Result where (==) x y = x===y newAdmin :: Admin newAdmin = {res=Undef, labels=[], args=[], name=[], mes = []} -instance Testable Bool where evaluate b genState result=:{args} = [{result & args = reverse args, res = if b OK CE}] +instance Testable Bool where + evaluate b genState result=:{Admin| args} = [{result & args = reverse args, res = if b OK CE}] -instance Testable Result where evaluate r genState result=:{args} = [{result & args = reverse args, res = r}] +instance Testable Result where + evaluate r genState result=:{Admin| args} = [{result & args = reverse args, res = r}] instance Testable Property where evaluate (Prop p) genState result = p genState result @@ -40,11 +42,11 @@ prop :: a -> Property | Testable a prop p = Prop (evaluate p) forAll :: !(a->b) ![a] GenState !Admin -> [Admin] | Testable b & TestArg a -forAll f [] genState r=:{args} = [{r & args = reverse args, res = OK}] // to handle empty sets of values +forAll f [] genState r=:{Admin| args} = [{r & args = reverse args, res = OK}] // to handle empty sets of values forAll f list genState r = diagonal [apply f a genState r \\ a<-list ] // copy the genState apply :: !(a->b) a GenState !Admin -> [Admin] | Testable b & TestArg a -apply f a genState r = evaluate (f a) genState {r & args = [show1 a:r.args]} +apply f a genState r = evaluate (f a) genState {Admin| r & args = [show1 a:r.Admin.args]} diagonal :: [[a]] -> [a] diagonal list = f 1 2 list [] @@ -70,16 +72,16 @@ derive bimap [], (,), (,,), (,,,), (,,,,), (,,,,,) = { maxTests :: Int , maxArgs :: Int , everyOutput :: Int Admin [String] -> [String] - , counterExampleOutput :: Int Int Int [String] [String] [String] -> [String] + , counterExampleOutput :: CounterExample [String] -> [String] , beforeStartOutput :: [String] -> [String] - , resultOutput :: TestsResult [(!String, !Int)] [String] -> [String] + , resultOutput :: TestsResult [CounterExample] [(!String, !Int)] [String] -> [String] , fails :: Int , randoms :: [Int] , genState :: GenState } /** - * Represents the combined results of all tests for a single property. + * The combined results of all tests for a single property. * This is in contrast to {{Result}} which represents the result of a single test. */ :: TestsResult = { maxTests :: !Int //* Maximum number of tests @@ -87,7 +89,7 @@ derive bimap [], (,), (,,), (,,,), (,,,,), (,,,,,) , resultType :: !ResultType //* Type of the result } /** - * Represent the type of the combined result, together with information + * The type of the combined result, together with information * specific to that type of result. */ :: ResultType = Proof !Int //* Proof by exhaustive testing: nTests @@ -96,6 +98,16 @@ derive bimap [], (,), (,,), (,,,), (,,,,), (,,,,,) | Undefined !Int //* Undefined result: nUnd | NoTests !Int !Int !Int //* No tests performed: maxArgs nTests nUnd +/** + * A counter examples. + */ +:: CounterExample = { maxTests :: !Int //* Maximal number of tests for run in which counter example is found + , nTests :: !Int //* maxTests MINUS number of test at which counter example is found + , nE :: !Int //* Number of counter example + , args :: ![String] //* Arguments used for test + , name :: ![String] //* Name of property + } + verboseConfig = { maxTests = NrOfTest , maxArgs = 2*NrOfTest @@ -108,7 +120,7 @@ verboseConfig , genState = genState } -verboseEvery n r c = [blank,toString n,":":showArgs r.args (r.mes++c)] +verboseEvery n r c = [blank,toString n,":":showArgs r.Admin.args (r.mes++c)] traceConfig = { maxTests = 100 @@ -121,7 +133,7 @@ traceConfig , randoms = aStream , genState = genState } -traceEvery n r c = [toString n,":":showArgs r.args ["\n":r.mes++c]] +traceEvery n r c = [toString n,":":showArgs r.Admin.args ["\n":r.mes++c]] blank :: String blank =: { createArray len ' ' & [0] = '\r', [len-1] = '\r' } where len = 81 @@ -181,30 +193,28 @@ animate2 n r c = ["\r \r",toString n," ":c] = c -noCounterExampleOutput :: Int Int Int [String] [String] [String] -> [String] -noCounterExampleOutput _ _ _ _ _ acc = acc +noCounterExampleOutput :: CounterExample [String] -> [String] +noCounterExampleOutput _ acc = acc noBeforeOutput :: ![String] -> [String] noBeforeOutput _ = [] noEveryOutput _ _ c = ["":c] // FIXME: empty string required to prevent stack overflow, why? -humanReadableCEOutput :: Int Int Int [String] [String] [String] -> [String] -humanReadableCEOutput maxTests nTests nE args name acc = - [ "\r" - : showName True - name - [ "Counterexample " - , toString (nE+1) - , " found after " - , pluralisen English (maxTests - nTests + 1) "test" - , ":" - : showArgs args ["\n":acc] - ] - ] - -humanReadableResOutput :: Bool TestsResult [(String, Int)] [String] -> [String] -humanReadableResOutput addWhite {maxTests, nRej, resultType} labels name = withBlank $ showName True name resStr +humanReadableCEOutput :: CounterExample [String] -> [String] +humanReadableCEOutput {maxTests, nTests, nE, args, name} acc = + showName True + name + [ "Counterexample " + , toString (nE+1) + , " found after " + , pluralisen English (maxTests - nTests + 1) "test" + , ":" + : showArgs args ["\n":acc] + ] + +humanReadableResOutput :: Bool TestsResult [CounterExample] [(String, Int)] [String] -> [String] +humanReadableResOutput addWhite {maxTests, nRej, resultType} _ labels name = withBlank $ showName True name resStr where resStr = case resultType of Proof nTests -> ["Proof: ", msgStr: conclude addWhite nTests 0 labels] @@ -253,12 +263,12 @@ where jsonEventStart :: ![String] -> [String] jsonEventStart name = [toString $ toJSON {StartEvent | name = concat $ showName False name []}, "\n"] -jsonEventEnd :: TestsResult [(String, Int)] [String] -> [String] -jsonEventEnd res labels name = [toString (toJSON endEvent) +++ "\n"] +jsonEventEnd :: TestsResult [CounterExample] [(String, Int)] [String] -> [String] +jsonEventEnd res counterExamples labels name = [toString (toJSON endEvent) +++ "\n"] where endEvent = { name = concat $ showName False name [] , event = eventType - , message = concat $ humanReadableResOutput False res labels [] + , message = concat $ foldl (flip humanReadableCEOutput) (humanReadableResOutput False res counterExamples labels []) counterExamples } eventType = case res.resultType of @@ -368,14 +378,15 @@ testConfig :: RandomStream Config p -> [String] | Testable p testConfig rs {maxTests,maxArgs,everyOutput,counterExampleOutput,beforeStartOutput,resultOutput,fails,genState} p // we first have to evaluate to get the name # res = evaluate p genState newAdmin - = [concat $ beforeStartOutput (hd res).Admin.name : analyse res maxTests maxArgs 0 0 0 [] []] + = [concat $ beforeStartOutput (hd res).Admin.name : analyse res maxTests maxArgs 0 0 0 [] [] []] where - analyse :: ![.Admin] !Int !Int !Int !Int !Int ![(String,Int)] ![String] -> [String] - analyse results nTests nArgs nRej nUnd nE labels name = + analyse :: ![.Admin] !Int !Int !Int !Int !Int [CounterExample] ![(String,Int)] ![String] -> [String] + analyse results nTests nArgs nRej nUnd nE counterExamples labels name = case analyse` results nTests nArgs nRej nUnd nE of // testing of property finished Just resType -> resultOutput {maxTests = maxTests, nRej = nRej, resultType = resType} + counterExamples labels name // continue with testing property @@ -383,22 +394,32 @@ where let [res:rest] = results in everyOutput (maxTests-nTests+1) res ( case res.res of - OK = analyse rest (nTests-1) (nArgs-1) nRej nUnd nE (admin res.labels labels) res.Admin.name - Pass = analyse rest (nTests-1) (nArgs-1) nRej nUnd nE (admin res.labels labels) res.Admin.name // NOT YET CORRECT ? - CE = counterExampleOutput maxTests nTests nE res.args res.Admin.name more - where + OK = analyse rest (nTests-1) (nArgs-1) nRej nUnd nE + counterExamples (admin res.labels labels) res.Admin.name + Pass = analyse rest (nTests-1) (nArgs-1) nRej nUnd nE + counterExamples (admin res.labels labels) res.Admin.name // NOT YET CORRECT ? + CE = counterExampleOutput counterExample more + where + counterExample = { maxTests = maxTests + , nTests = nTests + , nE = nE + , args = res.Admin.args + , name = res.Admin.name + } + more | nE+1