Clean up dotty output of TAs.
* src/taalgos/dotty.cc: Clean up output of TAs. * src/tgbatest/ltl2tgba.cc: Fix memory management, and use the TA printer for TGTA. * wrap/python/spot.i (as_ta): New function to convert a tgta_explicit into a TA. * wrap/python/ajax/spot.in: Use this new function to display automata.
This commit is contained in:
Alexandre Duret-Lutz
parent
852cd0d553
commit
d4130f15bf
4 changed files with 94 additions and 66 deletions
|
|
@ -1,4 +1,4 @@
|
|||
// Copyright (C) 2010 Laboratoire de Recherche et Developpement
|
||||
// Copyright (C) 2010, 2012 Laboratoire de Recherche et Developpement
|
||||
// de l Epita (LRDE).
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
|
|
@ -44,37 +44,32 @@ namespace spot
|
|||
|
||||
int n = 0;
|
||||
|
||||
spot::state* artificial_initial_state =
|
||||
t_automata_->get_artificial_initial_state();
|
||||
artificial_initial_state_ = t_automata_->get_artificial_initial_state();
|
||||
|
||||
ta::states_set_t init_states_set;
|
||||
|
||||
ta::states_set_t::const_iterator it;
|
||||
|
||||
if (artificial_initial_state != 0)
|
||||
{
|
||||
init_states_set.insert(artificial_initial_state);
|
||||
|
||||
}
|
||||
if (artificial_initial_state_)
|
||||
{
|
||||
init_states_set.insert(artificial_initial_state_);
|
||||
os_ << " 0 [label=\"\", style=invis, height=0]\n 0 -> 1\n";
|
||||
}
|
||||
else
|
||||
{
|
||||
init_states_set = t_automata_->get_initial_states_set();
|
||||
}
|
||||
|
||||
for (it = (init_states_set.begin()); it != init_states_set.end(); it++)
|
||||
{
|
||||
// cout << (*it).first << " => " << (*it).second << endl;
|
||||
|
||||
bdd init_condition = t_automata_->get_state_condition(*it);
|
||||
std::string label = bdd_format_formula(t_automata_->get_dict(),
|
||||
init_condition);
|
||||
++n;
|
||||
os_ << -n << " [label=\"\", style=invis, height=0]" << std::endl;
|
||||
os_ << " " << -n << " -> " << n << " " << "[label=\"" + label
|
||||
+ "\"]" << std::endl;
|
||||
|
||||
}
|
||||
{
|
||||
init_states_set = t_automata_->get_initial_states_set();
|
||||
|
||||
for (it = init_states_set.begin();
|
||||
it != init_states_set.end(); it++)
|
||||
{
|
||||
bdd init_condition = t_automata_->get_state_condition(*it);
|
||||
std::string label = bdd_format_formula(t_automata_->get_dict(),
|
||||
init_condition);
|
||||
++n;
|
||||
os_ << " " << -n << " [label=\"\", style=invis, height=0]\n "
|
||||
<< -n << " -> " << n << " [label=\"" << label << "\"]\n";
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void
|
||||
|
|
@ -87,47 +82,45 @@ namespace spot
|
|||
process_state(const state* s, int n)
|
||||
{
|
||||
|
||||
std::string shape = "ellipse";
|
||||
std::string style = "solid";
|
||||
std::string style;
|
||||
if (t_automata_->is_accepting_state(s))
|
||||
{
|
||||
shape = "doublecircle";
|
||||
style = "bold";
|
||||
}
|
||||
style = ",peripheries=2";
|
||||
|
||||
if (t_automata_->is_livelock_accepting_state(s))
|
||||
{
|
||||
shape = "octagon";
|
||||
style = "bold";
|
||||
}
|
||||
if (t_automata_->is_livelock_accepting_state(s)
|
||||
&& t_automata_->is_accepting_state(s))
|
||||
{
|
||||
shape = "doubleoctagon";
|
||||
style = "bold";
|
||||
}
|
||||
|
||||
os_ << " " << n << " [label=" << quote_unless_bare_word(
|
||||
t_automata_->format_state(s)) << "]" << "[shape=\"" + shape + "\"]"
|
||||
<< "[style=\"" + style + "\"]" << std::endl;
|
||||
if (t_automata_->is_livelock_accepting_state(s))
|
||||
style += ",shape=box";
|
||||
|
||||
os_ << " " << n << " [label=";
|
||||
if (s == artificial_initial_state_)
|
||||
os_ << "init";
|
||||
else
|
||||
os_ << quote_unless_bare_word(t_automata_->format_state(s));
|
||||
os_ << style << "]\n";
|
||||
}
|
||||
|
||||
void
|
||||
process_link(int in, int out, const ta_succ_iterator* si)
|
||||
{
|
||||
bdd_dict* d = t_automata_->get_dict();
|
||||
std::string label =
|
||||
((in == 1 && artificial_initial_state_)
|
||||
? bdd_format_formula(d, si->current_condition())
|
||||
: bdd_format_accset(d, si->current_condition()));
|
||||
|
||||
if (label.empty())
|
||||
label = "{}";
|
||||
|
||||
label += ("\n" +
|
||||
bdd_format_accset(d, si->current_acceptance_conditions()));
|
||||
|
||||
|
||||
os_ << " " << in << " -> " << out << " [label=\"";
|
||||
escape_str(os_, bdd_format_accset(t_automata_->get_dict(),
|
||||
si->current_condition()) + "\n" + bdd_format_accset(
|
||||
t_automata_->get_dict(), si->current_acceptance_conditions()))
|
||||
|
||||
<< "\"]" << std::endl;
|
||||
|
||||
escape_str(os_, label);
|
||||
os_ << "\"]\n";
|
||||
}
|
||||
|
||||
private:
|
||||
std::ostream& os_;
|
||||
spot::state* artificial_initial_state_;
|
||||
};
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1107,17 +1107,21 @@ main(int argc, char** argv)
|
|||
{
|
||||
spot::ta* testing_automata = 0;
|
||||
|
||||
tm.start("conversion to TA");
|
||||
testing_automata
|
||||
= tgba_to_ta(a, atomic_props_set_bdd, degeneralize_opt
|
||||
== DegenSBA, opt_with_artificial_initial_state,
|
||||
opt_single_pass_emptiness_check,
|
||||
opt_with_artificial_livelock);
|
||||
tm.stop("conversion to TA");
|
||||
|
||||
spot::ta* testing_automata_nm = 0;
|
||||
if (opt_bisim_ta)
|
||||
{
|
||||
tm.start("TA bisimulation");
|
||||
testing_automata_nm = testing_automata;
|
||||
testing_automata = minimize_ta(testing_automata);
|
||||
tm.stop("TA bisimulation");
|
||||
}
|
||||
|
||||
if (output != -1)
|
||||
|
|
@ -1125,14 +1129,15 @@ main(int argc, char** argv)
|
|||
tm.start("producing output");
|
||||
switch (output)
|
||||
{
|
||||
case 0:
|
||||
spot::dotty_reachable(std::cout, testing_automata);
|
||||
break;
|
||||
case 12:
|
||||
stats_reachable(testing_automata).dump(std::cout);
|
||||
break;
|
||||
default:
|
||||
assert(!"unknown output option");
|
||||
case 0:
|
||||
spot::dotty_reachable(std::cout, testing_automata);
|
||||
break;
|
||||
case 12:
|
||||
stats_reachable(testing_automata).dump(std::cout);
|
||||
break;
|
||||
default:
|
||||
std::cerr << "unsupported output option" << std::endl;
|
||||
exit(1);
|
||||
}
|
||||
tm.stop("producing output");
|
||||
}
|
||||
|
|
@ -1148,19 +1153,39 @@ main(int argc, char** argv)
|
|||
}
|
||||
if (tgta_opt)
|
||||
{
|
||||
to_free2 = a;
|
||||
spot::tgta* tgta = tgba_to_tgta(a, atomic_props_set_bdd);
|
||||
if (opt_bisim_ta)
|
||||
{
|
||||
tm.start("TA bisimulation");
|
||||
a = minimize_tgta(tgta);
|
||||
minimized = a;
|
||||
tm.stop("TA bisimulation");
|
||||
delete tgta;
|
||||
}
|
||||
else
|
||||
{
|
||||
a = tgta;
|
||||
}
|
||||
to_free2 = a;
|
||||
|
||||
to_free = tgta;
|
||||
if (output != -1)
|
||||
{
|
||||
tm.start("producing output");
|
||||
switch (output)
|
||||
{
|
||||
case 0:
|
||||
spot::dotty_reachable(std::cout,
|
||||
dynamic_cast<spot::ta*>(a));
|
||||
break;
|
||||
case 12:
|
||||
stats_reachable(a).dump(std::cout);
|
||||
break;
|
||||
default:
|
||||
std::cerr << "unsupported output option" << std::endl;
|
||||
exit(1);
|
||||
}
|
||||
tm.stop("producing output");
|
||||
}
|
||||
output = -1;
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -1465,6 +1490,7 @@ main(int argc, char** argv)
|
|||
delete ec;
|
||||
}
|
||||
|
||||
delete to_free2;
|
||||
if (show_fc)
|
||||
delete a;
|
||||
if (f)
|
||||
|
|
@ -1477,7 +1503,6 @@ main(int argc, char** argv)
|
|||
delete degeneralized;
|
||||
delete aut_scc;
|
||||
delete to_free;
|
||||
delete to_free2;
|
||||
delete echeck_inst;
|
||||
delete temp_dir_sim;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -287,9 +287,11 @@ However you may download the <a href="''' + cgi.escape(autprefix)
|
|||
|
||||
def render_automaton(automaton, dont_run_dot, issba, deco = None):
|
||||
dotsrc = spot.ostringstream()
|
||||
if isinstance(automaton, spot.ta):
|
||||
if isinstance(automaton, spot.ta): # TA/GTA
|
||||
spot.dotty_reachable(dotsrc, automaton)
|
||||
else:
|
||||
elif hasattr(automaton, 'as_ta'): # TGTA
|
||||
spot.dotty_reachable(dotsrc, automaton.as_ta())
|
||||
else: # TGBA
|
||||
spot.dotty_reachable(dotsrc, automaton, issba, deco)
|
||||
render_dot_maybe(dotsrc.str(), dont_run_dot)
|
||||
|
||||
|
|
|
|||
|
|
@ -317,6 +317,14 @@ using namespace spot;
|
|||
|
||||
}
|
||||
|
||||
%extend spot::tgta_explicit {
|
||||
const spot::ta*
|
||||
as_ta(const spot::tgta_explicit* t)
|
||||
{
|
||||
return dynamic_cast<const spot::ta*>(t);
|
||||
}
|
||||
}
|
||||
|
||||
%nodefaultctor std::ostream;
|
||||
namespace std {
|
||||
class ostream {};
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue