Merge branch 'master' into multi-objective

Jenkinsfile

@@ -31,8 +31,9 @@ node {
    }
    
    stage('Test') {
-       dir("build")
-       sh "make check"
+       	dir("build") {
+       	    sh "make check"
+	}
    }
    
    stage('Archive') {

src/storm/cli/entrypoints.h

@@ -76,6 +76,7 @@ namespace storm {
         void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant = false) {
             for (auto const& property : properties) {
                 std::cout << std::endl << "Model checking property: " << property << " ...";
+                std::cout.flush();
                 std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, property.getFilter().getFormula(), onlyInitialStatesRelevant));
                 if (result) {
                     std::cout << " done." << std::endl;
@@ -96,6 +97,7 @@ namespace storm {
             for (auto const& property : properties) {
                 STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc || model->getType() == storm::models::ModelType::Ctmc, storm::exceptions::InvalidSettingsException, "Currently parametric verification is only available for DTMCs and CTMCs.");
                 std::cout << std::endl << "Model checking property: " << property << " ...";
+                std::cout.flush();
                 std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, property.getFilter().getFormula(), onlyInitialStatesRelevant));
                 if (result) {
                     std::cout << " done." << std::endl;
@@ -119,6 +121,7 @@ namespace storm {
             typedef double ValueType;
             for (auto const& property : properties) {
                 std::cout << std::endl << "Model checking property: " << property << " ...";
+                std::cout.flush();
                 std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithAbstractionRefinementEngine<DdType, ValueType>(model, property.getFilter().getFormula(), onlyInitialStatesRelevant));
                 if (result) {
                     std::cout << " done." << std::endl;
@@ -138,6 +141,7 @@ namespace storm {
 
             for (auto const& property : formulas) {
                 std::cout << std::endl << "Model checking property: " << property << " ...";
+                std::cout.flush();
                 bool formulaSupported = false;
                 std::unique_ptr<storm::modelchecker::CheckResult> result;
 
@@ -187,6 +191,7 @@ namespace storm {
         void verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant = false) {
             for (auto const& property : formulas) {
                 std::cout << std::endl << "Model checking property: " << property << " ...";
+                std::cout.flush();
                 std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithHybridEngine(model, property.getFilter().getFormula(), onlyInitialStatesRelevant));
 
                 if (result) {
@@ -205,6 +210,7 @@ namespace storm {
         void verifySymbolicModelWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant = false) {
             for (auto const& property : formulas) {
                 std::cout << std::endl << "Model checking property: " << property << " ...";
+                std::cout.flush();
                 std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithDdEngine(model, property.getFilter().getFormula(), onlyInitialStatesRelevant));
                 if (result) {
                     std::cout << " done." << std::endl;

src/storm/models/sparse/Model.cpp

@@ -360,6 +360,17 @@ namespace storm {
             std::set<storm::RationalFunctionVariable> getProbabilityParameters(Model<storm::RationalFunction> const& model) {
                 return storm::storage::getVariables(model.getTransitionMatrix());
             }
+
+
+
+            std::set<storm::RationalFunctionVariable> getRewardParameters(Model<storm::RationalFunction> const& model) {
+                std::set<storm::RationalFunctionVariable> result;
+                for(auto rewModel : model.getRewardModels()) {
+                    std::set<storm::RationalFunctionVariable> tmp = getRewardModelParameters(rewModel.second);
+                    result.insert(tmp.begin(), tmp.end());
+                }
+                return result;
+            }
 #endif
             
             template class Model<double>;

src/storm/models/sparse/Model.h

@@ -374,6 +374,7 @@ namespace storm {
             
 #ifdef STORM_HAVE_CARL
             std::set<storm::RationalFunctionVariable> getProbabilityParameters(Model<storm::RationalFunction> const& model);
+            std::set<storm::RationalFunctionVariable> getRewardParameters(Model<storm::RationalFunction> const& model);
 #endif
         } // namespace sparse
     } // namespace models

src/storm/models/sparse/StandardRewardModel.cpp

@@ -298,7 +298,24 @@ namespace storm {
                 << std::noboolalpha;
                 return out;
             }
-            
+
+            std::set<storm::RationalFunctionVariable> getRewardModelParameters(StandardRewardModel<storm::RationalFunction> const& rewModel) {
+                std::set<storm::RationalFunctionVariable> vars;
+                if (rewModel.hasTransitionRewards()) {
+                    vars = storm::storage::getVariables(rewModel.getTransitionRewardMatrix());
+                }
+                if (rewModel.hasStateActionRewards()) {
+                    std::set<storm::RationalFunctionVariable> tmp =  storm::utility::vector::getVariables(rewModel.getStateActionRewardVector());
+                    vars.insert(tmp.begin(), tmp.end());
+                }
+                if (rewModel.hasStateRewards()) {
+                    std::set<storm::RationalFunctionVariable> tmp = storm::utility::vector::getVariables(rewModel.getStateRewardVector());
+                    vars.insert(tmp.begin(), tmp.end());
+                }
+                return vars;
+
+            }
+
             // Explicitly instantiate the class.
             template std::vector<double> StandardRewardModel<double>::getTotalRewardVector(storm::storage::SparseMatrix<double> const& transitionMatrix) const;
             template std::vector<double> StandardRewardModel<double>::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::BitVector const& filter) const;

src/storm/models/sparse/StandardRewardModel.h

@@ -1,11 +1,11 @@
-#ifndef STORM_MODELS_SPARSE_STANDARDREWARDMODEL_H_
-#define STORM_MODELS_SPARSE_STANDARDREWARDMODEL_H_
+#pragma once
 
 #include <vector>
 #include <boost/optional.hpp>
 
 #include "storm/storage/SparseMatrix.h"
 #include "storm/utility/OsDetection.h"
+#include "storm/adapters/CarlAdapter.h"
 
 namespace storm {
     namespace models {
@@ -296,8 +296,8 @@ namespace storm {
             
             template <typename ValueType>
             std::ostream& operator<<(std::ostream& out, StandardRewardModel<ValueType> const& rewardModel);
+
+            std::set<storm::RationalFunctionVariable> getRewardModelParameters(StandardRewardModel<storm::RationalFunction> const& rewModel);
         }
     }
 }
-
-#endif /* STORM_MODELS_SPARSE_STANDARDREWARDMODEL_H_ */

src/storm/storage/jani/Property.cpp

@@ -5,7 +5,7 @@ namespace storm {
         
         
         std::ostream& operator<<(std::ostream& os, FilterExpression const& fe) {
-            return os << "Obtain " << toString(fe.getFilterType()) << " the 'initial'-states with values described by '" << *fe.getFormula() << "'";
+            return os << "Obtain " << toString(fe.getFilterType()) << " of the 'initial'-states with values described by '" << *fe.getFormula() << "'";
         }
         
         Property::Property(std::string const& name, std::shared_ptr<storm::logic::Formula const> const& formula, std::string const& comment)

src/storm/utility/vector.h

@@ -10,6 +10,7 @@
 #include <algorithm>
 #include <functional>
 #include <numeric>
+#include <storm/adapters/CarlAdapter.h>
 
 #include "storm/storage/BitVector.h"
 #include "storm/utility/constants.h"
@@ -822,6 +823,14 @@ namespace storm {
                 return std::any_of(v.begin(), v.end(), [](T value){return !storm::utility::isZero(value);});
             }
 
+            inline std::set<storm::RationalFunctionVariable> getVariables(std::vector<storm::RationalFunction> const& vector) {
+                std::set<storm::RationalFunctionVariable> result;
+                for(auto const& entry : vector) {
+                    entry.gatherVariables(result);
+                }
+                return result;
+            }
+
             /*!
              * Output vector as string.
              *

src/test/modelchecker/GameBasedDtmcModelCheckerTest.cpp

@@ -17,7 +17,11 @@
 
 #include "storm/settings/modules/GeneralSettings.h"
 
+#if defined STORM_HAVE_MSAT
 TEST(GameBasedDtmcModelCheckerTest, Die_Cudd) {
+#else
+TEST(GameBasedDtmcModelCheckerTest, DISABLED_Die_Cudd) {
+#endif
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
 	auto checker = std::make_shared<storm::modelchecker::GameBasedMdpModelChecker<storm::dd::DdType::CUDD, storm::models::symbolic::Dtmc<storm::dd::DdType::CUDD>>>(program);
     
@@ -49,7 +53,11 @@ TEST(GameBasedDtmcModelCheckerTest, Die_Cudd) {
     EXPECT_NEAR(1.0/6.0, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
 }
 
+#if defined STORM_HAVE_MSAT
 TEST(GameBasedDtmcModelCheckerTest, Die_Sylvan) {
+#else
+TEST(GameBasedDtmcModelCheckerTest, DISABLED_Die_Sylvan) {
+#endif
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
     
     // A parser that we use for conveniently constructing the formulas.
@@ -82,7 +90,11 @@ TEST(GameBasedDtmcModelCheckerTest, Die_Sylvan) {
     EXPECT_NEAR(1.0/6.0, quantitativeResult3[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
 }
 
+#if defined STORM_HAVE_MSAT
 TEST(GameBasedDtmcModelCheckerTest, SynchronousLeader_Cudd) {
+#else
+TEST(GameBasedDtmcModelCheckerTest, DISABLED_SynchronousLeader_Cudd) {
+#endif
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm");
     program = program.substituteConstants();
     
@@ -100,7 +112,11 @@ TEST(GameBasedDtmcModelCheckerTest, SynchronousLeader_Cudd) {
     EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
 }
 
+#if defined STORM_HAVE_MSAT
 TEST(GameBasedDtmcModelCheckerTest, SynchronousLeader_Sylvan) {
+#else
+TEST(GameBasedDtmcModelCheckerTest, DISABLED_SynchronousLeader_Sylvan) {
+#endif
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm");
     program = program.substituteConstants();
 

src/test/modelchecker/GameBasedMdpModelCheckerTest.cpp

@@ -16,7 +16,11 @@
 
 #include "storm/utility/storm.h"
 
+#if defined STORM_HAVE_MSAT
 TEST(GameBasedMdpModelCheckerTest, Dice_Cudd) {
+#else
+TEST(GameBasedMdpModelCheckerTest, DISABLED_Dice_Cudd) {
+#endif
     std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm";
 
     storm::prism::Program program = storm::parseProgram(programFile);
@@ -87,7 +91,11 @@ TEST(GameBasedMdpModelCheckerTest, Dice_Cudd) {
     EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
 }
 
+#if defined STORM_HAVE_MSAT
 TEST(GameBasedMdpModelCheckerTest, Dice_Sylvan) {
+#else
+TEST(GameBasedMdpModelCheckerTest, DISABLED_Dice_Sylvan) {
+#endif
     std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm";
     
     storm::prism::Program program = storm::parseProgram(programFile);

src/test/parser/JaniParserTest.cpp

@@ -1,21 +0,0 @@
-#include "gtest/gtest.h"
-#include "storm-config.h"
-#include "storm/parser/JaniParser.h"
-#include "storm/storage/jani/Model.h"
-#include "storm/storage/jani/Property.h"
-
-
-TEST(JaniParser, DieTest) {
-    std::string testFileInput = STORM_TEST_RESOURCES_DIR"/../examples/exported-jani-models/dice.jani";
-    storm::jani::Model model = storm::parser::JaniParser::parse(testFileInput).first;
-}
-
-TEST(JaniParser, BrpTest) {
-    std::string testFileInput = STORM_TEST_RESOURCES_DIR"/../examples/exported-jani-models/brp.jani";
-    storm::jani::Model model = storm::parser::JaniParser::parse(testFileInput).first;
-}
-
-TEST(JaniParser, ConsensusTest) {
-    std::string testFileInput = STORM_TEST_RESOURCES_DIR"/../examples/exported-jani-models/coin2.jani";
-    storm::jani::Model model = storm::parser::JaniParser::parse(testFileInput).first;
-}

src/test/permissiveschedulers/SmtPermissiveSchedulerTest.cpp

@@ -11,9 +11,11 @@
 #include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
 
 
-#if defined(STORM_HAVE_MSAT) || defined(STORM_HAVE_Z3)
-
+#if defined STORM_HAVE_MSAT
 TEST(SmtPermissiveSchedulerTest, DieSelection) {
+#else
+TEST(SmtPermissiveSchedulerTest, DISABLED_DieSelection) {
+#endif
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/die_c1.nm");
     storm::parser::FormulaParser formulaParser(program);
     
@@ -57,5 +59,3 @@ TEST(SmtPermissiveSchedulerTest, DieSelection) {
     //
     
 }
-
-#endif // STORM_HAVE_MSAT || STORM_HAVE_Z3