TPS-TEST2 : MEXPR

TPS-TEST2 is a top-level command.
Like TPS-TEST (see the help message for that command), but calls
the TEST top level and attempts to prove one theorem repeatedly with several
different values of some crucial flags, to see how the time taken will vary.

TEST-THEOREMS should contain a list of dotted pairs of theorems and modes
in which they can be proven; the searchlist which is used should have at
least one setting in which the theorem can be proven (otherwise tps-test2
will never finish that theorem).

The output file (by default, tps-test2-output.doc) will contain a summary of
the results. If this file already exists, it will be renamed by adding .bak
to its name.
The command format for TPS-TEST2 is:

 <n>TPS-TEST2 SEARCHLIST QUIET-RUN   EXPU   OUTPUT TESTWIN 
"SYMBOL" "YESNO" "YESNO" "FILESPEC" "YESNO"


The arguments have the following meaning:
SEARCHLIST : Searchlist to use?
QUIET-RUN : Run quietly?
EXPU : EXPUNGE and assert defaults between each theorem?
OUTPUT : Short output file
TESTWIN : Send output to the TEST window?

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage