Commit 08c77318 authored by Thomas Badie's avatar Thomas Badie Committed by Alexandre Duret-Lutz
Browse files

Add the "don't care" simulation

* src/tgba/bddprint.cc, src/tgba/bddprint.hh: Add bdd_print_isop
that prints the bdd into a Irreductible Sum Of Product.
* src/tgbaalgos/dupexp.cc, src/tgbaalgos/dupexp.hh: Add a way to
know which states (in the input) is which (in the result).
* src/tgbaalgos/simulation.cc, src/tgbaalgos/simulation.hh: Add
the Don't Care Simulation and the Don't Care Iterated Simulation.
* src/tgbatest/ltl2tgba.cc, src/tgbatest/spotlbtt.test,
src/tgbatest/Makefile.am, src/tgbatest/sim.test: Test them.
* bench/ltl2tgba/algorithms, bench/ltl2tgba/README,
bench/ltl2tgba/algorithms: Add a way to bench the don't care
simulation.
parent 5796114e
......@@ -38,6 +38,13 @@ this benchmark.
The timeout value, common to the three benchmarks, is also set here.
You can also benchmark some simulations algorithms by setting the
variable "BENCH_SIMULATION". For example by running:
BENCH_SIMULATION=t make -j3 run
You run the simulation benchmark on the three kind of formulae.
* small
* big
* known
......
......@@ -4,18 +4,35 @@
# the tools starts with "-".
set dummy
if test -n "$BENCH_SIMULATION"; then
translator="../../src/tgbatest/ltl2tgba"
set "$@" "$translator -R3 -Rm -r7 -t %s >%T" \
"$translator -t -RDS -Rm -r7 -R3 %s >%T" \
"$translator -t -RDCS -r7 -Rm -R3 %s >%T" \
"$translator -t -RRS -r7 -R3 -Rm %s >%T" \
"$translator -t -RIS -r7 -R3 -Rm %s >%T" \
"$translator -t -RDCIS -r7 -Rm -R3 %s >%T" \
"$translator -t -R3 -Rm -r7 -DS %s >%T" \
"$translator -t -r7 -R3 -Rm -RDS -DS %s >%T" \
"$translator -t -RDCS -r7 -Rm -R3 -DS %s >%T" \
"$translator -t -RRS -r7 -R3 -Rm -DS %s >%T" \
"$translator -t -RIS -r7 -R3 -Rm -DS %s >%T" \
"$translator -t -RDCIS -r7 -R3 -Rm -DS %s >%T"
else
# Add third-party tools if they are available
test -n "$SPIN" && set "$@" "$SPIN -f %s >%N"
test -n "$LTL2BA" && set "$@" "$LTL2BA -f %s >%N"
test -n "$LTL3BA" && set "$@" "$LTL3BA -f %s >%N" \
"$LTL3BA -M -f %s >%N" \
"$LTL3BA -S -f %s >%N" \
"$LTL3BA -S -M -f %s >%N"
test -n "$SPIN" && set "$@" "$SPIN -f %s >%N"
test -n "$LTL2BA" && set "$@" "$LTL2BA -f %s >%N"
test -n "$LTL3BA" && set "$@" "$LTL3BA -f %s >%N" \
"$LTL3BA -M -f %s >%N" \
"$LTL3BA -S -f %s >%N" \
"$LTL3BA -S -M -f %s >%N"
# Use -s to output a neverclaim, like the other tools.
set "$@" "$LTL2TGBA --det -s %s >%N" \
"$LTL2TGBA --small -s %s >%N"
set "$@" "$LTL2TGBA --det -s %s >%N" \
"$LTL2TGBA --small -s %s >%N"
fi;
# If you want to add your own tool, you can add it here.
# See 'man ltlcross' for the list of %-escape you may use
# to specify input formula and output automaton.
......
......@@ -25,6 +25,7 @@
#include "bddprint.hh"
#include "ltlvisit/tostring.hh"
#include "formula2bdd.hh"
#include "misc/minato.hh"
namespace spot
{
......@@ -242,4 +243,28 @@ namespace spot
{
utf8 = true;
}
std::ostream&
bdd_print_isop(std::ostream& os, const bdd_dict* d, bdd b)
{
dict = d;
want_acc = true;
minato_isop isop(b);
bdd p;
while ((p = isop.next()) != bddfalse)
{
os << bdd_format_set(d, p);
}
return os;
}
std::string
bdd_format_isop(const bdd_dict* d, bdd b)
{
std::ostringstream os;
bdd_print_isop(os, d, b);
return os.str();
}
}
......@@ -113,6 +113,23 @@ namespace spot
/// \brief Enable UTF-8 output for bdd printers.
void enable_utf8();
/// \brief Format a BDD as an irredundant sum of product.
/// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print.
/// \return The BDD formated as a string.
std::string
bdd_format_isop(const bdd_dict* d, bdd b);
/// \brief Print a BDD as an irredundant sum of product.
/// \param os The output stream.
/// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print.
std::ostream&
bdd_print_isop(std::ostream& os, const bdd_dict* d, bdd b);
}
#endif // SPOT_TGBA_BDDPRINT_HH
......@@ -56,10 +56,31 @@ namespace spot
out_->add_acceptance_conditions(t, si->current_acceptance_conditions());
}
private:
protected:
tgba_explicit_number* out_;
};
template <typename T>
class dupexp_iter_save: public dupexp_iter<T>
{
public:
dupexp_iter_save(const tgba* a,
std::map<const state*,
const state*,
state_ptr_less_than>& relation)
: dupexp_iter<T>(a),
relation_(relation)
{
}
void process_state(const state* s, int n, tgba_succ_iterator*)
{
relation_[this->out_->add_state(n)] = const_cast<state*>(s);
}
std::map<const state*, const state*, state_ptr_less_than>& relation_;
};
} // anonymous
tgba_explicit_number*
......@@ -78,4 +99,25 @@ namespace spot
return di.result();
}
tgba_explicit_number*
tgba_dupexp_bfs(const tgba* aut,
std::map<const state*,
const state*, state_ptr_less_than>& rel)
{
dupexp_iter_save<tgba_reachable_iterator_breadth_first> di(aut,
rel);
di.run();
return di.result();
}
tgba_explicit_number*
tgba_dupexp_dfs(const tgba* aut,
std::map<const state*,
const state*, state_ptr_less_than>& rel)
{
dupexp_iter_save<tgba_reachable_iterator_depth_first> di(aut,
rel);
di.run();
return di.result();
}
}
......@@ -35,6 +35,21 @@ namespace spot
/// numbering states in depth first order as they are processed.
/// \ingroup tgba_misc
tgba_explicit_number* tgba_dupexp_dfs(const tgba* aut);
/// \brief Build an explicit automata from all states of \a aut,
/// numbering states in bread first order as they are processed.
/// \ingroup tgba_misc
tgba_explicit_number*
tgba_dupexp_bfs(const tgba* aut,
std::map<const state*, const state*,
state_ptr_less_than>& relation);
/// \brief Build an explicit automata from all states of \a aut,
/// numbering states in depth first order as they are processed.
/// \ingroup tgba_misc
tgba_explicit_number*
tgba_dupexp_dfs(const tgba* aut,
std::map<const state*, const state*,
state_ptr_less_than>& relation);
}
#endif // SPOT_TGBAALGOS_DUPEXP_HH
// -*- coding: utf-8 -*-
// Copyright (C) 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2012, 2013 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
//
// This file is part of Spot, a model checking library.
//
......@@ -20,6 +20,8 @@
#include <queue>
#include <map>
#include <utility>
#include <cmath>
#include <limits>
#include "tgba/tgbaexplicit.hh"
#include "simulation.hh"
#include "misc/acccompl.hh"
......@@ -28,6 +30,9 @@
#include "tgba/bddprint.hh"
#include "tgbaalgos/reachiter.hh"
#include "tgbaalgos/sccfilter.hh"
#include "tgbaalgos/scc.hh"
#include "tgbaalgos/dupexp.hh"
#include "tgbaalgos/dotty.hh"
// The way we developed this algorithm is the following: We take an
// automaton, and reverse all these acceptance conditions. We reverse
......@@ -85,6 +90,10 @@
// same thing to rebuild the automaton.
// In the signature,
// 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
{
namespace
......@@ -100,10 +109,66 @@ namespace spot
state_ptr_hash,
state_ptr_equal> map_state_unsigned;
typedef std::map<const state*, const state*,
state_ptr_less_than> map_state_state;
// Get the list of state for each class.
typedef std::map<bdd, std::list<const state*>,
bdd_less_than> map_bdd_lstate;
typedef std::map<bdd, const state*,
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::pair<constraint_key, 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 (std::list<constraint>::const_iterator it = list.begin();
it != list.end();
++it)
{
if (feed_me.find(it->first) == feed_me.end())
feed_me[it->first] = it->second;
}
}
// This class helps to compare two automata in term of
// size.
struct automaton_size
{
automaton_size()
......@@ -117,21 +182,116 @@ namespace spot
return transitions != r.transitions || states != r.states;
}
inline bool operator<(const automaton_size& r)
{
if (states < r.states)
return true;
if (states > r.states)
return false;
if (transitions < r.transitions)
return true;
if (transitions > r.transitions)
return false;
return false;
}
inline bool operator>(const automaton_size& r)
{
if (states < r.states)
return false;
if (states > r.states)
return true;
if (transitions < r.transitions)
return false;
if (transitions > r.transitions)
return true;
return false;
}
int transitions;
int states;
};
// This class takes an automaton and creates a copy with all
// acceptance conditions complemented.
template <bool Cosimulation>
// This class takes an automaton, and return a (maybe new)
// automaton. If Cosimulation is equal to true, we create a new
// automaton. Otherwise, we create a new one. The returned
// automaton is similar to the old one, except that the acceptance
// condition on the transitions are complemented.
// There is a specialization below.
template <bool Cosimulation, bool ReverseComplement = false>
class acc_compl_automaton:
public tgba_reachable_iterator_depth_first
{
public:
acc_compl_automaton(const tgba* a)
: tgba_reachable_iterator_depth_first(a),
size(0),
ea_(down_cast<tgba_explicit_number*>(const_cast<tgba*>(a))),
ac_(ea_->all_acceptance_conditions(),
ea_->neg_acceptance_conditions())
{
assert(ea_);
out_ = ea_;
}
void process_link(const state*, int,
const state*, int,
const tgba_succ_iterator* si)
{
bdd acc = ReverseComplement
? ac_.reverse_complement(si->current_acceptance_conditions())
: ac_.complement(si->current_acceptance_conditions());
const tgba_explicit_succ_iterator<state_explicit_number>* tmpit =
down_cast<const tgba_explicit_succ_iterator
<state_explicit_number>*>(si);
typename tgba_explicit_number::transition* t =
ea_->get_transition(tmpit);
t->acceptance_conditions = acc;
}
void process_state(const state* s, int, tgba_succ_iterator*)
{
++size;
previous_class_[s] = bddfalse;
old_name_[s] = s;
order_.push_back(s);
}
~acc_compl_automaton()
{
}
public:
size_t size;
tgba_explicit_number* out_;
map_state_bdd previous_class_;
std::list<const state*> order_;
map_state_state old_name_;
private:
tgba_explicit_number* ea_;
acc_compl ac_;
};
// The specialization for Cosimulation equals to true: We need to
// copy.
template <>
class acc_compl_automaton<true>:
public tgba_reachable_iterator_depth_first
{
public:
acc_compl_automaton(const tgba* a)
: tgba_reachable_iterator_depth_first(a),
size(0),
out_(new tgba_explicit_number(a->get_dict())),
out_(new tgba_explicit_number(a->get_dict())),
ea_(a),
ac_(ea_->all_acceptance_conditions(),
ea_->neg_acceptance_conditions()),
......@@ -147,10 +307,11 @@ namespace spot
map_state_unsigned::const_iterator i = state2int.find(s);
if (i == state2int.end())
{
i = state2int.insert(std::make_pair(s, ++current_max)).first;
const state* to_add = out_->add_state(current_max);
previous_class_[to_add] = bddfalse;
order_.push_back(to_add);
i = state2int.insert(std::make_pair(s, ++current_max)).first;
state* in_new_aut = out_->add_state(current_max);
previous_class_[in_new_aut] = bddfalse;
old_name_[in_new_aut] = s;
order_.push_back(in_new_aut);
}
return i->second;
}
......@@ -161,21 +322,20 @@ namespace spot
int,
const tgba_succ_iterator* si)
{
int src = get_state(in_s);
int dst = get_state(out_s);
unsigned src = get_state(in_s);
unsigned dst = get_state(out_s);
// In the case of the cosimulation, we want to have all the
// ingoing transition, and to keep the rest of the code
// similar, we just create equivalent transition in the other
// direction. Since we do not have to run through the
// automaton to get the signature, this is correct.
if (Cosimulation)
std::swap(src, dst);
std::swap(src, dst);
bdd acc = ac_.complement(si->current_acceptance_conditions());
tgba_explicit_number::transition* t
= out_->create_transition(src, dst);
= out_->create_transition(src, dst);
out_->add_acceptance_conditions(t, acc);
out_->add_conditions(t, si->current_condition());
}
......@@ -187,6 +347,7 @@ namespace spot
~acc_compl_automaton()
{
// Because we don't know what get_init_state returns...
init_->destroy();
}
......@@ -195,33 +356,54 @@ namespace spot
tgba_explicit_number* out_;
map_state_bdd previous_class_;
std::list<const state*> order_;
map_state_state old_name_;
private:
const state* init_;
const tgba* ea_;
acc_compl ac_;
map_state_unsigned state2int;
unsigned current_max;
state* init_;
};
// The direct_simulation. If Cosimulation is true, we are doing a
// cosimulation. Seems obvious, but it's better to be clear.
template <bool Cosimulation>
class direct_simulation
{
protected:
// Shortcut used in update_po and go_to_next_it.
typedef std::map<bdd, bdd, bdd_less_than> map_bdd_bdd;
public:
direct_simulation(const tgba* t)
: a_(0),
po_size_(0),
all_class_var_(bddtrue)
direct_simulation(const tgba* t, const map_constraint* map_cst = 0)
: a_(0),
po_size_(0),
all_class_var_(bddtrue),
map_cst_(map_cst),
original_(t),
dont_delete_old_(false)
{
acc_compl_automaton<Cosimulation>
acc_compl(t);
// We need to do a dupexp for being able to run scc_map later.
// new_original_ is the map that contains the relation between
// the names (addresses) of the states in the automaton
// returned by dupexp, and in automaton given in argument to
// the constructor.
a_ = tgba_dupexp_dfs(t, new_original_);
scc_map_ = new scc_map(a_);
scc_map_->build_map();
old_a_ = a_;
acc_compl_automaton<Cosimulation> acc_compl(a_);
// We'll start our work by replacing all the acceptance
// conditions by their complement.
acc_compl.run();
// Contains the relation between the names of the states in
// the automaton returned by the complementation and the one
// get in argument to the constructor of acc_compl.
old_name_ = acc_compl.old_name_;
a_ = acc_compl.out_;
initial_state = a_->get_init_state();
......@@ -237,6 +419,8 @@ namespace spot
unsigned set_num = a_->get_dict()
->register_anonymous_variables(size_a_ + 1, a_);
all_proms_ = bdd_support(a_->all_acceptance_conditions());
bdd_initial = bdd_ithvar(set_num++);
bdd init = bdd_ithvar(set_num++);
......@@ -267,19 +451,25 @@ namespace spot
relation_[init] = init;
order_ = acc_compl.order_;
all_acceptance_conditions_ = a_->all_acceptance_conditions();
}
// Reverse all the acceptance condition at the destruction of
// this object, because it occurs after the return of the
// function simulation.
~direct_simulation()
virtual ~direct_simulation()
{
delete a_;
delete scc_map_;
if (!dont_delete_old_)
delete old_a_;
// Since a_ is a new automaton only if we are doing a
// cosimulation.
if (Cosimulation)
delete a_;
}
// We update the name of the class.
// We update the name of the classes.
void update_previous_class()
{
std::list<bdd>::iterator it_bdd = used_var_.begin();
......@@ -305,13 +495,11 @@ namespace spot
else
previous_class_[*it_s] = *it_bdd;
}
if (it->first != bddfalse)
++it_bdd;
}
}
// The core loop of the algorithm.
tgba* run()
void main_loop()
{
unsigned int nb_partition_before = 0;
unsigned int nb_po_before = po_size_ - 1;
......@@ -328,6 +516,12 @@ namespace spot
}
update_previous_class();
}
// The core loop of the algorithm.
tgba* run()
{
main_loop();
return build_result();
}
......@@ -340,7 +534,23 @@ namespace spot
for (sit->first(); !sit->done(); sit->next())
{
const state* dst = sit->current_state();
bdd acc = sit->current_acceptance_conditions();
bdd acc = bddtrue;
map_constraint::const_iterator it;
// We are using new_original_[old_name_[...]] because we
// give the constraints in the original automaton, so we
// need to use this heavy computation.
if (map_cst_
&& ((it = map_cst_
->find(std::make_pair(new_original_[old_name_[src]],
new_original_[old_name_[dst]])))
!= map_cst_->end()))
{
acc = it->second;
}
else
{
acc = sit->current_acceptance_conditions();
}
// to_add is a conjunction of the acceptance condition,
// the label of the transition and the class of the
......@@ -364,11 +574,6 @@ namespace spot
void update_sig()