From bb5949f6de8295128f91ad5974d5e951ba6b5b44 Mon Sep 17 00:00:00 2001 From: Thomas Badie Date: Thu, 24 Nov 2011 22:47:41 +0100 Subject: [PATCH] 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. --- ChangeLog | 25 +++ README | 2 + configure.ac | 3 + iface/dve2/Makefile.am | 2 +- iface/dve2/defs.in | 36 ++++ iface/dve2/dve2check.cc | 17 +- iface/dve2/kripke.test | 42 +++++ src/Makefile.am | 7 +- src/kripke/Makefile.am | 8 +- src/kripke/kripkeexplicit.cc | 290 +++++++++++++++++++++++++++++ src/kripke/kripkeexplicit.hh | 194 +++++++++++++++++++ src/kripke/kripkeprint.cc | 66 +++++++ src/kripke/kripkeprint.hh | 53 ++++++ src/kripkeparse/.gitignore | 11 ++ src/kripkeparse/Makefile.am | 65 +++++++ src/kripkeparse/fmterror.cc | 43 +++++ src/kripkeparse/kripkeparse.yy | 230 +++++++++++++++++++++++ src/kripkeparse/kripkescan.ll | 115 ++++++++++++ src/kripkeparse/parsedecl.hh | 41 ++++ src/kripkeparse/public.hh | 68 +++++++ src/kripkeparse/scankripke.ll | 117 ++++++++++++ src/kripketest/.gitignore | 2 + src/kripketest/Makefile.am | 42 +++++ src/kripketest/bad_parsing.test | 91 +++++++++ src/kripketest/defs.in | 128 +++++++++++++ src/kripketest/kripke.test | 71 +++++++ src/kripketest/origin | 4 + src/kripketest/parse_print_test.cc | 58 ++++++ 28 files changed, 1824 insertions(+), 7 deletions(-) create mode 100755 iface/dve2/kripke.test create mode 100644 src/kripke/kripkeexplicit.cc create mode 100644 src/kripke/kripkeexplicit.hh create mode 100644 src/kripke/kripkeprint.cc create mode 100644 src/kripke/kripkeprint.hh create mode 100644 src/kripkeparse/.gitignore create mode 100644 src/kripkeparse/Makefile.am create mode 100644 src/kripkeparse/fmterror.cc create mode 100644 src/kripkeparse/kripkeparse.yy create mode 100644 src/kripkeparse/kripkescan.ll create mode 100644 src/kripkeparse/parsedecl.hh create mode 100644 src/kripkeparse/public.hh create mode 100644 src/kripkeparse/scankripke.ll create mode 100644 src/kripketest/.gitignore create mode 100644 src/kripketest/Makefile.am create mode 100755 src/kripketest/bad_parsing.test create mode 100644 src/kripketest/defs.in create mode 100755 src/kripketest/kripke.test create mode 100644 src/kripketest/origin create mode 100644 src/kripketest/parse_print_test.cc diff --git a/ChangeLog b/ChangeLog index 431485ee2..9eca0327a 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,28 @@ +2011-05-07 Thomas Badie + + 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 Fix bench/emptchk/pml2tgba.pl for more recent Spin version. diff --git a/README b/README index 3692a71f0..485748b5b 100644 --- a/README +++ b/README @@ -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. diff --git a/configure.ac b/configure.ac index 3c00fd337..e34f7b72f 100644 --- a/configure.ac +++ b/configure.ac @@ -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 diff --git a/iface/dve2/Makefile.am b/iface/dve2/Makefile.am index dc74b995a..aef5a7530 100644 --- a/iface/dve2/Makefile.am +++ b/iface/dve2/Makefile.am @@ -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: diff --git a/iface/dve2/defs.in b/iface/dve2/defs.in index fccf16cd0..fd8ed2bb7 100644 --- a/iface/dve2/defs.in +++ b/iface/dve2/defs.in @@ -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 diff --git a/iface/dve2/dve2check.cc b/iface/dve2/dve2check.cc index cffc5e808..ee994b489 100644 --- a/iface/dve2/dve2check.cc +++ b/iface/dve2/dve2check.cc @@ -33,6 +33,8 @@ #include "misc/timer.hh" #include "misc/memusage.hh" #include +#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; + } } diff --git a/iface/dve2/kripke.test b/iface/dve2/kripke.test new file mode 100755 index 000000000..984e88267 --- /dev/null +++ b/iface/dve2/kripke.test @@ -0,0 +1,42 @@ +#! /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 diff --git a/src/Makefile.am b/src/Makefile.am index bc78f2485..46898d037 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -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 diff --git a/src/kripke/Makefile.am b/src/kripke/Makefile.am index 79169cfed..2fdd84c44 100644 --- a/src/kripke/Makefile.am +++ b/src/kripke/Makefile.am @@ -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 diff --git a/src/kripke/kripkeexplicit.cc b/src/kripke/kripkeexplicit.cc new file mode 100644 index 000000000..3153f4ff3 --- /dev/null +++ b/src/kripke/kripkeexplicit.cc @@ -0,0 +1,290 @@ +// 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 +#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(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(other); + assert(s); + return s - this; + } + + size_t + state_kripke::hash() const + { + return + reinterpret_cast(this) - static_cast(0); + } + + state_kripke* + state_kripke::clone() const + { + return const_cast(this); + } + + //////////////////////////// + // Support for succ_iterator + + const std::list& + 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(s); + assert(se); + std::map::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::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(local_state); + assert(s); + (void) global_state; + (void) global_automaton; + state_kripke* it = const_cast(s); + return new kripke_explicit_succ_iterator(it, bddtrue); + } + + bdd + kripke_explicit::state_condition(const state* s) const + { + const state_kripke* f = down_cast(s); + assert(f); + return (f->as_bdd()); + } + + bdd + kripke_explicit::state_condition(const std::string name) const + { + std::map::const_iterator it; + it = ns_nodes_.find(name); + assert(it != ns_nodes_.end()); + return state_condition(it->second); + } + + const std::map& + 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(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::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. diff --git a/src/kripke/kripkeexplicit.hh b/src/kripke/kripkeexplicit.hh new file mode 100644 index 000000000..1d9aefc8f --- /dev/null +++ b/src/kripke/kripkeexplicit.hh @@ -0,0 +1,194 @@ +// 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 +# 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& get_succ() const; + + bdd bdd_; + std::list 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); + + ~kripke_explicit_succ_iterator(); + + virtual void first(); + virtual void next(); + virtual bool done() const; + + virtual state_kripke* current_state() const; + + private: + const state_kripke* s_; + std::list::const_iterator it_; + }; + + + /// \class kripke_explicit + /// \brief Kripke Structure. + class kripke_explicit : public kripke + { + public: + kripke_explicit(bdd_dict*); + kripke_explicit(bdd_dict*, state_kripke*); + ~kripke_explicit(); + + bdd_dict* get_dict() const; + 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* local_state, + const spot::state* global_state = 0, + const tgba* global_automaton = 0) const; + + /// \function state_condition + /// \brief Get the condition on the state, designed by the adress, + /// or by his name. + bdd state_condition(const state* s) const; + bdd state_condition(const std::string) const; + + /// \brief Return the name of the state. + std::string format_state(const state*) const; + + + + /// \brief Check if the state already exist, and create it if not. + /// used by the parser for more simplicity. + void add_state(std::string); + + /// \function add_transition + /// \brief Add a transition between two state. + /// Allow to do this with the two adress, or just the source adress, + void add_transition(std::string source, + std::string dest); + + /// \function add_conditions + /// \brief Add a condition in bdd format to the state, + /// name by his name or his address. + /// \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 on_me The state where add. + /// \param f the formula to add. + void add_condition(const ltl::formula* f, + std::string on_me); + + const std::map& + sn_get() const; + + private: + /// \brief Add a state in the two map. + void add_state(std::string, state_kripke*); + + void add_conditions(bdd add, + state_kripke* on_me); + + /// or with the two name. + void add_transition(state_kripke* source, + const state_kripke* dest); + void add_transition(std::string source, + const state_kripke* dest); + + + + + bdd_dict* dict_; + state_kripke* init_; + std::map ns_nodes_; + std::map sn_nodes_; + }; +} +#endif /* !SPOT_KRIPKEEXPLICIT_HH_ */ diff --git a/src/kripke/kripkeprint.cc b/src/kripke/kripkeprint.cc new file mode 100644 index 000000000..be4c312b6 --- /dev/null +++ b/src/kripke/kripkeprint.cc @@ -0,0 +1,66 @@ +// 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 "kripkeprint.hh" +#include "kripkeexplicit.hh" +#include "../tgba/bddprint.hh" +#include "misc/escape.hh" +#include + +namespace spot +{ + KripkePrinter::KripkePrinter(const kripke* automata, + std::ostream& os) + : tgba_reachable_iterator_breadth_first(automata), os_(os) + { + } + + void KripkePrinter::start() + { + } + + void KripkePrinter::process_state(const state* s, + int, + tgba_succ_iterator* si) + { + const bdd_dict* d = automata_->get_dict(); + std::string cur = automata_->format_state(s); + os_ << "\""; + escape_str(os_, automata_->format_state(s)); + os_ << "\", \""; + const kripke* automata = down_cast + (automata_); + assert(automata); + escape_str(os_, bdd_format_formula(d, + automata->state_condition(s))); + + os_ << "\","; + for (si->first(); !si->done(); si->next()) + { + state* dest = si->current_state(); + os_ << " \""; + escape_str(os_, automata_->format_state(dest)); + os_ << "\""; + } + os_ << ";" << std::endl; + } + +} // End namespace Spot diff --git a/src/kripke/kripkeprint.hh b/src/kripke/kripkeprint.hh new file mode 100644 index 000000000..124b6f735 --- /dev/null +++ b/src/kripke/kripkeprint.hh @@ -0,0 +1,53 @@ +// 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_KRIPKEPRINT_HH +# define SPOT_KRIPKE_KRIPKEPRINT_HH + +# include +# include "tgbaalgos/reachiter.hh" +namespace spot +{ + + class kripke_explicit; + class state_kripke; + class kripke_succ_iterator; + class kripke; + + /// \brief Iterate over all reachable states of a spot::kripke + /// Override start and process_state methods from + /// tgba_reachable_iterator_breadth_first. + class KripkePrinter : public tgba_reachable_iterator_breadth_first + { + public: + KripkePrinter(const kripke* state, std::ostream& os); + + void start(); + + void process_state(const state*, int, tgba_succ_iterator* si); + + private: + std::ostream& os_; + }; + +} // End namespace spot + +#endif /* !KRIPKEPRINT_HH_ */ diff --git a/src/kripkeparse/.gitignore b/src/kripkeparse/.gitignore new file mode 100644 index 000000000..0bb28fc07 --- /dev/null +++ b/src/kripkeparse/.gitignore @@ -0,0 +1,11 @@ +Makefile +Makefile.in +location.hh +kripkeparse.hh +kripkeparse.cc +kripkeparse.output +kripkescan.cc +position.hh +stack.hh +*.lo +*.la diff --git a/src/kripkeparse/Makefile.am b/src/kripkeparse/Makefile.am new file mode 100644 index 000000000..7df816daa --- /dev/null +++ b/src/kripkeparse/Makefile.am @@ -0,0 +1,65 @@ +## Copyright (C) 2011 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 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. + +AM_CPPFLAGS = -I$(srcdir)/.. $(BUDDY_CPPFLAGS) -DYY_NO_INPUT +# Disable -Werror because too many versions of flex yield warnings. +AM_CXXFLAGS = $(WARNING_CXXFLAGS:-Werror=) + +kripkeparsedir = $(pkgincludedir)/kripkeparse + +kripkeparse_HEADERS = \ + public.hh \ + location.hh \ + position.hh + +noinst_LTLIBRARIES = libkripkeparse.la + +KRIPKEPARSE_YY = kripkeparse.yy +FROM_KRIPKEPARSE_YY_MAIN = kripkeparse.cc +FROM_KRIPKEPARSE_YY_OTHERS = \ + stack.hh \ + position.hh \ + location.hh \ + kripkeparse.hh + +FROM_KRIPKEPARSE_YY = \ + $(FROM_KRIPKEPARSE_YY_MAIN) \ + $(FROM_KRIPKEPARSE_YY_OTHERS) + +BUILT_SOURCES = $(FROM_KRIPKEPARSE_YY) +MAINTAINERCLEANFILES = $(FROM_KRIPKEPARSE_YY) + +$(FROM_KRIPKEPARSE_YY_MAIN): $(srcdir)/$(KRIPKEPARSE_YY) +## We must cd into $(srcdir) first because if we tell bison to read +## $(srcdir)/$(KRIPKEPARSE_YY), it will also use the value of $(srcdir)/ +## in the generated include statements. + cd $(srcdir) && \ + bison -Wall -Werror --report=all \ + $(KRIPKEPARSE_YY) -o $(FROM_KRIPKEPARSE_YY_MAIN) +$(FROM_KRIPKEPARSE_YY_OTHERS): $(KRIPKEPARSE_YY) + @test -f $@ || $(MAKE) $(AM_MAKEFLAGS) $(FROM_KRIPKEPARSE_YY_MAIN) + +EXTRA_DIST = $(KRIPKEPARSE_YY) + +libkripkeparse_la_SOURCES = \ + $(FROM_KRIPKEPARSE_YY) \ + kripkescan.ll \ + parsedecl.hh \ + fmterror.cc diff --git a/src/kripkeparse/fmterror.cc b/src/kripkeparse/fmterror.cc new file mode 100644 index 000000000..0ae5549bf --- /dev/null +++ b/src/kripkeparse/fmterror.cc @@ -0,0 +1,43 @@ +// 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 +#include "public.hh" + +namespace spot +{ + bool + format_kripke_parse_errors(std::ostream& os, + const std::string& filename, + kripke_parse_error_list& error_list) + { + bool printed = false; + spot::kripke_parse_error_list::iterator it; + for (it = error_list.begin(); it != error_list.end(); ++it) + { + if (filename != "-") + os << filename << ":"; + os << it->first << ": "; + os << it->second << std::endl; + printed = true; + } + return printed; + } +} diff --git a/src/kripkeparse/kripkeparse.yy b/src/kripkeparse/kripkeparse.yy new file mode 100644 index 000000000..4b4c0fad3 --- /dev/null +++ b/src/kripkeparse/kripkeparse.yy @@ -0,0 +1,230 @@ +// 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. + +%language "C++" +%locations +%defines +%expect 0 +%name-prefix "kripkeyy" +%debug +%error-verbose + +%code requires +{ +#include +#include +#include "public.hh" + +/* Cache parsed formulae. Labels on arcs are frequently identical and + it would be a waste of time to parse them to formula* over and + over, and to register all their atomic_propositions in the + bdd_dict. Keep the bdd result around so we can reuse it. */ +typedef std::map formula_cache; +} + +%parse-param {spot::kripke_parse_error_list& error_list} +%parse-param {spot::ltl::environment& parse_environment} +%parse-param {spot::kripke_explicit*& result} +%parse-param {formula_cache& fcache} + +%union +{ + int token; + std::string* str; + spot::ltl::formula* f; + std::list* list; +} + +%code +{ +#include "kripke/kripkeexplicit.hh" + /* Unfortunately Bison 2.3 uses the same guards in all parsers :( */ +#undef BISON_POSITION_HH +#undef BISON_LOCATION_HH +#include "ltlparse/public.hh" +#include + +/* tgbaparse.hh and parsedecl.hh include each other recursively. + We must ensure that YYSTYPE is declared (by the above %union) + before parsedecl.hh uses it. */ +#include "parsedecl.hh" + +using namespace spot::ltl; +#include + //typedef std::pair pair; +} + +%token STRING UNTERMINATED_STRING IDENT +%token COMA "," +%token SEMICOL ";" +%type strident string +%type condition +%type follow_list + +%destructor { delete $$; } +%destructor { + std::cout << $$->size() << std::endl; + for (std::list::iterator i = $$->begin(); + i != $$->end(); ++i) + delete (*i); + delete $$; + } + +%printer { debug_stream() << *$$; } + +%% + +kripke: +lines { + } +| { +} +; + +/* At least one line. */ +lines: line { } +| lines line { } + ; + +line: +strident "," condition "," follow_list ";" +{ + result->add_state(*$1); + if ($3) + { + formula_cache::const_iterator i = fcache.find(*$3); + if (i == fcache.end()) + { + parse_error_list pel; + formula* f = spot::ltl::parse(*$3, pel, parse_environment); + for (parse_error_list::iterator i = pel.begin(); + i != pel.end(); ++i) + { + //Adjust the diagnostic to the current position. + location here = @3; + here.end.line = here.begin.line + i->first.end.line - 1; + here.end.column = + here.begin.column + i->first.end.column; + here.begin.line += i->first.begin.line - 1; + here.begin.column += i->first.begin.column; + error_list.push_back(spot::kripke_parse_error(here, + i->second)); + } + if (f) + result->add_condition(f, *$1); + else + result->add_conditions(bddfalse, *$1); + fcache[*$3] = result->state_condition(*$1); + } + else + { + result->add_conditions(i->second, *$1); + } + delete $3; + } + std::list::iterator i; + for (i = $5->begin(); i != $5->end(); ++i) + { + result->add_transition(*$1, **i); + delete *i; + } + + delete $1; + delete $5; +} +; + + +string: STRING + { $$ = $1; } + | UNTERMINATED_STRING + { + $$ = $1; + error_list.push_back(spot::kripke_parse_error(@1, + "unterminated string")); + } +; + +strident: string +{ $$ = $1; } +| IDENT +{ $$ = $1; } +; + +follow_list: +follow_list strident +{ + $$ = $1; + $$->push_back($2); +} +| { + $$ = new std::list; + } +; + +condition: + { + $$ = 0; + } + | string + { + $$ = $1; + } + ; + +%% + +void +kripkeyy::parser::error(const location_type& location, + const std::string& message) +{ + error_list.push_back(spot::kripke_parse_error(location, message)); +} + +namespace spot +{ + kripke_explicit* + kripke_parse(const std::string& name, + kripke_parse_error_list& error_list, + bdd_dict* dict, + environment& env, + bool debug) + { + if (kripkeyyopen(name)) + { + error_list.push_back + (kripke_parse_error(kripkeyy::location(), + std::string("Cannot open file ") + name)); + return 0; + } + formula_cache fcache; + kripke_explicit* result = new kripke_explicit(dict); + kripkeyy::parser parser(error_list, env, result, fcache); + parser.set_debug_level(debug); + parser.parse(); + kripkeyyclose(); + + return result; + } +} + +// Local Variables: +// mode: c++ +// End: diff --git a/src/kripkeparse/kripkescan.ll b/src/kripkeparse/kripkescan.ll new file mode 100644 index 000000000..93aa34ec9 --- /dev/null +++ b/src/kripkeparse/kripkescan.ll @@ -0,0 +1,115 @@ +/* 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.*/ + +%option noyywrap +%option prefix="kripkeyy" +%option outfile="lex.yy.c" +%x STATE_STRING + +%{ +#include +#include "kripkeparse/parsedecl.hh" + + +#define YY_USER_ACTION \ + yylloc->columns(yyleng); + +#define YY_NEVER_INTERACTIVE 1 + + typedef kripkeyy::parser::token token; + + +%} + +eol \n|\r|\n\r|\r\n + +%% + +%{ + yylloc->step (); +%} + +[a-zA-Z][a-zA-Z0-9_]* { + yylval->str = new std::string(yytext, yyleng); + return token::IDENT; + } + + /* discard whitespace */ +{eol} yylloc->lines(yyleng); yylloc->step(); +[ \t]+ yylloc->step(); + +\" { + yylval->str = new std::string; + BEGIN(STATE_STRING); + } + +"," { + return token::COMA; + } + +";" return token::SEMICOL; + +. return *yytext; + + /* Handle \" and \\ in strings. */ +{ + \" { + BEGIN(INITIAL); + return token::STRING; + } + \\["\\] yylval->str->append(1, yytext[1]); + [^"\\]+ yylval->str->append(yytext, yyleng); + <> { + BEGIN(INITIAL); + return token::UNTERMINATED_STRING; + } +} + +%{ + /* Dummy use of yyunput to shut up a gcc warning. */ + (void) &yyunput; +%} + +%% + +namespace spot +{ + int + kripkeyyopen(const std::string &name) + { + if (name == "-") + { + yyin = stdin; + } + else + { + yyin = fopen(name.c_str(), "r"); + if (!yyin) + return 1; + } + return 0; + } + + void + kripkeyyclose() + { + fclose(yyin); + } +} diff --git a/src/kripkeparse/parsedecl.hh b/src/kripkeparse/parsedecl.hh new file mode 100644 index 000000000..9186307cc --- /dev/null +++ b/src/kripkeparse/parsedecl.hh @@ -0,0 +1,41 @@ +// 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_KRIPKEPARSE_PARSEDECL_HH +# define SPOT_KRIPKEPARSE_PARSEDECL_HH + +# include +# include "kripkeparse.hh" +# include "location.hh" + +# define YY_DECL \ + int kripkeyylex (kripkeyy::parser::semantic_type *yylval, \ + kripkeyy::location *yylloc) + +YY_DECL; + +namespace spot +{ + int kripkeyyopen(const std::string& name); + void kripkeyyclose(); +} + +#endif /* !PARSEDECL_HH_ */ diff --git a/src/kripkeparse/public.hh b/src/kripkeparse/public.hh new file mode 100644 index 000000000..7cc9163b7 --- /dev/null +++ b/src/kripkeparse/public.hh @@ -0,0 +1,68 @@ +// 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_KRIPKEPARSE_PUBLIC_HH +# define SPOT_KRIPKEPARSE_PUBLIC_HH + +# include "kripke/kripkeexplicit.hh" +// Unfortunately Bison 2.3 uses the same guards in all parsers :( +# undef BISON_LOCATION_HH +# undef BISON_POSITION_HH +# include "kripkeparse/location.hh" +# include "ltlenv/defaultenv.hh" +# include +# include +# include +# include + +namespace spot +{ + + /// \brief A parse diagnostic with its location. + typedef std::pair kripke_parse_error; + /// \brief A list of parser diagnostics, as filled by parse. + typedef std::list kripke_parse_error_list; + + + + kripke_explicit* + kripke_parse(const std::string& name, + kripke_parse_error_list& error_list, + bdd_dict* dict, + ltl::environment& env + = ltl::default_environment::instance(), + bool debug = false); + + + /// \brief Format diagnostics produced by spot::kripke_parse. + /// \param os Where diagnostics should be output. + /// \param filename The filename that should appear in the diagnostics. + /// \param error_list The error list filled by spot::ltl::parse while + /// parsing \a ltl_string. + /// \return \c true if any diagnostic was output. + bool format_kripke_parse_errors(std::ostream& os, + const std::string& filename, + kripke_parse_error_list& error_list); + +} + + +#endif /* !SPOT_KRIPKEPARSE_PUBLIC_HH_ */ diff --git a/src/kripkeparse/scankripke.ll b/src/kripkeparse/scankripke.ll new file mode 100644 index 000000000..a1e6e95a5 --- /dev/null +++ b/src/kripkeparse/scankripke.ll @@ -0,0 +1,117 @@ +/* Copyright (C) 2011 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. +*/ +%option noyywrap + //%option prefix="tgbayy" +%option prefix="kripkeyy" +%option outfile="lex.yy.c" +%x STATE_STRING + +%{ +#include +#include "parsekripke.tab.hh" + + +#define YY_USER_ACTION \ + yylloc->columns(yyleng); + +#define YY_NEVER_INTERACTIVE 1 + + typedef kripkeyy::parser::token token; + + +%} + +eol \n|\r|\n\r|\r\n + +%% + +%{ + yylloc->step (); +%} + +[a-zA-Z][a-zA-Z0-9_]* { + yylval->str = new std::string(yytext, yyleng); + return token::IDENT; + } + + /* discard whitespace */ +{eol} yylloc->lines(yyleng); yylloc->step(); +[ \t]+ yylloc->step(); + +\" { + yylval->str = new std::string; + BEGIN(STATE_STRING); + } + +"," { + return token::COMA; + } + +";" return token::SEMICOL; + +. return *yytext; + + /* Handle \" and \\ in strings. */ +{ + \" { + BEGIN(INITIAL); + return token::STRING; + } + \\["\\] yylval->str->append(1, yytext[1]); + [^"\\]+ yylval->str->append(yytext, yyleng); + <> { + BEGIN(INITIAL); + return token::UNTERMINATED_STRING; + } +} + +%{ + /* Dummy use of yyunput to shut up a gcc warning. */ + (void) &yyunput; +%} + +%% + + //namespace spot + //{ + int + kripkeyyopen(const std::string &name) + { + if (name == "-") + { + yyin = stdin; + } + else + { + yyin = fopen(name.c_str(), "r"); + if (!yyin) + return 1; + } + return 0; + } + + void + kripkeyyclose() + { + fclose(yyin); + } +//} diff --git a/src/kripketest/.gitignore b/src/kripketest/.gitignore new file mode 100644 index 000000000..282522db0 --- /dev/null +++ b/src/kripketest/.gitignore @@ -0,0 +1,2 @@ +Makefile +Makefile.in diff --git a/src/kripketest/Makefile.am b/src/kripketest/Makefile.am new file mode 100644 index 000000000..9d5b75be2 --- /dev/null +++ b/src/kripketest/Makefile.am @@ -0,0 +1,42 @@ +## Copyright (C) 2011 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 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. + +AM_CPPFLAGS = -I$(srcdir)/.. $(BUDDY_CPPFLAGS) + +kripketestdir = $(pkgincludedir)/kripketest + +kripketest_HEADERS = + + +LDADD = ../libspot.la ../../buddy/src/.libs/libbdd.so + +check_SCRIPTS = defs + +parse_print_SOURCES = parse_print_test.cc +check_PROGRAMS = \ +parse_print + +TESTS = \ + kripke.test \ + bad_parsing.test + +EXTRA_DIST = $(TESTS) + +distclean-local: + rm -rf $(TESTS:.test=.dir) diff --git a/src/kripketest/bad_parsing.test b/src/kripketest/bad_parsing.test new file mode 100755 index 000000000..b61706592 --- /dev/null +++ b/src/kripketest/bad_parsing.test @@ -0,0 +1,91 @@ +#! /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 + +set -e + +cat >input <<\EOF +state; +EOF + +cat >expected <<\EOF +input:1.6: syntax error, unexpected ;, expecting "," +EOF + +run 1 ../parse_print input 2> output +cat output | grep -v + > res +diff expected res + +rm -f output res expected + +cat >input <<\EOF +state1, "a & b, state2; +EOF + +cat >expected <<\EOF +input:1.9-24: unterminated string +input:1.25-24: syntax error, unexpected $end, expecting "," +EOF + +run 1 ../parse_print input 2> output +cat output | grep -v + > res +diff expected res + +rm -f output res expected + + +cat >input <<\EOF +state, "", ; +,,; +EOF + +cat >expected <<\EOF +input:1.9-8: empty input +input:2.1: syntax error, unexpected ",", expecting $end +EOF + +run 1 ../parse_print input 2> output +cat output | grep -v + > res +diff expected res + +rm -f output res expected + +cat >input <<\EOF +state,, state3 +state2, "a & b", state2; +EOF + + +s="input:2.7: syntax error, unexpected \",\", expecting STRING" +s2=" or UNTERMINATED_STRING or IDENT or ;" +string="$s$s2"; + +echo $string > expected + +run 1 ../parse_print input 2> output +cat output | grep -v + > res +diff expected res + +rm -f output res expected + diff --git a/src/kripketest/defs.in b/src/kripketest/defs.in new file mode 100644 index 000000000..1af322042 --- /dev/null +++ b/src/kripketest/defs.in @@ -0,0 +1,128 @@ +# -*- shell-script -*- +# Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement +# de l'Epita (LRDE). +# Copyright (C) 2003, 2004, 2006 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. + +# Ensure we are running from the right directory. +test -f ./defs || { + echo "defs: not found in current directory" 1>&2 + exit 1 +} + +# If srcdir is not set, then we are not running from `make check'. +if test -z "$srcdir"; then + # compute $srcdir. + srcdir=`echo "$0" | sed -e 's,/[^\\/]*$,,'` + test $srcdir = $0 && srcdir=. +fi + +# Ensure $srcdir is set correctly. +test -f $srcdir/defs.in || { + echo "$srcdir/defs.in not found, check \$srcdir" 1>&2 + exit 1 +} + +echo "== Running test $0" + +me=`echo "$0" | sed -e 's,.*[\\/],,;s/\.test$//'` + +testSubDir=$me.dir +chmod -R a+rwx $testSubDir > /dev/null 2>&1 +rm -rf $testSubDir > /dev/null 2>&1 +mkdir $testSubDir +cd $testSubDir + +# Adjust srcdir now that we are in a subdirectory. We still want to +# source directory corresponding to the build directory that contains +# $testSubDir. +case $srcdir in + # I + [\\/$]* | ?:[\\/]* );; + *) srcdir=../$srcdir +esac + +DOT='@DOT@' +top_builddir='../@top_builddir@' +LBTT="@LBTT@" +LBTT_TRANSLATE="@LBTT_TRANSLATE@" +VALGRIND='@VALGRIND@' +SPIN='@SPIN@' +LTL2BA='@LTL2BA@' +top_srcdir='../@top_srcdir@' + +run() +{ + 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 "$@" || + 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 +} + +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 diff --git a/src/kripketest/kripke.test b/src/kripketest/kripke.test new file mode 100755 index 000000000..59743f532 --- /dev/null +++ b/src/kripketest/kripke.test @@ -0,0 +1,71 @@ +#! /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 + +set -e + + +cat >input <<\EOF +state1, "!b", state2; +state2, "a&b", state3; +state3, "a", state4 state1; +state4, "b", state1; +EOF + +run2 0 ../parse_print input + +cat >input <<\EOF +state1, , state1 state2; +state2, , state1 state2; +EOF + +run2 0 ../parse_print input + +cat >input <<\EOF +state42, "!b & !a", state40; +state40, "!a | b", state42; +EOF + +run2 0 ../parse_print input + +cat >input <<\EOF +state1, "a&b", state1; +EOF + +run2 0 ../parse_print input + +cat >input <<\EOF +state51,,state60 state17 state3 state18 state62; +EOF + +run2 0 ../parse_print input + +cat >input <<\EOF +s42, "a&b|c&d", s51 s69 s73 s7; +s7, "a&a&a&!a", s42 s51 s69 s73 s42; +EOF + +run2 0 ../parse_print input + diff --git a/src/kripketest/origin b/src/kripketest/origin new file mode 100644 index 000000000..8d2e4ce30 --- /dev/null +++ b/src/kripketest/origin @@ -0,0 +1,4 @@ +state1, "!b", state2; +state2, "a&b", state3; +state3, "a", state4 state1; +state4, "b", state1; diff --git a/src/kripketest/parse_print_test.cc b/src/kripketest/parse_print_test.cc new file mode 100644 index 000000000..e09aac34a --- /dev/null +++ b/src/kripketest/parse_print_test.cc @@ -0,0 +1,58 @@ +// 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 "../kripkeparse/public.hh" +#include "../kripkeparse/parsedecl.hh" +#include "../kripke/kripkeprint.hh" +#include "../tgba/bddprint.hh" +#include "ltlast/allnodes.hh" + + +using namespace spot; + +int main(int argc, char** argv) +{ + int returnValue = 0; + kripke_parse_error_list pel; + bdd_dict* dict = new bdd_dict; + + kripke_explicit* k = kripke_parse(argv[1], pel, dict); + if (!pel.empty()) + { + format_kripke_parse_errors(std::cerr, argv[1], pel); + returnValue = 1; + } + + if (!returnValue) + { + KripkePrinter* kp = new KripkePrinter(k, std::cout); + kp->run(); + delete kp; + } + + delete k; + delete dict; + assert(ltl::atomic_prop::instance_count() == 0); + assert(ltl::unop::instance_count() == 0); + assert(ltl::binop::instance_count() == 0); + assert(ltl::multop::instance_count() == 0); + return returnValue; +}