Commit 66aa6d08 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

ltlsynt: make sure the previous Xor optimization actually works

* spot/tl/simplify.hh, spot/tl/simplify.cc,
spot/twaalgos/translate.cc: Update the tl_simplification
options after all preferences have been given.
* bin/ltlsynt.cc: Display the size of the translation output.
* tests/core/ltlsynt.test: Add test case.
parent 6bfa9793
Pipeline #18930 passed with stages
in 138 minutes and 4 seconds
......@@ -384,8 +384,12 @@ namespace
if (want_time)
trans_time = sw.stop();
if (verbose)
std::cerr << "translating formula done in "
<< trans_time << " seconds\n";
{
std::cerr << "translating formula done in "
<< trans_time << " seconds\n";
std::cerr << "automaton has " << aut->num_states()
<< " states and " << aut->num_sets() << " colors\n";
}
spot::twa_graph_ptr dpa = nullptr;
switch (opt_solver)
......
......@@ -4100,6 +4100,12 @@ namespace spot
return simplify_recursively(f, cache_);
}
tl_simplifier_options&
tl_simplifier::options()
{
return cache_->options;
}
formula
tl_simplifier::negative_normal_form(formula f, bool negated)
{
......
......@@ -112,6 +112,14 @@ namespace spot
/// constructor).
formula simplify(formula f);
#ifndef SWIG
/// The simplifier options.
///
/// Those should can still be changed before the first formula is
/// simplified.
tl_simplifier_options& options();
#endif
/// Build the negative normal form of formula \a f.
/// All negations of the formula are pushed in front of the
/// atomic propositions. Operators <=>, =>, xor are all removed
......
......@@ -106,10 +106,6 @@ namespace spot
throw std::runtime_error
("tls-impl should take a value between 0 and 3");
}
if (comp_susp_ > 0 || (ltl_split_ && type_ == Generic))
options.favor_event_univ = true;
if (type_ == Generic && ltl_split_ && (pref_ & Deterministic))
options.keep_top_xor = true;
simpl_owned_ = simpl_ = new tl_simplifier(options, dict);
}
......@@ -419,6 +415,18 @@ namespace spot
twa_graph_ptr translator::run(formula* f)
{
if (simpl_owned_)
{
// Modify the options according to set_pref() and set_type().
// We do it for all translation, but really only the first one
// matters.
auto& opt = simpl_owned_->options();
if (comp_susp_ > 0 || (ltl_split_ && type_ == Generic))
opt.favor_event_univ = true;
if (type_ == Generic && ltl_split_ && (pref_ & Deterministic))
opt.keep_top_xor = true;
}
// Do we want to relabel Boolean subformulas?
// If we have a huge formula such as
// (a1 & a2 & ... & an) U (b1 | b2 | ... | bm)
......
......@@ -103,6 +103,7 @@ diff out exp
cat >exp <<EOF
translating formula done in X seconds
automaton has 3 states and 2 colors
split inputs and outputs done in X seconds
automaton has 9 states
determinization done
......@@ -117,6 +118,21 @@ ltlsynt --ins='a' --outs='b' -f 'GFa <-> GFb' --verbose --realizability 2> out
sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
diff outx exp
cat >exp <<EOF
translating formula done in X seconds
automaton has 16 states and 2 colors
split inputs and outputs done in X seconds
automaton has 47 states
LAR construction done in X seconds
DPA has 47 states, 4 colors
parity game built in X seconds
parity game solved in X seconds
EOF
ltlsynt --ins='a,b,c,d' --outs='e' -f '(Fa & Fb & Fc & Fd) <-> GFe' \
--verbose --realizability --algo=lar 2> out
sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
diff outx exp
for r in '' '--real'; do
opts="$r --ins=a --outs=b -f"
ltlsynt --algo=ds $opts 'GFa <-> GFb' --csv=FILE || :
......
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