Added tests for quantiles.

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
+

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<delay -> (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<delay -> (x'=min(x+1,kx+1));
+	[] s=1 -> fast : (s'=5) & (x'=0) + slow : (s'=6) & (x'=0);
+	// start_fast
+	[time] s=2 & x<delay -> (x'=min(x+1,kx+1));
+	[] s=2 -> fast : (s'=5) & (x'=0) + slow : (s'=7) & (x'=0);
+	// start_slow
+	[time] s=3 & x<delay -> (x'=min(x+1,kx+1));
+	[] s=3 -> fast : (s'=6) & (x'=0) + slow : (s'=8) & (x'=0);
+	// slow_start
+	[time] s=4 & x<delay -> (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

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<WIDTH ->  (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<HEIGHT ->  (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<WIDTH -> 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<HEIGHT -> 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
+
+	

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
+

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<storm::RationalNumber>(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<typename TestType>
+    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<ValueType>();
+            }
+            return storm::utility::convertNumber<ValueType>(input);
+        }
+        
+        template <typename MT>
+        std::pair<std::shared_ptr<MT>, 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<MT>, 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<MT>();
+            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, true); // only initial states are relevant
+            }
+            return result;
+        }
+        
+        template <typename MT>
+        typename std::enable_if<std::is_same<MT, storm::models::sparse::Mdp<ValueType>>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type
+        createModelChecker(std::shared_ptr<MT> const& model) const {
+            return std::make_shared<storm::modelchecker::SparseMdpPrctlModelChecker<MT>>(*model);
+        }
+        template <typename MT>
+        typename std::enable_if<std::is_same<MT, storm::models::sparse::Dtmc<ValueType>>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type
+        createModelChecker(std::shared_ptr<MT> const& model) const {
+            return std::make_shared<storm::modelchecker::SparseDtmcPrctlModelChecker<MT>>(*model);
+        }
+        
+        std::pair<bool, std::string> compareResult(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::unique_ptr<storm::modelchecker::CheckResult>& result, std::vector<std::string> const& expected) {
+            bool equal = true;
+            std::string errorMessage = "";
+            auto filter = getInitialStateFilter(model);
+            result->filter(*filter);
+            std::vector<std::vector<ValueType>> resultPoints;
+            if (result->isExplicitParetoCurveCheckResult()) {
+                resultPoints = result->asExplicitParetoCurveCheckResult<ValueType>().getPoints();
+            } else {
+                if (!result->isExplicitQuantitativeCheckResult()) {
+                    return { false, "The CheckResult has unexpected type."};
+                }
+                resultPoints = {{ result->asExplicitQuantitativeCheckResult<ValueType>().getMax() }};
+            }
+            std::vector<std::vector<ValueType>> expectedPoints;
+            for (auto const& pointAsString : expected) {
+                std::vector<ValueType> 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<storm::modelchecker::QualitativeCheckResult> getInitialStateFilter(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) const {
+            return std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(model->getInitialStates());
+        }
+    };
+  
+    typedef ::testing::Types<
+            UnsoundEnvironment,
+            SoundEnvironment,
+            ExactEnvironment
+        > TestingTypes;
+    
+    TYPED_TEST_CASE(QuantileQueryTest, TestingTypes);
+    
+
+    TYPED_TEST(QuantileQueryTest, simple_Dtmc) {
+        typedef storm::models::sparse::Dtmc<typename TestFixture::ValueType> 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<ModelType>(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<ModelType>(model);
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+        std::vector<std::string> expectedResult;
+        std::pair<bool, std::string> 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<typename TestFixture::ValueType> 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<ModelType>(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<ModelType>(model);
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+        std::vector<std::string> expectedResult;
+        std::pair<bool, std::string> 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<typename TestFixture::ValueType> ModelType;
+
+        std::string formulasString = "quantile(min TIME, min ROUNDS, Pmax>0.95 [F{\"time\"}<=TIME,{\"rounds\"}<=ROUNDS \"done\"]);\n";
+        
+        auto modelFormulas = this->template buildModelFormulas<ModelType>(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<ModelType>(model);
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+        std::vector<std::string> expectedResult;
+        std::pair<bool, std::string> 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<typename TestFixture::ValueType> 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<ModelType>(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<ModelType>(model);
+        std::unique_ptr<storm::modelchecker::CheckResult> result;
+        std::vector<std::string> expectedResult;
+        std::pair<bool, std::string> 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;
+    
+    }
+}