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

* src/ltlast/formulae.hh: Rename as ...

Browse source 
* src/ltlast/formula.hh: ... this.
* src/ltlast/Makefile.am (libltlast_a_SOURCES): Adjust.
* src/ltlast/formula.hh (formulae): Rename as ...
(formula): ... this.
Adjust all uses.
This commit is contained in:
Alexandre Duret-Lutz 2003-04-16 13:11:34 +00:00
parent 532f9131f5
commit ef2d6323e0
22 changed files with 104 additions and 97 deletions
Download patch file Download diff file Expand all files Collapse all files

9
ChangeLog
View file

@ -1,4 +1,11 @@
2003-04-16 Alexandre DURET-LUTZ <aduret@circe.lip6.fr> 2003-04-16 Alexandre DURET-LUTZ <aduret@src.lip6.fr>
* src/ltlast/formulae.hh: Rename as ...
* src/ltlast/formula.hh: ... this.
* src/ltlast/Makefile.am (libltlast_a_SOURCES): Adjust.
* src/ltlast/formula.hh (formulae): Rename as ...
(formula): ... this.
Adjust all uses.
* src/ltlparse/public.hh (format_parse_errors): New function. * src/ltlparse/public.hh (format_parse_errors): New function.
* src/ltlparse/fmterror.cc: New file. * src/ltlparse/fmterror.cc: New file.

2
src/ltlast/Makefile.am
View file

@ -10,7 +10,7 @@ libltlast_a_SOURCES = \
binop.hh \ binop.hh \
constant.cc \ constant.cc \
constant.hh \ constant.hh \
formulae.hh \ formula.hh \
multop.cc \ multop.cc \
multop.hh \ multop.hh \
predecl.hh \ predecl.hh \

4
src/ltlast/atomic_prop.hh
View file

