spot::realizability_simplifier_base Class Reference

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

#include <spot/tl/apcollect.hh>

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 }
typedef std::vector< std::tuple< formula, bool, formula > >	mapping_t

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)
std::pair< formula, mapping_t >	simplify (formula f)
	Simplify a formula, returning a mapping. More...

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

Enumerator
polarity	remove APs with single polarity
global_equiv	remove equivalent APs
global_equiv_output_only	likewise, but don't consider equivalent input and output

Member Function Documentation

simplify()

std::pair< formula, mapping_t > spot::realizability_simplifier_base::simplify

(

formula

f

)

Simplify a formula, returning a mapping.

---

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

• spot/tl/apcollect.hh