mcrl2/pbes/lts2pbes.h

Include file:

#include "mcrl2/pbes/lts2pbes.h"

add your file description here.

Functions

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.

Parameters:

  • 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.