Modifier and Type | Class and Description |
---|---|
protected static class |
KeyValueProtocol.Service |
Constructor and Description |
---|
KeyValueProtocol(InputStream in,
OutputStream out)
Constructor
|
Modifier and Type | Method and 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
|
QueryVerificationResult |
query(UppaalSystem system,
Query query,
QueryFeedback f)
Verify a query on an instantiated UPPAAL model.
|
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,
String data)
Send the message to the out stream using the service and data string
|
protected void |
sendMessage(KeyValueProtocol.Service service,
SymbolicState state)
Send the message to the out stream using the service and symbolic state
|
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.
|
public KeyValueProtocol(InputStream in, OutputStream out)
in
- - The input streamout
- - The output streampublic void close() throws IOException
Protocol
close
in interface Protocol
IOException
- engine crash or problem in communication.public SystemState getInitial(UppaalSystem system) throws EngineException, IOException
system
- - The uppaal systemIOException
- engine crash or problem in communication.EngineException
- problem in the Uppaal engine.protected SystemLocation[] parseLocationVector(String property, UppaalSystem system)
property
- - The property string that contains the variable datasystem
- - The uppaal systemprotected int[] parseVariableVector(String property, UppaalSystem system)
property
- - The property string that includes the variablesystem
- - The uppaal systemprotected Polyhedron parseZone(String property, UppaalSystem system)
property
- - The property that includes the zone datasystem
- - The uppaal systempublic String getOptionsInfo() throws EngineException, IOException
Protocol
getOptionsInfo
in interface Protocol
EngineException
- problem in the Uppaal engine.IOException
- engine crash or problem in communication.public ArrayList<SymbolicTransition> getTransitions(UppaalSystem system, SymbolicState state) throws EngineException, IOException, CannotEvaluateException
Protocol
getTransitions
in interface Protocol
system
- - The uppaal systemstate
- - The symbolic state of the systemEngineException
- error in the server protocol.IOException
- I/O communication error.CannotEvaluateException
- some expression could not be evaluated.protected SymbolicState parseState(Properties data, UppaalSystem system, String locations, String variables, String zone)
data
- - The set of the propertiessystem
- - The uppaal systemlocations
- - The locations of the systemvariables
- - The variables stringzone
- - The zone of the systemprotected SystemEdgeSelect[] parseEdges(Properties data, UppaalSystem system, String edges)
data
- - The set of the propertiessystem
- - The uppaal systemedges
- - The string includes edges of the systempublic String getVersion() throws IOException, EngineException
Protocol
getVersion
in interface Protocol
IOException
- engine crash or problem in communication.EngineException
- problem in the Uppaal engine.public QueryVerificationResult query(UppaalSystem system, Query query, QueryFeedback f) throws EngineException, IOException
Protocol
query
in interface Protocol
system
- - The uppaal systemquery
- - The queryf
- - The query feed backEngineException
- error in the server protocol.IOException
- I/O communication error.protected void setProgress(QueryFeedback f, Properties data)
f
- - The feedback from a verifierdata
- - The set of the propertiesprotected void setSystemInfo(QueryFeedback f, Properties data)
f
- - The feedback from a verifierdata
- - The set of the propertiespublic void setOptions(String options) throws EngineException, IOException
Protocol
setOptions
in interface Protocol
options
- - The options stringEngineException
- problem in the Uppaal engine.IOException
- engine crash or problem in communication.public UppaalSystem upload(Document document, ArrayList<Problem> problems) throws EngineException, IOException
Protocol
upload
in interface Protocol
document
- - The system documentproblems
- - The problem array listEngineException
- error in the server protocol.IOException
- I/O communication error.public UppaalSystem upload(Document document) throws EngineException, IOException
Protocol
upload
in interface Protocol
document
- - The system documentEngineException
- error in the server protocol.IOException
- I/O communication error.protected void sendMessage(KeyValueProtocol.Service service) throws IOException
service
- - The service objectIOException
- engine crashed or communication was disrupted.protected void sendMessage(KeyValueProtocol.Service service, String data) throws IOException
service
- - The service objectdata
- - The data stringIOException
- engine crashed or communication was disrupted.protected void sendMessage(KeyValueProtocol.Service service, SymbolicState state) throws IOException
service
- - The service objectstate
- - The symbolic stateIOException
- engine crash or problem in communication.protected String localiseString(String str)
str
- - The localise stringprotected List<Properties> recvProperties(KeyValueProtocol.Service serviceName) throws IOException, EngineException
serviceName
- - The service itemIOException
- engine crash or problem in communication.EngineException
- problem in the Uppaal engine.protected List<Properties> recvProperties(KeyValueProtocol.Service serviceName, boolean allow_progress) throws IOException, EngineException
serviceName
- - The service objectallow_progress
- - The allowed progressIOException
- engine crash or problem in communication.EngineException
- problem in the Uppaal engine.protected String recvString(KeyValueProtocol.Service serviceName) throws IOException, EngineException
serviceName
- - The service item from the enum of the serviceIOException
- engine crash or problem in communication.EngineException
- problem in the Uppaal engine.protected String recvBlock(KeyValueProtocol.Service serviceName, boolean allow_progress) throws IOException, EngineException
serviceName
- - The service itemallow_progress
- - The allowed progressIOException
- engine crash or problem in communication.EngineException
- problem in the Uppaal engine.protected List<String> recvLines(KeyValueProtocol.Service serviceName, boolean allow_progress) throws IOException, EngineException
serviceName
- - The service item nameallow_progress
- - The allowed progressIOException
- engine crash or problem in communication.EngineException
- problem in the Uppaal engine.protected List<String> readLines() throws IOException
IOException
- engine crash or problem in communication.protected String escape(String str)
str
- - The input data stringpublic LscProcess uploadLsc(Document document, ArrayList<Problem> problems) throws EngineException, IOException
uploadLsc
in interface Protocol
document
- - The model documentproblems
- - The list of the problemsIOException
- engine crash or problem in communication.EngineException
- problem in the Uppaal engine.public GanttChart getGanttChart(UppaalSystem system, BigDecimal globalTime) throws EngineException, IOException
getGanttChart
in interface Protocol
system
- - The uppaal systemglobalTime
- - The global timeIOException
- engine crash or problem in communication.EngineException
- problem in the Uppaal engine.public ConcreteSuccessor getConcreteSuccessor(UppaalSystem system, ConcreteState state, SystemEdgeSelect[] edges, BigDecimal currentTime, BigDecimal delay) throws EngineException, IOException
getConcreteSuccessor
in interface Protocol
system
- - The uppaal systemstate
- - The concrete stateedges
- - The select edges of the systemcurrentTime
- - The current timedelay
- - The dalay timeIOException
- engine crash or problem in communication.EngineException
- problem in the Uppaal engine.public ConcreteState getConcreteInitial(UppaalSystem system) throws EngineException, IOException
Protocol
getConcreteInitial
in interface Protocol
system
- the compiled Uppaal system representation.EngineException
- error in the server protocol.IOException
- I/O communication error.public SymbolicState getSymbolicInitial(UppaalSystem system) throws EngineException, IOException
Protocol
getSymbolicInitial
in interface Protocol
system
- the compiled Uppaal system representation.EngineException
- error in the server protocol.IOException
- I/O communication error.Copyright © 2014 Uppsala University and Aalborg University. All Rights Reserved.