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

determinize: remove superfluous options

Browse source 
bisimulation and complete just trigger extra algorithms to be called at
the end of this one, so they need not be part of this algorithm.

* spot/twaalgos/determinize.cc, spot/twaalgos/determinize.hh: Reduce
the number of options.
* tests/core/safra.cc: Implement those options here.
This commit is contained in:
Alexandre Duret-Lutz 2016-02-05 23:28:10 +01:00
parent e0c2452534
commit 8e26852a1b
3 changed files with 25 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

12
spot/twaalgos/determinize.cc
View file

@ -32,7 +32,7 @@
#include <spot/twaalgos/degen.hh> #include <spot/twaalgos/degen.hh>
#include <spot/twaalgos/sccfilter.hh> #include <spot/twaalgos/sccfilter.hh>
#include <spot/twaalgos/simulation.hh> #include <spot/twaalgos/simulation.hh>
#include <spot/twaalgos/complete.hh>
namespace spot namespace spot
{ {
@ -607,9 +607,9 @@ namespace spot
} }
twa_graph_ptr twa_graph_ptr
tgba_determinisation(const const_twa_graph_ptr& a, bool bisimulation, tgba_determinisation(const const_twa_graph_ptr& a,
bool pretty_print, bool scc_opt, bool use_bisimulation, bool pretty_print, bool scc_opt,
bool complete, bool use_stutter) bool use_bisimulation, bool use_stutter)
{ {
// Degeneralize // Degeneralize
twa_graph_ptr aut = spot::degeneralize_tba(a); twa_graph_ptr aut = spot::degeneralize_tba(a);
@ -729,12 +729,8 @@ namespace spot
res->prop_deterministic(true); res->prop_deterministic(true);
res->prop_state_acc(false); res->prop_state_acc(false);
if (bisimulation)
res = simulation(res);
if (pretty_print) if (pretty_print)
res->set_named_prop("state-names", print_debug(seen)); res->set_named_prop("state-names", print_debug(seen));
if (complete)
spot::complete_here(res);
return res; return res;
} }
} }

2
spot/twaalgos/determinize.hh
View file

@ -25,10 +25,8 @@ namespace spot
{ {
SPOT_API twa_graph_ptr SPOT_API twa_graph_ptr
tgba_determinisation(const const_twa_graph_ptr& aut, tgba_determinisation(const const_twa_graph_ptr& aut,
bool bisimulation = false,
bool pretty_print = false, bool pretty_print = false,
bool scc_opt = false, bool scc_opt = false,
bool use_bisimulation = false, bool use_bisimulation = false,
bool complete = false,
bool use_stutter = false); bool use_stutter = false);
} }

35
tests/core/safra.cc
View file

@ -20,15 +20,17 @@
#include <iostream> #include <iostream>
#include <cstring> #include <cstring>
#include "spot/tl/parse.hh" // spot::parse_infix_psl #include <spot/tl/parse.hh> // spot::parse_infix_psl
#include "spot/tl/formula.hh" // spot::formula #include <spot/tl/formula.hh> // spot::formula
#include "spot/parseaut/public.hh" #include <spot/parseaut/public.hh>
#include "spot/twa/twagraph.hh" #include <spot/twa/twagraph.hh>
#include "spot/twaalgos/degen.hh" #include <spot/twaalgos/degen.hh>
#include "spot/twaalgos/dot.hh" // print_dot #include <spot/twaalgos/dot.hh> // print_dot
#include "spot/twaalgos/hoa.hh" // print_hoa #include <spot/twaalgos/hoa.hh> // print_hoa
#include "spot/twaalgos/determinize.hh" #include <spot/twaalgos/determinize.hh>
#include "spot/twaalgos/translate.hh" #include <spot/twaalgos/translate.hh>
#include <spot/twaalgos/complete.hh>
#include <spot/twaalgos/simulation.hh>
int help(); int help();
@ -117,18 +119,23 @@ int main(int argc, char* argv[])
spot::translator trans(dict); spot::translator trans(dict);
trans.set_pref(spot::postprocessor::Deterministic); trans.set_pref(spot::postprocessor::Deterministic);
auto tmp = trans.run(f); auto tmp = trans.run(f);
res = spot::tgba_determinisation(tmp, sim, pretty_print, scc_opt, res = spot::tgba_determinisation(tmp, pretty_print, scc_opt,
use_bisim, complete, use_stutter); use_bisim, use_stutter);
} }
else if (in_hoa) else if (in_hoa)
{ {
auto aut = spot::parse_aut(input, dict); auto aut = spot::parse_aut(input, dict);
if (aut->format_errors(std::cerr)) if (aut->format_errors(std::cerr))
return 2; return 2;
res = tgba_determinisation(aut->aut, sim, pretty_print, scc_opt, res = tgba_determinisation(aut->aut, pretty_print, scc_opt,
use_bisim, complete, use_stutter); use_bisim, use_stutter);
} }
res->merge_edges(); if (sim)
res = simulation(res);
else
res->merge_edges();
if (complete)
spot::complete_here(res);
if (out_hoa) if (out_hoa)
{ {