G.  Task Directories

The system generates in the current working directory (respectively the directory specified by the ) two subdirectories named .ProofNavigator and .PETASKS.Tag.0.

The directory .ProofNavigator represents a context directory of essentially that form that is described in the manual of the RISC ProofNavigator [5]; it is used, if the user enters in the Analyze view directly (not in the context of any task as described below) commands for the RISC ProofNavigator. In order to save disk space, the format of the entries has been slightly changed: for every declaration of a logical entity name of kind kind, rather than three separate files kind_name_hash.txt, kind_name_time.txt, and kind_name_refs.xml, a single file kind_name_info.xml is generated that combines the information of the three files; furthermore, the file kind_name_decl.xgz is not generated any more.

The directory .PETASKS.Tag.0 represents the persistent store for the task tree of the program; Tag is a number that denotes the time when the program was started that created this directory. The content of the directory is a hierarchy of subdirectories that corresponds to the hierarchy of task folders and tasks of the program. Each directory is named Name.Tag.Cntr where Name is derived from the name of the task folder respectively task, Tag denotes the time when the program was started that created this directory, and Cntr represents an automatically generated sequence counter.

The content of each task directory depends on the particular kind of the task. Currently the directory may contain the following items:

File goal_

This file contains the log of an attempt to perform the task fully automatically by translating it to a CVCL query and invoking CVCL.

Directory ProofNavigator

This represents a context directory of the RISC ProofNavigator [5] that contains all information related to an attempt to perform the task by a computer-assisted manual proof (also here the contents have been slightly changed as described above).

The directory .PETASKS.Tag.0 and each of its subdirectories contains a file .PEDIR; if the directory contains also a file FREED this indicates that the directory was freed and may be reused. If a new directory is to be created, it is first attempted to reuse a directory with the same basic Name from a previous invocation of the program (as indicated by Tag) or a freed directory of the same invocation (as indicated by Tag and FREED); in both cases, thus previously created RISC ProofNavigator proofs of tasks with the same names will be retained. Otherwise, a new directory is created; if a directory of the desired name already exists, the value of Cntr is incremented to yield a new directory name.