with esmViz

libraries/Gast/ESMSpec.dcl

+definition module ESMSpec
+
+import StdClass, StdMaybe
+import gast //gen
+
+::	Traces		   s i o :== [[SeenTrans s i o]]
+::	ESM            s i o =   { s_0 :: s					// the initial state
+							 , d_F :: Spec s i o		// the state transition function (\delta_F)
+							 , out :: s i -> [[o]]		// outputs to be used if spec does not give them
+							 , pred:: (SeenTrans s i o)->[[String]] // consitency issues
+							 }
+::	KnownAutomaton s i o =   {trans :: [SeenTrans s i o]
+							 ,issues:: [(SeenTrans s i o,[String])]
+							 }
+::	SeenTrans      s i o :== (s,i,[o],s)
+
+tupToSpec :: (state input -> [([output],state)]) -> Spec state input output // conversion for old specificaions
+
+class render a :: !a -> String		// show a concise text representation for rendering purposes
+
+enumerate		:: [a] | ggen{|*|} a
+
+possibleInputs	:: (ESM s i o) [s] -> [i] | gEq{|*|} s & ggen{|*|}, gEq{|*|} i
+nextStates		:: (ESM s i o) i ![s] -> [s] | gEq{|*|} s
+addStep			:: (ESM s i o) [s] i !(Traces s i o) -> Traces s i o | gEq{|*|} s
+narrowTraces	:: (Traces s i o) [s] -> Traces s i o | gEq{|*|} s
+
+nodesOf			:: !(KnownAutomaton s i o) -> [s] | gEq{|*|} s
+edgesFrom		:: s !(KnownAutomaton s i o) -> [SeenTrans s i o] | gEq{|*|} s
+edgesTo			:: s !(KnownAutomaton s i o) -> [SeenTrans s i o] | gEq{|*|} s
+
+startStates		:: ![SeenTrans s i o] -> [s] | gEq{|*|} s
+targetStates	:: ![SeenTrans s i o] -> [s] | gEq{|*|} s
+
+addTransitions :: !Int (ESM s i o) [s] [i] !(KnownAutomaton s i o) -> KnownAutomaton s i o | gEq{|*|}, render s & render, ggen{|*|}, gEq{|*|} i & gEq{|*|} o
+
+nrOf			:: !(KnownAutomaton s i o) s -> Int | gEq{|*|}, render s
+
+gisMember  :: a ![a] -> Bool | gEq{|*|} a
+gremoveDup :: !.[a] -> .[a] | gEq{|*|} a
+gelemIndex :: a ![a] -> Maybe Int | gEq{|*|} a

libraries/Gast/ESMSpec.icl

