Commit bb5949f6 authored by Thomas Badie's avatar Thomas Badie Committed by Alexandre Duret-Lutz

Add text I/O for Kripke structures.

* src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
src/kripke/kripkeprint.cc, src/kripke/kripkeprint.hh: New files.
* src/kripke/Makefile.am: Add them.
* src/kripkeparse/fmterror.cc, src/kripkeparse/kripkeparse.yy,
src/kripkeparse/kripkescan.ll, src/kripkeparse/parsedecl.hh,
src/kripkeparse/public.hh, src/kripkeparse/scankripke.ll: New
files.
* src/kripkeparse/Makefile.am: Add them.
* src/kripketest/bad_parsing.test, src/kripketest/defs.in,
src/kripketest/kripke.test, src/kripketest/origin,
src/kripketest/parse_print_test.cc: New files.
* src/kripketest/Makefile.am: Add them.
* src/Makefile.am (SUBDIRS): Add kripkeparse and kripketest.
* README: Document src/kripketest/ and src/kripkeparse/.
* configure.ac: Generate src/kripkeparse/Makefile,
src/kripketest/Makefile, src/kripketest/defs.
* iface/dve2/defs.in (run2): New function.
* iface/dve2/dve2check.cc (syntax, main): Add option -gK.
* iface/dve2/kripke.test: New file.
* iface/dve2/Makefile.am (TESTS): Add kripke.test.
parent 71d1a4fe
2011-05-07 Thomas Badie <badie@lrde.epita.fr>
Add text I/O for Kripke structures.
* src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
src/kripke/kripkeprint.cc, src/kripke/kripkeprint.hh: New files.
* src/kripke/Makefile.am: Add them.
* src/kripkeparse/fmterror.cc, src/kripkeparse/kripkeparse.yy,
src/kripkeparse/kripkescan.ll, src/kripkeparse/parsedecl.hh,
src/kripkeparse/public.hh, src/kripkeparse/scankripke.ll: New
files.
* src/kripkeparse/Makefile.am: Add them.
* src/kripketest/bad_parsing.test, src/kripketest/defs.in,
src/kripketest/kripke.test, src/kripketest/origin,
src/kripketest/parse_print_test.cc: New files.
* src/kripketest/Makefile.am: Add them.
* src/Makefile.am (SUBDIRS): Add kripkeparse and kripketest.
* README: Document src/kripketest/ and src/kripkeparse/.
* configure.ac: Generate src/kripkeparse/Makefile,
src/kripketest/Makefile, src/kripketest/defs.
* iface/dve2/defs.in (run2): New function.
* iface/dve2/dve2check.cc (syntax, main): Add option -gK.
* iface/dve2/kripke.test: New file.
* iface/dve2/Makefile.am (TESTS): Add kripke.test.
2011-11-24 Alexandre Duret-Lutz <adl@lrde.epita.fr>
Fix bench/emptchk/pml2tgba.pl for more recent Spin version.
......
......@@ -107,6 +107,8 @@ Core directories
src/ Sources for libspot.
kripke/ Kripke Structure interface.
kripkeparse/ Parser for explicit Kripke.
kripketest/ Tests for kripke explicit.
ltlast/ LTL abstract syntax tree (including nodes for ELTL).
ltlenv/ LTL environments.
ltlparse/ Parser for LTL formulae.
......
......@@ -118,6 +118,9 @@ AC_CONFIG_FILES([
src/ltlast/Makefile
src/ltlenv/Makefile
src/ltlparse/Makefile
src/kripkeparse/Makefile
src/kripketest/Makefile
src/kripketest/defs
src/ltltest/defs
src/ltltest/Makefile
src/ltlvisit/Makefile
......
......@@ -38,7 +38,7 @@ dve2check_LDADD = libspotdve2.la
check_SCRIPTS = defs
TESTS = dve2check.test finite.test
TESTS = dve2check.test finite.test kripke.test
EXTRA_DIST = $(TESTS) beem-peterson.4.dve finite.dve
distclean-local:
......
......@@ -88,4 +88,40 @@ run()
test $exitcode = $expected_exitcode || exit 1
}
run2()
{
expected_exitcode=$1
shift
exitcode=0
if test -n "$VALGRIND"; then
exec 6>valgrind.err
GLIBCPP_FORCE_NEW=1 \
../../../libtool --mode=execute \
$VALGRIND --tool=memcheck --leak-check=yes --log-fd=6 -q "$@" | grep -v + > log ||
exitcode=$?
cat valgrind.err 1>&2
test -z "`sed 1q valgrind.err`" || exit 50
rm -f valgrind.err
else
"$@" || exitcode=$?
fi
test $exitcode = $expected_exitcode || exit 1
exec 6>valgrind.err
../../../libtool --mode=execute \
$VALGRIND --tool=memcheck --leak-check=yes --log-fd=6 -q $1 log \
| grep -v + > log2 ||
exitcode=$?
cat valgrind.err 1>&2
test -z "`sed 1q valgrind.err`" || exit 50
rm -f valgrind.err
test $exitcode = $expected_exitcode || exit 1
diff log log2 || exit 42
rm -f log log2
}
set -x
......@@ -33,6 +33,8 @@
#include "misc/timer.hh"
#include "misc/memusage.hh"
#include <cstring>
#include "kripke/kripkeexplicit.hh"
#include "kripke/kripkeprint.hh"
static void
syntax(char* prog)
......@@ -58,6 +60,8 @@ syntax(char* prog)
<< std::endl
<< " -gm output the model state-space in dot format"
<< std::endl
<< " -gK output the model state-space in Kripke format"
<< std::endl
<< " -gp output the product state-space in dot format"
<< std::endl
<< " -T time the different phases of the execution"
......@@ -80,7 +84,7 @@ main(int argc, char **argv)
bool use_timer = false;
enum { DotFormula, DotModel, DotProduct, EmptinessCheck }
enum { DotFormula, DotModel, DotProduct, EmptinessCheck, Kripke }
output = EmptinessCheck;
bool accepting_run = false;
bool expect_counter_example = false;
......@@ -128,6 +132,9 @@ main(int argc, char **argv)
case 'f':
output = DotFormula;
break;
case 'K':
output = Kripke;
break;
default:
goto error;
}
......@@ -242,6 +249,14 @@ main(int argc, char **argv)
tm.stop("dotty output");
goto safe_exit;
}
if (output == Kripke)
{
tm.start("kripke output");
spot::KripkePrinter p (model, std::cout);
p.run();
tm.stop("kripke output");
goto safe_exit;
}
}
......
#! /bin/sh
# Copyright (C) 2011 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 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.
. ./defs
divine compile > output 2>&1
if grep -i ltsmin output; then
:
else
echo "divine not installed, or no ltsmin interface"
exit 77
fi
set -e
run 0 ${top_builddir}/iface/dve2/dve2check -gK \
${srcdir}/finite.dve 'F("P.a > 5")' | grep -v + > parse
run2 0 ${top_builddir}/src/kripketest/parse_print parse
rm -f parse
......@@ -28,8 +28,8 @@ AUTOMAKE_OPTIONS = subdir-objects
# libspot.la needed by the tests).
SUBDIRS = misc ltlenv ltlast ltlvisit ltlparse eltlparse tgba \
tgbaalgos tgbaparse evtgba evtgbaalgos evtgbaparse kripke \
saba sabaalgos neverparse . ltltest eltltest tgbatest \
evtgbatest sabatest sanity
saba sabaalgos neverparse kripkeparse . ltltest eltltest \
tgbatest evtgbatest sabatest sanity kripketest
lib_LTLIBRARIES = libspot.la
libspot_la_SOURCES =
......@@ -50,7 +50,8 @@ libspot_la_LIBADD = \
evtgbaparse/libevtgbaparse.la \
saba/libsaba.la \
sabaalgos/libsabaalgos.la \
kripke/libkripke.la
kripke/libkripke.la \
kripkeparse/libkripkeparse.la
# Dummy C++ source to cause C++ linking.
nodist_EXTRA_libspot_la_SOURCES = _.cc
......
......@@ -24,9 +24,13 @@ kripkedir = $(pkgincludedir)/kripke
kripke_HEADERS = \
fairkripke.hh \
kripke.hh
kripke.hh \
kripkeexplicit.hh \
kripkeprint.hh
noinst_LTLIBRARIES = libkripke.la
libkripke_la_SOURCES = \
fairkripke.cc \
kripke.cc
kripke.cc \
kripkeexplicit.cc \
kripkeprint.cc
// Copyright (C) 2011 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 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 "kripkeexplicit.hh"
#include "../tgba/bddprint.hh"
#include "tgba/formula2bdd.hh"
#include <iostream>
#include "../tgba/state.hh"
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*>(0);
}
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()
{
}
void kripke_explicit_succ_iterator::first()
{
it_ = s_->get_succ().begin();
}
void kripke_explicit_succ_iterator::next()
{
++it_;
}
bool kripke_explicit_succ_iterator::done() const
{
return it_ == s_->get_succ().end();
}
state_kripke* kripke_explicit_succ_iterator::current_state() const
{
assert(!done());
return *it_;
}
/////////////////////////////////////
// kripke_explicit
kripke_explicit::kripke_explicit(bdd_dict* dict)
: dict_(dict),
init_(0)
{
}
kripke_explicit::kripke_explicit(bdd_dict* dict,
state_kripke* init)
: dict_(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()
{
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_;
}
bdd_dict*
kripke_explicit::get_dict() const
{
return dict_;
}
// FIXME : Change the bddtrue.
kripke_explicit_succ_iterator*
kripke_explicit::succ_iter(const spot::state* local_state,
const spot::state* global_state,
const tgba* global_automaton) const
{
const state_kripke* s = down_cast<const state_kripke*>(local_state);
assert(s);
(void) global_state;
(void) global_automaton;
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)
{
state_kripke* neo = 0;
std::map<std::string, state_kripke*>::iterator destination
= ns_nodes_.find(dest);
if (ns_nodes_.find(dest) == ns_nodes_.end())
{
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(const ltl::formula* f,
std::string on_me)
{
add_conditions(formula_to_bdd(f, dict_, this), on_me);
f->destroy();
}
} // End namespace spot.
// Copyright (C) 2011 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 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_KRIPKE_KRIPKEEXPLICIT_HH
# define SPOT_KRIPKE_KRIPKEEXPLICIT_HH
# include <iosfwd>
# include "kripke.hh"
# include "ltlast/formula.hh"
# include "kripkeprint.hh"
namespace spot
{
// Define in kripkeprint.hh
class KripkeVisitor;
/// \brief Concrete class for kripke states.
class 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
///
/// \FIXME For moment : Only there to can instantiate state_kripke.
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 add_me The state to add.
void add_succ(state_kripke*);
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 kripke_explicit_succ_iterator : public kripke_succ_iterator
{
public:
kripke_explicit_succ_iterator(const state_kripke*,
bdd);