Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
291   895   142   2.33
24   713   0.49   125
125     1.14  
1    
 
  QedeqNotNullTraverserTest       Line # 98 291 142 22.7% 0.22727273
 
  (7)
 
1    /* This file is part of the project "Hilbert II" - http://www.qedeq.org
2    *
3    * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
4    *
5    * "Hilbert II" is free software; you can redistribute
6    * it and/or modify it under the terms of the GNU General Public
7    * License as published by the Free Software Foundation; either
8    * version 2 of the License, or (at your option) any later version.
9    *
10    * This program is distributed in the hope that it will be useful,
11    * but WITHOUT ANY WARRANTY; without even the implied warranty of
12    * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13    * GNU General Public License for more details.
14    */
15   
16    package org.qedeq.kernel.se.visitor;
17   
18    import java.io.ByteArrayOutputStream;
19    import java.io.IOException;
20    import java.lang.reflect.InvocationTargetException;
21    import java.lang.reflect.Method;
22    import java.util.List;
23    import java.util.Stack;
24   
25    import org.qedeq.base.io.TextOutput;
26    import org.qedeq.base.test.QedeqTestCase;
27    import org.qedeq.base.trace.Trace;
28    import org.qedeq.kernel.se.base.list.Atom;
29    import org.qedeq.kernel.se.base.list.Element;
30    import org.qedeq.kernel.se.base.list.ElementList;
31    import org.qedeq.kernel.se.base.module.Add;
32    import org.qedeq.kernel.se.base.module.Author;
33    import org.qedeq.kernel.se.base.module.AuthorList;
34    import org.qedeq.kernel.se.base.module.Axiom;
35    import org.qedeq.kernel.se.base.module.ChangedRule;
36    import org.qedeq.kernel.se.base.module.ChangedRuleList;
37    import org.qedeq.kernel.se.base.module.Chapter;
38    import org.qedeq.kernel.se.base.module.ChapterList;
39    import org.qedeq.kernel.se.base.module.Conclusion;
40    import org.qedeq.kernel.se.base.module.ConditionalProof;
41    import org.qedeq.kernel.se.base.module.Existential;
42    import org.qedeq.kernel.se.base.module.FormalProof;
43    import org.qedeq.kernel.se.base.module.FormalProofLine;
44    import org.qedeq.kernel.se.base.module.FormalProofLineList;
45    import org.qedeq.kernel.se.base.module.FormalProofList;
46    import org.qedeq.kernel.se.base.module.Formula;
47    import org.qedeq.kernel.se.base.module.FunctionDefinition;
48    import org.qedeq.kernel.se.base.module.Header;
49    import org.qedeq.kernel.se.base.module.Hypothesis;
50    import org.qedeq.kernel.se.base.module.Import;
51    import org.qedeq.kernel.se.base.module.ImportList;
52    import org.qedeq.kernel.se.base.module.InitialFunctionDefinition;
53    import org.qedeq.kernel.se.base.module.InitialPredicateDefinition;
54    import org.qedeq.kernel.se.base.module.Latex;
55    import org.qedeq.kernel.se.base.module.LatexList;
56    import org.qedeq.kernel.se.base.module.LinkList;
57    import org.qedeq.kernel.se.base.module.LiteratureItem;
58    import org.qedeq.kernel.se.base.module.LiteratureItemList;
59    import org.qedeq.kernel.se.base.module.Location;
60    import org.qedeq.kernel.se.base.module.LocationList;
61    import org.qedeq.kernel.se.base.module.ModusPonens;
62    import org.qedeq.kernel.se.base.module.Node;
63    import org.qedeq.kernel.se.base.module.PredicateDefinition;
64    import org.qedeq.kernel.se.base.module.Proof;
65    import org.qedeq.kernel.se.base.module.ProofList;
66    import org.qedeq.kernel.se.base.module.Proposition;
67    import org.qedeq.kernel.se.base.module.Qedeq;
68    import org.qedeq.kernel.se.base.module.Reason;
69    import org.qedeq.kernel.se.base.module.Rename;
70    import org.qedeq.kernel.se.base.module.Rule;
71    import org.qedeq.kernel.se.base.module.Section;
72    import org.qedeq.kernel.se.base.module.SectionList;
73    import org.qedeq.kernel.se.base.module.Specification;
74    import org.qedeq.kernel.se.base.module.Subsection;
75    import org.qedeq.kernel.se.base.module.SubsectionList;
76    import org.qedeq.kernel.se.base.module.SubsectionType;
77    import org.qedeq.kernel.se.base.module.SubstFree;
78    import org.qedeq.kernel.se.base.module.SubstFunc;
79    import org.qedeq.kernel.se.base.module.SubstPred;
80    import org.qedeq.kernel.se.base.module.Term;
81    import org.qedeq.kernel.se.base.module.Universal;
82    import org.qedeq.kernel.se.base.module.UsedByList;
83    import org.qedeq.kernel.se.common.DefaultModuleAddress;
84    import org.qedeq.kernel.se.common.ModuleAddress;
85    import org.qedeq.kernel.se.common.ModuleDataException;
86    import org.qedeq.kernel.se.dto.list.DefaultAtom;
87    import org.qedeq.kernel.se.dto.list.DefaultElementList;
88    import org.qedeq.kernel.se.test.QedeqVoCreator;
89   
90    /**
91    * Test visitor concept for {@link org.qedeq.kernel.visitor.QedeqVisitor}.
92    * This class doesn't test much existing code directly, but checks that the
93    * {@link QedeqNotNullTraverser} works correctly for
94    * the list part.
95    *
96    * @author Michael Meyling
97    */
 
98    public class QedeqNotNullTraverserTest extends QedeqTestCase {
99   
100    /** This class. */
101    private static final Class CLASS = QedeqNotNullTraverserTest.class;
102   
103    private final ByteArrayOutputStream out = new ByteArrayOutputStream();
104   
105    private final TextOutput text = new TextOutput("local", out, "UTF-8");
106   
107    // private final TextOutput text = new TextOutput("local", new PrintStream(System.out));
108   
109    private final Stack stack = new Stack();
110   
111    private static ModuleAddress address;
112   
 
113  2 toggle static {
114  2 try {
115  2 address = new DefaultModuleAddress("http://memory.org/sample.xml");
116    } catch (IOException e) {
117  0 e.printStackTrace();
118    }
119    }
120   
121    private final QedeqVisitor visitor = new AbstractModuleVisitor() {
122   
 
123  19 toggle public void visitEnter(Atom atom) {
124  19 handleComma();
125  19 text.print("\"");
126  19 text.print(atom.getString());
127    }
128   
 
129  19 toggle public void visitLeave(Atom atom) {
130  19 text.print("\"");
131    }
132   
 
133  21 toggle public void visitEnter(ElementList list) {
134  21 handleComma();
135  21 text.print(list.getOperator() + "(");
136  21 stack.push(Boolean.FALSE);
137    }
138   
 
139  21 toggle public void visitLeave(ElementList list) {
140  21 text.print(")");
141  21 stack.pop();
142    }
143   
 
144  40 toggle private void handleComma() {
145  40 if (!stack.isEmpty() && ((Boolean) stack.peek()).booleanValue()) {
146  17 text.print(", ");
147    } else {
148  23 if (!stack.isEmpty()) {
149  21 stack.pop();
150  21 stack.push(Boolean.TRUE);
151    }
152    }
153    }
154   
155    };
156   
157    private final QedeqNotNullTraverser trans = new QedeqNotNullTraverser(address,
158    visitor);
159   
160    /**
161    * Test visitor concept.
162    */
 
163  1 toggle public void testVisit() throws Exception {
164  1 Element el = new DefaultElementList("myOperator", new Element[] {
165    new DefaultAtom("Hello"),
166    new DefaultAtom("Again"),
167    new DefaultElementList("again", new Element[] {
168    new DefaultAtom("one"),
169    new DefaultAtom("two"),
170    new DefaultAtom("three")
171    })
172    });
173   
174  1 trans.accept(el);
175  1 Trace.trace(CLASS, this, "testVisit", out.toString("ISO-8859-1"));
176  1 assertEquals("myOperator(\"Hello\", \"Again\", again(\"one\", \"two\", \"three\"))",
177    out.toString("ISO-8859-1"));
178    }
179   
180    /**
181    * Test generation.
182    */
 
183  1 toggle public void testGeneration() throws Exception {
184  1 Element el = new DefaultElementList("EQUI", new Element[] {
185    new DefaultElementList("PREDCON", new Element[] {
186    new DefaultAtom("equal"),
187    new DefaultElementList("VAR", new Element[] {
188    new DefaultAtom("y"),
189    }),
190    new DefaultElementList("CLASS", new Element[] {
191    new DefaultElementList("VAR", new Element[] {
192    new DefaultAtom("x"),
193    }),
194    new DefaultElementList("PREDVAR", new Element[] {
195    new DefaultAtom("\\phi"),
196    new DefaultElementList("VAR", new Element[] {
197    new DefaultAtom("x"),
198    })
199    })
200    })
201    }),
202    new DefaultElementList("FORALL", new Element[] {
203    new DefaultElementList("VAR", new Element[] {
204    new DefaultAtom("z"),
205    }),
206    new DefaultElementList("EQUI", new Element[] {
207    new DefaultElementList("PREDCON", new Element[] {
208    new DefaultAtom("in"),
209    new DefaultElementList("VAR", new Element[] {
210    new DefaultAtom("z"),
211    }),
212    new DefaultElementList("VAR", new Element[] {
213    new DefaultAtom("y"),
214    })
215    }),
216    new DefaultElementList("PREDCON", new Element[] {
217    new DefaultAtom("in"),
218    new DefaultElementList("VAR", new Element[] {
219    new DefaultAtom("z"),
220    }),
221    new DefaultElementList("CLASS", new Element[] {
222    new DefaultElementList("VAR", new Element[] {
223    new DefaultAtom("x"),
224    }),
225    new DefaultElementList("PREDVAR", new Element[] {
226    new DefaultAtom("\\phi"),
227    new DefaultElementList("VAR", new Element[] {
228    new DefaultAtom("x"),
229    })
230    })
231    })
232    })
233    })
234    })
235    });
236  1 trans.accept(el);
237  1 Trace.trace(CLASS, this, "testGeneration", out.toString("ISO-8859-1"));
238  1 assertEquals("EQUI(PREDCON(\"equal\", VAR(\"y\"), CLASS(VAR(\"x\"), PREDVAR(\"\\phi\","
239    + " VAR(\"x\")))), FORALL(VAR(\"z\"), EQUI(PREDCON(\"in\", VAR(\"z\"), VAR(\"y\")),"
240    + " PREDCON(\"in\", VAR(\"z\"), CLASS(VAR(\"x\"), PREDVAR(\"\\phi\", VAR(\"x\")))))))",
241    out.toString("ISO-8859-1"));
242  1 Trace.trace(CLASS, this, "testGeneration", el.toString());
243    }
244   
 
245  6 toggle protected void setUp() throws Exception {
246  6 super.setUp();
247  6 out.reset();
248    }
249   
 
250  6 toggle protected void tearDown() throws Exception {
251  6 super.tearDown();
252    }
253   
254    private final QedeqVisitor visitor2 = new QedeqVisitor() {
255   
 
256  0 toggle public void visitEnter(Atom atom) {
257  0 handleComma();
258  0 text.print("\"");
259  0 text.print(atom.getString());
260    }
261   
 
262  0 toggle public void visitLeave(Atom atom) {
263  0 text.print("\"");
264    }
265   
 
266  0 toggle public void visitEnter(ElementList list) {
267  0 handleComma();
268  0 text.print(list.getOperator() + "(");
269  0 stack.push(Boolean.FALSE);
270    }
271   
 
272  0 toggle public void visitLeave(ElementList list) {
273  0 text.print(")");
274  0 stack.pop();
275    }
276   
 
277  0 toggle private void handleComma() {
278  0 if (!stack.isEmpty() && ((Boolean) stack.peek()).booleanValue()) {
279  0 text.print(", ");
280    } else {
281  0 if (!stack.isEmpty()) {
282  0 stack.pop();
283  0 stack.push(Boolean.TRUE);
284    }
285    }
286    }
287   
 
288  0 toggle public void visitEnter(Author author) {
289  0 text.println("<author email=\"" + author.getEmail() + "\">");
290  0 text.pushLevel();
291    }
292   
 
293  0 toggle public void visitEnter(AuthorList authorList) {
294  0 text.println("<authorlist>");
295  0 text.pushLevel();
296    }
297   
 
298  0 toggle public void visitEnter(Axiom axiom) {
299  0 text.println("<axiom>");
300  0 text.pushLevel();
301    }
302   
 
303  0 toggle public void visitEnter(Chapter chapter) {
304  0 text.println("<chapter>");
305  0 text.pushLevel();
306    }
307   
 
308  0 toggle public void visitEnter(ChapterList chapterList) {
309  0 text.println("<chapterlist>");
310  0 text.pushLevel();
311    }
312   
 
313  0 toggle public void visitEnter(Formula formula) {
314  0 text.println("<formula>");
315  0 text.pushLevel();
316    }
317   
 
318  0 toggle public void visitEnter(InitialFunctionDefinition functionDefinition) {
319  0 text.println("<initialfunctiondefinition>");
320  0 text.pushLevel();
321    }
322   
 
323  0 toggle public void visitEnter(FunctionDefinition functionDefinition) {
324  0 text.println("<functiondefinition>");
325  0 text.pushLevel();
326    }
327   
 
328  0 toggle public void visitEnter(Header header) {
329  0 text.println("<header>");
330  0 text.pushLevel();
331    }
332   
 
333  0 toggle public void visitEnter(Import imp) {
334  0 text.println("<import>");
335  0 text.pushLevel();
336    }
337   
 
338  0 toggle public void visitEnter(ImportList importList) {
339  0 text.println("<importlist>");
340  0 text.pushLevel();
341    }
342   
 
343  0 toggle public void visitEnter(Latex latex) {
344  0 text.println("<latex>");
345  0 text.pushLevel();
346    }
347   
 
348  0 toggle public void visitEnter(LatexList latexList) {
349  0 text.println("<latexlist>");
350  0 text.pushLevel();
351    }
352   
 
353  0 toggle public void visitEnter(LinkList linkList) {
354  0 text.println("<linklist>");
355  0 text.pushLevel();
356    }
357   
 
358  0 toggle public void visitEnter(LiteratureItem literatureItem) {
359  0 text.println("<literatureitem>");
360  0 text.pushLevel();
361    }
362   
 
363  0 toggle public void visitEnter(LiteratureItemList literatureItemList) {
364  0 text.println("<literatureitemlist>");
365  0 text.pushLevel();
366    }
367   
 
368  0 toggle public void visitEnter(Location location) {
369  0 text.println("<location>");
370  0 text.pushLevel();
371    }
372   
 
373  0 toggle public void visitEnter(LocationList locationList) {
374  0 text.println("<locationlist>");
375  0 text.pushLevel();
376    }
377   
 
378  0 toggle public void visitEnter(Node node) {
379  0 text.println("<node>");
380  0 text.pushLevel();
381    }
382   
 
383  0 toggle public void visitEnter(InitialPredicateDefinition predicateDefinition) {
384  0 text.println("<initialpredicatedefinition>");
385  0 text.pushLevel();
386    }
387   
 
388  0 toggle public void visitEnter(PredicateDefinition predicateDefinition) {
389  0 text.println("<predicatedefinition>");
390  0 text.pushLevel();
391    }
392   
 
393  0 toggle public void visitEnter(FormalProof proof) {
394  0 text.println("<formalproof>");
395  0 text.pushLevel();
396    }
397   
 
398  0 toggle public void visitEnter(FormalProofList proofList) {
399  0 text.println("<formalprooflist>");
400  0 text.pushLevel();
401    }
402   
 
403  0 toggle public void visitEnter(FormalProofLine proofLine) {
404  0 text.println("<formalproofline>");
405  0 text.pushLevel();
406    }
407   
 
408  0 toggle public void visitEnter(Reason reason) {
409  0 text.println("<reason>");
410  0 text.pushLevel();
411    }
412   
 
413  0 toggle public void visitEnter(ModusPonens reason) {
414  0 text.println("<modusponens>");
415  0 text.pushLevel();
416    }
417   
 
418  0 toggle public void visitEnter(Add reason) {
419  0 text.println("<add>");
420  0 text.pushLevel();
421    }
422   
 
423  0 toggle public void visitEnter(Rename reason) {
424  0 text.println("<rename>");
425  0 text.pushLevel();
426    }
427   
 
428  0 toggle public void visitEnter(SubstFree reason) {
429  0 text.println("<substfree>");
430  0 text.pushLevel();
431    }
432   
 
433  0 toggle public void visitEnter(SubstFunc reason) {
434  0 text.println("<substfunc>");
435  0 text.pushLevel();
436    }
437   
 
438  0 toggle public void visitEnter(SubstPred reason) {
439  0 text.println("<substpred>");
440  0 text.pushLevel();
441    }
442   
 
443  0 toggle public void visitEnter(Existential reason) {
444  0 text.println("<existential>");
445  0 text.pushLevel();
446    }
447   
 
448  0 toggle public void visitEnter(Universal reason) {
449  0 text.println("<universal>");
450  0 text.pushLevel();
451    }
452   
 
453  0 toggle public void visitEnter(ConditionalProof reason) {
454  0 text.println("<conditionalproof>");
455  0 text.pushLevel();
456    }
457   
 
458  0 toggle public void visitEnter(Hypothesis hypothesis) {
459  0 text.println("<hypothesis>");
460  0 text.pushLevel();
461    }
462   
 
463  0 toggle public void visitEnter(Conclusion conclusion) {
464  0 text.println("<conclusion>");
465  0 text.pushLevel();
466    }
467   
 
468  0 toggle public void visitEnter(FormalProofLineList proofLineList) {
469  0 text.println("<formalprooflinelist>");
470  0 text.pushLevel();
471    }
472   
 
473  0 toggle public void visitEnter(Proof proof) {
474  0 text.println("<proof>");
475  0 text.pushLevel();
476    }
477   
 
478  0 toggle public void visitEnter(ProofList proofList) {
479  0 text.println("<prooflist>");
480  0 text.pushLevel();
481    }
482   
 
483  0 toggle public void visitEnter(Proposition proposition) {
484  0 text.println("<proposition>");
485  0 text.pushLevel();
486    }
487   
 
488  0 toggle public void visitEnter(Qedeq qedeq) {
489  0 text.println("<qedeq>");
490  0 text.pushLevel();
491    }
492   
 
493  0 toggle public void visitEnter(Rule rule) {
494  0 text.println("<rule>");
495  0 text.pushLevel();
496    }
497   
 
498  0 toggle public void visitEnter(ChangedRuleList list) {
499  0 text.println("<changedrulelist>");
500  0 text.pushLevel();
501    }
502   
 
503  0 toggle public void visitEnter(ChangedRule rule) {
504  0 text.println("<changedrule>");
505  0 text.pushLevel();
506    }
507   
 
508  0 toggle public void visitEnter(Section section) {
509  0 text.println("<section>");
510  0 text.pushLevel();
511    }
512   
 
513  0 toggle public void visitEnter(SectionList sectionList) {
514  0 text.println("<sectionlist>");
515  0 text.pushLevel();
516    }
517   
 
518  0 toggle public void visitEnter(Specification specification) {
519  0 text.println("<specification>");
520  0 text.pushLevel();
521    }
522   
 
523  0 toggle public void visitEnter(Subsection subsection) {
524  0 text.println("<subsection>");
525  0 text.pushLevel();
526    }
527   
 
528  0 toggle public void visitEnter(SubsectionList subsectionList) {
529  0 text.println("<subsectionlist>");
530  0 text.pushLevel();
531    }
532   
 
533  0 toggle public void visitEnter(SubsectionType subsectionType) {
534  0 text.println("<subsectiontype>");
535  0 text.pushLevel();
536    }
537   
 
538  0 toggle public void visitEnter(Term term) {
539  0 text.println("<term>");
540  0 text.pushLevel();
541    }
542   
 
543  0 toggle public void visitEnter(UsedByList usedByList) {
544  0 text.println("<usedbylist>");
545  0 text.pushLevel();
546    }
547   
 
548  0 toggle public void visitLeave(Author author) throws ModuleDataException {
549  0 text.popLevel();
550  0 text.println("</author>");
551    }
552   
 
553  0 toggle public void visitLeave(AuthorList authorList) {
554  0 text.popLevel();
555  0 text.println("</authorlist>");
556    }
557   
 
558  0 toggle public void visitLeave(Axiom axiom) {
559  0 text.popLevel();
560  0 text.println("</axiom>");
561    }
562   
 
563  0 toggle public void visitLeave(Chapter chapter) {
564  0 text.popLevel();
565  0 text.println("</chapter>");
566    }
567   
 
568  0 toggle public void visitLeave(ChapterList chapterList) {
569  0 text.popLevel();
570  0 text.println("</chapterlist>");
571    }
572   
 
573  0 toggle public void visitLeave(Formula formula) {
574  0 text.popLevel();
575  0 text.println("</formula>");
576    }
577   
 
578  0 toggle public void visitLeave(InitialFunctionDefinition functionDefinition) {
579  0 text.popLevel();
580  0 text.println("</initialfunctiondefinition>");
581    }
582   
 
583  0 toggle public void visitLeave(FunctionDefinition functionDefinition) {
584  0 text.popLevel();
585  0 text.println("</functiondefinition>");
586    }
587   
 
588  0 toggle public void visitLeave(Header header) {
589  0 text.popLevel();
590  0 text.println("</header>");
591    }
592   
 
593  0 toggle public void visitLeave(Import imp) {
594  0 text.popLevel();
595  0 text.println("</import>");
596    }
597   
 
598  0 toggle public void visitLeave(ImportList importList) {
599  0 text.popLevel();
600  0 text.println("</importlist>");
601    }
602   
 
603  0 toggle public void visitLeave(Latex latex) {
604  0 text.popLevel();
605  0 text.println("</latex>");
606    }
607   
 
608  0 toggle public void visitLeave(LatexList latexList) {
609  0 text.popLevel();
610  0 text.println("</latexlist>");
611    }
612   
 
613  0 toggle public void visitLeave(LinkList linkList) {
614  0 text.popLevel();
615  0 text.println("</linklist>");
616    }
617   
 
618  0 toggle public void visitLeave(LiteratureItem literatureItem) {
619  0 text.popLevel();
620  0 text.println("</literatureitem>");
621    }
622   
 
623  0 toggle public void visitLeave(LiteratureItemList literatureItemList) {
624  0 text.popLevel();
625  0 text.println("</literatureitemlist>");
626    }
627   
 
628  0 toggle public void visitLeave(Location location) {
629  0 text.popLevel();
630  0 text.println("</location>");
631    }
632   
 
633  0 toggle public void visitLeave(LocationList locationList) {
634  0 text.popLevel();
635  0 text.println("</locationlist>");
636    }
637   
 
638  0 toggle public void visitLeave(Node node) {
639  0 text.popLevel();
640  0 text.println("</node>");
641    }
642   
 
643  0 toggle public void visitLeave(InitialPredicateDefinition predicateDefinition) {
644  0 text.popLevel();
645  0 text.println("</initialpredicatedefinition>");
646    }
647   
 
648  0 toggle public void visitLeave(PredicateDefinition predicateDefinition) {
649  0 text.popLevel();
650  0 text.println("</predicatedefinition>");
651    }
652   
 
653  0 toggle public void visitLeave(FormalProofList proofList) {
654  0 text.popLevel();
655  0 text.println("</formalproofList>");
656    }
657   
 
658  0 toggle public void visitLeave(FormalProof proof) {
659  0 text.popLevel();
660  0 text.println("</proof>");
661    }
662   
 
663  0 toggle public void visitLeave(FormalProofLine proofLine) {
664  0 text.popLevel();
665  0 text.println("</formalproofline>");
666    }
667   
 
668  0 toggle public void visitLeave(Reason reason) {
669  0 text.popLevel();
670  0 text.println("</reason>");
671    }
672   
 
673  0 toggle public void visitLeave(FormalProofLineList proofLineList) {
674  0 text.popLevel();
675  0 text.println("</formalprooflinelist>");
676    }
677   
 
678  0 toggle public void visitLeave(ModusPonens reason) {
679  0 text.popLevel();
680  0 text.println("</modulsponens>");
681    }
682   
 
683  0 toggle public void visitLeave(Add reason) {
684  0 text.popLevel();
685  0 text.println("</add>");
686    }
687   
 
688  0 toggle public void visitLeave(Rename reason) {
689  0 text.popLevel();
690  0 text.println("</rename>");
691    }
692   
 
693  0 toggle public void visitLeave(SubstFree reason) {
694  0 text.popLevel();
695  0 text.println("</substfree>");
696    }
697   
 
698  0 toggle public void visitLeave(SubstFunc reason) {
699  0 text.popLevel();
700  0 text.println("</substfunc>");
701    }
702   
 
703  0 toggle public void visitLeave(SubstPred reason) {
704  0 text.popLevel();
705  0 text.println("</substpred>");
706    }
707   
 
708  0 toggle public void visitLeave(Existential reason) {
709  0 text.popLevel();
710  0 text.println("</existential>");
711    }
712   
 
713  0 toggle public void visitLeave(Universal reason) {
714  0 text.popLevel();
715  0 text.println("</universal>");
716    }
717   
 
718  0 toggle public void visitLeave(ConditionalProof reason) {
719  0 text.popLevel();
720  0 text.println("</conditionalproof>");
721    }
722   
 
723  0 toggle public void visitLeave(Hypothesis hypothesis) {
724  0 text.popLevel();
725  0 text.println("</hypothesis>");
726    }
727   
 
728  0 toggle public void visitLeave(Conclusion conclusion) {
729  0 text.popLevel();
730  0 text.println("</conclusion>");
731    }
732   
 
733  0 toggle public void visitLeave(Proof proof) {
734  0 text.popLevel();
735  0 text.println("</proof>");
736    }
737   
 
738  0 toggle public void visitLeave(ProofList proofList) {
739  0 text.popLevel();
740  0 text.println("</prooflist>");
741    }
742   
 
743  0 toggle public void visitLeave(Proposition proposition) {
744  0 text.popLevel();
745  0 text.println("</proposition>");
746    }
747   
 
748  0 toggle public void visitLeave(Qedeq qedeq) {
749  0 text.popLevel();
750  0 text.println("</qedeq>");
751    }
752   
 
753  0 toggle public void visitLeave(Rule rule) {
754  0 text.popLevel();
755  0 text.println("</rule>");
756    }
757   
 
758  0 toggle public void visitLeave(ChangedRuleList list) {
759  0 text.popLevel();
760  0 text.println("</changedrulelist>");
761    }
762   
 
763  0 toggle public void visitLeave(ChangedRule rule) {
764  0 text.popLevel();
765  0 text.println("</changedrule>");
766    }
767   
 
768  0 toggle public void visitLeave(Section section) {
769  0 text.popLevel();
770  0 text.println("</section>");
771    }
772   
 
773  0 toggle public void visitLeave(SectionList sectionList) {
774  0 text.popLevel();
775  0 text.println("</sectionlist>");
776    }
777   
 
778  0 toggle public void visitLeave(Specification specification) {
779  0 text.popLevel();
780  0 text.println("</specification>");
781    }
782   
 
783  0 toggle public void visitLeave(Subsection subsection) {
784  0 text.popLevel();
785  0 text.println("</subsection>");
786    }
787   
 
788  0 toggle public void visitLeave(SubsectionList subsectionList) {
789  0 text.popLevel();
790  0 text.println("</subsectionlist>");
791    }
792   
 
793  0 toggle public void visitLeave(SubsectionType subsectionType) {
794  0 text.popLevel();
795  0 text.println("</subsectiontype>");
796    }
797   
 
798  0 toggle public void visitLeave(Term term) {
799  0 text.popLevel();
800  0 text.println("</term>");
801    }
802   
 
803  0 toggle public void visitLeave(UsedByList usedByList) {
804  0 text.popLevel();
805  0 text.println("</usedbylist>");
806    }
807   
808    };
809   
 
810  1 toggle public void testQedeq() throws Exception {
811    // QedeqNotNullTraverser trans2 = new QedeqNotNullTraverser(address,
812    // visitor2);
813  1 final QedeqNotNullTraverser trans2 = new QedeqNotNullTraverser(address);
814  1 ;
815  1 final QedeqVisitorTester testVisitor = new QedeqVisitorTester(trans2) {
 
816  1429 toggle public void checkEnter() {
817    // super.checkEnter();
818    // System.out.println(">" + getContext());
819    // System.out.println(")" + trans2.getCurrentContext().getLocationWithinModule());
820  1429 assertEquals(trans2.getCurrentContext().getLocationWithinModule(), getContext());
821    }
 
822  1429 toggle public void checkLeave() {
823    // super.checkLeave();
824    // System.out.println("(" + getContext());
825  1429 assertEquals(trans2.getCurrentContext().getLocationWithinModule(), getContext());
826    }
827    };
828  1 trans2.setVisitor(testVisitor);
829  1 final List list = new QedeqVoCreator().create();
830  153 for (int i = 0; i < list.size(); i++) {
831    // System.out.print(qedeq);
832    // System.out.println();
833    // System.out.println(out.toString("UTF-8"));
834  152 trans2.accept((Qedeq) list.get(i));
835  152 assertEquals(0, testVisitor.getLevel());
836    }
837    }
838   
839   
 
840  1 toggle public void testQedeq2() throws Exception {
841  1 QedeqNotNullTraverser trans2 = new QedeqNotNullTraverser(address,
842    visitor2);
843  1 try {
844  1 trans2.accept((Qedeq) null);
845  0 fail("Execption expected");
846    } catch (Exception e) {
847    // ok
848    }
849    }
850   
 
851  1 toggle public void testAcceptors1() throws Exception {
852  1 QedeqNotNullTraverser trans2 = new QedeqNotNullTraverser(address,
853    visitor2);
854  1 final Method[] methods = trans2.getClass().getMethods();
855  74 for (int i = 0; i < methods.length; i++) {
856  73 final Method method = methods[i];
857  73 if (!"accept".equals(method.getName())) {
858  19 continue;
859    }
860  54 assertEquals(1, method.getParameterTypes().length);
861  54 if (Qedeq.class == method.getParameterTypes()[0]) {
862  1 continue;
863    }
864  53 method.invoke(trans2, new Object[] {null });
865    }
866    }
867   
 
868  1 toggle public void testAcceptors2() throws Throwable {
869  1 QedeqNotNullTraverser trans2 = new QedeqNotNullTraverser(address,
870    visitor2);
871  1 final Method[] methods = trans2.getClass().getMethods();
872  74 for (int i = 0; i < methods.length; i++) {
873  73 final Method method = methods[i];
874  73 if (!"accept".equals(method.getName())) {
875  19 continue;
876    }
877  54 assertEquals(1, method.getParameterTypes().length);
878  54 if (Qedeq.class == method.getParameterTypes()[0]) {
879  1 continue;
880    }
881  53 Thread.currentThread().interrupt();
882  53 try {
883  53 method.invoke(trans2, new Object[] {null });
884  0 fail("Exception expected");
885    } catch (InvocationTargetException e) {
886  53 if (e.getCause() instanceof InterruptException) {
887    // ok
888    } else {
889  0 throw e.getCause();
890    }
891    }
892  53 assertFalse(Thread.interrupted());
893    }
894    }
895    }