VERIFY can be started up under the assumption that (a) Quintus Prolog
3.0 is installed, and (b) the <#48#>verify<#48#> directory has been
properly installed as described in Section~#start#49>.
There are three ways to get started. Either invoke the QOF file <#50#>verify<#50#> from the Unix command line:
verbatim103#
Alternatively, Quintus Prolog can be invoked under Emacs. First
execute the command <#53#> prolog +<#53#> to run Emacs. At the Prolog
prompt in the Emacs window, VERIFY can be invoked by executing the
Prolog command <#54#>restore(verify).<#54#> (Help for either prolog or
emacs can be obtained by executing the prolog command <#55#>manual.<#55#>).
A third possibility is to call <#56#>qui<#56#> from the Unix command line to
invoke the X11 interface QUI (QUI can usually be invoked by executing
<#393#>22
doing the Prolog procedure <#57#>restore(verify).<#57#> as before.
The Prolog command ``<#58#>routines.<#58#>'' will provide a list of all the
VERIFY procedures that can be invoked.
verbatim104#
In addition, some routines are available for examining the files in
the current directory, or changing to a new directory in the Unix file
system.
- <#1296#><#62#>cd(directory).<#62#> ---<#1296#>
- changes the current directory to be
<#63#>directory<#63#>. For example, cd(..) moves up one level, and
cd(sensor) changes the current directory to the subdirectory <#64#>sensor<#64#>.
- <#1297#><#65#>pwd.<#65#> ---<#1297#>
- returns the path of the current directory.
- <#1298#>Other commands ---<#1298#>
- Other commands include: <#66#>cat(filename),
date, ls(directory), ls-l(directory), ls-l(directory),
ls-a(directory)<#66#> and <#67#>ls-al(directory)<#67#>.
Although VERIFY is up and running, nothing can be verified until two
files are created:
- <#1299#><#70#>sample.ttm<#70#><#1299#>
- --- this is the file containg the Prolog code
describing the real-time system as a TTM called <#71#>sample<#71#>.
- <#1300#><#72#>sample.sf<#72#><#1300#>
- --- this file contains state-formulas that are
used to specify the property to be verified.