alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

* src/tgbaalgos/emptinesscheck.hh (emptiness_check::check2): Move

Browse source 
into ...
(emptiness_check_shy): This new subclass of emptiness_check.
* src/tgbaalgos/emptinesscheck.cc, src/tgbatest/ltl2tgba.cc,
iface/gspn/ltlgspn.cc: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2004-04-13 11:44:42 +00:00
parent be17fc19f5
commit b85e930232
5 changed files with 77 additions and 48 deletions
Download patch file Download diff file Expand all files Collapse all files

6
ChangeLog
View file

@ -1,5 +1,11 @@
2004-04-13 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/emptinesscheck.hh (emptiness_check::check2): Move
into ...
(emptiness_check_shy): This new subclass of emptiness_check.
* src/tgbaalgos/emptinesscheck.cc, src/tgbatest/ltl2tgba.cc,
iface/gspn/ltlgspn.cc: Adjust.
* src/tgba/bdddict.hh (bdd_dict::annon_free_list): Hide from Swig.
* src/tgbaalgo/semptinesscheck.hh (counter_example): New class,

14
iface/gspn/ltlgspn.cc
View file

@ -169,13 +169,16 @@ main(int argc, char **argv)
case Couvreur:
case Couvreur2:
{
spot::emptiness_check ec(prod);
bool res;
spot::emptiness_check* ec;
if (check == Couvreur)
res = ec.check();
ec = new spot::emptiness_check(prod);
else
res = ec.check2();
const spot::emptiness_check_status* ecs = ec.result();
ec = new spot::emptiness_check_shy(prod);
bool res = ec->check();
const spot::emptiness_check_status* ecs = ec->result();
if (!res)
{
if (compute_counter_example)
@ -196,6 +199,7 @@ main(int argc, char **argv)
ecs->print_stats(std::cout);
}
std::cout << std::endl;
delete ec;
if (!res)
exit(1);
}

27
src/tgbaalgos/emptinesscheck.cc
View file

@ -111,8 +111,6 @@ namespace spot
typedef std::pair<const spot::state*, tgba_succ_iterator*> pair_state_iter;
emptiness_check::emptiness_check(const tgba* a)
{
ecs_ = new emptiness_check_status(a);
@ -309,6 +307,23 @@ namespace spot
return true;
}
const emptiness_check_status*
emptiness_check::result() const
{
return ecs_;
}
//////////////////////////////////////////////////////////////////////
emptiness_check_shy::emptiness_check_shy(const tgba* a)
: emptiness_check(a)
{
}
emptiness_check_shy::~emptiness_check_shy()
{
}
struct successor {
bdd acc;
const spot::state* s;
@ -316,7 +331,7 @@ namespace spot
};
bool
emptiness_check::check2()
emptiness_check_shy::check()
{
// We use five main data in this algorithm:
// * emptiness_check::root, a stack of strongly connected components (SCC),
@ -474,12 +489,6 @@ namespace spot
}
}
const emptiness_check_status*
emptiness_check::result() const
{
return ecs_;
}
//////////////////////////////////////////////////////////////////////
bool

64
src/tgbaalgos/emptinesscheck.hh
View file

@ -80,6 +80,7 @@ namespace spot
void print_stats(std::ostream& os) const;
};
//@{
/// \brief Check whether the language of an automate is empty.
///
/// This is based on the following paper.
@ -100,41 +101,39 @@ namespace spot
/// isbn = {3-540-66587-0}
/// }
/// \endverbatim
///
/// check() returns true if the automaton's language is empty. When
/// it return false, a stack of SCC has been built and can
/// later be used by counter_example().
///
/// There are two variants of this algorithm: emptiness_check() and
/// emptiness_check_shy(). They differ in their memory usage, the
/// number for successors computed before they are used and the way
/// the depth first search is directed.
///
/// emptiness_check() performs a straightforward depth first search.
/// The DFS stacks store tgba_succ_iterators, so that only the
/// iterators which really are explored are computed.
///
/// emptiness_check_shy() try to explore successors which are
/// visited states first. this helps to merge SCCs and generally
/// helps to produce shorter counter-examples. However this
/// algorithm cannot stores unprocessed successors as
/// tgba_succ_iterators: it must compute all successors of a state
/// at once in order to decide which to explore first, and must keep
/// a list of all unexplored successors in its DFS stack.
class emptiness_check
{
public:
emptiness_check(const tgba* a);
~emptiness_check();
virtual ~emptiness_check();
//@{
/// \brief check whether an automaton's language is empty
///
/// Returns true if the automaton's language is empty. When
/// it return false, a stack of SCC has been built and can
/// later be used by counter_example().
///
/// There are two variants of this algorithm: check() and check2().
/// They differ in their memory usage, the number for successors computed
/// before they are used and the way the depth first search is directed.
///
/// check() performs a straightforward depth first search. The DFS
/// stacks store tgba_succ_iterators, so that only the iterators which
/// really are explored are computed.
///
/// check2() try to explore successors which are visited states first.
/// this helps to merge SCCs and generally helps to produce shorter
/// counter-examples. However this algorithm cannot stores unprocessed
/// successors as tgba_succ_iterators: it must compute all successors
/// of a state at once in order to decide which to explore first, and
/// must keep a list of all unexplored successors in its DFS stack.
bool check();
bool check2();
//@}
/// check whether the automaton's language is empty
virtual bool check();
const emptiness_check_status* result() const;
private:
protected:
emptiness_check_status* ecs_;
/// \brief Remove a strongly component from the hash.
///
@ -142,9 +141,18 @@ namespace spot
/// state. In other words, it removes the strongly connected
/// component that contains this state.
void remove_component(const state* start_delete);
};
class emptiness_check_shy : public emptiness_check
{
public:
emptiness_check_shy(const tgba* a);
virtual ~emptiness_check_shy();
virtual bool check();
};
//@}
class counter_example
{

14
src/tgbatest/ltl2tgba.cc
View file

@ -364,28 +364,30 @@ main(int argc, char** argv)
case Couvreur:
case Couvreur2:
{
spot::emptiness_check ec = spot::emptiness_check(a);
bool res;
spot::emptiness_check* ec;
if (echeck == Couvreur)
res = ec.check();
ec = new spot::emptiness_check(a);
else
res = ec.check2();
ec = new spot::emptiness_check_shy(a);
bool res = ec->check();
if (expect_counter_example)
{
if (res)
{
exit_code = 1;
delete ec;
break;
}
spot::counter_example ce(ec.result());
spot::counter_example ce(ec->result());
ce.print_result(std::cout);
}
else
{
exit_code = !res;
}
delete ec;
}
break;
case MagicSearch: