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

safra: Ensure automata is degeneralized

Browse source 
* src/tests/safra.cc, src/tests/safra.test:  Update it.
* src/twaalgos/safra.cc: Here;
This commit is contained in:
Alexandre Lewkowicz 2015-05-25 13:12:32 +02:00 • committed by Alexandre Duret-Lutz
parent 20fc8b0269
commit 8b1f9d3712
3 changed files with 38 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

28
src/tests/safra.cc
View file

@ -18,23 +18,43 @@
// along with this program. If not, see <http://www.gnu.org/licenses/>. // along with this program. If not, see <http://www.gnu.org/licenses/>.
#include <iostream> #include <iostream>
#include <cstring>
#include "twa/twagraph.hh"
#include "twaalgos/safra.hh" #include "twaalgos/safra.hh"
#include "twaalgos/translate.hh"
#include "hoaparse/public.hh" #include "hoaparse/public.hh"
#include "ltlparse/public.hh"
#include "twaalgos/dotty.hh" #include "twaalgos/dotty.hh"
int main(int argc, char* argv[]) int main(int argc, char* argv[])
{ {
if (argc <= 1) if (argc <= 2)
return 1; return 1;
char* input = argv[1]; char* input = argv[2];
spot::hoa_parse_error_list pel;
auto dict = spot::make_bdd_dict(); auto dict = spot::make_bdd_dict();
spot::twa_graph_ptr res;
if (!strncmp(argv[1], "-f", 2))
{
spot::ltl::parse_error_list pel;
const spot::ltl::formula* f =
spot::ltl::parse(input, pel, spot::ltl::default_environment::instance(),
false);
spot::translator trans(dict);
trans.set_pref(spot::postprocessor::Deterministic);
auto tmp = trans.run(f);
res = spot::tgba_determinisation(tmp);
f->destroy();
}
else if (!strncmp(argv[1], "--hoa", 5))
{
spot::hoa_parse_error_list pel;
auto aut = spot::hoa_parse(input, pel, dict); auto aut = spot::hoa_parse(input, pel, dict);
if (spot::format_hoa_parse_errors(std::cerr, input, pel)) if (spot::format_hoa_parse_errors(std::cerr, input, pel))
return 2; return 2;
auto res = tgba_determinisation(aut->aut); res = tgba_determinisation(aut->aut);
}
spot::dotty_reachable(std::cout, res); spot::dotty_reachable(std::cout, res);
} }

4
src/tests/safra.test
View file

@ -60,7 +60,7 @@ digraph G {
} }
EOF EOF
run 0 ../safra input.hoa > out.dot run 0 ../safra --hoa input.hoa > out.dot
diff out.dot out.exp diff out.dot out.exp
cat >input.hoa << EOF cat >input.hoa << EOF
@ -98,5 +98,5 @@ digraph G {
} }
EOF EOF
run 0 ../safra input.hoa > out.dot run 0 ../safra --hoa input.hoa > out.dot
diff out.dot out.exp diff out.dot out.exp

11
src/twaalgos/safra.cc
View file

@ -20,6 +20,7 @@
#include <deque> #include <deque>
#include "safra.hh" #include "safra.hh"
#include "twaalgos/degen.hh"
namespace spot namespace spot
{ {
@ -44,7 +45,6 @@ namespace spot
res.emplace_back(safra_state(nb_braces_.size()), t.cond); res.emplace_back(safra_state(nb_braces_.size()), t.cond);
} }
safra_state& ss = res[idx].first; safra_state& ss = res[idx].first;
assert(ss.nb_braces_.size() == ss.is_green_.size());
ss.update_succ(node.second, t.dst, t.acc); ss.update_succ(node.second, t.dst, t.acc);
assert(ss.nb_braces_.size() == ss.is_green_.size()); assert(ss.nb_braces_.size() == ss.is_green_.size());
} }
@ -150,6 +150,8 @@ namespace spot
// TODO handle multiple accepting sets // TODO handle multiple accepting sets
if (acc.count()) if (acc.count())
{ {
assert(acc.has(0) && acc.count() == 1 &&
"Only one TBA are accepted at the moment");
// Accepting transition generate new braces: step A1 // Accepting transition generate new braces: step A1
copy.emplace_back(nb_braces_.size()); copy.emplace_back(nb_braces_.size());
// nb_braces_ gets updated later so put 0 for now // nb_braces_ gets updated later so put 0 for now
@ -227,8 +229,13 @@ namespace spot
} }
twa_graph_ptr twa_graph_ptr
tgba_determinisation(const const_twa_graph_ptr& aut) tgba_determinisation(const const_twa_graph_ptr& a)
{ {
const_twa_graph_ptr aut;
if (a->acc().is_generalized_buchi())
aut = spot::degeneralize_tba(a);
else
aut = a;
auto res = make_twa_graph(aut->get_dict()); auto res = make_twa_graph(aut->get_dict());
res->copy_ap_of(aut); res->copy_ap_of(aut);
res->prop_copy(aut, res->prop_copy(aut,