* src/misc/optionmap.cc, src/misc/optionmap.hh (option_map::get,
option_map::set): Handle default values. (anonymous::to_int): Do not print anything. * src/tgbaalgos/gv04.cc, src/tgbaalgos/gv04.hh, src/tgbaalgos/tau03.cc, src/tgbaalgos/tau03.hh, src/tgbaalgos/tau03opt.cc, src/tgbaalgos/tau03opt.hh, src/tgbaalgos/ce.cc, src/tgbaalgos/ce.hh: Take an option_map in the constructor. * src/tgbaalgos/gtec.cc, src/tgbaalgos/gtec.hh: Likewise. Handle the "poprem", "group", and "shy" options via the option_map. Supply a couvreur99() wrapper to the shy/non-shy variant. * src/tgbatest/ltl2tgba.cc, src/tgbatest/randtgba.cc, iface/gspn/ssp.cc: Adjust.
This commit is contained in:
Alexandre Duret-Lutz
parent
77888e9293
commit
f3effb9da0
20 changed files with 274 additions and 203 deletions
|
|
@ -129,7 +129,8 @@ namespace spot
|
|||
|
||||
protected:
|
||||
/// React when options are modified.
|
||||
virtual void options_updated(const option_map& old)
|
||||
virtual void
|
||||
options_updated(const option_map& old)
|
||||
{
|
||||
(void)old;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -77,8 +77,8 @@ namespace spot
|
|||
}
|
||||
|
||||
couvreur99_check_result::couvreur99_check_result
|
||||
(const couvreur99_check_status* ecs)
|
||||
: emptiness_check_result(ecs->aut), ecs_(ecs)
|
||||
(const couvreur99_check_status* ecs, option_map o)
|
||||
: emptiness_check_result(ecs->aut, o), ecs_(ecs)
|
||||
{
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -34,7 +34,8 @@ namespace spot
|
|||
public acss_statistics
|
||||
{
|
||||
public:
|
||||
couvreur99_check_result(const couvreur99_check_status* ecs);
|
||||
couvreur99_check_result(const couvreur99_check_status* ecs,
|
||||
option_map o = option_map());
|
||||
|
||||
virtual tgba_run* accepting_run();
|
||||
|
||||
|
|
|
|||
|
|
@ -30,10 +30,11 @@ namespace spot
|
|||
}
|
||||
|
||||
couvreur99_check::couvreur99_check(const tgba* a,
|
||||
bool poprem,
|
||||
option_map o,
|
||||
const numbered_state_heap_factory* nshf)
|
||||
: emptiness_check(a), poprem_(poprem)
|
||||
: emptiness_check(a, o)
|
||||
{
|
||||
poprem_ = o.get("poprem", 1);
|
||||
ecs_ = new couvreur99_check_status(a, nshf);
|
||||
}
|
||||
|
||||
|
|
@ -262,7 +263,7 @@ namespace spot
|
|||
// cycle.
|
||||
ecs_->cycle_seed = spi.first;
|
||||
set_states(ecs_->states());
|
||||
return new couvreur99_check_result(ecs_);
|
||||
return new couvreur99_check_result(ecs_, options());
|
||||
}
|
||||
}
|
||||
// This automaton recognizes no word.
|
||||
|
|
@ -288,12 +289,13 @@ namespace spot
|
|||
//////////////////////////////////////////////////////////////////////
|
||||
|
||||
couvreur99_check_shy::couvreur99_check_shy(const tgba* a,
|
||||
bool poprem,
|
||||
bool group,
|
||||
option_map o,
|
||||
const numbered_state_heap_factory*
|
||||
nshf)
|
||||
: couvreur99_check(a, poprem, nshf), num(1), group_(group)
|
||||
: couvreur99_check(a, o, nshf), num(1)
|
||||
{
|
||||
group_ = o.get("group", 1);
|
||||
|
||||
// Setup depth-first search from the initial state.
|
||||
todo.push_back(todo_item(0, 0));
|
||||
todo.back().q.push_front(successor(bddtrue, ecs_->aut->get_init_state()));
|
||||
|
|
@ -409,7 +411,7 @@ namespace spot
|
|||
// We have found an accepting SCC. Clean up TODO.
|
||||
clear_todo();
|
||||
set_states(ecs_->states());
|
||||
return new couvreur99_check_result(ecs_);
|
||||
return new couvreur99_check_result(ecs_, options());
|
||||
}
|
||||
|
||||
continue;
|
||||
|
|
@ -491,7 +493,7 @@ namespace spot
|
|||
clear_todo();
|
||||
set_states(ecs_->states());
|
||||
delete iter;
|
||||
return new couvreur99_check_result(ecs_);
|
||||
return new couvreur99_check_result(ecs_, options());
|
||||
}
|
||||
// Group the pending successors of formed SCC if requested.
|
||||
if (group_)
|
||||
|
|
@ -560,7 +562,7 @@ namespace spot
|
|||
// We have found an accepting SCC. Clean up TODO.
|
||||
clear_todo();
|
||||
set_states(ecs_->states());
|
||||
return new couvreur99_check_result(ecs_);
|
||||
return new couvreur99_check_result(ecs_, options());
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -573,4 +575,14 @@ namespace spot
|
|||
return ecs_->h->find(s).second;
|
||||
}
|
||||
|
||||
emptiness_check*
|
||||
couvreur99(const tgba* a,
|
||||
option_map o,
|
||||
const numbered_state_heap_factory* nshf)
|
||||
{
|
||||
if (o.get("shy"))
|
||||
return new couvreur99_check_shy(a, o, nshf);
|
||||
return new couvreur99_check(a, o, nshf);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -113,19 +113,43 @@ namespace spot
|
|||
/// at once in order to decide which to explore first, and must keep
|
||||
/// a list of all unexplored successors in its DFS stack.
|
||||
///
|
||||
/// The \c poprem parameter specifies how the algorithm should
|
||||
/// handle the destruction of non-accepting maximal strongly
|
||||
/// connected components. If \c poprem is true, the algorithm will
|
||||
/// keep a list of all states of a SCC that are fully processed and
|
||||
/// should be removed once the MSCC is popped. If \c poprem is
|
||||
/// false, the MSCC will be traversed again (i.e. generating the
|
||||
/// successors of the root recursively) for deletion. This is
|
||||
/// a choice between memory and speed.
|
||||
/// The couvreur99() function is a wrapper around these two flavors
|
||||
/// of the algorithm. \a options is an option map that specifies
|
||||
/// which algorithms should be used, and how.
|
||||
///
|
||||
/// The following options are available.
|
||||
/// \li \c "shy" : if non zero, then spot::couvreur99_check_shy is used,
|
||||
/// otherwise (and by default) spot::couvreur99_check is used.
|
||||
///
|
||||
/// \li \c "poprem" : specifies how the algorithm should handle the
|
||||
/// destruction of non-accepting maximal strongly connected
|
||||
/// components. If \c poprem is non null, the algorithm will keep a
|
||||
/// list of all states of a SCC that are fully processed and should
|
||||
/// be removed once the MSCC is popped. If \c poprem is null (the
|
||||
/// default), the MSCC will be traversed again (i.e. generating the
|
||||
/// successors of the root recursively) for deletion. This is a
|
||||
/// choice between memory and speed.
|
||||
///
|
||||
/// \li \c "group" : this options is used only by spot::couvreur99_check_shy.
|
||||
/// If non null (the default), the successors of all the
|
||||
/// states that belong to the same SCC will be considered when
|
||||
/// choosing a successor. Otherwise, only the successor of the
|
||||
/// topmost state on the DFS stack are considered.
|
||||
emptiness_check*
|
||||
couvreur99(const tgba* a,
|
||||
option_map options = option_map(),
|
||||
const numbered_state_heap_factory* nshf
|
||||
= numbered_state_heap_hash_map_factory::instance());
|
||||
|
||||
|
||||
/// \brief An implementation of the Couvreur99 emptiness-check algorithm.
|
||||
///
|
||||
/// See the documentation for spot::couvreur99.
|
||||
class couvreur99_check: public emptiness_check, public ec_statistics
|
||||
{
|
||||
public:
|
||||
couvreur99_check(const tgba* a,
|
||||
bool poprem = true,
|
||||
option_map o = option_map(),
|
||||
const numbered_state_heap_factory* nshf
|
||||
= numbered_state_heap_hash_map_factory::instance());
|
||||
virtual ~couvreur99_check();
|
||||
|
|
@ -161,18 +185,12 @@ namespace spot
|
|||
/// \brief A version of spot::couvreur99_check that tries to visit
|
||||
/// known states first.
|
||||
///
|
||||
/// If \a group is true (the default), the successors of all the
|
||||
/// states that belong to the same SCC will be considered when
|
||||
/// choosing a successor. Otherwise, only the successor of the
|
||||
/// topmost state on the DFS stack are considered.
|
||||
///
|
||||
/// See the documentation for spot::couvreur99_check
|
||||
/// See the documentation for spot::couvreur99.
|
||||
class couvreur99_check_shy : public couvreur99_check
|
||||
{
|
||||
public:
|
||||
couvreur99_check_shy(const tgba* a,
|
||||
bool poprem = true,
|
||||
bool group = true,
|
||||
option_map o = option_map(),
|
||||
const numbered_state_heap_factory* nshf
|
||||
= numbered_state_heap_hash_map_factory::instance());
|
||||
virtual ~couvreur99_check_shy();
|
||||
|
|
@ -231,6 +249,7 @@ namespace spot
|
|||
virtual int* find_state(const state* s);
|
||||
};
|
||||
|
||||
|
||||
/// @}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -69,8 +69,8 @@ namespace spot
|
|||
int dftop; // Top of DFS stack.
|
||||
bool violation; // Whether an accepting run was found.
|
||||
|
||||
gv04(const tgba *a)
|
||||
: emptiness_check(a), accepting(a->all_acceptance_conditions())
|
||||
gv04(const tgba *a, option_map o)
|
||||
: emptiness_check(a, o), accepting(a->all_acceptance_conditions())
|
||||
{
|
||||
assert(a->number_of_acceptance_conditions() <= 1);
|
||||
}
|
||||
|
|
@ -243,7 +243,8 @@ namespace spot
|
|||
gv04& data;
|
||||
|
||||
result(gv04& data)
|
||||
: emptiness_check_result(data.automaton()), data(data)
|
||||
: emptiness_check_result(data.automaton(), data.options()),
|
||||
data(data)
|
||||
{
|
||||
}
|
||||
|
||||
|
|
@ -405,8 +406,8 @@ namespace spot
|
|||
} // anonymous
|
||||
|
||||
emptiness_check*
|
||||
explicit_gv04_check(const tgba* a)
|
||||
explicit_gv04_check(const tgba* a, option_map o)
|
||||
{
|
||||
return new gv04(a);
|
||||
return new gv04(a, o);
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
//
|
||||
|
|
@ -22,6 +22,8 @@
|
|||
#ifndef SPOT_TGBAALGOS_GV04_HH
|
||||
# define SPOT_TGBAALGOS_GV04_HH
|
||||
|
||||
#include "misc/optionmap.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
class tgba;
|
||||
|
|
@ -51,7 +53,8 @@ namespace spot
|
|||
/// isbn = {3-540-21299-X}
|
||||
/// }
|
||||
/// \endverbatim
|
||||
emptiness_check* explicit_gv04_check(const tgba* a);
|
||||
emptiness_check* explicit_gv04_check(const tgba* a,
|
||||
option_map o = option_map());
|
||||
}
|
||||
|
||||
#endif // SPOT_TGBAALGOS_GV04_HH
|
||||
|
|
|
|||
|
|
@ -131,7 +131,7 @@ namespace spot
|
|||
/// \sa spot::explicit_se05_search
|
||||
///
|
||||
emptiness_check* bit_state_hashing_se05_search(const tgba *a, size_t size,
|
||||
option_map o = option_map());
|
||||
option_map o = option_map());
|
||||
|
||||
/// @}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -53,8 +53,8 @@ namespace spot
|
|||
{
|
||||
public:
|
||||
/// \brief Initialize the search algorithm on the automaton \a a
|
||||
tau03_search(const tgba *a, size_t size)
|
||||
: emptiness_check(a),
|
||||
tau03_search(const tgba *a, size_t size, option_map o)
|
||||
: emptiness_check(a, o),
|
||||
h(size),
|
||||
all_cond(a->all_acceptance_conditions())
|
||||
{
|
||||
|
|
@ -375,9 +375,9 @@ namespace spot
|
|||
|
||||
} // anonymous
|
||||
|
||||
emptiness_check* explicit_tau03_search(const tgba *a)
|
||||
emptiness_check* explicit_tau03_search(const tgba *a, option_map o)
|
||||
{
|
||||
return new tau03_search<explicit_tau03_search_heap>(a, 0);
|
||||
return new tau03_search<explicit_tau03_search_heap>(a, 0, o);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
//
|
||||
|
|
@ -93,7 +93,8 @@ namespace spot
|
|||
/// }
|
||||
/// \endverbatim
|
||||
///
|
||||
emptiness_check* explicit_tau03_search(const tgba *a);
|
||||
emptiness_check* explicit_tau03_search(const tgba *a,
|
||||
option_map o = option_map());
|
||||
|
||||
/// @}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -62,8 +62,8 @@ namespace spot
|
|||
{
|
||||
public:
|
||||
/// \brief Initialize the search algorithm on the automaton \a a
|
||||
tau03_opt_search(const tgba *a, size_t size)
|
||||
: emptiness_check(a),
|
||||
tau03_opt_search(const tgba *a, size_t size, option_map o)
|
||||
: emptiness_check(a, o),
|
||||
current_weight(a->neg_acceptance_conditions()),
|
||||
h(size),
|
||||
all_acc(a->all_acceptance_conditions())
|
||||
|
|
@ -497,9 +497,9 @@ namespace spot
|
|||
|
||||
} // anonymous
|
||||
|
||||
emptiness_check* explicit_tau03_opt_search(const tgba *a)
|
||||
emptiness_check* explicit_tau03_opt_search(const tgba *a, option_map o)
|
||||
{
|
||||
return new tau03_opt_search<explicit_tau03_opt_search_heap>(a, 0);
|
||||
return new tau03_opt_search<explicit_tau03_opt_search_heap>(a, 0, o);
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
|||
|
|
@ -95,7 +95,8 @@ namespace spot
|
|||
/// the path stored in the blue stack. Such a vector is associated to each
|
||||
/// state of this stack.
|
||||
///
|
||||
emptiness_check* explicit_tau03_opt_search(const tgba *a);
|
||||
emptiness_check* explicit_tau03_opt_search(const tgba *a,
|
||||
option_map o = option_map());
|
||||
|
||||
/// @}
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue