reachability_treet::scheduler_framet Struct Reference

#include <reachability_tree.h>

Public Member Functions
void	ensure_thread_count (unsigned int count)
void	reset (unsigned int count)
void	mark_all_explored (unsigned int count)
bool	is_explored (unsigned int tid) const
void	mark_explored (unsigned int tid)
bool	is_sleeping (unsigned int tid) const

Public Attributes
std::vector< bool >	explored_threads
std::map< unsigned int, execution_statet::transition_footprintt >	sleeping
	Sleep set (–sleep-sets): threads whose exploration from this node would revisit an equivalent interleaving, each mapped to the footprint of the transition it took when it was put to sleep – which is the transition it would take from here, for as long as it stays asleep.

Member Function Documentation

ensure_thread_count()

void reachability_treet::scheduler_framet::ensure_thread_count

(

unsigned int

count

)

is_explored()

bool reachability_treet::scheduler_framet::is_explored

(

unsigned int

tid

)

const

is_sleeping()

bool reachability_treet::scheduler_framet::is_sleeping

(

unsigned int

tid

)

const

mark_all_explored()

void reachability_treet::scheduler_framet::mark_all_explored

(

unsigned int

count

)

mark_explored()

void reachability_treet::scheduler_framet::mark_explored

(

unsigned int

tid

)

reset()

void reachability_treet::scheduler_framet::reset

(

unsigned int

count

)

Member Data Documentation

explored_threads

std::vector<bool> reachability_treet::scheduler_framet::explored_threads

sleeping

std::map<unsigned int, execution_statet::transition_footprintt> reachability_treet::scheduler_framet::sleeping

Sleep set (–sleep-sets): threads whose exploration from this node would revisit an equivalent interleaving, each mapped to the footprint of the transition it took when it was put to sleep – which is the transition it would take from here, for as long as it stays asleep.

Empty unless the flag is on.

---

The documentation for this struct was generated from the following files:

• src/goto-symex/scheduler/reachability_tree.h
• src/goto-symex/scheduler/reachability_tree.cpp