diff --git a/src/graph/graph.hh b/src/graph/graph.hh index 79e1a0c7a..8a9789db2 100644 --- a/src/graph/graph.hh +++ b/src/graph/graph.hh @@ -24,7 +24,7 @@ #include #include #include - +#include namespace spot { @@ -197,7 +197,7 @@ namespace spot trans_storage_t&>::type operator*() { - return g_->transitions_[t_]; + return g_->trans_storage(t_); } trans_iterator operator++() @@ -244,6 +244,11 @@ namespace spot return {nullptr, 0}; } + void recycle(transition t) + { + t_ = t; + } + protected: transition t_; Graph* g_; @@ -309,6 +314,16 @@ namespace spot transitions_.resize(1); } + unsigned num_states() const + { + return states_.size(); + } + + unsigned num_transitions() const + { + return transitions_.size(); + } + template state new_state(Args&&... args) { @@ -317,11 +332,26 @@ namespace spot return s; } + state_storage_t& + state_storage(state s) + { + assert(s < states_.size()); + return states_[s]; + } + + const state_storage_t& + state_storage(state s) const + { + assert(s < states_.size()); + return states_[s]; + } + // Do not use State_Data& as return type, because State_Data might // be void. typename state_storage_t::data_t& state_data(state s) { + assert(s < states_.size()); return states_[s].data(); } @@ -329,17 +359,49 @@ namespace spot const typename state_storage_t::data_t& state_data(state s) const { + assert(s < states_.size()); return states_[s].data(); } + trans_storage_t& + trans_storage(transition s) + { + assert(s < transitions_.size()); + return transitions_[s]; + } + + const trans_storage_t& + trans_storage(transition s) const + { + assert(s < transitions_.size()); + return transitions_[s]; + } + + typename trans_storage_t::data_t& + trans_data(transition s) + { + assert(s < transitions_.size()); + return transitions_[s].data(); + } + + const typename trans_storage_t::data_t& + trans_data(transition s) const + { + assert(s < transitions_.size()); + return transitions_[s].data(); + } + template transition new_transition(state src, out_state dst, Args&&... args) { + assert(src < states_.size()); + transition t = transitions_.size(); transitions_.emplace_back(dst, 0, std::forward(args)...); transition st = states_[src].succ_tail; + assert(st < t || !st); if (!st) states_[src].succ = t; else diff --git a/src/graphtest/Makefile.am b/src/graphtest/Makefile.am index 2863c728e..eb33d9f88 100644 --- a/src/graphtest/Makefile.am +++ b/src/graphtest/Makefile.am @@ -22,12 +22,13 @@ AM_CPPFLAGS = -I$(srcdir)/.. -I.. $(BUDDY_CPPFLAGS) AM_CXXFLAGS = $(WARNING_CXXFLAGS) LDADD = ../libspot.la -noinst_PROGRAMS = graph ngraph +noinst_PROGRAMS = graph ngraph tgbagraph graph_SOURCES = graph.cc ngraph_SOURCES = ngraph.cc +tgbagraph_SOURCES = tgbagraph.cc -TESTS = graph.test ngraph.test +TESTS = graph.test ngraph.test tgbagraph.test EXTRA_DIST = $(TESTS) diff --git a/src/graphtest/tgbagraph.cc b/src/graphtest/tgbagraph.cc new file mode 100644 index 000000000..67a3df7e6 --- /dev/null +++ b/src/graphtest/tgbagraph.cc @@ -0,0 +1,60 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2014 Laboratoire de Recherche et Développement de +// l'Epita. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + + +#include +#include "tgba/tgbagraph.hh" +#include "tgbaalgos/dotty.hh" +#include "ltlenv/defaultenv.hh" + +void f1() +{ + spot::bdd_dict d; + + auto& e = spot::ltl::default_environment::instance(); + + spot::tgba_digraph tg(&d); + auto& g = tg.get_graph(); + + auto* f1 = e.require("p1"); + auto* f2 = e.require("p2"); + bdd p1 = bdd_ithvar(d.register_proposition(f1, &tg)); + bdd p2 = bdd_ithvar(d.register_proposition(f2, &tg)); + bdd a1 = bdd_ithvar(d.register_acceptance_variable(f1, &tg)); + bdd a2 = bdd_ithvar(d.register_acceptance_variable(f2, &tg)); + f1->destroy(); + f2->destroy(); + + auto s1 = g.new_state(); + auto s2 = g.new_state(); + auto s3 = g.new_state(); + g.new_transition(s1, s2, p1, bddfalse); + g.new_transition(s1, s3, p2, !a1 & a2); + g.new_transition(s2, s3, p1 & p2, a1 & !a2); + g.new_transition(s3, s1, p1 | p2, (!a1 & a2) | (a1 & !a2)); + g.new_transition(s3, s2, p1 >> p2, bddfalse); + g.new_transition(s3, s3, bddtrue, (!a1 & a2) | (a1 & !a2)); + + spot::dotty_reachable(std::cout, &tg); +} + +int main() +{ + f1(); +} diff --git a/src/graphtest/tgbagraph.test b/src/graphtest/tgbagraph.test new file mode 100755 index 000000000..23f58c5d8 --- /dev/null +++ b/src/graphtest/tgbagraph.test @@ -0,0 +1,52 @@ +#!/bin/sh +# -*- coding: utf-8 -*- +# Copyright (C) 2014 Laboratoire de Recherche et Développement de +# l'Epita (LRDE). +# +# This file is part of Spot, a model checking library. +# +# Spot is free software; you can redistribute it and/or modify it +# under the terms of the GNU General Public License as published by +# the Free Software Foundation; either version 3 of the License, or +# (at your option) any later version. +# +# Spot is distributed in the hope that it will be useful, but WITHOUT +# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +# License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see . + +# While running some benchmark, Tomáš Babiak found that Spot took too +# much time (i.e. >1h) to translate those six formulae. It turns out +# that the WDBA minimization was performed after the degeneralization +# algorithm, while this is not necessary (WDBA will produce a BA, so +# we may as well skip degeneralization). Translating these formulae +# in the test-suite ensure that they don't take too much time (the +# buildfarm will timeout if it does). + +. ./defs + +set -e + +run 0 ../tgbagraph | tee stdout + +cat >expected < 1 + 1 [label="0"] + 1 -> 2 [label="p1\n"] + 1 -> 3 [label="p2\n{Acc[p2]}"] + 2 [label="1"] + 2 -> 3 [label="p1 & p2\n{Acc[p1]}"] + 3 [label="2"] + 3 -> 1 [label="p1 | p2\n{Acc[p2], Acc[p1]}"] + 3 -> 2 [label="!p1 | p2\n"] + 3 -> 3 [label="1\n{Acc[p2], Acc[p1]}"] +} +EOF + +diff stdout expected + diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index b63844f86..328e07c84 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche et +## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche et ## Développement de l'Epita (LRDE). ## Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -44,6 +44,7 @@ tgba_HEADERS = \ tgbabddcoredata.hh \ tgbabddfactory.hh \ tgbaexplicit.hh \ + tgbagraph.hh \ tgbakvcomplement.hh \ tgbamask.hh \ tgbaproxy.hh \ diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh new file mode 100644 index 000000000..1e5cb5bfc --- /dev/null +++ b/src/tgba/tgbagraph.hh @@ -0,0 +1,313 @@ +// -*- coding: utf-8 -*- +// Copyright (C) 2014 Laboratoire de Recherche et Développement de +// l'Epita. +// +// This file is part of Spot, a model checking library. +// +// Spot is free software; you can redistribute it and/or modify it +// under the terms of the GNU General Public License as published by +// the Free Software Foundation; either version 3 of the License, or +// (at your option) any later version. +// +// Spot is distributed in the hope that it will be useful, but WITHOUT +// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public +// License for more details. +// +// You should have received a copy of the GNU General Public License +// along with this program. If not, see . + +#ifndef SPOT_TGBA_TGBAGRAPH_HH +# define SPOT_TGBA_TGBAGRAPH_HH + +#include "graph/graph.hh" +#include "tgba/bdddict.hh" +#include "tgba/tgba.hh" +#include "misc/bddop.hh" +#include + +namespace spot +{ + + struct SPOT_API tgba_graph_state: public spot::state + { + public: + virtual ~tgba_graph_state() noexcept + { + } + + virtual int compare(const spot::state* other) const + { + auto o = down_cast(other); + assert(o); + + // Do not simply return "other - this", it might not fit in an int. + if (o < this) + return -1; + if (o > this) + return 1; + return 0; + } + + virtual size_t hash() const + { + return + reinterpret_cast(this) - static_cast(nullptr); + } + + virtual tgba_graph_state* + clone() const + { + return const_cast(this); + } + + virtual void destroy() const + { + } + }; + + struct SPOT_API tgba_graph_trans_data + { + bdd cond; + bdd acc; + + explicit tgba_graph_trans_data() + : cond(bddfalse), acc(bddfalse) + { + } + + tgba_graph_trans_data(bdd cond, bdd acc) + : cond(cond), acc(acc) + { + } + }; + + + template + class tgba_digraph_succ_iterator: public tgba_succ_iterator + { + private: + typedef typename Graph::transition transition; + typedef typename Graph::state_data_t state; + const Graph* g_; + transition t_; + transition p_; + + public: + tgba_digraph_succ_iterator(const Graph* g, transition t) + : g_(g), t_(t) + { + } + + virtual void recycle(transition t) + { + t_ = t; + } + + virtual bool first() + { + p_ = t_; + return p_; + } + + virtual bool next() + { + p_ = g_->trans_storage(p_).next_succ; + return p_; + } + + virtual bool done() const + { + return !p_; + } + + virtual tgba_graph_state* current_state() const + { + assert(!done()); + return const_cast + (&g_->state_data(g_->trans_storage(p_).dst)); + } + + virtual bdd current_condition() const + { + assert(!done()); + return g_->trans_data(p_).cond; + } + + virtual bdd current_acceptance_conditions() const + { + assert(!done()); + return g_->trans_data(p_).acc; + } + + transition pos() const + { + return p_; + } + + }; + + class tgba_digraph: public tgba + { + protected: + typedef digraph graph_t; + graph_t g_; + bdd_dict* dict_; + bdd all_acceptance_conditions_; + bdd neg_acceptance_conditions_; + mutable const tgba_graph_state* init_; + + public: + tgba_digraph(bdd_dict* dict) + : dict_(dict), init_(nullptr) + { + } + + virtual ~tgba_digraph() + { + dict_->unregister_all_my_variables(this); + // Prevent this state from being destroyed by ~tgba(), + // as the state will be destroyed when g_ is destroyed. + last_support_conditions_input_ = 0; + } + + graph_t& get_graph() + { + return g_; + } + + const graph_t& get_graph() const + { + return g_; + } + + virtual bdd_dict* get_dict() const + { + return this->dict_; + } + + unsigned num_states() const + { + return g_.num_states(); + } + + unsigned num_transitions() const + { + return g_.num_transitions(); + } + + + void set_init_state(graph_t::state s) + { + init_ = &g_.state_data(s); + } + + void set_init_state(const state* s) + { + init_ = down_cast(s); + assert(init_); + } + + virtual tgba_graph_state* get_init_state() const + { + if (num_states() == 0) + const_cast(g_).new_state(); + if (!init_) + init_ = &g_.state_data(0); + return const_cast(init_); + } + + virtual graph_t::state get_init_state_number() const + { + if (num_states() == 0) + const_cast(g_).new_state(); + if (!init_) + return 0; + return state_number(init_); + } + + virtual tgba_succ_iterator* + succ_iter(const state* st) const + { + auto s = down_cast(st); + assert(s); + assert(s->succ < g_.num_transitions()); + + if (this->iter_cache_) + { + auto it = + down_cast*>(this->iter_cache_); + it->recycle(s->succ); + this->iter_cache_ = nullptr; + return it; + } + return new tgba_digraph_succ_iterator(&g_, s->succ); + } + + graph_t::state + state_number(const state* st) const + { + auto s = down_cast(st); + assert(s); + return s - &g_.state_storage(0); + } + + const state* + state_from_number(graph_t::state n) const + { + return &g_.state_data(n); + } + + virtual std::string format_state(const state* st) const + { + std::stringstream ss; + ss << state_number(st); + return ss.str(); + } + + tgba_graph_trans_data& trans_data(const tgba_succ_iterator* it) + { + auto* i = down_cast*>(it); + return g_.trans_data(i->pos()); + } + + + void set_acceptance_conditions(bdd all) + { + bdd sup = bdd_support(all); + this->dict_->register_acceptance_variables(sup, this); + neg_acceptance_conditions_ = bddtrue; + while (sup != bddtrue) + { + neg_acceptance_conditions_ &= bdd_nithvar(bdd_var(sup)); + sup = bdd_high(sup); + } + all_acceptance_conditions_ = + compute_all_acceptance_conditions(neg_acceptance_conditions_); + } + + /// \brief Copy the acceptance conditions of another tgba. + void copy_acceptance_conditions_of(const tgba *a) + { + set_acceptance_conditions(a->neg_acceptance_conditions()); + } + + virtual bdd all_acceptance_conditions() const + { + return all_acceptance_conditions_; + } + + virtual bdd neg_acceptance_conditions() const + { + return neg_acceptance_conditions_; + } + + virtual bdd compute_support_conditions(const state*) const + { + return bddtrue; + } + }; + +} + +#endif // SPOT_TGBA_TGBAGRAPH_HH