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

Replace the constant_term visitor by a flag in the formulae.

Browse source 
* src/ltlast/formula.hh (formula::accepts_eword): New method.
(formula::is.accepting_eword): New flag.
* src/ltlast/formula.cc (print_formula_props): Display the new
property.
* src/ltlast/atomic_prop.cc, src/ltlast/automatop.cc,
src/ltlast/binop.cc, src/ltlast/bunop.cc, src/ltlast/constant.cc,
src/ltlast/multop.cc, src/ltlast/unop.cc: Update
is.accepting_eword as appropriate.
* src/ltltest/consterm.cc, src/tgbaalgos/ltl2tgba_fm.cc: Adjust to
use accepts_eword().
* src/ltlvisit/consterm.cc, src/ltlvisit/consterm.hh: Delete.
* src/ltlvisit/Makefile.am: Remove these files.
This commit is contained in:
Alexandre Duret-Lutz 2010-12-09 10:15:19 +01:00
parent 546260e7a0
commit 48cde88b9b
14 changed files with 73 additions and 268 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ltlast/atomic_prop.cc
View file

@ -45,6 +45,7 @@ namespace spot
is.eventual = false;
is.universal = false;
is.not_marked = true;
is.accepting_eword = false;
}
atomic_prop::~atomic_prop()

1
src/ltlast/automatop.cc
View file

@ -41,6 +41,7 @@ namespace spot
is.eventual = false;
is.universal = false;
is.not_marked = true;
is.accepting_eword = false;
unsigned s = v->size();
for (unsigned i = 0; i < s; ++i)

6
src/ltlast/binop.cc
View file

@ -56,6 +56,7 @@ namespace spot
case Equiv:
is.sugar_free_boolean = false;
is.in_nenoform = false;
is.accepting_eword = false;
break;
case EConcatMarked:
is.not_marked = false;
@ -65,6 +66,7 @@ namespace spot
is.ltl_formula = false;
is.boolean = false;
is.eltl_formula = false;
is.accepting_eword = false;
break;
case U:
// 1 U a = Fa
@ -72,6 +74,7 @@ namespace spot
is.eventual = 1;
is.boolean = false;
is.eltl_formula = false;
is.accepting_eword = false;
break;
case W:
// a W 0 = Ga
@ -79,6 +82,7 @@ namespace spot
is.universal = 1;
is.boolean = false;
is.eltl_formula = false;
is.accepting_eword = false;
break;
case R:
// 0 R a = Ga
@ -86,6 +90,7 @@ namespace spot
is.universal = 1;
is.boolean = false;
is.eltl_formula = false;
is.accepting_eword = false;
break;
case M:
// a M 1 = Fa
@ -93,6 +98,7 @@ namespace spot
is.eventual = 1;
is.boolean = false;
is.eltl_formula = false;
is.accepting_eword = false;
break;
}
}

17
src/ltlast/bunop.cc
View file

@ -35,16 +35,21 @@ namespace spot
{
props = child->get_props();
is.boolean = false;
is.ltl_formula = false;
is.eltl_formula = false;
is.eventual = false;
is.universal = false;
switch (op_)
{
case Equal:
case Star:
if (min_ == 0)
is.accepting_eword = true;
break;
case Equal:
case Goto:
is.boolean = false;
is.ltl_formula = false;
is.eltl_formula = false;
is.eventual = false;
is.universal = false;
is.accepting_eword = (min_ == 0);
break;
}
}

2
src/ltlast/constant.cc
View file

@ -51,6 +51,7 @@ namespace spot
is.eventual = true;
is.universal = true;
is.not_marked = true;
is.accepting_eword = false;
break;
case constant::EmptyWord:
is.boolean = false;
@ -64,6 +65,7 @@ namespace spot
is.eventual = false;
is.universal = false;
is.not_marked = true;
is.accepting_eword = true;
break;
}
}

1
src/ltlast/formula.cc
View file

@ -86,6 +86,7 @@ namespace spot
proprint(is_eventual, "e", "pure eventuality");
proprint(is_universal, "u", "purely universal");
proprint(is_marked, "+", "marked");
proprint(accepts_eword, "0", "accepts the empty word");
return out;
}
}

11
src/ltlast/formula.hh
View file

@ -211,6 +211,12 @@ namespace spot
return !is.not_marked;
}
/// Whether the formula accepts [*0].
bool accepts_eword() const
{
return is.accepting_eword;
}
/// The properties as a field of bits. For internal use.
unsigned get_props() const
{
@ -252,7 +258,7 @@ namespace spot
// "the formula is".
bool boolean:1; // No temporal operators.
bool sugar_free_boolean:1; // Only AND, OR, and NOT operators.
bool in_nenoform:1; // Negative Normal Form
bool in_nenoform:1; // Negative Normal Form.
bool X_free:1; // No X operators.
bool sugar_free_ltl:1; // No F and G operators.
bool ltl_formula:1; // Only LTL operators.
@ -260,7 +266,8 @@ namespace spot
bool psl_formula:1; // Only PSL operators.
bool eventual:1; // Purely eventual formula.
bool universal:1; // Purely universal formula.
bool not_marked:1; // No occurrence of EConcatMarked
bool not_marked:1; // No occurrence of EConcatMarked.
bool accepting_eword:1; // Accepts the empty word.
};
union
{

36
src/ltlast/multop.cc
View file

@ -28,7 +28,6 @@
#include "multop.hh"
#include "constant.hh"
#include "visitor.hh"
#include "ltlvisit/consterm.hh"
namespace spot
{
@ -40,10 +39,6 @@ namespace spot
unsigned s = v->size();
assert(s > 1);
props = (*v)[0]->get_props();
for (unsigned i = 1; i < s; ++i)
props &= (*v)[i]->get_props();
switch (op)
{
case Concat:
@ -53,15 +48,29 @@ namespace spot
is.eltl_formula = false;
is.eventual = false;
is.universal = false;
break;
// fall through
case AndNLM:
// The non-matching-length-And (&) can only appear in the
// rational parts of PSL formula. We don't remove the
// Boolean flag, because applied to atomic propositions a&b
// has the same effect as a&&b.
case And:
case Or:
props = (*v)[0]->get_props();
for (unsigned i = 1; i < s; ++i)
props &= (*v)[i]->get_props();
break;
case Or:
{
bool ew = (*v)[0]->accepts_eword();
props = (*v)[0]->get_props();
for (unsigned i = 1; i < s; ++i)
{
ew |= (*v)[i]->accepts_eword();
props &= (*v)[i]->get_props();
}
is.accepting_eword = ew;
break;
}
}
}
@ -280,21 +289,20 @@ namespace spot
++i;
}
}
// We have a* & [*0] & 0 = 0 // already checked above
// but a* & [*0] & c* = [*0]
// So if [*0] has been seen, check if all term recognize the
// We have a* & [*0] & c = 0
// and a* & [*0] & c* = [*0]
// So if [*0] has been seen, check if alls term recognize the
// empty word.
if (weak_abs_seen)
{
bool acc_empty = true;
bool acc_eword = true;
for (i = v->begin(); i != v->end(); ++i)
{
if (acc_empty)
acc_empty = constant_term_as_bool(*i);
acc_eword &= (*i)->accepts_eword();
(*i)->destroy();
}
delete v;
if (acc_empty)
if (acc_eword)
return weak_abs;
else
return constant::false_instance();

6
src/ltlast/unop.cc
View file

@ -40,34 +40,40 @@ namespace spot
{
case Not:
is.in_nenoform = !!dynamic_cast<atomic_prop*>(child);
is.accepting_eword = false;
break;
case X:
is.boolean = false;
is.X_free = false;
is.eltl_formula = false;
is.accepting_eword = false;
break;
case F:
is.boolean = false;
is.eltl_formula = false;
is.sugar_free_ltl = false;
is.eventual = true;
is.accepting_eword = false;
break;
case G:
is.boolean = false;
is.eltl_formula = false;
is.sugar_free_ltl = false;
is.universal = true;
is.accepting_eword = false;
break;
case Finish:
is.boolean = false;
is.ltl_formula = false;
is.psl_formula = false;
is.accepting_eword = false;
break;
case Closure:
case NegClosure:
is.boolean = false;
is.ltl_formula = false;
is.eltl_formula = false;
is.accepting_eword = false;
break;
}
}

