The version of LTSA contained on the CDROM included with the book and in the download (version 7/1/99) has the three bugs listed below, in decreasing order of importance. It is unlikely that you will encounter any of these problems in using the LTSA and they do not affect the correctness of any of the FSP models in the book. To update your copy of the software contained on the CDROM or from the download, first download the following classes.zip file:
Simply copy the downloaded classes.zip file into the directory "$(INSTALLDIR)/Concurrency/lib". The default value for $(INSTALDIR) when you installed the Concurrency software was "C:/Program Files". The new classes.zip file replaces the file of the same name in "$(INSTALLDIR)/Concurrency/lib".
LTSA uses a lazy composition strategy to avoid the problem of state explosion in intermediate composite processes. If the minimize during composition option is not set then where possible, the LTSA does not build the composite process but delays it until the target composition is built. In some circumstance, it is not safe to delay the composition (eg. when hiding is used) and then LTSA builds the intermediate composition. In the version of LTSA released with the book, there are some situations where the intermediate composite is not built when it should be. When this occurs, the target composition is incorrect. The bug happens when a relabelling of the target composite causes additional synchronization in an intermediate-level (constituent) composite process. An example of this situation is shown below:
P = (a->b->c->STOP). Q = (c->d->e->STOP). ||S = (P||Q). ||F = S/{n/{b,d}}.For target F to be built correctly, S must be composed before F. The new release of LTSA, automatically performs this composition.
When high priority ("<<") is applied to a process then the actions in the high-priority set should be higher than the silent action "tau". In the LTSA released with the book, "tau" has the same priority as the high-priority actions. This release deals with the priority of "tau" correctly. Note that the previous release deals correctly with the priority of "tau" in relation to the low-priority operator (">>") and since priority must be applied before hiding, the problem described above does not usually arise.
The new release allows label valued variables, that can be converted to integers, to be used in expressions, the previous release did not. For example, the process below would not compile under the previous release, put does with this release:
set I = {[0],[5],[10]} P = P[0], P[x:I] = (a[x] -> if x<10 then P[x+5]).
This version is a precursor of a version that will support visual animations, the only symptom of this is that animation, actions and controls are now reserved words.
The version number of LTSA can be found in the Help/About dialogue box.