std::cout<<std::endl<<"Extended command for lower bounded property to size "<<commandSet.size()<<" in "<<std::chrono::duration_cast<std::chrono::milliseconds>(endTime-startTime).count()<<"ms."<<std::endl;
std::cout<<std::endl<<"Extended command for lower bounded property to size "<<commandSet.size()<<" in "<<std::chrono::duration_cast<std::chrono::milliseconds>(endTime-startTime).count()<<"ms."<<std::endl;
std::cout<<std::endl<<"Generating minimal label counterexample for formula "<<*formula<<std::endl;
std::cout<<std::endl<<"Generating minimal label counterexample for formula "<<*formula<<std::endl;
STORM_LOG_THROW(formula->isProbabilityOperatorFormula(),storm::exceptions::InvalidPropertyException,"Counterexample generation does not support this kind of formula. Expecting a probability operator as the outermost formula element.");
STORM_LOG_THROW(formula->isProbabilityOperatorFormula(),storm::exceptions::InvalidPropertyException,"Counterexample generation does not support this kind of formula. Expecting a probability operator as the outermost formula element.");
STORM_LOG_THROW(!storm::logic::isLowerBound(comparisonType),storm::exceptions::NotSupportedException,"Lower bounds in counterexamples are only supported for eventually formulas.");
STORM_LOG_THROW(!storm::logic::isLowerBound(comparisonType),storm::exceptions::NotSupportedException,"Lower bounds in counterexamples are only supported for eventually formulas.");
std::cout<<std::endl<<"Computed minimal command set of size "<<commandSet.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 "<<commandSet.size()<<" in "<<std::chrono::duration_cast<std::chrono::milliseconds>(endTime-startTime).count()<<"ms."<<std::endl;
STORM_LOG_THROW(!pathFormula.hasLowerBound()&&pathFormula.hasUpperBound(),storm::exceptions::InvalidPropertyException,"Formula needs to have single upper time bound.");
STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(),storm::exceptions::InvalidPropertyException,"Formula needs to have discrete upper time bound.");
STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(),storm::exceptions::InvalidOperationException,"Checking non-trivial bounded until probabilities can only be computed for the initial states of the model.");
STORM_LOG_THROW(!pathFormula.hasLowerBound()&&pathFormula.hasUpperBound(),storm::exceptions::InvalidPropertyException,"Formula needs to have single upper time bound.");
STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(),storm::exceptions::InvalidPropertyException,"Formula needs to have discrete upper time bound.");
STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(),storm::exceptions::InvalidOperationException,"Checking non-trivial bounded until probabilities can only be computed for the initial states of the model.");
STORM_LOG_THROW(objectiveFormula->hasOptimalityType(),storm::exceptions::InvalidPropertyException,"Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
// lower bounded until formulas with non-trivial left hand side are excluded as this would require some additional effort (in particular the ProductModel::transformMemoryState method).
// lower bounded until formulas with non-trivial left hand side are excluded as this would require some additional effort (in particular the ProductModel::transformMemoryState method).
STORM_LOG_THROW(dimension.isUpperBounded||subformula.getLeftSubformula(dim).isTrueFormula(),storm::exceptions::NotSupportedException,"Lower bounded until formulas are only supported by this method if the left subformula is 'true'. Got "<<subformula<<" instead.");
STORM_LOG_THROW(dimension.isUpperBounded||subformula.getLeftSubformula(dim).isTrueFormula(),storm::exceptions::NotSupportedException,"Lower bounded until formulas are only supported by this method if the left subformula is 'true'. Got "<<subformula<<" instead.");
// We assume that there is no end component in which objective reward is earned
// We assume that there is no end component in which objective reward is earned
STORM_LOG_ASSERT(!storm::utility::graph::checkIfECWithChoiceExists(epochModel.epochMatrix,epochModel.epochMatrix.transpose(true),allProductStates,~zeroObjRewardChoices&~stepChoices),"There is a scheduler that yields infinite reward for one objective. This case should be excluded");
STORM_LOG_ASSERT(!storm::utility::graph::checkIfECWithChoiceExists(epochModel.epochMatrix,epochModel.epochMatrix.transpose(true),allProductStates,~zeroObjRewardChoices&~stepChoices),"There is a scheduler that yields infinite reward for one objective. This case should be excluded");
STORM_LOG_ASSERT(ecElimResult.oldToNewStateMapping[productState]<epochModel.epochMatrix.getRowGroupCount(),"Selected product state does not exist in the epoch model.");
STORM_LOG_ASSERT(productToEpochModelStateMapping[productState]<epochModel.epochMatrix.getRowGroupCount(),"Selected product state does not exist in the epoch model.");
xxxxxxxxxx