Package com.uppaal.engine

Class Engine

java.lang.Object
com.uppaal.engine.Engine
public class Engine
extends Object
State-less wrapper for a UPPAAL server connection.

If you want to communicate with the UPPAAL verification engine, this is the class to use. It is a thin wrapper around the EngineStub class and provides a state-less interface to the verification engine. In contrast to the EngineStub class, it can work with several model instances at the same time (although with reduced speed) and transparently connect and reconnect to the engine.

The various connection modes are documented in the EngineStub class.

Before connecting to the engine, a document should be created, please see Document for sample code.

The following code demonstrates how to connect to a local UPPAAL engine via standard input/output streams using server protocol: 

 Engine engine = new Engine();
 engine.setServerPath(enginePath);
 engine.connect();
where enginePath is a path to server executable. On Windows the enginePath is "uppaal-version\\bin-Windows\\server.exe" and on Linux it is "uppaal-version/bin-Linux/server".

Alternatively one can use a Linux server by starting socketserver utility on a remote computer. The socketserver uses default port 2350 and can be reached as follows: 

 Engine engine = new Engine(EngineStub.BOTH, 2350, "hostname", enginePath);
 engine.connect();
If the connection fails, then the local server execution will be used instead.

Then the model document can be uploaded, syntax-checked and compiled as follows: 

 ArrayList<Problem> problems = new ArrayList<Problem>();
 UppaalSystem system = engine.getSystem(doc, problems);
The array problems contains errors and warnings if any. If the compilation was successful the system object contains a reference to a compiled system model.

The following code can be used to execute and print random transitions: 

 SymbolicState state = engine.getInitialState(system);
 while (state != null) {
      ArrayList<SymbolicTransition> trans = engine.getTransitions(system, state);
      Transition tr = trans.get((int)Math.floor(Math.random()*trans.size()));
      if (tr.getSize()==0) { // transition without edges, something special:
          System.out.println(tr.getEdgeDescription());
      } else { // one or more edges involved:
          System.out.print("(");
          for (SystemEdge e: tr.getEdges()) {
              System.out.print(e.getProcessName()+": "
                  + e.getEdge().getName()+", ");
          }
          System.out.println(")");
      }
      state = tr.getTarget(); // deadlock "transitions" will give null
 }
The verifier functionality can be accessed by calling the query(UppaalSystem, String, Query, QueryFeedback) method.

The options string in the query method is a concatenation of one option per line: an option name and a choice name (or one or more values) separated by space.

For example at the time of this writing the default list of options was: 

order 0
reduction 1
representation 0
trace 0
extrapolation 0
hashsize 27
reuse 1
smcparametric 1
modest 0
statistical 0.01 0.01 0.05 0.05 0.05 0.9 1.1 0.0 0.0 1280.0 0.01
The options may vary from version to version and depends on the actual server binary used. One can inspect the list of available options by requesting getOptionsInfo() which will bring an XML description of all options.
See Also:
Document, EngineStub

  • Field Details

    • stub

      protected EngineStub stub
      The stub for the server connection.

  • Constructor Details

    • Engine

      public Engine()
      Constructs an Engine object for local connections. Make sure the engine path is set before connecting.

    • Engine

      public Engine​(int mode, int port, String host, String path)
      Constructs an Engine object for the given connection settings.
      Parameters:
      mode - specifies mode: EngineStub.LOCAL (executed locally), EngineStub.SERVER (connected to remote socket) or EngineStub.BOTH (try remote and fallback to local when socket connection fails).
      port - the socket port number (default 2350)
      host - the hostname of the remote computer where the socketserver is started
      path - a path to server binary for local execution.

  • Method Details