Use 'const formula*' instead of 'formula*' everywhere.

The distinction makes no sense since Spot 0.5, where we switched from
mutable furmulae to immutable formulae.  The difference between
const_visitor and visitor made no sense either.  They have been merged
into one: visitor.

* iface/dve2/dve2check.cc, iface/gspn/ltlgspn.cc,
src/eltlparse/eltlparse.yy, src/eltlparse/public.hh,
src/evtgbatest/ltl2evtgba.cc, src/kripkeparse/kripkeparse.yy,
src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
src/ltlast/automatop.cc, src/ltlast/automatop.hh, src/ltlast/binop.cc,
src/ltlast/binop.hh, src/ltlast/bunop.cc, src/ltlast/bunop.hh,
src/ltlast/constant.cc, src/ltlast/constant.hh, src/ltlast/formula.cc,
src/ltlast/formula.hh, src/ltlast/formula_tree.cc,
src/ltlast/formula_tree.hh, src/ltlast/multop.cc,
src/ltlast/multop.hh, src/ltlast/predecl.hh, src/ltlast/refformula.cc,
src/ltlast/refformula.hh, src/ltlast/unop.cc, src/ltlast/unop.hh,
src/ltlast/visitor.hh, src/ltlenv/declenv.cc, src/ltlenv/declenv.hh,
src/ltlenv/defaultenv.cc, src/ltlenv/defaultenv.hh,
src/ltlenv/environment.hh, src/ltlparse/ltlfile.cc,
src/ltlparse/ltlfile.hh, src/ltlparse/ltlparse.yy,
src/ltlparse/public.hh, src/ltltest/consterm.cc,
src/ltltest/equals.cc, src/ltltest/genltl.cc, src/ltltest/kind.cc,
src/ltltest/length.cc, src/ltltest/randltl.cc, src/ltltest/readltl.cc,
src/ltltest/reduc.cc, src/ltltest/syntimpl.cc,
src/ltltest/tostring.cc, src/ltlvisit/apcollect.cc,
src/ltlvisit/apcollect.hh, src/ltlvisit/clone.cc,
src/ltlvisit/clone.hh, src/ltlvisit/contain.cc,
src/ltlvisit/contain.hh, src/ltlvisit/dotty.cc,
src/ltlvisit/length.cc, src/ltlvisit/lunabbrev.cc,
src/ltlvisit/lunabbrev.hh, src/ltlvisit/mark.cc, src/ltlvisit/mark.hh,
src/ltlvisit/nenoform.cc, src/ltlvisit/nenoform.hh,
src/ltlvisit/postfix.cc, src/ltlvisit/postfix.hh,
src/ltlvisit/randomltl.cc, src/ltlvisit/randomltl.hh,
src/ltlvisit/reduce.cc, src/ltlvisit/reduce.hh,
src/ltlvisit/simpfg.cc, src/ltlvisit/simpfg.hh,
src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh,
src/ltlvisit/snf.cc, src/ltlvisit/snf.hh, src/ltlvisit/tostring.cc,
src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh,
src/ltlvisit/wmunabbrev.cc, src/ltlvisit/wmunabbrev.hh,
src/neverparse/neverclaimparse.yy, src/sabatest/sabacomplementtgba.cc,
src/tgba/bdddict.cc, src/tgba/formula2bdd.cc, src/tgba/taatgba.cc,
src/tgba/taatgba.hh, src/tgbaalgos/eltl2tgba_lacim.cc,
src/tgbaalgos/ltl2taa.cc, src/tgbaalgos/ltl2tgba_fm.cc,
src/tgbaalgos/ltl2tgba_lacim.cc, src/tgbaalgos/minimize.cc,
src/tgbaalgos/randomgraph.cc, src/tgbaparse/tgbaparse.yy,
src/tgbatest/complementation.cc, src/tgbatest/ltl2tgba.cc,
src/tgbatest/ltlprod.cc, src/tgbatest/mixprod.cc,
src/tgbatest/randtgba.cc: Massive adjustment!
* src/tgbatest/reductgba.cc: Delete.
This commit is contained in:
Alexandre Duret-Lutz 2012-05-01 23:38:55 +02:00
parent 0f0ada825a
commit bf62d439c9
98 changed files with 1318 additions and 1535 deletions

21
NEWS
View file

@ -6,10 +6,6 @@ New in spot 0.8.3a:
Expressions (SERE), and a couple of operators to bridge SERE and Expressions (SERE), and a couple of operators to bridge SERE and
LTL. See doc/tl/tl.pdf for the list of operators and their LTL. See doc/tl/tl.pdf for the list of operators and their
semantics. semantics.
- The constructors for temporal formulae will perform some trivial
simplifications based on associativity, commutativity,
idempotence, and neutral elements. See doc/tl/tl.pdf for the
list of such simplifications.
- Formula rewritings have been completely revamped, and augmented - Formula rewritings have been completely revamped, and augmented
with rules for PSL operators (and some new LTL rules as well). with rules for PSL operators (and some new LTL rules as well).
See doc/tl/tl.pdf for the list of the rewritings implemented. See doc/tl/tl.pdf for the list of the rewritings implemented.
@ -51,13 +47,24 @@ New in spot 0.8.3a:
* Interface changes: * Interface changes:
- Operators ->, <->, U, W, R, and M are now parsed as - Operators ->, <->, U, W, R, and M are now parsed as
right-associative to better match the PSL standard. right-associative to better match the PSL standard.
- The constructors for temporal formulae will perform some trivial
simplifications based on associativity, commutativity,
idempotence, and neutral elements. See doc/tl/tl.pdf for the
list of such simplifications.
- Formula instances now have many methods to inspect their
properties (membership to syntactic classes, absence of X
operator, etc...) in constant time.
- LTL/PSL formulae are now handled everywhere as 'const formula*'
and not just 'formula*'. This reflects the true nature of these
(immutable) formula objects, and cleanups a lot of code.
Unfortunately, it is a backward incompatible change: you may have
to add 'const' to a couple of lines in your code, and change
'ltl::const_vistitor' into 'ltl::visitor' if you have written a
custom visitor.
- The new entry point for LTL/PSL simplifications is the function - The new entry point for LTL/PSL simplifications is the function
ltl_simplifier::simplify() declared in src/ltlvisit/simplify.hh. ltl_simplifier::simplify() declared in src/ltlvisit/simplify.hh.
The ltl_simplifier class implements a cache. The ltl_simplifier class implements a cache.
Functions such as reduce() or reduce_tau03() are deprecated. Functions such as reduce() or reduce_tau03() are deprecated.
- Formula instances now have many methods to inspect their
properties (membership to syntactic classes, absence of X
operator, etc...) in constant time.
- The old game-theory-based implementations for direct and delayed - The old game-theory-based implementations for direct and delayed
simulation reductions have been removed. The old direct simulation reductions have been removed. The old direct
simulation would only work on degeneralized automata, and yet simulation would only work on degeneralized automata, and yet

View file

@ -1,4 +1,4 @@
// Copyright (C) 2011 Laboratoire de Recherche et Developpement de // Copyright (C) 2011, 2012 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE) // l'Epita (LRDE)
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -177,8 +177,8 @@ main(int argc, char **argv)
spot::tgba* product = 0; spot::tgba* product = 0;
spot::emptiness_check_instantiator* echeck_inst = 0; spot::emptiness_check_instantiator* echeck_inst = 0;
int exit_code = 0; int exit_code = 0;
spot::ltl::formula* f = 0; const spot::ltl::formula* f = 0;
spot::ltl::formula* deadf = 0; const spot::ltl::formula* deadf = 0;
if (dead == 0 || !strcasecmp(dead, "true")) if (dead == 0 || !strcasecmp(dead, "true"))
{ {
@ -222,7 +222,7 @@ main(int argc, char **argv)
{ {
spot::ltl::ltl_simplifier_options opt(true, true, true, true, true); spot::ltl::ltl_simplifier_options opt(true, true, true, true, true);
spot::ltl::ltl_simplifier simp(opt); spot::ltl::ltl_simplifier simp(opt);
spot::ltl::formula* r = simp.simplify(f); const spot::ltl::formula* r = simp.simplify(f);
f->destroy(); f->destroy();
f = r; f = r;
} }

View file

@ -1,6 +1,9 @@
// Copyright (C) 2003, 2004, 2006, 2007, 2008, 2009 Laboratoire // -*- coding: utf-8 -*-
// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis // Copyright (C) 2008, 2009, 2011, 2012 Laboratoire de Recherche et
// Coopératifs (SRC), Université Pierre et Marie Curie. // Developpement de l'Epita (LRDE)
// Copyright (C) 2003, 2004, 2006, 2007 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. // This file is part of Spot, a model checking library.
// //
@ -229,8 +232,8 @@ main(int argc, char **argv)
} }
spot::ltl::parse_error_list pel; spot::ltl::parse_error_list pel;
spot::ltl::formula* f = spot::ltl::parse(argv[formula_index + 1], const spot::ltl::formula* f =
pel, env); spot::ltl::parse(argv[formula_index + 1], pel, env);
if (spot::ltl::format_parse_errors(std::cerr, if (spot::ltl::format_parse_errors(std::cerr,
argv[formula_index + 1], pel)) argv[formula_index + 1], pel))

View file

@ -64,7 +64,7 @@ namespace spot
%parse-param {spot::eltl::aliasmap& amap} %parse-param {spot::eltl::aliasmap& amap}
%parse-param {spot::eltl::parse_error_list_t &pe} %parse-param {spot::eltl::parse_error_list_t &pe}
%parse-param {spot::ltl::environment &parse_environment} %parse-param {spot::ltl::environment &parse_environment}
%parse-param {spot::ltl::formula* &result} %parse-param {const spot::ltl::formula* &result}
%lex-param {spot::eltl::parse_error_list_t &pe} %lex-param {spot::eltl::parse_error_list_t &pe}
%expect 0 %expect 0
%pure-parser %pure-parser
@ -74,7 +74,7 @@ namespace spot
std::string* sval; std::string* sval;
spot::ltl::nfa* nval; spot::ltl::nfa* nval;
spot::ltl::automatop::vec* aval; spot::ltl::automatop::vec* aval;
spot::ltl::formula* fval; const spot::ltl::formula* fval;
/// To handle aliases. /// To handle aliases.
spot::ltl::formula_tree::node* pval; spot::ltl::formula_tree::node* pval;
@ -520,7 +520,7 @@ namespace spot
{ {
namespace eltl namespace eltl
{ {
formula* const formula*
parse_file(const std::string& name, parse_file(const std::string& name,
parse_error_list& error_list, parse_error_list& error_list,
environment& env, environment& env,
@ -533,7 +533,7 @@ namespace spot
spair("-", std::string("Cannot open file ") + name))); spair("-", std::string("Cannot open file ") + name)));
return 0; return 0;
} }
formula* result = 0; const formula* result = 0;
nfamap nmap; nfamap nmap;
aliasmap amap; aliasmap amap;
parse_error_list_t pe; parse_error_list_t pe;
@ -546,14 +546,14 @@ namespace spot
return result; return result;
} }
formula* const formula*
parse_string(const std::string& eltl_string, parse_string(const std::string& eltl_string,
parse_error_list& error_list, parse_error_list& error_list,
environment& env, environment& env,
bool debug) bool debug)
{ {
flex_scan_string(eltl_string.c_str()); flex_scan_string(eltl_string.c_str());
formula* result = 0; const formula* result = 0;
nfamap nmap; nfamap nmap;
aliasmap amap; aliasmap amap;
parse_error_list_t pe; parse_error_list_t pe;

View file

@ -1,5 +1,6 @@
// Copyright (C) 2008, 2010 Laboratoire de Recherche et Développement // -*- coding: utf-8 -*-
// de l'Epita (LRDE). // Copyright (C) 2008, 2010, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -64,10 +65,11 @@ namespace spot
/// 0 if the file could not be opened. /// 0 if the file could not be opened.
/// ///
/// \warning This function is not reentrant. /// \warning This function is not reentrant.
formula* parse_file(const std::string& filename, const formula* parse_file(const std::string& filename,
parse_error_list& error_list, parse_error_list& error_list,
environment& env = default_environment::instance(), environment& env =
bool debug = false); default_environment::instance(),
bool debug = false);
/// \brief Build a formula from an ELTL string. /// \brief Build a formula from an ELTL string.
/// \param eltl_string The string to parse. /// \param eltl_string The string to parse.
@ -79,10 +81,11 @@ namespace spot
/// 0 if the input was unparsable. /// 0 if the input was unparsable.
/// ///
/// \warning This function is not reentrant. /// \warning This function is not reentrant.
formula* parse_string(const std::string& eltl_string, const formula* parse_string(const std::string& eltl_string,
parse_error_list& error_list, parse_error_list& error_list,
environment& env = default_environment::instance(), environment& env =
bool debug = false); default_environment::instance(),
bool debug = false);
/// \brief Format diagnostics produced by spot::eltl::parse. /// \brief Format diagnostics produced by spot::eltl::parse.
/// \param os Where diagnostics should be output. /// \param os Where diagnostics should be output.

View file

@ -1,7 +1,8 @@
// Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement // -*- coding: utf-8 -*-
// de l'Epita (LRDE). // Copyright (C) 2008, 2009, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
// Pierre et Marie Curie. // Pierre et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -84,7 +85,7 @@ main(int argc, char** argv)
while (tok) while (tok)
{ {
unobservables->insert unobservables->insert
(static_cast<spot::ltl::atomic_prop*>(env.require(tok))); (static_cast<const spot::ltl::atomic_prop*>(env.require(tok)));
tok = strtok(0, ", \t;"); tok = strtok(0, ", \t;");
} }
} }
@ -100,7 +101,7 @@ main(int argc, char** argv)
spot::bdd_dict* dict = new spot::bdd_dict(); spot::bdd_dict* dict = new spot::bdd_dict();
spot::ltl::formula* f = 0; const spot::ltl::formula* f = 0;
{ {
spot::ltl::parse_error_list pel; spot::ltl::parse_error_list pel;

View file

@ -1,4 +1,5 @@
// Copyright (C) 2011 Laboratoire de Recherche et Developpement // -*- coding: utf-8 -*-
// Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE) // de l'Epita (LRDE)
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -48,7 +49,7 @@ typedef std::map<std::string, bdd> formula_cache;
{ {
int token; int token;
std::string* str; std::string* str;
spot::ltl::formula* f; const spot::ltl::formula* f;
std::list<std::string*>* list; std::list<std::string*>* list;
} }
@ -113,7 +114,7 @@ strident "," condition "," follow_list ";"
if (i == fcache.end()) if (i == fcache.end())
{ {
parse_error_list pel; parse_error_list pel;
formula* f = spot::ltl::parse(*$3, pel, parse_environment); const formula* f = spot::ltl::parse(*$3, pel, parse_environment);
for (parse_error_list::iterator i = pel.begin(); for (parse_error_list::iterator i = pel.begin();
i != pel.end(); ++i) i != pel.end(); ++i)
{ {
@ -158,7 +159,7 @@ string: STRING
{ {
$$ = $1; $$ = $1;
error_list.push_back(spot::kripke_parse_error(@1, error_list.push_back(spot::kripke_parse_error(@1,
"unterminated string")); "unterminated string"));
} }
; ;

View file

@ -1,8 +1,9 @@
// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement // -*- coding: utf-8 -*-
// de l'Epita (LRDE). // Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -71,13 +72,7 @@ namespace spot
} }
void void
atomic_prop::accept(visitor& v) atomic_prop::accept(visitor& v) const
{
v.visit(this);
}
void
atomic_prop::accept(const_visitor& v) const
{ {
v.visit(this); v.visit(this);
} }
@ -96,18 +91,19 @@ namespace spot
atomic_prop::map atomic_prop::instances; atomic_prop::map atomic_prop::instances;
atomic_prop* const atomic_prop*
atomic_prop::instance(const std::string& name, environment& env) atomic_prop::instance(const std::string& name, environment& env)
{ {
pair p(name, &env); pair p(name, &env);
// FIXME: Use lower_bound, or a hash_map.
map::iterator i = instances.find(p); map::iterator i = instances.find(p);
const atomic_prop* ap;
if (i != instances.end()) if (i != instances.end())
{ ap = i->second;
return static_cast<atomic_prop*>(i->second->clone()); else
} ap = instances[p] = new atomic_prop(name, env);
atomic_prop* ap = new atomic_prop(name, env); ap->clone();
instances[p] = ap; return ap;
return static_cast<atomic_prop*>(ap->clone());
} }
unsigned unsigned

View file

@ -45,10 +45,10 @@ namespace spot
public: public:
/// Build an atomic proposition with name \a name in /// Build an atomic proposition with name \a name in
/// environment \a env. /// environment \a env.
static atomic_prop* instance(const std::string& name, environment& env); static const atomic_prop*
instance(const std::string& name, environment& env);
virtual void accept(visitor& visitor); virtual void accept(visitor& visitor) const;
virtual void accept(const_visitor& visitor) const;
/// Get the name of the atomic proposition. /// Get the name of the atomic proposition.
const std::string& name() const; const std::string& name() const;
@ -68,7 +68,7 @@ namespace spot
virtual ~atomic_prop(); virtual ~atomic_prop();
typedef std::pair<std::string, environment*> pair; typedef std::pair<std::string, environment*> pair;
typedef std::map<pair, atomic_prop*> map; typedef std::map<pair, const atomic_prop*> map;
static map instances; static map instances;
private: private:

View file

@ -1,5 +1,6 @@
// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et // -*- coding: utf-8 -*-
// Developpement de l'Epita (LRDE) // Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche
// et Développement de l'Epita (LRDE)
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -84,36 +85,34 @@ namespace spot
} }
void void
automatop::accept(visitor& v) automatop::accept(visitor& v) const
{
v.visit(this);
}
void
automatop::accept(const_visitor& v) const
{ {
v.visit(this); v.visit(this);
} }
automatop::map automatop::instances; automatop::map automatop::instances;
automatop* const automatop*
automatop::instance(const nfa::ptr nfa, vec* v, bool negated) automatop::instance(const nfa::ptr nfa, vec* v, bool negated)
{ {
assert(nfa != 0); assert(nfa != 0);
triplet p(std::make_pair(nfa, negated), v); triplet p(std::make_pair(nfa, negated), v);
map::iterator i = instances.find(p); map::iterator i = instances.find(p);
const automatop* res;
if (i != instances.end()) if (i != instances.end())
{ {
// The instance already exists. // The instance already exists.
for (vec::iterator vi = v->begin(); vi != v->end(); ++vi) for (vec::iterator vi = v->begin(); vi != v->end(); ++vi)
(*vi)->destroy(); (*vi)->destroy();
delete v; delete v;
return static_cast<automatop*>(i->second->clone()); res = i->second;
} }
automatop* res = new automatop(nfa, v, negated); else
instances[p] = res; {
return static_cast<automatop*>(res->clone()); res = instances[p] = new automatop(nfa, v, negated);
}
res->clone();
return res;
} }
unsigned unsigned
@ -128,12 +127,6 @@ namespace spot
return (*children_)[n]; return (*children_)[n];
} }
formula*
automatop::nth(unsigned n)
{
return (*children_)[n];
}
const spot::ltl::nfa::ptr const spot::ltl::nfa::ptr
automatop::get_nfa() const automatop::get_nfa() const
{ {
@ -165,6 +158,5 @@ namespace spot
} }
return os; return os;
} }
} }
} }

View file

@ -1,5 +1,6 @@
// Copyright (C) 2008, 2009 Laboratoire de Recherche et Developpement // -*- coding: utf-8 -*-
// de l'Epita (LRDE) // Copyright (C) 2008, 2009, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE)
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -40,7 +41,7 @@ namespace spot
{ {
public: public:
/// List of formulae. /// List of formulae.
typedef std::vector<formula*> vec; typedef std::vector<const formula*> vec;
/// \brief Build a spot::ltl::automatop with many children. /// \brief Build a spot::ltl::automatop with many children.
/// ///
@ -48,11 +49,10 @@ namespace spot
/// the caller should allocate it with \c new, but not use it /// the caller should allocate it with \c new, but not use it
/// (especially not destroy it) after it has been passed to /// (especially not destroy it) after it has been passed to
/// spot::ltl::automatop. /// spot::ltl::automatop.
static automatop* static const automatop*
instance(const nfa::ptr nfa, vec* v, bool negated); instance(const nfa::ptr nfa, vec* v, bool negated);
virtual void accept(visitor& v); virtual void accept(visitor& v) const;
virtual void accept(const_visitor& v) const;
/// Get the number of argument. /// Get the number of argument.
unsigned size() const; unsigned size() const;
@ -60,10 +60,6 @@ namespace spot
/// ///
/// Starting with \a n = 0. /// Starting with \a n = 0.
const formula* nth(unsigned n) const; const formula* nth(unsigned n) const;
/// \brief Get the nth argument.
///
/// Starting with \a n = 0.
formula* nth(unsigned n);
/// Get the NFA of this operator. /// Get the NFA of this operator.
const spot::ltl::nfa::ptr get_nfa() const; const spot::ltl::nfa::ptr get_nfa() const;
@ -96,7 +92,7 @@ namespace spot
return *p1.second < *p2.second; return *p1.second < *p2.second;
} }
}; };
typedef std::map<triplet, automatop*, tripletcmp> map; typedef std::map<triplet, const automatop*, tripletcmp> map;
static map instances; static map instances;
automatop(const nfa::ptr, vec* v, bool negated); automatop(const nfa::ptr, vec* v, bool negated);

View file

