There is a global tool configuration that can be saved once set. You can access it through
configuration dialog shown on the picture below.
Settings are saved in the .timestoolrc
file in your home directory.
tab allows you to choose look and feel of Times
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
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)
will look for the server executable in the directory where
file is located.
The host name (or IP address) and the port number of a remote server are to be set in the Host
fields respectively. Find more information about setting up a remote server in the
Using the Connection
group of radio buttons specify which server you want to use. When
option is selected Times
will try to connect remote (or
local) server first, and in case of failure - the local (or remote) one.
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
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.
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
- 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
- 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.