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

Adds an optimization to pbesinst_structure_graph. More...

#include <pbesinst_structure_graph2.h>

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

Classes

struct  Rplus_traverser
 

Public Types

typedef pbesinst_structure_graph_algorithm super
 

Public Member Functions

 pbesinst_structure_graph_algorithm2 (const pbessolve_options &options, const pbes &p, structure_graph &G)
 
void rewrite_psi (const std::size_t thread_index, pbes_expression &result, const fixpoint_symbol &symbol, const propositional_variable_instantiation &X, const pbes_expression &psi) override
 
void on_report_equation (const std::size_t thread_index, 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 on_discovered_elements (const std::set< propositional_variable_instantiation > &elements) override
 This function is called when new elements are added to discovered.
 
void on_end_while_loop () override
 This function is called right after the while loop is finished.
 
- Public Member Functions inherited from mcrl2::pbes_system::pbesinst_structure_graph_algorithm
 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

template<typename T >
pbes_expression expr (const T &x) const
 
Rplus_traverser::stack_element Rplus (const pbes_expression &x)
 
bool solution_found (const propositional_variable_instantiation &init) const override
 
bool todo_has_only_undefined_nodes () const
 
void prune_todo_list (const propositional_variable_instantiation &init, pbesinst_lazy_todo &todo, std::size_t regeneration_period)
 
bool strategies_are_set_in_solved_nodes () const
 
- Protected Member Functions inherited from mcrl2::pbes_system::pbesinst_structure_graph_algorithm
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

std::array< vertex_set, 2 > S
 
std::array< strategy_vector, 2 > tau
 
std::array< detail::computation_guard, 2 > S_guard
 
atermpp::vector< pbes_expressionb
 
detail::computation_guard find_loops_guard
 
detail::computation_guard fatal_attractors_guard
 
detail::periodic_guard reset_guard
 
- Protected Attributes inherited from mcrl2::pbes_system::pbesinst_structure_graph_algorithm
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

Adds an optimization to pbesinst_structure_graph.

Definition at line 73 of file pbesinst_structure_graph2.h.

Member Typedef Documentation

◆ super

Constructor & Destructor Documentation

◆ pbesinst_structure_graph_algorithm2()

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

Definition at line 504 of file pbesinst_structure_graph2.h.

Member Function Documentation

◆ expr()

template<typename T >
pbes_expression mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::expr ( const T &  x) const
inlineprotected

Definition at line 86 of file pbesinst_structure_graph2.h.

◆ on_discovered_elements()

void mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::on_discovered_elements ( const std::set< propositional_variable_instantiation > &  )
inlineoverridevirtual

This function is called when new elements are added to discovered.

Reimplemented from mcrl2::pbes_system::pbesinst_lazy_algorithm.

Definition at line 560 of file pbesinst_structure_graph2.h.

◆ on_end_while_loop()

void mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::on_end_while_loop ( )
inlineoverridevirtual

This function is called right after the while loop is finished.

Reimplemented from mcrl2::pbes_system::pbesinst_lazy_algorithm.

Definition at line 636 of file pbesinst_structure_graph2.h.

◆ on_report_equation()

void mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::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_structure_graph_algorithm.

Definition at line 537 of file pbesinst_structure_graph2.h.

◆ prune_todo_list()

void mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::prune_todo_list ( const propositional_variable_instantiation init,
pbesinst_lazy_todo todo,
std::size_t  regeneration_period 
)
inlineprotected

Definition at line 396 of file pbesinst_structure_graph2.h.

◆ rewrite_psi()

void mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::rewrite_psi ( const std::size_t  thread_index,
pbes_expression result,
const fixpoint_symbol symbol,
const propositional_variable_instantiation X,
const pbes_expression psi 
)
inlineoverridevirtual

Reimplemented from mcrl2::pbes_system::pbesinst_lazy_algorithm.

Definition at line 514 of file pbesinst_structure_graph2.h.

◆ Rplus()

Rplus_traverser::stack_element mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::Rplus ( const pbes_expression x)
inlineprotected

Definition at line 350 of file pbesinst_structure_graph2.h.

◆ solution_found()

bool mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::solution_found ( const propositional_variable_instantiation init) const
inlineoverrideprotectedvirtual

Reimplemented from mcrl2::pbes_system::pbesinst_lazy_algorithm.

Definition at line 357 of file pbesinst_structure_graph2.h.

◆ strategies_are_set_in_solved_nodes()

bool mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::strategies_are_set_in_solved_nodes ( ) const
inlineprotected

Definition at line 471 of file pbesinst_structure_graph2.h.

◆ todo_has_only_undefined_nodes()

bool mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::todo_has_only_undefined_nodes ( ) const
inlineprotected

Definition at line 364 of file pbesinst_structure_graph2.h.

Member Data Documentation

◆ b

atermpp::vector<pbes_expression> mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::b
protected

Definition at line 80 of file pbesinst_structure_graph2.h.

◆ fatal_attractors_guard

detail::computation_guard mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::fatal_attractors_guard
protected

Definition at line 82 of file pbesinst_structure_graph2.h.

◆ find_loops_guard

detail::computation_guard mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::find_loops_guard
protected

Definition at line 81 of file pbesinst_structure_graph2.h.

◆ reset_guard

detail::periodic_guard mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::reset_guard
protected

Definition at line 83 of file pbesinst_structure_graph2.h.

◆ S

std::array<vertex_set, 2> mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::S
protected

Definition at line 76 of file pbesinst_structure_graph2.h.

◆ S_guard

std::array<detail::computation_guard, 2> mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::S_guard
protected

Definition at line 78 of file pbesinst_structure_graph2.h.

◆ tau

std::array<strategy_vector, 2> mcrl2::pbes_system::pbesinst_structure_graph_algorithm2::tau
protected

Definition at line 77 of file pbesinst_structure_graph2.h.


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