Package com.uppaal.engine

Class EngineStub

java.lang.Object
com.uppaal.engine.EngineStub
public class EngineStub
extends Object
A thin stub for the server protocol.

The EngineStub class takes care of connecting to and disconnecting from the server. Connections can be local and remote. For local (aka. native) connections, the server process is started by the engine stub on the local machine and communication is handled via pipes. On disconnect the server process is killed. Remote connections do not start a server. Instead, the stub will try to connect to a running server.

The serverHost and serverPort properties determine which host and on which port to connect to the server for remote connections. The connectionMode is used to determine the kind of connection to establish. If connectionMode is BOTH, then the stub will first attempt to create a remote connection and if that fails create a local connection. The serverPath holds the name of the server executable to execute in local mode. After a successful connection has been established the port to which the connection has been established can be queried with getConnectedPort(). Notice that the serverPort property plays no role for local connections.

The server protocol is not state less, as there is a notion of uploading a model and certain operations are only valid after uploading a model. You most likely want to use the Engine class rather than the EngineStub.

  • Field Details

    • LOCAL

      public static int LOCAL
      Local connections only.

    • SERVER

      public static int SERVER
      Remote connections only..

    • BOTH

      public static int BOTH
      Try remote connection first, then local.

    • DEFAULT_HOST

      public static String DEFAULT_HOST
      The default host for remote connections.

    • DEFAULT_PORT

      public static int DEFAULT_PORT
      The default port for remote connections.

  • Constructor Details

    • EngineStub

      public EngineStub()
      Constructs an EngineStub in LOCAL connection mode.

    • EngineStub

      public EngineStub​(int mode, int port, String host, String path)
      Constructs an EngineStub with the given mode, port, port and server path values.
      Parameters:
      mode - - The mode number
      port - - The port number
      host - - The host number
      path - - The path string

  • Method Details

    • getErrorStream

      public String getErrorStream()
      Snapshot of an error stream from the (local) server process. Normally there should be no content in the error stream, but sometimes it just crashes due to unforseen circumstances like linking errors, unintended pure virtual method call or just unforseen exception. The (remote) socketserver combines both output and error streams into output, so expect empty error stream there.
      Returns:
      null if error stream is empty and string content if there is something.

    • getServerPort

      public int getServerPort()
      Returns the current server port.
      Returns:
      serverPort - The server port number

    • setServerPort

      public void setServerPort​(int port)
      Sets the server port. The server port is used in REMOTE mode to determine which port on the server to connect to.
      Parameters:
      port - - The port number

    • getConnectionMode

      public int getConnectionMode()
      Returns the current connection mode.
      Returns:
      The connection mode

    • setConnectionMode

      public void setConnectionMode​(int mode)
      Sets the connection mode. Mode is either LOCAL, SERVER or BOTH. In BOTH the stub will first try to build a remote connection and if that fails attempt to create a local connection.
      Parameters:
      mode - - The connection mode

    • getServerHost

      public String getServerHost()
      Returns the current server host.
      Returns:
      The server host

    • setServerHost

      public void setServerHost​(String host)
      Sets the server host. In SERVER mode the engine will try to connect to this host.
      Parameters:
      host - - The host string

    • getServerPath

      public String getServerPath()
      Returns the current server path.
      Returns:
      The server path string

    • getConnectedPort

      public int getConnectedPort()
      Returns the port the engine is connected to.
      Returns:
      The connected port number

    • setServerPath

      public void setServerPath​(String path)
      Sets the server path. The server path should include the path to, filename of and options for the server binary.
      Parameters:
      path - - The server path

    • isConnected

      public boolean isConnected()
      Returns true if the engine is connected to a server.
      Returns:
      True - The engine is connected

    • isRemoteConnection

      public boolean isRemoteConnection()
      Returns true if the engine is connected to a remote server.
      Returns:
      True - The engine is connected to a remove server

    • connect

      public void connect() throws EngineException, IOException
      Connect to the server. Depending on the connection mode setting either a remote or local connection will be established (or both). Remote connections are made according to the server host and server port settings. Local connections are established according to the server path setting.
      Throws:
      IOException - engine crash or problem in communication.
      EngineException - problem in the Uppaal engine.

    • disconnect

      public void disconnect()
      Disconnect from the server. If connected to the server, the connection will be cut by closing the socket and making sure the socket server process is terminated if in LOCAL mode. The engine waits for the socket server to terminate by itself after closing the socket connection. If the socket server is still running after 2 seconds it is killed.

    • kill

      public void kill()
      Kill the server connection the hard way. The socket is closed, and the socket server is killed.

    • handshake

      public void handshake() throws IOException, EngineException
      Performs a handshake with the server. Done automatically by connect().
      Throws:
      IOException - engine crash or problem in communication.
      EngineException - problem in the Uppaal engine.

    • getVersion

      public String getVersion() throws IOException, EngineException
      Returns the version string of the server. The stub must be connected.
      Returns:
      The version string of the server
      Throws:
      IOException - engine crash or problem in communication.
      EngineException - problem in the Uppaal engine.

    • getOptionsInfo

      public String getOptionsInfo() throws EngineException, IOException
      Returns information about available options. The information is returned as an XML document. The stub must be connected.
      Returns:
      The information about available options
      Throws:
      IOException - engine crash or problem in communication.
      EngineException - problem in the Uppaal engine.

    • setOptions

      public void setOptions​(String options) throws EngineException, IOException
      Sets server options used for verification. The stub must be connected. TODO: Document format.
      Parameters:
      options - - The server options
      Throws:
      IOException - engine crash or problem in communication.
      EngineException - problem in the Uppaal engine.

    • getSymbolicInitial

      public SymbolicState getSymbolicInitial​(UppaalSystem system) throws EngineException, IOException, CannotEvaluateException
      Returns the initial state for the system. The stub must be connected and the system must be the last one uploaded to the server.
      Parameters:
      system - - The uppaal system
      Returns:
      The symbolic initial state for the system
      Throws:
      IOException - I/O communication error.
      EngineException - error in the server protocol.
      CannotEvaluateException - some expression could not be evaluated.

    • getConcreteInitial

      public ConcreteState getConcreteInitial​(UppaalSystem system) throws EngineException, IOException, CannotEvaluateException
      Returns the initial concrete state for the system. The stub must be connected and the system must be the last one uploaded to the server.
      Parameters:
      system - - The uppaal system
      Returns:
      The concrete initial state for the system
      Throws:
      IOException - I/O communication error.
      EngineException - error in the server protocol.
      CannotEvaluateException - some expression could not be evaluated.

    • getConcreteSuccessor

      public ConcreteSuccessor getConcreteSuccessor​(UppaalSystem system, ConcreteState state, SystemEdgeSelect[] edges, BigDecimal currentTime, BigDecimal delay) throws EngineException, IOException, CannotEvaluateException
      Get the concrete successor
      Parameters:
      system - - The uppaal system
      state - - The concrete state
      edges - - The array of the selected system edge
      currentTime - - The current time
      delay - - The delay value
      Returns:
      The concrete successor
      Throws:
      IOException - I/O communication error.
      EngineException - error in the server protocol.
      CannotEvaluateException - some expression could not be evaluated.

    • getGanttChart

      public GanttChart getGanttChart​(UppaalSystem system, BigDecimal globalTime) throws EngineException, IOException
      Get the gantt chart
      Parameters:
      system - - The uppaal system
      globalTime - - The global time
      Returns:
      The gantt chart
      Throws:
      IOException - I/O communication error.
      EngineException - error in the server protocol.

    • getTransitions

      public ArrayList<SymbolicTransition> getTransitions​(UppaalSystem system, SymbolicState state) throws EngineException, IOException, CannotEvaluateException
      Returns the list of outgoing transitions for the state. The stub must be connected, the state must belong to the system, and the system must be the last one uploaded to the server.
      Parameters:
      system - - The uppaal system
      state - - symbolic state of the system
      Returns:
      The list of outgoing transitions for the state
      Throws:
      IOException - I/O communication error.
      EngineException - error in the server protocol.
      CannotEvaluateException - some expression could not be evaluated.

    • upload

      public UppaalSystem upload​(Document document, ArrayList<Problem> problems) throws EngineException, IOException
      Upload the document to the server. If no errors occurred, the instantiated system is returned. Otherwise, null is returned and error reports are stored in the problems vector. Even if no errors occurred, warnings may have been added to the problems vector. The stub must be connected.
      Parameters:
      document - - The document
      problems - - The list of the error reports that are stored in the problems vector.
      Returns:
      Upload the document to the server
      Throws:
      IOException - I/O communication error.
      EngineException - error in the server protocol.

    • uploadLsc

      public LscProcess uploadLsc​(Document document, ArrayList<Problem> problems) throws EngineException, IOException
      Upload the lsc process to the server. If no errors occurred, the instantiated system is returned. Otherwise, null is returned and error reports are stored in the problems vector. Even if no errors occurred, warnings may have been added to the problems vector.
      Parameters:
      document - - The document
      problems - - The list of the error reports that are stored in the problems vector.
      Returns:
      The instantiated system
      Throws:
      IOException - I/O communication error.
      EngineException - error in the server protocol.

    • upload

      public UppaalSystem upload​(Document document) throws EngineException, IOException
      Upload the document to the server. If no errors occurred, the instantiated system is returned. Otherwise, null is returned. The stub must be connected.
      Parameters:
      document - - The document
      Returns:
      The instantiated uppaal system
      Throws:
      IOException - I/O communication error.
      EngineException - error in the server protocol.

    • query

      public QueryResult query​(UppaalSystem system, Query query, QueryFeedback f) throws EngineException, IOException
      Verify a query on an instantiated UPPAAL model. Returns 'T' if property is satisfied, 'F' if it is not satisfied, 'M' if it is maybe satisfied, and 'E' if an error occurred. Progress feedback and traces are provided via the feedback object. The stub must be connected and the system must be the last one uploaded to the server.
      Parameters:
      system - - The uppaal system
      query - - The query
      f - - The feedback of the query from a verifier.
      Returns:
      - 'T' if property is satisfied, 'F' if it is not satisfied, 'M' if it is maybe satisfied, 'E' if an error occurred.
      Throws:
      IOException - I/O communication error.
      EngineException - error in the server protocol.

    • query

      public QueryResult query​(UppaalSystem system, SymbolicState state, Query query, QueryFeedback f) throws EngineException, IOException, CannotEvaluateException
      Verify a guery on an instantiated UPPAAL model with custom initial state. Returns 'T' if property is satisfied, 'F' if it is not satisfied, 'M' if it is maybe satisfied, and 'E' if an error occurred. Progress feedback and traces are provided via the feedback object. The stub must be connected and the system must be the last one uploaded to the server.
      Parameters:
      system - UppaalSystem representation
      state - initial symbolic state to start exploration from
      query - property to verify
      f - feedback handler
      Returns:
      Throws:
      EngineException
      IOException
      CannotEvaluateException