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

Back out all Thomas's changes on emptiness checks since

Browse source 
2004-08-23.  Some of these will need to be reintegrated more
slowly and cleanly.

* src/tgbaalgos/Makefile.am, src/tgbaalgos/gtec/ce.cc,
src/tgbaalgos/gtec/ce.hh, src/tgbatest/Makefile.am,
src/tgbatest/emptchk.test, src/tgbatest/ltl2tgba.cc: Revert.
* src/tgbaalgos/colordfs.cc, src/tgbaalgos/colordfs.hh,
src/tgbaalgos/minimalce.cc, src/tgbaalgos/minimalce.hh,
src/tgbaalgos/nesteddfs.cc, src/tgbaalgos/nesteddfs.hh,
src/tgbaalgos/nesteddfsgen.cc, src/tgbaalgos/nesteddfsgen.hh,
src/tgbaalgos/tarjan_on_fly.cc, src/tgbaalgos/tarjan_on_fly.hh:
Delete.
This commit is contained in:
Alexandre Duret-Lutz 2004-10-15 10:33:55 +00:00
parent 01987350b7
commit ed6db92642
17 changed files with 48 additions and 3492 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/tgbaalgos/Makefile.am
View file

@ -27,43 +27,33 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS)
tgbaalgosdir = $(pkgincludedir)/tgbaalgos
tgbaalgos_HEADERS = \
colordfs.hh \
dotty.hh \
dupexp.hh \
lbtt.hh \
ltl2tgba_fm.hh \
ltl2tgba_lacim.hh \
magic.hh \
minimalce.hh \
nesteddfs.hh \
nesteddfsgen.hh \
neverclaim.hh \
powerset.hh \
reachiter.hh \
save.hh \
stats.hh \
reductgba_sim.hh \
tarjan_on_fly.hh
reductgba_sim.hh
noinst_LTLIBRARIES = libtgbaalgos.la
libtgbaalgos_la_SOURCES = \
colordfs.cc \
dotty.cc \
dupexp.cc \
lbtt.cc \
ltl2tgba_fm.cc \
ltl2tgba_lacim.cc \
magic.cc \
minimalce.cc \
nesteddfs.cc \
nesteddfsgen.cc \
neverclaim.cc \
powerset.cc \
reachiter.cc \
save.cc \
stats.cc \
reductgba_sim.cc \
reductgba_sim_del.cc \
tarjan_on_fly.cc
reductgba_sim_del.cc
libtgbaalgos_la_LIBADD = gtec/libgtec.la

435
src/tgbaalgos/colordfs.cc
View file

@ -1,435 +0,0 @@
// 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 <iterator>
#include <cassert>
#include "colordfs.hh"
#include "tgba/bddprint.hh"
namespace spot
{
colordfs_search::colordfs_search(const tgba_tba_proxy* a)
: a(a), x(0), counter_(0)
{
Maxdepth = -1;
}
colordfs_search::~colordfs_search()
{
hash_type::const_iterator s = h.begin();
while (s != h.end())
{
// Advance the iterator before deleting the "key" pointer.
const state* ptr = s->first;
++s;
delete ptr;
}
if (x)
delete x;
// Release all iterators on the stack.
while (!stack.empty())
{
delete stack.front().second;
stack.pop_front();
}
}
bool
colordfs_search::push(const state* s, color c)
{
tgba_succ_iterator* i = a->succ_iter(s);
i->first();
/*
hash_type::iterator hi = h.find(s);
if (hi != h.end())
if (hi->second.depth <= (int)stack.size())
//return false; // FIXME
return true;
*/
color_state cs = { c, true , stack.size() }; // FIXME
h[s] = cs;
stack.push_front(state_iter_pair(s, i));
// We build the counter example
bdd b = bddfalse;
if (!i->done()) // if the state is dead.
b = i->current_condition();
counter_->prefix.push_back(ce::state_ce(s->clone(), b));
return true;
}
void
colordfs_search::pop()
{
const state* s = stack.begin()->first;
tgba_succ_iterator* i = stack.begin()->second;
delete i;
//std::cout << "pop : " << a->format_state(s) << std::endl;
hash_type::iterator hi = h.find(s);
assert(hi != h.end());
hi->second.is_in_cp = false;
stack.pop_front();
//delete s;
// We build the counter example
delete counter_->prefix.back().first;
counter_->prefix.pop_back();
}
bool
colordfs_search::all_succ_black(const state* s)
{
bool return_value = true;
hash_type::iterator hi;
const state* s2;
tgba_succ_iterator* i = a->succ_iter(s);
int n = 0;
for (i->first(); !i->done(); i->next(), n++)
{
s2 = i->current_state();
hi = h.find(s2);
if (hi != h.end())
return_value &= (hi->second.c == black);
else
return_value = false;
delete s2;
}
delete i;
hi = h.find(s);
assert(hi != h.end());
if (return_value)
hi->second.c = black;
return return_value;
}
ce::counter_example*
colordfs_search::check()
{
clock();
counter_ = new ce::counter_example(a);
const state *s = a->get_init_state();
if (dfs_blue_min(s))
counter_->build_cycle(x);
else
{
delete counter_;
counter_ = 0;
}
tps_ = clock();
return counter_;
}
bool
colordfs_search::dfs_blue(const state* s, bdd)
{
std::cout << "dfs_blue : " << std::endl;
if (stack.empty())
// It's a new search.
push(a->get_init_state(), blue);
else
tstack.pop_front();
while (!stack.empty())
{
recurse:
tgba_succ_iterator *i = stack.front().second;
hash_type::iterator hi;
//std::cout << a->format_state(p.first) << std::endl;
while (!i->done())
{
const state* s2 = i->current_state();
hi = h.find(s2);
if (a->state_is_accepting(s2) &&
(hi != h.end() && hi->second.is_in_cp))
{
//ce::state_ce ce;
//ce = ce::state_ce(s2, i->current_condition());
x = const_cast<state*>(s2);
//push(s2, blue); //
//delete i;
return true;// a counter example is found !!
}
else if (hi == h.end() || hi->second.c == white)
{
push(s2, blue);
goto recurse;
}
else
delete s2;
i->next();
}
s = stack.front().first;
pop();
if (!all_succ_black(s) &&
a->state_is_accepting(s))
{
if (dfs_red(s))
return true;
hash_type::iterator hi = h.find(s);
assert(hi == h.end());
hi->second.c = black;
}
delete s; //
}
return false;
}
bool
colordfs_search::dfs_red(const state* s)
{
std::cout << "dfs_red : " << a->format_state(s) << std::endl;
if (!push(s, red))
return false;
hash_type::iterator hi;
tgba_succ_iterator* i = a->succ_iter(s);
int n = 0;
for (i->first(); !i->done(); i->next(), n++)
{
const state* s2 = i->current_state();
hi = h.find(s2);
if (hi != h.end() && hi->second.is_in_cp &&
(a->state_is_accepting(s2) ||
(hi->second.c == blue)))
{
//ce::state_ce ce;
//ce = ce::state_ce(s2->clone(), i->current_condition());
x = const_cast<state*>(s2);
delete i;
return true;// a counter example is found !!
}
if (hi != h.end() && hi->second.c == blue)
{
delete s2; // FIXME
if (dfs_red(hi->first))
{
delete i;
return true;
}
}
else
delete s2;
}
delete i;
hi = h.find(s);
assert(hi == h.end());
hi->second.c = black;
//std::cout << "dfs_red : pop" << std::endl;
pop();
return false;
}
///////////////////////////////////////////////////////////////////////
// for minimisation
bool
colordfs_search::dfs_blue_min(const state* s, bdd)
{
//std::cout << "dfs_blue : " << a->format_state(s) << std::endl;
if (!push(s, blue))
return false;
hash_type::iterator hi = h.find(s);
if (hi != h.end())
{
if (((int)stack.size() + 1) < hi->second.depth)
hi->second.depth = stack.size(); // for minimize
}
else
{
assert(0);
}
if (Maxdepth == -1 || ((int)stack.size() + 1 < Maxdepth))
{
tgba_succ_iterator* i = a->succ_iter(s);
int n = 0;
for (i->first(); !i->done(); i->next(), n++)
{
const state* s2 = i->current_state();
//std::cout << "s2 : " << a->format_state(s2) << std::endl;
hi = h.find(s2);
if (a->state_is_accepting(s2) &&
(hi != h.end() && hi->second.is_in_cp))
{
Maxdepth = stack.size();
ce::state_ce ce;
ce = ce::state_ce(s2, i->current_condition());
x = const_cast<state*>(s2);
delete i;
return true;// a counter example is found !!
}
else if (hi == h.end() || hi->second.c == white)
{
int res = dfs_blue_min(s2, i->current_acceptance_conditions());
if (res == 1)
{
delete i;
return true;
}
}
else
delete s2; // FIXME
}
delete i;
pop();
if (!all_succ_black(s) &&
a->state_is_accepting(s))
{
if (dfs_red_min(s))
return 1;
dfs_black(s);
}
}
return false;
}
bool
colordfs_search::dfs_red_min(const state* s)
{
//std::cout << "dfs_red : " << a->format_state(s) << std::endl;
if (!push(s, red))
return false;
hash_type::iterator hi = h.find(s);
if (hi != h.end())
{
if (((int)stack.size() + 1) < hi->second.depth)
hi->second.depth = stack.size(); // for minimize
}
else
assert(0);
if (Maxdepth == -1 || ((int)stack.size() + 1 < Maxdepth))
{
tgba_succ_iterator* i = a->succ_iter(s);
int n = 0;
for (i->first(); !i->done(); i->next(), n++)
{
const state* s2 = i->current_state();
hi = h.find(s2);
if (hi != h.end() && hi->second.is_in_cp &&
(a->state_is_accepting(s2) ||
(hi->second.c == blue)))
{
Maxdepth = stack.size();
ce::state_ce ce;
ce = ce::state_ce(s2->clone(), i->current_condition());
x = const_cast<state*>(s2);
delete i;
return true;// a counter example is found !!
}
if (hi != h.end() &&
(hi->second.c == blue))
// || ((int)stack.size() + 1) < hi->second.depth))
{
delete s2; // FIXME
if (dfs_red_min(hi->first))
{
delete i;
return true;
}
}
else
delete s2;
}
delete i;
//std::cout << "dfs_red : pop" << std::endl;
pop();
}
return false;
}
void
colordfs_search::dfs_black(const state* s)
{
//std::cout << "dfs_black" << a->format_state(s) << std::endl;
hash_type::iterator hi = h.find(s);
if (hi == h.end()) // impossible
{
color_state cs = { black, false, stack.size() };
h[s] = cs;
}
else
hi->second.c = black;
tgba_succ_iterator* i = a->succ_iter(s);
for (i->first(); !i->done(); i->next())
{
const state* s2 = i->current_state();
hi = h.find(s2);
if (hi == h.end())
{
color_state cs = { black, false, stack.size() };
h[s2] = cs;
dfs_black(s2);
}
else
{
delete s2;
if (hi->second.c != black)
dfs_black(hi->first);
}
}
delete i;
}
std::ostream&
colordfs_search::print_stat(std::ostream& os) const
{
int ce_size = 0;
if (counter_)
ce_size = counter_->size();
os << "Size of Counter Example : " << ce_size << std::endl
<< "States explored : " << h.size() << std::endl
<< "Computed time : " << tps_ << " microseconds" << std::endl;
return os;
}
}

