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

* src/tgbaalgos/emptinesscheck.hh, src/tgbaalgos/emptinesscheck.cc:

Browse source 
Delete and split into ...
* src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh,
src/tgbaalgos/gtec/explscc.cc, src/tgbaalgos/gtec/explscc.hh,
src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh,
src/tgbaalgos/gtec/nsheap.cc, src/tgbaalgos/gtec/nsheap.hh,
src/tgbaalgos/gtec/sccstack.cc, src/tgbaalgos/gtec/sccstack.hh,
src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh: ...
these new files.
* src/tgbaalgos/gtec/Makefile.am: New file.
* src/tgbaalgos/Makefile.am (SUBDIRS, libtgbaalgos_la_LIBADD):
Recurse into gtec and link gtec/libgtec.la.
(tgbaalgos_HEADERS, libtgbaalgos_la_SOURCES): Remove emptinesscheck.hh
and emptinesscheck.cc.
* configure.ac: Output src/tgbalagos/gtec/Makefile.
* iface/gspn/ltlgspn.cc, src/tgbatest/ltl2tgba.cc: Update includes.
* README: Update tree description.
This commit is contained in:
Alexandre Duret-Lutz 2004-04-14 10:56:36 +00:00
parent d8f5bf608a
commit 579c343e13
22 changed files with 1738 additions and 1342 deletions
Download patch file Download diff file Expand all files Collapse all files

24
ChangeLog
View file

@ -1,8 +1,28 @@
2004-04-14 Alexandre Duret-Lutz <adl@src.lip6.fr>
* src/tgbaalgos/emptinesscheck.hh, src/tgbaalgos/emptinesscheck.cc:
Delete and split into ...
* src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh,
src/tgbaalgos/gtec/explscc.cc, src/tgbaalgos/gtec/explscc.hh,
src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh,
src/tgbaalgos/gtec/nsheap.cc, src/tgbaalgos/gtec/nsheap.hh,
src/tgbaalgos/gtec/sccstack.cc, src/tgbaalgos/gtec/sccstack.hh,
src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh: ...
these new files.
* src/tgbaalgos/gtec/Makefile.am: New file.
* src/tgbaalgos/Makefile.am (SUBDIRS, libtgbaalgos_la_LIBADD):
Recurse into gtec and link gtec/libgtec.la.
(tgbaalgos_HEADERS, libtgbaalgos_la_SOURCES): Remove emptinesscheck.hh
and emptinesscheck.cc.
* configure.ac: Output src/tgbalagos/gtec/Makefile.
* iface/gspn/ltlgspn.cc, src/tgbatest/ltl2tgba.cc: Update includes.
* README: Update tree description.
2004-04-13 Alexandre Duret-Lutz <adl@src.lip6.fr> 2004-04-13 Alexandre Duret-Lutz <adl@src.lip6.fr>
* tgbaalgos/emptinesscheck.hh (numbered_state_heap_const_iterator, * src/tgbaalgos/emptinesscheck.hh (numbered_state_heap_const_iterator,
numbered_state_heap, numbered_state_heap_hash_map): New classes. numbered_state_heap, numbered_state_heap_hash_map): New classes.
* tgbaalgos/emptinesscheck.cc * src/tgbaalgos/emptinesscheck.cc
(numbered_state_heap_hash_map_const_iterator): New class. (numbered_state_heap_hash_map_const_iterator): New class.
(numbered_state_heap_hash_map): Implement it. (numbered_state_heap_hash_map): Implement it.

1
README
View file

@ -65,6 +65,7 @@ src/ Sources for libspot.
misc/ Miscellaneous support files. misc/ Miscellaneous support files.
tgba/ TGBA objects and cousins. tgba/ TGBA objects and cousins.
tgbaalgos/ Algorithms on TGBAs. tgbaalgos/ Algorithms on TGBAs.
gtec/ Generalized Tarjan Emptiness-Check.
tgbaparse/ Parser for explicit TGBAs. tgbaparse/ Parser for explicit TGBAs.
tgbatest/ Tests for tgba/, tgbaalgos/, and tgbaparse/. tgbatest/ Tests for tgba/, tgbaalgos/, and tgbaparse/.
doc/ Documentation for libspot. doc/ Documentation for libspot.

1
configure.ac
View file

