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

more explicit instantiations for rational function and some more tests for eigen solver 

Former-commit-id: b97e838b22
tempestpy_adaptions
dehnert 9 years ago
parent
4e14ecb869
commit
2096c54b84
6 changed files with 113 additions and 4 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. 7
      src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
  2. 1
      src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
  3. 1
      src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
  4. 12
      src/storage/SparseMatrix.cpp
  5. 2
      src/utility/solver.cpp
  6. 94
      test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp

7
src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
View File

@ -445,7 +445,7 @@ namespace storm {
}
// Start by decomposing the DTMC into its BSCCs.
storm::storage::StronglyConnectedComponentDecomposition<double> bsccDecomposition(probabilityMatrix, storm::storage::BitVector(probabilityMatrix.getRowCount(), true), false, true);
storm::storage::StronglyConnectedComponentDecomposition<ValueType> bsccDecomposition(probabilityMatrix, storm::storage::BitVector(probabilityMatrix.getRowCount(), true), false, true);
STORM_LOG_DEBUG("Found " << bsccDecomposition.size() << " BSCCs.");
@ -593,7 +593,7 @@ namespace storm {
// At this point, all BSCCs are known to contain exactly one state, which is why we can set all values
// directly (based on whether or not the contained state is a psi state).
if (psiStates.get(*bscc.begin())) {
bsccLra[bsccIndex] = 1;
bsccLra[bsccIndex] = storm::utility::one<ValueType>();
}
}
@ -701,10 +701,11 @@ namespace storm {
template std::vector<double> SparseCtmcCslHelper<double>::computeInstantaneousRewards(storm::storage::SparseMatrix<double> const& rateMatrix, std::vector<double> const& exitRateVector, storm::models::sparse::StandardRewardModel<double> const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
template std::vector<double> SparseCtmcCslHelper<double>::computeCumulativeRewards(storm::storage::SparseMatrix<double> const& rateMatrix, std::vector<double> const& exitRateVector, storm::models::sparse::StandardRewardModel<double> const& rewardModel, double timeBound, storm::utility::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
template std::vector<double> SparseCtmcCslHelper<double>::computeReachabilityRewards(storm::storage::SparseMatrix<double> const& rateMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, std::vector<double> const& exitRateVector, storm::models::sparse::StandardRewardModel<double> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
#ifdef STORM_HAVE_CARL
template std::vector<storm::RationalFunction> SparseCtmcCslHelper<storm::RationalFunction>::computeUntilProbabilitiesElimination(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper<storm::RationalFunction>::computeReachabilityTimesElimination(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative);
template std::vector<storm::RationalFunction> SparseCtmcCslHelper<storm::RationalFunction>::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<storm::RationalFunction> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<storm::RationalFunction> const* exitRateVector, bool qualitative, storm::utility::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
#endif
}
}

1
src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
View File

@ -146,5 +146,6 @@ namespace storm {
}
template class SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>>;
template class SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>>;
}
}

1
src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
View File

@ -401,6 +401,7 @@ namespace storm {
}
template class SparseDtmcPrctlHelper<double>;
template class SparseDtmcPrctlHelper<storm::RationalFunction>;
}
}
}

12
src/storage/SparseMatrix.cpp
View File

@ -1018,6 +1018,11 @@ namespace storm {
typename std::pair<storm::storage::SparseMatrix<RationalFunction>, std::vector<RationalFunction>> SparseMatrix<RationalFunction>::getJacobiDecomposition() const {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This operation is not supported.");
}
template<>
typename std::pair<storm::storage::SparseMatrix<Interval>, std::vector<Interval>> SparseMatrix<Interval>::getJacobiDecomposition() const {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This operation is not supported.");
}
#endif
template<typename ValueType>
@ -1144,6 +1149,11 @@ namespace storm {
}
}
template<>
void SparseMatrix<Interval>::performSuccessiveOverRelaxationStep(Interval omega, std::vector<Interval>& x, std::vector<Interval> const& b) const {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This operation is not supported.");
}
template<typename ValueType>
void SparseMatrix<ValueType>::multiplyVectorWithMatrix(std::vector<value_type> const& vector, std::vector<value_type>& result) const {
const_iterator it = this->begin();
@ -1457,7 +1467,7 @@ namespace storm {
template bool SparseMatrix<int>::isSubmatrixOf(SparseMatrix<storm::storage::sparse::state_type> const& matrix) const;
#ifdef STORM_HAVE_CARL
// Rat Function
// Rat Number
template class MatrixEntry<typename SparseMatrix<RationalNumber>::index_type, RationalNumber>;
template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, RationalNumber> const& entry);
template class SparseMatrixBuilder<RationalNumber>;

2
src/utility/solver.cpp
View File

@ -215,6 +215,8 @@ namespace storm {
template class NativeLinearEquationSolverFactory<double>;
template class MinMaxLinearEquationSolverFactory<double>;
template class GameSolverFactory<double>;
template class EigenLinearEquationSolverFactory<storm::RationalFunction>;
}
}
}

94
test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp
View File

@ -60,6 +60,100 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die) {
EXPECT_NEAR(11.0 / 3.0, quantitativeResult4[0], storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
}
TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalNumber) {
// FIXME: this should use rational numbers not functions.
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>(program).translate();
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
ASSERT_EQ(dtmc->getNumberOfStates(), 13ull);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull);
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>> checker(*dtmc, std::make_unique<storm::utility::solver::EigenLinearEquationSolverFactory<storm::RationalFunction>>());
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
EXPECT_EQ(storm::RationalFunction(1) / storm::RationalFunction(6), quantitativeResult1[0]);
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
EXPECT_EQ(storm::RationalFunction(1) / storm::RationalFunction(6), quantitativeResult2[0]);
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
EXPECT_EQ(storm::RationalFunction(1) / storm::RationalFunction(6), quantitativeResult3[0]);
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
EXPECT_EQ(storm::RationalFunction(11) / storm::RationalFunction(3), quantitativeResult4[0]);
}
TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalFunction) {
// FIXME: this should use rational numbers not functions.
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/parametric_die.pm");
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitPrismModelBuilder<storm::RationalFunction>(program).translate();
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
ASSERT_EQ(dtmc->getNumberOfStates(), 13ull);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull);
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>> checker(*dtmc, std::make_unique<storm::utility::solver::EigenLinearEquationSolverFactory<storm::RationalFunction>>());
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
std::cout << quantitativeResult1 << std::endl;
// EXPECT_EQ(storm::RationalFunction(1) / storm::RationalFunction(6), quantitativeResult1[0]);
//
// formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
//
// result = checker.check(*formula);
// storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
//
// EXPECT_EQ(storm::RationalFunction(1) / storm::RationalFunction(6), quantitativeResult2[0]);
//
// formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
//
// result = checker.check(*formula);
// storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
//
// EXPECT_EQ(storm::RationalFunction(1) / storm::RationalFunction(6), quantitativeResult3[0]);
//
// formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
//
// result = checker.check(*formula);
// storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
//
// EXPECT_EQ(storm::RationalFunction(11) / storm::RationalFunction(3), quantitativeResult4[0]);
}
TEST(EigenDtmcPrctlModelCheckerTest, Crowds) {
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.lab", "", "");

Write Preview
Loading…
Cancel
Save