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

autfilt: handle alternation with --equivalent-to and friends

* bin/autfilt.cc (ensure_deterministic): Remove alternation on demand.
(process_automaton): Prefer twa::intersects() over
product()/is_empty().
* spot/twa/twa.cc (remove_fin_maybe): Also remove alternation.
* tests/core/alternating.test: More tests.
parent 77ce4170
...@@ -468,9 +468,9 @@ static int opt_highlight_nondet_states = -1; ...@@ -468,9 +468,9 @@ static int opt_highlight_nondet_states = -1;
static int opt_highlight_nondet_edges = -1; static int opt_highlight_nondet_edges = -1;
static spot::twa_graph_ptr static spot::twa_graph_ptr
ensure_deterministic(const spot::twa_graph_ptr& aut) ensure_deterministic(const spot::twa_graph_ptr& aut, bool nonalt = false)
{ {
if (spot::is_deterministic(aut)) if (!(nonalt && aut->is_alternating()) && spot::is_deterministic(aut))
return aut; return aut;
spot::postprocessor p; spot::postprocessor p;
p.set_type(spot::postprocessor::Generic); p.set_type(spot::postprocessor::Generic);
...@@ -567,7 +567,7 @@ parse_opt(int key, char* arg, struct argp_state*) ...@@ -567,7 +567,7 @@ parse_opt(int key, char* arg, struct argp_state*)
error(2, 0, "only one --equivalent-to option can be given"); error(2, 0, "only one --equivalent-to option can be given");
opt->equivalent_pos = read_automaton(arg, opt->dict); opt->equivalent_pos = read_automaton(arg, opt->dict);
opt->equivalent_neg = opt->equivalent_neg =
spot::dtwa_complement(ensure_deterministic(opt->equivalent_pos)); spot::dtwa_complement(ensure_deterministic(opt->equivalent_pos, true));
break; break;
case OPT_GENERALIZED_RABIN: case OPT_GENERALIZED_RABIN:
if (arg) if (arg)
...@@ -638,7 +638,7 @@ parse_opt(int key, char* arg, struct argp_state*) ...@@ -638,7 +638,7 @@ parse_opt(int key, char* arg, struct argp_state*)
break; break;
case OPT_INCLUDED_IN: case OPT_INCLUDED_IN:
{ {
auto aut = ensure_deterministic(read_automaton(arg, opt->dict)); auto aut = ensure_deterministic(read_automaton(arg, opt->dict), true);
aut = spot::dtwa_complement(aut); aut = spot::dtwa_complement(aut);
if (!opt->included_in) if (!opt->included_in)
opt->included_in = aut; opt->included_in = aut;
...@@ -1088,13 +1088,13 @@ namespace ...@@ -1088,13 +1088,13 @@ namespace
if (opt_is_empty) if (opt_is_empty)
matched &= aut->is_empty(); matched &= aut->is_empty();
if (opt->intersect) if (opt->intersect)
matched &= !spot::product(aut, opt->intersect)->is_empty(); matched &= aut->intersects(opt->intersect);
if (opt->included_in) if (opt->included_in)
matched &= spot::product(aut, opt->included_in)->is_empty(); matched &= !aut->intersects(opt->included_in);
if (opt->equivalent_pos) if (opt->equivalent_pos)
matched &= spot::product(aut, opt->equivalent_neg)->is_empty() matched &= !aut->intersects(opt->equivalent_neg)
&& spot::product(dtwa_complement(ensure_deterministic(aut)), && (!dtwa_complement(ensure_deterministic(aut, true))->
opt->equivalent_pos)->is_empty(); intersects(opt->equivalent_pos));
if (matched && !opt->acc_words.empty()) if (matched && !opt->acc_words.empty())
for (auto& word_aut: opt->acc_words) for (auto& word_aut: opt->acc_words)
......
...@@ -25,6 +25,7 @@ ...@@ -25,6 +25,7 @@
#include <spot/twaalgos/couvreurnew.hh> #include <spot/twaalgos/couvreurnew.hh>
#include <spot/twaalgos/word.hh> #include <spot/twaalgos/word.hh>
#include <spot/twaalgos/remfin.hh> #include <spot/twaalgos/remfin.hh>
#include <spot/twaalgos/alternation.hh>
#include <spot/twa/twaproduct.hh> #include <spot/twa/twaproduct.hh>
#include <utility> #include <utility>
...@@ -48,14 +49,15 @@ namespace spot ...@@ -48,14 +49,15 @@ namespace spot
namespace namespace
{ {
// Remove Fin-acceptance and alternation.
const_twa_ptr remove_fin_maybe(const const_twa_ptr& a) const_twa_ptr remove_fin_maybe(const const_twa_ptr& a)
{ {
if (!a->acc().uses_fin_acceptance())
return a;
auto aa = std::dynamic_pointer_cast<const twa_graph>(a); auto aa = std::dynamic_pointer_cast<const twa_graph>(a);
if ((!aa || !aa->is_alternating()) && !a->acc().uses_fin_acceptance())
return a;
if (!aa) if (!aa)
aa = make_twa_graph(a, twa::prop_set::all()); aa = make_twa_graph(a, twa::prop_set::all());
return remove_fin(aa); return remove_fin(remove_alternation(aa));
} }
} }
......
...@@ -202,3 +202,74 @@ State: 1 ...@@ -202,3 +202,74 @@ State: 1
--END-- --END--
EOF EOF
diff expected res diff expected res
cat >ex1<<EOF
HOA: v1
States: 3
Start: 0
AP: 1 "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: univ-branch trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
State: 0
[0] 0
[!0] 0&1
State: 1
[!0] 1 {0}
[0] 2
State: 2
[t] 2
--END--
EOF
cat >ex2<<EOF
HOA: v1
States: 3
Start: 0&1
AP: 1 "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: univ-branch trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
State: 0
[0] 0
[!0] 0&1
State: 1
[!0] 1 {0}
[0] 2
State: 2
[t] 2
--END--
EOF
cat >ex3<<EOF
HOA: v1
States: 3
Start: 0
AP: 1 "a"
acc-name: co-Buchi
Acceptance: 1 Fin(0)
properties: univ-branch trans-labels explicit-labels trans-acc complete
properties: deterministic
--BODY--
State: 0
[0] 1
[!0] 0&1
State: 1
[!0] 1 {0}
[0] 2
State: 2
[t] 2
--END--
EOF
autfilt -q --equivalent-to=ex1 ex2
autfilt -q --included-in=ex1 ex2
autfilt -q --equivalent-to=ex1 ex3 && exit 1
autfilt -q --intersect=ex1 ex3
:
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