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

#include <spot/tl/apcollect.hh>

Inheritance diagram for spot::realizability_simplifier:

Collaboration diagram for spot::realizability_simplifier:

Public Types
enum	realizability_simplifier_option { polarity = 1 , global_equiv = 2 , global_equiv_output_only = 6 , global_equiv_moore = 10 }

typedef std::vector< std::tuple< formula, bool, formula > >	mapping_t

Public Member Functions
	realizability_simplifier (formula f, const std::vector< std::string > &inputs, unsigned options=polarity\|global_equiv, std::ostream *verbose=nullptr)

formula	simplified_formula () const
	Return the simplified formula.

const std::vector< std::tuple< formula, bool, formula > > &	get_mapping () const
	Returns a vector of (from,from_is_input,to)

void	merge_mapping (const realizability_simplifier &other)
	Augment the current mapping with output variable renaming from another realizability_simplifier.

void	patch_mealy (twa_graph_ptr mealy) const
	Patch a Mealy machine to add the missing APs.

void	patch_game (twa_graph_ptr mealy) const
	Patch a game to add the missing APs.

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

Protected Attributes
data *	data_

Detailed Description

Simplify a reactive specification, preserving realizability.

Member Enumeration Documentation

◆ realizability_simplifier_option

enum spot::realizability_simplifier_base::realizability_simplifier_option

inherited

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)

Member Function Documentation

◆ get_mapping()

const std::vector< std::tuple< formula, bool, formula > > & spot::realizability_simplifier::get_mapping ( ) const

inline

Returns a vector of (from,from_is_input,to)

◆ merge_mapping()

void spot::realizability_simplifier::merge_mapping ( const realizability_simplifier & other )

Augment the current mapping with output variable renaming from another realizability_simplifier.

◆ patch_game()

void spot::realizability_simplifier::patch_game ( twa_graph_ptr mealy ) const

Patch a game to add the missing APs.

◆ patch_mealy()

void spot::realizability_simplifier::patch_mealy ( twa_graph_ptr mealy ) const

Patch a Mealy machine to add the missing APs.

◆ simplified_formula()

formula spot::realizability_simplifier::simplified_formula ( ) const

inline

Return the simplified formula.

◆ simplify()

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

inherited

Simplify a formula, returning a mapping.

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

spot/tl/apcollect.hh

Public Types

Public Member Functions

Protected Attributes