improvements to user interface

[Stephen Siegel]

At the end of a verification run, the system just prints "true" of "false". It should say something like "The property holds on all executions" or "The property does not hold: counterexample found".

During a comparison, instead of naming the models "P1" and "P2", how about "Spec" and "Impl".

The stuff initially printed out is as follows:

MiniMP version 1.0
URL: http://vsl.cis.udel.edu

Minimp initialized with 1 process
Program runs in compare mode.
Program parsed succesfully.
IR generated succesfully.

Can we replace that instead with the following form:

+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|    version 1.0       1 Sep 2009       http://vsl.cis.udel.edu/tass   |
+----------------------------------------------------------------------+

            Function          : compare
            specification     : foo.mmp (np=1)
            implementation    : bar.mmp (np=5)
            Deadlock detection: potential [absolute, ignore]
            Reduction         : Urgent [Standard]
            
[etc. for any other options]

For verify model, the Function is "verify" and instead of specification and implementation, just "model".

The stuff about parsing and the IR should only be printed out if the verbose option is selected.

If the user enters an incorrect command line, the system should not only respond with a complaint about the input, but should also display a usage message that describes the commandline interface

Usage:

tass verify [options] model.mmp
tass compare [options] spec.mmp impl.mmp

Options:
  -reduce=std   : no reductions
  -reduce=urgent :

etc.

[ywei]

Fixed.