alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

autfilt: complement of non-deterministic automata as well

Browse source 
* bin/autfilt.cc: Determinize automata before complementation
if needed.
* tests/core/complement.test: Adjust.
* NEWS: Mention the new feature.
This commit is contained in:
Alexandre Duret-Lutz 2016-02-12 17:00:20 +01:00
parent 6a662a6d8e
commit 9799a6455e
3 changed files with 42 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

5
NEWS
View file

@ -32,6 +32,11 @@ New in spot 1.99.7a (not yet released)
fail to find a deterministic automaton (even if one exists) and fail to find a deterministic automaton (even if one exists) and
return a nondeterministic automaton. return a nondeterministic automaton.
* "autfilt --complement" now also works for non-deterministic
automata but will output a deterministic automaton.
"autfilt --complement --tgba" will likely output a
nondeterministic TGBA.
Library: Library:
* Building products with different dictionaries now raise an * Building products with different dictionaries now raise an

25
bin/autfilt.cc
View file

@ -562,17 +562,6 @@ namespace
if (opt_complement_acc) if (opt_complement_acc)
aut->set_acceptance(aut->acc().num_sets(), aut->set_acceptance(aut->acc().num_sets(),
aut->get_acceptance().complement()); aut->get_acceptance().complement());
if (opt_complement)
{
if (!spot::is_deterministic(aut))
{
std::cerr << filename << ':'
<< haut->loc << (": --complement currently supports "
"only deterministic automata\n");
exit(2);
}
aut = spot::dtwa_complement(aut);
}
if (opt_rem_fin) if (opt_rem_fin)
aut = remove_fin(aut); aut = remove_fin(aut);
if (opt_dnf_acc) if (opt_dnf_acc)
@ -658,6 +647,20 @@ namespace
return 0; return 0;
} }
if (opt_complement)
{
if (!spot::is_deterministic(aut))
{
// let's determinize that automaton
spot::postprocessor p;
p.set_type(spot::postprocessor::Generic);
p.set_pref(spot::postprocessor::Deterministic);
p.set_level(level);
aut = p.run(aut);
}
aut = spot::dtwa_complement(aut);
}
aut = post.run(aut, nullptr); aut = post.run(aut, nullptr);
if (randomize_st || randomize_tr) if (randomize_st || randomize_tr)

27
tests/core/complement.test
View file

@ -1,6 +1,6 @@
#!/bin/sh #!/bin/sh
# -*- coding: utf-8 -*- # -*- coding: utf-8 -*-
# Copyright (C) 2015 Laboratoire de Recherche et Développement de # Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de
# l'Epita (LRDE). # l'Epita (LRDE).
# #
# This file is part of Spot, a model checking library. # This file is part of Spot, a model checking library.
@ -93,6 +93,25 @@ State: 3
EOF EOF
diff out expected diff out expected
# The complement of a nondeterministic automaton is currently done via
$ltl2tgba -H 'FGa' | $autfilt --complement 2>out && exit 1 # a determinization.
grep 'deterministic' out $ltl2tgba -H 'FGa' | $autfilt --complement >out
cat >expected <<EOF
HOA: v1
States: 2
Start: 0
AP: 1 "a"
acc-name: parity min even 2
Acceptance: 2 Inf(0) | Fin(1)
properties: trans-labels explicit-labels trans-acc complete
properties: deterministic stutter-invariant
--BODY--
State: 0
[0] 1 {1}
[!0] 0
State: 1
[0] 1 {1}
[!0] 0 {0}
--END--
EOF
diff out expected