From cb83e855a46aed901a2b9c201ba169f1d85d9692 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 10 Mar 2011 22:37:44 +0100 Subject: [PATCH] Add support for finite behaviors in the DVE interface. * iface/dve2/dve2.hh (load_dve2): Take a "dead" argument. * iface/dve2/dve2.cc (callback_context): Add a destructor to simplify... (dve2_succ_iterator::~dve2_succ_iterator) ... this one. (convert_aps): Skip the dead proposition. (dve2_kripke::dve2_kripke): Take a dead argument, and setup alive_prop and dead_prop. (compute_state_condition, get_succ): Use a cache for the conditions and successor of the last state, to share some work between these two function. Add loops on dead states. (load_dve2): Pass dead to dve2_kripke and convert_aps. * iface/dve2/dve2check.cc: Add a -dDEAD option. * iface/dve2/finite.test, iface/dve2/finite.dve: New file. * iface/dve2/Makefile.am: Declare them. --- ChangeLog | 20 ++++++ iface/dve2/Makefile.am | 4 +- iface/dve2/dve2.cc | 136 +++++++++++++++++++++++++++++++++++----- iface/dve2/dve2.hh | 18 +++++- iface/dve2/dve2check.cc | 27 +++++++- iface/dve2/finite.dve | 11 ++++ iface/dve2/finite.test | 50 +++++++++++++++ 7 files changed, 246 insertions(+), 20 deletions(-) create mode 100755 iface/dve2/finite.dve create mode 100755 iface/dve2/finite.test diff --git a/ChangeLog b/ChangeLog index c80a95bca..9adb1c4af 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,23 @@ +2011-03-10 Alexandre Duret-Lutz + + Add support for finite behaviors in the DVE interface. + + * iface/dve2/dve2.hh (load_dve2): Take a "dead" argument. + * iface/dve2/dve2.cc (callback_context): Add a destructor + to simplify... + (dve2_succ_iterator::~dve2_succ_iterator) ... this one. + (convert_aps): Skip the dead proposition. + (dve2_kripke::dve2_kripke): Take a dead argument, and + setup alive_prop and dead_prop. + (compute_state_condition, get_succ): Use a cache for the + conditions and successor of the last state, to share + some work between these two function. Add loops on dead + states. + (load_dve2): Pass dead to dve2_kripke and convert_aps. + * iface/dve2/dve2check.cc: Add a -dDEAD option. + * iface/dve2/finite.test, iface/dve2/finite.dve: New file. + * iface/dve2/Makefile.am: Declare them. + 2011-03-10 Alexandre Duret-Lutz * iface/dve2/dve2.cc (convert_aps): Fix two typos while diff --git a/iface/dve2/Makefile.am b/iface/dve2/Makefile.am index 28c6b6155..dc74b995a 100644 --- a/iface/dve2/Makefile.am +++ b/iface/dve2/Makefile.am @@ -38,8 +38,8 @@ dve2check_LDADD = libspotdve2.la check_SCRIPTS = defs -TESTS = dve2check.test -EXTRA_DIST = $(TESTS) beem-peterson.4.dve +TESTS = dve2check.test finite.test +EXTRA_DIST = $(TESTS) beem-peterson.4.dve finite.dve distclean-local: rm -rf $(TESTS:.test=.dir) diff --git a/iface/dve2/dve2.cc b/iface/dve2/dve2.cc index d16918dc4..57ec1cbf6 100644 --- a/iface/dve2/dve2.cc +++ b/iface/dve2/dve2.cc @@ -133,6 +133,13 @@ namespace spot typedef std::vector transitions_t; transitions_t transitions; int state_size; + + ~callback_context() + { + callback_context::transitions_t::const_iterator it; + for (it = transitions.begin(); it != transitions.end(); ++it) + (*it)->destroy(); + } }; void transition_callback(void* arg, transition_info_t*, int *dst) @@ -159,10 +166,6 @@ namespace spot ~dve2_succ_iterator() { - for (it_ = cc_->transitions.begin(); - it_ != cc_->transitions.end(); - ++it_) - (*it_)->destroy(); delete cc_; } @@ -222,6 +225,7 @@ namespace spot convert_aps(const ltl::atomic_prop_set* aps, const dve2_interface* d, bdd_dict* dict, + const ltl::formula* dead, prop_set& out) { int errors = 0; @@ -253,6 +257,9 @@ namespace spot for (ltl::atomic_prop_set::const_iterator ap = aps->begin(); ap != aps->end(); ++ap) { + if (*ap == dead) + continue; + std::string str = (*ap)->name(); const char* s = str.c_str(); @@ -495,14 +502,46 @@ namespace spot { public: - dve2_kripke(const dve2_interface* d, bdd_dict* dict, const prop_set* ps) - : d_(d), dict_(dict), ps_(ps) + dve2_kripke(const dve2_interface* d, bdd_dict* dict, const prop_set* ps, + const ltl::formula* dead) + : d_(d), dict_(dict), ps_(ps), state_condition_last_state_(0), + state_condition_last_cc_(0) { state_size_ = d_->get_state_variable_count(); vname_ = new const char*[state_size_]; for (int i = 0; i < state_size_; ++i) vname_[i] = d_->get_state_variable_name(i); + + // Register the "dead" proposition. There are three cases to + // consider: + // * If DEAD is "false", it means we are not interested in finite + // sequences of the system. + // * If DEAD is "true", we want to check finite sequences as well + // as infinite sequences, but do not need to distinguish them. + // * If DEAD is any other string, this is the name a property + // that should be true when looping on a dead state, and false + // otherwise. + // We handle these three cases by setting ALIVE_PROP and DEAD_PROP + // appropriately. ALIVE_PROP is the bdd that should be ANDed + // to all transitions leaving a live state, while DEAD_PROP should + // be ANDed to all transitions leaving a dead state. + if (dead == ltl::constant::false_instance()) + { + alive_prop = bddtrue; + dead_prop = bddfalse; + } + else if (dead == ltl::constant::false_instance()) + { + alive_prop = bddtrue; + dead_prop = bddtrue; + } + else + { + int var = dict->register_proposition(dead, d_); + dead_prop = bdd_ithvar(var); + alive_prop = bdd_nithvar(var); + } } ~dve2_kripke() @@ -515,6 +554,10 @@ namespace spot delete d_; delete ps_; lt_dlexit(); + + if (state_condition_last_state_) + state_condition_last_state_->destroy(); + delete state_condition_last_cc_; // Might be 0 already. } virtual @@ -529,6 +572,17 @@ namespace spot bdd compute_state_condition(const dve2_state* s) const { + // If we just computed it, don't do it twice. + if (s == state_condition_last_state_) + return state_condition_last_cond_; + + if (state_condition_last_state_) + { + state_condition_last_state_->destroy(); + delete state_condition_last_cc_; // Might be 0 already. + state_condition_last_cc_ = 0; + } + bdd res = bddtrue; for (prop_set::const_iterator i = ps_->begin(); i != ps_->end(); ++i) @@ -565,6 +619,29 @@ namespace spot else res &= bdd_nithvar(i->bddvar); } + + callback_context* cc = new callback_context; + cc->state_size = state_size_; + int t = d_->get_successors(0, s->vars, transition_callback, cc); + assert((unsigned)t == cc->transitions.size()); + state_condition_last_cc_ = cc; + + if (t) + { + res &= alive_prop; + } + else + { + res &= dead_prop; + + // Add a self-loop to dead-states if we care about these. + if (res != bddfalse) + cc->transitions.push_back(s->clone()); + } + + state_condition_last_cond_ = res; + state_condition_last_state_ = s->clone(); + return res; } @@ -576,13 +653,29 @@ namespace spot const dve2_state* s = dynamic_cast(local_state); assert(s); - callback_context* cc = new callback_context; - cc->state_size = state_size_; - int t = d_->get_successors(0, s->vars, transition_callback, cc); - (void) t; - assert((unsigned)t == cc->transitions.size()); + // This may also compute successors in state_condition_last_cc + bdd scond = compute_state_condition(s); - return new dve2_succ_iterator(cc, compute_state_condition(s)); + callback_context* cc; + + if (state_condition_last_cc_) + { + cc = state_condition_last_cc_; + state_condition_last_cc_ = 0; // Now owned by the iterator. + } + else + { + cc = new callback_context; + cc->state_size = state_size_; + int t = d_->get_successors(0, s->vars, transition_callback, cc); + assert((unsigned)t == cc->transitions.size()); + + // Add a self-loop to dead-states if we care about these. + if (t == 0 && scond != bddfalse) + cc->transitions.push_back(s->clone()); + } + + return new dve2_succ_iterator(cc, scond); } virtual @@ -629,6 +722,17 @@ namespace spot bdd_dict* dict_; const char** vname_; const prop_set* ps_; + bdd alive_prop; + bdd dead_prop; + + // This cache is used to speedup repeated calls to state_condition() + // and get_succ(). + // If state_condition_last_state_ != 0, then state_condition_last_cond_ + // contain its (recently computed) condition. If additionally + // state_condition_last_cc_ != 0, then it contains the successors. + mutable const dve2_state* state_condition_last_state_; + mutable bdd state_condition_last_cond_; + mutable callback_context* state_condition_last_cc_; }; } @@ -686,7 +790,9 @@ namespace spot kripke* load_dve2(const std::string& file_arg, bdd_dict* dict, - ltl::atomic_prop_set* to_observe, bool verbose) + const ltl::atomic_prop_set* to_observe, + const ltl::formula* dead, + bool verbose) { std::string file; if (file_arg.find_first_of("/\\") != std::string::npos) @@ -786,7 +892,7 @@ namespace spot } prop_set* ps = new prop_set; - int errors = convert_aps(to_observe, d, dict, *ps); + int errors = convert_aps(to_observe, d, dict, dead, *ps); if (errors) { delete ps; @@ -796,6 +902,6 @@ namespace spot return 0; } - return new dve2_kripke(d, dict, ps); + return new dve2_kripke(d, dict, ps, dead); } } diff --git a/iface/dve2/dve2.hh b/iface/dve2/dve2.hh index 90a210786..8026bbfbd 100644 --- a/iface/dve2/dve2.hh +++ b/iface/dve2/dve2.hh @@ -23,7 +23,7 @@ #include "kripke/kripke.hh" #include "ltlvisit/apcollect.hh" - +#include "ltlast/constant.hh" namespace spot @@ -36,6 +36,17 @@ namespace spot // When the *.dve source is supplied, the *.dve2C will be updated // only if it is not newer. // + // The dead parameter is used to control the behavior of the model + // on dead states (i.e. the final states of finite sequences). + // If DEAD is "false", it means we are not + // interested in finite sequences of the system, and dead state + // will have no successor. If DEAD is + // "true", we want to check finite sequences as well as infinite + // sequences, but do not need to distinguish them. In that case + // dead state will have a loop labeled by true. If DEAD is any + // other string, this is the name a property that should be true + // when looping on a dead state, and false otherwise. + // // This function returns 0 on error. // // \a file the name of the *.dve source file or of the *.dve2C @@ -43,10 +54,13 @@ namespace spot // \a to_observe the list of atomic propositions that should be observed // in the model // \a dict the BDD dictionary to use + // \a dead an atomic proposition or constant to use for looping on + // dead states // \a verbose whether to output verbose messages kripke* load_dve2(const std::string& file, bdd_dict* dict, - ltl::atomic_prop_set* to_observe, + const ltl::atomic_prop_set* to_observe, + const ltl::formula* dead = ltl::constant::true_instance(), bool verbose = true); } diff --git a/iface/dve2/dve2check.cc b/iface/dve2/dve2check.cc index d35e416cc..20531af6f 100644 --- a/iface/dve2/dve2check.cc +++ b/iface/dve2/dve2check.cc @@ -42,6 +42,9 @@ syntax(char* prog) std::cerr << "usage: " << prog << " [options] model formula" << std::endl << std::endl << "Options:" << std::endl + << " -dDEAD use DEAD as property for marking DEAD states" + << std::endl + << " (by default DEAD = true)" << std::endl << " -e[ALGO] run emptiness check, expect an accepting run" << std::endl << " -E[ALGO] run emptiness check, expect no accepting run" @@ -71,6 +74,7 @@ main(int argc, char **argv) output = EmptinessCheck; bool accepting_run = false; bool expect_counter_example = false; + char *dead = 0; const char* echeck_algo = "Cou99"; @@ -86,6 +90,9 @@ main(int argc, char **argv) case 'C': accepting_run = true; break; + case 'd': + dead = opt + 1; + break; case 'e': case 'E': { @@ -135,6 +142,7 @@ main(int argc, char **argv) spot::ltl::default_environment& env = spot::ltl::default_environment::instance(); + spot::ltl::atomic_prop_set ap; spot::bdd_dict* dict = new spot::bdd_dict(); spot::kripke* model = 0; @@ -143,6 +151,21 @@ main(int argc, char **argv) spot::emptiness_check_instantiator* echeck_inst = 0; int exit_code = 0; spot::ltl::formula* f = 0; + spot::ltl::formula* deadf = 0; + + if (dead == 0 || !strcasecmp(dead, "true")) + { + deadf = spot::ltl::constant::true_instance(); + std::cerr << "true" << std::endl; + } + else if (!strcasecmp(dead, "false")) + { + deadf = spot::ltl::constant::false_instance(); + } + else + { + deadf = env.require(dead); + } if (output == EmptinessCheck) { @@ -175,7 +198,7 @@ main(int argc, char **argv) if (output != DotFormula) { tm.start("loading dve2"); - model = spot::load_dve2(argv[1], dict, &ap, true); + model = spot::load_dve2(argv[1], dict, &ap, deadf, true); tm.stop("loading dve2"); if (!model) @@ -304,6 +327,8 @@ main(int argc, char **argv) f->destroy(); delete dict; + deadf->destroy(); + if (use_timer) tm.print(std::cout); tm.reset_all(); // This helps valgrind. diff --git a/iface/dve2/finite.dve b/iface/dve2/finite.dve new file mode 100755 index 000000000..db9ed8da9 --- /dev/null +++ b/iface/dve2/finite.dve @@ -0,0 +1,11 @@ +process P { + int a = 0, b = 0; + state x; + init x; + + trans + x -> x { guard a < 3 && b < 3; effect a = a + 1; }, + x -> x { guard a < 3 && b < 3; effect b = b + 1; }; +} + +system async; diff --git a/iface/dve2/finite.test b/iface/dve2/finite.test new file mode 100755 index 000000000..b2f50e83d --- /dev/null +++ b/iface/dve2/finite.test @@ -0,0 +1,50 @@ +#!/bin/sh +# 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. + + +. ./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 ../dve2check -gm $srcdir/finite.dve '"P.a < 10"' > stdout +test "`grep ' -> ' stdout | wc -l`" = 25 +test "`grep 'P=0' stdout | wc -l`" = 15 + +run 0 ../dve2check -dtrue -gm $srcdir/finite.dve '"P.a < 10"' > stdout2 +cmp stdout stdout2 + +run 0 ../dve2check -dfalse -gm $srcdir/finite.dve '"P.a < 10"' > stdout +test "`grep ' -> ' stdout | wc -l`" = 19 +test "`grep 'P=0' stdout | wc -l`" = 15 + +run 0 ../dve2check -ddead -e $srcdir/finite.dve \ + '!(G(dead -> ("P.a==3" | "P.b==3")))' + +run 0 ../dve2check -ddead -E $srcdir/finite.dve \ + '!(G(dead -> ("P.a==2" | "P.b==3")))'