public class Engine extends Object
If you want to communicate with the UPPAAL verification engine, this is the class to use. It is a thin wrapper around the EngineStub class and provides a state-less interface to the verification engine. In contrast to the EngineStub class, it can work with several model instances at the same time (although with reduced speed) and transparently connect and reconnect to the engine.
The various connection modes are documented in the EngineStub class.
Before connecting to the engine, a document should be created, please see
Document
for sample code.
The following code demonstrates how to connect to a local UPPAAL engine via standard input/output streams using server protocol:
Engine engine = new Engine(); engine.setServerPath(enginePath); engine.connect();where enginePath is a path to server executable. On Windows the enginePath is "uppaal-version\\bin-Win32\\server.exe" and on Linux it is "uppaal-version/bin-Linux/server".
Alternatively one can use a Linux server by starting socketserver utility on a remote computer. The socketserver uses default port 2350 and can be reached as follows:
Engine engine = new Engine(EngineStub.BOTH, 2350, "hostname", enginePath); engine.connect();If the connection fails, then the local server execution will be used instead.
Then the model document can be uploaded, syntax-checked and compiled as follows:
ArrayList<Problem> problems = new ArrayList<Problem>(); UppaalSystem system = engine.getSystem(doc, problems);The array problems contains errors and warnings if any. If the compilation was successful the system object contains a reference to a compiled system model.
The following code can be used to execute and print random transitions:
SystemState state = engine.getInitialState(system); while (state != null) { ArrayList<Transition> trans = engine.getTransitions(system, state); Transition tr = trans.get((int)Math.floor(Math.random()*trans.size())); if (tr.getSize()==0) { // transition without edges, something special: System.out.println(tr.getEdgeDescription()); } else { // one or more edges involved: System.out.print("("); for (SystemEdge e: tr.getEdges()) { System.out.print(e.getProcessName()+": " + e.getEdge().getName()+", "); } System.out.println(")"); } state = tr.getTarget(); // deadlock "transitions" will give null }The verifier functionality can be accessed by calling the
#query(UppaalSystem, String, QueryProperty, QueryFeedback)
method.
The options string in the query method is a concatenation of one option per line: an option name and a choice name (or one or more values) separated by space.
For example at the time of this writing the default list of options was:
order 0 reduction 1 representation 0 trace 0 extrapolation 0 hashsize 27 reuse 1 smcparametric 1 modest 0 statistical 0.01 0.01 0.05 0.05 0.05 0.9 1.1 0.0 0.0 1280.0 0.01The options may vary from version to version and depends on the actual server binary used. One can inspect the list of available options by requesting
getOptionsInfo()
which will bring an XML
description of all options.Document
,
EngineStub
Modifier and Type | Field and Description |
---|---|
protected EngineStub |
stub
The stub for the server connection.
|
Constructor and Description |
---|
Engine()
Constructs an Engine object for local connections.
|
Engine(int mode,
int port,
String host,
String path)
Constructs an Engine object for the given connection settings.
|
Modifier and Type | Method and Description |
---|---|
void |
cancel()
Forced disconnection from the server.
|
void |
connect()
Connects to the server, if not already connected.
|
protected void |
connected()
Called whenever a connection to the server is established.
|
void |
disconnect()
Disconnect from the server.
|
protected void |
disconnected()
Called when disconnecting from the server.
|
ConcreteState |
getConcreteInitialState(UppaalSystem system)
Computes the concrete initial state of the compiled UPPAAL system.
|
ConcreteSuccessor |
getConcreteSuccessor(UppaalSystem system,
ConcreteState state,
SystemEdgeSelect[] edges,
BigDecimal currentTime,
BigDecimal delay)
Computes a concrete successor after chosen transition and delay.
|
GanttChart |
getGanttChart(UppaalSystem system,
BigDecimal globalTime)
Creates a Gantt chart for the compiled system.
|
SymbolicState |
getInitialState(UppaalSystem system)
Computes the symbolic initial state of the compiled UPPAAL system.
|
LscProcess |
getLscProcess(Document document,
ArrayList<Problem> problems)
Compiles an LSC process from Uppaal document and stores any warnings
and errors in the problems list.
|
String |
getOptionsInfo()
Returns information about available options.
|
UppaalSystem |
getSystem()
Addition for concrete simulation: Get the uppaal system
|
UppaalSystem |
getSystem(Document document,
ArrayList<Problem> problems)
Compiles the document and builds a system instance.
|
ArrayList<SymbolicTransition> |
getTransitions(UppaalSystem system,
SymbolicState state)
Returns the list of outgoing transitions for the state of the
given system.
|
String |
getVersion()
Returns the version string of the server.
|
QueryVerificationResult |
query(UppaalSystem system,
String options,
Query query,
QueryFeedback f)
Verify a query on an instantiated UPPAAL model.
|
void |
setConnectionMode(int mode)
Sets the connection mode.
|
void |
setServerHost(String host)
Sets the server host.
|
void |
setServerPath(String path)
Sets the server path.
|
void |
setServerPort(int port)
Sets the server port.
|
void |
submit(Job job)
Submit the job to the verification engine.
|
protected EngineStub stub
public Engine()
public Engine(int mode, int port, String host, String path)
mode
- specifies mode: EngineStub.LOCAL (executed locally),
EngineStub.SERVER (connected to remote socket) or EngineStub.BOTH
(try remote and fallback to local when socket connection fails).port
- the socket port number (default 2350)host
- the hostname of the remote computer where the socketserver is startedpath
- a path to server binary for local execution.public void setServerPath(String path)
path
- - The new pathpublic void setServerPort(int port)
port
- - The new portpublic void setServerHost(String host)
host
- - The hostpublic void setConnectionMode(int mode)
mode
- - The mode (local, server or both)public void disconnect()
public void cancel()
public String getVersion() throws EngineException, IOException
IOException
- I/O communication error.EngineException
- error in the server protocol.public String getOptionsInfo() throws EngineException, IOException
IOException
- I/O communication error.EngineException
- error in the server protocol.public ArrayList<SymbolicTransition> getTransitions(UppaalSystem system, SymbolicState state) throws EngineException, CannotEvaluateException
system
- - The uppaal systemstate
- - the state of the systemEngineException
- error in the server protocol.CannotEvaluateException
- some expression could not be evaluated.public ConcreteSuccessor getConcreteSuccessor(UppaalSystem system, ConcreteState state, SystemEdgeSelect[] edges, BigDecimal currentTime, BigDecimal delay) throws EngineException, CannotEvaluateException
system
- - The uppaal systemstate
- - The concrete stateedges
- - The array of the selected edgescurrentTime
- - The current timedelay
- - The delay timeEngineException
- error in the server protocol.CannotEvaluateException
public GanttChart getGanttChart(UppaalSystem system, BigDecimal globalTime) throws EngineException
system
- - The uppaal systemglobalTime
- - The global timeEngineException
- error in the server protocol.public UppaalSystem getSystem(Document document, ArrayList<Problem> problems) throws EngineException
document
- the (AST of) Uppaal document .problems
- list for storing problems (warnings and errors).EngineException
- error in the server protocol.public UppaalSystem getSystem()
public SymbolicState getInitialState(UppaalSystem system) throws EngineException, CannotEvaluateException
system
- the compiled Uppaal system instance.EngineException
- error in the server protocol.CannotEvaluateException
- some expression could not be evaluated.public ConcreteState getConcreteInitialState(UppaalSystem system) throws EngineException, CannotEvaluateException
system
- the compiled Uppaal systemEngineException
- error in the server protocol.CannotEvaluateException
- some expression could not be evaluated.public LscProcess getLscProcess(Document document, ArrayList<Problem> problems) throws EngineException
document
- the (AST of) Uppaal document.problems
- - the list for storing problems (warnings and errors).EngineException
- error in the server protocol.public QueryVerificationResult query(UppaalSystem system, String options, Query query, QueryFeedback f) throws EngineException
The given options are applied to the verification.
system
- a reference to compiled system.options
- verification options.query
- a query to be checked.f
- a callback for progress feedback, status and traces.EngineException
- error in the server protocol.public void connect() throws EngineException, IOException
EngineException
- error in the server protocol.IOException
- I/O communication error.protected void connected() throws IOException, EngineException
EngineException
- error in the server protocol.IOException
- I/O communication error.protected void disconnected()
public void submit(Job job)
job
- - The jobCopyright © 2014 Uppsala University and Aalborg University. All Rights Reserved.