diff --git a/src/taalgos/dotty.cc b/src/taalgos/dotty.cc index a4716d9b0..52aa30898 100644 --- a/src/taalgos/dotty.cc +++ b/src/taalgos/dotty.cc @@ -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_; }; } diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc index ee5be9e7e..5ac0de8dc 100644 --- a/src/tgbatest/ltl2tgba.cc +++ b/src/tgbatest/ltl2tgba.cc @@ -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(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; } diff --git a/wrap/python/ajax/spot.in b/wrap/python/ajax/spot.in index 829cd51f2..fd0b7b872 100755 --- a/wrap/python/ajax/spot.in +++ b/wrap/python/ajax/spot.in @@ -287,9 +287,11 @@ However you may download the