mCRL2
Loading...
Searching...
No Matches
modal_formula.cpp File Reference

Go to the source code of this file.

Namespaces

namespace  mcrl2
 A class that takes a linear process specification and checks all tau-summands of that LPS for confluence.
 
namespace  mcrl2::action_formulas
 
namespace  mcrl2::action_formulas::detail
 
namespace  mcrl2::regular_formulas
 
namespace  mcrl2::regular_formulas::detail
 
namespace  mcrl2::state_formulas
 
namespace  mcrl2::state_formulas::detail
 
namespace  mcrl2::state_formulas::algorithms
 

Functions

std::string mcrl2::action_formulas::pp (const action_formula &x)
 
std::string mcrl2::action_formulas::pp (const and_ &x)
 
std::string mcrl2::action_formulas::pp (const at &x)
 
std::string mcrl2::action_formulas::pp (const exists &x)
 
std::string mcrl2::action_formulas::pp (const false_ &x)
 
std::string mcrl2::action_formulas::pp (const forall &x)
 
std::string mcrl2::action_formulas::pp (const imp &x)
 
std::string mcrl2::action_formulas::pp (const multi_action &x)
 
std::string mcrl2::action_formulas::pp (const not_ &x)
 
std::string mcrl2::action_formulas::pp (const or_ &x)
 
std::string mcrl2::action_formulas::pp (const true_ &x)
 
std::set< data::variablemcrl2::action_formulas::find_all_variables (const action_formulas::action_formula &x)
 
action_formula mcrl2::action_formulas::detail::parse_action_formula (const std::string &text)
 
std::string mcrl2::regular_formulas::pp (const alt &x)
 
std::string mcrl2::regular_formulas::pp (const regular_formula &x)
 
std::string mcrl2::regular_formulas::pp (const seq &x)
 
std::string mcrl2::regular_formulas::pp (const trans &x)
 
std::string mcrl2::regular_formulas::pp (const trans_or_nil &x)
 
std::string mcrl2::regular_formulas::pp (const untyped_regular_formula &x)
 
regular_formula mcrl2::regular_formulas::detail::parse_regular_formula (const std::string &text)
 
std::string mcrl2::state_formulas::pp (const and_ &x)
 
std::string mcrl2::state_formulas::pp (const const_multiply &x)
 
std::string mcrl2::state_formulas::pp (const const_multiply_alt &x)
 
std::string mcrl2::state_formulas::pp (const delay &x)
 
std::string mcrl2::state_formulas::pp (const delay_timed &x)
 
std::string mcrl2::state_formulas::pp (const exists &x)
 
std::string mcrl2::state_formulas::pp (const false_ &x)
 
std::string mcrl2::state_formulas::pp (const forall &x)
 
std::string mcrl2::state_formulas::pp (const imp &x)
 
std::string mcrl2::state_formulas::pp (const infimum &x)
 
std::string mcrl2::state_formulas::pp (const may &x)
 
std::string mcrl2::state_formulas::pp (const minus &x)
 
std::string mcrl2::state_formulas::pp (const mu &x)
 
std::string mcrl2::state_formulas::pp (const must &x)
 
std::string mcrl2::state_formulas::pp (const not_ &x)
 
std::string mcrl2::state_formulas::pp (const nu &x)
 
std::string mcrl2::state_formulas::pp (const or_ &x)
 
std::string mcrl2::state_formulas::pp (const plus &x)
 
std::string mcrl2::state_formulas::pp (const state_formula &x)
 
std::string mcrl2::state_formulas::pp (const state_formula_specification &x)
 
std::string mcrl2::state_formulas::pp (const sum &x)
 
std::string mcrl2::state_formulas::pp (const supremum &x)
 
std::string mcrl2::state_formulas::pp (const true_ &x)
 
std::string mcrl2::state_formulas::pp (const variable &x)
 
std::string mcrl2::state_formulas::pp (const yaled &x)
 
std::string mcrl2::state_formulas::pp (const yaled_timed &x)
 
state_formula mcrl2::state_formulas::normalize_sorts (const state_formula &x, const data::sort_specification &sortspec)
 
state_formulas::state_formula mcrl2::state_formulas::translate_user_notation (const state_formulas::state_formula &x)
 
std::set< data::sort_expressionmcrl2::state_formulas::find_sort_expressions (const state_formulas::state_formula &x)
 
std::set< data::variablemcrl2::state_formulas::find_all_variables (const state_formulas::state_formula &x)
 
std::set< data::variablemcrl2::state_formulas::find_free_variables (const state_formulas::state_formula &x)
 
std::set< core::identifier_stringmcrl2::state_formulas::find_identifiers (const state_formulas::state_formula &x)
 
std::set< process::action_labelmcrl2::state_formulas::find_action_labels (const state_formulas::state_formula &x)
 
state_formula mcrl2::state_formulas::detail::parse_state_formula (const std::string &text)
 
state_formula_specification mcrl2::state_formulas::detail::parse_state_formula_specification (const std::string &text)
 
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.
 
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.
 
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.
 
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.
 
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.
 
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.
 
bool mcrl2::state_formulas::algorithms::is_monotonous (const state_formula &f)
 Returns true if the state formula is monotonous.
 
state_formula mcrl2::state_formulas::algorithms::normalize (const state_formula &x, bool quantitative=false, bool negated=false)
 
bool mcrl2::state_formulas::algorithms::is_normalized (const state_formula &x)
 Checks if a state formula is normalized.
 
bool mcrl2::state_formulas::algorithms::is_timed (const state_formula &x)
 
std::set< core::identifier_stringmcrl2::state_formulas::algorithms::find_state_variable_names (const state_formula &x)
 Returns the names of the state variables that occur in x.