mcrl2/modal_formula/algorithms.h

Include file:

#include "mcrl2/modal_formula/algorithms.h"

add your file description here.

Functions

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_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.

bool is_normalized(const state_formula &x)

Checks if a state formula is normalized.

Returns: True if the state formula is normalized

state_formula normalize(const state_formula &x)

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

state_formula parse_state_formula(std::istream &in, lps::specification &spec)

Parses a state formula from an input stream.

Parameters:

• in A stream from which can be read

• spec A linear process specification

Returns: The converted modal formula

state_formula parse_state_formula(const std::string &formula_text, lps::specification &spec)

Parses a state formula from text.

Parameters:

• formula_text A string

• spec A linear process specification

Returns: The converted modal formula

state_formula_specification parse_state_formula_specification(std::istream &in)

Parses a state formula specification from an input stream.

state_formula_specification parse_state_formula_specification(const std::string &text)

Parses a state formula specification from text.

state_formula_specification parse_state_formula_specification(std::istream &in, lps::specification &lpsspec)

Parses a state formula specification from an input stream.

state_formula_specification parse_state_formula_specification(const std::string &text, lps::specification &lpsspec)

Parses a state formula specification from text.