Merge branch 'master' of https://github.com/dopefishh/tt2015

[tt2015.git] / a3 / code / Gast / confSM.dcl

diff --git a/a3/code/Gast/confSM.dcl b/a3/code/Gast/confSM.dcl
deleted file mode 100644 (file)
index 2b7d51f..0000000
--- a/a3/code/Gast/confSM.dcl
+++ /dev/null
@@ -1,55 +0,0 @@
-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