Combined CTMC Analysis

[ifndefJOSH]

In stamina::checker::StaminaModelChecker, two transient analysis are being performed, one for $P_{min}$ and one for $P_{max}$. If we have already performed the model-checking, we should have all of the state probabilities for a given time-bound. Therefore, we should be able to only perform checking once, and then find the values as follows, given $s_a$ the absorbing state, and $p(s_a)$ the (normalized) reachability of $s_a$. (Note, this is not $\pi(s_a)$!)

Note that $P_{min}$ is normally calculated as follows:

$$P_{min} = P_{=?}[\psi\ U^I\ \phi\ \wedge\ \neg\ \hat{s}]$$
but it should be able to be calculated as follows:

$$ P_{min} = P_{max} - p(s_a) $$

So we can use the typical $P_{max}$ computation:

$$
P_{max} = P_{=?}[\psi\ U^I\ \phi\ \vee\ \hat{s}]
$$
And then get $p(s_a)$ from the CheckResult (not sure how yet)

This occurs at StaminaModelChecker.cpp:214

auto result_lower = checker->check(
	// env,
	storm::modelchecker::CheckTask<>(*(propMin.getRawFormula()), true)
);
min_results->result = result_lower->asExplicitQuantitativeCheckResult<double>()[*model->getInitialStates().begin()];
auto result_upper = checker->check(
	// env,
	storm::modelchecker::CheckTask<>(*(propMax.getRawFormula()), true)
);
max_results->result = result_upper->asExplicitQuantitativeCheckResult<double>()[*model->getInitialStates().begin()];

This could be changed to something like

auto result_upper = checker->check(
	// env,
	storm::modelchecker::CheckTask<>(*(propMax.getRawFormula()), true)
);
max_results->result = result_upper->asExplicitQuantitativeCheckResult<double>()[*model->getInitialStates().begin()];
min_results->result = max_results->result - /* Wherever to get p(s_a) */;

I tried result_upper->asExplicitQuantitativeCheckResult<double>()[0], as well as a number of other things, (since the absorbing state index is 0), but this didn't work.

[ifndefJOSH]

This optimization may already be happening in Storm though. checker->check may not re-build the normalized matrix or re-do the power method/gauss method/jacobi method/whatever, so this may be unnecessary.