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

ec: Renault et al LPAR'13 emptiness check

Browse source 
In order to reuse the computation of the
intersection between kripke and twa efficiently,
we use template inheritance through the
"mixin templates" technique.

* spot/Makefile.am, spot/mc/Makefile.am,
spot/mc/ec.hh, spot/mc/unionfind.cc,
spot/mc/unionfind.hh: here.
This commit is contained in:
Etienne Renault 2016-03-17 16:23:28 +01:00
parent 87de88c80c
commit 3bafe693ef
5 changed files with 419 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

3
spot/Makefile.am
View file

@ -26,7 +26,7 @@ AUTOMAKE_OPTIONS = subdir-objects
# end, after building '.' (since the current directory contains
# libspot.la needed by the tests)
SUBDIRS = misc priv tl graph twa twacube twaalgos ta taalgos kripke \
twacube_algos parseaut parsetl . ltsmin gen
twacube_algos mc parseaut parsetl . ltsmin gen
lib_LTLIBRARIES = libspot.la
libspot_la_SOURCES =
@ -44,6 +44,7 @@ libspot_la_LIBADD = \
twa/libtwa.la \
twacube_algos/libtwacube_algos.la \
twacube/libtwacube.la \
mc/libmc.la \
../lib/libgnu.la \
../picosat/libpico.la

13
spot/mc/Makefile.am
View file

@ -1,9 +1,6 @@
## -*- coding: utf-8 -*-
## Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015, 2016 Laboratoire
## de Recherche et Développement de l'Epita (LRDE).
## 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.
## Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement de
## l'Epita (LRDE).
##
## This file is part of Spot, a model checking library.
##
@ -24,7 +21,9 @@ AM_CPPFLAGS = -I$(top_builddir) -I$(top_srcdir) $(BUDDY_CPPFLAGS)
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
mcdir = $(pkgincludedir)/mc
mc_HEADERS = reachability.hh intersect.hh
mc_HEADERS = reachability.hh intersect.hh ec.hh unionfind.hh
noinst_LTLIBRARIES = libmc.la
libmc_la_SOURCES = \
unionfind.cc

266
spot/mc/ec.hh Normal file
View file

