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

Modify the ELTL parser to be able to support PSL operators. Add a

Browse source 
new keyword in the ELTL format: finish, which applies to an
automaton operator and tells whether it just completed.

* src/eltlparse/eltlparse.yy: Clean it. Add finish.
* src/eltlparse/eltlscan.ll: Add finish.
* src/formula_tree.cc, src/formula_tree.hh: New files. Define a
small AST representing formulae where atomic props are unknown
which is used in the ELTL parser.
* src/ltlast/automatop.cc, ltlast/automatop.hh, ltlast/nfa.cc,
ltlast/nfa.hh: Adjust.
* src/ltlast/unop.cc, src/ltlast/unop.hh: Finish is an unop.
* src/ltlvisit/basicreduce.cc, src/ltlvisit/nenoform.cc,
src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc,
src/ltlvisit/tostring.cc, src/ltlvisit/tunabbrev.cc,
src/tgba/formula2bdd.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/ltl2tgba_lacim.cc: Handle finish in switches.
* src/tgbaalgos/eltl2tgba_lacim.cc: Translate finish.
* src/tgbatest/eltl2tgba.test: More tests.
This commit is contained in:
Damien Lefortier 2009-06-05 01:17:19 +02:00
parent 4de885afb1
commit e48338e8d8
23 changed files with 479 additions and 237 deletions
Download patch file Download diff file Expand all files Collapse all files

22
ChangeLog
View file

@ -1,3 +1,25 @@
2009-06-05 Damien Lefortier <dam@lrde.epita.fr>
Modify the ELTL parser to be able to support PSL operators. Add a
new keyword in the ELTL format: finish, which applies to an
automaton operator and tells whether it just completed.
* src/eltlparse/eltlparse.yy: Clean it. Add finish.
* src/eltlparse/eltlscan.ll: Add finish.
* src/formula_tree.cc, src/formula_tree.hh: New files. Define a
small AST representing formulae where atomic props are unknown
which is used in the ELTL parser.
* src/ltlast/automatop.cc, ltlast/automatop.hh, ltlast/nfa.cc,
ltlast/nfa.hh: Adjust.
* src/ltlast/unop.cc, src/ltlast/unop.hh: Finish is an unop.
* src/ltlvisit/basicreduce.cc, src/ltlvisit/nenoform.cc,
src/ltlvisit/reduce.cc, src/ltlvisit/syntimpl.cc,
src/ltlvisit/tostring.cc, src/ltlvisit/tunabbrev.cc,
src/tgba/formula2bdd.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/ltl2tgba_lacim.cc: Handle finish in switches.
* src/tgbaalgos/eltl2tgba_lacim.cc: Translate finish.
* src/tgbatest/eltl2tgba.test: More tests.
2009-06-02 Alexandre Duret-Lutz <adl@lrde.epita.fr> 2009-06-02 Alexandre Duret-Lutz <adl@lrde.epita.fr>
* src/tgbatest/scc.test: Redirect stdout into file `stdout' * src/tgbatest/scc.test: Redirect stdout into file `stdout'

333
src/eltlparse/eltlparse.yy
View file

