Using the APIs.

MaudeProcessInteract.

This API encapsulates the methods to read from and write in the buffers of the Maude process to simplify the communication with it. Its main methods are:

public void sendToMaude(String txt) { ... }
public String readOutLineMaude() { ... }
public String readErrLineMaude() { ... }
public String readOutMaudeNoBlock(int maxLen) { ... }
public String readErrMaudeNoBlock(int maxLen) { ... }

The first one allows us to send any text to Maude to execute it. The four remaining methods are the methods to get the results from Maude. We have blocking and non blocking versions of them. The methods readOutLineMaude and readErrLineMaude will return the first available line in the buffer. If there is not any line in the buffer (or the line is not complete, i.e., does not finishes with a carriage return) the invocation of this method will be blocked.

If you use the non blocking versions instead, you can specify the maximum number of characters that you want to read. These methods will never block the execution of your program. If the buffers are empty, the result will be an empty string.

This API is designed to develop programs at a very low level of abstraction (Maude consoles, a new API, etc.), and the programmer has to be very careful when using these methods because its very easy to block the Maude process or the program itself. To run Maude programs from a Java program you should use the Batch API instead.

MaudeProcessBatch.

The functioning if this API is very simple: every command to be executed in Maude must be packed in a Job which is sent to the Maude process. This process mantains a queue with all the jobs that are waiting to be executed. One job encapsulates all the relevant information for a given set of Maude commands.

This API is the proper API to interact with Maude from a Java program. The class MaudeProcessBatch defines the following methods to create and add Jobs. You can see all the methods in this figure.

public List<IMaudeJob> createAndRunJobs (InputStream input) throws ParseException { ... }
public List<IMaudeJob> createAndRunJobs (String input) throws ParseException { ... }
public List<IMaudeJob> createJobs (String input) throws ParseException { ... }
public List<IMaudeJob> createJobs (InputStream input) throws ParseException { ... }
synchronized public void addJob(IMaudeJob job) { ... }

The Maude process executes the jobs asynchronously by default, i.e., once the jobs are sent to Maude, the Java program continues normally the execution of the following statements. Nevertheless, we provide the methods:

• MaudeJob.waitUntilfinish(). This method stops the execution of the program when it is invoked until the job is finished.
• MaudeProcessBatch.waitUntilFinish(). In this case, the execution will be suspended until all the jobs of the queue will be completed.

The main problem to execute Maude code from a Java program is to determine when one job has been completely processed and Maude is executing the next one.

The Full Maude code can be easily decomposed in simple commands, because each one of them are enclosed between brackets «(», «)». For a long string with Full Maude commands the MaudeProcessBatch class parses the contents, and returns a list of simple jobs. In this case, every one of the results returned by Maude corresponds to one Job.

In Core Maude we can not decompose easily a list of Maude commands. In this case, the solution is to execute one command after the command that we want to process. The result of that command has to be known a priori, and it must not cause any collateral efect. In this case, we always execute the reduction of a boolean expresion:

reduce true and false and true and false . 

You can see how to use the APIs in the examples provided in our plugin of test case available in the MOMENT CVS server.