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

step bounded properties for dtmcs in a new helper, and now with support for (extra) lower bounds

tempestpy_adaptions
Sebastian Junges 4 years ago
parent
406ffbdc7f
commit
843e6a9b6b
5 changed files with 125 additions and 43 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. 94
      src/storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.cpp
  2. 25
      src/storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.h
  3. 8
      src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
  4. 39
      src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
  5. 2
      src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h

94
src/storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.cpp
View File

@ -0,0 +1,94 @@
#include "storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.h"
#include "storm/modelchecker/hints/ExplicitModelCheckerHint.h"
#include "storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/utility/macros.h"
#include "storm/utility/vector.h"
#include "storm/utility/graph.h"
#include "storm/storage/expressions/Expression.h"
#include "storm/solver/Multiplier.h"
#include "storm/utility/SignalHandler.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
namespace storm {
namespace modelchecker {
namespace helper {
template<typename ValueType>
SparseDeterministicStepBoundedHorizonHelper<ValueType>::SparseDeterministicStepBoundedHorizonHelper()
{
// Intentionally left empty.
}
template<typename ValueType>
std::vector<ValueType> SparseDeterministicStepBoundedHorizonHelper<ValueType>::compute(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint64_t lowerBound, uint64_t upperBound, ModelCheckerHint const& hint)
{
std::vector<ValueType> result(transitionMatrix.getRowCount(), storm::utility::zero<ValueType>());
// If we identify the states that have probability 0 of reaching the target states, we can exclude them in the further analysis.
storm::storage::BitVector maybeStates;
storm::storage::BitVector makeZeroColumns;
if (hint.isExplicitModelCheckerHint() && hint.template asExplicitModelCheckerHint<ValueType>().getComputeOnlyMaybeStates()) {
maybeStates = hint.template asExplicitModelCheckerHint<ValueType>().getMaybeStates();
} else {
maybeStates = storm::utility::graph::performProbGreater0(backwardTransitions, phiStates, psiStates, true, upperBound);
if (lowerBound == 0) {
maybeStates &= ~psiStates;
} else {
makeZeroColumns = psiStates;
}
}
STORM_LOG_INFO("Preprocessing: " << maybeStates.getNumberOfSetBits() << " non-target states with probability greater 0.");
if (lowerBound == 0) {
storm::utility::vector::setVectorValues<ValueType>(result, psiStates,
storm::utility::one<ValueType>());
}
if (!maybeStates.empty()) {
// We can eliminate the rows and columns from the original transition probability matrix that have probability 0.
storm::storage::SparseMatrix<ValueType> submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, true, makeZeroColumns);
// Create the vector of one-step probabilities to go to target states.
std::vector<ValueType> b = transitionMatrix.getConstrainedRowSumVector(maybeStates, psiStates);
// Create the vector with which to multiply.
std::vector<ValueType> subresult(maybeStates.getNumberOfSetBits());
// Perform the matrix vector multiplication
auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, submatrix);
if (lowerBound == 0) {
multiplier->repeatedMultiply(env, subresult, &b, upperBound);
} else {
multiplier->repeatedMultiply(env, subresult, &b, upperBound - lowerBound + 1);
submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, true);
multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, submatrix);
b = std::vector<ValueType>(b.size(), storm::utility::zero<ValueType>());
multiplier->repeatedMultiply(env, subresult, &b, lowerBound - 1);
}
// Set the values of the resulting vector accordingly.
storm::utility::vector::setVectorValues(result, maybeStates, subresult);
}
return result;
}
template class SparseDeterministicStepBoundedHorizonHelper<double>;
template class SparseDeterministicStepBoundedHorizonHelper<storm::RationalNumber>;
template class SparseDeterministicStepBoundedHorizonHelper<storm::RationalFunction>;
}
}
}//
// Created by Sebastian Junges on 8/20/20.
//

25
src/storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.h
View File

@ -0,0 +1,25 @@
#pragma once
#include "storm/modelchecker/hints/ModelCheckerHint.h"
#include "storm/modelchecker/prctl/helper/SolutionType.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/utility/solver.h"
#include "storm/solver/SolveGoal.h"
namespace storm {
namespace modelchecker {
namespace helper {
template<typename ValueType>
class SparseDeterministicStepBoundedHorizonHelper {
public:
SparseDeterministicStepBoundedHorizonHelper();
std::vector<ValueType> compute(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint64_t lowerBound, uint64_t upperBound, ModelCheckerHint const& hint = ModelCheckerHint());
private:
};
}
}
}