@ -36,53 +36,22 @@
#include <boost/shared_ptr.hpp> #include <boost/shared_ptr.hpp>
#include "public.hh" #include "public.hh"
#include "ltlast/allnodes.hh" #include "ltlast/allnodes.hh"
#include "ltlast/formula_tree.hh"
#include "ltlvisit/destroy.hh" #include "ltlvisit/destroy.hh"
#include "ltlvisit/clone.hh"
namespace spot namespace spot
{ {
namespace eltl namespace eltl
{ {
typedef std::map<std::string, nfa::ptr> nfamap;
/// The following parser allows one to define aliases of automaton /// The following parser allows one to define aliases of automaton
/// operators such as: F=U(true,$0). Internally it's handled by /// operators such as: F=U(true,$0). Internally it's handled by
/// creating a small AST associated with each alias in order to /// creating a small AST associated with each alias in order to
/// instanciate the right automatop after: U(constant(1), AP(f)) /// instanciate the right automatop after: U(constant(1), AP(f))
/// for the formula F(f). /// for the formula F(f).
/// typedef std::map<std::string, formula_tree::node_ptr> aliasmap;
struct alias
{
virtual ~alias() {};
};
/// We use boost::shared_ptr to easily handle deletion.
typedef boost::shared_ptr<alias> alias_ptr;
struct alias_not : alias
{
alias_ptr child;
};
struct alias_binop : alias
{
binop::type op;
alias_ptr lhs;
alias_ptr rhs;
};
struct alias_multop : alias
{
multop::type op;
alias_ptr lhs;
alias_ptr rhs;
};
struct alias_nfa : alias
{
std::vector<alias_ptr> children;
spot::ltl::nfa::ptr nfa;
};
struct alias_arg : alias
{
int i;
};
typedef std::map<std::string, nfa::ptr> nfamap;
typedef std::map<std::string, alias_ptr> aliasmap;
/// Implementation details for error handling. /// Implementation details for error handling.
struct parse_error_list_t struct parse_error_list_t
@ -91,104 +60,51 @@ namespace spot
std::string file_; std::string file_;
}; };
/// TODO: maybe implementing a visitor could be better than using namespace spot::ltl::formula_tree;
/// dynamic casting all the time here.
/// Instanciate the formula corresponding to the given alias.
static formula*
alias2formula(const alias_ptr ap, spot::ltl::automatop::vec* v)
{
if (alias_not* a = dynamic_cast<alias_not*>(ap.get()))
return unop::instance(unop::Not, alias2formula(a->child, v));
if (alias_arg* a = dynamic_cast<alias_arg*>(ap.get()))
return a->i == -1 ? constant::true_instance() :
a->i == -2 ? constant::false_instance() : v->at(a->i);
if (alias_nfa* a = dynamic_cast<alias_nfa*>(ap.get()))
{
automatop::vec* va = new automatop::vec;
std::vector<alias_ptr>::const_iterator i = a->children.begin();
while (i != a->children.end())
va->push_back(alias2formula(*i++, v));
return automatop::instance(a->nfa, va, false);
}
if (alias_binop* a = dynamic_cast<alias_binop*>(ap.get()))
return binop::instance(a->op,
alias2formula(a->lhs, v),
alias2formula(a->rhs, v));
if (alias_multop* a = dynamic_cast<alias_multop*>(ap.get()))
return multop::instance(a->op,
alias2formula(a->lhs, v),
alias2formula(a->rhs, v));
/* Unreachable code. */
assert(0);
}
/// Get the arity of a given alias.
static size_t
arity(const alias_ptr ap)
{
if (alias_not* a = dynamic_cast<alias_not*>(ap.get()))
return arity(a->child);
if (alias_arg* a = dynamic_cast<alias_arg*>(ap.get()))
return std::max(a->i + 1, 0);
if (alias_nfa* a = dynamic_cast<alias_nfa*>(ap.get()))
{
size_t res = 0;
std::vector<alias_ptr>::const_iterator i = a->children.begin();
while (i != a->children.end())
res = std::max(arity(*i++), res);
return res;
}
if (alias_binop* a = dynamic_cast<alias_binop*>(ap.get()))
return std::max(arity(a->lhs), arity(a->rhs));
if (alias_multop* a = dynamic_cast<alias_multop*>(ap.get()))
return std::max(arity(a->lhs), arity(a->rhs));
/* Unreachable code. */
assert(0);
}
/// Alias an existing alias, as in Strong=G(F($0))->G(F($1)), /// Alias an existing alias, as in Strong=G(F($0))->G(F($1)),
/// where F is an alias. /// where F is an alias.
/// ///
/// \param ap The original alias. /// \param ap The original alias.
/// \param v The arguments of the new alias. /// \param v The arguments of the new alias.
static alias_ptr static node_ptr
realias(const alias_ptr ap, std::vector<alias_ptr> v) realias(const node_ptr ap, std::vector<node_ptr> v)
{ {
if (alias_not* a = dynamic_cast<alias_not*>(ap.get())) if (node_atomic* a = dynamic_cast<node_atomic*>(ap.get())) // Do it.
{
alias_not* res = new alias_not;
res->child = realias(a->child, v);
return alias_ptr(res);
}
if (alias_arg* a = dynamic_cast<alias_arg*>(ap.get())) // Do it.
return a->i < 0 ? ap : v.at(a->i); return a->i < 0 ? ap : v.at(a->i);
if (alias_nfa* a = dynamic_cast<alias_nfa*>(ap.get()))
// Traverse the tree.
if (node_unop* a = dynamic_cast<node_unop*>(ap.get()))
{ {
alias_nfa* res = new alias_nfa; node_unop* res = new node_unop;
std::vector<alias_ptr>::const_iterator i = a->children.begin(); res->op = a->op;
res->child = realias(a->child, v);
return node_ptr(res);
}
if (node_nfa* a = dynamic_cast<node_nfa*>(ap.get()))
{
node_nfa* res = new node_nfa;
std::vector<node_ptr>::const_iterator i = a->children.begin();
while (i != a->children.end()) while (i != a->children.end())
res->children.push_back(realias(*i++, v)); res->children.push_back(realias(*i++, v));
res->nfa = a->nfa; res->nfa = a->nfa;
return alias_ptr(res); return node_ptr(res);
} }
if (alias_binop* a = dynamic_cast<alias_binop*>(ap.get())) if (node_binop* a = dynamic_cast<node_binop*>(ap.get()))
{ {
alias_binop* res = new alias_binop; node_binop* res = new node_binop;
res->op = a->op; res->op = a->op;
res->lhs = realias(a->lhs, v); res->lhs = realias(a->lhs, v);
res->rhs = realias(a->rhs, v); res->rhs = realias(a->rhs, v);
return alias_ptr(res); return node_ptr(res);
} }
if (alias_multop* a = dynamic_cast<alias_multop*>(ap.get())) if (node_multop* a = dynamic_cast<node_multop*>(ap.get()))
{ {
alias_multop* res = new alias_multop; node_multop* res = new node_multop;
res->op = a->op; res->op = a->op;
res->lhs = realias(a->lhs, v); res->lhs = realias(a->lhs, v);
res->rhs = realias(a->rhs, v); res->rhs = realias(a->rhs, v);
return alias_ptr(res); return node_ptr(res);
} }
/* Unreachable code. */ /* Unreachable code. */
@ -235,6 +151,15 @@ namespace spot
} \ } \
} }
#define INSTANCIATE_OP(Name, TypeNode, TypeOp, L, R) \
{ \
TypeNode* res = new TypeNode; \
res->op = TypeOp; \
res->lhs = formula_tree::node_ptr(L); \
res->rhs = formula_tree::node_ptr(R); \
Name = res; \
}
} }
%parse-param {spot::eltl::nfamap& nmap} %parse-param {spot::eltl::nfamap& nmap}
@ -254,8 +179,8 @@ namespace spot
spot::ltl::formula* fval; spot::ltl::formula* fval;
/// To handle aliases. /// To handle aliases.
spot::eltl::alias* pval; spot::ltl::formula_tree::node* pval;
spot::eltl::alias_nfa* bval; spot::ltl::formula_tree::node_nfa* bval;
} }
%code { %code {
@ -283,6 +208,7 @@ using namespace spot::ltl;
%token ACC "accept" %token ACC "accept"
EQ "=" EQ "="
FIN "finish"
LPAREN "(" LPAREN "("
RPAREN ")" RPAREN ")"
COMMA "," COMMA ","
@ -304,10 +230,8 @@ using namespace spot::ltl;
%type <nval> nfa_def %type <nval> nfa_def
%type <fval> subformula %type <fval> subformula
%type <aval> arg_list %type <aval> arg_list
%type <ival> nfa_arg %type <pval> nfa_arg
%type <pval> nfa_alias %type <bval> nfa_arg_list
%type <pval> nfa_alias_arg
%type <bval> nfa_alias_arg_list
%destructor { delete $$; } "atomic proposition" %destructor { delete $$; } "atomic proposition"
%destructor { spot::ltl::destroy($$); } subformula %destructor { spot::ltl::destroy($$); } subformula
@ -335,7 +259,7 @@ nfa: IDENT "=" "(" nfa_def ")"
nmap[*$1] = nfa::ptr($4); nmap[*$1] = nfa::ptr($4);
delete $1; delete $1;
} }
| IDENT "=" nfa_alias | IDENT "=" nfa_arg
{ {
/// Recursivity issues of aliases are handled by a parse error. /// Recursivity issues of aliases are handled by a parse error.
aliasmap::iterator i = amap.find(*$1); aliasmap::iterator i = amap.find(*$1);
@ -348,7 +272,7 @@ nfa: IDENT "=" "(" nfa_def ")"
delete $1; delete $1;
YYERROR; YYERROR;
} }
amap[*$1] = alias_ptr($3); amap.insert(make_pair(*$1, formula_tree::node_ptr($3)));
delete $1; delete $1;
} }
; ;
@ -359,7 +283,7 @@ nfa_def: /* empty */
} }
| nfa_def STATE STATE nfa_arg | nfa_def STATE STATE nfa_arg
{ {
$1->add_transition($2, $3, $4); $1->add_transition($2, $3, formula_tree::node_ptr($4));
$$ = $1; $$ = $1;
} }
| nfa_def ACC STATE | nfa_def ACC STATE
@ -369,21 +293,94 @@ nfa_def: /* empty */
} }
; ;
nfa_alias: IDENT "(" nfa_alias_arg_list ")" nfa_arg_list: nfa_arg
{
$$ = new formula_tree::node_nfa;
$$->children.push_back(formula_tree::node_ptr($1));
}
| nfa_arg_list "," nfa_arg
{
$1->children.push_back(formula_tree::node_ptr($3));
$$ = $1;
}
;
nfa_arg: ARG
{
if ($1 == -1)
{
std::string s = "out of range integer";
PARSE_ERROR(@1, s);
YYERROR;
}
formula_tree::node_atomic* res = new formula_tree::node_atomic;
res->i = $1;
$$ = res;
}
| CONST_TRUE
{
formula_tree::node_atomic* res = new formula_tree::node_atomic;
res->i = formula_tree::True;
$$ = res;
}
| CONST_FALSE
{
formula_tree::node_atomic* res = new formula_tree::node_atomic;
res->i = formula_tree::False;
$$ = res;
}
| OP_NOT nfa_arg
{
formula_tree::node_unop* res = new formula_tree::node_unop;
res->op = unop::Not;
res->child = formula_tree::node_ptr($2);
$$ = res;
}
| FIN "(" nfa_arg ")"
{
formula_tree::node_unop* res = new formula_tree::node_unop;
res->op = unop::Finish;
res->child = formula_tree::node_ptr($3);
$$ = res;
}
| nfa_arg OP_AND nfa_arg
{
INSTANCIATE_OP($$, formula_tree::node_multop, multop::And, $1, $3);
}
| nfa_arg OP_OR nfa_arg
{
INSTANCIATE_OP($$, formula_tree::node_multop, multop::Or, $1, $3);
}
| nfa_arg OP_XOR nfa_arg
{
INSTANCIATE_OP($$, formula_tree::node_binop, binop::Xor, $1, $3);
}
| nfa_arg OP_IMPLIES nfa_arg
{
INSTANCIATE_OP($$, formula_tree::node_binop, binop::Implies, $1, $3);
}
| nfa_arg OP_EQUIV nfa_arg
{
INSTANCIATE_OP($$, formula_tree::node_binop, binop::Equiv, $1, $3);
}
| IDENT "(" nfa_arg_list ")"
{ {
aliasmap::const_iterator i = amap.find(*$1); aliasmap::const_iterator i = amap.find(*$1);
if (i != amap.end()) if (i != amap.end())
{ {
CHECK_ARITY(@1, $1, $3->children.size(), arity(i->second)); int arity = formula_tree::arity(i->second);
CHECK_ARITY(@1, $1, $3->children.size(), arity);
// Hack to return the right type without screwing with the // Hack to return the right type without screwing with the
// boost::shared_ptr memory handling by using get for // boost::shared_ptr memory handling by using get for
// example. FIXME: Wait for the next version of boost and // example. FIXME: Wait for the next version of boost and
// modify the %union to handle alias_ptr. // modify the %union to handle formula_tree::node_ptr.
alias_not* tmp1 = new alias_not; formula_tree::node_unop* tmp1 = new formula_tree::node_unop;
tmp1->op = unop::Not;
tmp1->child = realias(i->second, $3->children); tmp1->child = realias(i->second, $3->children);
alias_not* tmp2 = new alias_not; formula_tree::node_unop* tmp2 = new formula_tree::node_unop;
tmp2->child = alias_ptr(tmp1); tmp2->op = unop::Not;
tmp2->child = formula_tree::node_ptr(tmp1);
$$ = tmp2; $$ = tmp2;
delete $3; delete $3;
} }
@ -398,73 +395,6 @@ nfa_alias: IDENT "(" nfa_alias_arg_list ")"
} }
delete $1; delete $1;
} }
| OP_NOT nfa_alias
{
alias_not* res = new alias_not;
res->child = alias_ptr($2);
$$ = res;
}
| nfa_alias OP_IMPLIES nfa_alias
{
alias_binop* res = new alias_binop;
res->op = binop::Implies;
res->lhs = alias_ptr($1);
res->rhs = alias_ptr($3);
$$ = res;
}
// More TBD here.
nfa_alias_arg: nfa_arg
{
alias_arg* res = new alias_arg;
res->i = $1;
$$ = res;
}
| CONST_FALSE
{
alias_arg* res = new alias_arg;
res->i = -2;
$$ = res;
}
| OP_NOT nfa_alias_arg
{
alias_not* res = new alias_not;
res->child = alias_ptr($2);
$$ = res;
}
// More TBD here.
nfa_alias_arg_list: nfa_alias_arg
{
$$ = new alias_nfa;
$$->children.push_back(alias_ptr($1));
}
| nfa_alias // Cannot factorize because <pval> != <bval>.
{
$$ = new alias_nfa;
$$->children.push_back(alias_ptr($1));
}
| nfa_alias_arg_list "," nfa_alias_arg
{
$1->children.push_back(alias_ptr($3));
$$ = $1;
}
;
nfa_arg: ARG
{
if ($1 == -1)
{
std::string s = "out of range integer";
PARSE_ERROR(@1, s);
YYERROR;
}
$$ = $1;
}
| CONST_TRUE
{ $$ = -1; }
;
/* Formulae. */ /* Formulae. */
@ -490,12 +420,11 @@ subformula: ATOMIC_PROP
aliasmap::iterator i = amap.find(*$2); aliasmap::iterator i = amap.find(*$2);
if (i != amap.end()) if (i != amap.end())
{ {
CHECK_ARITY(@1, $2, 2, arity(i->second)); CHECK_ARITY(@1, $2, 2, formula_tree::arity(i->second));
automatop::vec* v = new automatop::vec; automatop::vec v;
v->push_back($1); v.push_back($1);
v->push_back($3); v.push_back($3);
$$ = alias2formula(i->second, v); $$ = instanciate(i->second, v);
delete v;
} }
else else
{ {
@ -514,8 +443,8 @@ subformula: ATOMIC_PROP
aliasmap::iterator i = amap.find(*$1); aliasmap::iterator i = amap.find(*$1);
if (i != amap.end()) if (i != amap.end())
{ {
CHECK_ARITY(@1, $1, $3->size(), arity(i->second)); CHECK_ARITY(@1, $1, $3->size(), formula_tree::arity(i->second));
$$ = alias2formula(i->second, $3); $$ = instanciate(i->second, *$3);
delete $3; delete $3;
} }
else else

1
src/eltlparse/eltlscan.ll
View file

@ -101,6 +101,7 @@ eol \n|\r|\n\r|\r\n
<INITIAL>"=" return token::EQ; <INITIAL>"=" return token::EQ;
<IINTIAL>"accept" return token::ACC; <IINTIAL>"accept" return token::ACC;
<IINTIAL>"finish" return token::FIN;
<INITIAL>[tT][rR][uU][eE] { <INITIAL>[tT][rR][uU][eE] {
return token::CONST_TRUE; return token::CONST_TRUE;

2
src/ltlast/Makefile.am
View file

@ -31,6 +31,7 @@ ltlast_HEADERS = \
binop.hh \ binop.hh \
constant.hh \ constant.hh \
formula.hh \ formula.hh \
formula_tree.hh \
multop.hh \ multop.hh \
nfa.hh \ nfa.hh \
predecl.hh \ predecl.hh \
@ -45,6 +46,7 @@ libltlast_la_SOURCES = \
binop.cc \ binop.cc \
constant.cc \ constant.cc \
formula.cc \ formula.cc \
formula_tree.cc \
multop.cc \ multop.cc \
nfa.cc \ nfa.cc \
refformula.cc \ refformula.cc \

1
src/ltlast/automatop.cc
View file

@ -21,6 +21,7 @@
#include <iostream> #include <iostream>
#include "automatop.hh" #include "automatop.hh"
#include "nfa.hh"
#include "visitor.hh" #include "visitor.hh"
namespace spot namespace spot

4
src/ltlast/automatop.hh
View file

@ -88,11 +88,11 @@ namespace spot
typedef std::map<triplet, formula*, paircmp> map; typedef std::map<triplet, formula*, paircmp> map;
static map instances; static map instances;
automatop(const nfa::ptr nfa, vec* v, bool negated); automatop(const nfa::ptr, vec* v, bool negated);
virtual ~automatop(); virtual ~automatop();
private: private:
nfa::ptr nfa_; const nfa::ptr nfa_;
vec* children_; vec* children_;
bool negated_; bool negated_;
}; };

88
src/ltlast/formula_tree.cc Normal file
View file

@ -0,0 +1,88 @@
// Copyright (C) 2009 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 <cassert>
#include "formula_tree.hh"
#include "allnodes.hh"
#include "ltlvisit/clone.hh"
namespace spot
{
namespace ltl
{
namespace formula_tree
{
formula*
instanciate(const node_ptr np, const std::vector<formula*>& v)
{
if (node_atomic* n = dynamic_cast<node_atomic*>(np.get()))
return n->i == True ? constant::true_instance() :
n->i == False ? constant::false_instance() : clone(v.at(n->i));
if (node_unop* n = dynamic_cast<node_unop*>(np.get()))
return unop::instance(n->op, instanciate(n->child, v));
if (node_nfa* n = dynamic_cast<node_nfa*>(np.get()))
{
automatop::vec* va = new automatop::vec;
std::vector<node_ptr>::const_iterator i = n->children.begin();
while (i != n->children.end())
va->push_back(instanciate(*i++, v));
return automatop::instance(n->nfa, va, false);
}
if (node_binop* n = dynamic_cast<node_binop*>(np.get()))
return binop::instance(n->op,
instanciate(n->lhs, v),
instanciate(n->rhs, v));
if (node_multop* n = dynamic_cast<node_multop*>(np.get()))
return multop::instance(n->op,
instanciate(n->lhs, v),
instanciate(n->rhs, v));
/* Unreachable code. */
assert(0);
}
size_t
arity(const node_ptr np)
{
if (node_atomic* n = dynamic_cast<node_atomic*>(np.get()))
return std::max(n->i + 1, 0);
if (node_unop* n = dynamic_cast<node_unop*>(np.get()))
return arity(n->child);
if (node_nfa* n = dynamic_cast<node_nfa*>(np.get()))
{
size_t res = 0;
std::vector<node_ptr>::const_iterator i = n->children.begin();
while (i != n->children.end())
res = std::max(arity(*i++), res);
return res;
}
if (node_binop* n = dynamic_cast<node_binop*>(np.get()))
return std::max(arity(n->lhs), arity(n->rhs));
if (node_multop* n = dynamic_cast<node_multop*>(np.get()))
return std::max(arity(n->lhs), arity(n->rhs));
/* Unreachable code. */
assert(0);
}
}
}
}

88
src/ltlast/formula_tree.hh Normal file
View file

@ -0,0 +1,88 @@
// Copyright (C) 2009 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.
/// \file ltlast/formula_tree.hh
/// \brief Trees representing formulae where atomic propositions are unknown
#ifndef SPOT_LTLAST_FORMULA_TREE_HH
# define SPOT_LTLAST_FORMULA_TREE_HH
# include <vector>
# include <boost/shared_ptr.hpp>
# include "formula.hh"
# include "multop.hh"
# include "binop.hh"
# include "unop.hh"
# include "nfa.hh"
namespace spot
{
namespace ltl
{
/// Trees representing formulae where atomic propositions are unknown.
namespace formula_tree
{
struct node
{
virtual ~node() {};
};
/// We use boost::shared_ptr to easily handle deletion.
typedef boost::shared_ptr<node> node_ptr;
struct node_unop : node
{
unop::type op;
node_ptr child;
};
struct node_binop : node
{
binop::type op;
node_ptr lhs;
node_ptr rhs;
};
struct node_multop : node
{
multop::type op;
node_ptr lhs;
node_ptr rhs;
};
struct node_nfa : node
{
std::vector<node_ptr> children;
spot::ltl::nfa::ptr nfa;
};
/// Integer values for True and False used in node_atomic.
enum { True = -1, False = -2 };
struct node_atomic : node
{
int i;
};
/// Instanciate the formula corresponding to the node with
/// atomic propositions taken from \a v.
formula* instanciate(const node_ptr np, const std::vector<formula*>& v);
/// Get the arity.
size_t arity(const node_ptr np);
}
}
}
#endif // SPOT_LTLAST_FORMULA_TREE_HH_

10
src/ltlast/nfa.cc
View file

@ -21,6 +21,7 @@
#include <cassert> #include <cassert>
#include "nfa.hh" #include "nfa.hh"
#include "formula_tree.hh"
namespace spot namespace spot
{ {
@ -61,15 +62,16 @@ namespace spot
} }
void void
nfa::add_transition(int src, int dst, int label) nfa::add_transition(int src, int dst, const label lbl)
{ {
state* s = add_state(src); state* s = add_state(src);
nfa::transition* t = new transition; nfa::transition* t = new transition;
t->dst = add_state(dst); t->dst = add_state(dst);
t->label = label; t->lbl = lbl;
s->push_back(t); s->push_back(t);
if (label >= arity_) size_t arity = formula_tree::arity(formula_tree::node_ptr(lbl));
arity_ = label + 1; if (arity >= arity_)
arity_ = arity;
} }
void void

16
src/ltlast/nfa.hh
View file

@ -36,16 +36,24 @@ namespace spot
{ {
/// Forward declaration. See below. /// Forward declaration. See below.
class succ_iterator; class succ_iterator;
/// Forward declaration. NFA's labels are reprensented by nodes
/// which are defined in formula_tree.hh, included in nfa.cc.
namespace formula_tree
{
class node;
}
/// \brief Nondeterministic Finite Automata used by automata operators. /// \brief Nondeterministic Finite Automata used by automata operators.
/// ///
/// States & labels are represented by integers. /// States are represented by integers.
/// Labels are represented by formula_tree's nodes.
/// Currently, only one initial state is possible. /// Currently, only one initial state is possible.
class nfa class nfa
{ {
public: public:
struct transition; struct transition;
typedef std::list<transition*> state; typedef std::list<transition*> state;
typedef boost::shared_ptr<formula_tree::node> label;
/// Iterator over the successors of a state. /// Iterator over the successors of a state.
typedef succ_iterator iterator; typedef succ_iterator iterator;
typedef boost::shared_ptr<nfa> ptr; typedef boost::shared_ptr<nfa> ptr;
@ -53,14 +61,14 @@ namespace spot
/// Explicit transitions. /// Explicit transitions.
struct transition struct transition
{ {
int label; label lbl;
const state* dst; const state* dst;
}; };
nfa(); nfa();
~nfa(); ~nfa();
void add_transition(int src, int dst, int label); void add_transition(int src, int dst, const label lbl);
void set_init_state(int name); void set_init_state(int name);
void set_final(int name); void set_final(int name);
@ -101,7 +109,7 @@ namespace spot
is_map is_; is_map is_;
si_map si_; si_map si_;
int arity_; size_t arity_;
std::string name_; std::string name_;
state* init_; state* init_;

2
src/ltlast/unop.cc
View file

@ -88,6 +88,8 @@ namespace spot
return "F"; return "F";
case G: case G:
return "G"; return "G";
case Finish:
return "Finish";
} }
// Unreachable code. // Unreachable code.
assert(0); assert(0);

2
src/ltlast/unop.hh
View file

@ -37,7 +37,7 @@ namespace spot
class unop : public ref_formula class unop : public ref_formula
{ {
public: public:
enum type { Not, X, F, G }; enum type { Not, X, F, G, Finish }; // Finish is used in ELTL formulae.
/// Build an unary operator with operation \a op and /// Build an unary operator with operation \a op and
/// child \a child. /// child \a child.

4
src/ltlvisit/basicreduce.cc
View file

@ -223,6 +223,10 @@ namespace spot
result_ = unop::instance(unop::G, result_); result_ = unop::instance(unop::G, result_);
return; return;
case unop::Finish:
result_ = unop::instance(unop::Finish, result_);
return;
} }
/* Unreachable code. */ /* Unreachable code. */
assert(0); assert(0);

6
src/ltlvisit/nenoform.cc
View file

@ -102,6 +102,12 @@ namespace spot
result_ = unop::instance(negated_ ? unop::F : unop::G, result_ = unop::instance(negated_ ? unop::F : unop::G,
recurse(f)); recurse(f));
return; return;
case unop::Finish:
result_ = unop::instance(unop::Finish, recurse_(f, false));
if (negated_)
result_ = unop::instance(unop::Not, result_);
return;
} }
/* Unreachable code. */ /* Unreachable code. */
assert(0); assert(0);

4
src/ltlvisit/reduce.cc
View file

@ -97,6 +97,10 @@ namespace spot
|| !is_universal(result_)) || !is_universal(result_))
result_ = unop::instance(unop::G, result_); result_ = unop::instance(unop::G, result_);
return; return;
case unop::Finish:
result_ = unop::instance(unop::Finish, result_);
return;
} }
/* Unreachable code. */ /* Unreachable code. */
assert(0); assert(0);

