MaudeProcessTest.java
/**
* Copyright (C) The MOMENT project, 2004-2006.
* http://moment.dsic.upv.es
*
* This file is part of the Maude Simple GUI plug-in.
* Contributed by Abel Gómez, <agomez@dsic.upv.es>.
*
* The Maude Simple GUI plug-in is free software; you can redistribute it and/or
* modify it under the terms of the GNU Library General Public License as
* published by the Free Software Foundation; either version 2 of the
* License, or (at your option) any later version.
*
* The Maude Simple GUI plug-in is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
* Library General Public License for more details.
*
* You should have received a copy of the GNU Lesser General Public
* License along with the Maude Development Tools plugin, see the file license.txt.
* If not, write to the Free Software Foundation, Inc., 51 Franklin Street,
* Fifth Floor, Boston, MA 02110-1301 USA
*
*/
package es.upv.dsic.issi.moment.mdt.maudedaemon.tests;
import java.io.IOException;
import java.util.List;
import es.upv.dsic.issi.moment.maudedaemon.core.MaudeDaemonPlugin;
import es.upv.dsic.issi.moment.maudedaemon.maude.IMaudeJob;
import es.upv.dsic.issi.moment.maudedaemon.maude.IMaudeProcessBatch;
import es.upv.dsic.issi.moment.maudedaemon.maude.IMaudeProcessInteract;
import es.upv.dsic.issi.moment.maudedaemon.parser.ParseException;
import junit.framework.TestCase;
/**
*
* @author Abel Gómez. agomez@dsic.upv.es
*
*/
public class MaudeProcessTests extends TestCase {
public MaudeProcessTests(String arg0) {
super(arg0);
}
public void testCreateCoreMaudeProcessInteract() {
IMaudeProcessInteract maudePI = MaudeDaemonPlugin.getDefault().getNewMaudeProcessInteract();
maudePI.configMaudeFromPrefs();
maudePI.setAutoConfig(false);
maudePI.setCoreMaude();
try {
maudePI.execMaude();
} catch (IOException e) {
e.printStackTrace();
}
assertTrue("Maude is running.",maudePI.isRunning());
assertTrue("Maude is running in Core Maude mode.",maudePI.isCoreMaude());
maudePI.quitMaude();
assertFalse("Maude process finished.",maudePI.isRunning());
}
public void testCreateCoreMaudeProcessBatch() {
IMaudeProcessBatch maudePB = MaudeDaemonPlugin.getDefault().getNewMaudeProcessBatch();
maudePB.configMaudeFromPrefs();
maudePB.setAutoConfig(false);
maudePB.setCoreMaude();
try {
maudePB.execMaude();
} catch (IOException e) {
e.printStackTrace();
}
assertTrue("Maude is running.",maudePB.isRunning());
assertTrue("Maude is running in Core Maude mode.",maudePB.isCoreMaude());
maudePB.quitMaude();
assertFalse("Maude process finished.",maudePB.isRunning());
}
public void testCreateFullMaudeProcessInteract() {
IMaudeProcessInteract maudePI = MaudeDaemonPlugin.getDefault().getNewMaudeProcessInteract();
maudePI.configMaudeFromPrefs();
maudePI.setAutoConfig(false);
maudePI.setFullMaude();
try {
maudePI.execMaude();
} catch (IOException e) {
e.printStackTrace();
}
assertTrue("Maude is running.",maudePI.isRunning());
assertTrue("Maude is running in Full Maude mode.",maudePI.isFullMaude());
maudePI.quitMaude();
assertFalse("Maude process finished.",maudePI.isRunning());
}
public void testCreateFullMaudeProcessBatch() {
IMaudeProcessBatch maudePB = MaudeDaemonPlugin.getDefault().getNewMaudeProcessBatch();
maudePB.configMaudeFromPrefs();
maudePB.setAutoConfig(false);
maudePB.setFullMaude();
try {
maudePB.execMaude();
} catch (IOException e) {
e.printStackTrace();
}
assertTrue("Maude is running.",maudePB.isRunning());
assertTrue("Maude is running in Full Maude mode.",maudePB.isFullMaude());
maudePB.quitMaude();
assertFalse("Maude process finished.",maudePB.isRunning());
}
public void testMaudeJobPeano() {
IMaudeProcessBatch maudePB = MaudeDaemonPlugin.getDefault().getNewMaudeProcessBatch();
maudePB.configMaudeFromPrefs();
maudePB.setAutoConfig(false);
maudePB.setCoreMaude();
try {
maudePB.execMaude();
} catch (IOException e) {
e.printStackTrace();
}
assertTrue("Maude is running.",maudePB.isRunning());
assertTrue("Maude is running in Core Maude mode.",maudePB.isCoreMaude());
String peanoNatExtraModule =
"fmod PEANO-NAT-EXTRA is\n" +
" sort Nat .\n" +
" op 0 : -> Nat [ctor] .\n" +
" op s : Nat -> Nat [ctor iter] .\n" +
" op _+_ : Nat Nat -> Nat .\n" +
" vars M N : Nat .\n" +
" eq 0 + N = N .\n" +
" eq s(M) + N = s(M + N) .\n" +
"endfm\n";
try {
IMaudeJob mj = maudePB.createAndRunJobs(peanoNatExtraModule).get(0);
maudePB.waitUntilFinish();
assertTrue("Module loaded without errors.", !mj.isFailed() && mj.getOut().length() == 0);
mj = maudePB.createAndRunJobs("red s(s(0)) + s(0) .\n").get(0);
mj.waitUntilFinish();
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)"));
} catch (ParseException e) {
e.printStackTrace();
}
maudePB.quitMaude();
assertFalse("Maude process finished.",maudePB.isRunning());
}
public void testFullMaude() {
IMaudeProcessBatch maudePB = MaudeDaemonPlugin.getDefault().getNewMaudeProcessBatch();
maudePB.configMaudeFromPrefs();
maudePB.setAutoConfig(false);
maudePB.setFullMaude();
try {
maudePB.execMaude();
} catch (IOException e) {
e.printStackTrace();
}
assertTrue("Maude is running.",maudePB.isRunning());
assertTrue("Maude is running in Full Maude mode.",maudePB.isFullMaude());
String fullMaudeCommands =
"(fth FUNCTION(X :: TRIV | Y :: TRIV) is\n" +
" op f : X@Elt -> Y@Elt .\n" +
"endfth)\n" +
"(fmod FMAP(F :: FUNCTION(X :: TRIV | Y :: TRIV)) is\n" +
" sorts IndSet(X) DepSet(Y) .\n" +
" subsort X@Elt < IndSet(X) .\n" +
" subsort Y@Elt < DepSet(Y) .\n" +
" op __ : IndSet(X) IndSet(X) -> IndSet(X) [ctor assoc comm id: ind-null] .\n" +
" op _;_ : DepSet(Y) DepSet(Y) -> DepSet(Y) [ctor assoc comm id: dep-null] .\n" +
" op ind-null : -> IndSet(X) [ctor] .\n" +
" op dep-null : -> DepSet(Y) [ctor] .\n" +
" op fmap : IndSet(X) -> DepSet(Y) .\n" +
" var N : X@Elt . var NS : IndSet(X) .\n" +
" eq fmap(N NS) = f(N) ; fmap(NS) .\n" +
" eq fmap(ind-null) = dep-null .\n" +
"endfm)\n" +
"(fmod NEGATIVE is\n" +
" pr NAT . pr INT .\n" +
" op _timesneg1 : Nat -> Int .\n" +
" var N : Nat .\n" +
" eq N timesneg1 = - N .\n" +
"endfm)\n" +
"(view Triv-Nat from TRIV to NAT is sort Elt to Nat . endv)\n" +
"(view Triv-Int from TRIV to INT is sort Elt to Int . endv)\n" +
"(view Fun-Neg(X :: TRIV | Y :: TRIV) from FUNCTION(X | Y) to NEGATIVE is\n" +
" op f to _timesneg1 .\n" +
"endv)\n" +
"(red in FMAP(Fun-Neg(Triv-Nat | Triv-Int)) : fmap(5 9 11 2 0) .)\n";
try {
List<IMaudeJob> mjs = maudePB.createAndRunJobs(fullMaudeCommands);
maudePB.waitUntilFinish();
for (IMaudeJob mj : mjs) {
System.out.println("Processing job:");
System.out.println(mj.getInput());
System.out.println("Raw result:");
System.out.println(mj.getOut());
System.out.println("Filtered result:");
System.out.println(mj.getResult());
System.out.println("Error messages:");
System.out.println(mj.getError());
System.out.println("=====================================================\n\n");
}
} catch (ParseException e) {
e.printStackTrace();
}
maudePB.quitMaude();
assertFalse("Maude process finished.",maudePB.isRunning());
}
}