+implementation module ESMSpec
+
+import StdBool, StdFunc, StdList, StdListExtensions, StdMaybe, StdMisc, StdString, StdTuple
+import GenPrint, GenEq
+import gast
+
+tupToSpec :: (state input -> [([output],state)]) -> Spec state input output // conversion for old specificaions
+tupToSpec fun = \s i = [Pt o t \\ (o,t) <- fun s i]
+
+enumerate :: [a] | ggen{|*|} a
+enumerate = generateAll aStream
+
+possibleInputs :: (ESM s i o) [s] -> [i] | gEq{|*|} s & ggen{|*|}, gEq{|*|} i
+possibleInputs esm states = gremoveDup (take 100 [i \\ s<-states, i<-enumerate | not (isEmpty (esm.d_F s i))])
+
+nextStates :: (ESM s i o) i ![s] -> [s] | gEq{|*|} s
+nextStates esm i states
+	= gremoveDup	[ t
+				\\	s <- states
+				,	target <- esm.d_F s i
+				,	t <- case target of
+							Pt outs u = [u];
+							Ft f = [u \\ o<-esm.out s i, u<-f o]
+				]
+
+narrowTraces :: (Traces s i o) [s] -> Traces s i o | gEq{|*|} s
+narrowTraces trace states = fst (pruneTraces trace states)
+
+pruneTraces :: (Traces s i o) [s] -> (Traces s i o,[s]) | gEq{|*|} s
+pruneTraces [] states = ([],states)
+pruneTraces [trans:rest] states
+	# (rest ,states) = pruneTraces rest states
+	# trans = [tr\\tr=:(s,i,o,t)<-trans|gisMember t states]
+	= ([trans:rest],startStates trans)
+
+addStep :: (ESM s i o) [s] i !(Traces s i o) -> Traces s i o | gEq{|*|} s
+addStep esm states i trace
+	= 	narrowTraces trace states ++
+		[[	(s,i,o,t)
+		 \\ s <- states
+		 ,	target <- esm.d_F s i
+		 , (o,t) <- case target of
+						Pt outs u = [(outs,u)];
+						Ft f = [ (o,u) \\ o<-esm.out s i, u<-f o]
+		]]
+
+nodesOf :: !(KnownAutomaton s i o) -> [s] | gEq{|*|} s
+//nodesOf automaton				= gremoveDup (flatten [[startnode,endnode] \\ (startnode,_,_,endnode) <- automaton.trans])
+nodesOf automaton				= gremoveDup ([s \\ (s,_,_,t) <- automaton.trans]++[t \\ (s,_,_,t) <- automaton.trans])
+
+edgesFrom :: s !(KnownAutomaton s i o) -> [SeenTrans s i o] | gEq{|*|} s
+edgesFrom startnode automaton	= [edge \\ edge=:(s,i,o,t) <- automaton.trans | s===startnode]
+
+edgesTo :: s !(KnownAutomaton s i o) -> [SeenTrans s i o] | gEq{|*|} s
+edgesTo endnode automaton		= [edge \\ edge=:(s,i,o,t) <- automaton.trans | t===endnode]
+
+startStates :: ![SeenTrans s i o] -> [s] | gEq{|*|} s
+startStates transitions			= gremoveDup [ s \\ (s,i,o,t) <- transitions ]
+
+targetStates :: ![SeenTrans s i o] -> [s] | gEq{|*|} s
+targetStates transitions		= gremoveDup [ t \\ (s,i,o,t) <- transitions ]
+
+addTransitions :: !Int (ESM s i o) [s] [i] !(KnownAutomaton s i o) -> KnownAutomaton s i o | gEq{|*|}, render s & render, ggen{|*|}, gEq{|*|} i & gEq{|*|} o
+addTransitions n esm startstates is automaton
+	| n>0 && not (isEmpty startstates)
+		# newSeenTrans
+			=	[	(s,i,o,t)
+				\\	s <- startstates
+				,	i <- map snd (sortBy (\(a,_) (b,_).a<b) (map (\i.(render i,i)) is)) // is // sort inputs
+				,	target <- esm.d_F s i
+				,	(o,t) <- case target of
+								Pt outs u = [(outs,u)];
+								Ft f = [ (o,u) \\ o<-esm.out s i, u<-f o]
+				]
+		# newStates	= targetStates newSeenTrans
+		# newTrans	= [t \\ t <- newSeenTrans | not (gisMember t automaton.trans)]
+		# newIssues	= [(t,e) \\ t<-newTrans, e <- esm.pred t | not (isEmpty e)]
+		= addTransitions (n-1) esm newStates (possibleInputs esm newStates) {trans=mix automaton.trans newTrans, issues=newIssues++automaton.issues}
+	| otherwise		= automaton
+
+mix :: [SeenTrans s i o] [SeenTrans s i o] -> [SeenTrans s i o] | render s & render i
+mix known new = foldl (insertBy less) known new
+
+insertBy :: (a a->Bool) [a] a -> [a]
+insertBy le [] e = [e]
+insertBy le l=:[a:x] e
+	| le e a
+		= [e:l]
+		= [a:insertBy le x e]
+
+less :: (SeenTrans s i o) (SeenTrans s i o) -> Bool | render s & render i
+less (s1,i1,o1,t1) (s2,i2,o2,t2)
+	# rs1 = render s1
+	# rs2 = render s2
+	# ro1 = render i1
+	# ro2 = render i2
+	# rt1 = render t1
+	# rt2 = render t2
+	= rs1<rs2 || (rs1==rs2 && (ro1<ro2 || (ro1==ro2 && rt1<=rt2)))
+
+nrOf :: !(KnownAutomaton s i o) s -> Int | gEq{|*|}, render s
+nrOf automaton s
+	= case gelemIndex s (nodesOf automaton) of
+		Just i					= i
+		nothing					= abort ("nrOf applied to unknown state: "+++render s+++"\n")
+
+gisMember :: a ![a] -> Bool | gEq{|*|} a
+gisMember x [hd:tl] = hd===x || gisMember x tl
+gisMember _ _       = False
+
+gremoveDup :: !.[a] -> .[a] | gEq{|*|} a
+gremoveDup [x:xs] = [x:gremoveDup (filter ((=!=) x) xs)]
+gremoveDup _      = []
+
+gelemIndex :: a ![a] -> Maybe Int | gEq{|*|} a
+gelemIndex x l = scan 0 x l
+where
+	scan i x [a:r]
+		| x===a	= Just i
+				= scan (i+1) x r
+	scan i x _ = Nothing
+