4
src/ltlvisit/syntimpl.cc
View file

@ -241,6 +241,8 @@ namespace spot
if (syntactic_implication(f, constant::false_instance())) if (syntactic_implication(f, constant::false_instance()))
result_ = true; result_ = true;
return; return;
case unop::Finish:
return;
} }
/* Unreachable code. */ /* Unreachable code. */
assert(0); assert(0);
@ -431,6 +433,8 @@ namespace spot
destroy(tmp); destroy(tmp);
return; return;
} }
case unop::Finish:
return;
} }
/* Unreachable code. */ /* Unreachable code. */
assert(0); assert(0);

8
src/ltlvisit/tostring.cc
View file

@ -144,6 +144,10 @@ namespace spot
case unop::G: case unop::G:
os_ << "G"; os_ << "G";
break; break;
case unop::Finish:
os_ << "finish";
need_parent = true;
break;
} }
top_level_ = false; top_level_ = false;
@ -297,6 +301,10 @@ namespace spot
case unop::G: case unop::G:
os_ << "[]"; os_ << "[]";
break; break;
case unop::Finish:
os_ << "finish";
need_parent = true;
break;
} }
top_level_ = false; top_level_ = false;

1
src/ltlvisit/tunabbrev.cc
View file

@ -39,6 +39,7 @@ namespace spot
{ {
switch (uo->op()) switch (uo->op())
{ {
case unop::Finish:
case unop::X: case unop::X:
case unop::Not: case unop::Not:
this->super::visit(uo); this->super::visit(uo);

1
src/tgba/formula2bdd.cc
View file

@ -72,6 +72,7 @@ namespace spot
{ {
switch (node->op()) switch (node->op())
{ {
case unop::Finish:
case unop::F: case unop::F:
case unop::G: case unop::G:
case unop::X: case unop::X:

45
src/tgbaalgos/eltl2tgba_lacim.cc
View file

@ -21,6 +21,7 @@
#include "ltlast/visitor.hh" #include "ltlast/visitor.hh"
#include "ltlast/allnodes.hh" #include "ltlast/allnodes.hh"
#include "ltlast/formula_tree.hh"
#include "ltlvisit/lunabbrev.hh" #include "ltlvisit/lunabbrev.hh"
#include "ltlvisit/nenoform.hh" #include "ltlvisit/nenoform.hh"
#include "ltlvisit/destroy.hh" #include "ltlvisit/destroy.hh"
@ -40,7 +41,7 @@ namespace spot
{ {
public: public:
eltl_trad_visitor(tgba_bdd_concrete_factory& fact, bool root = false) eltl_trad_visitor(tgba_bdd_concrete_factory& fact, bool root = false)
: fact_(fact), root_(root) : fact_(fact), root_(root), finish_()
{ {
} }
@ -87,6 +88,18 @@ namespace spot
res_ = bdd_not(recurse(node->child())); res_ = bdd_not(recurse(node->child()));
return; return;
} }
case unop::Finish:
{
// Ensure finish_[node->child()] has been computed if
// node->child() is an automaton operator.
bdd f = recurse(node->child());
finish_map_::const_iterator it = finish_.find(node->child());
if (it == finish_.end())
res_ = f;
else
res_ = finish_[node->child()];
return;
}
case unop::X: case unop::X:
case unop::F: case unop::F:
case unop::G: case unop::G:
@ -152,9 +165,20 @@ namespace spot
visit(const automatop* node) visit(const automatop* node)
{ {
nmap m; nmap m;
bdd finish = bddfalse;
bdd acc = bddtrue; bdd acc = bddtrue;
std::vector<formula*> v;
for (unsigned i = 0; i < node->size(); ++i)
v.push_back(const_cast<formula*>(node->nth(i)));
std::pair<int, int> vp = std::pair<int, int> vp =
recurse_state(node, node->nfa()->get_init_state(), m, acc); recurse_state(node->nfa(),
node->nfa()->get_init_state(), v, m, acc, finish);
// Update finish_ with finish(node).
// FIXME: when node is loop, it does not make sense; hence the bddtrue.
finish_[node] = !node->nfa()->is_loop() ? bddtrue : finish;
bdd tmp = bddtrue; bdd tmp = bddtrue;
for (nmap::iterator it = m.begin(); it != m.end(); ++it) for (nmap::iterator it = m.begin(); it != m.end(); ++it)
@ -180,15 +204,22 @@ namespace spot
tgba_bdd_concrete_factory& fact_; tgba_bdd_concrete_factory& fact_;
bool root_; bool root_;
/// BDD associated to each automatop A representing finish(A).
typedef Sgi::hash_map<const ltl::formula*, bdd,
ltl::formula_ptr_hash> finish_map_;
finish_map_ finish_;
// Table containing the two now variables associated with each state. // Table containing the two now variables associated with each state.
// TODO: a little documentation about that. // TODO: a little documentation about that.
typedef Sgi::hash_map< typedef Sgi::hash_map<
const nfa::state*, std::pair<int, int>, ptr_hash<nfa::state> > nmap; const nfa::state*, std::pair<int, int>, ptr_hash<nfa::state> > nmap;
std::pair<int, int>& std::pair<int, int>&
recurse_state(const automatop* n, const nfa::state* s, nmap& m, bdd& acc) recurse_state(const nfa::ptr& nfa, const nfa::state* s,
const std::vector<formula*>& v,
nmap& m, bdd& acc, bdd& finish)
{ {
const nfa::ptr nfa = n->nfa();
bool is_loop = nfa->is_loop(); bool is_loop = nfa->is_loop();
nmap::iterator it; nmap::iterator it;
it = m.find(s); it = m.find(s);
@ -209,16 +240,18 @@ namespace spot
bdd tmpacc = bddfalse; bdd tmpacc = bddfalse;
for (nfa::iterator i = nfa->begin(s); i != nfa->end(s); ++i) for (nfa::iterator i = nfa->begin(s); i != nfa->end(s); ++i)
{ {
bdd f = (*i)->label == -1 ? bddtrue : recurse(n->nth((*i)->label)); bdd f = recurse(formula_tree::instanciate((*i)->lbl, v));
if (nfa->is_final((*i)->dst)) if (nfa->is_final((*i)->dst))
{ {
tmp1 |= f; tmp1 |= f;
tmp2 |= f; tmp2 |= f;
tmpacc |= f; tmpacc |= f;
finish |= bdd_ithvar(v1) & f;
} }
else else
{ {
std::pair<int, int> vp = recurse_state(n, (*i)->dst, m, acc); std::pair<int, int> vp =
recurse_state(nfa, (*i)->dst, v, m, acc, finish);
tmp1 |= (f & bdd_ithvar(vp.first + 1)); tmp1 |= (f & bdd_ithvar(vp.first + 1));
tmp2 |= (f & bdd_ithvar(vp.second + 1)); tmp2 |= (f & bdd_ithvar(vp.second + 1));
if (is_loop) if (is_loop)

2
src/tgbaalgos/ltl2tgba_fm.cc
View file

@ -358,6 +358,8 @@ namespace spot
res_ = bdd_ithvar(x); res_ = bdd_ithvar(x);
return; return;
} }
case unop::Finish:
assert(!"unsupported operator");
} }
/* Unreachable code. */ /* Unreachable code. */
assert(0); assert(0);

2
src/tgbaalgos/ltl2tgba_lacim.cc
View file

@ -146,6 +146,8 @@ namespace spot
res_ = next; res_ = next;
return; return;
} }
case unop::Finish:
assert(!"unsupported operator");
} }
/* Unreachable code. */ /* Unreachable code. */
assert(0); assert(0);

34
src/tgbatest/eltl2tgba.test
View file

@ -145,3 +145,37 @@ T(f)
EOF EOF
check_construct input check_construct input
cat >input <<EOF
include input1
Fusion=
(
0 1 \$0 & !finish(\$0)
1 1 !finish(\$0)
1 2 \$1 & finish(\$0)
0 2 \$0 & \$1 & finish(\$0)
accept 2
)
%
Fusion(F(a),b)
EOF
check_construct input
cat >input <<EOF
Concat=
(
0 1 \$0 & !finish(\$0)
1 1 !finish(\$0)
1 2 finish(\$0)
0 2 \$0 & finish(\$0)
2 3 \$1
accept 3
)
%
Concat(a,b)
EOF
check_construct input
check_true 'a&X(b)'
check_false '!(a&X(b))'