sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Removed a lot of debug output. 

Former-commit-id: cbe28c66ae
tempestpy_adaptions
dehnert 10 years ago
parent
7fa6b568b4
commit
ccc60ef145
2 changed files with 1 additions and 52 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 46
      src/modelchecker/csl/SparseCtmcCslModelChecker.cpp
  2. 7
      src/utility/numerical.h

46
src/modelchecker/csl/SparseCtmcCslModelChecker.cpp
View File

@ -50,8 +50,6 @@ namespace storm {
upperBound = pathFormula.getUpperBound();
}
std::cout << "initial: " << this->getModel().getInitialStates() << std::endl;
std::unique_ptr<CheckResult> result = std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeBoundedUntilProbabilitiesHelper(leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), this->getModel().getExitRateVector(), qualitative, lowerBound, upperBound)));
return result;
@ -107,7 +105,6 @@ namespace storm {
storm::utility::vector::setVectorValues<ValueType>(result, psiStates, storm::utility::one<ValueType>());
} else {
if (comparator.isZero(lowerBound)) {
std::cout << "case [0, t]" << std::endl;
// In this case, the interval is of the form [0, t].
// Note that this excludes [0, inf] since this is untimed reachability and we considered this case earlier.
@ -121,18 +118,14 @@ namespace storm {
// Compute the uniformized matrix.
storm::storage::SparseMatrix<ValueType> uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), statesWithProbabilityGreater0, psiStates, uniformizationRate, exitRates);
// storm::storage::SparseMatrix<ValueType> uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), storm::storage::BitVector(this->getModel().getNumberOfStates(), true), psiStates, uniformizationRate, exitRates);
// Finally compute the transient probabilities.
std::vector<ValueType> psiStateValues(statesWithProbabilityGreater0.getNumberOfSetBits(), storm::utility::zero<ValueType>());
storm::utility::vector::setVectorValues(psiStateValues, psiStates % statesWithProbabilityGreater0, storm::utility::one<ValueType>());
// storm::utility::vector::setVectorValues(psiStateValues, psiStates, storm::utility::one<ValueType>());
std::vector<ValueType> subresult = this->computeTransientProbabilities(uniformizedMatrix, uniformizationRate * upperBound, psiStateValues, *this->linearEquationSolver);
storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0, subresult);
// result = this->computeTransientProbabilities(uniformizedMatrix, uniformizationRate * upperBound, psiStateValues, *this->linearEquationSolver);
} else if (comparator.isInfinity(upperBound)) {
std::cout << "case [t, inf]" << std::endl;
// In this case, the interval is of the form [t, inf] with t != 0.
// Start by computing the (unbounded) reachability probabilities of reaching psi states while
@ -159,7 +152,6 @@ namespace storm {
result = this->computeTransientProbabilities(uniformizedMatrix, uniformizationRate * lowerBound, result, *this->linearEquationSolver);
} else {
// In this case, the interval is of the form [t, t'] with t != 0 and t' != inf.
std::cout << "case [t, t']" << std::endl;
// Find the maximal rate of all 'maybe' states to take it as the uniformization rate.
ValueType uniformizationRate = 0;
@ -199,11 +191,6 @@ namespace storm {
}
}
std::cout << "final result" << std::endl;
for (uint_fast64_t index = 0; index < result.size(); ++index) {
std::cout << "result[" << index << "] = " << result[index] << std::endl;
}
return result;
}
@ -249,16 +236,6 @@ namespace storm {
element /= std::get<2>(foxGlynnResult);
}
std::cout << "fox glynn:" << std::endl;
std::cout << "left: " << std::get<0>(foxGlynnResult) << std::endl;
std::cout << "right: " << std::get<1>(foxGlynnResult) << std::endl;
std::cout << "total: " << std::get<2>(foxGlynnResult) << std::endl;
int i = 0;
for (auto const& weight : std::get<3>(foxGlynnResult)) {
std::cout << "weight[" << i << "]: " << weight << std::endl;
++i;
}
// Initialize result.
std::vector<ValueType> result;
uint_fast64_t startingIteration = std::get<0>(foxGlynnResult);
@ -271,41 +248,20 @@ namespace storm {
}
std::vector<ValueType> multiplicationResult(result.size());
std::cout << "starting vector:" << std::endl;
for (int i = 0; i < result.size(); ++i) {
std::cout << i << ": " << result[i] << std::endl;
}
// Perform the matrix-vector multiplications (without adding).
if (std::get<0>(foxGlynnResult) > 1) {
linearEquationSolver.performMatrixVectorMultiplication(uniformizedMatrix, values, nullptr, std::get<0>(foxGlynnResult) - 1, &multiplicationResult);
}
std::cout << "vector after initial mult phase:" << std::endl;
for (int i = 0; i < result.size(); ++i) {
std::cout << i << ": " << result[i] << std::endl;
}
// For the indices that fall in between the truncation points, we need to perform the matrix-vector
// multiplication, scale and add the result.
ValueType weight = 0;
std::function<ValueType(ValueType const&, ValueType const&)> addAndScale = [&weight] (ValueType const& a, ValueType const& b) { std::cout << "computing " << a << " + " << weight << " * " << b << " = " << (a + weight * b) << std::endl; return a + weight * b; };
std::function<ValueType(ValueType const&, ValueType const&)> addAndScale = [&weight] (ValueType const& a, ValueType const& b) { return a + weight * b; };
for (uint_fast64_t index = startingIteration; index <= std::get<1>(foxGlynnResult); ++index) {
linearEquationSolver.performMatrixVectorMultiplication(uniformizedMatrix, values, nullptr, 1, &multiplicationResult);
weight = std::get<3>(foxGlynnResult)[index - std::get<0>(foxGlynnResult)];
std::cout << "setting weight for index " << index << "(" << (index - std::get<0>(foxGlynnResult)) << ") " << " to " << std::get<3>(foxGlynnResult)[index - std::get<0>(foxGlynnResult)] << std::endl;
storm::utility::vector::applyPointwiseInPlace(result, values, addAndScale);
std::cout << "values after index: " << index << std::endl;
for (int i = 0; i < values.size(); ++i) {
std::cout << i << ": " << values[i] << std::endl;
}
std::cout << "result after index: " << index << std::endl;
for (int i = 0; i < result.size(); ++i) {
std::cout << i << ": " << result[i] << std::endl;
}
}
return result;

