From 248e68a10376776384e206180eaaed8f23d9b8ac Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Tue, 3 Jan 2017 12:26:15 +0100
Subject: [PATCH 1/5] jenkinsfile updated
---
Jenkinsfile | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/Jenkinsfile b/Jenkinsfile
index d7a7f5377..6dd30cdbc 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -31,8 +31,9 @@ node {
}
stage('Test') {
- dir("build")
- sh "make check"
+ dir("build") {
+ sh "make check"
+ }
}
stage('Archive') {
From 1f82fa27e868ce2151bf8f923bdf16fcef200941 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Tue, 3 Jan 2017 13:29:03 +0100
Subject: [PATCH 2/5] reward parameters
---
src/storm/models/sparse/Model.cpp | 11 +++++++++++
src/storm/models/sparse/Model.h | 1 +
.../models/sparse/StandardRewardModel.cpp | 19 ++++++++++++++++++-
src/storm/models/sparse/StandardRewardModel.h | 8 ++++----
src/storm/utility/vector.h | 9 +++++++++
5 files changed, 43 insertions(+), 5 deletions(-)
diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp
index d115e49f7..b00ef9b6f 100644
--- a/src/storm/models/sparse/Model.cpp
+++ b/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>;
diff --git a/src/storm/models/sparse/Model.h b/src/storm/models/sparse/Model.h
index 51f43eb57..583ffbb93 100644
--- a/src/storm/models/sparse/Model.h
+++ b/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
diff --git a/src/storm/models/sparse/StandardRewardModel.cpp b/src/storm/models/sparse/StandardRewardModel.cpp
index c82041437..8b7e8c349 100644
--- a/src/storm/models/sparse/StandardRewardModel.cpp
+++ b/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;
diff --git a/src/storm/models/sparse/StandardRewardModel.h b/src/storm/models/sparse/StandardRewardModel.h
index 6651b789b..8fcfa48ef 100644
--- a/src/storm/models/sparse/StandardRewardModel.h
+++ b/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_ */
diff --git a/src/storm/utility/vector.h b/src/storm/utility/vector.h
index f0cf1330e..dc22fa310 100644
--- a/src/storm/utility/vector.h
+++ b/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.
*
From 3795519fea5163683eb9b881d0a0769b142c20ff Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Tue, 3 Jan 2017 13:31:51 +0100
Subject: [PATCH 3/5] removed old unit tests for jani parser, to be replaced by
regression tests
---
src/test/parser/JaniParserTest.cpp | 21 ---------------------
1 file changed, 21 deletions(-)
delete mode 100644 src/test/parser/JaniParserTest.cpp
diff --git a/src/test/parser/JaniParserTest.cpp b/src/test/parser/JaniParserTest.cpp
deleted file mode 100644
index 91d019382..000000000
--- a/src/test/parser/JaniParserTest.cpp
+++ /dev/null
@@ -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;
-}
From 3b4b5e3a38efe60174388925f8a4a219fab1e155 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Tue, 3 Jan 2017 15:19:13 +0100
Subject: [PATCH 4/5] disable tests which depend on mathsat if mathsat is not
available, gives a warning in verbose output
---
.../GameBasedDtmcModelCheckerTest.cpp | 16 ++++++++++++++++
.../GameBasedMdpModelCheckerTest.cpp | 8 ++++++++
.../SmtPermissiveSchedulerTest.cpp | 8 ++++----
3 files changed, 28 insertions(+), 4 deletions(-)
diff --git a/src/test/modelchecker/GameBasedDtmcModelCheckerTest.cpp b/src/test/modelchecker/GameBasedDtmcModelCheckerTest.cpp
index 4cc504f39..2a4f64c4d 100644
--- a/src/test/modelchecker/GameBasedDtmcModelCheckerTest.cpp
+++ b/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();
diff --git a/src/test/modelchecker/GameBasedMdpModelCheckerTest.cpp b/src/test/modelchecker/GameBasedMdpModelCheckerTest.cpp
index 441b03b37..20087e136 100644
--- a/src/test/modelchecker/GameBasedMdpModelCheckerTest.cpp
+++ b/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);
diff --git a/src/test/permissiveschedulers/SmtPermissiveSchedulerTest.cpp b/src/test/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
index 734cf6c83..ae9fad1d2 100644
--- a/src/test/permissiveschedulers/SmtPermissiveSchedulerTest.cpp
+++ b/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
From e08fad7b4ab56887f569eef37ce4926498f22b10 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 4 Jan 2017 14:30:43 +0100
Subject: [PATCH 5/5] improved "Model checking property .." output a little.
---
src/storm/cli/entrypoints.h | 6 ++++++
src/storm/storage/jani/Property.cpp | 2 +-
2 files changed, 7 insertions(+), 1 deletion(-)
diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h
index f47f4bc10..dab863e69 100644
--- a/src/storm/cli/entrypoints.h
+++ b/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;
diff --git a/src/storm/storage/jani/Property.cpp b/src/storm/storage/jani/Property.cpp
index 17e175a04..c26ede01d 100644
--- a/src/storm/storage/jani/Property.cpp
+++ b/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)