c6dd811b08
* src/ltlast/binop.hh, src/ltlast/binop.cc (EConcat, UConcat): Add these new operators. * src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Parse these new operators. * src/ltlvisit/simpfg.cc, src/ltlvisit/syntimpl.cc, src/ltlvisit/tostring.cc, src/ltlvisit/basicreduce.cc, src/ltlvisit/consterm.cc, src/ltlvisit/lunabbrev.cc, src/ltlvisit/nenoform.cc, src/ltlvisit/reduce.cc src/tgba/formula2bdd.cc, src/tgbaalgos/eltl2tgba_lacim.cc, src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_lacim.cc: Add these new operators into the switches.
1009 lines
26 KiB
C++
1009 lines
26 KiB
C++
// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et
|
|
// Développement de l'Epita (LRDE).
|
|
// Copyright (C) 2003, 2004, 2005, 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.
|
|
|
|
#include "misc/hash.hh"
|
|
#include "misc/bddalloc.hh"
|
|
#include "misc/bddlt.hh"
|
|
#include "misc/minato.hh"
|
|
#include "ltlast/visitor.hh"
|
|
#include "ltlast/allnodes.hh"
|
|
#include "ltlvisit/lunabbrev.hh"
|
|
#include "ltlvisit/nenoform.hh"
|
|
#include "ltlvisit/tostring.hh"
|
|
#include "ltlvisit/postfix.hh"
|
|
#include "ltlvisit/apcollect.hh"
|
|
#include <cassert>
|
|
#include <memory>
|
|
#include "ltl2tgba_fm.hh"
|
|
#include "ltlvisit/contain.hh"
|
|
|
|
namespace spot
|
|
{
|
|
using namespace ltl;
|
|
|
|
namespace
|
|
{
|
|
|
|
// Helper dictionary. We represent formulae using BDDs to
|
|
// simplify them, and then translate BDDs back into formulae.
|
|
//
|
|
// The name of the variables are inspired from Couvreur's FM paper.
|
|
// "a" variables are promises (written "a" in the paper)
|
|
// "next" variables are X's operands (the "r_X" variables from the paper)
|
|
// "var" variables are atomic propositions.
|
|
class translate_dict
|
|
{
|
|
public:
|
|
|
|
translate_dict(bdd_dict* dict)
|
|
: dict(dict),
|
|
a_set(bddtrue),
|
|
var_set(bddtrue),
|
|
next_set(bddtrue)
|
|
{
|
|
}
|
|
|
|
~translate_dict()
|
|
{
|
|
fv_map::iterator i;
|
|
for (i = next_map.begin(); i != next_map.end(); ++i)
|
|
i->first->destroy();
|
|
dict->unregister_all_my_variables(this);
|
|
}
|
|
|
|
bdd_dict* dict;
|
|
|
|
typedef bdd_dict::fv_map fv_map;
|
|
typedef bdd_dict::vf_map vf_map;
|
|
|
|
fv_map next_map; ///< Maps "Next" variables to BDD variables
|
|
vf_map next_formula_map; ///< Maps BDD variables to "Next" variables
|
|
|
|
bdd a_set;
|
|
bdd var_set;
|
|
bdd next_set;
|
|
|
|
int
|
|
register_proposition(const formula* f)
|
|
{
|
|
int num = dict->register_proposition(f, this);
|
|
var_set &= bdd_ithvar(num);
|
|
return num;
|
|
}
|
|
|
|
int
|
|
register_a_variable(const formula* f)
|
|
{
|
|
int num = dict->register_acceptance_variable(f, this);
|
|
a_set &= bdd_ithvar(num);
|
|
return num;
|
|
}
|
|
|
|
int
|
|
register_next_variable(const formula* f)
|
|
{
|
|
int num;
|
|
// Do not build a Next variable that already exists.
|
|
fv_map::iterator sii = next_map.find(f);
|
|
if (sii != next_map.end())
|
|
{
|
|
num = sii->second;
|
|
}
|
|
else
|
|
{
|
|
f = f->clone();
|
|
num = dict->register_anonymous_variables(1, this);
|
|
next_map[f] = num;
|
|
next_formula_map[num] = f;
|
|
}
|
|
next_set &= bdd_ithvar(num);
|
|
return num;
|
|
}
|
|
|
|
std::ostream&
|
|
dump(std::ostream& os) const
|
|
{
|
|
fv_map::const_iterator fi;
|
|
os << "Next Variables:" << std::endl;
|
|
for (fi = next_map.begin(); fi != next_map.end(); ++fi)
|
|
{
|
|
os << " " << fi->second << ": Next[";
|
|
to_string(fi->first, os) << "]" << std::endl;
|
|
}
|
|
os << "Shared Dict:" << std::endl;
|
|
dict->dump(os);
|
|
return os;
|
|
}
|
|
|
|
formula*
|
|
var_to_formula(int var) const
|
|
{
|
|
vf_map::const_iterator isi = next_formula_map.find(var);
|
|
if (isi != next_formula_map.end())
|
|
return isi->second->clone();
|
|
isi = dict->acc_formula_map.find(var);
|
|
if (isi != dict->acc_formula_map.end())
|
|
return isi->second->clone();
|
|
isi = dict->var_formula_map.find(var);
|
|
if (isi != dict->var_formula_map.end())
|
|
return isi->second->clone();
|
|
assert(0);
|
|
// Never reached, but some GCC versions complain about
|
|
// a missing return otherwise.
|
|
return 0;
|
|
}
|
|
|
|
formula*
|
|
conj_bdd_to_formula(bdd b)
|
|
{
|
|
if (b == bddfalse)
|
|
return constant::false_instance();
|
|
multop::vec* v = new multop::vec;
|
|
while (b != bddtrue)
|
|
{
|
|
int var = bdd_var(b);
|
|
formula* res = var_to_formula(var);
|
|
bdd high = bdd_high(b);
|
|
if (high == bddfalse)
|
|
{
|
|
res = unop::instance(unop::Not, res);
|
|
b = bdd_low(b);
|
|
}
|
|
else
|
|
{
|
|
assert(bdd_low(b) == bddfalse);
|
|
b = high;
|
|
}
|
|
assert(b != bddfalse);
|
|
v->push_back(res);
|
|
}
|
|
return multop::instance(multop::And, v);
|
|
}
|
|
|
|
const formula*
|
|
bdd_to_formula(bdd f)
|
|
{
|
|
if (f == bddfalse)
|
|
return constant::false_instance();
|
|
|
|
multop::vec* v = new multop::vec;
|
|
|
|
minato_isop isop(f);
|
|
bdd cube;
|
|
while ((cube = isop.next()) != bddfalse)
|
|
v->push_back(conj_bdd_to_formula(cube));
|
|
|
|
return multop::instance(multop::Or, v);
|
|
}
|
|
|
|
void
|
|
conj_bdd_to_acc(tgba_explicit_formula* a, bdd b,
|
|
state_explicit_formula::transition* t)
|
|
{
|
|
assert(b != bddfalse);
|
|
while (b != bddtrue)
|
|
{
|
|
int var = bdd_var(b);
|
|
bdd high = bdd_high(b);
|
|
if (high == bddfalse)
|
|
{
|
|
// Simply ignore negated acceptance variables.
|
|
b = bdd_low(b);
|
|
}
|
|
else
|
|
{
|
|
formula* ac = var_to_formula(var);
|
|
|
|
if (!a->has_acceptance_condition(ac))
|
|
a->declare_acceptance_condition(ac->clone());
|
|
a->add_acceptance_condition(t, ac);
|
|
b = high;
|
|
}
|
|
assert(b != bddfalse);
|
|
}
|
|
}
|
|
};
|
|
|
|
|
|
|
|
// Gather all promises of a formula. These are the
|
|
// right-hand sides of U or F operators.
|
|
class ltl_promise_visitor: public postfix_visitor
|
|
{
|
|
public:
|
|
ltl_promise_visitor(translate_dict& dict)
|
|
: dict_(dict), res_(bddtrue)
|
|
{
|
|
}
|
|
|
|
virtual
|
|
~ltl_promise_visitor()
|
|
{
|
|
}
|
|
|
|
bdd
|
|
result() const
|
|
{
|
|
return res_;
|
|
}
|
|
|
|
using postfix_visitor::doit;
|
|
|
|
virtual void
|
|
doit(unop* node)
|
|
{
|
|
if (node->op() == unop::F)
|
|
res_ &= bdd_ithvar(dict_.register_a_variable(node->child()));
|
|
}
|
|
|
|
virtual void
|
|
doit(binop* node)
|
|
{
|
|
if (node->op() == binop::U)
|
|
res_ &= bdd_ithvar(dict_.register_a_variable(node->second()));
|
|
}
|
|
|
|
private:
|
|
translate_dict& dict_;
|
|
bdd res_;
|
|
};
|
|
|
|
|
|
// The rewrite rules used here are adapted from Jean-Michel
|
|
// Couvreur's FM paper.
|
|
class ltl_trad_visitor: public const_visitor
|
|
{
|
|
public:
|
|
ltl_trad_visitor(translate_dict& dict)
|
|
: dict_(dict)
|
|
{
|
|
}
|
|
|
|
virtual
|
|
~ltl_trad_visitor()
|
|
{
|
|
}
|
|
|
|
bdd
|
|
result() const
|
|
{
|
|
return res_;
|
|
}
|
|
|
|
void
|
|
visit(const atomic_prop* node)
|
|
{
|
|
res_ = bdd_ithvar(dict_.register_proposition(node));
|
|
}
|
|
|
|
void
|
|
visit(const constant* node)
|
|
{
|
|
switch (node->val())
|
|
{
|
|
case constant::True:
|
|
res_ = bddtrue;
|
|
return;
|
|
case constant::False:
|
|
res_ = bddfalse;
|
|
return;
|
|
case constant::EmptyWord:
|
|
assert(!"unsupported operator");
|
|
}
|
|
/* Unreachable code. */
|
|
assert(0);
|
|
}
|
|
|
|
void
|
|
visit(const unop* node)
|
|
{
|
|
switch (node->op())
|
|
{
|
|
case unop::F:
|
|
{
|
|
// r(Fy) = r(y) + a(y)r(XFy)
|
|
const formula* child = node->child();
|
|
bdd y = recurse(child);
|
|
int a = dict_.register_a_variable(child);
|
|
int x = dict_.register_next_variable(node);
|
|
res_ = y | (bdd_ithvar(a) & bdd_ithvar(x));
|
|
return;
|
|
}
|
|
case unop::G:
|
|
{
|
|
// The paper suggests that we optimize GFy
|
|
// as
|
|
// r(GFy) = (r(y) + a(y))r(XGFy)
|
|
// instead of
|
|
// r(GFy) = (r(y) + a(y)r(XFy)).r(XGFy)
|
|
// but this is just a particular case
|
|
// of the "merge all states with the same
|
|
// symbolic rewriting" optimization we do later.
|
|
// (r(Fy).r(GFy) and r(GFy) have the same symbolic
|
|
// rewriting.) Let's keep things simple here.
|
|
|
|
// r(Gy) = r(y)r(XGy)
|
|
const formula* child = node->child();
|
|
int x = dict_.register_next_variable(node);
|
|
bdd y = recurse(child);
|
|
res_ = y & bdd_ithvar(x);
|
|
return;
|
|
}
|
|
case unop::Not:
|
|
{
|
|
// r(!y) = !r(y)
|
|
res_ = bdd_not(recurse(node->child()));
|
|
return;
|
|
}
|
|
case unop::X:
|
|
{
|
|
// r(Xy) = Next[y]
|
|
int x = dict_.register_next_variable(node->child());
|
|
res_ = bdd_ithvar(x);
|
|
return;
|
|
}
|
|
case unop::Finish:
|
|
case unop::Star:
|
|
assert(!"unsupported operator");
|
|
}
|
|
/* Unreachable code. */
|
|
assert(0);
|
|
}
|
|
|
|
void
|
|
visit(const binop* node)
|
|
{
|
|
bdd f1 = recurse(node->first());
|
|
bdd f2 = recurse(node->second());
|
|
|
|
switch (node->op())
|
|
{
|
|
// r(f1 logical-op f2) = r(f1) logical-op r(f2)
|
|
case binop::Xor:
|
|
res_ = bdd_apply(f1, f2, bddop_xor);
|
|
return;
|
|
case binop::Implies:
|
|
res_ = bdd_apply(f1, f2, bddop_imp);
|
|
return;
|
|
case binop::Equiv:
|
|
res_ = bdd_apply(f1, f2, bddop_biimp);
|
|
return;
|
|
case binop::U:
|
|
{
|
|
// r(f1 U f2) = r(f2) + a(f2)r(f1)r(X(f1 U f2))
|
|
int a = dict_.register_a_variable(node->second());
|
|
int x = dict_.register_next_variable(node);
|
|
res_ = f2 | (bdd_ithvar(a) & f1 & bdd_ithvar(x));
|
|
return;
|
|
}
|
|
case binop::W:
|
|
{
|
|
// r(f1 W f2) = r(f2) + r(f1)r(X(f1 U f2))
|
|
int x = dict_.register_next_variable(node);
|
|
res_ = f2 | (f1 & bdd_ithvar(x));
|
|
return;
|
|
}
|
|
case binop::R:
|
|
{
|
|
// r(f1 R f2) = r(f1)r(f2) + r(f2)r(X(f1 U f2))
|
|
int x = dict_.register_next_variable(node);
|
|
res_ = (f1 & f2) | (f2 & bdd_ithvar(x));
|
|
return;
|
|
}
|
|
case binop::M:
|
|
{
|
|
// r(f1 M f2) = r(f1)r(f2) + a(f1)r(f2)r(X(f1 M f2))
|
|
int a = dict_.register_a_variable(node->first());
|
|
int x = dict_.register_next_variable(node);
|
|
res_ = (f1 & f2) | (bdd_ithvar(a) & f2 & bdd_ithvar(x));
|
|
return;
|
|
}
|
|
case binop::UConcat:
|
|
case binop::EConcat:
|
|
assert(!"unsupported operator");
|
|
break;
|
|
}
|
|
/* Unreachable code. */
|
|
assert(0);
|
|
}
|
|
|
|
void
|
|
visit(const automatop*)
|
|
{
|
|
assert(!"unsupported operator");
|
|
}
|
|
|
|
void
|
|
visit(const multop* node)
|
|
{
|
|
int op = -1;
|
|
switch (node->op())
|
|
{
|
|
case multop::And:
|
|
op = bddop_and;
|
|
res_ = bddtrue;
|
|
break;
|
|
case multop::Or:
|
|
op = bddop_or;
|
|
res_ = bddfalse;
|
|
break;
|
|
case multop::Concat:
|
|
assert(!"unsupported operator");
|
|
}
|
|
assert(op != -1);
|
|
unsigned s = node->size();
|
|
for (unsigned n = 0; n < s; ++n)
|
|
{
|
|
res_ = bdd_apply(res_, recurse(node->nth(n)), op);
|
|
}
|
|
}
|
|
|
|
bdd
|
|
recurse(const formula* f)
|
|
{
|
|
ltl_trad_visitor v(dict_);
|
|
f->accept(v);
|
|
return v.result();
|
|
}
|
|
|
|
|
|
private:
|
|
translate_dict& dict_;
|
|
bdd res_;
|
|
};
|
|
|
|
|
|
// Check whether a formula has a R, W, or G operator at its
|
|
// top-level (preceding logical operators do not count).
|
|
class ltl_possible_fair_loop_visitor: public const_visitor
|
|
{
|
|
public:
|
|
ltl_possible_fair_loop_visitor()
|
|
: res_(false)
|
|
{
|
|
}
|
|
|
|
virtual
|
|
~ltl_possible_fair_loop_visitor()
|
|
{
|
|
}
|
|
|
|
bool
|
|
result() const
|
|
{
|
|
return res_;
|
|
}
|
|
|
|
void
|
|
visit(const atomic_prop*)
|
|
{
|
|
}
|
|
|
|
void
|
|
visit(const constant*)
|
|
{
|
|
}
|
|
|
|
void
|
|
visit(const unop* node)
|
|
{
|
|
if (node->op() == unop::G)
|
|
res_ = true;
|
|
}
|
|
|
|
void
|
|
visit(const binop* node)
|
|
{
|
|
switch (node->op())
|
|
{
|
|
// r(f1 logical-op f2) = r(f1) logical-op r(f2)
|
|
case binop::Xor:
|
|
case binop::Implies:
|
|
case binop::Equiv:
|
|
node->first()->accept(*this);
|
|
if (!res_)
|
|
node->second()->accept(*this);
|
|
return;
|
|
case binop::U:
|
|
case binop::M:
|
|
return;
|
|
case binop::R:
|
|
case binop::W:
|
|
res_ = true;
|
|
return;
|
|
case binop::UConcat:
|
|
case binop::EConcat:
|
|
node->second()->accept(*this);
|
|
return;
|
|
}
|
|
/* Unreachable code. */
|
|
assert(0);
|
|
}
|
|
|
|
void
|
|
visit(const automatop*)
|
|
{
|
|
assert(!"unsupported operator");
|
|
}
|
|
|
|
void
|
|
visit(const multop* node)
|
|
{
|
|
unsigned s = node->size();
|
|
for (unsigned n = 0; n < s && !res_; ++n)
|
|
{
|
|
node->nth(n)->accept(*this);
|
|
}
|
|
}
|
|
|
|
private:
|
|
bool res_;
|
|
};
|
|
|
|
// Check whether a formula can be part of a fair loop.
|
|
// Cache the result for efficiency.
|
|
class possible_fair_loop_checker
|
|
{
|
|
public:
|
|
bool
|
|
check(const formula* f)
|
|
{
|
|
pfl_map::const_iterator i = pfl_.find(f);
|
|
if (i != pfl_.end())
|
|
return i->second;
|
|
ltl_possible_fair_loop_visitor v;
|
|
f->accept(v);
|
|
bool rel = v.result();
|
|
pfl_[f] = rel;
|
|
return rel;
|
|
}
|
|
|
|
private:
|
|
typedef Sgi::hash_map<const formula*, bool, formula_ptr_hash> pfl_map;
|
|
pfl_map pfl_;
|
|
};
|
|
|
|
class formula_canonizer
|
|
{
|
|
public:
|
|
formula_canonizer(translate_dict& d,
|
|
bool fair_loop_approx, bdd all_promises)
|
|
: v_(d),
|
|
fair_loop_approx_(fair_loop_approx),
|
|
all_promises_(all_promises)
|
|
{
|
|
// For cosmetics, register 1 initially, so the algorithm will
|
|
// not register an equivalent formula first.
|
|
b2f_[bddtrue] = constant::true_instance();
|
|
}
|
|
|
|
~formula_canonizer()
|
|
{
|
|
while (!f2b_.empty())
|
|
{
|
|
formula_to_bdd_map::iterator i = f2b_.begin();
|
|
const formula* f = i->first;
|
|
f2b_.erase(i);
|
|
f->destroy();
|
|
}
|
|
}
|
|
|
|
bdd
|
|
translate(const formula* f, bool* new_flag = 0)
|
|
{
|
|
// Use the cached result if available.
|
|
formula_to_bdd_map::const_iterator i = f2b_.find(f);
|
|
if (i != f2b_.end())
|
|
return i->second;
|
|
|
|
if (new_flag)
|
|
*new_flag = true;
|
|
|
|
// Perform the actual translation.
|
|
f->accept(v_);
|
|
bdd res = v_.result();
|
|
|
|
// Apply the fair-loop approximation if requested.
|
|
if (fair_loop_approx_)
|
|
{
|
|
// If the source cannot possibly be part of a fair
|
|
// loop, make all possible promises.
|
|
if (fair_loop_approx_
|
|
&& f != constant::true_instance()
|
|
&& !pflc_.check(f))
|
|
res &= all_promises_;
|
|
}
|
|
|
|
f2b_[f->clone()] = res;
|
|
|
|
// Register the reverse mapping if it is not already done.
|
|
if (b2f_.find(res) == b2f_.end())
|
|
b2f_[res] = f;
|
|
return res;
|
|
}
|
|
|
|
const formula*
|
|
canonize(const formula* f)
|
|
{
|
|
bool new_variable = false;
|
|
bdd b = translate(f, &new_variable);
|
|
|
|
bdd_to_formula_map::iterator i = b2f_.find(b);
|
|
// Since we have just translated the formula, it is
|
|
// necessarily in b2f_.
|
|
assert(i != b2f_.end());
|
|
|
|
if (i->second != f)
|
|
{
|
|
// The translated bdd maps to an already seen formula.
|
|
f->destroy();
|
|
f = i->second->clone();
|
|
}
|
|
return f;
|
|
}
|
|
|
|
private:
|
|
ltl_trad_visitor v_;
|
|
// Map each formula to its associated bdd. This speed things up when
|
|
// the same formula is translated several times, which especially
|
|
// occurs when canonize() is called repeatedly inside exprop.
|
|
typedef std::map<bdd, const formula*, bdd_less_than> bdd_to_formula_map;
|
|
bdd_to_formula_map b2f_;
|
|
// Map a representation of successors to a canonical formula.
|
|
// We do this because many formulae (such as `aR(bRc)' and
|
|
// `aR(bRc).(bRc)') are equivalent, and are trivially identified
|
|
// by looking at the set of successors.
|
|
typedef std::map<const formula*, bdd> formula_to_bdd_map;
|
|
formula_to_bdd_map f2b_;
|
|
|
|
possible_fair_loop_checker pflc_;
|
|
bool fair_loop_approx_;
|
|
bdd all_promises_;
|
|
};
|
|
|
|
}
|
|
|
|
typedef std::map<bdd, bdd, bdd_less_than> prom_map;
|
|
typedef Sgi::hash_map<const formula*, prom_map, formula_ptr_hash> dest_map;
|
|
|
|
static void
|
|
fill_dests(translate_dict& d, dest_map& dests, bdd label, const formula* dest)
|
|
{
|
|
bdd conds = bdd_existcomp(label, d.var_set);
|
|
bdd promises = bdd_existcomp(label, d.a_set);
|
|
|
|
dest_map::iterator i = dests.find(dest);
|
|
if (i == dests.end())
|
|
{
|
|
dests[dest][promises] = conds;
|
|
}
|
|
else
|
|
{
|
|
i->second[promises] |= conds;
|
|
dest->destroy();
|
|
}
|
|
}
|
|
|
|
|
|
tgba_explicit_formula*
|
|
ltl_to_tgba_fm(const formula* f, bdd_dict* dict,
|
|
bool exprop, bool symb_merge, bool branching_postponement,
|
|
bool fair_loop_approx, const atomic_prop_set* unobs,
|
|
int reduce_ltl)
|
|
{
|
|
// Normalize the formula. We want all the negations on
|
|
// the atomic propositions. We also suppress logic
|
|
// abbreviations such as <=>, =>, or XOR, since they
|
|
// would involve negations at the BDD level.
|
|
formula* f1 = unabbreviate_logic(f);
|
|
formula* f2 = negative_normal_form(f1);
|
|
f1->destroy();
|
|
|
|
// Simplify the formula, if requested.
|
|
if (reduce_ltl)
|
|
{
|
|
formula* tmp = reduce(f2, reduce_ltl);
|
|
f2->destroy();
|
|
f2 = tmp;
|
|
}
|
|
|
|
typedef std::set<const formula*, formula_ptr_less_than> set_type;
|
|
set_type formulae_to_translate;
|
|
|
|
translate_dict d(dict);
|
|
|
|
// Compute the set of all promises that can possibly occurre
|
|
// inside the formula.
|
|
bdd all_promises = bddtrue;
|
|
if (fair_loop_approx || unobs)
|
|
{
|
|
ltl_promise_visitor pv(d);
|
|
f2->accept(pv);
|
|
all_promises = pv.result();
|
|
}
|
|
|
|
formula_canonizer fc(d, fair_loop_approx, all_promises);
|
|
|
|
// These are used when atomic propositions are interpreted as
|
|
// events. There are two kinds of events: observable events are
|
|
// those used in the formula, and unobservable events or other
|
|
// events that can occur at anytime. All events exclude each
|
|
// other.
|
|
bdd observable_events = bddfalse;
|
|
bdd unobservable_events = bddfalse;
|
|
if (unobs)
|
|
{
|
|
bdd neg_events = bddtrue;
|
|
std::auto_ptr<atomic_prop_set> aps(atomic_prop_collect(f));
|
|
for (atomic_prop_set::const_iterator i = aps->begin();
|
|
i != aps->end(); ++i)
|
|
{
|
|
int p = d.register_proposition(*i);
|
|
bdd pos = bdd_ithvar(p);
|
|
bdd neg = bdd_nithvar(p);
|
|
observable_events = (observable_events & neg) | (neg_events & pos);
|
|
neg_events &= neg;
|
|
}
|
|
for (atomic_prop_set::const_iterator i = unobs->begin();
|
|
i != unobs->end(); ++i)
|
|
{
|
|
int p = d.register_proposition(*i);
|
|
bdd pos = bdd_ithvar(p);
|
|
bdd neg = bdd_nithvar(p);
|
|
unobservable_events = ((unobservable_events & neg)
|
|
| (neg_events & pos));
|
|
observable_events &= neg;
|
|
neg_events &= neg;
|
|
}
|
|
}
|
|
bdd all_events = observable_events | unobservable_events;
|
|
|
|
|
|
tgba_explicit_formula* a = new tgba_explicit_formula(dict);
|
|
|
|
formulae_to_translate.insert(f2);
|
|
a->set_init_state(f2);
|
|
|
|
while (!formulae_to_translate.empty())
|
|
{
|
|
// Pick one formula.
|
|
const formula* now = *formulae_to_translate.begin();
|
|
formulae_to_translate.erase(formulae_to_translate.begin());
|
|
|
|
// Translate it into a BDD to simplify it.
|
|
bdd res = fc.translate(now);
|
|
|
|
// Handle exclusive events.
|
|
if (unobs)
|
|
{
|
|
res &= observable_events;
|
|
int n = d.register_next_variable(now);
|
|
res |= unobservable_events & bdd_ithvar(n) & all_promises;
|
|
}
|
|
|
|
// We used to factor only Next and A variables while computing
|
|
// prime implicants, with
|
|
// minato_isop isop(res, d.next_set & d.a_set);
|
|
// in order to obtain transitions with formulae of atomic
|
|
// proposition directly, but unfortunately this led to strange
|
|
// factorizations. For instance f U g was translated as
|
|
// r(f U g) = g + a(g).r(X(f U g)).(f + g)
|
|
// instead of just
|
|
// r(f U g) = g + a(g).r(X(f U g)).f
|
|
// Of course both formulae are logically equivalent, but the
|
|
// latter is "more deterministic" than the former, so it should
|
|
// be preferred.
|
|
//
|
|
// Therefore we now factor all variables. This may lead to more
|
|
// transitions than necessary (e.g., r(f + g) = f + g will be
|
|
// coded as two transitions), but we later merge all transitions
|
|
// with same source/destination and acceptance conditions. This
|
|
// is the goal of the `dests' hash.
|
|
//
|
|
// Note that this is still not optimal. For instance it is
|
|
// better to encode `f U g' as
|
|
// r(f U g) = g + a(g).r(X(f U g)).f.!g
|
|
// because that leads to a deterministic automaton. In order
|
|
// to handle this, we take the conditions of any transition
|
|
// going to true (it's `g' here), and remove it from the other
|
|
// transitions.
|
|
//
|
|
// In `exprop' mode, considering all possible combinations of
|
|
// outgoing propositions generalizes the above trick.
|
|
dest_map dests;
|
|
|
|
// Compute all outgoing arcs.
|
|
|
|
// If EXPROP is set, we will refine the symbolic
|
|
// representation of the successors for all combinations of
|
|
// the atomic properties involved in the formula.
|
|
// VAR_SET is the set of these properties.
|
|
bdd var_set = bdd_existcomp(bdd_support(res), d.var_set);
|
|
// ALL_PROPS is the combinations we have yet to consider.
|
|
// We used to start with `all_props = bddtrue', but it is
|
|
// more efficient to start with the set of all satisfiable
|
|
// variables combinations.
|
|
bdd all_props = bdd_existcomp(res, d.var_set);
|
|
while (all_props != bddfalse)
|
|
{
|
|
bdd one_prop_set = bddtrue;
|
|
if (exprop)
|
|
one_prop_set = bdd_satoneset(all_props, var_set, bddtrue);
|
|
all_props -= one_prop_set;
|
|
|
|
typedef std::map<bdd, const formula*, bdd_less_than> succ_map;
|
|
succ_map succs;
|
|
|
|
// Compute prime implicants.
|
|
// The reason we use prime implicants and not bdd_satone()
|
|
// is that we do not want to get any negation in front of Next
|
|
// or Acc variables. We wouldn't know what to do with these.
|
|
// We never added negations in front of these variables when
|
|
// we built the BDD, so prime implicants will not "invent" them.
|
|
//
|
|
// FIXME: minato_isop is quite expensive, and I (=adl)
|
|
// don't think we really care that much about getting the
|
|
// smalled sum of products that minato_isop strives to
|
|
// compute. Given that Next and Acc variables should
|
|
// always be positive, maybe there is a faster way to
|
|
// compute the successors? E.g. using bdd_satone() and
|
|
// ignoring negated Next and Acc variables.
|
|
minato_isop isop(res & one_prop_set);
|
|
bdd cube;
|
|
while ((cube = isop.next()) != bddfalse)
|
|
{
|
|
bdd label = bdd_exist(cube, d.next_set);
|
|
bdd dest_bdd = bdd_existcomp(cube, d.next_set);
|
|
const formula* dest = d.conj_bdd_to_formula(dest_bdd);
|
|
|
|
// Simplify the formula, if requested.
|
|
if (reduce_ltl)
|
|
{
|
|
formula* tmp = reduce(dest, reduce_ltl);
|
|
dest->destroy();
|
|
dest = tmp;
|
|
// Ignore the arc if the destination reduces to false.
|
|
if (dest == constant::false_instance())
|
|
continue;
|
|
}
|
|
|
|
// If we already know a state with the same
|
|
// successors, use it in lieu of the current one.
|
|
if (symb_merge)
|
|
dest = fc.canonize(dest);
|
|
|
|
// If we are not postponing the branching, we can
|
|
// declare the outgoing transitions immediately.
|
|
// Otherwise, we merge transitions with identical
|
|
// label, and declare the outgoing transitions in a
|
|
// second loop.
|
|
if (!branching_postponement)
|
|
{
|
|
fill_dests(d, dests, label, dest);
|
|
}
|
|
else
|
|
{
|
|
succ_map::iterator si = succs.find(label);
|
|
if (si == succs.end())
|
|
succs[label] = dest;
|
|
else
|
|
si->second =
|
|
multop::instance(multop::Or,
|
|
const_cast<formula*>(si->second),
|
|
const_cast<formula*>(dest));
|
|
}
|
|
}
|
|
if (branching_postponement)
|
|
for (succ_map::const_iterator si = succs.begin();
|
|
si != succs.end(); ++si)
|
|
fill_dests(d, dests, si->first, si->second);
|
|
}
|
|
|
|
// Check for an arc going to 1 (True). Register it first, that
|
|
// way it will be explored before others during model checking.
|
|
dest_map::const_iterator i = dests.find(constant::true_instance());
|
|
// COND_FOR_TRUE is the conditions of the True arc, so we
|
|
// can remove them from all other arcs. It might sounds that
|
|
// this is not needed when exprop is used, but in fact it is
|
|
// complementary.
|
|
//
|
|
// Consider
|
|
// f = r(X(1) R p) = p.(1 + r(X(1) R p))
|
|
// with exprop the two outgoing arcs would be
|
|
// p p
|
|
// f ----> 1 f ----> f
|
|
//
|
|
// where in fact we could output
|
|
// p
|
|
// f ----> 1
|
|
//
|
|
// because there is no point in looping on f if we can go to 1.
|
|
bdd cond_for_true = bddfalse;
|
|
if (i != dests.end())
|
|
{
|
|
// When translating LTL for an event-based logic with
|
|
// unobservable events, the 1 state should accept all events,
|
|
// even unobservable events.
|
|
if (unobs && now == constant::true_instance())
|
|
cond_for_true = all_events;
|
|
else
|
|
{
|
|
// There should be only one transition going to 1 (true) ...
|
|
assert(i->second.size() == 1);
|
|
prom_map::const_iterator j = i->second.begin();
|
|
// ... and it is not expected to make any promises (unless
|
|
// fair loop approximations are used).
|
|
assert(fair_loop_approx || j->first == bddtrue);
|
|
cond_for_true = j->second;
|
|
}
|
|
if (!a->has_state(constant::true_instance()))
|
|
formulae_to_translate.insert(constant::true_instance());
|
|
state_explicit_formula::transition* t =
|
|
a->create_transition(now, constant::true_instance());
|
|
a->add_condition(t, d.bdd_to_formula(cond_for_true));
|
|
}
|
|
// Register other transitions.
|
|
for (i = dests.begin(); i != dests.end(); ++i)
|
|
{
|
|
const formula* dest = i->first;
|
|
// The cond_for_true optimization can cause some
|
|
// transitions to be removed. So we have to remember
|
|
// whether a formula is actually reachable.
|
|
bool reachable = false;
|
|
|
|
// Will this be a new state?
|
|
bool seen = a->has_state(dest);
|
|
|
|
if (dest != constant::true_instance())
|
|
{
|
|
for (prom_map::const_iterator j = i->second.begin();
|
|
j != i->second.end(); ++j)
|
|
{
|
|
bdd cond = j->second - cond_for_true;
|
|
if (cond == bddfalse) // Skip false transitions.
|
|
continue;
|
|
state_explicit_formula::transition* t =
|
|
a->create_transition(now, dest);
|
|
a->add_condition(t, d.bdd_to_formula(cond));
|
|
d.conj_bdd_to_acc(a, j->first, t);
|
|
reachable = true;
|
|
}
|
|
}
|
|
else
|
|
{
|
|
// "1" is reachable.
|
|
reachable = true;
|
|
}
|
|
if (reachable && !seen)
|
|
formulae_to_translate.insert(dest);
|
|
else
|
|
dest->destroy();
|
|
}
|
|
}
|
|
|
|
// Turn all promises into real acceptance conditions.
|
|
a->complement_all_acceptance_conditions();
|
|
return a;
|
|
}
|
|
|
|
}
|