@ -64,6 +64,7 @@ AC_CONFIG_FILES([
src/ltlvisit/Makefile src/ltlvisit/Makefile
src/tgba/Makefile src/tgba/Makefile
src/tgbaalgos/Makefile src/tgbaalgos/Makefile
src/tgbaalgos/gtec/Makefile
src/tgbaparse/Makefile src/tgbaparse/Makefile
src/tgbatest/Makefile src/tgbatest/Makefile
src/tgbatest/defs src/tgbatest/defs

3
iface/gspn/ltlgspn.cc
View file

@ -35,7 +35,8 @@
#include "tgbaalgos/ltl2tgba_lacim.hh" #include "tgbaalgos/ltl2tgba_lacim.hh"
#include "tgbaalgos/ltl2tgba_fm.hh" #include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgbaalgos/magic.hh" #include "tgbaalgos/magic.hh"
#include "tgbaalgos/emptinesscheck.hh" #include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/gtec/ce.hh"
void void

6
src/tgbaalgos/Makefile.am
View file

@ -19,6 +19,8 @@
## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA ## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
## 02111-1307, USA. ## 02111-1307, USA.
SUBDIRS = gtec
AM_CPPFLAGS = -I$(srcdir)/.. $(BUDDY_CPPFLAGS) AM_CPPFLAGS = -I$(srcdir)/.. $(BUDDY_CPPFLAGS)
AM_CXXFLAGS = $(WARNING_CXXFLAGS) AM_CXXFLAGS = $(WARNING_CXXFLAGS)
@ -27,7 +29,6 @@ tgbaalgosdir = $(pkgincludedir)/tgbaalgos
tgbaalgos_HEADERS = \ tgbaalgos_HEADERS = \
dotty.hh \ dotty.hh \
dupexp.hh \ dupexp.hh \
emptinesscheck.hh \
lbtt.hh \ lbtt.hh \
ltl2tgba_fm.hh \ ltl2tgba_fm.hh \
ltl2tgba_lacim.hh \ ltl2tgba_lacim.hh \
@ -41,7 +42,6 @@ noinst_LTLIBRARIES = libtgbaalgos.la
libtgbaalgos_la_SOURCES = \ libtgbaalgos_la_SOURCES = \
dotty.cc \ dotty.cc \
dupexp.cc \ dupexp.cc \
emptinesscheck.cc \
lbtt.cc \ lbtt.cc \
ltl2tgba_fm.cc \ ltl2tgba_fm.cc \
ltl2tgba_lacim.cc \ ltl2tgba_lacim.cc \
@ -50,3 +50,5 @@ libtgbaalgos_la_SOURCES = \
reachiter.cc \ reachiter.cc \
save.cc \ save.cc \
stats.cc stats.cc
libtgbaalgos_la_LIBADD = gtec/libgtec.la

1042
src/tgbaalgos/emptinesscheck.cc
View file

File diff suppressed because it is too large Load diff

294
src/tgbaalgos/emptinesscheck.hh
View file

@ -1,294 +0,0 @@
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// 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 2 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 Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#ifndef SPOT_EMPTINESS_CHECK_HH
# define SPOT_EMPTINESS_CHECK_HH
#include "tgba/tgba.hh"
#include "misc/hash.hh"
#include <stack>
#include <list>
#include <utility>
#include <iostream>
namespace spot
{
class scc_stack
{
public:
struct connected_component
{
// During the Depth path we keep the connected component that we met.
public:
connected_component(int index = -1);
int index;
/// The bdd condition is the union of all acceptance conditions of
/// transitions which connect the states of the connected component.
bdd condition;
};
connected_component& top();
void pop();
void push(int index);
size_t size() const;
bool empty() const;
typedef std::stack<connected_component> stack_type;
stack_type s;
};
class numbered_state_heap_const_iterator
{
public:
virtual ~numbered_state_heap_const_iterator() {}
virtual void first() = 0;
virtual void next() = 0;
virtual bool done() const = 0;
virtual const state* get_state() const = 0;
virtual int get_index() const = 0;
};
class numbered_state_heap
{
public:
virtual ~numbered_state_heap() {}
//@{
/// \brief Is state in the heap?
///
/// Returns 0 if \a s is not in the heap. or a pointer to
/// its number if it is.
virtual const int* find(const state* s) const = 0;
virtual int* find(const state* s) = 0;
//@}
virtual void insert(const state* s, int index) = 0;
virtual int size() const = 0;
virtual numbered_state_heap_const_iterator* iterator() const = 0;
/// \brief Return a state which is equal to \a s, but is in \c h,
/// and free \a s if it is different.
///
/// Doing so simplify memory management, because we don't have to
/// track which state need to be kept or deallocated: all key in
/// \c h should last for the whole life of the emptiness_check.
virtual const state* filter(const state* s) const = 0;
};
class numbered_state_heap_hash_map : public numbered_state_heap
{
public:
virtual ~numbered_state_heap_hash_map();
virtual const int* find(const state* s) const;
virtual int* find(const state* s);
virtual void insert(const state* s, int index);
virtual int size() const;
virtual numbered_state_heap_const_iterator* iterator() const;
virtual const state* filter(const state* s) const;
protected:
typedef Sgi::hash_map<const state*, int,
state_ptr_hash, state_ptr_equal> hash_type;
hash_type h; ///< Map of visited states.
friend class numbered_state_heap_hash_map_const_iterator;
};
class emptiness_check_status
{
public:
emptiness_check_status(const tgba* aut);
~emptiness_check_status();
const tgba* aut;
scc_stack root;
numbered_state_heap_hash_map h; ///< Map of visited states.
/// Output statistics about this object.
void print_stats(std::ostream& os) const;
};
//@{
/// \brief Check whether the language of an automate is empty.
///
/// This is based on the following paper.
/// \verbatim
/// @InProceedings{couvreur.99.fm,
/// author = {Jean-Michel Couvreur},
/// title = {On-the-fly Verification of Temporal Logic},
/// pages = {253--271},
/// editor = {Jeannette M. Wing and Jim Woodcock and Jim Davies},
/// booktitle = {Proceedings of the World Congress on Formal Methods in
/// the Development of Computing Systems (FM'99)},
/// publisher = {Springer-Verlag},
/// series = {Lecture Notes in Computer Science},
/// volume = {1708},
/// year = {1999},
/// address = {Toulouse, France},
/// month = {September},
/// 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);
virtual ~emptiness_check();
/// check whether the automaton's language is empty
virtual bool check();
const emptiness_check_status* result() const;
protected:
emptiness_check_status* ecs_;
/// \brief Remove a strongly component from the hash.
///
/// This function remove all accessible state from a given
/// 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 explicit_connected_component: public scc_stack::connected_component
{
public:
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
/// s if it is different (acting like
/// numbered_state_heap::filter), or 0 otherwise.
virtual const state* has_state(const state* s) const = 0;
/// Insert a new state in the SCC.
virtual void insert(const state* s) = 0;
};
class connected_component_hash_set: public explicit_connected_component
{
public:
virtual ~connected_component_hash_set() {}
virtual const state* has_state(const state* s) const;
virtual void insert(const state* s);
protected:
typedef Sgi::hash_set<const state*,
state_ptr_hash, state_ptr_equal> set_type;
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,
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;
typedef std::list<state_proposition> cycle_path;
state_sequence suffix;
cycle_path period;
/// \brief Display the example computed by counter_example().
///
/// \param restrict optional automaton to project the example on.
std::ostream& print_result(std::ostream& os,
const tgba* restrict = 0) const;
/// Output statistics about this object.
void print_stats(std::ostream& os) const;
protected:
/// Called by counter_example to find a path which traverses all
/// acceptance conditions in the accepted SCC.
void accepting_path (const explicit_connected_component* scc,
const state* start, bdd acc_to_traverse);
/// Complete a cycle that caraterise the period of the counter
/// example. Append a sequence to the path given by accepting_path.
void complete_cycle(const explicit_connected_component* scc,
const state* from, const state* to);
private:
const emptiness_check_status* ecs_;
};
}
#endif // SPOT_EMPTINESS_CHECK_HH

6
src/tgbaalgos/gtec/.cvsignore Normal file
View file

@ -0,0 +1,6 @@
.deps
.libs
*.lo
*.la
Makefile
Makefile.in

42
src/tgbaalgos/gtec/Makefile.am Normal file
View file

@ -0,0 +1,42 @@
## Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
## département Systèmes Répartis Coopératifs (SRC), Université Pierre
## et Marie Curie.
##
## 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 2 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 Spot; see the file COPYING. If not, write to the Free
## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
## 02111-1307, USA.
AM_CPPFLAGS = -I$(srcdir)/../.. $(BUDDY_CPPFLAGS)
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
gtecdir = $(pkgincludedir)/tgbaalgos/gtec
gtec_HEADERS = \
ce.hh \
explscc.hh \
gtec.hh \
nsheap.hh \
sccstack.hh \
status.hh
noinst_LTLIBRARIES = libgtec.la
libgtec_la_SOURCES = \
ce.cc \
explscc.cc \
gtec.cc \
nsheap.cc \
sccstack.cc \
status.cc

443
src/tgbaalgos/gtec/ce.cc Normal file
View file

@ -0,0 +1,443 @@
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// 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 2 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 Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#include "ce.hh"
#include "tgba/bddprint.hh"
#include <map>
namespace spot
{
namespace
{
typedef std::pair<const spot::state*, tgba_succ_iterator*> pair_state_iter;
}
counter_example::counter_example(const emptiness_check_status* ecs,
const explicit_connected_component_factory*
eccf)
: ecs_(ecs)
{
assert(!ecs_->root.empty());
assert(suffix.empty());
scc_stack::stack_type root = ecs_->root.s;
int comp_size = root.size();
// Transform the stack of connected component into an array.
explicit_connected_component** scc =
new (explicit_connected_component*)[comp_size];
for (int j = comp_size - 1; 0 <= j; --j)
{
scc[j] = eccf->build();
scc[j]->index = root.top().index;
scc[j]->condition = root.top().condition;
root.pop();
}
assert(root.empty());
// Build the set of states for all SCCs.
numbered_state_heap_const_iterator* i = ecs_->h.iterator();
for (i->first(); !i->done(); i->next())
{
int index = i->get_index();
// Skip states from dead SCCs.
if (index < 0)
continue;
assert(index != 0);
// Find the SCC this state belongs to.
int j;
for (j = 1; j < comp_size; ++j)
if (index < scc[j]->index)
break;
scc[j - 1]->insert(i->get_state());
}
delete i;
suffix.push_front(ecs_->h.filter(ecs_->aut->get_init_state()));
// We build a path trough each SCC in the stack. For the
// first SCC, the starting state is the initial state of the
// automaton. The destination state is the closest state
// from the next SCC. This destination state becomes the
// starting state when building a path though the next SCC.
for (int k = 0; k < comp_size - 1; ++k)
{
// FIFO for the breadth-first search.
// (we are looking for the closest state in the next SCC.)
std::deque<pair_state_iter> todo;
// Record the father of each state, while performing the BFS.
typedef std::map<const state*, const state*,
state_ptr_less_than> father_map;
father_map father;
// Initial state of the BFS.
const state* start = suffix.back();
{
tgba_succ_iterator* i = ecs_->aut->succ_iter(start);
todo.push_back(pair_state_iter(start, i));
}
while (!todo.empty())
{
const state* src = todo.front().first;
tgba_succ_iterator* i = todo.front().second;
todo.pop_front();
for (i->first(); !i->done(); i->next())
{
const state* dest = i->current_state();
// Are we leaving this SCC?
const state* h_dest = scc[k]->has_state(dest);
if (!h_dest)
{
// If we have found a state in the next SCC.
// Unwind the path and populate SUFFIX.
h_dest = scc[k+1]->has_state(dest);
if (h_dest)
{
state_sequence seq;
seq.push_front(h_dest);
while (src->compare(start))
{
seq.push_front(src);
src = father[src];
}
// Append SEQ to SUFFIX.
suffix.splice(suffix.end(), seq);
// Exit this BFS for this SCC.
while (!todo.empty())
{
delete todo.front().second;
todo.pop_front();
}
break;
}
// Restrict the BFS to state inside the SCC.
continue;
}
if (father.find(h_dest) == father.end())
{
todo.push_back
(pair_state_iter(h_dest, ecs_->aut->succ_iter(h_dest)));
father[h_dest] = src;
}
}
delete i;
}
}
accepting_path(scc[comp_size - 1], suffix.back(),
scc[comp_size - 1]->condition);
for (int j = comp_size - 1; 0 <= j; --j)
delete scc[j];
delete[] scc;
}
void
counter_example::complete_cycle(const explicit_connected_component* scc,
const state* from,
const state* to)
{
// If by change or period already ends on the state we have
// to reach back, we are done.
if (from == to
&& ! period.empty())
return;
// Records backlinks to parent state during the BFS.
// (This also stores the propositions of this link.)
std::map<const state*, state_proposition, state_ptr_less_than> father;
// BFS queue.
std::deque<pair_state_iter> todo;
// Initial state.
{
tgba_succ_iterator* i = ecs_->aut->succ_iter(from);
todo.push_back(pair_state_iter(from, i));
}
while (!todo.empty())
{
const state* src = todo.front().first;
tgba_succ_iterator* i = todo.front().second;
todo.pop_front();
for (i->first(); !i->done(); i->next())
{
const state* dest = i->current_state();
// Do not escape this SCC or visit a state already visited.
const state* h_dest = scc->has_state(dest);
if (!h_dest)
{
delete dest;
continue;
}
if (father.find(h_dest) != father.end())
continue;
bdd cond = i->current_condition();
// If we have reached our destination, unwind the path
// and populate PERIOD.
if (h_dest == to)
{
cycle_path p;
p.push_front(state_proposition(h_dest, cond));
while (src != from)
{
const state_proposition& psi = father[src];
p.push_front(state_proposition(src, psi.second));
src = psi.first;
}
period.splice(period.end(), p);
// Exit the BFS, but release all iterators first.
while (!todo.empty())
{
delete todo.front().second;
todo.pop_front();
}
break;
}
// Common case: record backlinks and continue BFS.
todo.push_back(pair_state_iter(h_dest,
ecs_->aut->succ_iter(h_dest)));
father[h_dest] = state_proposition(src, cond);
}
delete i;
}
}
namespace
{
struct triplet
{
const state* s; // Current state.
tgba_succ_iterator* iter; // Iterator to successor of the current state.
bdd acc; // All acceptance conditions traversed by
// the path so far.
triplet (const state* s, tgba_succ_iterator* iter, bdd acc)
: s(s), iter(iter), acc(acc)
{
}
};
}
void
counter_example::accepting_path(const explicit_connected_component* scc,
const state* start, bdd acc_to_traverse)
{
// State seen during the DFS.
typedef Sgi::hash_set<const state*,
state_ptr_hash, state_ptr_equal> set_type;
set_type seen;
// DFS stack.
std::stack<triplet> todo;
while (acc_to_traverse != bddfalse)
{
// Initial state.
{
tgba_succ_iterator* i = ecs_->aut->succ_iter(start);
i->first();
todo.push(triplet(start, i, bddfalse));
seen.insert(start);
}
// The path being explored currently.
cycle_path path;
// The best path seen so far.
cycle_path best_path;
// The acceptance conditions traversed by BEST_PATH.
bdd best_acc = bddfalse;
while (!todo.empty())
{
tgba_succ_iterator* iter = todo.top().iter;
const state* s = todo.top().s;
// Nothing more to explore, backtrack.
if (iter->done())
{
todo.pop();
delete iter;
seen.erase(s);
if (todo.size())
{
assert(path.size());
path.pop_back();
}
continue;
}
// We must not escape the current SCC.
const state* dest = iter->current_state();
const state* h_dest = scc->has_state(dest);
if (!h_dest)
{
delete dest;
iter->next();
continue;
}
bdd acc = iter->current_acceptance_conditions() | todo.top().acc;
path.push_back(state_proposition(h_dest,
iter->current_condition()));
// Advance iterator for next step.
iter->next();
if (seen.find(h_dest) == seen.end())
{
// A new state: continue the DFS.
tgba_succ_iterator* di = ecs_->aut->succ_iter(h_dest);
di->first();
todo.push(triplet(h_dest, di, acc));
seen.insert(h_dest);
continue;
}
// We have completed a full cycle.
// If we already have a best path, let see if the current
// one is better.
if (best_path.size())
{
// When comparing the merits of two paths, only the
// acceptance conditions we are trying the traverse
// are important.
bdd acc_restrict = acc & acc_to_traverse;
bdd best_acc_restrict = best_acc & acc_to_traverse;
// If the best path and the current one traverse the
// same acceptance conditions, we keep the shorter
// path. Otherwise, we keep the path which has the
// more acceptance conditions.
if (best_acc_restrict == acc_restrict)
{
if (best_path.size() <= path.size())
goto backtrack_path;
}
else
{
// `best_acc_restrict >> acc_restrict' is true
// when the set of acceptance conditions of
// best_acc_restrict is included in the set of
// acceptance conditions of acc_restrict.
//
// FIXME: It would be better to count the number
// of acceptance conditions.
if (bddtrue != (best_acc_restrict >> acc_restrict))
goto backtrack_path;
}
}
// The current path the best one.
best_path = path;
best_acc = acc;
backtrack_path:
// Continue exploration from parent to find better paths.
// (Do not pop PATH if ITER is done, because that will be
// done at the top of the loop, among other things.)
if (!iter->done())
path.pop_back();
}
// Append our best path to the period.
for (cycle_path::iterator it = best_path.begin();
it != best_path.end(); ++it)
period.push_back(*it);
// Prepare to find another path for the remaining acceptance
// conditions.
acc_to_traverse -= best_acc;
start = period.back().first;
}
// Complete the path so that it goes back to its beginning,
// forming a cycle.
complete_cycle(scc, start, suffix.back());
}
std::ostream&
counter_example::print_result(std::ostream& os, const tgba* restrict) const
{
os << "Prefix:" << std::endl;
const bdd_dict* d = ecs_->aut->get_dict();
for (state_sequence::const_iterator i_se = suffix.begin();
i_se != suffix.end(); ++i_se)
{
os << " ";
if (restrict)
{
const state* s = ecs_->aut->project_state(*i_se, restrict);
assert(s);
os << restrict->format_state(s) << std::endl;
delete s;
}
else
{
os << ecs_->aut->format_state(*i_se) << std::endl;
}
}
os << "Cycle:" <<std::endl;
for (cycle_path::const_iterator it = period.begin();
it != period.end(); ++it)
{
os << " | " << bdd_format_set(d, it->second) << std::endl;
os << " ";
if (restrict)
{
const state* s = ecs_->aut->project_state(it->first, restrict);
assert(s);
os << restrict->format_state(s) << std::endl;
delete s;
}
else
{
os << ecs_->aut->format_state(it->first) << std::endl;
}
}
return os;
}
void
counter_example::print_stats(std::ostream& os) const
{
ecs_->print_stats(os);
os << suffix.size() << " states in suffix" << std::endl;
os << period.size() << " states in period" << std::endl;
}
}

68
src/tgbaalgos/gtec/ce.hh Normal file
View file

@ -0,0 +1,68 @@
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// 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 2 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 Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#ifndef SPOT_TGBAALGOS_GTEC_CE_HH
# define SPOT_TGBAALGOS_GTEC_CE_HH
#include "status.hh"
#include "explscc.hh"
namespace spot
{
class counter_example
{
public:
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;
typedef std::list<state_proposition> cycle_path;
state_sequence suffix;
cycle_path period;
/// \brief Display the example computed by counter_example().
///
/// \param restrict optional automaton to project the example on.
std::ostream& print_result(std::ostream& os,
const tgba* restrict = 0) const;
/// Output statistics about this object.
void print_stats(std::ostream& os) const;
protected:
/// Called by counter_example to find a path which traverses all
/// acceptance conditions in the accepted SCC.
void accepting_path (const explicit_connected_component* scc,
const state* start, bdd acc_to_traverse);
/// Complete a cycle that caraterise the period of the counter
/// example. Append a sequence to the path given by accepting_path.
void complete_cycle(const explicit_connected_component* scc,
const state* from, const state* to);
private:
const emptiness_check_status* ecs_;
};
}
#endif // SPOT_TGBAALGOS_GTEC_CE_HH

65
src/tgbaalgos/gtec/explscc.cc Normal file
View file

@ -0,0 +1,65 @@
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// 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 2 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 Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#include "explscc.hh"
namespace spot
{
const state*
connected_component_hash_set::has_state(const state* s) const
{
set_type::const_iterator it = states.find(s);
if (it != states.end())
{
if (s != *it)
delete s;
return *it;
}
else
return 0;
}
void
connected_component_hash_set::insert(const state* s)
{
states.insert(s);
}
//////////////////////////////////////////////////////////////////////
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;
}
}

89
src/tgbaalgos/gtec/explscc.hh Normal file
View file

@ -0,0 +1,89 @@
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// 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 2 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 Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#ifndef SPOT_TGBAALGOS_GTEC_EXPLSCC_HH
# define SPOT_TGBAALGOS_GTEC_EXPLSCC_HH
#include "misc/hash.hh"
#include "tgba/state.hh"
#include "sccstack.hh"
namespace spot
{
/// An SCC storing all its states explicitly.
class explicit_connected_component: public scc_stack::connected_component
{
public:
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
/// s if it is different (acting like
/// numbered_state_heap::filter), or 0 otherwise.
virtual const state* has_state(const state* s) const = 0;
/// Insert a new state in the SCC.
virtual void insert(const state* s) = 0;
};
/// A straightforward implementation of explicit_connected_component
/// using a hash.
class connected_component_hash_set: public explicit_connected_component
{
public:
virtual ~connected_component_hash_set() {}
virtual const state* has_state(const state* s) const;
virtual void insert(const state* s);
protected:
typedef Sgi::hash_set<const state*,
state_ptr_hash, state_ptr_equal> set_type;
set_type states;
};
/// Abstract factory for explicit_connected_component.
class explicit_connected_component_factory
{
public:
virtual ~explicit_connected_component_factory() {}
/// Create an explicit_connected_component.
virtual explicit_connected_component* build() const = 0;
};
/// \brief Factory for connected_component_hash_set.
///
/// This class is a singleton. Retrieve the instance using instance().
class connected_component_hash_set_factory :
public explicit_connected_component_factory
{
public:
virtual connected_component_hash_set* build() const;
/// Get the unique instance of this class.
static const connected_component_hash_set_factory* instance();
protected:
virtual ~connected_component_hash_set_factory() {}
/// Construction is forbiden.
connected_component_hash_set_factory();
};
}
#endif // SPOT_TGBAALGOS_GTEC_EXPLSCC_HH

414
src/tgbaalgos/gtec/gtec.cc Normal file
View file

@ -0,0 +1,414 @@
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// 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 2 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 Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#include "gtec.hh"
namespace spot
{
namespace
{
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);
}
emptiness_check::~emptiness_check()
{
delete ecs_;
}
void
emptiness_check::remove_component(const state* from)
{
// Remove from H all states which are reachable from state FROM.
// Stack of iterators towards states to remove.
std::stack<tgba_succ_iterator*> to_remove;
// Remove FROM itself, and prepare to remove its successors.
// (FROM should be in H, otherwise it means all reachable
// states from FROM have already been removed and there is no
// point in calling remove_component.)
int* hi = ecs_->h.find(from);
assert(hi);
assert(*hi != -1);
*hi = -1;
tgba_succ_iterator* i = ecs_->aut->succ_iter(from);
for (;;)
{
// Remove each destination of this iterator.
for (i->first(); !i->done(); i->next())
{
state* s = i->current_state();
int *hi = ecs_->h.find(s);
assert(hi);
if (*hi != -1)
{
*hi = -1;
to_remove.push(ecs_->aut->succ_iter(s));
}
delete s;
}
delete i;
if (to_remove.empty())
break;
i = to_remove.top();
to_remove.pop();
}
}
bool
emptiness_check::check()
{
// We use five main data in this algorithm:
// * emptiness_check::root, a stack of strongly connected components (SCC),
// * emptiness_check::h, a hash of all visited nodes, with their order,
// (it is called "Hash" in Couvreur's paper)
// * arc, a stack of acceptance conditions between each of these SCC,
std::stack<bdd> arc;
// * num, the number of visited nodes. Used to set the order of each
// visited node,
int num = 1;
// * todo, the depth-first search stack. This holds pairs of the
// form (STATE, ITERATOR) where ITERATOR is a tgba_succ_iterator
// over the successors of STATE. In our use, ITERATOR should
// always be freed when TODO is popped, but STATE should not because
// it is also used as a key in H.
std::stack<pair_state_iter> todo;
// Setup depth-first search from the initial state.
{
state* init = ecs_->aut->get_init_state();
ecs_->h.insert(init, 1);
ecs_->root.push(1);
arc.push(bddfalse);
tgba_succ_iterator* iter = ecs_->aut->succ_iter(init);
iter->first();
todo.push(pair_state_iter(init, iter));
}
while (!todo.empty())
{
assert(ecs_->root.size() == arc.size());
// We are looking at the next successor in SUCC.
tgba_succ_iterator* succ = todo.top().second;
// If there is no more successor, backtrack.
if (succ->done())
{
// We have explored all successors of state CURR.
const state* curr = todo.top().first;
// Backtrack TODO.
todo.pop();
// When backtracking the root of an SCC, we must also
// remove that SCC from the ARC/ROOT stacks. We must
// discard from H all reachable states from this SCC.
int* i = ecs_->h.find(curr);
assert(i);
assert(!ecs_->root.empty());
if (ecs_->root.top().index == *i)
{
assert(!arc.empty());
arc.pop();
ecs_->root.pop();
remove_component(curr);
}
delete succ;
// Do not delete CURR: it is a key in H.
continue;
}
// We have a successor to look at. Fetch the values
// (destination state, acceptance conditions of the arc)
// we are interested in...
const state* dest = succ->current_state();
bdd acc = succ->current_acceptance_conditions();
// ... and point the iterator to the next successor, for
// the next iteration.
succ->next();
// We do not need SUCC from now on.
// Are we going to a new state?
int* i = ecs_->h.find(dest);
if (!i)
{
// Yes. Number it, stack it, and register its successors
// for later processing.
ecs_->h.insert(dest, ++num);
ecs_->root.push(num);
arc.push(acc);
tgba_succ_iterator* iter = ecs_->aut->succ_iter(dest);
iter->first();
todo.push(pair_state_iter(dest, iter));
continue;
}
// We know the state exists. Since a state can have several
// representations (i.e., objects), make sure we delete
// anything but the first one seen (the one used as key in H).
(void) ecs_->h.filter(dest);
// If we have reached a dead component, ignore it.
if (*i == -1)
continue;
// Now this is the most interesting case. We have reached a
// state S1 which is already part of a non-dead SCC. Any such
// non-dead SCC has necessarily been crossed by our path to
// this state: there is a state S2 in our path which belongs
// to this SCC too. We are going to merge all states between
// this S1 and S2 into this SCC.
//
// This merge is easy to do because the order of the SCC in
// ROOT is ascending: we just have to merge all SCCs from the
// top of ROOT that have an index greater to the one of
// the SCC of S2 (called the "threshold").
int threshold = *i;
while (threshold < ecs_->root.top().index)
{
assert(!ecs_->root.empty());
assert(!arc.empty());
acc |= ecs_->root.top().condition;
acc |= arc.top();
ecs_->root.pop();
arc.pop();
}
// Note that we do not always have
// threshold == ecs_->root.top().index
// after this loop, the SCC whose index is threshold might have
// been merged with a lower SCC.
// Accumulate all acceptance conditions into the merged SCC.
ecs_->root.top().condition |= acc;
if (ecs_->root.top().condition
== ecs_->aut->all_acceptance_conditions())
{
// We have found an accepting SCC.
// Release all iterators in TODO.
while (!todo.empty())
{
delete todo.top().second;
todo.pop();
}
return false;
}
}
// This automaton recognizes no word.
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;
successor(bdd acc, const spot::state* s): acc(acc), s(s) {}
};
bool
emptiness_check_shy::check()
{
// We use five main data in this algorithm:
// * emptiness_check::root, a stack of strongly connected components (SCC),
// * emptiness_check::h, a hash of all visited nodes, with their order,
// (it is called "Hash" in Couvreur's paper)
// * arc, a stack of acceptance conditions between each of these SCC,
std::stack<bdd> arc;
// * num, the number of visited nodes. Used to set the order of each
// visited node,
int num = 1;
// * todo, the depth-first search stack. This holds pairs of the
// form (STATE, SUCCESSORS) where SUCCESSORS is a list of
// (ACCEPTANCE_CONDITIONS, STATE) pairs.
typedef std::list<successor> succ_queue;
typedef std::pair<const state*, succ_queue> pair_state_successors;
std::stack<pair_state_successors> todo;
// Setup depth-first search from the initial state.
todo.push(pair_state_successors(0, succ_queue()));
todo.top().second.push_front(successor(bddtrue,
ecs_->aut->get_init_state()));
for (;;)
{
assert(ecs_->root.size() == arc.size());
// Get the successors of the current state.
succ_queue& queue = todo.top().second;
// First, we process all successors that we have already seen.
// This is an idea from Soheib Baarir. It helps to merge SCCs
// and get shorter traces faster.
succ_queue::iterator q = queue.begin();
while (q != queue.end())
{
int* i = ecs_->h.find(q->s);
if (!i)
{
// Skip unknown states.
++q;
continue;
}
// Skip states from dead SCCs.
if (*i != -1)
{
// Now this is the most interesting case. We have
// reached a state S1 which is already part of a
// non-dead SCC. Any such non-dead SCC has
// necessarily been crossed by our path to this
// state: there is a state S2 in our path which
// belongs to this SCC too. We are going to merge
// all states between this S1 and S2 into this
// SCC.
//
// This merge is easy to do because the order of
// the SCC in ROOT is ascending: we just have to
// merge all SCCs from the top of ROOT that have
// an index greater to the one of the SCC of S2
// (called the "threshold").
int threshold = *i;
bdd acc = q->acc;
while (threshold < ecs_->root.top().index)
{
assert(!ecs_->root.empty());
assert(!arc.empty());
acc |= ecs_->root.top().condition;
acc |= arc.top();
ecs_->root.pop();
arc.pop();
}
// Note that we do not always have
// threshold == ecs_->root.top().index
// after this loop, the SCC whose index is threshold
// might have been merged with a lower SCC.
// Accumulate all acceptance conditions into the
// merged SCC.
ecs_->root.top().condition |= acc;
if (ecs_->root.top().condition
== ecs_->aut->all_acceptance_conditions())
{
// We have found an accepting SCC. Clean up TODO.
// We must delete all states of apparing in TODO
// unless they are used as keys in H.
while (!todo.empty())
{
succ_queue& queue = todo.top().second;
for (succ_queue::iterator q = queue.begin();
q != queue.end(); ++q)
{
int* i = ecs_->h.find(q->s);
if (!i)
delete q->s;
else
// Delete the state if it is a clone
// of a state in the heap.
(void) ecs_->h.filter(q->s);
}
todo.pop();
}
return false;
}
}
// We know the state exists. Since a state can have several
// representations (i.e., objects), make sure we delete
// anything but the first one seen (the one used as key in H).
(void) ecs_->h.filter(q->s);
// Remove that state from the queue, so we do not
// recurse into it.
succ_queue::iterator old = q++;
queue.erase(old);
}
// If there is no more successor, backtrack.
if (queue.empty())
{
// We have explored all successors of state CURR.
const state* curr = todo.top().first;
// Backtrack TODO.
todo.pop();
if (todo.empty())
// This automaton recognizes no word.
return true;
// When backtracking the root of an SCC, we must also
// remove that SCC from the ARC/ROOT stacks. We must
// discard from H all reachable states from this SCC.
int* i = ecs_->h.find(curr);
assert(i);
assert(!ecs_->root.empty());
if (ecs_->root.top().index == *i)
{
assert(!arc.empty());
arc.pop();
ecs_->root.pop();
remove_component(curr);
}
continue;
}
// Recurse. (Finally!)
// Pick one successor off the list, and schedule its
// successors first on TODO. Update the various hashes and
// stacks.
successor succ = queue.front();
queue.pop_front();
ecs_->h.insert(succ.s, ++num);
ecs_->root.push(num);
arc.push(succ.acc);
todo.push(pair_state_successors(succ.s, succ_queue()));
succ_queue& new_queue = todo.top().second;
tgba_succ_iterator* iter = ecs_->aut->succ_iter(succ.s);
for (iter->first(); ! iter->done(); iter->next())
new_queue.push_back(successor(iter->current_acceptance_conditions(),
iter->current_state()));
delete iter;
}
}
}

114
src/tgbaalgos/gtec/gtec.hh Normal file
View file

@ -0,0 +1,114 @@
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// 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 2 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 Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#ifndef SPOT_TGBAALGOS_GTEC_GTEC_HH
# define SPOT_TGBAALGOS_GTEC_GTEC_HH
#include "status.hh"
namespace spot
{
/// \brief Check whether the language of an automate is empty.
///
/// This is based on the following paper.
/// \verbatim
/// @InProceedings{couvreur.99.fm,
/// author = {Jean-Michel Couvreur},
/// title = {On-the-fly Verification of Temporal Logic},
/// pages = {253--271},
/// editor = {Jeannette M. Wing and Jim Woodcock and Jim Davies},
/// booktitle = {Proceedings of the World Congress on Formal Methods in
/// the Development of Computing Systems (FM'99)},
/// publisher = {Springer-Verlag},
/// series = {Lecture Notes in Computer Science},
/// volume = {1708},
/// year = {1999},
/// address = {Toulouse, France},
/// month = {September},
/// 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 is available
/// using result() (spot::counter_example needs it).
///
/// There are two variants of this algorithm: spot::emptiness_check and
/// spot::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.
///
/// spot::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.
///
/// spot::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);
virtual ~emptiness_check();
/// Check whether the automaton's language is empty.
virtual bool check();
/// \brief Return the status of the emptiness-check.
///
/// When check() succeed, the status should be passed along
/// to spot::counter_example.
///
/// This status should not be deleted, it is a pointer
/// to a member of this class that will be deleted when
/// the emptiness_check object is deleted.
const emptiness_check_status* result() const;
protected:
emptiness_check_status* ecs_;
/// \brief Remove a strongly component from the hash.
///
/// This function remove all accessible state from a given
/// state. In other words, it removes the strongly connected
/// component that contains this state.
void remove_component(const state* start_delete);
};
/// \brief A version of spot::emptiness_check try to visit known
/// states first.
///
/// See the documentation for spot::emptiness_check
class emptiness_check_shy : public emptiness_check
{
public:
emptiness_check_shy(const tgba* a);
virtual ~emptiness_check_shy();
virtual bool check();
};
}
#endif // SPOT_TGBAALGOS_GTEC_GTEC_HH

133
src/tgbaalgos/gtec/nsheap.cc Normal file
View file

@ -0,0 +1,133 @@
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// 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 2 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 Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#include "nsheap.hh"
namespace spot
{
class numbered_state_heap_hash_map_const_iterator :
public numbered_state_heap_const_iterator
{
public:
numbered_state_heap_hash_map_const_iterator
(const numbered_state_heap_hash_map::hash_type& h)
: numbered_state_heap_const_iterator(), h(h)
{
}
~numbered_state_heap_hash_map_const_iterator()
{
}
virtual void
first()
{
i = h.begin();
}
virtual void
next()
{
++i;
}
virtual bool
done() const
{
return i == h.end();
}
virtual const state*
get_state() const
{
return i->first;
}
virtual int
get_index() const
{
return i->second;
}
private:
numbered_state_heap_hash_map::hash_type::const_iterator i;
const numbered_state_heap_hash_map::hash_type& h;
};
numbered_state_heap_hash_map::~numbered_state_heap_hash_map()
{
// Free keys in H.
hash_type::iterator i = h.begin();
while (i != h.end())
{
// Advance the iterator before deleting the key.
const state* s = i->first;
++i;
delete s;
}
}
const int*
numbered_state_heap_hash_map::find(const state* s) const
{
hash_type::const_iterator i = h.find(s);
if (i == h.end())
return 0;
return &i->second;
}
int*
numbered_state_heap_hash_map::find(const state* s)
{
hash_type::iterator i = h.find(s);
if (i == h.end())
return 0;
return &i->second;
}
void
numbered_state_heap_hash_map::insert(const state* s, int index)
{
h[s] = index;
}
int
numbered_state_heap_hash_map::size() const
{
return h.size();
}
numbered_state_heap_const_iterator*
numbered_state_heap_hash_map::iterator() const
{
return new numbered_state_heap_hash_map_const_iterator(h);
}
const state*
numbered_state_heap_hash_map::filter(const state* s) const
{
hash_type::const_iterator i = h.find(s);
assert(i != h.end());
if (s != i->first)
delete s;
return i->first;
}
}

108
src/tgbaalgos/gtec/nsheap.hh Normal file
View file

@ -0,0 +1,108 @@
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// 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 2 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 Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#ifndef SPOT_TGBAALGOS_GTEC_NSHEAP_HH
# define SPOT_TGBAALGOS_GTEC_NSHEAP_HH
#include "tgba/state.hh"
#include "misc/hash.hh"
namespace spot
{
/// Iterator on numbered_state_heap objects.
class numbered_state_heap_const_iterator
{
public:
virtual ~numbered_state_heap_const_iterator() {}
//@{
/// Iteration
virtual void first() = 0;
virtual void next() = 0;
virtual bool done() const = 0;
//@}
//@{
/// Inspection
virtual const state* get_state() const = 0;
virtual int get_index() const = 0;
//@}
};
/// Keep track of a large quantity of indexed states.
class numbered_state_heap
{
public:
virtual ~numbered_state_heap() {}
//@{
/// \brief Is state in the heap?
///
/// Returns 0 if \a s is not in the heap. or a pointer to
/// its number if it is.
virtual const int* find(const state* s) const = 0;
virtual int* find(const state* s) = 0;
//@}
/// Add a new state \a s with index \a index
virtual void insert(const state* s, int index) = 0;
/// The number of stored states.
virtual int size() const = 0;
/// Return an iterator on the states/indexes pairs.
virtual numbered_state_heap_const_iterator* iterator() const = 0;
/// \brief Filter state clones.
///
/// Return a state which is equal to \a s, but is an actual key in
/// the heap, and free \a s if it is a clone of that state.
///
/// Doing so simplify memory management, because we don't have to
/// track which state need to be kept or deallocated: all key in
/// the heap should last for the whole life of the emptiness-check.
virtual const state* filter(const state* s) const = 0;
};
/// A straightforward implementation of numbered_state_heap with a hash map.
class numbered_state_heap_hash_map : public numbered_state_heap
{
public:
virtual ~numbered_state_heap_hash_map();
virtual const int* find(const state* s) const;
virtual int* find(const state* s);
virtual void insert(const state* s, int index);
virtual int size() const;
virtual numbered_state_heap_const_iterator* iterator() const;
virtual const state* filter(const state* s) const;
protected:
typedef Sgi::hash_map<const state*, int,
state_ptr_hash, state_ptr_equal> hash_type;
hash_type h; ///< Map of visited states.
friend class numbered_state_heap_hash_map_const_iterator;
};
}
#endif // SPOT_TGBAALGOS_GTEC_NSHEAP_HH

