Class KeyValueProtocol

  • All Implemented Interfaces:
    Protocol

    public class KeyValueProtocol
    extends Object
    implements Protocol
    IMPORTANT
    • Constructor Detail

      • KeyValueProtocol

        public KeyValueProtocol​(InputStream in,
                                OutputStream out)
        Constructor
        Parameters:
        in - - The input stream
        out - - The output stream
    • Method Detail

      • close

        public void close()
                   throws IOException
        Description copied from interface: Protocol
        Disconnect from the server.
        Specified by:
        close in interface Protocol
        Throws:
        IOException - engine crash or problem in communication.
      • parseLocationVector

        protected SystemLocation[] parseLocationVector​(String property,
                                                       UppaalSystem system)
        Parses location vector
        Parameters:
        property - - The property string that contains the variable data
        system - - The uppaal system
        Returns:
        locations - The array of the system locations
      • parseVariableVector

        protected int[] parseVariableVector​(String property,
                                            UppaalSystem system)
        Parse the variable vector
        Parameters:
        property - - The property string that includes the variable
        system - - The uppaal system
        Returns:
        variables - The list of the system variable
      • parseZone

        protected Polyhedron parseZone​(String property,
                                       UppaalSystem system)
        Parse the zone of the uppaal system
        Parameters:
        property - - The property that includes the zone data
        system - - The uppaal system
        Returns:
        zone - The polyhedron object
      • getOptionsInfo

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

        protected SymbolicState parseState​(Properties data,
                                           UppaalSystem system,
                                           String locations,
                                           String variables,
                                           String zone)
        Parse the symbolic state
        Parameters:
        data - - The set of the properties
        system - - The uppaal system
        locations - - The locations of the system
        variables - - The variables string
        zone - - The zone of the system
        Returns:
        A new symbolic state
      • parseEdges

        protected SystemEdgeSelect[] parseEdges​(Properties data,
                                                UppaalSystem system,
                                                String edges)
        Parse edges in the system
        Parameters:
        data - - The set of the properties
        system - - The uppaal system
        edges - - The string includes edges of the system
        Returns:
        edgesList - The list of selected edges
      • query

        public QueryResult query​(UppaalSystem system,
                                 Query query,
                                 QueryFeedback f)
                          throws EngineException,
                                 IOException
        Description copied from interface: Protocol
        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.
        Specified by:
        query in interface Protocol
        Parameters:
        system - - The uppaal system
        query - - The query
        f - - The query feed back
        Returns:
        The query verification results
        Throws:
        EngineException - error in the server protocol.
        IOException - I/O communication error.
      • query

        public QueryResult query​(UppaalSystem system,
                                 SymbolicState state,
                                 Query query,
                                 QueryFeedback f)
                          throws EngineException,
                                 IOException
        Description copied from interface: Protocol
        Verify a query 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.
        Specified by:
        query in interface Protocol
        Parameters:
        system - system model representation
        state - initial symbolic state
        query - the property to check for
        f - feedback handler
        Returns:
        Throws:
        EngineException
        IOException
      • setProgress

        protected void setProgress​(QueryFeedback f,
                                   Properties data)
        Set the progress: When server sends a progress update on verification status.
        Parameters:
        f - - The feedback from a verifier
        data - - The set of the properties
      • setSystemInfo

        protected void setSystemInfo​(QueryFeedback f,
                                     Properties data)
        Set the system information: Before start processing a query
        Parameters:
        f - - The feedback from a verifier
        data - - The set of the properties
      • setOptions

        public void setOptions​(String options)
                        throws EngineException,
                               IOException
        Description copied from interface: Protocol
        Sets server options used for verification. The stub must be connected. TODO: Document format.
        Specified by:
        setOptions in interface Protocol
        Parameters:
        options - - The options string
        Throws:
        EngineException - problem in the Uppaal engine.
        IOException - engine crash or problem in communication.
      • upload

        public UppaalSystem upload​(Document document,
                                   ArrayList<Problem> problems)
                            throws EngineException,
                                   IOException
        Description copied from interface: Protocol
        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.
        Specified by:
        upload in interface Protocol
        Parameters:
        document - - The system document
        problems - - The problem array list
        Returns:
        the compiled system representation
        Throws:
        EngineException - error in the server protocol.
        IOException - I/O communication error.
      • upload

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

        protected void sendMessage​(KeyValueProtocol.Service service)
                            throws IOException
        Send the message to the out stream using only the service
        Parameters:
        service - - The service object
        Throws:
        IOException - engine crashed or communication was disrupted.
      • sendMessage

        protected void sendMessage​(KeyValueProtocol.Service service,
                                   String data)
                            throws IOException
        Send the message to the out stream using the service and data string
        Parameters:
        service - - The service object
        data - - The data string
        Throws:
        IOException - engine crashed or communication was disrupted.
      • sendMessage

        protected void sendMessage​(KeyValueProtocol.Service service,
                                   SymbolicState state)
                            throws IOException
        Send the message to the out stream using the service and symbolic state
        Parameters:
        service - - The service object
        state - - The symbolic state
        Throws:
        IOException - engine crash or problem in communication.
      • sendMessage

        protected void sendMessage​(KeyValueProtocol.Service service,
                                   SymbolicState state,
                                   String query)
                            throws IOException
        Send the message to the out stream using the service and symbolic state
        Parameters:
        service - - The service object
        state - - The symbolic state
        Throws:
        IOException - engine crash or problem in communication.
      • localiseString

        protected String localiseString​(String str)
        Parameters:
        str - - The localise string
        Returns:
        str - The String
      • recvProperties

        protected List<Properties> recvProperties​(KeyValueProtocol.Service serviceName,
                                                  boolean allow_progress)
                                           throws IOException,
                                                  EngineException
        Recovery all properties from the allowed progress
        Parameters:
        serviceName - - The service object
        allow_progress - - The allowed progress
        Returns:
        result - The list of the property
        Throws:
        IOException - engine crash or problem in communication.
        EngineException - problem in the Uppaal engine.
      • recvBlock

        protected String recvBlock​(KeyValueProtocol.Service serviceName,
                                   boolean allow_progress)
                            throws IOException,
                                   EngineException
        Checks the string of the block from the BufferedReader.
        Parameters:
        serviceName - - The service item
        allow_progress - - The allowed progress
        Returns:
        block - The string builder
        Throws:
        IOException - engine crash or problem in communication.
        EngineException - problem in the Uppaal engine.
      • recvLines

        protected List<String> recvLines​(KeyValueProtocol.Service serviceName,
                                         boolean allow_progress)
                                  throws IOException,
                                         EngineException
        Checks serviceName, checks for OK or ERROR (don't use for PROGRESS messages)
        Parameters:
        serviceName - - The service item name
        allow_progress - - The allowed progress
        Returns:
        dataLines - The list of the data line
        Throws:
        IOException - engine crash or problem in communication.
        EngineException - problem in the Uppaal engine.
      • readLines

        protected List<String> readLines()
                                  throws IOException
        Read lines until "."-line-terminator, remove (escaping) start-of-line-"."s
        Returns:
        lines - The list of the string
        Throws:
        IOException - engine crash or problem in communication.
      • escape

        protected String escape​(String str)
        Escape the string.
        Parameters:
        str - - The input data string
        Returns:
        result - The string of the string builder
      • getSymbolicInitial

        public SymbolicState getSymbolicInitial​(UppaalSystem system)
                                         throws EngineException,
                                                IOException
        Description copied from interface: Protocol
        Returns the symbolic initial state for the system. The stub must be connected and the system must be the last one uploaded to the server.
        Specified by:
        getSymbolicInitial in interface Protocol
        Parameters:
        system - the compiled Uppaal system representation.
        Returns:
        initial symbolic state.
        Throws:
        EngineException - error in the server protocol.
        IOException - I/O communication error.