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

Add support for finite behaviors in the DVE interface.

Browse source 
* 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.
This commit is contained in:
Alexandre Duret-Lutz 2011-03-10 22:37:44 +01:00
parent ef976c93d0
commit cb83e855a4
7 changed files with 246 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

4
iface/dve2/Makefile.am
View file

@ -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)

136
iface/dve2/dve2.cc
View file

@ -133,6 +133,13 @@ namespace spot
typedef std::vector<dve2_state*> 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<const dve2_state*>(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);
}
}

18
iface/dve2/dve2.hh
View file

@ -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);
}

27
iface/dve2/dve2check.cc
View file

@ -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.

11
iface/dve2/finite.dve Executable file
View file

@ -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;

50
iface/dve2/finite.test Executable file
View file

@ -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")))'