Frac 2.8.0 Release Notes:

TINA Version 3.8.0 introduced ktz profiles, the scan tool and some enhancements of the model checking tools selt and muse (notably option -script). In addition to supporting the previous verification workflows for fiacre descriptions, frac 2.8.0 takes advantage of these additions.

Ktz profiles:

As of tina version 3.8.0, 6 ktz profile options have been added:

- to tool sift, for a reduction of ktz size at the source;

- to tool ktzio, for a reduction of ktz size in retrospect.

See ktz profiles for details.

Scan tool -- Verification of reachability properties:

In addition of selt (for checking LTL properties) and muse (for mu-calculus properties), tool scan checks reachability from a ktz file on the fly:

- scan model.ktz -n f is true if no state of model.ktz obeys f (we
therefore check AG -f in CTL speak).

- scan model.ktz -r f is true if at least one state of model.ktz satisfies f (we therefore check EF f in CTL speak). For memory, the "present f" pattern of fiacre expresses AF f, which is stronger.

- option -id s: if -script is passed (see below) and the output is boolean (-b), prints the string s before the boolean result instead of the verified formula. This makes possible to identify the property checked in a similar way to the assert command of selt or muse.

Option -script for selt, muse and scan tools:

The option must appear at the end of the command line. Its effects are:

- For selt/muse: the first expected argument is a file of commands in ltl/mmc format; the second if the ktz file (without -script, it's the opposite).

- For selt/muse: property declarations are silent (nothing is printed).

- For selt/muse/scan: if the output is boolean (-b), and if no message to print after evaluation of a formula is specified by an assert command (or by the -id option for scan), then the verified formula is printed before the result of its evaluation.

The intended use of the -script option is obviously to allow to use selt or muse as script interpreters; in this usage, the first argument passed is the script itself. For tool scan, which does not have a language of commands, the script is a shell script invoking tool scan; option -script only provides then echoing of properties (see third item above).

"prove" verification directive in fiacre descriptions

The "assert" verification directive is renamed into "prove" and admits in addition a formula as an argument (which can of course be an identifier). The assert directive is still accepted but a warning flags it as obsolete and frac handles it like prove.

New model-checking options for frac and tts descriptions:

So far, whether or not properties are specified in the source fiacre, frac generated a file a .ltl file of commands for tool selt, check on the .ktz file built from the .tts description by tina or sift. From now on, in addition to the .ltl file produced by default, frac can also produce a .mmc file for verification by the muse tool or a
.rch shell script for verification by the scan tool. This is controled by frac by three additional options:

-selt if you want the generation of the .ltl file (default);

-muse if you also want the generation of .mmc for muse;

-scan if you also want the generation of .rch for scan.

Note that in all cases, for backward compatibility reasons, the .ltl file is produced.

- The .ltl file contains the fiacre properties translated into LTL for tool selt, for those definable in LTL. A warning will be issued by frac for each property not definable in LTL;

- The .mmc file contains the fiacre properties translated into CTL for muse, for those definable in CTL (a warning is printed by frac for the others);

- The .rch file contains the fiacre properties translated into reachability properties and corresponding scan calls, for those definable (a warning is printed by frac for those which are no).

Note: LTL properties can have the same truth value as their negation, this because they are implicitly universally quantified over all execution traces. This is not true for the logics supported by tools muse and scan. Accordingly, Fiacre formulas checked by muse or scan do not necessarily have the same truth value as that of their translation into LTL for tool selt; This can be confusing for beginners; beware of this seemingly counterintuitive aspect of LTL when interpreting verification results.

Also, to make verification easier:

On Unix/Linux, frac makes executable the files .ltl, .mmc and .rch generated (for Windows, MinGW or Cygwin, you will have to do it by hand). If the tina tools are found by the PATH, we can check properties by running these scripts with ktz file produced by sift as argument, rather than invoking selt, muse or scan by hand (which is still possible). Typical workflows will be:

As before version 2.8.0 (and still possible):

Build the ktz file by: sift app.tts app.ktz Check properties by:
selt app.ktz -q -b app.tts/app.ltl
and/or:
muse app.ktz -q -b app.tts/app.mmc


(it is up to you to sort the results)

Note: The -muse option was not then public then (nor correct!), and the scan tool was not available.>/p>

Or making use of 2.8.0 enhancements:

For verification by selt or muse:

build the ktz file by:
sift app.tts [-ks] app-ks.ktz

check properties by:
app.tts/app.ltl app-ks.ktz
and/or:
app.tts/app.mmc app-ks.ktz

For selt (.ltl script) and muse (.mmc script), the ktz file must provide the reachability relation, its profile must therefore be kts (default), lts or ks. The kts profile is always adequate. The lts profile is if the properties only involve transitions. Dually, the ks profile is adequate if they only involve states. If applicable, profles lts and ks may significantly reduce the size of the ktz file.

For verification by scan:
build the ktz file by:
sift app.tts -rsd app-rsd.ktz
or, if a ktz file app.ktz with profile kts of ks has already been produced:
ktzio app.ktz -rsd app-rsd.ktz
check properties by:
app.tts/app.rch app-rsd.ktz

For scan (.rch script), any profile is acceptable, but the benefit is maximum with the three profiles retaining only the state properties and without the transition relation: rsf if the properties can also concern the firable transitions, rsd if we wish to keep deadlocks, or rs otherwise. The recommended rsd profile drastically reduces the size of the ktz file.

The scripts print for each directive "prove" the property verified followed by the result of its verification, or the message specified by the prove options, if any. No post processing of the results is therefore necessary, in general, for the presentation of verification results.

Compatibility

Finally, note that the properties of fiacre descriptions can be checked exactly like they were in frac versions 2.7.0 and earlier, with any version of the tina toolbox; backward compatibility is enforced. For benefiting from ktz profiles or tool scan, you will need to use tina-3.8.0 or later.