61
src/tgbaalgos/gtec/sccstack.cc Normal file
View file

@ -0,0 +1,61 @@
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// 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 2 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 Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#include "sccstack.hh"
namespace spot
{
scc_stack::connected_component::connected_component(int i)
{
index = i;
condition = bddfalse;
}
scc_stack::connected_component&
scc_stack::top()
{
return s.top();
}
void
scc_stack::pop()
{
s.pop();
}
void
scc_stack::push(int index)
{
s.push(connected_component(index));
}
size_t
scc_stack::size() const
{
return s.size();
}
bool
scc_stack::empty() const
{
return s.empty();
}
}

67
src/tgbaalgos/gtec/sccstack.hh Normal file
View file

@ -0,0 +1,67 @@
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// 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 2 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 Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#ifndef SPOT_TGBAALGOS_GTEC_SCCSTACK_HH
# define SPOT_TGBAALGOS_GTEC_SCCSTACK_HH
#include <stack>
#include <bdd.h>
namespace spot
{
// A stack of Strongly-Connected Components, as needed by the
// Tarjan-Couvreur algorithm.
class scc_stack
{
public:
struct connected_component
{
public:
connected_component(int index = -1);
/// Index of the SCC.
int index;
/// The bdd condition is the union of all acceptance conditions of
/// transitions which connect the states of the connected component.
bdd condition;
};
/// Stack a new SCC with index \a index.
void push(int index);
/// Access the top SCC.
connected_component& top();
/// Pop the top SCC.
void pop();
/// How many SCC are in stack.
size_t size() const;
/// Is the stack empty?
bool empty() const;
typedef std::stack<connected_component> stack_type;
stack_type s;
};
}
#endif // SPOT_TGBAALGOS_GTEC_SCCSTACK_HH

