mCRL2
Loading...
Searching...
No Matches
mcrl2::pbes_system::pbesinst_structure_graph_algorithm Class Reference

Variant of pbesinst that will compute a structure graph for a PBES. The result will be put in the structure graph that is passed in the constructor. More...

#include <pbesinst_structure_graph.h>

Inheritance diagram for mcrl2::pbes_system::pbesinst_structure_graph_algorithm:
mcrl2::pbes_system::pbesinst_lazy_algorithm mcrl2::pbes_system::pbesinst_structure_graph_algorithm2

Public Member Functions

 pbesinst_structure_graph_algorithm (const pbessolve_options &options, const pbes &p, structure_graph &G)
 
void on_report_equation (const std::size_t, const propositional_variable_instantiation &X, const pbes_expression &psi, std::size_t k) override
 Reports BES equations that are produced by the algorithm. This function is called for every BES equation X = psi with rank k that is produced. By default it does nothing.
 
void run () override
 Runs the algorithm. The result is obtained by calling the function get_result.
 
- Public Member Functions inherited from mcrl2::pbes_system::pbesinst_lazy_algorithm
 pbesinst_lazy_algorithm (const pbessolve_options &options, const pbes &p)
 Constructor.
 
virtual ~pbesinst_lazy_algorithm ()=default
 
virtual void on_report_equation (const std::size_t, const propositional_variable_instantiation &, const pbes_expression &, std::size_t)
 Reports BES equations that are produced by the algorithm. This function is called for every BES equation X = psi with rank k that is produced. By default it does nothing.
 
virtual void on_discovered_elements (const std::set< propositional_variable_instantiation > &)
 This function is called when new elements are added to discovered.
 
virtual void on_end_while_loop ()
 This function is called right after the while loop is finished.
 
void next_todo (propositional_variable_instantiation &result)
 
const fixpoint_symbolsymbol (std::size_t i) const
 
virtual void rewrite_psi (const std::size_t, pbes_expression &result, const fixpoint_symbol &symbol, const propositional_variable_instantiation &X, const pbes_expression &psi)
 
virtual bool solution_found (const propositional_variable_instantiation &) const
 
virtual void run_thread (const std::size_t thread_index, pbesinst_lazy_todo &todo, std::atomic< std::size_t > &number_of_active_processes, data::mutable_indexed_substitution<> sigma, enumerate_quantifiers_rewriter R)
 
virtual void run ()
 Runs the algorithm. The result is obtained by calling the function get_result.
 
const pbes_equation_indexequation_index () const
 
enumerate_quantifiers_rewriterrewriter ()
 

Protected Member Functions

void SG0 (const propositional_variable_instantiation &X, const pbes_expression &psi, std::size_t k)
 
structure_graph::index_type SG1 (const pbes_expression &psi)
 
std::string status_message (std::size_t equation_count) override
 
- Protected Member Functions inherited from mcrl2::pbes_system::pbesinst_lazy_algorithm
virtual std::string status_message (std::size_t equation_count)
 
pbes preprocess (const pbes &x) const
 
data::rewriter construct_rewriter (const pbes &pbesspec)
 

Protected Attributes

detail::structure_graph_builder m_graph_builder
 
- Protected Attributes inherited from mcrl2::pbes_system::pbesinst_lazy_algorithm
const pbessolve_optionsm_options
 Algorithm options.
 
data::rewriter datar
 Data rewriter.
 
pbes m_pbes
 A PBES.
 
pbes_equation_index m_equation_index
 A lookup map for PBES equations.
 
pbesinst_lazy_todo todo
 The propositional variable instantiations that need to be handled.
 
atermpp::indexed_set< propositional_variable_instantiation, true > discovered
 The propositional variable instantiations that have been discovered (not necessarily handled).
 
propositional_variable_instantiation init
 The initial value (after rewriting).
 
std::size_t m_iteration_count = 0
 
enumerate_quantifiers_rewriter m_global_R
 The rewriter.
 
utilities::mutex m_todo_access
 
volatile bool m_must_abort = false
 

Additional Inherited Members

- Static Protected Member Functions inherited from mcrl2::pbes_system::pbesinst_lazy_algorithm
static void rewrite_true_false (pbes_expression &result, const fixpoint_symbol &symbol, const propositional_variable_instantiation &X, const pbes_expression &psi)
 

Detailed Description

Variant of pbesinst that will compute a structure graph for a PBES. The result will be put in the structure graph that is passed in the constructor.

Definition at line 28 of file pbesinst_structure_graph.h.

Constructor & Destructor Documentation

◆ pbesinst_structure_graph_algorithm()

mcrl2::pbes_system::pbesinst_structure_graph_algorithm::pbesinst_structure_graph_algorithm ( const pbessolve_options options,
const pbes p,
structure_graph G 
)
inline

Definition at line 114 of file pbesinst_structure_graph.h.

Member Function Documentation

◆ on_report_equation()

void mcrl2::pbes_system::pbesinst_structure_graph_algorithm::on_report_equation ( const std::size_t  ,
const propositional_variable_instantiation ,
const pbes_expression ,
std::size_t   
)
inlineoverridevirtual

Reports BES equations that are produced by the algorithm. This function is called for every BES equation X = psi with rank k that is produced. By default it does nothing.

Reimplemented from mcrl2::pbes_system::pbesinst_lazy_algorithm.

Reimplemented in mcrl2::pbes_system::pbesinst_structure_graph_algorithm2.

Definition at line 123 of file pbesinst_structure_graph.h.

◆ run()

void mcrl2::pbes_system::pbesinst_structure_graph_algorithm::run ( )
inlineoverridevirtual

Runs the algorithm. The result is obtained by calling the function get_result.

Reimplemented from mcrl2::pbes_system::pbesinst_lazy_algorithm.

Definition at line 137 of file pbesinst_structure_graph.h.

◆ SG0()

void mcrl2::pbes_system::pbesinst_structure_graph_algorithm::SG0 ( const propositional_variable_instantiation X,
const pbes_expression psi,
std::size_t  k 
)
inlineprotected

Definition at line 33 of file pbesinst_structure_graph.h.

◆ SG1()

structure_graph::index_type mcrl2::pbes_system::pbesinst_structure_graph_algorithm::SG1 ( const pbes_expression psi)
inlineprotected

Definition at line 67 of file pbesinst_structure_graph.h.

◆ status_message()

std::string mcrl2::pbes_system::pbesinst_structure_graph_algorithm::status_message ( std::size_t  equation_count)
inlineoverrideprotectedvirtual

Reimplemented from mcrl2::pbes_system::pbesinst_lazy_algorithm.

Definition at line 101 of file pbesinst_structure_graph.h.

Member Data Documentation

◆ m_graph_builder

detail::structure_graph_builder mcrl2::pbes_system::pbesinst_structure_graph_algorithm::m_graph_builder
protected

Definition at line 31 of file pbesinst_structure_graph.h.


The documentation for this class was generated from the following file: