diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index 9c70023a7..fdcf0bb3a 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -321,6 +321,8 @@ namespace storm { // Get some data members for convenience. typename storm::storage::SparseMatrix const& transitionMatrix = this->getModel().getTransitionMatrix(); + ValueType one = storm::utility::one(); + ValueType zero = storm::utility::zero(); // First we check which states are in BSCCs. We use this later to speed up reachability analysis storm::storage::BitVector statesInBsccs(numOfStates); @@ -340,11 +342,9 @@ namespace storm { 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 - storm::storage::SparseMatrix bsccEquationSystem = transitionMatrix.getSubmatrix(false, statesInBsccs, statesInBsccs, true).transpose(); - - ValueType one = storm::utility::one(); - ValueType zero = storm::utility::zero(); + storm::storage::SparseMatrix bsccEquationSystem = transitionMatrix.getSubmatrix(false, statesInBsccs, statesInBsccs, true); + //subtract identity matrix for (uint_fast64_t row = 0; row < bsccEquationSystem.getRowCount(); ++row) { for (auto& entry : bsccEquationSystem.getRow(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 bsccEquationSystemRightSide(bsccEquationSystem.getColumnCount(), zero); std::vector bsccEquationSystemSolution(bsccEquationSystem.getColumnCount(), one); @@ -392,7 +394,7 @@ namespace storm { rewardRightSide.push_back(reward); } - storm::storage::SparseMatrix rewardEquationSystemMatrix = transitionMatrix.getSubmatrix(false, statesNotInBsccs, statesNotInBsccs); + storm::storage::SparseMatrix rewardEquationSystemMatrix = transitionMatrix.getSubmatrix(false, statesNotInBsccs, statesNotInBsccs, true); rewardEquationSystemMatrix.convertToEquationSystem(); std::vector rewardSolution(rewardEquationSystemMatrix.getColumnCount(), one); diff --git a/test/functional/modelchecker/SparseDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SparseDtmcPrctlModelCheckerTest.cpp index c204d36dd..7f53f45b4 100644 --- a/test/functional/modelchecker/SparseDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseDtmcPrctlModelCheckerTest.cpp @@ -127,3 +127,148 @@ TEST(SparseDtmcPrctlModelCheckerTest, SynchronousLeader) { EXPECT_NEAR(1.0448979589010925, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision()); } + +TEST(SparseDtmcPrctlModelCheckerTest, LRA_SingleBscc) { + storm::storage::SparseMatrixBuilder matrixBuilder; + std::shared_ptr> dtmc; + + { + matrixBuilder = storm::storage::SparseMatrixBuilder(2, 2, 2); + matrixBuilder.addNextValue(0, 1, 1.); + matrixBuilder.addNextValue(1, 0, 1.); + storm::storage::SparseMatrix transitionMatrix = matrixBuilder.build(); + + storm::models::sparse::StateLabeling ap(2); + ap.addLabel("a"); + ap.addLabelToState("a", 1); + + dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap, boost::none, boost::none, boost::none)); + + storm::modelchecker::SparseDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + + auto labelFormula = std::make_shared("a"); + auto lraFormula = std::make_shared(labelFormula); + + std::unique_ptr result = std::move(checker.check(*lraFormula)); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(.5, quantitativeResult1[1], storm::settings::nativeEquationSolverSettings().getPrecision()); + } + { + matrixBuilder = storm::storage::SparseMatrixBuilder(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 transitionMatrix = matrixBuilder.build(); + + storm::models::sparse::StateLabeling ap(2); + ap.addLabel("a"); + ap.addLabelToState("a", 1); + + dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap, boost::none, boost::none, boost::none)); + + storm::modelchecker::SparseDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + + auto labelFormula = std::make_shared("a"); + auto lraFormula = std::make_shared(labelFormula); + + std::unique_ptr result = std::move(checker.check(*lraFormula)); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); + EXPECT_NEAR(.5, quantitativeResult1[1], storm::settings::nativeEquationSolverSettings().getPrecision()); + } + + { + matrixBuilder = storm::storage::SparseMatrixBuilder(3, 3, 3); + matrixBuilder.addNextValue(0, 1, 1); + matrixBuilder.addNextValue(1, 2, 1); + matrixBuilder.addNextValue(2, 0, 1); + storm::storage::SparseMatrix transitionMatrix = matrixBuilder.build(); + + storm::models::sparse::StateLabeling ap(3); + ap.addLabel("a"); + ap.addLabelToState("a", 2); + + dtmc.reset(new storm::models::sparse::Dtmc(transitionMatrix, ap, boost::none, boost::none, boost::none)); + + storm::modelchecker::SparseDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + + auto labelFormula = std::make_shared("a"); + auto lraFormula = std::make_shared(labelFormula); + + std::unique_ptr result = std::move(checker.check(*lraFormula)); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + 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 matrixBuilder; + std::shared_ptr> mdp; + + { + matrixBuilder = storm::storage::SparseMatrixBuilder(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 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(transitionMatrix, ap, boost::none, boost::none, boost::none)); + + storm::modelchecker::SparseDtmcPrctlModelChecker checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); + + auto labelFormula = std::make_shared("a"); + auto lraFormula = std::make_shared(labelFormula); + + std::unique_ptr result = std::move(checker.check(*lraFormula)); + storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); + + 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()); + } +} \ No newline at end of file