@ -5,7 +5,7 @@
# include "storm/solver/Z3SmtSolver.h"
# include "storm/counterexamples/HighLevelCounterexample.h"
# include "storm-counterexamples /counterexamples/HighLevelCounterexample.h"
# include "storm/storage/prism/Program.h"
# include "storm/storage/expressions/Expression.h"
@ -49,14 +49,20 @@ namespace storm {
/ / The set of labels that matter in terms of minimality .
boost : : container : : flat_set < uint_fast64_t > minimalityLabels ;
/ / A set of labels that is definitely known to be taken in the final solution .
boost : : container : : flat_set < uint_fast64_t > knownLabels ;
boost : : container : : flat_set < uint64_t > dontCareLabels ;
/ / A list of relevant choices for each relevant state .
std : : map < uint_fast64_t , std : : list < uint_fast64_t > > relevantChoicesForRelevantStates ;
} ;
struct GeneratorStats {
} ;
struct VariableInformation {
/ / The manager responsible for the constraints we are building .
std : : shared_ptr < storm : : expressions : : ExpressionManager > manager ;
@ -154,10 +160,12 @@ namespace storm {
std : : set_difference ( relevancyInformation . relevantLabels . begin ( ) , relevancyInformation . relevantLabels . end ( ) , relevancyInformation . knownLabels . begin ( ) , relevancyInformation . knownLabels . end ( ) , std : : inserter ( remainingLabels , remainingLabels . end ( ) ) ) ;
relevancyInformation . relevantLabels = remainingLabels ;
}
relevancyInformation . dontCareLabels = dontCareLabels ;
std : : set_difference ( relevancyInformation . relevantLabels . begin ( ) , relevancyInformation . relevantLabels . end ( ) , dontCareLabels . begin ( ) , dontCareLabels . end ( ) , std : : inserter ( relevancyInformation . minimalityLabels , relevancyInformation . minimalityLabels . begin ( ) ) ) ;
STORM_LOG_DEBUG ( " Found " < < relevancyInformation . relevantLabels . size ( ) < < " relevant and " < < relevancyInformation . knownLabels . size ( ) < < " known labels. " ) ;
STORM_LOG_DEBUG ( " Found " < < relevancyInformation . minimalityLabels . size ( ) < < " labels to minize over. " ) ;
return relevancyInformation ;
}
@ -649,10 +657,11 @@ namespace storm {
/ / Popping the disjunction of negated guards from the solver stack .
localSolver - > pop ( ) ;
STORM_LOG_ERROR_COND ( backwardImplicationAdded , " Error in adding cuts for counterexample generation (backward implication misses a label set). " ) ;
} else {
STORM_LOG_DEBUG ( " Selection is enabled in initial state. " ) ;
}
STORM_LOG_ERROR_COND ( backwardImplicationAdded , " Error in adding cuts for counterexample generation (backward implication misses a label set). " ) ;
}
} else if ( symbolicModel . isJaniModel ( ) ) {
STORM_LOG_WARN ( " Model uses assignment levels, did not assert backward implications. " ) ;
@ -1153,112 +1162,6 @@ namespace storm {
return relaxingVariable ;
}
/*!
* Asserts that the input vector encodes a decimal smaller or equal to one .
*
* @ param context The Z3 context in which to build the expressions .
* @ param solver The solver to use for the satisfiability evaluation .
* @ param input The binary encoded input number .
*/
static void assertLessOrEqualOne ( z3 : : context & context , z3 : : solver & solver , std : : vector < z3 : : expr > input ) {
std : : transform ( input . begin ( ) , input . end ( ) , input . begin ( ) , [ ] ( z3 : : expr e ) - > z3 : : expr { return ! e ; } ) ;
assertConjunction ( context , solver , input ) ;
}
/*!
* Asserts that at most one of given literals may be true at any time .
*
* @ param context The Z3 context in which to build the expressions .
* @ param solver The solver to use for the satisfiability evaluation .
* @ param blockingVariables A vector of variables out of which only one may be true .
*/
static void assertAtMostOne ( z3 : : context & context , z3 : : solver & solver , std : : vector < z3 : : expr > const & literals ) {
std : : vector < z3 : : expr > counter = createCounterCircuit ( context , literals ) ;
assertLessOrEqualOne ( context , solver , counter ) ;
}
/*!
* Performs one Fu - Malik - Maxsat step .
*
* @ param context The Z3 context in which to build the expressions .
* @ param solver The solver to use for the satisfiability evaluation .
* @ param variableInformation A structure with information about the variables for the labels .
* @ return True iff the constraint system was satisfiable .
*/
static bool fuMalikMaxsatStep ( z3 : : context & context , z3 : : solver & solver , std : : vector < z3 : : expr > & auxiliaryVariables , std : : vector < z3 : : expr > & softConstraints , uint_fast64_t & nextFreeVariableIndex ) {
z3 : : expr_vector assumptions ( context ) ;
for ( auto const & auxiliaryVariable : auxiliaryVariables ) {
assumptions . push_back ( ! auxiliaryVariable ) ;
}
/ / Check whether the assumptions are satisfiable .
STORM_LOG_DEBUG ( " Invoking satisfiability checking. " ) ;
z3 : : check_result result = solver . check ( assumptions ) ;
STORM_LOG_DEBUG ( " Done invoking satisfiability checking. " ) ;
if ( result = = z3 : : sat ) {
return true ;
} else {
STORM_LOG_DEBUG ( " Computing unsat core. " ) ;
z3 : : expr_vector unsatCore = solver . unsat_core ( ) ;
STORM_LOG_DEBUG ( " Computed unsat core. " ) ;
std : : vector < z3 : : expr > blockingVariables ;
blockingVariables . reserve ( unsatCore . size ( ) ) ;
/ / Create stringstream to build expression names .
std : : stringstream variableName ;
for ( uint_fast64_t softConstraintIndex = 0 ; softConstraintIndex < softConstraints . size ( ) ; + + softConstraintIndex ) {
for ( uint_fast64_t coreIndex = 0 ; coreIndex < unsatCore . size ( ) ; + + coreIndex ) {
bool isContainedInCore = false ;
if ( softConstraints [ softConstraintIndex ] = = unsatCore [ coreIndex ] ) {
isContainedInCore = true ;
}
if ( isContainedInCore ) {
variableName . clear ( ) ;
variableName . str ( " " ) ;
variableName < < " b " < < nextFreeVariableIndex ;
blockingVariables . push_back ( context . bool_const ( variableName . str ( ) . c_str ( ) ) ) ;
variableName . clear ( ) ;
variableName . str ( " " ) ;
variableName < < " a " < < nextFreeVariableIndex ;
+ + nextFreeVariableIndex ;
auxiliaryVariables [ softConstraintIndex ] = context . bool_const ( variableName . str ( ) . c_str ( ) ) ;
softConstraints [ softConstraintIndex ] = softConstraints [ softConstraintIndex ] | | blockingVariables . back ( ) ;
solver . add ( softConstraints [ softConstraintIndex ] | | auxiliaryVariables [ softConstraintIndex ] ) ;
}
}
}
assertAtMostOne ( context , solver , blockingVariables ) ;
}
return false ;
}
/*!
* Rules out the given command set for the given solver .
*
* @ param context The Z3 context in which to build the expressions .
* @ param solver The solver to use for the satisfiability evaluation .
* @ param commandSet The command set to rule out as a solution .
* @ param variableInformation A structure with information about the variables for the labels .
*/
static void ruleOutSolution ( z3 : : context & context , z3 : : solver & solver , boost : : container : : flat_set < uint_fast64_t > const & commandSet , VariableInformation const & variableInformation ) {
z3 : : expr blockSolutionExpression = context . bool_val ( false ) ;
for ( auto labelIndexPair : variableInformation . labelToIndexMap ) {
if ( commandSet . find ( labelIndexPair . first ) ! = commandSet . end ( ) ) {
blockSolutionExpression = blockSolutionExpression | | variableInformation . labelVariables [ labelIndexPair . second ] ;
}
}
solver . add ( blockSolutionExpression ) ;
}
/*!
* Determines the set of labels that was chosen by the given model .
@ -1316,7 +1219,7 @@ namespace storm {
* in order to satisfy the constraint system .
* @ return The smallest set of labels such that the constraint system of the solver is satisfiable .
*/
static boost : : container : : flat_set < uint_fast64_t > findSmallestCommandSet ( storm : : solver : : SmtSolver & solver , VariableInformation & variableInformation , uint_fast64_t & currentBound ) {
static boost : : optional < boost : : container : : flat_set < uint_fast64_t > > findSmallestCommandSet ( storm : : solver : : SmtSolver & solver , VariableInformation & variableInformation , uint_fast64_t & currentBound ) {
/ / Check if we can find a solution with the current bound .
storm : : expressions : : Expression assumption = ! variableInformation . auxiliaryVariables . back ( ) ;
@ -1331,6 +1234,10 @@ namespace storm {
solver . add ( variableInformation . auxiliaryVariables . back ( ) ) ;
variableInformation . auxiliaryVariables . push_back ( assertLessOrEqualKRelaxed ( solver , variableInformation , + + currentBound ) ) ;
assumption = ! variableInformation . auxiliaryVariables . back ( ) ;
if ( currentBound > ( 1 < < variableInformation . minimalityLabelVariables . size ( ) ) ) {
STORM_LOG_DEBUG ( " Constraint system fully explored: Bound exceeds maximum of " < < ( 1 < < variableInformation . minimalityLabelVariables . size ( ) ) ) ;
return boost : : none ;
}
}
/ / At this point we know that the constraint system was satisfiable , so compute the induced label
@ -1342,12 +1249,17 @@ namespace storm {
std : : vector < storm : : expressions : : Expression > formulae ;
boost : : container : : flat_set < uint_fast64_t > unknownLabels ;
std : : set_difference ( labelSet . begin ( ) , labelSet . end ( ) , relevancyInformation . knownLabels . begin ( ) , relevancyInformation . knownLabels . end ( ) , std : : inserter ( unknownLabels , unknownLabels . end ( ) ) ) ;
std : : set_intersection ( labelSet . begin ( ) , labelSet . end ( ) , relevancyInformation . minimalityLabels . begin ( ) , relevancyInformation . minimalityLabels . end ( ) , std : : inserter ( unknownLabels , unknownLabels . end ( ) ) ) ;
/ / std : : set_difference ( labelSet . begin ( ) , labelSet . end ( ) , relevancyInformation . knownLabels . begin ( ) , relevancyInformation . knownLabels . end ( ) , std : : inserter ( unknownLabels , unknownLabels . end ( ) ) ) ;
for ( auto const & label : unknownLabels ) {
formulae . emplace_back ( ! variableInformation . labelVariables . at ( variableInformation . labelToIndexMap . at ( label ) ) ) ;
}
boost : : container : : flat_set < uint_fast64_t > remainingLabels ;
std : : set_difference ( relevancyInformation . relevantLabels . begin ( ) , relevancyInformation . relevantLabels . end ( ) , labelSet . begin ( ) , labelSet . end ( ) , std : : inserter ( remainingLabels , remainingLabels . end ( ) ) ) ;
/ / std : : set_difference ( relevancyInformation . relevantLabels . begin ( ) , relevancyInformation . relevantLabels . end ( ) , labelSet . begin ( ) , labelSet . end ( ) , std : : inserter ( remainingLabels , remainingLabels . end ( ) ) ) ;
std : : set_difference ( relevancyInformation . minimalityLabels . begin ( ) , relevancyInformation . minimalityLabels . end ( ) , labelSet . begin ( ) , labelSet . end ( ) , std : : inserter ( remainingLabels , remainingLabels . end ( ) ) ) ;
for ( auto const & label : remainingLabels ) {
formulae . emplace_back ( variableInformation . labelVariables . at ( variableInformation . labelToIndexMap . at ( label ) ) ) ;
}
@ -1355,6 +1267,22 @@ namespace storm {
STORM_LOG_DEBUG ( " Ruling out single solution. " ) ;
assertDisjunction ( solver , formulae , * variableInformation . manager ) ;
}
static void ruleOutBiggerSolutions ( storm : : solver : : SmtSolver & solver , boost : : container : : flat_set < uint_fast64_t > const & labelSet , VariableInformation & variableInformation , RelevancyInformation const & relevancyInformation ) {
std : : vector < storm : : expressions : : Expression > formulae ;
boost : : container : : flat_set < uint_fast64_t > unknownLabels ;
std : : set_intersection ( labelSet . begin ( ) , labelSet . end ( ) , relevancyInformation . minimalityLabels . begin ( ) , relevancyInformation . minimalityLabels . end ( ) , std : : inserter ( unknownLabels , unknownLabels . end ( ) ) ) ;
/ / std : : set_difference ( labelSet . begin ( ) , labelSet . end ( ) , relevancyInformation . knownLabels . begin ( ) , relevancyInformation . knownLabels . end ( ) , std : : inserter ( unknownLabels , unknownLabels . end ( ) ) ) ;
for ( auto const & label : unknownLabels ) {
formulae . emplace_back ( ! variableInformation . labelVariables . at ( variableInformation . labelToIndexMap . at ( label ) ) ) ;
}
STORM_LOG_DEBUG ( " Ruling out set of solutions. " ) ;
assertDisjunction ( solver , formulae , * variableInformation . manager ) ;
}
/*!
* Analyzes the given sub - model that has a maximal reachability of zero ( i . e . no psi states are reachable ) and tries to construct assertions that aim to make at least one psi state reachable .
@ -1582,7 +1510,7 @@ namespace storm {
* Returns the sub - model obtained from removing all choices that do not originate from the specified filterLabelSet .
* Also returns the Labelsets of the sub - model .
*/
static std : : pair < std : : shared_ptr < storm : : models : : sparse : : Model < T > > , std : : vector < boost : : container : : flat_set < uint_fast64_t > > > restrictModelToLabelSet ( storm : : models : : sparse : : Model < T > const & model , boost : : container : : flat_set < uint_fast64_t > const & filterLabelSet ) {
static std : : pair < std : : shared_ptr < storm : : models : : sparse : : Model < T > > , std : : vector < boost : : container : : flat_set < uint_fast64_t > > > restrictModelToLabelSet ( storm : : models : : sparse : : Model < T > const & model , boost : : container : : flat_set < uint_fast64_t > const & filterLabelSet , boost : : optional < uint64_t > absorbState = boost : : none ) {
bool customRowGrouping = model . isOfType ( storm : : models : : ModelType : : Mdp ) ;
@ -1616,7 +1544,8 @@ namespace storm {
if ( customRowGrouping ) {
transitionMatrixBuilder . newRowGroup ( currentRow ) ;
}
transitionMatrixBuilder . addNextValue ( currentRow , state , storm : : utility : : one < T > ( ) ) ;
uint64_t targetState = absorbState = = boost : : none ? state : absorbState . get ( ) ;
transitionMatrixBuilder . addNextValue ( currentRow , targetState , storm : : utility : : one < T > ( ) ) ;
/ / Insert an empty label set for this choice
resultLabelSet . emplace_back ( ) ;
+ + currentRow ;
@ -1633,17 +1562,25 @@ namespace storm {
return std : : make_pair ( resultModel , std : : move ( resultLabelSet ) ) ;
}
static T computeMaximalReachabilityProbability ( Environment const & env , storm : : models : : sparse : : Model < T > const & model , storm : : storage : : BitVector const & phiStates , storm : : storage : : BitVector const & psiStates ) {
static T computeMaximalReachabilityProbability ( Environment const & env , storm : : models : : sparse : : Model < T > const & model , storm : : storage : : BitVector const & phiStates , storm : : storage : : BitVector const & psiStates , boost : : optional < std : : string > const & rewardName ) {
T result = storm : : utility : : zero < T > ( ) ;
std : : vector < T > allStatesResult ;
STORM_LOG_DEBUG ( " Invoking model checker. " ) ;
if ( model . isOfType ( storm : : models : : ModelType : : Dtmc ) ) {
allStatesResult = storm : : modelchecker : : helper : : SparseDtmcPrctlHelper < T > : : computeUntilProbabilities ( env , false , model . getTransitionMatrix ( ) , model . getBackwardTransitions ( ) , phiStates , psiStates , false ) ;
if ( rewardName = = boost : : none ) {
allStatesResult = storm : : modelchecker : : helper : : SparseDtmcPrctlHelper < T > : : computeUntilProbabilities ( env , false , model . getTransitionMatrix ( ) , model . getBackwardTransitions ( ) , phiStates , psiStates , false ) ;
} else {
allStatesResult = storm : : modelchecker : : helper : : SparseDtmcPrctlHelper < T > : : computeReachabilityRewards ( env , false , model . getTransitionMatrix ( ) , model . getBackwardTransitions ( ) , model . getRewardModel ( rewardName . get ( ) ) , psiStates , false ) ;
}
} else {
storm : : modelchecker : : helper : : SparseMdpPrctlHelper < T > modelCheckerHelper ;
allStatesResult = std : : move ( modelCheckerHelper . computeUntilProbabilities ( env , false , model . getTransitionMatrix ( ) , model . getBackwardTransitions ( ) , phiStates , psiStates , false , false ) . values ) ;
if ( rewardName = = boost : : none ) {
storm : : modelchecker : : helper : : SparseMdpPrctlHelper < T > modelCheckerHelper ;
allStatesResult = std : : move ( modelCheckerHelper . computeUntilProbabilities ( env , false , model . getTransitionMatrix ( ) , model . getBackwardTransitions ( ) , phiStates , psiStates , false , false ) . values ) ;
} else {
STORM_LOG_THROW ( rewardName ! = boost : : none , storm : : exceptions : : NotSupportedException , " Reward property counterexample generation is currently only supported for DTMCs. " ) ;
}
}
for ( auto state : model . getInitialStates ( ) ) {
result = std : : max ( result , allStatesResult [ state ] ) ;
@ -1664,6 +1601,9 @@ namespace storm {
bool encodeReachability ;
bool useDynamicConstraints ;
bool silent = false ;
uint64_t continueAfterFirstCounterexampleUntil = 0 ;
uint64_t maximumCounterexamples = 1 ;
uint64_t multipleCounterexampleSizeCap = 100000000 ;
} ;
/*!
@ -1673,12 +1613,14 @@ namespace storm {
* @ param model The sparse model in which to find the minimal command set .
* @ param phiStates A bit vector characterizing all phi states in the model .
* @ param psiStates A bit vector characterizing all psi states in the model .
* @ param probabilityThreshold The threshold that is to be achieved or exceeded .
* @ param propertyThreshold The threshold that is to be achieved or exceeded .
* @ param rewardName The name of the reward structure to use , or boost : : none if probabilities are considerd .
* @ param strictBound Indicates whether the threshold needs to be achieved ( true ) or exceeded ( false ) .
* @ param options A set of options for customization .
*/
static boost : : container : : flat_set < uint_fast64_t > getMinimalLabelSet ( Environment const & env , storm : : storage : : SymbolicModelDescription const & symbolicModel , storm : : models : : sparse : : Model < T > const & model , storm : : storage : : BitVector const & phiStates , storm : : storage : : BitVector const & psiStates , double probabilityThreshold , bool strictBound , boost : : container : : flat_set < uint_fast64_t > const & dontCareLabels = boost : : container : : flat_set < uint_fast64_t > ( ) , Options const & options = Options ( ) ) {
static std : : vector < boost : : container : : flat_set < uint_fast64_t > > getMinimalLabelSet ( Environment const & env , storm : : storage : : SymbolicModelDescription const & symbolicModel , storm : : models : : sparse : : Model < T > const & model , storm : : storage : : BitVector const & phiStates , storm : : storage : : BitVector const & psiStates , double propertyThreshold , boost : : optional < std : : string > const & rewardName , bool strictBound , boost : : container : : flat_set < uint_fast64_t > const & dontCareLabels = boost : : container : : flat_set < uint_fast64_t > ( ) , Options const & options = Options ( ) ) {
# ifdef STORM_HAVE_Z3
std : : vector < boost : : container : : flat_set < uint_fast64_t > > result ;
/ / Set up all clocks used for time measurement .
auto totalClock = std : : chrono : : high_resolution_clock : : now ( ) ;
auto timeOfLastMessage = std : : chrono : : high_resolution_clock : : now ( ) ;
@ -1718,10 +1660,10 @@ namespace storm {
/ / ( 1 ) Check whether its possible to exceed the threshold if checkThresholdFeasible is set .
double maximalReachabilityProbability = 0 ;
if ( options . checkThresholdFeasible ) {
maximalReachabilityProbability = computeMaximalReachabilityProbability ( env , model , phiStates , psiStates ) ;
maximalReachabilityProbability = computeMaximalReachabilityProbability ( env , model , phiStates , psiStates , rewardName ) ;
STORM_LOG_THROW ( ( strictBound & & maximalReachabilityProbability > = probabili tyThreshold ) | | ( ! strictBound & & maximalReachabilityProbability > probabili tyThreshold ) , storm : : exceptions : : InvalidArgumentException , " Given probability threshold " < < probabili tyThreshold < < " can not be " < < ( strictBound ? " achieved " : " exceeded " ) < < " in model with maximal reachability probability of " < < maximalReachabilityProbability < < " . " ) ;
std : : cout < < std : : endl < < " Maximal reachability in model is " < < maximalReachabilityProbability < < " . " < < std : : endl < < std : : endl ;
STORM_LOG_THROW ( ( strictBound & & maximalReachabilityProbability > = proper tyThreshold ) | | ( ! strictBound & & maximalReachabilityProbability > proper tyThreshold ) , storm : : exceptions : : InvalidArgumentException , " Given probability threshold " < < proper tyThreshold < < " can not be " < < ( strictBound ? " achieved " : " exceeded " ) < < " in model with maximal reachability probability of " < < maximalReachabilityProbability < < " . " ) ;
std : : cout < < std : : endl < < " Maximal property value in model is " < < maximalReachabilityProbability < < " . " < < std : : endl < < std : : endl ;
}
/ / ( 2 ) Identify all states and commands that are relevant , because only these need to be considered later .
@ -1762,10 +1704,10 @@ namespace storm {
/ / If there are no relevant labels , return directly .
if ( relevancyInformation . relevantLabels . empty ( ) ) {
return commandSet ;
return { commandSet } ;
} else if ( relevancyInformation . minimalityLabels . empty ( ) ) {
commandSet . insert ( relevancyInformation . relevantLabels . begin ( ) , relevancyInformation . relevantLabels . end ( ) ) ;
return commandSet ;
return { commandSet } ;
}
/ / Set up some variables for the iterations .
@ -1773,31 +1715,45 @@ namespace storm {
uint_fast64_t lastSize = 0 ;
uint_fast64_t iterations = 0 ;
uint_fast64_t currentBound = 0 ;
maximalReachabilityProbability = 0 ;
double maximalPropertyValue = 0 ;
uint_fast64_t zeroProbabilityCount = 0 ;
uint64_t smallestCounterexampleSize = model . getNumberOfChoices ( ) ; / / Definitive u
uint64_t progressDelay = storm : : settings : : getModule < storm : : settings : : modules : : GeneralSettings > ( ) . getShowProgressDelay ( ) ;
do {
STORM_LOG_DEBUG ( " Computing minimal command set. " ) ;
solverClock = std : : chrono : : high_resolution_clock : : now ( ) ;
commandSe t= findSmallestCommandSet ( * solver , variableInformation , currentBound ) ;
boost : : optional < boost : : container : : flat_set < uint_fast64_t > > smalles t= findSmallestCommandSet ( * solver , variableInformation , currentBound ) ;
totalSolverTime + = std : : chrono : : high_resolution_clock : : now ( ) - solverClock ;
STORM_LOG_DEBUG ( " Computed minimal command set of size " < < commandSet . size ( ) + relevancyInformation . knownLabels . size ( ) < < " ( " < < commandSet . size ( ) < < " + " < < relevancyInformation . knownLabels . size ( ) < < " ) " ) ;
if ( smallest = = boost : : none ) {
STORM_LOG_DEBUG ( " No further counterexamples. " ) ;
break ;
} else {
commandSet = smallest . get ( ) ;
}
STORM_LOG_DEBUG ( " Computed minimal command with bound " < < currentBound < < " and set of size " < < commandSet . size ( ) + relevancyInformation . knownLabels . size ( ) < < " ( " < < commandSet . size ( ) < < " + " < < relevancyInformation . knownLabels . size ( ) < < " ) " ) ;
/ / Restrict the given model to the current set of labels and compute the reachability probability .
modelCheckingClock = std : : chrono : : high_resolution_clock : : now ( ) ;
commandSet . insert ( relevancyInformation . knownLabels . begin ( ) , relevancyInformation . knownLabels . end ( ) ) ;
auto subChoiceOrigins = restrictModelToLabelSet ( model , commandSet ) ;
commandSet . insert ( relevancyInformation . dontCareLabels . begin ( ) , relevancyInformation . dontCareLabels . end ( ) ) ;
if ( commandSet . size ( ) > smallestCounterexampleSize + options . continueAfterFirstCounterexampleUntil | | ( result . size ( ) > 1 & & commandSet . size ( ) > options . multipleCounterexampleSizeCap ) ) {
STORM_LOG_DEBUG ( " No further counterexamples of similar size. " ) ;
break ;
}
auto subChoiceOrigins = restrictModelToLabelSet ( model , commandSet , psiStates . getNextSetIndex ( 0 ) ) ;
std : : shared_ptr < storm : : models : : sparse : : Model < T > > const & subModel = subChoiceOrigins . first ;
std : : vector < boost : : container : : flat_set < uint_fast64_t > > const & subLabelSets = subChoiceOrigins . second ;
/ / Now determine the maximal reachability probability in the sub - model .
maximalReachabilityProbability = computeMaximalReachabilityProbability ( env , * subModel , phiStates , psiStates ) ;
maximalPropertyValue = computeMaximalReachabilityProbability ( env , * subModel , phiStates , psiStates , rewardName ) ;
totalModelCheckingTime + = std : : chrono : : high_resolution_clock : : now ( ) - modelCheckingClock ;
/ / Depending on whether the threshold was successfully achieved or not , we proceed by either analyzing the bad solution or stopping the iteration process .
analysisClock = std : : chrono : : high_resolution_clock : : now ( ) ;
if ( ( strictBound & & maximalReachabilityProbability < probabili tyThreshold ) | | ( ! strictBound & & maximalReachabilityProbability < = probabili tyThreshold ) ) {
if ( maximalReachabilityProbability = = storm : : utility : : zero < T > ( ) ) {
if ( ( strictBound & & maximalPropertyValue < proper tyThreshold ) | | ( ! strictBound & & maximalPropertyValue < = proper tyThreshold ) ) {
if ( maximalPropertyValue = = storm : : utility : : zero < T > ( ) ) {
+ + zeroProbabilityCount ;
}
@ -1813,12 +1769,26 @@ namespace storm {
/ / the given threshold , we analyze the solution and try to guide the solver into the right direction .
analyzeInsufficientProbabilitySolution ( * solver , * subModel , subLabelSets , model , labelSets , phiStates , psiStates , commandSet , variableInformation , relevancyInformation ) ;
}
if ( relevancyInformation . dontCareLabels . size ( ) > 0 ) {
ruleOutSingleSolution ( * solver , commandSet , variableInformation , relevancyInformation ) ;
}
} else {
/ / Do not guide solver , just rule out current solution .
ruleOutSingleSolution ( * solver , commandSet , variableInformation , relevancyInformation ) ;
}
} else {
done = true ;
STORM_LOG_DEBUG ( " Found a counterexample. " ) ;
result . push_back ( commandSet ) ;
if ( options . maximumCounterexamples > result . size ( ) ) {
STORM_LOG_DEBUG ( " Exclude counterexample for future. " ) ;
ruleOutBiggerSolutions ( * solver , commandSet , variableInformation , relevancyInformation ) ;
} else {
STORM_LOG_DEBUG ( " Stop searching for further counterexamples. " ) ;
done = true ;
}
}
totalAnalysisTime + = ( std : : chrono : : high_resolution_clock : : now ( ) - analysisClock ) ;
+ + iterations ;
@ -1828,10 +1798,10 @@ namespace storm {
if ( static_cast < uint64_t > ( durationSinceLastMessage ) > = progressDelay | | lastSize < commandSet . size ( ) ) {
auto milliseconds = std : : chrono : : duration_cast < std : : chrono : : milliseconds > ( now - totalClock ) . count ( ) ;
if ( lastSize < commandSet . size ( ) ) {
std : : cout < < " Improved lower bound to " < < commandSet . size ( ) < < " after " < < milliseconds < < " ms. " < < std : : endl ;
std : : cout < < " Improved lower bound to " < < currentBound < < " after " < < milliseconds < < " ms. " < < std : : endl ;
lastSize = commandSet . size ( ) ;
} else {
std : : cout < < " Lower bound on label set size is " < < commandSet . size ( ) < < " after " < < milliseconds < < " ms (checked " < < iterations < < " models, " < < zeroProbabilityCount < < " could not reach the target set). " < < std : : endl ;
std : : cout < < " Lower bound on label set size is " < < currentBound < < " after " < < milliseconds < < " ms (checked " < < iterations < < " models, " < < zeroProbabilityCount < < " could not reach the target set). " < < std : : endl ;
timeOfLastMessage = std : : chrono : : high_resolution_clock : : now ( ) ;
}
}
@ -1863,7 +1833,7 @@ namespace storm {
std : : cout < < " * number of models that could not reach a target state: " < < zeroProbabilityCount < < " ( " < < 100 * static_cast < double > ( zeroProbabilityCount ) / iterations < < " %) " < < std : : endl < < std : : endl ;
}
return commandSe t;
return resul t;
# else
throw storm : : exceptions : : NotImplementedException ( ) < < " This functionality is unavailable since storm has been compiled without support for Z3. " ;
# endif
@ -1953,28 +1923,47 @@ namespace storm {
}
static boost : : container : : flat_set < uint_fast64_t > computeCounterexampleLabelSet ( Environment const & env , storm : : storage : : SymbolicModelDescription const & symbolicModel , storm : : models : : sparse : : Model < T > const & model , std : : shared_ptr < storm : : logic : : Formula const > const & formula , boost : : container : : flat_set < uint_fast64_t > const & dontCareLabels = boost : : container : : flat_set < uint_fast64_t > ( ) , Options const & options = Options ( true ) ) {
static std : : vector < boost : : container : : flat_set < uint_fast64_t > > computeCounterexampleLabelSet ( Environment const & env , storm : : storage : : SymbolicModelDescription const & symbolicModel , storm : : models : : sparse : : Model < T > const & model , std : : shared_ptr < storm : : logic : : Formula const > const & formula , boost : : container : : flat_set < uint_fast64_t > const & dontCareLabels = boost : : container : : flat_set < uint_fast64_t > ( ) , Options const & options = Options ( true ) ) {
STORM_LOG_THROW ( model . isOfType ( storm : : models : : ModelType : : Dtmc ) | | model . isOfType ( storm : : models : : ModelType : : Mdp ) , storm : : exceptions : : NotSupportedException , " MaxSAT-based counterexample generation is supported only for discrete-time models. " ) ;
if ( ! options . silent ) {
std : : cout < < std : : endl < < " Generating minimal label 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 ( ) ;
STORM_LOG_THROW ( probabilityOperator . hasBound ( ) , storm : : exceptions : : InvalidPropertyException , " Counterexample generation only supports bounded formulas. " ) ;
STORM_LOG_THROW ( probabilityOperator . getSubformula ( ) . isUntilFormula ( ) | | probabilityOperator . getSubformula ( ) . isEventuallyFormula ( ) , storm : : exceptions : : InvalidPropertyException , " Path formula is required to be of the form 'phi U psi' for counterexample generation. " ) ;
storm : : logic : : ComparisonType comparisonType ;
double threshold ;
boost : : optional < std : : string > rewardName = boost : : none ;
STORM_LOG_THROW ( formula - > isProbabilityOperatorFormula ( ) | | formula - > isRewardOperatorFormula ( ) , storm : : exceptions : : InvalidPropertyException , " Counterexample generation does not support this kind of formula. Expecting a probability operator as the outermost formula element. " ) ;
if ( formula - > isProbabilityOperatorFormula ( ) ) {
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 . getSubformula ( ) . isUntilFormula ( ) | | probabilityOperator . getSubformula ( ) . isEventuallyFormula ( ) , storm : : exceptions : : InvalidPropertyException , " Path formula is required to be of the form 'phi U psi' for counterexample generation. " ) ;
storm : : logic : : ComparisonType comparisonType = probabilityOperator . getComparisonType ( ) ;
bool strictBound = comparisonType = = storm : : logic : : ComparisonType : : Less ;
double threshold = probabilityOperator . getThresholdAs < T > ( ) ;
comparisonType = probabilityOperator . getComparisonType ( ) ;
threshold = probabilityOperator . getThresholdAs < T > ( ) ;
} else {
assert ( formula - > isRewardOperatorFormula ( ) ) ;
storm : : logic : : RewardOperatorFormula const & rewardOperator = formula - > asRewardOperatorFormula ( ) ;
STORM_LOG_THROW ( rewardOperator . hasBound ( ) , storm : : exceptions : : InvalidPropertyException , " Counterexample generation only supports bounded formulas. " ) ;
STORM_LOG_THROW ( rewardOperator . getSubformula ( ) . isEventuallyFormula ( ) , storm : : exceptions : : InvalidPropertyException , " Path formula is required to be of the form 'F phi' for counterexample generation. " ) ;
comparisonType = rewardOperator . getComparisonType ( ) ;
threshold = rewardOperator . getThresholdAs < T > ( ) ;
rewardName = rewardOperator . getRewardModelName ( ) ;
STORM_LOG_THROW ( ! storm : : logic : : isLowerBound ( comparisonType ) , storm : : exceptions : : NotSupportedException , " Lower bounds in counterexamples are only supported for probability formulas. " ) ;
}
bool strictBound = comparisonType = = storm : : logic : : ComparisonType : : Less ;
storm : : logic : : Formula const & subformula = formula - > asOperatorFormula ( ) . getSubformula ( ) ;
storm : : storage : : BitVector phiStates ;
storm : : storage : : BitVector psiStates ;
storm : : modelchecker : : SparsePropositionalModelChecker < storm : : models : : sparse : : Model < T > > modelchecker ( model ) ;
if ( probabilityOperator . getSubformula ( ) . isUntilFormula ( ) ) {
if ( s ubformula. isUntilFormula ( ) ) {
STORM_LOG_THROW ( ! storm : : logic : : isLowerBound ( comparisonType ) , storm : : exceptions : : NotSupportedException , " Lower bounds in counterexamples are only supported for eventually formulas. " ) ;
storm : : logic : : UntilFormula const & untilFormula = probabilityOperator . getSubformula ( ) . asUntilFormula ( ) ;
storm : : logic : : UntilFormula const & untilFormula = s ubformula. asUntilFormula ( ) ;
std : : unique_ptr < storm : : modelchecker : : CheckResult > leftResult = modelchecker . check ( env , untilFormula . getLeftSubformula ( ) ) ;
std : : unique_ptr < storm : : modelchecker : : CheckResult > rightResult = modelchecker . check ( env , untilFormula . getRightSubformula ( ) ) ;
@ -1984,8 +1973,8 @@ namespace storm {
phiStates = leftQualitativeResult . getTruthValuesVector ( ) ;
psiStates = rightQualitativeResult . getTruthValuesVector ( ) ;
} else if ( probabilityOperator . getS ubformula( ) . isEventuallyFormula ( ) ) {
storm : : logic : : EventuallyFormula const & eventuallyFormula = probabilityOperator . getS ubformula( ) . asEventuallyFormula ( ) ;
} else if ( s ubformula. isEventuallyFormula ( ) ) {
storm : : logic : : EventuallyFormula const & eventuallyFormula = s ubformula. asEventuallyFormula ( ) ;
std : : unique_ptr < storm : : modelchecker : : CheckResult > subResult = modelchecker . check ( env , eventuallyFormula . getSubformula ( ) ) ;
@ -2025,28 +2014,36 @@ namespace storm {
/ / Delegate the actual computation work to the function of equal name .
auto startTime = std : : chrono : : high_resolution_clock : : now ( ) ;
auto labelSet = getMinimalLabelSet ( env , symbolicModel , model , phiStates , psiStates , threshold , strictBound , dontCareLabels , options ) ;
auto labelSets = getMinimalLabelSet ( env , symbolicModel , model , phiStates , psiStates , threshold , rewardName , strictBound , dontCareLabels , options ) ;
auto endTime = std : : chrono : : high_resolution_clock : : now ( ) ;
if ( ! options . silent ) {
std : : cout < < std : : endl < < " Computed minimal label set of size " < < labelSet . size ( ) < < " in " < < std : : chrono : : duration_cast < std : : chrono : : milliseconds > ( endTime - startTime ) . count ( ) < < " ms. " < < std : : endl ;
for ( auto const & labelSet : labelSets ) {
std : : cout < < std : : endl < < " Computed minimal label set of size " < < labelSet . size ( ) ;
}
std : : cout < < std : : endl < < " in " < < std : : chrono : : duration_cast < std : : chrono : : milliseconds > ( endTime - startTime ) . count ( ) < < " ms. " < < std : : endl ;
}
/ / Extend the command set properly .
if ( lowerBoundedFormula ) {
extendLabelSetLowerBound ( model , labelSet , phiStates , psiStates , options . silent ) ;
for ( auto & labelSet : labelSets ) {
if ( lowerBoundedFormula ) {
extendLabelSetLowerBound ( model , labelSet , phiStates , psiStates , options . silent ) ;
}
}
return labelSet ;
return labelSets ;
}
static std : : shared_ptr < HighLevelCounterexample > computeCounterexample ( Environment const & env , storm : : storage : : SymbolicModelDescription const & symbolicModel , storm : : models : : sparse : : Model < T > const & model , std : : shared_ptr < storm : : logic : : Formula const > const & formula ) {
# ifdef STORM_HAVE_Z3
auto labelSet = computeCounterexampleLabelSet ( env , symbolicModel , model , formula ) ;
auto labelSets = computeCounterexampleLabelSet ( env , symbolicModel , model , formula ) ;
if ( symbolicModel . isPrismProgram ( ) ) {
return std : : make_shared < HighLevelCounterexample > ( symbolicModel . asPrismProgram ( ) . restrictCommands ( labelSet ) ) ;
return std : : make_shared < HighLevelCounterexample > ( symbolicModel . asPrismProgram ( ) . restrictCommands ( labelSets [ 0 ] ) ) ;
} else {
STORM_LOG_ASSERT ( symbolicModel . isJaniModel ( ) , " Unknown symbolic model description type. " ) ;
return std : : make_shared < HighLevelCounterexample > ( symbolicModel . asJaniModel ( ) . restrictEdges ( labelSet ) ) ;
return std : : make_shared < HighLevelCounterexample > ( symbolicModel . asJaniModel ( ) . restrictEdges ( labelSets [ 0 ] ) ) ;
}
# else
throw storm : : exceptions : : NotImplementedException ( ) < < " This functionality is unavailable since storm has been compiled without support for Z3. " ;
TimQu
7 years ago