Classes
struct	spot::hoa_abort
	Exception thrown by the HOA lexer upon reading an "--ABORT--" marker. More...

struct	spot::parsed_aut
	Result of the automaton parser. More...

struct	spot::automaton_parser_options
	Options controlling the behavior of the automaton stream parser. More...

class	spot::automaton_stream_parser
	Parse a stream of automata. More...

class	spot::hoa_alias_formater
	Help printing BDDs as text, using aliases. 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
	Shared pointer to parsed_aut. More...

typedef std::shared_ptr< const parsed_aut >	spot::const_parsed_aut_ptr
	Shared pointer to const parsed_aut. More...

Enumerations
enum class	spot::parsed_aut_type { HOA , NeverClaim , LBTT , DRA , DSA , PGAME , Unknown }
	Format type of a parsed automaton. More...

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_aiger (std::ostream &os, const_aig_ptr circuit)
	Print the aig to stream in AIGER format. More...

std::ostream &	spot::print_aiger (std::ostream &os, const const_twa_graph_ptr &aut, const char mode, const std::string terminating_signal=nullptr)
	Encode and print an automaton as an AIGER circuit. 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_dot (std::ostream &os, aig_ptr circuit, const char *=nullptr)
	Print an AIG circuit 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::vector< std::pair< std::string, bdd > > *	spot::get_aliases (const const_twa_ptr &g)
	Obtain aliases used in the HOA format. More...

void	spot::set_aliases (twa_ptr g, const std::vector< std::pair< std::string, bdd >> &aliases)
	Define all aliases used in the HOA format. More...

void	spot::create_alias_basis (const twa_graph_ptr &aut)
	Create an alias basis. 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...

void	spot::hoayyreset (void *scanner)
	Reset the HOA lexer state. More...

int	spot::hoayyopen (const std::string &name, void **scanner)
	Open an HOA file from a path. More...

int	spot::hoayyopen (int fd, void **scanner)
	Open an HOA file from a descriptor. More...

int	spot::hoayystring (const char data, void *scanner)
	Scan HOA data from a string. More...

void	spot::hoayyclose (void *scanner)
	Close the HOA lexer. More...

Detailed Description

Typedef Documentation

◆ const_parsed_aut_ptr

typedef std::shared_ptr<const parsed_aut> spot::const_parsed_aut_ptr

#include <spot/parseaut/public.hh>

Shared pointer to const parsed_aut.

◆ parse_aut_error

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

#include <spot/parseaut/public.hh>

A parse diagnostic with its location.

◆ parse_aut_error_list

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.

◆ parsed_aut_ptr

typedef std::shared_ptr<parsed_aut> spot::parsed_aut_ptr

#include <spot/parseaut/public.hh>

Shared pointer to parsed_aut.

Enumeration Type Documentation

◆ parsed_aut_type

enum spot::parsed_aut_type

strong

#include <spot/parseaut/public.hh>

Format type of a parsed automaton.

Function Documentation

◆ create_alias_basis()

void spot::create_alias_basis ( const twa_graph_ptr & aut )

#include <spot/twaalgos/hoa.hh>

Create an alias basis.

This uses spot::edge_separator to build a set of alias that can be used as a basis for all labels of the automaton.

Such a basis can be used to shorten the size of an output file when printing in HOA format (actually, calling print_hoa() with option 'b' will call this function). Such a basis may also be useful to help visualize an automaton (using spot::print_dot's @ option) when its labels are too large.

◆ get_aliases()

std::vector<std::pair<std::string, bdd> >* spot::get_aliases ( const const_twa_ptr & g )

#include <spot/twaalgos/hoa.hh>

Obtain aliases used in the HOA format.

Aliases are stored as a vector of pairs (name, bdd). The bdd is expected to use only variable registered by g.

◆ hoayyclose()

void spot::hoayyclose ( void * scanner )

#include <spot/parseaut/parsedecl.hh>

Close the HOA lexer.

◆ hoayyopen() [1/2]

int spot::hoayyopen	(	const std::string &	name,
		void **	scanner
	)

#include <spot/parseaut/parsedecl.hh>

Open an HOA file from a path.

◆ hoayyopen() [2/2]

int spot::hoayyopen	(	int	fd,
		void **	scanner
	)

#include <spot/parseaut/parsedecl.hh>

Open an HOA file from a descriptor.

◆ hoayyreset()

void spot::hoayyreset ( void * scanner )

#include <spot/parseaut/parsedecl.hh>

Reset the HOA lexer state.

◆ hoayystring()

int spot::hoayystring	(	const char *	data,
		void **	scanner
	)

#include <spot/parseaut/parsedecl.hh>

Scan HOA data from a string.

◆ parse_aut()

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

filename	The name of the file to parse.
dict	The BDD dictionary where to use.
env	The environment of atomic proposition into which parsing should take place.
opts	Additional 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 denotes the end of a stream.)

