There is a global tool configuration that can be saved once set. You can access it through
the
Times configuration dialog shown on the picture below.
Settings are saved in the
.timestoolrc file in your home directory.
Look&Feel Configuration
|
The
GUI tab allows you to choose look and feel of
Times graphical
user interface. Note "Macintosh" and "Windows"
styles are supported only on MacOS and Windows operating systems. The default and recommended
setting is "System" meaning that the look and feel will be chosen automatically according
to your operating system.
Server Connection Configuration
|
The second tab contains server connection options.
Times can perform
simulation and analysis using either local or remote server. The full path and file name of the
local server should be specified in
Path field. If no path specified (only the file name)
then
Times will look for the server executable in the directory where
timestool.jar file is located.
The host name (or IP address) and the port number of a remote server are to be set in the
Host
and
Port fields respectively. Find more information about setting up a remote server in the
Installation chapter.
Using the
Connection group of radio buttons specify which server you want to use. When
Try to... option is selected
Times will try to connect remote (or
local) server first, and in case of failure - the local (or remote) one.
Simulator Configuration
|
In the
Simulator tab you can configure the watches window of the simulator. Enable the
first checkbox if you want to observe internal variables of the automatically generated scheduler
automaton in the simulator. This option also enables showing scheduler transition arguments
in the
Enabled transitions view.
If the second checkbox is enabled, the differences between clocks will be shown in the
Clock
tab of the watches view in addition to the clock intervals.
Verifier Configuration
|
The server options are set in the
Verifier tab. These settings affect schedulability analysis
and verification processes.
- Search order option tells if the symbolic state-space exploration should be performed
in breadth-first or depth-first order.
- State Space Reduction option determines if control-structure analysis should be
performed to reduce the space requirements during verification. Possible values are none,
conservative (control-structure reduction saving all non-comitted states and all loop-entry points),
and aggressive (control-structure reduction saving only loop-entry points). Note that there is
normally a tradeoff between space requirement and speed.
- State Space Representation option determines how the state-space should be represented in
the model checker. Possible values are DBM (Difference Bound Matrices), the Compact Data Structure,
Under Approximation (by bit-state hashing), and Over Approximation (by convex-hull approximation).
- Clock Reduction flag activates (in-)active clock reduction.
- Diagnostic Trace flag enables generating of a trace (if there is one) that shows how
the checked property is (or is not) satisfied. The trace is automatically loaded into the
simulator. Note that this flag is automatically disabled when the State Space Representation
option is set to Over Approximation.
- Use optimized scheduler for tasks without sharing flag tells the Times
tool to generate (whenever possible) an optimized scheduler with two clocks. You can learn
more about two clocks scheduler encoding in our paper "Schedulability
Analysis Using Two Clocks".
Code Generator Configuration
|
In the fifth tab you can configure
Times code generator. In
Times 1.0 beta only brickOS is supported as a target platform.
brickOS is an open source embedded operating system, which provides a C and C++ programming environment
for the Lego Mindstorms Robotics Kits. You can find more about brickOS installation and configuration
here.
- brickOS is the only currently supported target platform.
- Include data logging code tells the Times
tool to include code that will create a log of the brick events when running
over the LNP protocol.
- brickOS directory is a path to the brickOS (legOS) installation
directory.
- Output base name is a path and name that is used as a base for
names of the generated files. When a project is loaded into Times
the output base name is set to the path and name of the project minus the ".xml" suffix.
This means that the Times tool will generate files in the same dirctory as the project file.
Modify this to generate files in another directory and/or with another name.
