+++ /dev/null
-implementation module confSM\r
-\r
-/*\r
- GAST: A Generic Automatic Software Test-system\r
- \r
- ioco: Input Output COnformance of reactive systems\r
-\r
- Pieter Koopman, 2004, 2005\r
- Radboud Universty, Nijmegen\r
- The Netherlands\r
- pieter@cs.ru.nl\r
-*/\r
-\r
-import StdEnv, MersenneTwister, gen, GenEq, genLibTest, testable, StdLib\r
-\r
-toSpec :: (state input -> [(state,[output])]) -> Spec state input output // conversion for old specificaions\r
-toSpec fun = \s i = [Pt o t \\ (t,o) <- fun s i]\r
-\r
-SpectoIUTstep :: (Spec t i o) (t i -> [[o]]) -> IUTstep (t,RandomStream) i o | genShow{|*|} t & genShow{|*|} i & genShow{|*|} o\r
-SpectoIUTstep spec outputGen = selectTrans\r
-where\r
- selectTrans (t,[r,r2,r3:rnd]) i\r
- # tuples = spec t i\r
- len = lengthN 353 0 tuples\r
- | len == 0\r
- = abort ("\n\nIUT is not input enabled in state "+show1 t+" for input "+show1 i+"\n")\r
- = case tuples !! ((abs r) rem len) of\r
- Pt o t = (o,(t,rnd))\r
- Ft f # outputs = outputGen t i\r
- leno = lengthN 31 0 outputs\r
- | leno == 0\r
- = abort ("\n\nOutput function yields no output in state "+show1 t+" for input "+show1 i+"\n")\r
- # output = outputs !! ((abs r2) rem leno)\r
- states = f output\r
- lens = lengthN 37 0 states\r
- | lens == 0\r
- = abort ("\n\nIUT is not input enabled in state "+show1 t+" for input "+show1 i+" output "+show1 output+"\n")\r
- = (output,(states !! ((abs r3) rem lens),rnd))\r
- \r
- // =abort "toUIT"\r
-\r
-:: NewInput i = NewInput i | Reset | End\r
-\r
-:: *TestState s i o\r
- = !{ spec :: !Spec s i o\r
-// , specW :: !SpecWorld s i\r
- , iniState:: !s\r
- , curState:: ![s]\r
- , nRej :: !Int\r
- , nTrun :: !Int\r
- , nPath :: !Int\r
- , nStep :: !Int\r
- , nTotal :: !Int\r
- , maxPath :: !Int\r
- , maxLen :: !Int\r
- , nOnPath :: !Int\r
- , inputs :: (RandomStream s -> [i])\r
- , input :: !((TestState s i o) -> *(NewInput i, TestState s i o))\r
- , n :: !Int\r
- , rnd :: RandomStream\r
- , h_in :: [i]\r
- , h_out :: [[o]]\r
- , h_state :: [[s]]\r
- , fileName:: String\r
- , errFile :: !*File\r
- , mesFile :: !*File\r
- , trace :: !Bool\r
- , incons :: [o] [s] -> Maybe [String]\r
- , stop :: [s] -> Bool\r
- }\r
-/*\r
-apply :: i (IUT s i o) -> ([o],IUT s i o) | genShow{|*|} s & genShow{|*|} i\r
-apply i (IUT f s [r:rnd])\r
- = case f s i of\r
- [] = abort ("IUT is not input enabled! State: "+++show1 s+++", input: "+++show1 i)\r
- list\r
- # n = length list\r
- (t,o) = list !! ((abs r) rem n)\r
- = (o,IUT f t rnd)\r
-*/\r
- \r
-switchSpec :: (Spec s i o) (TestState s i o) -> *(NewInput i, TestState s i o) | ggen{|*|} i\r
-switchSpec spec ts=:{nOnPath} = newSpec spec nOnPath ts\r
-\r
-newSpec :: (Spec s i o) !Int (TestState s i o) -> *(NewInput i, TestState s i o) | ggen{|*|} i\r
-newSpec spec2 0 ts=:{spec} = oldSpec spec {ts & spec = spec2}\r
-newSpec spec2 n ts\r
- # (i,ts) = onTheFly ts\r
- = case i of\r
- Reset = (i,{ ts & input = newSpec spec2 ts.nOnPath })\r
- NewInput _ = (i,{ ts & input = newSpec spec2 (n-1)})\r
- _ = (i,ts)\r
-\r
-oldSpec :: (Spec s i o) (TestState s i o) -> *(NewInput i, TestState s i o) | ggen{|*|} i\r
-oldSpec spec2 ts\r
- # (i,ts) = onTheFly ts\r
- = case i of\r
- Reset = (i,{ ts & input = newSpec spec2 ts.nOnPath })\r
- _ = (i,ts)\r
-\r
-onAndOff :: (TestState s i o) -> *(NewInput i, TestState s i o) | ggen{|*|} i\r
-onAndOff ts=:{nOnPath} = onPath nOnPath ts\r
-\r
-onPath :: Int (TestState s i o) -> *(NewInput i, TestState s i o) | ggen{|*|} i\r
-onPath 0 ts=:{spec}\r
- # (rnd1,rnd2) = split ts.rnd\r
- = offPath spec (ggen{|*|} 2 rnd1) {ts & spec = mkComplete spec, rnd = rnd2} \r
-onPath n ts\r
- # (i,ts) = onTheFly ts\r
- = case i of\r
- Reset = (i,{ ts & input = onPath ts.nOnPath })\r
- NewInput _ = (i,{ ts & input = onPath (n-1)})\r
- _ = (i,ts)\r
-\r
-mkComplete spec s i\r
- = case spec s i of\r
- [] = [Pt [] s]\r
- r = r\r
-\r
-offPath :: (Spec s i o) [i] (TestState s i o) -> *(NewInput i, TestState s i o) | ggen{|*|} i\r
-offPath spec [] ts = (Reset,{ ts & input = onPath ts.nOnPath })\r
-offPath spec [i:r] ts\r
- | ts.nStep >= ts.maxLen-1 || ts.nRej >= ts.maxLen-1\r
- = (Reset,{ ts & input = onPath ts.nOnPath })\r
- = (NewInput i,{ts & input = offPath spec r})\r
-\r
-onTheFly :: (TestState s i o) -> *(NewInput i, TestState s i o)\r
-onTheFly ts=:{curState,inputs,rnd,spec}\r
- # [r1,r2:rnd] = rnd\r
- = case [ i \\ s <- randomize curState (genRandInt r1) 2 (\_=[])\r
- , i <- inputs (genRandInt r2) s\r
- | not (isEmpty (spec s i))\r
- ] of\r
- [] = (Reset, {ts & rnd=rnd})\r
- is # max = 157 // the maximum number of outputs to consider\r
- n = lengthN max 0 is // the number of the selected input\r
- [r:rnd] = rnd\r
- i = is !! ((abs r) rem n)\r
- = (NewInput i,{ts & rnd = rnd})\r
-\r
-lengthN :: !Int !Int ![a] -> Int\r
-lengthN m n [] = n\r
-lengthN m n [a:x]\r
- | n<m\r
- = lengthN m (n+1) x\r
- = m\r
-\r
-fixedInputs [] ts = (End, ts)\r
-fixedInputs [[] :r] ts = (Reset, { ts & input = fixedInputs r })\r
-fixedInputs [[a:x]:r] ts=:{curState,spec} \r
- | isEmpty [t \\ s<- curState, t<-spec s a]\r
- = (Reset, { ts & input = fixedInputs r , nTrun = ts.nTrun+1})\r
- = (NewInput a, {ts & input = fixedInputs [x:r]})\r
-\r
-genLongInput :: s Int (Spec s i o) [i] [Int] -> [i]\r
-genLongInput s 0 spec inputs [r:x] = randomize inputs x 7 (\_.[])\r
-genLongInput s n spec inputs [r,r2:x]\r
- = case [ i \\ i <- inputs | not (isEmpty (spec s i)) ] of\r
- [] = []\r
- l # i = l !! ((abs r) rem (length l))\r
- = case spec s i of\r
- [] = abort "\n\nError in genLongInput, please report.\n\n"\r
- list # len = length list\r
- s = case list !! ((abs r2) rem len) of\r
- Pt o s = s\r
- Ft f = abort "genLongInput Ft f"\r
- = [ i : genLongInput s (n-1) spec inputs x ] \r
-\r
-genLongInputs :: s (Spec s i o) [i] Int [Int] -> [[i]]\r
-genLongInputs s spec inputs n [r:x] = [genLongInput s n spec inputs (genRandInt r): genLongInputs s spec inputs n x]\r
-\r
-testConfSM :: [TestOption s i o] (Spec s i o) s (IUTstep .t i o) .t (.t->.t) *File *File -> (.t,*File,*File)\r
- | ggen{|*|} i & gEq{|*|} s & gEq{|*|} o & genShow{|*|} s & genShow{|*|} i & genShow{|*|} o\r
-testConfSM opts spec s0 iut t reset console file\r
- # ts=:{fileName} = initState file console\r
- # (t,ts) = doTest ts iut t reset\r
- {mesFile,errFile} = ts\r
- = (t, mesFile, errFile)\r
-where\r
- initState file console\r
- = handleOptions opts\r
- { spec = spec\r
- // , specW = \s i.[]\r
- , iniState= s0\r
- , curState= [s0]\r
- , nRej = 0\r
- , nTrun = 0\r
- , nPath = 0\r
- , nStep = 0\r
- , nTotal = 0\r
- , maxPath = 100\r
- , maxLen = 1000\r
- , nOnPath = 50\r
- , inputs = (\rnd s -> ggen {|*|} 2 rnd)\r
- , input = onTheFly \r
- , n = 0\r
- , h_in = []\r
- , h_out = []\r
- , h_state = []\r
- , rnd = aStream\r
- , errFile = file\r
- , fileName= outputFile\r
- , mesFile = console <<< "Gast starts testing.\n"\r
- , trace = False\r
- , incons = \o ss -> Nothing\r
- , stop = (\states = False)\r
- }\r
-\r
-findFileName [] name = name\r
-findFileName [ErrorFile s:r] name = findFileName r s\r
-findFileName [_:r] name = findFileName r name\r
-\r
-doTest :: (TestState s i o) (IUTstep .t i o) .t (.t->.t) -> (.t,TestState s i o)\r
- | gEq{|*|} s & gEq{|*|} o & genShow{|*|} s & genShow{|*|} i & genShow{|*|} o\r
-doTest ts=:{input,curState,spec,incons,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
- 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
repositories / tt2015.git / blobdiff