mcrl2::state_formulas::algorithms Namespace Reference

Functions
state_formula	parse_state_formula (std::istream &in, lps::stochastic_specification &spec, const bool formula_is_quantitative)
	Parses a state formula from an input stream.
state_formula	parse_state_formula (const std::string &formula_text, lps::stochastic_specification &spec, const bool formula_is_quantitative)
	Parses a state formula from text.
state_formula_specification	parse_state_formula_specification (std::istream &in, const bool formula_is_quantitative)
	Parses a state formula specification from an input stream.
state_formula_specification	parse_state_formula_specification (const std::string &text, const bool formula_is_quantitative)
	Parses a state formula specification from text.
state_formula_specification	parse_state_formula_specification (std::istream &in, lps::stochastic_specification &lpsspec, const bool formula_is_quantitative)
	Parses a state formula specification from an input stream.
state_formula_specification	parse_state_formula_specification (const std::string &text, lps::stochastic_specification &lpsspec, const bool formula_is_quantitative)
	Parses a state formula specification from text.
bool	is_monotonous (const state_formula &f)
	Returns true if the state formula is monotonous.
state_formula	normalize (const state_formula &x)
	Normalizes a state formula, i.e. removes any occurrences of ! or =>.
bool	is_normalized (const state_formula &x)
	Checks if a state formula is normalized.
std::set< core::identifier_string >	find_state_variable_names (const state_formula &x)
	Returns the names of the state variables that occur in x.
bool	is_timed (const state_formula &x)
state_formula	normalize (const state_formula &x, bool quantitative=false, bool negated=false)

Function Documentation

find_state_variable_names()

std::set< core::identifier_string > mcrl2::state_formulas::algorithms::find_state_variable_names

(

const state_formula &

x

)

Returns the names of the state variables that occur in x.

Definition at line 207 of file modal_formula.cpp.

is_monotonous()

bool mcrl2::state_formulas::algorithms::is_monotonous

(

const state_formula &

f

)

Returns true if the state formula is monotonous.

Parameters

f	A modal formula

Returns

True if the state formula is monotonous.

Definition at line 187 of file modal_formula.cpp.

is_normalized()

bool mcrl2::state_formulas::algorithms::is_normalized

(

const state_formula &

x

)

Checks if a state formula is normalized.

Returns

True if the state formula is normalized

Definition at line 197 of file modal_formula.cpp.

is_timed()

bool mcrl2::state_formulas::algorithms::is_timed

(

const state_formula &

x

)

Definition at line 202 of file modal_formula.cpp.

normalize() [1/2]

state_formula mcrl2::state_formulas::algorithms::normalize

(

const state_formula &

x

)

Normalizes a state formula, i.e. removes any occurrences of ! or =>.

normalize() [2/2]

state_formula mcrl2::state_formulas::algorithms::normalize	(	const state_formula &	x,
		bool	quantitative = false,
		bool	negated = false
	)

Definition at line 192 of file modal_formula.cpp.

parse_state_formula() [1/2]

state_formula mcrl2::state_formulas::algorithms::parse_state_formula	(	const std::string &	formula_text,
		lps::stochastic_specification &	spec,
		const bool	formula_is_quantitative
	)

Parses a state formula from text.

Parameters

formula_text	A string
spec	A linear process specification
formula_is_quantitative	True if the formula is interpreted as a quantitative formula, instead of a classic boolean modal formula.

Returns

The converted modal formula

Definition at line 162 of file modal_formula.cpp.

parse_state_formula() [2/2]

state_formula mcrl2::state_formulas::algorithms::parse_state_formula	(	std::istream &	in,
		lps::stochastic_specification &	spec,
		const bool	formula_is_quantitative
	)

Parses a state formula from an input stream.

Parameters

in	A stream from which can be read
spec	A linear process specification
formula_is_quantitative	True if the formula is interpreted as a quantitative formula, instead of a classic boolean modal formula.

Returns

The converted modal formula

Definition at line 157 of file modal_formula.cpp.

parse_state_formula_specification() [1/4]

state_formula_specification mcrl2::state_formulas::algorithms::parse_state_formula_specification	(	const std::string &	text,
		const bool	formula_is_quantitative
	)

Parses a state formula specification from text.

Definition at line 172 of file modal_formula.cpp.

parse_state_formula_specification() [2/4]

state_formula_specification mcrl2::state_formulas::algorithms::parse_state_formula_specification	(	const std::string &	text,
		lps::stochastic_specification &	lpsspec,
		const bool	formula_is_quantitative
	)

Parses a state formula specification from text.

Definition at line 182 of file modal_formula.cpp.

parse_state_formula_specification() [3/4]

state_formula_specification mcrl2::state_formulas::algorithms::parse_state_formula_specification	(	std::istream &	in,
		const bool	formula_is_quantitative
	)

Parses a state formula specification from an input stream.

Definition at line 167 of file modal_formula.cpp.

parse_state_formula_specification() [4/4]

state_formula_specification mcrl2::state_formulas::algorithms::parse_state_formula_specification	(	std::istream &	in,
		lps::stochastic_specification &	lpsspec,
		const bool	formula_is_quantitative
	)

Parses a state formula specification from an input stream.

Definition at line 177 of file modal_formula.cpp.