4
src/ltltest/consterm.cc
View file

@ -22,7 +22,6 @@
#include <cassert>
#include <cstdlib>
#include "ltlparse/public.hh"
#include "ltlvisit/consterm.hh"
#include "ltlast/allnodes.hh"
void
@ -44,7 +43,7 @@ main(int argc, char **argv)
if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1))
return 2;
bool b = spot::ltl::constant_term_as_bool(f1);
bool b = f1->accepts_eword();
std::cout << b << std::endl;
@ -52,6 +51,7 @@ main(int argc, char **argv)
assert(spot::ltl::atomic_prop::instance_count() == 0);
assert(spot::ltl::unop::instance_count() == 0);
assert(spot::ltl::binop::instance_count() == 0);
assert(spot::ltl::bunop::instance_count() == 0);
assert(spot::ltl::multop::instance_count() == 0);
return b;
}

2
src/ltlvisit/Makefile.am
View file

@ -29,7 +29,6 @@ ltlvisitdir = $(pkgincludedir)/ltlvisit
ltlvisit_HEADERS = \
apcollect.hh \
basicreduce.hh \
consterm.hh \
contain.hh \
clone.hh \
destroy.hh \
@ -51,7 +50,6 @@ noinst_LTLIBRARIES = libltlvisit.la
libltlvisit_la_SOURCES = \
apcollect.cc \
basicreduce.cc \
consterm.cc \
contain.cc \
clone.cc \
destroy.cc \

175
src/ltlvisit/consterm.cc
View file

@ -1,175 +0,0 @@
// Copyright (C) 2010 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.
#include "ltlvisit/consterm.hh"
#include "ltlast/allnodes.hh"
#include "ltlast/visitor.hh"
namespace spot
{
namespace ltl
{
namespace
{
class consterm_visitor: public const_visitor
{
public:
consterm_visitor() {}
virtual ~consterm_visitor() {}
bool result() const { return result_; }
void
visit(const atomic_prop*)
{
result_ = false;
}
void
visit(const constant* c)
{
result_ = (c == constant::empty_word_instance());
}
void
visit(const binop* bo)
{
switch (bo->op())
{
case binop::Xor:
case binop::Implies:
case binop::Equiv:
assert(!"const_term not yet defined on Xor, Implies and Equiv");
break;
case binop::U:
case binop::W:
case binop::M:
case binop::R:
case binop::EConcat:
case binop::UConcat:
case binop::EConcatMarked:
assert(!"unsupported operator");
break;
}
}
void
visit(const bunop* bo)
{
switch (bo->op())
{
case bunop::Star:
if (bo->min() == 0)
result_ = true;
else
bo->child()->accept(*this);
break;
case bunop::Equal:
case bunop::Goto:
result_ = bo->min() == 0;
break;
}
}
void
visit(const unop* uo)
{
switch (uo->op())
{
case unop::Not:
result_ = false;
break;
case unop::X:
case unop::F:
case unop::G:
case unop::Finish:
case unop::Closure:
case unop::NegClosure:
assert(!"unsupported operator");
break;
}
}
void
visit(const automatop*)
{
assert(!"automatop not supported for constant term");
}
void
visit(const multop* mo)
{
// The fusion operator cannot be used to recognize the empty word.
if (mo->op() == multop::Fusion)
{
result_ = false;
return;
}
unsigned max = mo->size();
// This sets the initial value of result_.
mo->nth(0)->accept(*this);
for (unsigned n = 1; n < max; ++n)
{
bool r = constant_term_as_bool(mo->nth(n));
switch (mo->op())
{
case multop::Or:
result_ |= r;
if (result_)
return;
break;
case multop::And:
case multop::AndNLM:
case multop::Concat:
result_ &= r;
if (!result_)
return;
break;
case multop::Fusion:
/* Unreachable code */
assert(0);
break;
}
}
}
private:
bool result_;
};
}
bool constant_term_as_bool(const formula* f)
{
consterm_visitor v;
f->accept(v);
return v.result();
}
formula* constant_term(const formula* f)
{
return constant_term_as_bool(f) ?
constant::empty_word_instance() : constant::false_instance();
}
}
}

54
src/ltlvisit/consterm.hh
View file

