From c55e4920b268eb99939f2fe35227b342378fbfa8 Mon Sep 17 00:00:00 2001 From: lukpo Date: Fri, 27 Aug 2021 10:28:05 +0200 Subject: [PATCH] WIP created ShieldGenerationSmgRpatlModelCheckerTest.cpp for testing the generation of shielding files for SMGs --- ...ieldGenerationSmgRpatlModelCheckerTest.cpp | 137 ++++++++++++++++++ 1 file changed, 137 insertions(+) create mode 100644 src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp diff --git a/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp new file mode 100644 index 000000000..037af55d7 --- /dev/null +++ b/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp @@ -0,0 +1,137 @@ +#include +#include "test/storm_gtest.h" +#include "storm-config.h" + +#include "storm/api/builder.h" +#include "storm-parsers/api/model_descriptions.h" +#include "storm/api/properties.h" +#include "storm-parsers/api/properties.h" + +#include "storm/models/sparse/Smg.h" +#include "storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h" +#include "storm/modelchecker/results/QuantitativeCheckResult.h" +#include "storm/modelchecker/results/QualitativeCheckResult.h" +#include "storm/environment/solver/MinMaxSolverEnvironment.h" +#include "storm/environment/solver/TopologicalSolverEnvironment.h" +#include "storm/environment/solver/MultiplierEnvironment.h" +#include "storm/settings/modules/CoreSettings.h" +#include "storm/logic/Formulas.h" +#include "storm/exceptions/UncheckedRequirementException.h" + +namespace { + class DoubleViEnvironment { + public: + typedef double ValueType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-8)); + return env; + } + }; + + template + class ShieldGenerationSmgRpatlModelCheckerTest : public ::testing::Test { + public: + typedef typename TestType::ValueType ValueType; + ShieldGenerationSmgRpatlModelCheckerTest() : _environment(TestType::createEnvironment()) {} + storm::Environment const& env() const { return _environment; } + + std::pair>, std::vector>> buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { + std::pair>, std::vector>> 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(program, result.second)->template as>(); + return result; + } + + std::vector> getTasks(std::vector> const& formulas) const { + std::vector> result; + for (auto const& f : formulas) { + result.emplace_back(*f); + } + return result; + } + + ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber(input);} + + private: + storm::Environment _environment; + }; + + typedef ::testing::Types< + DoubleViEnvironment + > TestingTypes; + + TYPED_TEST_SUITE(ShieldGenerationSmgRpatlModelCheckerTest, TestingTypes,); + + TYPED_TEST(ShieldGenerationSmgRpatlModelCheckerTest, RightDecision) { + typedef typename TestFixture::ValueType ValueType; + + // testing that no shield is created + std::string formulasString = "<> Pmax=? [ F <=3 \"target\" ]"; + + // testing create shielding expressions + formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=5 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=5 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmin=? [ F \"target\" ]"; + formulasString += "; <> Pmin=? [ F \"target\" ]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/smg/rightDecision.nm", formulasString); + auto smg = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(11ul, smg->getNumberOfStates()); + EXPECT_EQ(15ul, smg->getNumberOfTransitions()); + ASSERT_EQ(smg->getType(), storm::models::ModelType::Smg); + EXPECT_EQ(14ull, smg->getNumberOfChoices()); + + //std::unique_ptr result; + storm::modelchecker::SparseSmgRpatlModelChecker> checker(*smg); + + // first result must not be a shielding result + auto result = checker.check(this->env(), tasks[0]); + EXPECT_FALSE( tasks[1].isShieldingTask()); + + // shielding results + storm::logic::ShieldingType type = storm::logic::ShieldingType::PreSafety; + std::string filename = "preSafetyShieldLambda1"; + storm::logic::ShieldComparison comparison = storm::logic::ShieldComparison::Relative; + double value = 0.9; + auto preSafetyShieldingExpression = std::shared_ptr(new storm::logic::ShieldExpression(type, filename, comparison, value)); + tasks[1].setShieldingExpression(preSafetyShieldingExpression); + EXPECT_TRUE(tasks[1].isShieldingTask()); + + result = checker.check(this->env(), tasks[1]); + + filename += ".shield"; + std::ifstream resultFile(filename); + std::stringstream resultBuffer; + resultBuffer << resultFile.rdbuf(); + std::string resultString = resultBuffer.str(); + std::cout << resultString << std::endl; + std::remove(filename.c_str()); + // THIS WORKS!! + + //TODO: EXPECT_EQUAL: string from solution and string from comparison-file + + // TODO: build back the values, e.g. we do not need a method for computing string-shields + // - testfiles for comparison, make an folder for that and name it like the test case names + // - this also would work fine fith mdps, so finish this example, add it to mdp folder + // - then we can go to solve examples, we have to integrate a lot of examples... + + result = checker.check(this->env(), tasks[2]); + result = checker.check(this->env(), tasks[3]); + result = checker.check(this->env(), tasks[4]); + result = checker.check(this->env(), tasks[5]); + result = checker.check(this->env(), tasks[6]); + result = checker.check(this->env(), tasks[7]); + result = checker.check(this->env(), tasks[8]); + } + + // TODO: create more test cases (files) +}