Rabin/streett pairs used by is_rabin_like and is_streett_like. More...

Collaboration diagram for spot::acc_cond::rs_pair:

Public Member Functions
	rs_pair (const rs_pair &)=default

rs_pair &	operator= (const rs_pair &)=default

	rs_pair (acc_cond::mark_t fin, acc_cond::mark_t inf) noexcept

bool	operator== (rs_pair o) const

bool	operator!= (rs_pair o) const

bool	operator< (rs_pair o) const

bool	operator<= (rs_pair o) const

bool	operator> (rs_pair o) const

bool	operator>= (rs_pair o) const

Detailed Description

Rabin/streett pairs used by is_rabin_like and is_streett_like.

These pairs hold two marks which can each contain one or no set number.

For instance is_streett_like() rewrites Inf(0)&(Inf(2)|Fin(1))&Fin(3) as three pairs: [(fin={},inf={0}),(fin={1},inf={2}),(fin={3},inf={})].

Empty marks should be interpreted in a way that makes them false in Streett, and true in Rabin.

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

Public Member Functions