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

Homogenize passing of automata as pointers, not references.

Browse source 
Disallow copy for security.

* src/tgba/tgbabddconcrete.hh (tgba_bdd_concrete): Disallow copy.
* src/tgba/tgbaexplicit.hh (tgba_explicit): Likewise.
* src/tgba/tgbaexplicit.cc (tgba_explicit::operator=,
tgba_explicit::tgba_explicit(tgba_explicit)): Remove.
* src/tgba/tgbabddconcreteproduct.cc
(tgba_bdd_concrete_product_factory::tgba_bdd_concrete_product_factory,
product): Take operand automata as pointers.
* src/tgba/tgbabddconcreteproduct.hh (product): Likewise.
* src/tgba/tgbaproduct.cc, src/tgba/tgbaproduct.hh:
(tgba_product): Disallow copy.
(tgba_product::tgba_product): Take operand automata as pointers.
* src/tgbaalgos/dotty.cc (dotty_state, dotty_rec, dotty_reachable):
Take tgba arguments as pointer.
* src/tgbaalgos/dotty.hh (dotty_reachable): Likewise.
* src/tgbaalgos/lbtt.cc (fill_todo, lbtt_reachable): Likewise.
* src/tgbaalgos/lbtt.hh (lbtt_reachable): Likewise.
* src/tgbaalgos/ltl2tgba.cc, src/tgbaalgos/ltl2tgba.hh (ltl_to_tgba):
Likewise.
* src/tgbaalgos/save.cc (save_rec, tgba_save_reachable): Likewise.
* src/tgbaalgos/save.hh (save): Likewise.
* src/tgbatest/explicit.cc, src/tgbatest/explprod.cc,
src/tgbatest/ltl2tgba.cc, src/tgbatest/ltlprod.cc,
src/tgbatest/mixprod.cc, src/tgbatest/readsave.cc,
src/tgbatest/spotlbtt.cc, src/tgbatest/tgbaread.cc,
src/tgbatest/tripprod.cc: Likewise.
This commit is contained in:
Alexandre Duret-Lutz 2003-07-14 22:20:35 +00:00
parent cab3be9795
commit 66b1630c31
25 changed files with 123 additions and 104 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/tgbaalgos/dotty.cc
View file

