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

*** empty log message ***

Browse source
This commit is contained in:
martinez 2004-05-10 15:43:18 +00:00
parent faf4a2af26
commit bafc92d0b8
15 changed files with 4510 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/ltlvisit/Makefile.am
View file

@ -33,7 +33,8 @@ ltlvisit_HEADERS = \
lunabbrev.hh \
nenoform.hh \
postfix.hh \
tunabbrev.hh
tunabbrev.hh \
reducform.hh
noinst_LTLIBRARIES = libltlvisit.la
libltlvisit_la_SOURCES = \
@ -45,4 +46,8 @@ libltlvisit_la_SOURCES = \
lunabbrev.cc \
nenoform.cc \
postfix.cc \
tunabbrev.cc
tunabbrev.cc \
reducform.cc \
basereduc.cc \
forminf.cc \
formlength.cc

578
src/ltlvisit/basereduc.cc Normal file
View file

@ -0,0 +1,578 @@
// Copyright (C) 2003 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 "reducform.hh"
#include "ltlast/allnodes.hh"
#include "ltlvisit/clone.hh"
#include <cassert>
#include "ltlvisit/destroy.hh"
namespace spot
{
namespace ltl
{
class basic_reduce_form_visitor : public visitor
{
public:
basic_reduce_form_visitor(){}
virtual ~basic_reduce_form_visitor(){}
formula*
result() const
{
return result_;
}
void
visit(atomic_prop* ap)
{
formula* f = ap->ref();
result_ = f;
}
void
visit(constant* c)
{
switch (c->val())
{
case constant::True:
result_ = constant::true_instance();
return;
case constant::False:
result_ = constant::false_instance();
return;
}
}
void
visit(unop* uo)
{
formula* f = uo->child();
result_ = basic_reduce_form(f);
switch (uo->op())
{
case unop::Not:
result_ = unop::instance(unop::Not, result_);
return;
case unop::X:
/* X(true) = true
X(false) = false */
if (node_type(result_) == (node_type_form_visitor::Const))
return;
/* XGF(f) = GF(f) */
if (is_GF(result_)) return;
/* X(f1 & GF(f2)) = X(f1) & GF(F2) */
/* X(f1 | GF(f2)) = X(f1) | GF(F2) */
if (node_type(result_) == (node_type_form_visitor::Multop)) {
if (spot::ltl::nb_term_multop(result_) == 2) {
if (is_GF(((multop*)result_)->nth(0)) ||
is_FG(((multop*)result_)->nth(0))) {
multop::vec* res = new multop::vec;
res->push_back(unop::instance(unop::F, basic_reduce_form(((multop*)result_)->nth(1))));
res->push_back(basic_reduce_form(((multop*)result_)->nth(0)));
f = result_;
result_ = multop::instance(((multop*)(result_))->op(), res);
spot::ltl::destroy(f);
return;
}
if (is_GF(((multop*)result_)->nth(1)) ||
is_FG(((multop*)result_)->nth(1))) {
multop::vec* res = new multop::vec;
res->push_back(unop::instance(unop::F, basic_reduce_form(((multop*)result_)->nth(0))));
res->push_back(basic_reduce_form(((multop*)result_)->nth(1)));
f = result_;
result_ = multop::instance(((multop*)(result_))->op(), res);
spot::ltl::destroy(f);
return;
}
}
}
result_ = unop::instance(unop::X, result_);
return;
case unop::F:
/* F(true) = true
F(false) = false */
if (node_type(result_) == (node_type_form_visitor::Const))
return;
/* FX(a) = XF(a) */
if (node_type(result_) == (node_type_form_visitor::Unop))
if ( ((unop*)(result_))->op() == unop::X ){
f = result_;
result_ = unop::instance(unop::X,
unop::instance(unop::F,
basic_reduce_form(((unop*)(result_))->child()) ));
spot::ltl::destroy(f);
return;
}
/* F(f1 & GF(f2)) = F(f1) & GF(F2) */
if (node_type(result_) == (node_type_form_visitor::Multop)) {
if ( ((multop*)(result_))->op() == multop::And ) {
if (spot::ltl::nb_term_multop(result_) == 2) {
if (is_GF(((multop*)result_)->nth(0)) ||
is_FG(((multop*)result_)->nth(0))) {
multop::vec* res = new multop::vec;
res->push_back(unop::instance(unop::F, basic_reduce_form(((multop*)result_)->nth(1))));
res->push_back(basic_reduce_form(((multop*)result_)->nth(0)));
spot::ltl::destroy(result_);
result_ = multop::instance(multop::And, res);
return;
}
if (is_GF(((multop*)result_)->nth(1)) ||
is_FG(((multop*)result_)->nth(1))) {
multop::vec* res = new multop::vec;
res->push_back(unop::instance(unop::F, basic_reduce_form(((multop*)result_)->nth(0))));
res->push_back(basic_reduce_form(((multop*)result_)->nth(1)));
spot::ltl::destroy(result_);
result_ = multop::instance(multop::And, res);
return;
}
}
}
}
result_ = unop::instance(unop::F, result_);
return;
case unop::G:
/* G(true) = true
G(false) = false */
if (node_type(result_) == (node_type_form_visitor::Const))
return;
/* G(a R b) = G(b) */
if (node_type(result_) == node_type_form_visitor::Binop)
if ( ((binop*)(result_))->op() == binop::R ){
f = result_;
result_ = unop::instance(unop::G, basic_reduce_form(((binop*)(result_))->second()));
spot::ltl::destroy(f);
return;
}
/* GX(a) = XG(a) */
if (node_type(result_) == (node_type_form_visitor::Unop))
if ( ((unop*)(result_))->op() == unop::X ){
f = result_;
result_ = unop::instance(unop::X,
unop::instance(unop::G,
basic_reduce_form(((unop*)(result_))->child()) ));
spot::ltl::destroy(f);
return;
}
/* G(f1 | GF(f2)) = G(f1) | GF(F2) */
if (node_type(result_) == (node_type_form_visitor::Multop)) {
if ( ((multop*)(f))->op() == multop::Or ) {
if (spot::ltl::nb_term_multop(result_) == 2) {
if (is_GF(((multop*)result_)->nth(0)) ||
is_FG(((multop*)result_)->nth(0))) {
multop::vec* res = new multop::vec;
res->push_back(unop::instance(unop::G, basic_reduce_form(((multop*)result_)->nth(1))));
res->push_back(basic_reduce_form(((multop*)result_)->nth(0)));
spot::ltl::destroy(result_);
result_ = multop::instance(multop::Or, res);
return;
}
if (is_GF(((multop*)result_)->nth(1)) ||
is_FG(((multop*)result_)->nth(1))) {
multop::vec* res = new multop::vec;
res->push_back(unop::instance(unop::G, basic_reduce_form(((multop*)result_)->nth(0))));
res->push_back(basic_reduce_form(((multop*)result_)->nth(1)));
spot::ltl::destroy(result_);
result_ = multop::instance(multop::Or, res);
return;
}
}
}
}
result_ = unop::instance(unop::G, result_);
return;
}
/* Unreachable code. */
assert(0);
}
void
visit(binop* bo)
{
formula* f1 = bo->first();
formula* f2 = bo->second();
formula* ftmp = NULL;
node_type_form_visitor v1;
node_type_form_visitor v2;
switch (bo->op())
{
case binop::Xor:
result_ = binop::instance(binop::Xor,
basic_reduce_form(f1),
basic_reduce_form(f2));
return;
case binop::Equiv:
result_ = binop::instance(binop::Equiv,
basic_reduce_form(f1),
basic_reduce_form(f2));
return;
case binop::Implies:
result_ = binop::instance(binop::Implies,
basic_reduce_form(f1),
basic_reduce_form(f2));
return;
case binop::U:
f2 = basic_reduce_form(f2);
/* a U false = false
a U true = true */
if (node_type(f2) == (node_type_form_visitor::Const)) {
result_ = f2;
return;
}
f1 = basic_reduce_form(f1);
/* X(a) U X(b) = X(a U b) */
if ( node_type(f1) == (node_type_form_visitor::Unop)
&& node_type(f2) == (node_type_form_visitor::Unop)) {
if ( (((unop*)(f1))->op() == unop::X)
&& (((unop*)(f2))->op() == unop::X) ) {
ftmp = binop::instance(binop::U,
basic_reduce_form(((unop*)(f1))->child()),
basic_reduce_form(((unop*)(f2))->child()));
result_ = unop::instance(unop::X, basic_reduce_form(ftmp));
spot::ltl::destroy(f1);
spot::ltl::destroy(f2);
spot::ltl::destroy(ftmp);
return;
}
}
result_ = binop::instance(binop::U, f1, f2);
return;
case binop::R:
f2 = basic_reduce_form(f2);
/* a R false = false
a R true = true */
if (node_type(f2) == (node_type_form_visitor::Const)) {
result_ = f2;
return;
}
f1 = basic_reduce_form(f1);
/* X(a) R X(b) = X(a R b) */
if ( node_type(f1) == (node_type_form_visitor::Unop)
&& node_type(f2) == (node_type_form_visitor::Unop)) {
if ( (((unop*)(f1))->op() == unop::X)
&& (((unop*)(f2))->op() == unop::X) ) {
ftmp = binop::instance(bo->op(),
basic_reduce_form(((unop*)(f1))->child()),
basic_reduce_form(((unop*)(f2))->child()));
result_ = unop::instance(unop::X, basic_reduce_form(ftmp));
spot::ltl::destroy(f1);
spot::ltl::destroy(f2);
spot::ltl::destroy(ftmp);
return;
}
}
result_ = binop::instance(bo->op(),
f1, f2);
return;
}
/* Unreachable code. */
assert(0);
}
void
visit(multop* mo)
{
if (mo == NULL);
multop::type op = mo->op();
unsigned mos = mo->size();
multop::vec* res = new multop::vec;
multop::vec* tmpX = new multop::vec;
multop::vec* tmpU = new multop::vec;
multop::vec* tmpUright = NULL;
multop::vec* tmpR = new multop::vec;
multop::vec* tmpRright = NULL;
multop::vec* tmpFG = new multop::vec;
multop::vec* tmpGF = new multop::vec;
multop::vec* tmpOther = new multop::vec;
formula* ftmp = NULL;
for (unsigned i = 0; i < mos; ++i)
res->push_back(basic_reduce_form(mo->nth(i)));
switch (op)
{
case multop::And:
for (multop::vec::iterator i = res->begin(); i != res->end(); i++) {
if (*i == NULL) continue;
switch (node_type(*i)) {
case node_type_form_visitor::Unop:
/* Xa & Xb = X(a & b)*/
if (((unop*)(*i))->op() == unop::X) {
tmpX->push_back( spot::ltl::basic_reduce_form(((unop*)(*i))->child()) );
break;
}
/* FG(a) & FG(b) = FG(a & b)*/
if (is_FG(*i)) {
tmpFG->push_back( spot::ltl::basic_reduce_form( ((unop*)((unop*)(*i))->child())->child() ) );
break;
}
tmpOther->push_back(spot::ltl::basic_reduce_form(*i));
break;
/* A GERER !!!!!!!!!!!!!!!!!!!!!!!
case node_type_form_visitor::Const:
tmpX->push_back( spot::ltl::clone((*i)) );
break;
*/
case node_type_form_visitor::Binop:
/* (a U b) & (c U b) = (a & c) U b */
if (((binop*)(*i))->op() == binop::U) {
ftmp = ((binop*)(*i))->second();
tmpUright = new multop::vec;
for (multop::vec::iterator j = i; j != res->end(); j++)
{
if (*j == NULL) continue;
if (node_type(*j) == node_type_form_visitor::Binop)
{
if (((binop*)(*j))->op() == binop::U)
{
if (ftmp == ((binop*)(*j))->second())
{
tmpUright->push_back(spot::ltl::basic_reduce_form(((binop*)(*j))->first() ));
if (j != i) {
spot::ltl::destroy(*j);
*j = NULL;
}
}
}
}
}
tmpU->push_back(binop::instance(binop::U,
multop::instance(multop::And,tmpUright),
basic_reduce_form(ftmp)));
break;
}
/* (a R b) & (a R c) = a R (b & c) */
if (((binop*)(*i))->op() == binop::R) {
ftmp = ((binop*)(*i))->first();
tmpRright = new multop::vec;
for (multop::vec::iterator j = i; j != res->end(); j++)
{
if (*j == NULL) continue;
if (node_type(*j) == node_type_form_visitor::Binop)
{
if (((binop*)(*j))->op() == binop::R)
{
if (ftmp == ((binop*)(*j))->first())
{
tmpRright->push_back(spot::ltl::basic_reduce_form(((binop*)(*j))->second() ));
if (j != i) {
spot::ltl::destroy(*j);
*j = NULL;
}
}
}
}
}
tmpR->push_back(binop::instance(binop::R,
basic_reduce_form(ftmp),
multop::instance(multop::And,tmpRright)));
break;
}
tmpOther->push_back(spot::ltl::basic_reduce_form(*i));
break;
default:
tmpOther->push_back(spot::ltl::basic_reduce_form(*i));
break;
}
spot::ltl::destroy(*i);
}
delete(tmpGF);
tmpGF = NULL;
break;
case multop::Or:
for (multop::vec::iterator i = res->begin(); i != res->end(); i++) {
if (*i == NULL) continue;
switch (node_type(*i)) {
case node_type_form_visitor::Unop:
/* Xa | Xb = X(a | b)*/
if (((unop*)(*i))->op() == unop::X) {
tmpX->push_back( spot::ltl::basic_reduce_form(((unop*)(*i))->child()) );
break;
}
/* GF(a) & GF(b) = GF(a & b)*/
if (is_GF(*i)) {
tmpGF->push_back( spot::ltl::basic_reduce_form( ((unop*)((unop*)(*i))->child())->child() ) );
break;
}
tmpOther->push_back(spot::ltl::basic_reduce_form(*i));
break;
case node_type_form_visitor::Binop:
/* (a U b) | (a U c) = a U (b | c) */
if (((binop*)(*i))->op() == binop::U) {
ftmp = ((binop*)(*i))->first();
tmpUright = new multop::vec;
for (multop::vec::iterator j = i; j != res->end(); j++)
{
if (*j == NULL) continue;
if (node_type(*j) == node_type_form_visitor::Binop)
{
if (((binop*)(*j))->op() == binop::U)
{
if (ftmp == ((binop*)(*j))->first())
{
tmpUright->push_back(spot::ltl::basic_reduce_form(((binop*)(*j))->second() ));
if (j != i) {
spot::ltl::destroy(*j);
*j = NULL;
}
}
}
}
}
tmpU->push_back(binop::instance(binop::U,
basic_reduce_form(ftmp),
multop::instance(multop::Or,tmpUright)));
break;
}
/* (a R b) | (c R b) = (a | c) R b */
if (((binop*)(*i))->op() == binop::R) {
ftmp = ((binop*)(*i))->second();
tmpRright = new multop::vec;
for (multop::vec::iterator j = i; j != res->end(); j++)
{
if (*j == NULL) continue;
if (node_type(*j) == node_type_form_visitor::Binop)
{
if (((binop*)(*j))->op() == binop::R)
{
if (ftmp == ((binop*)(*j))->second())
{
tmpRright->push_back(spot::ltl::basic_reduce_form(((binop*)(*j))->first() ));
if (j != i) {
spot::ltl::destroy(*j);
*j = NULL;
}
}
}
}
}
tmpR->push_back(binop::instance(binop::R,
multop::instance(multop::Or,tmpRright),
basic_reduce_form(ftmp)));
break;
}
tmpOther->push_back(spot::ltl::basic_reduce_form(*i));
break;
default:
tmpOther->push_back(spot::ltl::basic_reduce_form(*i));
break;
}
spot::ltl::destroy(*i);
}
delete(tmpFG);
tmpFG = NULL;
break;
}
res->clear();
delete(res);
if (tmpX->size())
tmpOther->push_back(unop::instance(unop::X,multop::instance(mo->op(),tmpX)));
else delete(tmpX);
if (tmpU->size())
tmpOther->push_back(multop::instance(mo->op(),tmpU));
else delete(tmpU);
if (tmpR->size())
tmpOther->push_back(multop::instance(mo->op(),tmpR));
else delete(tmpR);
if (tmpGF != NULL)
if (tmpGF->size())
tmpOther->push_back(unop::instance(unop::G,
unop::instance(unop::F,
multop::instance(mo->op(),tmpGF))));
if (tmpFG != NULL)
if (tmpFG->size())
tmpOther->push_back(unop::instance(unop::G,
unop::instance(unop::F,
multop::instance(mo->op(),tmpFG))));
result_ = multop::instance(op, tmpOther);
return;
}
protected:
formula* result_;
};
formula* basic_reduce_form(const formula* f)
{
basic_reduce_form_visitor v;
const_cast<formula*>(f)->accept(v);
return v.result();
}
}
}

619
src/ltlvisit/forminf.cc Normal file
View file

@ -0,0 +1,619 @@
// Copyright (C) 2003 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 "reducform.hh"
#include "ltlast/allnodes.hh"
#include <cassert>
#include "lunabbrev.hh"
#include "nenoform.hh"
#include "ltlvisit/destroy.hh"
namespace spot
{
namespace ltl
{
bool
is_GF(const formula* f)
{
if ((const unop*)f != NULL)
if (((const unop*)f)->op() == unop::G)
if ((const unop*)(((const unop*)f)->child()) != NULL)
if (((const unop*)((const unop*)f)->child())->op() == unop::F)
return true;
return false;
}
bool
is_FG(const formula* f)
{
if ((const unop*)f != NULL)
if (((const unop*)f)->op() == unop::F)
if ((const unop*)(((const unop*)f)->child()) != NULL)
if (((const unop*)((const unop*)f)->child())->op() == unop::G)
return true;
return false;
}
int
nb_term_multop(const formula* f)
{
if ((const multop*)f == NULL) return -1;
unsigned mos = ((const multop*)(f))->size();
return mos;
}
node_type_form_visitor::node_type_form_visitor(){}
node_type_form_visitor::type
node_type_form_visitor::result() const { return result_;}
void
node_type_form_visitor::visit(const atomic_prop* ap){
if (ap == NULL);
result_ = node_type_form_visitor::Atom;
}
void
node_type_form_visitor::visit(const constant* c){
if (c == NULL);
result_ = node_type_form_visitor::Const;
}
void
node_type_form_visitor::visit(const unop* uo){
if (uo == NULL);
result_ = node_type_form_visitor::Unop;
}
void
node_type_form_visitor::visit(const binop* bo){
if (bo == NULL);
result_ = node_type_form_visitor::Binop;
}
void
node_type_form_visitor::visit(const multop* mo){
if (mo == NULL);
result_ = node_type_form_visitor::Multop;
}
node_type_form_visitor::type node_type(const formula* f)
{
node_type_form_visitor v;
if (f == NULL) std::cout << "f == NULL !!!!!!!!" << std::endl;
const_cast<formula*>(f)->accept(v);
return v.result();
}
class form_eventual_universal_visitor : public const_visitor
{
public:
form_eventual_universal_visitor()
{
eventual = false; // faux au départ
universal = false;
}
virtual ~form_eventual_universal_visitor()
{
}
bool
is_eventual() const
{
return eventual;
}
bool
is_universal() const
{
return universal;
}
void
visit(const atomic_prop* ap)
{
if (ap);
}
void
visit(const constant* c)
{
if (c->val());
}
void
visit(const unop* uo)
{
const formula* f1 = uo->child();
switch (uo->op())
{
case unop::Not:
case unop::X:
eventual = recurse_ev(f1);
universal = recurse_un(f1);
return;
case unop::F:
eventual = true;
return;
case unop::G:
universal = true;
return;
}
/* Unreachable code. */
assert(0);
}
void
visit(const binop* bo)
{
const formula* f1 = bo->first();
switch (bo->op())
{
case binop::Xor:
case binop::Equiv:
case binop::Implies:
return;
case binop::U:
if (node_type(f1) == node_type_form_visitor::Const)
if (((const constant*)f1)->val() == constant::True)
eventual = true;
return;
case binop::R:
if (node_type(f1) != node_type_form_visitor::Const)
if (((const constant*)f1)->val() == constant::False)
universal = true;
return;
}
/* Unreachable code. */
assert(0);
}
void
visit(const multop* mo)
{
if (mo == NULL);
unsigned mos = mo->size();
eventual = true;
universal = true;
for (unsigned i = 0; i < mos; ++i){
if ( !(recurse_ev(mo->nth(i))) ){
eventual = false;
break;
}
}
for (unsigned i = 0; i < mos; ++i){
if ( !(recurse_un(mo->nth(i))) ){
universal = false;
break;
}
}
}
bool
recurse_ev(const formula* f)
{
form_eventual_universal_visitor v;
const_cast<formula*>(f)->accept(v);
return v.is_eventual();
}
bool
recurse_un(const formula* f)
{
form_eventual_universal_visitor v;
const_cast<formula*>(f)->accept(v);
return v.is_universal();
}
protected:
bool eventual;
bool universal;
};
bool is_eventual(const formula* f)
{
form_eventual_universal_visitor v;
const_cast<formula*>(f)->accept(v);
return v.is_eventual();
}
bool is_universal(const formula* f)
{
form_eventual_universal_visitor v;
const_cast<formula*>(f)->accept(v);
return v.is_universal();
}
/////////////////////////////////////////////////////////////////////////
class inf_form_right_recurse_visitor : public const_visitor
{
public:
inf_form_right_recurse_visitor(const formula *f)
{
this->f = f;
result_ = false; // faux au départ
}
virtual ~inf_form_right_recurse_visitor()
{
}
/*
bool special_case(const formula* f2,binop::operator op)
{
const binop* b = (const binop*)f;
const binop* b2 = (const binop*)f2;
if ((b != NULL) && (b2 != NULL) &&
(b->op() == b2_>op() == op))
if (inf_form(b2->first(),b->first())
&& inf_form(b2->second(),b->second()) )
return true;
return false;
}
*/
int
result() const
{
return result_;
}
void
visit(const atomic_prop* ap)
{
if ((const atomic_prop*)f == ap)
result_ = true;
}
void
visit(const constant* c)
{
switch (c->val())
{
case constant::True:
result_ = true;
return;
case constant::False:
result_ = false;
return;
}
}
void
visit(const unop* uo)
{
const formula* f1 = uo->child();
const formula* tmp = NULL;
switch (uo->op())
{
case unop::Not:// à gérer !!
return;
case unop::X:// à gérer !!
return;
case unop::F:
// F(a) = true U a
result_ = inf_form(f,f1);
return;
case unop::G:
// G(a) = false R a
tmp = constant::false_instance();
if ( inf_form(f,tmp) )
result_ = true;
spot::ltl::destroy(tmp);
return;
}
/* Unreachable code. */
assert(0);
}
void
visit(const binop* bo)
{
const formula* f1 = bo->first();
const formula* f2 = bo->second();
switch (bo->op())
{
case binop::Xor:
case binop::Equiv:
case binop::Implies:
return;
case binop::U:
if ( (inf_form(f,f2)) )
result_ = true;
return;
case binop::R:
if ( (inf_form(f,f1)) && (inf_form(f,f2)) )
result_ = true;
return;
}
/* Unreachable code. */
assert(0);
}
void
visit(const multop* mo)
{
if (mo == NULL);
multop::type op = mo->op();
unsigned mos = mo->size();
switch (op)
{
case multop::And:
for (unsigned i = 0; (i < mos) ; ++i)
if ( !(inf_form(f,mo->nth(i))) )
return;
result_ = true;
break;
case multop::Or:
for (unsigned i = 0; i < mos && !result_; ++i)
if ( (inf_form(f,mo->nth(i))) )
result_ = true;
break;
}
}
bool
recurse(const formula* f1, const formula* f2)
{
if (f1 == f2) return true;
inf_form_right_recurse_visitor v(f2);
const_cast<formula*>(f1)->accept(v);
return v.result();
}
protected:
bool result_; // true si f < f1, false sinon.
const formula* f;
};
/////////////////////////////////////////////////////////////////////////
class inf_form_left_recurse_visitor : public const_visitor
{
public:
inf_form_left_recurse_visitor(const formula *f)
{
this->f = f;
result_ = false;
}
virtual ~inf_form_left_recurse_visitor()
{
}
bool special_case(const formula* f2)
{
if ((node_type(f) == node_type_form_visitor::Binop)
&& (node_type(f2) == node_type_form_visitor::Binop))
if (((const binop*)f)->op() == ((const binop*)f2)->op())
if (inf_form(((const binop*)f2)->first(),((const binop*)f)->first())
&& inf_form(((const binop*)f2)->second(),((const binop*)f)->second()) )
return true;
return false;
}
int
result() const
{
return result_;
}
void
visit(const atomic_prop* ap)
{
inf_form_right_recurse_visitor v(ap);
const_cast<formula*>(f)->accept(v);
result_ = v.result();
}
void
visit(const constant* c)
{
inf_form_right_recurse_visitor v(c);
switch (c->val())
{
case constant::True:
const_cast<formula*>(f)->accept(v);
result_ = v.result();
return;
case constant::False:
result_ = true;
return;
}
/* Unreachable code. */
assert(0);
}
void
visit(const unop* uo)
{
const formula* f1 = uo->child();
const formula* tmp = NULL;
inf_form_right_recurse_visitor v(uo);
switch (uo->op())
{
case unop::Not:
if (uo == f)
result_ = true;
return;
case unop::X:
if (node_type(f) == node_type_form_visitor::Unop)
if (((const unop*)f)->op() == unop::X) {
result_ = inf_form(f1,((const unop*)f)->child());
}
return;
case unop::F:
// F(a) = true U a
tmp = binop::instance(binop::U,constant::true_instance(),clone(f1));
if (this->special_case(tmp)){
result_ = true;
spot::ltl::destroy(tmp);
return;
}
if ( inf_form(tmp,f) )
result_ = true;
spot::ltl::destroy(tmp);
return;
case unop::G:
// F(a) = false R a
tmp = binop::instance(binop::R,constant::false_instance(),clone(f1));
if (this->special_case(tmp)){
result_ = true;
spot::ltl::destroy(tmp);
return;
}
if ( inf_form(f1,f) )
result_ = true;
spot::ltl::destroy(tmp);
return;
}
/* Unreachable code. */
assert(0);
}
void
visit(const binop* bo)
{
if (this->special_case(bo))
{
result_ = true;
return;
}
const formula* f1 = bo->first();
const formula* f2 = bo->second();
switch (bo->op())
{
case binop::Xor:
case binop::Equiv:
case binop::Implies:
return;
case binop::U:
if ( (inf_form(f1,f)) && (inf_form(f2,f)) )
result_ = true;
return;
case binop::R:
if ( (inf_form(f2,f)) )
result_ = true;
return;
}
/* Unreachable code. */
assert(0);
}
void
visit(const multop* mo)
{
if (mo == NULL);
multop::type op = mo->op();
unsigned mos = mo->size();
switch (op)
{
case multop::And:
for (unsigned i = 0; (i < mos) && !result_ ; ++i)
if ( (inf_form(mo->nth(i),f)) )
result_ = true;
break;
case multop::Or:
for (unsigned i = 0; i < mos ; ++i)
if ( !(inf_form(mo->nth(i),f)) )
return;
result_ = true;
break;
}
}
protected:
bool result_; // true if f1 < f, 1 otherwise.
const formula* f;
};
bool inf_form(const formula* f1, const formula* f2)
{
// f1 and f2 are unabbreviate
if (f1 == f2) return true;
inf_form_left_recurse_visitor v1(f2);
inf_form_right_recurse_visitor v2(f1);
if ( (node_type(f1) == node_type_form_visitor::Const) &&
(node_type(f2) == node_type_form_visitor::Const) )
if ( (((const constant*)f2)->val() == constant::True) ||
(((const constant*)f1)->val() == constant::False) )
{
return true;
}
const_cast<formula*>(f1)->accept(v1);
if (v1.result()) {
return true;
}
const_cast<formula*>(f2)->accept(v2);
if (v2.result()) {
return true;
}
return false;
}
bool infneg_form(const formula* f1, const formula* f2, int n)
{
const formula* ftmp1;
const formula* ftmp2;
const formula* ftmp3 = unop::instance(unop::Not,(n == 0)? clone(f1) : clone(f2));
const formula* ftmp4 = spot::ltl::negative_normal_form((n == 0)? f2 : f1);
const formula* ftmp5;
const formula* ftmp6;
bool retour;
ftmp2 = spot::ltl::unabbreviate_logic(ftmp3);
ftmp1 = spot::ltl::negative_normal_form(ftmp2);
ftmp5 = spot::ltl::unabbreviate_logic(ftmp4);
ftmp6 = spot::ltl::negative_normal_form(ftmp5);
if (n == 0)
retour = inf_form(ftmp1, ftmp6);
else
retour = inf_form(ftmp6, ftmp1);
spot::ltl::destroy(ftmp1);
spot::ltl::destroy(ftmp2);
spot::ltl::destroy(ftmp3);
spot::ltl::destroy(ftmp4);
spot::ltl::destroy(ftmp5);
spot::ltl::destroy(ftmp6);
return retour;
}
}
}

103
src/ltlvisit/formlength.cc Normal file
View file

@ -0,0 +1,103 @@
// Copyright (C) 2003 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 "reducform.hh"
#include "ltlast/allnodes.hh"
#include <cassert>
#include "lunabbrev.hh"
#include "nenoform.hh"
#include "ltlvisit/destroy.hh"
namespace spot
{
namespace ltl
{
class length_form_visitor : public const_visitor
{
public:
length_form_visitor()
{
result_ = 0;
}
virtual ~length_form_visitor()
{
}
int
result() const
{
return result_;
}
void
visit(const atomic_prop* ap)
{
if (ap);
result_ = 1;
}
void
visit(const constant* c)
{
if (c);
result_ = 1;
}
void
visit(const unop* uo)
{
if (uo);
result_ = 1 + form_length(uo->child());
}
void
visit(const binop* bo)
{
if (bo);
result_ = 1 + form_length(bo->first()) + form_length(bo->second());
}
void
visit(const multop* mo)
{
unsigned mos = mo->size();
for (unsigned i = 0; i < mos; ++i)
result_ += form_length(mo->nth(i));
}
protected:
int result_; // size of the formula
};
int
form_length(const formula* f)
{
length_form_visitor v;
const_cast<formula*>(f)->accept(v);
return v.result();
}
}
}