@ -1,8 +1,9 @@
// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement // -*- coding: utf-8 -*-
// de l'Epita (LRDE). // Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris // Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -34,7 +35,7 @@ namespace spot
{ {
namespace ltl namespace ltl
{ {
binop::binop(type op, formula* first, formula* second) binop::binop(type op, const formula* first, const formula* second)
: ref_formula(BinOp), op_(op), first_(first), second_(second) : ref_formula(BinOp), op_(op), first_(first), second_(second)
{ {
// Beware: (f U g) is a pure eventuality if both operands // Beware: (f U g) is a pure eventuality if both operands
@ -270,13 +271,7 @@ namespace spot
} }
void void
binop::accept(visitor& v) binop::accept(visitor& v) const
{
v.visit(this);
}
void
binop::accept(const_visitor& v) const
{ {
v.visit(this); v.visit(this);
} }
@ -287,24 +282,12 @@ namespace spot
return first_; return first_;
} }
formula*
binop::first()
{
return first_;
}
const formula* const formula*
binop::second() const binop::second() const
{ {
return second_; return second_;
} }
formula*
binop::second()
{
return second_;
}
binop::type binop::type
binop::op() const binop::op() const
{ {
@ -344,8 +327,8 @@ namespace spot
binop::map binop::instances; binop::map binop::instances;
formula* const formula*
binop::instance(type op, formula* first, formula* second) binop::instance(type op, const formula* first, const formula* second)
{ {
// Sort the operands of commutative operators, so that for // Sort the operands of commutative operators, so that for
// example the formula instance for 'a xor b' is the same as // example the formula instance for 'a xor b' is the same as
@ -544,17 +527,22 @@ namespace spot
pairf pf(first, second); pairf pf(first, second);
pair p(op, pf); pair p(op, pf);
// FIXME: Use lower_bound or hash_map.
map::iterator i = instances.find(p); map::iterator i = instances.find(p);
const binop* res;
if (i != instances.end()) if (i != instances.end())
{ {
// This instance already exists. // This instance already exists.
first->destroy(); first->destroy();
second->destroy(); second->destroy();
return static_cast<binop*>(i->second->clone()); res = i->second;
} }
binop* ap = new binop(op, first, second); else
instances[p] = ap; {
return static_cast<binop*>(ap->clone()); res = instances[p] = new binop(op, first, second);
}
res->clone();
return res;
} }
unsigned unsigned

View file

@ -106,19 +106,16 @@ namespace spot
/// - [*0] []-> Exp = 1 /// - [*0] []-> Exp = 1
/// - Exp []-> 1 = 1 /// - Exp []-> 1 = 1
/// - boolExp <>-> Exp = !boolExp | Exp /// - boolExp <>-> Exp = !boolExp | Exp
static formula* instance(type op, formula* first, formula* second); static const formula* instance(type op,
const formula* first,
const formula* second);
virtual void accept(visitor& v); virtual void accept(visitor& v) const;
virtual void accept(const_visitor& v) const;
/// Get the first operand. /// Get the first operand.
const formula* first() const; const formula* first() const;
/// Get the first operand.
formula* first();
/// Get the second operand. /// Get the second operand.
const formula* second() const; const formula* second() const;
/// Get the second operand.
formula* second();
/// Get the type of this operator. /// Get the type of this operator.
type op() const; type op() const;
@ -135,18 +132,18 @@ namespace spot
static std::ostream& dump_instances(std::ostream& os); static std::ostream& dump_instances(std::ostream& os);
protected: protected:
typedef std::pair<formula*, formula*> pairf; typedef std::pair<const formula*, const formula*> pairf;
typedef std::pair<type, pairf> pair; typedef std::pair<type, pairf> pair;
typedef std::map<pair, binop*> map; typedef std::map<pair, const binop*> map;
static map instances; static map instances;
binop(type op, formula* first, formula* second); binop(type op, const formula* first, const formula* second);
virtual ~binop(); virtual ~binop();
private: private:
type op_; type op_;
formula* first_; const formula* first_;
formula* second_; const formula* second_;
}; };
/// \brief Cast \a f into a binop /// \brief Cast \a f into a binop
@ -154,12 +151,12 @@ namespace spot
/// Cast \a f into a binop iff it is a binop instance. Return 0 /// Cast \a f into a binop iff it is a binop instance. Return 0
/// otherwise. This is faster than \c dynamic_cast. /// otherwise. This is faster than \c dynamic_cast.
inline inline
binop* const binop*
is_binop(formula* f) is_binop(const formula* f)
{ {
if (f->kind() != formula::BinOp) if (f->kind() != formula::BinOp)
return 0; return 0;
return static_cast<binop*>(f); return static_cast<const binop*>(f);
} }
/// \brief Cast \a f into a binop if it has type \a op. /// \brief Cast \a f into a binop if it has type \a op.
@ -167,15 +164,13 @@ namespace spot
/// Cast \a f into a binop iff it is a unop instance with operator \a op. /// Cast \a f into a binop iff it is a unop instance with operator \a op.
/// Returns 0 otherwise. /// Returns 0 otherwise.
inline inline
binop* const binop*
is_binop(formula* f, binop::type op) is_binop(const formula* f, binop::type op)
{ {
if (f->kind() != formula::BinOp) if (const binop* bo = is_binop(f))
return 0; if (bo->op() == op)
binop* bo = static_cast<binop*>(f); return bo;
if (bo->op() != op) return 0;
return 0;
return bo;
} }
/// \brief Cast \a f into a binop if it has type \a op1 or \a op2. /// \brief Cast \a f into a binop if it has type \a op1 or \a op2.
@ -183,15 +178,12 @@ namespace spot
/// Cast \a f into a binop iff it is a unop instance with operator \a op1 or /// Cast \a f into a binop iff it is a unop instance with operator \a op1 or
/// \a op2. Returns 0 otherwise. /// \a op2. Returns 0 otherwise.
inline inline
binop* const binop*
is_binop(formula* f, binop::type op1, binop::type op2) is_binop(const formula* f, binop::type op1, binop::type op2)
{ {
if (f->kind() != formula::BinOp) if (const binop* bo = is_binop(f))
return 0; if (bo->op() == op1 || bo->op() == op2)
binop* bo = static_cast<binop*>(f); return bo;
binop::type op = bo->op();
if (op == op1 || op == op2)
return bo;
return 0; return 0;
} }
@ -199,8 +191,8 @@ namespace spot
/// ///
/// Return 0 otherwise. /// Return 0 otherwise.
inline inline
binop* const binop*
is_U(formula* f) is_U(const formula* f)
{ {
return is_binop(f, binop::U); return is_binop(f, binop::U);
} }
@ -209,8 +201,8 @@ namespace spot
/// ///
/// Return 0 otherwise. /// Return 0 otherwise.
inline inline
binop* const binop*
is_M(formula* f) is_M(const formula* f)
{ {
return is_binop(f, binop::M); return is_binop(f, binop::M);
} }
@ -219,8 +211,8 @@ namespace spot
/// ///
/// Return 0 otherwise. /// Return 0 otherwise.
inline inline
binop* const binop*
is_R(formula* f) is_R(const formula* f)
{ {
return is_binop(f, binop::R); return is_binop(f, binop::R);
} }
@ -229,8 +221,8 @@ namespace spot
/// ///
/// Return 0 otherwise. /// Return 0 otherwise.
inline inline
binop* const binop*
is_W(formula* f) is_W(const formula* f)
{ {
return is_binop(f, binop::W); return is_binop(f, binop::W);
} }

View file

@ -33,9 +33,9 @@ namespace spot
{ {
// Can't build it on startup, because it uses // Can't build it on startup, because it uses
// constant::true_instance that may not have been built yet... // constant::true_instance that may not have been built yet...
formula* bunop::one_star_ = 0; const formula* bunop::one_star_ = 0;
bunop::bunop(type op, formula* child, unsigned min, unsigned max) bunop::bunop(type op, const formula* child, unsigned min, unsigned max)
: ref_formula(BUnOp), op_(op), child_(child), min_(min), max_(max) : ref_formula(BUnOp), op_(op), child_(child), min_(min), max_(max)
{ {
props = child->get_props(); props = child->get_props();
@ -95,13 +95,7 @@ namespace spot
} }
void void
bunop::accept(visitor& v) bunop::accept(visitor& v) const
{
v.visit(this);
}
void
bunop::accept(const_visitor& v) const
{ {
v.visit(this); v.visit(this);
} }
@ -112,12 +106,6 @@ namespace spot
return child_; return child_;
} }
formula*
bunop::child()
{
return child_;
}
unsigned unsigned
bunop::min() const bunop::min() const
{ {
@ -187,8 +175,9 @@ namespace spot
bunop::map bunop::instances; bunop::map bunop::instances;
formula* const formula*
bunop::instance(type op, formula* child, unsigned min, unsigned max) bunop::instance(type op, const formula* child,
unsigned min, unsigned max)
{ {
assert(min <= max); assert(min <= max);
@ -225,9 +214,8 @@ namespace spot
// - Exp[*i..j][*min..max] = Exp[*i(min)..j(max)] // - Exp[*i..j][*min..max] = Exp[*i(min)..j(max)]
// if i*(min+1)<=j(min)+1. // if i*(min+1)<=j(min)+1.
if (child->kind() == BUnOp) if (const bunop* s = is_bunop(child))
{ {
bunop* s = static_cast<bunop*>(child);
unsigned i = s->min(); unsigned i = s->min();
unsigned j = s->max(); unsigned j = s->max();
@ -242,7 +230,7 @@ namespace spot
// (Because i<=j, this entails that the other intervals also // (Because i<=j, this entails that the other intervals also
// overlap). // overlap).
formula* exp = s->child(); const formula* exp = s->child();
if (j == unbounded) if (j == unbounded)
{ {
min *= i; min *= i;
@ -283,25 +271,26 @@ namespace spot
child->destroy(); child->destroy();
return i->second->clone(); return i->second->clone();
} }
bunop* ap = new bunop(op, child, min, max); const bunop* res = instances[p] = new bunop(op, child, min, max);
instances[p] = ap; res->clone();
return static_cast<bunop*>(ap->clone()); return res;
} }
formula* const formula*
bunop::sugar_goto(formula* b, unsigned min, unsigned max) bunop::sugar_goto(const formula* b, unsigned min, unsigned max)
{ {
assert(b->is_boolean()); assert(b->is_boolean());
// b[->min..max] is implemented as ((!b)[*];b)[*min..max] // b[->min..max] is implemented as ((!b)[*];b)[*min..max]
formula* s = bunop::instance(bunop::Star, const formula* s =
unop::instance(unop::Not, b->clone())); bunop::instance(bunop::Star,
unop::instance(unop::Not, b->clone()));
return bunop::instance(bunop::Star, return bunop::instance(bunop::Star,
multop::instance(multop::Concat, s, b), multop::instance(multop::Concat, s, b),
min, max); min, max);
} }
formula* const formula*
bunop::sugar_equal(formula* b, unsigned min, unsigned max) bunop::sugar_equal(const formula* b, unsigned min, unsigned max)
{ {
assert(b->is_boolean()); assert(b->is_boolean());
// b[=0..] = 1[*] // b[=0..] = 1[*]
@ -312,12 +301,13 @@ namespace spot
} }
// b[=min..max] is implemented as ((!b)[*];b)[*min..max];(!b)[*] // b[=min..max] is implemented as ((!b)[*];b)[*min..max];(!b)[*]
formula* s = bunop::instance(bunop::Star, const formula* s =
unop::instance(unop::Not, b->clone())); bunop::instance(bunop::Star,
formula* t = bunop::instance(bunop::Star, unop::instance(unop::Not, b->clone()));
multop::instance(multop::Concat, const formula* t =
s->clone(), b), bunop::instance(bunop::Star,
min, max); multop::instance(multop::Concat,
s->clone(), b), min, max);
return multop::instance(multop::Concat, t, s); return multop::instance(multop::Concat, t, s);
} }

View file

@ -57,10 +57,10 @@ namespace spot
/// These rewriting rules imply that it is not possible to build /// These rewriting rules imply that it is not possible to build
/// an LTL formula object that is SYNTACTICALLY equal to one of /// an LTL formula object that is SYNTACTICALLY equal to one of
/// these left expressions. /// these left expressions.
static formula* instance(type op, static const formula* instance(type op,
formula* child, const formula* child,
unsigned min = 0, unsigned min = 0,
unsigned max = unbounded); unsigned max = unbounded);
/// \brief Implement <code>b[->i..j]</code> using the Kleen star. /// \brief Implement <code>b[->i..j]</code> using the Kleen star.
/// ///
@ -71,9 +71,9 @@ namespace spot
/// [->1..]. /// [->1..].
/// ///
/// \pre \a child must be a Boolean formula. /// \pre \a child must be a Boolean formula.
static formula* sugar_goto(formula* child, static const formula* sugar_goto(const formula* child,
unsigned min = 1, unsigned min = 1,
unsigned max = unbounded); unsigned max = unbounded);
/// \brief Implement b[=i..j] using the Kleen star. /// \brief Implement b[=i..j] using the Kleen star.
/// ///
@ -81,17 +81,14 @@ namespace spot
/// <code>((!b)[*];b)[*i..j];(!b)[*]</code>. /// <code>((!b)[*];b)[*i..j];(!b)[*]</code>.
/// ///
/// \pre \a child must be a Boolean formula. /// \pre \a child must be a Boolean formula.
static formula* sugar_equal(formula* child, static const formula* sugar_equal(const formula* child,
unsigned min = 0, unsigned min = 0,
unsigned max = unbounded); unsigned max = unbounded);
virtual void accept(visitor& v); virtual void accept(visitor& v) const;
virtual void accept(const_visitor& v) const;
/// Get the sole operand of this operator. /// Get the sole operand of this operator.
const formula* child() const; const formula* child() const;
/// Get the sole operand of this operator.
formula* child();
/// Minimum number of repetition. /// Minimum number of repetition.
unsigned min() const; unsigned min() const;
@ -122,7 +119,7 @@ namespace spot
/// A global instance is returned, and it should not be /// A global instance is returned, and it should not be
/// destroyed. Remember to clone it if you use it to build a /// destroyed. Remember to clone it if you use it to build a
/// formula. /// formula.
static formula* one_star() static const formula* one_star()
{ {
if (!one_star_) if (!one_star_)
one_star_ = instance(Star, constant::true_instance()); one_star_ = instance(Star, constant::true_instance());
@ -131,20 +128,20 @@ namespace spot
protected: protected:
typedef std::pair<unsigned, unsigned> pairu; typedef std::pair<unsigned, unsigned> pairu;
typedef std::pair<type, formula*> pairo; typedef std::pair<type, const formula*> pairo;
typedef std::pair<pairo, pairu> pair; typedef std::pair<pairo, pairu> pair;
typedef std::map<pair, bunop*> map; typedef std::map<pair, const bunop*> map;
static map instances; static map instances;
bunop(type op, formula* child, unsigned min, unsigned max); bunop(type op, const formula* child, unsigned min, unsigned max);
virtual ~bunop(); virtual ~bunop();
private: private:
type op_; type op_;
formula* child_; const formula* child_;
unsigned min_; unsigned min_;
unsigned max_; unsigned max_;
static formula* one_star_; static const formula* one_star_;
}; };
/// \brief Cast \a f into a bunop. /// \brief Cast \a f into a bunop.
@ -152,12 +149,12 @@ namespace spot
/// Cast \a f into a bunop iff it is a bunop instance. Return 0 /// Cast \a f into a bunop iff it is a bunop instance. Return 0
/// otherwise. This is faster than \c dynamic_cast. /// otherwise. This is faster than \c dynamic_cast.
inline inline
bunop* const bunop*
is_bunop(const formula* f) is_bunop(const formula* f)
{ {
if (f->kind() != formula::BUnOp) if (f->kind() != formula::BUnOp)
return 0; return 0;
return static_cast<bunop*>(const_cast<formula*>(f)); return static_cast<const bunop*>(f);
} }
/// \brief Cast \a f into a bunop if it has type \a op. /// \brief Cast \a f into a bunop if it has type \a op.
@ -165,22 +162,20 @@ namespace spot
/// Cast \a f into a bunop iff it is a bunop instance with operator \a op. /// Cast \a f into a bunop iff it is a bunop instance with operator \a op.
/// Returns 0 otherwise. /// Returns 0 otherwise.
inline inline
bunop* const bunop*
is_bunop(const formula* f, bunop::type op) is_bunop(const formula* f, bunop::type op)
{ {
if (f->kind() != formula::BUnOp) if (const bunop* bo = is_bunop(f))
return 0; if (bo->op() == op)
bunop* bo = static_cast<bunop*>(const_cast<formula*>(f)); return bo;
if (bo->op() != op) return 0;
return 0;
return bo;
} }
/// \brief Cast \a f into a bunop if it is a Star. /// \brief Cast \a f into a bunop if it is a Star.
/// ///
/// Return 0 otherwise. /// Return 0 otherwise.
inline inline
bunop* const bunop*
is_Star(const formula* f) is_Star(const formula* f)
{ {
return is_bunop(f, bunop::Star); return is_bunop(f, bunop::Star);
@ -190,10 +185,10 @@ namespace spot
/// ///
/// Return 0 otherwise. /// Return 0 otherwise.
inline inline
bunop* const bunop*
is_KleenStar(const formula* f) is_KleenStar(const formula* f)
{ {
if (bunop* b = is_Star(f)) if (const bunop* b = is_Star(f))
if (b->min() == 0 && b->max() == bunop::unbounded) if (b->min() == 0 && b->max() == bunop::unbounded)
return b; return b;
return 0; return 0;

View file

@ -1,8 +1,9 @@
// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et D<>veloppement // -*- coding: utf-8 -*-
// de l'Epita (LRDE). // Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris // Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris
// 6 (LIP6), d<EFBFBD>partement Syst<73>mes R<>partis Coop<6F>ratifs (SRC), // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Universit<EFBFBD> Pierre et Marie Curie. // Université Pierre et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -106,13 +107,7 @@ namespace spot
} }
void void
constant::accept(visitor& v) constant::accept(visitor& v) const
{
v.visit(this);
}
void
constant::accept(const_visitor& v) const
{ {
v.visit(this); v.visit(this);
} }

View file

@ -37,8 +37,7 @@ namespace spot
{ {
public: public:
enum type { False, True, EmptyWord }; enum type { False, True, EmptyWord };
virtual void accept(visitor& v); virtual void accept(visitor& v) const;
virtual void accept(const_visitor& v) const;
/// Return the value of the constant. /// Return the value of the constant.
type val() const; type val() const;
@ -74,12 +73,12 @@ namespace spot
/// Cast \a f into a constant iff it is a constant instance. /// Cast \a f into a constant iff it is a constant instance.
/// Return 0 otherwise. This is faster than \c dynamic_cast. /// Return 0 otherwise. This is faster than \c dynamic_cast.
inline inline
constant* const constant*
is_constant(formula* f) is_constant(const formula* f)
{ {
if (f->kind() != formula::Constant) if (f->kind() != formula::Constant)
return 0; return 0;
return static_cast<constant*>(f); return static_cast<const constant*>(f);
} }
} }
} }

View file

@ -32,11 +32,11 @@ namespace spot
{ {
size_t formula::max_count = 0; size_t formula::max_count = 0;
formula* const formula*
formula::clone() const formula::clone() const
{ {
const_cast<formula*>(this)->ref_(); this->ref_();
return const_cast<formula*>(this); return this;
} }
formula::~formula() formula::~formula()
@ -46,18 +46,18 @@ namespace spot
void void
formula::destroy() const formula::destroy() const
{ {
if (const_cast<formula*>(this)->unref_()) if (this->unref_())
delete this; delete this;
} }
void void
formula::ref_() formula::ref_() const
{ {
// Not reference counted by default. // Not reference counted by default.
} }
bool bool
formula::unref_() formula::unref_() const
{ {
// Not reference counted by default. // Not reference counted by default.
return false; return false;

View file

@ -82,6 +82,7 @@ namespace spot
BUnOp, BUnOp,
AutomatOp }; AutomatOp };
protected:
formula(opkind k) : count_(max_count++), kind_(k) formula(opkind k) : count_(max_count++), kind_(k)
{ {
// If the counter of formulae ever loops, we want to skip the // If the counter of formulae ever loops, we want to skip the
@ -92,16 +93,15 @@ namespace spot
max_count = 3; max_count = 3;
} }
/// Entry point for vspot::ltl::visitor instances. public:
virtual void accept(visitor& v) = 0; /// Entry point for spot::ltl::visitor instances.
/// Entry point for vspot::ltl::const_visitor instances. virtual void accept(visitor& v) const = 0;
virtual void accept(const_visitor& v) const = 0;
/// \brief clone this node /// \brief clone this node
/// ///
/// This increments the reference counter of this node (if one is /// This increments the reference counter of this node (if one is
/// used). /// used).
formula* clone() const; const formula* clone() const;
/// \brief release this node /// \brief release this node
/// ///
/// This decrements the reference counter of this node (if one is /// This decrements the reference counter of this node (if one is
@ -293,10 +293,10 @@ namespace spot
virtual ~formula(); virtual ~formula();
/// \brief increment reference counter if any /// \brief increment reference counter if any
virtual void ref_(); virtual void ref_() const;
/// \brief decrement reference counter if any, return true when /// \brief decrement reference counter if any, return true when
/// the instance must be deleted (usually when the counter hits 0). /// the instance must be deleted (usually when the counter hits 0).
virtual bool unref_(); virtual bool unref_() const;
/// \brief The hash key of this formula. /// \brief The hash key of this formula.
size_t count_; size_t count_;

View file

@ -1,4 +1,5 @@
// Copyright (C) 2009 Laboratoire de Recherche et Développement // -*- coding: utf-8 -*-
// Copyright (C) 2009, 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -28,8 +29,8 @@ namespace spot
{ {
namespace formula_tree namespace formula_tree
{ {
formula* const formula*
instanciate(const node_ptr np, const std::vector<formula*>& v) instanciate(const node_ptr np, const std::vector<const formula*>& v)
{ {
if (node_atomic* n = dynamic_cast<node_atomic*>(np.get())) if (node_atomic* n = dynamic_cast<node_atomic*>(np.get()))
return n->i == True ? constant::true_instance() : return n->i == True ? constant::true_instance() :

View file

@ -1,4 +1,4 @@
// Copyright (C) 2009 Laboratoire de Recherche et Développement // Copyright (C) 2009, 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -76,7 +76,8 @@ namespace spot
/// Instanciate the formula corresponding to the node with /// Instanciate the formula corresponding to the node with
/// atomic propositions taken from \a v. /// atomic propositions taken from \a v.
formula* instanciate(const node_ptr np, const std::vector<formula*>& v); const formula* instanciate(const node_ptr np,
const std::vector<const formula*>& v);
/// Get the arity. /// Get the arity.
size_t arity(const node_ptr np); size_t arity(const node_ptr np);

View file

@ -119,13 +119,7 @@ namespace spot
} }
void void
multop::accept(visitor& v) multop::accept(visitor& v) const
{
v.visit(this);
}
void
multop::accept(const_visitor& v) const
{ {
v.visit(this); v.visit(this);
} }
@ -142,18 +136,12 @@ namespace spot
return (*children_)[n]; return (*children_)[n];
} }
formula* const formula*
multop::nth(unsigned n)
{
return (*children_)[n];
}
formula*
multop::all_but(unsigned n) const multop::all_but(unsigned n) const
{ {
unsigned s = size(); unsigned s = size();
vec* v = new vec; vec* v = new vec;
v->reserve(s-1); v->reserve(s - 1);
for (unsigned pos = 0; pos < n; ++pos) for (unsigned pos = 0; pos < n; ++pos)
v->push_back(nth(pos)->clone()); v->push_back(nth(pos)->clone());
for (unsigned pos = n + 1; pos < s; ++pos) for (unsigned pos = n + 1; pos < s; ++pos)
@ -192,35 +180,37 @@ namespace spot
return 0; return 0;
} }
namespace
void
gather_bool(multop::vec* v, multop::type op)
{ {
// Gather all boolean terms. static void
multop::vec* b = new multop::vec; gather_bool(multop::vec* v, multop::type op)
multop::vec::iterator i = v->begin(); {
while (i != v->end()) // Gather all boolean terms.
{ multop::vec* b = new multop::vec;
if ((*i)->is_boolean()) multop::vec::iterator i = v->begin();
{ while (i != v->end())
b->push_back(*i); {
i = v->erase(i); if ((*i)->is_boolean())
} {
else b->push_back(*i);
{ i = v->erase(i);
++i; }
} else
} {
// - AndNLM(Exps1...,Bool1,Exps2...,Bool2,Exps3...) = ++i;
// AndNLM(Exps1...,Exps2...,Exps3...,And(Bool1,Bool2)) }
// - AndRat(Exps1...,Bool1,Exps2...,Bool2,Exps3...) = }
// AndRat(Exps1...,Exps2...,Exps3...,And(Bool1,Bool2)) // - AndNLM(Exps1...,Bool1,Exps2...,Bool2,Exps3...) =
// - OrRat(Exps1...,Bool1,Exps2...,Bool2,Exps3...) = // AndNLM(Exps1...,Exps2...,Exps3...,And(Bool1,Bool2))
// AndRat(Exps1...,Exps2...,Exps3...,Or(Bool1,Bool2)) // - AndRat(Exps1...,Bool1,Exps2...,Bool2,Exps3...) =
if (!b->empty()) // AndRat(Exps1...,Exps2...,Exps3...,And(Bool1,Bool2))
v->push_back(multop::instance(op, b)); // - OrRat(Exps1...,Bool1,Exps2...,Bool2,Exps3...) =
else // AndRat(Exps1...,Exps2...,Exps3...,Or(Bool1,Bool2))
delete b; if (!b->empty())
v->push_back(multop::instance(op, b));
else
delete b;
}
} }
multop::map multop::instances; multop::map multop::instances;
@ -230,7 +220,7 @@ namespace spot
// operator). For instance if `+' designates the OR operator and // operator). For instance if `+' designates the OR operator and
// `0' is false (the neutral element for `+') , then `f+f+0' is // `0' is false (the neutral element for `+') , then `f+f+0' is
// equivalent to `f'. // equivalent to `f'.
formula* const formula*
multop::instance(type op, vec* v) multop::instance(type op, vec* v)
{ {
// Inline children of same kind. // Inline children of same kind.
@ -252,9 +242,8 @@ namespace spot
i = v->erase(i); i = v->erase(i);
continue; continue;
} }
if ((*i)->kind() == MultOp) if (const multop* p = is_multop(*i))
{ {
multop* p = static_cast<multop*>(*i);
if (p->op() == op) if (p->op() == op)
{ {
unsigned ps = p->size(); unsigned ps = p->size();
@ -286,11 +275,11 @@ namespace spot
unsigned orig_size = v->size(); unsigned orig_size = v->size();
formula* neutral; const formula* neutral;
formula* neutral2; const formula* neutral2;
formula* abs; const formula* abs;
formula* abs2; const formula* abs2;
formula* weak_abs; const formula* weak_abs;
switch (op) switch (op)
{ {
case And: case And:
@ -343,7 +332,7 @@ namespace spot
// If FExps2... and FExps3 all accept [*0]. // If FExps2... and FExps3 all accept [*0].
{ {
vec::iterator i = v->begin(); vec::iterator i = v->begin();
formula* os = bunop::one_star(); const formula* os = bunop::one_star();
while (i != v->end()) while (i != v->end())
{ {
while (i != v->end() && !(*i)->accepts_eword()) while (i != v->end() && !(*i)->accepts_eword())
@ -433,7 +422,7 @@ namespace spot
// std::unique(), because we must destroy() any formula we drop. // std::unique(), because we must destroy() any formula we drop.
// Also ignore neutral elements and handle absorbent elements. // Also ignore neutral elements and handle absorbent elements.
{ {
formula* last = 0; const formula* last = 0;
vec::iterator i = v->begin(); vec::iterator i = v->begin();
bool weak_abs_seen = false; bool weak_abs_seen = false;
while (i != v->end()) while (i != v->end())
@ -512,11 +501,11 @@ namespace spot
while (i != v->end()) while (i != v->end())
{ {
vec::iterator fpos = i; vec::iterator fpos = i;
formula* f; const formula* f;
unsigned min; unsigned min;
unsigned max; unsigned max;
bool changed = false; bool changed = false;
if (bunop* is = is_Star(*i)) if (const bunop* is = is_Star(*i))
{ {
f = is->child(); f = is->child();
min = is->min(); min = is->min();
@ -531,10 +520,10 @@ namespace spot
++i; ++i;
while (i != v->end()) while (i != v->end())
{ {
formula* f2; const formula* f2;
unsigned min2; unsigned min2;
unsigned max2; unsigned max2;
if (bunop* is = is_Star(*i)) if (const bunop* is = is_Star(*i))
{ {
f2 = is->child(); f2 = is->child();
if (f2 != f) if (f2 != f)
@ -563,8 +552,8 @@ namespace spot
} }
if (changed) if (changed)
{ {
formula* newfs = bunop::instance(bunop::Star, f->clone(), const formula* newfs =
min, max); bunop::instance(bunop::Star, f->clone(), min, max);
(*fpos)->destroy(); (*fpos)->destroy();
*fpos = newfs; *fpos = newfs;
} }
@ -586,7 +575,7 @@ namespace spot
// arguments of a Fusion operator to // arguments of a Fusion operator to
// a list with a single formula that // a list with a single formula that
// accepts [*0]. // accepts [*0].
formula* res = (*v)[0]; const formula* res = (*v)[0];
if (op != Fusion || orig_size == 1 if (op != Fusion || orig_size == 1
|| !res->accepts_eword()) || !res->accepts_eword())
{ {
@ -600,6 +589,8 @@ namespace spot
// The hash key. // The hash key.
pair p(op, v); pair p(op, v);
const multop* res;
// FIXME: Use lower_bound or hash_map.
map::iterator i = instances.find(p); map::iterator i = instances.find(p);
if (i != instances.end()) if (i != instances.end())
{ {
@ -607,19 +598,20 @@ namespace spot
for (vec::iterator vi = v->begin(); vi != v->end(); ++vi) for (vec::iterator vi = v->begin(); vi != v->end(); ++vi)
(*vi)->destroy(); (*vi)->destroy();
delete v; delete v;
return static_cast<multop*>(i->second->clone()); res = i->second;
} }
else
// This is the first instance of this formula. {
// This is the first instance of this formula.
// Record the instance in the map, // Record the instance in the map,
multop* ap = new multop(op, v); res = instances[p] = new multop(op, v);
instances[p] = ap; }
return ap->clone(); res->clone();
return res;
} }
formula* const formula*
multop::instance(type op, formula* first, formula* second) multop::instance(type op, const formula* first, const formula* second)
{ {
vec* v = new vec; vec* v = new vec;
v->push_back(first); v->push_back(first);

View file

@ -44,7 +44,7 @@ namespace spot
enum type { Or, OrRat, And, AndRat, AndNLM, Concat, Fusion }; enum type { Or, OrRat, And, AndRat, AndNLM, Concat, Fusion };
/// List of formulae. /// List of formulae.
typedef std::vector<formula*> vec; typedef std::vector<const formula*> vec;
/// \brief Build a spot::ltl::multop with two children. /// \brief Build a spot::ltl::multop with two children.
/// ///
@ -57,7 +57,8 @@ namespace spot
/// This functions can perform slight optimizations and /// This functions can perform slight optimizations and
/// may not return an ltl::multop object. See the other /// may not return an ltl::multop object. See the other
/// instance function for the list of rewritings. /// instance function for the list of rewritings.
static formula* instance(type op, formula* first, formula* second); static const formula*
instance(type op, const formula* first, const formula* second);
/// \brief Build a spot::ltl::multop with many children. /// \brief Build a spot::ltl::multop with many children.
/// ///
@ -120,10 +121,9 @@ namespace spot
/// - Fusion(Exp) = Exp /// - Fusion(Exp) = Exp
/// - Fusion(Exps1...,BoolExp1...BoolExpN,Exps2,Exps3...) = /// - Fusion(Exps1...,BoolExp1...BoolExpN,Exps2,Exps3...) =
/// Fusion(Exps1...,And(BoolExp1...BoolExpN),Exps2,Exps3...) /// Fusion(Exps1...,And(BoolExp1...BoolExpN),Exps2,Exps3...)
static formula* instance(type op, vec* v); static const formula* instance(type op, vec* v);
virtual void accept(visitor& v); virtual void accept(visitor& v) const;
virtual void accept(const_visitor& v) const;
/// Get the number of children. /// Get the number of children.
unsigned size() const; unsigned size() const;
@ -131,17 +131,13 @@ namespace spot
/// ///
/// Starting with \a n = 0. /// Starting with \a n = 0.
const formula* nth(unsigned n) const; const formula* nth(unsigned n) const;
/// \brief Get the nth child.
///
/// Starting with \a n = 0.
formula* nth(unsigned n);
/// \brief construct a formula without the nth child. /// \brief construct a formula without the nth child.
/// ///
/// If the formula \c f is <code>a|b|c|d</code> and <code>d</code> /// If the formula \c f is <code>a|b|c|d</code> and <code>d</code>
/// is child number 2, then calling <code>f->all_but(2)</code> will /// is child number 2, then calling <code>f->all_but(2)</code> will
/// return a new formula <code>a|b|d</code>. /// return a new formula <code>a|b|d</code>.
formula* all_but(unsigned n) const; const formula* all_but(unsigned n) const;
/// Get the type of this operator. /// Get the type of this operator.
type op() const; type op() const;
@ -170,7 +166,7 @@ namespace spot
return *p1.second < *p2.second; return *p1.second < *p2.second;
} }
}; };
typedef std::map<pair, multop*, paircmp> map; typedef std::map<pair, const multop*, paircmp> map;
static map instances; static map instances;
multop(type op, vec* v); multop(type op, vec* v);
@ -187,12 +183,12 @@ namespace spot
/// Cast \a f into a multop iff it is a multop instance. Return 0 /// Cast \a f into a multop iff it is a multop instance. Return 0
/// otherwise. This is faster than \c dynamic_cast. /// otherwise. This is faster than \c dynamic_cast.
inline inline
multop* const multop*
is_multop(formula* f) is_multop(const formula* f)
{ {
if (f->kind() != formula::MultOp) if (f->kind() != formula::MultOp)
return 0; return 0;
return static_cast<multop*>(f); return static_cast<const multop*>(f);
} }
/// \brief Cast \a f into a multop if it has type \a op. /// \brief Cast \a f into a multop if it has type \a op.
@ -200,15 +196,13 @@ namespace spot
/// Cast \a f into a multop iff it is a multop instance with operator \a op. /// Cast \a f into a multop iff it is a multop instance with operator \a op.
/// Returns 0 otherwise. /// Returns 0 otherwise.
inline inline
multop* const multop*
is_multop(const formula* f, multop::type op) is_multop(const formula* f, multop::type op)
{ {
if (f->kind() != formula::MultOp) if (const multop* mo = is_multop(f))
return 0; if (mo->op() == op)
multop* mo = static_cast<multop*>(const_cast<formula*>(f)); return mo;
if (mo->op() != op) return 0;
return 0;
return mo;
} }
/// \brief Cast \a f into a multop if it has type \a op1 or \a op2. /// \brief Cast \a f into a multop if it has type \a op1 or \a op2.
@ -216,22 +210,20 @@ namespace spot
/// Cast \a f into a multop iff it is a multop instance with /// Cast \a f into a multop iff it is a multop instance with
/// operator \a op1 or \a op2. Returns 0 otherwise. /// operator \a op1 or \a op2. Returns 0 otherwise.
inline inline
multop* const multop*
is_multop(const formula* f, multop::type op1, multop::type op2) is_multop(const formula* f, multop::type op1, multop::type op2)
{ {
if (f->kind() != formula::MultOp) if (const multop* mo = is_multop(f))
return 0; if (mo->op() == op1 || mo->op() == op2)
multop* mo = static_cast<multop*>(const_cast<formula*>(f)); return mo;
if (mo->op() != op1 && mo->op() != op2) return 0;
return 0;
return mo;
} }
/// \brief Cast \a f into a multop if it is an And. /// \brief Cast \a f into a multop if it is an And.
/// ///
/// Return 0 otherwise. /// Return 0 otherwise.
inline inline
multop* const multop*
is_And(const formula* f) is_And(const formula* f)
{ {
return is_multop(f, multop::And); return is_multop(f, multop::And);
@ -241,7 +233,7 @@ namespace spot
/// ///
/// Return 0 otherwise. /// Return 0 otherwise.
inline inline
multop* const multop*
is_AndRat(const formula* f) is_AndRat(const formula* f)
{ {
return is_multop(f, multop::AndRat); return is_multop(f, multop::AndRat);
@ -251,7 +243,7 @@ namespace spot
/// ///
/// Return 0 otherwise. /// Return 0 otherwise.
inline inline
multop* const multop*
is_AndNLM(const formula* f) is_AndNLM(const formula* f)
{ {
return is_multop(f, multop::AndNLM); return is_multop(f, multop::AndNLM);
@ -261,7 +253,7 @@ namespace spot
/// ///
/// Return 0 otherwise. /// Return 0 otherwise.
inline inline
multop* const multop*
is_Or(const formula* f) is_Or(const formula* f)
{ {
return is_multop(f, multop::Or); return is_multop(f, multop::Or);
@ -271,7 +263,7 @@ namespace spot
/// ///
/// Return 0 otherwise. /// Return 0 otherwise.
inline inline
multop* const multop*
is_OrRat(const formula* f) is_OrRat(const formula* f)
{ {
return is_multop(f, multop::OrRat); return is_multop(f, multop::OrRat);
@ -281,7 +273,7 @@ namespace spot
/// ///
/// Return 0 otherwise. /// Return 0 otherwise.
inline inline
multop* const multop*
is_Concat(const formula* f) is_Concat(const formula* f)
{ {
return is_multop(f, multop::Concat); return is_multop(f, multop::Concat);
@ -291,7 +283,7 @@ namespace spot
/// ///
/// Return 0 otherwise. /// Return 0 otherwise.
inline inline
multop* const multop*
is_Fusion(const formula* f) is_Fusion(const formula* f)
{ {
return is_multop(f, multop::Fusion); return is_multop(f, multop::Fusion);

View file

@ -1,5 +1,5 @@
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement de // Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et
// l'Epita (LRDE). // Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
@ -36,7 +36,6 @@ namespace spot
namespace ltl namespace ltl
{ {
struct visitor; struct visitor;
struct const_visitor;
class atomic_prop; class atomic_prop;
class automatop; class automatop;

View file

@ -1,7 +1,8 @@
// Copyright (C) 2010 Laboratoire de Recherche de Developpement de // -*- coding: utf-8 -*-
// Copyright (C) 2010, 2012 Laboratoire de Recherche de Developpement de
// l'EPITA (LRDE). // l'EPITA (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -38,20 +39,20 @@ namespace spot
} }
void void
ref_formula::ref_() ref_formula::ref_() const
{ {
++ref_counter_; ++ref_counter_;
} }
bool bool
ref_formula::unref_() ref_formula::unref_() const
{ {
assert(ref_counter_ > 0); assert(ref_counter_ > 0);
return !--ref_counter_; return !--ref_counter_;
} }
unsigned unsigned
ref_formula::ref_count_() ref_formula::ref_count_() const
{ {
return ref_counter_; return ref_counter_;
} }

View file

@ -1,8 +1,9 @@
// Copyright (C) 2010 Laboratoire de Recherche de Developpement de // -*- coding: utf-8 -*-
// l'EPITA (LRDE). // Copyright (C) 2010, 2012 Laboratoire de Recherche de Developpement
// de l'EPITA (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -40,12 +41,12 @@ namespace spot
protected: protected:
virtual ~ref_formula(); virtual ~ref_formula();
ref_formula(opkind k); ref_formula(opkind k);
void ref_(); void ref_() const;
bool unref_(); bool unref_() const;
/// Number of references to this formula. /// Number of references to this formula.
unsigned ref_count_(); unsigned ref_count_() const;
private: private:
unsigned ref_counter_; mutable unsigned ref_counter_;
}; };
} }

View file

@ -1,8 +1,9 @@
// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement // -*- coding: utf-8 -*-
// de l'Epita (LRDE). // Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris // Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -32,7 +33,7 @@ namespace spot
{ {
namespace ltl namespace ltl
{ {
unop::unop(type op, formula* child) unop::unop(type op, const formula* child)
: ref_formula(UnOp), op_(op), child_(child) : ref_formula(UnOp), op_(op), child_(child)
{ {
props = child->get_props(); props = child->get_props();
@ -161,13 +162,7 @@ namespace spot
} }
void void
unop::accept(visitor& v) unop::accept(visitor& v) const
{
v.visit(this);
}
void
unop::accept(const_visitor& v) const
{ {
v.visit(this); v.visit(this);
} }
@ -178,12 +173,6 @@ namespace spot
return child_; return child_;
} }
formula*
unop::child()
{
return child_;
}
unop::type unop::type
unop::op() const unop::op() const
{ {
@ -217,8 +206,8 @@ namespace spot
unop::map unop::instances; unop::map unop::instances;
formula* const formula*
unop::instance(type op, formula* child) unop::instance(type op, const formula* child)
{ {
// Some trivial simplifications. // Some trivial simplifications.
@ -227,10 +216,9 @@ namespace spot
case F: case F:
case G: case G:
{ {
if (child->kind() == UnOp) if (const unop* u = is_unop(child))
{ {
// F and G are idempotent. // F and G are idempotent.
unop* u = static_cast<unop*>(child);
if (u->op() == op) if (u->op() == op)
return u; return u;
} }
@ -258,29 +246,28 @@ namespace spot
return bunop::instance(bunop::Star, return bunop::instance(bunop::Star,
constant::true_instance(), 1); constant::true_instance(), 1);
if (child->kind() == UnOp) if (const unop* u = is_unop(child))
{ {
unop* u = static_cast<unop*>(child);
// "Not" is an involution. // "Not" is an involution.
if (u->op() == op) if (u->op() == op)
{ {
formula* c = u->child()->clone(); const formula* c = u->child()->clone();
u->destroy(); u->destroy();
return c; return c;
} }
// !Closure(Exp) = NegClosure(Exp) // !Closure(Exp) = NegClosure(Exp)
if (u->op() == Closure) if (u->op() == Closure)
{ {
formula* c = unop::instance(NegClosure, const formula* c = unop::instance(NegClosure,
u->child()->clone()); u->child()->clone());
u->destroy(); u->destroy();
return c; return c;
} }
// !NegClosure(Exp) = Closure(Exp) // !NegClosure(Exp) = Closure(Exp)
if (u->op() == NegClosure) if (u->op() == NegClosure)
{ {
formula* c = unop::instance(Closure, const formula* c = unop::instance(Closure,
u->child()->clone()); u->child()->clone());
u->destroy(); u->destroy();
return c; return c;
} }
@ -323,17 +310,21 @@ namespace spot
break; break;
} }
const unop* res;
pair p(op, child); pair p(op, child);
map::iterator i = instances.find(p); map::iterator i = instances.find(p);
if (i != instances.end()) if (i != instances.end())
{ {
// This instance already exists. // This instance already exists.
child->destroy(); child->destroy();
return static_cast<unop*>(i->second->clone()); res = i->second;
} }
unop* ap = new unop(op, child); else
instances[p] = ap; {
return static_cast<unop*>(ap->clone()); res = instances[p] = new unop(op, child);
}
res->clone();
return res;
} }
unsigned unsigned

View file

@ -87,15 +87,12 @@ namespace spot
/// grammar. Spot cannot read it either. However some /// grammar. Spot cannot read it either. However some
/// BDD-based algorithm may need to negate any constant, so we /// BDD-based algorithm may need to negate any constant, so we
/// handle this one as well. /// handle this one as well.
static formula* instance(type op, formula* child); static const formula* instance(type op, const formula* child);
virtual void accept(visitor& v); virtual void accept(visitor& v) const;
virtual void accept(const_visitor& v) const;
/// Get the sole operand of this operator. /// Get the sole operand of this operator.
const formula* child() const; const formula* child() const;
/// Get the sole operand of this operator.
formula* child();
/// Get the type of this operator. /// Get the type of this operator.
type op() const; type op() const;
@ -112,16 +109,16 @@ namespace spot
static std::ostream& dump_instances(std::ostream& os); static std::ostream& dump_instances(std::ostream& os);
protected: protected:
typedef std::pair<type, formula*> pair; typedef std::pair<type, const formula*> pair;
typedef std::map<pair, unop*> map; typedef std::map<pair, const unop*> map;
static map instances; static map instances;
unop(type op, formula* child); unop(type op, const formula* child);
virtual ~unop(); virtual ~unop();
private: private:
type op_; type op_;
formula* child_; const formula* child_;
}; };
@ -130,12 +127,12 @@ namespace spot
/// Cast \a f into a unop iff it is a unop instance. Return 0 /// Cast \a f into a unop iff it is a unop instance. Return 0
/// otherwise. This is faster than \c dynamic_cast. /// otherwise. This is faster than \c dynamic_cast.
inline inline
unop* const unop*
is_unop(const formula* f) is_unop(const formula* f)
{ {
if (f->kind() != formula::UnOp) if (f->kind() != formula::UnOp)
return 0; return 0;
return static_cast<unop*>(const_cast<formula*>(f)); return static_cast<const unop*>(f);
} }
/// \brief Cast \a f into a unop if it has type \a op. /// \brief Cast \a f into a unop if it has type \a op.
@ -143,22 +140,20 @@ namespace spot
/// Cast \a f into a unop iff it is a unop instance with operator \a op. /// Cast \a f into a unop iff it is a unop instance with operator \a op.
/// Returns 0 otherwise. /// Returns 0 otherwise.
inline inline
unop* const unop*
is_unop(const formula* f, unop::type op) is_unop(const formula* f, unop::type op)
{ {
if (f->kind() != formula::UnOp) if (const unop* uo = is_unop(f))
return 0; if (uo->op() == op)
unop* uo = static_cast<unop*>(const_cast<formula*>(f)); return uo;
if (uo->op() != op) return 0;
return 0;
return uo;
} }
/// \brief Cast \a f into a unop if it is a Not. /// \brief Cast \a f into a unop if it is a Not.
/// ///
/// Return 0 otherwise. /// Return 0 otherwise.
inline inline
unop* const unop*
is_Not(const formula* f) is_Not(const formula* f)
{ {
return is_unop(f, unop::Not); return is_unop(f, unop::Not);
@ -168,7 +163,7 @@ namespace spot
/// ///
/// Return 0 otherwise. /// Return 0 otherwise.
inline inline
unop* const unop*
is_X(const formula* f) is_X(const formula* f)
{ {
return is_unop(f, unop::X); return is_unop(f, unop::X);
@ -178,7 +173,7 @@ namespace spot
/// ///
/// Return 0 otherwise. /// Return 0 otherwise.
inline inline
unop* const unop*
is_F(const formula* f) is_F(const formula* f)
{ {
return is_unop(f, unop::F); return is_unop(f, unop::F);
@ -188,7 +183,7 @@ namespace spot
/// ///
/// Return 0 otherwise. /// Return 0 otherwise.
inline inline
unop* const unop*
is_G(const formula* f) is_G(const formula* f)
{ {
return is_unop(f, unop::G); return is_unop(f, unop::G);
@ -198,26 +193,24 @@ namespace spot
/// ///
/// Return 0 otherwise. /// Return 0 otherwise.
inline inline
unop* const unop*
is_GF(const formula* f) is_GF(const formula* f)
{ {
unop* op = is_G(f); if (const unop* op = is_G(f))
if (!op) return is_F(op->child());
return 0; return 0;
return is_F(op->child());
} }
/// \brief Cast \a f into a unop if has the form FG(...). /// \brief Cast \a f into a unop if has the form FG(...).
/// ///
/// Return 0 otherwise. /// Return 0 otherwise.
inline inline
unop* const unop*
is_FG(const formula* f) is_FG(const formula* f)
{ {
unop* op = is_F(f); if (const unop* op = is_F(f))
if (!op) return is_G(op->child());
return 0; return 0;
return is_G(op->child());
} }
} }
} }

View file

@ -1,4 +1,4 @@
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement // Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -32,38 +32,15 @@ namespace spot
{ {
namespace ltl namespace ltl
{ {
/// \brief Formula visitor that can modify the formula. /// \brief Formula visitor
/// \ingroup ltl_essential /// \ingroup ltl_essential
/// ///
/// Writing visitors is the prefered way /// Implementing visitors is the prefered way
/// to traverse a formula, since it doesn't /// to traverse a formula, since it does not
/// involve any cast. /// involve any cast.
///
/// If you do not need to modify the visited formula, inherit from
/// spot::ltl:const_visitor instead.
struct visitor struct visitor
{ {
virtual ~visitor() {} virtual ~visitor() {}
virtual void visit(atomic_prop* node) = 0;
virtual void visit(constant* node) = 0;
virtual void visit(binop* node) = 0;
virtual void visit(unop* node) = 0;
virtual void visit(multop* node) = 0;
virtual void visit(automatop* node) = 0;
virtual void visit(bunop* node) = 0;
};
/// \brief Formula visitor that cannot modify the formula.
///
/// Writing visitors is the prefered way
/// to traverse a formula, since it doesn't
/// involve any cast.
///
/// If you want to modify the visited formula, inherit from
/// spot::ltl:visitor instead.
struct const_visitor
{
virtual ~const_visitor() {}
virtual void visit(const atomic_prop* node) = 0; virtual void visit(const atomic_prop* node) = 0;
virtual void visit(const constant* node) = 0; virtual void visit(const constant* node) = 0;
virtual void visit(const binop* node) = 0; virtual void visit(const binop* node) = 0;
@ -72,8 +49,6 @@ namespace spot
virtual void visit(const automatop* node) = 0; virtual void visit(const automatop* node) = 0;
virtual void visit(const bunop* node) = 0; virtual void visit(const bunop* node) = 0;
}; };
} }
} }

View file

@ -1,4 +1,4 @@
// Copyright (C) 2009 Laboratoire de Recherche et Développement // Copyright (C) 2009, 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -47,7 +47,7 @@ namespace spot
return true; return true;
} }
ltl::formula* const formula*
declarative_environment::require(const std::string& prop_str) declarative_environment::require(const std::string& prop_str)
{ {
prop_map::iterator i = props_.find(prop_str); prop_map::iterator i = props_.find(prop_str);

View file

@ -1,7 +1,8 @@
// Copyright (C) 2009 Laboratoire de Recherche et Développement // -*- coding: utf-8 -*-
// Copyright (C) 2009, 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -49,12 +50,12 @@ namespace spot
/// proposition was already declared. /// proposition was already declared.
bool declare(const std::string& prop_str); bool declare(const std::string& prop_str);
virtual ltl::formula* require(const std::string& prop_str); virtual const formula* require(const std::string& prop_str);
/// Get the name of the environment. /// Get the name of the environment.
virtual const std::string& name(); virtual const std::string& name();
typedef std::map<const std::string, ltl::atomic_prop*> prop_map; typedef std::map<const std::string, const atomic_prop*> prop_map;
/// Get the map of atomic proposition known to this environment. /// Get the map of atomic proposition known to this environment.
const prop_map& get_prop_map() const; const prop_map& get_prop_map() const;

View file

@ -1,5 +1,8 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -31,7 +34,7 @@ namespace spot
{ {
} }
formula* const formula*
default_environment::require(const std::string& s) default_environment::require(const std::string& s)
{ {
return atomic_prop::instance(s, *this); return atomic_prop::instance(s, *this);

View file

@ -1,5 +1,8 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -40,7 +43,7 @@ namespace spot
{ {
public: public:
virtual ~default_environment(); virtual ~default_environment();
virtual formula* require(const std::string& prop_str); virtual const formula* require(const std::string& prop_str);
virtual const std::string& name(); virtual const std::string& name();
/// Get the sole instance of spot::ltl::default_environment. /// Get the sole instance of spot::ltl::default_environment.

View file

@ -1,4 +1,4 @@
// Copyright (C) 2008 Laboratoire de Recherche et Développement // Copyright (C) 2008, 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@ -53,7 +53,7 @@ namespace spot
/// ///
/// \return 0 iff \a prop_str is not part of the environment, /// \return 0 iff \a prop_str is not part of the environment,
/// or the associated spot::ltl::formula otherwise. /// or the associated spot::ltl::formula otherwise.
virtual formula* require(const std::string& prop_str) = 0; virtual const formula* require(const std::string& prop_str) = 0;
/// Get the name of the environment. /// Get the name of the environment.
virtual const std::string& name() = 0; virtual const std::string& name() = 0;

View file

@ -1,4 +1,4 @@
// Copyright (C) 2010 Laboratoire de Recherche et Développement // Copyright (C) 2010, 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -46,7 +46,7 @@ namespace spot
} }
} }
formula* ltl_file::next() const formula* ltl_file::next()
{ {
if (!in.good()) if (!in.good())
return 0; return 0;
@ -60,7 +60,7 @@ namespace spot
while (input == ""); while (input == "");
spot::ltl::parse_error_list pel; spot::ltl::parse_error_list pel;
formula* f = parse(input, pel); const formula* f = parse(input, pel);
int ret = spot::ltl::format_parse_errors(std::cerr, input, pel); int ret = spot::ltl::format_parse_errors(std::cerr, input, pel);
if (ret) if (ret)
exit(ret); exit(ret);

View file

@ -1,4 +1,4 @@
// Copyright (C) 2010 Laboratoire de Recherche et Développement // Copyright (C) 2010, 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -37,7 +37,7 @@ namespace spot
ltl_file(const std::string& filename); ltl_file(const std::string& filename);
ltl_file(const char* filename); ltl_file(const char* filename);
/// Return the next parsed LTL formula, and 0 at end of file. /// Return the next parsed LTL formula, and 0 at end of file.
formula* next(); const formula* next();
private: private:
std::ifstream in; std::ifstream in;
}; };

View file

@ -41,11 +41,11 @@
%parse-param {spot::ltl::parse_error_list &error_list} %parse-param {spot::ltl::parse_error_list &error_list}
%parse-param {spot::ltl::environment &parse_environment} %parse-param {spot::ltl::environment &parse_environment}
%parse-param {spot::ltl::formula* &result} %parse-param {const spot::ltl::formula* &result}
%union %union
{ {
std::string* str; std::string* str;
spot::ltl::formula* ltl; const spot::ltl::formula* ltl;
unsigned num; unsigned num;
minmax_t minmax; minmax_t minmax;
} }
@ -671,13 +671,13 @@ namespace spot
{ {
namespace ltl namespace ltl
{ {
formula* const formula*
parse(const std::string& ltl_string, parse(const std::string& ltl_string,
parse_error_list& error_list, parse_error_list& error_list,
environment& env, environment& env,
bool debug) bool debug)
{ {
formula* result = 0; const formula* result = 0;
flex_set_buffer(ltl_string.c_str(), flex_set_buffer(ltl_string.c_str(),
ltlyy::parser::token::START_LTL); ltlyy::parser::token::START_LTL);
ltlyy::parser parser(error_list, env, result); ltlyy::parser parser(error_list, env, result);
@ -686,13 +686,13 @@ namespace spot
return result; return result;
} }
formula* const formula*
parse_sere(const std::string& sere_string, parse_sere(const std::string& sere_string,
parse_error_list& error_list, parse_error_list& error_list,
environment& env, environment& env,
bool debug) bool debug)
{ {
formula* result = 0; const formula* result = 0;
flex_set_buffer(sere_string.c_str(), flex_set_buffer(sere_string.c_str(),
ltlyy::parser::token::START_SERE); ltlyy::parser::token::START_SERE);
ltlyy::parser parser(error_list, env, result); ltlyy::parser parser(error_list, env, result);

View file

@ -67,10 +67,10 @@ namespace spot
/// was parsed succesfully, check \a error_list for emptiness. /// was parsed succesfully, check \a error_list for emptiness.
/// ///
/// \warning This function is not reentrant. /// \warning This function is not reentrant.
formula* parse(const std::string& ltl_string, const formula* parse(const std::string& ltl_string,
parse_error_list& error_list, parse_error_list& error_list,
environment& env = default_environment::instance(), environment& env = default_environment::instance(),
bool debug = false); bool debug = false);
/// \brief Build a formula from a string representing a SERE. /// \brief Build a formula from a string representing a SERE.
/// \param sere_string The string to parse. /// \param sere_string The string to parse.
@ -87,10 +87,11 @@ namespace spot
/// was parsed succesfully, check \a error_list for emptiness. /// was parsed succesfully, check \a error_list for emptiness.
/// ///
/// \warning This function is not reentrant. /// \warning This function is not reentrant.
formula* parse_sere(const std::string& sere_string, const formula* parse_sere(const std::string& sere_string,
parse_error_list& error_list, parse_error_list& error_list,
environment& env = default_environment::instance(), environment& env =
bool debug = false); default_environment::instance(),
bool debug = false);
/// \brief Format diagnostics produced by spot::ltl::parse /// \brief Format diagnostics produced by spot::ltl::parse
/// or spot::ltl::ratexp /// or spot::ltl::ratexp

View file

@ -1,5 +1,6 @@
// Copyright (C) 2010, 2011 Laboratoire de Recherche et Developement // -*- coding: utf-8 -*-
// de l'Epita (LRDE). // Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et
// Dévelopement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -38,7 +39,7 @@ main(int argc, char **argv)
syntax(argv[0]); syntax(argv[0]);
spot::ltl::parse_error_list p1; spot::ltl::parse_error_list p1;
spot::ltl::formula* f1 = spot::ltl::parse_sere(argv[1], p1); const spot::ltl::formula* f1 = spot::ltl::parse_sere(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;

View file

@ -1,8 +1,9 @@
// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et // -*- coding: utf-8 -*-
// Développement de l'Epita (LRDE). // Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de // Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -57,13 +58,13 @@ main(int argc, char** argv)
syntax(argv[0]); syntax(argv[0]);
spot::ltl::parse_error_list p1; spot::ltl::parse_error_list p1;
spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1); const spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1);
if (check_first && spot::ltl::format_parse_errors(std::cerr, argv[1], p1)) if (check_first && 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::formula* f2 = spot::ltl::parse(argv[2], p2); const 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;
@ -72,7 +73,7 @@ main(int argc, char** argv)
{ {
#if (defined LUNABBREV) || (defined TUNABBREV) || (defined NENOFORM) #if (defined LUNABBREV) || (defined TUNABBREV) || (defined NENOFORM)
spot::ltl::formula* tmp; const spot::ltl::formula* tmp;
#endif #endif
#ifdef LUNABBREV #ifdef LUNABBREV
tmp = f1; tmp = f1;
@ -99,7 +100,7 @@ main(int argc, char** argv)
spot::ltl::ltl_simplifier_options opt(true, true, true, false, false); spot::ltl::ltl_simplifier_options opt(true, true, true, false, false);
spot::ltl::ltl_simplifier simp(opt); spot::ltl::ltl_simplifier simp(opt);
{ {
spot::ltl::formula* tmp; const spot::ltl::formula* tmp;
tmp = f1; tmp = f1;
f1 = simp.simplify(f1); f1 = simp.simplify(f1);
tmp->destroy(); tmp->destroy();
@ -111,7 +112,7 @@ main(int argc, char** argv)
spot::ltl::ltl_simplifier_options opt(false, false, false, true, false); spot::ltl::ltl_simplifier_options opt(false, false, false, true, false);
spot::ltl::ltl_simplifier simp(opt); spot::ltl::ltl_simplifier simp(opt);
{ {
spot::ltl::formula* tmp; const spot::ltl::formula* tmp;
tmp = f1; tmp = f1;
f1 = simp.simplify(f1); f1 = simp.simplify(f1);
tmp->destroy(); tmp->destroy();
@ -123,7 +124,7 @@ main(int argc, char** argv)
spot::ltl::ltl_simplifier_options opt(false, false, false, true, true); spot::ltl::ltl_simplifier_options opt(false, false, false, true, true);
spot::ltl::ltl_simplifier simp(opt); spot::ltl::ltl_simplifier simp(opt);
{ {
spot::ltl::formula* tmp; const spot::ltl::formula* tmp;
tmp = f1; tmp = f1;
f1 = simp.simplify(f1); f1 = simp.simplify(f1);
tmp->destroy(); tmp->destroy();

View file

@ -1,5 +1,6 @@
// Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement de // -*- coding: utf-8 -*-
// l'Epita (LRDE). // Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -155,18 +156,18 @@ to_int(const char* s)
// F(p_1 & F(p_2 & F(p_3 & ... F(p_n)))) // F(p_1 & F(p_2 & F(p_3 & ... F(p_n))))
formula* E_n(std::string name, int n) const formula* E_n(std::string name, int n)
{ {
if (n <= 0) if (n <= 0)
return constant::true_instance(); return constant::true_instance();
formula* result = 0; const formula* result = 0;
for (; n > 0; --n) for (; n > 0; --n)
{ {
std::ostringstream p; std::ostringstream p;
p << name << n; p << name << n;
formula* f = env.require(p.str()); const formula* f = env.require(p.str());
if (result) if (result)
result = And_(f, result); result = And_(f, result);
else else
@ -177,13 +178,13 @@ formula* E_n(std::string name, int n)
} }
// p & X(p & X(p & ... X(p))) // p & X(p & X(p & ... X(p)))
formula* phi_n(std::string name, int n) const formula* phi_n(std::string name, int n)
{ {
if (n <= 0) if (n <= 0)
return constant::true_instance(); return constant::true_instance();
formula* result = 0; const formula* result = 0;
formula* p = env.require(name); const formula* p = env.require(name);
for (; n > 0; --n) for (; n > 0; --n)
{ {
if (result) if (result)
@ -194,19 +195,19 @@ formula* phi_n(std::string name, int n)
return result; return result;
} }
formula* N_n(std::string name, int n) const formula* N_n(std::string name, int n)
{ {
return unop::instance(unop::F, phi_n(name, n)); return unop::instance(unop::F, phi_n(name, n));
} }
// p & X(p) & XX(p) & XXX(p) & ... X^n(p) // p & X(p) & XX(p) & XXX(p) & ... X^n(p)
formula* phi_prime_n(std::string name, int n) const formula* phi_prime_n(std::string name, int n)
{ {
if (n <= 0) if (n <= 0)
return constant::true_instance(); return constant::true_instance();
formula* result = 0; const formula* result = 0;
formula* p = env.require(name); const formula* p = env.require(name);
for (; n > 0; --n) for (; n > 0; --n)
{ {
if (result) if (result)
@ -222,7 +223,7 @@ formula* phi_prime_n(std::string name, int n)
return result; return result;
} }
formula* N_prime_n(std::string name, int n) const formula* N_prime_n(std::string name, int n)
{ {
return F_(phi_prime_n(name, n)); return F_(phi_prime_n(name, n));
} }
@ -230,12 +231,12 @@ formula* N_prime_n(std::string name, int n)
// GF(p_1) & GF(p_2) & ... & GF(p_n) if conj == true // GF(p_1) & GF(p_2) & ... & GF(p_n) if conj == true
// GF(p_1) | GF(p_2) | ... | GF(p_n) if conj == false // GF(p_1) | GF(p_2) | ... | GF(p_n) if conj == false
formula* GF_n(std::string name, int n, bool conj = true) const formula* GF_n(std::string name, int n, bool conj = true)
{ {
if (n <= 0) if (n <= 0)
return conj ? constant::true_instance() : constant::false_instance(); return conj ? constant::true_instance() : constant::false_instance();
formula* result = 0; const formula* result = 0;
multop::type op = conj ? multop::And : multop::Or; multop::type op = conj ? multop::And : multop::Or;
@ -243,7 +244,7 @@ formula* GF_n(std::string name, int n, bool conj = true)
{ {
std::ostringstream p; std::ostringstream p;
p << name << i; p << name << i;
formula* f = G_(F_(env.require(p.str()))); const formula* f = G_(F_(env.require(p.str())));
if (result) if (result)
result = multop::instance(op, f, result); result = multop::instance(op, f, result);
@ -255,12 +256,12 @@ formula* GF_n(std::string name, int n, bool conj = true)
// FG(p_1) | FG(p_2) | ... | FG(p_n) if conj == false // FG(p_1) | FG(p_2) | ... | FG(p_n) if conj == false
// FG(p_1) & FG(p_2) & ... & FG(p_n) if conj == true // FG(p_1) & FG(p_2) & ... & FG(p_n) if conj == true
formula* FG_n(std::string name, int n, bool conj = false) const formula* FG_n(std::string name, int n, bool conj = false)
{ {
if (n <= 0) if (n <= 0)
return conj ? constant::true_instance() : constant::false_instance(); return conj ? constant::true_instance() : constant::false_instance();
formula* result = 0; const formula* result = 0;
multop::type op = conj ? multop::And : multop::Or; multop::type op = conj ? multop::And : multop::Or;
@ -268,7 +269,7 @@ formula* FG_n(std::string name, int n, bool conj = false)
{ {
std::ostringstream p; std::ostringstream p;
p << name << i; p << name << i;
formula* f = F_(G_(env.require(p.str()))); const formula* f = F_(G_(env.require(p.str())));
if (result) if (result)
result = multop::instance(op, f, result); result = multop::instance(op, f, result);
@ -280,8 +281,9 @@ formula* FG_n(std::string name, int n, bool conj = false)
// (((p1 OP p2) OP p3)...OP pn) if right_assoc == false // (((p1 OP p2) OP p3)...OP pn) if right_assoc == false
// (p1 OP (p2 OP (p3 OP (... pn) if right_assoc == true // (p1 OP (p2 OP (p3 OP (... pn) if right_assoc == true
formula* bin_n(std::string name, int n, const formula*
binop::type op, bool right_assoc = false) bin_n(std::string name, int n,
binop::type op, bool right_assoc = false)
{ {
if (n <= 0) if (n <= 0)
{ {
@ -289,13 +291,13 @@ formula* bin_n(std::string name, int n,
exit(1); exit(1);
} }
formula* result = 0; const formula* result = 0;
for (int i = 1; i <= n; ++i) for (int i = 1; i <= n; ++i)
{ {
std::ostringstream p; std::ostringstream p;
p << name << (right_assoc ? (n + 1 - i) : i); p << name << (right_assoc ? (n + 1 - i) : i);
formula* f = env.require(p.str()); const formula* f = env.require(p.str());
if (!result) if (!result)
result = f; result = f;
else if (right_assoc) else if (right_assoc)
@ -307,12 +309,12 @@ formula* bin_n(std::string name, int n,
} }
// (GF(p1)|FG(p2))&(GF(p2)|FG(p3))&...&(GF(pn)|FG(p{n+1}))" // (GF(p1)|FG(p2))&(GF(p2)|FG(p3))&...&(GF(pn)|FG(p{n+1}))"
formula* R_n(std::string name, int n) const formula* R_n(std::string name, int n)
{ {
if (n <= 0) if (n <= 0)
return constant::true_instance(); return constant::true_instance();
formula* pi; const formula* pi;
{ {
std::ostringstream p; std::ostringstream p;
@ -320,18 +322,18 @@ formula* R_n(std::string name, int n)
pi = env.require(p.str()); pi = env.require(p.str());
} }
formula* result = 0; const formula* result = 0;
for (int i = 1; i <= n; ++i) for (int i = 1; i <= n; ++i)
{ {
formula* gf = G_(F_(pi)); const formula* gf = G_(F_(pi));
std::ostringstream p; std::ostringstream p;
p << name << i + 1; p << name << i + 1;
pi = env.require(p.str()); pi = env.require(p.str());
formula* fg = G_(F_(pi->clone())); const formula* fg = G_(F_(pi->clone()));
formula* f = Or_(gf, fg); const formula* f = Or_(gf, fg);
if (result) if (result)
result = And_(f, result); result = And_(f, result);
@ -343,12 +345,12 @@ formula* R_n(std::string name, int n)
} }
// (F(p1)|G(p2))&(F(p2)|G(p3))&...&(F(pn)|G(p{n+1}))" // (F(p1)|G(p2))&(F(p2)|G(p3))&...&(F(pn)|G(p{n+1}))"
formula* Q_n(std::string name, int n) const formula* Q_n(std::string name, int n)
{ {
if (n <= 0) if (n <= 0)
return constant::true_instance(); return constant::true_instance();
formula* pi; const formula* pi;
{ {
std::ostringstream p; std::ostringstream p;
@ -356,17 +358,17 @@ formula* Q_n(std::string name, int n)
pi = env.require(p.str()); pi = env.require(p.str());
} }
formula* result = 0; const formula* result = 0;
for (int i = 1; i <= n; ++i) for (int i = 1; i <= n; ++i)
{ {
formula* f = F_(pi); const formula* f = F_(pi);
std::ostringstream p; std::ostringstream p;
p << name << i + 1; p << name << i + 1;
pi = env.require(p.str()); pi = env.require(p.str());
formula* g = G_(pi->clone()); const formula* g = G_(pi->clone());
f = Or_(f, g); f = Or_(f, g);
@ -381,13 +383,13 @@ formula* Q_n(std::string name, int n)
// OP(p1) | OP(p2) | ... | OP(Pn) if conj == false // OP(p1) | OP(p2) | ... | OP(Pn) if conj == false
// OP(p1) & OP(p2) & ... & OP(Pn) if conj == true // OP(p1) & OP(p2) & ... & OP(Pn) if conj == true
formula* combunop_n(std::string name, int n, const formula* combunop_n(std::string name, int n,
unop::type op, bool conj = false) unop::type op, bool conj = false)
{ {
if (n <= 0) if (n <= 0)
return conj ? constant::true_instance() : constant::false_instance(); return conj ? constant::true_instance() : constant::false_instance();
formula* result = 0; const formula* result = 0;
multop::type cop = conj ? multop::And : multop::Or; multop::type cop = conj ? multop::And : multop::Or;
@ -395,7 +397,7 @@ formula* combunop_n(std::string name, int n,
{ {
std::ostringstream p; std::ostringstream p;
p << name << i; p << name << i;
formula* f = unop::instance(op, env.require(p.str())); const formula* f = unop::instance(op, env.require(p.str()));
if (result) if (result)
result = multop::instance(cop, f, result); result = multop::instance(cop, f, result);
@ -406,20 +408,21 @@ formula* combunop_n(std::string name, int n,
} }
// !((GF(p1)&GF(p2)&...&GF(pn))->G(q -> F(r))) // !((GF(p1)&GF(p2)&...&GF(pn))->G(q -> F(r)))
// From "Fast LTL to Büchi Automata Translation" [gastin.01.cav] // From "Fast LTL to Büchi Automata Translation" [gastin.01.cav]
formula* fair_response(std::string p, std::string q, std::string r, int n) const formula*
fair_response(std::string p, std::string q, std::string r, int n)
{ {
formula* fair = GF_n(p, n); const formula* fair = GF_n(p, n);
formula* resp = G_(Implies_(env.require(q), F_(env.require(r)))); const formula* resp = G_(Implies_(env.require(q), F_(env.require(r))));
return Not_(Implies_(fair, resp)); return Not_(Implies_(fair, resp));
} }
// Builds X(X(...X(p))) with n occurrences of X. // Builds X(X(...X(p))) with n occurrences of X.
formula* X_n(formula* p, int n) const formula* X_n(const formula* p, int n)
{ {
assert(n >= 0); assert(n >= 0);
formula* res = p; const formula* res = p;
while (n--) while (n--)
res = X_(res); res = X_(res);
return res; return res;
@ -427,13 +430,13 @@ formula* X_n(formula* p, int n)
// Based on LTLcounter.pl from Kristin Rozier. // Based on LTLcounter.pl from Kristin Rozier.
// http://shemesh.larc.nasa.gov/people/kyr/benchmarking_scripts/ // http://shemesh.larc.nasa.gov/people/kyr/benchmarking_scripts/
const formula*
formula* ltl_counter(std::string bit, std::string marker, int n, bool linear) ltl_counter(std::string bit, std::string marker, int n, bool linear)
{ {
formula* b = env.require(bit); const formula* b = env.require(bit);
formula* neg_b = Not_(b); const formula* neg_b = Not_(b);
formula* m = env.require(marker); const formula* m = env.require(marker);
formula* neg_m = Not_(m); // to destroy const formula* neg_m = Not_(m); // to destroy
multop::vec* res = new multop::vec(4); multop::vec* res = new multop::vec(4);
@ -453,7 +456,7 @@ formula* ltl_counter(std::string bit, std::string marker, int n, bool linear)
else else
{ {
// G(m -> X(!m & X(!m X(m)))) [if n = 3] // G(m -> X(!m & X(!m X(m)))) [if n = 3]
formula* p = m->clone(); const formula* p = m->clone();
for (int i = n - 1; i > 0; --i) for (int i = n - 1; i > 0; --i)
p = And_(neg_m->clone(), X_(p)); p = And_(neg_m->clone(), X_(p));
(*res)[0] = And_(m->clone(), (*res)[0] = And_(m->clone(),
@ -472,7 +475,7 @@ formula* ltl_counter(std::string bit, std::string marker, int n, bool linear)
else else
{ {
// !b & X(!b & X(!b)) [if n = 3] // !b & X(!b & X(!b)) [if n = 3]
formula* p = neg_b->clone(); const formula* p = neg_b->clone();
for (int i = n - 1; i > 0; --i) for (int i = n - 1; i > 0; --i)
p = And_(neg_b->clone(), X_(p)); p = And_(neg_b->clone(), X_(p));
(*res)[1] = p; (*res)[1] = p;
@ -482,8 +485,8 @@ formula* ltl_counter(std::string bit, std::string marker, int n, bool linear)
// If the least significant bit is 0, it will be 1 at the next time, // If the least significant bit is 0, it will be 1 at the next time,
// and other bits stay the same. // and other bits stay the same.
formula* Xnm1_b = X_n(b->clone(), n - 1); const formula* Xnm1_b = X_n(b->clone(), n - 1);
formula* Xn_b = X_(Xnm1_b); // to destroy const formula* Xn_b = X_(Xnm1_b); // to destroy
(*res)[2] = (*res)[2] =
G_(Implies_(And_(m->clone(), neg_b->clone()), G_(Implies_(And_(m->clone(), neg_b->clone()),
AndX_(Xnm1_b->clone(), U_(And_(Not_(m->clone()), AndX_(Xnm1_b->clone(), U_(And_(Not_(m->clone()),
@ -493,8 +496,8 @@ formula* ltl_counter(std::string bit, std::string marker, int n, bool linear)
// From the least significant bit to the first 0, all the bits // From the least significant bit to the first 0, all the bits
// are flipped on the next value. Remaining bits are identical. // are flipped on the next value. Remaining bits are identical.
formula* Xnm1_negb = X_n(neg_b, n - 1); const formula* Xnm1_negb = X_n(neg_b, n - 1);
formula* Xn_negb = X_(Xnm1_negb); // to destroy const formula* Xn_negb = X_(Xnm1_negb); // to destroy
(*res)[3] = (*res)[3] =
G_(Implies_(And_(m->clone(), b->clone()), G_(Implies_(And_(m->clone(), b->clone()),
AndX_(Xnm1_negb->clone(), AndX_(Xnm1_negb->clone(),
@ -515,15 +518,15 @@ formula* ltl_counter(std::string bit, std::string marker, int n, bool linear)
return multop::instance(multop::And, res); return multop::instance(multop::And, res);
} }
formula* ltl_counter_carry(std::string bit, std::string marker, const formula* ltl_counter_carry(std::string bit, std::string marker,
std::string carry, int n, bool linear) std::string carry, int n, bool linear)
{ {
formula* b = env.require(bit); const formula* b = env.require(bit);
formula* neg_b = Not_(b); const formula* neg_b = Not_(b);
formula* m = env.require(marker); const formula* m = env.require(marker);
formula* neg_m = Not_(m); // to destroy const formula* neg_m = Not_(m); // to destroy
formula* c = env.require(carry); const formula* c = env.require(carry);
formula* neg_c = Not_(c); // to destroy const formula* neg_c = Not_(c); // to destroy
multop::vec* res = new multop::vec(6); multop::vec* res = new multop::vec(6);
@ -543,7 +546,7 @@ formula* ltl_counter_carry(std::string bit, std::string marker,
else else
{ {
// G(m -> X(!m & X(!m X(m)))) [if n = 3] // G(m -> X(!m & X(!m X(m)))) [if n = 3]
formula* p = m->clone(); const formula* p = m->clone();
for (int i = n - 1; i > 0; --i) for (int i = n - 1; i > 0; --i)
p = And_(neg_m->clone(), X_(p)); p = And_(neg_m->clone(), X_(p));
(*res)[0] = And_(m->clone(), (*res)[0] = And_(m->clone(),
@ -562,14 +565,14 @@ formula* ltl_counter_carry(std::string bit, std::string marker,
else else
{ {
// !b & X(!b & X(!b)) [if n = 3] // !b & X(!b & X(!b)) [if n = 3]
formula* p = neg_b->clone(); const formula* p = neg_b->clone();
for (int i = n - 1; i > 0; --i) for (int i = n - 1; i > 0; --i)
p = And_(neg_b->clone(), X_(p)); p = And_(neg_b->clone(), X_(p));
(*res)[1] = p; (*res)[1] = p;
} }
formula* Xn_b = X_n(b->clone(), n); // to destroy const formula* Xn_b = X_n(b->clone(), n); // to destroy
formula* Xn_negb = X_n(neg_b, n); // to destroy const formula* Xn_negb = X_n(neg_b, n); // to destroy
// If m is 1 and b is 0 then c is 0 and n steps later b is 1. // If m is 1 and b is 0 then c is 0 and n steps later b is 1.
(*res)[2] = G_(Implies_(And_(m->clone(), neg_b->clone()), (*res)[2] = G_(Implies_(And_(m->clone(), neg_b->clone()),
@ -642,7 +645,7 @@ main(int argc, char** argv)
int f = to_int(argv[1]); int f = to_int(argv[1]);
int n = to_int(argv[2]); int n = to_int(argv[2]);
formula* res = 0; const formula* res = 0;
switch (f) switch (f)
{ {

View file

@ -1,4 +1,5 @@
// Copyright (C) 2010 Laboratoire de Recherche et Developement de // -*- coding: utf-8 -*-
// Copyright (C) 2010, 2012 Laboratoire de Recherche et Developement de
// l'Epita (LRDE). // l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -38,7 +39,7 @@ main(int argc, char **argv)
syntax(argv[0]); syntax(argv[0]);
spot::ltl::parse_error_list p1; spot::ltl::parse_error_list p1;
spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1); const 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;

View file

@ -1,3 +1,4 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012 Laboratoire de Recherche et Developement de // Copyright (C) 2012 Laboratoire de Recherche et Developement de
// l'Epita (LRDE). // l'Epita (LRDE).
// //
@ -47,7 +48,7 @@ main(int argc, char **argv)
} }
spot::ltl::parse_error_list p1; spot::ltl::parse_error_list p1;
spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1); const 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;

View file

@ -185,7 +185,7 @@ main(int argc, char** argv)
} }
else else
{ {
ap->insert(static_cast<spot::ltl::atomic_prop*> ap->insert(static_cast<const spot::ltl::atomic_prop*>
(env.require(argv[argn]))); (env.require(argv[argn])));
} }
} }
@ -310,14 +310,14 @@ main(int argc, char** argv)
while (max_tries_u--) while (max_tries_u--)
{ {
spot::srand(opt_s++); spot::srand(opt_s++);
spot::ltl::formula* f = 0; const spot::ltl::formula* f = 0;
int max_tries_r = 1000; int max_tries_r = 1000;
while (max_tries_r--) while (max_tries_r--)
{ {
f = rf->generate(opt_f); f = rf->generate(opt_f);
if (opt_r) if (opt_r)
{ {
spot::ltl::formula* g = simp.simplify(f); const spot::ltl::formula* g = simp.simplify(f);
f->destroy(); f->destroy();
if (spot::ltl::length(g) < opt_r) if (spot::ltl::length(g) < opt_r)
{ {

View file

@ -1,7 +1,8 @@
// Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement // -*- coding: utf-8 -*-
// de l'Epita (LRDE). // Copyright (C) 2008, 2009, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
// Pierre et Marie Curie. // Pierre et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -76,8 +77,8 @@ main(int argc, char** argv)
spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::ltl::parse_error_list pel; spot::ltl::parse_error_list pel;
spot::ltl::formula* f = spot::ltl::parse(argv[formula_index], const spot::ltl::formula* f = spot::ltl::parse(argv[formula_index],
pel, env, debug); pel, env, debug);
exit_code = exit_code =
spot::ltl::format_parse_errors(std::cerr, argv[formula_index], pel); spot::ltl::format_parse_errors(std::cerr, argv[formula_index], pel);

View file

@ -144,8 +144,8 @@ main(int argc, char** argv)
o.reduce_size_strictly = true; o.reduce_size_strictly = true;
spot::ltl::ltl_simplifier* simp_size = new spot::ltl::ltl_simplifier(o); spot::ltl::ltl_simplifier* simp_size = new spot::ltl::ltl_simplifier(o);
spot::ltl::formula* f1 = 0; const spot::ltl::formula* f1 = 0;
spot::ltl::formula* f2 = 0; const spot::ltl::formula* f2 = 0;
std::ifstream* fin = 0; std::ifstream* fin = 0;
@ -201,7 +201,7 @@ main(int argc, char** argv)
} }
{ {
spot::ltl::formula* ftmp1; const spot::ltl::formula* ftmp1;
ftmp1 = f1; ftmp1 = f1;
f1 = simp_size->negative_normal_form(f1, false); f1 = simp_size->negative_normal_form(f1, false);
@ -211,7 +211,7 @@ main(int argc, char** argv)
std::string f1s_before = spot::ltl::to_string(f1); std::string f1s_before = spot::ltl::to_string(f1);
std::string f1l; std::string f1l;
spot::ltl::formula* input_f = f1; const spot::ltl::formula* input_f = f1;
f1 = simp_size->simplify(input_f); f1 = simp_size->simplify(input_f);
if (!simp_size->are_equivalent(input_f, f1)) if (!simp_size->are_equivalent(input_f, f1))
{ {
@ -222,7 +222,7 @@ main(int argc, char** argv)
} }
else else
{ {
spot::ltl::formula* maybe_larger = simp->simplify(input_f); const spot::ltl::formula* maybe_larger = simp->simplify(input_f);
f1l = spot::ltl::to_string(maybe_larger); f1l = spot::ltl::to_string(maybe_larger);
if (!simp->are_equivalent(input_f, maybe_larger)) if (!simp->are_equivalent(input_f, maybe_larger))
{ {

View file

@ -1,7 +1,8 @@
// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et // -*- coding: utf-8 -*-
// Développement de l'Epita (LRDE). // Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche
// et Développement de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
// Pierre et Marie Curie. // Pierre et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -49,19 +50,19 @@ main(int argc, char** argv)
int opt = atoi(argv[1]); int opt = atoi(argv[1]);
spot::ltl::parse_error_list p1; spot::ltl::parse_error_list p1;
spot::ltl::formula* ftmp1 = spot::ltl::parse(argv[2], p1); const spot::ltl::formula* ftmp1 = spot::ltl::parse(argv[2], p1);
if (spot::ltl::format_parse_errors(std::cerr, argv[2], p1)) if (spot::ltl::format_parse_errors(std::cerr, argv[2], p1))
return 2; return 2;
spot::ltl::parse_error_list p2; spot::ltl::parse_error_list p2;
spot::ltl::formula* ftmp2 = spot::ltl::parse(argv[3], p2); const spot::ltl::formula* ftmp2 = spot::ltl::parse(argv[3], p2);
if (spot::ltl::format_parse_errors(std::cerr, argv[3], p2)) if (spot::ltl::format_parse_errors(std::cerr, argv[3], p2))
return 2; return 2;
spot::ltl::formula* f1 = spot::ltl::negative_normal_form(ftmp1); const spot::ltl::formula* f1 = spot::ltl::negative_normal_form(ftmp1);
spot::ltl::formula* f2 = spot::ltl::negative_normal_form(ftmp2); const spot::ltl::formula* f2 = spot::ltl::negative_normal_form(ftmp2);
std::string f1s = spot::ltl::to_string(f1); std::string f1s = spot::ltl::to_string(f1);
std::string f2s = spot::ltl::to_string(f2); std::string f2s = spot::ltl::to_string(f2);

View file

@ -1,7 +1,8 @@
// Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement // -*- coding: utf-8 -*-
// de l'Epita (LRDE). // Copyright (C) 2008, 2009, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -42,7 +43,7 @@ main(int argc, char **argv)
syntax(argv[0]); syntax(argv[0]);
spot::ltl::parse_error_list p1; spot::ltl::parse_error_list p1;
spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1); const 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;
@ -53,7 +54,7 @@ main(int argc, char **argv)
std::string f1s = spot::ltl::to_string(f1); std::string f1s = spot::ltl::to_string(f1);
std::cout << f1s << std::endl; std::cout << f1s << std::endl;
spot::ltl::formula* f2 = spot::ltl::parse(f1s, p1); const spot::ltl::formula* f2 = spot::ltl::parse(f1s, p1);
if (spot::ltl::format_parse_errors(std::cerr, f1s, p1)) if (spot::ltl::format_parse_errors(std::cerr, f1s, p1))
return 2; return 2;

View file

@ -1,5 +1,8 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -40,7 +43,7 @@ namespace spot
{ {
} }
virtual void doit(spot::ltl::atomic_prop* ap) virtual void doit(const spot::ltl::atomic_prop* ap)
{ {
sap->insert(ap); sap->insert(ap);
} }
@ -56,7 +59,7 @@ namespace spot
if (!s) if (!s)
s = new atomic_prop_set; s = new atomic_prop_set;
atomic_prop_collector v(s); atomic_prop_collector v(s);
const_cast<formula*>(f)->accept(v); f->accept(v);
return s; return s;
} }

View file

@ -1,5 +1,8 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -33,7 +36,8 @@ namespace spot
/// @{ /// @{
/// Set of atomic propositions. /// Set of atomic propositions.
typedef std::set<atomic_prop*, formula_ptr_less_than> atomic_prop_set; typedef std::set<const atomic_prop*,
formula_ptr_less_than> atomic_prop_set;
/// \brief Return the set of atomic propositions occurring in a formula. /// \brief Return the set of atomic propositions occurring in a formula.
/// ///

View file

@ -1,4 +1,4 @@
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement // Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -36,46 +36,46 @@ namespace spot
{ {
} }
formula* const formula*
clone_visitor::result() const clone_visitor::result() const
{ {
return result_; return result_;
} }
void void
clone_visitor::visit(atomic_prop* ap) clone_visitor::visit(const atomic_prop* ap)
{ {
result_ = ap->clone(); result_ = ap->clone();
} }
void void
clone_visitor::visit(constant* c) clone_visitor::visit(const constant* c)
{ {
result_ = c->clone(); result_ = c->clone();
} }
void void
clone_visitor::visit(bunop* bo) clone_visitor::visit(const bunop* bo)
{ {
result_ = bunop::instance(bo->op(), recurse(bo->child()), result_ = bunop::instance(bo->op(), recurse(bo->child()),
bo->min(), bo->max()); bo->min(), bo->max());
} }
void void
clone_visitor::visit(unop* uo) clone_visitor::visit(const unop* uo)
{ {
result_ = unop::instance(uo->op(), recurse(uo->child())); result_ = unop::instance(uo->op(), recurse(uo->child()));
} }
void void
clone_visitor::visit(binop* bo) clone_visitor::visit(const binop* bo)
{ {
result_ = binop::instance(bo->op(), result_ = binop::instance(bo->op(),
recurse(bo->first()), recurse(bo->second())); recurse(bo->first()), recurse(bo->second()));
} }
void void
clone_visitor::visit(automatop* ao) clone_visitor::visit(const automatop* ao)
{ {
automatop::vec* res = new automatop::vec; automatop::vec* res = new automatop::vec;
for (unsigned i = 0; i < ao->size(); ++i) for (unsigned i = 0; i < ao->size(); ++i)
@ -84,7 +84,7 @@ namespace spot
} }
void void
clone_visitor::visit(multop* mo) clone_visitor::visit(const multop* mo)
{ {
multop::vec* res = new multop::vec; multop::vec* res = new multop::vec;
unsigned mos = mo->size(); unsigned mos = mo->size();
@ -93,17 +93,16 @@ namespace spot
result_ = multop::instance(mo->op(), res); result_ = multop::instance(mo->op(), res);
} }
formula* const formula*
clone_visitor::recurse(formula* f) clone_visitor::recurse(const formula* f)
{ {
return f->clone(); return f->clone();
} }
formula* const formula*
clone(const formula* f) clone(const formula* f)
{ {
formula* res = const_cast<formula*>(f)->clone(); return f->clone();
return res;
} }
} }
} }

View file

@ -1,7 +1,8 @@
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement // -*- coding: utf-8 -*-
// de l'Epita (LRDE). // Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -44,32 +45,32 @@ namespace spot
clone_visitor(); clone_visitor();
virtual ~clone_visitor(); virtual ~clone_visitor();
formula* result() const; const formula* result() const;
void visit(atomic_prop* ap); void visit(const atomic_prop* ap);
void visit(unop* uo); void visit(const unop* uo);
void visit(binop* bo); void visit(const binop* bo);
void visit(automatop* mo); void visit(const automatop* mo);
void visit(multop* mo); void visit(const multop* mo);
void visit(constant* c); void visit(const constant* c);
void visit(bunop* c); void visit(const bunop* c);
virtual formula* recurse(formula* f); virtual const formula* recurse(const formula* f);
protected: protected:
formula* result_; const formula* result_;
}; };
#if __GNUC__ #if __GNUC__
/// \brief Clone a formula. /// \brief Clone a formula.
/// \ingroup ltl_essential /// \ingroup ltl_essential
/// \deprecated Use f->clone() instead. /// \deprecated Use f->clone() instead.
formula* clone(const formula* f) __attribute__ ((deprecated)); const formula* clone(const formula* f) __attribute__ ((deprecated));
#else #else
/// \brief Clone a formula. /// \brief Clone a formula.
/// \ingroup ltl_essential /// \ingroup ltl_essential
/// \deprecated Use f->clone() instead. /// \deprecated Use f->clone() instead.
formula* clone(const formula* f); const formula* clone(const formula* f);
#endif #endif
} }
} }

View file

@ -1,7 +1,8 @@
// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement // -*- coding: utf-8 -*-
// de l'Epita (LRDE). // Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2006, 2007 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2006, 2007 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -87,7 +88,8 @@ namespace spot
// Check whether L(l) is a subset of L(g). // Check whether L(l) is a subset of L(g).
bool bool
language_containment_checker::contained(const formula* l, const formula* g) language_containment_checker::contained(const formula* l,
const formula* g)
{ {
if (l == g) if (l == g)
return true; return true;
@ -153,7 +155,7 @@ namespace spot
} }
formula* const formula*
reduce_tau03(const formula* f, bool stronger) reduce_tau03(const formula* f, bool stronger)
{ {
if (!f->is_psl_formula()) if (!f->is_psl_formula())

View file

@ -1,4 +1,4 @@
// Copyright (C) 2011 Laboratoire de Recherche et Developpement de // Copyright (C) 2011, 2012 Laboratoire de Recherche et Developpement de
// l'Epita (LRDE). // l'Epita (LRDE).
// Copyright (C) 2006 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2006 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -88,10 +88,10 @@ namespace spot
/// title = {On Translating Linear Temporal Logic into Alternating and /// title = {On Translating Linear Temporal Logic into Alternating and
/// Nondeterministic Automata}, /// Nondeterministic Automata},
/// institution = {Helsinki University of Technology, Laboratory for /// institution = {Helsinki University of Technology, Laboratory for
/// Theoretical Computer Science}, /// Theoretical Computer Science},
/// address = {Espoo, Finland}, /// address = {Espoo, Finland},
/// month = dec, /// month = dec,
/// number = {A83}, /// number = {A83},
/// pages = {132}, /// pages = {132},
/// type = {Research Report}, /// type = {Research Report},
/// year = {2003}, /// year = {2003},
@ -106,10 +106,11 @@ namespace spot
/// ///
/// \deprecated Use spot::ltl::ltl_simplifier instead. /// \deprecated Use spot::ltl::ltl_simplifier instead.
#if __GNUC__ #if __GNUC__
formula* reduce_tau03(const formula* f, const formula* reduce_tau03(const formula* f,
bool stronger = true) __attribute__ ((deprecated)); bool stronger = true)
__attribute__ ((deprecated));
#else #else
formula* reduce_tau03(const formula* f, bool stronger = true); const formula* reduce_tau03(const formula* f, bool stronger = true);
#endif #endif
} }
} }

View file

@ -35,7 +35,7 @@ namespace spot
{ {
namespace namespace
{ {
class dotty_visitor: public const_visitor class dotty_visitor: public visitor
{ {
public: public:
typedef Sgi::hash_map<const formula*, int, ptr_hash<formula> > map; typedef Sgi::hash_map<const formula*, int, ptr_hash<formula> > map;

View file

@ -47,7 +47,7 @@ namespace spot
} }
virtual void virtual void
visit(multop* mo) visit(const multop* mo)
{ {
unsigned s = mo->size(); unsigned s = mo->size();
for (unsigned i = 0; i < s; ++i) for (unsigned i = 0; i < s; ++i)
@ -58,7 +58,7 @@ namespace spot
} }
virtual void virtual void
doit_default(formula*) doit_default(const formula*)
{ {
++result_; ++result_;
} }
@ -71,7 +71,7 @@ namespace spot
{ {
virtual void virtual void
visit(unop* uo) visit(const unop* uo)
{ {
++result_; ++result_;
// Boolean formula have length one. // Boolean formula have length one.
@ -80,7 +80,7 @@ namespace spot
} }
virtual void virtual void
visit(multop* mo) visit(const multop* mo)
{ {
// Boolean formula have length one. // Boolean formula have length one.
if (mo->is_boolean()) if (mo->is_boolean())
@ -104,7 +104,7 @@ namespace spot
length(const formula* f) length(const formula* f)
{ {
length_visitor v; length_visitor v;
const_cast<formula*>(f)->accept(v); f->accept(v);
return v.result(); return v.result();
} }
@ -112,7 +112,7 @@ namespace spot
length_boolone(const formula* f) length_boolone(const formula* f)
{ {
length_boolone_visitor v; length_boolone_visitor v;
const_cast<formula*>(f)->accept(v); f->accept(v);
return v.result(); return v.result();
} }

View file

@ -1,7 +1,8 @@
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement // -*- coding: utf-8 -*-
// de l'Epita (LRDE). // Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// d�partement Syst�mes R�partis Coop�ratifs (SRC), Universit� Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -39,10 +40,10 @@ namespace spot
} }
void void
unabbreviate_logic_visitor::visit(binop* bo) unabbreviate_logic_visitor::visit(const binop* bo)
{ {
formula* f1 = recurse(bo->first()); const formula* f1 = recurse(bo->first());
formula* f2 = recurse(bo->second()); const formula* f2 = recurse(bo->second());
binop::type op = bo->op(); binop::type op = bo->op();
switch (op) switch (op)
@ -50,11 +51,12 @@ namespace spot
/* f1 ^ f2 == (f1 & !f2) | (f2 & !f1) */ /* f1 ^ f2 == (f1 & !f2) | (f2 & !f1) */
case binop::Xor: case binop::Xor:
{ {
formula* a = multop::instance(multop::And, f1->clone(), const formula* a =
unop::instance(unop::Not, multop::instance(multop::And, f1->clone(),
f2->clone())); unop::instance(unop::Not, f2->clone()));
formula* b = multop::instance(multop::And, f2, const formula* b =
unop::instance(unop::Not, f1)); multop::instance(multop::And, f2,
unop::instance(unop::Not, f1));
result_ = multop::instance(multop::Or, a, b); result_ = multop::instance(multop::Or, a, b);
return; return;
} }
@ -66,8 +68,8 @@ namespace spot
/* f1 <=> f2 == (f1 & f2) | (!f1 & !f2) */ /* f1 <=> f2 == (f1 & f2) | (!f1 & !f2) */
case binop::Equiv: case binop::Equiv:
{ {
formula* f1c = f1->clone(); const formula* f1c = f1->clone();
formula* f2c = f2->clone(); const formula* f2c = f2->clone();
result_ = result_ =
multop::instance(multop::Or, multop::instance(multop::Or,
@ -97,19 +99,19 @@ namespace spot
assert(0); assert(0);
} }
formula* const formula*
unabbreviate_logic_visitor::recurse(formula* f) unabbreviate_logic_visitor::recurse(const formula* f)
{ {
return unabbreviate_logic(f); return unabbreviate_logic(f);
} }
formula* const formula*
unabbreviate_logic(const formula* f) unabbreviate_logic(const formula* f)
{ {
if (f->is_sugar_free_boolean()) if (f->is_sugar_free_boolean())
return f->clone(); return f->clone();
unabbreviate_logic_visitor v; unabbreviate_logic_visitor v;
const_cast<formula*>(f)->accept(v); f->accept(v);
return v.result(); return v.result();
} }
} }

View file

@ -1,5 +1,8 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -48,9 +51,9 @@ namespace spot
virtual ~unabbreviate_logic_visitor(); virtual ~unabbreviate_logic_visitor();
using super::visit; using super::visit;
void visit(binop* bo); void visit(const binop* bo);
virtual formula* recurse(formula* f); virtual const formula* recurse(const formula* f);
}; };
/// \brief Clone and rewrite a formula to remove most of the abbreviated /// \brief Clone and rewrite a formula to remove most of the abbreviated
@ -60,7 +63,7 @@ namespace spot
/// This will rewrite binary operators such as binop::Implies, /// This will rewrite binary operators such as binop::Implies,
/// binop::Equals, and binop::Xor, using only unop::Not, multop::Or, /// binop::Equals, and binop::Xor, using only unop::Not, multop::Or,
/// and multop::And. /// and multop::And.
formula* unabbreviate_logic(const formula* f); const formula* unabbreviate_logic(const formula* f);
} }
} }

View file

@ -33,7 +33,7 @@ namespace spot
{ {
class simplify_mark_visitor : public visitor class simplify_mark_visitor : public visitor
{ {
formula* result_; const formula* result_;
mark_tools* tools_; mark_tools* tools_;
public: public:
@ -46,44 +46,44 @@ namespace spot
{ {
} }
formula* const formula*
result() result()
{ {
return result_; return result_;
} }
void void
visit(atomic_prop* ao) visit(const atomic_prop* ao)
{ {
result_ = ao->clone(); result_ = ao->clone();
} }
void void
visit(constant* c) visit(const constant* c)
{ {
result_ = c->clone(); result_ = c->clone();
} }
void void
visit(bunop* bo) visit(const bunop* bo)
{ {
result_ = bo->clone(); result_ = bo->clone();
} }
void void
visit(unop* uo) visit(const unop* uo)
{ {
result_ = uo->clone(); result_ = uo->clone();
} }
void void
visit(automatop* ao) visit(const automatop* ao)
{ {
result_ = ao->clone(); result_ = ao->clone();
} }
void void
visit(multop* mo) visit(const multop* mo)
{ {
unsigned mos = mo->size(); unsigned mos = mo->size();
multop::vec* res = new multop::vec; multop::vec* res = new multop::vec;
@ -101,12 +101,13 @@ namespace spot
break; break;
case multop::And: case multop::And:
{ {
typedef std::set<std::pair<formula*, formula*> > pset; typedef std::set<std::pair<const formula*,
const formula*> > pset;
pset Epairs, EMpairs; pset Epairs, EMpairs;
for (unsigned i = 0; i < mos; ++i) for (unsigned i = 0; i < mos; ++i)
{ {
formula* f = mo->nth(i); const formula* f = mo->nth(i);
if (f->kind() != formula::BinOp) if (f->kind() != formula::BinOp)
{ {
@ -114,7 +115,7 @@ namespace spot
} }
else else
{ {
binop* bo = static_cast<binop*>(f); const binop* bo = static_cast<const binop*>(f);
switch (bo->op()) switch (bo->op())
{ {
case binop::Xor: case binop::Xor:
@ -157,13 +158,13 @@ namespace spot
} }
void void
visit(binop* bo) visit(const binop* bo)
{ {
result_ = bo->clone(); result_ = bo->clone();
} }
formula* const formula*
recurse(formula* f) recurse(const formula* f)
{ {
return tools_->simplify_mark(f); return tools_->simplify_mark(f);
} }
@ -172,7 +173,7 @@ namespace spot
class mark_visitor : public visitor class mark_visitor : public visitor
{ {
formula* result_; const formula* result_;
mark_tools* tools_; mark_tools* tools_;
public: public:
@ -184,44 +185,44 @@ namespace spot
{ {
} }
formula* const formula*
result() result()
{ {
return result_; return result_;
} }
void void
visit(atomic_prop* ap) visit(const atomic_prop* ap)
{ {
result_ = ap->clone(); result_ = ap->clone();
} }
void void
visit(constant* c) visit(const constant* c)
{ {
result_ = c->clone(); result_ = c->clone();
} }
void void
visit(bunop* bo) visit(const bunop* bo)
{ {
result_ = bo->clone(); result_ = bo->clone();
} }
void void
visit(unop* uo) visit(const unop* uo)
{ {
result_ = uo->clone(); result_ = uo->clone();
} }
void void
visit(automatop* ao) visit(const automatop* ao)
{ {
result_ = ao->clone(); result_ = ao->clone();
} }
void void
visit(multop* mo) visit(const multop* mo)
{ {
multop::vec* res = new multop::vec; multop::vec* res = new multop::vec;
unsigned mos = mo->size(); unsigned mos = mo->size();
@ -231,7 +232,7 @@ namespace spot
} }
void void
visit(binop* bo) visit(const binop* bo)
{ {
switch (bo->op()) switch (bo->op())
{ {
@ -249,8 +250,8 @@ namespace spot
case binop::EConcatMarked: case binop::EConcatMarked:
case binop::EConcat: case binop::EConcat:
{ {
formula* f1 = bo->first()->clone(); const formula* f1 = bo->first()->clone();
formula* f2 = recurse(bo->second()); const formula* f2 = recurse(bo->second());
result_ = binop::instance(binop::EConcatMarked, f1, f2); result_ = binop::instance(binop::EConcatMarked, f1, f2);
return; return;
} }
@ -259,8 +260,8 @@ namespace spot
assert(0); assert(0);
} }
formula* const formula*
recurse(formula* f) recurse(const formula* f)
{ {
return tools_->mark_concat_ops(f); return tools_->mark_concat_ops(f);
} }
@ -301,21 +302,21 @@ namespace spot
} }
} }
formula* const formula*
mark_tools::mark_concat_ops(const formula* f) mark_tools::mark_concat_ops(const formula* f)
{ {
f2f_map::iterator i = markops_.find(f); f2f_map::iterator i = markops_.find(f);
if (i != markops_.end()) if (i != markops_.end())
return i->second->clone(); return i->second->clone();
const_cast<formula*>(f)->accept(*markvisitor_); f->accept(*markvisitor_);
formula* r = down_cast<mark_visitor*>(markvisitor_)->result(); const formula* r = down_cast<mark_visitor*>(markvisitor_)->result();
markops_[f->clone()] = r->clone(); markops_[f->clone()] = r->clone();
return r; return r;
} }
formula* const formula*
mark_tools::simplify_mark(const formula* f) mark_tools::simplify_mark(const formula* f)
{ {
if (!f->is_marked()) if (!f->is_marked())
@ -325,9 +326,10 @@ namespace spot
if (i != simpmark_.end()) if (i != simpmark_.end())
return i->second->clone(); return i->second->clone();
const_cast<formula*>(f)->accept(*simpvisitor_); f->accept(*simpvisitor_);
formula* r = down_cast<simplify_mark_visitor*>(simpvisitor_)->result(); const formula* r =
down_cast<simplify_mark_visitor*>(simpvisitor_)->result();
simpmark_[f->clone()] = r->clone(); simpmark_[f->clone()] = r->clone();
return r; return r;
} }

View file

@ -1,5 +1,5 @@
// Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement // Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et
// de l'Epita (LRDE). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -36,9 +36,9 @@ namespace spot
/// \ingroup ltl_rewriting /// \ingroup ltl_rewriting
/// ///
/// \param f The formula to rewrite. /// \param f The formula to rewrite.
formula* mark_concat_ops(const formula* f); const formula* mark_concat_ops(const formula* f);
formula* simplify_mark(const formula* f); const formula* simplify_mark(const formula* f);
mark_tools(); mark_tools();
~mark_tools(); ~mark_tools();

View file

@ -1,7 +1,8 @@
// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement // -*- coding: utf-8 -*-
// de l'Epita (LRDE). // Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -27,7 +28,7 @@ namespace spot
{ {
namespace ltl namespace ltl
{ {
formula* const formula*
negative_normal_form(const formula* f, bool negated) negative_normal_form(const formula* f, bool negated)
{ {
if (!negated && f->is_in_nenoform()) if (!negated && f->is_in_nenoform())

View file

@ -1,7 +1,8 @@
// Copyright (C) 2011 Laboratoire de Recherche et Développement de // -*- coding: utf-8 -*-
// Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement de
// l'Epita (LRDE). // l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -45,8 +46,8 @@ namespace spot
/// or spot::ltl::unabbreviate_ltl first. (Calling these functions /// or spot::ltl::unabbreviate_ltl first. (Calling these functions
/// after spot::ltl::negative_normal_form would likely produce a /// after spot::ltl::negative_normal_form would likely produce a
/// formula which is not in negative normal form.) /// formula which is not in negative normal form.)
const formula*
formula* negative_normal_form(const formula* f, bool negated = false); negative_normal_form(const formula* f, bool negated = false);
} }
} }

View file

@ -1,4 +1,5 @@
// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et // -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE). // Développement de l'Epita (LRDE).
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -37,20 +38,20 @@ namespace spot
} }
void void
postfix_visitor::visit(atomic_prop* ap) postfix_visitor::visit(const atomic_prop* ap)
{ {
doit(ap); doit(ap);
} }
void void
postfix_visitor::visit(unop* uo) postfix_visitor::visit(const unop* uo)
{ {
uo->child()->accept(*this); uo->child()->accept(*this);
doit(uo); doit(uo);
} }
void void
postfix_visitor::visit(binop* bo) postfix_visitor::visit(const binop* bo)
{ {
bo->first()->accept(*this); bo->first()->accept(*this);
bo->second()->accept(*this); bo->second()->accept(*this);
@ -58,7 +59,7 @@ namespace spot
} }
void void
postfix_visitor::visit(automatop* ao) postfix_visitor::visit(const automatop* ao)
{ {
unsigned s = ao->size(); unsigned s = ao->size();
for (unsigned i = 0; i < s; ++i) for (unsigned i = 0; i < s; ++i)
@ -67,7 +68,7 @@ namespace spot
} }
void void
postfix_visitor::visit(multop* mo) postfix_visitor::visit(const multop* mo)
{ {
unsigned s = mo->size(); unsigned s = mo->size();
for (unsigned i = 0; i < s; ++i) for (unsigned i = 0; i < s; ++i)
@ -76,62 +77,62 @@ namespace spot
} }
void void
postfix_visitor::visit(bunop* so) postfix_visitor::visit(const bunop* so)
{ {
so->child()->accept(*this); so->child()->accept(*this);
doit(so); doit(so);
} }
void void
postfix_visitor::visit(constant* c) postfix_visitor::visit(const constant* c)
{ {
doit(c); doit(c);
} }
void void
postfix_visitor::doit(atomic_prop* ap) postfix_visitor::doit(const atomic_prop* ap)
{ {
doit_default(ap); doit_default(ap);
} }
void void
postfix_visitor::doit(unop* uo) postfix_visitor::doit(const unop* uo)
{ {
doit_default(uo); doit_default(uo);
} }
void void
postfix_visitor::doit(binop* bo) postfix_visitor::doit(const binop* bo)
{ {
doit_default(bo); doit_default(bo);
} }
void void
postfix_visitor::doit(multop* mo) postfix_visitor::doit(const multop* mo)
{ {
doit_default(mo); doit_default(mo);
} }
void void
postfix_visitor::doit(automatop* ao) postfix_visitor::doit(const automatop* ao)
{ {
doit_default(ao); doit_default(ao);
} }
void void
postfix_visitor::doit(bunop* so) postfix_visitor::doit(const bunop* so)
{ {
doit_default(so); doit_default(so);
} }
void void
postfix_visitor::doit(constant* c) postfix_visitor::doit(const constant* c)
{ {
doit_default(c); doit_default(c);
} }
void void
postfix_visitor::doit_default(formula* f) postfix_visitor::doit_default(const formula* f)
{ {
(void)f; (void)f;
// Dummy implementation that does nothing. // Dummy implementation that does nothing.

View file

@ -1,4 +1,4 @@
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement // Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -43,22 +43,22 @@ namespace spot
postfix_visitor(); postfix_visitor();
virtual ~postfix_visitor(); virtual ~postfix_visitor();
void visit(atomic_prop* ap); void visit(const atomic_prop* ap);
void visit(unop* uo); void visit(const unop* uo);
void visit(binop* bo); void visit(const binop* bo);
void visit(multop* mo); void visit(const multop* mo);
void visit(automatop* c); void visit(const automatop* c);
void visit(constant* c); void visit(const constant* c);
void visit(bunop* c); void visit(const bunop* c);
virtual void doit(atomic_prop* ap); virtual void doit(const atomic_prop* ap);
virtual void doit(unop* uo); virtual void doit(const unop* uo);
virtual void doit(binop* bo); virtual void doit(const binop* bo);
virtual void doit(multop* mo); virtual void doit(const multop* mo);
virtual void doit(automatop* mo); virtual void doit(const automatop* mo);
virtual void doit(constant* c); virtual void doit(const constant* c);
virtual void doit(bunop* c); virtual void doit(const bunop* c);
virtual void doit_default(formula* f); virtual void doit_default(const formula* f);
}; };
} }
} }

View file

@ -1,7 +1,8 @@
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche // Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche
// et Développement de l'Epita (LRDE). // et Développement de l'Epita (LRDE).
// Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 // Copyright (C) 2005 Laboratoire d'Informatique de Paris 6
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
// Pierre et Marie Curie. // Pierre et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -35,7 +36,7 @@ namespace spot
{ {
namespace namespace
{ {
static formula* static const formula*
ap_builder(const random_formula* rl, int n) ap_builder(const random_formula* rl, int n)
{ {
assert(n == 1); assert(n == 1);
@ -45,7 +46,7 @@ namespace spot
return (*i)->clone(); return (*i)->clone();
} }
static formula* static const formula*
true_builder(const random_formula*, int n) true_builder(const random_formula*, int n)
{ {
assert(n == 1); assert(n == 1);
@ -53,7 +54,7 @@ namespace spot
return constant::true_instance(); return constant::true_instance();
} }
static formula* static const formula*
boolform_builder(const random_formula* rl, int n) boolform_builder(const random_formula* rl, int n)
{ {
assert(n >= 1); assert(n >= 1);
@ -61,7 +62,7 @@ namespace spot
return rs->rb.generate(n); return rs->rb.generate(n);
} }
static formula* static const formula*
false_builder(const random_formula*, int n) false_builder(const random_formula*, int n)
{ {
assert(n == 1); assert(n == 1);
@ -69,7 +70,7 @@ namespace spot
return constant::false_instance(); return constant::false_instance();
} }
static formula* static const formula*
eword_builder(const random_formula*, int n) eword_builder(const random_formula*, int n)
{ {
assert(n == 1); assert(n == 1);
@ -78,14 +79,14 @@ namespace spot
} }
template <unop::type Op> template <unop::type Op>
static formula* static const formula*
unop_builder(const random_formula* rl, int n) unop_builder(const random_formula* rl, int n)
{ {
assert(n >= 2); assert(n >= 2);
return unop::instance(Op, rl->generate(n - 1)); return unop::instance(Op, rl->generate(n - 1));
} }
static formula* static const formula*
closure_builder(const random_formula* rl, int n) closure_builder(const random_formula* rl, int n)
{ {
assert(n >= 2); assert(n >= 2);
@ -94,7 +95,7 @@ namespace spot
} }
template <binop::type Op> template <binop::type Op>
static formula* static const formula*
binop_builder(const random_formula* rl, int n) binop_builder(const random_formula* rl, int n)
{ {
assert(n >= 3); assert(n >= 3);
@ -104,7 +105,7 @@ namespace spot
} }
template <binop::type Op> template <binop::type Op>
static formula* static const formula*
binop_SERELTL_builder(const random_formula* rl, int n) binop_SERELTL_builder(const random_formula* rl, int n)
{ {
assert(n >= 3); assert(n >= 3);
@ -115,7 +116,7 @@ namespace spot
} }
template <bunop::type Op> template <bunop::type Op>
static formula* static const formula*
bunop_unbounded_builder(const random_formula* rl, int n) bunop_unbounded_builder(const random_formula* rl, int n)
{ {
assert(n >= 2); assert(n >= 2);
@ -123,7 +124,7 @@ namespace spot
} }
template <bunop::type Op> template <bunop::type Op>
static formula* static const formula*
bunop_bounded_builder(const random_formula* rl, int n) bunop_bounded_builder(const random_formula* rl, int n)
{ {
assert(n >= 2); assert(n >= 2);
@ -133,7 +134,7 @@ namespace spot
} }
template <bunop::type Op> template <bunop::type Op>
static formula* static const formula*
bunop_bool_bounded_builder(const random_formula* rl, int n) bunop_bool_bounded_builder(const random_formula* rl, int n)
{ {
assert(n >= 2); assert(n >= 2);
@ -145,7 +146,7 @@ namespace spot
template <multop::type Op> template <multop::type Op>
static formula* static const formula*
multop_builder(const random_formula* rl, int n) multop_builder(const random_formula* rl, int n)
{ {
assert(n >= 3); assert(n >= 3);
@ -197,7 +198,7 @@ namespace spot
assert(total_2_and_more_ != 0.0); assert(total_2_and_more_ != 0.0);
} }
formula* const formula*
random_formula::generate(int n) const random_formula::generate(int n) const
{ {
assert(n > 0); assert(n > 0);

View file

@ -1,7 +1,8 @@
// Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement de // -*- coding: utf-8 -*-
// l'Epita (LRDE). // Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -61,7 +62,7 @@ namespace spot
/// n, because some simple simplifications are performed by the /// n, because some simple simplifications are performed by the
/// AST. (For instance the formula <code>a | a</code> is /// AST. (For instance the formula <code>a | a</code> is
/// automatically reduced to <code>a</code> by spot::ltl::multop.) /// automatically reduced to <code>a</code> by spot::ltl::multop.)
formula* generate(int n) const; const formula* generate(int n) const;
/// \brief Print the priorities of each operator, constants, /// \brief Print the priorities of each operator, constants,
/// and atomic propositions. /// and atomic propositions.
@ -84,7 +85,7 @@ namespace spot
const char* name; const char* name;
int min_n; int min_n;
double proba; double proba;
typedef formula* (*builder)(const random_formula* rl, int n); typedef const formula* (*builder)(const random_formula* rl, int n);
builder build; builder build;
void setup(const char* name, int min_n, builder build); void setup(const char* name, int min_n, builder build);
}; };

View file

@ -1,5 +1,5 @@
// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et // Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche
// Développement de l'Epita (LRDE). // et Développement de l'Epita (LRDE).
// Copyright (C) 2004, 2006, 2007 Laboratoire d'Informatique de // Copyright (C) 2004, 2006, 2007 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
@ -30,7 +30,7 @@ namespace spot
{ {
namespace ltl namespace ltl
{ {
formula* const formula*
reduce(const formula* f, int opt) reduce(const formula* f, int opt)
{ {
ltl_simplifier_options o; ltl_simplifier_options o;
@ -40,7 +40,7 @@ namespace spot
o.containment_checks = opt & Reduce_Containment_Checks; o.containment_checks = opt & Reduce_Containment_Checks;
o.containment_checks_stronger = opt & Reduce_Containment_Checks_Stronger; o.containment_checks_stronger = opt & Reduce_Containment_Checks_Stronger;
ltl_simplifier simplifier(o); ltl_simplifier simplifier(o);
return const_cast<formula*>(simplifier.simplify(f)); return simplifier.simplify(f);
} }
bool bool

View file

@ -1,7 +1,8 @@
// Copyright (C) 2010, 2011 Laboratoire de Recherche et Developpement // -*- coding: utf-8 -*-
// de l'Epita (LRDE). // Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6 // Copyright (C) 2004, 2006 Laboratoire d'Informatique de Paris 6
// (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
// Pierre et Marie Curie. // Pierre et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -70,10 +71,10 @@ namespace spot
/// ///
/// \deprecated Use spot::ltl::ltl_simplifier instead. /// \deprecated Use spot::ltl::ltl_simplifier instead.
#if __GNUC__ #if __GNUC__
formula* const formula*
reduce(const formula* f, int opt = Reduce_All) __attribute__ ((deprecated)); reduce(const formula* f, int opt = Reduce_All) __attribute__ ((deprecated));
#else #else
formula* reduce(const formula* f, int opt = Reduce_All); const formula* reduce(const formula* f, int opt = Reduce_All);
#endif #endif
/// @} /// @}

View file

@ -1,7 +1,8 @@
// Copyright (C) 2010 Laboratoire de Recherche et Développement de // -*- coding: utf-8 -*-
// Copyright (C) 2010, 2012 Laboratoire de Recherche et Développement de
// l'Epita (LRDE). // l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -40,10 +41,10 @@ namespace spot
} }
void void
simplify_f_g_visitor::visit(binop* bo) simplify_f_g_visitor::visit(const binop* bo)
{ {
formula* f1 = recurse(bo->first()); const formula* f1 = recurse(bo->first());
formula* f2 = recurse(bo->second()); const formula* f2 = recurse(bo->second());
binop::type op = bo->op(); binop::type op = bo->op();
switch (op) switch (op)
@ -89,19 +90,19 @@ namespace spot
assert(0); assert(0);
} }
formula* const formula*
simplify_f_g_visitor::recurse(formula* f) simplify_f_g_visitor::recurse(const formula* f)
{ {
return simplify_f_g(f); return simplify_f_g(f);
} }
formula* const formula*
simplify_f_g(const formula* f) simplify_f_g(const formula* f)
{ {
if (f->is_boolean()) if (f->is_boolean())
return f->clone(); return f->clone();
simplify_f_g_visitor v; simplify_f_g_visitor v;
const_cast<formula*>(f)->accept(v); f->accept(v);
return v.result(); return v.result();
} }
} }

View file

@ -1,7 +1,8 @@
// Copyright (C) 2010 Laboratoire de Recherche et Développement de // -*- coding: utf-8 -*-
// l'Epita (LRDE). // Copyright (C) 2010, 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -49,9 +50,9 @@ namespace spot
virtual ~simplify_f_g_visitor(); virtual ~simplify_f_g_visitor();
using super::visit; using super::visit;
void visit(binop* bo); void visit(const binop* bo);
virtual formula* recurse(formula* f); virtual const formula* recurse(const formula* f);
}; };
/// \brief Replace <code>true U f</code> and <code>false R g</code> by /// \brief Replace <code>true U f</code> and <code>false R g</code> by
@ -65,7 +66,7 @@ namespace spot
/// - a W false = G a /// - a W false = G a
/// ///
/// \ingroup ltl_rewriting /// \ingroup ltl_rewriting
formula* simplify_f_g(const formula* f); const formula* simplify_f_g(const formula* f);
} }
} }

File diff suppressed because it is too large Load diff

View file

@ -77,7 +77,7 @@ namespace spot
/// Simplify the formula \a f (using options supplied to the /// Simplify the formula \a f (using options supplied to the
/// constructor). /// constructor).
formula* simplify(const formula* f); const formula* simplify(const formula* f);
/// Build the negative normal form of formula \a f. /// Build the negative normal form of formula \a f.
/// All negations of the formula are pushed in front of the /// All negations of the formula are pushed in front of the
@ -87,7 +87,8 @@ namespace spot
/// \param f The formula to normalize. /// \param f The formula to normalize.
/// \param negated If \c true, return the negative normal form of /// \param negated If \c true, return the negative normal form of
/// \c !f /// \c !f
formula* negative_normal_form(const formula* f, bool negated = false); const formula*
negative_normal_form(const formula* f, bool negated = false);
/// \brief Syntactic implication. /// \brief Syntactic implication.
/// ///

View file

@ -33,7 +33,7 @@ namespace spot
// E° // E°
class snf_visitor: public visitor class snf_visitor: public visitor
{ {
formula* result_; const formula* result_;
snf_cache* cache_; snf_cache* cache_;
public: public:
@ -41,27 +41,27 @@ namespace spot
{ {
} }
formula* const formula*
result() const result() const
{ {
return result_; return result_;
} }
void void
visit(atomic_prop*) visit(const atomic_prop*)
{ {
assert(!"unexpected operator"); assert(!"unexpected operator");
} }
void void
visit(constant* c) visit(const constant* c)
{ {
assert(c == constant::empty_word_instance()); assert(c == constant::empty_word_instance());
result_ = constant::false_instance(); result_ = constant::false_instance();
} }
void void
visit(bunop* bo) visit(const bunop* bo)
{ {
bunop::type op = bo->op(); bunop::type op = bo->op();
switch (op) switch (op)
@ -75,25 +75,25 @@ namespace spot
} }
void void
visit(unop*) visit(const unop*)
{ {
assert(!"unexpected operator"); assert(!"unexpected operator");
} }
void void
visit(binop*) visit(const binop*)
{ {
assert(!"unexpected operator"); assert(!"unexpected operator");
} }
void void
visit(automatop*) visit(const automatop*)
{ {
assert(!"unexpected operator"); assert(!"unexpected operator");
} }
void void
visit(multop* mo) visit(const multop* mo)
{ {
multop::type op = mo->op(); multop::type op = mo->op();
switch (op) switch (op)
@ -134,14 +134,14 @@ namespace spot
break; break;
case multop::AndRat: case multop::AndRat:
// FIXME: Can we deal with AndRat in a better way // FIXME: Can we deal with AndRat in a better way
// when it accepts [*0]. // when it accepts [*0]?
result_ = mo->clone(); result_ = mo->clone();
break; break;
} }
} }
formula* const formula*
recurse(formula* f) recurse(const formula* f)
{ {
if (!f->accepts_eword()) if (!f->accepts_eword())
return f->clone(); return f->clone();
@ -164,11 +164,11 @@ namespace spot
} }
formula* const formula*
star_normal_form(const formula* sere, snf_cache* cache) star_normal_form(const formula* sere, snf_cache* cache)
{ {
snf_visitor v(cache); snf_visitor v(cache);
return v.recurse(const_cast<formula*>(sere)); return v.recurse(sere);
} }
} }

View file

@ -52,8 +52,8 @@ namespace spot
/// ///
/// \param sere the SERE to rewrite /// \param sere the SERE to rewrite
/// \param cache an optional cache /// \param cache an optional cache
formula* star_normal_form(const formula* sere, const formula* star_normal_form(const formula* sere,
snf_cache* cache = 0); snf_cache* cache = 0);
} }
} }

View file

@ -183,11 +183,11 @@ namespace spot
// If the formula has the form (!b)[*], return b. // If the formula has the form (!b)[*], return b.
static static
formula* const formula*
strip_star_not(const formula* f) strip_star_not(const formula* f)
{ {
if (bunop* s = is_Star(f)) if (const bunop* s = is_Star(f))
if (unop* n = is_Not(s->child())) if (const unop* n = is_Not(s->child()))
return n->child(); return n->child();
return 0; return 0;
} }
@ -195,11 +195,11 @@ namespace spot
// If the formula as position i in multop mo has the form // If the formula as position i in multop mo has the form
// (!b)[*];b with b being a Boolean formula, return b. // (!b)[*];b with b being a Boolean formula, return b.
static static
formula* const formula*
match_goto(const multop *mo, unsigned i) match_goto(const multop *mo, unsigned i)
{ {
assert(i + 1 < mo->size()); assert(i + 1 < mo->size());
formula* b = strip_star_not(mo->nth(i)); const formula* b = strip_star_not(mo->nth(i));
if (!b || !b->is_boolean()) if (!b || !b->is_boolean())
return 0; return 0;
if (mo->nth(i + 1) == b) if (mo->nth(i + 1) == b)
@ -207,7 +207,7 @@ namespace spot
return 0; return 0;
} }
class to_string_visitor: public const_visitor class to_string_visitor: public visitor
{ {
public: public:
to_string_visitor(std::ostream& os, to_string_visitor(std::ostream& os,
@ -301,13 +301,13 @@ namespace spot
in_ratexp_ = true; in_ratexp_ = true;
top_level_ = true; top_level_ = true;
{ {
multop* m = is_multop(bo->first(), multop::Concat); const multop* m = is_multop(bo->first(), multop::Concat);
if (m) if (m)
{ {
unsigned s = m->size(); unsigned s = m->size();
if (m->nth(s - 1) == constant::true_instance()) if (m->nth(s - 1) == constant::true_instance())
{ {
formula* tmp = m->all_but(s - 1); const formula* tmp = m->all_but(s - 1);
tmp->accept(*this); tmp->accept(*this);
tmp->destroy(); tmp->destroy();
onelast = true; onelast = true;
@ -409,11 +409,11 @@ namespace spot
switch (op) switch (op)
{ {
case bunop::Star: case bunop::Star:
if (multop* mo = is_Concat(c)) if (const multop* mo = is_Concat(c))
{ {
unsigned s = mo->size(); unsigned s = mo->size();
if (s == 2) if (s == 2)
if (formula* b = match_goto(mo, 0)) if (const formula* b = match_goto(mo, 0))
{ {
c = b; c = b;
sugar = Goto; sugar = Goto;
@ -602,7 +602,7 @@ namespace spot
if (i + 1 < max) if (i + 1 < max)
{ {
// Try to match (!b)[*];b // Try to match (!b)[*];b
formula* b = match_goto(mo, i); const formula* b = match_goto(mo, i);
if (b) if (b)
{ {
emit_bunop_child(b); emit_bunop_child(b);
@ -622,10 +622,10 @@ namespace spot
continue; continue;
} }
// Try to match ((!b)[*];b)[*i..j];(!b)[*] // Try to match ((!b)[*];b)[*i..j];(!b)[*]
if (bunop* s = is_Star(mo->nth(i))) if (const bunop* s = is_Star(mo->nth(i)))
if (formula* b2 = strip_star_not(mo->nth(i + 1))) if (const formula* b2 = strip_star_not(mo->nth(i + 1)))
if (multop* sc = is_Concat(s->child())) if (const multop* sc = is_Concat(s->child()))
if (formula* b1 = match_goto(sc, 0)) if (const formula* b1 = match_goto(sc, 0))
if (b1 == b2) if (b1 == b2)
{ {
emit_bunop_child(b1); emit_bunop_child(b1);
@ -754,7 +754,7 @@ namespace spot
to_spin_string(const formula* f, std::ostream& os, bool full_parent) to_spin_string(const formula* f, std::ostream& os, bool full_parent)
{ {
// Remove xor, ->, and <-> first. // Remove xor, ->, and <-> first.
formula* fu = unabbreviate_logic(f); const formula* fu = unabbreviate_logic(f);
// Also remove W and M. // Also remove W and M.
f = unabbreviate_wm(fu); f = unabbreviate_wm(fu);
fu->destroy(); fu->destroy();

View file

@ -1,4 +1,4 @@
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement // Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -37,7 +37,7 @@ namespace spot
} }
void void
unabbreviate_ltl_visitor::visit(unop* uo) unabbreviate_ltl_visitor::visit(const unop* uo)
{ {
switch (uo->op()) switch (uo->op())
{ {
@ -61,19 +61,19 @@ namespace spot
} }
} }
formula* const formula*
unabbreviate_ltl_visitor::recurse(formula* f) unabbreviate_ltl_visitor::recurse(const formula* f)
{ {
return unabbreviate_ltl(f); return unabbreviate_ltl(f);
} }
formula* const formula*
unabbreviate_ltl(const formula* f) unabbreviate_ltl(const formula* f)
{ {
if (f->is_sugar_free_boolean() && f->is_sugar_free_ltl()) if (f->is_sugar_free_boolean() && f->is_sugar_free_ltl())
return f->clone(); return f->clone();
unabbreviate_ltl_visitor v; unabbreviate_ltl_visitor v;
const_cast<formula*>(f)->accept(v); f->accept(v);
return v.result(); return v.result();
} }

View file

@ -1,7 +1,8 @@
// Copyright (C) 2011 Laboratoire de Recherche et Développement de // -*- coding: utf-8 -*-
// Copyright (C) 2011, 2012 Laboratoire de Recherche et Développement de
// l'Epita (LRDE). // l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
// et Marie Curie. // et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -53,9 +54,9 @@ namespace spot
virtual ~unabbreviate_ltl_visitor(); virtual ~unabbreviate_ltl_visitor();
using super::visit; using super::visit;
void visit(unop* uo); void visit(const unop* uo);
formula* recurse(formula* f); const formula* recurse(const formula* f);
}; };
/// \brief Clone and rewrite a formula to remove most of the /// \brief Clone and rewrite a formula to remove most of the
@ -66,7 +67,7 @@ namespace spot
/// ///
/// This will also rewrite unary operators such as unop::F, /// This will also rewrite unary operators such as unop::F,
/// and unop::G, using only binop::U, and binop::R. /// and unop::G, using only binop::U, and binop::R.
formula* unabbreviate_ltl(const formula* f); const formula* unabbreviate_ltl(const formula* f);
} }
} }

View file

@ -44,10 +44,10 @@ namespace spot
} }
using super::visit; using super::visit;
void visit(binop* bo) void visit(const binop* bo)
{ {
formula* f1 = recurse(bo->first()); const formula* f1 = recurse(bo->first());
formula* f2 = recurse(bo->second()); const formula* f2 = recurse(bo->second());
binop::type op = bo->op(); binop::type op = bo->op();
switch (op) switch (op)
{ {
@ -76,7 +76,7 @@ namespace spot
} }
} }
virtual formula* recurse(formula* f) virtual const formula* recurse(const formula* f)
{ {
if (f->is_boolean()) if (f->is_boolean())
return f->clone(); return f->clone();
@ -86,11 +86,11 @@ namespace spot
}; };
} }
formula* const formula*
unabbreviate_wm(const formula* f) unabbreviate_wm(const formula* f)
{ {
unabbreviate_wm_visitor v; unabbreviate_wm_visitor v;
return v.recurse(const_cast<formula*>(f)); return v.recurse(f);
} }
} }
} }

View file

@ -37,7 +37,7 @@ namespace spot
/// and <code>a M b</code> is replaced by <code>b U (b & a)</code>. /// and <code>a M b</code> is replaced by <code>b U (b & a)</code>.
/// ///
/// \ingroup ltl_rewriting /// \ingroup ltl_rewriting
formula* unabbreviate_wm(const formula* f); const formula* unabbreviate_wm(const formula* f);
} }
} }

View file

@ -1,5 +1,6 @@
/* Copyright (C) 2010, 2011 Laboratoire de Recherche et Développement /* -*- coding: utf-8 -*-
** de l'Epita (LRDE). ** Copyright (C) 2010, 2011, 2012 Laboratoire de Recherche et
** Développement de l'Epita (LRDE).
** **
** This file is part of Spot, a model checking library. ** This file is part of Spot, a model checking library.
** **
@ -34,7 +35,7 @@
#include "ltlast/constant.hh" #include "ltlast/constant.hh"
#include "public.hh" #include "public.hh"
typedef std::pair<spot::ltl::formula*, std::string*> pair; typedef std::pair<const spot::ltl::formula*, std::string*> pair;
} }
%parse-param {spot::neverclaim_parse_error_list& error_list} %parse-param {spot::neverclaim_parse_error_list& error_list}
@ -193,7 +194,7 @@ transition:
else else
{ {
spot::ltl::parse_error_list pel; spot::ltl::parse_error_list pel;
spot::ltl::formula* f = spot::ltl::parse(*$3, pel); const spot::ltl::formula* f = spot::ltl::parse(*$3, pel);
delete $3; delete $3;
for(spot::ltl::parse_error_list::const_iterator i = pel.begin(); for(spot::ltl::parse_error_list::const_iterator i = pel.begin();
i != pel.end(); ++i) i != pel.end(); ++i)

View file

@ -1,4 +1,5 @@
// Copyright (C) 2009 Laboratoire de Recherche et Développement // -*- coding: utf-8 -*-
// Copyright (C) 2009, 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -68,10 +69,9 @@ int main(int argc, char* argv[])
spot::bdd_dict* dict = new spot::bdd_dict(); spot::bdd_dict* dict = new spot::bdd_dict();
spot::tgba* a; spot::tgba* a;
spot::ltl::formula* f1 = 0;
spot::ltl::parse_error_list p1; spot::ltl::parse_error_list p1;
f1 = spot::ltl::parse(formula, p1); const spot::ltl::formula* f1 = spot::ltl::parse(formula, p1);
if (spot::ltl::format_parse_errors(std::cerr, formula, p1)) if (spot::ltl::format_parse_errors(std::cerr, formula, p1))
return 2; return 2;

View file

@ -1,8 +1,9 @@
// Copyright (C) 2009 Laboratoire de Recherche et Développement // -*- coding: utf-8 -*-
// Copyright (C) 2009, 2012 Laboratoire de Recherche et Développement
// de l'Epita (LRDE). // de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -153,7 +154,7 @@ namespace spot
// FIXME: We could be smarter and reuse unused "$n" numbers. // FIXME: We could be smarter and reuse unused "$n" numbers.
s << ltl::to_string(i->second) << "$" s << ltl::to_string(i->second) << "$"
<< ++clone_counts[var]; << ++clone_counts[var];
ltl::formula* f = const ltl::formula* f =
ltl::atomic_prop::instance(s.str(), ltl::atomic_prop::instance(s.str(),
ltl::default_environment::instance()); ltl::default_environment::instance());
int res = register_acceptance_variable(f, for_me); int res = register_acceptance_variable(f, for_me);

View file

@ -33,7 +33,7 @@ namespace spot
namespace namespace
{ {
class formula_to_bdd_visitor: public ltl::const_visitor class formula_to_bdd_visitor: public ltl::visitor
{ {
public: public:
formula_to_bdd_visitor(bdd_dict* d, void* owner) formula_to_bdd_visitor(bdd_dict* d, void* owner)
@ -183,7 +183,7 @@ namespace spot
}; };
// Convert a BDD which is known to be a conjonction into a formula. // Convert a BDD which is known to be a conjonction into a formula.
static ltl::formula* static const ltl::formula*
conj_to_formula(bdd b, const bdd_dict* d) conj_to_formula(bdd b, const bdd_dict* d)
{ {
if (b == bddfalse) if (b == bddfalse)
@ -194,7 +194,7 @@ namespace spot
int var = bdd_var(b); int var = bdd_var(b);
bdd_dict::vf_map::const_iterator isi = d->var_formula_map.find(var); bdd_dict::vf_map::const_iterator isi = d->var_formula_map.find(var);
assert(isi != d->var_formula_map.end()); assert(isi != d->var_formula_map.end());
formula* res = isi->second->clone(); const formula* res = isi->second->clone();
bdd high = bdd_high(b); bdd high = bdd_high(b);
if (high == bddfalse) if (high == bddfalse)

View file

@ -1,5 +1,6 @@
// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement // -*- coding: utf-8 -*-
// de l'Epita (LRDE) // Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE)
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -207,7 +208,8 @@ namespace spot
} }
bounds_t bounds; bounds_t bounds;
for (taa_tgba::state_set::const_iterator i = s->begin(); i != s->end(); ++i) for (taa_tgba::state_set::const_iterator i = s->begin();
i != s->end(); ++i)
bounds.push_back(std::make_pair((*i)->begin(), (*i)->end())); bounds.push_back(std::make_pair((*i)->begin(), (*i)->end()));
/// Sorting might make the cartesian product faster by not /// Sorting might make the cartesian product faster by not
@ -409,7 +411,7 @@ namespace spot
return ltl::to_string(label); return ltl::to_string(label);
} }
ltl::formula* const ltl::formula*
taa_tgba_formula::clone_if(const label_t& label) const taa_tgba_formula::clone_if(const label_t& label) const
{ {
return label->clone(); return label->clone();

View file

@ -1,5 +1,6 @@
// Copyright (C) 2009, 2011 Laboratoire de Recherche et Développement // -*- coding: utf-8 -*-
// de l'Epita (LRDE). // Copyright (C) 2009, 2011, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -346,7 +347,7 @@ namespace spot
~taa_tgba_formula(); ~taa_tgba_formula();
protected: protected:
virtual std::string label_to_string(const label_t& label) const; virtual std::string label_to_string(const label_t& label) const;
virtual ltl::formula* clone_if(const label_t& label) const; virtual const ltl::formula* clone_if(const label_t& label) const;
}; };
} }

View file

@ -35,7 +35,7 @@ namespace spot
using namespace ltl; using namespace ltl;
/// \brief Recursively translate a formula into a BDD. /// \brief Recursively translate a formula into a BDD.
class eltl_trad_visitor : public const_visitor class eltl_trad_visitor : public visitor
{ {
public: public:
eltl_trad_visitor(tgba_bdd_concrete_factory& fact, bool root = false) eltl_trad_visitor(tgba_bdd_concrete_factory& fact, bool root = false)
@ -185,9 +185,9 @@ namespace spot
bdd finish = bddfalse; bdd finish = bddfalse;
bdd acc = bddtrue; bdd acc = bddtrue;
std::vector<formula*> v; std::vector<const formula*> v;
for (unsigned i = 0; i < node->size(); ++i) for (unsigned i = 0; i < node->size(); ++i)
v.push_back(const_cast<formula*>(node->nth(i))); v.push_back(node->nth(i));
std::pair<int, int> vp = std::pair<int, int> vp =
recurse_state(node->get_nfa(), recurse_state(node->get_nfa(),
@ -234,7 +234,7 @@ namespace spot
std::pair<int, int>& std::pair<int, int>&
recurse_state(const nfa::ptr& nfa, const nfa::state* s, recurse_state(const nfa::ptr& nfa, const nfa::state* s,
const std::vector<formula*>& v, const std::vector<const formula*>& v,
nmap& m, bdd& acc, bdd& finish) nmap& m, bdd& acc, bdd& finish)
{ {
bool is_loop = nfa->is_loop(); bool is_loop = nfa->is_loop();

View file

@ -35,7 +35,7 @@ namespace spot
using namespace ltl; using namespace ltl;
/// \brief Recursively translate a formula into a TAA. /// \brief Recursively translate a formula into a TAA.
class ltl2taa_visitor : public const_visitor class ltl2taa_visitor : public visitor
{ {
public: public:
ltl2taa_visitor(taa_tgba_formula* res, language_containment_checker* lcc, ltl2taa_visitor(taa_tgba_formula* res, language_containment_checker* lcc,
@ -216,7 +216,7 @@ namespace spot
std::vector<const formula*> u; // Union std::vector<const formula*> u; // Union
std::vector<const formula*> a; // Acceptance conditions std::vector<const formula*> a; // Acceptance conditions
std::copy(i1->Q.begin(), i1->Q.end(), ii(u, u.end())); std::copy(i1->Q.begin(), i1->Q.end(), ii(u, u.end()));
formula* f = i1->condition->clone(); // Refined rule const formula* f = i1->condition->clone(); // Refined rule
if (!refined_ || !contained) if (!refined_ || !contained)
{ {
std::copy(i2->Q.begin(), i2->Q.end(), ii(u, u.end())); std::copy(i2->Q.begin(), i2->Q.end(), ii(u, u.end()));
@ -394,8 +394,7 @@ namespace spot
{ {
std::vector<const formula*> u; // Union std::vector<const formula*> u; // Union
std::vector<const formula*> a; // Acceptance conditions std::vector<const formula*> a; // Acceptance conditions
formula* f = constant::true_instance(); const formula* f = constant::true_instance();
formula* g = 0;
for (unsigned i = 0; i < vs.size(); ++i) for (unsigned i = 0; i < vs.size(); ++i)
{ {
if (vs[i].succ_.empty()) if (vs[i].succ_.empty())
@ -405,7 +404,7 @@ namespace spot
f = multop::instance(multop::And, ss.condition->clone(), f); f = multop::instance(multop::And, ss.condition->clone(), f);
for (unsigned i = 0; i < ss.acc.size(); ++i) for (unsigned i = 0; i < ss.acc.size(); ++i)
{ {
g = ss.acc[i]->clone(); const formula* g = ss.acc[i]->clone();
a.push_back(g); a.push_back(g);
to_free_.push_back(g); to_free_.push_back(g);
} }

View file

@ -190,7 +190,7 @@ namespace spot
return os; return os;
} }
formula* const formula*
var_to_formula(int var) const var_to_formula(int var) const
{ {
vf_map::const_iterator isi = next_formula_map.find(var); vf_map::const_iterator isi = next_formula_map.find(var);
@ -216,7 +216,7 @@ namespace spot
return res; return res;
} }
formula* const formula*
conj_bdd_to_formula(bdd b, multop::type op = multop::And) const conj_bdd_to_formula(bdd b, multop::type op = multop::And) const
{ {
if (b == bddfalse) if (b == bddfalse)
@ -225,7 +225,7 @@ namespace spot
while (b != bddtrue) while (b != bddtrue)
{ {
int var = bdd_var(b); int var = bdd_var(b);
formula* res = var_to_formula(var); const formula* res = var_to_formula(var);
bdd high = bdd_high(b); bdd high = bdd_high(b);
if (high == bddfalse) if (high == bddfalse)
{ {
@ -243,13 +243,13 @@ namespace spot
return multop::instance(op, v); return multop::instance(op, v);
} }
formula* const formula*
conj_bdd_to_sere(bdd b) const conj_bdd_to_sere(bdd b) const
{ {
return conj_bdd_to_formula(b, multop::AndRat); return conj_bdd_to_formula(b, multop::AndRat);
} }
formula* const formula*
bdd_to_formula(bdd f) bdd_to_formula(bdd f)
{ {
if (f == bddfalse) if (f == bddfalse)
@ -265,7 +265,7 @@ namespace spot
return multop::instance(multop::Or, v); return multop::instance(multop::Or, v);
} }
formula* const formula*
bdd_to_sere(bdd f) bdd_to_sere(bdd f)
{ {
if (f == bddfalse) if (f == bddfalse)
@ -297,7 +297,7 @@ namespace spot
} }
else else
{ {
formula* ac = var_to_formula(var); const formula* ac = var_to_formula(var);
if (!a->has_acceptance_condition(ac)) if (!a->has_acceptance_condition(ac))
a->declare_acceptance_condition(ac->clone()); a->declare_acceptance_condition(ac->clone());
@ -369,14 +369,14 @@ namespace spot
using postfix_visitor::doit; using postfix_visitor::doit;
virtual void virtual void
doit(unop* node) doit(const unop* node)
{ {
if (node->op() == unop::F) if (node->op() == unop::F)
res_ &= bdd_ithvar(dict_.register_a_variable(node->child())); res_ &= bdd_ithvar(dict_.register_a_variable(node->child()));
} }
virtual void virtual void
doit(binop* node) doit(const binop* node)
{ {
if (node->op() == binop::U) if (node->op() == binop::U)
res_ &= bdd_ithvar(dict_.register_a_variable(node->second())); res_ &= bdd_ithvar(dict_.register_a_variable(node->second()));
@ -388,15 +388,15 @@ namespace spot
}; };
bdd translate_ratexp(const formula* f, translate_dict& dict, bdd translate_ratexp(const formula* f, translate_dict& dict,
formula* to_concat = 0); const formula* to_concat = 0);
// Rewrite rule for rational operators. // Rewrite rule for rational operators.
class ratexp_trad_visitor: public const_visitor class ratexp_trad_visitor: public visitor
{ {
public: public:
// negated should only be set for constants or atomic properties // negated should only be set for constants or atomic properties
ratexp_trad_visitor(translate_dict& dict, ratexp_trad_visitor(translate_dict& dict,
formula* to_concat = 0) const formula* to_concat = 0)
: dict_(dict), to_concat_(to_concat) : dict_(dict), to_concat_(to_concat)
{ {
} }
@ -451,15 +451,15 @@ namespace spot
{ {
bdd label = bdd_exist(cube, dict_.next_set); bdd label = bdd_exist(cube, dict_.next_set);
bdd dest_bdd = bdd_existcomp(cube, dict_.next_set); bdd dest_bdd = bdd_existcomp(cube, dict_.next_set);
formula* dest = dict_.conj_bdd_to_sere(dest_bdd); const formula* dest = dict_.conj_bdd_to_sere(dest_bdd);
if (dest == constant::empty_word_instance()) if (dest == constant::empty_word_instance())
{ {
out |= label & next_to_concat(); out |= label & next_to_concat();
} }
else else
{ {
formula* dest2 = multop::instance(multop::Concat, dest, const formula* dest2 = multop::instance(multop::Concat, dest,
to_concat_->clone()); to_concat_->clone());
if (dest2 != constant::false_instance()) if (dest2 != constant::false_instance())
{ {
int x = dict_.register_next_variable(dest2); int x = dict_.register_next_variable(dest2);
@ -528,7 +528,7 @@ namespace spot
void void
visit(const bunop* bo) visit(const bunop* bo)
{ {
formula* f; const formula* f;
unsigned min = bo->min(); unsigned min = bo->min();
unsigned max = bo->max(); unsigned max = bo->max();
@ -578,8 +578,7 @@ namespace spot
{ {
bdd label = bdd_exist(cube, dict_.next_set); bdd label = bdd_exist(cube, dict_.next_set);
bdd dest_bdd = bdd_existcomp(cube, dict_.next_set); bdd dest_bdd = bdd_existcomp(cube, dict_.next_set);
formula* dest = dict_.conj_bdd_to_sere(dest_bdd); const formula* dest = dict_.conj_bdd_to_sere(dest_bdd);
formula* dest2;
int x; int x;
if (dest == constant::empty_word_instance()) if (dest == constant::empty_word_instance())
{ {
@ -588,8 +587,9 @@ namespace spot
} }
else else
{ {
dest2 = multop::instance(multop::Concat, dest, const formula*
f->clone()); dest2 = multop::instance(multop::Concat, dest,
f->clone());
if (dest2 != constant::false_instance()) if (dest2 != constant::false_instance())
{ {
x = dict_.register_next_variable(dest2); x = dict_.register_next_variable(dest2);
@ -644,7 +644,7 @@ namespace spot
{ {
delete non_final; delete non_final;
// (a* & b*);c = (a*|b*);c // (a* & b*);c = (a*|b*);c
formula* f = multop::instance(multop::OrRat, final); const formula* f = multop::instance(multop::OrRat, final);
res_ = recurse_and_concat(f); res_ = recurse_and_concat(f);
f->destroy(); f->destroy();
break; break;
@ -656,17 +656,22 @@ namespace spot
// (F_1 & ... & F_n & N_1 & ... & N_m) // (F_1 & ... & F_n & N_1 & ... & N_m)
// = (F_1 | ... | F_n);[*] && (N_1 & ... & N_m) // = (F_1 | ... | F_n);[*] && (N_1 & ... & N_m)
// | (F_1 | ... | F_n) && (N_1 & ... & N_m);[*] // | (F_1 | ... | F_n) && (N_1 & ... & N_m);[*]
formula* f = multop::instance(multop::OrRat, final); const formula* f =
formula* n = multop::instance(multop::AndNLM, non_final); multop::instance(multop::OrRat, final);
formula* t = bunop::instance(bunop::Star, const formula* n =
constant::true_instance()); multop::instance(multop::AndNLM, non_final);
formula* ft = multop::instance(multop::Concat, const formula* t =
f->clone(), t->clone()); bunop::instance(bunop::Star, constant::true_instance());
formula* nt = multop::instance(multop::Concat, const formula* ft =
n->clone(), t); multop::instance(multop::Concat, f->clone(), t->clone());
formula* ftn = multop::instance(multop::AndRat, ft, n); const formula* nt =
formula* fnt = multop::instance(multop::AndRat, f, nt); multop::instance(multop::Concat, n->clone(), t);
formula* all = multop::instance(multop::OrRat, ftn, fnt); const formula* ftn =
multop::instance(multop::AndRat, ft, n);
const formula* fnt =
multop::instance(multop::AndRat, f, nt);
const formula* all =
multop::instance(multop::OrRat, ftn, fnt);
res_ = recurse_and_concat(all); res_ = recurse_and_concat(all);
all->destroy(); all->destroy();
break; break;
@ -680,7 +685,7 @@ namespace spot
// N_1 && (N_2;[*]) && ... && (N_n;[*]) // N_1 && (N_2;[*]) && ... && (N_n;[*])
// | (N_1;[*]) && N_2 && ... && (N_n;[*]) // | (N_1;[*]) && N_2 && ... && (N_n;[*])
// | (N_1;[*]) && (N_2;[*]) && ... && N_n // | (N_1;[*]) && (N_2;[*]) && ... && N_n
formula* star = const formula* star =
bunop::instance(bunop::Star, constant::true_instance()); bunop::instance(bunop::Star, constant::true_instance());
multop::vec* disj = new multop::vec; multop::vec* disj = new multop::vec;
for (unsigned n = 0; n < s; ++n) for (unsigned n = 0; n < s; ++n)
@ -688,7 +693,7 @@ namespace spot
multop::vec* conj = new multop::vec; multop::vec* conj = new multop::vec;
for (unsigned m = 0; m < s; ++m) for (unsigned m = 0; m < s; ++m)
{ {
formula* f = node->nth(m)->clone(); const formula* f = node->nth(m)->clone();
if (n != m) if (n != m)
f = multop::instance(multop::Concat, f = multop::instance(multop::Concat,
f, star->clone()); f, star->clone());
@ -697,7 +702,7 @@ namespace spot
disj->push_back(multop::instance(multop::AndRat, conj)); disj->push_back(multop::instance(multop::AndRat, conj));
} }
star->destroy(); star->destroy();
formula* all = multop::instance(multop::OrRat, disj); const formula* all = multop::instance(multop::OrRat, disj);
res_ = recurse_and_concat(all); res_ = recurse_and_concat(all);
all->destroy(); all->destroy();
break; break;
@ -757,7 +762,7 @@ namespace spot
bdd res = recurse(node->nth(0)); bdd res = recurse(node->nth(0));
// the tail // the tail
formula* tail = node->all_but(0); const formula* tail = node->all_but(0);
bdd tail_bdd; bdd tail_bdd;
bool tail_computed = false; bool tail_computed = false;
@ -770,7 +775,7 @@ namespace spot
{ {
bdd label = bdd_exist(cube, dict_.next_set); bdd label = bdd_exist(cube, dict_.next_set);
bdd dest_bdd = bdd_existcomp(cube, dict_.next_set); bdd dest_bdd = bdd_existcomp(cube, dict_.next_set);
formula* dest = dict_.conj_bdd_to_sere(dest_bdd); const formula* dest = dict_.conj_bdd_to_sere(dest_bdd);
if (dest->accepts_eword()) if (dest->accepts_eword())
{ {
@ -790,11 +795,11 @@ namespace spot
// If the destination is not a constant, it // If the destination is not a constant, it
// means it can have successors. Fusion the // means it can have successors. Fusion the
// tail and append anything to concatenate. // tail and append anything to concatenate.
formula* dest2 = multop::instance(multop::Fusion, dest, const formula* dest2 =
tail->clone()); multop::instance(multop::Fusion, dest, tail->clone());
if (to_concat_) if (to_concat_)
dest2 = multop::instance(multop::Concat, dest2, dest2 = multop::instance(multop::Concat, dest2,
to_concat_->clone()); to_concat_->clone());
if (dest2 != constant::false_instance()) if (dest2 != constant::false_instance())
{ {
int x = dict_.register_next_variable(dest2); int x = dict_.register_next_variable(dest2);
@ -814,7 +819,7 @@ namespace spot
} }
bdd bdd
recurse(const formula* f, formula* to_concat = 0) recurse(const formula* f, const formula* to_concat = 0)
{ {
return translate_ratexp(f, dict_, to_concat); return translate_ratexp(f, dict_, to_concat);
} }
@ -829,12 +834,12 @@ namespace spot
private: private:
translate_dict& dict_; translate_dict& dict_;
bdd res_; bdd res_;
formula* to_concat_; const formula* to_concat_;
}; };
bdd bdd
translate_ratexp(const formula* f, translate_dict& dict, translate_ratexp(const formula* f, translate_dict& dict,
formula* to_concat) const formula* to_concat)
{ {
// static unsigned indent = 0; // static unsigned indent = 0;
// for (unsigned i = indent; i > 0; --i) // for (unsigned i = indent; i > 0; --i)
@ -1049,7 +1054,7 @@ namespace spot
// The rewrite rules used here are adapted from Jean-Michel // The rewrite rules used here are adapted from Jean-Michel
// Couvreur's FM paper, augmented to support rational operators. // Couvreur's FM paper, augmented to support rational operators.
class ltl_trad_visitor: public const_visitor class ltl_trad_visitor: public visitor
{ {
public: public:
ltl_trad_visitor(translate_dict& dict, bool mark_all = false, ltl_trad_visitor(translate_dict& dict, bool mark_all = false,
@ -1200,8 +1205,7 @@ namespace spot
} }
else else
{ {
formula* dest2 = const formula* dest2 = unop::instance(op, dest);
unop::instance(op, const_cast<formula*>(dest));
if (dest2 == constant::false_instance()) if (dest2 == constant::false_instance())
continue; continue;
int x = dict_.register_next_variable(dest2); int x = dict_.register_next_variable(dest2);
@ -1241,7 +1245,7 @@ namespace spot
bdd label = bdd_satoneset(all_props, var_set, bddtrue); bdd label = bdd_satoneset(all_props, var_set, bddtrue);
all_props -= label; all_props -= label;
formula* dest = const formula* dest =
dict_.bdd_to_sere(bdd_exist(f1 & label, dict_.var_set)); dict_.bdd_to_sere(bdd_exist(f1 & label, dict_.var_set));
// !{ Exp } is false if Exp accepts the empty word. // !{ Exp } is false if Exp accepts the empty word.
@ -1369,7 +1373,7 @@ namespace spot
bdd label = bdd_satoneset(all_props, var_set, bddtrue); bdd label = bdd_satoneset(all_props, var_set, bddtrue);
all_props -= label; all_props -= label;
formula* dest = const formula* dest =
dict_.bdd_to_sere(bdd_exist(f1 & label, dict_.bdd_to_sere(bdd_exist(f1 & label,
dict_.var_set)); dict_.var_set));
@ -1394,7 +1398,7 @@ namespace spot
{ {
bdd label = bdd_exist(cube, dict_.next_set); bdd label = bdd_exist(cube, dict_.next_set);
bdd dest_bdd = bdd_existcomp(cube, dict_.next_set); bdd dest_bdd = bdd_existcomp(cube, dict_.next_set);
formula* dest = dict_.conj_bdd_to_sere(dest_bdd); const formula* dest = dict_.conj_bdd_to_sere(dest_bdd);
if (dest == constant::empty_word_instance()) if (dest == constant::empty_word_instance())
{ {
@ -1402,8 +1406,8 @@ namespace spot
} }
else else
{ {
formula* dest2 = binop::instance(op, dest, const formula* dest2 =
node->second()->clone()); binop::instance(op, dest, node->second()->clone());
if (dest2 != constant::false_instance()) if (dest2 != constant::false_instance())
{ {
int x = dict_.register_next_variable(dest2); int x = dict_.register_next_variable(dest2);
@ -1443,8 +1447,8 @@ namespace spot
{ {
bdd label = bdd_exist(cube, dict_.next_set); bdd label = bdd_exist(cube, dict_.next_set);
bdd dest_bdd = bdd_existcomp(cube, dict_.next_set); bdd dest_bdd = bdd_existcomp(cube, dict_.next_set);
formula* dest = dict_.conj_bdd_to_sere(dest_bdd); const formula* dest = dict_.conj_bdd_to_sere(dest_bdd);
formula* dest2 = const formula* dest2 =
binop::instance(op, dest, node->second()->clone()); binop::instance(op, dest, node->second()->clone());
bdd udest = bdd udest =
@ -1563,7 +1567,7 @@ namespace spot
// Check whether a formula has a R, W, or G operator at its // Check whether a formula has a R, W, or G operator at its
// top-level (preceding logical operators do not count). // top-level (preceding logical operators do not count).
class ltl_possible_fair_loop_visitor: public const_visitor class ltl_possible_fair_loop_visitor: public visitor
{ {
public: public:
ltl_possible_fair_loop_visitor() ltl_possible_fair_loop_visitor()
@ -1737,13 +1741,13 @@ namespace spot
{ {
bdd label = bdd_exist(cube, d_.next_set); bdd label = bdd_exist(cube, d_.next_set);
bdd dest_bdd = bdd_existcomp(cube, d_.next_set); bdd dest_bdd = bdd_existcomp(cube, d_.next_set);
formula* dest = const formula* dest =
d_.conj_bdd_to_formula(dest_bdd); d_.conj_bdd_to_formula(dest_bdd);
// Handle a Miyano-Hayashi style unrolling for // Handle a Miyano-Hayashi style unrolling for
// rational operators. Marked nodes correspond to // rational operators. Marked nodes correspond to
// subformulae in the Miyano-Hayashi set. // subformulae in the Miyano-Hayashi set.
formula* tmp = d_.mt.simplify_mark(dest); const formula* tmp = d_.mt.simplify_mark(dest);
dest->destroy(); dest->destroy();
dest = tmp; dest = tmp;
@ -1759,7 +1763,7 @@ namespace spot
// We have no marked operators, but still // We have no marked operators, but still
// have other rational operator to check. // have other rational operator to check.
// Start a new marked cycle. // Start a new marked cycle.
formula* dest2 = d_.mt.mark_concat_ops(dest); const formula* dest2 = d_.mt.mark_concat_ops(dest);
dest->destroy(); dest->destroy();
dest = dest2; dest = dest2;
} }
@ -1864,7 +1868,7 @@ namespace spot
bool fair_loop_approx, const atomic_prop_set* unobs, bool fair_loop_approx, const atomic_prop_set* unobs,
ltl_simplifier* simplifier) ltl_simplifier* simplifier)
{ {
formula* f2; const formula* f2;
ltl_simplifier* s = simplifier; ltl_simplifier* s = simplifier;
// Simplify the formula, if requested. // Simplify the formula, if requested.
@ -1942,7 +1946,7 @@ namespace spot
// This is in case the initial state is equivalent to true... // This is in case the initial state is equivalent to true...
if (symb_merge) if (symb_merge)
f2 = const_cast<formula*>(fc.canonize(f2)); f2 = fc.canonize(f2);
formulae_to_translate.insert(f2); formulae_to_translate.insert(f2);
a->set_init_state(f2); a->set_init_state(f2);
@ -2043,7 +2047,7 @@ namespace spot
// Simplify the formula, if requested. // Simplify the formula, if requested.
if (simplifier) if (simplifier)
{ {
formula* tmp = simplifier->simplify(dest); const formula* tmp = simplifier->simplify(dest);
dest->destroy(); dest->destroy();
dest = tmp; dest = tmp;
// Ignore the arc if the destination reduces to false. // Ignore the arc if the destination reduces to false.
@ -2072,9 +2076,7 @@ namespace spot
succs[label] = dest; succs[label] = dest;
else else
si->second = si->second =
multop::instance(multop::Or, multop::instance(multop::Or, si->second, dest);
const_cast<formula*>(si->second),
const_cast<formula*>(dest));
} }
} }
if (branching_postponement) if (branching_postponement)

View file

@ -41,7 +41,7 @@ namespace spot
/// ///
/// The algorithm used here is adapted from Jean-Michel Couvreur's /// The algorithm used here is adapted from Jean-Michel Couvreur's
/// Probataf tool. /// Probataf tool.
class ltl_trad_visitor: public const_visitor class ltl_trad_visitor: public visitor
{ {
public: public:
ltl_trad_visitor(tgba_bdd_concrete_factory& fact, bool root = false) ltl_trad_visitor(tgba_bdd_concrete_factory& fact, bool root = false)

View file

@ -648,7 +648,8 @@ namespace spot
{ {
assert(f); assert(f);
ltl::formula* neg_f = ltl::unop::instance(ltl::unop::Not, f->clone()); const ltl::formula* neg_f =
ltl::unop::instance(ltl::unop::Not, f->clone());
aut_neg_f = ltl_to_tgba_fm(neg_f, aut_f->get_dict()); aut_neg_f = ltl_to_tgba_fm(neg_f, aut_f->get_dict());
neg_f->destroy(); neg_f->destroy();

View file

@ -1,8 +1,9 @@
// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et // -*- coding: utf-8 -*-
// Développement de l'Epita (LRDE). // Copyright (C) 2008, 2009, 2010, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2004, 2005, 2007 Laboratoire d'Informatique de // Copyright (C) 2004, 2005, 2007 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -116,7 +117,7 @@ namespace spot
bdd allneg = bddtrue; bdd allneg = bddtrue;
for (int i = 0; i < n_acc; ++i) for (int i = 0; i < n_acc; ++i)
{ {
ltl::formula* f = env->require(acc(i)); const ltl::formula* f = env->require(acc(i));
int v = dict->register_acceptance_variable(f, res); int v = dict->register_acceptance_variable(f, res);
res->declare_acceptance_condition(f); res->declare_acceptance_condition(f);
allneg &= bdd_nithvar(v); allneg &= bdd_nithvar(v);

View file

@ -1,8 +1,9 @@
/* Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement /* -*- coding: utf-8 -*-
** de l'Epita (LRDE). ** Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et
** Développement de l'Epita (LRDE).
** Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de ** Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de
** Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), ** Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
** Université Pierre et Marie Curie. ** Université Pierre et Marie Curie.
** **
** This file is part of Spot, a model checking library. ** This file is part of Spot, a model checking library.
** **
@ -49,8 +50,8 @@ typedef std::map<std::string, bdd> formula_cache;
{ {
int token; int token;
std::string* str; std::string* str;
spot::ltl::formula* f; const spot::ltl::formula* f;
std::list<spot::ltl::formula*>* list; std::list<const spot::ltl::formula*>* list;
} }
%code %code
@ -80,7 +81,7 @@ typedef std::pair<bool, spot::ltl::formula*> pair;
%destructor { delete $$; } <str> %destructor { delete $$; } <str>
%destructor { %destructor {
for (std::list<spot::ltl::formula*>::iterator i = $$->begin(); for (std::list<const spot::ltl::formula*>::iterator i = $$->begin();
i != $$->end(); ++i) i != $$->end(); ++i)
(*i)->destroy(); (*i)->destroy();
delete $$; delete $$;
@ -113,7 +114,8 @@ line: strident ',' strident ',' condition ',' acc_list ';'
if (i == fcache.end()) if (i == fcache.end())
{ {
parse_error_list pel; parse_error_list pel;
formula* f = spot::ltl::parse(*$5, pel, parse_environment); const formula* f =
spot::ltl::parse(*$5, pel, parse_environment);
for (parse_error_list::iterator i = pel.begin(); for (parse_error_list::iterator i = pel.begin();
i != pel.end(); ++i) i != pel.end(); ++i)
{ {
@ -139,7 +141,7 @@ line: strident ',' strident ',' condition ',' acc_list ';'
} }
delete $5; delete $5;
} }
std::list<formula*>::iterator i; std::list<const formula*>::iterator i;
for (i = $7->begin(); i != $7->end(); ++i) for (i = $7->begin(); i != $7->end(); ++i)
result->add_acceptance_condition(t, *i); result->add_acceptance_condition(t, *i);
delete $1; delete $1;
@ -170,7 +172,7 @@ condition:
acc_list: acc_list:
{ {
$$ = new std::list<formula*>; $$ = new std::list<const formula*>;
} }
| acc_list strident | acc_list strident
{ {
@ -180,7 +182,7 @@ acc_list:
} }
else if (*$2 != "" && *$2 != "false") else if (*$2 != "" && *$2 != "false")
{ {
formula* f = parse_envacc.require(*$2); const formula* f = parse_envacc.require(*$2);
if (! result->has_acceptance_condition(f)) if (! result->has_acceptance_condition(f))
{ {
error_list.push_back(spot::tgba_parse_error(@2, error_list.push_back(spot::tgba_parse_error(@2,
@ -200,7 +202,7 @@ acc_list:
acc_decl: acc_decl:
| acc_decl strident | acc_decl strident
{ {
formula* f = parse_envacc.require(*$2); const formula* f = parse_envacc.require(*$2);
if (! f) if (! f)
{ {
std::string s = "acceptance condition `"; std::string s = "acceptance condition `";

View file

@ -1,4 +1,4 @@
// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et // Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE). // Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -162,7 +162,7 @@ int main(int argc, char* argv[])
else if (print_formula) else if (print_formula)
{ {
spot::tgba* a; spot::tgba* a;
spot::ltl::formula* f1 = 0; const spot::ltl::formula* f1 = 0;
spot::ltl::parse_error_list p1; spot::ltl::parse_error_list p1;
f1 = spot::ltl::parse(file, p1); f1 = spot::ltl::parse(file, p1);
@ -186,7 +186,7 @@ int main(int argc, char* argv[])
else if (stats) else if (stats)
{ {
spot::tgba* a; spot::tgba* a;
spot::ltl::formula* f1 = 0; const spot::ltl::formula* f1 = 0;
if (formula) if (formula)
{ {
@ -247,7 +247,7 @@ int main(int argc, char* argv[])
delete a; delete a;
if (formula) if (formula)
{ {
spot::ltl::formula* nf1 = const spot::ltl::formula* nf1 =
spot::ltl::unop::instance(spot::ltl::unop::Not, spot::ltl::unop::instance(spot::ltl::unop::Not,
f1->clone()); f1->clone());
spot::tgba* a2 = spot::ltl_to_tgba_fm(nf1, dict); spot::tgba* a2 = spot::ltl_to_tgba_fm(nf1, dict);
@ -266,14 +266,14 @@ int main(int argc, char* argv[])
else else
{ {
spot::ltl::parse_error_list p1; spot::ltl::parse_error_list p1;
spot::ltl::formula* f1 = spot::ltl::parse(file, p1); const spot::ltl::formula* f1 = spot::ltl::parse(file, p1);
if (spot::ltl::format_parse_errors(std::cerr, file, p1)) if (spot::ltl::format_parse_errors(std::cerr, file, p1))
return 2; return 2;
spot::tgba* Af = spot::ltl_to_tgba_fm(f1, dict); spot::tgba* Af = spot::ltl_to_tgba_fm(f1, dict);
spot::ltl::formula* nf1 = spot::ltl::unop::instance(spot::ltl::unop::Not, const spot::ltl::formula* nf1 =
f1->clone()); spot::ltl::unop::instance(spot::ltl::unop::Not, f1->clone());
spot::tgba* Anf = spot::ltl_to_tgba_fm(nf1, dict); spot::tgba* Anf = spot::ltl_to_tgba_fm(nf1, dict);
spot::tgba* nAf; spot::tgba* nAf;

View file

@ -659,7 +659,7 @@ main(int argc, char** argv)
while (tok) while (tok)
{ {
unobservables->insert unobservables->insert
(static_cast<spot::ltl::atomic_prop*>(env.require(tok))); (static_cast<const spot::ltl::atomic_prop*>(env.require(tok)));
tok = strtok(0, ", \t;"); tok = strtok(0, ", \t;");
} }
} }
@ -730,7 +730,7 @@ main(int argc, char** argv)
input = argv[formula_index]; input = argv[formula_index];
} }
spot::ltl::formula* f = 0; const spot::ltl::formula* f = 0;
if (!from_file) // Reading a formula, not reading an automaton from a file. if (!from_file) // Reading a formula, not reading an automaton from a file.
{ {
switch (translation) switch (translation)
@ -825,7 +825,7 @@ main(int argc, char** argv)
if (simp) if (simp)
{ {
tm.start("reducing formula"); tm.start("reducing formula");
spot::ltl::formula* t = simp->simplify(f); const spot::ltl::formula* t = simp->simplify(f);
f->destroy(); f->destroy();
tm.stop("reducing formula"); tm.stop("reducing formula");
f = t; f = t;

View file

@ -1,8 +1,9 @@
// Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement // -*- coding: utf-8 -*-
// de l'Epita (LRDE). // Copyright (C) 2008, 2009, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de // Copyright (C) 2003, 2004 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -49,13 +50,13 @@ main(int argc, char** argv)
spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::ltl::parse_error_list pel1; spot::ltl::parse_error_list pel1;
spot::ltl::formula* f1 = spot::ltl::parse(argv[1], pel1, env); const spot::ltl::formula* f1 = spot::ltl::parse(argv[1], pel1, env);
if (spot::ltl::format_parse_errors(std::cerr, argv[1], pel1)) if (spot::ltl::format_parse_errors(std::cerr, argv[1], pel1))
return 2; return 2;
spot::ltl::parse_error_list pel2; spot::ltl::parse_error_list pel2;
spot::ltl::formula* f2 = spot::ltl::parse(argv[2], pel2, env); const spot::ltl::formula* f2 = spot::ltl::parse(argv[2], pel2, env);
if (spot::ltl::format_parse_errors(std::cerr, argv[2], pel2)) if (spot::ltl::format_parse_errors(std::cerr, argv[2], pel2))
return 2; return 2;

View file

@ -1,8 +1,9 @@
// Copyright (C) 2008, 2009 Laboratoire de Recherche et Développement // -*- coding: utf-8 -*-
// de l'Epita (LRDE). // Copyright (C) 2008, 2009, 2012 Laboratoire de Recherche et
// Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
@ -52,7 +53,7 @@ main(int argc, char** argv)
spot::ltl::environment& env(spot::ltl::default_environment::instance()); spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::ltl::parse_error_list pel1; spot::ltl::parse_error_list pel1;
spot::ltl::formula* f1 = spot::ltl::parse(argv[1], pel1, env); const spot::ltl::formula* f1 = spot::ltl::parse(argv[1], pel1, env);
if (spot::ltl::format_parse_errors(std::cerr, argv[1], pel1)) if (spot::ltl::format_parse_errors(std::cerr, argv[1], pel1))
return 2; return 2;

View file

@ -1,5 +1,5 @@
// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et // Copyright (C) 2008, 2009, 2010, 2011, 2012 Laboratoire de Recherche
// Développement de l'Epita (LRDE). // et Développement de l'Epita (LRDE).
// Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
@ -487,7 +487,7 @@ print_ar_stats(ar_stats_type& ar_stats, const std::string s)
std::cout << std::setiosflags(old); std::cout << std::setiosflags(old);
} }
spot::ltl::formula* const spot::ltl::formula*
generate_formula(const spot::ltl::random_ltl& rl, generate_formula(const spot::ltl::random_ltl& rl,
spot::ltl::ltl_simplifier& simp, spot::ltl::ltl_simplifier& simp,
int opt_f, int opt_s, int opt_f, int opt_s,
@ -499,14 +499,14 @@ generate_formula(const spot::ltl::random_ltl& rl,
while (max_tries_u--) while (max_tries_u--)
{ {
spot::srand(opt_s++); spot::srand(opt_s++);
spot::ltl::formula* f; const spot::ltl::formula* f;
int max_tries_l = 1000; int max_tries_l = 1000;
while (max_tries_l--) while (max_tries_l--)
{ {
f = rl.generate(opt_f); f = rl.generate(opt_f);
if (opt_l) if (opt_l)
{ {
spot::ltl::formula* g = simp.simplify(f); const spot::ltl::formula* g = simp.simplify(f);
f->destroy(); f->destroy();
if (spot::ltl::length(g) < opt_l) if (spot::ltl::length(g) < opt_l)
{ {
@ -788,7 +788,7 @@ main(int argc, char** argv)
} }
else else
{ {
ap->insert(static_cast<spot::ltl::atomic_prop*> ap->insert(static_cast<const spot::ltl::atomic_prop*>
(env.require(argv[argn]))); (env.require(argv[argn])));
} }
} }
@ -853,9 +853,8 @@ main(int argc, char** argv)
{ {
if (opt_F) if (opt_F)
{ {
spot::ltl::formula* f = generate_formula(rl, simp, const spot::ltl::formula* f =
opt_f, opt_ec_seed, generate_formula(rl, simp, opt_f, opt_ec_seed, opt_l, opt_u);
opt_l, opt_u);
if (!f) if (!f)
exit(1); exit(1);
formula = spot::ltl_to_tgba_fm(f, dict, true); formula = spot::ltl_to_tgba_fm(f, dict, true);
@ -871,7 +870,7 @@ main(int argc, char** argv)
else if (input == "") else if (input == "")
break; break;
spot::ltl::parse_error_list pel; spot::ltl::parse_error_list pel;
spot::ltl::formula* f = spot::ltl::parse(input, pel, env); const spot::ltl::formula* f = spot::ltl::parse(input, pel, env);
if (spot::ltl::format_parse_errors(std::cerr, input, pel)) if (spot::ltl::format_parse_errors(std::cerr, input, pel))
{ {
exit_code = 1; exit_code = 1;
@ -882,7 +881,7 @@ main(int argc, char** argv)
spot::ltl::atomic_prop_collect(f); spot::ltl::atomic_prop_collect(f);
for (spot::ltl::atomic_prop_set::iterator i = tmp->begin(); for (spot::ltl::atomic_prop_set::iterator i = tmp->begin();
i != tmp->end(); ++i) i != tmp->end(); ++i)
apf->insert(dynamic_cast<spot::ltl::atomic_prop*> apf->insert(dynamic_cast<const spot::ltl::atomic_prop*>
((*i)->clone())); ((*i)->clone()));
f->destroy(); f->destroy();
delete tmp; delete tmp;
@ -897,7 +896,7 @@ main(int argc, char** argv)
for (spot::ltl::atomic_prop_set::iterator i = ap->begin(); for (spot::ltl::atomic_prop_set::iterator i = ap->begin();
i != ap->end(); ++i) i != ap->end(); ++i)
apf->insert(dynamic_cast<spot::ltl::atomic_prop*>((*i)->clone())); apf->insert(static_cast<const spot::ltl::atomic_prop*>((*i)->clone()));
if (!opt_S) if (!opt_S)
{ {

View file

@ -1,179 +0,0 @@
// Copyright (C) 2008, 2009, 2011 Laboratoire de Recherche et Développement
// de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
//
// This file is part of Spot, a model checking library.
//
// Spot is free software; you can redistribute it and/or modify it
// under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2 of the License, or
// (at your option) any later version.
//
// Spot is distributed in the hope that it will be useful, but WITHOUT
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
// License for more details.
//
// You should have received a copy of the GNU General Public License
// along with Spot; see the file COPYING. If not, write to the Free
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
#include <cstdlib>
#include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgbaalgos/reductgba_sim.hh"
#include "tgba/tgbareduc.hh"
#include "ltlast/allnodes.hh"
#include "ltlparse/public.hh"
#include "tgbaalgos/ltl2tgba_lacim.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgba/bddprint.hh"
#include "tgbaalgos/dotty.hh"
#include "tgbaalgos/lbtt.hh"
#include "tgba/tgbatba.hh"
#include "tgbaalgos/magic.hh"
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/gtec/ce.hh"
#include "tgbaparse/public.hh"
#include "tgbaalgos/dupexp.hh"
#include "tgbaalgos/neverclaim.hh"
#include "tgbaalgos/sccfilter.hh"
#include "misc/escape.hh"
void
syntax(char* prog)
{
#ifdef REDUCCMP
std::cerr << prog << " option file" << std::endl;
#else
std::cerr << prog << " option formula" << std::endl;
#endif
exit(2);
}
int
main(int argc, char** argv)
{
if (argc < 3)
syntax(argv[0]);
int o = spot::Reduce_None;
switch (atoi(argv[1]))
{
case 0:
o = spot::Reduce_Scc;
break;
case 1:
o = spot::Reduce_quotient_Dir_Sim;
break;
case 2:
o = spot::Reduce_transition_Dir_Sim;
break;
case 3:
o = spot::Reduce_quotient_Del_Sim;
break;
case 4:
o = spot::Reduce_transition_Del_Sim;
break;
case 5:
o = spot::Reduce_quotient_Dir_Sim |
spot::Reduce_transition_Dir_Sim |
spot::Reduce_Scc;
break;
case 6:
o = spot::Reduce_quotient_Del_Sim |
spot::Reduce_transition_Del_Sim |
spot::Reduce_Scc;
break;
case 7:
// No Reduction
break;
default:
return 2;
}
int exit_code = 0;
spot::direct_simulation_relation* rel_dir = 0;
spot::delayed_simulation_relation* rel_del = 0;
spot::tgba* automata = 0;
spot::tgba_reduc* automatareduc = 0;
spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::bdd_dict* dict = new spot::bdd_dict();
#ifdef REDUCCMP
spot::tgba_parse_error_list pel;
automata = spot::tgba_parse(argv[2], pel, dict, env, env, false);
if (spot::format_tgba_parse_errors(std::cerr, argv[2], pel))
return 2;
#else
spot::ltl::parse_error_list p1;
spot::ltl::formula* f = spot::ltl::parse(argv[2], p1, env);
if (spot::ltl::format_parse_errors(std::cerr, argv[2], p1))
return 2;
automata = spot::ltl_to_tgba_fm(f, dict,
false, true,
false, true);
#endif
spot::dotty_reachable(std::cout, automata);
automatareduc = new spot::tgba_reduc(automata);
if (o & spot::Reduce_quotient_Dir_Sim)
{
rel_dir = spot::get_direct_relation_simulation(automatareduc, std::cout);
automatareduc->quotient_state(rel_dir);
}
else if (o & spot::Reduce_quotient_Del_Sim)
{
std::cout << "get delayed" << std::endl;
rel_del = spot::get_delayed_relation_simulation(automatareduc, std::cout);
std::cout << "quotient state" << std::endl;
automatareduc->quotient_state(rel_del);
std::cout << "end" << std::endl;
}
if (rel_dir != 0)
{
automatareduc->display_rel_sim(rel_dir, std::cout);
spot::free_relation_simulation(rel_dir);
}
if (rel_del != 0)
{
automatareduc->display_rel_sim(rel_del, std::cout);
spot::free_relation_simulation(rel_del);
}
spot::tgba* res = automatareduc;
if (o & spot::Reduce_Scc)
{
res = spot::scc_filter(automatareduc);
delete automatareduc;
}
spot::dotty_reachable(std::cout, res);
delete res;
delete automata;
#ifndef REDUCCMP
if (f != 0)
f->destroy();
#endif
assert(spot::ltl::atomic_prop::instance_count() == 0);
assert(spot::ltl::unop::instance_count() == 0);
assert(spot::ltl::binop::instance_count() == 0);
assert(spot::ltl::multop::instance_count() == 0);
if (dict != 0)
delete dict;
return exit_code;
}