- Generated by
1.15.0
|
ESBMC
Efficient SMT-based Context-Bounded Model Checker
|
Why the schedule space shrank. More...
#include <reachability_tree.h>
Public Member Functions | |
| bool | is_concurrent () const |
Public Attributes | |
| unsigned long | peak_threads = 1 |
| Largest thread count any explored state reached, main included. | |
| unsigned long | schedules_explored = 0 |
| Formulas handed to the caller. | |
| unsigned long | pruned_by_mpor = 0 |
| These three prune counters share a unit: context-switch points at which that reduction stopped the search from branching further. | |
| unsigned long | pruned_by_hash = 0 |
| unsigned long | pruned_by_sleep = 0 |
| Switch targets a sleep set removed. | |
| unsigned long | pruned_by_cs_bound = 0 |
| Only counts points where a switch was still available, i.e. | |
Why the schedule space shrank.
Without these, the contribution of each reduction can only be obtained by toggling its flag and re-running the whole verification, which does not scale to a benchmark set (issue #6831, cause 1).
|
inline |
| unsigned long reachability_treet::reduction_statst::peak_threads = 1 |
Largest thread count any explored state reached, main included.
Also what decides whether the run is worth reporting on at all.
| unsigned long reachability_treet::reduction_statst::pruned_by_cs_bound = 0 |
Only counts points where a switch was still available, i.e.
where the bound truncated rather than the program simply terminating.
| unsigned long reachability_treet::reduction_statst::pruned_by_hash = 0 |
| unsigned long reachability_treet::reduction_statst::pruned_by_mpor = 0 |
These three prune counters share a unit: context-switch points at which that reduction stopped the search from branching further.
| unsigned long reachability_treet::reduction_statst::pruned_by_sleep = 0 |
Switch targets a sleep set removed.
Not the same unit as the others: each node decides its next thread twice (get_next_formula and again via step_next_state on backtracking), so one skip can count twice. Read it as "did sleep sets fire, and roughly how hard", not as a count of nodes.
| unsigned long reachability_treet::reduction_statst::schedules_explored = 0 |
Formulas handed to the caller.
One per schedule under the default DFS; –schedule folds every interleaving into one, so it reports 1.
Not all of them ran to the end of a schedule: an MPOR or hash prune cuts the prefix and get_next_formula still returns a formula for it, so under DFS the complete schedules are schedules_explored - pruned_by_mpor - pruned_by_hash. Comparing this figure across configurations without that subtraction reads a reduction that is working as one that made the search bigger (issue #6831, #6953).
1.15.0