@ -2,14 +2,14 @@
# define SPOT_LTLAST_ATOMIC_PROP_HH # define SPOT_LTLAST_ATOMIC_PROP_HH
#include <string> #include <string>
#include "formulae.hh" #include "formula.hh"
namespace spot namespace spot
{ {
namespace ltl namespace ltl
{ {
class atomic_prop : public formulae class atomic_prop : public formula
{ {
public: public:
atomic_prop(std::string name); atomic_prop(std::string name);

10
src/ltlast/binop.cc
View file

@ -6,7 +6,7 @@ namespace spot
{ {
namespace ltl namespace ltl
{ {
binop::binop(type op, formulae* first, formulae* second) binop::binop(type op, formula* first, formula* second)
: op_(op), first_(first), second_(second) : op_(op), first_(first), second_(second)
{ {
} }
@ -27,25 +27,25 @@ namespace spot
v.visit(this); v.visit(this);
} }
const formulae* const formula*
binop::first() const binop::first() const
{ {
return first_; return first_;
} }
formulae* formula*
binop::first() binop::first()
{ {
return first_; return first_;
} }
const formulae* const formula*
binop::second() const binop::second() const
{ {
return second_; return second_;
} }
formulae* formula*
binop::second() binop::second()
{ {
return second_; return second_;

18
src/ltlast/binop.hh
View file

@ -1,38 +1,38 @@
#ifndef SPOT_LTLAST_BINOP_HH #ifndef SPOT_LTLAST_BINOP_HH
# define SPOT_LTLAST_BINOP_HH # define SPOT_LTLAST_BINOP_HH
#include "formulae.hh" #include "formula.hh"
namespace spot namespace spot
{ {
namespace ltl namespace ltl
{ {
class binop : public formulae class binop : public formula
{ {
public: public:
// And and Or are not here. Because they // And and Or are not here. Because they
// are often nested we represent them as multops. // are often nested we represent them as multops.
enum type { Xor, Implies, Equiv, U, R }; enum type { Xor, Implies, Equiv, U, R };
binop(type op, formulae* first, formulae* second); binop(type op, formula* first, formula* second);
virtual ~binop(); virtual ~binop();
virtual void accept(visitor& v); virtual void accept(visitor& v);
virtual void accept(const_visitor& v) const; virtual void accept(const_visitor& v) const;
const formulae* first() const; const formula* first() const;
formulae* first(); formula* first();
const formulae* second() const; const formula* second() const;
formulae* second(); formula* second();
type op() const; type op() const;
const char* op_name() const; const char* op_name() const;
private: private:
type op_; type op_;
formulae* first_; formula* first_;
formulae* second_; formula* second_;
}; };
} }

8
src/ltlast/constant.hh
View file

@ -1,14 +1,14 @@
#ifndef SPOT_LTLAST_CONSTANT_HH #ifndef SPOT_LTLAST_CONSTANT_HH
# define SPOT_LTLAST_CONSTANT_HH # define SPOT_LTLAST_CONSTANT_HH
#include "formulae.hh" #include "formula.hh"
namespace spot namespace spot
{ {
namespace ltl namespace ltl
{ {
class constant : public formulae class constant : public formula
{ {
public: public:
enum type { False, True }; enum type { False, True };
@ -19,8 +19,8 @@ namespace spot
virtual void accept(visitor& v); virtual void accept(visitor& v);
virtual void accept(const_visitor& v) const; virtual void accept(const_visitor& v) const;
const formulae* child() const; const formula* child() const;
formulae* child(); formula* child();
type val() const; type val() const;
const char* val_name() const; const char* val_name() const;

2
src/ltlast/formulae.hh → src/ltlast/formula.hh
View file

@ -8,7 +8,7 @@ namespace spot
namespace ltl namespace ltl
{ {
class formulae class formula
{ {
public: public:
virtual void accept(visitor& v) = 0; virtual void accept(visitor& v) = 0;

12
src/ltlast/multop.cc
View file

@ -7,7 +7,7 @@ namespace spot
{ {
namespace ltl namespace ltl
{ {
multop::multop(type op, formulae* first, formulae* second) multop::multop(type op, formula* first, formula* second)
: op_(op) : op_(op)
{ {
children_.reserve(2); children_.reserve(2);
@ -16,9 +16,9 @@ namespace spot
} }
void void
multop::add(formulae* f) multop::add(formula* f)
{ {
// If the formulae we add is itself a multop for the same operator, // If the formula we add is itself a multop for the same operator,
// merge its children with ours. // merge its children with ours.
multop* p = dynamic_cast<multop*>(f); multop* p = dynamic_cast<multop*>(f);
if (p && p->op() == op()) if (p && p->op() == op())
@ -26,7 +26,7 @@ namespace spot
unsigned ps = p->size(); unsigned ps = p->size();
for (unsigned i = 0; i < ps; ++i) for (unsigned i = 0; i < ps; ++i)
children_.push_back(p->nth(i)); children_.push_back(p->nth(i));
// that sub-formulae is now useless // that sub-formula is now useless
delete f; delete f;
} }
else else
@ -57,13 +57,13 @@ namespace spot
return children_.size(); return children_.size();
} }
const formulae* const formula*
multop::nth(unsigned n) const multop::nth(unsigned n) const
{ {
return children_[n]; return children_[n];
} }
formulae* formula*
multop::nth(unsigned n) multop::nth(unsigned n)
{ {
return children_[n]; return children_[n];

14
src/ltlast/multop.hh
View file

@ -2,22 +2,22 @@
# define SPOT_LTLAST_MULTOP_HH # define SPOT_LTLAST_MULTOP_HH
#include <vector> #include <vector>
#include "formulae.hh" #include "formula.hh"
namespace spot namespace spot
{ {
namespace ltl namespace ltl
{ {
class multop : public formulae class multop : public formula
{ {
public: public:
enum type { Or, And }; enum type { Or, And };
// A multop has at least two arguments. // A multop has at least two arguments.
multop(type op, formulae* first, formulae* second); multop(type op, formula* first, formula* second);
// More argument can be added. // More argument can be added.
void add(formulae* f); void add(formula* f);
virtual ~multop(); virtual ~multop();
@ -25,15 +25,15 @@ namespace spot
virtual void accept(const_visitor& v) const; virtual void accept(const_visitor& v) const;
unsigned size() const; unsigned size() const;
const formulae* nth(unsigned n) const; const formula* nth(unsigned n) const;
formulae* nth(unsigned n); formula* nth(unsigned n);
type op() const; type op() const;
const char* op_name() const; const char* op_name() const;
private: private:
type op_; type op_;
std::vector<formulae*> children_; std::vector<formula*> children_;
}; };
} }

2
src/ltlast/predecl.hh
View file

@ -10,7 +10,7 @@ namespace spot {
struct unop; struct unop;
struct constant; struct constant;
struct binop; struct binop;
struct formulae; struct formula;
struct multop; struct multop;
} }
} }

6
src/ltlast/unop.cc
View file

@ -6,7 +6,7 @@ namespace spot
{ {
namespace ltl namespace ltl
{ {
unop::unop(type op, formulae* child) unop::unop(type op, formula* child)
: op_(op), child_(child) : op_(op), child_(child)
{ {
} }
@ -27,13 +27,13 @@ namespace spot
v.visit(this); v.visit(this);
} }
const formulae* const formula*
unop::child() const unop::child() const
{ {
return child_; return child_;
} }
formulae* formula*
unop::child() unop::child()
{ {
return child_; return child_;

12
src/ltlast/unop.hh
View file

@ -1,33 +1,33 @@
#ifndef SPOT_LTLAST_UNOP_HH #ifndef SPOT_LTLAST_UNOP_HH
# define SPOT_LTLAST_UNOP_HH # define SPOT_LTLAST_UNOP_HH
#include "formulae.hh" #include "formula.hh"
namespace spot namespace spot
{ {
namespace ltl namespace ltl
{ {
class unop : public formulae class unop : public formula
{ {
public: public:
enum type { Not, X, F, G }; enum type { Not, X, F, G };
unop(type op, formulae* child); unop(type op, formula* child);
virtual ~unop(); virtual ~unop();
virtual void accept(visitor& v); virtual void accept(visitor& v);
virtual void accept(const_visitor& v) const; virtual void accept(const_visitor& v) const;
const formulae* child() const; const formula* child() const;
formulae* child(); formula* child();
type op() const; type op() const;
const char* op_name() const; const char* op_name() const;
private: private:
type op_; type op_;
formulae* child_; formula* child_;
}; };
} }

48
src/ltlparse/ltlparse.yy
View file

@ -3,7 +3,7 @@
#include "public.hh" #include "public.hh"
#include "ltlast/allnodes.hh" #include "ltlast/allnodes.hh"
extern spot::ltl::formulae* result; extern spot::ltl::formula* result;
%} %}
@ -13,7 +13,7 @@ extern spot::ltl::formulae* result;
{ {
int token; int token;
std::string* str; std::string* str;
spot::ltl::formulae* ltl; spot::ltl::formula* ltl;
} }
%{ %{
@ -58,10 +58,10 @@ namespace spot
%token CONST_FALSE %token CONST_FALSE
%token END_OF_INPUT %token END_OF_INPUT
%type <ltl> result ltl_formulae subformulae %type <ltl> result ltl_formula subformula
%% %%
result: ltl_formulae END_OF_INPUT result: ltl_formula END_OF_INPUT
{ result = $$ = $1; { result = $$ = $1;
YYACCEPT; YYACCEPT;
} }
@ -82,57 +82,57 @@ many_errors_diagnosed : many_errors
{ error_list->push_back(parse_error(@1, { error_list->push_back(parse_error(@1,
"unexpected input ignored")); } "unexpected input ignored")); }
ltl_formulae: subformulae ltl_formula: subformula
{ $$ = $1; } { $$ = $1; }
| many_errors_diagnosed subformulae | many_errors_diagnosed subformula
{ $$ = $2; } { $$ = $2; }
| ltl_formulae many_errors_diagnosed | ltl_formula many_errors_diagnosed
{ $$ = $1; } { $$ = $1; }
many_errors: error many_errors: error
| many_errors error | many_errors error
subformulae: ATOMIC_PROP subformula: ATOMIC_PROP
{ $$ = new atomic_prop(*$1); delete $1; } { $$ = new atomic_prop(*$1); delete $1; }
| CONST_TRUE | CONST_TRUE
{ $$ = new constant(constant::True); } { $$ = new constant(constant::True); }
| CONST_FALSE | CONST_FALSE
{ $$ = new constant(constant::False); } { $$ = new constant(constant::False); }
| PAR_OPEN subformulae PAR_CLOSE | PAR_OPEN subformula PAR_CLOSE
{ $$ = $2; } { $$ = $2; }
| PAR_OPEN error PAR_CLOSE | PAR_OPEN error PAR_CLOSE
{ error_list->push_back(parse_error(@$, { error_list->push_back(parse_error(@$,
"treating this parenthetical block as false")); "treating this parenthetical block as false"));
$$ = new constant(constant::False); $$ = new constant(constant::False);
} }
| PAR_OPEN subformulae many_errors PAR_CLOSE | PAR_OPEN subformula many_errors PAR_CLOSE
{ error_list->push_back(parse_error(@3, { error_list->push_back(parse_error(@3,
"unexpected input ignored")); "unexpected input ignored"));
$$ = $2; $$ = $2;
} }
| OP_NOT subformulae | OP_NOT subformula
{ $$ = new unop(unop::Not, $2); } { $$ = new unop(unop::Not, $2); }
| subformulae OP_AND subformulae | subformula OP_AND subformula
{ $$ = new multop(multop::And, $1, $3); } { $$ = new multop(multop::And, $1, $3); }
| subformulae OP_OR subformulae | subformula OP_OR subformula
{ $$ = new multop(multop::Or, $1, $3); } { $$ = new multop(multop::Or, $1, $3); }
| subformulae OP_XOR subformulae | subformula OP_XOR subformula
{ $$ = new binop(binop::Xor, $1, $3); } { $$ = new binop(binop::Xor, $1, $3); }
| subformulae OP_IMPLIES subformulae | subformula OP_IMPLIES subformula
{ $$ = new binop(binop::Implies, $1, $3); } { $$ = new binop(binop::Implies, $1, $3); }
| subformulae OP_EQUIV subformulae | subformula OP_EQUIV subformula
{ $$ = new binop(binop::Equiv, $1, $3); } { $$ = new binop(binop::Equiv, $1, $3); }
| subformulae OP_U subformulae | subformula OP_U subformula
{ $$ = new binop(binop::U, $1, $3); } { $$ = new binop(binop::U, $1, $3); }
| subformulae OP_R subformulae | subformula OP_R subformula
{ $$ = new binop(binop::R, $1, $3); } { $$ = new binop(binop::R, $1, $3); }
| OP_F subformulae | OP_F subformula
{ $$ = new unop(unop::F, $2); } { $$ = new unop(unop::F, $2); }
| OP_G subformulae | OP_G subformula
{ $$ = new unop(unop::G, $2); } { $$ = new unop(unop::G, $2); }
| OP_X subformulae | OP_X subformula
{ $$ = new unop(unop::X, $2); } { $$ = new unop(unop::X, $2); }
// | subformulae many_errors // | subformula many_errors
// { error_list->push_back(parse_error(@2, // { error_list->push_back(parse_error(@2,
// "ignoring these unexpected trailing tokens")); // "ignoring these unexpected trailing tokens"));
// $$ = $1; // $$ = $1;
@ -155,7 +155,7 @@ yy::Parser::error_()
error_list->push_back(parse_error(location, message)); error_list->push_back(parse_error(location, message));
} }
formulae* result = 0; formula* result = 0;
namespace spot namespace spot
{ {
@ -163,7 +163,7 @@ namespace spot
{ {
parse_error_list* error_list; parse_error_list* error_list;
formulae* formula*
parse(const std::string& ltl_string, parse(const std::string& ltl_string,
parse_error_list& error_list, parse_error_list& error_list,
bool debug) bool debug)

4
src/ltlparse/public.hh
View file

@ -2,7 +2,7 @@
# define SPOT_LTLPARSE_PUBLIC_HH # define SPOT_LTLPARSE_PUBLIC_HH
# include <string> # include <string>
# include "ltlast/formulae.hh" # include "ltlast/formula.hh"
# include "location.hh" # include "location.hh"
# include <list> # include <list>
# include <utility> # include <utility>
@ -16,7 +16,7 @@ namespace spot
typedef std::list<parse_error> parse_error_list; typedef std::list<parse_error> parse_error_list;
// Beware: this function is *not* reentrant. // Beware: this function is *not* reentrant.
formulae* parse(const std::string& ltl_string, formula* parse(const std::string& ltl_string,
parse_error_list& error_list, parse_error_list& error_list,
bool debug = false); bool debug = false);

6
src/ltltest/equals.cc
View file

@ -5,7 +5,7 @@
void void
syntax(char *prog) syntax(char *prog)
{ {
std::cerr << prog << " formulae1 formulae2" << std::endl; std::cerr << prog << " formula1 formula2" << std::endl;
exit(2); exit(2);
} }
@ -17,13 +17,13 @@ main(int argc, char **argv)
spot::ltl::parse_error_list p1; spot::ltl::parse_error_list p1;
spot::ltl::formulae *f1 = spot::ltl::parse(argv[1], p1); spot::ltl::formula *f1 = spot::ltl::parse(argv[1], p1);
if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1)) if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1))
return 2; return 2;
spot::ltl::parse_error_list p2; spot::ltl::parse_error_list p2;
spot::ltl::formulae *f2 = spot::ltl::parse(argv[2], p2); spot::ltl::formula *f2 = spot::ltl::parse(argv[2], p2);
if (spot::ltl::format_parse_errors(std::cerr, argv[2], p2)) if (spot::ltl::format_parse_errors(std::cerr, argv[2], p2))
return 2; return 2;

10
src/ltltest/readltl.cc
View file

@ -6,7 +6,7 @@
void void
syntax(char *prog) syntax(char *prog)
{ {
std::cerr << prog << " [-d] formulae" << std::endl; std::cerr << prog << " [-d] formula" << std::endl;
exit(2); exit(2);
} }
@ -19,23 +19,23 @@ main(int argc, char **argv)
syntax(argv[0]); syntax(argv[0]);
bool debug = false; bool debug = false;
int formulae_index = 1; int formula_index = 1;
if (!strcmp(argv[1], "-d")) if (!strcmp(argv[1], "-d"))
{ {
debug = true; debug = true;
if (argc < 3) if (argc < 3)
syntax(argv[0]); syntax(argv[0]);
formulae_index = 2; formula_index = 2;
} }
spot::ltl::parse_error_list pel; spot::ltl::parse_error_list pel;
spot::ltl::formulae *f = spot::ltl::parse(argv[formulae_index], spot::ltl::formula *f = spot::ltl::parse(argv[formula_index],
pel, debug); pel, debug);
spot::ltl::parse_error_list::iterator it; spot::ltl::parse_error_list::iterator it;
exit_code = exit_code =
spot::ltl::format_parse_errors(std::cerr, argv[formulae_index], pel); spot::ltl::format_parse_errors(std::cerr, argv[formula_index], pel);
if (f) if (f)
{ {

2
src/ltlvisit/dotty.cc
View file

@ -95,7 +95,7 @@ namespace spot
}; };
void void
dotty(const formulae& f, std::ostream& os) dotty(const formula& f, std::ostream& os)
{ {
dotty_visitor v(os); dotty_visitor v(os);
os << "digraph G {" << std::endl; os << "digraph G {" << std::endl;

4
src/ltlvisit/dotty.hh
View file

@ -1,14 +1,14 @@
#ifndef SPOT_LTLVISIT_DOTTY_HH #ifndef SPOT_LTLVISIT_DOTTY_HH
# define SPOT_LTLVISIT_DOTTY_HH # define SPOT_LTLVISIT_DOTTY_HH
#include <ltlast/formulae.hh> #include <ltlast/formula.hh>
#include <iostream> #include <iostream>
namespace spot namespace spot
{ {
namespace ltl namespace ltl
{ {
void dotty(const formulae& f, std::ostream& os); void dotty(const formula& f, std::ostream& os);
} }
} }

2
src/ltlvisit/dump.cc
View file

@ -69,7 +69,7 @@ namespace spot
}; };
void void
dump(const formulae& f, std::ostream& os) dump(const formula& f, std::ostream& os)
{ {
dump_visitor v(os); dump_visitor v(os);
f.accept(v); f.accept(v);

4
src/ltlvisit/dump.hh
View file

@ -1,14 +1,14 @@
#ifndef SPOT_LTLVISIT_DUMP_HH #ifndef SPOT_LTLVISIT_DUMP_HH
# define SPOT_LTLVISIT_DUMP_HH # define SPOT_LTLVISIT_DUMP_HH
#include <ltlast/formulae.hh> #include <ltlast/formula.hh>
#include <iostream> #include <iostream>
namespace spot namespace spot
{ {
namespace ltl namespace ltl
{ {
void dump(const formulae& f, std::ostream& os); void dump(const formula& f, std::ostream& os);
} }
} }

12
src/ltlvisit/equals.cc
View file

@ -6,7 +6,7 @@ namespace spot
{ {
namespace ltl namespace ltl
{ {
equals_visitor::equals_visitor(const formulae* f) equals_visitor::equals_visitor(const formula* f)
: f_(f), result_(false) : f_(f), result_(false)
{ {
} }
@ -84,7 +84,7 @@ namespace spot
for (unsigned nf = 0; nf < m_size; ++nf) for (unsigned nf = 0; nf < m_size; ++nf)
{ {
unsigned np; unsigned np;
const formulae* mnth = m->nth(nf); const formula* mnth = m->nth(nf);
for (np = 0; np < p_size; ++np) for (np = 0; np < p_size; ++np)
{ {
if (equals(p->nth(np), mnth)) if (equals(p->nth(np), mnth))
@ -94,7 +94,7 @@ namespace spot
} }
} }
// We we haven't found mnth in any child of p, then // We we haven't found mnth in any child of p, then
// the two formulaes aren't equal. // the two formulas aren't equal.
if (np == p_size) if (np == p_size)
return; return;
} }
@ -114,7 +114,7 @@ namespace spot
// Compare with marked children. // Compare with marked children.
unsigned np2; unsigned np2;
const formulae *pnth = p->nth(np); const formula *pnth = p->nth(np);
for (np2 = 0; np2 < p_size; ++np2) for (np2 = 0; np2 < p_size; ++np2)
if (p_seen[np2] && equals(p->nth(np2), pnth)) if (p_seen[np2] && equals(p->nth(np2), pnth))
break; break;
@ -124,13 +124,13 @@ namespace spot
return; return;
} }
// The two formulaes match. // The two formulas match.
result_ = true; result_ = true;
} }
bool bool
equals(const formulae* f1, const formulae* f2) equals(const formula* f1, const formula* f2)
{ {
equals_visitor v(f1); equals_visitor v(f1);
f2->accept(v); f2->accept(v);

10
src/ltlvisit/equals.hh
View file

@ -1,4 +1,4 @@
#include "ltlast/formulae.hh" #include "ltlast/formula.hh"
#include "ltlast/visitor.hh" #include "ltlast/visitor.hh"
namespace spot namespace spot
@ -10,11 +10,11 @@ namespace spot
class equals_visitor : public const_visitor class equals_visitor : public const_visitor
{ {
public: public:
equals_visitor(const formulae* f); equals_visitor(const formula* f);
virtual ~equals_visitor(); virtual ~equals_visitor();
// Return true iff the visitor has visited a // Return true iff the visitor has visited a
// formulae which is equal to `f'. // formula which is equal to `f'.
bool result() const; bool result() const;
void visit(const atomic_prop* ap); void visit(const atomic_prop* ap);
@ -24,11 +24,11 @@ namespace spot
void visit(const constant* c); void visit(const constant* c);
private: private:
const formulae* f_; const formula* f_;
bool result_; bool result_;
}; };
bool equals(const formulae* f1, const formulae* f2); bool equals(const formula* f1, const formula* f2);
} }
} }