Commit 0b212cd2 authored by Thomas van Noort's avatar Thomas van Noort

Post-migration cleanup: removing redundant folders and folders that are...

Post-migration cleanup: removing redundant folders and folders that are already contained in other repositories
parent 0670cf7b
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
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
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
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
This diff is collapsed.
This diff is collapsed.
definition module confSM
/*
GAST: A Generic Automatic Software Test-system
ioco: Input Output COnformance of reactive systems
Pieter Koopman, 2004-2008
Radboud Universty, Nijmegen
The Netherlands
pieter@cs.ru.nl
*/
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])
derive genShow Trans
:: IUTstep t i o :== t -> .(i -> .([o],t))
SpectoIUTstep :: (Spec t i o) (t i -> [[o]]) -> IUTstep (t,RandomStream) i o | genShow{|*|} t & genShow{|*|} i & genShow{|*|} o
toSpec :: (state input -> [(state,[output])]) -> Spec state input output
genLongInputs :: s (Spec s i o) [i] Int [Int] -> [[i]]
generateFSMpaths :: s (Spec s i o) [i] (s->[i]) -> [[i]] | gEq{|*|} s
:: TestOption s i o
= Ntests Int
| Nsequences Int
| Seed Int
| Randoms [Int]
| FixedInputs [[i]]
| InputFun (RandomStream s -> [i])
| OnPath Int
// | OutputFun ([s] i -> o)
| FSM [i] (s->[i]) // inputs state_identification
| 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) *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])
propDeterministic :: (Spec s i o) s i -> Bool
propTotal :: (Spec s i o) s i -> Bool
//propComplete :: (Spec s i o) s i -> Bool // equal to propTotal
propComplete spec s i :== propTotal spec s i
This diff is collapsed.
definition module gast
/*
GAST: A Generic Automatic Software Test-system
Pieter Koopman, 2004-2008
Radboud Universty, Nijmegen
The Netherlands
pieter@cs.ru.nl
*/
import MersenneTwister, gen, GenEq, genLibTest, testable, confSM, stdProperty
\ No newline at end of file
implementation module gast
/*
GAST: A Generic Automatic Software Test-system
Pieter Koopman, 2004
Radboud Universty, Nijmegen
The Netherlands
pieter@cs.ru.nl
*/
\ No newline at end of file
definition module gen
/*
GAST: A Generic Automatic Software Test-system
gen: generic generation of values of a type
Pieter Koopman, 2004
Radboud Universty, Nijmegen
The Netherlands
pieter@cs.ru.nl
*/
import StdGeneric
randomize :: [a] [Int] Int ([Int] -> [a]) -> [a]
generic ggen a :: Int [Int] -> [a]
derive ggen Int, Bool, Real, Char, UNIT, PAIR, EITHER, CONS, OBJECT, FIELD, (,), (,,), (,,,), [], String
maxint :: Int
minint :: Int
StrLen :== 80
implementation module gen
/*
GAST: A Generic Automatic Software Test-system
gen: generic generation of values of a type
Pieter Koopman, 2004
Radboud Universty, Nijmegen
The Netherlands
pieter@cs.ru.nl
*/
import StdEnv, StdGeneric, MersenneTwister
// -------
:: RandomStream :== [Int]
aStream :: RandomStream
aStream = genRandInt 42
split :: RandomStream -> (RandomStream,RandomStream)
split [r,s:rnd]
# seed = r*s
| seed==0
= split rnd
= (genRandInt seed, rnd)
// -------
randomize :: [a] [Int] Int ([Int] -> [a]) -> [a]
randomize list rnd n c = rand list rnd n []
where
rand [] rnd m [] = c rnd
rand [] rnd m [x] = [x:c rnd]
rand [] rnd m l = rand l rnd n []
rand [a:x] [i:rnd] m l
| m==0 || (i rem m) == 0
= [a:rand x rnd (m-1) l]
= rand x rnd m [a:l]
// -------
generic ggen a :: Int [Int] -> [a]
maxint :: Int
maxint = 2147483647
minint :: Int
minint = -2147483648
ggen{|Int|} n rnd = randomize [0,1,-1,maxint,minint] rnd 5 id
ggen{|Bool|} n rnd = randomize [False,True] rnd 2 \_.[]
ggen{|Char|} n rnd = randomize (map toChar [32..126] ++ ['\t\n\r']) rnd 98 (\_.[])
ggen{|Real|} n rnd = randomize [0.0,1.0,-1.0] rnd 3 (\[s:x] -> f x (genRandReal s))
where f [i,j:x] [r:s]
| r==0.0
= [r:f x s]
# r = if (isOdd i) r (~r)
r = if (isOdd j) r (1.0/r)
= [r:f x s]
bias :== 1024
ggen{|UNIT|} n rnd = [UNIT]
ggen{|PAIR|} f g n rnd
# (rn2,rnd) = split rnd
= map (\(a,b)=PAIR a b) (diag2 (f n rnd) (g n rn2)) // inlinen !?
ggen{|EITHER|} f g n rnd
# (r1,rnd) = split rnd
(r2,rnd) = split rnd
= Merge n rnd (f n r1) (g (n+1) r2)
where
Merge :: Int RandomStream [a] [b] -> [EITHER a b] // Correct, strict in none of the lists!
Merge n [i:r] as bs
| (i rem n) <> 0
// | (i rem bias) > n+(bias/2)
= case as of
[] = map RIGHT bs
[a:as] = [LEFT a: Merge n r as bs]
= case bs of
[] = map LEFT as
[b:bs] = [RIGHT b: Merge n r as bs]
/* Merge :: RandomStream [a] [b] -> [EITHER a b] // Wrong, strict in both lists
Merge r [] bs = map RIGHT bs
Merge r as [] = map LEFT as
Merge [i:r] [a:as] [b:bs]
| isOdd i
= [LEFT a, RIGHT b:Merge r as bs]
= [RIGHT b, LEFT a:Merge r as bs]
*//* = Merge (isOdd (hd rnd)) (f r1) (g r2)
where
Merge :: Bool [a] [b] -> [EITHER a b]
Merge r as bs
| r
= case as of
[] = map RIGHT bs
[a:as] = [LEFT a: Merge (not r) as bs]
= case bs of
[] = map LEFT as
[b:bs] = [RIGHT b: Merge (not r) as bs]
*/
ggen{|CONS|} f n rnd = map CONS (f n rnd)
ggen{|OBJECT|} f n rnd = map OBJECT (f n rnd)
ggen{|FIELD|} f n rnd = map FIELD (f n rnd)
ggen{|String|} n rnd = ["hello world!","Tested with GAST!": rndStrings 0 rnd]
where
rndStrings 0 rnd = ["": rndStrings 1 rnd]
rndStrings len [r,s:rnd]
# (chars,rnd) = seqList (repeatn ((abs r) rem len) genElem) rnd
string = {c \\ c<-chars}
= [string:rndStrings ((len rem StrLen)+1) rnd]
class genElem a where genElem :: RandomStream -> .(a,RandomStream)
instance genElem Int where genElem [r:rnd] = (r,rnd)
instance genElem Char where genElem [r:rnd] = (toChar (32+((abs r) rem 94)),rnd)
instance genElem Bool where genElem [r:rnd] = (isOdd r,rnd)
instance