STORM_LOG_THROW(timeInstant>=0,storm::exceptions::InvalidJaniException,"Only non-negative time-instants are allowed");
if(!accTime&&!accSteps){
@ -284,7 +284,7 @@ namespace storm {
STORM_LOG_THROW(false,storm::exceptions::NotSupportedException,"Instant/Cumul. Reward for reward constraints not supported currently.");
}
//STORM_LOG_THROW(!accTime && !accSteps, storm::exceptions::NotSupportedException, "storm only allows accumulation if a step- or time-bound is given.");
//STORM_LOG_THROW(!accTime && !accSteps, storm::exceptions::NotSupportedException, "Storm only allows accumulation if a step- or time-bound is given.");
STORM_LOG_THROW(pi.hasUpperBound(),storm::exceptions::NotSupportedException,"storm only supports step-bounded until with an upper bound");
STORM_LOG_THROW(pi.hasUpperBound(),storm::exceptions::NotSupportedException,"Storm only supports step-bounded until with an upper bound");
if(pi.hasLowerBound()){
STORM_LOG_THROW(pi.lowerBound.evaluateAsInt()==0,storm::exceptions::NotSupportedException,"storm only supports step-bounded until without a (non-trivial) lower-bound");
STORM_LOG_THROW(pi.lowerBound.evaluateAsInt()==0,storm::exceptions::NotSupportedException,"Storm only supports step-bounded until without a (non-trivial) lower-bound");
STORM_LOG_THROW(false,storm::exceptions::NotSupportedException,"storm is compiled without MathSAT support.");
STORM_LOG_THROW(false,storm::exceptions::NotSupportedException,"Storm is compiled without MathSAT support.");
#endif
}
@ -162,7 +162,7 @@ namespace storm {
}
returnthis->lastResult;
#else
STORM_LOG_THROW(false,storm::exceptions::NotSupportedException,"storm is compiled without MathSAT support.");
STORM_LOG_THROW(false,storm::exceptions::NotSupportedException,"Storm is compiled without MathSAT support.");
#endif
}
@ -190,7 +190,7 @@ namespace storm {
}
returnthis->lastResult;
#else
STORM_LOG_THROW(false,storm::exceptions::NotSupportedException,"storm is compiled without MathSAT support.");
STORM_LOG_THROW(false,storm::exceptions::NotSupportedException,"Storm is compiled without MathSAT support.");
#endif
}
@ -219,7 +219,7 @@ namespace storm {
}
returnthis->lastResult;
#else
STORM_LOG_THROW(false,storm::exceptions::NotSupportedException,"storm is compiled without MathSAT support.");
STORM_LOG_THROW(false,storm::exceptions::NotSupportedException,"Storm is compiled without MathSAT support.");
#endif
}
#endif
@ -230,7 +230,7 @@ namespace storm {
STORM_LOG_THROW(this->lastResult==SmtSolver::CheckResult::Sat,storm::exceptions::InvalidStateException,"Unable to create model for formula that was not determined to be satisfiable.");
returnthis->convertMathsatModelToValuation();
#else
STORM_LOG_THROW(false,storm::exceptions::NotSupportedException,"storm is compiled without MathSAT support.");
STORM_LOG_THROW(false,storm::exceptions::NotSupportedException,"Storm is compiled without MathSAT support.");
#endif
}
@ -239,7 +239,7 @@ namespace storm {
STORM_LOG_THROW(this->lastResult==SmtSolver::CheckResult::Sat,storm::exceptions::InvalidStateException,"Unable to create model for formula that was not determined to be satisfiable.");
STORM_LOG_THROW(false,storm::exceptions::NotSupportedException,"storm is compiled without Z3 support.");
STORM_LOG_THROW(false,storm::exceptions::NotSupportedException,"Storm is compiled without Z3 support.");
#endif
}
@ -125,7 +125,7 @@ namespace storm {
}
returnthis->lastResult;
#else
STORM_LOG_THROW(false,storm::exceptions::NotSupportedException,"storm is compiled without Z3 support.");
STORM_LOG_THROW(false,storm::exceptions::NotSupportedException,"Storm is compiled without Z3 support.");
#endif
}
@ -152,7 +152,7 @@ namespace storm {
}
returnthis->lastResult;
#else
STORM_LOG_THROW(false,storm::exceptions::NotSupportedException,"storm is compiled without Z3 support.");
STORM_LOG_THROW(false,storm::exceptions::NotSupportedException,"Storm is compiled without Z3 support.");
#endif
}
@ -180,7 +180,7 @@ namespace storm {
}
returnthis->lastResult;
#else
STORM_LOG_THROW(false,storm::exceptions::NotSupportedException,"storm is compiled without Z3 support.");
STORM_LOG_THROW(false,storm::exceptions::NotSupportedException,"Storm is compiled without Z3 support.");
#endif
}
#endif
@ -190,7 +190,7 @@ namespace storm {
STORM_LOG_THROW(this->lastResult==SmtSolver::CheckResult::Sat,storm::exceptions::InvalidStateException,"Unable to create model for formula that was not determined to be satisfiable.");
STORM_LOG_THROW(false,storm::exceptions::NotSupportedException,"storm is compiled without Z3 support.");
STORM_LOG_THROW(false,storm::exceptions::NotSupportedException,"Storm is compiled without Z3 support.");
#endif
}
@ -199,7 +199,7 @@ namespace storm {
STORM_LOG_THROW(this->lastResult==SmtSolver::CheckResult::Sat,storm::exceptions::InvalidStateException,"Unable to create model for formula that was not determined to be satisfiable.");