mcrl2/pbes/lts2pbes.h

Include file:

#include "mcrl2/pbes/lts2pbes.h"

add your file description here.

Classes

• mcrl2::pbes_system::lts2pbes_algorithm

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.