Class 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 Detail

      • 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 Detail

      • 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 Detail

      • 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.
      • 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.
      • 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.