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

Fixed a model building problem. Included checking of reward properties on CTMCs and wrote tests for it. 

Former-commit-id: a137bd20ac
tempestpy_adaptions
dehnert 10 years ago
parent
a851fad65d
commit
49bed497b0
7 changed files with 499 additions and 70 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. 33
      examples/ctmc/embedded/embedded_debug.sm
  2. 8
      src/builder/ExplicitPrismModelBuilder.cpp
  3. 28
      src/modelchecker/csl/SparseCtmcCslModelChecker.cpp
  4. 213
      test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
  5. 196
      test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
  6. 58
      test/functional/modelchecker/SparseCtmcCslModelCheckerTest.cpp
  7. 23
      test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp

33
examples/ctmc/embedded/embedded_debug.sm
View File

@ -1,33 +0,0 @@
ctmc
// constants
const int MAX_COUNT;
const int MIN_SENSORS = 2;
const int MIN_ACTUATORS = 1;
// rates
const double lambda_p = 1/(365*24*60*60); // 1 year
const double lambda_s = 1/(30*24*60*60); // 1 month
const double lambda_a = 1/(2*30*24*60*60); // 2 months
const double tau = 1/60; // 1 min
const double delta_f = 1/(24*60*60); // 1 day
const double delta_r = 1/30; // 30 secs
// sensors
module sensors
s : [0..3] init 3; // number of sensors working
[] s>1 -> s*lambda_s : (s'=s-1); // failure of a single sensor
endmodule
// input processor
// (takes data from sensors and passes onto main processor)
module proci
i : [0..2] init 2; // 2=ok, 1=transient fault, 0=failed
[] i>0 & s>=MIN_SENSORS -> lambda_p : (i'=0); // failure of processor
endmodule

8
src/builder/ExplicitPrismModelBuilder.cpp
View File

@ -127,11 +127,6 @@ namespace storm {
#endif #endif
} }
// Now that we have defined all the constants in the program, we need to substitute their appearances in
// all expressions in the program so we can then evaluate them without having to store the values of the
// constants in the state (i.e., valuation).
preparedProgram = preparedProgram.substituteConstants();
storm::prism::RewardModel rewardModel = storm::prism::RewardModel(); storm::prism::RewardModel rewardModel = storm::prism::RewardModel();
// Select the appropriate reward model. // Select the appropriate reward model.
@ -165,6 +160,9 @@ namespace storm {
} }
} }
// Now that the program is fixed, we we need to substitute all constants with their concrete value.
preparedProgram = preparedProgram.substituteConstants();
ModelComponents modelComponents = buildModelComponents(preparedProgram, rewardModel, options); ModelComponents modelComponents = buildModelComponents(preparedProgram, rewardModel, options);
std::shared_ptr<storm::models::sparse::Model<ValueType>> result; std::shared_ptr<storm::models::sparse::Model<ValueType>> result;

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

@ -339,23 +339,35 @@ namespace storm {
template<class ValueType> template<class ValueType>
std::vector<ValueType> SparseCtmcCslModelChecker<ValueType>::computeCumulativeRewardsHelper(double timeBound) const { std::vector<ValueType> SparseCtmcCslModelChecker<ValueType>::computeCumulativeRewardsHelper(double timeBound) const {
// Only compute the result if the model has a state-based reward this->getModel(). // Only compute the result if the model has a state-based reward this->getModel().
STORM_LOG_THROW(this->getModel().hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
STORM_LOG_THROW(this->getModel().hasStateRewards() || this->getModel().hasTransitionRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
// Initialize result to state rewards of the this->getModel().
std::vector<ValueType> result(this->getModel().getStateRewardVector());
// If the time bound is zero, the result is the constant zero vector.
if (timeBound == 0) {
return std::vector<ValueType>(this->getModel().getNumberOfStates(), storm::utility::zero<ValueType>());
}
// If the time-bound is not zero, we need to perform a transient analysis.
if (timeBound > 0) {
// Otherwise, we need to perform some computations.
// Start with the uniformization.
ValueType uniformizationRate = 0; ValueType uniformizationRate = 0;
for (auto const& rate : this->getModel().getExitRateVector()) { for (auto const& rate : this->getModel().getExitRateVector()) {
uniformizationRate = std::max(uniformizationRate, rate); uniformizationRate = std::max(uniformizationRate, rate);
} }
storm::storage::SparseMatrix<ValueType> uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), storm::storage::BitVector(this->getModel().getNumberOfStates(), true), storm::storage::BitVector(this->getModel().getNumberOfStates()), uniformizationRate, this->getModel().getExitRateVector()); storm::storage::SparseMatrix<ValueType> uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), storm::storage::BitVector(this->getModel().getNumberOfStates(), true), storm::storage::BitVector(this->getModel().getNumberOfStates()), uniformizationRate, this->getModel().getExitRateVector());
result = this->computeTransientProbabilities<true>(uniformizedMatrix, timeBound, uniformizationRate, result, *this->linearEquationSolver);
// Compute the total state reward vector.
std::vector<ValueType> totalRewardVector;
if (this->getModel().hasTransitionRewards()) {
totalRewardVector = this->getModel().getTransitionMatrix().getPointwiseProductRowSumVector(this->getModel().getTransitionRewardMatrix());
if (this->getModel().hasStateRewards()) {
storm::utility::vector::addVectorsInPlace(totalRewardVector, this->getModel().getStateRewardVector());
}
} else {
totalRewardVector = std::vector<ValueType>(this->getModel().getStateRewardVector());
} }
return result;
// Finally, compute the transient probabilities.
return this->computeTransientProbabilities<true>(uniformizedMatrix, timeBound, uniformizationRate, totalRewardVector, *this->linearEquationSolver);
} }
template<class ValueType> template<class ValueType>

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