@ -1,54 +0,0 @@
// Copyright (C) 2010 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.
#ifndef SPOT_LTLVISIT_CONSTERM_HH
# define SPOT_LTLVISIT_CONSTERM_HH
#include "ltlast/formula.hh"
namespace spot
{
namespace ltl
{
/// \brief Compute the constant term of a formula.
/// \ingroup ltl_misc
///
/// The constant term of a formula is the empty word if the empty
/// word is a model of the formula, it is false otherwise.
///
/// \see constant_term_as_bool
formula* constant_term(const formula* f);
/// \brief Compute the constant term of a formula.
/// \ingroup ltl_misc
///
/// The constant term of a formula is the empty word if the empty
/// word is a model of the formula, it is false otherwise.
///
/// This variant of the function return true instead of
/// constant::empty_word_instance() and false instead of
/// constant::false_instance().
///
/// \see constant_term
bool constant_term_as_bool(const formula* f);
}
}
#endif // SPOT_LTLVISIT_LENGTH_HH

25
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -38,7 +38,6 @@
#include <memory>
#include "ltl2tgba_fm.hh"
#include "ltlvisit/contain.hh"
#include "ltlvisit/consterm.hh"
#include "tgba/bddprint.hh"
namespace spot
@ -506,7 +505,7 @@ namespace spot
for (unsigned n = 0; n < s; ++n)
{
const formula* f = node->nth(n);
if (constant_term_as_bool(f))
if (f->accepts_eword())
final->push_back(f->clone());
else
non_final->push_back(f->clone());
@ -593,12 +592,12 @@ namespace spot
dest2->destroy();
res_ |= label & bdd_ithvar(x);
}
if (constant_term_as_bool(node))
if (node->accepts_eword())
res_ |= label & next_to_concat();
}
}
}
if (constant_term_as_bool(node))
if (node->accepts_eword())
res_ |= now_to_concat();
break;
@ -652,7 +651,7 @@ namespace spot
bdd dest_bdd = bdd_existcomp(cube, dict_.next_set);
formula* dest = dict_.conj_bdd_to_formula(dest_bdd);
if (constant_term_as_bool(dest))
if (dest->accepts_eword())
{
// The destination is a final state. Make sure we
// can also exit if tail is satisfied.
@ -838,7 +837,7 @@ namespace spot
case unop::Closure:
{
rat_seen_ = true;
if (constant_term_as_bool(node->child()))
if (node->child()->accepts_eword())
{
res_ = bddtrue;
return;
@ -864,7 +863,7 @@ namespace spot
dict_.var_set));
const formula* dest2;
if (constant_term_as_bool(dest))
if (dest->accepts_eword())
{
dest->destroy();
res_ |= label;
@ -891,7 +890,7 @@ namespace spot
formula* dest = dict_.conj_bdd_to_formula(dest_bdd);
const formula* dest2;
if (constant_term_as_bool(dest))
if (dest->accepts_eword())
{
dest->destroy();
res_ |= label;
@ -915,7 +914,7 @@ namespace spot
rat_seen_ = true;
has_marked_ = true;
if (constant_term_as_bool(node->child()))
if (node->child()->accepts_eword())
{
res_ = bddfalse;
return;
@ -945,7 +944,7 @@ namespace spot
dict_.var_set));
// !{ Exp } is false if Exp accepts the empty word.
if (constant_term_as_bool(dest))
if (dest->accepts_eword())
{
dest->destroy();
continue;
@ -1084,7 +1083,7 @@ namespace spot
dest2->destroy();
res_ |= label & bdd_ithvar(x);
}
if (constant_term_as_bool(dest))
if (dest->accepts_eword())
res_ |= label & f2;
}
}
@ -1112,7 +1111,7 @@ namespace spot
dest2->destroy();
res_ |= label & bdd_ithvar(x);
}
if (constant_term_as_bool(dest))
if (dest->accepts_eword())
res_ |= label & f2;
}
}
@ -1154,7 +1153,7 @@ namespace spot
bdd udest =
bdd_ithvar(dict_.register_next_variable(dest2));
if (constant_term_as_bool(dest))
if (dest->accepts_eword())
udest &= f2;
dest2->destroy();