Opened 17 years ago
Last modified 17 years ago
#21 closed enhancement
improvements to user interface — at Version 1
| Reported by: | Stephen Siegel | Owned by: | ywei |
|---|---|---|---|
| Priority: | minor | Milestone: | |
| Component: | User Interface | Version: | 1.0 |
| Keywords: | Cc: |
Description (last modified by )
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.