8
src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
View File

@ -1,4 +1,5 @@
#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
#include "storm/modelchecker/helper/finitehorizon/SparseDeterministicStepBoundedHorizonHelper.h"
#include <vector>
#include <memory>
@ -70,15 +71,16 @@ namespace storm {
auto numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeRewardBoundedValues(env, this->getModel(), formula);
return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
} else {
STORM_LOG_THROW(!pathFormula.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have (a single) upper time bound, and no lower bound.");
STORM_LOG_THROW(pathFormula.hasIntegerLowerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete lower time bound.");
STORM_LOG_THROW(pathFormula.hasIntegerUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have discrete upper time bound.");
std::unique_ptr<CheckResult> leftResultPointer = this->check(env, pathFormula.getLeftSubformula());
std::unique_ptr<CheckResult> rightResultPointer = this->check(env, pathFormula.getRightSubformula());
ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<ValueType>::computeStepBoundedUntilProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictUpperBound<uint64_t>(), checkTask.getHint());
storm::modelchecker::helper::SparseDeterministicStepBoundedHorizonHelper<ValueType> helper;
std::vector<ValueType> numericResult = helper.compute(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getNonStrictLowerBound<uint64_t>(), pathFormula.getNonStrictUpperBound<uint64_t>(), checkTask.getHint());
std::unique_ptr<CheckResult> result = std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
return result;
return result;
// NOLINT #include // For exit(). #if GTEST_HAS_SEH # include #endif #if GTEST_HAS_EXCEPTIONS # include // For set_terminate(). # include #endif using testing::Test; #if GTEST_HAS_SEH class SehExceptionInConstructorTest : public Test { public: SehExceptionInConstructorTest() { RaiseException(42, 0, 0, NULL); } }; TEST_F(SehExceptionInConstructorTest, ThrowsExceptionInConstructor) {} class SehExceptionInDestructorTest : public Test { public: ~SehExceptionInDestructorTest() { RaiseException(42, 0, 0, NULL); } }; TEST_F(SehExceptionInDestructorTest, ThrowsExceptionInDestructor) {} class SehExceptionInSetUpTestCaseTest : public Test { public: static void SetUpTestCase() { RaiseException(42, 0, 0, NULL); } }; TEST_F(SehExceptionInSetUpTestCaseTest, ThrowsExceptionInSetUpTestCase) {} class SehExceptionInTearDownTestCaseTest : public Test { public: static void TearDownTestCase() { RaiseException(42, 0, 0, NULL); } }; TEST_F(SehExceptionInTearDownTestCaseTest, ThrowsExceptionInTearDownTestCase) {} class SehExceptionInSetUpTest : public Test { protected: virtual void SetUp() { RaiseException(42, 0, 0, NULL); } }; TEST_F(SehExceptionInSetUpTest, ThrowsExceptionInSetUp) {} class SehExceptionInTearDownTest : public Test { protected: virtual void TearDown() { RaiseException(42, 0, 0, NULL); } }; TEST_F(SehExceptionInTearDownTest, ThrowsExceptionInTearDown) {} TEST(SehExceptionTest, ThrowsSehException) { RaiseException(42, 0, 0, NULL); } #endif // GTEST_HAS_SEH #if GTEST_HAS_EXCEPTIONS class CxxExceptionInConstructorTest : public Test { public: CxxExceptionInConstructorTest() { // Without this macro VC++ complains about unreachable code at the end of // the constructor. GTEST_SUPPRESS_UNREACHABLE_CODE_WARNING_BELOW_( throw std::runtime_error("Standard C++ exception")); } static void TearDownTestCase() { printf("%s", "CxxExceptionInConstructorTest::TearDownTestCase() " "called as expected.\n"); } protected: ~CxxExceptionInConstructorTest() { ADD_FAILURE() << "CxxExceptionInConstructorTest destructor " << "called unexpectedly."; } virtual void SetUp() { ADD_FAILURE() << "CxxExceptionInConstructorTest::SetUp() " << "called unexpectedly."; } virtual void TearDown() { ADD_FAILURE() << "CxxExceptionInConstructorTest::TearDown() " << "called unexpectedly."; } }; TEST_F(CxxExceptionInConstructorTest, ThrowsExceptionInConstructor) { ADD_FAILURE() << "CxxExceptionInConstructorTest test body " << "called unexpectedly."; } class CxxExceptionInDestructorTest : public Test { public: static void TearDownTestCase() { printf("%s", "CxxExceptionInDestructorTest::TearDownTestCase() " "called as expected.\n"); } protected: ~CxxExceptionInDestructorTest() { GTEST_SUPPRESS_UNREACHABLE_CODE_WARNING_BELOW_( throw std::runtime_error("Standard C++ exception")); } }; TEST_F(CxxExceptionInDestructorTest, ThrowsExceptionInDestructor) {} class CxxExceptionInSetUpTestCaseTest : public Test { public: CxxExceptionInSetUpTestCaseTest() { printf("%s", "CxxExceptionInSetUpTestCaseTest constructor " "called as expected.\n"); } static void SetUpTestCase() { throw std::runtime_error("Standard C++ exception"); } static void TearDownTestCase() { printf("%s", "CxxExceptionInSetUpTestCaseTest::TearDownTestCase() " "called as expected.\n"); } protected: ~CxxExceptionInSetUpTestCaseTest() { printf("%s", "CxxExceptionInSetUpTestCaseTest destructor " "called as expected.\n"); } virtual void SetUp() { printf("%s", "CxxExceptionInSetUpTestCaseTest::SetUp() " "called as expected.\n"); } virtual void TearDown() { printf("%s", "CxxExceptionInSetUpTestCaseTest::TearDown() " "called as expected.\n"); } }; TEST_F(CxxExceptionInSetUpTestCaseTest, ThrowsExceptionInSetUpTestCase) { printf("%s", "CxxExceptionInSetUpTestCaseTest test body " "called as expected.\n"); } class CxxExceptionInTearDownTestCaseTest : public Test { public: static void TearDownTestCase() { throw std::runtime_error("Standard C++ exception"); } }; TEST_F(CxxExceptionInTearDownTestCaseTest, ThrowsExceptionInTearDownTestCase) {} class CxxExceptionInSetUpTest : public Test { public: static void TearDownTestCase() { printf("%s", "CxxExceptionInSetUpTest::TearDownTestCase() " "called as expected.\n"); } protected: ~CxxExceptionInSetUpTest() { printf("%s", "CxxExceptionInSetUpTest destructor " "called as expected.\n"); } virtual void SetUp() { throw std::runtime_error("Standard C++ exception"); } virtual void TearDown() { printf("%s", "CxxExceptionInSetUpTest::TearDown() " "called as expected.\n"); } }; TEST_F(CxxExceptionInSetUpTest, ThrowsExceptionInSetUp) { ADD_FAILURE() << "CxxExceptionInSetUpTest test body " << "called unexpectedly."; } class CxxExceptionInTearDownTest : public Test { public: static void TearDownTestCase() { printf("%s", "CxxExceptionInTearDownTest::TearDownTestCase() " "called as expected.\n"); } protected: ~CxxExceptionInTearDownTest() { printf("%s", "CxxExceptionInTearDownTest destructor " "called as expected.\n"); } virtual void TearDown() { throw std::runtime_error("Standard C++ exception"); } }; TEST_F(CxxExceptionInTearDownTest, ThrowsExceptionInTearDown) {} class CxxExceptionInTestBodyTest : public Test { public: static void TearDownTestCase() { printf("%s", "CxxExceptionInTestBodyTest::TearDownTestCase() " "called as expected.\n"); } protected: ~CxxExceptionInTestBodyTest() { printf("%s", "CxxExceptionInTestBodyTest destructor " "called as expected.\n"); } virtual void TearDown() { printf("%s", "CxxExceptionInTestBodyTest::TearDown() " "called as expected.\n"); } }; TEST_F(CxxExceptionInTestBodyTest, ThrowsStdCxxException) { throw std::runtime_error("Standard C++ exception"); } TEST(CxxExceptionTest, ThrowsNonStdCxxException) { throw "C-string"; } // This terminate handler aborts the program using exit() rather than abort(). // This avoids showing pop-ups on Windows systems and core dumps on Unix-like // ones. void TerminateHandler() { fprintf(stderr, "%s\n", "Unhandled C++ exception terminating the program."); fflush(NULL); exit(3); } #endif // GTEST_HAS_EXCEPTIONS int main(int argc, char** argv) { #if GTEST_HAS_EXCEPTIONS std::set_terminate(&TerminateHandler); #endif testing::InitGoogleTest(&argc, argv); return RUN_ALL_TESTS(); }