Commit f08a26f7 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

hoa: rename hoaf_reachable() to hoa_reachable()

* src/tgbaalgos/hoaf.cc, src/tgbaalgos/hoaf.hh: Rename to...
* src/tgbaalgos/hoa.cc, src/tgbaalgos/hoa.hh: ... these, and
fix the function names.
* src/tgbaalgos/Makefile.am, src/bin/autfilt.cc,
src/bin/dstar2tgba.cc, src/bin/ltl2tgba.cc, src/tgbatest/ltl2tgba.cc:
Adjust all calls.
parent 5b5c5edc
...@@ -32,7 +32,7 @@ ...@@ -32,7 +32,7 @@
#include "tgbaalgos/dotty.hh" #include "tgbaalgos/dotty.hh"
#include "tgbaalgos/lbtt.hh" #include "tgbaalgos/lbtt.hh"
#include "tgbaalgos/hoaf.hh" #include "tgbaalgos/hoa.hh"
#include "tgbaalgos/neverclaim.hh" #include "tgbaalgos/neverclaim.hh"
#include "tgbaalgos/save.hh" #include "tgbaalgos/save.hh"
#include "tgbaalgos/stats.hh" #include "tgbaalgos/stats.hh"
...@@ -127,7 +127,7 @@ const struct argp_child children[] = ...@@ -127,7 +127,7 @@ const struct argp_child children[] =
enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa } format = Dot; enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa } format = Dot;
bool utf8 = false; bool utf8 = false;
const char* stats = ""; const char* stats = "";
const char* hoaf_opt = 0; const char* hoa_opt = 0;
spot::option_map extra_options; spot::option_map extra_options;
static int static int
...@@ -147,7 +147,7 @@ parse_opt(int key, char* arg, struct argp_state*) ...@@ -147,7 +147,7 @@ parse_opt(int key, char* arg, struct argp_state*)
break; break;
case 'H': case 'H':
format = Hoa; format = Hoa;
hoaf_opt = arg; hoa_opt = arg;
break; break;
case 'M': case 'M':
type = spot::postprocessor::Monitor; type = spot::postprocessor::Monitor;
...@@ -315,7 +315,7 @@ namespace ...@@ -315,7 +315,7 @@ namespace
spot::lbtt_reachable(std::cout, aut, false); spot::lbtt_reachable(std::cout, aut, false);
break; break;
case Hoa: case Hoa:
spot::hoaf_reachable(std::cout, aut, hoaf_opt) << '\n'; spot::hoa_reachable(std::cout, aut, hoa_opt) << '\n';
break; break;
case Spot: case Spot:
spot::tgba_save_reachable(std::cout, aut); spot::tgba_save_reachable(std::cout, aut);
......
...@@ -32,7 +32,7 @@ ...@@ -32,7 +32,7 @@
#include "tgbaalgos/dotty.hh" #include "tgbaalgos/dotty.hh"
#include "tgbaalgos/lbtt.hh" #include "tgbaalgos/lbtt.hh"
#include "tgbaalgos/hoaf.hh" #include "tgbaalgos/hoa.hh"
#include "tgbaalgos/neverclaim.hh" #include "tgbaalgos/neverclaim.hh"
#include "tgbaalgos/save.hh" #include "tgbaalgos/save.hh"
#include "tgbaalgos/stats.hh" #include "tgbaalgos/stats.hh"
...@@ -128,7 +128,7 @@ const struct argp_child children[] = ...@@ -128,7 +128,7 @@ const struct argp_child children[] =
enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa } format = Dot; enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa } format = Dot;
bool utf8 = false; bool utf8 = false;
const char* stats = ""; const char* stats = "";
const char* hoaf_opt = 0; const char* hoa_opt = 0;
spot::option_map extra_options; spot::option_map extra_options;
static int static int
...@@ -148,7 +148,7 @@ parse_opt(int key, char* arg, struct argp_state*) ...@@ -148,7 +148,7 @@ parse_opt(int key, char* arg, struct argp_state*)
break; break;
case 'H': case 'H':
format = Hoa; format = Hoa;
hoaf_opt = arg; hoa_opt = arg;
break; break;
case 'M': case 'M':
type = spot::postprocessor::Monitor; type = spot::postprocessor::Monitor;
...@@ -324,7 +324,7 @@ namespace ...@@ -324,7 +324,7 @@ namespace
spot::lbtt_reachable(std::cout, aut, false); spot::lbtt_reachable(std::cout, aut, false);
break; break;
case Hoa: case Hoa:
spot::hoaf_reachable(std::cout, aut, hoaf_opt) << '\n'; spot::hoa_reachable(std::cout, aut, hoa_opt) << '\n';
break; break;
case Spot: case Spot:
spot::tgba_save_reachable(std::cout, aut); spot::tgba_save_reachable(std::cout, aut);
......
...@@ -38,7 +38,7 @@ ...@@ -38,7 +38,7 @@
#include "tgbaalgos/lbtt.hh" #include "tgbaalgos/lbtt.hh"
#include "tgbaalgos/neverclaim.hh" #include "tgbaalgos/neverclaim.hh"
#include "tgbaalgos/save.hh" #include "tgbaalgos/save.hh"
#include "tgbaalgos/hoaf.hh" #include "tgbaalgos/hoa.hh"
#include "tgbaalgos/stats.hh" #include "tgbaalgos/stats.hh"
#include "tgbaalgos/translate.hh" #include "tgbaalgos/translate.hh"
#include "tgba/bddprint.hh" #include "tgba/bddprint.hh"
...@@ -73,7 +73,7 @@ static const argp_option options[] = ...@@ -73,7 +73,7 @@ static const argp_option options[] =
{ "csv-escape", OPT_CSV, 0, 0, "quote formula output by %f in --format " { "csv-escape", OPT_CSV, 0, 0, "quote formula output by %f in --format "
"for use in CSV file", 0 }, "for use in CSV file", 0 },
{ "dot", OPT_DOT, 0, 0, "GraphViz's format (default)", 0 }, { "dot", OPT_DOT, 0, 0, "GraphViz's format (default)", 0 },
{ "hoaf", 'H', "s|t|m|l", OPTION_ARG_OPTIONAL, { "hoa", 'H', "s|t|m|l", OPTION_ARG_OPTIONAL,
"Output the automaton in HOA format. Add letters to select " "Output the automaton in HOA format. Add letters to select "
"(s) state-based acceptance, (t) transition-based acceptance, " "(s) state-based acceptance, (t) transition-based acceptance, "
"(m) mixed acceptance, (l) single-line output", 0 }, "(m) mixed acceptance, (l) single-line output", 0 },
...@@ -126,7 +126,7 @@ const struct argp_child children[] = ...@@ -126,7 +126,7 @@ const struct argp_child children[] =
enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa } format = Dot; enum output_format { Dot, Lbtt, Lbtt_t, Spin, Spot, Stats, Hoa } format = Dot;
bool utf8 = false; bool utf8 = false;
const char* stats = ""; const char* stats = "";
const char* hoaf_opt = 0; const char* hoa_opt = 0;
spot::option_map extra_options; spot::option_map extra_options;
static int static int
...@@ -144,7 +144,7 @@ parse_opt(int key, char* arg, struct argp_state*) ...@@ -144,7 +144,7 @@ parse_opt(int key, char* arg, struct argp_state*)
break; break;
case 'H': case 'H':
format = Hoa; format = Hoa;
hoaf_opt = arg; hoa_opt = arg;
break; break;
case 'M': case 'M':
type = spot::postprocessor::Monitor; type = spot::postprocessor::Monitor;
...@@ -254,7 +254,7 @@ namespace ...@@ -254,7 +254,7 @@ namespace
spot::lbtt_reachable(std::cout, aut, false); spot::lbtt_reachable(std::cout, aut, false);
break; break;
case Hoa: case Hoa:
spot::hoaf_reachable(std::cout, aut, hoaf_opt, f) << '\n'; spot::hoa_reachable(std::cout, aut, hoa_opt, f) << '\n';
break; break;
case Spot: case Spot:
spot::tgba_save_reachable(std::cout, aut); spot::tgba_save_reachable(std::cout, aut);
......
...@@ -43,7 +43,7 @@ tgbaalgos_HEADERS = \ ...@@ -43,7 +43,7 @@ tgbaalgos_HEADERS = \
emptiness.hh \ emptiness.hh \
emptiness_stats.hh \ emptiness_stats.hh \
gv04.hh \ gv04.hh \
hoaf.hh \ hoa.hh \
isdet.hh \ isdet.hh \
isweakscc.hh \ isweakscc.hh \
lbtt.hh \ lbtt.hh \
...@@ -93,7 +93,7 @@ libtgbaalgos_la_SOURCES = \ ...@@ -93,7 +93,7 @@ libtgbaalgos_la_SOURCES = \
dupexp.cc \ dupexp.cc \
emptiness.cc \ emptiness.cc \
gv04.cc \ gv04.cc \
hoaf.cc \ hoa.cc \
isdet.cc \ isdet.cc \
isweakscc.cc \ isweakscc.cc \
lbtt.cc \ lbtt.cc \
......
...@@ -24,7 +24,7 @@ ...@@ -24,7 +24,7 @@
#include <sstream> #include <sstream>
#include <map> #include <map>
#include "tgba/tgba.hh" #include "tgba/tgba.hh"
#include "hoaf.hh" #include "hoa.hh"
#include "reachiter.hh" #include "reachiter.hh"
#include "misc/escape.hh" #include "misc/escape.hh"
#include "misc/bddlt.hh" #include "misc/bddlt.hh"
...@@ -226,20 +226,20 @@ namespace spot ...@@ -226,20 +226,20 @@ namespace spot
std::ostream& std::ostream&
hoaf_reachable(std::ostream& os, hoa_reachable(std::ostream& os,
const const_tgba_ptr& aut, const const_tgba_ptr& aut,
const ltl::formula* f, const ltl::formula* f,
hoaf_acceptance acceptance, hoa_acceptance acceptance,
hoaf_alias alias, hoa_alias alias,
bool newline) bool newline)
{ {
(void) alias; (void) alias;
metadata md(aut); metadata md(aut);
if (acceptance == Hoaf_Acceptance_States if (acceptance == Hoa_Acceptance_States
&& !md.state_acc) && !md.state_acc)
acceptance = Hoaf_Acceptance_Transitions; acceptance = Hoa_Acceptance_Transitions;
unsigned num_states = md.nm.size(); unsigned num_states = md.nm.size();
...@@ -281,9 +281,9 @@ namespace spot ...@@ -281,9 +281,9 @@ namespace spot
} }
os << nl; os << nl;
os << "properties: trans-labels explicit-labels"; os << "properties: trans-labels explicit-labels";
if (acceptance == Hoaf_Acceptance_States) if (acceptance == Hoa_Acceptance_States)
os << " state-acc"; os << " state-acc";
else if (acceptance == Hoaf_Acceptance_Transitions) else if (acceptance == Hoa_Acceptance_Transitions)
os << " trans-acc"; os << " trans-acc";
if (md.is_complete) if (md.is_complete)
os << " complete"; os << " complete";
...@@ -293,16 +293,16 @@ namespace spot ...@@ -293,16 +293,16 @@ namespace spot
os << "--BODY--" << nl; os << "--BODY--" << nl;
for (unsigned i = 0; i < num_states; ++i) for (unsigned i = 0; i < num_states; ++i)
{ {
hoaf_acceptance this_acc = acceptance; hoa_acceptance this_acc = acceptance;
if (this_acc == Hoaf_Acceptance_Mixed) if (this_acc == Hoa_Acceptance_Mixed)
this_acc = (md.common_acc[i] ? this_acc = (md.common_acc[i] ?
Hoaf_Acceptance_States : Hoaf_Acceptance_Transitions); Hoa_Acceptance_States : Hoa_Acceptance_Transitions);
tgba_succ_iterator* j = aut->succ_iter(md.nm[i]); tgba_succ_iterator* j = aut->succ_iter(md.nm[i]);
j->first(); j->first();
os << "State: " << i; os << "State: " << i;
if (this_acc == Hoaf_Acceptance_States && !j->done()) if (this_acc == Hoa_Acceptance_States && !j->done())
md.emit_acc(os, aut, j->current_acceptance_conditions()); md.emit_acc(os, aut, j->current_acceptance_conditions());
os << nl; os << nl;
...@@ -310,7 +310,7 @@ namespace spot ...@@ -310,7 +310,7 @@ namespace spot
{ {
const state* dst = j->current_state(); const state* dst = j->current_state();
os << '[' << md.sup[j->current_condition()] << "] " << md.sm[dst]; os << '[' << md.sup[j->current_condition()] << "] " << md.sm[dst];
if (this_acc == Hoaf_Acceptance_Transitions) if (this_acc == Hoa_Acceptance_Transitions)
md.emit_acc(os, aut, j->current_acceptance_conditions()); md.emit_acc(os, aut, j->current_acceptance_conditions());
os << nl; os << nl;
dst->destroy(); dst->destroy();
...@@ -324,14 +324,14 @@ namespace spot ...@@ -324,14 +324,14 @@ namespace spot
} }
std::ostream& std::ostream&
hoaf_reachable(std::ostream& os, hoa_reachable(std::ostream& os,
const const_tgba_ptr& aut, const const_tgba_ptr& aut,
const char* opt, const char* opt,
const ltl::formula* f) const ltl::formula* f)
{ {
bool newline = true; bool newline = true;
hoaf_acceptance acceptance = Hoaf_Acceptance_States; hoa_acceptance acceptance = Hoa_Acceptance_States;
hoaf_alias alias = Hoaf_Alias_None; hoa_alias alias = Hoa_Alias_None;
if (opt) if (opt)
while (*opt) while (*opt)
...@@ -342,17 +342,17 @@ namespace spot ...@@ -342,17 +342,17 @@ namespace spot
newline = false; newline = false;
break; break;
case 'm': case 'm':
acceptance = Hoaf_Acceptance_Mixed; acceptance = Hoa_Acceptance_Mixed;
break; break;
case 's': case 's':
acceptance = Hoaf_Acceptance_States; acceptance = Hoa_Acceptance_States;
break; break;
case 't': case 't':
acceptance = Hoaf_Acceptance_Transitions; acceptance = Hoa_Acceptance_Transitions;
break; break;
} }
} }
return hoaf_reachable(os, aut, f, acceptance, alias, newline); return hoa_reachable(os, aut, f, acceptance, alias, newline);
} }
} }
...@@ -17,8 +17,8 @@ ...@@ -17,8 +17,8 @@
// You should have received a copy of the GNU General Public License // You should have received a copy of the GNU General Public License
// along with this program. If not, see <http://www.gnu.org/licenses/>. // along with this program. If not, see <http://www.gnu.org/licenses/>.
#ifndef SPOT_TGBAALGOS_HOAF_HH #ifndef SPOT_TGBAALGOS_HOA_HH
# define SPOT_TGBAALGOS_HOAF_HH # define SPOT_TGBAALGOS_HOA_HH
#include <iosfwd> #include <iosfwd>
#include "ltlast/formula.hh" #include "ltlast/formula.hh"
...@@ -26,15 +26,15 @@ ...@@ -26,15 +26,15 @@
namespace spot namespace spot
{ {
enum hoaf_alias { Hoaf_Alias_None, Hoaf_Alias_Ap, Hoaf_Alias_Cond }; enum hoa_alias { Hoa_Alias_None, Hoa_Alias_Ap, Hoa_Alias_Cond };
enum hoaf_acceptance enum hoa_acceptance
{ {
Hoaf_Acceptance_States, /// state-based acceptance if Hoa_Acceptance_States, /// state-based acceptance if
/// (globally) possible /// (globally) possible
/// transition-based acceptance /// transition-based acceptance
/// otherwise. /// otherwise.
Hoaf_Acceptance_Transitions, /// transition-based acceptance globally Hoa_Acceptance_Transitions, /// transition-based acceptance globally
Hoaf_Acceptance_Mixed /// mix state-based and transition-based Hoa_Acceptance_Mixed /// mix state-based and transition-based
}; };
/// \ingroup tgba_io /// \ingroup tgba_io
...@@ -49,18 +49,18 @@ namespace spot ...@@ -49,18 +49,18 @@ namespace spot
/// \param alias Whether aliases should be used in output. /// \param alias Whether aliases should be used in output.
/// \param newlines Whether to use newlines in output. /// \param newlines Whether to use newlines in output.
SPOT_API std::ostream& SPOT_API std::ostream&
hoaf_reachable(std::ostream& os, hoa_reachable(std::ostream& os,
const const_tgba_ptr& g, const const_tgba_ptr& g,
const ltl::formula* f = 0, const ltl::formula* f = 0,
hoaf_acceptance acceptance = Hoaf_Acceptance_States, hoa_acceptance acceptance = Hoa_Acceptance_States,
hoaf_alias alias = Hoaf_Alias_None, hoa_alias alias = Hoa_Alias_None,
bool newlines = true); bool newlines = true);
SPOT_API std::ostream& SPOT_API std::ostream&
hoaf_reachable(std::ostream& os, hoa_reachable(std::ostream& os,
const const_tgba_ptr& g, const const_tgba_ptr& g,
const char* opt, const char* opt,
const ltl::formula* f = 0); const ltl::formula* f = 0);
} }
#endif // SPOT_TGBAALGOS_HOAF_HH #endif // SPOT_TGBAALGOS_HOA_HH
...@@ -36,7 +36,7 @@ ...@@ -36,7 +36,7 @@
#include "tgbaalgos/save.hh" #include "tgbaalgos/save.hh"
#include "tgbaalgos/dotty.hh" #include "tgbaalgos/dotty.hh"
#include "tgbaalgos/lbtt.hh" #include "tgbaalgos/lbtt.hh"
#include "tgbaalgos/hoaf.hh" #include "tgbaalgos/hoa.hh"
#include "tgbaalgos/degen.hh" #include "tgbaalgos/degen.hh"
#include "tgba/tgbaproduct.hh" #include "tgba/tgbaproduct.hh"
#include "tgbaalgos/reducerun.hh" #include "tgbaalgos/reducerun.hh"
...@@ -385,7 +385,7 @@ checked_main(int argc, char** argv) ...@@ -385,7 +385,7 @@ checked_main(int argc, char** argv)
bool opt_closure = false; bool opt_closure = false;
bool opt_stutterize = false; bool opt_stutterize = false;
bool spin_comments = false; bool spin_comments = false;
const char* hoaf_opt = 0; const char* hoa_opt = 0;
spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::ltl::atomic_prop_set* unobservables = 0; spot::ltl::atomic_prop_set* unobservables = 0;
spot::tgba_ptr system_aut = 0; spot::tgba_ptr system_aut = 0;
...@@ -554,7 +554,7 @@ checked_main(int argc, char** argv) ...@@ -554,7 +554,7 @@ checked_main(int argc, char** argv)
else if (!strncmp(argv[formula_index], "-H", 2)) else if (!strncmp(argv[formula_index], "-H", 2))
{ {
output = 17; output = 17;
hoaf_opt = argv[formula_index] + 2; hoa_opt = argv[formula_index] + 2;
} }
else if (!strcmp(argv[formula_index], "-k")) else if (!strcmp(argv[formula_index], "-k"))
{ {
...@@ -1718,7 +1718,7 @@ checked_main(int argc, char** argv) ...@@ -1718,7 +1718,7 @@ checked_main(int argc, char** argv)
} }
case 17: case 17:
{ {
hoaf_reachable(std::cout, a, hoaf_opt, f) << '\n'; hoa_reachable(std::cout, a, hoa_opt, f) << '\n';
break; break;
} }
default: default:
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment