mcrl2::bes::boolean_equation_system

Include file:

#include "mcrl2/bes/boolean_equation_system.h
class mcrl2::bes::boolean_equation_system

boolean equation system

Public types

type equation_type

typedef for boolean_equation

Protected attributes

std::vector<boolean_equation> m_equations

The equations.

boolean_expression m_initial_state

The initial state.

Protected member functions

void init_term(const atermpp::aterm_appl &t)

Initialize the boolean_equation_system with an atermpp::aterm_appl.

Parameters:

  • t A term

Public member functions

std::set<boolean_variable> binding_variables() const

Returns the set of binding variables of the boolean_equation_system, i.e. the variables that occur on the left hand side of an equation.

Returns: The binding variables of the equation system

boolean_equation_system()

Constructor.

boolean_equation_system(const std::vector<boolean_equation> &equations, boolean_expression initial_state)

Constructor.

Parameters:

  • equations A sequence of boolean equations
  • initial_state An initial state
const std::vector<boolean_equation> &equations() const

Returns the equations.

Returns: The equations

std::vector<boolean_equation> &equations()

Returns the equations.

Returns: The equations

const boolean_expression &initial_state() const

Returns the initial state.

Returns: The initial state.

boolean_expression &initial_state()

Returns the initial state.

Returns: The initial state.

bool is_closed() const

Returns true if all occurring variables are binding variables.

Returns: True if the equation system is closed

bool is_well_typed() const

Returns true. Some checks will be added later.

Returns: The value true.

void load(std::istream &stream, bool binary = true, const std::string &source = "")

Reads the boolean equation system from a stream.

Parameters:

  • stream The stream to read from.
  • binary An indicaton whether the stream is in binary format.
  • source The source from which the stream originates. Used for error messages.
std::set<boolean_variable> occurring_variables() const

Returns the set of occurring variables of the boolean_equation_system, i.e. the variables that occur in the right hand side of an equation or in the initial state.

Returns: The occurring variables of the equation system

void save(std::ostream &stream, bool binary = true) const

Writes the boolean equation system to a stream.

Parameters:

  • binary If binary is true the boolean equation system is saved in compressed binary format. Otherwise an ascii representation is saved. In general the binary format is much more compact than the ascii representation.
  • stream An output stream
  • binary If true, the file is saved in binary format