@ -0,0 +1,266 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016 Laboratoire de Recherche et
// Developpement de l'Epita
//
// 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 3 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 this program. If not, see <http://www.gnu.org/licenses/>.
#pragma once
#include <spot/twa/acc.hh>
#include <spot/mc/unionfind.hh>
#include <spot/mc/intersect.hh>
namespace spot
{
/// \brief This class implements the sequential emptiness check as
/// presented in "Three SCC-based Emptiness Checks for Generalized
/// B\¨uchi Automata" (Renault et al, LPAR 2013). Among the three
/// emptiness check that has been proposed we opted to implement
/// the Gabow's one.
template<typename State, typename SuccIterator,
typename StateHash, typename StateEqual>
class ec_renault13lpar : public intersect<State, SuccIterator,
StateHash, StateEqual,
ec_renault13lpar<State, SuccIterator,
StateHash, StateEqual>>
{
// Ease the manipulation
using typename intersect<State, SuccIterator, StateHash, StateEqual,
ec_renault13lpar<State, SuccIterator,
StateHash,
StateEqual>>::product_state;
public:
ec_renault13lpar(kripkecube<State, SuccIterator>& sys,
twacube* twa)
: intersect<State, SuccIterator, StateHash, StateEqual,
ec_renault13lpar<State, SuccIterator,
StateHash, StateEqual>>(sys, twa),
acc_(twa->acc())
{
}
virtual ~ec_renault13lpar()
{
}
/// \brief This method is called at the begining of the exploration.
/// here we do not need to setup any information.
void setup()
{
}
/// \brief This method is called to notify the emptiness checks
/// that a new state has been discovered. If this method return
/// false, the state will not be explored. The parameter \a dfsnum
/// specify an unique id for the state \a s. Parameter \a cond represents
/// The value on the ingoing edge to \a s.
bool push_state(product_state, unsigned dfsnum, acc_cond::mark_t cond)
{
uf_.makeset(dfsnum);
roots_.push_back({dfsnum, cond, 0U});
return true;
}
/// \brief This method is called to notify the emptiness checks
/// that a state will be popped. If the method return false, then
/// the state will be popped. Otherwise the state \a newtop will
/// become the new top of the DFS stack. If the state \a top is
/// the only one in the DFS stak, the parameter \a is_initial is set
/// to true and both \a newtop and \a newtop_dfsnum have inconsistency
/// values.
bool pop_state(product_state, unsigned top_dfsnum, bool,
product_state, unsigned)
{
if (top_dfsnum == roots_.back().dfsnum)
{
roots_.pop_back();
uf_.markdead(top_dfsnum);
}
return true;
}
/// \brief This method is called for every closing, back, or forward edge.
/// Return true if a counterexample has been found.
bool update(product_state, unsigned,
product_state, unsigned dst_dfsnum,
acc_cond::mark_t cond)
{
if (uf_.isdead(dst_dfsnum))
return false;
while (!uf_.sameset(dst_dfsnum, roots_.back().dfsnum))
{
auto& el = roots_.back();
roots_.pop_back();
uf_.unite(dst_dfsnum, el.dfsnum);
cond |= el.acc | el.ingoing;
}
roots_.back().acc |= cond;
found_ = acc_.accepting(roots_.back().acc);
return found_;
}
bool counterexample_found()
{
return found_;
}
std::string trace()
{
assert(counterexample_found());
std::string res = "Prefix:\n";
// Compute the prefix of the accepting run
for (auto& s : this->todo)
res += " " + std::to_string(s.st.st_prop) +
+ "*" + this->sys_.to_string(s.st.st_kripke) + "\n";
// Compute the accepting cycle
res += "Cycle:\n";
struct ctrx_element
{
const product_state* prod_st;
ctrx_element* parent_st;
SuccIterator* it_kripke;
std::shared_ptr<trans_index> it_prop;
};
std::queue<ctrx_element*> bfs;
acc_cond::mark_t acc = 0U;
bfs.push(new ctrx_element({&this->todo.back().st, nullptr,
this->sys_.succ(this->todo.back().st.st_kripke),
this->twa_->succ(this->todo.back().st.st_prop)}));
while (true)
{
here:
auto* front = bfs.front();
bfs.pop();
// PUSH all successors of the state.
while (!front->it_kripke->done())
{
while (!front->it_prop->done())
{
if (this->twa_->get_cubeset().intersect
(this->twa_->trans_data(front->it_prop).cube_,
front->it_kripke->condition()))
{
const product_state dst = {
front->it_kripke->state(),
this->twa_->trans_storage(front->it_prop).dst
};
// Skip Unknown states or not same SCC
auto it = this->map.find(dst);
if (it == this->map.end() ||
!uf_.sameset(it->second,
this->map[this->todo.back().st]))
{
front->it_prop->next();
continue;
}
// This is a valid transition. If this transition
// is the one we are looking for, update the counter-
// -example and flush the bfs queue.
auto mark = this->twa_->trans_data(front->it_prop).acc_;
if (!acc.has(mark))
{
ctrx_element* current = front;
while (current != nullptr)
{
// FIXME also display acc?
res = res + " " +
std::to_string(current->prod_st->st_prop) +
+ "*" +
this->sys_. to_string(current->prod_st
->st_kripke) +
"\n";
current = current->parent_st;
}
// empty the queue
while (!bfs.empty())
{
auto* e = bfs.front();
bfs.pop();
delete e;
}
// update acceptance
acc |= mark;
if (this->twa_->acc().accepting(acc))
return res;
const product_state* q = &(it->first);
ctrx_element* root = new ctrx_element({
q , nullptr,
this->sys_.succ(q->st_kripke),
this->twa_->succ(q->st_prop)
});
bfs.push(root);
goto here;
}
// Otherwise increment iterator and push successor.
const product_state* q = &(it->first);
ctrx_element* root = new ctrx_element({
q , nullptr,
this->sys_.succ(q->st_kripke),
this->twa_->succ(q->st_prop)
});
bfs.push(root);
}
front->it_prop->next();
}
front->it_prop->reset();
front->it_kripke->next();
}
}
// never reach here;
return res;
}
// Refine stats to display
virtual std::string stats() override
{
return
std::to_string(this->dfs_number) + " unique states visited\n" +
std::to_string(roots_.size()) +
" strongly connected components in search stack\n" +
std::to_string(this->transitions) + " transitions explored\n";
}
private:
bool found_ = false; ///< \brief A counterexample is detected?
struct root_element {
unsigned dfsnum;
acc_cond::mark_t ingoing;
acc_cond::mark_t acc;
};
/// \brief the root stack.
std::vector<root_element> roots_;
int_unionfind uf_;
acc_cond acc_;
};
}