libraries/Gast/ESMVizTool.dcl

+definition module ESMVizTool
+
+import StdiData
+import ESMSpec
+
+/*
+esmVizTool :: !(ESM s i o) *HSt -> ((Bool,String),Html,*HSt)
+					| iData, gEq{|*|}, render s 
+                    & iData, gEq{|*|}, render, ggen{|*|} i 
+                    & iData, gEq{|*|}, render o
+*/
+esmVizTool :: !(ESM s i o) *World -> *World | iData, gEq{|*|}, render s & iData, gEq{|*|}, render, ggen{|*|} i & iData, gEq{|*|}, render o
+
+toHtmlString :: a -> String | gPrint{|*|} a

libraries/Gast/ESMVizTool.icl

+implementation module ESMVizTool
+
+import StdEnv, StdListExtensions
+import StdiData
+import StdiTasks //iTasks, iTaskDB
+import ESMSpec
+import iDataGraphvizForm
+import GenPrint
+
+derive gForm  KnownAutomaton, Maybe, []
+derive gUpd   KnownAutomaton, Maybe, []
+derive gPrint KnownAutomaton, Maybe
+derive gParse KnownAutomaton, Maybe
+
+//esmVizTool :: !(ESM s i o) *HSt -> (Bool,Html,*HSt) | iData, gEq{|*|}, render s & iData, gEq{|*|}, render, ggen{|*|} i & iData, gEq{|*|}, render o
+esmVizTool :: !(ESM s i o) *World -> *World | iData, gEq{|*|}, render s & iData, gEq{|*|}, render, ggen{|*|} i & iData, gEq{|*|}, render o
+esmVizTool esm world
+	 = singleUserTask [] (iterateTask DiGraphFlow (newKA,[esm.s_0],[],1)) world
+where
+	DiGraphFlow	st=:(ka,as,trace,n)
+	 =	orTaskL	[state
+				,chooseTaskV [] (sortBy (\(a,_) (b,_).a<b) [(render i,step i) \\ i<-possibleInputs esm as])
+				,[Br] !>> chooseTask [] [("Back" ,back),("Prune",prune),("Reset",return_V (newKA,[esm.s_0],[],1)),("Clear trace",return_V (ka,as,[],n))]
+	    		,stepN <<! traceHtml trace <<! legend
+	    		]
+	where
+		state 	=	issuesToHtml ka.issues
+					!>>	editTask "OK" (mkDigraph ThisExe (ka,esm.s_0,as,allEdgesFound esm ka,map fst ka.issues,flatten trace))
+					=>> \dig -> let (as`,trace`) = findSelectedStates dig ka as trace
+							  	in return_V (ka,as`,trace`,n)
+		step i 	= let next   = nextStates esm i as
+					  ka`    = addTransitions 1 esm as [i] ka
+					  trace` = addStep esm as i trace
+				  in return_V (ka`,next,trace`,n)
+		back | isEmpty trace
+				= return_V (ka,as,[],n)
+				= let next   = startStates (last trace)
+					  trace` = init trace
+				  in return_V (ka,next,trace`,n)
+		stepN 	= editTask "Add All" n
+				  =>> \n -> if (n>0)
+				  		(return_V (addTransitions n esm as (possibleInputs esm as) ka,as,trace,n)) 
+				  		(return_V (ka,as,trace,1))
+		prune	= return_V ({trans=[t\\t<-ka.trans|gisMember t onTraces],issues=[i\\i=:(t,_)<-ka.issues|gisMember t onTraces]},as,trace,n) where onTraces = flatten trace
+
+newKA = {trans=[],issues=[]}
+
+iterateTask :: (a->Task a) a -> Task a | iData a
+iterateTask task a = task a =>> iterateTask task
+
+orTaskL :: [Task a] -> Task a | iData a
+orTaskL l = foldl1 (-||-) l
+
+foldl1 op [a]   = a
+foldl1 op [a:x] = op a (foldl1 op x)
+
+traceHtml trace
+   = [H3 [] "Trace:"
+     ,Table []
+       [Tr [] [Td [] (map Txt (flatten [transToStrings t [] \\ t <- step]))]
+           \\ step <- trace
+       ]
+     , Br
+     ]
+
+legend
+ =	[ H3 [] "Legend:"
+	, Txt "Double circled state: intial state."
+	, Br
+	, Txt "Red state: current state (change state by click + OK-button)."
+	, Br
+	, Txt "Blue state: all defined inputs have been applied."
+	, Br
+	, Txt "Blue transitions: part of the current trace."
+	, Br
+	, Txt "Red transitions: an issue was found on this trace. Arrow heads are slightly bigger on trace."
+	]
+
+issuesToHtml :: [(SeenTrans s i o,[String])] -> HtmlCode | render s & render i & render o
+issuesToHtml [] = []
+issuesToHtml l
+	=	[H3 [] "Issues found:"
+		:	[ Table []
+				[ Tr [] [Td [] (map Txt (transToStrings t [": ":ss])) ]
+				\\ (t,ss) <- l
+				]
+			]
+		]
+
+transToStrings :: (SeenTrans s i o) [String] -> [String] | render s & render i & render o
+transToStrings (s,i,o,t) c = ["(",render s,",",render i,",[":showList "," o ["],",render t,")":c]]
+
+showList :: !String ![a] [String] -> [String] | render a
+showList delimit []    c = c
+showList delimit [x]   c = [render x:c]
+showList delimit [x:r] c = [render x,delimit:showList delimit r c]
+
+findSelectedStates :: Digraph (KnownAutomaton s i o) [s] (Traces s i o) -> ([s],Traces s i o) | render, gEq{|*|} s
+findSelectedStates (Digraph _ _ _ Nothing) _ as t = (as,t)
+findSelectedStates (Digraph _ _ nodes (Just (Node nr))) ka as trace
+	# as` = take 1
+			[  s
+			\\ NodeDef nr` _ atts _ <- nodes | nr`==nr
+			,  (NAtt_label label) <- atts
+			,  s <- nodesOf ka | render s == label
+			]
+	= case as` of
+		[]	 = (as,trace)
+		[ns] | gisMember ns as
+				= (as`,narrowTraces trace as`)
+			 # oneStep = [tr \\ tr=:(s,i,o,t)<-ka.trans | t===ns && gisMember s as]
+			 | not (isEmpty oneStep)
+			 = (as`,trace++[oneStep])
+			 = (as`,partTraces trace ns [])
+			 = (as`,[]) // ??
+
+partTraces :: (Traces s i o) s (Traces s i o) -> (Traces s i o) | gEq{|*|} s
+partTraces [] s seen = []
+partTraces [trans:rest] s seen
+	| gisMember s (targetStates trans)
+		= narrowTraces (reverse [trans:seen]) [s]
+		= partTraces rest s [trans:seen]
+
+allEdgesFound :: (ESM s i o) (KnownAutomaton s i o) -> [s] | gEq{|*|} s & ggen{|*|} i
+allEdgesFound esm automaton
+	= [s \\ s <- nodesOf automaton
+	      | length (edgesFrom s automaton) == length [t \\ i<-enumerate,t<-nextStates esm i [s]] 
+	  ]
+
+toHtmlString :: a -> String | gPrint{|*|} a
+toHtmlString x
+	# string = printToString x
+	= {checkChar c \\ c <-: string}
+where
+	checkChar '"' = '\''
+	checkChar  c  = c

