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

* src/tgbaalgos/neverclaim.hh (never_claim_reachable): Document

Browse source 
arguments.
* src/tgbaalgos/neverclaim.cc (never_claim_bfs::state_is_accepting):
New method.
(never_claim_bfs::get_state_label, never_claim_bfs::process_state):
Use it.
This commit is contained in:
Alexandre Duret-Lutz 2004-04-21 20:08:36 +00:00
parent 231a77a05f
commit 2f84bee41c
3 changed files with 38 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

7
ChangeLog
View file

@ -1,5 +1,12 @@
2004-04-21 Alexandre Duret-Lutz <adl@gnu.org> 2004-04-21 Alexandre Duret-Lutz <adl@gnu.org>
* src/tgbaalgos/neverclaim.hh (never_claim_reachable): Document
arguments.
* src/tgbaalgos/neverclaim.cc (never_claim_bfs::state_is_accepting):
New method.
(never_claim_bfs::get_state_label, never_claim_bfs::process_state):
Use it.
* wrap/python/cgi/ltl2tgba.in: Use darker color and introduce * wrap/python/cgi/ltl2tgba.in: Use darker color and introduce
the new variable dot_bgcolor. the new variable dot_bgcolor.

33
src/tgbaalgos/neverclaim.cc
View file

@ -35,8 +35,10 @@ namespace spot
class never_claim_bfs : public tgba_reachable_iterator_breadth_first class never_claim_bfs : public tgba_reachable_iterator_breadth_first
{ {
public: public:
never_claim_bfs(const tgba_tba_proxy* a, std::ostream& os, const ltl::formula* f) never_claim_bfs(const tgba_tba_proxy* a, std::ostream& os,
: tgba_reachable_iterator_breadth_first(a), os_(os), f_(f), accept_all_(-1), fi_needed_(false) const ltl::formula* f)
: tgba_reachable_iterator_breadth_first(a),
os_(os), f_(f), accept_all_(-1), fi_needed_(false)
{ {
} }
@ -68,12 +70,19 @@ namespace spot
delete init_; delete init_;
} }
bool
state_is_accepting(const state *s)
{
return
dynamic_cast<const tgba_tba_proxy*>(automata_)->state_is_accepting(s);
}
std::string std::string
get_state_label(const state* s, int n) get_state_label(const state* s, int n)
{ {
std::string label; std::string label;
if (s->compare(init_) == 0) if (s->compare(init_) == 0)
if (dynamic_cast<const tgba_tba_proxy*>(automata_)->state_is_accepting(s)) if (state_is_accepting(s))
label = "accept_init"; label = "accept_init";
else else
label = "T0_init"; label = "T0_init";
@ -83,7 +92,7 @@ namespace spot
ost << n; ost << n;
std::string ns(ost.str()); std::string ns(ost.str());
if (dynamic_cast<const tgba_tba_proxy*>(automata_)->state_is_accepting(s)) if (state_is_accepting(s))
{ {
tgba_succ_iterator* it = automata_->succ_iter(s); tgba_succ_iterator* it = automata_->succ_iter(s);
it->first(); it->first();
@ -92,7 +101,8 @@ namespace spot
else else
{ {
state* current = it->current_state(); state* current = it->current_state();
if (it->current_condition() != bddtrue || s->compare(current) != 0) if (it->current_condition() != bddtrue
|| s->compare(current) != 0)
label = "accept_S" + ns; label = "accept_S" + ns;
else else
label = "accept_all"; label = "accept_all";
@ -125,9 +135,10 @@ namespace spot
else else
{ {
state* current =it->current_state(); state* current =it->current_state();
if (dynamic_cast<const tgba_tba_proxy*>(automata_)->state_is_accepting(s) && if (state_is_accepting(s)
(it->current_condition() == bddtrue) && s->compare(init_) != 0 && && it->current_condition() == bddtrue
s->compare(current) == 0) && s->compare(init_) != 0
&& s->compare(current) == 0)
accept_all_ = n; accept_all_ = n;
else else
{ {
@ -150,7 +161,8 @@ namespace spot
if (in != accept_all_) if (in != accept_all_)
{ {
os_ << " :: (" ; os_ << " :: (" ;
const ltl::formula* f = bdd_to_formula(si->current_condition(), automata_->get_dict()); const ltl::formula* f = bdd_to_formula(si->current_condition(),
automata_->get_dict());
to_spin_string(f, os_); to_spin_string(f, os_);
destroy(f); destroy(f);
state* current = si->current_state(); state* current = si->current_state();
@ -168,7 +180,8 @@ namespace spot
}; };
std::ostream& std::ostream&
never_claim_reachable(std::ostream& os, const tgba_tba_proxy* g, const ltl::formula* f) never_claim_reachable(std::ostream& os, const tgba_tba_proxy* g,
const ltl::formula* f)
{ {
never_claim_bfs n(g, os, f); never_claim_bfs n(g, os, f);
n.run(); n.run();

9
src/tgbaalgos/neverclaim.hh
View file

@ -29,7 +29,14 @@
namespace spot namespace spot
{ {
/// \brief Print reachable states in Spin never claim format. /// \brief Print reachable states in Spin never claim format.
std::ostream& never_claim_reachable(std::ostream& os, const tgba_tba_proxy* g, const ltl::formula* f=0); ///
/// \param os The output stream to print on.
/// \param g The degeneralized automaton to output.
/// \param f The (optional) formula associated to the automaton. If given
/// it will be output as a comment.
std::ostream& never_claim_reachable(std::ostream& os,
const tgba_tba_proxy* g,
const ltl::formula* f = 0);
} }
#endif // SPOT_TGBAALGOS_NEVERCLAIM_HH #endif // SPOT_TGBAALGOS_NEVERCLAIM_HH