91
src/ltlvisit/lunabbrev.cc
View file

@ -22,12 +22,58 @@
#include "ltlast/allnodes.hh"
#include "ltlvisit/clone.hh"
#include "lunabbrev.hh"
//#include "reducform.hh"
#include <cassert>
namespace spot
{
namespace ltl
{
class node_type_form_visitor : public const_visitor
{
public:
enum type { Atom, Const, Unop, Binop, Multop };
node_type_form_visitor(){}
type
result() const { return result_;}
void
visit(const atomic_prop* ap){
if (ap == NULL);
result_ = node_type_form_visitor::Atom;
}
void
visit(const constant* c){
if (c == NULL);
result_ = node_type_form_visitor::Const;
}
void
visit(const unop* uo){
if (uo == NULL);
result_ = node_type_form_visitor::Unop;
}
void
visit(const binop* bo){
if (bo == NULL);
result_ = node_type_form_visitor::Binop;
}
void
visit(const multop* mo){
if (mo == NULL);
result_ = node_type_form_visitor::Multop;
}
protected:
type result_;
};
unabbreviate_logic_visitor::unabbreviate_logic_visitor()
{
}
@ -36,11 +82,38 @@ namespace spot
{
}
/*
void
unabbreviate_logic_visitor::visit(unop* uo)
{
formula* f = uo->child();
switch (uo->op())
{
case unop::Not:
case unop::X:
result_ = unop::instance(uo->op(),recurse(f));
return;
case unop::F:
result_ = binop::instance(binop::U,constant::true_instance(),recurse(f));
return;
case unop::G:
result_ = binop::instance(binop::R,constant::false_instance(),recurse(f));
return;
}
// Unreachable code.
assert(0);
}
*/
void
unabbreviate_logic_visitor::visit(binop* bo)
{
formula* f1 = recurse(bo->first());
formula* f2 = recurse(bo->second());
node_type_form_visitor v;
const_cast<formula*>(f1)->accept(v);
switch (bo->op())
{
/* f1 ^ f2 == (f1 & !f2) | (f2 & !f1) */
@ -69,10 +142,24 @@ namespace spot
unop::instance(unop::Not,
f2)));
return;
/* f1 U f2 == f1 U f2 */
/* f1 R f2 == f1 R f2 */
/* true U f2 == F(f2) */
case binop::U:
if ( v.result() == node_type_form_visitor::Const )
if ( ((constant*)f1)->val() == constant::True ) {
result_ = unop::instance(unop::F,f2);
return;
}
result_ = binop::instance(bo->op(), f1, f2);
return;
/* false R f2 == G(f2) */
case binop::R:
if ( v.result() == node_type_form_visitor::Const )
if ( ((constant*)f1)->val() == constant::False ) {
result_ = unop::instance(unop::G,f2);
return;
}
result_ = binop::instance(bo->op(), f1, f2);
return;
}

1
src/ltlvisit/lunabbrev.hh
View file

@ -47,6 +47,7 @@ namespace spot
virtual ~unabbreviate_logic_visitor();
using super::visit;
//void visit(unop* uo);
void visit(binop* bo);
virtual formula* recurse(formula* f);

1
src/ltlvisit/nenoform.hh
View file

@ -43,6 +43,7 @@ namespace spot
/// or spot::ltl::unabbreviate_ltl first. (Calling these functions
/// after spot::ltl::negative_normal_form would likely produce a
/// formula which is not in negative normal form.)
formula* negative_normal_form(const formula* f, bool negated = false);
}
}

