Package com.uppaal.engine

Interface QueryFeedback

public interface QueryFeedback
Defines the interface to receive feedback from a verifier. Defines the interface for objects that are used to receive feedback from a verification. The engine will first call setLength to the set the length of trace to be loaded, followed by zero or more calls to setCurrent to provide progress information, and finally call setTrace when the trace has been loaded.
See Also:
Engine.query(com.uppaal.model.system.UppaalSystem, java.lang.String, com.uppaal.model.core2.Query, com.uppaal.engine.QueryFeedback)

  • Method Summary

    Modifier and Type Method Description
    void appendText​(String s)
    Allows engine to add arbitrary text to the verifier status field.
    void setCurrent​(int pos)
    Called when pos elements of the trace have been loaded.
    void setFeedback​(String feedback)
    Called after a verification in case there is no trace.
    void setLength​(int length)
    Called when the length of a trace is known.
    void setProgress​(int load, long vm, long rss, long cached, long avail, long swap, long swapfree, long user, long sys, long timestamp)
    Called when server sends a progress update on verification status.
    void setProgressAvail​(boolean availability)
    Called before sending query to server.
    void setResultText​(String s)
    Allows engine to add arbitrary text beside the "status" image.
    void setSystemInfo​(long vmsize, long physsize, long swapsize)
    Called before start processing a query.
    void setTrace​(char result, String feedback, ConcreteTrace trace, QueryResult queryVerificationResult)
    Called after a verification in case there is trace.
    void setTrace​(char result, String feedback, SymbolicTrace trace, QueryResult queryVerificationResult)
    Called when the complete trace has been loaded.

  • Method Details

    • setProgressAvail

      void setProgressAvail​(boolean availability)
      Called before sending query to server.
      Parameters:
      availability - indicates whether progress information will be available.

    • setProgress

      void setProgress​(int load, long vm, long rss, long cached, long avail, long swap, long swapfree, long user, long sys, long timestamp)
      Called when server sends a progress update on verification status.
      Parameters:
      load - the PWList load in states
      vm - the virtual memory usage in kilo bytes
      rss - the resident (working set) memory usage in kilo bytes
      cached - memory used by system (I/O buffers, caches) in kilo bytes
      avail - the available (free) physical memory in kilo bytes
      swap - the swap (pagefile) memory usage in kilo bytes
      swapfree - - Without the swap (pagefile) memory usage
      user - the user time CPU usage in milliseconds
      sys - the system (kernel) time CPU usage in milliseconds
      timestamp - the timestamp of statistics in milliseconds

    • setSystemInfo

      void setSystemInfo​(long vmsize, long physsize, long swapsize)
      Called before start processing a query.
      Parameters:
      vmsize - the total virtual memory size in kilo bytes
      physsize - the total physical memory size in kilo bytes
      swapsize - the total swap memory size in kilo bytes

    • setLength

      void setLength​(int length)
      Called when the length of a trace is known.
      Parameters:
      length - the length of the trace in transitions

    • setCurrent

      void setCurrent​(int pos)
      Called when pos elements of the trace have been loaded. This provides progress information while loading traces.
      Parameters:
      pos - the number of transitions loaded

    • setTrace

      void setTrace​(char result, String feedback, SymbolicTrace trace, QueryResult queryVerificationResult)
      Called when the complete trace has been loaded.
      Parameters:
      result - 'T' if the query is satisfied, 'F' if the query is not satisfied, 'M' if the query is maybe satisfied and 'E' in case of errors.
      feedback - is a feedback string to report to the user
      trace - the trace returned by the server. May be null if no trace was returned.
      queryVerificationResult - - The query verification result object

    • setTrace

      void setTrace​(char result, String feedback, ConcreteTrace trace, QueryResult queryVerificationResult)
      Called after a verification in case there is trace.
      Parameters:
      result - - The verification result
      feedback - - The feed back string
      trace - - The list of the trace data
      queryVerificationResult - - The query verification result

    • setFeedback

      void setFeedback​(String feedback)
      Called after a verification in case there is no trace. Set a feedback.
      Parameters:
      feedback - - The feed back string

    • appendText

      void appendText​(String s)
      Allows engine to add arbitrary text to the verifier status field.
      Parameters:
      s - Text to add.

    • setResultText

      void setResultText​(String s)
      Allows engine to add arbitrary text beside the "status" image.
      Parameters:
      s - Text to add.