Package com.uppaal.engine

Class KeyValueProtocol

java.lang.Object

com.uppaal.engine.KeyValueProtocol

All Implemented Interfaces:

Protocol

public class KeyValueProtocol
extends Object
implements Protocol

IMPORTANT

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
protected static class	KeyValueProtocol.Service

Constructor Summary

Constructors

Constructor	Description
KeyValueProtocol(InputStream in, OutputStream out)	Constructor

Method Summary

Modifier and Type	Method	Description
void	close()	Disconnect from the server.
protected String	escape(String str)	Escape the string.
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 concrete successor: concrete state and the list of the concrete transitions
GanttChart	getGanttChart(UppaalSystem system, BigDecimal globalTime)	Get gantt chart
SystemState	getInitial(UppaalSystem system)	Get the initial of the uppaal system
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	localiseString(String str)
protected SystemEdgeSelect[]	parseEdges(Properties data, UppaalSystem system, String edges)	Parse edges in the system
protected SystemLocation[]	parseLocationVector(String property, UppaalSystem system)	Parses location vector
protected SymbolicState	parseState(Properties data, UppaalSystem system, String locations, String variables, String zone)	Parse the symbolic state
protected int[]	parseVariableVector(String property, UppaalSystem system)	Parse the variable vector
protected Polyhedron	parseZone(String property, UppaalSystem system)	Parse the zone of the uppaal system
QueryResult	query(UppaalSystem system, Query query, QueryFeedback f)	Verify a query on an instantiated UPPAAL model.
QueryResult	query(UppaalSystem system, SymbolicState state, Query query, QueryFeedback f)	Verify a query on an instantiated UPPAAL model with custom initial state.
protected List<String>	readLines()	Read lines until "."-line-terminator, remove (escaping) start-of-line-"."s
protected String	recvBlock(KeyValueProtocol.Service serviceName, boolean allow_progress)	Checks the string of the block from the BufferedReader.
protected List<String>	recvLines(KeyValueProtocol.Service serviceName, boolean allow_progress)	Checks serviceName, checks for OK or ERROR (don't use for PROGRESS messages)
protected List<Properties>	recvProperties(KeyValueProtocol.Service serviceName)	Recovery all properties
protected List<Properties>	recvProperties(KeyValueProtocol.Service serviceName, boolean allow_progress)	Recovery all properties from the allowed progress
protected String	recvString(KeyValueProtocol.Service serviceName)	Checks the imported string from the service object
protected void	sendMessage(KeyValueProtocol.Service service)	Send the message to the out stream using only the service
protected void	sendMessage(KeyValueProtocol.Service service, SymbolicState state)	Send the message to the out stream using the service and symbolic state
protected void	sendMessage(KeyValueProtocol.Service service, SymbolicState state, String query)	Send the message to the out stream using the service and symbolic state
protected void	sendMessage(KeyValueProtocol.Service service, String data)	Send the message to the out stream using the service and data string
void	setOptions(String options)	Sets server options used for verification.
protected void	setProgress(QueryFeedback f, Properties data)	Set the progress: When server sends a progress update on verification status.
protected void	setSystemInfo(QueryFeedback f, Properties data)	Set the system information: Before start processing a query
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)	Upload the lsc.

Methods inherited from class java.lang.Object

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

Constructor Details

KeyValueProtocol

public KeyValueProtocol(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.

getInitial

public SystemState getInitial(UppaalSystem system) throws EngineException, IOException

Get the initial of the uppaal system

Parameters:

system - - The uppaal system

Returns:

The system state

Throws:

IOException - engine crash or problem in communication.

EngineException - problem in the Uppaal engine.

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.

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.

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

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

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) throws IOException, EngineException

Recovery all properties

Parameters:

serviceName - - The service item

Returns:

The list of the property

Throws:

IOException - engine crash or problem in communication.

EngineException - problem in the Uppaal engine.

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.

recvString

protected String recvString(KeyValueProtocol.Service serviceName) throws IOException, EngineException

Checks the imported string from the service object

Parameters:

serviceName - - The service item from the enum of the service

Returns:

The string

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

uploadLsc

public LscProcess uploadLsc(Document document, ArrayList<Problem> problems) throws EngineException, IOException

Upload the lsc.

Specified by:

uploadLsc in interface Protocol

Parameters:

document - - The model document

problems - - The list of the problems

Returns:

null

Throws:

IOException - engine crash or problem in communication.

EngineException - problem in the Uppaal engine.

getGanttChart

public GanttChart getGanttChart(UppaalSystem system, BigDecimal globalTime) throws EngineException, IOException

Get gantt chart

Specified by:

getGanttChart in interface Protocol

Parameters:

system - - The uppaal system

globalTime - - The global time

Returns:

The list of the gantt chart rows

Throws:

IOException - engine crash or problem in communication.

EngineException - problem in the Uppaal engine.

getConcreteSuccessor

public ConcreteSuccessor getConcreteSuccessor(UppaalSystem system, ConcreteState state, SystemEdgeSelect[] edges, BigDecimal currentTime, BigDecimal delay) throws EngineException, IOException

Get concrete successor: concrete state and the list of the concrete transitions

Specified by:

getConcreteSuccessor in interface Protocol

Parameters:

system - - The uppaal system

state - - The concrete state

edges - - The select edges of the system

currentTime - - The current time

delay - - The dalay time

Returns:

The concrete successor object

Throws:

IOException - engine crash or problem in communication.

EngineException - problem in the Uppaal engine.

getConcreteInitial

public ConcreteState getConcreteInitial(UppaalSystem system) throws EngineException, IOException

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.

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.