diff --git a/src/test/storm-pars/CMakeLists.txt b/src/test/storm-pars/CMakeLists.txt index 28c5a391d..ba3994449 100644 --- a/src/test/storm-pars/CMakeLists.txt +++ b/src/test/storm-pars/CMakeLists.txt @@ -9,7 +9,7 @@ register_source_groups_from_filestructure("${ALL_FILES}" test) # Note that the tests also need the source files, except for the main file include_directories(${GTEST_INCLUDE_DIR}) -foreach (testsuite modelchecker utility) +foreach (testsuite analysis modelchecker utility) file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp) add_executable (test-pars-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp) diff --git a/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp b/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp new file mode 100644 index 000000000..2847c9a43 --- /dev/null +++ b/src/test/storm-pars/analysis/AssumptionCheckerTest.cpp @@ -0,0 +1,71 @@ +// +// Created by Jip Spel on 19.09.18. +// + +// TODO: cleanup includes +#include "gtest/gtest.h" +#include "storm-config.h" +#include "test/storm_gtest.h" + +#include "storm-parsers/parser/FormulaParser.h" +#include "storm/logic/Formulas.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm-parsers/parser/AutoParser.h" +#include "storm-parsers/parser/PrismParser.h" +#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/api/builder.h" + +#include "storm-pars/analysis/AssumptionChecker.h" +#include "storm-pars/analysis/Lattice.h" +#include "storm/storage/expressions/BinaryRelationExpression.h" +#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h" + +#include "storm-pars/api/storm-pars.h" +#include "storm/api/storm.h" + +#include "storm-parsers/api/storm-parsers.h" + +// TODO: extend +TEST(AssumptionCheckerTest, Brp) { + std::string programFile = STORM_TEST_RESOURCES_DIR "/pdtmc/brp16_2.pm"; + std::string formulaAsString = "P<=0.84 [F s=5 ]"; + std::string constantsAsString = ""; //e.g. pL=0.9,TOACK=0.5 + + // Program and formula + storm::prism::Program program = storm::api::parseProgram(programFile); + program = storm::utility::prism::preprocess(program, constantsAsString); + std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); + std::shared_ptr> model = storm::api::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> dtmc = model->as>(); + auto simplifier = storm::transformer::SparseParametricDtmcSimplifier>(*dtmc); + + ASSERT_TRUE(simplifier.simplify(*(formulas[0]))); // TODO: verwacht path formula? + model = simplifier.getSimplifiedModel(); + + dtmc = model->as>(); + + ASSERT_EQ(dtmc->getNumberOfStates(), 193ull); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 383ull); + + auto checker = storm::analysis::AssumptionChecker(formulas[0], dtmc, 3); + + // Check on samples + auto expressionManager = std::make_shared(storm::expressions::ExpressionManager()); + expressionManager->declareRationalVariable("7"); + expressionManager->declareRationalVariable("5"); + + auto assumption = std::make_shared( + storm::expressions::BinaryRelationExpression(*expressionManager, expressionManager->getBooleanType(), + expressionManager->getVariable("7").getExpression().getBaseExpressionPointer(), + expressionManager->getVariable("5").getExpression().getBaseExpressionPointer(), + storm::expressions::BinaryRelationExpression::RelationType::GreaterOrEqual)); + EXPECT_FALSE(checker.checkOnSamples(assumption)); + + auto emptyLattice = new storm::analysis::Lattice(storm::storage::BitVector(8), storm::storage::BitVector(8), 8); + // Validate assumptions + EXPECT_FALSE(checker.validateAssumption(assumption, emptyLattice)); + EXPECT_FALSE(checker.validated(assumption)); +} +