Using VTAL

VTAL is written in Java. There are three ways to start it:

If you have downloaded the Java class files and installed them properly in your classpath, you can start VTAL with the command java logic.Main.
You can run the system as an applet from within a browser. This means that you can not load or save your scenario description files, due to the applet security restrictions.
You can run the system as a Castanet channel, by connecting to the Castanet tuner at anton.ida.liu.se:8081. This is as safe as running the system as an applet, since Castanet channels are subject to the same security restrictions as applets; however, you will be able to run the system even when you are offline, and you will be able to load scenario descriptions from and save scenario descriptions to a special local directory. More information about the Castanet tuner is available at http://www.marimba.com.

Below, I will assume that you have already started the system.

Working with scenario descriptions

When you start VTAL, it opens a main window, which looks approximately like this (but without the text in the two text areas):

This window is used when you work with action scenario descriptions.

Writing an action scenario description

Action scenario descriptions are written in the upper (white) text area according to the TAL introduction. You write your action scenario descriptions as plain text. When you want the system to parse your scenario, you can press the Update button or select Convert from the File menu. (This is not necessary if you want to show the models of the scenario; whenever you select an operation that needs the scenario description, it will be re-parsed automatically if it has changed.) Any syntactic or semantic errors will be shown in a dialog box.

Unfortunately, this standard text input field is not very easy to use; in some cases it even refuses to accept certain characters such as '+' and '<'. Usually, it is easier to write scenario descriptions in your favorite text editor and re-read them from disk using the Reload button after you make changes to it.

Opening and saving action scenario descriptions

[These functions cannot be used in an applet.]

You can read scenario descriptions from disk using the File/Open Scenario Description menu item. Select the scenario description file in the dialog box.

You can write scenario descriptions to disk using the File/Save Scenario Description menu item.

If you have read a scenario description from disk or written it to disk, you can reload the file from disk by pressing the Reload button. This is useful if you write your scenario descriptions in an external text editor; every time you make some changes and save them, you press Reload in the VTAL window.

The File/Save Scenario Description in T_EX Format menu item should not be used; it is not fully implemented yet.

Translating action scenario descriptions

When your scenario description is parsed, it is converted into several other forms, some of which are used internally when reasoning about the scenario and some of which correspond to different levels of abstractions between the high-level scenario description you write and the low-level base logic You can choose which translation you want to see in the lower text area by selecting it in the choice box between the text areas:

Original scenario description -- this is the scenario description in the upper text area, parsed and converted back to text.
Instantiated scenario description -- the original scenario description with all action law schemas instantiated with action occurrence statements. This means that if you had "[t1,t2] paint ~> [t1,t2] color := green" and "[5,8] paint", you now have "[5,8] color := green".
L(SD) scenario description -- this is the instantiated scenario description with certain high-level macros expanded.
Expanded scenario description -- the L(SD) scenario description fully expanded into the low-level logic.
Circumscribed scenario description -- the expanded scenario description with the circumscription and no-change axioms added. (These axioms are what forces the logic to conclude that no fluents change unless we have explicitly stated that they must change.)
Internal scenario description -- this is what is really used internally when the models of a scenario description are calculated. This scenario description together with some hard-coded implementation details is logically equivalent to the circumscribed scenario description, but we can reason with this internal representation much more efficiently than with the circumscribed scenario.
Definition of occlusion -- this is the definition of a predicate, "Occlude", in the low-level logic.

Working with more than one scenario description

You can work with more than one scenario description at once by opening more than one main window. Open a new window by selecting File/New window.

Showing the preferred models of a scenario description

There are two ways to show the preferred models of a scenario description:

Select File/Show minimal models, or click the Show models button. A status window will pop up; when all calculations are done, it will disappear and a model window will be shown. This window will show you all preferred models of the scenario description.
Select File/Show interpretation, or click the Show initial button. As in the previous case, a status window will pop up, and when all calculations are done, it will disappear and a model window will be shown. The difference is that with Show interpretation, only a first approximation of the preferred models will be shown. This approximation will in some cases be much faster than if the system had to perform the complete calculations.

You may get an Inherent contradiction in scenario error. This means that your scenario contradicts itself; there are no models of the scenario. This may happen if you state that something should be true and false at the same time, for example.

