spot  2.7.5
Classes | Macros | Enumerations | Functions
formula.hh File Reference

LTL/PSL formula interface. More...

#include <spot/misc/common.hh>
#include <memory>
#include <cstdint>
#include <initializer_list>
#include <cassert>
#include <vector>
#include <string>
#include <iterator>
#include <iosfwd>
#include <sstream>
#include <list>
#include <cstddef>
#include <limits>
Include dependency graph for formula.hh:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  spot::fnode
 Actual storage for formula nodes. More...
 
struct  spot::formula_ptr_less_than_bool_first
 
class  spot::formula
 Main class for temporal logic formula. More...
 
class  spot::formula::formula_child_iterator
 Allow iterating over children. More...
 
struct  std::hash< spot::formula >
 

Macros

#define SPOT_DEF_UNOP(Name)
 
#define SPOT_DEF_BINOP(Name)
 
#define SPOT_DEF_MULTOP(Name)
 
#define SPOT_DEF_BUNOP(Name)
 
#define SPOT_DEF_PROP(Name)
 

Enumerations

enum  spot::op : uint8_t {
  spot::op::ff, spot::op::tt, spot::op::eword, spot::op::ap,
  spot::op::Not, spot::op::X, spot::op::F, spot::op::G,
  spot::op::Closure, spot::op::NegClosure, spot::op::NegClosureMarked, spot::op::Xor,
  spot::op::Implies, spot::op::Equiv, spot::op::U, spot::op::R,
  spot::op::W, spot::op::M, spot::op::EConcat, spot::op::EConcatMarked,
  spot::op::UConcat, spot::op::Or, spot::op::OrRat, spot::op::And,
  spot::op::AndRat, spot::op::AndNLM, spot::op::Concat, spot::op::Fusion,
  spot::op::Star, spot::op::FStar
}
 Operator types. More...
 

Functions

int spot::atomic_prop_cmp (const fnode *f, const fnode *g)
 Order two atomic propositions. More...
 
std::ostream & spot::print_formula_props (std::ostream &out, const formula &f, bool abbreviated=false)
 Print the properties of formula f on stream out. More...
 
std::list< std::string > spot::list_formula_props (const formula &f)
 List the properties of formula f. More...
 
std::ostream & spot::operator<< (std::ostream &os, const formula &f)
 Print a formula. More...
 

Detailed Description

LTL/PSL formula interface.

Macro Definition Documentation

◆ SPOT_DEF_BINOP

#define SPOT_DEF_BINOP (   Name)
Value:
static formula Name(const formula& f, const formula& g) \
{ \
return binop(op::Name, f, g); \
} \
static formula Name(const formula& f, formula&& g) \
{ \
return binop(op::Name, f, std::move(g)); \
} \
static formula Name(formula&& f, const formula& g) \
{ \
return binop(op::Name, std::move(f), g); \
} \
static formula Name(formula&& f, formula&& g) \
{ \
return binop(op::Name, std::move(f), std::move(g)); \
}

◆ SPOT_DEF_BUNOP

#define SPOT_DEF_BUNOP (   Name)
Value:
static formula Name(const formula& f, \
uint8_t min = 0U, \
uint8_t max = unbounded()) \
{ \
return bunop(op::Name, f, min, max); \
} \
static formula Name(formula&& f, \
uint8_t min = 0U, \
uint8_t max = unbounded()) \
{ \
return bunop(op::Name, std::move(f), min, max); \
}

◆ SPOT_DEF_MULTOP

#define SPOT_DEF_MULTOP (   Name)
Value:
static formula Name(const std::vector<formula>& l) \
{ \
return multop(op::Name, l); \
} \
\
static formula Name(std::vector<formula>&& l) \
{ \
return multop(op::Name, std::move(l)); \
}

◆ SPOT_DEF_PROP

#define SPOT_DEF_PROP (   Name)
Value:
bool Name() const \
{ \
return ptr_->Name(); \
}

◆ SPOT_DEF_UNOP

#define SPOT_DEF_UNOP (   Name)
Value:
static formula Name(const formula& f) \
{ \
return unop(op::Name, f); \
} \
static formula Name(formula&& f) \
{ \
return unop(op::Name, std::move(f)); \
}

Function Documentation

◆ atomic_prop_cmp()

int spot::atomic_prop_cmp ( const fnode f,
const fnode g 
)

Order two atomic propositions.

Referenced by spot::fnode::has_spin_atomic_props().

◆ list_formula_props()

std::list<std::string> spot::list_formula_props ( const formula f)

List the properties of formula f.

Referenced by spot::formula::traverse().

◆ operator<<()

std::ostream& spot::operator<< ( std::ostream &  os,
const formula f 
)

Print a formula.

◆ print_formula_props()

std::ostream& spot::print_formula_props ( std::ostream &  out,
const formula f,
bool  abbreviated = false 
)

Print the properties of formula f on stream out.

Referenced by spot::formula::traverse().


Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Fri Feb 27 2015 10:00:07 for spot by doxygen 1.8.13