7
src/utility/numerical.h
View File

@ -14,8 +14,6 @@ namespace storm {
storm::utility::ConstantsComparator<ValueType> comparator;
STORM_LOG_THROW(!comparator.isZero(lambda), storm::exceptions::InvalidArgumentException, "Error in Fox-Glynn algorithm: lambda must not be zero.");
std::cout << "calling Fox-Glynn with " << lambda << ", " << overflow << ", " << underflow << ", " << accuracy << std::endl;
// This code is a modified version of the one in PRISM. According to their implementation, for lambda
// smaller than 400, we compute the result using the naive method.
if (lambda < 400) {
@ -79,8 +77,6 @@ namespace storm {
dkl = 1.0 / (1 - std::exp(-(2.0 / 9.0)*(k * sqrt2 * sqrtLambda + 1.5)));
}
std::cout << "k for upper: " << k << std::endl;
// Left hand side of the equation in Corollary 1.
rightTruncationPoint = static_cast<uint_fast64_t>(std::ceil((m + k * sqrt2 * sqrtLambda + 1.5)));
@ -89,11 +85,8 @@ namespace storm {
// Right hand side of the equation in Corollary 2.
while ((accuracy / 2.0) < ((bLambda * std::exp(-(k*k / 2.0))) / (k * sqrt2 * sqrtpi))) {
std::cout << "k=" << k << " produces: " << ((bLambda * std::exp(-(k*k / 2.0))) / (k * sqrt2 * sqrtpi)) << std::endl;
++k;
}
std::cout << "k=" << k << " produces: " << ((bLambda * std::exp(-(k*k / 2.0))) / (k * sqrt2 * sqrtpi)) << std::endl;
std::cout << "k for lower: " << k << std::endl;
// Left hand side of the equation in Corollary 2.
leftTruncationPoint = static_cast<uint_fast64_t>(std::max(std::trunc(m - k * sqrtLambda - 1.5), storm::utility::zero<ValueType>()));

Write Preview
Loading…
Cancel
Save