Help printing BDDs as text, using aliases. More...

#include <spot/twaalgos/hoa.hh>

Collaboration diagram for spot::hoa_alias_formater:

Public Types
typedef std::vector< std::pair< std::string, bdd > >	aliases_t

Public Member Functions
	hoa_alias_formater (const const_twa_graph_ptr &aut, const char false_str, const char true_str, const char or_str, const char and_str, const char not_str, const char lpar_str, const char *rpar_str, std::function< std::string(int)> ap_printer)
	Initialize this class from the aliases defined for an automaton. More...

std::string	encode_label (bdd label, unsigned aliases_start=0)
	Attempt to format a BDD label using aliases. More...

aliases_t *	aliases ()
	Retrieve the list of aliases. More...

Detailed Description

Help printing BDDs as text, using aliases.

Constructor & Destructor Documentation

◆ hoa_alias_formater()

spot::hoa_alias_formater::hoa_alias_formater	(	const const_twa_graph_ptr &	aut,
		const char *	false_str,
		const char *	true_str,
		const char *	or_str,
		const char *	and_str,
		const char *	not_str,
		const char *	lpar_str,
		const char *	rpar_str,
		std::function< std::string(int)>	ap_printer
	)

Initialize this class from the aliases defined for an automaton.

The aliases are taken from the named-property "aliases", defined in the automaton. If no such named-property exist, the aliases() method will return a null pointer.

Note that any alias that uses an atomic proposition not registered in the automaton is not only ignored, but also removed from the alias list stored in the automaton.

The or_str, and_str, and ap_printer arguments are used to print operators OR, AND, and to print atomic propositions that are not aliases. lpar_str and rpar_str are used to group conjuncts that appear in a disjunction.

Member Function Documentation

◆ aliases()

aliases_t* spot::hoa_alias_formater::aliases ( )

inline

Retrieve the list of aliases.

This points to the same list that the automaton's "aliasaes" named properties points to. Will return nullptr if no aliases are defined.

Note: Aliases involving atomic propositions that are not declared in the automaton have been removed by this class' constructor.

◆ encode_label()

std::string spot::hoa_alias_formater::encode_label	(	bdd	label,
		unsigned	aliases_start = `0`
	)

Attempt to format a BDD label using aliases.

The returned pair should be interpreted as a disjunction between an expression involving aliases, and a BDD that could not be expressed using aliases.

The conversion works in several attempts, in the following order:

If an alias A exists for label, "@A" is returned.
If an alias A exists for the negation of label, "!@A" is returned.
If label is true or false, true_str or false_str are returned as specified at construction.
If label can be built as a disjunction of positive aliases, such a disjunction is returned as "@A | @B | @C".
If label can be built from a conjunction of aliases or negated aliases, it is returned as "@A&!@B&@C". Note that this check first attempt to use aliases that represent cubes before trying other aliases.
Otherwise label is split in irredundant-sum-of-products and each clause is encoded as a conjunctions of (possibly negated) aliases using only those that are cubes. Any remaining literal is encoded with the ap_printer() function passed to the constructor.

The aliases to be used are those returned by the aliases() method. The vector returned by aliases() is scanned from position aliases_start. As this vector is stored in the opposite order of how aliases should be stored in the HOA output, adjusting aliases_start is helpful to encode an aliases using only previously defined aliases (i.e., aliases that appear later in the sequence returned by aliases()).

The documentation for this class was generated from the following file:

spot/twaalgos/hoa.hh