Package com.uppaal.engine
Interface Protocol
-
- All Known Implementing Classes:
DotProtocol
,KeyValueProtocol
public interface Protocol
-
-
Method Summary
All Methods Instance Methods Abstract Methods Modifier and Type Method Description void
close()
Disconnect from the server.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 successorGanttChart
getGanttChart(UppaalSystem system, BigDecimal globalTime)
Get the gantt chartString
getLeaseRequest(String license_key, String duration)
Generate a lease request for the given license keyString
getLicensee()
Retrieves licensee information from associated valid license/lease information.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.String
installLease(String lease)
Installs an encrypted and encoded lease from the license server webpage.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.void
setOptions(String options)
Sets server options used for verification.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)
-
-
-
Method Detail
-
close
void close() throws IOException
Disconnect from the server.- Throws:
IOException
- engine crash or problem in communication.
-
getVersion
String getVersion() throws IOException, EngineException
Returns the version string of the server. The stub must be connected.- Returns:
- The version
- Throws:
IOException
- engine crash or problem in communication.EngineException
- problem in the Uppaal engine.
-
getLicensee
String getLicensee() throws IOException, EngineException
Retrieves licensee information from associated valid license/lease information.- Returns:
- licensee name
- Throws:
IOException
EngineException
-
getLeaseRequest
String getLeaseRequest(String license_key, String duration) throws IOException, EngineException
Generate a lease request for the given license key- Parameters:
license_key
- the license keyduration
- the lease duration period- Returns:
- an encrypted and encoded lease request to be submitted to license server.
- Throws:
IOException
EngineException
-
installLease
String installLease(String lease) throws IOException, EngineException
Installs an encrypted and encoded lease from the license server webpage.- Parameters:
lease
- the lease response from the license server- Returns:
- Throws:
IOException
EngineException
-
getOptionsInfo
String getOptionsInfo() throws EngineException, IOException
Returns information about available options. The information is returned as an XML document. The stub must be connected.- Returns:
- The options information
- Throws:
IOException
- engine crash or problem in communication.EngineException
- problem in the Uppaal engine.
-
setOptions
void setOptions(String options) throws EngineException, IOException
Sets server options used for verification. The stub must be connected. TODO: Document format.- Parameters:
options
- - The options string- Throws:
IOException
- engine crash or problem in communication.EngineException
- problem in the Uppaal engine.
-
getSymbolicInitial
SymbolicState getSymbolicInitial(UppaalSystem system) throws EngineException, IOException, CannotEvaluateException
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.- Parameters:
system
- the compiled Uppaal system representation.- Returns:
- initial symbolic state.
- Throws:
IOException
- I/O communication error.EngineException
- error in the server protocol.CannotEvaluateException
- some expression could not be evaluated.
-
getConcreteInitial
ConcreteState getConcreteInitial(UppaalSystem system) throws EngineException, IOException, CannotEvaluateException
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.- Parameters:
system
- the compiled Uppaal system representation.- Returns:
- initial concrete state
- Throws:
IOException
- I/O communication error.EngineException
- error in the server protocol.CannotEvaluateException
- some expression could not be evaluated.
-
getConcreteSuccessor
ConcreteSuccessor getConcreteSuccessor(UppaalSystem system, ConcreteState state, SystemEdgeSelect[] edges, BigDecimal currentTime, BigDecimal delay) throws EngineException, IOException, CannotEvaluateException
Get the concrete simulation successor- Parameters:
system
- - The uppaal systemstate
- - The concrete simulator stateedges
- - The vector of the selected system edgescurrentTime
- - the current simulation timedelay
- - The delay time- Returns:
- concrete successor object
- Throws:
IOException
- I/O communication error.EngineException
- error in the server protocol.CannotEvaluateException
- some expression could not be evaluated.
-
getGanttChart
GanttChart getGanttChart(UppaalSystem system, BigDecimal globalTime) throws EngineException, IOException
Get the gantt chart- Parameters:
system
- - The uppaal systemglobalTime
- - The global time- Returns:
- The gantt chart object
- Throws:
IOException
- I/O communication error.EngineException
- error in the server protocol.
-
getTransitions
ArrayList<SymbolicTransition> getTransitions(UppaalSystem system, SymbolicState state) throws EngineException, IOException, CannotEvaluateException
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.- Parameters:
system
- - The uppaal systemstate
- - The symbolic state of the system- Returns:
- The array list of the symbolic transition
- Throws:
IOException
- I/O communication error.EngineException
- error in the server protocol.CannotEvaluateException
- some expression could not be evaluated.
-
upload
UppaalSystem upload(Document document, ArrayList<Problem> problems) throws EngineException, IOException
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.- Parameters:
document
- - The system documentproblems
- - The problem array list- Returns:
- the compiled system representation
- Throws:
IOException
- I/O communication error.EngineException
- error in the server protocol.
-
uploadLsc
LscProcess uploadLsc(Document document, ArrayList<Problem> problems) throws EngineException, IOException
- Throws:
EngineException
IOException
-
upload
UppaalSystem upload(Document document) throws EngineException, IOException
Upload the document to the server. If no errors occurred, the instantiated system is returned. Otherwise, null is returned. The stub must be connected.- Parameters:
document
- - The system document- Returns:
- The Uppaal system
- Throws:
IOException
- I/O communication error.EngineException
- error in the server protocol.
-
query
QueryResult query(UppaalSystem system, Query query, QueryFeedback f) throws EngineException, IOException
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.- Parameters:
system
- - The uppaal systemquery
- - The queryf
- - The query feed back- Returns:
- The query verification results
- Throws:
IOException
- I/O communication error.EngineException
- error in the server protocol.
-
query
QueryResult query(UppaalSystem system, SymbolicState state, Query query, QueryFeedback f) throws EngineException, IOException, CannotEvaluateException
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.- Parameters:
system
- system model representationstate
- initial symbolic statequery
- the property to check forf
- feedback handler- Returns:
- Throws:
EngineException
IOException
CannotEvaluateException
-
-