Include file:

#include "mcrl2/pbes/lps2pbes.h
class mcrl2::pbes_system::lps2pbes_algorithm

Algorithm for translating a state formula and a timed specification to a pbes.

Protected attributes

bool mcrl2::pbes_system::lps2pbes_algorithm::m_check_only
data::set_identifier_generator mcrl2::pbes_system::lps2pbes_algorithm::m_generator

Protected member functions

void run(const state_formulas::state_formula &f, bool structured, bool unoptimized, std::vector<pbes_equation> &equations, Parameters &parameters)

Public member functions

lps2pbes_algorithm(bool check_only = false)


pbes run(const state_formulas::state_formula &formula, const lps::specification &lpsspec, bool structured = false, bool unoptimized = false, bool preprocess_modal_operators = false, bool generate_counter_example = false, const data::variable &T = data::undefined_real_variable())

Runs the translation algorithm.


  • formula A modal formula that represents a property about the system modeled by the given specification
  • lpsspec A linear process specification
  • structured use the ‘structured’ approach of generating equations
  • unoptimized do not optimize the resulting PBES.
  • preprocess_modal_operators insert dummy fixpoints in modal operators, which may lead to smaller PBESs
  • generate_counter_example If true, then the PBES is enhanced with additional equations that are used to extract a counter example.
  • T The time parameter. If T == data::variable() the untimed version of lps2pbes is applied.

Returns: A PBES that encodes the property applied to the given specification