Include file:

#include "mcrl2/pbes/lts2pbes.h"

add your file description here.


pbes mcrl2::pbes_system::lts2pbes(const lts::lts_lts_t &l, const state_formulas::state_formula_specification &formspec, bool preprocess_modal_operators = false, bool generate_counter_example = false)

Translates an LTS and a modal formula into a PBES that represents the corresponding model checking problem.


  • l A labelled transition system.
  • formspec A modal formula specification.
  • preprocess_modal_operators A boolean indicating that modal operators must be preprocessed.
  • generate_counter_example A boolean indicating that a counter example must be generated.