93
spot/mc/unionfind.cc Normal file
View file

@ -0,0 +1,93 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016 Laboratoire de Recherche et
// Developpement de l'Epita
//
// 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 3 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 this program. If not, see <http://www.gnu.org/licenses/>.
#include <spot/mc/unionfind.hh>
#include <assert.h>
namespace spot
{
int int_unionfind::root(int i)
{
assert(i > 0);
int p = id[i];
if (p == DEAD)
return DEAD;
if (p < 0)
return i;
int gp = id[p];
if (gp == DEAD)
return DEAD;
if (gp < 0)
return p;
p = root(p);
id[i] = p;
return p;
}
int_unionfind::int_unionfind() : id()
{
id.push_back(DEAD);
}
void int_unionfind::makeset(int e)
{
assert(e == (int) id.size());
id.push_back(-1);
}
bool int_unionfind::unite(int e1, int e2)
{
// IPC - Immediate Parent Check
int p1 = id[e1];
int p2 = id[e2];
if ((p1 < 0 ? e1 : p1) == (p2 < 0 ? e2 : p2))
return false;
int root1 = root(e1);
int root2 = root(e2);
if (root1 == root2)
return false;
int rk1 = -id[root1];
int rk2 = -id[root2];
if (rk1 < rk2)
id[root1] = root2;
else {
id[root2] = root1;
if (rk1 == rk2)
id[root1] = -(rk1 + 1);
}
return true;
}
void int_unionfind::markdead(int e)
{
id[root(e)] = DEAD;
}
bool int_unionfind::sameset(int e1, int e2)
{
assert(e1 < (int)id.size() && e2 < (int)id.size());
return root(e1) == root(e2);
}
bool int_unionfind::isdead(int e)
{
assert(e < (int)id.size());
return root(e) == DEAD;
}
}

52
spot/mc/unionfind.hh Normal file
View file

@ -0,0 +1,52 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2015, 2016 Laboratoire de Recherche et
// Developpement de l'Epita
//
// 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 3 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 this program. If not, see <http://www.gnu.org/licenses/>.
#pragma once
#include <spot/misc/common.hh>
#include <vector>
namespace spot
{
/// \brief This Union-Find data structure is a particular
/// union-find, dedicated for emptiness checks below, see ec.hh. The
/// key of this union-find is int. Moreover, we suppose that only
/// consecutive int are inserted. This union-find includes most of
/// the classical optimisations (IPC, LR, PC, MS).
class SPOT_API int_unionfind final
{
private:
// Store the parent relation, i.e. -1 or x < id.size()
std::vector<int> id;
// id of a specially managed partition of "dead" elements
const int DEAD = 0;
int root(int i);
public:
int_unionfind();
void makeset(int e);
bool unite(int e1, int e2);
void markdead(int e);
bool sameset(int e1, int e2);
bool isdead(int e);
};
}