Algorithms related to the temporal hierarchy

Enumerations
enum class	spot::prcheck { Auto , via_CoBuchi , via_Rabin , via_Parity }
	Enum used to change the behavior of is_persistence() or is_recurrence(). More...

Functions
bool	spot::is_persistence (formula f, twa_graph_ptr aut=nullptr, prcheck algo=prcheck::Auto)
	Return true if f represents a persistence property. More...
bool	spot::is_recurrence (formula f, twa_graph_ptr aut=nullptr, prcheck algo=prcheck::Auto)
	Return true if f represents a recurrence property. More...
bool	spot::is_obligation (formula f, twa_graph_ptr aut=nullptr, ocheck algo=ocheck::Auto)
	Return true if f has the recurrence property. More...
char	spot::mp_class (formula f)
	Return the class of f in the temporal hierarchy of Manna and Pnueli (PODC'90). More...
std::string	spot::mp_class (formula f, const char *opt)
	Return the class of f in the temporal hierarchy of Manna and Pnueli (PODC'90). More...
std::string	spot::mp_class (char mpc, const char *opt)
	Expand a class in the temporal hierarchy of Manna and Pnueli (PODC'90). More...

Detailed Description

Enumeration Type Documentation

prcheck

enum class spot::prcheck

strong

#include <spot/tl/hierarchy.hh>

Enum used to change the behavior of is_persistence() or is_recurrence().

If PR_Auto, both methods will first check the environment variable SPOT_PR_CHECK to see if one algorithm or the other is wanted to be forced. Otherwise, it will make the most appropriate decision.

If PR_via_Rabin, they will check if the formula is detbuchi_realizable going through a rabin automaton: TGBA->DPA->DRA->(D?)BA.

If PR_via_CoBuchi, they will check if the formula is cobuchi_realizable.

If PR_via_Parity, they will check if the formula is detbuchi/cobuchi-realizable by calling reduce_parity() on a DPA.

Note that is_persistence() and is_recurrence() will work on a formula f or its negation because of the duality of both classes (see https://spot.lrde.epita.fr/hierarchy.html for details). For instance if is_recurrence() wants to use PR_via_CoBuchi it will check if !f is cobuchi_realizable.

Function Documentation

is_obligation()

bool spot::is_obligation	(	formula	f,
		twa_graph_ptr	aut = nullptr,
		ocheck	algo = ocheck::Auto
	)

#include <spot/tl/hierarchy.hh>

Return true if f has the recurrence property.

Actually, it calls is_persistence() with the negation of f.

Parameters

f	the formula to check.
aut	the corresponding automaton (not required).
algo	the algorithm to use.

aut is constructed from f if not supplied.

If algo is ocheck::via_WDBA, aut is converted into a WDBA which is then checked for equivalence with aut. If algo is ocheck::via_CoBuchi, we test that both f and !f are co-Büchi realizable. If algo is ocheck::via_Rabin, we test that both f and !f are DBA-realizable.

Auto currently defaults to via_WDBA, unless the SPOT_O_CHECK environment variable specifies otherwise.

is_persistence()

bool spot::is_persistence	(	formula	f,
		twa_graph_ptr	aut = nullptr,
		prcheck	algo = prcheck::Auto
	)

#include <spot/tl/hierarchy.hh>

Return true if f represents a persistence property.

Parameters

f	the formula to check.
aut	the corresponding automaton (not required).
algo	the algorithm to use (see enum class prcheck).

is_recurrence()

bool spot::is_recurrence	(	formula	f,
		twa_graph_ptr	aut = nullptr,
		prcheck	algo = prcheck::Auto
	)

#include <spot/tl/hierarchy.hh>

Return true if f represents a recurrence property.

Actually, it calls is_persistence() with the negation of f.

Parameters

f	the formula to check.
aut	the corresponding automaton (not required).
algo	the algorithm to use (see enum class prcheck).

mp_class() [1/3]

std::string spot::mp_class	(	char	mpc,
		const char *	opt
	)

#include <spot/tl/hierarchy.hh>

Expand a class in the temporal hierarchy of Manna and Pnueli (PODC'90).

mpc should be a character among B, G, S, O, P, R, T specifying a class in the hierarchy.

The opt parameter should be a string specifying options for expressing the class. If opt is empty, the result is mpc. If opt contains 'w', then the string contains all the characters corresponding to the super-classes of mpc. If opt contains 'v', then the characters are replaced by the name of each class. Space and commas are ignored. Any ']' ends the processing of the options.

mp_class() [2/3]

char spot::mp_class

(

formula

f

)

#include <spot/tl/hierarchy.hh>

Return the class of f in the temporal hierarchy of Manna and Pnueli (PODC'90).

The class is indicated using a character among:

• 'B' (bottom) safety properties that are also guarantee properties
• 'G' guarantee properties that are not also safety properties
• 'S' safety properties that are not also guarantee properties
• 'O' obligation properties that are not safety or guarantee properties
• 'P' persistence properties that are not obligations
• 'R' recurrence properties that are not obligations
• 'T' (top) properties that are not persistence or recurrence properties

mp_class() [3/3]

std::string spot::mp_class	(	formula	f,
		const char *	opt
	)

#include <spot/tl/hierarchy.hh>

Return the class of f in the temporal hierarchy of Manna and Pnueli (PODC'90).

The opt parameter should be a string specifying options for expressing the class. If opt is empty, the result is one character among B, G, S, O, P, R, T, specifying the most precise class to which the formula belongs. If opt contains 'w', then the string contains all the characters corresponding to the classes that contain f. If opt contains 'v', then the characters are replaced by the name of each class. Space and commas are ignored. Any ']' ends the processing of the options.