libraries/Gast/confSM.dcl

@@ -5,13 +5,13 @@ definition module confSM
 	
 	ioco: Input Output COnformance of reactive systems
 
-	Pieter Koopman, 2004, 2005
+	Pieter Koopman, 2004-2008
 	Radboud Universty, Nijmegen
 	The Netherlands
 	pieter@cs.ru.nl
 */
 
-import StdEnv, MersenneTwister, gen, genLibTest, testable
+import StdEnv, MersenneTwister, gen, genLibTest, testable, StdMaybe
 
 :: Spec state input output :== state input -> [Trans output state]
 :: Trans output state = Pt [output] state | Ft ([output]->[state])
@@ -31,19 +31,22 @@ generateFSMpaths :: s (Spec s i o) [i] (s->[i]) -> [[i]] | gEq{|*|} s
 	| Seed Int
 	| Randoms [Int]
 	| FixedInputs [[i]]
-	| InputFun ([s] -> i)
+	| InputFun (RandomStream s -> [i])
 	| OnPath Int
 	//	| OutputFun ([s] i -> o)
 	| FSM [i] (s->[i]) // inputs state_identification
-	| Trace Bool
+	| MkTrace Bool
 	| OnTheFly
 	| SwitchSpec (Spec s i o)
 	| OnAndOffPath
 	| ErrorFile String
 	| Stop ([s] -> Bool)
