d2/d40/_counterexample_options_8h_source.html

#pragma once


#include <cstdint>


namespace storm::counterexamples {


struct CounterexampleOptions {

    bool encodeReachability = false;


    bool useDynamicConstraints = true;


    bool useSchedulerCuts = false;


    uint64_t shortestPathMaxK = 10;

};


}  // namespace storm::counterexamples

storm::counterexamples
Definition Counterexample.cpp:4

storm::counterexamples::CounterexampleOptions
The default values of the options that configure counterexample generation.
Definition CounterexampleOptions.h:11

storm::counterexamples::CounterexampleOptions::useDynamicConstraints
bool useDynamicConstraints
Whether dynamic constraints are generated in the MaxSAT-based generation.
Definition CounterexampleOptions.h:16

storm::counterexamples::CounterexampleOptions::shortestPathMaxK
uint64_t shortestPathMaxK
The maximal number of paths generated by the shortest-path-based generation.
Definition CounterexampleOptions.h:22

storm::counterexamples::CounterexampleOptions::useSchedulerCuts
bool useSchedulerCuts
Whether the scheduler cuts are added in the MILP-based generation.
Definition CounterexampleOptions.h:19

storm::counterexamples::CounterexampleOptions::encodeReachability
bool encodeReachability
Whether reachability of a target state is encoded in the MaxSAT-based generation.
Definition CounterexampleOptions.h:13