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

LraMdpPrctlModelCheckerTest: Test LRA computation for different environments. Added a testcase.

tempestpy_adaptions
Tim Quatmann 5 years ago
parent
48dbaa6fbd
commit
c1b3a4f991
6 changed files with 550 additions and 333 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. 74
      resources/examples/testfiles/mdp/cs_nfail3.nm
  2. 17
      src/storm/environment/solver/MinMaxSolverEnvironment.cpp
  3. 5
      src/storm/environment/solver/MinMaxSolverEnvironment.h
  4. 7
      src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
  5. 8
      src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
  6. 772
      src/test/storm/modelchecker/LraMdpPrctlModelCheckerTest.cpp

74
resources/examples/testfiles/mdp/cs_nfail3.nm
View File

@ -0,0 +1,74 @@
mdp
module server
s:[0..3];
i:[0..3];
j:[0..3];
// initial cancel loops
[client1_cancel] s=0 -> true;
[client2_cancel] s=0 -> true;
[client3_cancel] s=0 -> true;
// client i request/grant/cancel
[client1_request] s=0 -> (s'=1) & (i'=1);
[client1_grant] s=1 & i=1 -> (s'=2);
[client1_cancel] s=2 & i=1 -> (s'=0) & (i'=0);
[client2_request] s=0 -> (s'=1) & (i'=2);
[client2_grant] s=1 & i=2 -> (s'=2);
[client2_cancel] s=2 & i=2 -> (s'=0) & (i'=0);
[client3_request] s=0 -> (s'=1) & (i'=3);
[client3_grant] s=1 & i=3 -> (s'=2);
[client3_cancel] s=2 & i=3 -> (s'=0) & (i'=0);
// deny other requests when serving
[client1_request] s=2 -> (s'=3) & (j'=1);
[client1_deny] s=3 & j=1 -> (s'=2) & (j'=0);
[client2_request] s=2 -> (s'=3) & (j'=2);
[client2_deny] s=3 & j=2 -> (s'=2) & (j'=0);
[client3_request] s=2 -> (s'=3) & (j'=3);
[client3_deny] s=3 & j=3 -> (s'=2) & (j'=0);
// cancel loops when serving
[client1_cancel] s=2 & i!=1 -> true;
[client2_cancel] s=2 & i!=2 -> true;
[client3_cancel] s=2 & i!=3 -> true;
endmodule
module client1
c1:[-1..3];
[client1_ch_mind] c1=-1 -> 0.9:(c1'=0)+0.1:(c1'=3);
// change mind with probability 0.1
[client1_request] c1=0 -> (c1'=1);
[client1_deny] c1=1 -> (c1'=0);
[client1_grant] c1=1 -> (c1'=2);
[client1_useResource] c1=2 -> (c1'=2);
[client1_cancel] c1=2 -> (c1'=0);
[client1_cancel] c1=3 -> (c1'=1);
endmodule
module client2 = client1[ c1=c2, client1_ch_mind=client2_ch_mind, client1_request=client2_request,
client1_deny=client2_deny, client1_grant=client2_grant,
client1_useResource=client2_useResource, client1_cancel=client2_cancel]
endmodule
module client3 = client1[ c1=c3, client1_ch_mind=client3_ch_mind, client1_request=client3_request,
client1_deny=client3_deny, client1_grant=client3_grant,
client1_useResource=client3_useResource, client1_cancel=client3_cancel]
endmodule
rewards "grants"
[client1_grant] true : 1;
[client2_grant] true : 1;
[client3_grant] true : 1;
endrewards

17
src/storm/environment/solver/MinMaxSolverEnvironment.cpp
View File

@ -22,6 +22,8 @@ namespace storm {
STORM_LOG_ASSERT(considerRelativeTerminationCriterion || minMaxSettings.getConvergenceCriterion() == storm::settings::modules::MinMaxEquationSolverSettings::ConvergenceCriterion::Absolute, "Unknown convergence criterion"); STORM_LOG_ASSERT(considerRelativeTerminationCriterion || minMaxSettings.getConvergenceCriterion() == storm::settings::modules::MinMaxEquationSolverSettings::ConvergenceCriterion::Absolute, "Unknown convergence criterion");
multiplicationStyle = minMaxSettings.getValueIterationMultiplicationStyle(); multiplicationStyle = minMaxSettings.getValueIterationMultiplicationStyle();
symmetricUpdates = minMaxSettings.isForceIntervalIterationSymmetricUpdatesSet(); symmetricUpdates = minMaxSettings.isForceIntervalIterationSymmetricUpdatesSet();
lraMethod = minMaxSettings.getLraMethod();
lraMethodSetFromDefault = minMaxSettings.isLraMethodSetFromDefaultValue();
} }
MinMaxSolverEnvironment::~MinMaxSolverEnvironment() { MinMaxSolverEnvironment::~MinMaxSolverEnvironment() {
@ -81,4 +83,19 @@ namespace storm {
symmetricUpdates = value; symmetricUpdates = value;
} }
storm::solver::LraMethod const& MinMaxSolverEnvironment::getLraMethod() const {
return lraMethod;
}
bool const& MinMaxSolverEnvironment::isLraMethodSetFromDefault() const {
return lraMethodSetFromDefault;
}
void MinMaxSolverEnvironment::setLraMethod(storm::solver::LraMethod value, bool isSetFromDefault) {
lraMethod = value;
lraMethodSetFromDefault = isSetFromDefault;
}
} }

5
src/storm/environment/solver/MinMaxSolverEnvironment.h
View File

@ -27,6 +27,9 @@ namespace storm {
void setMultiplicationStyle(storm::solver::MultiplicationStyle value); void setMultiplicationStyle(storm::solver::MultiplicationStyle value);
bool isSymmetricUpdatesSet() const; bool isSymmetricUpdatesSet() const;
void setSymmetricUpdates(bool value); void setSymmetricUpdates(bool value);
storm::solver::LraMethod const& getLraMethod() const;
bool const& isLraMethodSetFromDefault() const;
void setLraMethod(storm::solver::LraMethod value, bool isSetFromDefault = false);
private: private:
storm::solver::MinMaxMethod minMaxMethod; storm::solver::MinMaxMethod minMaxMethod;
@ -36,6 +39,8 @@ namespace storm {
bool considerRelativeTerminationCriterion; bool considerRelativeTerminationCriterion;
storm::solver::MultiplicationStyle multiplicationStyle; storm::solver::MultiplicationStyle multiplicationStyle;
bool symmetricUpdates; bool symmetricUpdates;
storm::solver::LraMethod lraMethod;
bool lraMethodSetFromDefault;
}; };
} }

7
src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
View File

@ -877,12 +877,11 @@ namespace storm {
} }
// Solve MEC with the method specified in the settings // Solve MEC with the method specified in the settings
auto minMaxSettings = storm::settings::getModule<storm::settings::modules::MinMaxEquationSolverSettings>();
storm::solver::LraMethod method = minMaxSettings.getLraMethod();
if (storm::NumberTraits<ValueType>::IsExact && minMaxSettings.isLraMethodSetFromDefaultValue() && method != storm::solver::LraMethod::LinearProgramming) {
storm::solver::LraMethod method = env.solver().minMax().getLraMethod();
if (storm::NumberTraits<ValueType>::IsExact && env.solver().minMax().isLraMethodSetFromDefault() && method != storm::solver::LraMethod::LinearProgramming) {
STORM_LOG_INFO("Selecting 'LP' as the solution technique for long-run properties to guarantee exact results. If you want to override this, please explicitly specify a different LRA method."); STORM_LOG_INFO("Selecting 'LP' as the solution technique for long-run properties to guarantee exact results. If you want to override this, please explicitly specify a different LRA method.");
method = storm::solver::LraMethod::LinearProgramming; method = storm::solver::LraMethod::LinearProgramming;
} else if (env.solver().isForceSoundness() && minMaxSettings.isLraMethodSetFromDefaultValue() && method != storm::solver::LraMethod::ValueIteration) {
} else if (env.solver().isForceSoundness() && env.solver().minMax().isLraMethodSetFromDefault() && method != storm::solver::LraMethod::ValueIteration) {
STORM_LOG_INFO("Selecting 'VI' as the solution technique for long-run properties to guarantee sound results. If you want to override this, please explicitly specify a different LRA method."); STORM_LOG_INFO("Selecting 'VI' as the solution technique for long-run properties to guarantee sound results. If you want to override this, please explicitly specify a different LRA method.");
method = storm::solver::LraMethod::ValueIteration; method = storm::solver::LraMethod::ValueIteration;
} }

8
src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
View File

@ -26,7 +26,6 @@
#include "storm/settings/SettingsManager.h" #include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/ModelCheckerSettings.h" #include "storm/settings/modules/ModelCheckerSettings.h"
#include "storm/settings/modules/MinMaxEquationSolverSettings.h"
#include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/GeneralSettings.h"
#include "storm/settings/modules/CoreSettings.h" #include "storm/settings/modules/CoreSettings.h"
#include "storm/settings/modules/IOSettings.h" #include "storm/settings/modules/IOSettings.h"
@ -1410,12 +1409,11 @@ namespace storm {
} }
// Solve MEC with the method specified in the settings // Solve MEC with the method specified in the settings
auto minMaxSettings = storm::settings::getModule<storm::settings::modules::MinMaxEquationSolverSettings>();
storm::solver::LraMethod method = minMaxSettings.getLraMethod();
if (storm::NumberTraits<ValueType>::IsExact && minMaxSettings.isLraMethodSetFromDefaultValue() && method != storm::solver::LraMethod::LinearProgramming) {
storm::solver::LraMethod method = env.solver().minMax().getLraMethod();
if (storm::NumberTraits<ValueType>::IsExact && env.solver().minMax().isLraMethodSetFromDefault() && method != storm::solver::LraMethod::LinearProgramming) {
STORM_LOG_INFO("Selecting 'LP' as the solution technique for long-run properties to guarantee exact results. If you want to override this, please explicitly specify a different LRA method."); STORM_LOG_INFO("Selecting 'LP' as the solution technique for long-run properties to guarantee exact results. If you want to override this, please explicitly specify a different LRA method.");
method = storm::solver::LraMethod::LinearProgramming; method = storm::solver::LraMethod::LinearProgramming;
} else if (env.solver().isForceSoundness() && minMaxSettings.isLraMethodSetFromDefaultValue() && method != storm::solver::LraMethod::ValueIteration) {
} else if (env.solver().isForceSoundness() && env.solver().minMax().isLraMethodSetFromDefault() && method != storm::solver::LraMethod::ValueIteration) {
STORM_LOG_INFO("Selecting 'VI' as the solution technique for long-run properties to guarantee sound results. If you want to override this, please explicitly specify a different LRA method."); STORM_LOG_INFO("Selecting 'VI' as the solution technique for long-run properties to guarantee sound results. If you want to override this, please explicitly specify a different LRA method.");
method = storm::solver::LraMethod::ValueIteration; method = storm::solver::LraMethod::ValueIteration;
} }

772
src/test/storm/modelchecker/LraMdpPrctlModelCheckerTest.cpp
View File

@ -1,6 +1,15 @@
#include "gtest/gtest.h" #include "gtest/gtest.h"
#include "test/storm_gtest.h"
#include "storm-config.h" #include "storm-config.h"
#include "storm/api/builder.h"
#include "storm-conv/api/storm-conv.h"
#include "storm-parsers/api/model_descriptions.h"
#include "storm/api/properties.h"
#include "storm-parsers/api/properties.h"
#include "storm-parsers/parser/FormulaParser.h" #include "storm-parsers/parser/FormulaParser.h"
#include "storm/logic/Formulas.h" #include "storm/logic/Formulas.h"
#include "storm/solver/StandardMinMaxLinearEquationSolver.h" #include "storm/solver/StandardMinMaxLinearEquationSolver.h"
@ -13,332 +22,447 @@
#include "storm/settings/modules/NativeEquationSolverSettings.h" #include "storm/settings/modules/NativeEquationSolverSettings.h"
#include "storm-parsers/parser/AutoParser.h" #include "storm-parsers/parser/AutoParser.h"
TEST(LraMdpPrctlModelCheckerTest, LRA_SingleMec) {
storm::storage::SparseMatrixBuilder<double> matrixBuilder;
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp;
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
{
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);
mdp.reset(new storm::models::sparse::Mdp<double>(transitionMatrix, ap));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(.5, quantitativeResult1[1], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(.5, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(.5, quantitativeResult2[1], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
namespace {
class SparseValueTypeValueIterationEnvironment {
public:
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::sparse::Mdp<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setLraMethod(storm::solver::LraMethod::ValueIteration);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
return env;
}
};
class SparseValueTypeLinearProgrammingEnvironment {
public:
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::sparse::Mdp<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setLraMethod(storm::solver::LraMethod::LinearProgramming);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
return env;
}
};
class SparseRationalLinearProgrammingEnvironment {
public:
static const bool isExact = true;
typedef storm::RationalNumber ValueType;
typedef storm::models::sparse::Mdp<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setLraMethod(storm::solver::LraMethod::LinearProgramming);
return env;
}
};
template<typename TestType>
class LraMdpPrctlModelCheckerTest : public ::testing::Test {
public:
typedef typename TestType::ValueType ValueType;
typedef typename storm::models::sparse::Mdp<ValueType> SparseModelType;
LraMdpPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
storm::Environment const& env() const { return _environment; }
ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber<ValueType>(input);}
ValueType precision() const { return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");}
bool isSparseModel() const { return std::is_same<typename TestType::ModelType, SparseModelType>::value; }
std::pair<std::shared_ptr<SparseModelType>, std::vector<std::shared_ptr<storm::logic::Formula const>>> buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
std::pair<std::shared_ptr<SparseModelType>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
storm::prism::Program program = storm::api::parseProgram(pathToPrismFile);
program = storm::utility::prism::preprocess(program, constantDefinitionString);
result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<SparseModelType>();
return result;
}
std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> getTasks(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) const {
std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> result;
for (auto const& f : formulas) {
result.emplace_back(*f);
}
return result;
}
private:
storm::Environment _environment;
};
typedef ::testing::Types<
SparseValueTypeValueIterationEnvironment,
SparseValueTypeLinearProgrammingEnvironment
#ifdef STORM_HAVE_Z3_OPTIMIZE
, SparseRationalLinearProgrammingEnvironment
#endif
> TestingTypes;
TYPED_TEST_CASE(LraMdpPrctlModelCheckerTest, TestingTypes);
TYPED_TEST(LraMdpPrctlModelCheckerTest, LRA_SingleMec) {
typedef typename TestFixture::ValueType ValueType;
storm::storage::SparseMatrixBuilder<ValueType> matrixBuilder;
std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp;
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
{
matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(2, 2, 2);
matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
matrixBuilder.addNextValue(1, 0, this->parseNumber("1"));
storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
storm::models::sparse::StateLabeling ap(2);
ap.addLabel("a");
ap.addLabelToState("a", 1);
mdp.reset(new storm::models::sparse::Mdp<ValueType>(transitionMatrix, ap));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision());
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[1], this->precision());
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult2[0], this->precision());
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult2[1], this->precision());
}
{
matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(2, 2, 4);
matrixBuilder.addNextValue(0, 0, this->parseNumber("0.5"));
matrixBuilder.addNextValue(0, 1, this->parseNumber("0.5"));
matrixBuilder.addNextValue(1, 0, this->parseNumber("0.5"));
matrixBuilder.addNextValue(1, 1, this->parseNumber("0.5"));
storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
storm::models::sparse::StateLabeling ap(2);
ap.addLabel("a");
ap.addLabelToState("a", 1);
mdp.reset(new storm::models::sparse::Mdp<ValueType>(transitionMatrix, ap));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision());
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[1], this->precision());
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult2[0], this->precision());
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult2[1], this->precision());
}
{
matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(4, 3, 4, true, true, 3);
matrixBuilder.newRowGroup(0);
matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
matrixBuilder.newRowGroup(1);
matrixBuilder.addNextValue(1, 0, this->parseNumber("1"));
matrixBuilder.addNextValue(2, 2, this->parseNumber("1"));
matrixBuilder.newRowGroup(3);
matrixBuilder.addNextValue(3, 0, this->parseNumber("1"));
storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
storm::models::sparse::StateLabeling ap(3);
ap.addLabel("a");
ap.addLabelToState("a", 2);
ap.addLabel("b");
ap.addLabelToState("b", 0);
ap.addLabel("c");
ap.addLabelToState("c", 0);
ap.addLabelToState("c", 2);
mdp.reset(new storm::models::sparse::Mdp<ValueType>(transitionMatrix, ap));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[0], this->precision());
EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[1], this->precision());
EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[2], this->precision());
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[0], this->precision());
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[1], this->precision());
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[2], this->precision());
formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"b\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult3[0], this->precision());
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult3[1], this->precision());
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult3[2], this->precision());
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"b\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult4[0], this->precision());
EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult4[1], this->precision());
EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult4[2], this->precision());
formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"c\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("2/3"), quantitativeResult5[0], this->precision());
EXPECT_NEAR(this->parseNumber("2/3"), quantitativeResult5[1], this->precision());
EXPECT_NEAR(this->parseNumber("2/3"), quantitativeResult5[2], this->precision());
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"c\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult6[0], this->precision());
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult6[1], this->precision());
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult6[2], this->precision());
}
} }
{
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);
mdp.reset(new storm::models::sparse::Mdp<double>(transitionMatrix, ap));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(.5, quantitativeResult1[1], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(.5, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(.5, quantitativeResult2[1], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
TYPED_TEST(LraMdpPrctlModelCheckerTest, LRA) {
typedef typename TestFixture::ValueType ValueType;
storm::storage::SparseMatrixBuilder<ValueType> matrixBuilder;
std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp;
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
{
matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(4, 3, 4, true, true, 3);
matrixBuilder.newRowGroup(0);
matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
matrixBuilder.newRowGroup(1);
matrixBuilder.addNextValue(1, 1, this->parseNumber("1"));
matrixBuilder.addNextValue(2, 2, this->parseNumber("1"));
matrixBuilder.newRowGroup(3);
matrixBuilder.addNextValue(3, 2, this->parseNumber("1"));
storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
storm::models::sparse::StateLabeling ap(3);
ap.addLabel("a");
ap.addLabelToState("a", 0);
ap.addLabel("b");
ap.addLabelToState("b", 1);
ap.addLabel("c");
ap.addLabelToState("c", 2);
mdp.reset(new storm::models::sparse::Mdp<ValueType>(transitionMatrix, ap));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[0], this->precision());
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[1], this->precision());
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[2], this->precision());
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[0], this->precision());
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[1], this->precision());
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[2], this->precision());
formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"b\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("1"), quantitativeResult3[0], this->precision());
EXPECT_NEAR(this->parseNumber("1"), quantitativeResult3[1], this->precision());
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult3[2], this->precision());
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"b\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult4[0], this->precision());
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult4[1], this->precision());
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult4[2], this->precision());
formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"c\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("1"), quantitativeResult5[0], this->precision());
EXPECT_NEAR(this->parseNumber("1"), quantitativeResult5[1], this->precision());
EXPECT_NEAR(this->parseNumber("1"), quantitativeResult5[2], this->precision());
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"c\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult6[0], this->precision());
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult6[1], this->precision());
EXPECT_NEAR(this->parseNumber("1"), quantitativeResult6[2], this->precision());
}
{
matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(22, 15, 28, true, true, 15);
matrixBuilder.newRowGroup(0);
matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
matrixBuilder.newRowGroup(1);
matrixBuilder.addNextValue(1, 0, this->parseNumber("1"));
matrixBuilder.addNextValue(2, 2, this->parseNumber("1"));
matrixBuilder.addNextValue(3, 4, this->parseNumber("0.7"));
matrixBuilder.addNextValue(3, 6, this->parseNumber("0.3"));
matrixBuilder.newRowGroup(4);
matrixBuilder.addNextValue(4, 0, this->parseNumber("1"));
matrixBuilder.newRowGroup(5);
matrixBuilder.addNextValue(5, 4, this->parseNumber("1"));
matrixBuilder.addNextValue(6, 5, this->parseNumber("0.8"));
matrixBuilder.addNextValue(6, 9, this->parseNumber("0.2"));
matrixBuilder.newRowGroup(7);
matrixBuilder.addNextValue(7, 3, this->parseNumber("1"));
matrixBuilder.addNextValue(8, 5, this->parseNumber("1"));
matrixBuilder.newRowGroup(9);
matrixBuilder.addNextValue(9, 3, this->parseNumber("1"));
matrixBuilder.newRowGroup(10);
matrixBuilder.addNextValue(10, 7, this->parseNumber("1"));
matrixBuilder.newRowGroup(11);
matrixBuilder.addNextValue(11, 6, this->parseNumber("1"));
matrixBuilder.addNextValue(12, 8, this->parseNumber("1"));
matrixBuilder.newRowGroup(13);
matrixBuilder.addNextValue(13, 6, this->parseNumber("1"));
matrixBuilder.newRowGroup(14);
matrixBuilder.addNextValue(14, 10, this->parseNumber("1"));
matrixBuilder.newRowGroup(15);
matrixBuilder.addNextValue(15, 9, this->parseNumber("1"));
matrixBuilder.addNextValue(16, 11, this->parseNumber("1"));
matrixBuilder.newRowGroup(17);
matrixBuilder.addNextValue(17, 9, this->parseNumber("1"));
matrixBuilder.newRowGroup(18);
matrixBuilder.addNextValue(18, 5, this->parseNumber("0.4"));
matrixBuilder.addNextValue(18, 8, this->parseNumber("0.3"));
matrixBuilder.addNextValue(18, 11, this->parseNumber("0.3"));
matrixBuilder.newRowGroup(19);
matrixBuilder.addNextValue(19, 7, this->parseNumber("0.7"));
matrixBuilder.addNextValue(19, 12, this->parseNumber("0.3"));
matrixBuilder.newRowGroup(20);
matrixBuilder.addNextValue(20, 12, this->parseNumber("0.1"));
matrixBuilder.addNextValue(20, 13, this->parseNumber("0.9"));
matrixBuilder.addNextValue(21, 12, this->parseNumber("1"));
storm::storage::SparseMatrix<ValueType> 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::Mdp<ValueType>(transitionMatrix, ap));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("37 / 60"), quantitativeResult1[0], this->precision());
EXPECT_NEAR(this->parseNumber("2/3"), quantitativeResult1[3], this->precision());
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[6], this->precision());
EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[9], this->precision());
EXPECT_NEAR(this->parseNumber("31 / 60"), quantitativeResult1[12], this->precision());
EXPECT_NEAR(this->parseNumber("101 / 200"), quantitativeResult1[13], this->precision());
EXPECT_NEAR(this->parseNumber("31 / 60"), quantitativeResult1[14], this->precision());
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("0.1"), quantitativeResult2[0], this->precision());
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[3], this->precision());
EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult2[6], this->precision());
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[9], this->precision());
EXPECT_NEAR(this->parseNumber("0.1"), quantitativeResult2[12], this->precision());
EXPECT_NEAR(this->parseNumber("79 / 300"), quantitativeResult2[13], this->precision());
EXPECT_NEAR(this->parseNumber("0.1"), quantitativeResult2[14], this->precision());
}
} }
{
matrixBuilder = storm::storage::SparseMatrixBuilder<double>(4, 3, 4, true, true, 3);
matrixBuilder.newRowGroup(0);
matrixBuilder.addNextValue(0, 1, 1);
matrixBuilder.newRowGroup(1);
matrixBuilder.addNextValue(1, 0, 1);
matrixBuilder.addNextValue(2, 2, 1);
matrixBuilder.newRowGroup(3);
matrixBuilder.addNextValue(3, 0, 1);
storm::storage::SparseMatrix<double> transitionMatrix = matrixBuilder.build();
storm::models::sparse::StateLabeling ap(3);
ap.addLabel("a");
ap.addLabelToState("a", 2);
ap.addLabel("b");
ap.addLabelToState("b", 0);
ap.addLabel("c");
ap.addLabelToState("c", 0);
ap.addLabelToState("c", 2);
mdp.reset(new storm::models::sparse::Mdp<double>(transitionMatrix, ap));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1. / 3., quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(1. / 3., quantitativeResult1[1], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(1. / 3., quantitativeResult1[2], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0.0, quantitativeResult2[1], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0.0, quantitativeResult2[2], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"b\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.5, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0.5, quantitativeResult3[1], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0.5, quantitativeResult3[2], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"b\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1. / 3., quantitativeResult4[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(1. / 3., quantitativeResult4[1], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(1. / 3., quantitativeResult4[2], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"c\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(2. / 3., quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(2. / 3., quantitativeResult5[1], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(2. / 3., quantitativeResult5[2], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"c\"]");
TYPED_TEST(LraMdpPrctlModelCheckerTest, cs_nfail) {
typedef typename TestFixture::ValueType ValueType;
std::string formulasString = "R{\"grants\"}max=? [ MP ]";
auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/cs_nfail3.nm", formulasString);
auto model = std::move(modelFormulas.first);
auto tasks = this->getTasks(modelFormulas.second);
EXPECT_EQ(184ul, model->getNumberOfStates());
EXPECT_EQ(541ul, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
auto mdp = model->template as<storm::models::sparse::Mdp<ValueType>>();
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
std::unique_ptr<storm::modelchecker::CheckResult> result;
result = checker.check(this->env(), tasks[0]);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("333/1000"), quantitativeResult[*mdp->getInitialStates().begin()], this->precision());
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.5, quantitativeResult6[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0.5, quantitativeResult6[1], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0.5, quantitativeResult6[2], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
}
}
TEST(LraMdpPrctlModelCheckerTest, LRA) {
storm::storage::SparseMatrixBuilder<double> matrixBuilder;
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp;
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
{
matrixBuilder = storm::storage::SparseMatrixBuilder<double>(4, 3, 4, true, true, 3);
matrixBuilder.newRowGroup(0);
matrixBuilder.addNextValue(0, 1, 1);
matrixBuilder.newRowGroup(1);
matrixBuilder.addNextValue(1, 1, 1);
matrixBuilder.addNextValue(2, 2, 1);
matrixBuilder.newRowGroup(3);
matrixBuilder.addNextValue(3, 2, 1);
storm::storage::SparseMatrix<double> transitionMatrix = matrixBuilder.build();
storm::models::sparse::StateLabeling ap(3);
ap.addLabel("a");
ap.addLabelToState("a", 0);
ap.addLabel("b");
ap.addLabelToState("b", 1);
ap.addLabel("c");
ap.addLabelToState("c", 2);
mdp.reset(new storm::models::sparse::Mdp<double>(transitionMatrix, ap));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0.0, quantitativeResult1[1], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0.0, quantitativeResult1[2], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0.0, quantitativeResult2[1], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0.0, quantitativeResult2[2], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"b\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(1.0, quantitativeResult3[1], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0.0, quantitativeResult3[2], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"b\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult4[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0.0, quantitativeResult4[1], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0.0, quantitativeResult4[2], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"c\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(1.0, quantitativeResult5[1], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(1.0, quantitativeResult5[2], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"c\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0, quantitativeResult6[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0.0, quantitativeResult6[1], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(1.0, quantitativeResult6[2], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
} }
{
matrixBuilder = storm::storage::SparseMatrixBuilder<double>(22, 15, 28, true, true, 15);
matrixBuilder.newRowGroup(0);
matrixBuilder.addNextValue(0, 1, 1);
matrixBuilder.newRowGroup(1);
matrixBuilder.addNextValue(1, 0, 1);
matrixBuilder.addNextValue(2, 2, 1);
matrixBuilder.addNextValue(3, 4, 0.7);
matrixBuilder.addNextValue(3, 6, 0.3);
matrixBuilder.newRowGroup(4);
matrixBuilder.addNextValue(4, 0, 1);
matrixBuilder.newRowGroup(5);
matrixBuilder.addNextValue(5, 4, 1);
matrixBuilder.addNextValue(6, 5, 0.8);
matrixBuilder.addNextValue(6, 9, 0.2);
matrixBuilder.newRowGroup(7);
matrixBuilder.addNextValue(7, 3, 1);
matrixBuilder.addNextValue(8, 5, 1);
matrixBuilder.newRowGroup(9);
matrixBuilder.addNextValue(9, 3, 1);
matrixBuilder.newRowGroup(10);
matrixBuilder.addNextValue(10, 7, 1);
matrixBuilder.newRowGroup(11);
matrixBuilder.addNextValue(11, 6, 1);
matrixBuilder.addNextValue(12, 8, 1);
matrixBuilder.newRowGroup(13);
matrixBuilder.addNextValue(13, 6, 1);
matrixBuilder.newRowGroup(14);
matrixBuilder.addNextValue(14, 10, 1);
matrixBuilder.newRowGroup(15);
matrixBuilder.addNextValue(15, 9, 1);
matrixBuilder.addNextValue(16, 11, 1);
matrixBuilder.newRowGroup(17);
matrixBuilder.addNextValue(17, 9, 1);
matrixBuilder.newRowGroup(18);
matrixBuilder.addNextValue(18, 5, 0.4);
matrixBuilder.addNextValue(18, 8, 0.3);
matrixBuilder.addNextValue(18, 11, 0.3);
matrixBuilder.newRowGroup(19);
matrixBuilder.addNextValue(19, 7, 0.7);
matrixBuilder.addNextValue(19, 12, 0.3);
matrixBuilder.newRowGroup(20);
matrixBuilder.addNextValue(20, 12, 0.1);
matrixBuilder.addNextValue(20, 13, 0.9);
matrixBuilder.addNextValue(21, 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::Mdp<double>(transitionMatrix, ap));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(37. / 60., quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(2. / 3., quantitativeResult1[3], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0.5, quantitativeResult1[6], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(1. / 3., quantitativeResult1[9], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(31. / 60., quantitativeResult1[12], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(101. / 200., quantitativeResult1[13], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(31. / 60., quantitativeResult1[14], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.3 / 3., quantitativeResult2[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0.0, quantitativeResult2[3], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(1. / 3., quantitativeResult2[6], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0.0, quantitativeResult2[9], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0.3 / 3., quantitativeResult2[12], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(.79 / 3., quantitativeResult2[13], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(0.3 / 3., quantitativeResult2[14], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
}
}
}
Write Preview
Loading…
Cancel
Save