+	| Inconsistent ([o] [s] -> Maybe [String])
 
-testConfSM :: [TestOption s i o] (Spec s i o) s (IUTstep .t i o) .t (.t->.t) *d -> (.t,*d)
-			| FileSystem d & ggen{|*|} i & gEq{|*|} s & gEq{|*|} o & genShow{|*|} s & genShow{|*|} i & genShow{|*|} o
+//testConfSM :: [TestOption s i o] (Spec s i o) s (IUTstep .t i o) .t (.t->.t) *d -> (.t,*d)
+//			| FileSystem d & ggen{|*|} i & gEq{|*|} s & gEq{|*|} o & genShow{|*|} s & genShow{|*|} i & genShow{|*|} o
+testConfSM :: [TestOption s i o] (Spec s i o) s (IUTstep .t i o) .t (.t->.t) *File *File -> (.t,*File,*File)
+			| ggen{|*|} i & gEq{|*|} s & gEq{|*|} o & genShow{|*|} s & genShow{|*|} i & genShow{|*|} o
 
 (after) infix 0 :: [s] (Spec s i o) -> ([i] -> [s])
 

libraries/Gast/confSM.icl

@@ -39,10 +39,11 @@ where
  
  // =abort "toUIT"
 
-:: NewInput i = Input i | Reset | End
+:: NewInput i = NewInput i | Reset | End
 
 :: *TestState s i o
  =	!{	spec	:: !Spec s i o
+//	,	specW	:: !SpecWorld s i
 	,	iniState:: !s
 	,	curState:: ![s]
 	,	nRej	:: !Int
@@ -64,7 +65,8 @@ where
 	,	errFile	:: !*File
 	,	mesFile	:: !*File
 	,	trace	:: !Bool
-	,	stop	:: ([s] -> Bool)
+	,	incons	:: [o] [s] -> Maybe [String]
+	,	stop	:: [s] -> Bool
 	}
 /*
 apply :: i (IUT s i o) -> ([o],IUT s i o) | genShow{|*|} s & genShow{|*|} i
@@ -86,7 +88,7 @@ newSpec spec2 n ts
  # (i,ts) = onTheFly ts
  = case i of
 	Reset	= (i,{ ts & input = newSpec spec2 ts.nOnPath })
-	Input _	= (i,{ ts & input = newSpec spec2 (n-1)})
+	NewInput _	= (i,{ ts & input = newSpec spec2 (n-1)})
 	_		= (i,ts)
 
 oldSpec :: (Spec s i o) (TestState s i o) -> *(NewInput i, TestState s i o) | ggen{|*|} i
@@ -107,7 +109,7 @@ onPath n ts
  # (i,ts) = onTheFly ts
  = case i of
 	Reset	= (i,{ ts & input = onPath ts.nOnPath })
-	Input _	= (i,{ ts & input = onPath (n-1)})
+	NewInput _	= (i,{ ts & input = onPath (n-1)})
 	_		= (i,ts)
 
 mkComplete spec s i
@@ -120,7 +122,7 @@ offPath spec [] ts = (Reset,{ ts & input = onPath ts.nOnPath })
 offPath spec [i:r] ts
   | ts.nStep >= ts.maxLen-1 || ts.nRej >= ts.maxLen-1
 	= (Reset,{ ts & input = onPath ts.nOnPath })
-	= (Input i,{ts & input = offPath spec r})
+	= (NewInput i,{ts & input = offPath spec r})
 
 onTheFly :: (TestState s i o) -> *(NewInput i, TestState s i o)
 onTheFly ts=:{curState,inputs,rnd,spec}
@@ -134,7 +136,7 @@ onTheFly ts=:{curState,inputs,rnd,spec}
 			  n = lengthN max 0 is	// the number of the selected input
 			  [r:rnd] = rnd
 			  i = is !! ((abs r) rem n)
-			= (Input i,{ts & rnd = rnd})
+			= (NewInput i,{ts & rnd = rnd})
 
 lengthN :: !Int !Int ![a] -> Int
 lengthN m n [] = n
@@ -148,7 +150,7 @@ fixedInputs [[]   :r] ts = (Reset, { ts & input = fixedInputs r })
 fixedInputs [[a:x]:r] ts=:{curState,spec} 
 	| isEmpty [t \\ s<- curState, t<-spec s a]
 		= (Reset, { ts & input = fixedInputs r , nTrun = ts.nTrun+1})
-		= (Input a, {ts & input = fixedInputs [x:r]})
+		= (NewInput a, {ts & input = fixedInputs [x:r]})
 
 genLongInput :: s Int (Spec s i o) [i] [Int] -> [i]
 genLongInput s 0 spec inputs [r:x] = randomize inputs x 7 (\_.[])
@@ -167,6 +169,154 @@ genLongInput s n spec inputs [r,r2:x]
 genLongInputs :: s (Spec s i o) [i] Int [Int] -> [[i]]
 genLongInputs s spec inputs n [r:x] = [genLongInput s n spec inputs (genRandInt r): genLongInputs s spec inputs n x]
 
+testConfSM :: [TestOption s i o] (Spec s i o) s (IUTstep .t i o) .t (.t->.t) *File *File -> (.t,*File,*File)
+			| ggen{|*|} i & gEq{|*|} s & gEq{|*|} o & genShow{|*|} s & genShow{|*|} i & genShow{|*|} o
+testConfSM opts spec s0 iut t reset console file
+	# ts=:{fileName}		= initState file console
+	# (t,ts)	= doTest ts iut t reset
+	  {mesFile,errFile} = ts
+	= (t, mesFile, errFile)
+where
+	initState file console
+	 =	handleOptions opts
+	 	{	spec	= spec
+	// 	,	specW	= \s i.[]
+		,	iniState= s0
+		,	curState= [s0]
+		,	nRej	= 0
+		,	nTrun	= 0
+		,	nPath	= 0
+		,	nStep	= 0
+		,	nTotal	= 0
+		,	maxPath	= 100
+		,	maxLen	= 1000
+		,	nOnPath	= 50
+		,	inputs	= (\rnd s -> ggen {|*|} 2 rnd)
+		,	input	= onTheFly 
+		,	n		= 0
+		,	h_in	= []
+		,	h_out	= []
+		,	h_state	= []
+		,	rnd		= aStream
+		,	errFile	= file
+		,	fileName= outputFile
+		,	mesFile	= console <<< "Gast starts testing.\n"
+		,	trace	= False
+		,	incons	= \o ss -> Nothing
+		,	stop	= (\states = False)
+		}
+
+findFileName [] name = name
+findFileName [ErrorFile s:r] name = findFileName r s
+findFileName [_:r] name = findFileName r name
+
+doTest :: (TestState s i o) (IUTstep .t i o) .t (.t->.t) -> (.t,TestState s i o)
+		| gEq{|*|} s & gEq{|*|} o & genShow{|*|} s & genShow{|*|} i & genShow{|*|} o
+doTest ts=:{input,curState,spec,incons} step t reset
+  | isEmpty ts.curState
+	= (t, errorFound ts)
+  | ts.nStep >= ts.maxLen || ts.nRej >= ts.maxLen
+	= doTest (resetState ts) step (reset t) reset
+  | ts.nPath >= ts.maxPath
+  	| ts.nRej == 0 && ts.nTrun == 0
+	  = (t,{ts & mesFile = ts.mesFile	<<< "\nEnd of testing, maximum paths used. \n"
+										<<< ts.nPath
+										<<< " test paths executed successful, in total "
+										<<< ts.nTotal <<< " transitions.\n"})
+	  = (t,{ts & mesFile = ts.mesFile	<<< "\nEnd of testing, maximum paths used. \n"
+										<<< ts.nPath
+										<<< " test paths executed successful, "
+										<<< ts.nTrun <<< " paths truncated, "
+										<<< " in total "
+										<<< ts.nTotal <<< " transitions.\n"})
+  #	(inp,ts) = input ts
+  =	case inp of
+	  Reset	= doTest (resetState ts) step (reset t) reset
+	  End	| ts.nRej == 0 && ts.nTrun == 0
+			  = (t,{ts & mesFile = ts.mesFile	<<< "\nAll input paths tested successfully.\n"
+												<<< "All " <<< ts.nPath
+												<<< " executed test paths successful (Proof), in total "
+												<<< ts.nTotal <<< " transitions.\n"})
+			  = (t,{ts & mesFile = ts.mesFile	<<< "\nAll inputs tested successfully.\n"
+												<<< (ts.nPath-ts.nRej)
+												<<< "test path executed successful (Proof), " <<< ts.nRej
+												<<< " paths rejected " <<< ts.nTrun
+												<<< " paths truncated, "
+												<<< "in total " <<< ts.nTotal <<< " transitions.\n"})
+	  NewInput i	// assumption: only inputs allowed by spec will be generated:
+		#!	(iut_o,t) = step t i
+			tuples = [tup \\ s<-curState, tup<-spec s i]
+			states = mkset (newStates tuples iut_o)
+		| isEmpty states
+			#! errFile = ts.errFile <<< "Error found! Trace:\n"
+									<<< "SpecificationStates Input -> ObservedOutput\n"
+			   errFile = showError (ts.nStep+1) [curState:ts.h_state] [i:ts.h_in] [iut_o:ts.h_out] errFile
+			   errFile = errorInfo ts.nPath ts.nRej ts.nTrun (ts.nTotal+1) (errFile <<< "\n")
+			   mesFile = errorInfo ts.nPath ts.nRej ts.nTrun (ts.nTotal+1) ts.mesFile
+			   mesFile = mesFile <<< "See file \"" <<< ts.fileName <<< "\" for details about the error.\n"
+			= (t,{ts	& mesFile = mesFile
+						, errFile = errFile
+						, curState = []
+						})
+			= case incons iut_o states of
+				Nothing
+				   # mesFile = ts.mesFile <<< "paths: " <<< ts.nPath <<< ", rejected: " <<< ts.nRej <<< ", truncated: " <<< ts.nTrun <<< "...\r"
+				   = doTest {ts	& curState = states
+								, nStep = ts.nStep+1
+								, nTotal =ts.nTotal+1
+								, h_in = [i:ts.h_in]
+								, h_out = [iut_o:ts.h_out]
+								, h_state = [curState:ts.h_state]
+								, mesFile = if ts.trace (mesFile <<< ts.nPath <<< "," <<< ts.nStep <<< ": " <<< show1 ts.curState <<< " " <<< show1 i <<< " " <<< show1 iut_o <<< "\n") mesFile
+								}
+							step t reset
+				Just errors	
+					#! errFile = ts.errFile <<< "Inconsistency! Trace:\n"
+											<<< "SpecificationStates Input -> ObservedOutput\n"
+					   errFile = showError (ts.nStep+1) [curState:ts.h_state] [i:ts.h_in] [iut_o:ts.h_out] errFile
+					   errFile = errFile <<< "Inconsistency info:\n" <<< errors <<< "\n"
+					   errFile = errorInfo ts.nPath ts.nRej ts.nTrun (ts.nTotal+1) (errFile <<< "\n")
+					   mesFile = ts.mesFile <<< "Inconsistency found!\n" <<< errors <<< "\n\n"
+					   mesFile = errorInfo ts.nPath ts.nRej ts.nTrun (ts.nTotal+1) mesFile
+					   mesFile = mesFile <<< "See file \"" <<< ts.fileName <<< "\" for details.\n"
+					= (t,{ts	& mesFile = mesFile
+								, errFile = errFile
+								, curState = []
+								})
+where
+	errorInfo :: !Int !Int !Int !Int *File -> *File
+	errorInfo nPath nRej nTrun nTotal file
+	 = file	<<< "Error found in path " <<< (nPath+1) <<< ", "
+			<<< (nPath-nRej) <<< " paths executed, "
+			<<< nTrun <<< " tests truncated, in total "
+			<<< nTotal <<< " transitions.\n"
+
+outputFile = "testOut.txt"
+
+newStates [] iut_o = []