diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am
index b4bfcedad..8a9174ad5 100644
--- a/src/tgbaalgos/Makefile.am
+++ b/src/tgbaalgos/Makefile.am
@@ -29,6 +29,7 @@ tgbaalgosdir = $(pkgincludedir)/tgbaalgos
tgbaalgos_HEADERS = \
bfssteps.hh \
+ compsusp.hh \
cutscc.hh \
cycles.hh \
degen.hh \
@@ -73,6 +74,7 @@ tgbaalgos_HEADERS = \
noinst_LTLIBRARIES = libtgbaalgos.la
libtgbaalgos_la_SOURCES = \
bfssteps.cc \
+ compsusp.cc \
cutscc.cc \
cycles.cc \
degen.cc \
diff --git a/src/tgbaalgos/compsusp.cc b/src/tgbaalgos/compsusp.cc
new file mode 100644
index 000000000..7e1fdd013
--- /dev/null
+++ b/src/tgbaalgos/compsusp.cc
@@ -0,0 +1,441 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2012, 2013 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 .
+
+#include "compsusp.hh"
+#include "sccfilter.hh"
+#include "scc.hh"
+#include "tgba/tgbaexplicit.hh"
+#include "ltl2tgba_fm.hh"
+#include "minimize.hh"
+#include "simulation.hh"
+#include "safety.hh"
+#include "ltlast/allnodes.hh"
+#include "ltlvisit/tostring.hh"
+#include "ltlvisit/clone.hh"
+#include
+#include
+#include "ltlenv/environment.hh"
+
+namespace spot
+{
+ namespace
+ {
+ typedef std::map formula_bdd_map;
+
+ // An environment to store atomic proposition associated to
+ // suspended variable. (We don't use the default environment to
+ // avoid conflicts with user-defined atomic propositions that
+ // would share the same name.)
+ class suspended_environment: public ltl::environment
+ {
+ public:
+ const ltl::formula*
+ require(const std::string& s)
+ {
+ return ltl::atomic_prop::instance(s, *this);
+ }
+
+ const std::string&
+ name()
+ {
+ static std::string name("suspended environment");
+ return name;
+ }
+ };
+ static suspended_environment suspenv;
+
+ // Rewrite the suspendable subformulae "s" of an LTL formula in
+ // the form Gg where "g" is an atomic proposition representing
+ // "s". At the same time, populate maps that associate "s" to "g"
+ // and vice-versa.
+ class ltl_suspender_visitor: public ltl::clone_visitor
+ {
+ public:
+ typedef std::map fmap_t;
+ ltl_suspender_visitor(fmap_t& g2s, fmap_t& a2o, bool oblig)
+ : g2s_(g2s), a2o_(a2o), oblig_(oblig)
+ {
+ }
+
+ void
+ visit(const ltl::multop* mo)
+ {
+ ltl::multop::type op = mo->op();
+ switch (op)
+ {
+ case ltl::multop::Or:
+ case ltl::multop::And:
+ {
+ ltl::multop::vec* res = new ltl::multop::vec;
+ ltl::multop::vec* oblig = oblig_ ? new ltl::multop::vec : 0;
+ ltl::multop::vec* susp = new ltl::multop::vec;
+ unsigned mos = mo->size();
+ for (unsigned i = 0; i < mos; ++i)
+ {
+ const ltl::formula* c = mo->nth(i);
+ if (c->is_boolean())
+ res->push_back(c->clone());
+ else if (oblig_ && c->is_syntactic_obligation())
+ oblig->push_back(c->clone());
+ else if (c->is_eventual() && c->is_universal())
+ susp->push_back(c->clone());
+ else
+ res->push_back(recurse(c));
+ }
+ if (!oblig_ || oblig->empty())
+ {
+ delete oblig;
+ }
+ else
+ {
+ const ltl::formula* o = ltl::multop::instance(op, oblig);
+ res->push_back(recurse(o));
+ o->destroy();
+ }
+ if (susp->empty())
+ {
+ delete susp;
+ }
+ else
+ {
+ const ltl::formula* o = ltl::multop::instance(op, susp);
+ // Rewrite 'o' as 'G"o"'
+ const ltl::formula* g = recurse(o);
+ o->destroy();
+ if (op == ltl::multop::And)
+ {
+ res->push_back(g);
+ }
+ else
+ {
+ // res || susp -> (res && G![susp]) || G[susp])
+ const ltl::formula* r = ltl::multop::instance(op, res);
+ const ltl::unop* u =
+ down_cast(g);
+ const ltl::formula* gn =
+ ltl::unop::instance
+ (ltl::unop::G, ltl::unop::instance
+ (ltl::unop::Not, u->child()->clone()));
+ result_ = ltl::multop::instance
+ (ltl::multop::Or, ltl::multop::instance
+ (ltl::multop::And, r, gn),
+ g);
+ return;
+ }
+ }
+ result_ = ltl::multop::instance(op, res);
+ }
+ break;
+ case ltl::multop::OrRat:
+ case ltl::multop::AndRat:
+ case ltl::multop::AndNLM:
+ case ltl::multop::Concat:
+ case ltl::multop::Fusion:
+ this->ltl::clone_visitor::visit(mo);
+ break;
+ }
+ }
+
+
+ const ltl::formula*
+ recurse(const ltl::formula* f)
+ {
+ const ltl::formula* res;
+ if (f->is_boolean())
+ return f->clone();
+ if (oblig_ && f->is_syntactic_obligation())
+ {
+ fmap_t::const_iterator i = assoc_.find(f);
+ if (i != assoc_.end())
+ return i->second->clone();
+
+ std::ostringstream s;
+ s << "〈";
+ to_string(f, s);
+ s << "〉";
+ res = suspenv.require(s.str());
+ // We have to clone f, because it is not always a sub-tree
+ // of the original formula. (Think n-ary operators.)
+ a2o_[res] = f->clone();
+ assoc_[f] = res;
+ return res;
+ }
+ if (f->is_eventual() && f->is_universal())
+ {
+ fmap_t::const_iterator i = assoc_.find(f);
+ if (i != assoc_.end())
+ return ltl::unop::instance(ltl::unop::G, i->second->clone());
+
+ std::ostringstream s;
+ s << "[";
+ to_string(f, s);
+ s << "]";
+ res = suspenv.require(s.str());
+ // We have to clone f, because it is not always a sub-tree
+ // of the original formula. (Think n-ary operators.)
+ g2s_[res] = f->clone();
+ assoc_[f] = res;
+ return ltl::unop::instance(ltl::unop::G, res);
+ }
+ f->accept(*this);
+ return result_;
+ }
+
+ private:
+ fmap_t& g2s_;
+ fmap_t assoc_; // This one is only needed by the visitor.
+ fmap_t& a2o_;
+ bool oblig_;
+ };
+
+
+ typedef std::pair state_pair;
+
+ typedef std::map pair_map;
+ typedef std::deque pair_queue;
+
+ static
+ tgba*
+ susp_prod(tgba* left, const ltl::formula* f, bdd v)
+ {
+ bdd_dict* dict = left->get_dict();
+ const tgba* a1 = ltl_to_tgba_fm(f, dict, true, true);
+
+ const tgba* a2 = scc_filter(a1, false);
+ delete a1;
+ const tgba* right = iterated_simulations(a2);
+ delete a2;
+
+ tgba_explicit_number* res = new tgba_explicit_number(dict);
+ dict->register_all_variables_of(left, res);
+ dict->register_all_variables_of(right, res);
+ dict->unregister_variable(bdd_var(v), res);
+
+ // The left and right automata might have acceptance marker in
+ // common.
+ // For the example, assume left has acceptance conditions A,B,C,D
+ // while right has acceptance condition C,D,E,F.
+
+ // Negative acceptance variables...
+ // !A&!B&!C&!D
+ bdd lna = left->neg_acceptance_conditions();
+ // !C&!D&!E&!F
+ bdd rna = right->neg_acceptance_conditions();
+
+ // Missing acceptance variables...
+ // !E&!F
+ bdd lma = bdd_exist(rna, bdd_support(lna));
+ // !A&!B
+ bdd rma = bdd_exist(lna, bdd_support(rna));
+
+ // (A&!B&!C&!D + ... + !A&!B&!C&D) & !E&!F
+ bdd lac = left->all_acceptance_conditions() & lma;
+ // (C&!D&!E&!F + ... + !C&!D&!E&F) & !A&!B
+ bdd rac = right->all_acceptance_conditions() & rma;
+ bdd allacc = lac | rac;
+ res->set_acceptance_conditions(allacc);
+
+ // Acceptance condition to add to all transitions
+ // of the left automaton.
+ // !A&!B&!C&!D&E&!F | !A&!B&!C&!D&!E&F
+ bdd ladd = rac - lma;
+ bdd radd = lac - rma;
+
+ pair_map seen;
+ pair_queue todo;
+
+ state_pair p(left->get_init_state(), 0);
+ state* ris = right->get_init_state();
+ p.second = ris;
+ seen[p] = 0;
+ todo.push_back(p);
+ res->set_init_state(0);
+
+ typedef state_explicit_number::transition trans;
+
+ while (!todo.empty())
+ {
+ p = todo.front();
+ todo.pop_front();
+ const state* ls = p.first;
+ const state* rs = p.second;
+ int src = seen[p];
+
+ tgba_succ_iterator* li = left->succ_iter(ls);
+ for (li->first(); !li->done(); li->next())
+ {
+ state_pair d(li->current_state(), ris);
+ bdd lc = li->current_condition();
+
+ tgba_succ_iterator* ri = 0;
+ // Should we reset the right automaton?
+ if ((lc & v) == lc)
+ {
+ // No.
+ ri = right->succ_iter(rs);
+ ri->first();
+ }
+ // Yes. Reset the right automaton.
+ else
+ {
+ p.second = ris;
+ }
+
+ // This loops over all the right transitions
+ // if RI is defined. Otherwise this just makes
+ // one iteration as if the right automaton was
+ // looping in state 0 with "true".
+ while (!ri || !ri->done())
+ {
+ bdd cond = lc;
+ bdd ra = allacc;
+ if (ri)
+ {
+ cond = lc & ri->current_condition();
+ // Skip incompatible transitions.
+ if (cond == bddfalse)
+ {
+ ri->next();
+ continue;
+ }
+ d.second = ri->current_state();
+ ra = (ri->current_acceptance_conditions() & rma) | radd;
+ }
+
+ int dest = seen.size();
+ pair_map::const_iterator i = seen.find(d);
+ if (i != seen.end())
+ {
+ dest = i->second;
+ }
+ else
+ {
+ seen[d] = dest;
+ todo.push_back(d);
+ }
+
+ trans* t = res->create_transition(src, dest);
+ t->condition = bdd_exist(cond, v);
+ bdd la = (li->current_acceptance_conditions() & lma) | ladd;
+ t->acceptance_conditions = ra & la;
+
+ if (ri)
+ ri->next();
+ else
+ break;
+ }
+ delete ri;
+ }
+ }
+ delete left;
+ delete right;
+
+ return res;
+ }
+ }
+
+ tgba*
+ compsusp(const ltl::formula* f, bdd_dict* dict,
+ bool no_wdba, bool no_simulation,
+ bool early_susp, bool no_susp_product, bool wdba_smaller,
+ bool oblig)
+ {
+ ltl_suspender_visitor::fmap_t g2s;
+ ltl_suspender_visitor::fmap_t a2o;
+ ltl_suspender_visitor v(g2s, a2o, oblig);
+ const ltl::formula* g = v.recurse(f);
+
+ tgba* res;
+ {
+ // Translate the patched formula, and remove useless SCCs.
+ tgba* aut = spot::ltl_to_tgba_fm(g, dict, true, true, false, false, 0, 0);
+ res = scc_filter(aut, false);
+ delete aut;
+ }
+
+ if (!no_wdba)
+ {
+ tgba* min = minimize_obligation(res, g, 0, wdba_smaller);
+ if (min != res)
+ {
+ delete res;
+ res = min;
+ no_simulation = true;
+ }
+ }
+
+ if (!no_simulation)
+ {
+ tgba* sim = spot::iterated_simulations(res);
+ delete res;
+ res = sim;
+ }
+
+ spot::formula_bdd_map susp;
+ ltl_suspender_visitor::fmap_t::const_iterator it;
+ for (it = g2s.begin(); it != g2s.end(); ++it)
+ {
+ bdd_dict::fv_map::const_iterator j = dict->var_map.find(it->first);
+ assert(j != dict->var_map.end());
+ susp[it->second] = bdd_ithvar(j->second);
+ }
+
+ // Remove suspendable formulae from non-accepting SCCs.
+ bdd suspvars = bddtrue;
+ for (formula_bdd_map::const_iterator i = susp.begin();
+ i != susp.end(); ++i)
+ suspvars &= i->second;
+
+ bdd allaccap = bddtrue; // set of atomic prop used in accepting SCCs.
+ tgba* aut = res;
+ {
+ scc_map sm(aut);
+ sm.build_map();
+
+ // Restrict suspvars to the set of suspension labels that occur
+ // in accepting SCC.
+ unsigned sn = sm.scc_count();
+ for (unsigned n = 0; n < sn; n++)
+ if (sm.accepting(n))
+ allaccap &= sm.ap_set_of(n);
+
+ bdd ignored = bdd_exist(suspvars, allaccap);
+ suspvars = bdd_existcomp(suspvars, allaccap);
+ res = scc_filter(aut, false, &sm, suspvars, early_susp, ignored);
+ }
+ delete aut;
+
+ // Do we need to synchronize any suspended formula?
+ if (!susp.empty() && !no_susp_product)
+ for (formula_bdd_map::const_iterator i = susp.begin();
+ i != susp.end(); ++i)
+ if ((allaccap & i->second) == allaccap)
+ res = susp_prod(res, i->first, i->second);
+
+ g->destroy();
+
+ for (ltl_suspender_visitor::fmap_t::iterator i = g2s.begin();
+ i != g2s.end(); ++i)
+ i->second->destroy();
+ for (ltl_suspender_visitor::fmap_t::iterator i = a2o.begin();
+ i != a2o.end(); ++i)
+ i->second->destroy();
+ return res;
+ }
+}
diff --git a/src/tgbaalgos/compsusp.hh b/src/tgbaalgos/compsusp.hh
new file mode 100644
index 000000000..8aef32a73
--- /dev/null
+++ b/src/tgbaalgos/compsusp.hh
@@ -0,0 +1,58 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2012, 2013 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 .
+
+#ifndef SPOT_TGBAALGOS_COMPSUSP_HH
+# define SPOT_TGBAALGOS_COMPSUSP_HH
+
+#include "ltlast/formula.hh"
+
+namespace spot
+{
+ class tgba;
+ class bdd_dict;
+
+ /// \brief Compositional translation algorithm with resetable
+ /// suspension.
+ ///
+ /// Described in "Compositional Approach to Suspension and Other
+ /// Improvements to LTL Translation", Tomáš Babiak, Thomas Badie,
+ /// Alexandre Duret-Lutz, Mojmír Křetínský, Jan Strejček (SPIN'13).
+ ///
+ /// If \a no_wdba or \a no_simulation is true, the corresponding
+ /// operation is not performed on the skeleton automaton. If \a
+ /// early_susp is true, then composition starts on the transition
+ /// that enters the accepting SCC, not just in the SCC itself. If
+ /// \a no_susp_product is true, then the composition is not
+ /// performed and the skeleton automaton is returned for debugging.
+ /// If \a wdba_smaller is true, then the WDBA-minimization of the
+ /// skeleton is used only if it produces a smaller automaton.
+ ///
+ /// Finally the \a oblig flag is a work in progress and should not
+ /// be set to true.
+ ///
+ /// This interface is subject to change, and clients aiming for
+ /// long-term stability should better use the services of the
+ /// spot::translator class instead.
+ tgba* compsusp(const ltl::formula* f, bdd_dict* dict,
+ bool no_wdba = false, bool no_simulation = false,
+ bool early_susp = false, bool no_susp_product = false,
+ bool wdba_smaller = false, bool oblig = false);
+}
+
+#endif // SPOT_TGBAALGOS_COMPSUSP_HH
diff --git a/src/tgbaalgos/sccfilter.cc b/src/tgbaalgos/sccfilter.cc
index 2391798c3..3dc8776fb 100644
--- a/src/tgbaalgos/sccfilter.cc
+++ b/src/tgbaalgos/sccfilter.cc
@@ -195,7 +195,7 @@ namespace spot
}
}
- private:
+ protected:
T* out_;
const scc_map& sm_;
const std::vector& useless_;
@@ -205,14 +205,81 @@ namespace spot
remap_t remap_;
};
+ template
+ class filter_iter_susp: public filter_iter
+ {
+ public:
+ typedef filter_iter super;
+ filter_iter_susp(const tgba* a,
+ const scc_map& sm,
+ const std::vector& useless,
+ remap_table_t& remap_table,
+ unsigned max_num,
+ const std::vector& max_table,
+ bool remove_all_useless,
+ bdd susp_pos, bool early_susp, bdd ignored)
+ : super(a, sm, useless, remap_table, max_num, max_table,
+ remove_all_useless),
+ susp_pos(susp_pos), early_susp(early_susp), ignored(ignored)
+ {
+ }
+
+
+ void
+ process_link(const state* in_s, int in,
+ const state* out_s, int out,
+ const tgba_succ_iterator* si)
+ {
+ unsigned u = this->sm_.scc_of_state(out_s);
+ unsigned v = this->sm_.scc_of_state(in_s);
+ bool destacc = this->sm_.accepting(u);
+
+ typename super::output_t::state::transition* t =
+ create_transition(this->aut_, this->out_, in_s, in, out_s, out);
+
+ bdd cond = bdd_exist(si->current_condition(), ignored);
+ // Remove suspended variables on transitions going to
+ // non-accepting SCC, or on transition between SCC unless
+ // early_susp is set.
+ if (!destacc || (!early_susp && (u != this->sm_.scc_of_state(in_s))))
+ cond = bdd_exist(cond, susp_pos);
+
+ this->out_->add_conditions(t, cond);
+
+ // Regardless of all_, do not output any acceptance condition
+ // if the destination is not in an accepting SCC.
+ //
+ // If all_ is set, do not output any acceptance condition if the
+ // source is not in the same SCC as dest.
+ //
+ // (See the documentation of scc_filter() for a rational.)
+ if (destacc && (!this->all_ || u == v))
+ {
+ bdd acc = si->current_acceptance_conditions();
+ if (acc == bddfalse)
+ return;
+ t->acceptance_conditions = this->remap_[u][acc.id()];
+ }
+ }
+ protected:
+ bdd susp_pos;
+ bool early_susp;
+ bdd ignored;
+ };
+
} // anonymous
- tgba* scc_filter(const tgba* aut, bool remove_all_useless)
+ tgba* scc_filter(const tgba* aut, bool remove_all_useless,
+ scc_map* given_sm, bdd susp, bool early_susp, bdd ignored)
{
- scc_map sm(aut);
- sm.build_map();
- scc_stats ss = build_scc_stats(sm);
+ scc_map* sm = given_sm;
+ if (!sm)
+ {
+ sm = new scc_map(aut);
+ sm->build_map();
+ }
+ scc_stats ss = build_scc_stats(*sm);
remap_table_t remap_table(ss.scc_total);
std::vector max_table(ss.scc_total);
@@ -220,9 +287,9 @@ namespace spot
for (unsigned n = 0; n < ss.scc_total; ++n)
{
- if (!sm.accepting(n))
+ if (!sm->accepting(n))
continue;
- bdd all = sm.useful_acc_of(n);
+ bdd all = sm->useful_acc_of(n);
bdd negall = aut->neg_acceptance_conditions();
// Compute a set of useless acceptance conditions.
@@ -304,6 +371,7 @@ namespace spot
remap_table[n].insert(std::make_pair(bdd_var(c), --num));
}
+ tgba* ret;
// In most cases we will create a tgba_explicit_string copy of the
// initial tgba, but this is not very space efficient as the
// labels are built using the "format_state()" string output of
@@ -314,36 +382,81 @@ namespace spot
dynamic_cast(aut);
if (af)
{
- filter_iter fi(af, sm, ss.useless_scc_map,
- remap_table, max_num,
- max_table, remove_all_useless);
- fi.run();
- tgba_explicit_formula* res = fi.result();
- res->merge_transitions();
- return res;
- }
- const tgba_explicit_string* as =
- dynamic_cast(aut);
- if (as)
- {
- filter_iter fi(aut, sm, ss.useless_scc_map,
- remap_table, max_num,
- max_table, remove_all_useless);
- fi.run();
- tgba_explicit_string* res = fi.result();
- res->merge_transitions();
- return res;
+ if (susp == bddtrue)
+ {
+ filter_iter fi(af, *sm,
+ ss.useless_scc_map,
+ remap_table, max_num,
+ max_table,
+ remove_all_useless);
+ fi.run();
+ tgba_explicit_formula* res = fi.result();
+ res->merge_transitions();
+ ret = res;
+ }
+ else
+ {
+ filter_iter_susp fi(af, *sm,
+ ss.useless_scc_map,
+ remap_table, max_num,
+ max_table,
+ remove_all_useless,
+ susp, early_susp,
+ ignored);
+ fi.run();
+ tgba_explicit_formula* res = fi.result();
+ res->merge_transitions();
+ ret = res;
+ }
}
else
{
- filter_iter fi(aut, sm, ss.useless_scc_map,
- remap_table, max_num,
- max_table, remove_all_useless);
- fi.run();
- tgba_explicit_number* res = fi.result();
- res->merge_transitions();
- return res;
+ const tgba_explicit_string* as =
+ dynamic_cast(aut);
+ if (as)
+ {
+ filter_iter fi(aut, *sm, ss.useless_scc_map,
+ remap_table, max_num,
+ max_table,
+ remove_all_useless);
+ fi.run();
+ tgba_explicit_string* res = fi.result();
+ res->merge_transitions();
+ ret = res;
+ }
+ else
+ {
+ if (susp == bddtrue)
+ {
+ filter_iter fi(aut, *sm,
+ ss.useless_scc_map,
+ remap_table, max_num,
+ max_table,
+ remove_all_useless);
+ fi.run();
+ tgba_explicit_number* res = fi.result();
+ res->merge_transitions();
+ ret = res;
+ }
+ else
+ {
+ filter_iter_susp fi(aut, *sm,
+ ss.useless_scc_map,
+ remap_table, max_num,
+ max_table,
+ remove_all_useless,
+ susp, early_susp,
+ ignored);
+ fi.run();
+ tgba_explicit_number* res = fi.result();
+ res->merge_transitions();
+ ret = res;
+ }
+ }
}
+ if (!given_sm)
+ delete sm;
+ return ret;
}
}
diff --git a/src/tgbaalgos/sccfilter.hh b/src/tgbaalgos/sccfilter.hh
index fa4503b9a..791d04052 100644
--- a/src/tgbaalgos/sccfilter.hh
+++ b/src/tgbaalgos/sccfilter.hh
@@ -1,5 +1,5 @@
-// Copyright (C) 2009, 2010 Laboratoire de Recherche et Developpement
-// de l'Epita (LRDE).
+// Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et
+// Developpement de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
@@ -23,6 +23,7 @@
namespace spot
{
+ class scc_map;
/// \brief Prune unaccepting SCCs and remove superfluous acceptance
/// conditions.
@@ -45,7 +46,19 @@ namespace spot
/// remove_all_useless is \c false because some algorithms (like the
/// degeneralization) will work better if transitions going to an
/// accepting SCC are accepting.
- tgba* scc_filter(const tgba* aut, bool remove_all_useless = false);
+ ///
+ /// If \a given_sm is supplied, the function will use its result
+ /// without computing a map of its own.
+ ///
+ /// If \a susp is different from bddtrue, it should be a conjunction
+ /// of (positive) variables to be removed from transitions going to
+ /// non-accepting SCCs. If early_susp is false, the previous
+ /// variable are also removed from transitions entering an accepting
+ /// SCC. ignored is a conjunction of positive variables that should
+ /// be removed everywhere.
+ tgba* scc_filter(const tgba* aut, bool remove_all_useless = false,
+ scc_map* given_sm = 0, bdd susp = bddtrue,
+ bool early_susp = false, bdd ignored = bddtrue);
}
diff --git a/src/tgbatest/ltl2tgba.cc b/src/tgbatest/ltl2tgba.cc
index 415aa7dea..b109356a2 100644
--- a/src/tgbatest/ltl2tgba.cc
+++ b/src/tgbatest/ltl2tgba.cc
@@ -67,6 +67,7 @@
#include "tgbaalgos/isweakscc.hh"
#include "kripkeparse/public.hh"
#include "tgbaalgos/simulation.hh"
+#include "tgbaalgos/compsusp.hh"
#include "taalgos/tgba2ta.hh"
#include "taalgos/dotty.hh"
@@ -137,6 +138,8 @@ syntax(char* prog)
<< std::endl
<< " -taa use Tauriainen's TAA-based algorithm for LTL"
<< std::endl
+ << " -u use Compositional translation"
+ << std::endl
<< std::endl
<< "Options for Couvreur's FM algorithm (-f):" << std::endl
@@ -337,7 +340,8 @@ main(int argc, char** argv)
bool utf8_opt = false;
enum { NoDegen, DegenTBA, DegenSBA } degeneralize_opt = NoDegen;
enum { TransitionLabeled, StateLabeled } labeling_opt = TransitionLabeled;
- enum { TransFM, TransLaCIM, TransLaCIM_ELTL, TransLaCIM_ELTL_ops, TransTAA }
+ enum { TransFM, TransLaCIM, TransLaCIM_ELTL, TransLaCIM_ELTL_ops, TransTAA,
+ TransCompo }
translation = TransFM;
bool fm_red = false;
bool fm_exprop_opt = false;
@@ -400,6 +404,11 @@ main(int argc, char** argv)
spot::tgba* temp_iterated_sim = 0;
spot::tgba* temp_dont_care_sim = 0;
spot::tgba* temp_dont_care_iterated_sim = 0;
+ bool cs_nowdba = true;
+ bool cs_wdba_smaller = false;
+ bool cs_nosimul = true;
+ bool cs_early_start = false;
+ bool cs_oblig = false;
for (;;)
{
@@ -826,6 +835,50 @@ main(int argc, char** argv)
tok = strtok(0, ", \t;");
}
}
+ else if (!strncmp(argv[formula_index], "-u", 2))
+ {
+ translation = TransCompo;
+ const char* c = argv[formula_index] + 2;
+ while (*c != 0)
+ {
+ switch (*c)
+ {
+ case '2':
+ cs_nowdba = false;
+ cs_wdba_smaller = true;
+ break;
+ case 'w':
+ cs_nowdba = false;
+ cs_wdba_smaller = false;
+ break;
+ case 's':
+ cs_nosimul = false;
+ break;
+ case 'e':
+ cs_early_start = true;
+ break;
+ case 'W':
+ cs_nowdba = true;
+ break;
+ case 'S':
+ cs_nosimul = true;
+ break;
+ case 'E':
+ cs_early_start = false;
+ break;
+ case 'o':
+ cs_oblig = true;
+ break;
+ case 'O':
+ cs_oblig = false;
+ break;
+ default:
+ std::cerr << "Unknown suboption `" << *c
+ << "' for option -u" << std::endl;
+ }
+ ++c;
+ }
+ }
else if (!strcmp(argv[formula_index], "-v"))
{
output = 5;
@@ -906,6 +959,7 @@ main(int argc, char** argv)
case TransFM:
case TransLaCIM:
case TransTAA:
+ case TransCompo:
{
spot::ltl::parse_error_list pel;
tm.start("parsing formula");
@@ -1037,7 +1091,7 @@ main(int argc, char** argv)
if (f->is_psl_formula()
&& !f->is_ltl_formula()
- && translation != TransFM)
+ && (translation != TransFM && translation != TransCompo))
{
std::cerr << "Only the FM algorithm can translate PSL formulae;"
<< " I'm using it for this formula." << std::endl;
@@ -1055,6 +1109,13 @@ main(int argc, char** argv)
unobservables,
fm_red ? simp : 0);
break;
+ case TransCompo:
+ {
+ a = spot::compsusp(f, dict,
+ cs_nowdba, cs_nosimul, cs_early_start,
+ false, cs_wdba_smaller, cs_oblig);
+ break;
+ }
case TransTAA:
a = spot::ltl_to_taa(f, dict, containment);
break;
diff --git a/src/tgbatest/spotlbtt.test b/src/tgbatest/spotlbtt.test
index a151ea110..8eb69f9a9 100755
--- a/src/tgbatest/spotlbtt.test
+++ b/src/tgbatest/spotlbtt.test
@@ -240,6 +240,21 @@ Algorithm
Enabled = yes
}
+Algorithm
+{
+ Name = "Compositional Suspension"
+ Path = "${LBTT_TRANSLATE}"
+ Parameters = "--spot '../ltl2tgba -u -F -f -t'"
+ Enabled = yes
+}
+
+Algorithm
+{
+ Name = "Compositional Suspension (-r4)"
+ Path = "${LBTT_TRANSLATE}"
+ Parameters = "--spot '../ltl2tgba -u -r4 -F -f -t'"
+ Enabled = yes
+}
Algorithm
{