Commit 6c815004 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

Introduce an emptiness-check interface, and modify the existing

algorithms to conform to it, uniformly.  This will unfortunately
break third-party code that were using these algorithms.
* src/tgbaalgos/emptiness.cc, src/tgbaalgos/emptiness.hh: New files.
* src/tgbaalgos/Makefile.am: New files.
* src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh: Adjust to
conform to the new emptiness-check interface.
* src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh,
src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh,
src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh:
Likewise.  The classes have been renamed are as following
  emptiness_check -> couvreur99_check
  emptiness_check_shy -> couvreur99_check_shy
  counter_example -> couvreur99_check_result
* src/tgbatest/ltl2tgba.cc, iface/gspn/ltlgspn.cc, iface/gspn/ssp.hh,
iface/gspn/ssp.cc: Adjust to renaming and new interface.
parent 7010a02c
2004-10-27 Alexandre Duret-Lutz <adl@src.lip6.fr>
Introduce an emptiness-check interface, and modify the existing
algorithms to conform to it, uniformly. This will unfortunately
break third-party code that were using these algorithms.
* src/tgbaalgos/emptiness.cc, src/tgbaalgos/emptiness.hh: New files.
* src/tgbaalgos/Makefile.am: New files.
* src/tgbaalgos/magic.cc, src/tgbaalgos/magic.hh: Adjust to
conform to the new emptiness-check interface.
* src/tgbaalgos/gtec/ce.cc, src/tgbaalgos/gtec/ce.hh,
src/tgbaalgos/gtec/gtec.cc, src/tgbaalgos/gtec/gtec.hh,
src/tgbaalgos/gtec/status.cc, src/tgbaalgos/gtec/status.hh:
Likewise. The classes have been renamed are as following
emptiness_check -> couvreur99_check
emptiness_check_shy -> couvreur99_check_shy
emptiness_check_status -> couvreur99_check_status
counter_example -> couvreur99_check_result
* src/tgbatest/ltl2tgba.cc, iface/gspn/ltlgspn.cc, iface/gspn/ssp.hh,
iface/gspn/ssp.cc: Adjust to renaming and new interface.
* src/evtgbaalgos/tgba2evtgba.cc, src/evtgbaalgos/tgba2evtgba.hh:
New files.
* src/evtgbaalgos/Makefile.am (evtgbaalgos_HEADERS,
......
......@@ -216,25 +216,25 @@ main(int argc, char **argv)
case Couvreur4:
case Couvreur5:
{
spot::emptiness_check* ec;
spot::couvreur99_check* ec;
switch (check)
{
case Couvreur:
ec = new spot::emptiness_check(prod);
ec = new spot::couvreur99_check(prod);
break;
case Couvreur2:
ec = new spot::emptiness_check_shy(prod);
ec = new spot::couvreur99_check_shy(prod);
break;
#ifdef SSP
case Couvreur3:
ec = spot::emptiness_check_ssp_semi(prod);
ec = spot::couvreur99_check_ssp_semi(prod);
break;
case Couvreur4:
ec = spot::emptiness_check_ssp_shy_semi(prod);
ec = spot::couvreur99_check_ssp_shy_semi(prod);
break;
case Couvreur5:
ec = spot::emptiness_check_ssp_shy(prod);
ec = spot::couvreur99_check_ssp_shy(prod);
break;
#endif
default:
......@@ -244,30 +244,32 @@ main(int argc, char **argv)
ec = 0;
}
bool res = ec->check();
const spot::emptiness_check_status* ecs = ec->result();
if (!res)
spot::emptiness_check_result* res = ec->check();
const spot::couvreur99_check_status* ecs = ec->result();
if (res)
{
if (compute_counter_example)
{
spot::counter_example* ce;
spot::couvreur99_check_result* ce;
#ifndef SSP
ce = new spot::counter_example(ecs);
ce = new spot::couvreur99_check_result(ecs);
#else
switch (check)
{
case Couvreur:
case Couvreur2:
case Couvreur5:
ce = new spot::counter_example(ecs);
ce = new spot::couvreur99_check_result(ecs);
break;
default:
ce = spot::counter_example_ssp(ecs);
}
#endif
ce->print_result(std::cout, proj ? model : 0);
spot::tgba_run* run = ce->accepting_run();
// FIXME: reimplement the projection
spot::print_tgba_run(std::cout, run, prod);
ce->print_stats(std::cout);
delete run;
delete ce;
}
else
......@@ -275,6 +277,7 @@ main(int argc, char **argv)
std::cout << "non empty" << std::endl;
ecs->print_stats(std::cout);
}
delete res;
}
else
{
......@@ -283,7 +286,7 @@ main(int argc, char **argv)
}
std::cout << std::endl;
delete ec;
if (!res)
if (res)
exit(1);
}
break;
......@@ -292,12 +295,19 @@ main(int argc, char **argv)
spot::tgba_tba_proxy* d = new spot::tgba_tba_proxy(prod);
spot::magic_search ms(d);
if (ms.check())
spot::emptiness_check_result* res = ms.check();
if (res)
{
if (compute_counter_example)
ms.print_result (std::cout, proj ? model : 0);
{
spot::tgba_run* run = res->accepting_run();
// FIXME: reimplement the projection
spot::print_tgba_run(std::cout, run, prod);
delete run;
}
else
std::cout << "non-empty" << std::endl;
delete res;
exit(1);
}
else
......
......@@ -802,7 +802,7 @@ namespace spot
hash_type h; ///< Map of visited states.
friend class numbered_state_heap_ssp_const_iterator;
friend class emptiness_check_shy_ssp;
friend class couvreur99_check_shy_ssp;
};
......@@ -896,12 +896,12 @@ namespace spot
};
class emptiness_check_shy_ssp : public emptiness_check_shy
class couvreur99_check_shy_ssp : public couvreur99_check_shy
{
public:
emptiness_check_shy_ssp(const tgba* a)
: emptiness_check_shy(a,
numbered_state_heap_ssp_factory_semi::instance())
couvreur99_check_shy_ssp(const tgba* a)
: couvreur99_check_shy(a,
numbered_state_heap_ssp_factory_semi::instance())
{
}
......@@ -976,36 +976,37 @@ namespace spot
emptiness_check*
emptiness_check_ssp_semi(const tgba* ssp_automata)
couvreur99_check*
couvreur99_check_ssp_semi(const tgba* ssp_automata)
{
assert(dynamic_cast<const tgba_gspn_ssp*>(ssp_automata));
return
new emptiness_check(ssp_automata,
numbered_state_heap_ssp_factory_semi::instance());
new couvreur99_check(ssp_automata,
numbered_state_heap_ssp_factory_semi::instance());
}
emptiness_check*
emptiness_check_ssp_shy_semi(const tgba* ssp_automata)
couvreur99_check*
couvreur99_check_ssp_shy_semi(const tgba* ssp_automata)
{
assert(dynamic_cast<const tgba_gspn_ssp*>(ssp_automata));
return
new emptiness_check_shy
(ssp_automata,
new couvreur99_check_shy
(ssp_automata,
numbered_state_heap_ssp_factory_semi::instance());
}
emptiness_check*
emptiness_check_ssp_shy(const tgba* ssp_automata)
couvreur99_check*
couvreur99_check_ssp_shy(const tgba* ssp_automata)
{
assert(dynamic_cast<const tgba_gspn_ssp*>(ssp_automata));
return new emptiness_check_shy_ssp(ssp_automata);
return new couvreur99_check_shy_ssp(ssp_automata);
}
counter_example*
counter_example_ssp(const emptiness_check_status* status)
couvreur99_check_result*
counter_example_ssp(const couvreur99_check_status* status)
{
return new counter_example(status,
connected_component_ssp_factory::instance());
return new
couvreur99_check_result(status,
connected_component_ssp_factory::instance());
}
}
......@@ -48,11 +48,12 @@ namespace spot
const ltl::declarative_environment& env_;
};
emptiness_check* emptiness_check_ssp_semi(const tgba* ssp_automata);
emptiness_check* emptiness_check_ssp_shy_semi(const tgba* ssp_automata);
emptiness_check* emptiness_check_ssp_shy(const tgba* ssp_automata);
couvreur99_check* couvreur99_check_ssp_semi(const tgba* ssp_automata);
couvreur99_check* couvreur99_check_ssp_shy_semi(const tgba* ssp_automata);
couvreur99_check* couvreur99_check_ssp_shy(const tgba* ssp_automata);
counter_example* counter_example_ssp(const emptiness_check_status* status);
couvreur99_check_result*
counter_example_ssp(const couvreur99_check_status* status);
}
#endif // SPOT_IFACE_GSPN_SSP_GSPN_SSP_HH
......@@ -29,6 +29,7 @@ tgbaalgosdir = $(pkgincludedir)/tgbaalgos
tgbaalgos_HEADERS = \
dotty.hh \
dupexp.hh \
emptiness.hh \
lbtt.hh \
ltl2tgba_fm.hh \
ltl2tgba_lacim.hh \
......@@ -44,6 +45,7 @@ noinst_LTLIBRARIES = libtgbaalgos.la
libtgbaalgos_la_SOURCES = \
dotty.cc \
dupexp.cc \
emptiness.cc \
lbtt.cc \
ltl2tgba_fm.cc \
ltl2tgba_lacim.cc \
......
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// dpartement Systmes Rpartis Coopratifs (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 "emptiness.hh"
#include "tgba/tgba.hh"
#include "tgba/bddprint.hh"
namespace spot
{
tgba_run::~tgba_run()
{
for (steps::const_iterator i = prefix.begin(); i != prefix.end(); ++i)
delete i->s;
for (steps::const_iterator i = cycle.begin(); i != cycle.end(); ++i)
delete i->s;
}
tgba_run::tgba_run(const tgba_run& run)
{
for (steps::const_iterator i = run.prefix.begin();
i != run.prefix.end(); ++i)
{
step s = { s.s->clone(), i->label, i->acc };
prefix.push_back(s);
}
for (steps::const_iterator i = run.cycle.begin();
i != run.cycle.end(); ++i)
{
step s = { s.s->clone(), i->label, i->acc };
cycle.push_back(s);
}
}
std::ostream& print_tgba_run(std::ostream& os,
const tgba_run* run,
const tgba* a)
{
bdd_dict* d = a->get_dict();
os << "Prefix:" << std::endl;
for (tgba_run::steps::const_iterator i = run->prefix.begin();
i != run->prefix.end(); ++i)
{
os << " " << a->format_state(i->s) << std::endl;
os << " | ";
bdd_print_set(os, d, i->label);
os << "\t";
bdd_print_accset(os, d, i->acc);
os << std::endl;
}
os << "Cycle:" << std::endl;
for (tgba_run::steps::const_iterator i = run->cycle.begin();
i != run->cycle.end(); ++i)
{
os << " " << a->format_state(i->s) << std::endl;
os << " | ";
bdd_print_set(os, d, i->label);
os << "\t";
bdd_print_accset(os, d, i->acc);
os << std::endl;
}
return os;
}
tgba_run&
tgba_run::operator=(const tgba_run& run)
{
if (&run != this)
{
this->~tgba_run();
new(this) tgba_run(run);
}
return *this;
}
tgba_run*
emptiness_check_result::accepting_run()
{
return 0;
}
emptiness_check::~emptiness_check()
{
}
std::ostream&
emptiness_check::print_stats(std::ostream& os) const
{
return os;
}
}
// 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_EMPTINESS_HH
# define SPOT_TGBAALGOS_EMPTINESS_HH
#include <list>
#include <iosfwd>
#include <bdd.h>
#include "tgba/state.hh"
namespace spot
{
/// An accepted run, for a tgba.
struct tgba_run
{
struct step {
const state* s;
bdd label;
bdd acc;
};
typedef std::list<step> steps;
steps prefix;
steps cycle;
~tgba_run();
tgba_run()
{
};
tgba_run(const tgba_run& run);
tgba_run& operator=(const tgba_run& run);
};
class tgba;
std::ostream& print_tgba_run(std::ostream& os,
const tgba_run* run,
const tgba* a);
/// \brief The result of an emptiness check.
///
/// Instances of these class should not last longer than the
/// instances of emptiness_check that produced them as they
/// may reference data internal to the check.
class emptiness_check_result
{
public:
/// \brief Return a run accepted by the automata passed to
/// the emptiness check.
///
/// This method might actually compute the acceptance run. (Not
/// all emptiness check algorithms actually produce a
/// counter-example as a side-effect of checking emptiness, some
/// need some post-processing.)
///
/// This can also return 0 if the emptiness check algorithm
/// cannot produce a counter example (that does not mean there
/// is no counter-example; the mere existence of an instance of
/// this class asserts the existence of a counter-example).
virtual tgba_run* accepting_run();
};
/// Common interface to emptiness check algorithms.
class emptiness_check
{
public:
virtual ~emptiness_check();
/// \brief Check whether the automaton contain an accepting run.
///
/// Return 0 if the automaton accept no run. Return an instance
/// of emptiness_check_result otherwise. This instance might
/// allow to obtain one sample acceptance run. The result has to
/// be destroyed before the emptiness_check instance that
/// generated it.
///
/// Some emptiness_check algorithms may allow check() to be called
/// several time, but generally you should not assume that.
virtual emptiness_check_result* check() = 0;
/// Print statistics, if any.
virtual std::ostream& print_stats(std::ostream& os) const;
};
}
#endif // SPOT_TGBAALGOS_EMPTINESS_HH
......@@ -28,15 +28,22 @@ namespace spot
namespace
{
typedef std::pair<const spot::state*, tgba_succ_iterator*> pair_state_iter;
typedef std::pair<const state*, bdd> state_proposition;
}
counter_example::counter_example(const emptiness_check_status* ecs,
const explicit_connected_component_factory*
eccf)
: ecs_(ecs)
couvreur99_check_result::couvreur99_check_result
(const couvreur99_check_status* ecs,
const explicit_connected_component_factory* eccf)
: ecs_(ecs), eccf_(eccf)
{
}
tgba_run*
couvreur99_check_result::accepting_run()
{
run_ = new tgba_run;
assert(!ecs_->root.empty());
assert(suffix.empty());
scc_stack::stack_type root = ecs_->root.s;
int comp_size = root.size();
......@@ -45,7 +52,7 @@ namespace spot
new explicit_connected_component*[comp_size];
for (int j = comp_size - 1; 0 <= j; --j)
{
scc[j] = eccf->build();
scc[j] = eccf_->build();
scc[j]->index = root.top().index;
scc[j]->condition = root.top().condition;
root.pop();
......@@ -74,7 +81,9 @@ namespace spot
numbered_state_heap::state_index_p spi =
ecs_->h->index(ecs_->aut->get_init_state());
assert(spi.first);
suffix.push_front(spi.first);
/// FIXME: Should compute label and acceptance condition.
tgba_run::step s = { spi.first, bddtrue, bddfalse };
run_->prefix.push_front(s);
// We build a path trough each SCC in the stack. For the
// first SCC, the starting state is the initial state of the
......@@ -93,7 +102,7 @@ namespace spot
father_map father;
// Initial state of the BFS.
const state* start = suffix.back();
const state* start = run_->prefix.back().s;
{
tgba_succ_iterator* i = ecs_->aut->succ_iter(start);
todo.push_back(pair_state_iter(start, i));
......@@ -114,20 +123,26 @@ namespace spot
if (!h_dest)
{
// If we have found a state in the next SCC.
// Unwind the path and populate SUFFIX.
// Unwind the path and populate RUN_->PREFIX.
h_dest = scc[k+1]->has_state(dest);
if (h_dest)
{
state_sequence seq;
tgba_run::steps seq;
seq.push_front(h_dest);
/// FIXME: Should compute label and acceptance
/// condition.
tgba_run::step s = { h_dest, bddtrue, bddfalse };
seq.push_front(s);
while (src->compare(start))
{
seq.push_front(src);
/// FIXME: Should compute label and acceptance
/// condition.
tgba_run::step s = { h_dest, bddtrue, bddfalse };
seq.push_front(s);
src = father[src];
}
// Append SEQ to SUFFIX.
suffix.splice(suffix.end(), seq);
// Append SEQ to RUN_->PREFIX.
run_->prefix.splice(run_->prefix.end(), seq);
// Exit this BFS for this SCC.
while (!todo.empty())
{
......@@ -152,24 +167,37 @@ namespace spot
}
}
accepting_path(scc[comp_size - 1], suffix.back(),
accepting_path(scc[comp_size - 1], run_->prefix.back().s,
scc[comp_size - 1]->condition);
run_->prefix.pop_back(); // this state belongs to the cycle.
for (int j = comp_size - 1; 0 <= j; --j)
delete scc[j];
delete[] scc;
// Clone every state in the run before returning it. (We didn't
// do that before in the algorithm, because it's easier to follow
// if every state manipulated is the instance in the hash table.)
for (tgba_run::steps::iterator i = run_->prefix.begin();
i != run_->prefix.end(); ++i)
i->s = i->s->clone();
for (tgba_run::steps::iterator i = run_->cycle.begin();
i != run_->cycle.end(); ++i)
i->s = i->s->clone();
return run_;
}
void
counter_example::complete_cycle(const explicit_connected_component* scc,
const state* from,
const state* to)
couvreur99_check_result::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
// If by chance our cycle already ends on the state we have
// to reach back, we are done.
if (from == to
&& !period.empty())
&& !run_->cycle.empty())
return;
// Records backlinks to parent state during the BFS.
......@@ -207,18 +235,22 @@ namespace spot
bdd cond = i->current_condition();
// If we have reached our destination, unwind the path
// and populate PERIOD.
// and populate RUN_->CYCLE.
if (h_dest == to)
{
cycle_path p;
p.push_front(state_proposition(h_dest, cond));
tgba_run::steps p;
// FIXME: should compute acceptance condition.
tgba_run::step s = { h_dest, cond, bddfalse };
p.push_front(s);
while (src != from)
{
const state_proposition& psi = father[src];
p.push_front(state_proposition(src, psi.second));
// FIXME: should compute acceptance condition.
tgba_run::step s = { src, psi.second, bddfalse };
p.push_front(s);
src = psi.first;
}
period.splice(period.end(), p);