alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

ltlsynt: handle --algo with XARGMATCH

Browse source 
* bin/ltlsynt.cc: Use XARGMATCH for better error handling.
This commit is contained in:
Alexandre Duret-Lutz 2017-09-26 21:44:37 +02:00
parent 69daf9c261
commit c473e4ca0b
1 changed files with 25 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

42
bin/ltlsynt.cc
View file

@ -27,6 +27,8 @@
#include <unordered_map> #include <unordered_map>
#include <vector> #include <vector>
#include "argmatch.h"
#include "common_aoutput.hh" #include "common_aoutput.hh"
#include "common_finput.hh" #include "common_finput.hh"
#include "common_setup.hh" #include "common_setup.hh"
@ -54,12 +56,6 @@ enum
OPT_REAL OPT_REAL
}; };
enum solver
{
QP,
REC
};
static const argp_option options[] = static const argp_option options[] =
{ {
/**************************************************/ /**************************************************/
@ -72,7 +68,7 @@ static const argp_option options[] =
" propositions", 0}, " propositions", 0},
/**************************************************/ /**************************************************/
{ nullptr, 0, nullptr, 0, "Fine tuning:", 10 }, { nullptr, 0, nullptr, 0, "Fine tuning:", 10 },
{ "algo", OPT_ALGO, "ALGO", 0, { "algo", OPT_ALGO, "qp|rec", 0,
"choose the parity game algorithm, valid ones are rec (Zielonka's" "choose the parity game algorithm, valid ones are rec (Zielonka's"
" recursive algorithm, default) and qp (Calude et al.'s quasi-polynomial" " recursive algorithm, default) and qp (Calude et al.'s quasi-polynomial"
" time algorithm)", 0 }, " time algorithm)", 0 },
@ -104,7 +100,27 @@ std::unordered_map<unsigned, unsigned> bddvar_to_outputnum;
bool opt_print_pg(false); bool opt_print_pg(false);
bool opt_real(false); bool opt_real(false);
solver opt_solver(REC);
enum solver
{
QP,
REC
};
static char const *const solver_args[] =
{
"qp", "quasi-polynomial",
"recursive",
nullptr
};
static solver const solver_types[] =
{
QP, QP,
REC,
};
ARGMATCH_VERIFY(solver_args, solver_types);
solver opt_solver = REC;
namespace namespace
{ {
@ -687,15 +703,7 @@ parse_opt(int key, char* arg, struct argp_state*)
opt_print_pg = true; opt_print_pg = true;
break; break;
case OPT_ALGO: case OPT_ALGO:
if (arg && strcmp(arg, "rec") == 0) opt_solver = XARGMATCH("--algo", arg, solver_args, solver_types);
opt_solver = REC;
else if (arg && strcmp(arg, "qp") == 0)
opt_solver = QP;
else
{
std::cout << "Unknown solver: " << (arg ? arg : "") << '\n';
return 1;
}
break; break;
case OPT_REAL: case OPT_REAL:
opt_real = true; opt_real = true;