The model window

The model window above shows some of the models for the Extended Baby Protection Scenario. The rest of the models are shown below:

Timelines and colors

All models are shown as timelines, which show the values of fluents at different points in time. For example, in the lower half of the picture above, we see a model (actually, a "union" of two models) of the Extended Baby Protection Scenario:

There is a fluent called closed(thedoor). This fluent is boolean, so we only show one timeline corresponding to the value of the fluent at the given times. Red means that the fluent is false, green means that the fluent is true, gray means that both values are possible, and white means that although we don't know the value of the fluent, it must have the same value as the previous timepoint.

There are two fluents corresponding to the location of things: loc(gun) and loc(toy). Those fluents are not boolean, and therefore we see one timeline for each possible value. There are three possible locations: table, closet and floor.

The gun is not safe at time 0, 1, 4, or 5. It is definitely safe at time 2 and 3 (since it is in the closet and the door is closed). At time 6 to infinity, we are not sure whether the gun is safe or not (since we don't know whether we put it on the table or on the floor).
The toy is not safe at time 0-7, but it is safe at time 8 to infinity.

Solid colors indicate that the model has the same restrictions on values as the union model does. Lines indicate that the model differs from the union model. This makes it easier to see where the different models actually differ from each other. The following picture shows the same scenario as the previous picture, but scrolled down so that the two ordinary models are shown:

These models are equivalent to the union model, and therefore to each other, except for loc(gun) and safe(gun) at time 6 to infinity.

Actions

The actions that are performed are shown below the timelines. The blue "brackets" show the timepoints at which the actions are performed. This display is very rudimentary at this time:

Concurrent actions are displayed on top of each other
Arguments to actions are not shown at all

The initial interpretation

The uppermost model is not really a model; it is the initial interpretation. This is an initial approximation of the set of models, and can usually be disregarded.

The union of all models

The second "model" shown in the model window is the union of all preferred models. This "model" is not really a model, but it lets you quickly see the restrictions that are common to all models:

If the union model shows that only one value is allowed, then that value will be the same in all real models. For example, the model above shows that safe(gun) is red from time 0 to 1; therefore, the gun is unsafe in all models of the scenario. Similarly, the model shows that loc(gun) can only be closet at time 0, since that is the only green value; therefore, the gun is in the closet at time 0 in all models of the scenario.
If the union model shows that several values are allowed, then all you know is that each of those values is allowed in some scenario, and that none of the other values are allowed in any scenario. For example, loc(gun) is allowed to have the values table or floor at time 6. This means that there is at least one model in which the gun is on the table at time 6, that there is at least one model where the gun is on the floor at time 6, and that there is no model where the gun is in the closet at time 6.
If the union model shows that several values are allowed, there may still be complicated interdependencies between those values! From the union model above, you can see that there is a model where the gun is on the floor at time 6, and that there is a model where the gun is safe at time 6, but this does not mean that there is a model in which the gun is on the floor and safe in the same model at time 6.

Ordinary models

All models after the second one are "ordinary" models.

Manipulating the display

You can change the number of models that are shown at the same time by clicking the Add and Remove buttons.

You can zoom in and zoom out using the Zoom in and Zoom out buttons. Use the scrollbars to move around in the zoomed-in model. Select Zoom/Autozoom now to return to the standard zoom scale. Use the other items in the Zoom menu to zoom in or out only in the x or y direction.

Use the scrollbar to the right or the Page up, Up, Down and Page down buttons to see different models.

Known bugs

This system is still under development; it has not yet been extensively tested in some areas. There are several known bugs, some of which are listed here:

Lexical errors in a scenario description -- unknown characters that can not be part of a legal file -- result in an error message being dumped to the console instead of a dialog box informing the user of the error. The system uses a beta version of a parser generator which currently has no error recovery features; this will change in future versions of the parser generator, and therefore no workaround has been implemented in VTAL.
The system is not thread-safe. It is possible to start two operations at the same time even if those operations will interfere with each other; for example, it is possible to start two "Show models" threads for the same scenario simultaneously, causing the threads to overwrite each others' variable bindings. This will be fixed in future versions.
Some operations are not fully implemented.