Import of Pieter's latest version

Libraries/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
+							 , esm_name	:: String
+							 }
+::	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
+
+class renderEq a | render a & gEq{|*|} a
+
+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
+sharedNodesOf	:: !(KnownAutomaton s i o) -> [s] | gEq{|*|}, Eq 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
+addTransitions :: !Int (ESM s i o) [s] [i] !(KnownAutomaton s i o) -> KnownAutomaton s i o | render, gEq{|*|} s & render, gEq{|*|}, ggen{|*|} 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/ESMSpec.icl

+implementation module ESMSpec
+
+import StdBool, StdList, StdMaybe, StdMisc, StdString, StdTuple, StdOrdList
+import GenPrint, GenEq, Data.List
+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 = take 100 (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])
+
+sharedNodesOf :: !(KnownAutomaton s i o) -> [s] | gEq{|*|}, Eq s
+sharedNodesOf automaton
+ = [ n \\ n <- nodes, m <- nodes | n<>m && n === m ]
+where nodes = removeDup ([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 | render, gEq{|*|} s & render, gEq{|*|}, ggen{|*|} 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/ESMVizTool.dcl

+definition module ESMVizTool
+
+import ESMSpec
+import iTasks
+
+class all a | iTask, render, gEq{|*|} a
+
+
+/*
+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 | iTask, gEq{|*|}, render, Eq s & iTask, gEq{|*|}, render, ggen{|*|} i & iTask, gEq{|*|}, render o
+//esmVizTool :: !(ESM s i o) *World -> *World | iTask, renderEq s & iTask, renderEq, Eq, ggen{|*|} i & iTask, gEq{|*|}, render o
+esmVizTool :: !(ESM s i o) *World -> *World
+//			| iTask, render, gEq{|*|}, Eq s & iTask, render, gEq{|*|}, ggen{|*|} i & iTask, gEq{|*|}, render o
+			| all, Eq, genShow{|*|} s & all, genShow{|*|}, ggen{|*|} i & all o
+
+toHtmlString :: a -> String | gText{|*|} a

Libraries/ESMVizTool.icl

+implementation module ESMVizTool
+
+import iTasks
+import ESMSpec
+import GenPrint
+
+import Data.Graphviz
+import GraphvizVisualization
+
+derive bimap (,), Maybe
+derive class iTask KnownAutomaton, State
+
+finished_state_color :: (!Color,!Color)
+finished_state_color	= (Color "blue", Color "white")
+
+default_state_color :: (!Color,!Color)
+default_state_color		= (Color "grey90",Color "black")
+	
+shared_state_color :: (!Color,!Color)
+shared_state_color		= (Color "gray",Color "white")
+	
+shared_active_state_color :: (!Color,!Color)
+shared_active_state_color = (Color "gray",Color "red")
+
+active_state_color :: !Int -> (!Color,!Color)
+active_state_color nr	= (RGB 255 dim dim,Color "white")
+where
+	dim	= min 250 (255 - 255 / (min nr 3))
+	
+fontsize = 12.0 // 18.0
+
+:: State s i o
+ =	{ ka	:: !KnownAutomaton s i o
+	, ss	:: ![s]
+	, trace	:: !Traces s i o
+	, n		:: !Int
+	, r		:: !Int
+	}
+
+esmVizTool :: !(ESM s i o) *World -> *World
+			| all, Eq, genShow{|*|} s & all, genShow{|*|}, ggen{|*|} i & all o
+esmVizTool esm world
+	= startEngine (iterateTask (DiGraphFlow esm) newstate) world
+where
+	newstate = { ka = newKA, ss = [esm.s_0], trace = [], n = 1, r = 15102014}
+	 
+DiGraphFlow :: !(ESM s i o) (State s i o) -> Task (State s i o) 
+				| all, Eq, genShow{|*|} s & all, genShow{|*|}, ggen{|*|} i & all o
+DiGraphFlow	esm st=:{ka,ss,trace,n,r}
+ = (anyTask
+	[ state esm st
+	, selectInput
+	, editChoice "go to" [] nodes Nothing
+      >>* [OnAction ActionOk (hasValue (updateDig st))]
+    , updateInformation "Multiple steps" [] n
+		>>* [OnAction ActionOk (ifValue (\n.n>0) (doStepN esm st))]
+    ]	-|| viewIssues st
+    	-||	viewInformation (Title "Trace & legend") [ViewWith traceHtml] trace
+    )
+    >>= DiGraphFlow esm
+where
+	selectInput
+		| isEmpty inputs
+			= viewInformation "no transition from current state" [] "Use another action" >>| return st
+			=	(	enterInformation "input" []
+				>>* [ OnAction ActionYes (ifValue (\i.not (isEmpty (nextStates esm i ss))) (stepState esm st))
+					, OnAction (Action "I'm feeling lucky" []) (always systemInput)
+			    	, OnAction ActionPrevious (always (back st))
+			    	, OnAction (Action "Prune" []) (always (prune st))
+			    	, OnAction ActionNew (always (return newState))
+			    	, OnAction (Action "Clear trace" []) (always (return {st & trace  = []}))
+					])
+				-||-
+				(	viewInformation "select input" [] ""
+				>>* [	OnAction (Action (show1 inp) []) (always (stepState esm st inp))
+					\\	inp <- take 7 inputs
+					]
+				)
+	
+	systemInput
+		| isEmpty newInputs
+			| isEmpty inputs2
+				= return st
+				= stepState esm {st & r = rn} (inputs2!!((abs r) rem (length inputs2)))
+			= stepState esm {st & r = rn} (newInputs!!((abs r) rem (length newInputs)))
+
+	inputs		= possibleInputs esm ss
+	inputs2		= [ i \\ i <- inputs, (s,j,_,t) <- ka.trans | i === j && gisMember s ss && ~ (gisMember t ss) ]
+	newInputs	= filter (\i.not (gisMember i usedInputs)) inputs
+	usedInputs	= [ j \\ (s,j,_,_) <- ka.trans | gisMember s ss ]
+	rn			= hd (genRandInt r)
+	nodes		= toHead esm.s_0 (gremoveDup (nodesOf ka ++ ss))
+	newState 	= { ka = newKA, ss = [esm.s_0], trace = [], n = 1, r = rn}
+
+	//traceTweak	=  AfterLayout (tweakUI (\x -> appDeep [0] (fixedWidth 670 o fixedHeight 200) x)) 
+	
+stepStateN :: !(ESM s i o) !(State s i o) -> Task (State s i o) | all, Eq s & all, ggen{|*|} i & all o
+stepStateN esm st=:{ka,ss,trace,n,r}
+ =		updateInformation ("Steps","Add multiple stepStates...") [] n
+	>>= doStepN esm st
+	
+doStepN :: !(ESM s i o) !(State s i o) Int -> Task (State s i o) | all, Eq s & all, ggen{|*|} i & all o
+doStepN esm state=:{ka,ss,trace,r} n
+	= if (n>0)
+  		(return {state & ka = addTransitions n esm ss (possibleInputs esm ss) ka, r = rn })
+  		(return {state & n = 1})
+where rn = hd (genRandInt r)
+
+chooseTask :: !d ![(String,Task o)] -> Task o | descr d & iTask o 
+chooseTask msg tasks = enterChoice msg [] [(l, Hidden t) \\ (l,t) <- tasks] >>= \(l, Hidden t). t
+
+chooseTaskComBo :: !d ![(String,Task o)] -> Task o | descr d & iTask o 
+chooseTaskComBo msg tasks
+ =	updateChoice msg [] trans (trans !! 0)
+ 	>>= \(l, Hidden t). t
+	>>! return
+where
+	trans = [(l, Hidden t) \\ (l,t) <- tasks]
+
+prune :: !(State s i o) -> Task (State s i o) | all, Eq s & all, ggen{|*|} i & all o
+prune state=:{ka,ss,trace,n,r}
+	= return	{ state
+				& ka = 	{ ka
+						& trans =	[ t
+									\\	t <- ka.trans
+									|	gisMember t onTraces
+									]
+						, issues =	[ i
+									\\	i=:(t,_) <- ka.issues
+									|	gisMember t onTraces
+									]
+						}
+//				, r = rn
+				}
+where
+	onTraces = flatten trace
+	rn		= hd (genRandInt r)
+
+state :: !(ESM s i o) !(State s i o) -> Task (State s i o) | all, Eq, genShow{|*|} s & all, ggen{|*|} i & all o
+state esm st=:{ka,ss,trace,n,r} = digraph
+where
+	digraph = updateInformation Void [UpdateWith toView fromView] st <<@ AfterLayout (tweakUI (fixedWidth 800 o fixedHeight 350))
+	
+	//Make an editable digraph from the esm state
+	toView st=:{ka,ss,trace}
+		= includeChanges (mkDigraph esm.esm_name (ka, esm.s_0, ss, allEdgesFound esm ka, sharedNodesOf ka, map fst ka.issues, flatten trace)) 
+	//Map changes in the diagraph back to the esm state
+	fromView st dg = st
+		
+	 //(mkDigraph "ESM" (ka, esm.s_0, ss, allEdgesFound esm ka, sharedNodesOf ka, map fst ka.issues, flatten trace))
+	 //	>>= updateDig st
+
+mkDigraph :: String (KnownAutomaton s i o,s,[s],[s],[s],[SeenTrans s i o],[SeenTrans s i o]) -> Digraph | render, gEq{|*|}, genShow{|*|} s & render, gEq{|*|} i & render, gEq{|*|} o
+mkDigraph name (automaton,s_0,init_states,finished,shared,issues,trace)
+	= Digraph
+		name
+		graphAttributes
+		((if	(  gisMember s_0 (init_states ++ all_nodes) // is s_0 part of the current machine state
+			//	|| isEmpty automaton.trans
+			//	&& isEmpty init_states
+			 	)
+			[ NodeDef -1 // initil black node and arrow to s_0
+				[ ]
+				[ NAttLabel		""
+				, NAttStyle		NStyleFilled
+				, NAttColor		(Color "black")
+				, NAttShape		NShapeCircle
+	   			, NAttFixedSize	True
+	  			, NAttWidth		0.2
+				, NAttHeight	0.2
+				, NAttMargin	(SingleMargin 0.003)
+				]
+				[( //if (gisMember s_0 init_states)
+					gIndex s_0 (all_nodes ++ init_states)
+					//(nrOf automaton s_0)
+				 ,	[ EAttColor		(Color "black")
+					, EAttArrowSize	2.0
+					, EAttStyle		EStyleBold
+					]
+				 )
+				]
+			]
+			[]
+		) ++
+		(if (isEmpty automaton.trans)
+			if (isEmpty init_states)
+				[ NodeDef 0 [NStAllEdgesFound False] (nodeAttributes s_0 init_states False False) []]
+				[ NodeDef i [NStAllEdgesFound False] (nodeAttributes n init_states False False) []
+				\\	n <- toHead s_0 init_states
+				&	i <- [0..]
+				]
+			[NodeDef (gIndex n all_nodes) //(nrOf automaton n)
+					[ NStAllEdgesFound (gisMember n finished)]
+					(nodeAttributes n init_states (gisMember n finished)
+					(gisMember n shared))
+			         [ (gIndex t all_nodes	, [ EAttLabel (render i+++"/"+++showList ("[","]",",") o)
+			                                , EAttFontName "Ariel"
+			                                , EAttFontSize fontsize
+			                                , EAttLabelFontName "Ariel"
+			                                , EAttLabelFontSize fontsize
+			                                , EAttColor
+			                                			 (if (gisMember trans issues)
+			                                						(Color "red")
+			                                			 (if (gisMember trans trace)
+			                                						(Color "blue")
+			                                						(Color "black")))
+			                                , EAttArrowSize (if (gisMember trans trace) 2.0 1.2)
+			                                , EAttStyle (if (gisMember trans trace) EStyleBold EStyleSolid)
+			                                ])
+			         \\ trans=:(s,i,o,t) <- edgesFrom n automaton
+			         ]
+			\\ n <- all_nodes
+			]
+		)) Nothing
+where
+	graphAttributes				= [ GAttRankDir  RDLR // horizontal
+	//graphAttributes				= [ GAttRankDir  RDTB // RD_LR
+							  	  , GAttSize     		(Sizef 7.2 3.0 False)
+								 // , GAttSize			(Sizef 5.0 3.0 True)
+								  , GAttFontSize		9.0 // 12.0
+								  , GAttBGColor  		(Color "white")
+								  , GAttOrdering 		"in"			// "out"
+								  , GAttOutputOrder		OMEdgesFirst	// OMBreadthFirst	// OMEdgesFirst	//  PK
+								  ]
+	all_nodes = toHead s_0 (nodesOf automaton)
+	nodeAttributes n init_states finished shared
+								= (if (gisMember n init_states)
+										(if shared	[ NAttFillColor shac_backgr, NAttFontColor shac_txt ]
+													[ NAttFillColor act_backgr, NAttFontColor act_txt ])
+								  (if finished [ NAttFillColor done_backgr,NAttFontColor done_txt]
+								  		(if shared	[ NAttFillColor shar_backgr, NAttFontColor shar_txt ]
+									              	[ NAttFillColor def_backgr, NAttFontColor def_txt ])
+								  )) ++
+						          [ NAttLabel		(render n)
+						          , NAttTooltip		(show1 n)
+						          , NAttStyle		NStyleFilled
+						          , NAttShape		NShapeEllipse
+						          , NAttFontName	"Ariel"
+						          , NAttFontSize	fontsize
+						          , NAttFixedSize	False
+						          , NAttWidth 1.0
+						          ,	NAttHeight 1.0
+						          , NAttMargin		(SingleMargin 0.003)
+						          ]
+	where
+		( act_backgr, act_txt)	= active_state_color (length init_states)
+		(done_backgr,done_txt)	= finished_state_color
+		( def_backgr, def_txt)	= default_state_color
+		(shar_backgr,shar_txt)	= shared_state_color
+		(shac_backgr,shac_txt)	= shared_active_state_color
+
+	
+	showList :: !(!String,!String,!String) ![a] -> String | render a
+	showList (open,close,delimit) []  = open +++ close
+	showList (open,close,delimit) [x] = open +++ render x +++ close
+	showList (open,close,delimit) xs  = open +++ foldr (\x str->render x+++delimit+++str) "" (init xs) +++ render (last xs) +++ close
+
+toHead :: a [a] -> [a] | gEq{|*|} a
+toHead x l | gisMember x l && hd l =!= x
+	= [x: filter ((=!=) x) l]
+	= l
+
+gIndex :: a [a] -> Int | gEq{|*|} a
+gIndex a l
+ = case [ i \\ x <- l & i <- [0..] | a === x] of
+	[i:_] = i
+	[]    = -1
+
+includeChanges :: !Digraph -> Digraph
+includeChanges dg=:(Digraph _ _ _ Nothing)		= dg
+includeChanges (Digraph title atts nodes change)= Digraph title atts (map includeNodeChange nodes) Nothing
+where
+	(SelectedItem nr`)							= fromJust change
+	
+	includeNodeChange :: !NodeDef -> NodeDef
+	includeNodeChange (NodeDef nr st atts edges)
+		| nr == nr`								= NodeDef nr st (map replaceNodeAtt atts) edges
+		| otherwise								= NodeDef nr st (map defaultNodeAtt atts) edges
+	where
+		all_edges_found							= not (isEmpty [s \\ s=:(NStAllEdgesFound True) <- st])
+		
+		replaceNodeAtt (NAttFillColor _)		= NAttFillColor (fst (active_state_color 1))
+		replaceNodeAtt (NAttFontColor _)		= NAttFontColor (snd (active_state_color 1))
+		replaceNodeAtt att						= att
+		
+		defaultNodeAtt (NAttFillColor c)		= NAttFillColor (if all_edges_found (fst finished_state_color) (fst default_state_color))
+		defaultNodeAtt (NAttFontColor c)		= NAttFontColor (if all_edges_found (snd finished_state_color) (snd default_state_color))
+		defaultNodeAtt att						= att
+
+//TODO: Turn this into a (Diagraph State -> State function)
+updateDig :: !(State s i o) !s  -> Task (State s i o) | all, Eq, genShow{|*|} s & all, ggen{|*|} i & all o
+updateDig state=:{ka,ss,trace,n,r} ns
+	= return {state & ss = [ns], trace = findSelectedStates ns ka ss trace}
+where
+	findSelectedStates ns ka ss trace
+		| gisMember ns ss
+			= narrowTraces trace [ns]
+		# oneStep = [tr \\ tr=:(s,i,o,t)<-ka.trans | t===ns && gisMember s ss]
+		| not (isEmpty oneStep)
+			= trace++[oneStep]
+			= partTraces trace ns []
+
+stepState :: !(ESM s i o) (State s i o) i -> Task (State s i o) | all, Eq s & all, ggen{|*|} i & all o
+stepState esm state=:{ka,ss,trace,n,r} i
+		= let next   = nextStates esm i ss
+			  ka`    = addTransitions 1 esm ss [i] ka
+			  trace` = addStep esm ss i trace
+		//	  rn	 = hd (genRandInt r)
+		  in return {state & ka = ka`, ss = next, trace = trace`}
+
+back :: (State s i o) -> Task (State s i o) | all, Eq s & all, ggen{|*|} i & all o
+back state=:{ka,ss,trace,n,r}
+	| isEmpty trace
+		= return state
+		= let next   = startStates (last trace)
+			  trace` = init trace
+			  rn	 = hd (genRandInt r)
+		  in return {state & trace = trace`, ss = next, r = rn}
+
+newKA = {trans = [], issues = []}
+
+iterateTask :: (a->Task a) a -> Task a | iTask a
+iterateTask task a = task a >>= iterateTask task
+
+traceHtml :: (Traces a b c) -> HtmlTag | render a & render b & render c
+traceHtml trace
+   = DivTag []
+		[ H3Tag [] [Text "Trace:"]
+	    , TableTag []
+	       [ TrTag [] [TdTag [] (map Text (flatten [transToStrings t [] \\ t <- stepState]))]
+	       \\ stepState <- trace
+	       ]
+	    , BrTag []
+	    , H3Tag [] [Text "Legend:"]
+	    , TableTag []
+	       [ TrTag [] [TdTag [] [Text string]]
+	       \\ string <- [ "red node: current state"
+	       				, "blue node: all transitions from this node shown"
+	       				, "grey node: more transitions from this node exists"
+	       				, "black arrow: transition not in current trace"
+	       				, "blue arrow: transition in current trace"
+	       				, "red arrow: transition with an issue"
+	       				, "---"
+	       				, "Back: go to the previous state"
+	       				, "Prune: remove all correct transitions that are not on the trace"
+	       				, "Reset: start all over"
+	       				, "Clear trace: remove trace, but keep everything else"
+	       				]
+	       ]
+	    ]
+
+viewIssues :: (State s i o) -> Task [(SeenTrans s i o,[String])] | render, iTask s & render, iTask i & render, iTask o
+viewIssues st=:{ka}
+	= viewInformation "Issues" [ViewWith issuesToHtml] ka.issues
+where	
+	issuesToHtml :: [(SeenTrans s i o,[String])] -> HtmlTag | render s & render i & render o
+	issuesToHtml l
+		=	DivTag []
+			[ H3Tag [] [Text "Issues found:"]
+			: [ TableTag []