@ -0,0 +1,213 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/parser/PrismParser.h"
#include "src/parser/FormulaParser.h"
#include "src/logic/Formulas.h"
#include "src/builder/ExplicitPrismModelBuilder.h"
#include "src/solver/GmmxxLinearEquationSolver.h"
#include "src/modelchecker/csl/SparseCtmcCslModelChecker.h"
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/settings/SettingsManager.h"
TEST(GmmxxCtmcCslModelCheckerTest, Cluster) {
// Parse the model description.
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
std::shared_ptr<storm::logic::Formula> formula(nullptr);
// Build the model.
typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
options.buildRewards = true;
options.rewardModelName = "num_repairs";
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
// Create model checker.
storm::modelchecker::SparseCtmcCslModelChecker<double> modelchecker(*ctmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
// Start checking properties.
formula = formulaParser.parseFromString("P=? [ F<=100 !\"minimum\"]");
std::unique_ptr<storm::modelchecker::CheckResult> checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ F[100,100] !\"minimum\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ \"minimum\" U<=10 \"premium\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ !\"minimum\" U[1,inf] \"minimum\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0, quantitativeCheckResult4[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [C<=100]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision());
}
TEST(GmmxxCtmcCslModelCheckerTest, Embedded) {
// Parse the model description.
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
std::shared_ptr<storm::logic::Formula> formula(nullptr);
// Build the model.
typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
options.buildRewards = true;
options.rewardModelName = "up";
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
// Create model checker.
storm::modelchecker::SparseCtmcCslModelChecker<double> modelchecker(*ctmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
// Start checking properties.
formula = formulaParser.parseFromString("P=? [ F<=10000 \"down\"]");
std::unique_ptr<storm::modelchecker::CheckResult> checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_actuators\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_io\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_sensors\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [C<=10000]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(2.7719776270427521, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision());
}
TEST(GmmxxCtmcCslModelCheckerTest, Polling) {
// Parse the model description.
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
std::shared_ptr<storm::logic::Formula> formula(nullptr);
// Build the model.
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
// Create model checker.
storm::modelchecker::SparseCtmcCslModelChecker<double> modelchecker(*ctmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
// Start checking properties.
formula = formulaParser.parseFromString("P=?[ F<=10 \"target\"]");
std::unique_ptr<storm::modelchecker::CheckResult> checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1, quantitativeCheckResult1[initialState], storm::settings::generalSettings().getPrecision());
}
TEST(GmmxxCtmcCslModelCheckerTest, Fms) {
// No properties to check at this point.
}
TEST(GmmxxCtmcCslModelCheckerTest, Tandem) {
// Parse the model description.
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
std::shared_ptr<storm::logic::Formula> formula(nullptr);
// Build the model.
typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
options.buildRewards = true;
options.rewardModelName = "customers";
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin();
// Create model checker.
storm::modelchecker::SparseCtmcCslModelChecker<double> modelchecker(*ctmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::GmmxxLinearEquationSolver<double>()));
// Start checking properties.
formula = formulaParser.parseFromString("P=? [ F<=10 \"network_full\" ]");
std::unique_ptr<storm::modelchecker::CheckResult> checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ F<=10 \"first_queue_full\" ]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [I=10]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [C<=10]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [F \"first_queue_full\"&\"second_queue_full\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult6 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(262.85103661561755, quantitativeCheckResult6[initialState], storm::settings::generalSettings().getPrecision());
}

196
test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
View File

@ -0,0 +1,196 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/logic/Formulas.h"
#include "src/solver/GmmxxNondeterministicLinearEquationSolver.h"
#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/settings/SettingsManager.h"
#include "src/parser/AutoParser.h"
TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew");
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
ASSERT_EQ(mdp->getNumberOfStates(), 169ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull);
storm::modelchecker::SparseMdpPrctlModelChecker<double> checker(*mdp, std::shared_ptr<storm::solver::GmmxxNondeterministicLinearEquationSolver<double>>(new storm::solver::GmmxxNondeterministicLinearEquationSolver<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("two");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
auto minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
auto maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
result = checker.check(*maxProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("three");
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
result = checker.check(*minProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision());
maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
result = checker.check(*maxProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("four");
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
result = checker.check(*minProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision());
maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
result = checker.check(*maxProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
auto minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
result = checker.check(*minRewardOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.333329499, quantitativeResult7[0], storm::settings::nativeEquationSolverSettings().getPrecision());
auto maxRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
result = checker.check(*maxRewardOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult8 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.333329499, quantitativeResult8[0], storm::settings::nativeEquationSolverSettings().getPrecision());
abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", "");
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::sparse::Mdp<double>> stateRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
storm::modelchecker::SparseMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp, std::shared_ptr<storm::solver::GmmxxNondeterministicLinearEquationSolver<double>>(new storm::solver::GmmxxNondeterministicLinearEquationSolver<double>()));
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
result = stateRewardModelChecker.check(*minRewardOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult9 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.333329499, quantitativeResult9[0], storm::settings::nativeEquationSolverSettings().getPrecision());
maxRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
result = stateRewardModelChecker.check(*maxRewardOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult10 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.333329499, quantitativeResult10[0], storm::settings::nativeEquationSolverSettings().getPrecision());
abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew");
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::sparse::Mdp<double>> stateAndTransitionRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
storm::modelchecker::SparseMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::shared_ptr<storm::solver::GmmxxNondeterministicLinearEquationSolver<double>>(new storm::solver::GmmxxNondeterministicLinearEquationSolver<double>()));
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("done");
reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
result = stateAndTransitionRewardModelChecker.check(*minRewardOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(14.666658998, quantitativeResult11[0], storm::settings::nativeEquationSolverSettings().getPrecision());
maxRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
result = stateAndTransitionRewardModelChecker.check(*maxRewardOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult12 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(14.666658998, quantitativeResult12[0], storm::settings::nativeEquationSolverSettings().getPrecision());
}
TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.trans.rew");
ASSERT_EQ(storm::models::ModelType::Mdp, abstractModel->getType());
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
ASSERT_EQ(3172ull, mdp->getNumberOfStates());
ASSERT_EQ(7144ull, mdp->getNumberOfTransitions());
storm::modelchecker::SparseMdpPrctlModelChecker<double> checker(*mdp, std::shared_ptr<storm::solver::GmmxxNondeterministicLinearEquationSolver<double>>(new storm::solver::GmmxxNondeterministicLinearEquationSolver<double>()));
auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
auto minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, eventuallyFormula);
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*minProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
auto maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, eventuallyFormula);
result = checker.check(*maxProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto trueFormula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula>(trueFormula, labelFormula, 25);
minProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Minimize, boundedUntilFormula);
result = checker.check(*minProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0625, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision());
maxProbabilityOperatorFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(storm::logic::OptimalityType::Maximize, boundedUntilFormula);
result = checker.check(*maxProbabilityOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0625, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
auto minRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Minimize, reachabilityRewardFormula);
result = checker.check(*minRewardOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(4.285689611, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision());
auto maxRewardOperatorFormula = std::make_shared<storm::logic::RewardOperatorFormula>(storm::logic::OptimalityType::Maximize, reachabilityRewardFormula);
result = checker.check(*maxRewardOperatorFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(4.285689611, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision());
}

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

@ -19,13 +19,16 @@ TEST(SparseCtmcCslModelCheckerTest, Cluster) {
std::shared_ptr<storm::logic::Formula> formula(nullptr); std::shared_ptr<storm::logic::Formula> formula(nullptr);
// Build the model. // Build the model.
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
options.buildRewards = true;
options.rewardModelName = "num_repairs";
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>(); std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin(); uint_fast64_t initialState = *ctmc->getInitialStates().begin();
// Create model checker. // Create model checker.
storm::modelchecker::SparseCtmcCslModelChecker<double> modelchecker(*ctmc);
storm::modelchecker::SparseCtmcCslModelChecker<double> modelchecker(*ctmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::NativeLinearEquationSolver<double>()));
// Start checking properties. // Start checking properties.
formula = formulaParser.parseFromString("P=? [ F<=100 !\"minimum\"]"); formula = formulaParser.parseFromString("P=? [ F<=100 !\"minimum\"]");
@ -55,6 +58,13 @@ TEST(SparseCtmcCslModelCheckerTest, Cluster) {
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0, quantitativeCheckResult4[initialState], storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(0, quantitativeCheckResult4[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [C<=100]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision());
} }
TEST(SparseCtmcCslModelCheckerTest, Embedded) { TEST(SparseCtmcCslModelCheckerTest, Embedded) {
@ -64,13 +74,16 @@ TEST(SparseCtmcCslModelCheckerTest, Embedded) {
std::shared_ptr<storm::logic::Formula> formula(nullptr); std::shared_ptr<storm::logic::Formula> formula(nullptr);
// Build the model. // Build the model.
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
options.buildRewards = true;
options.rewardModelName = "up";
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>(); std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin(); uint_fast64_t initialState = *ctmc->getInitialStates().begin();
// Create model checker. // Create model checker.
storm::modelchecker::SparseCtmcCslModelChecker<double> modelchecker(*ctmc);
storm::modelchecker::SparseCtmcCslModelChecker<double> modelchecker(*ctmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::NativeLinearEquationSolver<double>()));
// Start checking properties. // Start checking properties.
formula = formulaParser.parseFromString("P=? [ F<=10000 \"down\"]"); formula = formulaParser.parseFromString("P=? [ F<=10000 \"down\"]");
@ -100,6 +113,13 @@ TEST(SparseCtmcCslModelCheckerTest, Embedded) {
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4[initialState], storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [C<=10000]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(2.7719776270427521, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision());
} }
TEST(SparseCtmcCslModelCheckerTest, Polling) { TEST(SparseCtmcCslModelCheckerTest, Polling) {
@ -136,14 +156,17 @@ TEST(SparseCtmcCslModelCheckerTest, Tandem) {
storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer()); storm::parser::FormulaParser formulaParser(program.getManager().getSharedPointer());
std::shared_ptr<storm::logic::Formula> formula(nullptr); std::shared_ptr<storm::logic::Formula> formula(nullptr);
// Build the model.
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program);
// Build the model with the customers reward structure.
typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
options.buildRewards = true;
options.rewardModelName = "customers";
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType());
std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>(); std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc = model->as<storm::models::sparse::Ctmc<double>>();
uint_fast64_t initialState = *ctmc->getInitialStates().begin(); uint_fast64_t initialState = *ctmc->getInitialStates().begin();
// Create model checker. // Create model checker.
storm::modelchecker::SparseCtmcCslModelChecker<double> modelchecker(*ctmc);
storm::modelchecker::SparseCtmcCslModelChecker<double> modelchecker(*ctmc, std::unique_ptr<storm::solver::LinearEquationSolver<double>>(new storm::solver::NativeLinearEquationSolver<double>()));
// Start checking properties. // Start checking properties.
formula = formulaParser.parseFromString("P=? [ F<=10 \"network_full\" ]"); formula = formulaParser.parseFromString("P=? [ F<=10 \"network_full\" ]");
@ -166,4 +189,25 @@ TEST(SparseCtmcCslModelCheckerTest, Tandem) {
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult()); ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision()); EXPECT_NEAR(1, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [I=10]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [C<=10]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [F \"first_queue_full\"&\"second_queue_full\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult6 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(262.78584491454814, quantitativeCheckResult6[initialState], storm::settings::generalSettings().getPrecision());
} }

23
test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp
View File

@ -2,7 +2,6 @@
#include "storm-config.h" #include "storm-config.h"
#include "src/logic/Formulas.h" #include "src/logic/Formulas.h"
#include "src/solver/GmmxxLinearEquationSolver.h"
#include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" #include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "src/settings/SettingsManager.h" #include "src/settings/SettingsManager.h"
@ -27,7 +26,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Die) {
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*eventuallyFormula); std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*eventuallyFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0/6.0, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
EXPECT_NEAR(1.0/6.0, quantitativeResult1[0], storm::settings::generalSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("two"); labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("two");
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula); eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
@ -35,7 +34,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Die) {
result = checker.check(*eventuallyFormula); result = checker.check(*eventuallyFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0/6.0, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
EXPECT_NEAR(1.0/6.0, quantitativeResult2[0], storm::settings::generalSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("three"); labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("three");
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula); eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
@ -43,7 +42,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Die) {
result = checker.check(*eventuallyFormula); result = checker.check(*eventuallyFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0/6.0, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
EXPECT_NEAR(1.0/6.0, quantitativeResult3[0], storm::settings::generalSettings().getPrecision());
auto done = std::make_shared<storm::logic::AtomicLabelFormula>("done"); auto done = std::make_shared<storm::logic::AtomicLabelFormula>("done");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(done); auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(done);
@ -51,7 +50,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Die) {
result = checker.check(*reachabilityRewardFormula); result = checker.check(*reachabilityRewardFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(11.0/3.0, quantitativeResult4[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
EXPECT_NEAR(11.0/3.0, quantitativeResult4[0], storm::settings::generalSettings().getPrecision());
} }
TEST(SparseDtmcEliminationModelCheckerTest, Crowds) { TEST(SparseDtmcEliminationModelCheckerTest, Crowds) {
@ -72,7 +71,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Crowds) {
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*eventuallyFormula); std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*eventuallyFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.3328800375801578281, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.3328800375801578281, quantitativeResult1[0], storm::settings::generalSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observeIGreater1"); labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observeIGreater1");
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula); eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
@ -80,7 +79,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Crowds) {
result = checker.check(*eventuallyFormula); result = checker.check(*eventuallyFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.1522194965, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.1522194965, quantitativeResult2[0], storm::settings::generalSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observeOnlyTrueSender"); labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observeOnlyTrueSender");
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula); eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
@ -88,7 +87,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Crowds) {
result = checker.check(*eventuallyFormula); result = checker.check(*eventuallyFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.32153724292835045, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.32153724292835045, quantitativeResult3[0], storm::settings::generalSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observe0Greater1"); labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observe0Greater1");
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula); eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
@ -100,7 +99,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Crowds) {
result = checker.check(*conditionalFormula); result = checker.check(*conditionalFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.15330064292476167, quantitativeResult4[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.15330064292476167, quantitativeResult4[0], storm::settings::generalSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observeOnlyTrueSender"); labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observeOnlyTrueSender");
eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula); eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
@ -112,7 +111,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Crowds) {
result = checker.check(*conditionalFormula); result = checker.check(*conditionalFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.96592521978041668, quantitativeResult5[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.96592521978041668, quantitativeResult5[0], storm::settings::generalSettings().getPrecision());
} }
TEST(SparseDtmcEliminationModelCheckerTest, SynchronousLeader) { TEST(SparseDtmcEliminationModelCheckerTest, SynchronousLeader) {
@ -132,7 +131,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, SynchronousLeader) {
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*eventuallyFormula); std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*eventuallyFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::generalSettings().getPrecision());
labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected"); labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula); auto reachabilityRewardFormula = std::make_shared<storm::logic::ReachabilityRewardFormula>(labelFormula);
@ -140,5 +139,5 @@ TEST(SparseDtmcEliminationModelCheckerTest, SynchronousLeader) {
result = checker.check(*reachabilityRewardFormula); result = checker.check(*reachabilityRewardFormula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0448979, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
EXPECT_NEAR(1.0448979, quantitativeResult3[0], storm::settings::generalSettings().getPrecision());
} }
Write Preview
Loading…
Cancel
Save