Optimizing closure and sl.
* src/tgbaalgos/closure.cc, src/tgbaalgos/closure.hh: Using vectors instead of sets and unordered maps, adding an overload to handle rvalue references. * src/tgbaalgos/stutterize.cc, src/tgbaalgos/stutterize.hh: Adding an overload to handle rvalue references. * bench/stutter/stutter_invariance_formulas.cc, bench/stutter/stutter_invariance_randomgraph.cc: Automata are modified in-place by is_stutter_invariant so they have to be copied before being processed. * src/tgbaalgos/stutter_invariance.cc, src/tgbaalgos/stutter_invariance.hh: Use the in-place version of closure and sl.
This commit is contained in:
Thibaud Michaud
Alexandre Duret-Lutz
parent
5817a3c11b
commit
fcf6e25132
8 changed files with 130 additions and 131 deletions
|
|
@ -23,6 +23,7 @@
|
|||
#include "bin/common_output.hh"
|
||||
#include "tgbaalgos/translate.hh"
|
||||
#include "tgbaalgos/stutter_invariance.hh"
|
||||
#include "tgbaalgos/dupexp.hh"
|
||||
#include "ltlast/allnodes.hh"
|
||||
#include "ltlvisit/apcollect.hh"
|
||||
#include "ltlvisit/length.hh"
|
||||
|
|
@ -30,13 +31,6 @@
|
|||
#include <argp.h>
|
||||
#include "error.h"
|
||||
|
||||
#include "tgbaalgos/closure.hh"
|
||||
#include "tgbaalgos/stutterize.hh"
|
||||
#include "tgbaalgos/dotty.hh"
|
||||
#include "tgba/tgbaproduct.hh"
|
||||
|
||||
static unsigned n = 10;
|
||||
|
||||
const char argp_program_doc[] ="";
|
||||
|
||||
const struct argp_child children[] =
|
||||
|
|
@ -74,8 +68,9 @@ namespace
|
|||
const spot::ltl::formula* nf =
|
||||
spot::ltl::unop::instance(spot::ltl::unop::Not,
|
||||
f->clone());
|
||||
spot::const_tgba_digraph_ptr a = trans.run(f);
|
||||
spot::const_tgba_digraph_ptr na = trans.run(nf);
|
||||
spot::tgba_digraph_ptr a = trans.run(f);
|
||||
spot::tgba_digraph_ptr na = trans.run(nf);
|
||||
unsigned num_states = a->num_states();
|
||||
spot::ltl::atomic_prop_set* ap = spot::ltl::atomic_prop_collect(f);
|
||||
bdd apdict = spot::ltl::atomic_prop_collect_as_bdd(f, a);
|
||||
bool res;
|
||||
|
|
@ -88,13 +83,16 @@ namespace
|
|||
setenv("SPOT_STUTTER_CHECK", algostr, true);
|
||||
|
||||
spot::stopwatch sw;
|
||||
auto dup_a = std::make_shared<spot::tgba_digraph>(a);
|
||||
auto dup_na = std::make_shared<spot::tgba_digraph>(na);
|
||||
|
||||
sw.start();
|
||||
for (unsigned i = 0; i < n; ++i)
|
||||
res = spot::is_stutter_invariant(a, na, apdict);
|
||||
res = spot::is_stutter_invariant(std::move(dup_a),
|
||||
std::move(dup_na), apdict);
|
||||
const double time = sw.stop();
|
||||
|
||||
std::cout << formula << ", " << algo << ", " << ap->size() << ", "
|
||||
<< a->num_states() << ", " << res << ", " << time << std::endl;
|
||||
<< num_states << ", " << res << ", " << time * 1000000 << std::endl;
|
||||
|
||||
if (algo > '1')
|
||||
assert(res == prev);
|
||||
|
|
|
|||
|
|
@ -75,18 +75,24 @@ main()
|
|||
|
||||
for (char algo = '1'; algo <= '8'; ++algo)
|
||||
{
|
||||
// set SPOT_STUTTER_CHECK environment variable
|
||||
// Set SPOT_STUTTER_CHECK environment variable.
|
||||
char algostr[2] = { 0 };
|
||||
algostr[0] = algo;
|
||||
setenv("SPOT_STUTTER_CHECK", algostr, true);
|
||||
|
||||
// Copy vec, because is_stutter_invariant modifies the
|
||||
// automata.
|
||||
std::vector<aut_pair_t> dup(vec);
|
||||
spot::stopwatch sw;
|
||||
sw.start();
|
||||
bool res;
|
||||
for (auto& a: vec)
|
||||
res = spot::is_stutter_invariant(a.first, a.second, apdict);
|
||||
res = spot::is_stutter_invariant(std::move(a.first),
|
||||
std::move(a.second),
|
||||
apdict);
|
||||
const double time = sw.stop();
|
||||
|
||||
vec = dup;
|
||||
std::cout << algo << ", " << props_n << ", " << states_n
|
||||
<< ", " << res << ", " << time << std::endl;
|
||||
}
|
||||
|
|
@ -95,6 +101,5 @@ main()
|
|||
}
|
||||
}
|
||||
|
||||
|
||||
return 0;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -21,101 +21,73 @@
|
|||
#include <deque>
|
||||
#include "closure.hh"
|
||||
#include "dupexp.hh"
|
||||
#include <algorithm>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
namespace
|
||||
tgba_digraph_ptr
|
||||
closure(tgba_digraph_ptr&& a)
|
||||
{
|
||||
struct transition
|
||||
{
|
||||
unsigned dst;
|
||||
acc_cond::mark_t acc;
|
||||
transition(unsigned dst, acc_cond::mark_t acc) :
|
||||
dst(dst), acc(acc)
|
||||
{
|
||||
}
|
||||
};
|
||||
unsigned n = a->num_states();
|
||||
std::vector<unsigned> todo;
|
||||
std::vector<std::vector<unsigned> > dst2trans(n);
|
||||
|
||||
struct transition_hash
|
||||
{
|
||||
size_t
|
||||
operator()(const transition& t) const
|
||||
for (unsigned state = 0; state < n; ++state)
|
||||
{
|
||||
return wang32_hash(t.dst) ^ wang32_hash(t.acc);
|
||||
}
|
||||
};
|
||||
auto trans = a->out(state);
|
||||
|
||||
struct transition_equal
|
||||
{
|
||||
bool
|
||||
operator()(const transition& left, const transition& right) const
|
||||
{
|
||||
return left.dst == right.dst
|
||||
&& left.acc == right.acc;
|
||||
}
|
||||
};
|
||||
for (auto it = trans.begin(); it != trans.end(); ++it)
|
||||
{
|
||||
todo.push_back(it.trans());
|
||||
dst2trans[it->dst].push_back(it.trans());
|
||||
}
|
||||
|
||||
typedef std::unordered_map<transition, unsigned, transition_hash,
|
||||
transition_equal> tmap_t;
|
||||
typedef std::set<unsigned> tset_t;
|
||||
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)
|
||||
{
|
||||
unsigned i =
|
||||
a->new_transition(state, t2.dst, cond, acc);
|
||||
dst2trans[t2.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)
|
||||
{
|
||||
tgba_digraph_ptr res = tgba_dupexp_dfs(a);
|
||||
unsigned n = res->num_states();
|
||||
tset_t todo;
|
||||
|
||||
for (unsigned state = 0; state < n; ++state)
|
||||
{
|
||||
tmap_t uniq;
|
||||
auto trans = res->out(state);
|
||||
|
||||
for (auto it = trans.begin(); it != trans.end(); ++it)
|
||||
{
|
||||
todo.insert(it.trans());
|
||||
uniq.emplace(transition(it->dst, it->acc), it.trans());
|
||||
}
|
||||
|
||||
while (!todo.empty())
|
||||
{
|
||||
unsigned t1 = *todo.begin();
|
||||
todo.erase(t1);
|
||||
tgba_graph_trans_data td = res->trans_data(t1);
|
||||
unsigned dst = res->trans_storage(t1).dst;
|
||||
|
||||
for (auto& t2 : res->out(dst))
|
||||
{
|
||||
bdd cond = td.cond & t2.cond;
|
||||
if (cond != bddfalse)
|
||||
{
|
||||
acc_cond::mark_t acc = td.acc | t2.acc;
|
||||
transition jump(t2.dst, acc);
|
||||
unsigned i;
|
||||
auto u = uniq.find(jump);
|
||||
|
||||
if (u == uniq.end())
|
||||
{
|
||||
i = res->new_transition(state, t2.dst, cond, acc);
|
||||
uniq.emplace(jump, i);
|
||||
todo.insert(i);
|
||||
}
|
||||
|
||||
else
|
||||
{
|
||||
bdd old_cond = res->trans_data(u->second).cond;
|
||||
if (!bdd_implies(cond, old_cond))
|
||||
{
|
||||
res->trans_data(u->second).cond = cond | old_cond;
|
||||
todo.insert(u->second);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
uniq.clear();
|
||||
}
|
||||
return res;
|
||||
return closure(make_tgba_digraph(a));
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -26,6 +26,11 @@ 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
|
||||
|
|
|
|||
|
|
@ -60,16 +60,16 @@ namespace spot
|
|||
}
|
||||
const ltl::formula* nf = ltl::unop::instance(ltl::unop::Not, f->clone());
|
||||
translator trans;
|
||||
auto aut_f = trans.run(f);
|
||||
auto aut_nf = trans.run(nf);
|
||||
tgba_digraph_ptr aut_f = trans.run(f);
|
||||
tgba_digraph_ptr aut_nf = trans.run(nf);
|
||||
bdd aps = atomic_prop_collect_as_bdd(f, aut_f);
|
||||
nf->destroy();
|
||||
return is_stutter_invariant(aut_f, aut_nf, aps);
|
||||
return is_stutter_invariant(std::move(aut_f), std::move(aut_nf), aps);
|
||||
}
|
||||
|
||||
bool
|
||||
is_stutter_invariant(const const_tgba_digraph_ptr& aut_f,
|
||||
const const_tgba_digraph_ptr& aut_nf, bdd aps)
|
||||
is_stutter_invariant(tgba_digraph_ptr&& aut_f,
|
||||
tgba_digraph_ptr&& aut_nf, bdd aps)
|
||||
{
|
||||
const char* stutter_check = getenv("SPOT_STUTTER_CHECK");
|
||||
char algo = stutter_check ? stutter_check[0] : '8';
|
||||
|
|
@ -79,32 +79,38 @@ namespace spot
|
|||
// sl(aut_f) x sl(aut_nf)
|
||||
case '1':
|
||||
{
|
||||
return product(sl(aut_f, aps), sl(aut_nf, aps))->is_empty();
|
||||
return product(sl(std::move(aut_f), aps),
|
||||
sl(std::move(aut_nf), aps))->is_empty();
|
||||
}
|
||||
// sl(cl(aut_f)) x aut_nf
|
||||
case '2':
|
||||
{
|
||||
return product(sl(closure(aut_f), aps), aut_nf)->is_empty();
|
||||
return product(sl(closure(std::move(aut_f)), aps),
|
||||
std::move(aut_nf))->is_empty();
|
||||
}
|
||||
// (cl(sl(aut_f)) x aut_nf
|
||||
case '3':
|
||||
{
|
||||
return product(closure(sl(aut_f, aps)), aut_nf)->is_empty();
|
||||
return product(closure(sl(std::move(aut_f), aps)),
|
||||
std::move(aut_nf))->is_empty();
|
||||
}
|
||||
// sl2(aut_f) x sl2(aut_nf)
|
||||
case '4':
|
||||
{
|
||||
return product(sl2(aut_f, aps), sl2(aut_nf, aps))->is_empty();
|
||||
return product(sl2(std::move(aut_f), aps),
|
||||
sl2(std::move(aut_nf), aps))->is_empty();
|
||||
}
|
||||
// sl2(cl(aut_f)) x aut_nf
|
||||
case '5':
|
||||
{
|
||||
return product(sl2(closure(aut_f), aps), aut_nf)->is_empty();
|
||||
return product(sl2(closure(std::move(aut_f)), aps),
|
||||
std::move(aut_nf))->is_empty();
|
||||
}
|
||||
// (cl(sl2(aut_f)) x aut_nf
|
||||
case '6':
|
||||
{
|
||||
return product(closure(sl2(aut_f, aps)), aut_nf)->is_empty();
|
||||
return product(closure(sl2(std::move(aut_f), aps)),
|
||||
std::move(aut_nf))->is_empty();
|
||||
}
|
||||
// on-the-fly sl(aut_f) x sl(aut_nf)
|
||||
case '7':
|
||||
|
|
@ -116,7 +122,8 @@ namespace spot
|
|||
// cl(aut_f) x cl(aut_nf)
|
||||
case '8':
|
||||
{
|
||||
return product(closure(aut_f), closure(aut_nf))->is_empty();
|
||||
return product(closure(std::move(aut_f)),
|
||||
closure(std::move(aut_nf)))->is_empty();
|
||||
}
|
||||
default:
|
||||
throw std::runtime_error("invalid value for SPOT_STUTTER_CHECK.");
|
||||
|
|
|
|||
|
|
@ -29,8 +29,8 @@ namespace spot
|
|||
is_stutter_invariant(const ltl::formula* f);
|
||||
|
||||
SPOT_API bool
|
||||
is_stutter_invariant(const const_tgba_digraph_ptr& aut_f,
|
||||
const const_tgba_digraph_ptr& aut_nf, bdd aps);
|
||||
is_stutter_invariant(tgba_digraph_ptr&& aut_f,
|
||||
tgba_digraph_ptr&& aut_nf, bdd aps);
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
|
|||
|
|
@ -133,38 +133,45 @@ namespace spot
|
|||
}
|
||||
|
||||
tgba_digraph_ptr
|
||||
sl2(const const_tgba_digraph_ptr& a, bdd atomic_propositions)
|
||||
sl2(tgba_digraph_ptr&& a, bdd atomic_propositions)
|
||||
{
|
||||
tgba_digraph_ptr res = tgba_dupexp_dfs(a);
|
||||
unsigned num_states = res->num_states();
|
||||
unsigned num_states = a->num_states();
|
||||
unsigned num_transitions = a->num_transitions();
|
||||
for (unsigned state = 0; state < num_states; ++state)
|
||||
{
|
||||
std::vector<unsigned> out;
|
||||
auto trans = res->out(state);
|
||||
auto trans = a->out(state);
|
||||
|
||||
for (auto it = trans.begin(); it != trans.end(); ++it)
|
||||
out.push_back(it.trans());
|
||||
for (auto it: out)
|
||||
for (auto it = trans.begin(); it != trans.end()
|
||||
&& it.trans() <= num_transitions; ++it)
|
||||
{
|
||||
if (res->trans_storage(it).dst != state)
|
||||
if (it->dst != state)
|
||||
{
|
||||
bdd all = res->trans_storage(it).cond;
|
||||
bdd all = it->cond;
|
||||
while (all != bddfalse)
|
||||
{
|
||||
unsigned dst = res->trans_storage(it).dst;
|
||||
unsigned dst = it->dst;
|
||||
bdd one = bdd_satoneset(all, atomic_propositions, bddtrue);
|
||||
unsigned tmp = res->new_state();
|
||||
res->new_transition(state, tmp, one,
|
||||
res->trans_storage(it).acc);
|
||||
res->new_transition(tmp, tmp, one, 0U);
|
||||
res->new_transition(tmp, dst, one,
|
||||
res->trans_storage(it).acc);
|
||||
unsigned tmp = a->new_state();
|
||||
unsigned i = a->new_transition(state, tmp, one,
|
||||
it->acc);
|
||||
assert(i > num_transitions);
|
||||
i = a->new_transition(tmp, tmp, one, 0U);
|
||||
assert(i > num_transitions);
|
||||
i = a->new_transition(tmp, dst, one,
|
||||
it->acc);
|
||||
assert(i > num_transitions);
|
||||
all -= one;
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
res->merge_transitions();
|
||||
return res;
|
||||
a->merge_transitions();
|
||||
return a;
|
||||
}
|
||||
|
||||
tgba_digraph_ptr
|
||||
sl2(const const_tgba_digraph_ptr& a, bdd atomic_propositions)
|
||||
{
|
||||
return sl2(make_tgba_digraph(a), atomic_propositions);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -38,6 +38,11 @@ namespace spot
|
|||
|
||||
SPOT_API tgba_digraph_ptr
|
||||
sl2(const const_tgba_digraph_ptr&, bdd);
|
||||
|
||||
#ifndef SWIG
|
||||
SPOT_API tgba_digraph_ptr
|
||||
sl2(tgba_digraph_ptr&&);
|
||||
#endif
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue