bin: use enums instead of #define for option codes

* src/bin/autfilt.cc, src/bin/common_aoutput.cc,
src/bin/common_finput.cc, src/bin/common_output.cc,
src/bin/common_post.cc, src/bin/common_setup.cc,
src/bin/common_trans.cc, src/bin/dstar2tgba.cc, src/bin/genltl.cc,
src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc, src/bin/ltlcross.cc,
src/bin/ltlfilt.cc, src/bin/ltlgrind.cc, src/bin/randaut.cc,
src/bin/randltl.cc: Here.

src/bin/autfilt.cc

@@ -60,31 +60,33 @@ Exit status:\n\
   1  if no automata were output (no match)\n\
   2  if any error has been reported";
 
-
+// Keep this list sorted
-#define OPT_TGBA 1
+enum {
-#define OPT_RANDOMIZE 2
+  OPT_ACC_SETS = 256,
-#define OPT_SEED 3
+  OPT_ARE_ISOMORPHIC,
-#define OPT_PRODUCT 4
+  OPT_CLEAN_ACC,
-#define OPT_MERGE 5
+  OPT_COMPLEMENT_ACC,
-#define OPT_ARE_ISOMORPHIC 6
+  OPT_COUNT,
-#define OPT_IS_COMPLETE 7
+  OPT_DESTUT,
-#define OPT_IS_DETERMINISTIC 8
+  OPT_DNF_ACC,
-#define OPT_STATES 9
+  OPT_EDGES,
-#define OPT_COUNT 10
+  OPT_INSTUT,
-#define OPT_EDGES 11
+  OPT_INTERSECT,
-#define OPT_ACC_SETS 12
+  OPT_IS_COMPLETE,
-#define OPT_DESTUT 13
+  OPT_IS_DETERMINISTIC,
-#define OPT_INSTUT 14
+  OPT_IS_EMPTY,
-#define OPT_IS_EMPTY 15
+  OPT_KEEP_STATES,
-#define OPT_INTERSECT 16
+  OPT_MASK_ACC,
-#define OPT_MASK_ACC 17
+  OPT_MERGE,
-#define OPT_SBACC 18
+  OPT_PRODUCT,
-#define OPT_STRIPACC 19
+  OPT_RANDOMIZE,
-#define OPT_KEEP_STATES 20
+  OPT_REM_FIN,
-#define OPT_DNF_ACC 21
+  OPT_SBACC,
-#define OPT_REM_FIN 22
+  OPT_SEED,
-#define OPT_CLEAN_ACC 23
+  OPT_STATES,
-#define OPT_COMPLEMENT_ACC 24
+  OPT_STRIPACC,
+  OPT_TGBA,
+};
 
 static const argp_option options[] =
   {

src/bin/common_aoutput.cc

@@ -40,10 +40,12 @@ const char* opt_name = nullptr;
 static const char* opt_output = nullptr;
 static const char* stats = "";
 
-#define OPT_DOT 1
+enum {
-#define OPT_LBTT 2
+  OPT_DOT = 1,
-#define OPT_STATS 3
+  OPT_LBTT,
-#define OPT_NAME 4
+  OPT_NAME,
+  OPT_STATS,
+};
 
 static const argp_option options[] =
   {

src/bin/common_finput.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
+// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -24,8 +24,10 @@
 #include <fstream>
 #include <cstring>
 
-#define OPT_LBT 1
+enum {
-#define OPT_LENIENT 2
+  OPT_LBT = 1,
+  OPT_LENIENT,
+};
 
 jobs_t jobs;
 bool lbt_input = false;

src/bin/common_output.cc

@@ -28,11 +28,13 @@
 #include "common_cout.hh"
 #include "error.h"
 
-#define OPT_SPOT 1
+enum {
-#define OPT_WRING 2
+  OPT_CSV = 1,
-#define OPT_LATEX 3
+  OPT_FORMAT,
-#define OPT_FORMAT 4
+  OPT_LATEX,
-#define OPT_CSV 5
+  OPT_SPOT,
+  OPT_WRING,
+};
 
 output_format_t output_format = spot_output;
 bool full_parenth = false;

src/bin/common_post.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
+// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -26,10 +26,12 @@ spot::postprocessor::output_pref pref = spot::postprocessor::Small;
 spot::postprocessor::output_pref comp = spot::postprocessor::Any;
 spot::postprocessor::optimization_level level = spot::postprocessor::High;
 
-#define OPT_SMALL 1
+enum {
-#define OPT_LOW 2
+  OPT_HIGH = 1,
-#define OPT_MEDIUM 3
+  OPT_LOW,
-#define OPT_HIGH 4
+  OPT_MEDIUM,
+  OPT_SMALL,
+};
 
 static const argp_option options[] =
   {

src/bin/common_setup.cc

@@ -57,9 +57,12 @@ setup(char** argv)
 // I mean, come on, why not also add -* to Darwinise more shell users?
 // We disable this option as well as -V (because --version don't need
 // a short version).
-#define OPT_VERSION 1
+enum {
-#define OPT_HELP 2
+  OPT_HELP = 1,
-#define OPT_USAGE 3
+  OPT_USAGE,
+  OPT_VERSION,
+};
+
 static const argp_option options[] =
   {
     { "version", OPT_VERSION, 0, 0, "print program version", -1 },

src/bin/common_trans.cc

@@ -383,7 +383,9 @@ exec_with_timeout(const char* cmd)
 }
 #endif // ENABLE_TIMEOUT
 
-#define OPT_LIST 1
+enum {
+  OPT_LIST = 1,
+};
 static const argp_option options[] =
 {
     /**************************************************/

src/bin/dstar2tgba.cc

@@ -50,11 +50,13 @@ Transition-based Generalized Büchi Automata in GraphViz's format by default.\n\
 If multiple files are supplied (one automaton per file), several automata\n\
 will be output.";
 
-#define OPT_TGBA 1
+enum {
-#define OPT_DOT 2
+  OPT_DOT = 1,
-#define OPT_LBTT 3
+  OPT_LBTT,
-#define OPT_STATS 4
+  OPT_NAME,
-#define OPT_NAME 5
+  OPT_STATS,
+  OPT_TGBA,
+};
 
 static const argp_option options[] =
   {

src/bin/genltl.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
+// Copyright (C) 2012, 2013, 2015 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -96,27 +96,29 @@ using namespace spot::ltl;
 const char argp_program_doc[] ="\
 Generate temporal logic formulas from predefined scalable patterns.";
 
-#define OPT_AND_F 1
+enum {
-#define OPT_AND_FG 2
+  OPT_AND_F = 1,
-#define OPT_AND_GF 3
+  OPT_AND_FG,
-#define OPT_CCJ_ALPHA 4
+  OPT_AND_GF,
-#define OPT_CCJ_BETA 5
+  OPT_CCJ_ALPHA,
-#define OPT_CCJ_BETA_PRIME 6
+  OPT_CCJ_BETA,
-#define OPT_GH_Q 7
+  OPT_CCJ_BETA_PRIME,
-#define OPT_GH_R 8
+  OPT_GH_Q,
-#define OPT_GO_THETA 9
+  OPT_GH_R,
-#define OPT_OR_FG 10
+  OPT_GO_THETA,
-#define OPT_OR_G 11
+  OPT_OR_FG,
-#define OPT_OR_GF 12
+  OPT_OR_G,
-#define OPT_R_LEFT 13
+  OPT_OR_GF,
-#define OPT_R_RIGHT 14
+  OPT_R_LEFT,
-#define OPT_RV_COUNTER 15
+  OPT_R_RIGHT,
-#define OPT_RV_COUNTER_CARRY 16
+  OPT_RV_COUNTER,
-#define OPT_RV_COUNTER_CARRY_LINEAR 17
+  OPT_RV_COUNTER_CARRY,
-#define OPT_RV_COUNTER_LINEAR 18
+  OPT_RV_COUNTER_CARRY_LINEAR,
-#define OPT_U_LEFT 19
+  OPT_RV_COUNTER_LINEAR,
-#define OPT_U_RIGHT 20
+  OPT_U_LEFT,
-#define LAST_CLASS 20
+  OPT_U_RIGHT,
+  LAST_CLASS,
+};
 
 const char* const class_name[LAST_CLASS] =
   {

src/bin/ltl2tgba.cc

@@ -46,7 +46,10 @@ the smallest Transition-based Generalized Büchi Automata, \
 in GraphViz's format.\n\
 If multiple formulas are supplied, several automata will be output.";
 
-#define OPT_TGBA 1
+
+enum {
+  OPT_TGBA = 1,
+};
 
 static const argp_option options[] =
   {

src/bin/ltl2tgta.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
+// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 //
 // This file is part of Spot, a model checking library.
@@ -52,12 +52,14 @@ the smallest Transition-based Generalized Büchi Automata, \
 in GraphViz's format.  The input formula is assumed to be \
 stuttering-insensitive.";
 
-#define OPT_TGTA 1
+enum {
-#define OPT_TA 2
+  OPT_GTA = 1,
-#define OPT_GTA 3
+  OPT_INIT,
-#define OPT_SPLV 4
+  OPT_SPLV,
-#define OPT_SPNO 5
+  OPT_SPNO,
-#define OPT_INIT 6
+  OPT_TA,
+  OPT_TGTA,
+};
 
 static const argp_option options[] =
   {

src/bin/ltlcross.cc

@@ -76,23 +76,24 @@ Exit status:\n\
   2  ltlcross aborted on error\n\
 ";
 
-
+enum {
-#define OPT_STATES 1
+  OPT_BOGUS = 256,
-#define OPT_DENSITY 2
+  OPT_COLOR,
-#define OPT_JSON 3
+  OPT_CSV,
-#define OPT_CSV 4
+  OPT_DENSITY,
-#define OPT_DUPS 5
+  OPT_DUPS,
-#define OPT_NOCHECKS 6
+  OPT_GRIND,
-#define OPT_STOP_ERR 7
+  OPT_IGNORE_EXEC_FAIL,
-#define OPT_SEED 8
+  OPT_JSON,
-#define OPT_PRODUCTS 9
+  OPT_NOCHECKS,
-#define OPT_COLOR 10
+  OPT_NOCOMP,
-#define OPT_NOCOMP 11
+  OPT_OMIT,
-#define OPT_OMIT 12
+  OPT_PRODUCTS,
-#define OPT_BOGUS 13
+  OPT_SEED,
-#define OPT_VERBOSE 14
+  OPT_STATES,
-#define OPT_GRIND 15
+  OPT_STOP_ERR,
-#define OPT_IGNORE_EXEC_FAIL 16
+  OPT_VERBOSE,
+};
 
 static const argp_option options[] =
   {

src/bin/ltlfilt.cc

@@ -55,38 +55,40 @@ Exit status:\n\
   1  if no formulas were output (no match)\n\
   2  if any error has been reported";
 
-#define OPT_SKIP_ERRORS 1
+enum {
-#define OPT_DROP_ERRORS 2
+  OPT_AP_N = 1,
-#define OPT_NNF 3
+  OPT_BOOLEAN,
-#define OPT_LTL 4
+  OPT_BOOLEAN_TO_ISOP,
-#define OPT_SYNTACTIC_SI 5
+  OPT_BSIZE_MAX,
-#define OPT_BOOLEAN 6
+  OPT_BSIZE_MIN,
-#define OPT_EVENTUAL 7
+  OPT_DROP_ERRORS,
-#define OPT_UNIVERSAL 8
+  OPT_EQUIVALENT_TO,
-#define OPT_SYNTACTIC_SAFETY 9
+  OPT_EVENTUAL,
-#define OPT_SYNTACTIC_GUARANTEE 10
+  OPT_GUARANTEE,
-#define OPT_SYNTACTIC_OBLIGATION 11
+  OPT_IGNORE_ERRORS,
-#define OPT_SYNTACTIC_RECURRENCE 12
+  OPT_IMPLIED_BY,
-#define OPT_SYNTACTIC_PERSISTENCE 13
+  OPT_IMPLY,
-#define OPT_SAFETY 14
+  OPT_LTL,
-#define OPT_GUARANTEE 15
+  OPT_NEGATE,
-#define OPT_OBLIGATION 16
+  OPT_NNF,
-#define OPT_SIZE_MIN 17
+  OPT_OBLIGATION,
-#define OPT_SIZE_MAX 18
+  OPT_RELABEL,
-#define OPT_BSIZE_MIN 19
+  OPT_RELABEL_BOOL,
-#define OPT_BSIZE_MAX 20
+  OPT_REMOVE_WM,
-#define OPT_IMPLIED_BY 21
+  OPT_REMOVE_X,
-#define OPT_IMPLY 22
+  OPT_SAFETY,
-#define OPT_EQUIVALENT_TO 23
+  OPT_SIZE_MAX,
-#define OPT_RELABEL 24
+  OPT_SIZE_MIN,
-#define OPT_RELABEL_BOOL 25
+  OPT_SKIP_ERRORS,
-#define OPT_REMOVE_WM 26
+  OPT_STUTTER_INSENSITIVE,
-#define OPT_BOOLEAN_TO_ISOP 27
+  OPT_SYNTACTIC_GUARANTEE,
-#define OPT_REMOVE_X 28
+  OPT_SYNTACTIC_OBLIGATION,
-#define OPT_STUTTER_INSENSITIVE 29
+  OPT_SYNTACTIC_PERSISTENCE,
-#define OPT_AP_N 30
+  OPT_SYNTACTIC_RECURRENCE,
-#define OPT_IGNORE_ERRORS 31
+  OPT_SYNTACTIC_SAFETY,
-#define OPT_NEGATE 256
+  OPT_SYNTACTIC_SI,
+  OPT_UNIVERSAL,
+};
 
 static const argp_option options[] =
   {

src/bin/ltlgrind.cc

@@ -33,14 +33,16 @@
 #include "ltlvisit/length.hh"
 #include "ltlvisit/mutation.hh"
 
-#define OPT_AP2CONST 1
+enum {
-#define OPT_SIMPLIFY_BOUNDS 2
+  OPT_AP2CONST = 1,
-#define OPT_REMOVE_MULTOP_OPERANDS 3
+  OPT_SIMPLIFY_BOUNDS,
-#define OPT_REMOVE_OPS 4
+  OPT_REMOVE_MULTOP_OPERANDS,
-#define OPT_SPLIT_OPS 5
+  OPT_REMOVE_OPS,
-#define OPT_REWRITE_OPS 6
+  OPT_SPLIT_OPS,
-#define OPT_REMOVE_ONE_AP 7
+  OPT_REWRITE_OPS,
-#define OPT_SORT 8
+  OPT_REMOVE_ONE_AP,
+  OPT_SORT,
+};
 
 static unsigned mutation_nb = 1;
 static unsigned max_output = -1U;

src/bin/randaut.cc

@@ -61,8 +61,10 @@ states, 1 to 3 acceptance sets, and three atomic propositions:\n\
   % randaut -n 3 --hoa -S5..10 -A1..3 3\n\
 ";
 
-#define OPT_SEED 1
+enum {
-#define OPT_STATE_ACC 2
+  OPT_SEED = 1,
+  OPT_STATE_ACC,
+};
 
 static const argp_option options[] =
   {

src/bin/randltl.cc

@@ -63,15 +63,17 @@ of X to occur by 10.\n\
   % randltl --ltl-priorities='xor=0, implies=0, equiv=0, X=10' -n10 a b c\n\
 ";
 
-#define OPT_DUMP_PRIORITIES 1
+enum {
-#define OPT_LTL_PRIORITIES 2
+  OPT_BOOLEAN_PRIORITIES = 1,
-#define OPT_SERE_PRIORITIES 3
+  OPT_DUMP_PRIORITIES,
-#define OPT_PSL_PRIORITIES 4
+  OPT_DUPS,
-#define OPT_BOOLEAN_PRIORITIES 5
+  OPT_LTL_PRIORITIES,
-#define OPT_SEED 6
+  OPT_PSL_PRIORITIES,
-#define OPT_TREE_SIZE 7
+  OPT_SEED,
-#define OPT_WF 8
+  OPT_SERE_PRIORITIES,
-#define OPT_DUPS 9
+  OPT_TREE_SIZE,
+  OPT_WF,
+};
 
 static const argp_option options[] =
   {