mcrl2::bes::detail::standard_form_traverser¶

Include file:

#include "mcrl2/bes/normal_forms.h

class mcrl2::bes::detail::standard_form_traverser¶: Traverser that implements the standard form normalization.

Public types¶

type mcrl2::bes::detail::standard_form_traverser::super¶: typedef for bes::boolean_expression_traverser< standard_form_traverser >

Public attributes¶

std::vector<boolean_equation> mcrl2::bes::detail::standard_form_traverser::m_equations¶: A vector containing generated equations.

std::vector<boolean_equation> mcrl2::bes::detail::standard_form_traverser::m_equations2¶: A vector containing generated equations with new variables.

std::vector<standard_form_pair> mcrl2::bes::detail::standard_form_traverser::m_expression_stack¶: A stack containing sub-terms.

boolean_expression mcrl2::bes::detail::standard_form_traverser::m_false¶: The expression corresponding to false.

utilities::number_postfix_generator mcrl2::bes::detail::standard_form_traverser::m_generator¶: For generating fresh variables.

bool mcrl2::bes::detail::standard_form_traverser::m_has_false¶: Is set to true if the value false is encountered in the BES.

bool mcrl2::bes::detail::standard_form_traverser::m_has_true¶: Is set to true if the value true is encountered in the BES.

std::string mcrl2::bes::detail::standard_form_traverser::m_name¶: The name of the variable of the current equation, with a trailing underscore added.

bool mcrl2::bes::detail::standard_form_traverser::m_recursive_form¶: If true, the result will be in standard recursive normal form, otherwise in standard form.

fixpoint_symbol mcrl2::bes::detail::standard_form_traverser::m_symbol¶: The fixpoint symbol of the current equation.

std::map<boolean_expression, boolean_variable> mcrl2::bes::detail::standard_form_traverser::m_table¶: Maps right hand sides of equations to their corresponding left hand side.

boolean_expression mcrl2::bes::detail::standard_form_traverser::m_true¶: The expression corresponding to true.

Public member functions¶

boolean_variable create_variable(const boolean_expression &expr, standard_form_type type, const std::string &hint)¶

Generates an equation var=expr for the expression expr (if it does not exist).

Returns: The variable var.

void enter(const boolean_equation &eq)¶: Enter an equation.

void enter(const boolean_equation_system &x)¶: Enter a boolean equation system.

void enter(const boolean_variable &x)¶

Enter boolean_variable node.

Parameters:

x A boolean variable.

void enter(const false_ &x)¶

Enter false node.

Parameters:

x A term

void enter(const true_ &x)¶

Enter true node.

Parameters:

x A term.

const std::vector<boolean_equation> &equations() const: Returns the generated equations.

boolean_variable fresh_variable(const std::string &hint)¶: Generates a fresh boolean variable.

void leave(const and_&)¶: Leave and node.

void leave(const boolean_equation &eq)¶: Leave an equation.

void leave(const boolean_equation_system&)¶: Leave a boolean equation system.

void leave(const imp&)¶: Leave imp node.

void leave(const not_&)¶: Leave not node.

void leave(const or_&)¶: Leave or node.

standard_form_pair pop(): Pops the stack and returns the popped element.

void push(const boolean_expression &first, standard_form_type second)¶: Pushes (first, second) on the stack.

boolean_expression result() const¶: Returns the top element of the expression stack, which is the result of the normalization.

standard_form_traverser(bool recursive_form = false)¶

Constructor.

Parameters:

recursive_form Determines whether or not the result will be in standard recursive normal form.