Warning: This function is not reentrant.

◆ print_aiger() [1/2]

std::ostream& spot::print_aiger	(	std::ostream &	os,
		const const_twa_graph_ptr &	aut,
		const char *	mode,
		const std::string *	terminating_signal = `nullptr`
	)

#include <spot/twaalgos/aiger.hh>

Encode and print an automaton as an AIGER circuit.

The circuit actually encodes the transition relation of the automaton, not its acceptance condition. Therefore, this function will reject automata whose acceptance condition is not trivial (i.e. true). States are encoded by latches (or registers) in the circuit. Atomic propositions are encoded as inputs and outputs of the circuit. To know which AP should be encoded as outputs, print_aiger() relies on the named property "synthesis-outputs", which is a bdd containing the conjunction of such output propositions. All other AP are encoded as inputs. If the named property is not set, all AP are encoded as inputs, and the circuit has no output.

Precondition: In order to ensure correctness, edge conditions have to have the form (input cond) & (output cond). The output cond does not need to be a minterm. Correct graphs are generated by spot::unsplit_2step

Parameters

os	The output stream to print on.
aut	The automaton to output.
mode	This param has to be of the form `ite\|isop\|both [+dc][+ud][+sub0\|+sub1\|+sub2]` Where `ite` means encoded via if-then-else normal form, `isop` means encoded via irredundant sum-of-products, `both` means trying both encodings to keep the smaller one. `+dc` is optional and tries to take advantage of "do not care" outputs to minimize the encoding. `+dual` is optional and indicates that the algorithm should also try to encode the negation of each condition in case its encoding is smaller. `+subN` indicates that the conditions can be separated into blocks with `sub0` being no separation, `sub1` separation into input/latches/gates (`isop` only) and `sub2` tries to seek common subformulas.
terminating_signal	If non-null, specifies the name of an extra output signal that is initially true and becomes false after the first self-loop (termination) of the Mealy machine.

◆ print_aiger() [2/2]

std::ostream& spot::print_aiger	(	std::ostream &	os,
		const_aig_ptr	circuit
	)

#include <spot/twaalgos/aiger.hh>

Print the aig to stream in AIGER format.

◆ print_dot() [1/2]

std::ostream& spot::print_dot	(	std::ostream &	os,
		aig_ptr	circuit,
		const char *	= `nullptr`
	)

#include <spot/twaalgos/dot.hh>

Print an AIG circuit in dot format.

◆ print_dot() [2/2]

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.

Parameters

os	output stream
g	automaton to print
options	an 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.

◆ print_hoa()

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

os	The output stream to print on.
g	The automaton to output.
opt	a set of characters each corresponding to a possible option: (b) create an alias basis if more >=2 AP are used, (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.

◆ print_lbtt()

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

g	The automaton to print.
os	Where to print.
opt	if "t", force transition-based acceptance, otherwise,

◆ print_never_claim()

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

os	The output stream to print on.
g	The (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 satisfy these requirements, call degeneralize() first.
opt	a string of option: 'c' to comment each state

◆ set_aliases()

void spot::set_aliases	(	twa_ptr	g,
		const std::vector< std::pair< std::string, bdd >> &	aliases
	)

#include <spot/twaalgos/hoa.hh>

Define all aliases used in the HOA format.

Aliases are stored as a vector of pairs (name, bdd). The bdd is expected to use only variable registered by g.

Pass an empty vector to remove existing aliases.

Classes

Typedefs

Enumerations

Functions

Detailed Description

Typedef Documentation

◆ const_parsed_aut_ptr

◆ parse_aut_error

◆ parse_aut_error_list

◆ parsed_aut_ptr

Enumeration Type Documentation

◆ parsed_aut_type

Function Documentation

◆ create_alias_basis()

◆ get_aliases()

◆ hoayyclose()

◆ hoayyopen() [1/2]

◆ hoayyopen() [2/2]

◆ hoayyreset()

◆ hoayystring()

◆ parse_aut()

◆ print_aiger() [1/2]

◆ print_aiger() [2/2]

◆ print_dot() [1/2]

◆ print_dot() [2/2]

◆ print_hoa()

◆ print_lbtt()

◆ print_never_claim()

◆ set_aliases()