[/] [trunk/] [src/] [maketest/] [testtransflip.sml] - Blame information for rev 43

Line No. Rev Author Line
1 4 tbourke 
structure TestTransFlip :
2 
sig
3 
  val runTest : {input: string, output: TextIO.outstream} -> OS.Process.status
4 
end
5 
=
6 
struct
7 
 
8 
  local structure TIO  = TextIO
9 
              and SIO  = TextIO.StreamIO
10 
              and S    = String
11 
              and SS   = Substring
12 
              and UP   = UppaalParse
13 
              and Env  = Environment
14 
              and TF   = TransitionFlipper
15 
              and E    = UppaalParse.Expression
16 
              and ECVT = ExpressionCvt
17 
  in
18 
 
19 
  val testName = "test"
20 
 
21 
  fun readSegments filename = let
22 
      fun readSegment strm = let
23 
          fun count (n, strm) = case SIO.inputLine strm
24 
                  of NONE => if n=0 then NONE else SOME n
25 
                   | SOME ("--\n", _) => SOME n
26 
                   | SOME (s, strm')  => count (n + S.size s, strm')
27 
        in
28 
          Option.map (fn n=> SIO.inputN (strm, n)) (count (0, strm))
29 
        end
30 
 
31 
      fun skipDelim strm = case SIO.inputLine strm
32 
                           of SOME ("--\n", strm') => strm'
33 
                            | _ => strm
34 
 
35 
      fun go strm = let in
36 
          case readSegment strm
37 
          of NONE => (SIO.closeIn strm; [])
38 
           | SOME (s, strm') => s :: go (skipDelim strm')
39 
        end
40 
    in
41 
      go (TIO.getInstream (TIO.openIn filename))
42 
    end
43 
 
44 
  fun parseTrans env tstr = let
45 
 
46 
      fun notNewline c = (c <> #"\n")
47 43 tbourke 
      fun expandTypes (E.BoundId (s,ty)) = E.BoundId(s,Env.expandTyIds (env,ty))
48 4 tbourke 
 
49 
      val (selstr, rest)     = SS.splitl notNewline (SS.full tstr)
50 
      val (actstr, guardstr) = SS.splitl notNewline (SS.triml 1 rest)
51 
 
52 
      (*val _ = TextIO.print "Parsing transition:select:"*)
53 
      val select     = if SS.isEmpty selstr then []
54 
                       else valOf (UP.parseSelect testName (SS.string selstr))
55 
      (*val _ = TextIO.print "sync:"*)
56 
      val (channame, subscripts) =
57 
                       case UP.parseSync testName (SS.string actstr) of
58 
                          NONE             => (Atom.atom "c", [])
59 
                        | SOME (nm, _, sl) => (nm, sl)
60 
      (*val _ = TextIO.print "guard:"*)
61 
      val guard      = valOf (UP.parseExpression testName (SS.string guardstr))
62 
      (*val _ = TextIO.print "\n"*)
63 
 
64 
    in
65 
      SOME (channame, {selectids=map expandTypes select,
66 
                       actionsubs=subscripts,
67 
                       guard=guard})
68 
    end
69 
    handle Option => NONE
70 
 
71 
  fun readTest filename = let
72 
      val (comments::decls::trans) = case readSegments filename
73 
          of all as (_::_::_) => all
74 
           | _ => Util.abort [filename, " does not contain enough sections."]
75 
      val env = case UP.parseDeclarations testName decls of
76 
                   NONE       => Util.abort ["bad declarations: ", filename]
77 
                 | SOME decls => Env.addDeclarations (Env.base_env,
78 
                                                      Env.GlobalScope, decls)
79 
      val trans = List.mapPartial (parseTrans env) trans
80 
 
81 
    in (env, comments, decls, trans) end
82 
    handle Bind => Util.abort ["bad test file: ", filename]
83 
 
84 
  fun checkName ((nm, tr), NONE)          = SOME (nm, [tr])
85 
    | checkName ((nm, tr), SOME (n, trs)) =
86 
        if Atom.compare (n, nm) = EQUAL
87 
        then SOME (nm, tr::trs)
88 
        else Util.abort ["Channel names are inconsistent: ",
89 
                         Atom.toString n, " <> ", Atom.toString nm]
90 
 
91 
  fun runTest {input, output=ostrm} = let
92 
      val (env, comment, decls, nmtrans) = readTest input
93 
      fun print s = TextIO.output (ostrm, s)
94 
 
95 
      val (transtysop, trans) = case foldl checkName NONE nmtrans
96 
           of NONE             => (TF.chanToSubRanges (env, Atom.atom "c"), [])
97 
              (* default to a channel named "c" if no transitions are given *)
98 
            | SOME (nm, trans) => (TF.chanToSubRanges (env, nm), rev trans)
99 
      val transtys = case transtysop
100 
                    of NONE     => []
101 
                     | SOME tys => tys
102 
      val _ = print comment
103 
      val _ = print "--------------------\n"
104 
      val _ = print decls
105 
      val _ = print "--------------------\nBEFORE:\n"
106 
      val _ = app (print o TF.toString) trans
107 
      val _ = print "\n--------------------\nAFTER:\n"
108 
      val trans' = TF.negateTransitions env (transtys, trans, E.trueExpr)
109 
      val _ = app (print o TF.toString) trans'
110 
      val _ = print "\n--------------------\n"
111 
    in OS.Process.success end
112 
    handle Env.DuplicateDefinition s =>
113 
                (Util.abort ["duplicate definition: ", s, "\n"])
114 
         | TF.FlipFailed reason => (Util.abort ["flip failed: ", reason, "\n"])
115 
         | e => (Util.abort ["exception: ", General.exnMessage e, "\n"])
116 
  end (* local *)
117 
end
118