Tool for UML Activity Diagrams (TATD).
----------------------------------------------
This tool is intended for UML activity diagrams (ATDs).
More about the drawing of ATDs can be found in chapter 5 of the 
user's guide and more about the use of this notation technique 
can be found in appendix A of the user's guide.
TATD supports model checking. More information about model 
checking can be found below.

Diagram editing in general.
---------------------------
Diagrams that are made by a diagram editor are a special
kind of graph consisting of nodes and edges and with a certain 
representation. In the representation of a graph, nodes and edges are 
shown as shapes (boxes, lines, diamonds etc.).

Documents should satisfy certain constraints. Most constraints 
are specific for the particular diagram technique supported by the 
editor. In the editors there are three kinds of constraints:
 
1. Built-in constraints which are constraints which can never be 
violated because there is no command in the user interface to achieve 
that.
 
2. Immediately enforced constraints: when you perform a command that 
would violate a constraint that is immediately enforced, this command 
is rejected immediately by the editor and a pop-up window with an error 
message is displayed.
 
3. Soft constraints which are constraints that can be violated.
Soft constraints are checked by the editor when the Check Document 
from the Document menu is issued by you. Check Document displays a list 
of error messages in a pop-up window. As opposed to the previous two 
classes of constraints, you are responsible for correcting the diagram.

Model checking.
---------------
With model checking, one can automatically verify whether or not an
activity diagram satisfies a particular requirement, given by the user.
If the activity diagram fails to satisfy the requirement, the counter-
example returned by the model checker is highlighted in the diagram.
Some entries under the Document menu are related to model checking. 

- Model Check Property: a popup dialog box appears in which you can type
a temporal logic formula (LTL or CTL). If you refer to a node n in the
diagram, use `in(n)' in your formula. Checkbox `syntactic encoding' 
means that the syntax of activity diagrams is encoded directly as input 
for the model checker. THIS ONLY WORKS FOR SAFE ACTIVITY DIAGRAMS. TCM
DOES NOT CHECK WHETHER OR NOT AN ACTIVITY DIAGRAM IS SAFE. 
Checkbox `reduction' means that the activity diagram is reduced (without 
sacrificing the truth value of the property!), before feeding it to the 
model checker. Checkbox `strong fairness' means that every loop is exited 
eventually. Preferred usage: check `reduction' and `strong fairness'. 

- Clear Trace: undo the highlighting of the counterexample trace.