STORM_LOG_ASSERT(manager,"Mutable expression manager required to define quantile bound variable.");
STORM_LOG_THROW(!manager->hasVariable(variableName),storm::exceptions::WrongFormatException,"Invalid quantile variable name '"<<variableName<<"' in property: variable already exists.");
STORM_LOG_WARN_COND(!dir.is_initialized(),"Optimization direction '"<<dir.get()<<"' for quantile variable "<<variableName<<" is ignored. This information will be derived from the subformula of the quantile.");
STORM_LOG_THROW(boundVariables.size()==1,storm::exceptions::InvalidArgumentException,"Requested unique bound variables. However, there are multiple bound variables defined.");
STORM_LOG_THROW(index<boundVariables.size(),storm::exceptions::InvalidArgumentException,"Requested bound variable with index"<<index<<". However, there are only "<<boundVariables.size()<<" bound variables.");
STORM_LOG_THROW(boundVariables.size()==1,storm::exceptions::InvalidArgumentException,"Requested unique optimization direction of the bound variables. However, there are multiple bound variables defined.");
STORM_LOG_THROW(index<boundVariables.size(),storm::exceptions::InvalidArgumentException,"Requested optimization direction with index"<<index<<". However, there are only "<<boundVariables.size()<<" bound variables.");
STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(),storm::exceptions::InvalidOperationException,"Computing quantiles is only supported for the initial states of a model.");
STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits()==1,storm::exceptions::InvalidOperationException,"Quantiles not supported on models with multiple initial states.");
STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(),storm::exceptions::InvalidOperationException,"Computing quantiles is only supported for models with a single initial states.");
STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(),storm::exceptions::InvalidOperationException,"Computing quantiles is only supported for the initial states of a model.");
STORM_LOG_THROW(this->getModel().getInitialStates().getNumberOfSetBits()==1,storm::exceptions::InvalidOperationException,"Quantiles not supported on models with multiple initial states.");
STORM_LOG_THROW(SingleObjectiveMode,storm::exceptions::NotSupportedException,"Letting lower bounds approach infinity is only supported in single objective mode.");// It most likely also works with multiple objectives with the same shape. However, we haven't checked this yet.
STORM_LOG_THROW(objectives.front().formula->isProbabilityOperatorFormula(),storm::exceptions::NotSupportedException,"Letting lower bounds approach infinity is only supported for probability operator formulas");
STORM_LOG_THROW(probabilityOperatorFormula.getSubformula().isBoundedUntilFormula()&&probabilityOperatorFormula.hasOptimalityType()&&storm::solver::maximize(probabilityOperatorFormula.getOptimalityType()),storm::exceptions::NotSupportedException,"Letting lower bounds approach infinity is only supported for maximizing bounded until probabilities.");
STORM_LOG_THROW(probabilityOperatorFormula.getSubformula().isBoundedUntilFormula(),storm::exceptions::NotSupportedException,"Letting lower bounds approach infinity is only supported for bounded until probabilities.");
STORM_LOG_THROW(!model.isNondeterministicModel()||(probabilityOperatorFormula.hasOptimalityType()&&storm::solver::maximize(probabilityOperatorFormula.getOptimalityType())),storm::exceptions::NotSupportedException,"Letting lower bounds approach infinity is only supported for maximizing bounded until probabilities.");
STORM_LOG_THROW(upperBoundedDimensions.empty()||!probabilityOperatorFormula.getSubformula().asBoundedUntilFormula().hasMultiDimensionalSubformulas(),storm::exceptions::NotSupportedException,"Letting lower bounds approach infinity is only supported if the formula has either only lower bounds or if it has a single goal state.");// This would fail because the upper bounded dimension(s) might be satisfied already. One should erase epoch steps in the epoch model (after applying the goal-unfolding).
STORM_LOG_DEBUG("Setting model for epoch "<<epochManager.toString(epoch));
STORM_LOG_THROW(getProb1Objectives().empty(),storm::exceptions::InvalidOperationException,"The objective "<<objectives[*getProb1Objectives().begin()].formula<<" is satisfied already in the initial state(s). This special case can not be handled by the reward unfolding.");// This case should have been handled 'from the outside'
// Check if we need to update the current epoch class
STORM_LOG_ASSERT(productState<epochSolution.productStateToSolutionVectorMap->size(),"Requested solution at an unexisting product state.");
STORM_LOG_ASSERT((*epochSolution.productStateToSolutionVectorMap)[productState]<epochSolution.solutions.size(),"Requested solution for epoch at a state for which no solution was stored.");
STORM_LOG_ASSERT(getProb1Objectives().empty(),"One of the objectives is already satisfied in the initial state. This special case is not handled.");// This case should have been handled 'from the outside'
STORM_LOG_ASSERT((*epochSolution.productStateToSolutionVectorMap)[productState]<epochSolution.solutions.size(),"Requested solution for epoch at product state "<<productState<<" for which no solution was stored.");
STORM_LOG_THROW(model.getInitialStates()==initialTransitionStates,storm::exceptions::NotSupportedException,"The objective "<<*objectives[objIndex].formula<<" is already satisfied in an initial state. This special case is not supported.");
prob1Objectives.set(objIndex,true);
// Such a situation can not be reduced (easily) to an expected reward computation and thus requires special treatment
STORM_LOG_THROW(quantileVariables.count(quantileVariable)==0,storm::exceptions::NotSupportedException,"Quantile formula considers the same bound variable twice.");
quantileVariables.insert(quantileVariable);
}
STORM_LOG_THROW(quantileFormula.getSubformula().isProbabilityOperatorFormula(),storm::exceptions::NotSupportedException,"Quantile formula needs probability operator inside. The formula "<<quantileFormula<<" is not supported.");
STORM_LOG_THROW(probOpFormula.getBound().comparisonType==storm::logic::ComparisonType::Greater||probOpFormula.getBound().comparisonType==storm::logic::ComparisonType::LessEqual,storm::exceptions::NotSupportedException,"Probability operator inside quantile formula needs to have bound > or <=.");
STORM_LOG_THROW(probOpFormula.hasBound(),storm::exceptions::InvalidOperationException,"Probability operator inside quantile formula needs to have a bound.");
STORM_LOG_THROW(!model.isNondeterministicModel()||probOpFormula.hasOptimalityType(),storm::exceptions::InvalidOperationException,"Probability operator inside quantile formula needs to have an optimality type.");
STORM_LOG_WARN_COND(probOpFormula.getBound().comparisonType==storm::logic::ComparisonType::Greater||probOpFormula.getBound().comparisonType==storm::logic::ComparisonType::LessEqual,"Probability operator inside quantile formula needs to have bound > or <=. The specified comparison type might lead to non-termination.");// This has to do with letting bound variables approach infinity, e.g., Pr>0.7 [F "goal"] holds iff Pr>0.7 [F<=B "goal"] holds for some B.
STORM_LOG_THROW(probOpFormula.getSubformula().isBoundedUntilFormula(),storm::exceptions::NotSupportedException,"Quantile formula needs bounded until probability operator formula as subformula. The formula "<<quantileFormula<<" is not supported.");
// Only > and <= are supported for upper bounds. This is to make sure that Pr>0.7 [F "goal"] holds iff Pr>0.7 [F<=B "goal"] holds for some B.
// Only >= and < are supported for lower bounds. (EC construction..)
// TODO
// Bounds are either constants or variables that are declared in the quantile formula.
// Prop op has optimality type
// No Prmin with lower cost bounds: Ec construction fails. In single obj we would do 1-Prmax[F "nonRewOrNonGoalEC"] but this invalidates other lower/upper cost bounds.
STORM_LOG_THROW(!boundedUntilFormula.hasLowerBound(dim),storm::exceptions::NotSupportedException,"Interval bounds are not supported within quantile formulas.");
STORM_LOG_THROW(!boundedUntilFormula.isUpperBoundStrict(dim),storm::exceptions::NotSupportedException,"Only non-strict upper reward bounds are supported for quantiles.");
STORM_LOG_THROW(!boundedUntilFormula.isLowerBoundStrict(dim),storm::exceptions::NotSupportedException,"Only non-strict lower reward bounds are supported for quantiles.");
STORM_LOG_THROW(boundExpression.isVariable(),storm::exceptions::NotSupportedException,"Non-trivial bound expressions such as '"<<boundExpression<<"' are not supported. Either specify a constant or a quantile variable.");
STORM_LOG_ASSERT(transformations.size()==origBoundedUntil.getDimension(),"Tried to replace the bound of a dimension that is higher than the number of dimensions of the formula.");
STORM_LOG_THROW(false,storm::exceptions::InvalidOperationException,"The bound variable '"<<dimVar.getName()<<"' is not specified within the quantile formula '"<<quantileFormula<<"'.");
STORM_LOG_THROW(false,storm::exceptions::NotSupportedException,"The quantile formula considers "<<getOpenDimensions().getNumberOfSetBits()<<" open dimensions. Only one- or two-dimensional quantiles are supported.");
STORM_LOG_ASSERT(consideredDimensions.isSubsetOf(getOpenDimensions()),"Considered dimensions for a quantile query should be a subset of the set of dimensions without a fixed bound.");
STORM_LOG_THROW(dimensionsAsBitVector.back().getNumberOfSetBits()==1,storm::exceptions::NotSupportedException,"There is not exactly one reward bound referring to quantile variable '"<<dirVar.second.getName()<<"'.");
// When maximizing bounds, the computed single dimensional quantile value is sat for all values of the other bound.
// Increase the computed value so that there is at least one unsat assignment of bounds with B[i] = singleQuantileValues[i]
++singleQuantileValues.back().first;
}
initPoint.push_back(subQueryCostLimit[i]);
++i;
}
// Decrease the value for lower cost bounds to convert >= to >
if(lowerCostBounds[i]){
--singleQuantileValues[i].first;
}
}
std::vector<int64_t>currentEpochValues={(int64_t)singleQuantileValues[0].first,(int64_t)singleQuantileValues[1].first};// signed int is needed to allow lower bounds >-1 (aka >=0).
STORM_LOG_THROW(dimensionsAsBitVector.back().getNumberOfSetBits()==1,storm::exceptions::NotSupportedException,"There is not exactly one reward bound referring to quantile variable '"<<dirVar.second.getName()<<"'.");
// When maximizing, we actually searched for each x-value the smallest y-value that leads to a property violation. Hence, decreasing y by one means property satisfaction
STORM_LOG_THROW(false,storm::exceptions::UnexpectedException,"The entries of the current cost limit candidate do not sum up to the current candidate sum.");
Tim Quatmann
6 years ago
xxxxxxxxxx