Simplify a reactive specification, preserving realizability. More...

Inheritance diagram for spot::realizability_simplifier_base:

Collaboration diagram for spot::realizability_simplifier_base:

Public Types
enum	realizability_simplifier_option { polarity = 1 , global_equiv = 2 , global_equiv_output_only = 6 , global_equiv_moore = 10 }
	Options for realizability simplification. More...

typedef std::vector< std::tuple< formula, bool, formula > >	mapping_t
	Mapping from removed to replacement formulas.

Public Member Functions
	realizability_simplifier_base (const std::vector< std::string > &in_or_out, bool is_input, unsigned options=polarity\|global_equiv, std::ostream *verbose=nullptr)
	Build a realizability simplifier.

std::pair< formula, mapping_t >	simplify (formula f)
	Simplify a formula, returning a mapping.

Protected Attributes
data *	data_
	Internal implementation data.

Detailed Description

Simplify a reactive specification, preserving realizability.

Member Typedef Documentation

Mapping from removed to replacement formulas.

Options for realizability simplification.

Enumerator
polarity	remove APs with single polarity
global_equiv	remove equivalent APs (Mealy semantics)
global_equiv_output_only	likewise, but don't consider equivalent input and output (Mealy semantics)
global_equiv_moore	remove equivalent APs (Moore semantics)

spot::realizability_simplifier_base::realizability_simplifier_base	(	const std::vector< std::string > &	in_or_out,
		bool	is_input,
		unsigned	options = `polarity\|global_equiv`,
		std::ostream *	verbose = `nullptr`
	)

Build a realizability simplifier.

std::pair< formula, mapping_t > spot::realizability_simplifier_base::simplify ( formula f )

Simplify a formula, returning a mapping.

data* spot::realizability_simplifier_base::data_

protected

Internal implementation data.

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