The default values of the options that configure counterexample generation. More...

Public Attributes
bool	encodeReachability = false
	Whether reachability of a target state is encoded in the MaxSAT-based generation.
bool	useDynamicConstraints = true
	Whether dynamic constraints are generated in the MaxSAT-based generation.
bool	useSchedulerCuts = false
	Whether the scheduler cuts are added in the MILP-based generation.
uint64_t	shortestPathMaxK = 10
	The maximal number of paths generated by the shortest-path-based generation.

Detailed Description

The default values of the options that configure counterexample generation.

Both the generators and the command-line settings take their defaults from here.

Definition at line 11 of file CounterexampleOptions.h.

Member Data Documentation

bool storm::counterexamples::CounterexampleOptions::encodeReachability = false

Whether reachability of a target state is encoded in the MaxSAT-based generation.

Definition at line 13 of file CounterexampleOptions.h.

uint64_t storm::counterexamples::CounterexampleOptions::shortestPathMaxK = 10

The maximal number of paths generated by the shortest-path-based generation.

Definition at line 22 of file CounterexampleOptions.h.

bool storm::counterexamples::CounterexampleOptions::useDynamicConstraints = true

Whether dynamic constraints are generated in the MaxSAT-based generation.

Definition at line 16 of file CounterexampleOptions.h.

bool storm::counterexamples::CounterexampleOptions::useSchedulerCuts = false

Whether the scheduler cuts are added in the MILP-based generation.

Definition at line 19 of file CounterexampleOptions.h.

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