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

Tests for DTMC LRA and some bugfixes. All tests pass. 

Former-commit-id: 589db6c2b3
main
David_Korzeniewski 11 years ago
parent
5acaed6048
commit
8e688f71ff
2 changed files with 152 additions and 5 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 12
      src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
  2. 145
      test/functional/modelchecker/SparseDtmcPrctlModelCheckerTest.cpp

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

@ -321,6 +321,8 @@ namespace storm {
// Get some data members for convenience. // Get some data members for convenience.
typename storm::storage::SparseMatrix<ValueType> const& transitionMatrix = this->getModel().getTransitionMatrix(); typename storm::storage::SparseMatrix<ValueType> const& transitionMatrix = this->getModel().getTransitionMatrix();
ValueType one = storm::utility::one<ValueType>();
ValueType zero = storm::utility::zero<ValueType>();
// First we check which states are in BSCCs. We use this later to speed up reachability analysis // First we check which states are in BSCCs. We use this later to speed up reachability analysis
storm::storage::BitVector statesInBsccs(numOfStates); storm::storage::BitVector statesInBsccs(numOfStates);
@ -340,11 +342,9 @@ namespace storm {
storm::storage::BitVector statesNotInBsccs = ~statesInBsccs; storm::storage::BitVector statesNotInBsccs = ~statesInBsccs;
// calculate steady state distribution for all BSCCs by calculating an eigenvector for the eigenvalue 1 of the transposed transition matrix for the bsccs // calculate steady state distribution for all BSCCs by calculating an eigenvector for the eigenvalue 1 of the transposed transition matrix for the bsccs
storm::storage::SparseMatrix<ValueType> bsccEquationSystem = transitionMatrix.getSubmatrix(false, statesInBsccs, statesInBsccs, true).transpose();
ValueType one = storm::utility::one<ValueType>();
ValueType zero = storm::utility::zero<ValueType>();
storm::storage::SparseMatrix<ValueType> bsccEquationSystem = transitionMatrix.getSubmatrix(false, statesInBsccs, statesInBsccs, true);
//subtract identity matrix
for (uint_fast64_t row = 0; row < bsccEquationSystem.getRowCount(); ++row) { for (uint_fast64_t row = 0; row < bsccEquationSystem.getRowCount(); ++row) {
for (auto& entry : bsccEquationSystem.getRow(row)) { for (auto& entry : bsccEquationSystem.getRow(row)) {
if (entry.getColumn() == row) { if (entry.getColumn() == row) {
@ -352,6 +352,8 @@ namespace storm {
} }
} }
} }
//now transpose, this internally removes all explicit zeros from the matrix that where introduced when subtracting the identity matrix
bsccEquationSystem = bsccEquationSystem.transpose();
std::vector<ValueType> bsccEquationSystemRightSide(bsccEquationSystem.getColumnCount(), zero); std::vector<ValueType> bsccEquationSystemRightSide(bsccEquationSystem.getColumnCount(), zero);
std::vector<ValueType> bsccEquationSystemSolution(bsccEquationSystem.getColumnCount(), one); std::vector<ValueType> bsccEquationSystemSolution(bsccEquationSystem.getColumnCount(), one);
@ -392,7 +394,7 @@ namespace storm {
rewardRightSide.push_back(reward); rewardRightSide.push_back(reward);
} }
storm::storage::SparseMatrix<ValueType> rewardEquationSystemMatrix = transitionMatrix.getSubmatrix(false, statesNotInBsccs, statesNotInBsccs);
storm::storage::SparseMatrix<ValueType> rewardEquationSystemMatrix = transitionMatrix.getSubmatrix(false, statesNotInBsccs, statesNotInBsccs, true);
rewardEquationSystemMatrix.convertToEquationSystem(); rewardEquationSystemMatrix.convertToEquationSystem();
std::vector<ValueType> rewardSolution(rewardEquationSystemMatrix.getColumnCount(), one); std::vector<ValueType> rewardSolution(rewardEquationSystemMatrix.getColumnCount(), one);

145
test/functional/modelchecker/SparseDtmcPrctlModelCheckerTest.cpp
View File

@ -127,3 +127,148 @@ TEST(SparseDtmcPrctlModelCheckerTest, SynchronousLeader) {
EXPECT_NEAR(1.0448979589010925, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0448979589010925, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision());
} }
TEST(SparseDtmcPrctlModelCheckerTest, LRA_SingleBscc) {
storm::storage::SparseMatrixBuilder<double> matrixBuilder;
std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc;
{
matrixBuilder = storm::storage::SparseMatrixBuilder<double>(2, 2, 2);
matrixBuilder.addNextValue(0, 1, 1.);
matrixBuilder.addNextValue(1, 0, 1.);
storm::storage::SparseMatrix<double> transitionMatrix = matrixBuilder.build();
storm::models::sparse::StateLabeling ap(2);
ap.addLabel("a");
ap.addLabelToState("a", 1);
dtmc.reset(new storm::models::sparse::Dtmc<double>(transitionMatrix, ap, boost::none, boost::none, boost::none));
storm::modelchecker::SparseDtmcPrctlModelChecker<double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("a");
auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(labelFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*lraFormula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(.5, quantitativeResult1[1], storm::settings::nativeEquationSolverSettings().getPrecision());
}
{
matrixBuilder = storm::storage::SparseMatrixBuilder<double>(2, 2, 4);
matrixBuilder.addNextValue(0, 0, .5);
matrixBuilder.addNextValue(0, 1, .5);
matrixBuilder.addNextValue(1, 0, .5);
matrixBuilder.addNextValue(1, 1, .5);
storm::storage::SparseMatrix<double> transitionMatrix = matrixBuilder.build();
storm::models::sparse::StateLabeling ap(2);
ap.addLabel("a");
ap.addLabelToState("a", 1);
dtmc.reset(new storm::models::sparse::Dtmc<double>(transitionMatrix, ap, boost::none, boost::none, boost::none));
storm::modelchecker::SparseDtmcPrctlModelChecker<double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("a");
auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(labelFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*lraFormula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(.5, quantitativeResult1[1], storm::settings::nativeEquationSolverSettings().getPrecision());
}
{
matrixBuilder = storm::storage::SparseMatrixBuilder<double>(3, 3, 3);
matrixBuilder.addNextValue(0, 1, 1);
matrixBuilder.addNextValue(1, 2, 1);
matrixBuilder.addNextValue(2, 0, 1);
storm::storage::SparseMatrix<double> transitionMatrix = matrixBuilder.build();
storm::models::sparse::StateLabeling ap(3);
ap.addLabel("a");
ap.addLabelToState("a", 2);
dtmc.reset(new storm::models::sparse::Dtmc<double>(transitionMatrix, ap, boost::none, boost::none, boost::none));
storm::modelchecker::SparseDtmcPrctlModelChecker<double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("a");
auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(labelFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*lraFormula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1. / 3., quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(1. / 3., quantitativeResult1[1], storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(1. / 3., quantitativeResult1[2], storm::settings::nativeEquationSolverSettings().getPrecision());
}
}
TEST(SparseDtmcPrctlModelCheckerTest, LRA) {
storm::storage::SparseMatrixBuilder<double> matrixBuilder;
std::shared_ptr<storm::models::sparse::Dtmc<double>> mdp;
{
matrixBuilder = storm::storage::SparseMatrixBuilder<double>(15, 15, 20, true);
matrixBuilder.addNextValue(0, 1, 1);
matrixBuilder.addNextValue(1, 4, 0.7);
matrixBuilder.addNextValue(1, 6, 0.3);
matrixBuilder.addNextValue(2, 0, 1);
matrixBuilder.addNextValue(3, 5, 0.8);
matrixBuilder.addNextValue(3, 9, 0.2);
matrixBuilder.addNextValue(4, 3, 1);
matrixBuilder.addNextValue(5, 3, 1);
matrixBuilder.addNextValue(6, 7, 1);
matrixBuilder.addNextValue(7, 8, 1);
matrixBuilder.addNextValue(8, 6, 1);
matrixBuilder.addNextValue(9, 10, 1);
matrixBuilder.addNextValue(10, 9, 1);
matrixBuilder.addNextValue(11, 9, 1);
matrixBuilder.addNextValue(12, 5, 0.4);
matrixBuilder.addNextValue(12, 8, 0.3);
matrixBuilder.addNextValue(12, 11, 0.3);
matrixBuilder.addNextValue(13, 7, 0.7);
matrixBuilder.addNextValue(13, 12, 0.3);
matrixBuilder.addNextValue(14, 12, 1);
storm::storage::SparseMatrix<double> transitionMatrix = matrixBuilder.build();
storm::models::sparse::StateLabeling ap(15);
ap.addLabel("a");
ap.addLabelToState("a", 1);
ap.addLabelToState("a", 4);
ap.addLabelToState("a", 5);
ap.addLabelToState("a", 7);
ap.addLabelToState("a", 11);
ap.addLabelToState("a", 13);
ap.addLabelToState("a", 14);
mdp.reset(new storm::models::sparse::Dtmc<double>(transitionMatrix, ap, boost::none, boost::none, boost::none));
storm::modelchecker::SparseDtmcPrctlModelChecker<double> checker(*mdp, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("a");
auto lraFormula = std::make_shared<storm::logic::LongRunAverageOperatorFormula>(labelFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*lraFormula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.3 / 3., quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0, quantitativeResult1[3], storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(1. / 3., quantitativeResult1[6], storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0, quantitativeResult1[9], storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.3/3., quantitativeResult1[12], storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(.79 / 3., quantitativeResult1[13], storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.3 / 3., quantitativeResult1[14], storm::settings::nativeEquationSolverSettings().getPrecision());
}
}
Write Preview
Loading…
Cancel
Save