simulation: get rid of the "don't care" simulation reductions
Those where never really publicized because they were slow and we failed to fix what we hopped to fix with them. They where never used by default. Getting rid of them will make it easier to cleanup the simulation code. * src/tgbaalgos/simulation.cc, src/tgbaalgos/simulation.hh: Remove the simulation code. * src/tgbaalgos/postproc.cc, src/tgbaalgos/postproc.hh, src/tgbatest/ltl2tgba.cc: Do not call it. * src/bin/spot-x.cc: Update doc. * src/tgbatest/sim.test: Delete this file. * src/tgbatest/Makefile.am: Adjust. * src/tgbatest/spotlbtt.test, bench/ltl2tgba/tools.sim: Remove uses to don't care simulation.
This commit is contained in:
Alexandre Duret-Lutz
parent
1d724beabd
commit
0159027395
10 changed files with 19 additions and 807 deletions
|
|
@ -1,6 +1,6 @@
|
|||
## -*- coding: utf-8; mode: sh -*-
|
||||
## Copyright (C) 2013 Laboratoire de Recherche et Développement de
|
||||
## l'Epita (LRDE).
|
||||
## Copyright (C) 2013, 2015 Laboratoire de Recherche et Développement
|
||||
## de l'Epita (LRDE).
|
||||
##
|
||||
## This file is part of Spot, a model checking library.
|
||||
##
|
||||
|
|
@ -25,11 +25,9 @@ set dummy \
|
|||
"$LTL2TGBA --lbtt -x simul=1 %f >%T" \
|
||||
"$LTL2TGBA --lbtt -x simul=2 %f >%T" \
|
||||
"$LTL2TGBA --lbtt -x simul=3 %f >%T" \
|
||||
"$LTL2TGBA --lbtt -x simul=4 %f >%T" \
|
||||
"$LTL2TGBA --lbtt --ba -x simul=0 %f >%T" \
|
||||
"$LTL2TGBA --lbtt --ba -x simul=1 %f >%T" \
|
||||
"$LTL2TGBA --lbtt --ba -x simul=2 %f >%T" \
|
||||
"$LTL2TGBA --lbtt --ba -x simul=3 %f >%T" \
|
||||
"$LTL2TGBA --lbtt --ba -x simul=4 %f >%T" \
|
||||
--timeout=300
|
||||
shift
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement
|
||||
// de l'Epita (LRDE).
|
||||
// Copyright (C) 2013, 2014, 2015 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
|
|
@ -86,15 +86,8 @@ with more states.") },
|
|||
{ DOC("simul", "Set to 0 to disable simulation-based reductions. \
|
||||
Set to 1 to use only direct simulation. Set to 2 to use only reverse \
|
||||
simulation. Set to 3 to iterate both direct and reverse simulations. \
|
||||
Set to 4 to apply only \"don't care\" direct simulation. Set to 5 to \
|
||||
iterate \"don't care\" direct simulation and reverse simulation. The \
|
||||
default is 3, except when option --low is specified, in which case the \
|
||||
default is 1.") },
|
||||
{ DOC("simul-limit", "Can be set to a positive integer to cap the \
|
||||
number of \"don't care\" transitions considered by the \
|
||||
\"don't care\"-simulation algorithm. A negative value (the default) \
|
||||
does not enforce any limit. Note that if there are N \"don't care\" \
|
||||
transitions, the algorithm may potentially test 2^N configurations.") },
|
||||
The default is 3, except when option --low is specified, in which case \
|
||||
the default is 1.") },
|
||||
{ DOC("ba-simul", "Set to 0 to disable simulation-based reductions \
|
||||
on the Büchi automaton (i.e., after degeneralization has been performed). \
|
||||
Set to 1 to use only direct simulation. Set to 2 to use only reverse \
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
|
||||
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
|
|
@ -48,7 +48,6 @@ namespace spot
|
|||
degen_cache_ = opt->get("degen-lcache", 1);
|
||||
degen_lskip_ = opt->get("degen-lskip", 1);
|
||||
simul_ = opt->get("simul", -1);
|
||||
simul_limit_ = opt->get("simul-limit", -1);
|
||||
scc_filter_ = opt->get("scc-filter", -1);
|
||||
ba_simul_ = opt->get("ba-simul", -1);
|
||||
tba_determinisation_ = opt->get("tba-det", 0);
|
||||
|
|
@ -87,10 +86,6 @@ namespace spot
|
|||
case 3:
|
||||
default:
|
||||
return iterated_simulations(a);
|
||||
case 4:
|
||||
return dont_care_simulation(a, simul_limit_);
|
||||
case 5:
|
||||
return dont_care_iterated_simulations(a, simul_limit_);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
|
||||
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
|
|
@ -117,7 +117,6 @@ namespace spot
|
|||
int degen_cache_;
|
||||
bool degen_lskip_;
|
||||
int simul_;
|
||||
int simul_limit_;
|
||||
int scc_filter_;
|
||||
int ba_simul_;
|
||||
bool tba_determinisation_;
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et Développement
|
||||
// de l'Epita (LRDE).
|
||||
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
|
|
@ -71,18 +71,9 @@
|
|||
// The automaton simulated is recomplemented to come back to its initial
|
||||
// state when the object Simulation is destroyed.
|
||||
//
|
||||
// Obviously these functions are possibly cut into several little one.
|
||||
// Obviously these functions are possibly cut into several little ones.
|
||||
// This is just the general development idea.
|
||||
|
||||
// How to use isop:
|
||||
// I need all variable non_acceptance & non_class.
|
||||
// bdd_support(sig(X)): All var
|
||||
// bdd_support(sig(X)) - allacc - allclassvar
|
||||
|
||||
|
||||
// TODO LIST: Play on the order of the selection in the
|
||||
// dont_care_simulation. The good place to work is in add_to_map_imply.
|
||||
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -102,49 +93,6 @@ namespace spot
|
|||
|
||||
typedef std::map<bdd, unsigned, bdd_less_than> map_bdd_state;
|
||||
|
||||
// Our constraint: (state_src, state_dst) = to_add.
|
||||
// We define the couple of state as the key of the constraint.
|
||||
typedef std::pair<const state*, const state*> constraint_key;
|
||||
|
||||
// But we need a comparator for that key.
|
||||
struct constraint_key_comparator
|
||||
{
|
||||
bool operator()(const constraint_key& l,
|
||||
const constraint_key& r) const
|
||||
{
|
||||
if (l.first->compare(r.first) < 0)
|
||||
return true;
|
||||
else
|
||||
if (l.first->compare(r.first) > 0)
|
||||
return false;
|
||||
|
||||
if (l.second->compare(r.second) < 0)
|
||||
return true;
|
||||
else
|
||||
if (l.second->compare(r.second) > 0)
|
||||
return false;
|
||||
|
||||
return false;
|
||||
}
|
||||
};
|
||||
|
||||
// The full definition of the constraint.
|
||||
typedef std::map<constraint_key, bdd,
|
||||
constraint_key_comparator> map_constraint;
|
||||
|
||||
typedef std::tuple<const state*, const state*, bdd> constraint;
|
||||
|
||||
// Helper to create the map of constraints to give to the
|
||||
// simulation.
|
||||
void add_to_map(const std::list<constraint>& list,
|
||||
map_constraint& feed_me)
|
||||
{
|
||||
for (auto& p: list)
|
||||
feed_me.emplace(std::make_pair(std::get<0>(p),
|
||||
std::get<1>(p)),
|
||||
std::get<2>(p));
|
||||
}
|
||||
|
||||
|
||||
// This class helps to compare two automata in term of
|
||||
// size.
|
||||
|
|
@ -239,12 +187,10 @@ namespace spot
|
|||
return aut->acc().marks(res.begin(), res.end());
|
||||
}
|
||||
|
||||
direct_simulation(const const_tgba_ptr& t,
|
||||
const map_constraint* map_cst = 0)
|
||||
direct_simulation(const const_tgba_ptr& t)
|
||||
: a_(0),
|
||||
po_size_(0),
|
||||
all_class_var_(bddtrue),
|
||||
map_cst_(map_cst),
|
||||
original_(t)
|
||||
{
|
||||
// We need to do a dupexp for being able to run scc_info later.
|
||||
|
|
@ -408,23 +354,7 @@ namespace spot
|
|||
|
||||
for (auto& t: a_->out(src))
|
||||
{
|
||||
bdd acc = bddtrue;
|
||||
|
||||
map_constraint::const_iterator it;
|
||||
// Check if we have a constraint about this edge in the
|
||||
// original automaton.
|
||||
if (map_cst_
|
||||
&& ((it = map_cst_
|
||||
->find(std::make_pair(new_original_[src],
|
||||
new_original_[t.dst])))
|
||||
!= map_cst_->end()))
|
||||
{
|
||||
acc = it->second;
|
||||
}
|
||||
else
|
||||
{
|
||||
acc = mark_to_bdd(t.acc);
|
||||
}
|
||||
bdd acc = mark_to_bdd(t.acc);
|
||||
|
||||
// to_add is a conjunction of the acceptance condition,
|
||||
// the label of the transition and the class of the
|
||||
|
|
@ -792,523 +722,9 @@ namespace spot
|
|||
std::unique_ptr<scc_info> scc_info_;
|
||||
std::vector<const state*> new_original_;
|
||||
|
||||
const map_constraint* map_cst_;
|
||||
|
||||
const_tgba_ptr original_;
|
||||
};
|
||||
|
||||
// For now, we don't try to handle cosimulation.
|
||||
class direct_simulation_dont_care: public direct_simulation<false, false>
|
||||
{
|
||||
typedef std::vector<std::list<constraint> > constraints;
|
||||
typedef std::map<bdd, // Source Class.
|
||||
std::map<bdd, // Destination (implied) Class.
|
||||
std::list<constraint>, // Constraints list.
|
||||
bdd_less_than>,
|
||||
bdd_less_than> constraint_list;
|
||||
typedef std::list<std::pair<bdd, bdd> > list_bdd_bdd;
|
||||
|
||||
|
||||
public:
|
||||
direct_simulation_dont_care(const const_tgba_ptr& t)
|
||||
: direct_simulation<false, false>(t)
|
||||
{
|
||||
// This variable is used in the new signature.
|
||||
on_cycle_ =
|
||||
bdd_ithvar(a_->get_dict()->register_anonymous_variables(1, this));
|
||||
|
||||
// This one is used for the iteration on all the
|
||||
// possibilities. Avoid computing two times "no constraints".
|
||||
empty_seen_ = false;
|
||||
|
||||
|
||||
// If this variable is set to true, we have a number limit of
|
||||
// simulation to run.
|
||||
has_limit_ = false;
|
||||
|
||||
notap = bdd_support(all_proms_) & all_class_var_ & on_cycle_;
|
||||
}
|
||||
|
||||
// This function computes the don't care signature of the state
|
||||
// src. This signature is similar to the classic one, excepts
|
||||
// that if the transition is on a SCC, we add a on_cycle_ on it,
|
||||
// otherwise we add !on_cycle_. This allows us to split the
|
||||
// signature later.
|
||||
bdd dont_care_compute_sig(unsigned src)
|
||||
{
|
||||
bdd res = bddfalse;
|
||||
|
||||
unsigned scc = scc_info_->scc_of(src);
|
||||
if (scc == -1U) // Unreachable
|
||||
return bddfalse;
|
||||
bool sccacc = scc_info_->is_accepting_scc(scc);
|
||||
|
||||
for (auto& t: a_->out(src))
|
||||
{
|
||||
bdd cl = previous_class_[t.dst];
|
||||
bdd acc;
|
||||
|
||||
if (scc != scc_info_->scc_of(t.dst))
|
||||
acc = !on_cycle_;
|
||||
else if (sccacc)
|
||||
acc = on_cycle_ & mark_to_bdd(t.acc);
|
||||
else
|
||||
acc = on_cycle_ & all_proms_;
|
||||
|
||||
bdd to_add = acc & t.cond & relation_[cl];
|
||||
res |= to_add;
|
||||
}
|
||||
|
||||
return res;
|
||||
}
|
||||
|
||||
// We used to have
|
||||
// sig(s1) = (f1 | g1)
|
||||
// sig(s2) = (f2 | g2)
|
||||
// and we say that s2 simulates s1 if sig(s1)=>sig(s2).
|
||||
// This amount to testing whether (f1|g1)=>(f2|g2),
|
||||
// which is equivalent to testing both
|
||||
// f1=>(f2|g2) and g1=>(f2|g2)
|
||||
// separately.
|
||||
//
|
||||
// Now we have a slightly improved version of this rule.
|
||||
// g1 and g2 are not on cycle, so they can make as many
|
||||
// promises as we wish, if that helps. Adding promises
|
||||
// to g2 will not help, but adding promises to g1 can.
|
||||
//
|
||||
// So we test whether
|
||||
// f1=>(f2|g2)
|
||||
// g1=>noprom(f2|g2)
|
||||
// Where noprom(f2|g2) removes all promises from f2|g2.
|
||||
// (g1 do not have promises, and neither do g2).
|
||||
|
||||
bool could_imply_aux(bdd f1, bdd g1, bdd left_class,
|
||||
bdd right, bdd right_class)
|
||||
{
|
||||
bdd f2g2 = bdd_exist(right, on_cycle_);
|
||||
bdd f2g2n = bdd_exist(f2g2, all_proms_);
|
||||
|
||||
bdd both = left_class & right_class;
|
||||
int lc = bdd_var(left_class);
|
||||
f1 = bdd_compose(f1, both, lc);
|
||||
g1 = bdd_compose(g1, both, lc);
|
||||
f2g2 = bdd_compose(f2g2, both, lc);
|
||||
f2g2n = bdd_compose(f2g2n, both, lc);
|
||||
|
||||
return bdd_implies(f1, f2g2) && bdd_implies(g1, f2g2n);
|
||||
}
|
||||
|
||||
bool could_imply(bdd left, bdd left_class,
|
||||
bdd right, bdd right_class)
|
||||
{
|
||||
bdd f1 = bdd_relprod(left, on_cycle_, on_cycle_);
|
||||
bdd g1 = bdd_relprod(left, !on_cycle_, on_cycle_);
|
||||
|
||||
//bdd f1 = bdd_restrict(left, on_cycle_);
|
||||
//bdd g1 = bdd_restrict(left, !on_cycle_);
|
||||
return could_imply_aux(f1, g1, left_class,
|
||||
right, right_class);
|
||||
}
|
||||
|
||||
void dont_care_update_po(const list_bdd_bdd& now_to_next,
|
||||
map_bdd_bdd& relation)
|
||||
{
|
||||
// This loop follows the pattern given by the paper.
|
||||
// foreach class do
|
||||
// | foreach class do
|
||||
// | | update po if needed
|
||||
// | od
|
||||
// od
|
||||
|
||||
for (list_bdd_bdd::const_iterator it1 = now_to_next.begin();
|
||||
it1 != now_to_next.end();
|
||||
++it1)
|
||||
{
|
||||
bdd accu = it1->second;
|
||||
|
||||
bdd f1 = bdd_relprod(it1->first, on_cycle_, on_cycle_);
|
||||
bdd g1 = bdd_relprod(it1->first, !on_cycle_, on_cycle_);
|
||||
|
||||
// bdd f1 = bdd_restrict(it1->first_, on_cycle_);
|
||||
// bdd g1 = bdd_restrict(it1->first_, !on_cycle_);
|
||||
|
||||
for (list_bdd_bdd::const_iterator it2 = now_to_next.begin();
|
||||
it2 != now_to_next.end();
|
||||
++it2)
|
||||
{
|
||||
// Skip the case managed by the initialization of accu.
|
||||
if (it1 == it2)
|
||||
continue;
|
||||
|
||||
if (could_imply_aux(f1, g1, it1->second,
|
||||
it2->first, it2->second))
|
||||
{
|
||||
accu &= it2->second;
|
||||
++po_size_;
|
||||
}
|
||||
}
|
||||
relation[it1->second] = accu;
|
||||
}
|
||||
}
|
||||
|
||||
#define ISOP(bdd) #bdd" - " << bdd_format_isop(a_->get_dict(), bdd)
|
||||
|
||||
inline bool is_out_scc(bdd b)
|
||||
{
|
||||
return bddfalse != bdd_relprod(b, !on_cycle_, on_cycle_);
|
||||
// return bddfalse != bdd_restrict(b, !on_cycle_);
|
||||
}
|
||||
|
||||
// This method solves three kind of problems, where we have two
|
||||
// conjunctions of variable (that corresponds to a particular
|
||||
// transition), and where left could imply right.
|
||||
// Three cases:
|
||||
// - αP₁ ⇒ xβP₁ where x is unknown.
|
||||
// - xβP₁ ⇒ αP₁ where x is unknown.
|
||||
// - xαP₁ ⇒ yβP₁ where x, y are unknown.
|
||||
void create_simple_constraint(bdd left, bdd right,
|
||||
unsigned src_left,
|
||||
unsigned src_right,
|
||||
std::list<constraint>& constraint)
|
||||
{
|
||||
assert(src_left != src_right);
|
||||
// Determine which is the current case.
|
||||
bool out_scc_left = is_out_scc(left);
|
||||
bool out_scc_right = is_out_scc(right);
|
||||
bdd dest_class = bdd_existcomp(left, all_class_var_);
|
||||
assert(revert_relation_.find(dest_class) != revert_relation_.end());
|
||||
unsigned dst_left = revert_relation_[dest_class];
|
||||
dest_class = bdd_existcomp(right, all_class_var_);
|
||||
unsigned dst_right = revert_relation_[dest_class];
|
||||
|
||||
assert(src_left != dst_left || src_right != dst_right);
|
||||
|
||||
left = bdd_exist(left, all_class_var_ & on_cycle_);
|
||||
right = bdd_exist(right, all_class_var_ & on_cycle_);
|
||||
|
||||
if (!out_scc_left && out_scc_right)
|
||||
{
|
||||
bdd b = bdd_exist(right, notap);
|
||||
bdd add = bdd_exist(left & b, bdd_support(b));
|
||||
|
||||
if (add != bddfalse && bdd_exist(add, all_proms_) == bddtrue)
|
||||
{
|
||||
assert(src_right != dst_right);
|
||||
|
||||
constraint.emplace_back(new_original_[src_right],
|
||||
new_original_[dst_right],
|
||||
add);
|
||||
}
|
||||
}
|
||||
else if (out_scc_left && !out_scc_right)
|
||||
{
|
||||
bdd b = bdd_exist(left, notap);
|
||||
bdd add = bdd_exist(right & b, bdd_support(b));
|
||||
|
||||
if (add != bddfalse && bdd_exist(add, all_proms_) == bddtrue)
|
||||
{
|
||||
assert(src_left != dst_left);
|
||||
|
||||
constraint.emplace_back(new_original_[src_left],
|
||||
new_original_[dst_left],
|
||||
add);
|
||||
}
|
||||
}
|
||||
else if (out_scc_left && out_scc_right)
|
||||
{
|
||||
bdd b = bdd_exist(left, notap);
|
||||
bdd add = bdd_exist(right & b, bdd_support(b));
|
||||
|
||||
if (add != bddfalse && bdd_exist(add, all_proms_) == bddtrue)
|
||||
{
|
||||
assert(src_left != dst_left && src_right != dst_right);
|
||||
// FIXME: cas pas compris.
|
||||
constraint.emplace_back(new_original_[src_left],
|
||||
new_original_[dst_left],
|
||||
add);
|
||||
constraint.emplace_back(new_original_[src_right],
|
||||
new_original_[dst_right],
|
||||
add);
|
||||
}
|
||||
|
||||
}
|
||||
else
|
||||
SPOT_UNREACHABLE();
|
||||
}
|
||||
|
||||
|
||||
// This function run over the signatures, and select the
|
||||
// transitions that are out of a SCC and call the function
|
||||
// create_simple_constraint to solve the problem.
|
||||
|
||||
// NOTE: Currently, this may not be the most accurate method,
|
||||
// because we check for equality in the destination part of the
|
||||
// signature. We may just check the destination that can be
|
||||
// implied instead.
|
||||
std::list<constraint> create_new_constraint(unsigned left,
|
||||
unsigned right,
|
||||
vector_state_bdd& state2sig)
|
||||
{
|
||||
bdd pcl = previous_class_[left];
|
||||
bdd pcr = previous_class_[right];
|
||||
|
||||
bdd sigl = state2sig[left];
|
||||
bdd sigr = state2sig[right];
|
||||
|
||||
std::list<constraint> res;
|
||||
|
||||
bdd ex = all_class_var_ & on_cycle_;
|
||||
|
||||
bdd both = pcl & pcr;
|
||||
int lc = bdd_var(pcl);
|
||||
#define DEST(x) bdd_compose(bdd_existcomp(x, ex), both, lc)
|
||||
|
||||
// Key is destination class, value is the signature part that
|
||||
// led to this destination class.
|
||||
map_bdd_bdd sigl_map;
|
||||
{
|
||||
minato_isop isop(sigl & on_cycle_);
|
||||
bdd cond_acc_dest;
|
||||
while ((cond_acc_dest = isop.next()) != bddfalse)
|
||||
sigl_map[DEST(cond_acc_dest)]
|
||||
|= cond_acc_dest;
|
||||
}
|
||||
{
|
||||
minato_isop isop(sigl & !on_cycle_);
|
||||
bdd cond_acc_dest;
|
||||
while ((cond_acc_dest = isop.next()) != bddfalse)
|
||||
sigl_map[DEST(cond_acc_dest)]
|
||||
|= cond_acc_dest;
|
||||
}
|
||||
map_bdd_bdd sigr_map;
|
||||
{
|
||||
minato_isop isop2(sigr & on_cycle_);
|
||||
bdd cond_acc_dest2;
|
||||
while ((cond_acc_dest2 = isop2.next()) != bddfalse)
|
||||
sigr_map[DEST(cond_acc_dest2)]
|
||||
|= cond_acc_dest2;
|
||||
}
|
||||
{
|
||||
minato_isop isop2(sigr & !on_cycle_);
|
||||
bdd cond_acc_dest2;
|
||||
while ((cond_acc_dest2 = isop2.next()) != bddfalse)
|
||||
sigr_map[DEST(cond_acc_dest2)]
|
||||
|= cond_acc_dest2;
|
||||
}
|
||||
|
||||
// Iterate over the transitions of both states.
|
||||
for (auto lp: sigl_map)
|
||||
for (auto rp: sigr_map)
|
||||
// And create constraints if any of the transitions
|
||||
// is out of the SCC and the left could imply the right.
|
||||
if ((is_out_scc(lp.second) || is_out_scc(rp.second))
|
||||
&& (bdd_exist(lp.first, on_cycle_) ==
|
||||
bdd_exist(rp.first, on_cycle_)))
|
||||
create_simple_constraint(lp.second, rp.second,
|
||||
left, right, res);
|
||||
return res;
|
||||
}
|
||||
|
||||
tgba_digraph_ptr run()
|
||||
{
|
||||
// Iterate the simulation until the end. We just don't return
|
||||
// an automaton. This allows us to get all the information
|
||||
// about the states and their signature.
|
||||
main_loop();
|
||||
|
||||
// Compute the don't care signatures,
|
||||
map_bdd_lstate dont_care_bdd_lstate;
|
||||
// Useful to keep track of who is who.
|
||||
vector_state_bdd dont_care_state2sig(size_a_);
|
||||
vector_state_bdd state2sig(size_a_);
|
||||
|
||||
list_bdd_bdd dont_care_now_to_now;
|
||||
map_bdd_state class2state;
|
||||
list_bdd_bdd now_to_now;
|
||||
bdd_lstate_.clear();
|
||||
|
||||
// Compute the don't care signature for all the states.
|
||||
for (unsigned s = 0; s < size_a_; ++s)
|
||||
{
|
||||
bdd clas = previous_class_[s];
|
||||
bdd sig = dont_care_compute_sig(s);
|
||||
dont_care_bdd_lstate[sig].push_back(s);
|
||||
dont_care_state2sig[s] = sig;
|
||||
dont_care_now_to_now.emplace_back(sig, clas);
|
||||
class2state[clas] = s;
|
||||
|
||||
sig = compute_sig(s);
|
||||
bdd_lstate_[sig].push_back(s);
|
||||
state2sig[s] = sig;
|
||||
now_to_now.push_back(std::make_pair(sig, clas));
|
||||
}
|
||||
|
||||
map_bdd_bdd dont_care_relation;
|
||||
map_bdd_bdd relation;
|
||||
update_po(now_to_now, relation);
|
||||
dont_care_update_po(dont_care_now_to_now, dont_care_relation);
|
||||
|
||||
constraint_list cc;
|
||||
|
||||
for (auto p: relation)
|
||||
revert_relation_[p.second] = class2state[p.first];
|
||||
|
||||
int number_constraints = 0;
|
||||
relation_ = relation;
|
||||
|
||||
|
||||
// make the diff between the two tables: imply and
|
||||
// could_imply.
|
||||
for (unsigned s = 0; s < size_a_; ++s)
|
||||
{
|
||||
bdd clas = previous_class_[s];
|
||||
assert(relation.find(clas) != relation.end());
|
||||
assert(dont_care_relation.find(clas) != dont_care_relation.end());
|
||||
|
||||
bdd care_rel = relation[clas];
|
||||
bdd dont_care_rel = dont_care_relation[clas];
|
||||
|
||||
if (care_rel == dont_care_rel)
|
||||
continue;
|
||||
|
||||
// If they are different we necessarily have
|
||||
// dont_care_rel == care_rel & diff
|
||||
bdd diff = bdd_exist(dont_care_rel, care_rel);
|
||||
assert(dont_care_rel == (care_rel & diff));
|
||||
assert(diff != bddtrue);
|
||||
|
||||
do
|
||||
{
|
||||
bdd cur_diff = bdd_ithvar(bdd_var(diff));
|
||||
cc[clas][cur_diff]
|
||||
= create_new_constraint(s,
|
||||
class2state[cur_diff],
|
||||
dont_care_state2sig);
|
||||
++number_constraints;
|
||||
diff = bdd_high(diff);
|
||||
}
|
||||
while (diff != bddtrue);
|
||||
}
|
||||
|
||||
|
||||
|
||||
#ifndef NDEBUG
|
||||
for (auto& i: class2state)
|
||||
assert(previous_class_[i.second] == i.first);
|
||||
#endif
|
||||
|
||||
tgba_digraph_ptr min = nullptr;
|
||||
|
||||
map_constraint cstr;
|
||||
|
||||
if (has_limit_)
|
||||
rec(cc, cstr, min, limit_);
|
||||
else
|
||||
rec(cc, cstr, min);
|
||||
|
||||
return min;
|
||||
}
|
||||
|
||||
#define ERASE(inner_map, bigger_map, it) \
|
||||
inner_map.erase(it); \
|
||||
if (inner_map.empty()) \
|
||||
bigger_map.erase(bigger_map.begin())
|
||||
|
||||
// Add and erase.
|
||||
void add_to_map_imply(constraint_list& constraints,
|
||||
map_constraint& cstr)
|
||||
{
|
||||
constraint_list::iterator it = constraints.begin();
|
||||
std::map<bdd,
|
||||
std::list<constraint>,
|
||||
bdd_less_than>::iterator it2 = it->second.begin();
|
||||
|
||||
add_to_map(it2->second, cstr);
|
||||
|
||||
bdd implied_list = relation_[it2->first]; // it2->first:
|
||||
// destination class.
|
||||
|
||||
ERASE(it->second, constraints, it2);
|
||||
if (constraints.empty())
|
||||
return;
|
||||
it = constraints.begin();
|
||||
// At worst, implied_list is equal to it2->first.
|
||||
while (implied_list != bddtrue)
|
||||
{
|
||||
bdd cur_implied = bdd_ithvar(bdd_var(implied_list));
|
||||
|
||||
std::map<bdd,
|
||||
std::list<constraint>,
|
||||
bdd_less_than>::iterator tmp
|
||||
= it->second.find(cur_implied);
|
||||
if (tmp != it->second.end())
|
||||
{
|
||||
add_to_map(tmp->second, cstr);
|
||||
ERASE(it->second, constraints, tmp);
|
||||
if (constraints.empty())
|
||||
return;
|
||||
}
|
||||
|
||||
implied_list = bdd_high(implied_list);
|
||||
}
|
||||
}
|
||||
|
||||
// Compute recursively all the combinations.
|
||||
void rec(constraint_list constraints,
|
||||
map_constraint cstr,
|
||||
tgba_digraph_ptr& min,
|
||||
int max_depth = std::numeric_limits<int>::max())
|
||||
{
|
||||
assert(max_depth > 0);
|
||||
while (!constraints.empty())
|
||||
{
|
||||
if (!--max_depth)
|
||||
break;
|
||||
add_to_map_imply(constraints, cstr);
|
||||
rec(constraints, cstr, min, max_depth);
|
||||
}
|
||||
|
||||
if (empty_seen_ && cstr.empty())
|
||||
return;
|
||||
else if (cstr.empty())
|
||||
empty_seen_ = true;
|
||||
|
||||
direct_simulation<false, false> dir_sim(original_, &cstr);
|
||||
tgba_digraph_ptr tmp = dir_sim.run();
|
||||
automaton_size cur_size(tmp);
|
||||
if (!min || min_size_ > cur_size)
|
||||
{
|
||||
min = tmp;
|
||||
min_size_ = cur_size;
|
||||
}
|
||||
}
|
||||
|
||||
void set_limit(int n)
|
||||
{
|
||||
has_limit_ = true;
|
||||
limit_ = n;
|
||||
}
|
||||
|
||||
private:
|
||||
// This bdd is used to differentiate parts of the signature that
|
||||
// are in a SCC and those that are not.
|
||||
bdd on_cycle_;
|
||||
|
||||
map_bdd_bdd dont_care_relation_;
|
||||
|
||||
map_bdd_state revert_relation_;
|
||||
|
||||
automaton_size min_size_;
|
||||
|
||||
bool empty_seen_;
|
||||
|
||||
bool has_limit_;
|
||||
int limit_;
|
||||
|
||||
bdd notap;
|
||||
};
|
||||
|
||||
|
||||
} // End namespace anonymous.
|
||||
|
||||
|
||||
|
|
@ -1383,34 +799,4 @@ namespace spot
|
|||
return iterated_simulations_<true>(t);
|
||||
}
|
||||
|
||||
tgba_digraph_ptr
|
||||
dont_care_simulation(const const_tgba_ptr& t, int limit)
|
||||
{
|
||||
direct_simulation<false, false> sim(t);
|
||||
direct_simulation_dont_care s(sim.run());
|
||||
if (limit > 0)
|
||||
s.set_limit(limit);
|
||||
return s.run();
|
||||
}
|
||||
|
||||
|
||||
tgba_digraph_ptr
|
||||
dont_care_iterated_simulations(const const_tgba_ptr& t, int limit)
|
||||
{
|
||||
tgba_digraph_ptr res = 0;
|
||||
automaton_size prev;
|
||||
automaton_size next;
|
||||
|
||||
do
|
||||
{
|
||||
prev = next;
|
||||
res = cosimulation(dont_care_simulation(res ? res : t, limit));
|
||||
res = scc_filter(res, true);
|
||||
next.set_size(res);
|
||||
}
|
||||
while (prev != next);
|
||||
|
||||
return res;
|
||||
}
|
||||
|
||||
} // End namespace spot.
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2012, 2013, 2014 Laboratoire de Recherche et
|
||||
// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
|
||||
// Développement de l'Epita (LRDE).
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
|
|
@ -79,8 +79,8 @@ namespace spot
|
|||
/// one state are included in the prefixes leading to one, the former
|
||||
/// state can be merged into the latter.
|
||||
///
|
||||
/// Reverse simulation is discussed in the following paper, bu
|
||||
/// following paper, but generalized to handle TGBA directly.
|
||||
/// Reverse simulation is discussed in the following paper,
|
||||
/// but generalized to handle TGBA directly.
|
||||
/** \verbatim
|
||||
@InProceedings{ somenzi.00.cav,
|
||||
author = {Fabio Somenzi and Roderick Bloem},
|
||||
|
|
@ -144,19 +144,6 @@ namespace spot
|
|||
iterated_simulations_sba(const const_tgba_ptr& automaton);
|
||||
/// @}
|
||||
|
||||
|
||||
|
||||
// FIXME: Remove: dont_care_*_simulation is broken since the move to
|
||||
// bitset acceptance, has never been really used, and really useful
|
||||
// (nor really well tested and understood), so we should remove it.
|
||||
SPOT_API tgba_digraph_ptr
|
||||
dont_care_simulation(const const_tgba_ptr& t, int limit = -1);
|
||||
|
||||
SPOT_API tgba_digraph_ptr
|
||||
dont_care_iterated_simulations(const const_tgba_ptr& t, int limit = -1);
|
||||
|
||||
|
||||
/// @}
|
||||
} // End namespace spot.
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
## -*- coding: utf-8 -*-
|
||||
## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
|
||||
## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de
|
||||
## Recherche et Développement de l'Epita (LRDE).
|
||||
## Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
|
||||
## Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||
|
|
@ -138,8 +138,6 @@ TESTS = \
|
|||
randpsl.test \
|
||||
cycles.test
|
||||
|
||||
XFAIL_TESTS = sim.test
|
||||
|
||||
EXTRA_DIST = $(TESTS)
|
||||
|
||||
distclean-local:
|
||||
|
|
|
|||
|
|
@ -210,8 +210,6 @@ syntax(char* prog)
|
|||
<< std::endl
|
||||
<< " -RIS iterate both direct and reverse simulations"
|
||||
<< std::endl
|
||||
<< " -RDCS reduce the automaton with direct simulation"
|
||||
<< std::endl
|
||||
<< " -Rm attempt to WDBA-minimize the automaton" << std::endl
|
||||
<< std::endl
|
||||
<< " -RM attempt to WDBA-minimize the automaton unless the "
|
||||
|
|
@ -390,9 +388,6 @@ checked_main(int argc, char** argv)
|
|||
bool reduction_dir_sim = false;
|
||||
bool reduction_rev_sim = false;
|
||||
bool reduction_iterated_sim = false;
|
||||
bool reduction_dont_care_sim = false;
|
||||
int limit_dont_care_sim = 0;
|
||||
bool reduction_iterated_dont_care_sim = false;
|
||||
bool opt_bisim_ta = false;
|
||||
bool ta_opt = false;
|
||||
bool tgta_opt = false;
|
||||
|
|
@ -719,18 +714,6 @@ checked_main(int argc, char** argv)
|
|||
{
|
||||
reduction_iterated_sim = true;
|
||||
}
|
||||
else if (!strncmp(argv[formula_index], "-RDCS", 5))
|
||||
{
|
||||
reduction_dont_care_sim = true;
|
||||
if (argv[formula_index][5] == '=')
|
||||
limit_dont_care_sim = to_int(argv[formula_index] + 6);
|
||||
}
|
||||
else if (!strncmp(argv[formula_index], "-RDCIS", 6))
|
||||
{
|
||||
reduction_iterated_dont_care_sim = true;
|
||||
if (argv[formula_index][6] == '=')
|
||||
limit_dont_care_sim = to_int(argv[formula_index] + 7);
|
||||
}
|
||||
else if (!strcmp(argv[formula_index], "-rL"))
|
||||
{
|
||||
simpltl = true;
|
||||
|
|
@ -1218,8 +1201,6 @@ checked_main(int argc, char** argv)
|
|||
// When the minimization succeed, simulation is useless.
|
||||
reduction_dir_sim = false;
|
||||
reduction_rev_sim = false;
|
||||
reduction_iterated_dont_care_sim = false;
|
||||
reduction_dont_care_sim = false;
|
||||
reduction_iterated_sim = false;
|
||||
assume_sba = true;
|
||||
}
|
||||
|
|
@ -1242,14 +1223,6 @@ checked_main(int argc, char** argv)
|
|||
}
|
||||
|
||||
|
||||
if (reduction_iterated_dont_care_sim)
|
||||
{
|
||||
tm.start("don't care iterated simulation");
|
||||
a = spot::dont_care_iterated_simulations(a, limit_dont_care_sim);
|
||||
tm.stop("don't care iterated simulation");
|
||||
assume_sba = false;
|
||||
}
|
||||
|
||||
if (reduction_iterated_sim)
|
||||
{
|
||||
tm.start("Reduction w/ iterated simulations");
|
||||
|
|
@ -1265,23 +1238,6 @@ checked_main(int argc, char** argv)
|
|||
tm.stop("SCC-filter post-sim");
|
||||
}
|
||||
|
||||
if (reduction_dont_care_sim)
|
||||
{
|
||||
tm.start("don't care simulation");
|
||||
a = spot::dont_care_simulation(a, limit_dont_care_sim);
|
||||
tm.stop("don't care simulation");
|
||||
|
||||
if (scc_filter)
|
||||
{
|
||||
auto aa = std::static_pointer_cast<const spot::tgba_digraph>(a);
|
||||
assert(aa);
|
||||
tm.start("SCC-filter on don't care");
|
||||
a = spot::scc_filter(aa, true);
|
||||
tm.stop("SCC-filter on don't care");
|
||||
}
|
||||
assume_sba = false;
|
||||
}
|
||||
|
||||
unsigned int n_acc = a->acc().num_sets();
|
||||
if (echeck_inst
|
||||
&& degeneralize_opt == NoDegen
|
||||
|
|
|
|||
|
|
@ -1,83 +0,0 @@
|
|||
#! /bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 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/>.
|
||||
|
||||
. ./defs
|
||||
set -e
|
||||
|
||||
cat >in.tgba <<EOF
|
||||
acc = "1";
|
||||
"i", "x", "b",;
|
||||
"i", "d2", "b",;
|
||||
"x", "ed", "a", "1";
|
||||
"ed", "ed", "a & b", "1";
|
||||
"d2", "d", "a",;
|
||||
"d", "d", "a", "1";
|
||||
EOF
|
||||
|
||||
run 0 ../ltl2tgba -X -RDCS -b in.tgba > out.tgba
|
||||
|
||||
cat >expected.tgba <<EOF
|
||||
acc = "0";
|
||||
"0", "1", "b",;
|
||||
"1", "1", "a", "0";
|
||||
EOF
|
||||
|
||||
diff out.tgba expected.tgba
|
||||
|
||||
run 0 ../ltl2tgba -RDCIS -b XXXXGFa > out.tgba
|
||||
|
||||
cat >expected.tgba <<EOF
|
||||
acc = "0";
|
||||
"0", "0", "a", "0";
|
||||
"0", "0", "!a",;
|
||||
EOF
|
||||
|
||||
diff out.tgba expected.tgba
|
||||
|
||||
run 0 ../ltl2tgba -RDCIS -kt 'Fp U Gq' > out
|
||||
cat >expected <<EOF
|
||||
sub trans.: 12
|
||||
transitions: 6
|
||||
states: 3
|
||||
nondeterministic states: 1
|
||||
EOF
|
||||
|
||||
diff out expected
|
||||
|
||||
|
||||
run 0 ../ltl2tgba -R3 -x -RDCS -kt 'F(a & GFa)' > out
|
||||
run 0 ../ltl2tgba -R3f -x -RDCS -kt 'F(a & GFa)' > out2
|
||||
diff out out2
|
||||
|
||||
|
||||
f='FG((Fp0 & (!p0 R (F!p1 U !p1))) | (G!p0 & (p0 U (Gp1 R p1))))'
|
||||
run 0 ../ltl2tgba -R3f -x -RDS -kt "$f" | grep -v sub > out
|
||||
run 0 ../ltl2tgba -R3f -x -RDCS -kt "$f" | grep -v sub > out2
|
||||
diff out out2
|
||||
|
||||
run 0 ../ltl2tgba -R3f -x -RDCS -kt "$f" > out2
|
||||
cat >expected <<EOF
|
||||
sub trans.: 13
|
||||
transitions: 8
|
||||
states: 3
|
||||
nondeterministic states: 1
|
||||
EOF
|
||||
|
||||
diff out2 expected
|
||||
|
|
@ -1,7 +1,7 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2009, 2010, 2011, 2012, 2014 Laboratoire de Recherche
|
||||
# et Développement de l'Epita (LRDE).
|
||||
# Copyright (C) 2009, 2010, 2011, 2012, 2014, 2015 Laboratoire de
|
||||
# Recherche et Développement de l'Epita (LRDE).
|
||||
# Copyright (C) 2003, 2004, 2005, 2006, 2007 Laboratoire
|
||||
# d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
|
||||
# Coopératifs (SRC), Université Pierre et Marie Curie.
|
||||
|
|
@ -134,23 +134,6 @@ Algorithm
|
|||
Enabled = yes
|
||||
}
|
||||
|
||||
Algorithm
|
||||
{
|
||||
Name = "Spot (Couvreur -- FM), don't care simulation"
|
||||
Path = "${LBTT_TRANSLATE}"
|
||||
Parameters = "--spot '../ltl2tgba -F -f -t -RDCS -r4 -R3f'"
|
||||
Enabled = no
|
||||
}
|
||||
|
||||
Algorithm
|
||||
{
|
||||
Name = "Spot (Couvreur -- FM), don't care iterated simulation"
|
||||
Path = "${LBTT_TRANSLATE}"
|
||||
Parameters = "--spot '../ltl2tgba -F -f -t -RDCIS -r4 -R3f'"
|
||||
Enabled = no
|
||||
}
|
||||
|
||||
|
||||
Algorithm
|
||||
{
|
||||
Name = "Spot (Couvreur -- FM), cosimulated"
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue