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

Added MA test case + fixes

tempestpy_adaptions
Tim Quatmann 4 years ago
parent
5bfb3b132e
commit
c990d27c50
4 changed files with 176 additions and 2 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 22
      resources/examples/testfiles/ma/multiobj_simple_lra.ma
  2. 4
      src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp
  3. 4
      src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
  4. 148
      src/test/storm/modelchecker/multiobjective/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp

22
resources/examples/testfiles/ma/multiobj_simple_lra.ma
View File

@ -0,0 +1,22 @@
ma
module main
x : [0..4];
[a] x=0 -> 0.5 : (x'=1) + 0.5 : (x'=0);
[b] x=0 -> (x'=2);
<> x=1 -> 6 : (x'=2) + 4 : (x'=4);
<> x=2 -> 5 : (x'=2) + 5 : (x'=3);
[c] x=3 -> 0.3 : (x'=2) + 0.7 : (x'=4);
[d] x=3 -> 0.3 : (x'=4) + 0.7 : (x'=2);
<> x=4 -> 5 : (x'=3);
endmodule
rewards "first"
true : 3;
[] x=2 : 10;
[d] true : 5;
endrewards
rewards "second"
x<2 : 42;
endrewards

4
src/storm/modelchecker/multiobjective/pcaa/StandardMaPcaaWeightVectorChecker.cpp
View File

@ -73,7 +73,9 @@ namespace storm {
storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper<typename SparseMdpModelType::ValueType> StandardMaPcaaWeightVectorChecker<SparseMdpModelType>::createDetInfiniteHorizonHelper(storm::storage::SparseMatrix<ValueType> const& transitions) const {
STORM_LOG_ASSERT(transitions.getRowGroupCount() == this->transitionMatrix.getRowGroupCount(), "Unexpected size of given matrix.");
// TODO: Right now, there is no dedicated support for "deterministic" Markov automata so we have to pick the nondeterministic one.
return storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper<ValueType>(transitions, this->markovianStates, this->exitRates);
auto result = storm::modelchecker::helper::SparseNondeterministicInfiniteHorizonHelper<ValueType>(transitions, this->markovianStates, this->exitRates);
result.setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);
return result;
}
template <class SparseMaModelType>

4
src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
View File

@ -118,7 +118,9 @@ namespace storm {
ValueType weight = storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType()) ? -weightVector[objIndex] : weightVector[objIndex];
storm::utility::vector::addScaledVector(weightedRewardVector, actionRewards[objIndex], weight);
if (!stateRewards.empty() && !stateRewards[objIndex].empty()) {
weightedStateRewardVector->resize(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
if (!weightedStateRewardVector) {
weightedStateRewardVector = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
}
storm::utility::vector::addScaledVector(weightedStateRewardVector.get(), stateRewards[objIndex], weight);
}
}

148
src/test/storm/modelchecker/multiobjective/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp
View File

@ -213,4 +213,152 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_pareto_2Obj) {
}
template <typename ValueType>
bool expectPointConained(std::vector<std::vector<ValueType>> const& pointset, std::vector<ValueType> const& point, ValueType precision) {
for (auto const& p : pointset) {
EXPECT_EQ(p.size(), point.size()) << "Missmatch in point dimension.";
bool found = true;
for (uint64_t i = 0; i < p.size(); ++i) {
if (storm::utility::abs<ValueType>(p[i] - point[i]) > precision) {
found = false;
break;
}
}
if (found) {
return true;
}
}
// prepare failure message:
std::stringstream errstr;
errstr << "Point [";
bool firstPi = true;
for (auto const& pi : point) {
if (firstPi) {
firstPi = false;
} else {
errstr << ", ";
}
errstr << pi;
}
errstr << "] is not contained in point set {";
bool firstP = true;
for (auto const& p : pointset) {
if (firstP) {
firstP = false;
} else {
errstr << ", \t";
}
errstr << "[";
firstPi = true;
for (auto const& pi : p) {
if (firstPi) {
firstPi = false;
} else {
errstr << ", ";
}
errstr << pi;
}
errstr << "]";
}
errstr << "}.";
ADD_FAILURE() << errstr.str();
return false;
}
template <typename ValueType>
bool expectSubset(std::vector<std::vector<ValueType>> const& lhs, std::vector<std::vector<ValueType>> const& rhs, ValueType precision) {
for (auto const& p : lhs) {
if (!expectPointConained(rhs, p, precision)) {
return false;
}
}
return true;
}
template <typename ValueType>
std::vector<std::vector<ValueType>> convertPointset(std::vector<std::vector<std::string>> const& in) {
std::vector<std::vector<ValueType>> out;
for (auto const& point_str : in) {
out.emplace_back();
for (auto const& pi_str : point_str) {
out.back().push_back(storm::utility::convertNumber<ValueType>(pi_str));
}
}
return out;
}
TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, simple_lra) {
if (!storm::test::z3AtLeastVersion(4,8,5)) {
GTEST_SKIP() << "Test disabled since it triggers a bug in the installed version of z3.";
}
storm::Environment env;
env.modelchecker().multi().setMethod(storm::modelchecker::multiobjective::MultiObjectiveMethod::Pcaa);
std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/multiobj_simple_lra.ma";
std::string formulasAsString = "multi(R{\"first\"}max=? [LRA], LRAmax=? [ x=4 ] );\n"; // pareto
formulasAsString += "multi(R{\"first\"}max=? [LRA], LRAmin=? [ x=4] );\n"; // pareto
formulasAsString += "multi(R{\"first\"}max=? [LRA], LRAmin=? [ x=4] , R{\"second\"}max=? [LRA]);\n"; // pareto
formulasAsString += "multi(R{\"first\"}max=? [LRA], LRAmax=? [ x=4] , R{\"second\"}max=? [C]);\n"; // pareto
formulasAsString += "multi(R{\"first\"}max=? [LRA], LRAmax=? [ x=4] , R{\"second\"}min=? [C]);\n"; // pareto
// programm, model, formula
storm::prism::Program program = storm::api::parseProgram(programFile);
program.checkValidity();
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
storm::generator::NextStateGeneratorOptions options(formulas);
auto ma = storm::builder::ExplicitModelBuilder<double>(program, options).build()->as<storm::models::sparse::MarkovAutomaton<double>>();
{
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[0]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
std::vector<std::vector<std::string>> expectedPoints;
expectedPoints.emplace_back(std::vector<std::string>({"98","3/10"}));
expectedPoints.emplace_back(std::vector<std::string>({"33","7/10"}));
double eps = 1e-4;
EXPECT_TRUE(expectSubset(result->asExplicitParetoCurveCheckResult<double>().getPoints(), convertPointset<double>(expectedPoints), eps)) << "Non-Pareto point found.";
EXPECT_TRUE(expectSubset(convertPointset<double>(expectedPoints), result->asExplicitParetoCurveCheckResult<double>().getPoints(), eps)) << "Pareto point missing.";
}
{
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[1]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
std::vector<std::vector<std::string>> expectedPoints;
expectedPoints.emplace_back(std::vector<std::string>({"98","3/10"}));
double eps = 1e-4;
EXPECT_TRUE(expectSubset(result->asExplicitParetoCurveCheckResult<double>().getPoints(), convertPointset<double>(expectedPoints), eps)) << "Non-Pareto point found.";
EXPECT_TRUE(expectSubset(convertPointset<double>(expectedPoints), result->asExplicitParetoCurveCheckResult<double>().getPoints(), eps)) << "Pareto point missing.";
}
{
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[2]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
std::vector<std::vector<std::string>> expectedPoints;
expectedPoints.emplace_back(std::vector<std::string>({"98","3/10", "0"}));
double eps = 1e-4;
EXPECT_TRUE(expectSubset(result->asExplicitParetoCurveCheckResult<double>().getPoints(), convertPointset<double>(expectedPoints), eps)) << "Non-Pareto point found.";
EXPECT_TRUE(expectSubset(convertPointset<double>(expectedPoints), result->asExplicitParetoCurveCheckResult<double>().getPoints(), eps)) << "Pareto point missing.";
}
{
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[3]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
std::vector<std::vector<std::string>> expectedPoints;
expectedPoints.emplace_back(std::vector<std::string>({"98", "3/10", "42/10"}));
expectedPoints.emplace_back(std::vector<std::string>({"33", "7/10", "42/10"}));
double eps = 1e-4;
EXPECT_TRUE(expectSubset(result->asExplicitParetoCurveCheckResult<double>().getPoints(), convertPointset<double>(expectedPoints), eps)) << "Non-Pareto point found.";
EXPECT_TRUE(expectSubset(convertPointset<double>(expectedPoints), result->asExplicitParetoCurveCheckResult<double>().getPoints(), eps)) << "Pareto point missing.";
}
{
std::unique_ptr<storm::modelchecker::CheckResult> result = storm::modelchecker::multiobjective::performMultiObjectiveModelChecking(env, *ma, formulas[4]->asMultiObjectiveFormula());
ASSERT_TRUE(result->isExplicitParetoCurveCheckResult());
std::vector<std::vector<std::string>> expectedPoints;
expectedPoints.emplace_back(std::vector<std::string>({"98", "3/10", "0"}));
expectedPoints.emplace_back(std::vector<std::string>({"33", "7/10", "0"}));
double eps = 1e-4;
EXPECT_TRUE(expectSubset(result->asExplicitParetoCurveCheckResult<double>().getPoints(), convertPointset<double>(expectedPoints), eps)) << "Non-Pareto point found.";
EXPECT_TRUE(expectSubset(convertPointset<double>(expectedPoints), result->asExplicitParetoCurveCheckResult<double>().getPoints(), eps)) << "Pareto point missing.";
}
}
#endif /* defined STORM_HAVE_HYPRO || defined STORM_HAVE_Z3_OPTIMIZE */
Write Preview
Loading…
Cancel
Save