392
src/ltlvisit/reducform.cc Normal file
View file

@ -0,0 +1,392 @@
// Copyright (C) 2003 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 "reducform.hh"
#include "ltlast/allnodes.hh"
#include <cassert>
#include "lunabbrev.hh"
#include "nenoform.hh"
#include "ltlvisit/destroy.hh"
namespace spot
{
namespace ltl
{
//class unabbreviate_FG_visitor::unabbreviate_logic_visitor()
class reduce_form_visitor : public visitor
{
public:
reduce_form_visitor()
{
/*
eventuality_ = false;
universality_ = false;
*/
}
virtual ~reduce_form_visitor()
{
}
formula*
result() const
{
return result_;
}
/*
bool
is_eventuality()
{
return eventuality_;
}
bool
is_universality()
{
return universality_;
}
*/
void
visit(atomic_prop* ap)
{
formula* f = ap->ref();
result_ = f;
}
void
visit(constant* c)
{
switch (c->val())
{
case constant::True:
result_ = constant::true_instance();
return;
case constant::False:
result_ = constant::false_instance();
return;
}
/* Unreachable code. */
assert(0);
}
void
visit(unop* uo)
{
result_ = recurse(uo->child());
switch (uo->op())
{
case unop::Not:
result_ = unop::instance(unop::Not, result_);
return;
case unop::X:
result_ = unop::instance(unop::X, result_);
return;
case unop::F:
/* if f is class of eventuality then F(f)=f */
if (!is_eventual(result_)) {
result_ = unop::instance(unop::F, result_);
}
return;
case unop::G:
/* if f is class of universality then G(f)=f */
if (!is_universal(result_)) {
result_ = unop::instance(unop::G, result_);
}
return;
}
/* Unreachable code. */
assert(0);
}
void
visit(binop* bo)
{
formula* f2 = recurse(bo->second());
/* if b is of class eventuality then a U b = b
if b is of class universality then a R b = b */
if ( ( is_eventual(f2) && ( (bo->op()) == binop::U )) ||
( is_universal(f2) && ( (bo->op()) == binop::R )) )
{
result_ = f2;
return;
}
/* case of implies */
formula* f1 = recurse(bo->first());
bool inf = inf_form(f1,f2);
bool infinv = inf_form(f2,f1);
//binop* ftmp = NULL;
bool infnegleft = infneg_form(f2,f1,0);
bool infnegright = infneg_form(f2,f1,1);
switch (bo->op())
{
case binop::Xor:
case binop::Equiv:
case binop::Implies:
result_ = binop::instance(bo->op(), f1, f2);
return;
case binop::U:
/* a < b => a U b = b */
if (inf)
{
result_ = f2;
spot::ltl::destroy(f1);
return;
}
/* !b < a => a U b = Fb */
if (infnegleft)
{
result_ = unop::instance(unop::F, f2);
spot::ltl::destroy(f1);
return;
}
/* a < b => a U (b U c) = (b U c) */
if (node_type(f2) == node_type_form_visitor::Binop)
if (((binop*)f2)->op() == binop::U)
if (inf_form(f1,((binop*)f2)->first())){
result_ = f2;
spot::ltl::destroy(f1);
return;
}
result_ = binop::instance(binop::U,
f1, f2);
return;
case binop::R:
/* b < a => a R b = b */
if (infinv)
{
result_ = f2;
spot::ltl::destroy(f1);
return;
}
/* b < !a => a R b = Gb */
if (infnegright)
{
result_ = unop::instance(unop::G, f2);
spot::ltl::destroy(f1);
return;
}
/* b < a => a R (b R c) = b R c */
if (node_type(f2) == node_type_form_visitor::Binop)
if (((binop*)f2)->op() == binop::R)
if (inf_form(((binop*)f2)->first(),f1)){
result_ = f2;
spot::ltl::destroy(f1);
return;
}
result_ = binop::instance(binop::R,
f1, f2);
return;
}
/* Unreachable code. */
assert(0);
}
void
visit(multop* mo)
{
formula* f1 = NULL;
formula* f2 = NULL;
unsigned mos = mo->size();
multop::vec* res = new multop::vec;
multop::vec::iterator index;
multop::vec::iterator indextmp;
for (unsigned i = 0; i < mos; ++i)
res->push_back(recurse(mo->nth(i)));
switch (mo->op())
{
case multop::Or:
index = indextmp = res->begin();
if (index != res->end())
{
f1 = *index;
index++;
}
for (; index != res->end();index++)
{
f2 = *index;
/* a < b => a + b = b */
if (inf_form(f1,f2)) // f1 < f2
{
f1 = f2;
spot::ltl::destroy(*indextmp);
res->erase(indextmp);
indextmp = index;
index--;
}
else if (inf_form(f2,f1)) // f2 < f1
{
spot::ltl::destroy(*index);
res->erase(index);
index--;
}
}
break;
case multop::And:
index = indextmp = res->begin();
if (mos)
{
f1 = mo->nth(0);
index++;
}
for (; index != res->end(); index++)
{
f2 = *index;
/* a < b => a & b = a */
if (inf_form(f1,f2)) // f1 < f2
{
spot::ltl::destroy(*index);
res->erase(index);
index--;
}
else if (inf_form(f2,f1)) // f2 < f1
{
f1 = f2;
spot::ltl::destroy(*indextmp);
res->erase(indextmp);
indextmp = index;
index--;
}
}
break;
}
/* f1 < !f2 => f1 & f2 = false
!f1 < f2 => f1 | f2 = true */
for (index = res->begin(); index != res->end(); index++){
for (indextmp = res->begin(); indextmp != res->end(); indextmp++){
if (index != indextmp){
if (infneg_form(*index,*indextmp, (mo->op() == multop::Or) ? 0 : 1)) {
for (multop::vec::iterator j = res->begin(); j != res->end(); j++){
spot::ltl::destroy(*j);
}
if (mo->op() == multop::Or)
result_ = constant::true_instance();
else
result_ = constant::false_instance();
return;
}
/*
if ((constant*)(*index) != NULL)
if (((((constant*)(*index))->val() == constant::True) &&
(mo->op() == multop::Or)) ||
(((((constant*)(*index))->val() == constant::False))
&& (mo->op() == multop::And))
) {
//std::cout << "constant" << std::endl;
for (multop::vec::iterator j = res->begin(); j != res->end(); j++){
spot::ltl::destroy(*j);
}
if (mo->op() == multop::Or)
result_ = constant::true_instance();
else
result_ = constant::false_instance();
std::cout << "2" << std::endl;
spot::ltl::dump(std::cout,mo);
return;
}
*/
}
}
}
if (res->size()) {
result_ = multop::instance(mo->op(),res);
return;
}
assert(0);
}
formula*
recurse(formula* f)
{
return reduce_form(f);
}
protected:
formula* result_;
/*
bool eventuality_;
bool universality_;
*/
};
formula*
reduce_form(const formula* f)
{
spot::ltl::formula* ftmp1;
spot::ltl::formula* ftmp2;
reduce_form_visitor v;
ftmp1 = spot::ltl::basic_reduce_form(f);
const_cast<formula*>(ftmp1)->accept(v);
ftmp2 = spot::ltl::basic_reduce_form(v.result());
spot::ltl::destroy(ftmp1);
spot::ltl::destroy(v.result());
return ftmp2;
}
formula*
reduce(const formula* f)
{
spot::ltl::formula* ftmp1;
spot::ltl::formula* ftmp2;
spot::ltl::formula* ftmp3;
ftmp1 = spot::ltl::unabbreviate_logic(f);
ftmp2 = spot::ltl::negative_normal_form(ftmp1);
ftmp3 = spot::ltl::reduce_form(ftmp2);
spot::ltl::destroy(ftmp1);
spot::ltl::destroy(ftmp2);
return ftmp3;
}
}
}

