@ -19,6 +19,8 @@
# include "storm/utility/solver.h"
# include "storm/solver/LpSolver.h"
# include "storm/storage/sparse/PrismChoiceOrigins.h"
# include "storm/settings/SettingsManager.h"
# include "storm/settings/modules/GeneralSettings.h"
# include "storm/settings/modules/CounterexampleGeneratorSettings.h"
@ -28,10 +30,10 @@ namespace storm {
/*!
* This class provides functionality to generate a minimal counterexample to a probabilistic reachability
* property in terms of used label s.
* property in terms of used command s.
*/
template < class T >
class MILPMinimalLabel SetGenerator {
class MILPMinimalCommand SetGenerator {
private :
/*!
* A helper class that provides the functionality to compute a hash value for pairs of state indices .
@ -55,21 +57,21 @@ namespace storm {
} ;
/*!
* A helper struct capturing information about relevant and problematic choices of states and which label s
* A helper struct capturing information about relevant and problematic choices of states and which command s
* are relevant .
*/
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 > > problematicChoicesForProblematicStates ;
boost : : container : : flat_set < uint_fast64_t > allRelevantLabel s ;
boost : : container : : flat_set < uint_fast64_t > knownLabel s ;
boost : : container : : flat_set < uint_fast64_t > allRelevantCommand s ;
boost : : container : : flat_set < uint_fast64_t > knownCommand s ;
} ;
/*!
* A helper struct capturing information about the variables of the MILP formulation .
*/
struct VariableInformation {
std : : unordered_map < uint_fast64_t , storm : : expressions : : Variable > label ToVariableMap;
std : : unordered_map < uint_fast64_t , storm : : expressions : : Variable > command ToVariableMap;
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 > stateToProbabilityVariableMap ;
@ -87,16 +89,16 @@ namespace storm {
* non - zero probability of satisfying phi until psi . Problematic states are relevant states that have at
* least one scheduler such that the probability of satisfying phi until psi is zero .
*
* @ param labeledM dpThe MDP whose states to search .
* @ param m dpThe MDP whose states to search .
* @ param phiStates A bit vector characterizing all states satisfying phi .
* @ param psiStates A bit vector characterizing all states satisfying psi .
* @ return A structure that stores the relevant and problematic states .
*/
static struct StateInformation determineRelevantAndProblematicStates ( storm : : models : : sparse : : Mdp < T > const & labeledM dp, storm : : storage : : BitVector const & phiStates , storm : : storage : : BitVector const & psiStates ) {
static struct StateInformation determineRelevantAndProblematicStates ( storm : : models : : sparse : : Mdp < T > const & m dp, storm : : storage : : BitVector const & phiStates , storm : : storage : : BitVector const & psiStates ) {
StateInformation result ;
result . relevantStates = storm : : utility : : graph : : performProbGreater0E ( labeledM dp. getBackwardTransitions ( ) , phiStates , psiStates ) ;
result . relevantStates = storm : : utility : : graph : : performProbGreater0E ( m dp. getBackwardTransitions ( ) , phiStates , psiStates ) ;
result . relevantStates & = ~ psiStates ;
result . problematicStates = storm : : utility : : graph : : performProb0E ( labeledM dp. getTransitionMatrix ( ) , labeledM dp. getNondeterministicChoiceIndices ( ) , labeledM dp. getBackwardTransitions ( ) , phiStates , psiStates ) ;
result . problematicStates = storm : : utility : : graph : : performProb0E ( m dp. getTransitionMatrix ( ) , m dp. getNondeterministicChoiceIndices ( ) , m dp. getBackwardTransitions ( ) , phiStates , psiStates ) ;
result . problematicStates & = result . relevantStates ;
STORM_LOG_DEBUG ( " Found " < < phiStates . getNumberOfSetBits ( ) < < " filter states. " ) ;
STORM_LOG_DEBUG ( " Found " < < psiStates . getNumberOfSetBits ( ) < < " target states. " ) ;
@ -108,21 +110,20 @@ namespace storm {
/*!
* Determines the relevant and problematic choices of the given MDP with respect to the given parameters .
*
* @ param labeledM dpThe MDP whose choices to search .
* @ param m dpThe MDP whose choices to search .
* @ param stateInformation The relevant and problematic states of 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
* of relevant label s.
* of relevant command s.
*/
static struct ChoiceInformation determineRelevantAndProblematicChoices ( storm : : models : : sparse : : Mdp < T > const & labeledMdp , StateInformation const & stateInformation , storm : : storage : : BitVector const & psiStates ) {
static struct ChoiceInformation determineRelevantAndProblematicChoices ( storm : : models : : sparse : : Mdp < T > const & mdp , storm : : storage : : sparse : : PrismChoiceOrigins const & choiceOrigins , StateInformation const & stateInformation , storm : : storage : : BitVector const & psiStates ) {
/ / Create result and shortcuts to needed data for convenience .
ChoiceInformation result ;
storm : : storage : : SparseMatrix < T > const & transitionMatrix = labeledMdp . getTransitionMatrix ( ) ;
std : : vector < uint_fast64_t > const & nondeterministicChoiceIndices = labeledMdp . getNondeterministicChoiceIndices ( ) ;
std : : vector < boost : : container : : flat_set < uint_fast64_t > > const & choiceLabeling = labeledMdp . getChoiceLabeling ( ) ;
storm : : storage : : SparseMatrix < T > const & transitionMatrix = mdp . getTransitionMatrix ( ) ;
std : : vector < uint_fast64_t > const & nondeterministicChoiceIndices = mdp . getNondeterministicChoiceIndices ( ) ;
/ / Now traverse all choices of all relevant states and check whether there is a relevant target state .
/ / If so , the associated label sbecome relevant . Also , if a choice of relevant state has at least one
/ / If so , the associated command sbecome relevant . Also , if a choice of relevant state has at least one
/ / relevant successor , the choice is considered to be relevant .
for ( auto state : stateInformation . relevantStates ) {
result . relevantChoicesForRelevantStates . emplace ( state , std : : list < uint_fast64_t > ( ) ) ;
@ -133,10 +134,10 @@ namespace storm {
bool currentChoiceRelevant = false ;
bool allSuccessorsProblematic = true ;
for ( auto const & successorEntry : transitionMatrix . getRow ( row ) ) {
/ / If there is a relevant successor , we need to add the label sof the current choice .
/ / If there is a relevant successor , we need to add the command sof the current choice .
if ( stateInformation . relevantStates . get ( successorEntry . getColumn ( ) ) | | psiStates . get ( successorEntry . getColumn ( ) ) ) {
for ( auto const & label : choiceLabeling [ row ] ) {
result . allRelevantLabel s . insert ( label ) ;
for ( auto const & command : choiceOrigins . getCommandSet ( row ) ) {
result . allRelevantCommand s . insert ( command ) ;
}
if ( ! currentChoiceRelevant ) {
currentChoiceRelevant = true ;
@ -156,30 +157,30 @@ namespace storm {
}
}
/ / Finally , determine the set of label sthat are known to be taken .
result . knownLabel s = storm : : utility : : counterexamples : : getGuaranteedLabelSet ( labeledMdp , psiStates , result . allRelevantLabel s ) ;
STORM_LOG_DEBUG ( " Found " < < result . allRelevantLabel s . size ( ) < < " relevant label s and " < < result . knownLabel s . size ( ) < < " known label s. " ) ;
/ / Finally , determine the set of command sthat are known to be taken .
result . knownCommand s = storm : : utility : : counterexamples : : getGuaranteedCommandSet ( mdp , choiceOrigins , psiStates , result . allRelevantCommand s ) ;
STORM_LOG_DEBUG ( " Found " < < result . allRelevantCommand s . size ( ) < < " relevant command s and " < < result . knownCommand s . size ( ) < < " known command s. " ) ;
return result ;
}
/*!
* Creates the variables for the label sof the model .
* Creates the variables for the command sof the model .
*
* @ param solver The MILP solver .
* @ param relevantLabel s The set of relevant label sof the model .
* @ return A mapping from label sto variable indices .
* @ param relevantCommand s The set of relevant command sof the model .
* @ return A mapping from command sto variable indices .
*/
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 ) {
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 ) {
std : : stringstream variableNameBuffer ;
std : : unordered_map < uint_fast64_t , storm : : expressions : : Variable > resultingMap ;
for ( auto const & label : relevantLabel s) {
for ( auto const & command : relevantCommand s) {
variableNameBuffer . str ( " " ) ;
variableNameBuffer . clear ( ) ;
variableNameBuffer < < " label " < < label ;
resultingMap [ label ] = solver . addBinaryVariable ( variableNameBuffer . str ( ) , 1 ) ;
variableNameBuffer < < " command " < < command ;
resultingMap [ command ] = solver . addBinaryVariable ( variableNameBuffer . str ( ) , 1 ) ;
}
return std : : make_pair ( resultingMap , relevantLabel s . size ( ) ) ;
return std : : make_pair ( resultingMap , relevantCommand s . size ( ) ) ;
}
/*!
@ -214,16 +215,16 @@ namespace storm {
* in the model .
*
* @ param solver The MILP solver .
* @ param labeledMdp The labeled MDP .
* @ param mdp The MDP .
* @ param stateInformation The information about the states of the model .
* @ return A mapping from initial states to choice variable indices .
*/
static std : : pair < std : : unordered_map < uint_fast64_t , storm : : expressions : : Variable > , uint_fast64_t > createInitialChoiceVariables ( storm : : solver : : LpSolver & solver , storm : : models : : sparse : : Mdp < T > const & labeledM dp, StateInformation const & stateInformation ) {
static std : : pair < std : : unordered_map < uint_fast64_t , storm : : expressions : : Variable > , uint_fast64_t > createInitialChoiceVariables ( storm : : solver : : LpSolver & solver , storm : : models : : sparse : : Mdp < T > const & m dp, StateInformation const & stateInformation ) {
std : : stringstream variableNameBuffer ;
uint_fast64_t numberOfVariablesCreated = 0 ;
std : : unordered_map < uint_fast64_t , storm : : expressions : : Variable > resultingMap ;
for ( auto initialState : labeledM dp. getStates ( " init " ) ) {
for ( auto initialState : m dp. getStates ( " init " ) ) {
/ / Only consider this initial state if it is relevant .
if ( stateInformation . relevantStates . get ( initialState ) ) {
variableNameBuffer . str ( " " ) ;
@ -275,11 +276,11 @@ namespace storm {
* Creates the variables for the problematic states in the model .
*
* @ param solver The MILP solver .
* @ param labeledMdp The labeled MDP .
* @ param mdp The MDP .
* @ param stateInformation The information about the states in the model .
* @ return A mapping from problematic states to the index of the corresponding variables .
*/
static std : : pair < std : : unordered_map < uint_fast64_t , storm : : expressions : : Variable > , uint_fast64_t > createProblematicStateVariables ( storm : : solver : : LpSolver & solver , storm : : models : : sparse : : Mdp < T > const & labeledM dp, StateInformation const & stateInformation , ChoiceInformation const & choiceInformation ) {
static std : : pair < std : : unordered_map < uint_fast64_t , storm : : expressions : : Variable > , uint_fast64_t > createProblematicStateVariables ( storm : : solver : : LpSolver & solver , storm : : models : : sparse : : Mdp < T > const & m dp, StateInformation const & stateInformation , ChoiceInformation const & choiceInformation ) {
std : : stringstream variableNameBuffer ;
uint_fast64_t numberOfVariablesCreated = 0 ;
std : : unordered_map < uint_fast64_t , storm : : expressions : : Variable > resultingMap ;
@ -297,7 +298,7 @@ namespace storm {
std : : list < uint_fast64_t > const & relevantChoicesForState = choiceInformation . relevantChoicesForRelevantStates . at ( state ) ;
for ( uint_fast64_t row : relevantChoicesForState ) {
for ( auto const & successorEntry : labeledM dp. getTransitionMatrix ( ) . getRow ( row ) ) {
for ( auto const & successorEntry : m dp. getTransitionMatrix ( ) . getRow ( row ) ) {
if ( stateInformation . relevantStates . get ( successorEntry . getColumn ( ) ) ) {
if ( resultingMap . find ( successorEntry . getColumn ( ) ) = = resultingMap . end ( ) ) {
variableNameBuffer . str ( " " ) ;
@ -317,12 +318,12 @@ namespace storm {
* Creates the variables for the problematic choices in the model .
*
* @ param solver The MILP solver .
* @ param labeledMdp The labeled MDP .
* @ param mdp The MDP .
* @ param stateInformation The information about the states in the model .
* @ param choiceInformation The information about the choices in the model .
* @ return A mapping from problematic choices to the index of the corresponding variables .
*/
static std : : pair < std : : unordered_map < std : : pair < uint_fast64_t , uint_fast64_t > , storm : : expressions : : Variable , PairHash > , uint_fast64_t > createProblematicChoiceVariables ( storm : : solver : : LpSolver & solver , storm : : models : : sparse : : Mdp < T > const & labeledM dp, StateInformation const & stateInformation , ChoiceInformation const & choiceInformation ) {
static std : : pair < std : : unordered_map < std : : pair < uint_fast64_t , uint_fast64_t > , storm : : expressions : : Variable , PairHash > , uint_fast64_t > createProblematicChoiceVariables ( storm : : solver : : LpSolver & solver , storm : : models : : sparse : : Mdp < T > const & m dp, StateInformation const & stateInformation , ChoiceInformation const & choiceInformation ) {
std : : stringstream variableNameBuffer ;
uint_fast64_t numberOfVariablesCreated = 0 ;
std : : unordered_map < std : : pair < uint_fast64_t , uint_fast64_t > , storm : : expressions : : Variable , PairHash > resultingMap ;
@ -330,7 +331,7 @@ namespace storm {
for ( auto state : stateInformation . problematicStates ) {
std : : list < uint_fast64_t > const & relevantChoicesForState = choiceInformation . relevantChoicesForRelevantStates . at ( state ) ;
for ( uint_fast64_t row : relevantChoicesForState ) {
for ( auto const & successorEntry : labeledM dp. getTransitionMatrix ( ) . getRow ( row ) ) {
for ( auto const & successorEntry : m dp. getTransitionMatrix ( ) . getRow ( row ) ) {
if ( stateInformation . relevantStates . get ( successorEntry . getColumn ( ) ) ) {
variableNameBuffer . str ( " " ) ;
variableNameBuffer . clear ( ) ;
@ -350,19 +351,19 @@ namespace storm {
* passed to the solver .
*
* @ param solver The MILP solver .
* @ param labeledMdp The labeled MDP .
* @ param mdp The MDP .
* @ param stateInformation The information about the states in the model .
* @ param choiceInformation The information about the choices in the model .
*/
static VariableInformation createVariables ( storm : : solver : : LpSolver & solver , storm : : models : : sparse : : Mdp < T > const & labeledM dp, StateInformation const & stateInformation , ChoiceInformation const & choiceInformation ) {
static VariableInformation createVariables ( storm : : solver : : LpSolver & solver , storm : : models : : sparse : : Mdp < T > const & m dp, StateInformation const & stateInformation , ChoiceInformation const & choiceInformation ) {
/ / Create a struct that stores all information about variables .
VariableInformation result ;
/ / 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 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 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 ) ;
@ -371,7 +372,7 @@ namespace storm {
STORM_LOG_DEBUG ( " Created variables for nondeterministic choices. " ) ;
/ / Create scheduler variables for nondeterministically choosing an initial state .
std : : pair < std : : unordered_map < uint_fast64_t , storm : : expressions : : Variable > , uint_fast64_t > initialChoiceVariableResult = createInitialChoiceVariables ( solver , labeledM dp, stateInformation ) ;
std : : pair < std : : unordered_map < uint_fast64_t , storm : : expressions : : Variable > , uint_fast64_t > initialChoiceVariableResult = createInitialChoiceVariables ( solver , m dp, stateInformation ) ;
result . initialStateToChoiceVariableMap = std : : move ( initialChoiceVariableResult . first ) ;
result . numberOfVariables + = initialChoiceVariableResult . second ;
STORM_LOG_DEBUG ( " Created variables for the nondeterministic choice of the initial state. " ) ;
@ -389,13 +390,13 @@ namespace storm {
STORM_LOG_DEBUG ( " Created variables for the virtual initial state. " ) ;
/ / Create variables for problematic states .
std : : pair < std : : unordered_map < uint_fast64_t , storm : : expressions : : Variable > , uint_fast64_t > problematicStateVariableResult = createProblematicStateVariables ( solver , labeledM dp, stateInformation , choiceInformation ) ;
std : : pair < std : : unordered_map < uint_fast64_t , storm : : expressions : : Variable > , uint_fast64_t > problematicStateVariableResult = createProblematicStateVariables ( solver , m dp, stateInformation , choiceInformation ) ;
result . problematicStateToVariableMap = std : : move ( problematicStateVariableResult . first ) ;
result . numberOfVariables + = problematicStateVariableResult . second ;
STORM_LOG_DEBUG ( " Created variables for the problematic states. " ) ;
/ / Create variables for problematic choices .
std : : pair < std : : unordered_map < std : : pair < uint_fast64_t , uint_fast64_t > , storm : : expressions : : Variable , PairHash > , uint_fast64_t > problematicTransitionVariableResult = createProblematicChoiceVariables ( solver , labeledM dp, stateInformation , choiceInformation ) ;
std : : pair < std : : unordered_map < std : : pair < uint_fast64_t , uint_fast64_t > , storm : : expressions : : Variable , PairHash > , uint_fast64_t > problematicTransitionVariableResult = createProblematicChoiceVariables ( solver , m dp, stateInformation , choiceInformation ) ;
result . problematicTransitionToVariableMap = problematicTransitionVariableResult . first ;
result . numberOfVariables + = problematicTransitionVariableResult . second ;
STORM_LOG_DEBUG ( " Created variables for the problematic choices. " ) ;
@ -469,26 +470,25 @@ namespace storm {
}
/*!
* Asserts constraints that make sure the label sare included in the solution set if the policy selects a
* choice that is labeled with the label in question .
* 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 .
*
* @ param solver The MILP solver .
* @ param labeledMdp The labeled MDP .
* @ param mdp The MDP .
* @ param stateInformation The information about the states 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 .
* @ return The total number of constraints that were created .
*/
static uint_fast64_t assertChoicesImplyLabel s ( storm : : solver : : LpSolver & solver , storm : : models : : sparse : : Mdp < T > const & labeledMdp , StateInformation const & stateInformation , ChoiceInformation const & choiceInformation , VariableInformation const & variableInformation ) {
static uint_fast64_t assertChoicesImplyCommand s ( storm : : solver : : LpSolver & solver , storm : : models : : sparse : : Mdp < T > const & mdp , storm : : storage : : sparse : : PrismChoiceOrigins const & choiceOrigins , StateInformation const & stateInformation , ChoiceInformation const & choiceInformation , VariableInformation const & variableInformation ) {
uint_fast64_t numberOfConstraintsCreated = 0 ;
std : : vector < boost : : container : : flat_set < uint_fast64_t > > const & choiceLabeling = labeledMdp . getChoiceLabeling ( ) ;
for ( auto state : stateInformation . relevantStates ) {
std : : list < storm : : expressions : : Variable > : : const_iterator choiceVariableIterator = variableInformation . stateToChoiceVariablesMap . at ( state ) . begin ( ) ;
for ( auto choice : choiceInformation . relevantChoicesForRelevantStates . at ( state ) ) {
for ( auto label : choiceLabeling [ choice ] ) {
storm : : expressions : : Expression constraint = variableInformation . label ToVariableMap. at ( label ) - * choiceVariableIterator > = solver . getConstant ( 0 ) ;
solver . addConstraint ( " ChoicesImplyLabel s " + std : : to_string ( numberOfConstraintsCreated ) , constraint ) ;
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 ) ;
+ + numberOfConstraintsCreated ;
}
+ + choiceVariableIterator ;
@ -524,14 +524,14 @@ namespace storm {
* Asserts constraints that encode the correct reachability probabilities for all states .
*
* @ param solver The MILP solver .
* @ param labeledMdp The labeled MDP .
* @ param mdp The MDP .
* @ param psiStates A bit vector characterizing the psi states in the model .
* @ param stateInformation The information about the states 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 .
* @ return The total number of constraints that were created .
*/
static uint_fast64_t assertReachabilityProbabilities ( storm : : solver : : LpSolver & solver , storm : : models : : sparse : : Mdp < T > const & labeledM dp, storm : : storage : : BitVector const & psiStates , StateInformation const & stateInformation , ChoiceInformation const & choiceInformation , VariableInformation const & variableInformation ) {
static uint_fast64_t assertReachabilityProbabilities ( storm : : solver : : LpSolver & solver , storm : : models : : sparse : : Mdp < T > const & m dp, storm : : storage : : BitVector const & psiStates , StateInformation const & stateInformation , ChoiceInformation const & choiceInformation , VariableInformation const & variableInformation ) {
uint_fast64_t numberOfConstraintsCreated = 0 ;
for ( auto state : stateInformation . relevantStates ) {
std : : list < storm : : expressions : : Variable > : : const_iterator choiceVariableIterator = variableInformation . stateToChoiceVariablesMap . at ( state ) . begin ( ) ;
@ -539,7 +539,7 @@ namespace storm {
storm : : expressions : : Expression constraint = variableInformation . stateToProbabilityVariableMap . at ( state ) ;
double rightHandSide = 1 ;
for ( auto const & successorEntry : labeledM dp. getTransitionMatrix ( ) . getRow ( choice ) ) {
for ( auto const & successorEntry : m dp. getTransitionMatrix ( ) . getRow ( choice ) ) {
if ( stateInformation . relevantStates . get ( successorEntry . getColumn ( ) ) ) {
constraint = constraint - solver . getConstant ( successorEntry . getValue ( ) ) * variableInformation . stateToProbabilityVariableMap . at ( successorEntry . getColumn ( ) ) ;
} else if ( psiStates . get ( successorEntry . getColumn ( ) ) ) {
@ -570,13 +570,13 @@ namespace storm {
* Asserts constraints that make sure an unproblematic state is reachable from each problematic state .
*
* @ param solver The MILP solver .
* @ param labeledMdp The labeled MDP .
* @ param mdp The MDP .
* @ param stateInformation The information about the states 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 .
* @ return The total number of constraints that were created .
*/
static uint_fast64_t assertUnproblematicStateReachable ( storm : : solver : : LpSolver & solver , storm : : models : : sparse : : Mdp < T > const & labeledM dp, StateInformation const & stateInformation , ChoiceInformation const & choiceInformation , VariableInformation const & variableInformation ) {
static uint_fast64_t assertUnproblematicStateReachable ( storm : : solver : : LpSolver & solver , storm : : models : : sparse : : Mdp < T > const & m dp, StateInformation const & stateInformation , ChoiceInformation const & choiceInformation , VariableInformation const & variableInformation ) {
uint_fast64_t numberOfConstraintsCreated = 0 ;
for ( auto stateListPair : choiceInformation . problematicChoicesForProblematicStates ) {
@ -590,7 +590,7 @@ namespace storm {
}
storm : : expressions : : Expression constraint = * choiceVariableIterator ;
for ( auto const & successorEntry : labeledM dp. getTransitionMatrix ( ) . getRow ( problematicChoice ) ) {
for ( auto const & successorEntry : m dp. getTransitionMatrix ( ) . getRow ( problematicChoice ) ) {
constraint = constraint - variableInformation . problematicTransitionToVariableMap . at ( std : : make_pair ( stateListPair . first , successorEntry . getColumn ( ) ) ) ;
}
constraint = constraint < = solver . getConstant ( 0 ) ;
@ -602,7 +602,7 @@ namespace storm {
for ( auto state : stateInformation . problematicStates ) {
for ( auto problematicChoice : choiceInformation . problematicChoicesForProblematicStates . at ( state ) ) {
for ( auto const & successorEntry : labeledM dp. getTransitionMatrix ( ) . getRow ( problematicChoice ) ) {
for ( auto const & successorEntry : m dp. getTransitionMatrix ( ) . getRow ( problematicChoice ) ) {
storm : : expressions : : Expression constraint = variableInformation . problematicStateToVariableMap . at ( state ) ;
constraint = constraint - variableInformation . problematicStateToVariableMap . at ( successorEntry . getColumn ( ) ) ;
constraint = constraint + variableInformation . problematicTransitionToVariableMap . at ( std : : make_pair ( state , successorEntry . getColumn ( ) ) ) ;
@ -617,19 +617,19 @@ namespace storm {
}
/*
* Asserts that label sthat are on all paths from initial to target states are definitely taken .
* Asserts that command sthat are on all paths from initial to target states are definitely taken .
*
* @ param solver The MILP solver .
* @ param choiceInformation The information about the choices in the model .
* @ param variableInformation A struct with information about the variables of the model .
* @ return The total number of constraints that were created .
*/
static uint_fast64_t assertKnownLabel s ( storm : : solver : : LpSolver & solver , ChoiceInformation const & choiceInformation , VariableInformation const & variableInformation ) {
static uint_fast64_t assertKnownCommand s ( storm : : solver : : LpSolver & solver , ChoiceInformation const & choiceInformation , VariableInformation const & variableInformation ) {
uint_fast64_t numberOfConstraintsCreated = 0 ;
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 ) ;
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 ) ;
+ + numberOfConstraintsCreated ;
}
@ -640,15 +640,15 @@ namespace storm {
* Asserts constraints that rule out many suboptimal policies .
*
* @ param solver The MILP solver .
* @ param labeledMdp The labeled MDP .
* @ param mdp The MDP .
* @ param psiStates A bit vector characterizing the psi states in the model .
* @ param stateInformation The information about the states 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 .
* @ return The total number of constraints that were created .
*/
static uint_fast64_t assertSchedulerCuts ( storm : : solver : : LpSolver & solver , storm : : models : : sparse : : Mdp < T > const & labeledM dp, storm : : storage : : BitVector const & psiStates , StateInformation const & stateInformation , ChoiceInformation const & choiceInformation , VariableInformation const & variableInformation ) {
storm : : storage : : SparseMatrix < T > backwardTransitions = labeledM dp. getBackwardTransitions ( ) ;
static uint_fast64_t assertSchedulerCuts ( storm : : solver : : LpSolver & solver , storm : : models : : sparse : : Mdp < T > const & m dp, storm : : storage : : BitVector const & psiStates , StateInformation const & stateInformation , ChoiceInformation const & choiceInformation , VariableInformation const & variableInformation ) {
storm : : storage : : SparseMatrix < T > backwardTransitions = m dp. getBackwardTransitions ( ) ;
uint_fast64_t numberOfConstraintsCreated = 0 ;
for ( auto state : stateInformation . relevantStates ) {
@ -657,7 +657,7 @@ namespace storm {
std : : list < storm : : expressions : : Variable > : : const_iterator choiceVariableIterator = variableInformation . stateToChoiceVariablesMap . at ( state ) . begin ( ) ;
for ( auto choice : choiceInformation . relevantChoicesForRelevantStates . at ( state ) ) {
bool psiStateReachableInOneStep = false ;
for ( auto const & successorEntry : labeledM dp. getTransitionMatrix ( ) . getRow ( choice ) ) {
for ( auto const & successorEntry : m dp. getTransitionMatrix ( ) . getRow ( choice ) ) {
if ( psiStates . get ( successorEntry . getColumn ( ) ) ) {
psiStateReachableInOneStep = true ;
}
@ -665,7 +665,7 @@ namespace storm {
if ( ! psiStateReachableInOneStep ) {
storm : : expressions : : Expression constraint = * choiceVariableIterator ;
for ( auto const & successorEntry : labeledM dp. getTransitionMatrix ( ) . getRow ( choice ) ) {
for ( auto const & successorEntry : m dp. getTransitionMatrix ( ) . getRow ( choice ) ) {
if ( state ! = successorEntry . getColumn ( ) & & stateInformation . relevantStates . get ( successorEntry . getColumn ( ) ) ) {
std : : list < storm : : expressions : : Variable > const & successorChoiceVariableIndices = variableInformation . stateToChoiceVariablesMap . at ( successorEntry . getColumn ( ) ) ;
@ -710,7 +710,7 @@ namespace storm {
bool choiceTargetsCurrentState = false ;
/ / Check if the current choice targets the current state .
for ( auto const & successorEntry : labeledM dp. getTransitionMatrix ( ) . getRow ( relevantChoice ) ) {
for ( auto const & successorEntry : m dp. getTransitionMatrix ( ) . getRow ( relevantChoice ) ) {
if ( state = = successorEntry . getColumn ( ) ) {
choiceTargetsCurrentState = true ;
break ;
@ -727,7 +727,7 @@ namespace storm {
/ / If the current state is an initial state and is selected as a successor state by the virtual
/ / initial state , then this also justifies making a choice in the current state .
if ( labeledM dp. getStates ( " init " ) . get ( state ) ) {
if ( m dp. getStates ( " init " ) . get ( state ) ) {
constraint = constraint - variableInformation . initialStateToChoiceVariableMap . at ( state ) ;
}
constraint = constraint < = solver . getConstant ( 0 ) ;
@ -738,7 +738,7 @@ namespace storm {
/ / Assert that at least one initial state selects at least one action .
storm : : expressions : : Expression constraint = solver . getConstant ( 0 ) ;
for ( auto initialState : labeledM dp. getStates ( " init " ) ) {
for ( auto initialState : m dp. getStates ( " init " ) ) {
for ( auto const & choiceVariable : variableInformation . stateToChoiceVariablesMap . at ( initialState ) ) {
constraint = constraint + choiceVariable ;
}
@ -770,7 +770,7 @@ namespace storm {
bool choiceTargetsPsiState = false ;
/ / Check if the current choice targets the current state .
for ( auto const & successorEntry : labeledM dp. getTransitionMatrix ( ) . getRow ( relevantChoice ) ) {
for ( auto const & successorEntry : m dp. getTransitionMatrix ( ) . getRow ( relevantChoice ) ) {
if ( psiStates . get ( successorEntry . getColumn ( ) ) ) {
choiceTargetsPsiState = true ;
break ;
@ -797,7 +797,7 @@ namespace storm {
* the given threshold .
*
* @ param solver The MILP solver .
* @ param labeledMdp The labeled MDP .
* @ param mdp The MDP .
* @ param psiStates A bit vector characterizing all psi states in the model .
* @ param stateInformation The information about the states in the model .
* @ param choiceInformation The information about the choices in the model .
@ -807,7 +807,7 @@ namespace storm {
* @ param includeSchedulerCuts If set to true , additional constraints are asserted that reduce the set of
* possible choices .
*/
static void buildConstraintSystem ( storm : : solver : : LpSolver & solver , storm : : models : : sparse : : Mdp < T > const & labeledMdp , 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 , storm : : storage : : sparse : : PrismChoiceOrigins const & choiceOrigins , storm : : 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 .
uint_fast64_t numberOfConstraints = assertProbabilityGreaterThanThreshold ( solver , variableInformation , probabilityThreshold , strictBound ) ;
STORM_LOG_DEBUG ( " Asserted that reachability probability exceeds threshold. " ) ;
@ -816,9 +816,9 @@ namespace storm {
numberOfConstraints + = assertValidPolicy ( solver , stateInformation , variableInformation ) ;
STORM_LOG_DEBUG ( " Asserted that policy is valid. " ) ;
/ / Add constraints that assert the label sthat belong to some taken choices are taken as well .
numberOfConstraints + = assertChoicesImplyLabel s ( solver , labeledMdp , stateInformation , choiceInformation , variableInformation ) ;
STORM_LOG_DEBUG ( " Asserted that label s implied by choices are taken. " ) ;
/ / Add constraints that assert the command sthat belong to some taken choices are taken as well .
numberOfConstraints + = assertChoicesImplyCommand s ( solver , mdp , choiceOrigins , stateInformation , choiceInformation , variableInformation ) ;
STORM_LOG_DEBUG ( " Asserted that command s implied by choices are taken. " ) ;
/ / Add constraints that encode that the reachability probability from states which do not pick any action
/ / is zero .
@ -826,20 +826,20 @@ namespace storm {
STORM_LOG_DEBUG ( " Asserted that reachability probability is zero if no choice is taken. " ) ;
/ / Add constraints that encode the reachability probabilities for states .
numberOfConstraints + = assertReachabilityProbabilities ( solver , labeledM dp, psiStates , stateInformation , choiceInformation , variableInformation ) ;
numberOfConstraints + = assertReachabilityProbabilities ( solver , m dp, psiStates , stateInformation , choiceInformation , variableInformation ) ;
STORM_LOG_DEBUG ( " Asserted constraints for reachability probabilities. " ) ;
/ / Add constraints that ensure the reachability of an unproblematic state from each problematic state .
numberOfConstraints + = assertUnproblematicStateReachable ( solver , labeledM dp, stateInformation , choiceInformation , variableInformation ) ;
numberOfConstraints + = assertUnproblematicStateReachable ( solver , m dp, stateInformation , choiceInformation , variableInformation ) ;
STORM_LOG_DEBUG ( " Asserted that unproblematic state reachable from problematic states. " ) ;
/ / 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. " ) ;
/ / 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. " ) ;
/ / If required , assert additional constraints that reduce the number of possible policies .
if ( includeSchedulerCuts ) {
numberOfConstraints + = assertSchedulerCuts ( solver , labeledM dp, psiStates , stateInformation , choiceInformation , variableInformation ) ;
numberOfConstraints + = assertSchedulerCuts ( solver , m dp, psiStates , stateInformation , choiceInformation , variableInformation ) ;
STORM_LOG_DEBUG ( " Asserted scheduler cuts. " ) ;
}
@ -850,19 +850,19 @@ namespace storm {
}
/*!
* Computes the set of label sthat was used in the given optimized model .
* Computes the set of command sthat was used in the given optimized model .
*
* @ param solver The MILP solver .
* @ param variableInformation A struct with information about the variables of the model .
*/
static boost : : container : : flat_set < uint_fast64_t > getUsedLabel sInSolution ( storm : : solver : : LpSolver const & solver , VariableInformation const & variableInformation ) {
static boost : : container : : flat_set < uint_fast64_t > getUsedCommand sInSolution ( storm : : solver : : LpSolver const & solver , VariableInformation const & variableInformation ) {
boost : : container : : flat_set < uint_fast64_t > result ;
for ( auto const & label VariablePair: variableInformation . label ToVariableMap) {
bool label Taken= solver . getBinaryValue ( label VariablePair. second ) ;
for ( auto const & command VariablePair: variableInformation . command ToVariableMap) {
bool command Taken= solver . getBinaryValue ( command VariablePair. second ) ;
if ( label Taken) {
result . insert ( label VariablePair. first ) ;
if ( command Taken) {
result . insert ( command VariablePair. first ) ;
}
}
return result ;
@ -873,12 +873,12 @@ namespace storm {
* it is selected by the subsystem computed by the solver .
*
* @ param solver The MILP solver .
* @ param labeledMdp The labeled MDP .
* @ param mdp The MDP .
* @ param stateInformation The information about the states 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 .
*/
static std : : map < uint_fast64_t , uint_fast64_t > getChoices ( storm : : solver : : LpSolver const & solver , storm : : models : : sparse : : Mdp < T > const & labeledM dp, StateInformation const & stateInformation , ChoiceInformation const & choiceInformation , VariableInformation const & variableInformation ) {
static std : : map < uint_fast64_t , uint_fast64_t > getChoices ( storm : : solver : : LpSolver const & solver , storm : : models : : sparse : : Mdp < T > const & m dp, StateInformation const & stateInformation , ChoiceInformation const & choiceInformation , VariableInformation const & variableInformation ) {
std : : map < uint_fast64_t , uint_fast64_t > result ;
for ( auto state : stateInformation . relevantStates ) {
@ -899,10 +899,10 @@ namespace storm {
* Computes the reachability probability and the selected initial state in the given optimized MILP model .
*
* @ param solver The MILP solver .
* @ param labeledMdp The labeled MDP .
* @ param mdp The MDP .
* @ param variableInformation A struct with information about the variables of the model .
*/
static std : : pair < uint_fast64_t , double > getReachabilityProbability ( storm : : solver : : LpSolver const & solver , storm : : models : : sparse : : Mdp < T > const & labeledM dp, VariableInformation const & variableInformation ) {
static std : : pair < uint_fast64_t , double > getReachabilityProbability ( storm : : solver : : LpSolver const & solver , storm : : models : : sparse : : Mdp < T > const & m dp, VariableInformation const & variableInformation ) {
uint_fast64_t selectedInitialState = 0 ;
for ( auto const & initialStateVariablePair : variableInformation . initialStateToChoiceVariableMap ) {
bool initialStateChosen = solver . getBinaryValue ( initialStateVariablePair . second ) ;
@ -917,18 +917,20 @@ namespace storm {
}
public :
static boost : : container : : flat_set < uint_fast64_t > getMinimalLabelSet ( storm : : models : : sparse : : Mdp < T > const & labeledMdp , storm : : storage : : BitVector const & phiStates , storm : : storage : : BitVector const & psiStates , double probabilityThreshold , bool strictBound , bool checkThresholdFeasible = false , bool includeSchedulerCuts = false ) {
/ / ( 0 ) Check whether the MDP is indeed labeled .
if ( ! labeledMdp . hasChoiceLabeling ( ) ) {
throw storm : : exceptions : : InvalidArgumentException ( ) < < " Minimal label set generation is impossible for unlabeled model. " ;
}
static boost : : container : : flat_set < uint_fast64_t > getMinimalCommandSet ( storm : : models : : sparse : : Mdp < T > const & mdp , std : : shared_ptr < storm : : storage : : sparse : : ChoiceOrigins > const & choiceOrigins , 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 ( choiceOrigins , storm : : exceptions : : InvalidArgumentException , " Restriction to command set is impossible for model without choice origns. " ) ;
STORM_LOG_THROW ( choiceOrigins - > isPrismChoiceOrigins ( ) , storm : : exceptions : : InvalidArgumentException , " Restriction to command set is impossible for model without prism choice origins. " ) ;
storm : : storage : : sparse : : PrismChoiceOrigins const & prismChoiceOrigins = choiceOrigins - > asPrismChoiceOrigins ( ) ;
/ / ( 1 ) Check whether its possible to exceed the threshold if checkThresholdFeasible is set .
double maximalReachabilityProbability = 0 ;
if ( checkThresholdFeasible ) {
storm : : modelchecker : : helper : : SparseMdpPrctlHelper < T > modelcheckerHelper ;
std : : vector < T > result = std : : move ( modelcheckerHelper . computeUntilProbabilities ( false , labeledM dp. getTransitionMatrix ( ) , labeledM dp. getBackwardTransitions ( ) , phiStates , psiStates , false , false , storm : : solver : : GeneralMinMaxLinearEquationSolverFactory < T > ( ) ) . values ) ;
for ( auto state : labeledM dp. getInitialStates ( ) ) {
std : : vector < T > result = std : : move ( modelcheckerHelper . computeUntilProbabilities ( false , m dp. getTransitionMatrix ( ) , m dp. getBackwardTransitions ( ) , phiStates , psiStates , false , false , storm : : solver : : GeneralMinMaxLinearEquationSolverFactory < T > ( ) ) . values ) ;
for ( auto state : m dp. getInitialStates ( ) ) {
maximalReachabilityProbability = std : : max ( maximalReachabilityProbability , result [ state ] ) ;
}
STORM_LOG_THROW ( ( strictBound & & maximalReachabilityProbability > = probabilityThreshold ) | | ( ! strictBound & & maximalReachabilityProbability > probabilityThreshold ) , storm : : exceptions : : InvalidArgumentException , " Given probability threshold " < < probabilityThreshold < < " can not be " < < ( strictBound ? " achieved " : " exceeded " ) < < " in model with maximal reachability probability of " < < maximalReachabilityProbability < < " . " ) ;
@ -936,40 +938,41 @@ namespace storm {
}
/ / ( 2 ) Identify relevant and problematic states .
StateInformation stateInformation = determineRelevantAndProblematicStates ( labeledM dp, phiStates , psiStates ) ;
StateInformation stateInformation = determineRelevantAndProblematicStates ( m dp, phiStates , psiStates ) ;
/ / ( 3 ) Determine sets of relevant label sand problematic choices .
ChoiceInformation choiceInformation = determineRelevantAndProblematicChoices ( labeledMdp , stateInformation , psiStates ) ;
/ / ( 3 ) Determine sets of relevant command sand problematic choices .
ChoiceInformation choiceInformation = determineRelevantAndProblematicChoices ( mdp , prismChoiceOrigins , stateInformation , psiStates ) ;
/ / ( 4 ) Encode resulting system as MILP problem .
std : : shared_ptr < storm : : solver : : LpSolver > solver = storm : : utility : : solver : : getLpSolver ( " MinimalCommandSetCounterexample " ) ;
/ / ( 4.1 ) Create variables .
VariableInformation variableInformation = createVariables ( * solver , labeledM dp, stateInformation , choiceInformation ) ;
VariableInformation variableInformation = createVariables ( * solver , m dp, stateInformation , choiceInformation ) ;
/ / ( 4.2 ) Construct constraint system .
buildConstraintSystem ( * solver , labeledMdp , psiStates , stateInformation , choiceInformation , variableInformation , probabilityThreshold , strictBound , includeSchedulerCuts ) ;
buildConstraintSystem ( * solver , mdp , prismChoiceOrigins , psiStates , stateInformation , choiceInformation , variableInformation , probabilityThreshold , strictBound , includeSchedulerCuts ) ;
/ / ( 4.3 ) Optimize the model .
solver - > optimize ( ) ;
/ / ( 4.4 ) Read off result from variables .
boost : : container : : flat_set < uint_fast64_t > usedLabelSet = getUsedLabel sInSolution ( * solver , variableInformation ) ;
usedLabel Set . insert ( choiceInformation . knownLabel s . begin ( ) , choiceInformation . knownLabel s . end ( ) ) ;
boost : : container : : flat_set < uint_fast64_t > usedCommandSet = getUsedCommand sInSolution ( * solver , variableInformation ) ;
usedCommand Set . insert ( choiceInformation . knownCommand s . begin ( ) , choiceInformation . knownCommand s . end ( ) ) ;
/ / ( 5 ) Return result .
return usedLabel Set ;
return usedCommand Set ;
}
/*!
* Computes a ( minimally labeled ) counterexample for the given model and ( safety ) formula . If the model satisfies the property , an exception is thrown .
* Computes a ( minimal ) counterexample with respect to the number of prism commands for the given model and ( safety ) formula . If the model satisfies the property , an exception is thrown .
*
* @ param labeledMdp A labeled MDP that is the model in which to generate the counterexample .
* @ param mdp An MDP that is the model in which to generate the counterexample .
* @ param choiceOrigins the choice origins generated for the mdp
* @ param formulaPtr A pointer to a safety formula . The outermost operator must be a probabilistic bound operator with a strict upper bound . The nested
* formula can be either an unbounded until formula or an eventually formula .
*/
static void computeCounterexample ( storm : : prism : : Program const & program , storm : : models : : sparse : : Mdp < T > const & labeledMdp , std : : shared_ptr < storm : : logic : : Formula const > const & formula ) {
std : : cout < < std : : endl < < " Generating minimal label counterexample for formula " < < * formula < < std : : endl ;
static void computeCounterexample ( storm : : prism : : Program const & program , storm : : models : : sparse : : Mdp < T > const & mdp , std : : shared_ptr < storm : : storage : : sparse : : ChoiceOrigins > const & choiceOrigins , std : : shared_ptr < storm : : logic : : Formula const > const & formula ) {
std : : cout < < std : : endl < < " Generating minimal command set counterexample for formula " < < * formula < < std : : endl ;
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 ( ) ;
@ -983,7 +986,7 @@ namespace storm {
storm : : storage : : BitVector phiStates ;
storm : : storage : : BitVector psiStates ;
storm : : modelchecker : : SparsePropositionalModelChecker < storm : : models : : sparse : : Mdp < T > > modelchecker ( labeledM dp) ;
storm : : modelchecker : : SparsePropositionalModelChecker < storm : : models : : sparse : : Mdp < T > > modelchecker ( m dp) ;
if ( probabilityOperator . getSubformula ( ) . isUntilFormula ( ) ) {
storm : : logic : : UntilFormula const & untilFormula = probabilityOperator . getSubformula ( ) . asUntilFormula ( ) ;
@ -1003,18 +1006,18 @@ namespace storm {
storm : : modelchecker : : ExplicitQualitativeCheckResult const & subQualitativeResult = subResult - > asExplicitQualitativeCheckResult ( ) ;
phiStates = storm : : storage : : BitVector ( labeledM dp. getNumberOfStates ( ) , true ) ;
phiStates = storm : : storage : : BitVector ( m dp. getNumberOfStates ( ) , true ) ;
psiStates = subQualitativeResult . getTruthValuesVector ( ) ;
}
/ / Delegate the actual computation work to the function of equal name .
auto startTime = std : : chrono : : high_resolution_clock : : now ( ) ;
boost : : container : : flat_set < uint_fast64_t > usedLabelSet = getMinimalLabelSet ( labeledMdp , phiStates , psiStates , threshold , strictBound , true , storm : : settings : : getModule < storm : : settings : : modules : : CounterexampleGeneratorSettings > ( ) . isUseSchedulerCutsSet ( ) ) ;
boost : : container : : flat_set < uint_fast64_t > usedCommandSet = getMinimalCommandSet ( mdp , choiceOrigins , phiStates , psiStates , threshold , strictBound , true , storm : : settings : : getModule < storm : : settings : : modules : : CounterexampleGeneratorSettings > ( ) . isUseSchedulerCutsSet ( ) ) ;
auto endTime = std : : chrono : : high_resolution_clock : : now ( ) ;
std : : cout < < std : : endl < < " Computed minimal label set of size " < < usedLabel Set . 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 " < < usedCommand Set . size ( ) < < " in " < < std : : chrono : : duration_cast < std : : chrono : : milliseconds > ( endTime - startTime ) . count ( ) < < " ms. " < < std : : endl ;
std : : cout < < " Resulting program: " < < std : : endl ;
storm : : prism : : Program restrictedProgram = program . restrictCommands ( usedLabel Set ) ;
storm : : prism : : Program restrictedProgram = program . restrictCommands ( usedCommand Set ) ;
std : : cout < < restrictedProgram < < std : : endl ;
std : : cout < < std : : endl < < " ------------------------------------------- " < < std : : endl ;
}
TimQu
10 years ago