Class Engine
- java.lang.Object
-
- com.uppaal.engine.Engine
-
public class Engine extends Object
State-less wrapper for a UPPAAL server connection.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();
whereenginePath
is a path to server executable. On Windows theenginePath
is"uppaal-version\\bin-Windows\\verifyta.exe"
and on Linux it is"uppaal-version/bin-Linux/verifyta"
.Alternatively one can use a Linux server by starting
socketserver
utility on a remote computer. Thesocketserver
uses default port 2350 and can be reached as follows:Engine engine = new Engine(EngineStub.BOTH, 2350, "hostname", enginePath); engine.connect();
If the remote connection fails, then the local engine 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 arrayproblems
contains errors and warnings if any. If the compilation was successful thesystem
object contains a reference to a compiled system model.The following code can be used to execute and print random transitions:
SymbolicState state = engine.getInitialState(system); while (state != null) { ArrayList<SymbolicTransition> 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 }
Theverifier
functionality can be accessed by calling thequery(UppaalSystem, String, Query, 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, one can set the search order and diagnostic trace with the following options:
--search-order 0 --diagnostic 0
The options may vary from version to version and depends on the actualverifyta
binary used. One can inspect the list of available options by requestinggetOptionsInfo()
which will bring an XML description of all available options.- See Also:
Document
,EngineStub
-
-
Field Summary
Fields Modifier and Type Field Description protected EngineStub
stub
The stub for the server connection.
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method 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.String
getLeaseRequest(String key, String duration)
String
getLicensee()
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 systemUppaalSystem
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.void
leaseInstall(String lease)
QueryResult
query(UppaalSystem system, SymbolicState state, String options, Query query, QueryFeedback f)
Verify a guery on an instantiated UPPAAL model.QueryResult
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.
-
-
-
Field Detail
-
stub
protected EngineStub stub
The stub for the server connection.
-
-
Constructor Detail
-
Engine
public Engine()
Constructs an Engine object for local connections. Make sure the engine path is set before connecting.
-
Engine
public Engine(int mode, int port, String host, String path)
Constructs an Engine object for the given connection settings.- Parameters:
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 toserver
binary for local execution.
-
-
Method Detail
-
setServerPath
public void setServerPath(String path)
Sets the server path. The server path should include the path to, filename of and options for the server binary.- Parameters:
path
- - The new path
-
setServerPort
public void setServerPort(int port)
Sets the server port. The server port is used in REMOTE mode to determine which port on the server to connect to.- Parameters:
port
- - The new port
-
setServerHost
public void setServerHost(String host)
Sets the server host. In SERVER mode the engine will try to connect to this host.- Parameters:
host
- - The host
-
setConnectionMode
public void setConnectionMode(int mode)
Sets the connection mode. Mode is either LOCAL, SERVER or BOTH. In BOTH the stub will first try to build a remote connection and if that fails attempt to create a local connection.- Parameters:
mode
- - The mode (local, server or both)
-
disconnect
public void disconnect()
Disconnect from the server.
-
cancel
public void cancel()
Forced disconnection from the server.
-
getVersion
public String getVersion() throws EngineException, IOException
Returns the version string of the server.- Returns:
- the server version
- Throws:
IOException
- I/O communication error.EngineException
- error in the server protocol.
-
getLicensee
public String getLicensee()
-
getLeaseRequest
public String getLeaseRequest(String key, String duration) throws EngineException
- Throws:
EngineException
-
leaseInstall
public void leaseInstall(String lease) throws EngineException
- Throws:
EngineException
-
getOptionsInfo
public String getOptionsInfo() throws EngineException, IOException
Returns information about available options. The information is returned as an XML document.- Returns:
- The option information
- Throws:
IOException
- I/O communication error.EngineException
- error in the server protocol.
-
getTransitions
public ArrayList<SymbolicTransition> getTransitions(UppaalSystem system, SymbolicState state) throws EngineException, CannotEvaluateException
Returns the list of outgoing transitions for the state of the given system.- Parameters:
system
- - The uppaal systemstate
- - the state of the system- Returns:
- The list of outgoing transitions for the state
- Throws:
EngineException
- error in the server protocol.CannotEvaluateException
- some expression could not be evaluated.
-
getConcreteSuccessor
public ConcreteSuccessor getConcreteSuccessor(UppaalSystem system, ConcreteState state, SystemEdgeSelect[] edges, BigDecimal currentTime, BigDecimal delay) throws EngineException, CannotEvaluateException
Computes a concrete successor after chosen transition and delay.- Parameters:
system
- - The uppaal systemstate
- - The concrete stateedges
- - The array of the selected edgescurrentTime
- - The current timedelay
- - The delay time- Returns:
- The concrete successor
- Throws:
EngineException
- error in the server protocol.CannotEvaluateException
-
getGanttChart
public GanttChart getGanttChart(UppaalSystem system, BigDecimal globalTime) throws EngineException
Creates a Gantt chart for the compiled system.- Parameters:
system
- - The uppaal systemglobalTime
- - The global time- Returns:
- the Gantt chart
- Throws:
EngineException
- error in the server protocol.
-
getSystem
public UppaalSystem getSystem(Document document, ArrayList<Problem> problems) throws EngineException
Compiles the document and builds a system instance. Problems (warnings and errors) are stored in the problems vector.- Parameters:
document
- the (AST of) Uppaal document .problems
- list for storing problems (warnings and errors).- Returns:
- the system if success, null otherwise.
- Throws:
EngineException
- error in the server protocol.
-
getSystem
public UppaalSystem getSystem()
Addition for concrete simulation: Get the uppaal system- Returns:
- system - The uppaal system
-
getInitialState
public SymbolicState getInitialState(UppaalSystem system) throws EngineException, CannotEvaluateException
Computes the symbolic initial state of the compiled UPPAAL system.- Parameters:
system
- the compiled Uppaal system instance.- Returns:
- the initial symbolic state
- Throws:
EngineException
- error in the server protocol.CannotEvaluateException
- some expression could not be evaluated.
-
getConcreteInitialState
public ConcreteState getConcreteInitialState(UppaalSystem system) throws EngineException, CannotEvaluateException
Computes the concrete initial state of the compiled UPPAAL system. If not successful an exception is thrown.- Parameters:
system
- the compiled Uppaal system- Returns:
- concrete initial state
- Throws:
EngineException
- error in the server protocol.CannotEvaluateException
- some expression could not be evaluated.
-
getLscProcess
public LscProcess getLscProcess(Document document, ArrayList<Problem> problems) throws EngineException
Compiles an LSC process from Uppaal document and stores any warnings and errors in the problems list.- Parameters:
document
- the (AST of) Uppaal document.problems
- - the list for storing problems (warnings and errors).- Returns:
- The LSC process representation
- Throws:
EngineException
- error in the server protocol.
-
query
public QueryResult query(UppaalSystem system, String options, Query query, QueryFeedback f) throws EngineException
Verify a query on an instantiated UPPAAL model.The given options are applied to the verification.
- Parameters:
system
- a reference to compiled system.options
- verification options.query
- a query to be checked.f
- a callback for progress feedback, status and traces.- Returns:
- 'T' if property is satisfied, 'F' if it is not satisfied, 'M' if it is maybe satisfied, and 'E' if an error occurred.
- Throws:
EngineException
- error in the server protocol.
-
query
public QueryResult query(UppaalSystem system, SymbolicState state, String options, Query query, QueryFeedback f) throws EngineException, IOException
Verify a guery on an instantiated UPPAAL model.The given options are applied to the verification.
- Parameters:
system
- a reference to compiled system.state
- a custom initial stateoptions
- verification options.query
- a query to be checked.f
- a callback for progress feedback, status and traces.- Returns:
- 'T' if property is satisfied, 'F' if it is not satisfied, 'M' if it is maybe satisfied, and 'E' if an error occurred.
- Throws:
EngineException
IOException
-
connect
public void connect() throws EngineException, IOException
Connects to the server, if not already connected.- Throws:
EngineException
- error in the server protocol.IOException
- I/O communication error.
-
connected
protected void connected() throws IOException, EngineException
Called whenever a connection to the server is established.- Throws:
EngineException
- error in the server protocol.IOException
- I/O communication error.
-
disconnected
protected void disconnected()
Called when disconnecting from the server.
-
submit
public void submit(Job job)
Submit the job to the verification engine.- Parameters:
job
- - The job
-
-