Skip to content
GitLab
Commit bb9b204d authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

stutter: gather all code in one place 

* src/tgba/tgbasl.cc, src/tgba/tgbasl.hh, src/tgbaalgos/closure.cc,
src/tgbaalgos/closure.hh, src/tgbaalgos/stutter_invariance.cc,
src/tgbaalgos/stutter_invariance.hh, src/tgbaalgos/stutterize.cc,
src/tgbaalgos/stutterize.hh: Delete these files, and merge their
contents into...
* src/tgbaalgos/stutter.cc, src/tgbaalgos/stutter.hh: ... these two.
* src/tgba/Makefile.am, src/tgbaalgos/Makefile.am: Adjust.
* wrap/python/spot.i: Adjust.
parent ab985afa
Hide whitespace changes
Inline Side-by-side
src/tgba/Makefile.am
View file @ bb9b204d
## -*- coding: utf-8 -*-
## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche et
## Développement de l'Epita (LRDE).
## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 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
## et Marie Curie.
......@@ -37,8 +37,7 @@ tgba_HEADERS = \
tgbamask.hh \
tgbaproxy.hh \
tgbaproduct.hh \
tgbasafracomplement.hh \
tgbasl.hh
tgbasafracomplement.hh
noinst_LTLIBRARIES = libtgba.la
libtgba_la_SOURCES = \
......@@ -51,5 +50,4 @@ libtgba_la_SOURCES = \
tgbaproduct.cc \
tgbamask.cc \
tgbaproxy.cc \
tgbasafracomplement.cc \
tgbasl.cc
tgbasafracomplement.cc
src/tgba/tgbasl.cc deleted 100644 → 0
View file @ ab985afa
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2011, 2012, 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 <http://www.gnu.org/licenses/>.
#include "tgbasl.hh"
#include "bddprint.hh"
namespace spot
{
namespace
{
class state_tgbasl: public state
{
public:
state_tgbasl(state* s, bdd cond) : s_(s), cond_(cond)
{
}
virtual
~state_tgbasl()
{
s_->destroy();
}
virtual int
compare(const state* other) const
{
const state_tgbasl* o =
down_cast<const state_tgbasl*>(other);
assert(o);
int res = s_->compare(o->real_state());
if (res != 0)
return res;
return cond_.id() - o->cond_.id();
}
virtual size_t
hash() const
{
return wang32_hash(s_->hash()) ^ wang32_hash(cond_.id());
}
virtual
state_tgbasl* clone() const
{
return new state_tgbasl(*this);
}
state*
real_state() const
{
return s_;
}
bdd
cond() const
{
return cond_;
}
private:
state* s_;
bdd cond_;
};
class tgbasl_succ_iterator : public tgba_succ_iterator
{
public:
tgbasl_succ_iterator(tgba_succ_iterator* it, const state_tgbasl* state,
bdd_dict_ptr d, bdd atomic_propositions)
: it_(it), state_(state), aps_(atomic_propositions), d_(d)
{
}
virtual
~tgbasl_succ_iterator()
{
delete it_;
}
// iteration
bool
first()
{
loop_ = false;
done_ = false;
need_loop_ = true;
if (it_->first())
{
cond_ = it_->current_condition();
next_edge();
}
return true;
}
bool
next()
{
if (cond_ != bddfalse)
{
next_edge();
return true;
}
if (!it_->next())
{
if (loop_ || !need_loop_)
done_ = true;
loop_ = true;
return !done_;
}
else
{
cond_ = it_->current_condition();
next_edge();
return true;
}
}
bool
done() const
{
return it_->done() && done_;
}
// inspection
state_tgbasl*
current_state() const
{
if (loop_)
return new state_tgbasl(state_->real_state(), state_->cond());
return new state_tgbasl(it_->current_state(), one_);
}
bdd
current_condition() const
{
if (loop_)
return state_->cond();
return one_;
}
acc_cond::mark_t
current_acceptance_conditions() const
{
if (loop_)
return 0U;
return it_->current_acceptance_conditions();
}
private:
void
next_edge()
{
one_ = bdd_satoneset(cond_, aps_, bddtrue);
cond_ -= one_;
if (need_loop_ && (state_->cond() == one_)
&& (state_ == it_->current_state()))
need_loop_ = false;
}
tgba_succ_iterator* it_;
const state_tgbasl* state_;
bdd cond_;
bdd one_;
bdd aps_;
bdd_dict_ptr d_;
bool loop_;
bool need_loop_;
bool done_;
};
}
tgbasl::tgbasl(const const_tgba_ptr& a, bdd atomic_propositions)
: tgba(a->get_dict()), a_(a), aps_(atomic_propositions)
{
auto d = get_dict();
d->register_all_propositions_of(&a_, this);
assert(acc_.num_sets() == 0);
acc_.add_sets(a_->acc().num_sets());
}
tgbasl::~tgbasl()
{
get_dict()->unregister_all_my_variables(this);
}
state*
tgbasl::get_init_state() const
{
return new state_tgbasl(a_->get_init_state(), bddfalse);
}
tgba_succ_iterator*
tgbasl::succ_iter(const state* state) const
{
const state_tgbasl* s = down_cast<const state_tgbasl*>(state);
assert(s);
return new tgbasl_succ_iterator(a_->succ_iter(s->real_state()), s,
a_->get_dict(), aps_);
}
bdd
tgbasl::compute_support_conditions(const state*) const
{
return bddtrue;
}
std::string
tgbasl::format_state(const state* state) const
{
const state_tgbasl* s = down_cast<const state_tgbasl*>(state);
assert(s);
return (a_->format_state(s->real_state())
+ ", "
+ bdd_format_formula(a_->get_dict(), s->cond()));
}
}
src/tgba/tgbasl.hh deleted 100644 → 0
View file @ ab985afa
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2013, 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 <http://www.gnu.org/licenses/>.
#ifndef SPOT_TGBA_TGBASL_HH
# define SPOT_TGBA_TGBASL_HH
#include "tgba.hh"
namespace spot
{
class SPOT_API tgbasl : public tgba
{
public:
tgbasl(const const_tgba_ptr& a, bdd ap);
virtual ~tgbasl();
virtual state* get_init_state() const;
virtual tgba_succ_iterator* succ_iter(const state* state) const;
virtual std::string format_state(const state* state) const;
protected:
virtual bdd compute_support_conditions(const state* state) const;
private:
const_tgba_ptr a_;
bdd aps_;
};
typedef std::shared_ptr<tgbasl> tgbasl_ptr;
inline tgbasl_ptr make_tgbasl(const const_tgba_ptr& aut, bdd ap)
{
return std::make_shared<tgbasl>(aut, ap);
}
}
#endif
src/tgbaalgos/Makefile.am
View file @ bb9b204d
## -*- coding: utf-8 -*-
## Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire
## Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire
## de Recherche et Développement de l'Epita (LRDE).
## Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris
## 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
......@@ -31,7 +31,6 @@ tgbaalgos_HEADERS = \
are_isomorphic.hh \
bfssteps.hh \
canonicalize.hh \
closure.hh \
complete.hh \
compsusp.hh \
cycles.hh \
......@@ -73,8 +72,7 @@ tgbaalgos_HEADERS = \
simulation.hh \
stats.hh \
stripacc.hh \
stutter_invariance.hh \
stutterize.hh \
stutter.hh \
tau03.hh \
tau03opt.hh \
translate.hh \
......@@ -85,7 +83,6 @@ libtgbaalgos_la_SOURCES = \
are_isomorphic.cc \
bfssteps.cc \
canonicalize.cc \
closure.cc \
complete.cc \
compsusp.cc \
cycles.cc \
......@@ -127,8 +124,7 @@ libtgbaalgos_la_SOURCES = \
simulation.cc \
stats.cc \
stripacc.cc \
stutter_invariance.cc \
stutterize.cc \
stutter.cc \
tau03.cc \
tau03opt.cc \
translate.cc \
......
src/tgbaalgos/closure.cc deleted 100644 → 0
View file @ ab985afa
// -*- coding: utf-8 -*-
// Copyright (C) 2014, 2015 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 <http://www.gnu.org/licenses/>.
#include <unordered_set>
#include <deque>
#include "closure.hh"
#include "dupexp.hh"
#include <algorithm>
namespace spot
{
tgba_digraph_ptr
closure(tgba_digraph_ptr&& a)
{
a->prop_keep({false, // state_based
true, // single_acc
false, // inherently_weak
false, // deterministic
});
unsigned n = a->num_states();
std::vector<unsigned> todo;
std::vector<std::vector<unsigned> > dst2trans(n);
for (unsigned state = 0; state < n; ++state)
{
auto trans = a->out(state);
for (auto it = trans.begin(); it != trans.end(); ++it)
{
todo.push_back(it.trans());
dst2trans[it->dst].push_back(it.trans());
}
while (!todo.empty())
{
auto t1 = a->trans_storage(todo.back());
todo.pop_back();
for (auto& t2 : a->out(t1.dst))
{
bdd cond = t1.cond & t2.cond;
if (cond != bddfalse)
{
bool need_new_trans = true;
acc_cond::mark_t acc = t1.acc | t2.acc;
for (auto& t: dst2trans[t2.dst])
{
auto& ts = a->trans_storage(t);
if (acc == ts.acc)
{
if (!bdd_implies(cond, ts.cond))
{
ts.cond = ts.cond | cond;
if (std::find(todo.begin(), todo.end(), t)
== todo.end())
todo.push_back(t);
}
need_new_trans = false;
}
}
if (need_new_trans)
{
// Load t2.dst first, because t2 can be
// invalidated by new_transition().
auto dst = t2.dst;
auto i = a->new_transition(state, dst, cond, acc);
dst2trans[dst].push_back(i);
todo.push_back(i);
}
}
}
}
for (auto& it: dst2trans)
it.clear();
}
return a;
}
tgba_digraph_ptr
closure(const const_tgba_digraph_ptr& a)
{
return closure(make_tgba_digraph(a, {true, true, true, true}));
}
}
src/tgbaalgos/closure.hh deleted 100644 → 0
View file @ ab985afa
// 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 <http://www.gnu.org/licenses/>.
#ifndef SPOT_TGBAALGOS_CLOSURE_HH
# define SPOT_TGBAALGOS_CLOSURE_HH
#include "tgba/tgbagraph.hh"
namespace spot
{
SPOT_API tgba_digraph_ptr
closure(const const_tgba_digraph_ptr&);
#ifndef SWIG
SPOT_API tgba_digraph_ptr
closure(tgba_digraph_ptr&&);
#endif
}
#endif
src/tgbaalgos/stutterize.cc → src/tgbaalgos/stutter.cc
View file @ bb9b204d
......@@ -17,12 +17,18 @@
// You should have received a copy of the GNU General Public License
// along with this program. If not, see <http://www.gnu.org/licenses/>.
#include "stutterize.hh"
#include "stutter.hh"
#include "tgba/tgba.hh"
#include "dupexp.hh"
#include "misc/hash.hh"
#include "misc/hashfunc.hh"
#include "ltlvisit/apcollect.hh"
#include "translate.hh"
#include "ltlast/unop.hh"
#include "ltlvisit/remove_x.hh"
#include "tgbaalgos/product.hh"
#include "tgba/tgbaproduct.hh"
#include "tgba/bddprint.hh"
#include <deque>
#include <unordered_map>
#include <unordered_set>
......@@ -32,6 +38,227 @@ namespace spot
{
namespace
{
class state_tgbasl: public state
{
public:
state_tgbasl(state* s, bdd cond) : s_(s), cond_(cond)
{
}
virtual
~state_tgbasl()
{
s_->destroy();
}
virtual int
compare(const state* other) const
{
const state_tgbasl* o =
down_cast<const state_tgbasl*>(other);
assert(o);
int res = s_->compare(o->real_state());
if (res != 0)
return res;
return cond_.id() - o->cond_.id();
}
virtual size_t
hash() const
{
return wang32_hash(s_->hash()) ^ wang32_hash(cond_.id());
}
virtual
state_tgbasl* clone() const
{
return new state_tgbasl(*this);
}
state*
real_state() const
{
return s_;
}
bdd
cond() const
{
return cond_;
}
private:
state* s_;
bdd cond_;
};
class tgbasl_succ_iterator : public tgba_succ_iterator
{
public:
tgbasl_succ_iterator(tgba_succ_iterator* it, const state_tgbasl* state,
bdd_dict_ptr d, bdd atomic_propositions)
: it_(it), state_(state), aps_(atomic_propositions), d_(d)
{
}
virtual
~tgbasl_succ_iterator()
{
delete it_;
}
// iteration
bool
first()
{
loop_ = false;
done_ = false;
need_loop_ = true;
if (it_->first())
{
cond_ = it_->current_condition();
next_edge();
}
return true;
}
bool
next()
{
if (cond_ != bddfalse)
{
next_edge();
return true;
}
if (!it_->next())
{
if (loop_ || !need_loop_)
done_ = true;
loop_ = true;
return !done_;
}
else
{
cond_ = it_->current_condition();
next_edge();
return true;
}
}
bool
done() const
{
return it_->done() && done_;
}