Running the test suite.

We provide a set of tests cases for you to easily check if everything is installed properly. Moreover, the tests cases are a very simple way to learn how to use the MaudeDaemon plugin. The tests cases use the JUnit facilities provided by Eclipse.

You can get the code provided to run the plugin of tests cases from the MOMENT CVS server.

You only need to download de project es.upv.dsic.issi.moment.mdt.maudedaemon.tests.

Showing the JUnit view.

The JUnit plugin provided by Eclipse allows you to easily see if the tests are executed succesfully or not. Yo can access to the JUnit view from the "Window -> Show View -> Other" menu...


Show a new view .

... and selecting the option JUnit from the Java folder.


Selecting the JUnit view.

Finally, the view will appear at the bottom of the Workbench.


The JUnit view

Running the tests.

The plugin only has a Java class, which contains all the methods to run the tests. you can execute them by right clicking over the Java class, and selecting the option JUnit Plug-in Test from the Run as (or Debug as) menu.


Running the tests.

Once you have executed this option, a new Eclipse instance will be launched, and probably, will ask you for set up the Maude preferences:


Configuring Maude.

You have to fill the required fields to properly run the tests as explained in the section Configuring the Maude Development Tools -> Basic Preferences.

The tests will run, and you will obtain the results of them:


Tests executed.

Tests cases avilable.

  1. public void testCreateCoreMaudeProcessInteract() {...};

    2. This tests simply creates and configures a MaudeProcessInteract instance, then executes the process, and finally stops it.

  2. public void testCreateCoreMaudeProcessBatch() {...};

    3. The second test creates and configures a MaudeProcessBatch instance. That is a Maude process running Core Maude in batch mode.

  3. public void testCreateFullMaudeProcessInteract() {...};
  4. public void testCreateFullMaudeProcessBatch() {...};

    5. This two methods perform the same tests than the first and the sencond methods, but in this case, running Full Maude.

  5. public void testMaudeJobPeano() {...};

    6. This method shows a simple example of how to load a module in Maude (PEANO-NAT-EXTRA, from the examples provided in the Maude web page), and how to reduce an expresion and get the result returned by Maude.

    The Maude module loaded is:

    ***********************************************************************
*** Chapter 2 - Functional Modules
*** Section 1 : Equations
***
*** PEANO-NAT-EXTRA : illustrates the fundamentals of equation
*** writing with the addition operator defined with Peano notation.
***
***********************************************************************


fmod PEANO-NAT-EXTRA is

  sort Nat .

  op 0 : -> Nat [ctor] .
  op s : Nat -> Nat [ctor iter] .
  op _+_ : Nat Nat -> Nat .

  vars M N : Nat .

  eq 0 + N = N .
  eq s(M) + N = s(M + N) .

endfm

    Once the module is loaded, the test case executes the next reduction command:

    red s(s(0)) + s(0) .

    This command is executed as follows:

    mj = maudePB.createAndRunJobs("red s(s(0)) + s(0) .\n").get(0);
    mj.waitUntilFinish();

    Finally we check that the results are correct with these assert statements:

    assertTrue("Operation executed correctly.", !mj.isFailed() && mj.getOut().length() > 0);
assertTrue("Check num. rewrites.", mj.getRewrites() == 3);
assertTrue("Last module.", mj.getActiveModule().equals("PEANO-NAT-EXTRA"));
assertTrue("Correct result", mj.getResult().equals("s^3(0)"));

    We can see that to get the filtered result of the operation reduction we use the method getResult(). If we want to look at the whole result provided by Maude, we should use the getOut() method.

  6. public void testFullMaude() {...};

    7. In this test case we execute a set of Full Maude commands. The Maude code is the following one: 

    ***************************************************************************
***  Chapter 5 - Parameterization
***	Section 5 : Parameterized Views and Theories
***
***  FMAP : another example of parameterized views and theories
***
**************************************************************************



(fth FUNCTION(X :: TRIV | Y :: TRIV) is

   op f : X@Elt -> Y@Elt .

endfth)

(fmod FMAP(F :: FUNCTION(X :: TRIV | Y :: TRIV)) is

   sorts IndSet(X) DepSet(Y) .
   subsort X@Elt < IndSet(X) .
   subsort Y@Elt < DepSet(Y) .
   
   op __ : IndSet(X) IndSet(X) -> IndSet(X) [ctor assoc comm id: ind-null] .
   op _;_ : DepSet(Y) DepSet(Y) -> DepSet(Y) [ctor assoc comm id: dep-null] .
   op ind-null : -> IndSet(X) [ctor] .
   op dep-null : -> DepSet(Y) [ctor] .

   op fmap : IndSet(X) -> DepSet(Y) .

   var N : X@Elt .	var NS : IndSet(X) .

   eq fmap(N NS) = f(N) ; fmap(NS) .
   eq fmap(ind-null) = dep-null .

endfm)

(fmod NEGATIVE is

   pr NAT .	pr INT .

   op _timesneg1 : Nat -> Int .

   var N : Nat .

   eq N timesneg1 = - N .

endfm)


(view Triv-Nat from TRIV to NAT is sort Elt to Nat .  endv)

(view Triv-Int from TRIV to INT is sort Elt to Int .  endv)

(view Fun-Neg(X :: TRIV | Y :: TRIV) from FUNCTION(X | Y) to NEGATIVE is

   op f to _timesneg1 .

endv)


(red in FMAP(Fun-Neg(Triv-Nat | Triv-Int)) : fmap(5 9 11 2 0) .)

    In this case, the Full Maude code is expected to be decomposed in seven MaudeJobs. To simplify the test process, the result of the execution of each job is shown in the Eclipse console.