com.uppaal.engine.DotProtocol

All Implemented Interfaces:: Protocol

public class DotProtocol
extends Object
implements Protocol

This class implements the interface 'protocol'

Constructor Summary

Constructors

Constructor Description

DotProtocol(InputStream in, OutputStream out)
Constructor

Method Summary

Modifier and Type	Method	Description
`void`	`close()`	Disconnect from the server.
`protected void`	`flush()`	Flushes the output stream.
`ConcreteState`	`getConcreteInitial(UppaalSystem system)`	Returns the concrete initial state for the system.
`ConcreteSuccessor`	`getConcreteSuccessor(UppaalSystem system, ConcreteState state, SystemEdgeSelect[] edges, BigDecimal currentTime, BigDecimal delay)`	Get the concrete simulation successor
`GanttChart`	`getGanttChart(UppaalSystem system, BigDecimal globalTime)`	Get the gantt chart
`String`	`getOptionsInfo()`	Returns information about available options.
`SymbolicState`	`getSymbolicInitial(UppaalSystem system)`	Returns the symbolic initial state for the system.
`ArrayList<SymbolicTransition>`	`getTransitions(UppaalSystem system, SymbolicState state)`	Returns the list of outgoing transitions for the state.
`String`	`getVersion()`	Returns the version string of the server.
`protected String`	`parseResults(String results, QueryResult result)`	Parses the feedback block which may consist of the following items: popup message (starts with M) verbose result for display in the property list (starts with R) a data for plot (starts with P).See server.cpp for details.
`QueryResult`	`query(UppaalSystem system, Query query, QueryFeedback f)`	Write the query data to the server
`QueryResult`	`query(UppaalSystem system, SymbolicState state, Query query, QueryFeedback f)`	Write the query data and the symbolic state to the server
`void`	`setOptions(String options)`	Sets server options used for verification.
`protected static String`	`unquote(String s)`	Get the unquote string
`UppaalSystem`	`upload(Document document)`	Upload the document to the server.
`UppaalSystem`	`upload(Document document, ArrayList<Problem> problems)`	Upload the document to the server.
`LscProcess`	`uploadLsc(Document document, ArrayList<Problem> problems)`
`protected void`	`write(ConcreteState state, BigDecimal delay)`	Writes the concrete state in the system to the output stream.
`protected void`	`write(SystemEdge[] edges)`	Writes the list of the edges to the output stream
`protected void`	`write(SystemEdgeSelect[] edges)`	Writes the list of the selected edges to the output stream
`protected void`	`write(Object o)`	Writes the object to the output stream following by a newline.
`protected void`	`write(String s)`	Writes the string to the output stream following by a newline.
`protected void`	`write(BigDecimal value)`	Writes the value to the output stream following by a new line

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Details
- DotProtocol
  
  public DotProtocol(InputStream in, OutputStream out)
  
  Constructor
  
  Parameters:
  
  in - - The input stream
  
  out - - The output stream
Method Details
- 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.
- getSymbolicInitial
  
  public SymbolicState getSymbolicInitial(UppaalSystem system) throws EngineException, IOException, CannotEvaluateException
  
  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.
  
  CannotEvaluateException - some expression could not be evaluated.
- getConcreteInitial
  
  public ConcreteState getConcreteInitial(UppaalSystem system) throws EngineException, IOException, CannotEvaluateException
  
  Description copied from interface: Protocol
  
  Returns the concrete initial state for the system. The stub must be connected and the system must be the last one uploaded to the server.
  
  Specified by:
  
  getConcreteInitial in interface Protocol
  
  Parameters:
  
  system - the compiled Uppaal system representation.
  
  Returns:
  
  initial concrete state
  
  Throws:
  
  EngineException - error in the server protocol.
  
  IOException - I/O communication error.
  
  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
  
  Description copied from interface: Protocol
  
  Get the concrete simulation successor
  
  Specified by:
  
  getConcreteSuccessor in interface Protocol
  
  Parameters:
  
  system - - The uppaal system
  
  state - - The concrete simulator state
  
  edges - - The vector of the selected system edges
  
  currentTime - - the current simulation time
  
  delay - - The delay time
  
  Returns:
  
  concrete successor object
  
  Throws:
  
  EngineException - error in the server protocol.
  
  IOException - I/O communication error.
  
  CannotEvaluateException - some expression could not be evaluated.
- 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.
- getTransitions
  
  public ArrayList<SymbolicTransition> getTransitions(UppaalSystem system, SymbolicState state) throws EngineException, IOException, CannotEvaluateException
  
  Description copied from interface: Protocol
  
  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.
  
  Specified by:
  
  getTransitions in interface Protocol
  
  Parameters:
  
  system - - The uppaal system
  
  state - - The symbolic state of the system
  
  Returns:
  
  The array list of the symbolic transition
  
  Throws:
  
  EngineException - error in the server protocol.
  
  IOException - I/O communication error.
  
  CannotEvaluateException - some expression could not be evaluated.
