a3/code/Gast/confSM.icl

   1 implementation module confSM
   2
   3 /*
   4         GAST: A Generic Automatic Software Test-system
   5
   6         ioco: Input Output COnformance of reactive systems
   7
   8         Pieter Koopman, 2004, 2005
   9         Radboud Universty, Nijmegen
  10         The Netherlands
  11         pieter@cs.ru.nl
  12 */
  13
  14 import StdEnv, MersenneTwister, gen, GenEq, genLibTest, testable, StdLib
  15
  16 toSpec :: (state input -> [(state,[output])]) -> Spec state input output // conversion for old specificaions
  17 toSpec fun = \s i = [Pt o t \\ (t,o) <- fun s i]
  18
  19 SpectoIUTstep :: (Spec t i o) (t i -> [[o]]) -> IUTstep (t,RandomStream) i o | genShow{|*|} t & genShow{|*|} i & genShow{|*|} o
  20 SpectoIUTstep spec outputGen = selectTrans
  21 where
  22         selectTrans (t,[r,r2,r3:rnd]) i
  23                 # tuples = spec t i
  24                   len = lengthN 353 0 tuples
  25                 | len == 0
  26                         = abort ("\n\nIUT is not input enabled in state "+show1 t+" for input "+show1 i+"\n")
  27                         = case tuples !! ((abs r) rem len) of
  28                                 Pt o t = (o,(t,rnd))
  29                                 Ft f  # outputs = outputGen t i
  30                                                 leno = lengthN 31 0 outputs
  31                                           | leno == 0
  32                                                 = abort ("\n\nOutput function yields no output in state "+show1 t+" for input "+show1 i+"\n")
  33                                                 # output = outputs !! ((abs r2) rem leno)
  34                                                   states = f output
  35                                                   lens = lengthN 37 0 states
  36                                                 | lens == 0
  37                                                         = abort ("\n\nIUT is not input enabled in state "+show1 t+" for input "+show1 i+" output "+show1 output+"\n")
  38                                                         = (output,(states !! ((abs r3) rem lens),rnd))
  39
  40  // =abort "toUIT"
  41
  42 :: NewInput i = NewInput i | Reset | End
  43
  44 :: *TestState s i o
  45  =      !{      spec    :: !Spec s i o
  46 //      ,       specW   :: !SpecWorld s i
  47         ,       iniState:: !s
  48         ,       curState:: ![s]
  49         ,       nRej    :: !Int
  50         ,       nTrun   :: !Int
  51         ,       nPath   :: !Int
  52         ,       nStep   :: !Int
  53         ,       nTotal  :: !Int
  54         ,       maxPath :: !Int
  55         ,       maxLen  :: !Int
  56         ,       nOnPath :: !Int
  57         ,       inputs  :: (RandomStream s -> [i])
  58         ,       input   :: !((TestState s i o) -> *(NewInput i, TestState s i o))
  59         ,       n               :: !Int
  60         ,       rnd             :: RandomStream
  61         ,       h_in    :: [i]
  62         ,       h_out   :: [[o]]
  63         ,       h_state :: [[s]]
  64         ,       fileName:: String
  65         ,       errFile :: !*File
  66         ,       mesFile :: !*File
  67         ,       trace   :: !Bool
  68         ,       incons  :: [o] [s] -> Maybe [String]
  69         ,       stop    :: [s] -> Bool
  70         }
  71 /*
  72 apply :: i (IUT s i o) -> ([o],IUT s i o) | genShow{|*|} s & genShow{|*|} i
  73 apply i (IUT f s [r:rnd])
  74         = case f s i of
  75                 []              = abort ("IUT is not input enabled! State: "+++show1 s+++", input: "+++show1 i)
  76                 list
  77                         # n             = length list
  78                           (t,o) = list !! ((abs r) rem n)
  79                         = (o,IUT f t rnd)
  80 */
  81
  82 switchSpec :: (Spec s i o) (TestState s i o) -> *(NewInput i, TestState s i o) | ggen{|*|} i
  83 switchSpec spec ts=:{nOnPath} = newSpec spec nOnPath ts
  84
  85 newSpec :: (Spec s i o) !Int (TestState s i o) -> *(NewInput i, TestState s i o) | ggen{|*|} i
  86 newSpec spec2 0 ts=:{spec} = oldSpec spec {ts & spec = spec2}
  87 newSpec spec2 n ts
  88  # (i,ts) = onTheFly ts
  89  = case i of
  90         Reset   = (i,{ ts & input = newSpec spec2 ts.nOnPath })
  91         NewInput _      = (i,{ ts & input = newSpec spec2 (n-1)})
  92         _               = (i,ts)
  93
  94 oldSpec :: (Spec s i o) (TestState s i o) -> *(NewInput i, TestState s i o) | ggen{|*|} i
  95 oldSpec spec2 ts
  96  # (i,ts) = onTheFly ts
  97  = case i of
  98         Reset   = (i,{ ts & input = newSpec spec2 ts.nOnPath })
  99         _               = (i,ts)
 100
 101 onAndOff :: (TestState s i o) -> *(NewInput i, TestState s i o) | ggen{|*|} i
 102 onAndOff ts=:{nOnPath} = onPath nOnPath ts
 103
 104 onPath :: Int (TestState s i o) -> *(NewInput i, TestState s i o) | ggen{|*|} i
 105 onPath 0 ts=:{spec}
 106  # (rnd1,rnd2) = split ts.rnd
 107  = offPath spec (ggen{|*|} 2 rnd1) {ts & spec = mkComplete spec, rnd = rnd2}
 108 onPath n ts
 109  # (i,ts) = onTheFly ts
 110  = case i of
 111         Reset   = (i,{ ts & input = onPath ts.nOnPath })
 112         NewInput _      = (i,{ ts & input = onPath (n-1)})
 113         _               = (i,ts)
 114
 115 mkComplete spec s i
 116         = case spec s i of
 117                 [] = [Pt [] s]
 118                 r  = r
 119
 120 offPath :: (Spec s i o) [i] (TestState s i o) -> *(NewInput i, TestState s i o) | ggen{|*|} i
 121 offPath spec [] ts = (Reset,{ ts & input = onPath ts.nOnPath })
 122 offPath spec [i:r] ts
 123   | ts.nStep >= ts.maxLen-1 || ts.nRej >= ts.maxLen-1
 124         = (Reset,{ ts & input = onPath ts.nOnPath })
 125         = (NewInput i,{ts & input = offPath spec r})
 126
 127 onTheFly :: (TestState s i o) -> *(NewInput i, TestState s i o)
 128 onTheFly ts=:{curState,inputs,rnd,spec}
 129         # [r1,r2:rnd] = rnd
 130         = case [ i      \\ s <- randomize curState (genRandInt r1) 2 (\_=[])
 131                                 ,  i <- inputs (genRandInt r2) s
 132                                 | not (isEmpty (spec s i))
 133                         ] of
 134                 []      = (Reset, {ts & rnd=rnd})
 135                 is      # max = 157                             // the maximum number of outputs to consider
 136                           n = lengthN max 0 is  // the number of the selected input
 137                           [r:rnd] = rnd
 138                           i = is !! ((abs r) rem n)
 139                         = (NewInput i,{ts & rnd = rnd})
 140
 141 lengthN :: !Int !Int ![a] -> Int
 142 lengthN m n [] = n
 143 lengthN m n [a:x]
 144         | n<m
 145                 = lengthN m (n+1) x
 146                 = m
 147
 148 fixedInputs []        ts = (End, ts)
 149 fixedInputs [[]   :r] ts = (Reset, { ts & input = fixedInputs r })
 150 fixedInputs [[a:x]:r] ts=:{curState,spec}
 151         | isEmpty [t \\ s<- curState, t<-spec s a]
 152                 = (Reset, { ts & input = fixedInputs r , nTrun = ts.nTrun+1})
 153                 = (NewInput a, {ts & input = fixedInputs [x:r]})
 154
 155 genLongInput :: s Int (Spec s i o) [i] [Int] -> [i]
 156 genLongInput s 0 spec inputs [r:x] = randomize inputs x 7 (\_.[])
 157 genLongInput s n spec inputs [r,r2:x]
 158         = case [ i \\ i <- inputs | not (isEmpty (spec s i)) ] of
 159                 []      = []
 160                 l       # i = l !! ((abs r) rem (length l))
 161                         = case spec s i of
 162                                 []              = abort "\n\nError in genLongInput, please report.\n\n"
 163                                 list    # len           = length list
 164                                                   s     = case list !! ((abs r2) rem len) of
 165                                                                 Pt o s = s
 166                                                                 Ft f = abort "genLongInput Ft f"
 167                                                 = [ i : genLongInput s (n-1) spec inputs x ]
 168
 169 genLongInputs :: s (Spec s i o) [i] Int [Int] -> [[i]]
 170 genLongInputs s spec inputs n [r:x] = [genLongInput s n spec inputs (genRandInt r): genLongInputs s spec inputs n x]
 171
 172 testConfSM :: [TestOption s i o] (Spec s i o) s (IUTstep .t i o) .t (.t->.t) *File *File -> (.t,*File,*File)
 173                         | ggen{|*|} i & gEq{|*|} s & gEq{|*|} o & genShow{|*|} s & genShow{|*|} i & genShow{|*|} o
 174 testConfSM opts spec s0 iut t reset console file
 175         # ts=:{fileName}                = initState file console
 176         # (t,ts)        = doTest ts iut t reset
 177           {mesFile,errFile} = ts
 178         = (t, mesFile, errFile)
 179 where
 180         initState file console
 181          =      handleOptions opts
 182                 {       spec    = spec
 183         //      ,       specW   = \s i.[]
 184                 ,       iniState= s0
 185                 ,       curState= [s0]
 186                 ,       nRej    = 0
 187                 ,       nTrun   = 0
 188                 ,       nPath   = 0
 189                 ,       nStep   = 0
 190                 ,       nTotal  = 0
 191                 ,       maxPath = 100
 192                 ,       maxLen  = 1000
 193                 ,       nOnPath = 50
 194                 ,       inputs  = (\rnd s -> ggen {|*|} 2 rnd)
 195                 ,       input   = onTheFly
 196                 ,       n               = 0
 197                 ,       h_in    = []
 198                 ,       h_out   = []
 199                 ,       h_state = []
 200                 ,       rnd             = aStream
 201                 ,       errFile = file
 202                 ,       fileName= outputFile
 203                 ,       mesFile = console <<< "Gast starts testing.\n"
 204                 ,       trace   = False
 205                 ,       incons  = \o ss -> Nothing
 206                 ,       stop    = (\states = False)
 207                 }
 208
 209 findFileName [] name = name
 210 findFileName [ErrorFile s:r] name = findFileName r s
 211 findFileName [_:r] name = findFileName r name
 212
 213 doTest :: (TestState s i o) (IUTstep .t i o) .t (.t->.t) -> (.t,TestState s i o)
 214                 | gEq{|*|} s & gEq{|*|} o & genShow{|*|} s & genShow{|*|} i & genShow{|*|} o
 215 doTest ts=:{input,curState,spec,incons} step t reset
 216   | isEmpty ts.curState
 217         = (t, errorFound ts)
 218   | ts.nStep >= ts.maxLen || ts.nRej >= ts.maxLen
 219         = doTest (resetState ts) step (reset t) reset
 220   | ts.nPath >= ts.maxPath
 221         | ts.nRej == 0 && ts.nTrun == 0
 222           = (t,{ts & mesFile = ts.mesFile       <<< "\nEnd of testing, maximum paths used. \n"
 223                                                                                 <<< ts.nPath
 224                                                                                 <<< " test paths executed successful, in total "
 225                                                                                 <<< ts.nTotal <<< " transitions.\n"})
 226           = (t,{ts & mesFile = ts.mesFile       <<< "\nEnd of testing, maximum paths used. \n"
 227                                                                                 <<< ts.nPath
 228                                                                                 <<< " test paths executed successful, "
 229                                                                                 <<< ts.nTrun <<< " paths truncated, "
 230                                                                                 <<< " in total "
 231                                                                                 <<< ts.nTotal <<< " transitions.\n"})
 232   #     (inp,ts) = input ts
 233   =     case inp of
 234           Reset = doTest (resetState ts) step (reset t) reset
 235           End   | ts.nRej == 0 && ts.nTrun == 0
 236                           = (t,{ts & mesFile = ts.mesFile       <<< "\nAll input paths tested successfully.\n"
 237                                                                                                 <<< "All " <<< ts.nPath
 238                                                                                                 <<< " executed test paths successful (Proof), in total "
 239                                                                                                 <<< ts.nTotal <<< " transitions.\n"})
 240                           = (t,{ts & mesFile = ts.mesFile       <<< "\nAll inputs tested successfully.\n"
 241                                                                                                 <<< (ts.nPath-ts.nRej)
 242                                                                                                 <<< "test path executed successful (Proof), " <<< ts.nRej
 243                                                                                                 <<< " paths rejected " <<< ts.nTrun
 244                                                                                                 <<< " paths truncated, "
 245                                                                                                 <<< "in total " <<< ts.nTotal <<< " transitions.\n"})
 246           NewInput i    // assumption: only inputs allowed by spec will be generated:
 247                 #!      (iut_o,t) = step t i
 248                         tuples = [tup \\ s<-curState, tup<-spec s i]
 249                         states = mkset (newStates tuples iut_o)
 250                 | isEmpty states
 251                         #! errFile = ts.errFile <<< "Issue found! Trace:\n"
 252                                                                         <<< "SpecificationStates Input -> ObservedOutput\n"
 253                            errFile = showError (ts.nStep+1) [curState:ts.h_state] [i:ts.h_in] [iut_o:ts.h_out] errFile
 254                            errFile = errorInfo ts.nPath ts.nRej ts.nTrun (ts.nTotal+1) (errFile <<< "\n")
 255                            mesFile = errorInfo ts.nPath ts.nRej ts.nTrun (ts.nTotal+1) ts.mesFile
 256                            mesFile = mesFile <<< "See file \"" <<< ts.fileName <<< "\" for details about the issue.\n"
 257                         = (t,{ts        & mesFile = mesFile
 258                                                 , errFile = errFile
 259                                                 , curState = []
 260                                                 })
 261                         = case incons iut_o states of
 262                                 Nothing
 263                                    # mesFile = ts.mesFile <<< "paths: " <<< ts.nPath <<< ", rejected: " <<< ts.nRej <<< ", truncated: " <<< ts.nTrun <<< "...\r"
 264                                    = doTest {ts & curState = states
 265                                                                 , nStep = ts.nStep+1
 266                                                                 , nTotal =ts.nTotal+1
 267                                                                 , h_in = [i:ts.h_in]
 268                                                                 , h_out = [iut_o:ts.h_out]
 269                                                                 , h_state = [curState:ts.h_state]
 270                                                                 , mesFile = if ts.trace (mesFile <<< ts.nPath <<< "," <<< ts.nStep <<< ": " <<< show1 ts.curState <<< " " <<< show1 i <<< " " <<< show1 iut_o <<< "\n") mesFile
 271                                                                 }
 272                                                         step t reset
 273                                 Just errors
 274                                         #! errFile = ts.errFile <<< "Inconsistency! Trace:\n"
 275                                                                                         <<< "SpecificationStates Input -> ObservedOutput\n"
 276                                            errFile = showError (ts.nStep+1) [curState:ts.h_state] [i:ts.h_in] [iut_o:ts.h_out] errFile
 277                                            errFile = errFile <<< "Inconsistency info:\n" <<< errors <<< "\n"
 278                                            errFile = errorInfo ts.nPath ts.nRej ts.nTrun (ts.nTotal+1) (errFile <<< "\n")
 279                                            mesFile = ts.mesFile <<< "Inconsistency found!\n" <<< errors <<< "\n\n"
 280                                            mesFile = errorInfo ts.nPath ts.nRej ts.nTrun (ts.nTotal+1) mesFile
 281                                            mesFile = mesFile <<< "See file \"" <<< ts.fileName <<< "\" for details.\n"
 282                                         = (t,{ts        & mesFile = mesFile
 283                                                                 , errFile = errFile
 284                                                                 , curState = []
 285                                                                 })
 286 where
 287         errorInfo :: !Int !Int !Int !Int *File -> *File
 288         errorInfo nPath nRej nTrun nTotal file
 289          = file <<< "Issue found in path " <<< (nPath+1) <<< ", "
 290                         <<< (nPath-nRej) <<< " paths executed, "
 291                         <<< nTrun <<< " tests truncated, in total "
 292                         <<< nTotal <<< " transitions.\n"
 293
 294 outputFile = "testOut.txt"
 295
 296 newStates [] iut_o = []
 297 newStates [Pt o s:r] iut_o
 298         | o === iut_o
 299                 = [s:newStates r iut_o]
 300                 = newStates r iut_o
 301 newStates [Ft f:r] iut_o = f iut_o ++ newStates r iut_o
 302
 303 resetState ts
 304   =     {ts     & curState = [ts.iniState]
 305                 , nPath    = ts.nPath+1
 306                 , nStep    = 0
 307                 , h_in     = []
 308                 , h_out    = []
 309                 , h_state  = []
 310                 , mesFile  = if ts.trace (ts.mesFile <<< "End of path reached: reset.\n") ts.mesFile
 311         }
 312
 313 errorFound ts=:{errFile,mesFile}
 314  # errFile = errFile <<< "Issue Found!\n"
 315  # mesFile = mesFile <<< "Issue Found!\n"
 316  = {ts & errFile = errFile,mesFile=mesFile}
 317
 318 restart testState = { testState & h_in = [], h_out = [], h_state = [] }
 319  /*
 320 testConfSM :: [TestOption s i o] (Spec s i o) s (IUTstep .t i o) .t (.t->.t) *d -> (.t,*d)
 321                         | FileSystem d & ggen{|*|} i & gEq{|*|} s & gEq{|*|} o & genShow{|*|} s & genShow{|*|} i & genShow{|*|} o
 322 testConfSM opts spec s0 iut t reset world
 323         # (console,world) = stdio world
 324           filename                = findFileName opts outputFile
 325         # (ok,file,world) = fopen filename FWriteText world
 326         | not ok
 327                 # console = console <<< "Cannot open output file "<<< filename
 328                 = (t, snd (fclose console world))
 329         # //console     = console <<< ".\n"
 330           ts=:{fileName}                = initState file console
 331         # (t,ts)        = doTest ts iut t reset
 332           {mesFile,errFile} = ts
 333         = (t, snd (fclose mesFile (snd (fclose errFile world))))
 334 where
 335         initState file console
 336          =      handleOptions opts
 337                 {       spec    = spec
 338                 ,       iniState= s0
 339                 ,       curState= [s0]
 340                 ,       nRej    = 0
 341                 ,       nTrun   = 0
 342                 ,       nPath   = 0
 343                 ,       nStep   = 0
 344                 ,       nTotal  = 0
 345                 ,       maxPath = 100
 346                 ,       maxLen  = 1000
 347                 ,       nOnPath = 50
 348                 ,       inputs  = (\rnd s -> ggen {|*|} 2 rnd)
 349                 ,       input   = onTheFly
 350                 ,       n               = 0
 351                 ,       h_in    = []
 352                 ,       h_out   = []
 353                 ,       h_state = []
 354                 ,       rnd             = aStream
 355                 ,       errFile = file
 356                 ,       fileName= outputFile
 357                 ,       mesFile = console <<< "Gast starts testing.\n"
 358                 ,       trace   = False
 359                 ,       incons  = \o ss -> Nothing
 360                 ,       stop    = (\states = False)
 361                 }
 362
 363 findFileName [] name = name
 364 findFileName [ErrorFile s:r] name = findFileName r s
 365 findFileName [_:r] name = findFileName r name
 366
 367 doTest :: (TestState s i o) (IUTstep .t i o) .t (.t->.t) -> (.t,TestState s i o)
 368                 | gEq{|*|} s & gEq{|*|} o & genShow{|*|} s & genShow{|*|} i & genShow{|*|} o
 369 doTest ts=:{input,curState,spec,stop} step t reset
 370   | isEmpty ts.curState
 371         = (t, errorFound ts)
 372   | ts.nStep >= ts.maxLen || ts.nRej >= ts.maxLen || stop curState
 373         = doTest (resetState ts) step (reset t) reset
 374   | ts.nPath >= ts.maxPath
 375         | ts.nRej == 0 && ts.nTrun == 0
 376           = (t,{ts & mesFile = ts.mesFile       <<< "\nEnd of testing, maximum paths used. \n"
 377                                                                                 <<< ts.nPath
 378                                                                                 <<< " test paths executed successful, in total "
 379                                                                                 <<< ts.nTotal <<< " transitions.\n"})
 380           = (t,{ts & mesFile = ts.mesFile       <<< "\nEnd of testing, maximum paths used. \n"
 381                                                                                 <<< ts.nPath
 382                                                                                 <<< " test paths executed successful, "
 383                                                                                 <<< ts.nTrun <<< " paths truncated, "
 384                                                                                 <<< " in total "
 385                                                                                 <<< ts.nTotal <<< " transitions.\n"})
 386   #     (inp,ts) = input ts
 387   =     case inp of
 388           Reset = doTest (resetState ts) step (reset t) reset
 389           End   | ts.nRej == 0 && ts.nTrun == 0
 390                           = (t,{ts & mesFile = ts.mesFile       <<< "\nAll input paths tested successfully.\n"
 391                                                                                                 <<< "All " <<< ts.nPath
 392                                                                                                 <<< " executed test paths successful (Proof), in total "
 393                                                                                                 <<< ts.nTotal <<< " transitions.\n"})
 394                           = (t,{ts & mesFile = ts.mesFile       <<< "\nAll inputs tested successfully.\n"
 395                                                                                                 <<< (ts.nPath-ts.nRej)
 396                                                                                                 <<< "test path executed successful (Proof), " <<< ts.nRej
 397                                                                                                 <<< " paths rejected " <<< ts.nTrun
 398                                                                                                 <<< " paths truncated, "
 399                                                                                                 <<< "in total " <<< ts.nTotal <<< " transitions.\n"})
 400 //        Input i       // assumption: only inputs allowed by spec will be generated:
 401           NewInput i    // assumption: only inputs allowed by spec will be generated:
 402                 #!      (iut_o,t) = step t i
 403                         tuples = [tup \\ s<-curState, tup<-spec s i]
 404                 = case mkset (newStates tuples iut_o) of
 405                         []      #! errFile = ts.errFile <<< "Issue found! Trace:\n"
 406                                                                                 <<< "SpecificationStates Input -> ObservedOutput\n"
 407                                    errFile = showError (ts.nStep+1) [curState:ts.h_state] [i:ts.h_in] [iut_o:ts.h_out] errFile
 408                                    errFile = errFile <<< "\nAllowed outputs and target states: " <<< show tuples <<< "\n"
 409                                    errFile = errorInfo ts.nPath ts.nRej ts.nTrun (ts.nTotal+1) (errFile <<< "\n")
 410                                    mesFile = errorInfo ts.nPath ts.nRej ts.nTrun (ts.nTotal+1) ts.mesFile
 411                                    mesFile = mesFile <<< "See file \"" <<< ts.fileName <<< "\" for details about the issue.\n"
 412
 413                                 = (t,{ts        & mesFile = mesFile
 414                                                         , errFile = errFile
 415                                                         , curState = []
 416                                                         })
 417                         states #! mesFile = ts.mesFile <<< "paths: " <<< ts.nPath <<< ", rejected: " <<< ts.nRej <<< ", truncated: " <<< ts.nTrun <<< "...\r"
 418                                    = doTest {ts & curState = states
 419                                                                 , nStep = ts.nStep+1
 420                                                                 , nTotal =ts.nTotal+1
 421                                                                 , h_in = [i:ts.h_in]
 422                                                                 , h_out = [iut_o:ts.h_out]
 423                                                                 , h_state = [curState:ts.h_state]
 424                                                                 , mesFile = if ts.trace (mesFile <<< ts.nPath <<< "," <<< ts.nStep <<< ": " <<< show1 ts.curState <<< " " <<< show1 i <<< " " <<< show1 iut_o <<< "\n") mesFile
 425                                                                 }
 426                                                         step t reset
 427                 where
 428                         errorInfo :: !Int !Int !Int !Int *File -> *File
 429                         errorInfo nPath nRej nTrun nTotal file
 430                          = file <<< "Issue found in path " <<< (nPath+1) <<< ", "
 431                                         <<< (nPath-nRej) <<< " paths executed to bound or end, "
 432                                         <<< nTrun <<< " paths truncated, in total "
 433                                         <<< nTotal <<< " transitions.\n"
 434
 435         //  = (t,{ts & mesFile = ts.mesFile <<< "\nAll inputs tested successfully\n"})
 436
 437 outputFile = "testOut.txt"
 438
 439 newStates [] iut_o = []
 440 newStates [Pt o s:r] iut_o
 441         | o === iut_o
 442                 = [s:newStates r iut_o]
 443                 = newStates r iut_o
 444 newStates [Ft f:r] iut_o = f iut_o ++ newStates r iut_o
 445
 446 resetState ts
 447   =     {ts     & curState = [ts.iniState]
 448                 , nPath    = ts.nPath+1
 449                 , nStep    = 0
 450                 , h_in     = []
 451                 , h_out    = []
 452                 , h_state  = []
 453                 , mesFile  = if ts.trace (ts.mesFile <<< "End of path reached: reset.\n") ts.mesFile
 454         }
 455
 456 errorFound ts=:{errFile,mesFile}
 457  # errFile = errFile <<< "Issue Found!\n"
 458  # mesFile = mesFile <<< "Issue Found!\n"
 459  = {ts & errFile = errFile,mesFile=mesFile}
 460
 461 restart testState = { testState & h_in = [], h_out = [], h_state = [] }
 462 */
 463 handleOptions [] ts = ts
 464 handleOptions [o:r] ts=:{mesFile}
 465         # ts = case o of
 466                                 Ntests n = {ts & maxLen = n}
 467                                 Nsequences n = {ts & maxPath = n}
 468                                 Seed n = {ts & rnd = genRandInt n}
 469                                 Randoms rnd = {ts & rnd = rnd }
 470                                 FixedInputs ll_input = {ts & input = fixedInputs ll_input }
 471                                 InputFun f = {ts & inputs = f }
 472                         //      OutputFun f = {test & } //([s] i -> o)
 473                                 FSM inp identify = {ts & input = fixedInputs (generateFSMpaths ts.iniState ts.spec inp identify) }
 474                                 MkTrace b = { ts & trace = b }
 475                                 OnPath n = { ts & nOnPath = n }
 476                                 OnAndOffPath = { ts & input = onAndOff }
 477                                 SwitchSpec spec = { ts & input = switchSpec spec }
 478                                 OnTheFly = { ts & input = onTheFly }
 479                                 ErrorFile f = { ts & fileName = f }
 480                                 Stop pred = { ts & stop = pred }
 481         = handleOptions r ts
 482
 483 showError :: Int [a] [b] [c] !*File -> *File | genShow{|*|} a & genShow{|*|} b & genShow{|*|} c
 484 showError n [a:x] [b:y] [c:z] file = showError (n-1) x y z file <<< "    " <<< n <<< ": " <<< show a <<< " " <<< show1 b <<< " -> " <<< show c <<< "\n"
 485 showError _ []    []    []    file = file
 486 showError _ _     _     _     file = file <<< "\n\n\tInternal error in \"showError\", please report to pieter@cs.ru.nl!\n\n"
 487
 488 /*
 489 testConf :: Int (Spec s i o) (Spec t i o) s t ([s] -> Bool) [[i]] *d -> *d
 490                         | FileSystem d & gEq{|*|} s & gEq{|*|} o & genShow{|*|} s & genShow{|*|} t & genShow{|*|} i & genShow{|*|} o //& <<< o
 491 testConf max spec imp state stateIUT stop paths world
 492         # (console,world) = stdio world
 493         # (ok,file,world) = fopen outputFile FWriteText world
 494         | not ok
 495                 = abort ("Cannot open output file "+++outputFile)
 496         # (file,console) = test 0 0 0 1 paths file console
 497         = snd (fclose console (snd (fclose file world)))
 498 where
 499         outputFile = "testOut.txt"
 500         test s t r n [] file console
 501                 = (file
 502                   ,console      <<< "All (" <<< (n-r-1) <<< ") executed test paths successful (Proof), " <<< ", rejected " <<< r
 503                                         <<< ", tests truncated " <<< t <<< ", in total " <<< s <<< " transitions.\n"
 504                   )
 505         test s t r n l  file console
 506                 | n > max
 507                         = (file
 508                           ,console      <<< max <<< " test paths used, testing terminated, " <<< r <<< " rejected, " <<< t <<< " tests truncated, in total "
 509                                                 <<< (n-r-1) <<< " paths executed, " <<< s <<< " transitions.\n"
 510                           )
 511         test s t r n [path:paths] file console
 512         //      | cbc spec [state] path
 513                         #!console = if ((n - r) bitand /*1023*/ /*31*/ 7 == 0)
 514                                                         (console <<< "paths: " <<< (n-1) <<< ", rejected: " <<< r <<< " paths executed: " <<< (n-r-1) <<<  ", truncated: " <<< t <<< "...\r")
 515                                                         console
 516                         # iut = IUT imp stateIUT (genRandInt 195773)
 517                         #! (ok, skipped, steps, file) = conf 0 [state] iut path [] [] [] [] file
 518                         #! file = file
 519                            s = s+steps
 520                         | ok
 521                                 | skipped       = test s (t + 1) r (n + 1) paths file console
 522                                                         = test s t r (n + 1) paths file console
 523                                 # 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"
 524                                 = (file,console)
 525         //              = test s t (r+1) (n+1) paths file
 526
 527         conf s [] iut path out this sts ex file
 528                 #! file = file  <<< "ERROR: output to last input was wrong!\n"
 529                                                 <<< "Expected outputs: " <<< show1 ex <<< "\n"
 530                    file = showError (length this) this out sts file
 531                 = (False, False, s, file)
 532         conf s states iut path out this sts ex file
 533                 | stop states
 534                         = (True, True, s, file)
 535         conf s states iut [] out this sts ex file = (True, False, s, file)
 536         conf s states iut [i:path] out this sts ex file
 537           #     (iutout,iut) = apply i iut
 538                 specifiedResp   = [ tup \\ s1 <- states, tup <- spec s1 i ]
 539           = case specifiedResp of
 540                         []      = (True, True, s, file)
 541                         _       # states2 = mkset [ s2 \\ (s2,specout) <- specifiedResp | specout === iutout ]
 542                                 = conf (s+1) states2 iut path [iutout:out] [i:this] [states:sts] (map snd specifiedResp) file
 543
 544         showError :: Int [a] [b] [s] !*File -> *File | genShow{|*|} a & genShow{|*|} b & genShow{|*|} s
 545         showError n [a:x] [b:y] [s:z] file = showError (n-1) x y z file <<< "    " <<< n <<< ": " <<< show s <<< " " <<< show1 a <<< " -> " <<< show b <<< "\n"
 546         showError _ []    []    []    file = file
 547         showError _ _     _     _     file = file <<< "\n\n\tInternal error in \"showError\", please report!\n\n"
 548 */
 549 mkset [a:xs] = [a:[x\\x<-xs|not (x===a)]]
 550 mkset []     = []
 551
 552 instance <<< [a] | <<< a
 553 where
 554         (<<<) file []    = file
 555         (<<<) file [a:x] = file <<< a <<< x
 556
 557 derive genShow Trans
 558
 559 // ----------------------------------------------
 560
 561 :: Transition state input output :== (state,input,[output],state)
 562
 563 :: LTS state input output // Labelled Transition System
 564         =       { trans         :: [Transition state input output]
 565                 , initial       :: state
 566                 // set of states and labels are not needed, this is determined by the type state.
 567                 }
 568
 569 generateLTS :: (Spec s i o) s (s->[i]) -> LTS s i o | gEq{|*|} s
 570 generateLTS spec s i = generateLTSpred (\_=True) spec s i
 571
 572 generateLTSpred :: (s->Bool) (Spec s i o) s (s->[i]) -> LTS s i o | gEq{|*|} s
 573 generateLTSpred p spec s inputs
 574  =      { trans         = generateTrans [] [s] spec inputs
 575         , initial       = s
 576         }
 577 where
 578 //      generateTrans :: [s] [s] (Spec s i o) (s->[i]) -> [(s,i,[o],s)] | gEq{|*|} s
 579         generateTrans seen [] spec inputs = []
 580         generateTrans seen [s:todo] spec inputs
 581                 | not (isEmpty [f \\ i <- inputs s, Ft f <- spec s i ])
 582                         = abort "Cannot handle (Ft f) transitions in FSM"
 583                 # trans = [ (s,i,o,t) \\ i <- inputs s, Pt o t <- spec s i ]
 584                   seen  = [ s:seen ]
 585                   new   = [ t \\ (_,_,_,t) <- trans | isNew seen t && p t ]
 586                 = trans ++ generateTrans seen (removeDup (todo++new)) spec inputs
 587 //      isNew :: [s] s -> Bool | gEq{|*|} s
 588         isNew [] t = True
 589         isNew [s:seen] t
 590                 | s===t
 591                         = False
 592                         = isNew seen t
 593 //      removeDup :: !.[a] -> .[a] | gEq{|*|} a
 594         removeDup [x:xs] = [x:removeDup (filter ((=!=) x) xs)]
 595         removeDup _      = []
 596
 597 A4 :: (LTS state input output) (state -> [input]) -> [[input]] | gEq{|*|} state
 598 A4 lts stateIdent = gen [([],lts.initial)] lts.trans []
 599 where
 600         gen _ [] _ = []
 601         gen [(input,state):tups] trans next
 602                 = step input trans state [] tups next False False
 603         gen [] t [] = []
 604         gen [] t l  = gen (reverse l) t []
 605
 606         step input [trans=:(s1, toki, toko,s2):r] state seentrans tups next ever now
 607                 | s1 === state
 608                         = step [toki:input] (revApp seentrans r) s2 [] tups [(input,state):next] True True
 609                         = step input r state [trans:seentrans] tups next ever now
 610         step input [] state seentrans tups next ever now
 611                 | now   = step input seentrans state [] tups next True False // input is extended
 612                 | ever  = [revApp input (stateIdent state): gen tups seentrans next]
 613                                 = gen tups seentrans next
 614
 615         revApp [] acc = acc
 616         revApp [a:x] acc = revApp x [a:acc]
 617
 618 generateFSMpaths :: s (Spec s i o) [i] (s->[i]) -> [[i]] | gEq{|*|} s
 619 generateFSMpaths start spec inputs identify = A4 (generateLTS spec start (\_=inputs)) identify
 620
 621 //----------------- the after operator from ioco theory -----------------//
 622 //----------------- yields the possible states after an input sequence --//
 623
 624 (after) infix 0 :: [s] (Spec s i o) -> ([i] -> [s])
 625 (after) s spec // = apply s
 626   = \i = case i of
 627                         []    = s
 628                         [i:r]
 629                                 | not (isEmpty [f \\ u<-s, Ft f <- spec u i ])
 630                                         = abort "Cannot handle (Ft f) transitions in (after)"
 631                                         = ([t \\ u<-s, Pt o t <- spec u i] after spec) r
 632 /*where
 633         apply [] i = []
 634         apply s [] = s
 635         apply s [i:r] = apply [t \\ u<-s, (t,o) <- spec u i] r
 636 */
 637 //----------------- properties of specifications -----------------//
 638
 639 propDeterministic :: (Spec s i o) s i -> Bool
 640 propDeterministic m s i = length (m s i) <= 1
 641
 642 propTotal :: (Spec s i o) s i -> Bool
 643 propTotal m s i = not (isEmpty (m s i))