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

lbtt: take options as a string like other print functions

* src/twaalgos/lbtt.hh (print_lbtt): Take a const char* opt argument.
* src/twaalgos/lbtt.cc: Use it, select state-based
vs. transition-based using automaton property, and implement output
for generalized state-based acceptance.
* src/bin/common_aoutput.cc, src/bin/common_aoutput.hh,
src/bin/dstar2tgba.cc: Adjust usage.  We do not need to handle
--lbtt=t as a special case anymore.
* src/tests/lbttparse.test, wrap/python/spot.py,
wrap/python/tests/automata-io.ipynb, wrap/python/tests/piperead.ipynb:
Adjust.
parent cf6c17b5
...@@ -38,6 +38,7 @@ automaton_format_t automaton_format = Dot; ...@@ -38,6 +38,7 @@ automaton_format_t automaton_format = Dot;
static const char* opt_dot = nullptr; static const char* opt_dot = nullptr;
static const char* opt_never = nullptr; static const char* opt_never = nullptr;
static const char* hoa_opt = nullptr; static const char* hoa_opt = nullptr;
static const char* opt_lbtt = nullptr;
const char* opt_name = nullptr; const char* opt_name = nullptr;
static const char* opt_output = nullptr; static const char* opt_output = nullptr;
static const char* stats = ""; static const char* stats = "";
...@@ -234,17 +235,13 @@ int parse_opt_aoutput(int key, char* arg, struct argp_state*) ...@@ -234,17 +235,13 @@ int parse_opt_aoutput(int key, char* arg, struct argp_state*)
opt_dot = arg; opt_dot = arg;
break; break;
case OPT_LBTT: case OPT_LBTT:
if (arg) automaton_format = Lbtt;
{ opt_lbtt = arg;
if (arg[0] == 't' && arg[1] == 0) // This test could be removed when more options are added,
automaton_format = Lbtt_t; // because print_lbtt will raise an exception anyway. The
else // error message is slightly better in the current way.
error(2, 0, "unknown argument for --lbtt: '%s'", arg); if (arg && (arg[0] != 't' || arg[1] != 0))
} error(2, 0, "unknown argument for --lbtt: '%s'", arg);
else
{
automaton_format = Lbtt;
}
break; break;
case OPT_NAME: case OPT_NAME:
opt_name = arg; opt_name = arg;
...@@ -322,10 +319,7 @@ automaton_printer::print(const spot::twa_graph_ptr& aut, ...@@ -322,10 +319,7 @@ automaton_printer::print(const spot::twa_graph_ptr& aut,
spot::print_dot(*out, aut, opt_dot); spot::print_dot(*out, aut, opt_dot);
break; break;
case Lbtt: case Lbtt:
spot::print_lbtt(*out, aut, type == spot::postprocessor::BA); spot::print_lbtt(*out, aut, opt_lbtt);
break;
case Lbtt_t:
spot::print_lbtt(*out, aut, false);
break; break;
case Hoa: case Hoa:
spot::print_hoa(*out, aut, hoa_opt) << '\n'; spot::print_hoa(*out, aut, hoa_opt) << '\n';
......
...@@ -39,7 +39,6 @@ ...@@ -39,7 +39,6 @@
enum automaton_format_t { enum automaton_format_t {
Dot, Dot,
Lbtt, Lbtt,
Lbtt_t,
Spin, Spin,
Stats, Stats,
Hoa, Hoa,
......
...@@ -150,12 +150,13 @@ static const struct argp_child children[] = ...@@ -150,12 +150,13 @@ static const struct argp_child children[] =
{ 0, 0, 0, 0 } { 0, 0, 0, 0 }
}; };
enum output_format { Dot, Lbtt, Lbtt_t, Spin, Stats, Hoa }; enum output_format { Dot, Lbtt, Spin, Stats, Hoa };
static output_format format = Dot; static output_format format = Dot;
static const char* opt_dot = nullptr; static const char* opt_dot = nullptr;
static const char* stats = ""; static const char* stats = "";
static const char* hoa_opt = nullptr; static const char* hoa_opt = nullptr;
static const char* opt_never = nullptr; static const char* opt_never = nullptr;
static const char* opt_lbtt = nullptr;
static const char* opt_name = nullptr; static const char* opt_name = nullptr;
static const char* opt_output = nullptr; static const char* opt_output = nullptr;
static spot::option_map extra_options; static spot::option_map extra_options;
...@@ -204,17 +205,10 @@ parse_opt(int key, char* arg, struct argp_state*) ...@@ -204,17 +205,10 @@ parse_opt(int key, char* arg, struct argp_state*)
opt_dot = arg; opt_dot = arg;
break; break;
case OPT_LBTT: case OPT_LBTT:
if (arg) format = Lbtt;
{ opt_lbtt = arg;
if (arg[0] == 't' && arg[1] == 0) if (arg && (arg[0] != 't' || arg[1] != 0))
format = Lbtt_t; error(2, 0, "unknown argument for --lbtt: '%s'", arg);
else
error(2, 0, "unknown argument for --lbtt: '%s'", arg);
}
else
{
format = Lbtt;
}
break; break;
case OPT_NAME: case OPT_NAME:
opt_name = arg; opt_name = arg;
...@@ -391,10 +385,7 @@ namespace ...@@ -391,10 +385,7 @@ namespace
spot::print_dot(*out, aut, opt_dot); spot::print_dot(*out, aut, opt_dot);
break; break;
case Lbtt: case Lbtt:
spot::print_lbtt(*out, aut, type == spot::postprocessor::BA); spot::print_lbtt(*out, aut, opt_lbtt);
break;
case Lbtt_t:
spot::print_lbtt(*out, aut, false);
break; break;
case Hoa: case Hoa:
spot::print_hoa(*out, aut, hoa_opt) << '\n'; spot::print_hoa(*out, aut, hoa_opt) << '\n';
......
...@@ -27,7 +27,11 @@ do ...@@ -27,7 +27,11 @@ do
# Make sure Spot can read the LBTT it produces # Make sure Spot can read the LBTT it produces
run 0 ../../bin/ltl2tgba --lbtt "$f" > out run 0 ../../bin/ltl2tgba --lbtt "$f" > out
s=`wc -l < out` s=`wc -l < out`
head -n 1 out | grep t if ../../bin/ltl2tgba -H "$f" | grep 'properties:.*state-acc'; then
head -n 1 out | grep t && exit 1
else
head -n 1 out | grep t
fi
run 0 ../../bin/autfilt --lbtt out > out2 run 0 ../../bin/autfilt --lbtt out > out2
s2=`wc -l < out2` s2=`wc -l < out2`
test "$s" -eq "$s2" test "$s" -eq "$s2"
......
...@@ -51,13 +51,13 @@ namespace spot ...@@ -51,13 +51,13 @@ namespace spot
sba_ = std::dynamic_pointer_cast<const twa_graph>(a); sba_ = std::dynamic_pointer_cast<const twa_graph>(a);
} }
bool acc_cond::mark_t
state_is_accepting(const state *s) const state_acc_sets(const state *s) const
{ {
// If the automaton has a SBA type, it's easier to just query the // If the automaton has a SBA type, it's easier to just query the
// state_is_accepting() method. // state_is_accepting() method.
if (sba_) if (sba_)
return sba_->state_is_accepting(s); return sba_->state_acc_sets(sba_->state_number(s));
// Otherwise, since we are dealing with a degeneralized // Otherwise, since we are dealing with a degeneralized
// automaton nonetheless, the transitions leaving an accepting // automaton nonetheless, the transitions leaving an accepting
...@@ -66,10 +66,11 @@ namespace spot ...@@ -66,10 +66,11 @@ namespace spot
// is not terribly efficient since we have to create the // is not terribly efficient since we have to create the
// iterator. // iterator.
twa_succ_iterator* it = aut_->succ_iter(s); twa_succ_iterator* it = aut_->succ_iter(s);
bool accepting = it->first() if (!it->first())
&& aut_->acc().accepting(it->current_acceptance_conditions()); return {};
auto res = it->current_acceptance_conditions();
aut_->release_iter(it); aut_->release_iter(it);
return accepting; return res;
} }
...@@ -84,12 +85,9 @@ namespace spot ...@@ -84,12 +85,9 @@ namespace spot
// Do we have state-based acceptance? // Do we have state-based acceptance?
if (sba_format_) if (sba_format_)
{ {
// We support only one acceptance condition in the for (auto i: state_acc_sets(s).sets())
// state-based format. body_ << ' ' << i;
if (state_is_accepting(s)) body_ << " -1";
body_ << " 0 -1";
else
body_ << " -1";
} }
body_ << '\n'; body_ << '\n';
} }
...@@ -117,7 +115,7 @@ namespace spot ...@@ -117,7 +115,7 @@ namespace spot
{ {
os_ << seen.size() << ' '; os_ << seen.size() << ' ';
if (sba_format_) if (sba_format_)
os_ << '1'; os_ << aut_->acc().num_sets();
else else
os_ << aut_->acc().num_sets() << 't'; os_ << aut_->acc().num_sets() << 't';
os_ << '\n' << body_.str() << "-1" << std::endl; os_ << '\n' << body_.str() << "-1" << std::endl;
...@@ -133,12 +131,24 @@ namespace spot ...@@ -133,12 +131,24 @@ namespace spot
} }
std::ostream& std::ostream&
print_lbtt(std::ostream& os, const const_twa_ptr& g, bool sba) print_lbtt(std::ostream& os, const const_twa_ptr& g, const char* opt)
{ {
if (!g->acc().is_generalized_buchi()) if (!g->acc().is_generalized_buchi())
throw std::runtime_error throw std::runtime_error
("LBTT only supports generalized Büchi acceptance"); ("LBTT only supports generalized Büchi acceptance");
bool sba = g->has_state_based_acc();
if (opt)
switch (char c = *opt++)
{
case 't':
sba = false;
break;
default:
throw std::runtime_error
(std::string("unknown option for print_lbtt(): ") + c);
}
lbtt_bfs b(g, os, sba); lbtt_bfs b(g, os, sba);
b.run(); b.run();
return os; return os;
......
...@@ -32,8 +32,9 @@ namespace spot ...@@ -32,8 +32,9 @@ namespace spot
/// ///
/// \param g The automata to print. /// \param g The automata to print.
/// \param os Where to print. /// \param os Where to print.
/// \param sba Assume \a g is an SBA and use LBTT's state-based /// \param opt if "t", force transition-based acceptance, otherwise,
/// acceptance format (similar to LBT's format). // default to state-based acceptance when the automaton is marked so.
SPOT_API std::ostream& SPOT_API std::ostream&
print_lbtt(std::ostream& os, const const_twa_ptr& g, bool sba = false); print_lbtt(std::ostream& os, const const_twa_ptr& g,
const char* opt = nullptr);
} }
...@@ -136,7 +136,7 @@ def _twa_to_str(a, format='hoa', opt=None): ...@@ -136,7 +136,7 @@ def _twa_to_str(a, format='hoa', opt=None):
return ostr.str() return ostr.str()
if format == 'lbtt': if format == 'lbtt':
ostr = ostringstream() ostr = ostringstream()
print_lbtt(ostr, a, bool(opt)) print_lbtt(ostr, a, opt)
return ostr.str() return ostr.str()
raise ValueError("unknown string format: " + format) raise ValueError("unknown string format: " + format)
......
This diff is collapsed.
This diff is collapsed.
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