124
src/tgbaalgos/colordfs.hh
View file

@ -1,124 +0,0 @@
// 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_COLORDFS_HH
# define SPOT_TGBAALGOS_COLORDFS_HH
#include "misc/hash.hh"
#include <list>
#include <utility>
#include <ostream>
#include "tgba/tgbatba.hh"
#include "tgbaalgos/minimalce.hh"
namespace spot
{
class colordfs_search: public emptiness_search
{
public:
/// Initialize the Colordfs Search algorithm on the automaton \a a.
colordfs_search(const tgba_tba_proxy *a);
virtual ~colordfs_search();
/// \brief Perform a Color DFS Search.
///
/// \return a new accepting path if there exists one, NULL otherwise.
///
/// check() can be called several times until it return false,
/// to enumerate all accepting paths.
virtual ce::counter_example* check();
/// \brief Print Stat.
std::ostream& print_stat(std::ostream& os) const;
private:
// The names "stack", "h", and "x", are those used in the paper.
/// \brief Records the color of a state.
enum color
{
white = 0,
blue = 1,
red = 2,
black = 3
};
struct color_state
{
color c;
bool is_in_cp;
int depth;
};
typedef std::pair<const state*, tgba_succ_iterator*> state_iter_pair;
typedef std::list<state_iter_pair> stack_type;
stack_type stack; ///< Stack of visited states on the path.
typedef std::list<bdd> tstack_type;
/// \brief Stack of transitions.
///
/// This is an addition to the data from the paper.
tstack_type tstack;
typedef Sgi::hash_map<const state*, color_state,
state_ptr_hash, state_ptr_equal> hash_type;
hash_type h; ///< Map of visited states.
/// The three dfs as explain in
/// @InProceedings(GaMoZe04spin,
/// Author = "Gastin, P. and Moro, P. and Zeitoun, M.",
/// Title = "Minimization of counterexamples in {SPIN}",
/// BookTitle = "Proceedings of the 11th SPIN Workshop (SPIN'04)",
/// Editor = "Graf, S. and Mounier, L.",
/// Publisher = SPRINGER,
/// Series = LNCS,
/// Number = 2989,
/// Year = 2004,
/// Pages = "92-108")
bool dfs_blue(const state* s, bdd acc = bddfalse);
bool dfs_red(const state* s);
bool dfs_blue_min(const state* s, bdd acc = bddfalse);
bool dfs_red_min(const state* s);
void dfs_black(const state* s);
/// Append a new state to the current path.
bool push(const state* s, color c);
/// Remove a state to the current path.
void pop();
/// Check if all successors of \a s are black and color
/// \a s in black if true.
bool all_succ_black(const state* s);
const tgba_tba_proxy* a; ///< The automata to check.
/// The state for which we are currently seeking an SCC.
const state* x;
int Maxdepth; ///< The size of the current counter example.
ce::counter_example* counter_;
clock_t tps_;
};
}
#endif // SPOT_TGBAALGOS_COLORDFS_HH

219
src/tgbaalgos/gtec/ce.cc
View file

