@ -2,6 +2,7 @@
# define STORM_COUNTEREXAMPLES_MILPMINIMALLABELSETGENERATOR_MDP_H_ # define STORM_COUNTEREXAMPLES_MILPMINIMALLABELSETGENERATOR_MDP_H_
# include <chrono> # include <chrono>
# include <boost/container/flat_set.hpp>
# include "storm/models/sparse/Mdp.h" # include "storm/models/sparse/Mdp.h"
# include "storm/logic/Formulas.h" # include "storm/logic/Formulas.h"
@ -33,10 +34,10 @@ namespace storm {
/*! /*!
* This class provides functionality to generate a minimal counterexample to a probabilistic reachability * This class provides functionality to generate a minimal counterexample to a probabilistic reachability
* property in terms of used command s.
* property in terms of used label s.
*/ */
template < class T > template < class T >
class MILPMinimalCommand SetGenerator {
class MILPMinimalLabel SetGenerator {
private : private :
/*! /*!
* A helper class that provides the functionality to compute a hash value for pairs of state indices . * A helper class that provides the functionality to compute a hash value for pairs of state indices .
@ -60,21 +61,21 @@ namespace storm {
} ; } ;
/*! /*!
* A helper struct capturing information about relevant and problematic choices of states and which command s
* A helper struct capturing information about relevant and problematic choices of states and which label s
* are relevant . * are relevant .
*/ */
struct ChoiceInformation { struct ChoiceInformation {
std : : unordered_map < uint_fast64_t , std : : list < uint_fast64_t > > relevantChoicesForRelevantStates ; std : : unordered_map < uint_fast64_t , std : : list < uint_fast64_t > > relevantChoicesForRelevantStates ;
std : : unordered_map < uint_fast64_t , std : : list < uint_fast64_t > > problematicChoicesForProblematicStates ; std : : unordered_map < uint_fast64_t , std : : list < uint_fast64_t > > problematicChoicesForProblematicStates ;
boost : : container : : flat_set < uint_fast64_t > allRelevantCommand s ;
boost : : container : : flat_set < uint_fast64_t > knownCommand s ;
boost : : container : : flat_set < uint_fast64_t > allRelevantLabel s ;
boost : : container : : flat_set < uint_fast64_t > knownLabel s ;
} ; } ;
/*! /*!
* A helper struct capturing information about the variables of the MILP formulation . * A helper struct capturing information about the variables of the MILP formulation .
*/ */
struct VariableInformation { struct VariableInformation {
std : : unordered_map < uint_fast64_t , storm : : expressions : : Variable > command ToVariableMap;
std : : unordered_map < uint_fast64_t , storm : : expressions : : Variable > label ToVariableMap;
std : : unordered_map < uint_fast64_t , std : : list < storm : : expressions : : Variable > > stateToChoiceVariablesMap ; std : : unordered_map < uint_fast64_t , std : : list < storm : : expressions : : Variable > > stateToChoiceVariablesMap ;
std : : unordered_map < uint_fast64_t , storm : : expressions : : Variable > initialStateToChoiceVariableMap ; std : : unordered_map < uint_fast64_t , storm : : expressions : : Variable > initialStateToChoiceVariableMap ;
std : : unordered_map < uint_fast64_t , storm : : expressions : : Variable > stateToProbabilityVariableMap ; std : : unordered_map < uint_fast64_t , storm : : expressions : : Variable > stateToProbabilityVariableMap ;
@ -117,17 +118,16 @@ namespace storm {
* @ param stateInformation The relevant and problematic states of the model . * @ param stateInformation The relevant and problematic states of the model .
* @ param psiStates A bit vector characterizing the psi states in the model . * @ param psiStates A bit vector characterizing the psi states in the model .
* @ return A structure that stores the relevant and problematic choices in the model as well as the set * @ return A structure that stores the relevant and problematic choices in the model as well as the set
* of relevant command s.
* of relevant label s.
*/ */
static struct ChoiceInformation determineRelevantAndProblematicChoices ( storm : : models : : sparse : : Mdp < T > const & mdp , StateInformation const & stateInformation , storm : : storage : : BitVector const & psiStates ) {
static struct ChoiceInformation determineRelevantAndProblematicChoices ( storm : : models : : sparse : : Mdp < T > const & mdp , std : : vector < boost : : container : : flat_set < uint_fast64_t > > const & labelSets , StateInformation const & stateInformation , storm : : storage : : BitVector const & psiStates ) {
/ / Create result and shortcuts to needed data for convenience . / / Create result and shortcuts to needed data for convenience .
ChoiceInformation result ; ChoiceInformation result ;
storm : : storage : : SparseMatrix < T > const & transitionMatrix = mdp . getTransitionMatrix ( ) ; storm : : storage : : SparseMatrix < T > const & transitionMatrix = mdp . getTransitionMatrix ( ) ;
std : : vector < uint_fast64_t > const & nondeterministicChoiceIndices = mdp . getNondeterministicChoiceIndices ( ) ; std : : vector < uint_fast64_t > const & nondeterministicChoiceIndices = mdp . getNondeterministicChoiceIndices ( ) ;
storm : : storage : : sparse : : PrismChoiceOrigins const & choiceOrigins = mdp . getChoiceOrigins ( ) - > asPrismChoiceOrigins ( ) ;
/ / Now traverse all choices of all relevant states and check whether there is a relevant target state . / / Now traverse all choices of all relevant states and check whether there is a relevant target state .
/ / If so , the associated command sbecome relevant . Also , if a choice of relevant state has at least one
/ / If so , the associated label sbecome relevant . Also , if a choice of relevant state has at least one
/ / relevant successor , the choice is considered to be relevant . / / relevant successor , the choice is considered to be relevant .
for ( auto state : stateInformation . relevantStates ) { for ( auto state : stateInformation . relevantStates ) {
result . relevantChoicesForRelevantStates . emplace ( state , std : : list < uint_fast64_t > ( ) ) ; result . relevantChoicesForRelevantStates . emplace ( state , std : : list < uint_fast64_t > ( ) ) ;
@ -138,10 +138,10 @@ namespace storm {
bool currentChoiceRelevant = false ; bool currentChoiceRelevant = false ;
bool allSuccessorsProblematic = true ; bool allSuccessorsProblematic = true ;
for ( auto const & successorEntry : transitionMatrix . getRow ( row ) ) { for ( auto const & successorEntry : transitionMatrix . getRow ( row ) ) {
/ / If there is a relevant successor , we need to add the command sof the current choice .
/ / If there is a relevant successor , we need to add the label sof the current choice .
if ( stateInformation . relevantStates . get ( successorEntry . getColumn ( ) ) | | psiStates . get ( successorEntry . getColumn ( ) ) ) { if ( stateInformation . relevantStates . get ( successorEntry . getColumn ( ) ) | | psiStates . get ( successorEntry . getColumn ( ) ) ) {
for ( auto const & command : choiceOrigins . getCommandSet ( row ) ) {
result . allRelevantCommand s . insert ( command ) ;
for ( auto const & label : labelSets [ row ] ) {
result . allRelevantLabel s . insert ( label ) ;
} }
if ( ! currentChoiceRelevant ) { if ( ! currentChoiceRelevant ) {
currentChoiceRelevant = true ; currentChoiceRelevant = true ;
@ -161,30 +161,30 @@ namespace storm {
} }
} }
/ / Finally , determine the set of command sthat are known to be taken .
result . knownCommand s = storm : : utility : : counterexamples : : getGuaranteedCommand Set ( mdp , psiStates , result . allRelevantCommand s ) ;
STORM_LOG_DEBUG ( " Found " < < result . allRelevantCommand s . size ( ) < < " relevant command s and " < < result . knownCommand s . size ( ) < < " known command s. " ) ;
/ / Finally , determine the set of label sthat are known to be taken .
result . knownLabel s = storm : : utility : : counterexamples : : getGuaranteedLabel Set ( mdp , labelSets , psiStates , result . allRelevantLabel s ) ;
STORM_LOG_DEBUG ( " Found " < < result . allRelevantLabel s . size ( ) < < " relevant label s and " < < result . knownLabel s . size ( ) < < " known label s. " ) ;
return result ; return result ;
} }
/*! /*!
* Creates the variables for the command sof the model .
* Creates the variables for the label sof the model .
* *
* @ param solver The MILP solver . * @ param solver The MILP solver .
* @ param relevantCommand s The set of relevant command sof the model .
* @ return A mapping from command sto variable indices .
* @ param relevantLabel s The set of relevant label sof the model .
* @ return A mapping from label sto variable indices .
*/ */
static std : : pair < std : : unordered_map < uint_fast64_t , storm : : expressions : : Variable > , uint_fast64_t > createCommand Variables ( storm : : solver : : LpSolver & solver , boost : : container : : flat_set < uint_fast64_t > const & relevantCommand s ) {
static std : : pair < std : : unordered_map < uint_fast64_t , storm : : expressions : : Variable > , uint_fast64_t > createLabel Variables ( storm : : solver : : LpSolver & solver , boost : : container : : flat_set < uint_fast64_t > const & relevantLabel s ) {
std : : stringstream variableNameBuffer ; std : : stringstream variableNameBuffer ;
std : : unordered_map < uint_fast64_t , storm : : expressions : : Variable > resultingMap ; std : : unordered_map < uint_fast64_t , storm : : expressions : : Variable > resultingMap ;
for ( auto const & command : relevantCommand s) {
for ( auto const & label : relevantLabel s) {
variableNameBuffer . str ( " " ) ; variableNameBuffer . str ( " " ) ;
variableNameBuffer . clear ( ) ; variableNameBuffer . clear ( ) ;
variableNameBuffer < < " command " < < command ;
resultingMap [ command ] = solver . addBinaryVariable ( variableNameBuffer . str ( ) , 1 ) ;
variableNameBuffer < < " label " < < label ;
resultingMap [ label ] = solver . addBinaryVariable ( variableNameBuffer . str ( ) , 1 ) ;
} }
return std : : make_pair ( resultingMap , relevantCommand s . size ( ) ) ;
return std : : make_pair ( resultingMap , relevantLabel s . size ( ) ) ;
} }
/*! /*!
@ -363,11 +363,11 @@ namespace storm {
/ / Create a struct that stores all information about variables . / / Create a struct that stores all information about variables .
VariableInformation result ; VariableInformation result ;
/ / Create variables for involved command s.
std : : pair < std : : unordered_map < uint_fast64_t , storm : : expressions : : Variable > , uint_fast64_t > commandVariableResult = createCommand Variables( solver , choiceInformation . allRelevantCommand s ) ;
result . command ToVariableMap= std : : move ( command VariableResult. first ) ;
result . numberOfVariables + = command VariableResult. second ;
STORM_LOG_DEBUG ( " Created variables for command s. " ) ;
/ / Create variables for involved label s.
std : : pair < std : : unordered_map < uint_fast64_t , storm : : expressions : : Variable > , uint_fast64_t > labelVariableResult = createLabel Variables( solver , choiceInformation . allRelevantLabel s ) ;
result . label ToVariableMap= std : : move ( label VariableResult. first ) ;
result . numberOfVariables + = label VariableResult. second ;
STORM_LOG_DEBUG ( " Created variables for label s. " ) ;
/ / Create scheduler variables for relevant states and their actions . / / Create scheduler variables for relevant states and their actions .
std : : pair < std : : unordered_map < uint_fast64_t , std : : list < storm : : expressions : : Variable > > , uint_fast64_t > schedulerVariableResult = createSchedulerVariables ( solver , stateInformation , choiceInformation ) ; std : : pair < std : : unordered_map < uint_fast64_t , std : : list < storm : : expressions : : Variable > > , uint_fast64_t > schedulerVariableResult = createSchedulerVariables ( solver , stateInformation , choiceInformation ) ;
@ -474,8 +474,8 @@ namespace storm {
} }
/*! /*!
* Asserts constraints that make sure the command sare included in the solution set if the policy selects a
* choice that originates from the command in question .
* Asserts constraints that make sure the label sare included in the solution set if the policy selects a
* choice that originates from the label in question .
* *
* @ param solver The MILP solver . * @ param solver The MILP solver .
* @ param mdp The MDP . * @ param mdp The MDP .
@ -484,17 +484,16 @@ namespace storm {
* @ param variableInformation A struct with information about the variables of the model . * @ param variableInformation A struct with information about the variables of the model .
* @ return The total number of constraints that were created . * @ return The total number of constraints that were created .
*/ */
static uint_fast64_t assertChoicesImplyCommands ( storm : : solver : : LpSolver & solver , storm : : models : : sparse : : Mdp < T > const & mdp , StateInformation const & stateInformation , ChoiceInformation const & choiceInformation , VariableInformation const & variableInformation ) {
storm : : storage : : sparse : : PrismChoiceOrigins const & choiceOrigins = mdp . getChoiceOrigins ( ) - > asPrismChoiceOrigins ( ) ;
static uint_fast64_t assertChoicesImplyLabels ( storm : : solver : : LpSolver & solver , storm : : models : : sparse : : Mdp < T > const & mdp , std : : vector < boost : : container : : flat_set < uint_fast64_t > > const & labelSets , StateInformation const & stateInformation , ChoiceInformation const & choiceInformation , VariableInformation const & variableInformation ) {
uint_fast64_t numberOfConstraintsCreated = 0 ; uint_fast64_t numberOfConstraintsCreated = 0 ;
for ( auto state : stateInformation . relevantStates ) { for ( auto state : stateInformation . relevantStates ) {
std : : list < storm : : expressions : : Variable > : : const_iterator choiceVariableIterator = variableInformation . stateToChoiceVariablesMap . at ( state ) . begin ( ) ; std : : list < storm : : expressions : : Variable > : : const_iterator choiceVariableIterator = variableInformation . stateToChoiceVariablesMap . at ( state ) . begin ( ) ;
for ( auto choice : choiceInformation . relevantChoicesForRelevantStates . at ( state ) ) { for ( auto choice : choiceInformation . relevantChoicesForRelevantStates . at ( state ) ) {
for ( auto command : choiceOrigins . getCommandSet ( choice ) ) {
storm : : expressions : : Expression constraint = variableInformation . command ToVariableMap. at ( command ) - * choiceVariableIterator > = solver . getConstant ( 0 ) ;
solver . addConstraint ( " ChoicesImplyCommand s " + std : : to_string ( numberOfConstraintsCreated ) , constraint ) ;
for ( auto label : labelSets [ choice ] ) {
storm : : expressions : : Expression constraint = variableInformation . label ToVariableMap. at ( label ) - * choiceVariableIterator > = solver . getConstant ( 0 ) ;
solver . addConstraint ( " ChoicesImplyLabel s " + std : : to_string ( numberOfConstraintsCreated ) , constraint ) ;
+ + numberOfConstraintsCreated ; + + numberOfConstraintsCreated ;
} }
+ + choiceVariableIterator ; + + choiceVariableIterator ;
@ -623,19 +622,19 @@ namespace storm {
} }
/* /*
* Asserts that command sthat are on all paths from initial to target states are definitely taken .
* Asserts that label sthat are on all paths from initial to target states are definitely taken .
* *
* @ param solver The MILP solver . * @ param solver The MILP solver .
* @ param choiceInformation The information about the choices in the model . * @ param choiceInformation The information about the choices in the model .
* @ param variableInformation A struct with information about the variables of the model . * @ param variableInformation A struct with information about the variables of the model .
* @ return The total number of constraints that were created . * @ return The total number of constraints that were created .
*/ */
static uint_fast64_t assertKnownCommand s ( storm : : solver : : LpSolver & solver , ChoiceInformation const & choiceInformation , VariableInformation const & variableInformation ) {
static uint_fast64_t assertKnownLabel s ( storm : : solver : : LpSolver & solver , ChoiceInformation const & choiceInformation , VariableInformation const & variableInformation ) {
uint_fast64_t numberOfConstraintsCreated = 0 ; uint_fast64_t numberOfConstraintsCreated = 0 ;
for ( auto command : choiceInformation . knownCommand s ) {
storm : : expressions : : Expression constraint = variableInformation . command ToVariableMap. at ( command ) = = solver . getConstant ( 1 ) ;
solver . addConstraint ( " KnownCommand s " + std : : to_string ( numberOfConstraintsCreated ) , constraint ) ;
for ( auto label : choiceInformation . knownLabel s ) {
storm : : expressions : : Expression constraint = variableInformation . label ToVariableMap. at ( label ) = = solver . getConstant ( 1 ) ;
solver . addConstraint ( " KnownLabel s " + std : : to_string ( numberOfConstraintsCreated ) , constraint ) ;
+ + numberOfConstraintsCreated ; + + numberOfConstraintsCreated ;
} }
@ -813,7 +812,7 @@ namespace storm {
* @ param includeSchedulerCuts If set to true , additional constraints are asserted that reduce the set of * @ param includeSchedulerCuts If set to true , additional constraints are asserted that reduce the set of
* possible choices . * possible choices .
*/ */
static void buildConstraintSystem ( storm : : solver : : LpSolver & solver , storm : : models : : sparse : : Mdp < T > const & mdp , storm : : storage : : BitVector const & psiStates , StateInformation const & stateInformation , ChoiceInformation const & choiceInformation , VariableInformation const & variableInformation , double probabilityThreshold , bool strictBound , bool includeSchedulerCuts = false ) {
static void buildConstraintSystem ( storm : : solver : : LpSolver & solver , storm : : models : : sparse : : Mdp < T > const & mdp , std : : vector < boost : : container : : flat_set < uint_fast64_t > > const & labelSets , st orm : : storage : : BitVector const & psiStates , StateInformation const & stateInformation , ChoiceInformation const & choiceInformation , VariableInformation const & variableInformation , double probabilityThreshold , bool strictBound , bool includeSchedulerCuts = false ) {
/ / Assert that the reachability probability in the subsystem exceeds the given threshold . / / Assert that the reachability probability in the subsystem exceeds the given threshold .
uint_fast64_t numberOfConstraints = assertProbabilityGreaterThanThreshold ( solver , variableInformation , probabilityThreshold , strictBound ) ; uint_fast64_t numberOfConstraints = assertProbabilityGreaterThanThreshold ( solver , variableInformation , probabilityThreshold , strictBound ) ;
STORM_LOG_DEBUG ( " Asserted that reachability probability exceeds threshold. " ) ; STORM_LOG_DEBUG ( " Asserted that reachability probability exceeds threshold. " ) ;
@ -822,9 +821,9 @@ namespace storm {
numberOfConstraints + = assertValidPolicy ( solver , stateInformation , variableInformation ) ; numberOfConstraints + = assertValidPolicy ( solver , stateInformation , variableInformation ) ;
STORM_LOG_DEBUG ( " Asserted that policy is valid. " ) ; STORM_LOG_DEBUG ( " Asserted that policy is valid. " ) ;
/ / Add constraints that assert the command sthat belong to some taken choices are taken as well .
numberOfConstraints + = assertChoicesImplyCommand s ( solver , mdp , stateInformation , choiceInformation , variableInformation ) ;
STORM_LOG_DEBUG ( " Asserted that command s implied by choices are taken. " ) ;
/ / Add constraints that assert the label sthat belong to some taken choices are taken as well .
numberOfConstraints + = assertChoicesImplyLabel s ( solver , mdp , labelSets , stateInformation , choiceInformation , variableInformation ) ;
STORM_LOG_DEBUG ( " Asserted that label s implied by choices are taken. " ) ;
/ / Add constraints that encode that the reachability probability from states which do not pick any action / / Add constraints that encode that the reachability probability from states which do not pick any action
/ / is zero . / / is zero .
@ -839,9 +838,9 @@ namespace storm {
numberOfConstraints + = assertUnproblematicStateReachable ( solver , mdp , stateInformation , choiceInformation , variableInformation ) ; numberOfConstraints + = assertUnproblematicStateReachable ( solver , mdp , stateInformation , choiceInformation , variableInformation ) ;
STORM_LOG_DEBUG ( " Asserted that unproblematic state reachable from problematic states. " ) ; STORM_LOG_DEBUG ( " Asserted that unproblematic state reachable from problematic states. " ) ;
/ / Add constraints that express that certain command sare already known to be taken .
numberOfConstraints + = assertKnownCommand s ( solver , choiceInformation , variableInformation ) ;
STORM_LOG_DEBUG ( " Asserted known command s are taken. " ) ;
/ / Add constraints that express that certain label sare already known to be taken .
numberOfConstraints + = assertKnownLabel s ( solver , choiceInformation , variableInformation ) ;
STORM_LOG_DEBUG ( " Asserted known label s are taken. " ) ;
/ / If required , assert additional constraints that reduce the number of possible policies . / / If required , assert additional constraints that reduce the number of possible policies .
if ( includeSchedulerCuts ) { if ( includeSchedulerCuts ) {
@ -861,14 +860,14 @@ namespace storm {
* @ param solver The MILP solver . * @ param solver The MILP solver .
* @ param variableInformation A struct with information about the variables of the model . * @ param variableInformation A struct with information about the variables of the model .
*/ */
static boost : : container : : flat_set < uint_fast64_t > getUsedCommand sInSolution ( storm : : solver : : LpSolver const & solver , VariableInformation const & variableInformation ) {
static boost : : container : : flat_set < uint_fast64_t > getUsedLabel sInSolution ( storm : : solver : : LpSolver const & solver , VariableInformation const & variableInformation ) {
boost : : container : : flat_set < uint_fast64_t > result ; boost : : container : : flat_set < uint_fast64_t > result ;
for ( auto const & command VariablePair: variableInformation . command ToVariableMap) {
bool command Taken= solver . getBinaryValue ( command VariablePair. second ) ;
for ( auto const & label VariablePair: variableInformation . label ToVariableMap) {
bool label Taken= solver . getBinaryValue ( label VariablePair. second ) ;
if ( command Taken) {
result . insert ( command VariablePair. first ) ;
if ( label Taken) {
result . insert ( label VariablePair. first ) ;
} }
} }
return result ; return result ;
@ -923,10 +922,9 @@ namespace storm {
} }
public : public :
static boost : : container : : flat_set < uint_fast64_t > getMinimalCommandSet ( storm : : models : : sparse : : Mdp < T > const & mdp , storm : : storage : : BitVector const & phiStates , storm : : storage : : BitVector const & psiStates , double probabilityThreshold , bool strictBound , bool checkThresholdFeasible = false , bool includeSchedulerCuts = false ) {
/ / ( 0 ) Check whether there are choice origins available
STORM_LOG_THROW ( mdp . hasChoiceOrigins ( ) , storm : : exceptions : : InvalidArgumentException , " Restriction to command set is impossible for model without choice origns. " ) ;
STORM_LOG_THROW ( mdp . getChoiceOrigins ( ) - > isPrismChoiceOrigins ( ) , storm : : exceptions : : InvalidArgumentException , " Restriction to command set is impossible for model without prism choice origins. " ) ;
static boost : : container : : flat_set < uint_fast64_t > getMinimalLabelSet ( storm : : models : : sparse : : Mdp < T > const & mdp , std : : vector < boost : : container : : flat_set < uint_fast64_t > > const & labelSets , storm : : storage : : BitVector const & phiStates , storm : : storage : : BitVector const & psiStates , double probabilityThreshold , bool strictBound , bool checkThresholdFeasible = false , bool includeSchedulerCuts = false ) {
/ / ( 0 ) Check whether the label sets are valid
STORM_LOG_THROW ( mdp . getNumberOfChoices ( ) = = labelSets . size ( ) , storm : : exceptions : : InvalidArgumentException , " The given number of labels does not match the number of choices. " ) ;
/ / ( 1 ) Check whether its possible to exceed the threshold if checkThresholdFeasible is set . / / ( 1 ) Check whether its possible to exceed the threshold if checkThresholdFeasible is set .
double maximalReachabilityProbability = 0 ; double maximalReachabilityProbability = 0 ;
@ -943,27 +941,27 @@ namespace storm {
/ / ( 2 ) Identify relevant and problematic states . / / ( 2 ) Identify relevant and problematic states .
StateInformation stateInformation = determineRelevantAndProblematicStates ( mdp , phiStates , psiStates ) ; StateInformation stateInformation = determineRelevantAndProblematicStates ( mdp , phiStates , psiStates ) ;
/ / ( 3 ) Determine sets of relevant command sand problematic choices .
ChoiceInformation choiceInformation = determineRelevantAndProblematicChoices ( mdp , stateInformation , psiStates ) ;
/ / ( 3 ) Determine sets of relevant label sand problematic choices .
ChoiceInformation choiceInformation = determineRelevantAndProblematicChoices ( mdp , labelSets , stateInformation , psiStates ) ;
/ / ( 4 ) Encode resulting system as MILP problem . / / ( 4 ) Encode resulting system as MILP problem .
std : : shared_ptr < storm : : solver : : LpSolver > solver = storm : : utility : : solver : : getLpSolver ( " MinimalCommand SetCounterexample " ) ;
std : : shared_ptr < storm : : solver : : LpSolver > solver = storm : : utility : : solver : : getLpSolver ( " MinimalLabel SetCounterexample " ) ;
/ / ( 4.1 ) Create variables . / / ( 4.1 ) Create variables .
VariableInformation variableInformation = createVariables ( * solver , mdp , stateInformation , choiceInformation ) ; VariableInformation variableInformation = createVariables ( * solver , mdp , stateInformation , choiceInformation ) ;
/ / ( 4.2 ) Construct constraint system . / / ( 4.2 ) Construct constraint system .
buildConstraintSystem ( * solver , mdp , psiStates , stateInformation , choiceInformation , variableInformation , probabilityThreshold , strictBound , includeSchedulerCuts ) ;
buildConstraintSystem ( * solver , mdp , labelSets , psiStates , stateInformation , choiceInformation , variableInformation , probabilityThreshold , strictBound , includeSchedulerCuts ) ;
/ / ( 4.3 ) Optimize the model . / / ( 4.3 ) Optimize the model .
solver - > optimize ( ) ; solver - > optimize ( ) ;
/ / ( 4.4 ) Read off result from variables . / / ( 4.4 ) Read off result from variables .
boost : : container : : flat_set < uint_fast64_t > usedCommandSet = getUsedCommand sInSolution ( * solver , variableInformation ) ;
usedCommand Set . insert ( choiceInformation . knownCommand s . begin ( ) , choiceInformation . knownCommand s . end ( ) ) ;
boost : : container : : flat_set < uint_fast64_t > usedLabelSet = getUsedLabel sInSolution ( * solver , variableInformation ) ;
usedLabel Set . insert ( choiceInformation . knownLabel s . begin ( ) , choiceInformation . knownLabel s . end ( ) ) ;
/ / ( 5 ) Return result . / / ( 5 ) Return result .
return usedCommand Set ;
return usedLabel Set ;
} }
/*! /*!
@ -976,6 +974,10 @@ namespace storm {
static std : : shared_ptr < PrismHighLevelCounterexample > computeCounterexample ( storm : : prism : : Program const & program , storm : : models : : sparse : : Mdp < T > const & mdp , std : : shared_ptr < storm : : logic : : Formula const > const & formula ) { static std : : shared_ptr < PrismHighLevelCounterexample > computeCounterexample ( storm : : prism : : Program const & program , storm : : models : : sparse : : Mdp < T > const & mdp , std : : shared_ptr < storm : : logic : : Formula const > const & formula ) {
std : : cout < < std : : endl < < " Generating minimal label counterexample for formula " < < * formula < < std : : endl ; std : : cout < < std : : endl < < " Generating minimal label counterexample for formula " < < * formula < < std : : endl ;
/ / Check whether there are choice origins available
STORM_LOG_THROW ( mdp . hasChoiceOrigins ( ) , storm : : exceptions : : InvalidArgumentException , " Restriction to minimal command set is impossible for model without choice origns. " ) ;
STORM_LOG_THROW ( mdp . getChoiceOrigins ( ) - > isPrismChoiceOrigins ( ) , storm : : exceptions : : InvalidArgumentException , " Restriction to command set is impossible for model without prism choice origins. " ) ;
STORM_LOG_THROW ( formula - > isProbabilityOperatorFormula ( ) , storm : : exceptions : : InvalidPropertyException , " Counterexample generation does not support this kind of formula. Expecting a probability operator as the outermost formula element. " ) ; STORM_LOG_THROW ( formula - > isProbabilityOperatorFormula ( ) , storm : : exceptions : : InvalidPropertyException , " Counterexample generation does not support this kind of formula. Expecting a probability operator as the outermost formula element. " ) ;
storm : : logic : : ProbabilityOperatorFormula const & probabilityOperator = formula - > asProbabilityOperatorFormula ( ) ; storm : : logic : : ProbabilityOperatorFormula const & probabilityOperator = formula - > asProbabilityOperatorFormula ( ) ;
STORM_LOG_THROW ( probabilityOperator . hasBound ( ) , storm : : exceptions : : InvalidPropertyException , " Counterexample generation only supports bounded formulas. " ) ; STORM_LOG_THROW ( probabilityOperator . hasBound ( ) , storm : : exceptions : : InvalidPropertyException , " Counterexample generation only supports bounded formulas. " ) ;
@ -1012,9 +1014,18 @@ namespace storm {
psiStates = subQualitativeResult . getTruthValuesVector ( ) ; psiStates = subQualitativeResult . getTruthValuesVector ( ) ;
} }
/ / Obtain the label sets for each choice .
/ / The label set of a choice corresponds to the set of prism commands that induce the choice .
storm : : storage : : sparse : : PrismChoiceOrigins const & choiceOrigins = mdp . getChoiceOrigins ( ) - > asPrismChoiceOrigins ( ) ;
std : : vector < boost : : container : : flat_set < uint_fast64_t > > labelSets ;
labelSets . reserve ( mdp . getNumberOfChoices ( ) ) ;
for ( uint_fast64_t choice = 0 ; choice < mdp . getNumberOfChoices ( ) ; + + choice ) {
labelSets . push_back ( choiceOrigins . getCommandSet ( choice ) ) ;
}
/ / Delegate the actual computation work to the function of equal name . / / Delegate the actual computation work to the function of equal name .
auto startTime = std : : chrono : : high_resolution_clock : : now ( ) ; auto startTime = std : : chrono : : high_resolution_clock : : now ( ) ;
boost : : container : : flat_set < uint_fast64_t > usedCommandSet = getMinimalCommandSet ( mdp , phiStates , psiStates , threshold , strictBound , true , storm : : settings : : getModule < storm : : settings : : modules : : CounterexampleGeneratorSettings > ( ) . isUseSchedulerCutsSet ( ) ) ;
boost : : container : : flat_set < uint_fast64_t > usedCommandSet = getMinimalLabel Set ( mdp , labelSets , phiStates , psiStates , threshold , strictBound , true , storm : : settings : : getModule < storm : : settings : : modules : : CounterexampleGeneratorSettings > ( ) . isUseSchedulerCutsSet ( ) ) ;
auto endTime = std : : chrono : : high_resolution_clock : : now ( ) ; auto endTime = std : : chrono : : high_resolution_clock : : now ( ) ;
std : : cout < < std : : endl < < " Computed minimal command set of size " < < usedCommandSet . size ( ) < < " in " < < std : : chrono : : duration_cast < std : : chrono : : milliseconds > ( endTime - startTime ) . count ( ) < < " ms. " < < std : : endl ; std : : cout < < std : : endl < < " Computed minimal command set of size " < < usedCommandSet . size ( ) < < " in " < < std : : chrono : : duration_cast < std : : chrono : : milliseconds > ( endTime - startTime ) . count ( ) < < " ms. " < < std : : endl ;
TimQu
9 years ago