// This file was generated by jmlunit on Mon Mar 16 13:16:28 EDT 2009. package org.jmlspecs.samples.digraph; import java.util.*; import java.awt.Color; /** Automatically-generated test driver for JML and JUnit based * testing of SearchableDigraph. The superclass of this class should be edited * to supply test data. However it's best not to edit this class * directly; instead use the command *
* jmlunit SearchableDigraph.java ** to regenerate this class whenever SearchableDigraph.java changes. */ public class SearchableDigraph_JML_Test extends SearchableDigraph_JML_TestData { /** Initialize this class. */ public SearchableDigraph_JML_Test(java.lang.String name) { super(name); } /** Run the tests. */ public static void main(java.lang.String[] args) { org.jmlspecs.jmlunit.JMLTestRunner.run(suite()); // You can also use a JUnit test runner such as: // junit.textui.TestRunner.run(suite()); } /** Test to see if the code for class SearchableDigraph * has been compiled with runtime assertion checking (i.e., by jmlc). * Code that is not compiled with jmlc would not make an effective test, * since no assertion checking would be done. */ public void test$IsRACCompiled() { junit.framework.Assert.assertTrue("code for class SearchableDigraph" + " was not compiled with jmlc" + " so no assertions will be checked!", org.jmlspecs.jmlrac.runtime.JMLChecker.isRACCompiled(SearchableDigraph.class) ); } /** Return the test suite for this test class. This will have * added to it at least test$IsRACCompiled(), and any test methods * written explicitly by the user in the superclass. It will also * have added test suites for each testing each method and * constructor. */ //@ ensures \result != null; public static junit.framework.Test suite() { SearchableDigraph_JML_Test testobj = new SearchableDigraph_JML_Test("SearchableDigraph_JML_Test"); junit.framework.TestSuite testsuite = testobj.overallTestSuite(); // Add instances of Test found by the reflection mechanism. testsuite.addTestSuite(SearchableDigraph_JML_Test.class); testobj.addTestSuiteForEachMethod(testsuite); return testsuite; } /** A JUnit test object that can run a single test method. This * is defined as a nested class solely for convenience; it can't * be defined once and for all because it must subclass its * enclosing class. */ protected static abstract class OneTest extends SearchableDigraph_JML_Test { /** Initialize this test object. */ public OneTest(String name) { super(name); } /** The result object that holds information about testing. */ protected junit.framework.TestResult result; //@ also //@ requires result != null; public void run(junit.framework.TestResult result) { this.result = result; super.run(result); } /* Run a single test and decide whether the test was * successful, meaningless, or a failure. This is the * Template Method pattern abstraction of the inner loop in a * JML/JUnit test. */ public void runTest() throws java.lang.Throwable { try { // The call being tested! doCall(); } catch (org.jmlspecs.jmlrac.runtime.JMLEntryPreconditionError e) { // meaningless test input addMeaningless(); } catch (org.jmlspecs.jmlrac.runtime.JMLAssertionError e) { // test failure int l = org.jmlspecs.jmlrac.runtime.JMLChecker.getLevel(); org.jmlspecs.jmlrac.runtime.JMLChecker.setLevel (org.jmlspecs.jmlrac.runtime.JMLOption.NONE); try { java.lang.String failmsg = this.failMessage(e); junit.framework.AssertionFailedError err = new junit.framework.AssertionFailedError(failmsg); err.setStackTrace(new java.lang.StackTraceElement[]{}); err.initCause(e); result.addFailure(this, err); } finally { org.jmlspecs.jmlrac.runtime.JMLChecker.setLevel(l); } } catch (java.lang.Throwable e) { // test success } } /** Call the method to be tested with the appropriate arguments. */ protected abstract void doCall() throws java.lang.Throwable; /** Format the error message for a test failure, based on the * method's arguments. */ protected abstract java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e); /** Inform listeners that a meaningless test was run. */ private void addMeaningless() { if (result instanceof org.jmlspecs.jmlunit.JMLTestResult) { ((org.jmlspecs.jmlunit.JMLTestResult)result) .addMeaningless(this); } } } /** Create the tests that are to be run for testing the class * SearchableDigraph. The framework will then run them. * @param overallTestSuite$ The suite accumulating all of the tests * for this driver class. */ //@ requires overallTestSuite$ != null; public void addTestSuiteForEachMethod (junit.framework.TestSuite overallTestSuite$) { try { this.addTestSuiteFor$TestSearchableDigraph(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestDFS(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestDFSVisit(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestTranspose(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestAddNode(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestRemoveNode(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestAddArc(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestRemoveArc(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestIsNode(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestIsArc(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestIsAPath(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestToString(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } try { this.addTestSuiteFor$TestUnconnected(overallTestSuite$); } catch (java.lang.Throwable ex) { overallTestSuite$.addTest (new org.jmlspecs.jmlunit.strategies.ConstructorFailed(ex)); } } /** Add tests for the SearchableDigraph contructor * to the overall test suite. */ private void addTestSuiteFor$TestSearchableDigraph (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("SearchableDigraph"); try { methodTests$.addTest (new TestSearchableDigraph()); } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the SearchableDigraph contructor. */ protected static class TestSearchableDigraph extends OneTest { /** Initialize this instance. */ public TestSearchableDigraph() { super("SearchableDigraph"); } protected void doCall() throws java.lang.Throwable { new SearchableDigraph(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tContructor 'SearchableDigraph'"; return msg; } } /** Add tests for the DFS method * to the overall test suite. */ private void addTestSuiteFor$TestDFS (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("DFS"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_samples_digraph_SearchableDigraphIter("DFS", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_samples_digraph_SearchableDigraphIter(\"DFS\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.samples.digraph.SearchableDigraph receiver$ = (org.jmlspecs.samples.digraph.SearchableDigraph) receivers$iter.get(); methodTests$.addTest (new TestDFS(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the DFS method. */ protected static class TestDFS extends OneTest { /** The receiver */ private org.jmlspecs.samples.digraph.SearchableDigraph receiver$; /** Initialize this instance. */ public TestDFS(org.jmlspecs.samples.digraph.SearchableDigraph receiver$) { super("DFS"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.DFS(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'DFS' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the DFSVisit method * to the overall test suite. */ private void addTestSuiteFor$TestDFSVisit (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("DFSVisit"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_samples_digraph_SearchableDigraphIter("DFSVisit", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_samples_digraph_SearchableDigraphIter(\"DFSVisit\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_samples_digraph_SearchableNode$1$iter = this.vorg_jmlspecs_samples_digraph_SearchableNodeIter("DFSVisit", 0); this.check_has_data (vorg_jmlspecs_samples_digraph_SearchableNode$1$iter, "this.vorg_jmlspecs_samples_digraph_SearchableNodeIter(\"DFSVisit\", 0)"); while (!vorg_jmlspecs_samples_digraph_SearchableNode$1$iter.atEnd()) { final org.jmlspecs.samples.digraph.SearchableDigraph receiver$ = (org.jmlspecs.samples.digraph.SearchableDigraph) receivers$iter.get(); final org.jmlspecs.samples.digraph.SearchableNode u = (org.jmlspecs.samples.digraph.SearchableNode) vorg_jmlspecs_samples_digraph_SearchableNode$1$iter.get(); methodTests$.addTest (new TestDFSVisit(receiver$, u)); vorg_jmlspecs_samples_digraph_SearchableNode$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the DFSVisit method. */ protected static class TestDFSVisit extends OneTest { /** The receiver */ private org.jmlspecs.samples.digraph.SearchableDigraph receiver$; /** Argument u */ private org.jmlspecs.samples.digraph.SearchableNode u; /** Initialize this instance. */ public TestDFSVisit(org.jmlspecs.samples.digraph.SearchableDigraph receiver$, org.jmlspecs.samples.digraph.SearchableNode u) { super("DFSVisit"+ ":" + (u==null? "null" :"{org.jmlspecs.samples.digraph.SearchableNode}")); this.receiver$ = receiver$; this.u = u; } protected void doCall() throws java.lang.Throwable { receiver$.DFSVisit(u); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'DFSVisit' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument u: " + this.u; return msg; } } /** Add tests for the transpose method * to the overall test suite. */ private void addTestSuiteFor$TestTranspose (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("transpose"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_samples_digraph_SearchableDigraphIter("transpose", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_samples_digraph_SearchableDigraphIter(\"transpose\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.samples.digraph.SearchableDigraph receiver$ = (org.jmlspecs.samples.digraph.SearchableDigraph) receivers$iter.get(); methodTests$.addTest (new TestTranspose(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the transpose method. */ protected static class TestTranspose extends OneTest { /** The receiver */ private org.jmlspecs.samples.digraph.SearchableDigraph receiver$; /** Initialize this instance. */ public TestTranspose(org.jmlspecs.samples.digraph.SearchableDigraph receiver$) { super("transpose"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.transpose(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'transpose' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the addNode method * to the overall test suite. */ private void addTestSuiteFor$TestAddNode (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("addNode"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_samples_digraph_SearchableDigraphIter("addNode", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_samples_digraph_SearchableDigraphIter(\"addNode\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_samples_digraph_NodeType$1$iter = this.vorg_jmlspecs_samples_digraph_NodeTypeIter("addNode", 0); this.check_has_data (vorg_jmlspecs_samples_digraph_NodeType$1$iter, "this.vorg_jmlspecs_samples_digraph_NodeTypeIter(\"addNode\", 0)"); while (!vorg_jmlspecs_samples_digraph_NodeType$1$iter.atEnd()) { final org.jmlspecs.samples.digraph.SearchableDigraph receiver$ = (org.jmlspecs.samples.digraph.SearchableDigraph) receivers$iter.get(); final org.jmlspecs.samples.digraph.NodeType arg1 = (org.jmlspecs.samples.digraph.NodeType) vorg_jmlspecs_samples_digraph_NodeType$1$iter.get(); methodTests$.addTest (new TestAddNode(receiver$, arg1)); vorg_jmlspecs_samples_digraph_NodeType$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the addNode method. */ protected static class TestAddNode extends OneTest { /** The receiver */ private org.jmlspecs.samples.digraph.SearchableDigraph receiver$; /** Argument arg1 */ private org.jmlspecs.samples.digraph.NodeType arg1; /** Initialize this instance. */ public TestAddNode(org.jmlspecs.samples.digraph.SearchableDigraph receiver$, org.jmlspecs.samples.digraph.NodeType arg1) { super("addNode"+ ":" + (arg1==null? "null" :"{org.jmlspecs.samples.digraph.NodeType}")); this.receiver$ = receiver$; this.arg1 = arg1; } protected void doCall() throws java.lang.Throwable { receiver$.addNode(arg1); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'addNode' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; return msg; } } /** Add tests for the removeNode method * to the overall test suite. */ private void addTestSuiteFor$TestRemoveNode (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("removeNode"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_samples_digraph_SearchableDigraphIter("removeNode", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_samples_digraph_SearchableDigraphIter(\"removeNode\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_samples_digraph_NodeType$1$iter = this.vorg_jmlspecs_samples_digraph_NodeTypeIter("removeNode", 0); this.check_has_data (vorg_jmlspecs_samples_digraph_NodeType$1$iter, "this.vorg_jmlspecs_samples_digraph_NodeTypeIter(\"removeNode\", 0)"); while (!vorg_jmlspecs_samples_digraph_NodeType$1$iter.atEnd()) { final org.jmlspecs.samples.digraph.SearchableDigraph receiver$ = (org.jmlspecs.samples.digraph.SearchableDigraph) receivers$iter.get(); final org.jmlspecs.samples.digraph.NodeType arg1 = (org.jmlspecs.samples.digraph.NodeType) vorg_jmlspecs_samples_digraph_NodeType$1$iter.get(); methodTests$.addTest (new TestRemoveNode(receiver$, arg1)); vorg_jmlspecs_samples_digraph_NodeType$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the removeNode method. */ protected static class TestRemoveNode extends OneTest { /** The receiver */ private org.jmlspecs.samples.digraph.SearchableDigraph receiver$; /** Argument arg1 */ private org.jmlspecs.samples.digraph.NodeType arg1; /** Initialize this instance. */ public TestRemoveNode(org.jmlspecs.samples.digraph.SearchableDigraph receiver$, org.jmlspecs.samples.digraph.NodeType arg1) { super("removeNode"+ ":" + (arg1==null? "null" :"{org.jmlspecs.samples.digraph.NodeType}")); this.receiver$ = receiver$; this.arg1 = arg1; } protected void doCall() throws java.lang.Throwable { receiver$.removeNode(arg1); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'removeNode' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; return msg; } } /** Add tests for the addArc method * to the overall test suite. */ private void addTestSuiteFor$TestAddArc (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("addArc"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_samples_digraph_SearchableDigraphIter("addArc", 2)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_samples_digraph_SearchableDigraphIter(\"addArc\", 2))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_samples_digraph_NodeType$1$iter = this.vorg_jmlspecs_samples_digraph_NodeTypeIter("addArc", 1); this.check_has_data (vorg_jmlspecs_samples_digraph_NodeType$1$iter, "this.vorg_jmlspecs_samples_digraph_NodeTypeIter(\"addArc\", 1)"); while (!vorg_jmlspecs_samples_digraph_NodeType$1$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_samples_digraph_NodeType$2$iter = this.vorg_jmlspecs_samples_digraph_NodeTypeIter("addArc", 0); this.check_has_data (vorg_jmlspecs_samples_digraph_NodeType$2$iter, "this.vorg_jmlspecs_samples_digraph_NodeTypeIter(\"addArc\", 0)"); while (!vorg_jmlspecs_samples_digraph_NodeType$2$iter.atEnd()) { final org.jmlspecs.samples.digraph.SearchableDigraph receiver$ = (org.jmlspecs.samples.digraph.SearchableDigraph) receivers$iter.get(); final org.jmlspecs.samples.digraph.NodeType arg1 = (org.jmlspecs.samples.digraph.NodeType) vorg_jmlspecs_samples_digraph_NodeType$1$iter.get(); final org.jmlspecs.samples.digraph.NodeType arg2 = (org.jmlspecs.samples.digraph.NodeType) vorg_jmlspecs_samples_digraph_NodeType$2$iter.get(); methodTests$.addTest (new TestAddArc(receiver$, arg1, arg2)); vorg_jmlspecs_samples_digraph_NodeType$2$iter.advance(); } vorg_jmlspecs_samples_digraph_NodeType$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the addArc method. */ protected static class TestAddArc extends OneTest { /** The receiver */ private org.jmlspecs.samples.digraph.SearchableDigraph receiver$; /** Argument arg1 */ private org.jmlspecs.samples.digraph.NodeType arg1; /** Argument arg2 */ private org.jmlspecs.samples.digraph.NodeType arg2; /** Initialize this instance. */ public TestAddArc(org.jmlspecs.samples.digraph.SearchableDigraph receiver$, org.jmlspecs.samples.digraph.NodeType arg1, org.jmlspecs.samples.digraph.NodeType arg2) { super("addArc"+ ":" + (arg1==null? "null" :"{org.jmlspecs.samples.digraph.NodeType}")+ "," +(arg2==null? "null" :"{org.jmlspecs.samples.digraph.NodeType}")); this.receiver$ = receiver$; this.arg1 = arg1; this.arg2 = arg2; } protected void doCall() throws java.lang.Throwable { receiver$.addArc(arg1, arg2); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'addArc' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; msg += "\n\tArgument arg2: " + this.arg2; return msg; } } /** Add tests for the removeArc method * to the overall test suite. */ private void addTestSuiteFor$TestRemoveArc (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("removeArc"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_samples_digraph_SearchableDigraphIter("removeArc", 2)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_samples_digraph_SearchableDigraphIter(\"removeArc\", 2))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_samples_digraph_NodeType$1$iter = this.vorg_jmlspecs_samples_digraph_NodeTypeIter("removeArc", 1); this.check_has_data (vorg_jmlspecs_samples_digraph_NodeType$1$iter, "this.vorg_jmlspecs_samples_digraph_NodeTypeIter(\"removeArc\", 1)"); while (!vorg_jmlspecs_samples_digraph_NodeType$1$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_samples_digraph_NodeType$2$iter = this.vorg_jmlspecs_samples_digraph_NodeTypeIter("removeArc", 0); this.check_has_data (vorg_jmlspecs_samples_digraph_NodeType$2$iter, "this.vorg_jmlspecs_samples_digraph_NodeTypeIter(\"removeArc\", 0)"); while (!vorg_jmlspecs_samples_digraph_NodeType$2$iter.atEnd()) { final org.jmlspecs.samples.digraph.SearchableDigraph receiver$ = (org.jmlspecs.samples.digraph.SearchableDigraph) receivers$iter.get(); final org.jmlspecs.samples.digraph.NodeType arg1 = (org.jmlspecs.samples.digraph.NodeType) vorg_jmlspecs_samples_digraph_NodeType$1$iter.get(); final org.jmlspecs.samples.digraph.NodeType arg2 = (org.jmlspecs.samples.digraph.NodeType) vorg_jmlspecs_samples_digraph_NodeType$2$iter.get(); methodTests$.addTest (new TestRemoveArc(receiver$, arg1, arg2)); vorg_jmlspecs_samples_digraph_NodeType$2$iter.advance(); } vorg_jmlspecs_samples_digraph_NodeType$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the removeArc method. */ protected static class TestRemoveArc extends OneTest { /** The receiver */ private org.jmlspecs.samples.digraph.SearchableDigraph receiver$; /** Argument arg1 */ private org.jmlspecs.samples.digraph.NodeType arg1; /** Argument arg2 */ private org.jmlspecs.samples.digraph.NodeType arg2; /** Initialize this instance. */ public TestRemoveArc(org.jmlspecs.samples.digraph.SearchableDigraph receiver$, org.jmlspecs.samples.digraph.NodeType arg1, org.jmlspecs.samples.digraph.NodeType arg2) { super("removeArc"+ ":" + (arg1==null? "null" :"{org.jmlspecs.samples.digraph.NodeType}")+ "," +(arg2==null? "null" :"{org.jmlspecs.samples.digraph.NodeType}")); this.receiver$ = receiver$; this.arg1 = arg1; this.arg2 = arg2; } protected void doCall() throws java.lang.Throwable { receiver$.removeArc(arg1, arg2); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'removeArc' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; msg += "\n\tArgument arg2: " + this.arg2; return msg; } } /** Add tests for the isNode method * to the overall test suite. */ private void addTestSuiteFor$TestIsNode (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("isNode"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_samples_digraph_SearchableDigraphIter("isNode", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_samples_digraph_SearchableDigraphIter(\"isNode\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_samples_digraph_NodeType$1$iter = this.vorg_jmlspecs_samples_digraph_NodeTypeIter("isNode", 0); this.check_has_data (vorg_jmlspecs_samples_digraph_NodeType$1$iter, "this.vorg_jmlspecs_samples_digraph_NodeTypeIter(\"isNode\", 0)"); while (!vorg_jmlspecs_samples_digraph_NodeType$1$iter.atEnd()) { final org.jmlspecs.samples.digraph.SearchableDigraph receiver$ = (org.jmlspecs.samples.digraph.SearchableDigraph) receivers$iter.get(); final org.jmlspecs.samples.digraph.NodeType arg1 = (org.jmlspecs.samples.digraph.NodeType) vorg_jmlspecs_samples_digraph_NodeType$1$iter.get(); methodTests$.addTest (new TestIsNode(receiver$, arg1)); vorg_jmlspecs_samples_digraph_NodeType$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the isNode method. */ protected static class TestIsNode extends OneTest { /** The receiver */ private org.jmlspecs.samples.digraph.SearchableDigraph receiver$; /** Argument arg1 */ private org.jmlspecs.samples.digraph.NodeType arg1; /** Initialize this instance. */ public TestIsNode(org.jmlspecs.samples.digraph.SearchableDigraph receiver$, org.jmlspecs.samples.digraph.NodeType arg1) { super("isNode"+ ":" + (arg1==null? "null" :"{org.jmlspecs.samples.digraph.NodeType}")); this.receiver$ = receiver$; this.arg1 = arg1; } protected void doCall() throws java.lang.Throwable { receiver$.isNode(arg1); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'isNode' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; return msg; } } /** Add tests for the isArc method * to the overall test suite. */ private void addTestSuiteFor$TestIsArc (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("isArc"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_samples_digraph_SearchableDigraphIter("isArc", 2)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_samples_digraph_SearchableDigraphIter(\"isArc\", 2))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_samples_digraph_NodeType$1$iter = this.vorg_jmlspecs_samples_digraph_NodeTypeIter("isArc", 1); this.check_has_data (vorg_jmlspecs_samples_digraph_NodeType$1$iter, "this.vorg_jmlspecs_samples_digraph_NodeTypeIter(\"isArc\", 1)"); while (!vorg_jmlspecs_samples_digraph_NodeType$1$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_samples_digraph_NodeType$2$iter = this.vorg_jmlspecs_samples_digraph_NodeTypeIter("isArc", 0); this.check_has_data (vorg_jmlspecs_samples_digraph_NodeType$2$iter, "this.vorg_jmlspecs_samples_digraph_NodeTypeIter(\"isArc\", 0)"); while (!vorg_jmlspecs_samples_digraph_NodeType$2$iter.atEnd()) { final org.jmlspecs.samples.digraph.SearchableDigraph receiver$ = (org.jmlspecs.samples.digraph.SearchableDigraph) receivers$iter.get(); final org.jmlspecs.samples.digraph.NodeType arg1 = (org.jmlspecs.samples.digraph.NodeType) vorg_jmlspecs_samples_digraph_NodeType$1$iter.get(); final org.jmlspecs.samples.digraph.NodeType arg2 = (org.jmlspecs.samples.digraph.NodeType) vorg_jmlspecs_samples_digraph_NodeType$2$iter.get(); methodTests$.addTest (new TestIsArc(receiver$, arg1, arg2)); vorg_jmlspecs_samples_digraph_NodeType$2$iter.advance(); } vorg_jmlspecs_samples_digraph_NodeType$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the isArc method. */ protected static class TestIsArc extends OneTest { /** The receiver */ private org.jmlspecs.samples.digraph.SearchableDigraph receiver$; /** Argument arg1 */ private org.jmlspecs.samples.digraph.NodeType arg1; /** Argument arg2 */ private org.jmlspecs.samples.digraph.NodeType arg2; /** Initialize this instance. */ public TestIsArc(org.jmlspecs.samples.digraph.SearchableDigraph receiver$, org.jmlspecs.samples.digraph.NodeType arg1, org.jmlspecs.samples.digraph.NodeType arg2) { super("isArc"+ ":" + (arg1==null? "null" :"{org.jmlspecs.samples.digraph.NodeType}")+ "," +(arg2==null? "null" :"{org.jmlspecs.samples.digraph.NodeType}")); this.receiver$ = receiver$; this.arg1 = arg1; this.arg2 = arg2; } protected void doCall() throws java.lang.Throwable { receiver$.isArc(arg1, arg2); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'isArc' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; msg += "\n\tArgument arg2: " + this.arg2; return msg; } } /** Add tests for the isAPath method * to the overall test suite. */ private void addTestSuiteFor$TestIsAPath (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("isAPath"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_samples_digraph_SearchableDigraphIter("isAPath", 2)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_samples_digraph_SearchableDigraphIter(\"isAPath\", 2))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_samples_digraph_NodeType$1$iter = this.vorg_jmlspecs_samples_digraph_NodeTypeIter("isAPath", 1); this.check_has_data (vorg_jmlspecs_samples_digraph_NodeType$1$iter, "this.vorg_jmlspecs_samples_digraph_NodeTypeIter(\"isAPath\", 1)"); while (!vorg_jmlspecs_samples_digraph_NodeType$1$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_samples_digraph_NodeType$2$iter = this.vorg_jmlspecs_samples_digraph_NodeTypeIter("isAPath", 0); this.check_has_data (vorg_jmlspecs_samples_digraph_NodeType$2$iter, "this.vorg_jmlspecs_samples_digraph_NodeTypeIter(\"isAPath\", 0)"); while (!vorg_jmlspecs_samples_digraph_NodeType$2$iter.atEnd()) { final org.jmlspecs.samples.digraph.SearchableDigraph receiver$ = (org.jmlspecs.samples.digraph.SearchableDigraph) receivers$iter.get(); final org.jmlspecs.samples.digraph.NodeType arg1 = (org.jmlspecs.samples.digraph.NodeType) vorg_jmlspecs_samples_digraph_NodeType$1$iter.get(); final org.jmlspecs.samples.digraph.NodeType arg2 = (org.jmlspecs.samples.digraph.NodeType) vorg_jmlspecs_samples_digraph_NodeType$2$iter.get(); methodTests$.addTest (new TestIsAPath(receiver$, arg1, arg2)); vorg_jmlspecs_samples_digraph_NodeType$2$iter.advance(); } vorg_jmlspecs_samples_digraph_NodeType$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the isAPath method. */ protected static class TestIsAPath extends OneTest { /** The receiver */ private org.jmlspecs.samples.digraph.SearchableDigraph receiver$; /** Argument arg1 */ private org.jmlspecs.samples.digraph.NodeType arg1; /** Argument arg2 */ private org.jmlspecs.samples.digraph.NodeType arg2; /** Initialize this instance. */ public TestIsAPath(org.jmlspecs.samples.digraph.SearchableDigraph receiver$, org.jmlspecs.samples.digraph.NodeType arg1, org.jmlspecs.samples.digraph.NodeType arg2) { super("isAPath"+ ":" + (arg1==null? "null" :"{org.jmlspecs.samples.digraph.NodeType}")+ "," +(arg2==null? "null" :"{org.jmlspecs.samples.digraph.NodeType}")); this.receiver$ = receiver$; this.arg1 = arg1; this.arg2 = arg2; } protected void doCall() throws java.lang.Throwable { receiver$.isAPath(arg1, arg2); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'isAPath' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; msg += "\n\tArgument arg2: " + this.arg2; return msg; } } /** Add tests for the toString method * to the overall test suite. */ private void addTestSuiteFor$TestToString (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("toString"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_samples_digraph_SearchableDigraphIter("toString", 0)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_samples_digraph_SearchableDigraphIter(\"toString\", 0))"); while (!receivers$iter.atEnd()) { final org.jmlspecs.samples.digraph.SearchableDigraph receiver$ = (org.jmlspecs.samples.digraph.SearchableDigraph) receivers$iter.get(); methodTests$.addTest (new TestToString(receiver$)); receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the toString method. */ protected static class TestToString extends OneTest { /** The receiver */ private org.jmlspecs.samples.digraph.SearchableDigraph receiver$; /** Initialize this instance. */ public TestToString(org.jmlspecs.samples.digraph.SearchableDigraph receiver$) { super("toString"); this.receiver$ = receiver$; } protected void doCall() throws java.lang.Throwable { receiver$.toString(); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'toString' applied to"; msg += "\n\tReceiver: " + this.receiver$; return msg; } } /** Add tests for the unconnected method * to the overall test suite. */ private void addTestSuiteFor$TestUnconnected (junit.framework.TestSuite overallTestSuite$) { junit.framework.TestSuite methodTests$ = this.emptyTestSuiteFor("unconnected"); try { org.jmlspecs.jmlunit.strategies.IndefiniteIterator receivers$iter = new org.jmlspecs.jmlunit.strategies.NonNullIteratorDecorator (this.vorg_jmlspecs_samples_digraph_SearchableDigraphIter("unconnected", 1)); this.check_has_data (receivers$iter, "new NonNullIteratorDecorator(this.vorg_jmlspecs_samples_digraph_SearchableDigraphIter(\"unconnected\", 1))"); while (!receivers$iter.atEnd()) { org.jmlspecs.jmlunit.strategies.IndefiniteIterator vorg_jmlspecs_samples_digraph_NodeType$1$iter = this.vorg_jmlspecs_samples_digraph_NodeTypeIter("unconnected", 0); this.check_has_data (vorg_jmlspecs_samples_digraph_NodeType$1$iter, "this.vorg_jmlspecs_samples_digraph_NodeTypeIter(\"unconnected\", 0)"); while (!vorg_jmlspecs_samples_digraph_NodeType$1$iter.atEnd()) { final org.jmlspecs.samples.digraph.SearchableDigraph receiver$ = (org.jmlspecs.samples.digraph.SearchableDigraph) receivers$iter.get(); final org.jmlspecs.samples.digraph.NodeType arg1 = (org.jmlspecs.samples.digraph.NodeType) vorg_jmlspecs_samples_digraph_NodeType$1$iter.get(); methodTests$.addTest (new TestUnconnected(receiver$, arg1)); vorg_jmlspecs_samples_digraph_NodeType$1$iter.advance(); } receivers$iter.advance(); } } catch (org.jmlspecs.jmlunit.strategies.TestSuiteFullException e$) { // methodTests$ doesn't want more tests } overallTestSuite$.addTest(methodTests$); } /** Test for the unconnected method. */ protected static class TestUnconnected extends OneTest { /** The receiver */ private org.jmlspecs.samples.digraph.SearchableDigraph receiver$; /** Argument arg1 */ private org.jmlspecs.samples.digraph.NodeType arg1; /** Initialize this instance. */ public TestUnconnected(org.jmlspecs.samples.digraph.SearchableDigraph receiver$, org.jmlspecs.samples.digraph.NodeType arg1) { super("unconnected"+ ":" + (arg1==null? "null" :"{org.jmlspecs.samples.digraph.NodeType}")); this.receiver$ = receiver$; this.arg1 = arg1; } protected void doCall() throws java.lang.Throwable { receiver$.unconnected(arg1); } protected java.lang.String failMessage (org.jmlspecs.jmlrac.runtime.JMLAssertionError e$) { java.lang.String msg = "\n\tMethod 'unconnected' applied to"; msg += "\n\tReceiver: " + this.receiver$; msg += "\n\tArgument arg1: " + this.arg1; return msg; } } /** Check that the iterator is non-null and not empty. */ private void check_has_data(org.jmlspecs.jmlunit.strategies.IndefiniteIterator iter, String call) { if (iter == null) { junit.framework.Assert.fail(call + " returned null"); } if (iter.atEnd()) { junit.framework.Assert.fail(call + " returned an empty iterator"); } } /** Converts a char to a printable String for display */ public static String charToString(char c) { if (c == '\n') { return "NL"; } else if (c == '\r') { return "CR"; } else if (c == '\t') { return "TAB"; } else if (Character.isISOControl(c)) { int i = (int)c; return "\\u" + Character.forDigit((i/2048)%16,16) + Character.forDigit((i/256)%16,16) + Character.forDigit((i/16)%16,16) + Character.forDigit((i)%16,16); } return Character.toString(c); } }