@ -10,7 +10,7 @@ namespace spot
/// Output and record a state.
static bool
dotty_state(std::ostream& os,
const tgba& g, state* st, seen_map& m, int& node)
const tgba* g, state* st, seen_map& m, int& node)
{
seen_map::iterator i = m.find(st);
@ -25,24 +25,24 @@ namespace spot
m[st] = node;
os << " " << node << " [label=\""
<< g.format_state(st) << "\"]" << std::endl;
<< g->format_state(st) << "\"]" << std::endl;
return true;
}
/// Process successors.
static void
dotty_rec(std::ostream& os,
const tgba& g, state* st, seen_map& m, int father)
const tgba* g, state* st, seen_map& m, int father)
{
tgba_succ_iterator* si = g.succ_iter(st);
tgba_succ_iterator* si = g->succ_iter(st);
for (si->first(); !si->done(); si->next())
{
int node;
state* s = si->current_state();
bool recurse = dotty_state(os, g, s, m, node);
os << " " << father << " -> " << node << " [label=\"";
bdd_print_set(os, g.get_dict(), si->current_condition()) << "\\n";
bdd_print_set(os, g.get_dict(), si->current_accepting_conditions())
bdd_print_set(os, g->get_dict(), si->current_condition()) << "\\n";
bdd_print_set(os, g->get_dict(), si->current_accepting_conditions())
<< "\"]" << std::endl;
if (recurse)
{
@ -58,10 +58,10 @@ namespace spot
}
std::ostream&
dotty_reachable(std::ostream& os, const tgba& g)
dotty_reachable(std::ostream& os, const tgba* g)
{
seen_map m;
state* state = g.get_init_state();
state* state = g->get_init_state();
os << "digraph G {" << std::endl;
os << " size=\"7.26,10.69\"" << std::endl;
os << " 0 [label=\"\", style=invis]" << std::endl;

2
src/tgbaalgos/dotty.hh
View file

@ -7,7 +7,7 @@
namespace spot
{
/// \brief Print reachable states in dot format.
std::ostream& dotty_reachable(std::ostream& os, const tgba& g);
std::ostream& dotty_reachable(std::ostream& os, const tgba* g);
}
#endif // SPOT_TGBAALGOS_DOTTY_HH

14
src/tgbaalgos/lbtt.cc
View file

@ -130,7 +130,7 @@ namespace spot
// a supplementary state, to act as initial state for LBTT.)
void
fill_todo(todo_set& todo, seen_map& seen, acp_seen_map& acp_seen,
state* state, const tgba& g,
state* state, const tgba* g,
minmax_pair& mmp, unsigned& state_number,
bool init)
{
@ -147,7 +147,7 @@ namespace spot
// Browse the successors of STATE to gather accepting
// conditions of outgoing transitions.
bdd_set acc_seen;
tgba_succ_iterator* si = g.succ_iter(state);
tgba_succ_iterator* si = g->succ_iter(state);
for (si->first(); !si->done(); si->next())
{
acc_seen.insert(si->current_accepting_conditions());
@ -176,9 +176,9 @@ namespace spot
}
std::ostream&
lbtt_reachable(std::ostream& os, const tgba& g)
lbtt_reachable(std::ostream& os, const tgba* g)
{
const bdd_dict* d = g.get_dict();
const bdd_dict* d = g->get_dict();
std::ostringstream body;
seen_map seen;
@ -189,8 +189,8 @@ namespace spot
minmax_pair mmp;
fill_todo(todo, seen, acp_seen,
g.get_init_state(), g, mmp, state_number, true);
accepting_cond_splitter acs(g.all_accepting_conditions());
g->get_init_state(), g, mmp, state_number, true);
accepting_cond_splitter acs(g->all_accepting_conditions());
while(! todo.empty())
{
@ -209,7 +209,7 @@ namespace spot
acs.split(body, sap.second);
body << "-1" << std::endl;
tgba_succ_iterator* si = g.succ_iter(sap.first);
tgba_succ_iterator* si = g->succ_iter(sap.first);
for (si->first(); !si->done(); si->next())
{
// We have put the accepting conditions on the state,

2
src/tgbaalgos/lbtt.hh
View file

@ -28,7 +28,7 @@ namespace spot
///
/// \param g The automata to print.
/// \param os Where to print.
std::ostream& lbtt_reachable(std::ostream& os, const tgba& g);
std::ostream& lbtt_reachable(std::ostream& os, const tgba* g);
}
#endif // SPOT_TGBAALGOS_LBTT_HH

5
src/tgbaalgos/ltl2tgba.cc
View file

@ -230,7 +230,7 @@ namespace spot
bool root_;
};
tgba_bdd_concrete
tgba_bdd_concrete*
ltl_to_tgba(const ltl::formula* f, bdd_dict* dict)
{
// Normalize the formula. We want all the negations on
@ -249,7 +249,6 @@ namespace spot
fact.finish();
// Finally setup the resulting automaton.
tgba_bdd_concrete g(fact, v.result());
return g;
return new tgba_bdd_concrete(fact, v.result());
}
}

2
src/tgbaalgos/ltl2tgba.hh
View file

@ -7,7 +7,7 @@
namespace spot
{
/// Build a spot::tgba_bdd_concrete from an LTL formula.
tgba_bdd_concrete ltl_to_tgba(const ltl::formula* f, bdd_dict* dict);
tgba_bdd_concrete* ltl_to_tgba(const ltl::formula* f, bdd_dict* dict);
}
#endif // SPOT_TGBA_LTL2TGBA_HH

18
src/tgbaalgos/save.cc
View file

@ -10,18 +10,18 @@ namespace spot
/// Process successors.
static void
save_rec(std::ostream& os, const tgba& g, state* st, seen_set& m)
save_rec(std::ostream& os, const tgba* g, state* st, seen_set& m)
{
m.insert(st);
std::string cur = g.format_state(st);
tgba_succ_iterator* si = g.succ_iter(st);
std::string cur = g->format_state(st);
tgba_succ_iterator* si = g->succ_iter(st);
for (si->first(); !si->done(); si->next())
{
state* s = si->current_state();
os << "\"" << cur << "\", \"" << g.format_state(s) << "\", ";
os << "\"" << cur << "\", \"" << g->format_state(s) << "\", ";
bdd_print_sat(os, g.get_dict(), si->current_condition()) << ",";
bdd_print_acc(os, g.get_dict(), si->current_accepting_conditions())
bdd_print_sat(os, g->get_dict(), si->current_condition()) << ",";
bdd_print_acc(os, g->get_dict(), si->current_accepting_conditions())
<< ";" << std::endl;
// Destination already explored?
@ -40,9 +40,9 @@ namespace spot
}
std::ostream&
tgba_save_reachable(std::ostream& os, const tgba& g)
tgba_save_reachable(std::ostream& os, const tgba* g)
{
const bdd_dict* d = g.get_dict();
const bdd_dict* d = g->get_dict();
os << "acc =";
for (bdd_dict::fv_map::const_iterator ai = d->acc_map.begin();
ai != d->acc_map.end(); ++ai)
@ -53,7 +53,7 @@ namespace spot
os << ";" << std::endl;
seen_set m;
state* state = g.get_init_state();
state* state = g->get_init_state();
save_rec(os, g, state, m);
// Finally delete all states used as keys in m:
for (seen_set::iterator i = m.begin(); i != m.end(); ++i)

2
src/tgbaalgos/save.hh
View file

@ -7,7 +7,7 @@
namespace spot
{
/// \brief Save reachable states in text format.
std::ostream& tgba_save_reachable(std::ostream& os, const tgba& g);
std::ostream& tgba_save_reachable(std::ostream& os, const tgba* g);
}
#endif // SPOT_TGBAALGOS_SAVE_HH