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

* src/tgbaalgos/emptinesscheck.hh

Browse source 
(explicit_connected_component_factory,
connected_component_hash_set_factory): New classes.
(counter_example::counter_example): Take an
explicit_connected_component_factory factory argument.
* src/tgbaalgos/emptinesscheck.cc: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2004-04-13 13:57:59 +00:00
parent 3e63c1a0ca
commit 7305dbb658
3 changed files with 59 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

10
ChangeLog
View file

@ -1,11 +1,21 @@
2004-04-13 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/emptinesscheck.hh
(explicit_connected_component_factory,
connected_component_hash_set_factory): New classes.
(counter_example::counter_example): Take an
explicit_connected_component_factory factory argument.
* src/tgbaalgos/emptinesscheck.cc: Adjust.
* src/tgbaalgos/emptinesscheck.hh (explicit_connected_component):
New class.
(counter_example::connected_component_set): Rename as ...
(connected_component_hash_set): ... this, and inherit from
explicit_connected_component.
(counter_example::accepting_path, counter_example::complete_cycle):
Take an explicit_connected_component argument instead of a
connected_component_set.
* src/tgbaalgos/emptinesscheck.cc: Adjust.
* src/tgbaalgos/emptinesscheck.hh
(counter_example::connected_component_set::has_state): Return

26
src/tgbaalgos/emptinesscheck.cc
View file

@ -513,7 +513,29 @@ namespace spot
//////////////////////////////////////////////////////////////////////
counter_example::counter_example(const emptiness_check_status* ecs)
connected_component_hash_set_factory::connected_component_hash_set_factory()
: explicit_connected_component_factory()
{
}
connected_component_hash_set*
connected_component_hash_set_factory::build() const
{
return new connected_component_hash_set();
}
const connected_component_hash_set_factory*
connected_component_hash_set_factory::instance()
{
static connected_component_hash_set_factory f;
return &f;
}
//////////////////////////////////////////////////////////////////////
counter_example::counter_example(const emptiness_check_status* ecs,
const explicit_connected_component_factory*
eccf)
: ecs_(ecs)
{
assert(!ecs_->root.empty());
@ -526,7 +548,7 @@ namespace spot
new (explicit_connected_component*)[comp_size];
for (int j = comp_size - 1; 0 <= j; --j)
{
scc[j] = new connected_component_hash_set();
scc[j] = eccf->build();
scc[j]->index = root.top().index;
scc[j]->condition = root.top().condition;
root.pop();

28
src/tgbaalgos/emptinesscheck.hh
View file

@ -157,7 +157,7 @@ namespace spot
class explicit_connected_component: public scc_stack::connected_component
{
public:
virtual ~explicit_connected_component() {};
virtual ~explicit_connected_component() {}
/// \brief Check if the SCC contains states \a s.
///
/// Return the representative of \a s in the SCC, and delete \a
@ -172,7 +172,7 @@ namespace spot
class connected_component_hash_set: public explicit_connected_component
{
public:
virtual ~connected_component_hash_set() {};
virtual ~connected_component_hash_set() {}
virtual const state* has_state(const state* s) const;
virtual void insert(const state* s);
protected:
@ -181,10 +181,32 @@ namespace spot
set_type states;
};
class explicit_connected_component_factory
{
public:
virtual ~explicit_connected_component_factory() {}
virtual explicit_connected_component* build() const = 0;
};
class connected_component_hash_set_factory :
public explicit_connected_component_factory
{
public:
virtual connected_component_hash_set* build() const;
static const connected_component_hash_set_factory* instance();
protected:
virtual ~connected_component_hash_set_factory() {}
connected_component_hash_set_factory();
};
class counter_example
{
public:
counter_example(const emptiness_check_status* ecs);
counter_example(const emptiness_check_status* ecs,
const explicit_connected_component_factory*
eccf = connected_component_hash_set_factory::instance());
typedef std::pair<const state*, bdd> state_proposition;
typedef std::list<const state*> state_sequence;