Configuration Browser friendly
Back to Contents
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.

(C) 2004 DARTS, IT Dept, CS, Uppsala University, Sweden