Backend mode for easier output parsing
This commit is contained in:
@@ -198,7 +198,14 @@ void ModelChecker::printReachWithSucc(void)
|
|||||||
while (!unproc.IsZero()) {
|
while (!unproc.IsZero()) {
|
||||||
BDD t;
|
BDD t;
|
||||||
t = unproc.PickOneMinterm(*pv);
|
t = unproc.PickOneMinterm(*pv);
|
||||||
|
if (opts->backend_mode)
|
||||||
|
{
|
||||||
|
cout << "G " << srs->decodedRctSysStateToStr(t) << endl;
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
cout << "Successors of " << srs->decodedRctSysStateToStr(t) << ":" << endl;
|
cout << "Successors of " << srs->decodedRctSysStateToStr(t) << ":" << endl;
|
||||||
|
}
|
||||||
srs->printDecodedRctSysStates(getSucc(t));
|
srs->printDecodedRctSysStates(getSucc(t));
|
||||||
unproc -= t;
|
unproc -= t;
|
||||||
}
|
}
|
||||||
|
|||||||
@@ -11,6 +11,7 @@ class Options
|
|||||||
bool part_tr_rel;
|
bool part_tr_rel;
|
||||||
bool reorder_reach;
|
bool reorder_reach;
|
||||||
bool reorder_trans;
|
bool reorder_trans;
|
||||||
|
bool backend_mode;
|
||||||
|
|
||||||
double enc_time;
|
double enc_time;
|
||||||
double enc_mem;
|
double enc_mem;
|
||||||
@@ -28,6 +29,8 @@ class Options
|
|||||||
reorder_reach = false;
|
reorder_reach = false;
|
||||||
reorder_trans = false;
|
reorder_trans = false;
|
||||||
|
|
||||||
|
backend_mode = false;
|
||||||
|
|
||||||
enc_time = 0;
|
enc_time = 0;
|
||||||
enc_mem = 0;
|
enc_mem = 0;
|
||||||
ver_time = 0;
|
ver_time = 0;
|
||||||
|
|||||||
@@ -31,7 +31,7 @@ int main(int argc, char **argv)
|
|||||||
int c;
|
int c;
|
||||||
int option_index = 0;
|
int option_index = 0;
|
||||||
|
|
||||||
while ((c = getopt_long(argc, argv, "c:bBmpPrsStTvxzh", long_options,
|
while ((c = getopt_long(argc, argv, "c:bBmpPrsStTvxzXh", long_options,
|
||||||
&option_index)) != -1) {
|
&option_index)) != -1) {
|
||||||
switch (c) {
|
switch (c) {
|
||||||
case 0:
|
case 0:
|
||||||
@@ -106,6 +106,10 @@ int main(int argc, char **argv)
|
|||||||
opts->reorder_trans = true;
|
opts->reorder_trans = true;
|
||||||
break;
|
break;
|
||||||
|
|
||||||
|
case 'X':
|
||||||
|
opts->backend_mode = true;
|
||||||
|
break;
|
||||||
|
|
||||||
case 'h':
|
case 'h':
|
||||||
dump_help_message = true;
|
dump_help_message = true;
|
||||||
break;
|
break;
|
||||||
@@ -259,6 +263,8 @@ void print_help(std::string path_str)
|
|||||||
endl
|
endl
|
||||||
<< " -p -- show progress (where possible)" << endl
|
<< " -p -- show progress (where possible)" << endl
|
||||||
<< endl
|
<< endl
|
||||||
|
<< " -X -- backend mode (makes output parsing easier)" << endl
|
||||||
|
<< endl
|
||||||
<< " Benchmarking options:" << endl
|
<< " Benchmarking options:" << endl
|
||||||
<< " -m -- measure and display time and memory usage" << endl
|
<< " -m -- measure and display time and memory usage" << endl
|
||||||
<< " -B -- display an easy to parse summary (enables -m)" << endl
|
<< " -B -- display an easy to parse summary (enables -m)" << endl
|
||||||
|
|||||||
@@ -573,7 +573,14 @@ void SymRS::printDecodedRctSysStates(const BDD &states)
|
|||||||
|
|
||||||
while (!unproc.IsZero()) {
|
while (!unproc.IsZero()) {
|
||||||
BDD t = unproc.PickOneMinterm(*pv_drs_flat);
|
BDD t = unproc.PickOneMinterm(*pv_drs_flat);
|
||||||
|
if (opts->backend_mode)
|
||||||
|
{
|
||||||
|
cout << "s " << decodedRctSysStateToStr(t) << endl;
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
cout << decodedRctSysStateToStr(t) << endl;
|
cout << decodedRctSysStateToStr(t) << endl;
|
||||||
|
}
|
||||||
|
|
||||||
if (opts->verbose > 9) {
|
if (opts->verbose > 9) {
|
||||||
BDD_PRINT(t);
|
BDD_PRINT(t);
|
||||||
|
|||||||
Reference in New Issue
Block a user