- getVersion
  
  public String getVersion() throws IOException, EngineException
  
  Description copied from interface: Protocol
  
  Returns the version string of the server. The stub must be connected.
  
  Specified by:
  
  getVersion in interface Protocol
  
  Returns:
  
  The version
  
  Throws:
  
  IOException - engine crash or problem in communication.
  
  EngineException - problem in the Uppaal engine.
- query
  
  public QueryResult query(UppaalSystem system, Query query, QueryFeedback f) throws EngineException, IOException
  
  Write the query data to the server
  
  Specified by:
  
  query in interface Protocol
  
  Parameters:
  
  system - - The Uppaal system
  
  query - - The query string
  
  f - - The feedback char: 'T'/'M'/'E'
  
  Returns:
  
  The query result object: .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. .exception - CannotEvaluateException
  
  Throws:
  
  EngineException - problem in Uppaal engine.
  
  IOException - engine crash or problem in communication.
- query
  
  public QueryResult query(UppaalSystem system, SymbolicState state, Query query, QueryFeedback f) throws EngineException, IOException, CannotEvaluateException
  
  Write the query data and the symbolic state to the server
  
  Specified by:
  
  query in interface Protocol
  
  Parameters:
  
  system - - The uppaal system
  
  state - - Representing a state in a system
  
  query - - The query string
  
  f - - The feedback char: 'T'/'M'/'E'
  
  Returns:
  
  '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.
  
  Throws:
  
  EngineException - problem in Uppaal engine.
  
  IOException - engine crash or problem in communication.
  
  CannotEvaluateException
- unquote
  
  protected static String unquote(String s)
  
  Get the unquote string
  
  Parameters:
  
  s - - The quote string
  
  Returns:
  
  The result string
- parseResults
  
  protected String parseResults(String results, QueryResult result)
  
  Parses the feedback block which may consist of the following items: popup message (starts with M) verbose result for display in the property list (starts with R) a data for plot (starts with P).See server.cpp for details.
  
  Parameters:
  
  result - - The encoded results string
  
  Returns:
  
  Message - the parsed message
- 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.
- write
  
  protected void write(String s) throws IOException
  
  Writes the string to the output stream following by a newline.
  
  Parameters:
  
  s - - The input string
  
  Throws:
  
  IOException - engine crash or problem in communication.
- write
  
  protected void write(Object o) throws IOException
  
  Writes the object to the output stream following by a newline.
  
  Parameters:
  
  o - - The object
  
  Throws:
  
  IOException - engine crash or problem in communication.
- write
  
  protected void write(BigDecimal value) throws IOException
  
  Writes the value to the output stream following by a new line
  
  Parameters:
  
  value - - The value
  
  Throws:
  
  IOException - engine crash or problem in communication.
- write
  
  protected void write(ConcreteState state, BigDecimal delay) throws IOException
  
  Writes the concrete state in the system to the output stream.
  
  Parameters:
  
  state - - The concrete state in the system
  
  delay - - The delay time
  
  Throws:
  
  IOException - engine crash or problem in communication.
- write
  
  protected void write(SystemEdge[] edges) throws IOException
  
  Writes the list of the edges to the output stream
  
  Parameters:
  
  edges - - The list of the edges
  
  Throws:
  
  IOException - engine crash or problem in communication.
- write
  
  protected void write(SystemEdgeSelect[] edges) throws IOException
  
  Writes the list of the selected edges to the output stream
  
  Parameters:
  
  edges - - The list of the selected edges
  
  Throws:
  
  IOException - engine crash or problem in communication.
- flush
  
  protected void flush() throws IOException
  
  Flushes the output stream.
  
  Throws:
  
  IOException - engine crash or problem in communication.
- uploadLsc
  
  public LscProcess uploadLsc(Document document, ArrayList<Problem> problems) throws EngineException, IOException
  
  Specified by:
  
  uploadLsc in interface Protocol
  
  Throws:
  
  EngineException
  
  IOException
- getGanttChart
  
  public GanttChart getGanttChart(UppaalSystem system, BigDecimal globalTime) throws EngineException, IOException
  
  Description copied from interface: Protocol
  
  Get the gantt chart
  
  Specified by:
  
  getGanttChart in interface Protocol
  
  Parameters:
  
  system - - The uppaal system
  
  globalTime - - The global time
  
  Returns:
  
  The gantt chart object
  
  Throws:
  
  EngineException - error in the server protocol.
  
  IOException - I/O communication error.

Class DotProtocol

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Constructor Details

Method Details