43
src/tgbaalgos/gtec/status.cc Normal file
View file

@ -0,0 +1,43 @@
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// 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 2 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 Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#include "status.hh"
namespace spot
{
emptiness_check_status::emptiness_check_status(const tgba* aut)
: aut(aut)
{
}
emptiness_check_status::~emptiness_check_status()
{
}
void
emptiness_check_status::print_stats(std::ostream& os) const
{
os << h.size() << " unique states visited" << std::endl;
os << root.size()
<< " strongly connected components in search stack"
<< std::endl;
}
}

53
src/tgbaalgos/gtec/status.hh Normal file
View file

@ -0,0 +1,53 @@
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie.
//
// 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 2 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 Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#ifndef SPOT_TGBAALGOS_GTEC_STATUS_HH
# define SPOT_TGBAALGOS_GTEC_STATUS_HH
#include "sccstack.hh"
#include "nsheap.hh"
#include "tgba/tgba.hh"
#include <iostream>
namespace spot
{
/// \brief The status of the emptiness-check on success.
///
/// This contains everything needed to construct a counter-example:
/// the automata, the stack of SCCs traversed by the counter-example,
/// and the heap of visited states with their indexes.
class emptiness_check_status
{
public:
emptiness_check_status(const tgba* aut);
~emptiness_check_status();
const tgba* aut;
scc_stack root;
numbered_state_heap_hash_map h; ///< Map of visited states.
/// Output statistics about this object.
void print_stats(std::ostream& os) const;
};
}
#endif // SPOT_TGBAALGOS_GTEC_STATUS_HH

3
src/tgbatest/ltl2tgba.cc
View file

@ -33,7 +33,8 @@
#include "tgbaalgos/lbtt.hh" #include "tgbaalgos/lbtt.hh"
#include "tgba/tgbatba.hh" #include "tgba/tgbatba.hh"
#include "tgbaalgos/magic.hh" #include "tgbaalgos/magic.hh"
#include "tgbaalgos/emptinesscheck.hh" #include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/gtec/ce.hh"
#include "tgbaparse/public.hh" #include "tgbaparse/public.hh"
#include "tgbaalgos/dupexp.hh" #include "tgbaalgos/dupexp.hh"