Commit afbaa54d authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

rewrite explicit Kripke structures and their parser

Fixes #4 and fixes #5.

* NEWS: Mention the change.
* src/kripkeparse/: Delete.
* README, src/Makefile.am, configure.ac: Adjust.
* src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
src/kripke/kripkeprint.cc, src/kripke/kripkeprint.hh: Delete.
* src/kripke/kripkegraph.hh: New file.
* src/kripke/Makefile.am: Adjust.
* src/parseaut/parseaut.yy, src/parseaut/public.hh: Add
an option to read kripke structures.
* src/tests/bad_parsing.test: Delete.
* src/tests/Makefile.am: Adjust.
* src/tests/kripke.test, src/tests/parse_print_test.cc: Rewrite.
* src/tests/ikwiad.cc, src/tests/parseaut.test,
iface/ltsmin/modelcheck.cc, wrap/python/spot_impl.i: Adjust.
parent 073d1545
......@@ -70,6 +70,14 @@ New in spot 1.99.5a (not yet released)
to syntethise larged automata with different acceptance
conditions.
* Explicit Kripke structure (i.e., stored as explciti graphs) have
been rewritten above the graph class, using an interface similar
to the twa class. The new class is called kripke_graph. The
custom Kripke parser and printer have been removed, because we can
now use print_hoa() with the "k" option to print Kripke structure
in the HOA format, and furthermore the parse_aut() function now
has an option to read HOA file and produce them as kripke_graph.
* Renamings:
is_guarantee_automaton() -> is_terminal_automaton()
tgba_run -> twa_run
......
......@@ -139,7 +139,6 @@ src/ Sources for libspot.
man/ Man pages for the above tools.
graph/ Graph representations.
kripke/ Kripke Structure interface.
kripkeparse/ Parser for explicit Kripke.
tl/ Temporal Logic formulas and algorithms.
misc/ Miscellaneous support files.
parseaut/ Parser for automata in multiple formats.
......@@ -147,7 +146,7 @@ src/ Sources for libspot.
priv/ Private algorithms, used internally but not exported.
ta/ TA objects and cousins (TGTA).
taalgos/ Algorithms on TA/TGTA.
tests/ Tests for the whole library.
tests/ Tests for the whole library.
twa/ TωA objects and cousins (Transition-based ω-Automata).
twaalgos/ Algorithms on TωA.
gtec/ Couvreur's Emptiness-Check.
......
......@@ -206,7 +206,6 @@ AC_CONFIG_FILES([
src/bin/man/Makefile
src/graph/Makefile
src/kripke/Makefile
src/kripkeparse/Makefile
src/Makefile
src/misc/Makefile
src/parseaut/Makefile
......
......@@ -28,8 +28,8 @@
#include "misc/timer.hh"
#include "misc/memusage.hh"
#include <cstring>
#include "kripke/kripkeexplicit.hh"
#include "kripke/kripkeprint.hh"
#include "kripke/kripkegraph.hh"
#include "twaalgos/hoa.hh"
static void
syntax(char* prog)
......@@ -236,7 +236,7 @@ checked_main(int argc, char **argv)
if (output == Kripke)
{
tm.start("kripke output");
spot::kripke_save_reachable_renumbered(std::cout, model);
spot::print_hoa(std::cout, model, "k");
tm.stop("kripke output");
goto safe_exit;
}
......
......@@ -26,14 +26,13 @@ AUTOMAKE_OPTIONS = subdir-objects
# end, after building '.' (since the current directory contains
# libspot.la needed by the tests)
SUBDIRS = misc priv tl graph twa twaalgos ta taalgos kripke \
kripkeparse parseaut parsetl . bin tests sanity
parseaut parsetl . bin tests sanity
lib_LTLIBRARIES = libspot.la
libspot_la_SOURCES =
libspot_la_LDFLAGS = $(BUDDY_LDFLAGS) -no-undefined $(SYMBOLIC_LDFLAGS)
libspot_la_LIBADD = \
kripke/libkripke.la \
kripkeparse/libkripkeparse.la \
misc/libmisc.la \
parseaut/libparseaut.la \
parsetl/libparsetl.la \
......
......@@ -26,12 +26,9 @@ kripke_HEADERS = \
fairkripke.hh \
fwd.hh \
kripke.hh \
kripkeexplicit.hh \
kripkeprint.hh
kripkegraph.hh
noinst_LTLIBRARIES = libkripke.la
libkripke_la_SOURCES = \
fairkripke.cc \
kripke.cc \
kripkeexplicit.cc \
kripkeprint.cc
kripke.cc
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE)
//
// 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 "kripkeexplicit.hh"
#include "twa/bddprint.hh"
#include "twa/formula2bdd.hh"
#include <iostream>
namespace spot
{
state_kripke::state_kripke()
: bdd_ (bddtrue)
{
}
void state_kripke::add_conditions(bdd f)
{
bdd_ &= f;
}
void state_kripke::add_succ(state_kripke* add_me)
{
// This method must add only state_kripke for now.
state_kripke* to_add = down_cast<state_kripke*>(add_me);
assert(to_add);
succ_.push_back(to_add);
}
int state_kripke::compare(const state* other) const
{
// This method should not be called to compare states from different
// automata, and all states from the same automaton will use the same
// state class.
const state_kripke* s = down_cast<const state_kripke*>(other);
assert(s);
return s - this;
}
size_t
state_kripke::hash() const
{
return
reinterpret_cast<const char*>(this) - static_cast<const char*>(nullptr);
}
state_kripke*
state_kripke::clone() const
{
return const_cast<state_kripke*>(this);
}
////////////////////////////
// Support for succ_iterator
const std::list<state_kripke*>&
state_kripke::get_succ() const
{
return succ_;
}
/////////////////////////////////////
// kripke_explicit_succ_iterator
kripke_explicit_succ_iterator::kripke_explicit_succ_iterator
(const state_kripke* s, bdd cond)
: kripke_succ_iterator(cond),
s_(s)
{
}
kripke_explicit_succ_iterator::~kripke_explicit_succ_iterator()
{
}
bool kripke_explicit_succ_iterator::first()
{
it_ = s_->get_succ().begin();
return it_ != s_->get_succ().end();
}
bool kripke_explicit_succ_iterator::next()
{
++it_;
return it_ != s_->get_succ().end();
}
bool kripke_explicit_succ_iterator::done() const
{
return it_ == s_->get_succ().end();
}
state_kripke* kripke_explicit_succ_iterator::dst() const
{
assert(!done());
return *it_;
}
/////////////////////////////////////
// kripke_explicit
kripke_explicit::kripke_explicit(const bdd_dict_ptr& dict,
state_kripke* init)
: kripke(dict),
init_(init)
{
}
std::string
kripke_explicit::format_state(const spot::state* s) const
{
assert(s);
const state_kripke* se = down_cast<const state_kripke*>(s);
assert(se);
std::map<const state_kripke*, std::string>::const_iterator it =
sn_nodes_.find (se);
assert(it != sn_nodes_.end());
return it->second;
}
kripke_explicit::~kripke_explicit()
{
get_dict()->unregister_all_my_variables(this);
std::map<const std::string, state_kripke*>::iterator it;
for (it = ns_nodes_.begin(); it != ns_nodes_.end(); ++it)
{
state_kripke* del_me = it->second;
delete del_me;
}
}
state_kripke*
kripke_explicit::get_init_state() const
{
return init_;
}
// FIXME: Change the bddtrue.
kripke_explicit_succ_iterator*
kripke_explicit::succ_iter(const spot::state* st) const
{
const state_kripke* s = down_cast<const state_kripke*>(st);
assert(s);
state_kripke* it = const_cast<state_kripke*>(s);
return new kripke_explicit_succ_iterator(it, bddtrue);
}
bdd
kripke_explicit::state_condition(const state* s) const
{
const state_kripke* f = down_cast<const state_kripke*>(s);
assert(f);
return (f->as_bdd());
}
bdd
kripke_explicit::state_condition(const std::string& name) const
{
std::map<const std::string, state_kripke*>::const_iterator it;
it = ns_nodes_.find(name);
assert(it != ns_nodes_.end());
return state_condition(it->second);
}
const std::map<const state_kripke*, std::string>&
kripke_explicit::sn_get() const
{
return sn_nodes_;
}
void kripke_explicit::add_state(std::string name,
state_kripke* state)
{
if (ns_nodes_.find(name) == ns_nodes_.end())
{
ns_nodes_[name] = state;
sn_nodes_[state] = name;
if (!init_)
init_ = state;
}
}
void kripke_explicit::add_state(std::string name)
{
if (ns_nodes_.find(name) == ns_nodes_.end())
{
state_kripke* state = new state_kripke;
add_state(name, state);
}
}
void kripke_explicit::add_transition(state_kripke* source,
const state_kripke* dest)
{
state_kripke* Dest = const_cast<state_kripke*>(dest);
source->add_succ(Dest);
}
void kripke_explicit::add_transition(std::string source,
const state_kripke* dest)
{
add_transition(ns_nodes_[source], dest);
}
void kripke_explicit::add_transition(std::string source,
std::string dest)
{
auto destination = ns_nodes_.find(dest);
if (destination == ns_nodes_.end())
{
state_kripke* neo = new state_kripke;
add_state(dest, neo);
add_transition(source, neo);
}
else
{
add_transition(source, destination->second);
}
}
void kripke_explicit::add_conditions(bdd add,
state_kripke* on_me)
{
on_me->add_conditions(add);
}
void kripke_explicit::add_conditions(bdd add,
std::string on_me)
{
add_conditions(add, ns_nodes_[on_me]);
}
void kripke_explicit::add_condition(formula f, std::string on_me)
{
add_conditions(formula_to_bdd(f, get_dict(), this), on_me);
}
} // End namespace spot.
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche
// et Développement de l'Epita (LRDE)
//
// 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 <iosfwd>
#include "kripke.hh"
#include "tl/formula.hh"
#include "kripkeprint.hh"
namespace spot
{
/// \brief Concrete class for kripke states.
class SPOT_API state_kripke : public state
{
friend class kripke_explicit;
friend class kripke_explicit_succ_iterator;
private:
state_kripke();
/// \brief Compare two states.
///
/// This method returns an integer less than, equal to, or greater
/// than zero if \a this is found, respectively, to be less than, equal
/// to, or greater than \a other according to some implicit total order.
///
/// For moment, this method only compare the adress on the heap of the
/// twice pointers.
virtual int compare (const state* other) const;
/// \brief Hash a state
virtual size_t hash() const;
/// \brief Duplicate a state.
virtual state_kripke* clone() const;
/// \brief Add a condition to the conditions already in the state.
/// \param f The condition to add.
void add_conditions(bdd f);
/// \brief Add a new successor in the list.
/// \param succ The successor state to add.
void add_succ(state_kripke* succ);
virtual bdd
as_bdd() const
{
return bdd_;
}
/// \brief Release a state.
///
virtual void
destroy() const
{
}
virtual
~state_kripke ()
{
}
////////////////////////////////
// Management for succ_iterator
const std::list<state_kripke*>& get_succ() const;
bdd bdd_;
std::list<state_kripke*> succ_;
};
/// \class kripke_explicit_succ_iterator
/// \brief Implement iterator pattern on successor of a state_kripke.
class SPOT_API kripke_explicit_succ_iterator : public kripke_succ_iterator
{
public:
kripke_explicit_succ_iterator(const state_kripke*, bdd);
~kripke_explicit_succ_iterator();
virtual bool first();
virtual bool next();
virtual bool done() const;
virtual state_kripke* dst() const;
private:
const state_kripke* s_;
std::list<state_kripke*>::const_iterator it_;
};
/// \class kripke_explicit
/// \brief Kripke Structure.
class SPOT_API kripke_explicit : public kripke
{
public:
kripke_explicit(const bdd_dict_ptr&, state_kripke* = nullptr);
~kripke_explicit();
state_kripke* get_init_state() const;
/// \brief Allow to get an iterator on the state we passed in
/// parameter.
kripke_explicit_succ_iterator*
succ_iter(const spot::state* state) const;
/// \brief Get the condition on the state
bdd state_condition(const state* s) const;
/// \brief Get the condition on the state
bdd state_condition(const std::string&) const;
/// \brief Return the name of the state.
std::string format_state(const state*) const;
/// \brief Create state, if it does not already exists.
///
/// Used by the parser.
void add_state(std::string);
/// \brief Add a transition between two states.
void add_transition(std::string source,
std::string dest);
/// \brief Add a BDD condition to the state
///
/// \param add the condition.
/// \param on_me where add the condition.
void add_conditions(bdd add,
std::string on_me);
/// \brief Add a formula to the state corresponding to the name.
///
/// \param f the formula to add.
/// \param on_me the state where to add.
void add_condition(formula f, std::string on_me);
/// \brief Return map between states and their names.
const std::map<const state_kripke*, std::string>&
sn_get() const;
private:
/// \brief Add a state in the two maps.
void add_state(std::string, state_kripke*);
void add_conditions(bdd add,
state_kripke* on_me);
void add_transition(std::string source,
const state_kripke* dest);
void add_transition(state_kripke* source,
const state_kripke* dest);
state_kripke* init_;
std::map<const std::string, state_kripke*> ns_nodes_;
std::map<const state_kripke*, std::string> sn_nodes_;
};
inline kripke_explicit_ptr
make_kripke_explicit(const bdd_dict_ptr& d,
state_kripke* init = nullptr)
{
return std::make_shared<kripke_explicit>(d, init);
}
}
// -*- coding: utf-8 -*-
// Copyright (C) 2011, 2012, 2013, 2014, 2015 Laboratoire de Recherche
// et Développement de l'Epita (LRDE)
//
// 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 <iosfwd>
#include "kripke.hh"
#include "graph/graph.hh"
#include "tl/formula.hh"
namespace spot
{
/// \brief Concrete class for kripke_graph states.
struct SPOT_API kripke_graph_state: public spot::state
{
public:
kripke_graph_state(bdd cond = bddfalse) noexcept
: cond_(cond)
{
}
virtual ~kripke_graph_state() noexcept
{
}
virtual int compare(const spot::state* other) const
{
auto o = down_cast<const kripke_graph_state*>(other);
assert(o);
// Do not simply return "other - this", it might not fit in an int.
if (o < this)
return -1;
if (o > this)
return 1;
return 0;
}
virtual size_t hash() const
{
return
reinterpret_cast<const char*>(this) - static_cast<const char*>(nullptr);
}
virtual kripke_graph_state*
clone() const
{
return const_cast<kripke_graph_state*>(this);
}
virtual void destroy() const
{
}
bdd cond() const
{
return cond_;
}
void cond(bdd c)
{
cond_ = c;
}
private:
bdd cond_;
};
template<class Graph>
class SPOT_API kripke_graph_succ_iterator final: public kripke_succ_iterator
{
private:
typedef typename Graph::edge edge;
typedef typename Graph::state_data_t state;
const Graph* g_;
edge t_;
edge p_;
public:
kripke_graph_succ_iterator(const Graph* g,
const typename Graph::state_storage_t* s):
kripke_succ_iterator(s->cond()),
g_(g),
t_(s->succ)
{
}