Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
GradientDescentInstantiationSearcher.cpp
Go to the documentation of this file.
2
3#include <cmath>
4#include <iostream>
5#include <random>
6
12
13namespace storm {
14namespace derivative {
15
16template<typename FunctionType>
18template<typename FunctionType>
20
21template<typename FunctionType, typename ConstantType>
22ConstantType GradientDescentInstantiationSearcher<FunctionType, ConstantType>::doStep(
24 const std::map<VariableType<FunctionType>, ConstantType>& gradient, uint64_t stepNum) {
25 const ConstantType precisionAsConstant = utility::convertNumber<ConstantType>(this->env.modelTolerance());
27 CoefficientType<FunctionType> const oldPos = position[steppingParameter];
28 ConstantType const oldPosAsConstant = utility::convertNumber<ConstantType>(position[steppingParameter]);
29
30 ConstantType projectedGradient;
32 // Project gradient
33 ConstantType newPlainPosition = oldPosAsConstant + precisionAsConstant * gradient.at(steppingParameter);
34 auto const lower =
35 region ? utility::convertNumber<ConstantType>(region->getLowerBoundary(steppingParameter)) : utility::zero<ConstantType>() + precisionAsConstant;
36 auto const upper =
37 region ? utility::convertNumber<ConstantType>(region->getUpperBoundary(steppingParameter)) : utility::one<ConstantType>() - precisionAsConstant;
38 if (newPlainPosition < lower || newPlainPosition > upper) {
39 projectedGradient = 0;
40 } else {
41 projectedGradient = gradient.at(steppingParameter);
42 }
43 } else if (constraintMethod == GradientDescentConstraintMethod::LOGISTIC_SIGMOID) {
44 // We want the derivative of f(logit(x)), this happens to be exp(x) * f'(logit(x)) / (exp(x) + 1)^2
45 const double expX = std::exp(utility::convertNumber<double>(oldPos));
46 projectedGradient = gradient.at(steppingParameter) * utility::convertNumber<ConstantType>(expX / std::pow(expX + 1, 2));
47 } else if (constraintMethod == GradientDescentConstraintMethod::BARRIER_INFINITY) {
48 if (oldPosAsConstant < precisionAsConstant) {
49 projectedGradient = 1000;
50 } else if (oldPosAsConstant > utility::one<ConstantType>() - precisionAsConstant) {
51 projectedGradient = -1000;
52 } else {
53 projectedGradient = gradient.at(steppingParameter);
54 }
55 } else if (constraintMethod == GradientDescentConstraintMethod::BARRIER_LOGARITHMIC) {
56 // Our barrier is:
57 // log(x) if 0 < x < 0.5
58 // log(1 - x) if 0.5 <= x < 1
59 // -infinity otherwise
60 // The gradient of this is
61 // 1/x, 1/(1-x), +/-infinity respectively
62 if (oldPosAsConstant >= precisionAsConstant && oldPosAsConstant <= utility::one<ConstantType>() - precisionAsConstant) {
63 /* const double mu = (double) parameters.size() / (double) stepNum; */
64 if (oldPosAsConstant * 2 < utility::one<ConstantType>()) {
65 projectedGradient = gradient.at(steppingParameter) + logarithmicBarrierTerm / (oldPosAsConstant - precisionAsConstant);
66 } else {
67 projectedGradient =
68 gradient.at(steppingParameter) - logarithmicBarrierTerm / (utility::one<ConstantType>() - precisionAsConstant - oldPosAsConstant);
69 }
70 } else {
71 if (oldPosAsConstant < precisionAsConstant) {
72 projectedGradient = utility::one<ConstantType>() / logarithmicBarrierTerm;
73 } else if (oldPosAsConstant > utility::one<ConstantType>() - precisionAsConstant) {
74 projectedGradient = -utility::one<ConstantType>() / logarithmicBarrierTerm;
75 }
76 }
77 } else {
78 projectedGradient = gradient.at(steppingParameter);
79 }
80
81 // Compute step based on used gradient descent method
82 ConstantType step;
83 if (Adam* adam = boost::get<Adam>(&gradientDescentType)) {
84 // For this algorihm, see the various sources available on the ADAM algorithm. This implementation should
85 // be correct, as it is compared with a run of keras's ADAM optimizer in the test.
86 adam->decayingStepAverage[steppingParameter] =
87 adam->averageDecay * adam->decayingStepAverage[steppingParameter] + (utility::one<ConstantType>() - adam->averageDecay) * projectedGradient;
88 adam->decayingStepAverageSquared[steppingParameter] = adam->squaredAverageDecay * adam->decayingStepAverageSquared[steppingParameter] +
89 (utility::one<ConstantType>() - adam->squaredAverageDecay) * utility::pow(projectedGradient, 2);
90
91 const ConstantType correctedGradient =
92 adam->decayingStepAverage[steppingParameter] / (utility::one<ConstantType>() - utility::pow(adam->averageDecay, stepNum + 1));
93 const ConstantType correctedSquaredGradient =
94 adam->decayingStepAverageSquared[steppingParameter] / (utility::one<ConstantType>() - utility::pow(adam->squaredAverageDecay, stepNum + 1));
95
96 const ConstantType toSqrt = correctedSquaredGradient;
97 ConstantType sqrtResult = constantTypeSqrt(toSqrt);
98
99 step = (adam->learningRate / (sqrtResult + precisionAsConstant)) * correctedGradient;
100 } else if (RAdam* radam = boost::get<RAdam>(&gradientDescentType)) {
101 // You can compare this with the RAdam paper's "Algorithm 2: Rectified Adam".
102 // The line numbers and comments are matched.
103 // Initializing / Compute Gradient: Already happened.
104 // 2: Compute maximum length of approximated simple moving average
105 const ConstantType maxLengthApproxSMA = 2 / (utility::one<ConstantType>() - radam->squaredAverageDecay) - utility::one<ConstantType>();
106
107 // 5: Update exponential moving 2nd moment
108 radam->decayingStepAverageSquared[steppingParameter] = radam->squaredAverageDecay * radam->decayingStepAverageSquared[steppingParameter] +
109 (utility::one<ConstantType>() - radam->squaredAverageDecay) * utility::pow(projectedGradient, 2);
110 // 6: Update exponential moving 1st moment
111 radam->decayingStepAverage[steppingParameter] =
112 radam->averageDecay * radam->decayingStepAverage[steppingParameter] + (utility::one<ConstantType>() - radam->averageDecay) * projectedGradient;
113 // 7: Compute bias corrected moving average
114 const ConstantType biasCorrectedMovingAverage =
115 radam->decayingStepAverage[steppingParameter] / (utility::one<ConstantType>() - utility::pow(radam->averageDecay, stepNum + 1));
116 const ConstantType squaredAverageDecayPow = utility::pow(radam->squaredAverageDecay, stepNum + 1);
117 // 8: Compute the length of the approximated single moving average
118 const ConstantType lengthApproxSMA =
119 maxLengthApproxSMA -
120 ((2 * (utility::convertNumber<ConstantType>(stepNum) + utility::one<ConstantType>()) * squaredAverageDecayPow) / (1 - squaredAverageDecayPow));
121 // 9: If the variance is tractable, i.e. lengthApproxSMA > 4, then
122 if (lengthApproxSMA > 4) {
123 // 10: Compute adaptive learning rate
124 const ConstantType adaptiveLearningRate =
125 constantTypeSqrt((utility::one<ConstantType>() - squaredAverageDecayPow) / radam->decayingStepAverageSquared[steppingParameter]);
126 // 11: Compute the variance rectification term
127 const ConstantType varianceRectification =
128 constantTypeSqrt(((lengthApproxSMA - 4) / (maxLengthApproxSMA - 4)) * ((lengthApproxSMA - 2) / (maxLengthApproxSMA - 2)) *
129 ((maxLengthApproxSMA) / (lengthApproxSMA)));
130 // 12: Update parameters with adaptive momentum
131 step = radam->learningRate * varianceRectification * biasCorrectedMovingAverage * adaptiveLearningRate;
132 } else {
133 // 14: Update parameters with un-adapted momentum
134 step = radam->learningRate * biasCorrectedMovingAverage;
135 }
136 } else if (RmsProp* rmsProp = boost::get<RmsProp>(&gradientDescentType)) {
137 rmsProp->rootMeanSquare[steppingParameter] = rmsProp->averageDecay * rmsProp->rootMeanSquare[steppingParameter] +
138 (utility::one<ConstantType>() - rmsProp->averageDecay) * projectedGradient * projectedGradient;
139
140 const ConstantType toSqrt = rmsProp->rootMeanSquare[steppingParameter] + precisionAsConstant;
141 ConstantType sqrtResult = constantTypeSqrt(toSqrt);
142
143 step = (rmsProp->learningRate / sqrtResult) * projectedGradient;
144 } else if (Plain* plain = boost::get<Plain>(&gradientDescentType)) {
145 if (useSignsOnly) {
146 if (projectedGradient < utility::zero<ConstantType>()) {
147 step = -plain->learningRate;
148 } else if (projectedGradient > utility::zero<ConstantType>()) {
149 step = plain->learningRate;
150 } else {
152 }
153 } else {
154 step = plain->learningRate * projectedGradient;
155 }
156 } else if (Momentum* momentum = boost::get<Momentum>(&gradientDescentType)) {
157 if (useSignsOnly) {
158 if (projectedGradient < utility::zero<ConstantType>()) {
159 step = -momentum->learningRate;
160 } else if (projectedGradient > utility::zero<ConstantType>()) {
161 step = momentum->learningRate;
162 } else {
164 }
165 } else {
166 step = momentum->learningRate * projectedGradient;
167 }
168 step += momentum->momentumTerm * momentum->pastStep.at(steppingParameter);
169 momentum->pastStep[steppingParameter] = step;
170 } else if (Nesterov* nesterov = boost::get<Nesterov>(&gradientDescentType)) {
171 if (useSignsOnly) {
172 if (projectedGradient < utility::zero<ConstantType>()) {
173 step = -nesterov->learningRate;
174 } else if (projectedGradient > utility::zero<ConstantType>()) {
175 step = nesterov->learningRate;
176 } else {
178 }
179 } else {
180 step = nesterov->learningRate * projectedGradient;
181 }
182 step += nesterov->momentumTerm * nesterov->pastStep.at(steppingParameter);
183 nesterov->pastStep[steppingParameter] = step;
184 } else {
185 STORM_LOG_ERROR("GradientDescentType was not a known one");
186 }
187
189 const CoefficientType<FunctionType> newPos = position[steppingParameter] + convertedStep;
190 position[steppingParameter] = newPos;
191 // Map parameter back to region
193 auto const lower = region ? region->getLowerBoundary(steppingParameter) : utility::zero<CoefficientType<FunctionType>>() + precision;
194 auto const upper = region ? region->getUpperBoundary(steppingParameter) : utility::one<CoefficientType<FunctionType>>() - precision;
195
196 position[steppingParameter] = utility::max(lower, position[steppingParameter]);
197 position[steppingParameter] = utility::min(upper, position[steppingParameter]);
198 }
199 return utility::abs<ConstantType>(oldPosAsConstant - utility::convertNumber<ConstantType>(position[steppingParameter]));
200}
201
202template<typename FunctionType, typename ConstantType>
204GradientDescentInstantiationSearcher<FunctionType, ConstantType>::stochasticGradientDescent(
206 uint_fast64_t initialStateModel = model.getStates("init").getNextSetIndex(0);
207
208 ExtendedConstantType currentValue;
209 switch (this->synthesisTask->getBound().comparisonType) {
213 break;
217 break;
218 }
219
220 // We count the number of iterations where the value changes less than the threshold, and terminate if it is large enough.
221 uint64_t tinyChangeIterations = 0;
222
223 std::map<VariableType<FunctionType>, ConstantType> deltaVector;
224
225 std::vector<VariableType<FunctionType>> parameterEnumeration;
226 for (auto parameter : this->parameters) {
227 parameterEnumeration.push_back(parameter);
228 }
229
230 utility::Stopwatch printUpdateStopwatch;
231 printUpdateStopwatch.start();
232
233 // The index to keep track of what parameter(s) to consider next.
234 // The "mini-batch", so the parameters to consider, are parameterNum..parameterNum+miniBatchSize-1
235 uint_fast64_t parameterNum = 0;
236 for (uint_fast64_t stepNum = 0; true; ++stepNum) {
237 if (printUpdateStopwatch.getTimeInSeconds() >= 15) {
238 printUpdateStopwatch.restart();
239 STORM_LOG_PROGRESS("Currently at " << currentValue << "\n");
240 }
241
242 std::vector<VariableType<FunctionType>> miniBatch;
243 for (uint_fast64_t i = parameterNum; i < std::min((uint_fast64_t)parameterEnumeration.size(), parameterNum + miniBatchSize); i++) {
244 miniBatch.push_back(parameterEnumeration[i]);
245 }
246
247 ExtendedConstantType oldValue = currentValue;
249
250 // If nesterov is enabled, we need to compute the gradient on the predicted position
251 std::map<VariableType<FunctionType>, CoefficientType<FunctionType>> nesterovPredictedPosition(position);
252 if (Nesterov* nesterov = boost::get<Nesterov>(&gradientDescentType)) {
254 for (auto const& parameter : miniBatch) {
255 ConstantType const addedTerm = nesterov->momentumTerm * nesterov->pastStep[parameter];
256 nesterovPredictedPosition[parameter] += storm::utility::convertNumber<CoefficientType<FunctionType>>(addedTerm);
257 nesterovPredictedPosition[parameter] = utility::max(precision, nesterovPredictedPosition[parameter]);
258 nesterovPredictedPosition[parameter] = utility::min(upperBound, nesterovPredictedPosition[parameter]);
259 }
260 }
262 // Apply sigmoid function
263 for (auto const& parameter : parameters) {
264 nesterovPredictedPosition[parameter] =
267 utility::convertNumber<CoefficientType<FunctionType>>(std::exp(-utility::convertNumber<double>(nesterovPredictedPosition[parameter]))));
268 }
269 }
270
271 // Compute the value of our position and terminate if it satisfies the bound or is
272 // zero or one when computing probabilities. The "valueVector" (just the probability/expected
273 // reward for eventually reaching the target from every state) is also used for computing
274 // the gradient later. We only need one computation of the "valueVector" per mini-batch.
275 //
276 // If nesterov is activated, we need to do this twice. First, to check the value of the current position.
277 // Second, to compute the valueVector at the nesterovPredictedPosition.
278 // If nesterov is deactivated, then nesterovPredictedPosition == position.
279
280 // Are we at a stochastic (in bounds) position?
281 bool stochasticPosition = true;
282 for (auto const& parameter : parameters) {
283 if (nesterovPredictedPosition[parameter] < 0 + precision || nesterovPredictedPosition[parameter] > 1 - precision) {
284 stochasticPosition = false;
285 break;
286 }
287 }
288
289 bool computeValue = true;
291 if (!stochasticPosition) {
292 computeValue = false;
293 }
294 }
295
296 if (computeValue) {
297 std::unique_ptr<storm::modelchecker::CheckResult> intermediateResult = instantiationModelChecker->check(env, nesterovPredictedPosition);
298 std::vector<ConstantType> valueVector = intermediateResult->asExplicitQuantitativeCheckResult<ConstantType>().getFiniteValueVector();
299 if (boost::get<Nesterov>(&gradientDescentType)) {
300 std::map<VariableType<FunctionType>, CoefficientType<FunctionType>> modelCheckPosition(position);
302 for (auto const& parameter : parameters) {
303 modelCheckPosition[parameter] =
307 }
308 }
309 std::unique_ptr<storm::modelchecker::CheckResult> terminationResult = instantiationModelChecker->check(env, modelCheckPosition);
310 std::vector<ConstantType> terminationValueVector = terminationResult->asExplicitQuantitativeCheckResult<ConstantType>().getFiniteValueVector();
311 currentValue = terminationValueVector[initialStateModel];
312 } else {
313 currentValue = valueVector[initialStateModel];
314 }
315
316 if (synthesisTask->getBound().isSatisfied(currentValue) && stochasticPosition) {
317 break;
318 }
319
320 for (auto const& parameter : miniBatch) {
321 auto checkResult = derivativeEvaluationHelper->check(env, nesterovPredictedPosition, parameter, valueVector);
322 ConstantType delta = storm::utility::getFinite(checkResult->getValueVector()[derivativeEvaluationHelper->getInitialState()]);
323 if (synthesisTask->getBound().comparisonType == logic::ComparisonType::Less ||
324 synthesisTask->getBound().comparisonType == logic::ComparisonType::LessEqual) {
325 delta = -delta;
326 }
327 deltaVector[parameter] = delta;
328 }
329 } else {
330 if (synthesisTask->getBound().comparisonType == logic::ComparisonType::Less ||
331 synthesisTask->getBound().comparisonType == logic::ComparisonType::LessEqual) {
333 } else {
335 }
336 }
337
338 // Log position and probability information for later use in visualizing the descent, if wished.
339 if (recordRun) {
340 VisualizationPoint point;
341 point.position = nesterovPredictedPosition;
342 point.value = currentValue;
343 walk.push_back(point);
344 }
345
346 // Perform the step. The actualChange is the change in position the step caused. This is different from the
347 // delta in multiple ways: First, it's multiplied with the learning rate and stuff. Second, if the current value
348 // is at epsilon, and the delta would step out of the constrained which is then corrected, the actualChange is the
349 // change from the last to the current corrected position (so might be zero while the delta is not).
350 for (auto const& parameter : miniBatch) {
351 doStep(parameter, position, deltaVector, stepNum);
352 }
353
354 if (storm::utility::isFinite(oldValue) && storm::utility::isFinite(currentValue) && storm::utility::abs(oldValue - currentValue) < terminationEpsilon) {
355 tinyChangeIterations += miniBatch.size();
356 if (tinyChangeIterations > parameterEnumeration.size()) {
357 break;
358 }
359 } else {
360 tinyChangeIterations = 0;
361 }
362
363 // Consider the next parameter
364 parameterNum = parameterNum + miniBatchSize;
365 if (parameterNum >= parameterEnumeration.size()) {
366 parameterNum = 0;
367 }
368
370 STORM_LOG_WARN("Aborting Gradient Descent, returning non-optimal value.");
371 break;
372 }
373 }
374 return currentValue;
375}
376
377template<typename FunctionType, typename ConstantType>
378std::pair<std::map<VariableType<FunctionType>, CoefficientType<FunctionType>>,
381 STORM_LOG_ASSERT(this->synthesisTask, "Call setup before calling gradientDescent.");
382
383 resetDynamicValues();
384
385 STORM_LOG_ASSERT(this->synthesisTask->isBoundSet(), "Task does not involve a bound.");
386
387 std::map<VariableType<FunctionType>, CoefficientType<FunctionType>> bestInstantiation;
388 // No value has been found yet; the first one we see is the best one so far, whichever direction we optimize in.
389 std::optional<ExtendedConstantType> bestValue;
390
391 std::random_device device;
392 std::default_random_engine engine(device());
393 std::uniform_real_distribution<> dist(0, 1);
394 bool initialGuess = true;
395 std::map<VariableType<FunctionType>, CoefficientType<FunctionType>> point;
396 while (true) {
397 STORM_LOG_PROGRESS("Trying out a new starting point\n");
398 if (initialGuess) {
399 STORM_LOG_PROGRESS("Trying initial guess (p->0.5 for every parameter p or set start point)\n");
400 }
401 // Generate random starting point
402 for (auto const& param : this->parameters) {
403 if (initialGuess) {
404 logarithmicBarrierTerm = utility::convertNumber<ConstantType>(0.1);
405 if (startPoint) {
406 point[param] = (*startPoint)[param];
407 } else {
409 }
410 } else if (!initialGuess && constraintMethod == GradientDescentConstraintMethod::BARRIER_LOGARITHMIC &&
411 logarithmicBarrierTerm > utility::convertNumber<ConstantType>(0.00001)) {
412 // Do nothing
413 } else {
414 logarithmicBarrierTerm = utility::convertNumber<ConstantType>(0.1);
415 point[param] = utility::convertNumber<CoefficientType<FunctionType>>(dist(engine));
416 }
417 }
418 initialGuess = false;
419
420 /* walk.clear(); */
421
422 stochasticWatch.start();
423 STORM_LOG_PROGRESS("Starting at " << point << "\n");
424 ExtendedConstantType prob = stochasticGradientDescent(point);
425 stochasticWatch.stop();
426
427 bool isFoundPointBetter = !bestValue;
428 if (bestValue) {
429 switch (this->synthesisTask->getBound().comparisonType) {
432 isFoundPointBetter = prob > *bestValue;
433 break;
436 isFoundPointBetter = prob < *bestValue;
437 break;
438 }
439 }
440 if (isFoundPointBetter) {
441 bestInstantiation = point;
442 bestValue = prob;
443 }
444
445 if (synthesisTask->getBound().isSatisfied(*bestValue)) {
446 STORM_LOG_PROGRESS("Aborting because the bound is satisfied\n");
447 break;
449 break;
450 } else {
452 logarithmicBarrierTerm = logarithmicBarrierTerm / 10;
453 STORM_LOG_PROGRESS("Smaller term\n" << *bestValue << "\n" << logarithmicBarrierTerm << "\n");
454 continue;
455 }
456 STORM_LOG_PROGRESS("Sorry, couldn't satisfy the bound (yet). Best found value so far: " << *bestValue << "\n");
457 continue;
458 }
459 }
460
462 // Apply sigmoid function
463 for (auto const& parameter : parameters) {
464 bestInstantiation[parameter] =
468 }
469 }
470
471 STORM_LOG_ASSERT(bestValue.has_value(), "Expected at least one evaluated instantiation.");
472 return std::make_pair(bestInstantiation, *bestValue);
473}
474
475template<typename FunctionType, typename ConstantType>
476void GradientDescentInstantiationSearcher<FunctionType, ConstantType>::resetDynamicValues() {
477 if (Adam* adam = boost::get<Adam>(&gradientDescentType)) {
478 for (auto const& parameter : this->parameters) {
479 adam->decayingStepAverage[parameter] = utility::zero<ConstantType>();
480 adam->decayingStepAverageSquared[parameter] = utility::zero<ConstantType>();
481 }
482 } else if (RAdam* radam = boost::get<RAdam>(&gradientDescentType)) {
483 for (auto const& parameter : this->parameters) {
484 radam->decayingStepAverage[parameter] = utility::zero<ConstantType>();
485 radam->decayingStepAverageSquared[parameter] = utility::zero<ConstantType>();
486 }
487 } else if (RmsProp* rmsProp = boost::get<RmsProp>(&gradientDescentType)) {
488 for (auto const& parameter : this->parameters) {
489 rmsProp->rootMeanSquare[parameter] = utility::zero<ConstantType>();
490 }
491 } else if (Momentum* momentum = boost::get<Momentum>(&gradientDescentType)) {
492 for (auto const& parameter : this->parameters) {
493 momentum->pastStep[parameter] = utility::zero<ConstantType>();
494 }
495 } else if (Nesterov* nesterov = boost::get<Nesterov>(&gradientDescentType)) {
496 for (auto const& parameter : this->parameters) {
497 nesterov->pastStep[parameter] = utility::zero<ConstantType>();
498 }
499 }
500}
501
502template<typename FunctionType, typename ConstantType>
504 // This emits a JSON document to stdout for external data collection, not a log message.
505 std::cout << "[";
506 for (auto s = walk.begin(); s != walk.end(); ++s) {
507 std::cout << "{";
508 auto point = s->position;
509 for (auto iter = point.begin(); iter != point.end(); ++iter) {
510 std::cout << "\"" << iter->first.name() << "\"";
511 std::cout << ":" << utility::convertNumber<double>(iter->second) << ",";
512 }
513 std::cout << "\"value\":" << s->value << "}";
514 if (std::next(s) != walk.end()) {
515 std::cout << ",";
516 }
517 }
518 std::cout << "]\n";
519 // Print value at last step for data collection
520 std::cout << storm::utility::convertNumber<double>(walk.at(walk.size() - 1).value) << "\n";
521}
522
523template<typename FunctionType, typename ConstantType>
524std::vector<typename GradientDescentInstantiationSearcher<FunctionType, ConstantType>::VisualizationPoint>
528
531} // namespace derivative
532} // namespace storm
storm::utility::ExtendedValueType< ConstantType > ExtendedConstantType
std::pair< std::map< typename utility::parametric::VariableType< FunctionType >::type, typename utility::parametric::CoefficientType< FunctionType >::type >, ExtendedConstantType > gradientDescent()
Perform Gradient Descent.
std::vector< VisualizationPoint > getVisualizationWalk()
Get the visualization walk that is recorded if recordRun is set to true in the constructor (false by ...
#define STORM_LOG_WARN(message)
Definition logging.h:35
#define STORM_LOG_PROGRESS(message)
Definition logging.h:49
#define STORM_LOG_ERROR(message)
Definition logging.h:36
#define STORM_LOG_ASSERT(cond, message)
Definition macros.h:9
typename utility::parametric::CoefficientType< FunctionType >::type CoefficientType
typename utility::parametric::VariableType< FunctionType >::type VariableType
bool isTerminate()
Check whether the program should terminate (due to some abort signal).
ValueType max(ValueType const &first, ValueType const &second)
ExtendedValueType< ValueType > positiveInfinity()
bool isFinite(ExtendedNumber< ValueType > const &value)
ExtendedValueType< ValueType > negativeInfinity()
ValueType min(ValueType const &first, ValueType const &second)
ValueType abs(ValueType const &number)
ValueType zero()
Definition constants.cpp:26
ValueType pow(ValueType const &value, int_fast64_t exponent)
ValueType one()
Definition constants.cpp:21
ValueType const & getFinite(ExtendedNumber< ValueType > const &value)
TargetType convertNumber(SourceType const &number)