diff --git a/resources/examples/testfiles/dtmc/quantiles_simple_dtmc.pm b/resources/examples/testfiles/dtmc/quantiles_simple_dtmc.pm new file mode 100644 index 000000000..7551aa7a6 --- /dev/null +++ b/resources/examples/testfiles/dtmc/quantiles_simple_dtmc.pm @@ -0,0 +1,20 @@ + +dtmc + +module main + s : [0..3] init 0; + + [] s=0 -> 0.4 : (s'=1) + 0.4 : (s'=2) + 0.2 : (s'=3); + [a] s=1 -> 1 : (s'=0); + [b] s=2 -> 1 : (s'=0); + [] s=3 -> 1 : (s'=3); +endmodule + +rewards "first" + [a] true : 1; +endrewards + +rewards "second" + [b] true : 2; +endrewards + diff --git a/resources/examples/testfiles/mdp/quantiles_firewire.nm b/resources/examples/testfiles/mdp/quantiles_firewire.nm new file mode 100644 index 000000000..447f5abf0 --- /dev/null +++ b/resources/examples/testfiles/mdp/quantiles_firewire.nm @@ -0,0 +1,80 @@ +// integer semantics version of abstract firewire protocol +// gxn 23/05/2001 + +mdp + +// wire delay +const int delay; + +// probability of choosing fast and slow +const double fast = 0.5; +const double slow = 1-fast; + +// largest constant the clock of the system is compared to +const int kx = 167; + +module abstract_firewire + + // clock + x : [0..kx+1]; + + // local state + s : [0..9]; + // 0 -start_start + // 1 -fast_start + // 2 -start_fast + // 3 -start_slow + // 4 -slow_start + // 5 -fast_fast + // 6 -fast_slow + // 7 -slow_fast + // 8 -slow_slow + // 9 -done + + // initial state + [time] s=0 & x (x'=min(x+1,kx+1)); + [round] s=0 -> fast : (s'=1) + slow : (s'=4); + [round] s=0 -> fast : (s'=2) + slow : (s'=3); + // fast_start + [time] s=1 & x (x'=min(x+1,kx+1)); + [] s=1 -> fast : (s'=5) & (x'=0) + slow : (s'=6) & (x'=0); + // start_fast + [time] s=2 & x (x'=min(x+1,kx+1)); + [] s=2 -> fast : (s'=5) & (x'=0) + slow : (s'=7) & (x'=0); + // start_slow + [time] s=3 & x (x'=min(x+1,kx+1)); + [] s=3 -> fast : (s'=6) & (x'=0) + slow : (s'=8) & (x'=0); + // slow_start + [time] s=4 & x (x'=min(x+1,kx+1)); + [] s=4 -> fast : (s'=7) & (x'=0) + slow : (s'=8) & (x'=0); + // fast_fast + [time] s=5 & (x<85) -> (x'=min(x+1,kx+1)); + [] s=5 & (x>=76) -> (s'=0) & (x'=0); + [] s=5 & (x>=76-delay) -> (s'=9) & (x'=0); + // fast_slow + [time] s=6 & x<167 -> (x'=min(x+1,kx+1)); + [] s=6 & x>=159-delay -> (s'=9) & (x'=0); + // slow_fast + [time] s=7 & x<167 -> (x'=min(x+1,kx+1)); + [] s=7 & x>=159-delay -> (s'=9) & (x'=0); + // slow_slow + [time] s=8 & x<167 -> (x'=min(x+1,kx+1)); + [] s=8 & x>=159 -> (s'=0) & (x'=0); + [] s=8 & x>=159-delay -> (s'=9) & (x'=0); + // done + [] s=9 -> (s'=s); + +endmodule + +// labels +label "done" = s=9; + +//reward structures +// time +rewards "time" + [time] true : 1; +endrewards +// number of rounds +rewards "rounds" + [round] true : 1; +endrewards diff --git a/resources/examples/testfiles/mdp/quantiles_resources.nm b/resources/examples/testfiles/mdp/quantiles_resources.nm new file mode 100644 index 000000000..6061465e4 --- /dev/null +++ b/resources/examples/testfiles/mdp/quantiles_resources.nm @@ -0,0 +1,72 @@ +mdp + +const int WIDTH = 5; +const int HEIGHT = 5; +const int XINIT = 3; +const int YINIT = 1; + +const double pAttack = 1/10; + +formula left_of_gold = x=2 & y=5; +formula right_of_gold = x=4 & y=5; +formula below_of_gold = (x=3 & y=4); +formula above_of_gold = false; +formula left_of_gem = (x=4 & y=4); +formula right_of_gem = false; +formula below_of_gem = (x=5 & y=3); +formula above_of_gem = (x=5 & y=5); +formula left_of_home = x=2 & y=1; +formula right_of_home = x=4 & y=1; +formula above_of_home = x=3 & y=2; +formula below_of_home = false; +formula left_of_enemy = (x=3 & y=5) | (x=2 & y=4); +formula right_of_enemy = (x=5 & y=5) | (x=4 & y=4); +formula above_of_enemy = x=3 & y=5; +formula below_of_enemy = (x=3 & y=3) | (x=4 & y=4); + +module robot + + gold : bool init false; + gem : bool init false; + attacked : bool init false; + + x : [1..WIDTH] init XINIT; + y : [1..HEIGHT] init YINIT; + + [right] !left_of_enemy & x (attacked'=false) & (x'=x+1) & (gold' = (gold & !left_of_home) | left_of_gold) & (gem' = (gem & !left_of_home) | left_of_gem); + [left] !right_of_enemy & x>1 -> (attacked'=false) & (x'=x-1) & (gold' = (gold & !right_of_home) | right_of_gold) & (gem' = (gem & !right_of_home) | right_of_gem); + [top] !below_of_enemy & y (attacked'=false) & (y'=y+1) & (gold' = (gold & !below_of_home) | below_of_gold) & (gem' = (gem & !below_of_home) | below_of_gem); + [down] !above_of_enemy & y>1 -> (attacked'=false) & (y'=y-1) & (gold' = (gold & !above_of_home) | above_of_gold) & (gem' = (gem & !above_of_home) | above_of_gem); + + [right] left_of_enemy & x pAttack : (attacked'=true) & (x'=XINIT) & (y'=YINIT) & (gold'=false) & (gem'=false) + (1-pAttack) : (attacked'=false) & (x'=x+1) & (gold' = (gold & !left_of_home) | left_of_gold) & (gem' = (gem & !left_of_home) | left_of_gem); + [left] right_of_enemy & x>1 -> pAttack : (attacked'=true) & (x'=XINIT) & (y'=YINIT) & (gold'=false) & (gem'=false) + (1-pAttack) : (attacked'=false) & (x'=x-1) & (gold' = (gold & !right_of_home) | right_of_gold) & (gem' = (gem & !right_of_home) | right_of_gem); + [top] below_of_enemy & y pAttack : (attacked'=true) & (x'=XINIT) & (y'=YINIT) & (gold'=false) & (gem'=false) + (1-pAttack) : (attacked'=false) & (y'=y+1) & (gold' = (gold & !below_of_home) | below_of_gold) & (gem' = (gem & !below_of_home) | below_of_gem); + [down] above_of_enemy & y>1 -> pAttack : (attacked'=true) & (x'=XINIT) & (y'=YINIT) & (gold'=false) & (gem'=false) + (1-pAttack) : (attacked'=false) & (y'=y-1) & (gold' = (gold & !above_of_home) | above_of_gold) & (gem' = (gem & !above_of_home) | above_of_gem); +endmodule + +rewards "attacks" + attacked : 1; +endrewards + +rewards "steps" + [left] true : 1; + [right] true : 1; + [top] true : 1; + [down] true : 1; +endrewards + +rewards "gold" + [right] left_of_home & gold : 1; + [left] right_of_home & gold : 1; + [top] below_of_home & gold : 1; + [down] above_of_home & gold : 1; +endrewards + +rewards "gem" + [right] left_of_home & gem : 1; + [left] right_of_home & gem : 1; + [top] below_of_home & gem : 1; + [down] above_of_home & gem: 1; +endrewards + + \ No newline at end of file diff --git a/resources/examples/testfiles/mdp/quantiles_simple_mdp.nm b/resources/examples/testfiles/mdp/quantiles_simple_mdp.nm new file mode 100644 index 000000000..011bc6232 --- /dev/null +++ b/resources/examples/testfiles/mdp/quantiles_simple_mdp.nm @@ -0,0 +1,31 @@ + +mdp + +module main + s : [0..6] init 6; + + [] s=6 -> 1 : (s'=0); + [] s=6 -> 1 : (s'=5); + [a] s=5 -> 1 : (s'=5); + [b] s=5 -> 1 : (s'=1); + [] s=0 -> 1/10: (s'=1) + 9/10: (s'=3); + [] s=0 -> 1/10: (s'=1) + 9/10: (s'=4); + [a] s=3 -> 1: (s'=0); + [b] s=3 -> 1: (s'=0); + [] s=1 -> 1: (s'=2); + [] s=2 -> 1: (s'=2); +endmodule + +rewards "first" + [a] true : 1; +endrewards + +rewards "second" + [b] s=3 : 1; + [b] s=5 : 2; +endrewards + +rewards "third" + true : 0.7; +endrewards + diff --git a/src/test/storm/modelchecker/QuantileQueryTest.cpp b/src/test/storm/modelchecker/QuantileQueryTest.cpp new file mode 100644 index 000000000..c6c718856 --- /dev/null +++ b/src/test/storm/modelchecker/QuantileQueryTest.cpp @@ -0,0 +1,302 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "test/storm_gtest.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/parser/CSVParser.h" + +#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h" +#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" +#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/environment/solver/MinMaxSolverEnvironment.h" +#include "storm/logic/Formulas.h" +#include "storm/storage/jani/Property.h" + +namespace { + + enum class MdpEngine {PrismSparse, JaniSparse, JitSparse, Hybrid, PrismDd, JaniDd}; + + class UnsoundEnvironment { + public: + typedef double ValueType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); + return env; + } + }; + + class SoundEnvironment { + public: + typedef double ValueType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setForceSoundness(true); + return env; + } + }; + + class ExactEnvironment { + public: + typedef storm::RationalNumber ValueType; + static storm::Environment createEnvironment() { + storm::Environment env; + return env; + } + }; + + template + class QuantileQueryTest : public ::testing::Test { + public: + typedef typename TestType::ValueType ValueType; + QuantileQueryTest() : _environment(TestType::createEnvironment()) {} + storm::Environment const& env() const { return _environment; } + ValueType parseNumber(std::string const& input) const { + if (input.find("inf") != std::string::npos) { + return storm::utility::infinity(); + } + return storm::utility::convertNumber(input); + } + + template + 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, true); // only initial states are relevant + } + return result; + } + + template + typename std::enable_if>::value, std::shared_ptr>>::type + createModelChecker(std::shared_ptr const& model) const { + return std::make_shared>(*model); + } + template + typename std::enable_if>::value, std::shared_ptr>>::type + createModelChecker(std::shared_ptr const& model) const { + return std::make_shared>(*model); + } + + std::pair compareResult(std::shared_ptr> const& model, std::unique_ptr& result, std::vector const& expected) { + bool equal = true; + std::string errorMessage = ""; + auto filter = getInitialStateFilter(model); + result->filter(*filter); + std::vector> resultPoints; + if (result->isExplicitParetoCurveCheckResult()) { + resultPoints = result->asExplicitParetoCurveCheckResult().getPoints(); + } else { + if (!result->isExplicitQuantitativeCheckResult()) { + return { false, "The CheckResult has unexpected type."}; + } + resultPoints = {{ result->asExplicitQuantitativeCheckResult().getMax() }}; + } + std::vector> expectedPoints; + for (auto const& pointAsString : expected) { + std::vector point; + for (auto const& entry : storm::parser::parseCommaSeperatedValues(pointAsString)) { + point.push_back(parseNumber(entry)); + } + expectedPoints.push_back(std::move(point)); + } + for (auto const& resPoint : resultPoints) { + bool contained = false; + for (auto const& expPoint : expectedPoints) { + if (resPoint == expPoint) { + contained = true; + break; + } + } + if (!contained) { + equal = false; + errorMessage += "The result " + storm::utility::vector::toString(resPoint) + " is not contained in the expected solution. "; + } + } + for (auto const& expPoint : expectedPoints) { + bool contained = false; + for (auto const& resPoint : resultPoints) { + if (resPoint == expPoint) { + contained = true; + break; + } + } + if (!contained) { + equal = false; + errorMessage += "The expected " + storm::utility::vector::toString(expPoint) + " is not contained in the obtained solution. "; + } + } + return {equal, errorMessage}; + } + + private: + storm::Environment _environment; + + std::unique_ptr getInitialStateFilter(std::shared_ptr> const& model) const { + return std::make_unique(model->getInitialStates()); + } + }; + + typedef ::testing::Types< + UnsoundEnvironment, + SoundEnvironment, + ExactEnvironment + > TestingTypes; + + TYPED_TEST_CASE(QuantileQueryTest, TestingTypes); + + + TYPED_TEST(QuantileQueryTest, simple_Dtmc) { + typedef storm::models::sparse::Dtmc ModelType; + + std::string formulasString = "quantile(max A, max B, P>0.95 [F{\"first\"}<=A,{\"second\"}<=B s=3]);\n"; + + auto modelFormulas = this->template buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/quantiles_simple_dtmc.pm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(4ul, model->getNumberOfStates()); + EXPECT_EQ(6ul, model->getNumberOfTransitions()); + auto checker = this->template createModelChecker(model); + std::unique_ptr result; + std::vector expectedResult; + std::pair compare; + uint64_t taskId = 0; + + expectedResult.clear(); + expectedResult.push_back("7, 18"); + expectedResult.push_back("8, 16"); + expectedResult.push_back("9, 14"); + result = checker->check(this->env(), tasks[taskId++]); + compare = this->compareResult(model, result, expectedResult); + EXPECT_TRUE(compare.first) << compare.second; + } + + TYPED_TEST(QuantileQueryTest, simple_Mdp) { + typedef storm::models::sparse::Mdp ModelType; + + std::string formulasString = "quantile(B1, B2, Pmax>0.5 [F{\"first\"}>=B1,{\"second\"}>=B2 s=1]);\n"; + formulasString += "quantile(B1, B2, Pmax>0.5 [F{\"first\"}<=B1,{\"second\"}<=B2 s=1]);\n"; + formulasString += "quantile(B1, B2, Pmin>0.5 [F{\"first\"}<=B1,{\"second\"}<=B2 s=1]);\n"; + formulasString += "quantile(B1, Pmax>0.5 [F{\"second\"}>=B1 s=1]);\n"; + formulasString += "quantile(B1, B2, B3, Pmax>0.5 [F{\"first\"}<=B1,{\"second\"}<=B2,{\"third\"}<=B3 s=1]);\n"; + + auto modelFormulas = this->template buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/quantiles_simple_mdp.nm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(7ul, model->getNumberOfStates()); + EXPECT_EQ(13ul, model->getNumberOfTransitions()); + auto checker = this->template createModelChecker(model); + std::unique_ptr result; + std::vector expectedResult; + std::pair compare; + uint64_t taskId = 0; + + expectedResult.clear(); + expectedResult.push_back(" 0, 6"); + expectedResult.push_back(" 1, 5"); + expectedResult.push_back(" 2, 4"); + expectedResult.push_back(" 3, 3"); + expectedResult.push_back("inf, 2"); + result = checker->check(this->env(), tasks[taskId++]); + compare = this->compareResult(model, result, expectedResult); + EXPECT_TRUE(compare.first) << compare.second; + + expectedResult.clear(); + expectedResult.push_back(" 0, 2"); + expectedResult.push_back(" 5, 1"); + expectedResult.push_back(" 6, 0"); + result = checker->check(this->env(), tasks[taskId++]); + compare = this->compareResult(model, result, expectedResult); + EXPECT_TRUE(compare.first) << compare.second; + + expectedResult.clear(); + result = checker->check(this->env(), tasks[taskId++]); + compare = this->compareResult(model, result, expectedResult); + EXPECT_TRUE(compare.first) << compare.second; + + expectedResult.clear(); + expectedResult.push_back(" 6"); + result = checker->check(this->env(), tasks[taskId++]); + compare = this->compareResult(model, result, expectedResult); + EXPECT_TRUE(compare.first) << compare.second; + + expectedResult.clear(); + expectedResult.push_back(" 0, 2, 1.4"); + expectedResult.push_back(" 5, 1, 9.8"); + expectedResult.push_back(" 6, 0, 9.8"); + result = checker->check(this->env(), tasks[taskId++]); + compare = this->compareResult(model, result, expectedResult); + EXPECT_TRUE(compare.first) << compare.second; + } + + TYPED_TEST(QuantileQueryTest, firewire) { + typedef storm::models::sparse::Mdp ModelType; + + std::string formulasString = "quantile(min TIME, min ROUNDS, Pmax>0.95 [F{\"time\"}<=TIME,{\"rounds\"}<=ROUNDS \"done\"]);\n"; + + auto modelFormulas = this->template buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/quantiles_firewire.nm", formulasString, "delay=36"); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(776ul, model->getNumberOfStates()); + EXPECT_EQ(1411ul, model->getNumberOfTransitions()); + auto checker = this->template createModelChecker(model); + std::unique_ptr result; + std::vector expectedResult; + std::pair compare; + uint64_t taskId = 0; + + expectedResult.clear(); + expectedResult.push_back("123, 1"); + result = checker->check(this->env(), tasks[taskId++]); + compare = this->compareResult(model, result, expectedResult); + EXPECT_TRUE(compare.first) << compare.second; + + } + + TYPED_TEST(QuantileQueryTest, resources) { + typedef storm::models::sparse::Mdp ModelType; + + std::string formulasString = "quantile(max GOLD, max GEM, Pmax>0.95 [F{\"gold\"}>=GOLD,{\"gem\"}>=GEM,{\"steps\"}<=100 true]);\n"; + + auto modelFormulas = this->template buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/quantiles_resources.nm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(94ul, model->getNumberOfStates()); + EXPECT_EQ(326ul, model->getNumberOfTransitions()); + auto checker = this->template createModelChecker(model); + std::unique_ptr result; + std::vector expectedResult; + std::pair compare; + uint64_t taskId = 0; + + expectedResult.clear(); + expectedResult.push_back("0, 10"); + expectedResult.push_back("1, 9"); + expectedResult.push_back("4, 8"); + expectedResult.push_back("7, 7"); + expectedResult.push_back("8, 4"); + expectedResult.push_back("9, 2"); + expectedResult.push_back("10, 0"); + result = checker->check(this->env(), tasks[taskId++]); + compare = this->compareResult(model, result, expectedResult); + EXPECT_TRUE(compare.first) << compare.second; + + } +}