diff --git a/ChangeLog b/ChangeLog index 61d49b435..1877ebb1a 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,16 @@ 2004-05-21 Alexandre Duret-Lutz + * iface/gspn/gspn.cc (tgba_gspn_private_): Define alive_prop, + and dead_prop from the dead argument passed to the constructor. + (tgba_succ_iterator_gspn): Stutter on dead transitions. + (tgba_gspn::tgba_gspn): Hand dead to tgba_gspn_private_. + (gspn_interface::gspn_interface): Hand dead to tgba_gspn. + * iface/gspn/gspn.hh (gspn_interface::gspn_interface): Take a + dead argument. + * iface/gspn/ltlgspn.cc [!SSP]: Add a option -d to specify the + dead property. + * iface/gspn/udcseltl.test: Try option -d. + * src/sanity/style.test: Check the iface/ tree too. * iface/gspn/gspn.cc, iface/gspn/ssp.cc: Fix style. diff --git a/iface/gspn/gspn.cc b/iface/gspn/gspn.cc index 1fdd981d9..26e0d2ed0 100644 --- a/iface/gspn/gspn.cc +++ b/iface/gspn/gspn.cc @@ -89,9 +89,11 @@ namespace spot size_t index_count; const state_gspn* last_state_conds_input; bdd last_state_conds_output; + bdd alive_prop; + bdd dead_prop; - - tgba_gspn_private_(bdd_dict* dict, const gspn_environment& env) + tgba_gspn_private_(bdd_dict* dict, gspn_environment& env, + const std::string& dead) : refs(1), dict(dict), all_indexes(0), last_state_conds_input(0) { const gspn_environment::prop_map& p = env.get_prop_map(); @@ -101,6 +103,11 @@ namespace spot for (gspn_environment::prop_map::const_iterator i = p.begin(); i != p.end(); ++i) { + // Skip the DEAD proposition, GreatSPN knows nothing + // about it. + if (i->first == dead) + continue; + int var = dict->register_proposition(i->second, this); AtomicProp index; int err = prop_index(i->first.c_str(), &index); @@ -129,6 +136,38 @@ namespace spot dict->unregister_all_my_variables(this); throw; } + + // Register the "dead" proposition. There are three cases to + // consider: + // * If DEAD is "false", it means we are not interested in finite + // sequences of the system. + // * If DEAD is "true", we want to check finite sequences as well + // as infinite sequences, but do not need to distinguish them. + // * If DEAD is any other string, this is the name a property + // that should be true when looping on a dead state, and false + // otherwise. + // We handle these three case by setting ALIVE_PROP and DEAD_PROP + // appropriately. ALIVE_PROP is the bdd that should be ANDed + // to all transitions leaving a live state, while DEAD_PROP should + // bdd ANDed to all transitions leaving a dead state. + if (!strcasecmp(dead.c_str(), "false")) + { + alive_prop = bddtrue; + dead_prop = bddfalse; + } + else if (!strcasecmp(dead.c_str(), "true")) + { + alive_prop = bddtrue; + dead_prop = bddtrue; + } + else + { + ltl::formula* f = env.require(dead); + assert(f); + int var = dict->register_proposition(f, this); + dead_prop = bdd_ithvar(var); + alive_prop = bdd_nithvar(var); + } } tgba_gspn_private_::~tgba_gspn_private_() @@ -193,21 +232,22 @@ namespace spot successors_(0), size_(0), current_(0), - data_(data) + data_(data), + from_state_(state) { int res = succ(state, &successors_, &size_); if (res) throw gspn_exeption("succ()", res); - assert(successors_); - // GSPN is expected to return a looping "dead" transition where - // there is no successor. - assert(size_ > 0); + // GreatSPN should return successors_ == 0 and size_ == 0 when a + // state has no successors. + assert((size_ <= 0) ^ (successors_ != 0)); } virtual ~tgba_succ_iterator_gspn() { - succ_free(successors_); + if (successors_) + succ_free(successors_); } virtual void @@ -232,14 +272,23 @@ namespace spot virtual state* current_state() const { - return new state_gspn(successors_[current_].s); + // If GreatSPN returned no successor, we stutter on the dead state. + return + new state_gspn(successors_ ? successors_[current_].s : from_state_); } virtual bdd current_condition() const { - bdd p = data_->index_to_bdd(successors_[current_].p); - return state_conds_ & p; + if (successors_) + { + bdd p = data_->index_to_bdd(successors_[current_].p); + return state_conds_ & p & data_->alive_prop; + } + else + { + return state_conds_ & data_->dead_prop; + } } virtual bdd @@ -254,6 +303,7 @@ namespace spot size_t size_; /// size of successors_ size_t current_; /// current position in successors_ tgba_gspn_private_* data_; + State from_state_; }; // tgba_succ_iterator_gspn @@ -269,7 +319,8 @@ namespace spot class tgba_gspn: public tgba { public: - tgba_gspn(bdd_dict* dict, const gspn_environment& env); + tgba_gspn(bdd_dict* dict, gspn_environment& env, + const std::string& dead); tgba_gspn(const tgba_gspn& other); tgba_gspn& operator=(const tgba_gspn& other); virtual ~tgba_gspn(); @@ -290,9 +341,10 @@ namespace spot }; - tgba_gspn::tgba_gspn(bdd_dict* dict, const gspn_environment& env) + tgba_gspn::tgba_gspn(bdd_dict* dict, gspn_environment& env, + const std::string& dead) { - data_ = new tgba_gspn_private_(dict, env); + data_ = new tgba_gspn_private_(dict, env, dead); } tgba_gspn::tgba_gspn(const tgba_gspn& other) @@ -410,8 +462,9 @@ namespace spot ////////////////////////////////////////////////////////////////////// gspn_interface::gspn_interface(int argc, char **argv, - bdd_dict* dict, const gspn_environment& env) - : dict_(dict), env_(env) + bdd_dict* dict, gspn_environment& env, + const std::string& dead) + : dict_(dict), env_(env), dead_(dead) { int res = initialize(argc, argv); if (res) @@ -428,9 +481,7 @@ namespace spot tgba* gspn_interface::automaton() const { - return new tgba_gspn(dict_, env_); + return new tgba_gspn(dict_, env_, dead_); } - - } diff --git a/iface/gspn/gspn.hh b/iface/gspn/gspn.hh index 5bd1927e2..4c48e2039 100644 --- a/iface/gspn/gspn.hh +++ b/iface/gspn/gspn.hh @@ -36,12 +36,14 @@ namespace spot { public: gspn_interface(int argc, char **argv, - bdd_dict* dict, const gspn_environment& env); + bdd_dict* dict, gspn_environment& env, + const std::string& dead = "true"); ~gspn_interface(); tgba* automaton() const; private: bdd_dict* dict_; - const gspn_environment& env_; + gspn_environment& env_; + const std::string dead_; }; } diff --git a/iface/gspn/ltlgspn.cc b/iface/gspn/ltlgspn.cc index 84f23900a..e8bae46d5 100644 --- a/iface/gspn/ltlgspn.cc +++ b/iface/gspn/ltlgspn.cc @@ -52,6 +52,12 @@ syntax(char* prog) << " -c compute an example" << std::endl << " (instead of just checking for emptiness)" << std::endl << std::endl +#ifndef SSP + << " -d DEAD" << std::endl + << " use DEAD as property for marking dead states" + << " (by default DEAD=true)" << std::endl +#endif + << " -e use Couvreur's emptiness-check (default)" << std::endl << " -e2 use Couvreur's emptiness-check's shy variant" << std::endl #ifdef SSP @@ -81,6 +87,7 @@ main(int argc, char **argv) enum { Lacim, Fm } trans = Lacim; bool compute_counter_example = false; bool proj = true; + std::string dead = "true"; spot::gspn_environment env; @@ -90,6 +97,17 @@ main(int argc, char **argv) { compute_counter_example = true; } +#ifndef SSP + else if (!strcmp(argv[formula_index], "-d")) + { + if (formula_index + 1 >= argc) + syntax(argv[0]); + dead = argv[++formula_index]; + if (strcasecmp(dead.c_str(), "true") + && strcasecmp(dead.c_str(), "false")) + env.declare(dead); + } +#endif else if (!strcmp(argv[formula_index], "-e")) { check = Couvreur; @@ -164,7 +182,7 @@ main(int argc, char **argv) if (spot::format_tgba_parse_errors(std::cerr, pel1)) return 2; #else - spot::gspn_interface gspn(2, argv, dict, env); + spot::gspn_interface gspn(2, argv, dict, env, dead); #endif spot::tgba* a_f = 0; diff --git a/iface/gspn/udcseltl.test b/iface/gspn/udcseltl.test index 1489e9e39..351306aa9 100755 --- a/iface/gspn/udcseltl.test +++ b/iface/gspn/udcseltl.test @@ -20,7 +20,8 @@ chmod +w udcs # !G(ReP1 => F(gsP1)) is false ../ltlgspn-srg -c -l -e udcs/udcs \ '!G(ReP1 => F(gsP1))' ReP1 gsP1 >output && exit 1 -../ltlgspn-srg -c -l -e2 udcs/udcs \ +../ltlgspn-srg -d dead -c -l -e2 udcs/udcs \ '!G(ReP1 => F(gsP1))' ReP1 gsP1 >output && exit 1 - +grep 'dead:0' output +grep 'dead:1' output && exit 1 :