diff --git a/bin/autfilt.cc b/bin/autfilt.cc index 1b57691ac..9b0fe7419 100644 --- a/bin/autfilt.cc +++ b/bin/autfilt.cc @@ -647,7 +647,7 @@ parse_opt(int key, char* arg, struct argp_state*) jobs.emplace_back(arg, true); break; case 'n': - opt_max_count = to_pos_int(arg); + opt_max_count = to_pos_int(arg, "-n/--max-count"); break; case 'u': opt->uniq = @@ -794,15 +794,17 @@ parse_opt(int key, char* arg, struct argp_state*) break; case OPT_HIGHLIGHT_NONDET: { - int v = arg ? to_pos_int(arg) : 1; + int v = arg ? to_pos_int(arg, "--highlight-nondet") : 1; opt_highlight_nondet_edges = opt_highlight_nondet_states = v; break; } case OPT_HIGHLIGHT_NONDET_STATES: - opt_highlight_nondet_states = arg ? to_pos_int(arg) : 1; + opt_highlight_nondet_states = + arg ? to_pos_int(arg, "--highlight-nondet-states") : 1; break; case OPT_HIGHLIGHT_NONDET_EDGES: - opt_highlight_nondet_edges = arg ? to_pos_int(arg) : 1; + opt_highlight_nondet_edges = + arg ? to_pos_int(arg, "--highlight-nondet-edges") : 1; break; case OPT_HIGHLIGHT_WORD: { @@ -1021,7 +1023,7 @@ parse_opt(int key, char* arg, struct argp_state*) opt_sccs = parse_range(arg, 0, std::numeric_limits::max()); break; case OPT_SEED: - opt_seed = to_int(arg); + opt_seed = to_int(arg, "--seed"); break; case OPT_SEP_SETS: opt_sep_sets = true; diff --git a/bin/common_conv.cc b/bin/common_conv.cc index 4320e6b9a..e63969b16 100644 --- a/bin/common_conv.cc +++ b/bin/common_conv.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2015, 2018 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -22,50 +22,54 @@ #include "error.h" int -to_int(const char* s) +to_int(const char* s, const char* where) { char* endptr; int res = strtol(s, &endptr, 10); if (*endptr) - error(2, 0, "failed to parse '%s' as an integer.", s); + error(2, 0, "failed to parse '%s' as an integer (in argument of %s).", + s, where); return res; } int -to_pos_int(const char* s) +to_pos_int(const char* s, const char* where) { - int res = to_int(s); + int res = to_int(s, where); if (res < 0) - error(2, 0, "%d is not positive", res); + error(2, 0, "%d is not positive (in argument of %s)", res, where); return res; } unsigned -to_unsigned (const char *s) +to_unsigned (const char *s, const char* where) { char* endptr; unsigned res = strtoul(s, &endptr, 10); if (*endptr) - error(2, 0, "failed to parse '%s' as an unsigned integer.", s); + error(2, 0, + "failed to parse '%s' as an unsigned integer (in argument of %s).", + s, where); return res; } float -to_float(const char* s) +to_float(const char* s, const char* where) { char* endptr; float res = strtof(s, &endptr); if (*endptr) - error(2, 0, "failed to parse '%s' as a float.", s); + error(2, 0, "failed to parse '%s' as a float (in argument of %s)", + s, where); return res; } float -to_probability(const char* s) +to_probability(const char* s, const char* where) { - float res = to_float(s); + float res = to_float(s, where); if (res < 0.0 || res > 1.0) - error(2, 0, "%f is not between 0 and 1.", res); + error(2, 0, "%f is not between 0 and 1 (in argument of %s).", res, where); return res; } diff --git a/bin/common_conv.hh b/bin/common_conv.hh index a41894539..617e97e23 100644 --- a/bin/common_conv.hh +++ b/bin/common_conv.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015 Laboratoire de Recherche et Développement de -// l'Epita (LRDE). +// Copyright (C) 2015, 2018 Laboratoire de Recherche et Développement +// de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -22,11 +22,11 @@ #include "common_sys.hh" #include -int to_int(const char* s); -int to_pos_int(const char* s); -unsigned to_unsigned (const char *s); -float to_float(const char* s); -float to_probability(const char* s); +int to_int(const char* s, const char* where); +int to_pos_int(const char* s, const char* where); +unsigned to_unsigned (const char *s, const char* where); +float to_float(const char* s, const char* where); +float to_probability(const char* s, const char* where); // Parse the comma or space seperate string of numbers. std::vector to_longs(const char* s); diff --git a/bin/common_trans.cc b/bin/common_trans.cc index dfd5ab2b9..a0b21e945 100644 --- a/bin/common_trans.cc +++ b/bin/common_trans.cc @@ -802,7 +802,7 @@ static int parse_opt_trans(int key, char* arg, struct argp_state*) tools_push_trans(arg); break; case 'T': - timeout = to_pos_int(arg); + timeout = to_pos_int(arg, "-T/--timeout"); #if !ENABLE_TIMEOUT std::cerr << "warning: setting a timeout is not supported " << "on your platform" << std::endl; @@ -865,7 +865,7 @@ static int parse_opt_autproc(int key, char* arg, struct argp_state*) tools_push_autproc(arg); break; case 'T': - timeout = to_pos_int(arg); + timeout = to_pos_int(arg, "-T/--timeout"); #if !ENABLE_TIMEOUT std::cerr << "warning: setting a timeout is not supported " << "on your platform" << std::endl; diff --git a/bin/ltlcross.cc b/bin/ltlcross.cc index c5591d0f4..e7195bb75 100644 --- a/bin/ltlcross.cc +++ b/bin/ltlcross.cc @@ -448,7 +448,7 @@ parse_opt(int key, char* arg, struct argp_state*) csv_output = arg ? arg : "-"; break; case OPT_DENSITY: - density = to_probability(arg); + density = to_probability(arg, "---density"); break; case OPT_DUPS: allow_dups = true; @@ -472,7 +472,7 @@ parse_opt(int key, char* arg, struct argp_state*) products_avg = false; ++arg; } - products = to_pos_int(arg); + products = to_pos_int(arg, "--products"); if (products == 0) products_avg = false; break; @@ -490,10 +490,10 @@ parse_opt(int key, char* arg, struct argp_state*) tools_push_trans(arg, true); break; case OPT_SEED: - seed = to_pos_int(arg); + seed = to_pos_int(arg, "--seed"); break; case OPT_STATES: - states = to_pos_int(arg); + states = to_pos_int(arg, "--states"); break; case OPT_STOP_ERR: stop_on_error = true; diff --git a/bin/ltldo.cc b/bin/ltldo.cc index d63e4e4ce..1b7afb48a 100644 --- a/bin/ltldo.cc +++ b/bin/ltldo.cc @@ -179,7 +179,7 @@ parse_opt(int key, char* arg, struct argp_state*) best_format = arg; break; case 'n': - opt_max_count = to_pos_int(arg); + opt_max_count = to_pos_int(arg, "-n/--max-count"); break; case ARGP_KEY_ARG: if (arg[0] == '-' && !arg[1]) diff --git a/bin/ltlfilt.cc b/bin/ltlfilt.cc index 127fc511e..dc507ff83 100644 --- a/bin/ltlfilt.cc +++ b/bin/ltlfilt.cc @@ -345,7 +345,7 @@ parse_opt(int key, char* arg, struct argp_state*) output_format = count_output; break; case 'n': - opt_max_count = to_pos_int(arg); + opt_max_count = to_pos_int(arg, "-n/--max-count"); break; case 'q': output_format = quiet_output; @@ -385,10 +385,10 @@ parse_opt(int key, char* arg, struct argp_state*) bsize = parse_range(arg, 0, std::numeric_limits::max()); break; case OPT_BSIZE_MIN: - bsize.min = to_int(arg); + bsize.min = to_int(arg, "--bsize-min"); break; case OPT_BSIZE_MAX: - bsize.max = to_int(arg); + bsize.max = to_int(arg, "--bsize-max"); break; case OPT_DEFINE: opt->output_define.reset(new output_file(arg ? arg : "-")); @@ -487,10 +487,10 @@ parse_opt(int key, char* arg, struct argp_state*) size = parse_range(arg, 0, std::numeric_limits::max()); break; case OPT_SIZE_MIN: - size.min = to_int(arg); + size.min = to_int(arg, "--size-min"); break; case OPT_SIZE_MAX: - size.max = to_int(arg); + size.max = to_int(arg, "--size-max"); break; case OPT_SKIP_ERRORS: error_style = skip_errors; diff --git a/bin/ltlgrind.cc b/bin/ltlgrind.cc index e6f9a2f75..2e141e863 100644 --- a/bin/ltlgrind.cc +++ b/bin/ltlgrind.cc @@ -134,10 +134,10 @@ parse_opt(int key, char* arg, struct argp_state*) switch (key) { case 'm': - mutation_nb = to_unsigned(arg); + mutation_nb = to_unsigned(arg, "-m/--mutations"); break; case 'n': - max_output = to_int(arg); + max_output = to_int(arg, "-n/--max-count"); break; case ARGP_KEY_ARG: // FIXME: use stat() to distinguish filename from string? diff --git a/bin/randaut.cc b/bin/randaut.cc index eeca8a26e..76e17085a 100644 --- a/bin/randaut.cc +++ b/bin/randaut.cc @@ -189,10 +189,7 @@ parse_opt(int key, char* arg, struct argp_state* as) spot::enable_utf8(); break; case 'a': - opt_acc_prob = to_float(arg); - if (opt_acc_prob < 0.0 || opt_acc_prob > 1.0) - error(2, 0, "probability of acceptance set membership " - "should be between 0.0 and 1.0"); + opt_acc_prob = to_probability(arg, "-a/--acc-probability"); break; case 'A': if (looks_like_a_range(arg)) @@ -215,15 +212,13 @@ parse_opt(int key, char* arg, struct argp_state* as) ba_wanted = true; break; case 'e': - opt_density = to_float(arg); - if (opt_density < 0.0 || opt_density > 1.0) - error(2, 0, "density should be between 0.0 and 1.0"); + opt_density = to_probability(arg, "-e/--density"); break; case 'D': opt_deterministic = true; break; case 'n': - opt_automata = to_int(arg); + opt_automata = to_int(arg, "-n/--automata"); break; case 'Q': opt_states = parse_range(arg); @@ -243,7 +238,7 @@ parse_opt(int key, char* arg, struct argp_state* as) opt_colored = true; break; case OPT_SEED: - opt_seed = to_int(arg); + opt_seed = to_int(arg, "--seed"); opt_seed_str = arg; break; case ARGP_KEY_ARG: diff --git a/bin/randltl.cc b/bin/randltl.cc index 042d9fa74..d35871151 100644 --- a/bin/randltl.cc +++ b/bin/randltl.cc @@ -168,7 +168,7 @@ parse_opt(int key, char* arg, struct argp_state* as) output = spot::randltlgenerator::LTL; break; case 'n': - opt_formulas = to_int(arg); + opt_formulas = to_int(arg, "-n/--formulas"); break; case 'P': output = spot::randltlgenerator::PSL; @@ -196,7 +196,7 @@ parse_opt(int key, char* arg, struct argp_state* as) opt_pS = arg; break; case OPT_SEED: - opt_seed = to_int(arg); + opt_seed = to_int(arg, "--seed"); break; case OPT_TREE_SIZE: opt_tree_size = parse_range(arg); diff --git a/tests/core/ltlcross3.test b/tests/core/ltlcross3.test index 2724af33d..16182cbd7 100755 --- a/tests/core/ltlcross3.test +++ b/tests/core/ltlcross3.test @@ -296,9 +296,12 @@ test `grep '"aborted",-1' out.csv | wc -l` -eq 4 test 5 = `wc -l < out.csv` check_csv out.csv +# Diagnose empty automata, and make sure %% is correctly replaced by % +ltlcross --density 2.01 ltl2tgba 2>stderr && exit 1 +grep 'not between 0 and 1' stderr # Diagnose empty automata, and make sure %% is correctly replaced by % -run 1 ltlcross ': %f >%O; echo %%>foo' -f a 2>stderr +run 1 ltlcross --density 0.01 ': %f >%O; echo %%>foo' -f a 2>stderr test 2 = `grep -c ':.*empty input' stderr` cat foo cat >expected<.*' stderr test 2 = `genltl --and-gf=1..4 | ltldo ltl2tgba -n2 | autfilt -c` test 3 = `genltl --and-gf=1..2 | ltldo ltl2tgba 'ltl2tgba -s' -n3 | autfilt -c` +ltldo ltl2tgba -n2a 2>err && exit 1 +grep "ltldo: failed to parse '2a'.*-n" err genltl --rv-counter=9 | ltldo ltl2tgba --stats=' print("%[up]R + %[uc]R + %[sp]R + %[sc]R - %R\n"); diff --git a/tests/core/randaut.test b/tests/core/randaut.test index 0951d2742..6707eb050 100755 --- a/tests/core/randaut.test +++ b/tests/core/randaut.test @@ -1,6 +1,6 @@ #!/bin/sh # -*- coding: utf-8 -*- -# Copyright (C) 2014, 2015, 2016, 2017 Laboratoire de Recherche et +# Copyright (C) 2014, 2015, 2016, 2017, 2018 Laboratoire de Recherche et # Développement de l'Epita (LRDE). # # This file is part of Spot, a model checking library. @@ -22,6 +22,13 @@ set -e +randaut -e foo 2>err && exit 1 +grep "randaut: failed to parse 'foo' as a float (in argument of -e" err +randaut -e 3.14 2>err && exit 1 +grep "randaut: 3.1.*is not between 0 and 1 (in argument of -e" err +randaut -n1a 3 2>err && exit 1 +grep "randaut: failed to parse '1a' as an integer.* -n/--automata)" err + randaut --spin -Q4 a b | ../ikwiad -H -XN - >out grep 'States: 4' out grep 'AP: 2' out