diff --git a/ChangeLog b/ChangeLog index 92dc644fa..18d103340 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,8 @@ 2005-02-02 Alexandre Duret-Lutz + * src/tgbaalgos/randomgraph.cc (random_graph): Make sure n > 0. + * src/tgbatest/randtgba.cc: Check the range of all arguments. + * bench/emptchk/models/eeaean1.pml: New file, from schwoon.05.tacas. * bench/emptchk/Makefile.am: Distribute models/eeaean1.pml and build models/eeaean1.tgba. diff --git a/src/tgbaalgos/randomgraph.cc b/src/tgbaalgos/randomgraph.cc index bf4904e8c..3575f5d7a 100644 --- a/src/tgbaalgos/randomgraph.cc +++ b/src/tgbaalgos/randomgraph.cc @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -94,6 +94,7 @@ namespace spot int n_acc, float a, float t, ltl::environment* env) { + assert(n > 0); tgba_explicit* res = new tgba_explicit(dict); int props_n = ap->size(); diff --git a/src/tgbaalgos/randomgraph.hh b/src/tgbaalgos/randomgraph.hh index fec64cb3f..7f776a61c 100644 --- a/src/tgbaalgos/randomgraph.hh +++ b/src/tgbaalgos/randomgraph.hh @@ -1,4 +1,4 @@ -// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), +// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. // @@ -33,7 +33,7 @@ namespace spot /// \brief Construct a tgba randomly. /// \ingroup tgba_misc /// - /// \param n The number of states wanted in the automata. All states + /// \param n The number of states wanted in the automata (>0). All states /// will be connected, and there will be no dead state. /// \param d The density of the automata. This is the probability /// (between 0.0 and 1.0), to add a transition between two diff --git a/src/tgbatest/randtgba.cc b/src/tgbatest/randtgba.cc index 99bc2e96e..4d1118158 100644 --- a/src/tgbatest/randtgba.cc +++ b/src/tgbatest/randtgba.cc @@ -214,6 +214,7 @@ syntax(char* prog) exit(2); } + int to_int(const char* s) { @@ -227,6 +228,32 @@ to_int(const char* s) return res; } +int +to_int_pos(const char* s, const char* arg) +{ + int res = to_int(s); + if (res <= 0) + { + std::cerr << "argument of " << arg + << " (" << res << ") must be positive" << std::endl; + exit(1); + } + return res; +} + +int +to_int_nonneg(const char* s, const char* arg) +{ + int res = to_int(s); + if (res < 0) + { + std::cerr << "argument of " << arg + << " (" << res << ") must be nonnegative" << std::endl; + exit(1); + } + return res; +} + float to_float(const char* s) { @@ -241,6 +268,19 @@ to_float(const char* s) return res; } +float +to_float_nonneg(const char* s, const char* arg) +{ + float res = to_float(s); + if (res < 0) + { + std::cerr << "argument of " << arg + << " (" << res << ") must be nonnegative" << std::endl; + exit(1); + } + return res; +} + struct ec_stat { int max_tgba_states; @@ -1086,14 +1126,14 @@ main(int argc, char** argv) { if (argc < argn + 3) syntax(argv[0]); - opt_n_acc = to_int(argv[++argn]); - opt_a = to_float(argv[++argn]); + opt_n_acc = to_int_nonneg(argv[++argn], "-a"); + opt_a = to_float_nonneg(argv[++argn], "-a"); } else if (!strcmp(argv[argn], "-d")) { if (argc < argn + 2) syntax(argv[0]); - opt_d = to_float(argv[++argn]); + opt_d = to_float_nonneg(argv[++argn], "-d"); } else if (!strcmp(argv[argn], "-D")) { @@ -1105,7 +1145,7 @@ main(int argc, char** argv) { if (argc < argn + 2) syntax(argv[0]); - opt_ec = to_int(argv[++argn]); + opt_ec = to_int_nonneg(argv[++argn], "-e"); } else if (!strcmp(argv[argn], "-g")) { @@ -1140,7 +1180,7 @@ main(int argc, char** argv) { if (argc < argn + 2) syntax(argv[0]); - opt_n = to_int(argv[++argn]); + opt_n = to_int_pos(argv[++argn], "-n"); } else if (!strcmp(argv[argn], "-O")) { @@ -1171,20 +1211,20 @@ main(int argc, char** argv) { if (argc < argn + 2) syntax(argv[0]); - opt_R = to_int(argv[++argn]); + opt_R = to_int_pos(argv[++argn], "-R"); } else if (!strcmp(argv[argn], "-s")) { if (argc < argn + 2) syntax(argv[0]); - opt_ec_seed = to_int(argv[++argn]); + opt_ec_seed = to_int_nonneg(argv[++argn], "-s"); spot::srand(opt_ec_seed); } else if (!strcmp(argv[argn], "-t")) { if (argc < argn + 2) syntax(argv[0]); - opt_t = to_float(argv[++argn]); + opt_t = to_float_nonneg(argv[++argn], "-t"); } else if (!strcmp(argv[argn], "-z")) { @@ -1202,13 +1242,13 @@ main(int argc, char** argv) { if (argc < argn + 2) syntax(argv[0]); - opt_f = to_int(argv[++argn]); + opt_f = to_int_pos(argv[++argn], "-f"); } else if (!strcmp(argv[argn], "-F")) { if (argc < argn + 2) syntax(argv[0]); - opt_F = to_int(argv[++argn]); + opt_F = to_int_nonneg(argv[++argn], "-F"); } else if (!strcmp(argv[argn], "-p")) { @@ -1220,7 +1260,7 @@ main(int argc, char** argv) { if (argc < argn + 2) syntax(argv[0]); - opt_l = to_int(argv[++argn]); + opt_l = to_int_nonneg(argv[++argn], "-l"); } else if (!strcmp(argv[argn], "-u")) {