Simplified result report
This commit is contained in:
@@ -601,8 +601,12 @@ bool ModelChecker::checkRSCTLKfull(FormRSCTLK *form)
|
|||||||
|
|
||||||
cleanup();
|
cleanup();
|
||||||
|
|
||||||
cout << "Formula " << form->toStr() << (result ? " holds" : " does not hold")
|
if (opts->backend_mode) {
|
||||||
<< endl;
|
cout << "Result:" << result << endl;
|
||||||
|
} else {
|
||||||
|
cout << "Formula " << form->toStr() << (result ? " holds" : " does not hold")
|
||||||
|
<< endl;
|
||||||
|
}
|
||||||
|
|
||||||
if (opts->measure) {
|
if (opts->measure) {
|
||||||
opts->ver_time = cpuTime() - opts->ver_time;
|
opts->ver_time = cpuTime() - opts->ver_time;
|
||||||
@@ -665,8 +669,12 @@ bool ModelChecker::checkRSCTLKbmc(FormRSCTLK *form)
|
|||||||
|
|
||||||
cleanup();
|
cleanup();
|
||||||
|
|
||||||
cout << "Formula " << form->toStr() << " " << (result ? "holds" :
|
if (opts->backend_mode) {
|
||||||
"does not hold") << endl;
|
cout << "result:" << result << endl;
|
||||||
|
} else {
|
||||||
|
cout << "Formula " << form->toStr() << " " << (result ? "holds" :
|
||||||
|
"does not hold") << endl;
|
||||||
|
}
|
||||||
|
|
||||||
if (opts->measure) {
|
if (opts->measure) {
|
||||||
opts->ver_time = cpuTime() - opts->ver_time;
|
opts->ver_time = cpuTime() - opts->ver_time;
|
||||||
|
|||||||
Reference in New Issue
Block a user