+implementation module confSM\r
+\r
+/*\r
+ GAST: A Generic Automatic Software Test-system\r
+ \r
+ ioco: Input Output COnformance of reactive systems\r
+\r
+ Pieter Koopman, 2004, 2005\r
+ Radboud Universty, Nijmegen\r
+ The Netherlands\r
+ pieter@cs.ru.nl\r
+*/\r
+\r
+import StdEnv, MersenneTwister, gen, GenEq, genLibTest, testable, StdLib\r
+\r
+toSpec :: (state input -> [(state,[output])]) -> Spec state input output // conversion for old specificaions\r
+toSpec fun = \s i = [Pt o t \\ (t,o) <- fun s i]\r
+\r
+SpectoIUTstep :: (Spec t i o) (t i -> [[o]]) -> IUTstep (t,RandomStream) i o | genShow{|*|} t & genShow{|*|} i & genShow{|*|} o\r
+SpectoIUTstep spec outputGen = selectTrans\r
+where\r
+ selectTrans (t,[r,r2,r3:rnd]) i\r
+ # tuples = spec t i\r
+ len = lengthN 353 0 tuples\r
+ | len == 0\r
+ = abort ("\n\nIUT is not input enabled in state "+show1 t+" for input "+show1 i+"\n")\r
+ = case tuples !! ((abs r) rem len) of\r
+ Pt o t = (o,(t,rnd))\r
+ Ft f # outputs = outputGen t i\r
+ leno = lengthN 31 0 outputs\r
+ | leno == 0\r
+ = abort ("\n\nOutput function yields no output in state "+show1 t+" for input "+show1 i+"\n")\r
+ # output = outputs !! ((abs r2) rem leno)\r
+ states = f output\r
+ lens = lengthN 37 0 states\r
+ | lens == 0\r
+ = abort ("\n\nIUT is not input enabled in state "+show1 t+" for input "+show1 i+" output "+show1 output+"\n")\r
+ = (output,(states !! ((abs r3) rem lens),rnd))\r
+ \r
+ // =abort "toUIT"\r
+\r
+:: NewInput i = NewInput i | Reset | End\r
+\r
+:: *TestState s i o\r
+ = !{ spec :: !Spec s i o\r
+// , specW :: !SpecWorld s i\r
+ , iniState:: !s\r
+ , curState:: ![s]\r
+ , nRej :: !Int\r
+ , nTrun :: !Int\r
+ , nPath :: !Int\r
+ , nStep :: !Int\r
+ , nTotal :: !Int\r
+ , maxPath :: !Int\r
+ , maxLen :: !Int\r
+ , nOnPath :: !Int\r
+ , inputs :: (RandomStream s -> [i])\r
+ , input :: !((TestState s i o) -> *(NewInput i, TestState s i o))\r
+ , n :: !Int\r
+ , rnd :: RandomStream\r
+ , h_in :: [i]\r
+ , h_out :: [[o]]\r
+ , h_state :: [[s]]\r
+ , fileName:: String\r
+ , errFile :: !*File\r
+ , mesFile :: !*File\r
+ , trace :: !Bool\r
+ , incons :: [o] [s] -> Maybe [String]\r
+ , stop :: [s] -> Bool\r
+ }\r
+/*\r
+apply :: i (IUT s i o) -> ([o],IUT s i o) | genShow{|*|} s & genShow{|*|} i\r
+apply i (IUT f s [r:rnd])\r
+ = case f s i of\r
+ [] = abort ("IUT is not input enabled! State: "+++show1 s+++", input: "+++show1 i)\r
+ list\r
+ # n = length list\r
+ (t,o) = list !! ((abs r) rem n)\r
+ = (o,IUT f t rnd)\r
+*/\r
+ \r
+switchSpec :: (Spec s i o) (TestState s i o) -> *(NewInput i, TestState s i o) | ggen{|*|} i\r
+switchSpec spec ts=:{nOnPath} = newSpec spec nOnPath ts\r
+\r
+newSpec :: (Spec s i o) !Int (TestState s i o) -> *(NewInput i, TestState s i o) | ggen{|*|} i\r
+newSpec spec2 0 ts=:{spec} = oldSpec spec {ts & spec = spec2}\r
+newSpec spec2 n ts\r
+ # (i,ts) = onTheFly ts\r
+ = case i of\r
+ Reset = (i,{ ts & input = newSpec spec2 ts.nOnPath })\r
+ NewInput _ = (i,{ ts & input = newSpec spec2 (n-1)})\r
+ _ = (i,ts)\r
+\r
+oldSpec :: (Spec s i o) (TestState s i o) -> *(NewInput i, TestState s i o) | ggen{|*|} i\r
+oldSpec spec2 ts\r
+ # (i,ts) = onTheFly ts\r
+ = case i of\r
+ Reset = (i,{ ts & input = newSpec spec2 ts.nOnPath })\r
+ _ = (i,ts)\r
+\r
+onAndOff :: (TestState s i o) -> *(NewInput i, TestState s i o) | ggen{|*|} i\r
+onAndOff ts=:{nOnPath} = onPath nOnPath ts\r
+\r
+onPath :: Int (TestState s i o) -> *(NewInput i, TestState s i o) | ggen{|*|} i\r
+onPath 0 ts=:{spec}\r
+ # (rnd1,rnd2) = split ts.rnd\r
+ = offPath spec (ggen{|*|} 2 rnd1) {ts & spec = mkComplete spec, rnd = rnd2} \r
+onPath n ts\r
+ # (i,ts) = onTheFly ts\r
+ = case i of\r
+ Reset = (i,{ ts & input = onPath ts.nOnPath })\r
+ NewInput _ = (i,{ ts & input = onPath (n-1)})\r
+ _ = (i,ts)\r
+\r
+mkComplete spec s i\r
+ = case spec s i of\r
+ [] = [Pt [] s]\r
+ r = r\r
+\r
+offPath :: (Spec s i o) [i] (TestState s i o) -> *(NewInput i, TestState s i o) | ggen{|*|} i\r
+offPath spec [] ts = (Reset,{ ts & input = onPath ts.nOnPath })\r
+offPath spec [i:r] ts\r
+ | ts.nStep >= ts.maxLen-1 || ts.nRej >= ts.maxLen-1\r
+ = (Reset,{ ts & input = onPath ts.nOnPath })\r
+ = (NewInput i,{ts & input = offPath spec r})\r
+\r
+onTheFly :: (TestState s i o) -> *(NewInput i, TestState s i o)\r
+onTheFly ts=:{curState,inputs,rnd,spec}\r
+ # [r1,r2:rnd] = rnd\r
+ = case [ i \\ s <- randomize curState (genRandInt r1) 2 (\_=[])\r
+ , i <- inputs (genRandInt r2) s\r
+ | not (isEmpty (spec s i))\r
+ ] of\r
+ [] = (Reset, {ts & rnd=rnd})\r
+ is # max = 157 // the maximum number of outputs to consider\r
+ n = lengthN max 0 is // the number of the selected input\r
+ [r:rnd] = rnd\r
+ i = is !! ((abs r) rem n)\r
+ = (NewInput i,{ts & rnd = rnd})\r
+\r
+lengthN :: !Int !Int ![a] -> Int\r
+lengthN m n [] = n\r
+lengthN m n [a:x]\r
+ | n<m\r
+ = lengthN m (n+1) x\r
+ = m\r
+\r
+fixedInputs [] ts = (End, ts)\r
+fixedInputs [[] :r] ts = (Reset, { ts & input = fixedInputs r })\r
+fixedInputs [[a:x]:r] ts=:{curState,spec} \r
+ | isEmpty [t \\ s<- curState, t<-spec s a]\r
+ = (Reset, { ts & input = fixedInputs r , nTrun = ts.nTrun+1})\r
+ = (NewInput a, {ts & input = fixedInputs [x:r]})\r
+\r
+genLongInput :: s Int (Spec s i o) [i] [Int] -> [i]\r
+genLongInput s 0 spec inputs [r:x] = randomize inputs x 7 (\_.[])\r
+genLongInput s n spec inputs [r,r2:x]\r
+ = case [ i \\ i <- inputs | not (isEmpty (spec s i)) ] of\r
+ [] = []\r
+ l # i = l !! ((abs r) rem (length l))\r
+ = case spec s i of\r
+ [] = abort "\n\nError in genLongInput, please report.\n\n"\r
+ list # len = length list\r
+ s = case list !! ((abs r2) rem len) of\r
+ Pt o s = s\r
+ Ft f = abort "genLongInput Ft f"\r
+ = [ i : genLongInput s (n-1) spec inputs x ] \r
+\r
+genLongInputs :: s (Spec s i o) [i] Int [Int] -> [[i]]\r
+genLongInputs s spec inputs n [r:x] = [genLongInput s n spec inputs (genRandInt r): genLongInputs s spec inputs n x]\r
+\r
+testConfSM :: [TestOption s i o] (Spec s i o) s (IUTstep .t i o) .t (.t->.t) *File *File -> (.t,*File,*File)\r
+ | ggen{|*|} i & gEq{|*|} s & gEq{|*|} o & genShow{|*|} s & genShow{|*|} i & genShow{|*|} o\r
+testConfSM opts spec s0 iut t reset console file\r
+ # ts=:{fileName} = initState file console\r
+ # (t,ts) = doTest ts iut t reset\r
+ {mesFile,errFile} = ts\r
+ = (t, mesFile, errFile)\r
+where\r
+ initState file console\r
+ = handleOptions opts\r
+ { spec = spec\r
+ // , specW = \s i.[]\r
+ , iniState= s0\r
+ , curState= [s0]\r
+ , nRej = 0\r
+ , nTrun = 0\r
+ , nPath = 0\r
+ , nStep = 0\r
+ , nTotal = 0\r
+ , maxPath = 100\r
+ , maxLen = 1000\r
+ , nOnPath = 50\r
+ , inputs = (\rnd s -> ggen {|*|} 2 rnd)\r
+ , input = onTheFly \r
+ , n = 0\r
+ , h_in = []\r
+ , h_out = []\r
+ , h_state = []\r
+ , rnd = aStream\r
+ , errFile = file\r
+ , fileName= outputFile\r
+ , mesFile = console <<< "Gast starts testing.\n"\r
+ , trace = False\r
+ , incons = \o ss -> Nothing\r
+ , stop = (\states = False)\r
+ }\r
+\r
+findFileName [] name = name\r
+findFileName [ErrorFile s:r] name = findFileName r s\r
+findFileName [_:r] name = findFileName r name\r
+\r
+doTest :: (TestState s i o) (IUTstep .t i o) .t (.t->.t) -> (.t,TestState s i o)\r
+ | gEq{|*|} s & gEq{|*|} o & genShow{|*|} s & genShow{|*|} i & genShow{|*|} o\r
+doTest ts=:{input,curState,spec,incons} step t reset\r
+ | isEmpty ts.curState\r
+ = (t, errorFound ts)\r
+ | ts.nStep >= ts.maxLen || ts.nRej >= ts.maxLen\r
+ = doTest (resetState ts) step (reset t) reset\r
+ | ts.nPath >= ts.maxPath\r
+ | ts.nRej == 0 && ts.nTrun == 0\r
+ = (t,{ts & mesFile = ts.mesFile <<< "\nEnd of testing, maximum paths used. \n"\r
+ <<< ts.nPath\r
+ <<< " test paths executed successful, in total "\r
+ <<< ts.nTotal <<< " transitions.\n"})\r
+ = (t,{ts & mesFile = ts.mesFile <<< "\nEnd of testing, maximum paths used. \n"\r
+ <<< ts.nPath\r
+ <<< " test paths executed successful, "\r
+ <<< ts.nTrun <<< " paths truncated, "\r
+ <<< " in total "\r
+ <<< ts.nTotal <<< " transitions.\n"})\r
+ # (inp,ts) = input ts\r
+ = case inp of\r
+ Reset = doTest (resetState ts) step (reset t) reset\r
+ End | ts.nRej == 0 && ts.nTrun == 0\r
+ = (t,{ts & mesFile = ts.mesFile <<< "\nAll input paths tested successfully.\n"\r
+ <<< "All " <<< ts.nPath\r
+ <<< " executed test paths successful (Proof), in total "\r
+ <<< ts.nTotal <<< " transitions.\n"})\r
+ = (t,{ts & mesFile = ts.mesFile <<< "\nAll inputs tested successfully.\n"\r
+ <<< (ts.nPath-ts.nRej)\r
+ <<< "test path executed successful (Proof), " <<< ts.nRej\r
+ <<< " paths rejected " <<< ts.nTrun\r
+ <<< " paths truncated, "\r
+ <<< "in total " <<< ts.nTotal <<< " transitions.\n"})\r
+ NewInput i // assumption: only inputs allowed by spec will be generated:\r
+ #! (iut_o,t) = step t i\r
+ tuples = [tup \\ s<-curState, tup<-spec s i]\r
+ states = mkset (newStates tuples iut_o)\r
+ | isEmpty states\r
+ #! errFile = ts.errFile <<< "Issue found! Trace:\n"\r
+ <<< "SpecificationStates Input -> ObservedOutput\n"\r
+ errFile = showError (ts.nStep+1) [curState:ts.h_state] [i:ts.h_in] [iut_o:ts.h_out] errFile\r
+ errFile = errorInfo ts.nPath ts.nRej ts.nTrun (ts.nTotal+1) (errFile <<< "\n")\r
+ mesFile = errorInfo ts.nPath ts.nRej ts.nTrun (ts.nTotal+1) ts.mesFile\r
+ mesFile = mesFile <<< "See file \"" <<< ts.fileName <<< "\" for details about the issue.\n"\r
+ = (t,{ts & mesFile = mesFile\r
+ , errFile = errFile\r
+ , curState = []\r
+ })\r
+ = case incons iut_o states of\r
+ Nothing\r
+ # mesFile = ts.mesFile <<< "paths: " <<< ts.nPath <<< ", rejected: " <<< ts.nRej <<< ", truncated: " <<< ts.nTrun <<< "...\r"\r
+ = doTest {ts & curState = states\r
+ , nStep = ts.nStep+1\r
+ , nTotal =ts.nTotal+1\r
+ , h_in = [i:ts.h_in]\r
+ , h_out = [iut_o:ts.h_out]\r
+ , h_state = [curState:ts.h_state]\r
+ , mesFile = if ts.trace (mesFile <<< ts.nPath <<< "," <<< ts.nStep <<< ": " <<< show1 ts.curState <<< " " <<< show1 i <<< " " <<< show1 iut_o <<< "\n") mesFile\r
+ }\r
+ step t reset\r
+ Just errors \r
+ #! errFile = ts.errFile <<< "Inconsistency! Trace:\n"\r
+ <<< "SpecificationStates Input -> ObservedOutput\n"\r
+ errFile = showError (ts.nStep+1) [curState:ts.h_state] [i:ts.h_in] [iut_o:ts.h_out] errFile\r
+ errFile = errFile <<< "Inconsistency info:\n" <<< errors <<< "\n"\r
+ errFile = errorInfo ts.nPath ts.nRej ts.nTrun (ts.nTotal+1) (errFile <<< "\n")\r
+ mesFile = ts.mesFile <<< "Inconsistency found!\n" <<< errors <<< "\n\n"\r
+ mesFile = errorInfo ts.nPath ts.nRej ts.nTrun (ts.nTotal+1) mesFile\r
+ mesFile = mesFile <<< "See file \"" <<< ts.fileName <<< "\" for details.\n"\r
+ = (t,{ts & mesFile = mesFile\r
+ , errFile = errFile\r
+ , curState = []\r
+ })\r
+where\r
+ errorInfo :: !Int !Int !Int !Int *File -> *File\r
+ errorInfo nPath nRej nTrun nTotal file\r
+ = file <<< "Issue found in path " <<< (nPath+1) <<< ", "\r
+ <<< (nPath-nRej) <<< " paths executed, "\r
+ <<< nTrun <<< " tests truncated, in total "\r
+ <<< nTotal <<< " transitions.\n"\r
+\r
+outputFile = "testOut.txt"\r
+\r
+newStates [] iut_o = []\r
+newStates [Pt o s:r] iut_o\r
+ | o === iut_o\r
+ = [s:newStates r iut_o]\r
+ = newStates r iut_o\r
+newStates [Ft f:r] iut_o = f iut_o ++ newStates r iut_o\r
+\r
+resetState ts\r
+ = {ts & curState = [ts.iniState]\r
+ , nPath = ts.nPath+1\r
+ , nStep = 0\r
+ , h_in = []\r
+ , h_out = []\r
+ , h_state = []\r
+ , mesFile = if ts.trace (ts.mesFile <<< "End of path reached: reset.\n") ts.mesFile\r
+ }\r
+\r
+errorFound ts=:{errFile,mesFile}\r
+ # errFile = errFile <<< "Issue Found!\n"\r
+ # mesFile = mesFile <<< "Issue Found!\n"\r
+ = {ts & errFile = errFile,mesFile=mesFile}\r
+\r
+restart testState = { testState & h_in = [], h_out = [], h_state = [] }\r
+ /*\r
+testConfSM :: [TestOption s i o] (Spec s i o) s (IUTstep .t i o) .t (.t->.t) *d -> (.t,*d)\r
+ | FileSystem d & ggen{|*|} i & gEq{|*|} s & gEq{|*|} o & genShow{|*|} s & genShow{|*|} i & genShow{|*|} o\r
+testConfSM opts spec s0 iut t reset world\r
+ # (console,world) = stdio world\r
+ filename = findFileName opts outputFile\r
+ # (ok,file,world) = fopen filename FWriteText world\r
+ | not ok\r
+ # console = console <<< "Cannot open output file "<<< filename\r
+ = (t, snd (fclose console world))\r
+ # //console = console <<< ".\n"\r
+ ts=:{fileName} = initState file console\r
+ # (t,ts) = doTest ts iut t reset\r
+ {mesFile,errFile} = ts\r
+ = (t, snd (fclose mesFile (snd (fclose errFile world))))\r
+where\r
+ initState file console\r
+ = handleOptions opts\r
+ { spec = spec\r
+ , iniState= s0\r
+ , curState= [s0]\r
+ , nRej = 0\r
+ , nTrun = 0\r
+ , nPath = 0\r
+ , nStep = 0\r
+ , nTotal = 0\r
+ , maxPath = 100\r
+ , maxLen = 1000\r
+ , nOnPath = 50\r
+ , inputs = (\rnd s -> ggen {|*|} 2 rnd)\r
+ , input = onTheFly \r
+ , n = 0\r
+ , h_in = []\r
+ , h_out = []\r
+ , h_state = []\r
+ , rnd = aStream\r
+ , errFile = file\r
+ , fileName= outputFile\r
+ , mesFile = console <<< "Gast starts testing.\n"\r
+ , trace = False\r
+ , incons = \o ss -> Nothing\r
+ , stop = (\states = False)\r
+ }\r
+\r
+findFileName [] name = name\r
+findFileName [ErrorFile s:r] name = findFileName r s\r
+findFileName [_:r] name = findFileName r name\r
+\r
+doTest :: (TestState s i o) (IUTstep .t i o) .t (.t->.t) -> (.t,TestState s i o)\r
+ | gEq{|*|} s & gEq{|*|} o & genShow{|*|} s & genShow{|*|} i & genShow{|*|} o\r
+doTest ts=:{input,curState,spec,stop} step t reset\r
+ | isEmpty ts.curState\r
+ = (t, errorFound ts)\r
+ | ts.nStep >= ts.maxLen || ts.nRej >= ts.maxLen || stop curState\r
+ = doTest (resetState ts) step (reset t) reset\r
+ | ts.nPath >= ts.maxPath\r
+ | ts.nRej == 0 && ts.nTrun == 0\r
+ = (t,{ts & mesFile = ts.mesFile <<< "\nEnd of testing, maximum paths used. \n"\r
+ <<< ts.nPath\r
+ <<< " test paths executed successful, in total "\r
+ <<< ts.nTotal <<< " transitions.\n"})\r
+ = (t,{ts & mesFile = ts.mesFile <<< "\nEnd of testing, maximum paths used. \n"\r
+ <<< ts.nPath\r
+ <<< " test paths executed successful, "\r
+ <<< ts.nTrun <<< " paths truncated, "\r
+ <<< " in total "\r
+ <<< ts.nTotal <<< " transitions.\n"})\r
+ # (inp,ts) = input ts\r
+ = case inp of\r
+ Reset = doTest (resetState ts) step (reset t) reset\r
+ End | ts.nRej == 0 && ts.nTrun == 0\r
+ = (t,{ts & mesFile = ts.mesFile <<< "\nAll input paths tested successfully.\n"\r
+ <<< "All " <<< ts.nPath\r
+ <<< " executed test paths successful (Proof), in total "\r
+ <<< ts.nTotal <<< " transitions.\n"})\r
+ = (t,{ts & mesFile = ts.mesFile <<< "\nAll inputs tested successfully.\n"\r
+ <<< (ts.nPath-ts.nRej)\r
+ <<< "test path executed successful (Proof), " <<< ts.nRej\r
+ <<< " paths rejected " <<< ts.nTrun\r
+ <<< " paths truncated, "\r
+ <<< "in total " <<< ts.nTotal <<< " transitions.\n"})\r
+// Input i // assumption: only inputs allowed by spec will be generated:\r
+ NewInput i // assumption: only inputs allowed by spec will be generated:\r
+ #! (iut_o,t) = step t i\r
+ tuples = [tup \\ s<-curState, tup<-spec s i]\r
+ = case mkset (newStates tuples iut_o) of\r
+ [] #! errFile = ts.errFile <<< "Issue found! Trace:\n"\r
+ <<< "SpecificationStates Input -> ObservedOutput\n"\r
+ errFile = showError (ts.nStep+1) [curState:ts.h_state] [i:ts.h_in] [iut_o:ts.h_out] errFile\r
+ errFile = errFile <<< "\nAllowed outputs and target states: " <<< show tuples <<< "\n"\r
+ errFile = errorInfo ts.nPath ts.nRej ts.nTrun (ts.nTotal+1) (errFile <<< "\n")\r
+ mesFile = errorInfo ts.nPath ts.nRej ts.nTrun (ts.nTotal+1) ts.mesFile\r
+ mesFile = mesFile <<< "See file \"" <<< ts.fileName <<< "\" for details about the issue.\n"\r
+\r
+ = (t,{ts & mesFile = mesFile\r
+ , errFile = errFile\r
+ , curState = []\r
+ })\r
+ states #! mesFile = ts.mesFile <<< "paths: " <<< ts.nPath <<< ", rejected: " <<< ts.nRej <<< ", truncated: " <<< ts.nTrun <<< "...\r"\r
+ = doTest {ts & curState = states\r
+ , nStep = ts.nStep+1\r
+ , nTotal =ts.nTotal+1\r
+ , h_in = [i:ts.h_in]\r
+ , h_out = [iut_o:ts.h_out]\r
+ , h_state = [curState:ts.h_state]\r
+ , mesFile = if ts.trace (mesFile <<< ts.nPath <<< "," <<< ts.nStep <<< ": " <<< show1 ts.curState <<< " " <<< show1 i <<< " " <<< show1 iut_o <<< "\n") mesFile\r
+ }\r
+ step t reset\r
+ where\r
+ errorInfo :: !Int !Int !Int !Int *File -> *File\r
+ errorInfo nPath nRej nTrun nTotal file\r
+ = file <<< "Issue found in path " <<< (nPath+1) <<< ", "\r
+ <<< (nPath-nRej) <<< " paths executed to bound or end, "\r
+ <<< nTrun <<< " paths truncated, in total "\r
+ <<< nTotal <<< " transitions.\n"\r
+\r
+ // = (t,{ts & mesFile = ts.mesFile <<< "\nAll inputs tested successfully\n"})\r
+\r
+outputFile = "testOut.txt"\r
+\r
+newStates [] iut_o = []\r
+newStates [Pt o s:r] iut_o\r
+ | o === iut_o\r
+ = [s:newStates r iut_o]\r
+ = newStates r iut_o\r
+newStates [Ft f:r] iut_o = f iut_o ++ newStates r iut_o\r
+\r
+resetState ts\r
+ = {ts & curState = [ts.iniState]\r
+ , nPath = ts.nPath+1\r
+ , nStep = 0\r
+ , h_in = []\r
+ , h_out = []\r
+ , h_state = []\r
+ , mesFile = if ts.trace (ts.mesFile <<< "End of path reached: reset.\n") ts.mesFile\r
+ }\r
+\r
+errorFound ts=:{errFile,mesFile}\r
+ # errFile = errFile <<< "Issue Found!\n"\r
+ # mesFile = mesFile <<< "Issue Found!\n"\r
+ = {ts & errFile = errFile,mesFile=mesFile}\r
+\r
+restart testState = { testState & h_in = [], h_out = [], h_state = [] }\r
+*/\r
+handleOptions [] ts = ts\r
+handleOptions [o:r] ts=:{mesFile}\r
+ # ts = case o of\r
+ Ntests n = {ts & maxLen = n}\r
+ Nsequences n = {ts & maxPath = n}\r
+ Seed n = {ts & rnd = genRandInt n}\r
+ Randoms rnd = {ts & rnd = rnd }\r
+ FixedInputs ll_input = {ts & input = fixedInputs ll_input }\r
+ InputFun f = {ts & inputs = f }\r
+ // OutputFun f = {test & } //([s] i -> o)\r
+ FSM inp identify = {ts & input = fixedInputs (generateFSMpaths ts.iniState ts.spec inp identify) }\r
+ MkTrace b = { ts & trace = b }\r
+ OnPath n = { ts & nOnPath = n }\r
+ OnAndOffPath = { ts & input = onAndOff }\r
+ SwitchSpec spec = { ts & input = switchSpec spec }\r
+ OnTheFly = { ts & input = onTheFly }\r
+ ErrorFile f = { ts & fileName = f }\r
+ Stop pred = { ts & stop = pred }\r
+ = handleOptions r ts\r
+\r
+showError :: Int [a] [b] [c] !*File -> *File | genShow{|*|} a & genShow{|*|} b & genShow{|*|} c\r
+showError n [a:x] [b:y] [c:z] file = showError (n-1) x y z file <<< " " <<< n <<< ": " <<< show a <<< " " <<< show1 b <<< " -> " <<< show c <<< "\n"\r
+showError _ [] [] [] file = file\r
+showError _ _ _ _ file = file <<< "\n\n\tInternal error in \"showError\", please report to pieter@cs.ru.nl!\n\n"\r
+\r
+/*\r
+testConf :: Int (Spec s i o) (Spec t i o) s t ([s] -> Bool) [[i]] *d -> *d \r
+ | FileSystem d & gEq{|*|} s & gEq{|*|} o & genShow{|*|} s & genShow{|*|} t & genShow{|*|} i & genShow{|*|} o //& <<< o\r
+testConf max spec imp state stateIUT stop paths world\r
+ # (console,world) = stdio world\r
+ # (ok,file,world) = fopen outputFile FWriteText world\r
+ | not ok\r
+ = abort ("Cannot open output file "+++outputFile)\r
+ # (file,console) = test 0 0 0 1 paths file console\r
+ = snd (fclose console (snd (fclose file world)))\r
+where\r
+ outputFile = "testOut.txt"\r
+ test s t r n [] file console\r
+ = (file\r
+ ,console <<< "All (" <<< (n-r-1) <<< ") executed test paths successful (Proof), " <<< ", rejected " <<< r\r
+ <<< ", tests truncated " <<< t <<< ", in total " <<< s <<< " transitions.\n"\r
+ )\r
+ test s t r n l file console\r
+ | n > max\r
+ = (file\r
+ ,console <<< max <<< " test paths used, testing terminated, " <<< r <<< " rejected, " <<< t <<< " tests truncated, in total "\r
+ <<< (n-r-1) <<< " paths executed, " <<< s <<< " transitions.\n"\r
+ )\r
+ test s t r n [path:paths] file console\r
+ // | cbc spec [state] path\r
+ #!console = if ((n - r) bitand /*1023*/ /*31*/ 7 == 0)\r
+ (console <<< "paths: " <<< (n-1) <<< ", rejected: " <<< r <<< " paths executed: " <<< (n-r-1) <<< ", truncated: " <<< t <<< "...\r")\r
+ console\r
+ # iut = IUT imp stateIUT (genRandInt 195773)\r
+ #! (ok, skipped, steps, file) = conf 0 [state] iut path [] [] [] [] file\r
+ #! file = file\r
+ s = s+steps\r
+ | ok\r
+ | skipped = test s (t + 1) r (n + 1) paths file console\r
+ = test s t r (n + 1) paths file console\r
+ # console = console <<< "Issue found after " <<< n <<< " paths, " <<< (n-r) <<< " paths executed, " <<< t <<< " tests truncated, in total " <<< s <<< " transitions.\n" <<< "See \"" <<< outputFile <<< "\" for details about the issue.\n"\r
+ = (file,console)\r
+ // = test s t (r+1) (n+1) paths file\r
+ \r
+ conf s [] iut path out this sts ex file\r
+ #! file = file <<< "ERROR: output to last input was wrong!\n"\r
+ <<< "Expected outputs: " <<< show1 ex <<< "\n"\r
+ file = showError (length this) this out sts file\r
+ = (False, False, s, file)\r
+ conf s states iut path out this sts ex file\r
+ | stop states\r
+ = (True, True, s, file)\r
+ conf s states iut [] out this sts ex file = (True, False, s, file)\r
+ conf s states iut [i:path] out this sts ex file\r
+ # (iutout,iut) = apply i iut\r
+ specifiedResp = [ tup \\ s1 <- states, tup <- spec s1 i ]\r
+ = case specifiedResp of\r
+ [] = (True, True, s, file)\r
+ _ # states2 = mkset [ s2 \\ (s2,specout) <- specifiedResp | specout === iutout ]\r
+ = conf (s+1) states2 iut path [iutout:out] [i:this] [states:sts] (map snd specifiedResp) file\r
+\r
+ showError :: Int [a] [b] [s] !*File -> *File | genShow{|*|} a & genShow{|*|} b & genShow{|*|} s\r
+ showError n [a:x] [b:y] [s:z] file = showError (n-1) x y z file <<< " " <<< n <<< ": " <<< show s <<< " " <<< show1 a <<< " -> " <<< show b <<< "\n"\r
+ showError _ [] [] [] file = file\r
+ showError _ _ _ _ file = file <<< "\n\n\tInternal error in \"showError\", please report!\n\n"\r
+*/\r
+mkset [a:xs] = [a:[x\\x<-xs|not (x===a)]]\r
+mkset [] = []\r
+\r
+instance <<< [a] | <<< a\r
+where\r
+ (<<<) file [] = file\r
+ (<<<) file [a:x] = file <<< a <<< x\r
+\r
+derive genShow Trans\r
+\r
+// ----------------------------------------------\r
+\r
+:: Transition state input output :== (state,input,[output],state)\r
+\r
+:: LTS state input output // Labelled Transition System\r
+ = { trans :: [Transition state input output]\r
+ , initial :: state\r
+ // set of states and labels are not needed, this is determined by the type state.\r
+ }\r
+\r
+generateLTS :: (Spec s i o) s (s->[i]) -> LTS s i o | gEq{|*|} s\r
+generateLTS spec s i = generateLTSpred (\_=True) spec s i\r
+\r
+generateLTSpred :: (s->Bool) (Spec s i o) s (s->[i]) -> LTS s i o | gEq{|*|} s\r
+generateLTSpred p spec s inputs\r
+ = { trans = generateTrans [] [s] spec inputs\r
+ , initial = s\r
+ }\r
+where\r
+// generateTrans :: [s] [s] (Spec s i o) (s->[i]) -> [(s,i,[o],s)] | gEq{|*|} s\r
+ generateTrans seen [] spec inputs = []\r
+ generateTrans seen [s:todo] spec inputs\r
+ | not (isEmpty [f \\ i <- inputs s, Ft f <- spec s i ])\r
+ = abort "Cannot handle (Ft f) transitions in FSM"\r
+ # trans = [ (s,i,o,t) \\ i <- inputs s, Pt o t <- spec s i ]\r
+ seen = [ s:seen ]\r
+ new = [ t \\ (_,_,_,t) <- trans | isNew seen t && p t ]\r
+ = trans ++ generateTrans seen (removeDup (todo++new)) spec inputs\r
+// isNew :: [s] s -> Bool | gEq{|*|} s\r
+ isNew [] t = True\r
+ isNew [s:seen] t\r
+ | s===t\r
+ = False\r
+ = isNew seen t\r
+// removeDup :: !.[a] -> .[a] | gEq{|*|} a\r
+ removeDup [x:xs] = [x:removeDup (filter ((=!=) x) xs)]\r
+ removeDup _ = []\r
+\r
+A4 :: (LTS state input output) (state -> [input]) -> [[input]] | gEq{|*|} state\r
+A4 lts stateIdent = gen [([],lts.initial)] lts.trans []\r
+where\r
+ gen _ [] _ = []\r
+ gen [(input,state):tups] trans next\r
+ = step input trans state [] tups next False False\r
+ gen [] t [] = []\r
+ gen [] t l = gen (reverse l) t []\r
+ \r
+ step input [trans=:(s1, toki, toko,s2):r] state seentrans tups next ever now\r
+ | s1 === state\r
+ = step [toki:input] (revApp seentrans r) s2 [] tups [(input,state):next] True True\r
+ = step input r state [trans:seentrans] tups next ever now\r
+ step input [] state seentrans tups next ever now \r
+ | now = step input seentrans state [] tups next True False // input is extended\r
+ | ever = [revApp input (stateIdent state): gen tups seentrans next]\r
+ = gen tups seentrans next\r
+ \r
+ revApp [] acc = acc\r
+ revApp [a:x] acc = revApp x [a:acc]\r
+\r
+generateFSMpaths :: s (Spec s i o) [i] (s->[i]) -> [[i]] | gEq{|*|} s\r
+generateFSMpaths start spec inputs identify = A4 (generateLTS spec start (\_=inputs)) identify\r
+\r
+//----------------- the after operator from ioco theory -----------------//\r
+//----------------- yields the possible states after an input sequence --//\r
+\r
+(after) infix 0 :: [s] (Spec s i o) -> ([i] -> [s])\r
+(after) s spec // = apply s\r
+ = \i = case i of\r
+ [] = s\r
+ [i:r]\r
+ | not (isEmpty [f \\ u<-s, Ft f <- spec u i ])\r
+ = abort "Cannot handle (Ft f) transitions in (after)"\r
+ = ([t \\ u<-s, Pt o t <- spec u i] after spec) r\r
+/*where\r
+ apply [] i = []\r
+ apply s [] = s\r
+ apply s [i:r] = apply [t \\ u<-s, (t,o) <- spec u i] r\r
+*/\r
+//----------------- properties of specifications -----------------//\r
+\r
+propDeterministic :: (Spec s i o) s i -> Bool\r
+propDeterministic m s i = length (m s i) <= 1\r
+\r
+propTotal :: (Spec s i o) s i -> Bool\r
+propTotal m s i = not (isEmpty (m s i))\r