spot  2.3.1
 All Classes Files Functions Variables Typedefs Enumerations Enumerator Friends Modules Pages
Classes | Typedefs | Enumerations | Functions

Classes

struct  spot::parsed_aut
 Result of the automaton parser. More...
 
struct  spot::automaton_parser_options
 
class  spot::automaton_stream_parser
 Parse a stream of automata. More...
 

Typedefs

typedef std::pair
< spot::location, std::string > 
spot::parse_aut_error
 A parse diagnostic with its location. More...
 
typedef std::list
< parse_aut_error > 
spot::parse_aut_error_list
 A list of parser diagnostics, as filled by parse. More...
 
typedef std::shared_ptr
< parsed_aut > 
spot::parsed_aut_ptr
 
typedef std::shared_ptr< const
parsed_aut > 
spot::const_parsed_aut_ptr
 

Enumerations

enum  parsed_aut_type {
  HOA, NeverClaim, LBTT, DRA,
  DSA, Unknown
}
 

Functions

parsed_aut_ptr spot::parse_aut (const std::string &filename, const bdd_dict_ptr &dict, environment &env=default_environment::instance(), automaton_parser_options opts={})
 Read the first spot::twa_graph from a file. More...
 
std::ostream & spot::print_dot (std::ostream &os, const const_twa_ptr &g, const char *options=nullptr)
 Print reachable states in dot format. More...
 
std::ostream & spot::print_hoa (std::ostream &os, const const_twa_ptr &g, const char *opt=nullptr)
 Print reachable states in Hanoi Omega Automata format. More...
 
std::ostream & spot::print_lbtt (std::ostream &os, const const_twa_ptr &g, const char *opt=nullptr)
 Print reachable states in LBTT's format. More...
 
std::ostream & spot::print_never_claim (std::ostream &os, const const_twa_ptr &g, const char *opt=nullptr)
 Print reachable states in Spin never claim format. More...
 

Detailed Description

Typedef Documentation

typedef std::pair<spot::location, std::string> spot::parse_aut_error

#include <spot/parseaut/public.hh>

A parse diagnostic with its location.

typedef std::list<parse_aut_error> spot::parse_aut_error_list

#include <spot/parseaut/public.hh>

A list of parser diagnostics, as filled by parse.

Function Documentation

parsed_aut_ptr spot::parse_aut ( const std::string &  filename,
const bdd_dict_ptr &  dict,
environment &  env = default_environment::instance(),
automaton_parser_options  opts = {} 
)

#include <spot/parseaut/public.hh>

Read the first spot::twa_graph from a file.

Parameters
filenameThe name of the file to parse.
dictThe BDD dictionary where to use.
envThe environment of atomic proposition into which parsing should take place.
optsAdditional options to pass to the parser.
Returns
A pointer to a parsed_aut structure.

This is a wrapper around spot::automaton_stream_parser that returns the first automaton of the file. Empty inputs are reported as syntax errors, so the aut field of the result is guaranteed not to be null if errors is empty. (This is unlike automaton_stream_parser::parse() where a null aut denots the end of a stream.)

Warning
This function is not reentrant.
std::ostream& spot::print_dot ( std::ostream &  os,
const const_twa_ptr &  g,
const char *  options = nullptr 
)

#include <spot/twaalgos/dot.hh>

Print reachable states in dot format.

If assume_sba is set, this assumes that the automaton is an SBA and use double elipse to mark accepting states.

Parameters
optionsan optional string of letters, each indicating a different option. Presently the following options are supported: 'v' for vertical output, 'h' for horizontal output, 't' force transition-based acceptance, 'N' hide the name of the automaton, 'n' shows the name, 'c' uses circle-shaped states, 'a' shows the acceptance, 'k' uses state-based labels if possible.
std::ostream& spot::print_hoa ( std::ostream &  os,
const const_twa_ptr &  g,
const char *  opt = nullptr 
)

#include <spot/twaalgos/hoa.hh>

Print reachable states in Hanoi Omega Automata format.

Parameters
osThe output stream to print on.
gThe automaton to output.
opta set of characters each corresponding to a possible option: (i) implicit labels for complete and deterministic automata, (k) state labels when possible, (s) state-based acceptance when possible, (t) transition-based acceptance, (m) mixed acceptance, (l) single-line output, (v) verbose properties, (1.1) use version 1.1 of the HOA format.
std::ostream& spot::print_lbtt ( std::ostream &  os,
const const_twa_ptr &  g,
const char *  opt = nullptr 
)

#include <spot/twaalgos/lbtt.hh>

Print reachable states in LBTT's format.

Parameters
gThe automata to print.
osWhere to print.
optif "t", force transition-based acceptance, otherwise,
std::ostream& spot::print_never_claim ( std::ostream &  os,
const const_twa_ptr &  g,
const char *  opt = nullptr 
)

#include <spot/twaalgos/neverclaim.hh>

Print reachable states in Spin never claim format.

Parameters
osThe output stream to print on.
gThe (state-based degeneralized) automaton to output. There should be only one acceptance condition, and all the transitions of a state should be either all accepting or all unaccepting. If your automaton does not satisfies these requirements, call degeneralize() first.
opta string of option: 'c' to comment each state

Please direct any question, comment, or bug report to the Spot mailing list at spot@lrde.epita.fr.
Generated on Mon Feb 20 2017 07:08:25 for spot by doxygen 1.8.8