@ -35,11 +35,6 @@ namespace spot
eccf)
: ecs_(ecs)
{
std::cout << "counter_example" << std::endl;
//counter_ = new ce::counter_example(ecs->aut);
assert(!ecs_->root.empty());
assert(suffix.empty());
@ -81,10 +76,6 @@ namespace spot
assert(spi.first);
suffix.push_front(spi.first);
/////
// counter_->prefix.push_front(ce::state_ce(spi.first->clone(), bddfalse));
////
// 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
@ -122,36 +113,21 @@ namespace spot
const state* h_dest = scc[k]->has_state(dest);
if (!h_dest)
{
// If we have found a state in greater SCC which.
// 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;
///
// ce::l_state_ce seq_count;
///
seq.push_front(h_dest);
while (src->compare(start))
{
///
// seq_count.push_front(ce::state_ce(src->clone(),
// bddfalse));
///
seq.push_front(src);
src = father[src];
}
// Append SEQ to SUFFIX.
suffix.splice(suffix.end(), seq);
///
// counter_->prefix.splice(counter_->prefix.end(),
// seq_count);
///
// Exit this BFS for this SCC.
while (!todo.empty())
{
@ -190,8 +166,6 @@ namespace spot
const state* from,
const state* to)
{
//std::cout << "complete_cycle" << std::endl;
// If by change or period already ends on the state we have
// to reach back, we are done.
if (from == to
@ -237,28 +211,14 @@ namespace spot
if (h_dest == to)
{
cycle_path p;
///
// ce::l_state_ce p_counter;
// p_counter.push_front(ce::state_ce(h_dest->clone(), cond));
///
p.push_front(state_proposition(h_dest, cond));
while (src != from)
{
const state_proposition& psi = father[src];
///
// p_counter.push_front(ce::state_ce(src->clone(),
// psi.second));
///
p.push_front(state_proposition(src, psi.second));
src = psi.first;
}
period.splice(period.end(), p);
///
// counter_->cycle.splice(counter_->cycle.end(),
// p_counter);
///
// Exit the BFS, but release all iterators first.
while (!todo.empty())
@ -296,9 +256,6 @@ namespace spot
}
////////////////////////////////////////////////////////////////////////
/*
void
counter_example::accepting_path(const explicit_connected_component* scc,
const state* start, bdd acc_to_traverse)
@ -338,9 +295,9 @@ namespace spot
todo.pop();
delete iter;
seen.erase(s);
if (!todo.empty())
if (todo.size())
{
assert(!path.empty());
assert(path.size());
path.pop_back();
}
continue;
@ -377,7 +334,7 @@ namespace spot
// If we already have a best path, let see if the current
// one is better.
if (!best_path.empty())
if (best_path.size())
{
// When comparing the merits of two paths, only the
// acceptance conditions we are trying the traverse
@ -423,12 +380,7 @@ namespace spot
// Append our best path to the period.
for (cycle_path::iterator it = best_path.begin();
it != best_path.end(); ++it)
{
period.push_back(*it);
ce::state_ce ce(it->first, it->second);
counter_->cycle.push_back(ce);
counter_->cycle.push_back(*it);
}
period.push_back(*it);
// Prepare to find another path for the remaining acceptance
// conditions.
@ -441,161 +393,6 @@ namespace spot
complete_cycle(scc, start, suffix.back());
}
*/
////////////////////////////////////////////////////////////////////////
void
counter_example::accepting_path(const explicit_connected_component* scc,
const state* start, bdd acc_to_traverse)
{
//std::cout << "accepting_path" << std::endl;
// 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)
{
//std::cout << "accepting_path : while (acc_to_traverse != bddfalse)"
// << std::endl;
// 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())
{
// std::cout << "accepting_path : while (!todo.empty())"
// << std::endl;
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.empty())
{
assert(!path.empty());
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.empty())
{
// 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);
//ce::state_ce ce(it->first->clone(), it->second);
//counter_->cycle.push_back(ce);
//counter_->cycle.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
{
@ -647,10 +444,4 @@ namespace spot
os << period.size() << " states in period" << std::endl;
}
ce::counter_example*
counter_example::get_counter_example() const
{
return counter_;
}
}

5
src/tgbaalgos/gtec/ce.hh
View file

@ -25,8 +25,6 @@
#include "status.hh"
#include "explscc.hh"
#include "tgbaalgos/minimalce.hh"
namespace spot
{
/// Compute a counter example from a spot::emptiness_check_status
@ -53,8 +51,6 @@ namespace spot
/// Output statistics about this object.
void print_stats(std::ostream& os) const;
ce::counter_example* get_counter_example() const;
protected:
/// Called by counter_example to find a path which traverses all
/// acceptance conditions in the accepted SCC.
@ -68,7 +64,6 @@ namespace spot
private:
const emptiness_check_status* ecs_;
ce::counter_example* counter_;
};
}

1006
src/tgbaalgos/minimalce.cc
View file

File diff suppressed because it is too large Load diff

237
src/tgbaalgos/minimalce.hh
View file

@ -1,237 +0,0 @@
// 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_MINIMALCE_HH
# define SPOT_TGBAALGOS_MINIMALCE_HH
#include "misc/hash.hh"
#include <list>
#include <utility>
#include <ostream>
#include <sstream>
#include "tgba/tgbatba.hh"
#include "tgba/bddprint.hh"
//#include "tgbaalgos/gtec/ce.hh"
#include <time.h>
namespace spot
{
enum search_opt
{
magic = 0,
nested = 1,
my_nested = 2
};
namespace ce
{
typedef std::pair<const state*, bdd> state_ce;
typedef std::list<state_ce> l_state_ce;
///////////////////////////////////////////////////////////////////////////
// Class counter example.
class counter_example
{
public :
counter_example(const tgba* a);
~counter_example();
void build_cycle(const state* x);
int size();
std::ostream& print(std::ostream& os) const;
bdd_dict* get_dict() const;
/// \brief Project a counter example on a tgba.
void project_ce(const tgba* aut, std::ostream& os = std::cout);
/// \brief Build a tgba from a counter example.
tgba* ce2tgba();
l_state_ce prefix;
l_state_ce cycle;
const tgba* automata_;
};
}
/////////////////////////////////////////////////////////////////////////////
// The base interface to build an emptiness check algorithm
class emptiness_search
{
protected:
emptiness_search();
public:
virtual ~emptiness_search();
virtual ce::counter_example* check() = 0;
/// \brief Print Stat.
virtual std::ostream& print_stat(std::ostream& os) const;
};
/////////////////////////////////////////////////////////////////////////////
// Perform a minimal search
class minimalce_search: public emptiness_search
{
public:
//minimalce_search(const tgba_tba_proxy *a, bool mode = false);
minimalce_search(const tgba_tba_proxy *a, int opt = nested);
virtual ~minimalce_search();
/// \brief Find the shortest counter example.
virtual ce::counter_example* check();
/// \brief Find a counter example shorter than \a min_ce.
//ce::counter_example* check(ce::counter_example* min_ce);
//ce::counter_example* find();
/// \brief Print Stat.
std::ostream& print_stat(std::ostream& os) const;
std::ostream& print_result(std::ostream& os,
const tgba* restrict = 0) const;
//ce::counter_example* get_minimal_cyle() const;
//ce::counter_example* get_minimal_prefix() const;
private:
/// \brief Minimisation is implemented on the magic search algorithm.
struct magic
{
bool seen_without : 1;
bool seen_with : 1;
bool seen_path : 1;
unsigned int depth;
};
struct magic_state
{
const state* s;
bool m;
};
enum search_mode
{
normal = 0,
careful = 1
};
//int mode;
typedef std::pair<magic_state, tgba_succ_iterator*> state_iter_pair;
typedef std::list<state_iter_pair> stack_type;
stack_type stack; ///< Stack of visited states on the path.
typedef std::list<bdd> tstack_type;
/// \brief Stack of transitions.
///
/// This is an addition to the data from the paper.
tstack_type tstack;
typedef Sgi::hash_map<const state*, magic,
state_ptr_hash, state_ptr_equal> hash_type;
hash_type h; ///< Map of visited states.
/// Append a new state to the current path.
bool push(const state* s, bool m);
/// Check whether we already visited \a s with the Magic bit set to \a m.
bool has(const state* s, bool m) const;
/// Check if \a s is in the path.
bool exist_path(const state* s) const;
/// Return the depth of the state \a s in stack.
int depth_path(const state* s) const;
void build_counter();
const tgba_tba_proxy* a; ///< The automata to check.
/// The state for which we are currently seeking an SCC.
const state* x;
/// \brief Active the nested search which produce a
/// smaller counter example.
bool nested_;
/// \brief Active the nested bis search which produce a
/// smaller counter example.
const state* x_bis;
bool my_nested_;
bool accepted_path_;
int accepted_depth_;
unsigned int Maxsize;
ce::counter_example* counter_;
std::list<ce::counter_example*> l_ce;
///////////////////////////////////////////////////////////////////
/*
//typedef std::pair<int, tgba_succ_iterator*> state_iter_pair;
typedef Sgi::hash_map<const state*, int,
state_ptr_hash, state_ptr_equal> hash_type;
hash_type h_lenght; ///< Map of visited states.
typedef std::pair<const state*, tgba_succ_iterator*> state_pair;
//typedef std::pair<const state*, bdd> state_pair;
typedef std::list<state_pair> stack_type;
//typedef std::list<const state*> stack_type;
stack_type stack; ///< Stack of visited states on the path.
const tgba_tba_proxy* a; ///< The automata to check.
/// The state for which we are currently seeking an SCC.
//const state* x;
ce::counter_example* min_ce;
std::list<ce::counter_example*> l_ce;
int nb_found;
bool mode_;
clock_t tps_;
/// \brief Perform the minimal search as explain in
/// @InProceedings(GaMoZe04spin,
/// Author = "Gastin, P. and Moro, P. and Zeitoun, M.",
/// Title = "Minimization of counterexamples in {SPIN}",
/// BookTitle = "Proceedings of the 11th SPIN Workshop (SPIN'04)",
/// Editor = "Graf, S. and Mounier, L.",
/// Publisher = SPRINGER,
/// Series = LNCS,
/// Number = 2989,
/// Year = 2004,
/// Pages = "92-108")
void recurse_find(const state* it,
std::ostringstream& os,
int mode = normal);
bool closes_accepting(const state* s,
int detph,
std::ostringstream& os) const;
int in_stack(const state* s, std::ostringstream& os) const;
/// Save the current path in stack as a counter example.
/// this counter example is the minimal that we have found yet.
void save_counter(const state* s, std::ostringstream& os);
*/
};
}
#endif // SPOT_TGBAALGOS_MINIMALCE_HH

322
src/tgbaalgos/nesteddfs.cc
View file

@ -1,322 +0,0 @@
// 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 <iterator>
#include <cassert>
#include "nesteddfs.hh"
#include "tgba/bddprint.hh"
namespace spot
{
nesteddfs_search::nesteddfs_search(const tgba_tba_proxy* a,
int opt)
: a(a), x(0),
x_bis(0),
accepted_path_(false)
{
nested_ = my_nested_ = false;
if (opt == nested)
nested_ = true;
if (opt == my_nested)
my_nested_ = true;
Maxsize = 0;
}
nesteddfs_search::~nesteddfs_search()
{
hash_type::const_iterator s = h.begin();
while (s != h.end())
{
// Advance the iterator before deleting the "key" pointer.
const state* ptr = s->first;
++s;
delete ptr;
}
if (x)
delete x;
// Release all iterators on the stack.
while (!stack.empty())
{
delete stack.front().second;
stack.pop_front();
}
}
bool
nesteddfs_search::push(const state* s, bool m)
{
/*
if ((Maxsize != 0) && // for minimize
(stack.size() + 1 > Maxsize))
return false;
*/
tgba_succ_iterator* i = a->succ_iter(s);
i->first();
hash_type::iterator hi = h.find(s);
if (hi == h.end())
{
//magic d = { !m, m, true, stack.size() + 1};
magic d = { !m, m, true };
h[s] = d;
}
else
{
hi->second.seen_without |= !m;
hi->second.seen_with |= m;
hi->second.seen_path = true; // for nested search
/*
if ((stack.size() + 1) < hi->second.depth) // for minimize
hi->second.depth = stack.size() + 1;
*/
if (hi->first != s)
delete s;
s = hi->first;
}
magic_state ms = { s, m };
stack.push_front(state_iter_pair(ms, i));
return true;
}
bool
nesteddfs_search::has(const state* s, bool m) const
{
hash_type::const_iterator i = h.find(s);
if (i == h.end())
return false;
if (!m && i->second.seen_without)
return true;
if (m && i->second.seen_with)
return true;
return false;
}
bool
nesteddfs_search::exist_path(const state* s) const
{
hash_type::const_iterator hi = h.find(s);
if (hi == h.end())
return false;
if (hi->second.seen_with)
return false;
return hi->second.seen_path && hi->second.seen_without;
}
int
nesteddfs_search::depth_path(const state* s) const
{
int depth = 0;
stack_type::const_reverse_iterator i;
for (i = stack.rbegin(); i != stack.rend(); ++i, ++depth)
if (s->compare(i->first.s) == 0)
break;
if (i != stack.rend())
return depth;
else
return stack.size() + 1;
}
ce::counter_example*
nesteddfs_search::check()
{
if (my_nested_)
{
accepted_path_ = false;
accepted_depth_ = 0;
}
if (stack.empty())
// It's a new search.
push(a->get_init_state(), false);
else
// Remove the transition to the cycle root.
tstack.pop_front();
assert(stack.size() == 1 + tstack.size());
while (!stack.empty())
{
recurse:
//std::cout << "recurse : "<< stack.size() << std::endl;
nesteddfs_search::state_iter_pair& p = stack.front();
tgba_succ_iterator* i = p.second;
const bool magic = p.first.m;
while (!i->done())
{
const state* s_prime = i->current_state();
//std::cout << a->format_state(s_prime) << std::endl;
bdd c = i->current_condition();
i->next();
if ((magic && 0 == s_prime->compare(x)) ||
(magic && (nested_ || my_nested_) && exist_path(s_prime)) ||
(!magic && my_nested_ && accepted_path_ &&
exist_path(s_prime) && depth_path(s_prime) <= accepted_path_))
{
if (nested_ || my_nested)
{
if (x)
delete x;
x = s_prime->clone();
}
delete s_prime;
tstack.push_front(c);
assert(stack.size() == tstack.size());
build_counter();
//Maxsize = stack.size();
//counter_->build_cycle(x);
return counter_;
}
if (!has(s_prime, magic))
{
if (my_nested_ && a->state_is_accepting(s_prime))
{
accepted_path_ = true;
accepted_depth_ = stack.size();
}
if (push(s_prime, magic))
{
tstack.push_front(c);
goto recurse;
}
// for minimize
}
delete s_prime;
}
const state* s = p.first.s;
delete i;
if (nested_ || my_nested_)
{
hash_type::iterator hi = h.find(((stack.front()).first).s);
assert (hi != h.end());
hi->second.seen_path = false;
}
stack.pop_front();
if (!magic && a->state_is_accepting(s))
{
if (!has(s, true))
{
if (x)
delete x;
x = s->clone();
push(s, true);
continue;
}
}
if (!stack.empty())
tstack.pop_front();
}
std::cout << "END CHECK" << std::endl;
assert(tstack.empty());
return 0;
}
std::ostream&
nesteddfs_search::print_result(std::ostream& os, const tgba* restrict) const
{
stack_type::const_reverse_iterator i;
tstack_type::const_reverse_iterator ti;
os << "Prefix:" << std::endl;
const bdd_dict* d = a->get_dict();
for (i = stack.rbegin(), ti = tstack.rbegin();
i != stack.rend(); ++i, ++ti)
{
if (i->first.s->compare(x) == 0)
os <<"Cycle:" <<std::endl;
const state* s = i->first.s;
if (restrict)
{
s = a->project_state(s, restrict);
assert(s);
os << " " << restrict->format_state(s) << std::endl;
delete s;
}
else
{
os << " " << a->format_state(s) << std::endl;
}
os << " | " << bdd_format_set(d, *ti) << std::endl;
}
if (restrict)
{
const state* s = a->project_state(x, restrict);
assert(s);
os << " " << restrict->format_state(s) << std::endl;
delete s;
}
else
{
os << " " << a->format_state(x) << std::endl;
}
return os;
}
std::ostream&
nesteddfs_search::print_stat(std::ostream& os) const
{
int ce_size = 0;
if (counter_)
ce_size = counter_->size();
os << "Size of Counter Example : " << ce_size << std::endl
<< "States explored : " << h.size() << std::endl;
return os;
}
void
nesteddfs_search::build_counter()
{
assert(stack.size() == tstack.size());
counter_ = new ce::counter_example(a);
stack_type::reverse_iterator i;
tstack_type::reverse_iterator ti;
for (i = stack.rbegin(), ti = tstack.rbegin();
i != stack.rend(); ++i, ++ti)
{
if (i->first.s->compare(x) == 0)
break;
ce::state_ce ce;
ce = ce::state_ce(i->first.s->clone(), *ti);
counter_->prefix.push_back(ce);
}
for (; i != stack.rend(); ++i, ++ti)
{
ce::state_ce ce;
ce = ce::state_ce(i->first.s->clone(), *ti);
counter_->cycle.push_back(ce);
}
//counter_->build_cycle(x);
}
}

142
src/tgbaalgos/nesteddfs.hh
View file

@ -1,142 +0,0 @@
// 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_NESTEDDFS_HH
# define SPOT_TGBAALGOS_NESTEDDFS_HH
#include "misc/hash.hh"
#include <list>
#include <utility>
#include <ostream>
#include "tgba/tgbatba.hh"
#include "tgbaalgos/minimalce.hh"
namespace spot
{
/*
enum search_opt
{
magic = 0,
nested = 1,
my_nested = 2
};
*/
class nesteddfs_search: public emptiness_search
{
public:
/// Initialize the Nesteddfs Search algorithm on the automaton \a a.
nesteddfs_search(const tgba_tba_proxy *a, int opt = nested);
virtual ~nesteddfs_search();
/// \brief Perform a Magic or a Nested DFS Search.
///
/// \return true iff the algorithm has found a new accepting
/// path.
///
/// check() can be called several times until it return false,
/// to enumerate all accepting paths.
virtual ce::counter_example* check();
/// \brief Print the last accepting path found.
///
/// Restrict printed states to \a the state space of restrict if
/// supplied.
std::ostream& print_result(std::ostream& os,
const tgba* restrict = 0) const;
/// \brief Print Stat.
std::ostream& print_stat(std::ostream& os) const;
private:
// The names "stack", "h", and "x", are those used in the paper.
/// \brief Records whether a state has be seen with the magic bit
/// on or off.
struct magic
{
bool seen_without : 1;
bool seen_with : 1;
bool seen_path : 1;
//unsigned int depth;
};
/// \brief A state for the spot::magic_search algorithm.
struct magic_state
{
const state* s;
bool m; ///< The state of the magic demon.
// int depth;
};
typedef std::pair<magic_state, tgba_succ_iterator*> state_iter_pair;
typedef std::list<state_iter_pair> stack_type;
stack_type stack; ///< Stack of visited states on the path.
typedef std::list<bdd> tstack_type;
/// \brief Stack of transitions.
///
/// This is an addition to the data from the paper.
tstack_type tstack;
typedef Sgi::hash_map<const state*, magic,
state_ptr_hash, state_ptr_equal> hash_type;
hash_type h; ///< Map of visited states.
/// Append a new state to the current path.
bool push(const state* s, bool m);
/// Check whether we already visited \a s with the Magic bit set to \a m.
bool has(const state* s, bool m) const;
/// Check if \a s is in the path.
bool exist_path(const state* s) const;
/// Return the depth of the state \a s in stack.
int depth_path(const state* s) const;
void build_counter();
const tgba_tba_proxy* a; ///< The automata to check.
/// The state for which we are currently seeking an SCC.
const state* x;
/// \brief Active the nested search which produce a
/// smaller counter example.
bool nested_;
/// \brief Active the nested bis search which produce a
/// smaller counter example.
const state* x_bis;
bool my_nested_;
bool accepted_path_;
int accepted_depth_;
unsigned int Maxsize;
ce::counter_example* counter_;
};
}
#endif // SPOT_TGBAALGOS_NESTEDDFS_HH

333
src/tgbaalgos/nesteddfsgen.cc
View file

@ -1,333 +0,0 @@
// 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 "tgbaalgos/nesteddfsgen.hh"
namespace spot
{
nesteddfsgen_search::nesteddfsgen_search(const tgba *a)
: a(a)
{
}
nesteddfsgen_search::~nesteddfsgen_search()
{
for (stack_type::iterator i = stack.begin();
i != stack.end(); ++i)
{
//delete i->first;
delete i->second;
}
for (hash_type::iterator i = h.begin();
i != h.end();)
{
const state *s = i->first;
++i;
delete s;
}
}
void
nesteddfsgen_search::free_states()
{
for (std::list<const state*>::iterator i = states->begin();
i != states->end(); ++i)
{
delete *i;
}
delete states;
}
//ce::counter_example*
/*
bool
nesteddfsgen_search::check()
{
hash_type::iterator hi, hi_next;
tgba_succ_iterator *iter, *iter_temp;
const state *init, *s, *s_next, *succ;
bdd cond1, cond2;
init = a->get_init_state();
iter_temp = a->succ_iter(init);
iter_temp->first();
stack.push_front(state_iter_pair(init, iter_temp));
while (!stack.empty())
{
s = stack.front().first;
iter = stack.front().second;
while (!iter->done())
{
succ = iter->current_state(); //
hi = h.find(succ);
if (hi != h.end() &&
(hi->second.in_stack ||
hi->second.processed))
{
delete succ;
iter->next();
continue;
}
iter_temp = a->succ_iter(succ);
iter_temp->first();
stack.push_front(state_iter_pair(succ, iter_temp));
if (hi != h.end())
hi->second.in_stack = 1;
else
{
state_info si = { 1, 0, bddfalse };
h[s] = si;
}
s = succ;
iter->next();
iter = iter_temp;
}
//delete iter;
iter = a->succ_iter(s);
hi = h.find(s);
for (iter->first(); !iter->done(); iter->next())
{
s_next = iter->current_state(); //
hi_next = h.find(s_next);
if (hi != h.end())
cond1 = hi->second.cond;
else
cond1 = bddfalse;
if (hi_next != h.end())
cond2 = hi_next->second.cond;
else
cond2 = bddfalse;
if ((!(iter->current_acceptance_conditions() | cond1) |
cond2) != bddtrue)
markConditions(s_next,
iter->current_acceptance_conditions()
| cond1);
//else
//delete s_next;
}
delete iter;
if (hi != h.end() &&
hi->second.cond == a->all_acceptance_conditions())
{
std::cout << "Counter example found" << std::endl;
return 1;
}
//free_states();
if (hi == h.end())
{
state_info si = { 0, 1, bddfalse };
h[s] = si;
}
else
{
hi->second.processed = 1;
//delete s;
}
hi = h.find(stack.front().first);
if (hi == h.end())
delete stack.front().first;
delete stack.front().second;
//iter = stack.front().second;
//delete iter;
stack.pop_front();
}
std::cout << "Automate is inf-empty" << std::endl;
return 0;
}
*/
bool
nesteddfsgen_search::check()
{
hash_type::iterator hi, hi_next;
tgba_succ_iterator *iter, *iter_temp;
const state *init, *s, *s_next, *succ;
bdd cond1, cond2;
init = a->get_init_state();
iter_temp = a->succ_iter(init);
iter_temp->first();
stack.push_front(state_iter_pair(init, iter_temp));
state_info si = { 1, 0, bddfalse };
h[init] = si;
while (!stack.empty())
{
recurse:
s = stack.front().first;
iter = stack.front().second;
while (!iter->done())
{
//std::cout << "while (!iter->done())" << std::endl;
succ = iter->current_state();
hi = h.find(succ);
if (hi != h.end() &&
(hi->second.in_stack ||
hi->second.processed))
{
delete succ;
iter->next();
continue;
}
iter->next();
iter = a->succ_iter(succ);
iter->first();
stack.push_front(state_iter_pair(succ, iter));
state_info si = { 1, 0, bddfalse };
h[succ] = si;
goto recurse;
}
iter = a->succ_iter(s);
hi = h.find(s);
for (iter->first(); !iter->done(); iter->next())
{
//std::cout << "for (iter->first(); !iter->done(); iter->next())"
//<< std::endl;
s_next = iter->current_state(); //
hi_next = h.find(s_next);
if (hi != h.end())
cond1 = hi->second.cond;
else
cond1 = bddfalse;
if (hi_next != h.end())
cond2 = hi_next->second.cond;
else
cond2 = bddfalse;
if ((!(iter->current_acceptance_conditions() | cond1) |
cond2) != bddtrue)
markConditions(s_next,
iter->current_acceptance_conditions()
| cond1);
else
delete s_next;
}
delete iter;
if (hi != h.end() &&
hi->second.cond == a->all_acceptance_conditions())
{
std::cout << "Counter example found" << std::endl;
return 1;
}
if (hi == h.end())
{
state_info si = { 0, 1, bddfalse };
h[s] = si;
}
else
{
hi->second.processed = 1;
}
hi = h.find(stack.front().first);
if (hi == h.end())
delete stack.front().first;
delete stack.front().second;
stack.pop_front();
}
std::cout << "Automate is inf-empty" << std::endl;
return 0;
}
void
nesteddfsgen_search::markConditions(const state* s, bdd conditions)
{
//std::cout << "markConditions" << std::endl;
states = new std::list<const state*>;
hash_type::iterator hi;
tgba_succ_iterator* iter;
const state *q_next, *q;
bdd cond;
states->push_front(s);
do
{
q = states->front();
states->pop_front();
hi = h.find(q);
if (hi != h.end())
{
delete q;
q = hi->first;
hi->second.cond |= conditions;
}
else
{
state_info si = { 0, 0, conditions };
h[q] = si;
}
iter = a->succ_iter(q);
for (iter->first(); !iter->done(); iter->next())
{
q_next = iter->current_state();
hi = h.find(q_next);
if (hi != h.end())
cond = hi->second.cond;
else
cond = bddfalse;
if ((hi != h.end() &&
(hi->second.in_stack || hi->second.processed)) &&
((!conditions | cond) != bddtrue))
{
states->push_front(q_next);
}
else
delete q_next;
}
delete iter;
}
while (!states->empty());
//delete s; // ??
free_states();
}
void
nesteddfsgen_search::print_stats(std::ostream& os) const
{
os << h.size() << " unique states visited" << std::endl;
os << "size of stack : " << stack.size() << std::endl;
}
}

81
src/tgbaalgos/nesteddfsgen.hh
View file

@ -1,81 +0,0 @@
// 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_NESTEDDFSGEN_HH
# define SPOT_TGBAALGOS_NESTEDDFSGEN_HH
#include "misc/hash.hh"
#include <list>
#include <utility>
#include <ostream>
#include "tgba/tgba.hh"
#include "tgbaalgos/minimalce.hh"
namespace spot
{
class nesteddfsgen_search
{
public:
/// Initialize the Nesteddfs Search algorithm on the automaton \a a.
nesteddfsgen_search(const tgba *a);
~nesteddfsgen_search();
/// \brief Find a counter example.
//ce::counter_example* check();
bool check();
void print_stats(std::ostream& os) const;
private:
struct state_info
{
bool in_stack : 1;
bool processed : 1;
bdd cond;
};
typedef Sgi::hash_map<const state*, state_info,
state_ptr_hash, state_ptr_equal> hash_type;
hash_type h; ///< Map of visited states.
//hash_type processed; ///< Map of processed states.
typedef std::pair<const state*, tgba_succ_iterator*> state_iter_pair;
typedef std::list<state_iter_pair> stack_type;
stack_type stack; ///< Stack of visited states on the path.
std::list<const state*> *states;
void markConditions(const state* s, bdd cond);
void free_states();
const tgba* a;
ce::counter_example* counter_;
};
}
#endif // SPOT_TGBAALGOS_NESTEDDFS_HH

193
src/tgbaalgos/tarjan_on_fly.cc
View file

@ -1,193 +0,0 @@
// 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 "tgbaalgos/tarjan_on_fly.hh"
namespace spot
{
tarjan_on_fly::tarjan_on_fly(const tgba_tba_proxy *a)
: a(a), x(0)
{
}
tarjan_on_fly::~tarjan_on_fly()
{
for (stack_type::iterator i = stack.begin();
i != stack.end(); ++i)
{
hash_type::iterator hi = h.find(i->s);
if (hi != h.end())
h.erase(hi);
delete i->s;
delete i->lasttr;
}
for (hash_type::iterator i = h.begin();
i != h.end();)
{
const state *s = i->first;
++i;
delete s;
}
}
bool
tarjan_on_fly::check()
{
tgba_succ_iterator* iter = 0;
const state* succ = 0;
int pos = 0;
top = dftop = -1;
violation = false;
const state* s = a->get_init_state();
push(s);
while (!violation && dftop >= 0)
{
s = stack[dftop].s;
iter = stack[dftop].lasttr;
if (iter == 0)
{
iter = a->succ_iter(s);
iter->first();
stack[dftop].lasttr = iter;
}
else
{
iter->next();
}
succ = 0;
if (!iter->done())
{
succ = iter->current_state();
if (h.find(succ) == h.end())
push(succ);
else
{
pos = in_stack(succ);
delete succ;
if (pos != -1) // succ is in stack
lowlinkupdate(dftop, pos);
}
}
else
pop();
}
return violation;
}
void
tarjan_on_fly::push(const state* s)
{
h[s] = top++;
struct_state ss = { s, 0, top, dftop, 0 };
if (a->state_is_accepting(s))
{
ss.acc = top;
x = s; // FIXME
}
else if (dftop >= 0)
ss.acc = stack[dftop].acc;
else
ss.acc = -1;
if (top < (int)stack.size())
{
const state* sdel = stack[top].s;
tgba_succ_iterator* iter = stack[top].lasttr;
if (h.find(sdel) == h.end())
{
assert(0);
delete sdel;
}
if (iter)
delete iter;
stack[top] = ss;
}
else
{
stack.push_back(ss);
}
dftop = top;
}
void
tarjan_on_fly::pop()
{
int p = stack[dftop].pre;
if (p >= 0)
lowlinkupdate(p, dftop);
if (stack[dftop].lowlink == dftop)
top = dftop - 1;
dftop = p;
}
void
tarjan_on_fly::lowlinkupdate(int f, int t)
{
if (stack[t].lowlink <= stack[f].lowlink)
{
if (stack[t].lowlink <= stack[f].acc)
{
violation = true;
}
stack[f].lowlink = stack[t].lowlink;
}
}
int
tarjan_on_fly::in_stack(const state* s) const
{
int n = 0;
stack_type::const_iterator i;
for (i = stack.begin(); i != stack.end(); ++i, ++n)
if (s->compare(i->s) == 0)
break;
if (i == stack.end())
return -1;
return n;
}
std::ostream&
tarjan_on_fly::print_stat(std::ostream& os) const
{
os << "States explored : " << h.size() << std::endl;
return os;
}
}

83
src/tgbaalgos/tarjan_on_fly.hh
View file

@ -1,83 +0,0 @@
// 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_TARJAN_ON_FLY_HH
# define SPOT_TGBAALGOS_TARJAN_ON_FLY_HH
#include "misc/hash.hh"
#include <list>
#include <utility>
#include <ostream>
#include "tgba/tgbatba.hh"
namespace spot
{
class tarjan_on_fly
{
public:
tarjan_on_fly(const tgba_tba_proxy *a);
virtual ~tarjan_on_fly();
/// \brief Return true if there exits an accepting path.
bool check();
/// \brief Print Stat.
std::ostream& print_stat(std::ostream& os) const;
private:
struct struct_state
{
const state* s;
tgba_succ_iterator* lasttr;
int lowlink;
int pre;
int acc;
};
//typedef std::pair<int, tgba_succ_iterator*> state_iter_pair;
typedef Sgi::hash_map<const state*, int,
state_ptr_hash, state_ptr_equal> hash_type;
hash_type h; ///< Map of visited states.
typedef std::vector<struct_state> stack_type;
stack_type stack; ///< Stack of visited states on the path.
const tgba_tba_proxy* a; ///< The automata to check.
int top;
int dftop;
bool violation;
const state* x;
void push(const state* s);
void pop();
void lowlinkupdate(int f, int t);
int in_stack(const state* s) const;
};
}
#endif // SPOT_TGBAALGOS_MINIMALCE_HH

4
src/tgbatest/Makefile.am
View file

@ -64,8 +64,6 @@ tripprod_SOURCES = tripprod.cc
# Keep this sorted by STRENGTH. Test basic things first,
# because such failures will be easier to diagnose and fix.
TESTS = \
reduccmp.test \
reductgba.test \
explicit.test \
tgbaread.test \
readsave.test \
@ -79,6 +77,8 @@ TESTS = \
tripprod.test \
mixprod.test \
dupexp.test \
reduccmp.test \
reductgba.test \
emptchk.test \
emptchke.test \
spotlbtt.test

61
src/tgbatest/emptchk.test
View file

@ -27,53 +27,32 @@ set -e
expect_ce()
{
#run 0 ./ltl2tgba -m -f "$1"
#run 0 ./ltl2tgba -ndfs -f "$1"
run 0 ./ltl2tgba -tj -f "$1"
#run 0 ./ltl2tgba -c -f "$1"
#run 0 ./ltl2tgba -ndfs2 -f "$1"
#run 0 ./ltl2tgba -ng -f "$1"
#run 0 ./ltl2tgba -ms -f "$1"
#run 0 ./ltl2tgba -msit -f "$1"
#run 0 ./ltl2tgba -e "$1"
#run 0 ./ltl2tgba -e -D "$1"
#run 0 ./ltl2tgba -e -f "$1"
#run 0 ./ltl2tgba -e -f -D "$1"
#run 0 ./ltl2tgba -e2 "$1"
#run 0 ./ltl2tgba -e2 -D "$1"
#run 0 ./ltl2tgba -e2 -f "$1"
#run 0 ./ltl2tgba -e2 -f -D "$1"
#run 0 ./ltl2tgba -mold "$1"
#run 0 ./ltl2tgba -mold -f "$1"
run 0 ./ltl2tgba -e "$1"
run 0 ./ltl2tgba -e -D "$1"
run 0 ./ltl2tgba -e -f "$1"
run 0 ./ltl2tgba -e -f -D "$1"
run 0 ./ltl2tgba -e2 "$1"
run 0 ./ltl2tgba -e2 -D "$1"
run 0 ./ltl2tgba -e2 -f "$1"
run 0 ./ltl2tgba -e2 -f -D "$1"
run 0 ./ltl2tgba -m "$1"
run 0 ./ltl2tgba -m -f "$1"
}
expect_no()
{
#run 0 ./ltl2tgba -M -f "$1"
#run 0 ./ltl2tgba -Ndfs -f "$1"
run 0 ./ltl2tgba -TJ -f "$1"
#run 0 ./ltl2tgba -C -f "$1"
#run 0 ./ltl2tgba -Ndfs2 -f "$1"
#run 0 ./ltl2tgba -NG -f "$1"
#run 0 ./ltl2tgba -Ms -f "$1"
#run 0 ./ltl2tgba -E "$1"
#run 0 ./ltl2tgba -E -D "$1"
#run 0 ./ltl2tgba -E -f "$1"
#run 0 ./ltl2tgba -E -f -D "$1"
#run 0 ./ltl2tgba -E2 "$1"
#run 0 ./ltl2tgba -E2 -D "$1"
#run 0 ./ltl2tgba -E2 -f "$1"
#run 0 ./ltl2tgba -E2 -f -D "$1"
#run 0 ./ltl2tgba -M "$1"
#run 0 ./ltl2tgba -M -f "$1"
run 0 ./ltl2tgba -E "$1"
run 0 ./ltl2tgba -E -D "$1"
run 0 ./ltl2tgba -E -f "$1"
run 0 ./ltl2tgba -E -f -D "$1"
run 0 ./ltl2tgba -E2 "$1"
run 0 ./ltl2tgba -E2 -D "$1"
run 0 ./ltl2tgba -E2 -f "$1"
run 0 ./ltl2tgba -E2 -f -D "$1"
run 0 ./ltl2tgba -M "$1"
run 0 ./ltl2tgba -M -f "$1"
}
expect_ce 'Fa & Xb & GFc & Gd'
expect_ce 'a'
expect_ce 'a U b'
expect_ce 'X a'

265
src/tgbatest/ltl2tgba.cc
View file

@ -36,11 +36,6 @@
#include "tgbaalgos/lbtt.hh"
#include "tgba/tgbatba.hh"
#include "tgbaalgos/magic.hh"
#include "tgbaalgos/nesteddfs.hh"
#include "tgbaalgos/nesteddfsgen.hh"
#include "tgbaalgos/colordfs.hh"
#include "tgbaalgos/tarjan_on_fly.hh"
//#include "tgbaalgos/minimalce.hh"
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/gtec/ce.hh"
#include "tgbaparse/public.hh"
@ -60,10 +55,6 @@ syntax(char* prog)
<< "reachability graph"
<< std::endl
<< " -A same as -a, but as a set" << std::endl
<< " -c color-search (implies -D), expect a counter-example"
<< std::endl
<< " -C color-search (implies -D), expect no counter-example"
<< std::endl
<< " -d turn on traces during parsing" << std::endl
<< " -D degeneralize the automaton" << std::endl
<< " -e emptiness-check (Couvreur), expect and compute "
@ -80,38 +71,12 @@ syntax(char* prog)
<< " -L fair-loop approximation (implies -f)" << std::endl
<< " -m magic-search (implies -D), expect a counter-example"
<< std::endl
<< " -ms minmimal-search (implies -D), expect a counter-example"
<< std::endl
<< " -msit minmimal-search (implies -D), expect a counter-example"
<< std::endl
<< " -mold magic-search (implies -D), expect a counter-example"
<< std::endl
<< " -M magic-search (implies -D), expect no counter-example"
<< std::endl
<< " -Mold magic-search (implies -D), expect no counter-example"
<< std::endl
<< " -n same as -m, but display more counter-examples"
<< std::endl
<< " -N display the never clain for Spin "
<< "(implies -D)" << std::endl
<< " -ndfs nesteddfs-search (implies -D), expect a "
<< "counter-example"
<< std::endl
<< " -Ndfs nesteddfs-search (implies -D), expect no "
<< "counter-example"
<< std::endl
<< " -ndfs2 modify-nesteddfs-search (implies -D), "
<< "expect a counter-example"
<< std::endl
<< " -Ndfs2 modify-nesteddfs-search (implies -D), "
<< "expect no counter-example"
<< std::endl
<< " -ng nesteddfs-search generalized (implies -D), expect a "
<< "counter-example"
<< std::endl
<< " -NG nesteddfs-search generalized (implies -D), expect no "
<< "counter-example"
<< std::endl
<< " -p branching postponement (implies -f)" << std::endl
<< " -r display the relation BDD, not the reachability graph"
<< std::endl
@ -146,12 +111,6 @@ syntax(char* prog)
<< " -S convert to explicit automata, and number states "
<< "in BFS order" << std::endl
<< " -t display reachable states in LBTT's format" << std::endl
<< " -T display reachable states in LBTT's format w/o "
<< "acceptance conditions" << std::endl
<< " -tj tarjan-on-fly (implies -D), expect a counter-example"
<< std::endl
<< " -TJ tarjan-on-fly (implies -D), expect no counter-example"
<< std::endl
<< " -U[PROPS] consider atomic properties PROPS as exclusive "
<< "events (implies -f)" << std::endl
<< " -v display the BDD variables used by the automaton"
@ -178,12 +137,7 @@ main(int argc, char** argv)
bool file_opt = false;
int output = 0;
int formula_index = 0;
enum { None, Couvreur, Couvreur2, MagicSearch, MagicSearchOld,
NestedDFSSearch, NestedDFSSearchModify, ColorDFSSearch,
TarjanOnFly, MinimalSearch, MinimalSearchIterative,
NestedGeneSearch} echeck = None;
spot::emptiness_search* es = 0;
spot::search_opt opt_nested_search = spot::magic;
enum { None, Couvreur, Couvreur2, MagicSearch } echeck = None;
enum { NoneDup, BFS, DFS } dupexp = NoneDup;
bool magic_many = false;
bool expect_counter_example = false;
@ -213,21 +167,6 @@ main(int argc, char** argv)
{
output = 4;
}
else if (!strcmp(argv[formula_index], "-c"))
{
echeck = ColorDFSSearch;
degeneralize_opt = true;
expect_counter_example = true;
output = -1;
magic_many = false;
}
else if (!strcmp(argv[formula_index], "-C"))
{
echeck = ColorDFSSearch;
degeneralize_opt = true;
expect_counter_example = false;
output = -1;
}
else if (!strcmp(argv[formula_index], "-d"))
{
debug_opt = true;
@ -275,61 +214,21 @@ main(int argc, char** argv)
}
else if (!strcmp(argv[formula_index], "-m"))
{
opt_nested_search = spot::magic;
echeck = MagicSearch;
degeneralize_opt = true;
expect_counter_example = true;
output = -1;
magic_many = true;
}
else if (!strcmp(argv[formula_index], "-M"))
{
opt_nested_search = spot::magic;
echeck = MagicSearch;
degeneralize_opt = true;
expect_counter_example = false;
output = -1;
}
else if (!strcmp(argv[formula_index], "-mold"))
{
echeck = MagicSearchOld;
degeneralize_opt = true;
expect_counter_example = true;
output = -1;
magic_many = true;
}
else if (!strcmp(argv[formula_index], "-Mold"))
{
echeck = MagicSearchOld;
degeneralize_opt = true;
expect_counter_example = false;
output = -1;
}
else if (!strcmp(argv[formula_index], "-ms"))
{
echeck = MinimalSearch;
degeneralize_opt = true;
expect_counter_example = true;
output = -1;
}
else if (!strcmp(argv[formula_index], "-Ms"))
{
echeck = MinimalSearch;
degeneralize_opt = true;
expect_counter_example = false;
output = -1;
}
else if (!strcmp(argv[formula_index], "-msit"))
{
echeck = MinimalSearchIterative;
degeneralize_opt = true;
expect_counter_example = true;
magic_many = true;
output = -1;
}
else if (!strcmp(argv[formula_index], "-n"))
{
echeck = MagicSearchOld;
echeck = MagicSearch;
degeneralize_opt = true;
expect_counter_example = true;
output = -1;
@ -340,53 +239,6 @@ main(int argc, char** argv)
degeneralize_opt = true;
output = 8;
}
else if (!strcmp(argv[formula_index], "-ndfs"))
{
opt_nested_search = spot::nested;
echeck = NestedDFSSearch;
degeneralize_opt = true;
expect_counter_example = true;
output = -1;
magic_many = true;
}
else if (!strcmp(argv[formula_index], "-Ndfs"))
{
opt_nested_search = spot::nested;
echeck = NestedDFSSearch;
degeneralize_opt = true;
expect_counter_example = false;
output = -1;
}
else if (!strcmp(argv[formula_index], "-ndfs2"))
{
opt_nested_search = spot::my_nested;
echeck = NestedDFSSearchModify;
degeneralize_opt = true;
expect_counter_example = true;
output = -1;
}
else if (!strcmp(argv[formula_index], "-Ndfs2"))
{
opt_nested_search = spot::my_nested;
echeck = NestedDFSSearchModify;
degeneralize_opt = true;
expect_counter_example = false;
output = -1;
}
else if (!strcmp(argv[formula_index], "-ng"))
{
echeck = NestedGeneSearch;
degeneralize_opt = true;
expect_counter_example = true;
output = -1;
}
else if (!strcmp(argv[formula_index], "-NG"))
{
echeck = NestedGeneSearch;
degeneralize_opt = true;
expect_counter_example = false;
output = -1;
}
else if (!strcmp(argv[formula_index], "-p"))
{
post_branching = true;
@ -460,20 +312,6 @@ main(int argc, char** argv)
{
output = 6;
}
else if (!strcmp(argv[formula_index], "-tj"))
{
echeck = TarjanOnFly;
degeneralize_opt = true;
expect_counter_example = true;
output = -1;
}
else if (!strcmp(argv[formula_index], "-TJ"))
{
echeck = TarjanOnFly;
degeneralize_opt = true;
expect_counter_example = false;
output = -1;
}
else if (!strncmp(argv[formula_index], "-U", 2))
{
unobservables = new spot::ltl::atomic_prop_set;
@ -730,18 +568,7 @@ main(int argc, char** argv)
}
break;
case NestedGeneSearch:
{
std::cout << "Nested DFS generalized" << std::endl;
spot::nesteddfsgen_search* ec = new spot::nesteddfsgen_search(a);
bool res = ec->check();
ec->print_stats(std::cout);
exit_code = expect_counter_example ? !res : res;
delete ec;
}
break;
case MagicSearchOld:
case MagicSearch:
{
std::cout << "Magic Search" << std::endl;
spot::magic_search ms(degeneralized);
@ -764,96 +591,10 @@ main(int argc, char** argv)
}
break;
case ColorDFSSearch:
std::cout << "Colored Search" << std::endl;
es = new spot::colordfs_search(degeneralized);
break;
case TarjanOnFly:
{
std::cout << "Tarjan On Fly" << std::endl;
spot::tarjan_on_fly* tof = new spot::tarjan_on_fly(degeneralized);
bool res = tof->check();
exit_code = expect_counter_example ? !res : res;
delete tof;
break;
}
case MinimalSearch:
{
std::cout << "Recursive Minimal Search" << std::endl;
es = new spot::colordfs_search(degeneralized);
spot::ce::counter_example* res = es->check();
res->print(std::cout);
std::cout << "Minimisation:" << std::endl;
es = new spot::minimalce_search(degeneralized, false);
res = es->check();
res->print(std::cout);
}
break;
case MinimalSearchIterative:
std::cout << "Iterative Minimal Search" << std::endl;
es = new spot::minimalce_search(degeneralized, true);
break;
case MagicSearch:
std::cout << "Magic Search" << std::endl;
es = new spot::nesteddfs_search(degeneralized, opt_nested_search);
break;
case NestedDFSSearch:
case NestedDFSSearchModify:
std::cout << "Nested DFS" << std::endl;
es = new spot::nesteddfs_search(degeneralized, opt_nested_search);
break;
default:
assert(0);
}
if (es)
{
spot::ce::counter_example* res = es->check();
if (expect_counter_example)
{
do
{
if (!res)
{
exit_code = 1;
break;
}
std::cout << "CE : " << std::endl
<< " size : " << res->size()
<< std::endl;
spot::tgba* aut = res->ce2tgba();
//spot::dotty_reachable(std::cout, aut);
res->print(std::cout);
es->print_stat(std::cout);
delete aut;
delete res;
res = 0;
}
while (magic_many && (res = es->check()));
}
else if (res)
{
exit_code = res->size();
std::cout << "res->size ?? : " << exit_code << std::endl;
}
else
{
exit_code = (res != 0);
std::cout << "res != 0 ?? : " << exit_code << std::endl;
}
if (res)
delete res;
}
if (es)
delete es;
if (f)
spot::ltl::destroy(f);
if (expl)