--- /dev/null
+definition module confSM\r
+\r
+/*\r
+ GAST: A Generic Automatic Software Test-system\r
+ \r
+ ioco: Input Output COnformance of reactive systems\r
+\r
+ Pieter Koopman, 2004-2008\r
+ Radboud Universty, Nijmegen\r
+ The Netherlands\r
+ pieter@cs.ru.nl\r
+*/\r
+\r
+import StdEnv, MersenneTwister, gen, genLibTest, testable, StdMaybe\r
+\r
+:: Spec state input output :== state input -> [Trans output state]\r
+:: Trans output state = Pt [output] state | Ft ([output]->[state])\r
+derive genShow Trans\r
+\r
+:: TestOption s i o\r
+ = Ntests Int\r
+ | Nsequences Int\r
+ | Seed Int\r
+ | Randoms [Int]\r
+ | FixedInputs [[i]]\r
+ | InputFun (RandomStream s -> [i])\r
+ | OnPath Int\r
+ | FSM [i] (s->[i]) // inputs state_identification\r
+ | MkTrace Bool\r
+ | OnTheFly\r
+ | SwitchSpec (Spec s i o)\r
+ | OnAndOffPath\r
+ | ErrorFile String\r
+ | Stop ([s] -> Bool)\r
+ | Inconsistent ([o] [s] -> Maybe [String])\r
+\r
+:: IUTstep t i o :== t -> .(i -> .([o],t))\r
+SpectoIUTstep :: (Spec t i o) (t i -> [[o]]) -> IUTstep (t,RandomStream) i o | genShow{|*|} t & genShow{|*|} i & genShow{|*|} o\r
+\r
+toSpec :: (state input -> [(state,[output])]) -> Spec state input output\r
+\r
+genLongInputs :: s (Spec s i o) [i] Int [Int] -> [[i]]\r
+generateFSMpaths :: s (Spec s i o) [i] (s->[i]) -> [[i]] | gEq{|*|} s\r
+\r
+//testConfSM :: [TestOption s i o] (Spec s i o) s (IUTstep .t i o) .t (.t->.t) *d -> (.t,*d)\r
+// | FileSystem d & ggen{|*|} i & gEq{|*|} s & gEq{|*|} o & genShow{|*|} s & genShow{|*|} i & genShow{|*|} o\r
+testConfSM :: [TestOption s i o] (Spec s i o) s (IUTstep .t i o) .t (.t->.t) *File *File -> (.t,*File,*File)\r
+ | ggen{|*|} i & gEq{|*|} s & gEq{|*|} o & genShow{|*|} s & genShow{|*|} i & genShow{|*|} o\r
+\r
+(after) infix 0 :: [s] (Spec s i o) -> ([i] -> [s])\r
+\r
+propDeterministic :: (Spec s i o) s i -> Bool\r
+propTotal :: (Spec s i o) s i -> Bool\r
+//propComplete :: (Spec s i o) s i -> Bool // equal to propTotal\r
+propComplete spec s i :== propTotal spec s i\r