86
src/ltlvisit/reducform.hh Normal file
View file

@ -0,0 +1,86 @@
// Copyright (C) 2003 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.
#ifndef SPOT_LTLVISIT_REDUCFORM_HH
# define SPOT_LTLVISIT_REDUCFORM_HH
#include "ltlast/formula.hh"
#include "ltlast/visitor.hh"
// For debog
#include "ltlvisit/dump.hh"
namespace spot
{
namespace ltl
{
formula* reduce(const formula* f);
/* Basic rewriting */
formula* basic_reduce_form(const formula* f);
/* formula rewriting using univerality, eventuality,
implies and basic_reduce_form */
formula* reduce_form(const formula* f);
/* detect easy case of implies */
bool inf_form(const formula* f1, const formula* f2);
/* true if f1 < f2, false otherwise */
bool infneg_form(const formula* f1, const formula* f2, int n);
/* true if !f1 < f2, false otherwise */
/* detect if a formula is of class eventuality or universality */
bool is_eventual(const formula* f);
bool is_universal(const formula* f);
/* detect if a formula is of form GF or FG */
bool is_GF(const formula* f);
bool is_FG(const formula* f);
/* To know the first node of a formula */
class node_type_form_visitor : public const_visitor
{
public:
enum type { Atom, Const, Unop, Binop, Multop };
node_type_form_visitor();
virtual ~node_type_form_visitor(){};
type result() const;
void visit(const atomic_prop* ap);
void visit(const constant* c);
void visit(const unop* uo);
void visit(const binop* bo);
void visit(const multop* mo);
protected:
type result_;
};
node_type_form_visitor::type node_type(const formula* f);
/* Obsolete */
int nb_term_multop(const formula* f);
formula* reduce_inf_form(const formula* f); /* Obsolete */
int form_length(const formula* f); /* For test */
}
}
#endif // SPOT_LTLVISIT_REDUCFORM_HH