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

Fixed some minor CTMC-related bugs. 

Former-commit-id: 3abb948542
tempestpy_adaptions
dehnert 10 years ago
parent
be66ef2751
commit
869f8c50c9
6 changed files with 14 additions and 16 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. 4
      src/modelchecker/csl/HybridCtmcCslModelChecker.cpp
  2. 6
      src/modelchecker/csl/SparseCtmcCslModelChecker.cpp
  3. 4
      src/storage/dd/CuddOdd.cpp
  4. 4
      test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
  5. 8
      test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
  6. 4
      test/functional/modelchecker/SparseCtmcCslModelCheckerTest.cpp

4
src/modelchecker/csl/HybridCtmcCslModelChecker.cpp
View File

@ -228,9 +228,6 @@ namespace storm {
HybridQuantitativeCheckResult<DdType> hybridResult(this->getModel().getReachableStates(), psiStates || (!statesWithProbabilityGreater0 && this->getModel().getReachableStates()),
psiStates.toAdd(), statesWithProbabilityGreater0NonPsi, odd, subResult);
// Determine the set of states that achieved a strictly positive probability.
std::unique_ptr<CheckResult> statesWithValuesGreaterZero = hybridResult.compareAgainstBound(storm::logic::ComparisonType::Greater, storm::utility::zero<ValueType>());
// Compute the set of relevant states.
storm::dd::Bdd<DdType> relevantStates = statesWithProbabilityGreater0 && phiStates;
@ -240,7 +237,6 @@ namespace storm {
// Build an ODD for the relevant states.
odd = storm::dd::Odd<DdType>(relevantStates);
std::vector<ValueType> result;
std::unique_ptr<CheckResult> explicitResult = hybridResult.toExplicitQuantitativeCheckResult();
std::vector<ValueType> newSubresult = std::move(explicitResult->asExplicitQuantitativeCheckResult<ValueType>().getValueVector());

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

@ -187,9 +187,9 @@ namespace storm {
storm::storage::BitVector relevantStates = statesWithProbabilityGreater0 & phiStates;
std::vector<ValueType> newSubresult = std::vector<ValueType>(relevantStates.getNumberOfSetBits());
storm::utility::vector::selectVectorValues(newSubresult, statesWithProbabilityGreater0NonPsi % relevantStates, subresult);
storm::utility::vector::setVectorValues(newSubresult, statesWithProbabilityGreater0NonPsi % relevantStates, subresult);
storm::utility::vector::setVectorValues(newSubresult, psiStates % relevantStates, storm::utility::one<ValueType>());
// Then compute the transient probabilities of being in such a state after t time units. For this,
// we must re-uniformize the CTMC, so we need to compute the second uniformized matrix.
uniformizationRate = storm::utility::zero<ValueType>();
@ -312,7 +312,7 @@ namespace storm {
if (computeCumulativeReward) {
result = std::vector<ValueType>(values.size());
std::function<ValueType (ValueType const&)> scaleWithUniformizationRate = [&uniformizationRate] (ValueType const& a) -> ValueType { return a / uniformizationRate; };
storm::utility::vector::applyPointwise(result, result, scaleWithUniformizationRate);
storm::utility::vector::applyPointwise(values, result, scaleWithUniformizationRate);
} else {
result = std::vector<ValueType>(values.size());
}

4
src/storage/dd/CuddOdd.cpp
View File

@ -113,7 +113,9 @@ namespace storm {
void Odd<DdType::CUDD>::expandValuesToVectorRec(uint_fast64_t oldOffset, storm::dd::Odd<DdType::CUDD> const& oldOdd, std::vector<double> const& oldValues, uint_fast64_t newOffset, storm::dd::Odd<DdType::CUDD> const& newOdd, std::vector<double>& newValues) {
if (oldOdd.isTerminalNode()) {
STORM_LOG_THROW(newOdd.isTerminalNode(), storm::exceptions::InvalidArgumentException, "The ODDs for the translation must have the same height.");
newValues[newOffset] += oldValues[oldOffset];
if (oldOdd.getThenOffset() != 0) {
newValues[newOffset] += oldValues[oldOffset];
}
} else {
expandValuesToVectorRec(oldOffset, oldOdd.getElseSuccessor(), oldValues, newOffset, newOdd.getElseSuccessor(), newValues);
expandValuesToVectorRec(oldOffset + oldOdd.getElseOffset(), oldOdd.getThenSuccessor(), oldValues, newOffset + newOdd.getElseOffset(), newOdd.getThenSuccessor(), newValues);

4
test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
View File

@ -53,7 +53,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Cluster) {
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.001105335651650576, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ \"minimum\" U<=10 \"premium\"]");
checkResult = modelchecker.check(*formula);
@ -139,7 +139,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Embedded) {
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(2.7720429852369946, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision());
}
TEST(GmmxxCtmcCslModelCheckerTest, Polling) {

8
test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
View File

@ -60,8 +60,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) {
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(ctmc->getReachableStates(), ctmc->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD> quantitativeCheckResult3 = checkResult->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
EXPECT_NEAR(0.001112543139248814, quantitativeCheckResult3.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(0.001112543139248814, quantitativeCheckResult3.getMax(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ \"minimum\" U<=10 \"premium\"]");
checkResult = modelchecker.check(*formula);
@ -163,8 +163,8 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded) {
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(ctmc->getReachableStates(), ctmc->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD> quantitativeCheckResult5 = checkResult->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD>();
EXPECT_NEAR(2.7720429852369946, quantitativeCheckResult5.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(2.7720429852369946, quantitativeCheckResult5.getMax(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5.getMax(), storm::settings::generalSettings().getPrecision());
}
TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling) {

4
test/functional/modelchecker/SparseCtmcCslModelCheckerTest.cpp
View File

@ -53,7 +53,7 @@ TEST(SparseCtmcCslModelCheckerTest, Cluster) {
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.001105335651650576, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ \"minimum\" U<=10 \"premium\"]");
checkResult = modelchecker.check(*formula);
@ -139,7 +139,7 @@ TEST(SparseCtmcCslModelCheckerTest, Embedded) {
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(2.7720429852369946, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision());
}
TEST(SparseCtmcCslModelCheckerTest, Polling) {

Write Preview
Loading…
Cancel
Save