From 5bbf4ab3194c7612dac80e613eee7c3e33299874 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 20 Jan 2017 16:56:39 +0100
Subject: [PATCH 01/24] fixed issue when parsing formula files
---
src/storm/parser/FormulaParserGrammar.cpp | 5 ++++-
1 file changed, 4 insertions(+), 1 deletion(-)
diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm/parser/FormulaParserGrammar.cpp
index dcf1634a6..70c63f22e 100644
--- a/src/storm/parser/FormulaParserGrammar.cpp
+++ b/src/storm/parser/FormulaParserGrammar.cpp
@@ -133,7 +133,10 @@ namespace storm {
#pragma clang diagnostic pop
- start = ((qi::eps > filterProperty[phoenix::push_back(qi::_val, qi::_1)] | qi::eps(phoenix::bind(&FormulaParserGrammar::areConstantDefinitionsAllowed, phoenix::ref(*this))) >> constantDefinition | qi::eps) % +(qi::char_("\n;"))) >> qi::skip(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi;
+ start = (qi::eps >> filterProperty[phoenix::push_back(qi::_val, qi::_1)]
+ | qi::eps(phoenix::bind(&FormulaParserGrammar::areConstantDefinitionsAllowed, phoenix::ref(*this))) >> constantDefinition
+ | qi::eps)
+ % +(qi::char_("\n;")) >> qi::skip(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi;
start.name("start");
// Enable the following lines to print debug output for most the rules.
From 5b4db6f00261ef6a1aa543e2b9e610eaa2a597cb Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 23 Jan 2017 20:41:03 +0100
Subject: [PATCH 02/24] fixed issue in JANI abstraction
---
src/storm/abstraction/MenuGameRefiner.cpp | 3 +
src/storm/abstraction/jani/EdgeAbstractor.cpp | 6 +-
src/storm/cli/entrypoints.h | 2 +-
.../abstraction/GameBasedMdpModelChecker.cpp | 3 +-
.../expressions/LinearityCheckVisitor.cpp | 79 ++++++++++++++++---
.../expressions/LinearityCheckVisitor.h | 3 +-
src/storm/storage/jani/Assignment.cpp | 2 +-
src/storm/storage/jani/Model.cpp | 2 +-
src/storm/storage/jani/TemplateEdge.cpp | 2 +-
9 files changed, 81 insertions(+), 21 deletions(-)
diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp
index 8a6161bc6..75555bdcd 100644
--- a/src/storm/abstraction/MenuGameRefiner.cpp
+++ b/src/storm/abstraction/MenuGameRefiner.cpp
@@ -706,6 +706,9 @@ namespace storm {
void MenuGameRefiner<Type, ValueType>::performRefinement(std::vector<RefinementCommand> const& refinementCommands) const {
for (auto const& command : refinementCommands) {
STORM_LOG_TRACE("Refining with " << command.getPredicates().size() << " predicates.");
+ for (auto const& predicate : command.getPredicates()) {
+ STORM_LOG_TRACE(predicate);
+ }
abstractor.get().refine(command);
}
diff --git a/src/storm/abstraction/jani/EdgeAbstractor.cpp b/src/storm/abstraction/jani/EdgeAbstractor.cpp
index e95690d8e..980db0846 100644
--- a/src/storm/abstraction/jani/EdgeAbstractor.cpp
+++ b/src/storm/abstraction/jani/EdgeAbstractor.cpp
@@ -662,10 +662,11 @@ namespace storm {
storm::dd::Add<DdType, ValueType> EdgeAbstractor<DdType, ValueType>::getEdgeDecoratorAdd(boost::optional<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& locationVariables) const {
storm::dd::Add<DdType, ValueType> result = this->getAbstractionInformation().getDdManager().template getAddZero<ValueType>();
for (uint_fast64_t destinationIndex = 0; destinationIndex < edge.get().getNumberOfDestinations(); ++destinationIndex) {
- result += this->getAbstractionInformation().encodeAux(destinationIndex, 0, this->getAbstractionInformation().getAuxVariableCount()).template toAdd<ValueType>() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(edge.get().getDestination(destinationIndex).getProbability()));
+ storm::dd::Add<DdType, ValueType> tmp = this->getAbstractionInformation().encodeAux(destinationIndex, 0, this->getAbstractionInformation().getAuxVariableCount()).template toAdd<ValueType>() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(edge.get().getDestination(destinationIndex).getProbability()));
if (locationVariables) {
- result *= this->getAbstractionInformation().encodeLocation(locationVariables.get().second, edge.get().getDestination(destinationIndex).getLocationIndex()).template toAdd<ValueType>();
+ tmp *= this->getAbstractionInformation().encodeLocation(locationVariables.get().second, edge.get().getDestination(destinationIndex).getLocationIndex()).template toAdd<ValueType>();
}
+ result += tmp;
}
storm::dd::Add<DdType, ValueType> tmp = this->getAbstractionInformation().getDdManager().template getAddOne<ValueType>();
@@ -675,6 +676,7 @@ namespace storm {
tmp *= this->getAbstractionInformation().encodePlayer1Choice(edgeId, this->getAbstractionInformation().getPlayer1VariableCount()).template toAdd<ValueType>();
result *= tmp;
+
return result;
}
diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h
index 1653d76ea..3d1a9397e 100644
--- a/src/storm/cli/entrypoints.h
+++ b/src/storm/cli/entrypoints.h
@@ -129,7 +129,7 @@ namespace storm {
modelCheckingWatch.stop();
if (result) {
STORM_PRINT_AND_LOG("Result (initial states): ");
- STORM_PRINT_AND_LOG(*result);
+ STORM_PRINT_AND_LOG(*result << std::endl);
STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
} else {
STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl);
diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
index 644584740..b1468d87a 100644
--- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
+++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
@@ -342,7 +342,6 @@ namespace storm {
storm::dd::Bdd<Type> globalConstraintStates = abstractor->getStates(constraintExpression);
storm::dd::Bdd<Type> globalTargetStates = abstractor->getStates(targetStateExpression);
- // globalTargetStates.template toAdd<ValueType>().exportToDot("target.dot");
// Enter the main-loop of abstraction refinement.
boost::optional<QualitativeResultMinMax<Type>> previousQualitativeResult = boost::none;
@@ -368,7 +367,9 @@ namespace storm {
}
// #ifdef LOCAL_DEBUG
+ // targetStates.template toAdd<ValueType>().exportToDot("target.dot");
// abstractor->exportToDot("game" + std::to_string(iterations) + ".dot", targetStates, game.getManager().getBddOne());
+ // game.getReachableStates().template toAdd<ValueType>().exportToDot("reach.dot");
// #endif
// (3) compute all states with probability 0/1 wrt. to the two different player 2 goals (min/max).
diff --git a/src/storm/storage/expressions/LinearityCheckVisitor.cpp b/src/storm/storage/expressions/LinearityCheckVisitor.cpp
index 44cb70728..18198ca0e 100644
--- a/src/storm/storage/expressions/LinearityCheckVisitor.cpp
+++ b/src/storm/storage/expressions/LinearityCheckVisitor.cpp
@@ -12,19 +12,44 @@ namespace storm {
// Intentionally left empty.
}
- bool LinearityCheckVisitor::check(Expression const& expression) {
- LinearityStatus result = boost::any_cast<LinearityStatus>(expression.getBaseExpression().accept(*this, boost::none));
+ bool LinearityCheckVisitor::check(Expression const& expression, bool booleanIsLinear) {
+ LinearityStatus result = boost::any_cast<LinearityStatus>(expression.getBaseExpression().accept(*this, booleanIsLinear));
return result == LinearityStatus::LinearWithoutVariables || result == LinearityStatus::LinearContainsVariables;
}
- boost::any LinearityCheckVisitor::visit(IfThenElseExpression const&, boost::any const&) {
- // An if-then-else expression is never linear.
- return LinearityStatus::NonLinear;
+ boost::any LinearityCheckVisitor::visit(IfThenElseExpression const& expression, boost::any const& data) {
+ bool booleanIsLinear = boost::any_cast<bool>(data);
+
+ if (booleanIsLinear) {
+ auto conditionResult = boost::any_cast<LinearityStatus>(expression.getCondition()->accept(*this, booleanIsLinear));
+ auto thenResult = boost::any_cast<LinearityStatus>(expression.getThenExpression()->accept(*this, booleanIsLinear));
+ auto elseResult = boost::any_cast<LinearityStatus>(expression.getElseExpression()->accept(*this, booleanIsLinear));
+
+ if (conditionResult != LinearityStatus::NonLinear && thenResult != LinearityStatus::NonLinear && elseResult != LinearityStatus::NonLinear) {
+ return LinearityStatus::LinearContainsVariables;
+ } else {
+ return LinearityStatus::NonLinear;
+ }
+ } else {
+ return LinearityStatus::NonLinear;
+ }
}
- boost::any LinearityCheckVisitor::visit(BinaryBooleanFunctionExpression const&, boost::any const&) {
- // Boolean function applications are not allowed in linear expressions.
- return LinearityStatus::NonLinear;
+ boost::any LinearityCheckVisitor::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) {
+ bool booleanIsLinear = boost::any_cast<bool>(data);
+
+ if (booleanIsLinear) {
+ auto leftResult = boost::any_cast<LinearityStatus>(expression.getFirstOperand()->accept(*this, booleanIsLinear));
+ auto rightResult = boost::any_cast<LinearityStatus>(expression.getSecondOperand()->accept(*this, booleanIsLinear));
+
+ if (leftResult != LinearityStatus::NonLinear && rightResult != LinearityStatus::NonLinear) {
+ return LinearityStatus::LinearContainsVariables;
+ } else {
+ return LinearityStatus::NonLinear;
+ }
+ } else {
+ return LinearityStatus::NonLinear;
+ }
}
boost::any LinearityCheckVisitor::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) {
@@ -56,15 +81,37 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Illegal binary numerical expression operator.");
}
- boost::any LinearityCheckVisitor::visit(BinaryRelationExpression const&, boost::any const&) {
- return LinearityStatus::NonLinear;
+ boost::any LinearityCheckVisitor::visit(BinaryRelationExpression const& expression, boost::any const& data) {
+ bool booleanIsLinear = boost::any_cast<bool>(data);
+
+ if (booleanIsLinear) {
+ auto leftResult = boost::any_cast<LinearityStatus>(expression.getFirstOperand()->accept(*this, booleanIsLinear));
+ auto rightResult = boost::any_cast<LinearityStatus>(expression.getSecondOperand()->accept(*this, booleanIsLinear));
+
+ if (leftResult != LinearityStatus::NonLinear && rightResult != LinearityStatus::NonLinear) {
+ return LinearityStatus::LinearContainsVariables;
+ } else {
+ return LinearityStatus::NonLinear;
+ }
+ } else {
+ return LinearityStatus::NonLinear;
+ }
}
boost::any LinearityCheckVisitor::visit(VariableExpression const&, boost::any const&) {
return LinearityStatus::LinearContainsVariables;
}
- boost::any LinearityCheckVisitor::visit(UnaryBooleanFunctionExpression const&, boost::any const&) {
+ boost::any LinearityCheckVisitor::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) {
+ bool booleanIsLinear = boost::any_cast<bool>(data);
+
+ if (booleanIsLinear) {
+ return boost::any_cast<LinearityStatus>(expression.getOperand()->accept(*this, booleanIsLinear));
+ } else {
+ return LinearityStatus::NonLinear;
+ }
+
+
// Boolean function applications are not allowed in linear expressions.
return LinearityStatus::NonLinear;
}
@@ -78,8 +125,14 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Illegal unary numerical expression operator.");
}
- boost::any LinearityCheckVisitor::visit(BooleanLiteralExpression const&, boost::any const&) {
- return LinearityStatus::NonLinear;
+ boost::any LinearityCheckVisitor::visit(BooleanLiteralExpression const& expression, boost::any const& data) {
+ bool booleanIsLinear = boost::any_cast<bool>(data);
+
+ if (booleanIsLinear) {
+ return LinearityStatus::LinearWithoutVariables;
+ } else {
+ return LinearityStatus::NonLinear;
+ }
}
boost::any LinearityCheckVisitor::visit(IntegerLiteralExpression const&, boost::any const&) {
diff --git a/src/storm/storage/expressions/LinearityCheckVisitor.h b/src/storm/storage/expressions/LinearityCheckVisitor.h
index 735481038..876869313 100644
--- a/src/storm/storage/expressions/LinearityCheckVisitor.h
+++ b/src/storm/storage/expressions/LinearityCheckVisitor.h
@@ -17,8 +17,9 @@ namespace storm {
* Checks that the given expression is linear.
*
* @param expression The expression to check for linearity.
+ * @param booleanIsLinear A flag indicating whether boolean components are considered linear.
*/
- bool check(Expression const& expression);
+ bool check(Expression const& expression, bool booleanIsLinear = false);
virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override;
virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) override;
diff --git a/src/storm/storage/jani/Assignment.cpp b/src/storm/storage/jani/Assignment.cpp
index 3b4f97a63..ba0b41c2a 100644
--- a/src/storm/storage/jani/Assignment.cpp
+++ b/src/storm/storage/jani/Assignment.cpp
@@ -46,7 +46,7 @@ namespace storm {
bool Assignment::isLinear() const {
storm::expressions::LinearityCheckVisitor linearityChecker;
- return linearityChecker.check(this->getAssignedExpression());
+ return linearityChecker.check(this->getAssignedExpression(), true);
}
std::ostream& operator<<(std::ostream& stream, Assignment const& assignment) {
diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp
index e02bac355..193e7388d 100644
--- a/src/storm/storage/jani/Model.cpp
+++ b/src/storm/storage/jani/Model.cpp
@@ -1124,7 +1124,7 @@ namespace storm {
bool result = true;
storm::expressions::LinearityCheckVisitor linearityChecker;
- result &= linearityChecker.check(this->getInitialStatesExpression());
+ result &= linearityChecker.check(this->getInitialStatesExpression(), true);
for (auto const& automaton : this->getAutomata()) {
result &= automaton.isLinear();
diff --git a/src/storm/storage/jani/TemplateEdge.cpp b/src/storm/storage/jani/TemplateEdge.cpp
index ef4adadf2..07b305ffc 100644
--- a/src/storm/storage/jani/TemplateEdge.cpp
+++ b/src/storm/storage/jani/TemplateEdge.cpp
@@ -139,7 +139,7 @@ namespace storm {
bool TemplateEdge::isLinear() const {
storm::expressions::LinearityCheckVisitor linearityChecker;
- bool result = linearityChecker.check(this->getGuard());
+ bool result = linearityChecker.check(this->getGuard(), true);
for (auto const& destination : destinations) {
result &= destination.isLinear();
}
From 37823d0bdab410584d10f36ab4cd9e751e61d8b5 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 26 Jan 2017 12:04:07 +0100
Subject: [PATCH 03/24] Fixed a configuration issue pointed out by Joachim
Klein
---
resources/3rdparty/CMakeLists.txt | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt
index 57b50fd5c..4077d6230 100644
--- a/resources/3rdparty/CMakeLists.txt
+++ b/resources/3rdparty/CMakeLists.txt
@@ -368,7 +368,7 @@ message(STATUS "Storm - Using shipped version of sylvan.")
message(STATUS "Storm - Linking with sylvan.")
add_imported_library(sylvan STATIC ${Sylvan_LIBRARY} ${Sylvan_INCLUDE_DIR})
add_dependencies(sylvan_STATIC sylvan)
-if(USE_SHIPPED_CARL)
+if(STORM_SHIPPED_CARL)
add_dependencies(sylvan carl)
endif()
list(APPEND STORM_DEP_TARGETS sylvan_STATIC)
From c467fa5f38729914b358f454aa2a899877ba76b3 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 31 Jan 2017 22:01:09 +0100
Subject: [PATCH 04/24] printing -1 as infinity for rational numbers and added
clipping result to valid range where appropriate
---
.../prctl/helper/HybridDtmcPrctlHelper.cpp | 3 +-
.../prctl/helper/SparseDtmcPrctlHelper.cpp | 2 +
.../ExplicitQuantitativeCheckResult.cpp | 48 ++++++++++++---
.../solver/EigenLinearEquationSolver.cpp | 6 +-
.../solver/GmmxxLinearEquationSolver.cpp | 7 +++
src/storm/solver/LinearEquationSolver.cpp | 16 +++++
src/storm/solver/LinearEquationSolver.h | 26 +++++++-
.../solver/MinMaxLinearEquationSolver.cpp | 15 +++++
src/storm/solver/MinMaxLinearEquationSolver.h | 20 +++++++
.../StandardMinMaxLinearEquationSolver.cpp | 6 ++
src/storm/utility/constants.cpp | 60 +++++++++++++------
src/storm/utility/vector.h | 16 +++++
12 files changed, 195 insertions(+), 30 deletions(-)
diff --git a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
index 8870456cd..af3bbc2cf 100644
--- a/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
+++ b/src/storm/modelchecker/prctl/helper/HybridDtmcPrctlHelper.cpp
@@ -73,6 +73,7 @@ namespace storm {
std::vector<ValueType> b = subvector.toVector(odd);
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(std::move(explicitSubmatrix));
+ solver->setBounds(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>());
solver->solveEquations(x, b);
// Return a hybrid check result that stores the numerical values explicitly.
@@ -140,7 +141,6 @@ namespace storm {
}
}
-
template<storm::dd::DdType DdType, typename ValueType>
std::unique_ptr<CheckResult> HybridDtmcPrctlHelper<DdType, ValueType>::computeInstantaneousRewards(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& transitionMatrix, RewardModelType const& rewardModel, uint_fast64_t stepBound, storm::solver::LinearEquationSolverFactory<ValueType> const& linearEquationSolverFactory) {
// Only compute the result if the model has at least one reward this->getModel().
@@ -238,6 +238,7 @@ namespace storm {
// Now solve the resulting equation system.
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(std::move(explicitSubmatrix));
+ solver->setLowerBound(storm::utility::zero<ValueType>());
solver->solveEquations(x, b);
// Return a hybrid check result that stores the numerical values explicitly.
diff --git a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
index 5d84bd9fb..f768a2428 100644
--- a/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
+++ b/src/storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
@@ -94,6 +94,7 @@ namespace storm {
// Now solve the created system of linear equations.
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(std::move(submatrix));
+ solver->setBounds(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>());
solver->solveEquations(x, b);
// Set values of resulting vector according to result.
@@ -217,6 +218,7 @@ namespace storm {
// Now solve the resulting equation system.
std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(std::move(submatrix));
+ solver->setLowerBound(storm::utility::zero<ValueType>());
solver->solveEquations(x, b);
// Set values of resulting vector according to result.
diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
index a4dd5f96c..5ea662a57 100644
--- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
+++ b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
@@ -122,10 +122,12 @@ namespace storm {
ValueType sum = storm::utility::zero<ValueType>();
if (this->isResultForAllStates()) {
for (auto& element : boost::get<vector_type>(values)) {
+ STORM_LOG_THROW(element != storm::utility::infinity<ValueType>(), storm::exceptions::InvalidOperationException, "Cannot compute the sum of values containing infinity.");
sum += element;
}
} else {
for (auto& element : boost::get<map_type>(values)) {
+ STORM_LOG_THROW(element.second != storm::utility::infinity<ValueType>(), storm::exceptions::InvalidOperationException, "Cannot compute the sum of values containing infinity.");
sum += element.second;
}
}
@@ -139,11 +141,13 @@ namespace storm {
ValueType sum = storm::utility::zero<ValueType>();
if (this->isResultForAllStates()) {
for (auto& element : boost::get<vector_type>(values)) {
+ STORM_LOG_THROW(element != storm::utility::infinity<ValueType>(), storm::exceptions::InvalidOperationException, "Cannot compute the average of values containing infinity.");
sum += element;
}
return sum / boost::get<vector_type>(values).size();
} else {
for (auto& element : boost::get<map_type>(values)) {
+ STORM_LOG_THROW(element.second != storm::utility::infinity<ValueType>(), storm::exceptions::InvalidOperationException, "Cannot compute the average of values containing infinity.");
sum += element.second;
}
return sum / boost::get<map_type>(values).size();
@@ -168,17 +172,47 @@ namespace storm {
template<typename ValueType>
void print(std::ostream& out, ValueType const& value) {
- out << value;
- if (std::is_same<ValueType, storm::RationalNumber>::value) {
- out << " (approx. " << storm::utility::convertNumber<double>(value) << ")";
+ if (value == storm::utility::infinity<ValueType>()) {
+ out << "inf";
+ } else {
+ out << value;
+ if (std::is_same<ValueType, storm::RationalNumber>::value) {
+ out << " (approx. " << storm::utility::convertNumber<double>(value) << ")";
+ }
}
}
template<typename ValueType>
- void printApproxRange(std::ostream& out, ValueType const& min, ValueType const& max) {
+ void printRange(std::ostream& out, ValueType const& min, ValueType const& max) {
+ out << "[";
+ if (min == storm::utility::infinity<ValueType>()) {
+ out << "inf";
+ } else {
+ out << min;
+ }
+ out << ", ";
+ if (max == storm::utility::infinity<ValueType>()) {
+ out << "inf";
+ } else {
+ out << max;
+ }
+ out << "]";
if (std::is_same<ValueType, storm::RationalNumber>::value) {
- out << " (approx. [" << storm::utility::convertNumber<double>(min) << ", " << storm::utility::convertNumber<double>(max) << "])";
+ out << " (approx. [";
+ if (min == storm::utility::infinity<ValueType>()) {
+ out << "inf";
+ } else {
+ out << storm::utility::convertNumber<double>(min);
+ }
+ out << ", ";
+ if (max == storm::utility::infinity<ValueType>()) {
+ out << "inf";
+ } else {
+ out << storm::utility::convertNumber<double>(max);
+ }
+ out << "])";
}
+ out << " (range)";
}
template<typename ValueType>
@@ -228,9 +262,7 @@ namespace storm {
if (printAsRange) {
std::pair<ValueType, ValueType> minmax = this->getMinMax();
- out << "[" << minmax.first << ", " << minmax.second << "]";
- printApproxRange(out, minmax.first, minmax.second);
- out << " (range)";
+ printRange(out, minmax.first, minmax.second);
}
return out;
diff --git a/src/storm/solver/EigenLinearEquationSolver.cpp b/src/storm/solver/EigenLinearEquationSolver.cpp
index bf80f4db9..b05fe6add 100644
--- a/src/storm/solver/EigenLinearEquationSolver.cpp
+++ b/src/storm/solver/EigenLinearEquationSolver.cpp
@@ -5,6 +5,7 @@
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/EigenEquationSolverSettings.h"
+#include "storm/utility/vector.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidSettingsException.h"
@@ -230,6 +231,9 @@ namespace storm {
}
}
+ // Make sure that all results conform to the bounds.
+ storm::utility::vector::clip(x, this->lowerBound, this->upperBound);
+
// Check if the solver converged and issue a warning otherwise.
if (converged) {
STORM_LOG_DEBUG("Iterative solver converged after " << numberOfIterations << " iterations.");
@@ -240,7 +244,7 @@ namespace storm {
}
}
- return false;
+ return true;
}
template<typename ValueType>
diff --git a/src/storm/solver/GmmxxLinearEquationSolver.cpp b/src/storm/solver/GmmxxLinearEquationSolver.cpp
index c92817ac2..31c358a22 100644
--- a/src/storm/solver/GmmxxLinearEquationSolver.cpp
+++ b/src/storm/solver/GmmxxLinearEquationSolver.cpp
@@ -13,6 +13,7 @@
#include "storm/solver/NativeLinearEquationSolver.h"
#include "storm/utility/gmm.h"
+#include "storm/utility/vector.h"
namespace storm {
namespace solver {
@@ -191,6 +192,9 @@ namespace storm {
clearCache();
}
+ // Make sure that all results conform to the bounds.
+ storm::utility::vector::clip(x, this->lowerBound, this->upperBound);
+
// Check if the solver converged and issue a warning otherwise.
if (iter.converged()) {
STORM_LOG_DEBUG("Iterative solver converged after " << iter.get_iteration() << " iterations.");
@@ -202,6 +206,9 @@ namespace storm {
} else if (method == GmmxxLinearEquationSolverSettings<ValueType>::SolutionMethod::Jacobi) {
uint_fast64_t iterations = solveLinearEquationSystemWithJacobi(x, b);
+ // Make sure that all results conform to the bounds.
+ storm::utility::vector::clip(x, this->lowerBound, this->upperBound);
+
// Check if the solver converged and issue a warning otherwise.
if (iterations < this->getSettings().getMaximalNumberOfIterations()) {
STORM_LOG_DEBUG("Iterative solver converged after " << iterations << " iterations.");
diff --git a/src/storm/solver/LinearEquationSolver.cpp b/src/storm/solver/LinearEquationSolver.cpp
index ca1eeda94..487b77f89 100644
--- a/src/storm/solver/LinearEquationSolver.cpp
+++ b/src/storm/solver/LinearEquationSolver.cpp
@@ -74,6 +74,22 @@ namespace storm {
cachedRowVector.reset();
}
+ template<typename ValueType>
+ void LinearEquationSolver<ValueType>::setLowerBound(ValueType const& value) {
+ lowerBound = value;
+ }
+
+ template<typename ValueType>
+ void LinearEquationSolver<ValueType>::setUpperBound(ValueType const& value) {
+ upperBound = value;
+ }
+
+ template<typename ValueType>
+ void LinearEquationSolver<ValueType>::setBounds(ValueType const& lower, ValueType const& upper) {
+ setLowerBound(lower);
+ setUpperBound(upper);
+ }
+
template<typename ValueType>
std::unique_ptr<LinearEquationSolver<ValueType>> LinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType>&& matrix) const {
return create(matrix);
diff --git a/src/storm/solver/LinearEquationSolver.h b/src/storm/solver/LinearEquationSolver.h
index 4912070d7..b94626cd2 100644
--- a/src/storm/solver/LinearEquationSolver.h
+++ b/src/storm/solver/LinearEquationSolver.h
@@ -70,7 +70,7 @@ namespace storm {
/*!
* Sets whether some of the generated data during solver calls should be cached.
- * This possibly decreases the runtime of subsequent calls but also increases memory consumption.
+ * This possibly increases the runtime of subsequent calls but also increases memory consumption.
*/
void setCachingEnabled(bool value) const;
@@ -83,11 +83,32 @@ namespace storm {
* Clears the currently cached data that has been stored during previous calls of the solver.
*/
virtual void clearCache() const;
+
+ /*!
+ * Sets a lower bound for the solution that can potentially used by the solver.
+ */
+ void setLowerBound(ValueType const& value);
+
+ /*!
+ * Sets an upper bound for the solution that can potentially used by the solver.
+ */
+ void setUpperBound(ValueType const& value);
+
+ /*!
+ * Sets bounds for the solution that can potentially used by the solver.
+ */
+ void setBounds(ValueType const& lower, ValueType const& upper);
protected:
// auxiliary storage. If set, this vector has getMatrixRowCount() entries.
mutable std::unique_ptr<std::vector<ValueType>> cachedRowVector;
-
+
+ // A lower bound if one was set.
+ boost::optional<ValueType> lowerBound;
+
+ // An upper bound if one was set.
+ boost::optional<ValueType> upperBound;
+
private:
/*!
* Retrieves the row count of the matrix associated with this solver.
@@ -101,7 +122,6 @@ namespace storm {
/// Whether some of the generated data during solver calls should be cached.
mutable bool cachingEnabled;
-
};
template<typename ValueType>
diff --git a/src/storm/solver/MinMaxLinearEquationSolver.cpp b/src/storm/solver/MinMaxLinearEquationSolver.cpp
index e7a332e13..02269a248 100644
--- a/src/storm/solver/MinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/MinMaxLinearEquationSolver.cpp
@@ -98,6 +98,21 @@ namespace storm {
// Intentionally left empty.
}
+ template<typename ValueType>
+ void MinMaxLinearEquationSolver<ValueType>::setLowerBound(ValueType const& value) {
+ lowerBound = value;
+ }
+
+ template<typename ValueType>
+ void MinMaxLinearEquationSolver<ValueType>::setUpperBound(ValueType const& value) {
+ upperBound = value;
+ }
+
+ template<typename ValueType>
+ void MinMaxLinearEquationSolver<ValueType>::setBounds(ValueType const& lower, ValueType const& upper) {
+ setLowerBound(lower);
+ setUpperBound(upper);
+ }
template<typename ValueType>
MinMaxLinearEquationSolverFactory<ValueType>::MinMaxLinearEquationSolverFactory(bool trackScheduler) : trackScheduler(trackScheduler) {
diff --git a/src/storm/solver/MinMaxLinearEquationSolver.h b/src/storm/solver/MinMaxLinearEquationSolver.h
index 592f00067..473438a38 100644
--- a/src/storm/solver/MinMaxLinearEquationSolver.h
+++ b/src/storm/solver/MinMaxLinearEquationSolver.h
@@ -145,6 +145,20 @@ namespace storm {
*/
virtual void clearCache() const;
+ /*!
+ * Sets a lower bound for the solution that can potentially used by the solver.
+ */
+ void setLowerBound(ValueType const& value);
+
+ /*!
+ * Sets an upper bound for the solution that can potentially used by the solver.
+ */
+ void setUpperBound(ValueType const& value);
+
+ /*!
+ * Sets bounds for the solution that can potentially used by the solver.
+ */
+ void setBounds(ValueType const& lower, ValueType const& upper);
protected:
/// The optimization direction to use for calls to functions that do not provide it explicitly. Can also be unset.
@@ -156,6 +170,12 @@ namespace storm {
/// The scheduler (if it could be successfully generated).
mutable boost::optional<std::unique_ptr<storm::storage::TotalScheduler>> scheduler;
+ // A lower bound if one was set.
+ boost::optional<ValueType> lowerBound;
+
+ // An upper bound if one was set.
+ boost::optional<ValueType> upperBound;
+
private:
/// Whether some of the generated data during solver calls should be cached.
bool cachingEnabled;
diff --git a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp
index 7a6e54df5..c9c405341 100644
--- a/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/StandardMinMaxLinearEquationSolver.cpp
@@ -112,6 +112,12 @@ namespace storm {
// Create a solver that we will use throughout the procedure. We will modify the matrix in each iteration.
auto solver = linearEquationSolverFactory->create(std::move(submatrix));
+ if (this->lowerBound) {
+ solver->setLowerBound(this->lowerBound.get());
+ }
+ if (this->upperBound) {
+ solver->setUpperBound(this->upperBound.get());
+ }
solver->setCachingEnabled(true);
Status status = Status::InProgress;
diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp
index 7eeae8106..a6326d5e8 100644
--- a/src/storm/utility/constants.cpp
+++ b/src/storm/utility/constants.cpp
@@ -226,6 +226,26 @@ namespace storm {
return std::make_pair(min, max);
}
+ template<>
+ std::pair<storm::RationalNumber, storm::RationalNumber> minmax(std::vector<storm::RationalNumber> const& values) {
+ assert(!values.empty());
+ storm::RationalNumber min = values.front();
+ storm::RationalNumber max = values.front();
+ for (auto const& vt : values) {
+ if (vt == storm::utility::infinity<storm::RationalNumber>()) {
+ max = vt;
+ } else {
+ if (vt < min) {
+ min = vt;
+ }
+ if (vt > max) {
+ max = vt;
+ }
+ }
+ }
+ return std::make_pair(min, max);
+ }
+
template<>
storm::RationalFunction minimum(std::vector<storm::RationalFunction> const&) {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum for rational functions is not defined.");
@@ -251,7 +271,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Maximum/maximum for rational functions is not defined.");
}
- template< typename K, typename ValueType>
+ template<typename K, typename ValueType>
std::pair<ValueType, ValueType> minmax(std::map<K, ValueType> const& values) {
assert(!values.empty());
ValueType min = values.begin()->second;
@@ -267,6 +287,26 @@ namespace storm {
return std::make_pair(min, max);
}
+ template<>
+ std::pair<storm::RationalNumber, storm::RationalNumber> minmax(std::map<uint64_t, storm::RationalNumber> const& values) {
+ assert(!values.empty());
+ storm::RationalNumber min = values.begin()->second;
+ storm::RationalNumber max = values.begin()->second;
+ for (auto const& vt : values) {
+ if (vt.second == storm::utility::infinity<storm::RationalNumber>()) {
+ max = vt.second;
+ } else {
+ if (vt.second < min) {
+ min = vt.second;
+ }
+ if (vt.second > max) {
+ max = vt.second;
+ }
+ }
+ }
+ return std::make_pair(min, max);
+ }
+
template<>
storm::RationalFunction minimum(std::map<uint64_t, storm::RationalFunction> const&) {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum for rational functions is not defined.");
@@ -274,14 +314,7 @@ namespace storm {
template< typename K, typename ValueType>
ValueType minimum(std::map<K, ValueType> const& values) {
- assert(!values.empty());
- ValueType min = values.begin()->second;
- for (auto const& vt : values) {
- if (vt.second < min) {
- min = vt.second;
- }
- }
- return min;
+ return minmax(values).first;
}
template<>
@@ -291,14 +324,7 @@ namespace storm {
template<typename K, typename ValueType>
ValueType maximum(std::map<K, ValueType> const& values) {
- assert(!values.empty());
- ValueType max = values.begin()->second;
- for (auto const& vt : values) {
- if (vt.second > max) {
- max = vt.second;
- }
- }
- return max;
+ return minmax(values).second;
}
#ifdef STORM_HAVE_CARL
diff --git a/src/storm/utility/vector.h b/src/storm/utility/vector.h
index dc22fa310..578a942a8 100644
--- a/src/storm/utility/vector.h
+++ b/src/storm/utility/vector.h
@@ -12,6 +12,8 @@
#include <numeric>
#include <storm/adapters/CarlAdapter.h>
+#include <boost/optional.hpp>
+
#include "storm/storage/BitVector.h"
#include "storm/utility/constants.h"
#include "storm/utility/macros.h"
@@ -738,6 +740,20 @@ namespace storm {
return true;
}
+ /*!
+ * Takes the input vector and ensures that all entries conform to the bounds.
+ */
+ template <typename ValueType>
+ void clip(std::vector<ValueType>& x, boost::optional<ValueType> const& lowerBound, boost::optional<ValueType> const& upperBound) {
+ for (auto& entry : x) {
+ if (lowerBound && entry < lowerBound.get()) {
+ entry = lowerBound.get();
+ } else if (upperBound && entry > upperBound.get()) {
+ entry = upperBound.get();
+ }
+ }
+ }
+
/*!
* Takes the given offset vector and applies the given contraint. That is, it produces another offset vector that contains
* the relative offsets of the entries given by the constraint.
From 03b634d14ae9adc7a414973023cafdbe68cc4e73 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Wed, 1 Feb 2017 13:45:10 +0100
Subject: [PATCH 05/24] suppress silly warning about no return after error
---
src/storm/parser/JaniParser.cpp | 2 ++
1 file changed, 2 insertions(+)
diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp
index 517c663ce..efe033d08 100644
--- a/src/storm/parser/JaniParser.cpp
+++ b/src/storm/parser/JaniParser.cpp
@@ -939,6 +939,8 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "No supported operator declaration found for complex expressions as " << expressionStructure.dump() << " in " << scopeDescription << ".");
}
assert(false);
+ // Silly warning suppression.
+ return storm::expressions::Expression();
}
From 41ffc5b82869f228f608b2fa36ae190d0c5bb2c6 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 2 Feb 2017 09:06:10 +0100
Subject: [PATCH 06/24] added cmake option to toggle link-time-optimization
---
CMakeLists.txt | 8 +++++++-
1 file changed, 7 insertions(+), 1 deletion(-)
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 7162aa250..2e76a3129 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -23,6 +23,8 @@ include(imported)
#############################################################
option(STORM_DEVELOPER "Sets whether the development mode is used." OFF)
option(STORM_ALLWARNINGS "Compile with even more warnings" OFF)
+option(STORM_USE_LTO "Sets whether link-time optimizations are enabled." ON)
+MARK_AS_ADVANCED(STORM_USE_LTO)
option(STORM_PORTABLE_RELEASE "Sets whether a release build needs to be portable to another machine." OFF)
MARK_AS_ADVANCED(STORM_PORTABLE_RELEASE)
option(STORM_USE_POPCNT "Sets whether the popcnt instruction is going to be used." ON)
@@ -215,7 +217,7 @@ if (STORM_COMPILER_CLANG OR STORM_COMPILER_APPLECLANG)
endif()
set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++14 -stdlib=${CLANG_STDLIB} -ftemplate-depth=1024")
- set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -flto -ffast-math -fno-finite-math-only")
+ set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -ffast-math -fno-finite-math-only")
set (CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} -Wl,-export_dynamic")
set (CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -Wl,-export_dynamic")
elseif (STORM_COMPILER_GCC)
@@ -225,6 +227,10 @@ elseif (STORM_COMPILER_GCC)
set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -rdynamic")
endif ()
+if (STORM_USE_LTO)
+ set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -flto")
+endif()
+
# In release mode, we turn on even more optimizations if we do not have to provide a portable binary.
if (NOT STORM_PORTABLE_RELEASE)
set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -march=native")
From ac1ca72094e52fb92e8de988db0eba21f5f2f99f Mon Sep 17 00:00:00 2001
From: JK <klein@tcs.inf.tu-dresden.de>
Date: Thu, 2 Feb 2017 09:57:54 +0100
Subject: [PATCH 07/24] Add support for ITE expression in the likelihood part
of commands (exact, parametric engine)
Support the conversion to rational numbers / rational functions for ITE expressions. Example:
... -> (s<4 ? p : q):(s'=...)
where s is a state variable and p, q are constants or parameters.
---
src/storm/storage/expressions/ExpressionEvaluator.cpp | 4 ++--
.../storage/expressions/ToRationalFunctionVisitor.cpp | 11 ++++++++---
.../storage/expressions/ToRationalFunctionVisitor.h | 6 +++++-
.../storage/expressions/ToRationalNumberVisitor.cpp | 11 ++++++++---
.../storage/expressions/ToRationalNumberVisitor.h | 6 +++++-
5 files changed, 28 insertions(+), 10 deletions(-)
diff --git a/src/storm/storage/expressions/ExpressionEvaluator.cpp b/src/storm/storage/expressions/ExpressionEvaluator.cpp
index abea0ce73..3305ec772 100644
--- a/src/storm/storage/expressions/ExpressionEvaluator.cpp
+++ b/src/storm/storage/expressions/ExpressionEvaluator.cpp
@@ -33,7 +33,7 @@ namespace storm {
}
#ifdef STORM_HAVE_CARL
- ExpressionEvaluator<RationalNumber>::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExprtkExpressionEvaluatorBase<RationalNumber>(manager) {
+ ExpressionEvaluator<RationalNumber>::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExprtkExpressionEvaluatorBase<RationalNumber>(manager), rationalNumberVisitor(*this) {
// Intentionally left empty.
}
@@ -57,7 +57,7 @@ namespace storm {
return this->rationalNumberVisitor.toRationalNumber(expression);
}
- ExpressionEvaluator<RationalFunction>::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExprtkExpressionEvaluatorBase<RationalFunction>(manager) {
+ ExpressionEvaluator<RationalFunction>::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExprtkExpressionEvaluatorBase<RationalFunction>(manager), rationalFunctionVisitor(*this) {
// Intentionally left empty.
}
diff --git a/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp b/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp
index 9f8ab16ec..6fa620157 100644
--- a/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp
+++ b/src/storm/storage/expressions/ToRationalFunctionVisitor.cpp
@@ -11,7 +11,7 @@ namespace storm {
#ifdef STORM_HAVE_CARL
template<typename RationalFunctionType>
- ToRationalFunctionVisitor<RationalFunctionType>::ToRationalFunctionVisitor() : ExpressionVisitor(), cache(new carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>()) {
+ ToRationalFunctionVisitor<RationalFunctionType>::ToRationalFunctionVisitor(ExpressionEvaluatorBase<RationalFunctionType> const& evaluator) : ExpressionVisitor(), cache(new carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>()), evaluator(evaluator) {
// Intentionally left empty.
}
@@ -21,8 +21,13 @@ namespace storm {
}
template<typename RationalFunctionType>
- boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(IfThenElseExpression const&, boost::any const&) {
- STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function.");
+ boost::any ToRationalFunctionVisitor<RationalFunctionType>::visit(IfThenElseExpression const& expression, boost::any const& data) {
+ bool conditionValue = evaluator.asBool(expression.getCondition());
+ if (conditionValue) {
+ return expression.getThenExpression()->accept(*this, data);
+ } else {
+ return expression.getElseExpression()->accept(*this, data);
+ }
}
template<typename RationalFunctionType>
diff --git a/src/storm/storage/expressions/ToRationalFunctionVisitor.h b/src/storm/storage/expressions/ToRationalFunctionVisitor.h
index 7c7cfacf5..6e90d36ce 100644
--- a/src/storm/storage/expressions/ToRationalFunctionVisitor.h
+++ b/src/storm/storage/expressions/ToRationalFunctionVisitor.h
@@ -8,6 +8,7 @@
#include "storm/storage/expressions/Expression.h"
#include "storm/storage/expressions/Expressions.h"
#include "storm/storage/expressions/ExpressionVisitor.h"
+#include "storm/storage/expressions/ExpressionEvaluatorBase.h"
#include "storm/storage/expressions/Variable.h"
namespace storm {
@@ -17,7 +18,7 @@ namespace storm {
template<typename RationalFunctionType>
class ToRationalFunctionVisitor : public ExpressionVisitor {
public:
- ToRationalFunctionVisitor();
+ ToRationalFunctionVisitor(ExpressionEvaluatorBase<RationalFunctionType> const& evaluator);
RationalFunctionType toRationalFunction(Expression const& expression);
@@ -53,6 +54,9 @@ namespace storm {
// A mapping from variables to their values.
std::unordered_map<storm::expressions::Variable, RationalFunctionType> valueMapping;
+
+ // A reference to an expression evaluator (mainly for resolving the boolean condition in IfThenElse expressions)
+ ExpressionEvaluatorBase<RationalFunctionType> const& evaluator;
};
#endif
}
diff --git a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp
index d4ba17c06..26ad15b5a 100644
--- a/src/storm/storage/expressions/ToRationalNumberVisitor.cpp
+++ b/src/storm/storage/expressions/ToRationalNumberVisitor.cpp
@@ -8,7 +8,7 @@
namespace storm {
namespace expressions {
template<typename RationalNumberType>
- ToRationalNumberVisitor<RationalNumberType>::ToRationalNumberVisitor() : ExpressionVisitor() {
+ ToRationalNumberVisitor<RationalNumberType>::ToRationalNumberVisitor(ExpressionEvaluatorBase<RationalNumberType> const& evaluator) : ExpressionVisitor(), evaluator(evaluator) {
// Intentionally left empty.
}
@@ -18,8 +18,13 @@ namespace storm {
}
template<typename RationalNumberType>
- boost::any ToRationalNumberVisitor<RationalNumberType>::visit(IfThenElseExpression const&, boost::any const&) {
- STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number.");
+ boost::any ToRationalNumberVisitor<RationalNumberType>::visit(IfThenElseExpression const& expression, boost::any const& data) {
+ bool conditionValue = evaluator.asBool(expression.getCondition());
+ if (conditionValue) {
+ return expression.getThenExpression()->accept(*this, data);
+ } else {
+ return expression.getElseExpression()->accept(*this, data);
+ }
}
template<typename RationalNumberType>
diff --git a/src/storm/storage/expressions/ToRationalNumberVisitor.h b/src/storm/storage/expressions/ToRationalNumberVisitor.h
index 6177fd2ae..89cb9f81f 100644
--- a/src/storm/storage/expressions/ToRationalNumberVisitor.h
+++ b/src/storm/storage/expressions/ToRationalNumberVisitor.h
@@ -7,6 +7,7 @@
#include "storm/storage/expressions/Expression.h"
#include "storm/storage/expressions/Expressions.h"
#include "storm/storage/expressions/ExpressionVisitor.h"
+#include "storm/storage/expressions/ExpressionEvaluatorBase.h"
#include "storm/storage/expressions/Variable.h"
namespace storm {
@@ -15,7 +16,7 @@ namespace storm {
template<typename RationalNumberType>
class ToRationalNumberVisitor : public ExpressionVisitor {
public:
- ToRationalNumberVisitor();
+ ToRationalNumberVisitor(ExpressionEvaluatorBase<RationalNumberType> const& evaluator);
RationalNumberType toRationalNumber(Expression const& expression);
@@ -34,6 +35,9 @@ namespace storm {
private:
std::unordered_map<storm::expressions::Variable, RationalNumberType> valueMapping;
+
+ // A reference to an expression evaluator (mainly for resolving the boolean condition in IfThenElse expressions)
+ ExpressionEvaluatorBase<RationalNumberType> const& evaluator;
};
}
}
From 95bd4b788318a5951830845ae7f5f88db7041cfc Mon Sep 17 00:00:00 2001
From: JK <klein@tcs.inf.tu-dresden.de>
Date: Thu, 2 Feb 2017 16:59:44 +0100
Subject: [PATCH 08/24] Add check that undefined constants / parameters do not
appear in the 'if' part of IfThenElseExpressions
---
.../CheckIfThenElseGuardVisitor.cpp | 71 +++++++++++++++++++
.../expressions/CheckIfThenElseGuardVisitor.h | 36 ++++++++++
src/storm/storage/expressions/Expression.cpp | 7 ++
src/storm/storage/expressions/Expression.h | 10 +++
src/storm/storage/prism/Command.cpp | 5 ++
5 files changed, 129 insertions(+)
create mode 100644 src/storm/storage/expressions/CheckIfThenElseGuardVisitor.cpp
create mode 100644 src/storm/storage/expressions/CheckIfThenElseGuardVisitor.h
diff --git a/src/storm/storage/expressions/CheckIfThenElseGuardVisitor.cpp b/src/storm/storage/expressions/CheckIfThenElseGuardVisitor.cpp
new file mode 100644
index 000000000..0bbb32fba
--- /dev/null
+++ b/src/storm/storage/expressions/CheckIfThenElseGuardVisitor.cpp
@@ -0,0 +1,71 @@
+#include "storm/storage/expressions/CheckIfThenElseGuardVisitor.h"
+
+#include "storm/storage/expressions/Expressions.h"
+
+namespace storm {
+ namespace expressions {
+
+ CheckIfThenElseGuardVisitor::CheckIfThenElseGuardVisitor(std::set<storm::expressions::Variable> const& variables) : variables(variables) {
+ // Intentionally left empty.
+ }
+
+ bool CheckIfThenElseGuardVisitor::check(storm::expressions::Expression const& expression) {
+ return boost::any_cast<bool>(expression.accept(*this, boost::none));
+ }
+
+ boost::any CheckIfThenElseGuardVisitor::visit(IfThenElseExpression const& expression, boost::any const& data) {
+ // check whether the 'if' condition depends on one of the variables
+ if (expression.getCondition()->toExpression().containsVariable(variables)) {
+ return true;
+ } else {
+ // recurse
+ return
+ boost::any_cast<bool>(expression.getThenExpression()->accept(*this, data)) ||
+ boost::any_cast<bool>(expression.getElseExpression()->accept(*this, data));
+ }
+ }
+
+ boost::any CheckIfThenElseGuardVisitor::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) {
+ return
+ boost::any_cast<bool>(expression.getFirstOperand()->accept(*this, data)) ||
+ boost::any_cast<bool>(expression.getSecondOperand()->accept(*this, data));
+ }
+
+ boost::any CheckIfThenElseGuardVisitor::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) {
+ return
+ boost::any_cast<bool>(expression.getFirstOperand()->accept(*this, data)) ||
+ boost::any_cast<bool>(expression.getSecondOperand()->accept(*this, data));
+ }
+
+ boost::any CheckIfThenElseGuardVisitor::visit(BinaryRelationExpression const& expression, boost::any const& data) {
+ return
+ boost::any_cast<bool>(expression.getFirstOperand()->accept(*this, data)) ||
+ boost::any_cast<bool>(expression.getSecondOperand()->accept(*this, data));
+ }
+
+ boost::any CheckIfThenElseGuardVisitor::visit(VariableExpression const& expression, boost::any const&) {
+ return false;
+ }
+
+ boost::any CheckIfThenElseGuardVisitor::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) {
+ return expression.getOperand()->accept(*this, data);
+ }
+
+ boost::any CheckIfThenElseGuardVisitor::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) {
+ return expression.getOperand()->accept(*this, data);
+ }
+
+ boost::any CheckIfThenElseGuardVisitor::visit(BooleanLiteralExpression const& expression, boost::any const&) {
+ return false;
+ }
+
+ boost::any CheckIfThenElseGuardVisitor::visit(IntegerLiteralExpression const& expression, boost::any const&) {
+ return false;
+ }
+
+ boost::any CheckIfThenElseGuardVisitor::visit(RationalLiteralExpression const& expression, boost::any const&) {
+ return false;
+ }
+
+ }
+}
diff --git a/src/storm/storage/expressions/CheckIfThenElseGuardVisitor.h b/src/storm/storage/expressions/CheckIfThenElseGuardVisitor.h
new file mode 100644
index 000000000..e2cac82e6
--- /dev/null
+++ b/src/storm/storage/expressions/CheckIfThenElseGuardVisitor.h
@@ -0,0 +1,36 @@
+#pragma once
+
+#include "storm/storage/expressions/ExpressionVisitor.h"
+#include <set>
+
+namespace storm {
+ namespace expressions {
+
+ class Expression;
+ class Variable;
+
+ // Visits all sub-expressions and returns true if any of them is an IfThenElseExpression
+ // where the 'if' part depends on one of the variables in the set passed in the constructor.
+ class CheckIfThenElseGuardVisitor : public ExpressionVisitor {
+ public:
+ CheckIfThenElseGuardVisitor(std::set<storm::expressions::Variable> const& variables);
+
+ bool check(storm::expressions::Expression const& expression);
+
+ virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override;
+ virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) override;
+ virtual boost::any visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) override;
+ virtual boost::any visit(BinaryRelationExpression const& expression, boost::any const& data) override;
+ virtual boost::any visit(VariableExpression const& expression, boost::any const& data) override;
+ virtual boost::any visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) override;
+ virtual boost::any visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) override;
+ virtual boost::any visit(BooleanLiteralExpression const& expression, boost::any const& data) override;
+ virtual boost::any visit(IntegerLiteralExpression const& expression, boost::any const& data) override;
+ virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) override;
+
+ private:
+ std::set<storm::expressions::Variable> const& variables;
+ };
+
+ }
+}
diff --git a/src/storm/storage/expressions/Expression.cpp b/src/storm/storage/expressions/Expression.cpp
index bb3dca82f..97e7046ab 100644
--- a/src/storm/storage/expressions/Expression.cpp
+++ b/src/storm/storage/expressions/Expression.cpp
@@ -7,6 +7,7 @@
#include "storm/storage/expressions/LinearityCheckVisitor.h"
#include "storm/storage/expressions/SyntacticalEqualityCheckVisitor.h"
#include "storm/storage/expressions/ChangeManagerVisitor.h"
+#include "storm/storage/expressions/CheckIfThenElseGuardVisitor.h"
#include "storm/storage/expressions/Expressions.h"
#include "storm/exceptions/InvalidTypeException.h"
#include "storm/exceptions/InvalidArgumentException.h"
@@ -118,6 +119,12 @@ namespace storm {
std::set_intersection(variables.begin(), variables.end(), appearingVariables.begin(), appearingVariables.end(), std::inserter(intersection, intersection.begin()));
return !intersection.empty();
}
+
+ bool Expression::containsVariableInITEGuard(std::set<storm::expressions::Variable> const& variables) const {
+ CheckIfThenElseGuardVisitor visitor(variables);
+ return visitor.check(*this);
+ }
+
bool Expression::isRelationalExpression() const {
if (!this->isFunctionApplication()) {
diff --git a/src/storm/storage/expressions/Expression.h b/src/storm/storage/expressions/Expression.h
index 3d6da87c9..874a1ecda 100644
--- a/src/storm/storage/expressions/Expression.h
+++ b/src/storm/storage/expressions/Expression.h
@@ -253,6 +253,16 @@ namespace storm {
*/
bool containsVariable(std::set<storm::expressions::Variable> const& variables) const;
+
+ /*!
+ * Retrieves whether the expression contains any of the given variables in the
+ * 'if' part of any sub-IfThenElseExpressions.
+ *
+ * @param variables The variables to search for.
+ * @return True iff any of the variables appear in the 'if' part of an ITE-expression.
+ */
+ bool containsVariableInITEGuard(std::set<storm::expressions::Variable> const& variables) const;
+
/*!
* Retrieves the base expression underlying this expression object. Note that prior to calling this, the
* expression object must be properly initialized.
diff --git a/src/storm/storage/prism/Command.cpp b/src/storm/storage/prism/Command.cpp
index 89948d4c8..be40cd1eb 100644
--- a/src/storm/storage/prism/Command.cpp
+++ b/src/storm/storage/prism/Command.cpp
@@ -67,6 +67,11 @@ namespace storm {
return false;
}
}
+
+ // check likelihood, undefined constants may not occur in 'if' part of IfThenElseExpression
+ if (update.getLikelihoodExpression().containsVariableInITEGuard(undefinedConstantVariables)) {
+ return false;
+ }
}
return true;
From cbb0b1e0f0799cb3c6f44848504abe087cf453b8 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sun, 5 Feb 2017 20:44:24 +0100
Subject: [PATCH 09/24] initial work on installation of storm
---
CMakeLists.txt | 21 ++++++++++++++++++++
resources/3rdparty/CMakeLists.txt | 33 ++++++++++++++++---------------
src/storm/CMakeLists.txt | 3 ++-
3 files changed, 40 insertions(+), 17 deletions(-)
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 2e76a3129..edf817f5b 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -33,6 +33,8 @@ option(USE_BOOST_STATIC_LIBRARIES "Sets whether the Boost libraries should be li
option(STORM_USE_INTELTBB "Sets whether the Intel TBB libraries should be used." OFF)
option(STORM_USE_GUROBI "Sets whether Gurobi should be used." OFF)
option(USE_CARL "Sets whether carl should be included." ON)
+option(STORM_FORCE_SHIPPED_CARL "Sets whether the shipped version of carl is to be used no matter whether carl is found or not." OFF)
+MARK_AS_ADVANCED(STORM_FORCE_SHIPPED_CARL)
option(USE_SMTRAT "Sets whether SMT-RAT should be included." OFF)
option(USE_HYPRO "Sets whether HyPro should be included." OFF)
option(XML_SUPPORT "Sets whether xml based format parsing should be included." ON)
@@ -266,6 +268,25 @@ else()
set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -fomit-frame-pointer")
endif()
+#############################################################
+##
+## RPATH settings
+##
+#############################################################
+
+# don't skip the full RPATH for the build tree
+SET(CMAKE_SKIP_BUILD_RPATH FALSE)
+
+# when building, don't use the install RPATH already (but only when installing)
+SET(CMAKE_BUILD_WITH_INSTALL_RPATH FALSE)
+
+# the RPATH to be used when installing
+SET(CMAKE_INSTALL_RPATH "${CMAKE_INSTALL_PREFIX}/lib")
+
+# don't add the automatically determined parts of the RPATH
+# which point to directories outside the build tree to the install RPATH
+SET(CMAKE_INSTALL_RPATH_USE_LINK_PATH TRUE)
+
#############################################################
##
## Generator specific settings
diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt
index 4077d6230..32cf3872e 100644
--- a/resources/3rdparty/CMakeLists.txt
+++ b/resources/3rdparty/CMakeLists.txt
@@ -178,8 +178,6 @@ include(${STORM_3RDPARTY_SOURCE_DIR}/include_cudd.cmake)
#############################################################
include(${STORM_3RDPARTY_SOURCE_DIR}/include_cpptemplate.cmake)
-
-
#############################################################
##
## carl
@@ -188,25 +186,25 @@ include(${STORM_3RDPARTY_SOURCE_DIR}/include_cpptemplate.cmake)
set(STORM_HAVE_CARL OFF)
if(USE_CARL)
- find_package(carl QUIET)
- if(carl_FOUND)
- set(STORM_SHIPPED_CARL OFF)
+ if (NOT STORM_FORCE_SHIPPED_CARL)
+ find_package(carl QUIET)
+ endif()
+ if(carl_FOUND AND NOT STORM_FORCE_SHIPPED_CARL)
+ set(STORM_SHIPPED_CARL OFF)
set(STORM_HAVE_CARL ON)
message(STATUS "Storm - Use system version of carl.")
message(STATUS "Storm - Linking with carl ${carl_VERSION} (CARL_USE_CLN_NUMBERS: ${CARL_USE_CLN_NUMBERS}).")
set(STORM_HAVE_CLN ${CARL_USE_CLN_NUMBERS})
else()
- set(STORM_SHIPPED_CARL ON)
+ set(STORM_SHIPPED_CARL ON)
# The first external project will be built at *configure stage*
message("START CARL CONFIG PROCESS")
file(MAKE_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download)
- execute_process(
- COMMAND ${CMAKE_COMMAND} ${STORM_3RDPARTY_SOURCE_DIR}/carl "-DSTORM_3RDPARTY_BINARY_DIR=${STORM_3RDPARTY_BINARY_DIR}"
- WORKING_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download
- OUTPUT_VARIABLE carlconfig_out
- RESULT_VARIABLE carlconfig_result
- )
-
+ execute_process(
+ COMMAND ${CMAKE_COMMAND} ${STORM_3RDPARTY_SOURCE_DIR}/carl "-DSTORM_3RDPARTY_BINARY_DIR=${STORM_3RDPARTY_BINARY_DIR}"
+ WORKING_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download
+ OUTPUT_VARIABLE carlconfig_out
+ RESULT_VARIABLE carlconfig_result)
if(NOT carlconfig_result)
message("${carlconfig_out}")
@@ -237,17 +235,20 @@ if(USE_CARL)
include(${STORM_3RDPARTY_BINARY_DIR}/carl/carlConfig.cmake)
message("CARL_USE_CLN_NUMBERS: ${CARL_USE_CLN_NUMBERS}")
set(STORM_HAVE_CLN ${CARL_USE_CLN_NUMBERS})
- add_dependencies(resources carl)
+ add_dependencies(resources carl)
set(carl_INCLUDE_DIR "${STORM_3RDPARTY_BINARY_DIR}/carl/include/")
- set(carl_LIBRARIES ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl${DYNAMIC_EXT})
+ set(carl_LIBRARIES ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl${DYNAMIC_EXT})
set(STORM_HAVE_CARL ON)
+
+ # install the carl dynamic library if we build it
+ get_filename_component(STORM_CARL_DYLIB_FULL_PATH ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl${DYNAMIC_EXT} REALPATH)
+ install(FILES ${STORM_CARL_DYLIB_FULL_PATH} DESTINATION lib)
endif()
if(STORM_USE_CLN_NUMBERS AND NOT STORM_HAVE_CLN)
message(FATAL_ERROR "Cannot use CLN numbers if carl is build without")
endif()
list(APPEND STORM_DEP_IMP_TARGETS lib_carl)
-
endif()
diff --git a/src/storm/CMakeLists.txt b/src/storm/CMakeLists.txt
index 363fbc0ab..d9135dcb9 100644
--- a/src/storm/CMakeLists.txt
+++ b/src/storm/CMakeLists.txt
@@ -51,7 +51,6 @@ add_executable(storm-main ${STORM_MAIN_SOURCES} ${STORM_MAIN_HEADERS})
target_link_libraries(storm-main storm)
set_target_properties(storm-main PROPERTIES OUTPUT_NAME "storm")
-
# Install storm headers to include directory.
foreach(HEADER ${STORM_LIB_HEADERS})
string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER})
@@ -69,3 +68,5 @@ add_custom_target(copy_storm_headers DEPENDS ${STORM_OUTPUT_HEADERS} ${STORM_LIB
add_dependencies(storm copy_storm_headers)
add_dependencies(storm copy_resources_headers)
+# install command
+install(TARGETS storm-main storm RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
\ No newline at end of file
From 1598f0db1eecb7b03e62dfaadb19a1ead5021588 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 6 Feb 2017 15:27:08 +0100
Subject: [PATCH 10/24] cmake version detection fix for when storm is not built
from git
---
CMakeLists.txt | 79 ++++++++++++++++++++-----------
resources/3rdparty/CMakeLists.txt | 62 ++++++++++++------------
src/storm/utility/storm-version.h | 21 ++++----
storm-version.cpp.in | 6 +--
4 files changed, 97 insertions(+), 71 deletions(-)
diff --git a/CMakeLists.txt b/CMakeLists.txt
index edf817f5b..3e4b17328 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -18,7 +18,7 @@ include(imported)
#############################################################
##
-## CMake options of Storm
+## CMake options of storm
##
#############################################################
option(STORM_DEVELOPER "Sets whether the development mode is used." OFF)
@@ -44,7 +44,7 @@ option(STORM_COMPILE_WITH_CCACHE "Compile using CCache [if found]" ON)
mark_as_advanced(STORM_COMPILE_WITH_CCACHE)
option(STORM_LOG_DISABLE_DEBUG "Disable log and trace message support" OFF)
option(STORM_USE_CLN_NUMBERS "Sets whether CLN or GMP numbers should be used" ON)
-option(BUILD_SHARED_LIBS "Build the Storm library dynamically" OFF)
+option(BUILD_SHARED_LIBS "Build the storm library dynamically" OFF)
set(BOOST_ROOT "" CACHE STRING "A hint to the root directory of Boost (optional).")
set(GUROBI_ROOT "" CACHE STRING "A hint to the root directory of Gurobi (optional).")
set(Z3_ROOT "" CACHE STRING "A hint to the root directory of Z3 (optional).")
@@ -55,6 +55,11 @@ set(ADDITIONAL_LINK_DIRS "" CACHE STRING "Additional directories added to the li
set(USE_XERCESC ${XML_SUPPORT})
mark_as_advanced(USE_XERCESC)
+# Sets the source from which storm is obtained. Can be either "git" or "archive". This
+# influences, among other things, the version information.
+set(STORM_SOURCE "git" CACHE STRING "The source from which storm is obtained: either 'git' or 'archive'.")
+mark_as_advanced(STORM_SOURCE)
+
# Set some CMAKE Variables as advanced
mark_as_advanced(CMAKE_OSX_ARCHITECTURES)
mark_as_advanced(CMAKE_OSX_SYSROOT)
@@ -84,17 +89,17 @@ if (STORM_DEVELOPER)
else()
set(STORM_LOG_DISABLE_DEBUG ON)
endif()
-message(STATUS "Storm - Building ${CMAKE_BUILD_TYPE} version.")
+message(STATUS "storm - Building ${CMAKE_BUILD_TYPE} version.")
if(STORM_COMPILE_WITH_CCACHE)
find_program(CCACHE_FOUND ccache)
mark_as_advanced(CCACHE_FOUND)
if(CCACHE_FOUND)
- message(STATUS "Storm - Using ccache")
+ message(STATUS "storm - Using ccache")
set_property(GLOBAL PROPERTY RULE_LAUNCH_COMPILE ccache)
set_property(GLOBAL PROPERTY RULE_LAUNCH_LINK ccache)
else()
- message(STATUS "Storm - Could not find ccache.")
+ message(STATUS "storm - Could not find ccache.")
endif()
endif()
@@ -120,7 +125,7 @@ else()
set(OPERATING_SYSTEM "Linux")
set(LINUX 1)
ENDIF()
-message(STATUS "Storm - Detected operating system ${OPERATING_SYSTEM}.")
+message(STATUS "storm - Detected operating system ${OPERATING_SYSTEM}.")
set(DYNAMIC_EXT ".so")
set(STATIC_EXT ".a")
@@ -298,12 +303,12 @@ if ("${CMAKE_GENERATOR}" STREQUAL "Xcode")
endif()
# Display information about build configuration.
-message(STATUS "Storm - Using compiler configuration ${STORM_COMPILER_ID} ${STORM_COMPILER_VERSION}.")
+message(STATUS "storm - Using compiler configuration ${STORM_COMPILER_ID} ${STORM_COMPILER_VERSION}.")
if (STORM_DEVELOPER)
- message(STATUS "Storm - CXX Flags: ${CMAKE_CXX_FLAGS}")
- message(STATUS "Storm - CXX Debug Flags: ${CMAKE_CXX_FLAGS_DEBUG}")
- message(STATUS "Storm - CXX Release Flags: ${CMAKE_CXX_FLAGS_RELEASE}")
- message(STATUS "Storm - Build type: ${CMAKE_BUILD_TYPE}")
+ message(STATUS "storm - CXX Flags: ${CMAKE_CXX_FLAGS}")
+ message(STATUS "storm - CXX Debug Flags: ${CMAKE_CXX_FLAGS_DEBUG}")
+ message(STATUS "storm - CXX Release Flags: ${CMAKE_CXX_FLAGS_RELEASE}")
+ message(STATUS "storm - Build type: ${CMAKE_BUILD_TYPE}")
endif()
#############################################################
@@ -343,27 +348,45 @@ endif(DOXYGEN_FOUND)
#############################################################
##
-## CMake-generated Config File for Storm
+## CMake-generated Config File for storm
##
#############################################################
-# Make a version file containing the current version from git.
-include(GetGitRevisionDescription)
-git_describe_checkout(STORM_GIT_VERSION_STRING)
-message(STATUS "Storm -- Git version string is ${STORM_GIT_VERSION_STRING}.")
-# Parse the git Tag into variables
-string(REGEX REPLACE "^([0-9]+)\\..*" "\\1" STORM_CPP_VERSION_MAJOR "${STORM_GIT_VERSION_STRING}")
-string(REGEX REPLACE "^[0-9]+\\.([0-9]+).*" "\\1" STORM_CPP_VERSION_MINOR "${STORM_GIT_VERSION_STRING}")
-string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.([0-9]+).*" "\\1" STORM_CPP_VERSION_PATCH "${STORM_GIT_VERSION_STRING}")
-string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-([0-9]+)\\-.*" "\\1" STORM_CPP_VERSION_COMMITS_AHEAD "${STORM_GIT_VERSION_STRING}")
-string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-([a-z0-9]+).*" "\\1" STORM_CPP_VERSION_HASH "${STORM_GIT_VERSION_STRING}")
-string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-[a-z0-9]+\\-(.*)" "\\1" STORM_CPP_VERSION_APPENDIX "${STORM_GIT_VERSION_STRING}")
-if ("${STORM_CPP_VERSION_APPENDIX}" MATCHES "^.*dirty.*$")
- set(STORM_CPP_VERSION_DIRTY 1)
+# If a version was provided, we use it. This is useful, for example, when storm is built
+# from a tarball.
+if (STORM_SOURCE STREQUAL "archive")
+ if (NOT DEFINED STORM_CPP_VERSION_MAJOR OR NOT DEFINED STORM_CPP_VERSION_MINOR OR NOT DEFINED STORM_CPP_VERSION_PATCH)
+ message(FATAL_ERROR "storm - Building from archive requires setting a version via cmake.")
+ endif()
+ message(STATUS "storm - Version is ${STORM_CPP_VERSION_MAJOR}.${STORM_CPP_VERSION_MINOR}.${STORM_CPP_VERSION_PATCH} (building from archive).")
+ set(STORM_CPP_VERSION_COMMITS_AHEAD boost::none)
+ set(STORM_CPP_VERSION_HASH boost::none)
+ set(STORM_CPP_VERSION_DIRTY boost::none)
else()
- set(STORM_CPP_VERSION_DIRTY 0)
+ if (DEFINED STORM_CPP_VERSION_MAJOR OR DEFINED STORM_CPP_VERSION_MINOR OR DEFINED STORM_CPP_VERSION_PATCH)
+ message(FATAL_ERROR "storm - Building from git does not support setting a version via cmake.")
+ endif()
+
+ # Make a version file containing the current version from git.
+ include(GetGitRevisionDescription)
+ get_git_head_revision(STORM_CPP_VERSION_REFSPEC STORM_CPP_GIT_HASH)
+ set(STORM_CPP_GIT_HASH "std::string(\"${STORM_CPP_GIT_HASH}\")")
+
+ git_describe_checkout(STORM_GIT_VERSION_STRING)
+ # Parse the git Tag into variables
+ string(REGEX REPLACE "^([0-9]+)\\..*" "\\1" STORM_CPP_VERSION_MAJOR "${STORM_GIT_VERSION_STRING}")
+ string(REGEX REPLACE "^[0-9]+\\.([0-9]+).*" "\\1" STORM_CPP_VERSION_MINOR "${STORM_GIT_VERSION_STRING}")
+ string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.([0-9]+).*" "\\1" STORM_CPP_VERSION_PATCH "${STORM_GIT_VERSION_STRING}")
+ string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-([0-9]+)\\-.*" "\\1" STORM_CPP_VERSION_COMMITS_AHEAD "${STORM_GIT_VERSION_STRING}")
+ string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-([a-z0-9]+).*" "\\1" STORM_CPP_TAG_HASH "${STORM_GIT_VERSION_STRING}")
+ string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-[a-z0-9]+\\-(.*)" "\\1" STORM_CPP_VERSION_APPENDIX "${STORM_GIT_VERSION_STRING}")
+ if ("${STORM_CPP_VERSION_APPENDIX}" MATCHES "^.*dirty.*$")
+ set(STORM_CPP_VERSION_DIRTY 1)
+ else()
+ set(STORM_CPP_VERSION_DIRTY 0)
+ endif()
+ message(STATUS "storm - Version is ${STORM_CPP_VERSION_MAJOR}.${STORM_CPP_VERSION_MINOR}.${STORM_CPP_VERSION_PATCH} (${STORM_CPP_VERSION_COMMITS_AHEAD} commits ahead of tag) build from ${STORM_CPP_GIT_HASH} (dirty: ${STORM_CPP_VERSION_DIRTY}) (building from git).")
endif()
-message(STATUS "Storm - Version is ${STORM_CPP_VERSION_MAJOR}.${STORM_CPP_VERSION_MINOR}.${STORM_CPP_VERSION_PATCH} (${STORM_CPP_VERSION_COMMITS_AHEAD} commits ahead of Tag) build from ${STORM_CPP_VERSION_HASH} (Dirty: ${STORM_CPP_VERSION_DIRTY}).")
# Configure a header file to pass some of the CMake settings to the source code
configure_file (
@@ -397,4 +420,4 @@ add_subdirectory(src)
include(export)
-include(StormCPackConfig.cmake)
+include(stormCPackConfig.cmake)
diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt
index 32cf3872e..fcadfbdd8 100644
--- a/resources/3rdparty/CMakeLists.txt
+++ b/resources/3rdparty/CMakeLists.txt
@@ -76,7 +76,7 @@ foreach(BOOSTLIB ${Boost_LIBRARIES})
list(APPEND STORM_DEP_TARGETS target-boost-${CNTVAR}_SHARED)
MATH(EXPR CNTVAR "${CNTVAR}+1")
endforeach()
-message(STATUS "Storm - Using boost ${Boost_VERSION} (library version ${Boost_LIB_VERSION}).")
+message(STATUS "storm - Using boost ${Boost_VERSION} (library version ${Boost_LIB_VERSION}).")
# set the information for the config header
set(STORM_BOOST_INCLUDE_DIR "${Boost_INCLUDE_DIRS}")
@@ -87,7 +87,7 @@ set(STORM_BOOST_INCLUDE_DIR "${Boost_INCLUDE_DIRS}")
#############################################################
# Use the shipped version of ExprTK
-message (STATUS "Storm - Including ExprTk.")
+message (STATUS "storm - Including ExprTk.")
add_imported_library_interface(ExprTk "${PROJECT_SOURCE_DIR}/resources/3rdparty/exprtk")
list(APPEND STORM_DEP_TARGETS ExprTk)
@@ -98,7 +98,7 @@ list(APPEND STORM_DEP_TARGETS ExprTk)
#############################################################
# Use the shipped version of Sparsepp
-message (STATUS "Storm - Including Sparsepp.")
+message (STATUS "storm - Including Sparsepp.")
include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/sparsepp")
# Add sparsepp.h to the headers that are copied to the include directory in thebuild directory.
@@ -117,7 +117,7 @@ list(APPEND STORM_RESOURCES_HEADERS "${CMAKE_BINARY_DIR}/include/resources/3rdpa
#############################################################
#use the shipped version of modernjson
-message (STATUS "Storm - Including ModernJSON.")
+message (STATUS "storm - Including ModernJSON.")
add_imported_library_interface(ModernJSON "${PROJECT_SOURCE_DIR}/resources/3rdparty/modernjson/src/")
list(APPEND STORM_DEP_TARGETS ModernJSON)
@@ -133,7 +133,7 @@ find_package(Z3 QUIET)
set(STORM_HAVE_Z3 ${Z3_FOUND})
if(Z3_FOUND)
- message (STATUS "Storm - Linking with Z3.")
+ message (STATUS "storm - Linking with Z3.")
add_imported_library(z3 SHARED ${Z3_LIBRARIES} ${Z3_INCLUDE_DIRS})
list(APPEND STORM_DEP_TARGETS z3_SHARED)
endif(Z3_FOUND)
@@ -156,7 +156,7 @@ if (STORM_USE_GUROBI)
find_package(Gurobi QUIET REQUIRED)
set(STORM_HAVE_GUROBI ${GUROBI_FOUND})
if (GUROBI_FOUND)
- message (STATUS "Storm - Linking with Gurobi.")
+ message (STATUS "storm - Linking with Gurobi.")
add_imported_library(Gurobi "" ${GUROBI_LIBRARY} ${GUROBI_INCLUDE_DIRS})
list(APPEND STORM_DEP_TARGETS Gurobi)
endif()
@@ -192,8 +192,8 @@ if(USE_CARL)
if(carl_FOUND AND NOT STORM_FORCE_SHIPPED_CARL)
set(STORM_SHIPPED_CARL OFF)
set(STORM_HAVE_CARL ON)
- message(STATUS "Storm - Use system version of carl.")
- message(STATUS "Storm - Linking with carl ${carl_VERSION} (CARL_USE_CLN_NUMBERS: ${CARL_USE_CLN_NUMBERS}).")
+ message(STATUS "storm - Use system version of carl.")
+ message(STATUS "storm - Linking with carl ${carl_VERSION} (CARL_USE_CLN_NUMBERS: ${CARL_USE_CLN_NUMBERS}).")
set(STORM_HAVE_CLN ${CARL_USE_CLN_NUMBERS})
else()
set(STORM_SHIPPED_CARL ON)
@@ -220,7 +220,7 @@ if(USE_CARL)
endif()
message("END CARL CONFIG PROCESS")
- message(STATUS "Storm - Using shipped version of carl.")
+ message(STATUS "storm - Using shipped version of carl.")
ExternalProject_Add(
carl
SOURCE_DIR ${STORM_3RDPARTY_BINARY_DIR}/carl
@@ -263,7 +263,7 @@ if(USE_SMTRAT)
find_package(smtrat QUIET REQUIRED)
if(smtrat_FOUND)
set(STORM_HAVE_SMTRAT ON)
- message(STATUS "Storm - Linking with smtrat.")
+ message(STATUS "storm - Linking with smtrat.")
include_directories("${smtrat_INCLUDE_DIR}")
list(APPEND STORM_LINK_LIBRARIES ${smtrat_LIBRARIES})
else()
@@ -283,7 +283,7 @@ if(USE_HYPRO)
find_package(hypro QUIET REQUIRED)
if(hypro_FOUND)
set(STORM_HAVE_HYPRO ON)
- message(STATUS "Storm - Linking with hypro.")
+ message(STATUS "storm - Linking with hypro.")
include_directories("${hypro_INCLUDE_DIR}")
list(APPEND STORM_LINK_LIBRARIES ${hypro_LIBRARIES})
else()
@@ -317,7 +317,7 @@ endif()
# MathSAT Defines
set(STORM_HAVE_MSAT ${ENABLE_MSAT})
if (ENABLE_MSAT)
- message (STATUS "Storm - Linking with MathSAT.")
+ message (STATUS "storm - Linking with MathSAT.")
link_directories("${MSAT_ROOT}/lib")
include_directories("${MSAT_ROOT}/include")
list(APPEND STORM_LINK_LIBRARIES "mathsat")
@@ -365,8 +365,8 @@ ExternalProject_Get_Property(sylvan source_dir)
ExternalProject_Get_Property(sylvan binary_dir)
set(Sylvan_INCLUDE_DIR "${source_dir}/src")
set(Sylvan_LIBRARY "${binary_dir}/src/libsylvan${STATIC_EXT}")
-message(STATUS "Storm - Using shipped version of sylvan.")
-message(STATUS "Storm - Linking with sylvan.")
+message(STATUS "storm - Using shipped version of sylvan.")
+message(STATUS "storm - Linking with sylvan.")
add_imported_library(sylvan STATIC ${Sylvan_LIBRARY} ${Sylvan_INCLUDE_DIR})
add_dependencies(sylvan_STATIC sylvan)
if(STORM_SHIPPED_CARL)
@@ -376,7 +376,7 @@ list(APPEND STORM_DEP_TARGETS sylvan_STATIC)
find_package(Hwloc QUIET REQUIRED)
if(HWLOC_FOUND)
- message(STATUS "Storm - Linking with hwloc ${HWLOC_VERSION}.")
+ message(STATUS "storm - Linking with hwloc ${HWLOC_VERSION}.")
add_imported_library(hwloc STATIC ${HWLOC_LIBRARIES} "")
list(APPEND STORM_DEP_TARGETS hwloc_STATIC)
else()
@@ -432,14 +432,14 @@ if (STORM_USE_INTELTBB)
find_package(TBB QUIET REQUIRED)
if (TBB_FOUND)
- message(STATUS "Storm - Found Intel TBB with interface version ${TBB_INTERFACE_VERSION}.")
- message(STATUS "Storm - Linking with Intel TBB in ${TBB_LIBRARY_DIRS}.")
+ message(STATUS "storm - Found Intel TBB with interface version ${TBB_INTERFACE_VERSION}.")
+ message(STATUS "storm - Linking with Intel TBB in ${TBB_LIBRARY_DIRS}.")
set(STORM_HAVE_INTELTBB ON)
link_directories(${TBB_LIBRARY_DIRS})
include_directories(${TBB_INCLUDE_DIRS})
list(APPEND STORM_LINK_LIBRARIES tbb tbbmalloc)
else(TBB_FOUND)
- message(FATAL_ERROR "Storm - TBB was requested, but not found.")
+ message(FATAL_ERROR "storm - TBB was requested, but not found.")
endif(TBB_FOUND)
endif(STORM_USE_INTELTBB)
@@ -451,7 +451,7 @@ endif(STORM_USE_INTELTBB)
find_package(Threads QUIET REQUIRED)
if (NOT Threads_FOUND)
- message(FATAL_ERROR "Storm - Threads was requested, but not found.")
+ message(FATAL_ERROR "storm - Threads was requested, but not found.")
endif()
include_directories(${THREADS_INCLUDE_DIRS})
list(APPEND STORM_LINK_LIBRARIES ${CMAKE_THREAD_LIBS_INIT})
@@ -491,11 +491,11 @@ if(ENABLE_CUDA)
COMPILE_OUTPUT_VARIABLE OUTPUT_TEST_VAR
)
if(NOT STORM_CUDA_COMPILE_RESULT_TYPEALIGNMENT)
- message(FATAL_ERROR "Storm (CudaPlugin) - Could not test type alignment, there was an Error while compiling the file ${PROJECT_SOURCE_DIR}/cuda/CMakeAlignmentCheck.cpp: ${OUTPUT_TEST_VAR}")
+ message(FATAL_ERROR "storm (CudaPlugin) - Could not test type alignment, there was an Error while compiling the file ${PROJECT_SOURCE_DIR}/cuda/CMakeAlignmentCheck.cpp: ${OUTPUT_TEST_VAR}")
elseif(STORM_CUDA_RUN_RESULT_TYPEALIGNMENT EQUAL 0)
message(STATUS "StoRM (CudaPlugin) - Result of Type Alignment Check: OK.")
else()
- message(FATAL_ERROR "Storm (CudaPlugin) - Result of Type Alignment Check: FAILED (Code ${STORM_CUDA_RUN_RESULT_TYPEALIGNMENT})")
+ message(FATAL_ERROR "storm (CudaPlugin) - Result of Type Alignment Check: FAILED (Code ${STORM_CUDA_RUN_RESULT_TYPEALIGNMENT})")
endif()
# Test for Float 64bit Alignment
@@ -504,15 +504,15 @@ if(ENABLE_CUDA)
COMPILE_OUTPUT_VARIABLE OUTPUT_TEST_VAR
)
if(NOT STORM_CUDA_COMPILE_RESULT_FLOATALIGNMENT)
- message(FATAL_ERROR "Storm (CudaPlugin) - Could not test float type alignment, there was an Error while compiling the file ${PROJECT_SOURCE_DIR}/cuda/CMakeFloatAlignmentCheck.cpp: ${OUTPUT_TEST_VAR}")
+ message(FATAL_ERROR "storm (CudaPlugin) - Could not test float type alignment, there was an Error while compiling the file ${PROJECT_SOURCE_DIR}/cuda/CMakeFloatAlignmentCheck.cpp: ${OUTPUT_TEST_VAR}")
elseif(STORM_CUDA_RUN_RESULT_FLOATALIGNMENT EQUAL 2)
- message(STATUS "Storm (CudaPlugin) - Result of Float Type Alignment Check: 64bit alignment active.")
+ message(STATUS "storm (CudaPlugin) - Result of Float Type Alignment Check: 64bit alignment active.")
set(STORM_CUDAPLUGIN_FLOAT_64BIT_ALIGN_DEF "define")
elseif(STORM_CUDA_RUN_RESULT_FLOATALIGNMENT EQUAL 3)
- message(STATUS "Storm (CudaPlugin) - Result of Float Type Alignment Check: 64bit alignment disabled.")
+ message(STATUS "storm (CudaPlugin) - Result of Float Type Alignment Check: 64bit alignment disabled.")
set(STORM_CUDAPLUGIN_FLOAT_64BIT_ALIGN_DEF "undef")
else()
- message(FATAL_ERROR "Storm (CudaPlugin) - Result of Float Type Alignment Check: FAILED (Code ${STORM_CUDA_RUN_RESULT_FLOATALIGNMENT})")
+ message(FATAL_ERROR "storm (CudaPlugin) - Result of Float Type Alignment Check: FAILED (Code ${STORM_CUDA_RUN_RESULT_FLOATALIGNMENT})")
endif()
#
# Make a version file containing the current version from git.
@@ -531,7 +531,7 @@ if(ENABLE_CUDA)
else()
set(STORM_CUDAPLUGIN_VERSION_DIRTY 0)
endif()
- message(STATUS "Storm (CudaPlugin) - Version information: ${STORM_CUDAPLUGIN_VERSION_MAJOR}.${STORM_CUDAPLUGIN_VERSION_MINOR}.${STORM_CUDAPLUGIN_VERSION_PATCH} (${STORM_CUDAPLUGIN_VERSION_COMMITS_AHEAD} commits ahead of Tag) build from ${STORM_CUDAPLUGIN_VERSION_HASH} (Dirty: ${STORM_CUDAPLUGIN_VERSION_DIRTY})")
+ message(STATUS "storm (CudaPlugin) - Version information: ${STORM_CUDAPLUGIN_VERSION_MAJOR}.${STORM_CUDAPLUGIN_VERSION_MINOR}.${STORM_CUDAPLUGIN_VERSION_PATCH} (${STORM_CUDAPLUGIN_VERSION_COMMITS_AHEAD} commits ahead of Tag) build from ${STORM_CUDAPLUGIN_VERSION_HASH} (Dirty: ${STORM_CUDAPLUGIN_VERSION_DIRTY})")
# Configure a header file to pass some of the CMake settings to the source code
@@ -565,9 +565,9 @@ if(ENABLE_CUDA)
if(CUSP_FOUND)
include_directories(${CUSP_INCLUDE_DIR})
cuda_include_directories(${CUSP_INCLUDE_DIR})
- message(STATUS "Storm (CudaPlugin) - Found CUSP Version ${CUSP_VERSION} in location ${CUSP_INCLUDE_DIR}.")
+ message(STATUS "storm (CudaPlugin) - Found CUSP Version ${CUSP_VERSION} in location ${CUSP_INCLUDE_DIR}.")
else()
- message(FATAL_ERROR "Storm (CudaPlugin) - Could not find CUSP.")
+ message(FATAL_ERROR "storm (CudaPlugin) - Could not find CUSP.")
endif()
#############################################################
@@ -578,9 +578,9 @@ if(ENABLE_CUDA)
if(THRUST_FOUND)
include_directories(${THRUST_INCLUDE_DIR})
cuda_include_directories(${THRUST_INCLUDE_DIR})
- message(STATUS "Storm (CudaPlugin) - Found Thrust Version ${THRUST_VERSION} in location ${THRUST_INCLUDE_DIR}.")
+ message(STATUS "storm (CudaPlugin) - Found Thrust Version ${THRUST_VERSION} in location ${THRUST_INCLUDE_DIR}.")
else()
- message(FATAL_ERROR "Storm (CudaPlugin) - Could not find Thrust. Check your CUDA installation.")
+ message(FATAL_ERROR "storm (CudaPlugin) - Could not find Thrust. Check your CUDA installation.")
endif()
include_directories(${CUDA_INCLUDE_DIRS})
@@ -590,7 +590,7 @@ if(ENABLE_CUDA)
${STORM_CUDA_KERNEL_FILES} ${STORM_CUDA_HEADER_FILES}
)
- message (STATUS "Storm - Linking with CUDA.")
+ message (STATUS "storm - Linking with CUDA.")
list(APPEND STORM_LINK_LIBRARIES ${STORM_CUDA_LIB_NAME})
include_directories("${PROJECT_SOURCE_DIR}/cuda/kernels/")
endif()
diff --git a/src/storm/utility/storm-version.h b/src/storm/utility/storm-version.h
index 1cfaca76b..5c2412670 100644
--- a/src/storm/utility/storm-version.h
+++ b/src/storm/utility/storm-version.h
@@ -3,8 +3,9 @@
#include <string>
#include <sstream>
-namespace storm
-{
+#include <boost/optional.hpp>
+
+namespace storm {
namespace utility {
struct StormVersion {
@@ -18,13 +19,13 @@ namespace storm
const static unsigned versionPatch;
/// The short hash of the git commit this build is based on
- const static std::string gitRevisionHash;
+ const static boost::optional<std::string> gitRevisionHash;
/// How many commits passed since the tag was last set.
- const static unsigned commitsAhead;
+ const static boost::optional<unsigned> commitsAhead;
/// 0 iff there no files were modified in the checkout, 1 otherwise.
- const static unsigned dirty;
+ const static boost::optional<unsigned> dirty;
/// The system which has compiled Storm.
const static std::string systemName;
@@ -47,11 +48,13 @@ namespace storm
static std::string longVersionString() {
std::stringstream sstream;
sstream << "version: " << versionMajor << "." << versionMinor << "." << versionPatch;
- if (commitsAhead != 0) {
- sstream << " (+" << commitsAhead << " commits)";
+ if (commitsAhead && commitsAhead.get() > 0) {
+ sstream << " (+" << commitsAhead.get() << " commits)";
+ }
+ if (gitRevisionHash) {
+ sstream << " build from revision " << gitRevisionHash.get();
}
- sstream << " build from revision " << gitRevisionHash;
- if (dirty == 1) {
+ if (dirty && dirty.get() == 1) {
sstream << " (DIRTY)";
}
sstream << "." << std::endl;
diff --git a/storm-version.cpp.in b/storm-version.cpp.in
index 71625a18d..d5673c38a 100644
--- a/storm-version.cpp.in
+++ b/storm-version.cpp.in
@@ -8,9 +8,9 @@ namespace storm {
const unsigned StormVersion::versionMajor = @STORM_CPP_VERSION_MAJOR@;
const unsigned StormVersion::versionMinor = @STORM_CPP_VERSION_MINOR@;
const unsigned StormVersion::versionPatch = @STORM_CPP_VERSION_PATCH@;
- const std::string StormVersion::gitRevisionHash = "@STORM_CPP_VERSION_HASH@";
- const unsigned StormVersion::commitsAhead = @STORM_CPP_VERSION_COMMITS_AHEAD@;
- const unsigned StormVersion::dirty = @STORM_CPP_VERSION_DIRTY@;
+ const boost::optional<std::string> StormVersion::gitRevisionHash = @STORM_CPP_GIT_HASH@;
+ const boost::optional<unsigned> StormVersion::commitsAhead = @STORM_CPP_VERSION_COMMITS_AHEAD@;
+ const boost::optional<unsigned> StormVersion::dirty = @STORM_CPP_VERSION_DIRTY@;
const std::string StormVersion::systemName = "@CMAKE_SYSTEM_NAME@";
const std::string StormVersion::systemVersion = "@CMAKE_SYSTEM_VERSION@";
const std::string StormVersion::cxxCompiler = "@STORM_COMPILER_ID@ @CMAKE_CXX_COMPILER_VERSION@";
From 87bb94f23a3d3e65de548e678536228b56016759 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 6 Feb 2017 17:20:40 +0100
Subject: [PATCH 11/24] undo wrong replace
---
CMakeLists.txt | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 3e4b17328..557eb009c 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -420,4 +420,4 @@ add_subdirectory(src)
include(export)
-include(stormCPackConfig.cmake)
+include(StormCPackConfig.cmake)
From 7cdc34bdc48601c6294a1ecfd9ecd936896639bb Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 6 Feb 2017 17:54:59 +0100
Subject: [PATCH 12/24] renamed version variables to make them consistent
---
CMakeLists.txt | 46 +++++++++++++++++++++++++-------------------
storm-version.cpp.in | 12 ++++++------
2 files changed, 32 insertions(+), 26 deletions(-)
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 557eb009c..f0d00bb29 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -352,40 +352,46 @@ endif(DOXYGEN_FOUND)
##
#############################################################
-# If a version was provided, we use it. This is useful, for example, when storm is built
-# from a tarball.
+# If storm is built from an archive, we need to skip the version detection based on git.
if (STORM_SOURCE STREQUAL "archive")
- if (NOT DEFINED STORM_CPP_VERSION_MAJOR OR NOT DEFINED STORM_CPP_VERSION_MINOR OR NOT DEFINED STORM_CPP_VERSION_PATCH)
+ if (NOT DEFINED STORM_VERSION_MAJOR OR NOT DEFINED STORM_VERSION_MINOR OR NOT DEFINED STORM_VERSION_PATCH)
message(FATAL_ERROR "storm - Building from archive requires setting a version via cmake.")
endif()
- message(STATUS "storm - Version is ${STORM_CPP_VERSION_MAJOR}.${STORM_CPP_VERSION_MINOR}.${STORM_CPP_VERSION_PATCH} (building from archive).")
- set(STORM_CPP_VERSION_COMMITS_AHEAD boost::none)
- set(STORM_CPP_VERSION_HASH boost::none)
- set(STORM_CPP_VERSION_DIRTY boost::none)
+ message(STATUS "storm - Version is ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH} (building from archive).")
+ set(STORM_VERSION_COMMITS_AHEAD boost::none)
+ set(STORM_VERSION_GIT_HASH boost::none)
+ set(STORM_VERSION_DIRTY boost::none)
else()
- if (DEFINED STORM_CPP_VERSION_MAJOR OR DEFINED STORM_CPP_VERSION_MINOR OR DEFINED STORM_CPP_VERSION_PATCH)
+ if (DEFINED STORM_VERSION_MAJOR OR DEFINED STORM_VERSION_MINOR OR DEFINED STORM_VERSION_PATCH)
message(FATAL_ERROR "storm - Building from git does not support setting a version via cmake.")
endif()
# Make a version file containing the current version from git.
include(GetGitRevisionDescription)
- get_git_head_revision(STORM_CPP_VERSION_REFSPEC STORM_CPP_GIT_HASH)
- set(STORM_CPP_GIT_HASH "std::string(\"${STORM_CPP_GIT_HASH}\")")
+ get_git_head_revision(STORM_VERSION_REFSPEC STORM_VERSION_GIT_HASH)
git_describe_checkout(STORM_GIT_VERSION_STRING)
# Parse the git Tag into variables
- string(REGEX REPLACE "^([0-9]+)\\..*" "\\1" STORM_CPP_VERSION_MAJOR "${STORM_GIT_VERSION_STRING}")
- string(REGEX REPLACE "^[0-9]+\\.([0-9]+).*" "\\1" STORM_CPP_VERSION_MINOR "${STORM_GIT_VERSION_STRING}")
- string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.([0-9]+).*" "\\1" STORM_CPP_VERSION_PATCH "${STORM_GIT_VERSION_STRING}")
- string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-([0-9]+)\\-.*" "\\1" STORM_CPP_VERSION_COMMITS_AHEAD "${STORM_GIT_VERSION_STRING}")
- string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-([a-z0-9]+).*" "\\1" STORM_CPP_TAG_HASH "${STORM_GIT_VERSION_STRING}")
- string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-[a-z0-9]+\\-(.*)" "\\1" STORM_CPP_VERSION_APPENDIX "${STORM_GIT_VERSION_STRING}")
- if ("${STORM_CPP_VERSION_APPENDIX}" MATCHES "^.*dirty.*$")
- set(STORM_CPP_VERSION_DIRTY 1)
+ string(REGEX REPLACE "^([0-9]+)\\..*" "\\1" STORM_VERSION_MAJOR "${STORM_GIT_VERSION_STRING}")
+ string(REGEX REPLACE "^[0-9]+\\.([0-9]+).*" "\\1" STORM_VERSION_MINOR "${STORM_GIT_VERSION_STRING}")
+ string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.([0-9]+).*" "\\1" STORM_VERSION_PATCH "${STORM_GIT_VERSION_STRING}")
+ string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-([0-9]+)\\-.*" "\\1" STORM_VERSION_COMMITS_AHEAD "${STORM_GIT_VERSION_STRING}")
+ string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-([a-z0-9]+).*" "\\1" STORM_VERSION_TAG_HASH "${STORM_GIT_VERSION_STRING}")
+ string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-[a-z0-9]+\\-(.*)" "\\1" STORM_VERSION_APPENDIX "${STORM_GIT_VERSION_STRING}")
+ if ("${STORM_VERSION_APPENDIX}" MATCHES "^.*dirty.*$")
+ set(STORM_VERSION_DIRTY 1)
else()
- set(STORM_CPP_VERSION_DIRTY 0)
+ set(STORM_VERSION_DIRTY 0)
endif()
- message(STATUS "storm - Version is ${STORM_CPP_VERSION_MAJOR}.${STORM_CPP_VERSION_MINOR}.${STORM_CPP_VERSION_PATCH} (${STORM_CPP_VERSION_COMMITS_AHEAD} commits ahead of tag) build from ${STORM_CPP_GIT_HASH} (dirty: ${STORM_CPP_VERSION_DIRTY}) (building from git).")
+ if (STORM_VERSION_DIRTY)
+ set(STORM_VERSION_DIRTY_STR "yes")
+ else()
+ set(STORM_VERSION_DIRTY_STR "no")
+ endif()
+ message(STATUS "storm - version is ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH} (${STORM_VERSION_COMMITS_AHEAD} commits ahead of tag), building from git: ${STORM_VERSION_GIT_HASH} (dirty: ${STORM_VERSION_DIRTY_STR}).")
+
+ # proper type conversion so we can assign it to an optional
+ set(STORM_VERSION_GIT_HASH "std::string(\"${STORM_VERSION_GIT_HASH}\")")
endif()
# Configure a header file to pass some of the CMake settings to the source code
diff --git a/storm-version.cpp.in b/storm-version.cpp.in
index d5673c38a..23a993169 100644
--- a/storm-version.cpp.in
+++ b/storm-version.cpp.in
@@ -5,12 +5,12 @@
namespace storm {
namespace utility {
- const unsigned StormVersion::versionMajor = @STORM_CPP_VERSION_MAJOR@;
- const unsigned StormVersion::versionMinor = @STORM_CPP_VERSION_MINOR@;
- const unsigned StormVersion::versionPatch = @STORM_CPP_VERSION_PATCH@;
- const boost::optional<std::string> StormVersion::gitRevisionHash = @STORM_CPP_GIT_HASH@;
- const boost::optional<unsigned> StormVersion::commitsAhead = @STORM_CPP_VERSION_COMMITS_AHEAD@;
- const boost::optional<unsigned> StormVersion::dirty = @STORM_CPP_VERSION_DIRTY@;
+ const unsigned StormVersion::versionMajor = @STORM_VERSION_MAJOR@;
+ const unsigned StormVersion::versionMinor = @STORM_VERSION_MINOR@;
+ const unsigned StormVersion::versionPatch = @STORM_VERSION_PATCH@;
+ const boost::optional<std::string> StormVersion::gitRevisionHash = @STORM_VERSION_GIT_HASH@;
+ const boost::optional<unsigned> StormVersion::commitsAhead = @STORM_VERSION_COMMITS_AHEAD@;
+ const boost::optional<unsigned> StormVersion::dirty = @STORM_VERSION_DIRTY@;
const std::string StormVersion::systemName = "@CMAKE_SYSTEM_NAME@";
const std::string StormVersion::systemVersion = "@CMAKE_SYSTEM_VERSION@";
const std::string StormVersion::cxxCompiler = "@STORM_COMPILER_ID@ @CMAKE_CXX_COMPILER_VERSION@";
From 77598a8774679fe3de8f6a71e7dd9a6c4fbc0be4 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Mon, 6 Feb 2017 15:08:18 +0100
Subject: [PATCH 13/24] gspn extension
---
src/storm-gspn/storage/gspn/GSPN.cpp | 13 +++++++++----
src/storm-gspn/storage/gspn/GSPN.h | 17 ++++++++++++++---
src/storm-gspn/storage/gspn/GspnBuilder.cpp | 3 +++
src/storm-gspn/storm-gspn.h | 3 +--
4 files changed, 27 insertions(+), 9 deletions(-)
diff --git a/src/storm-gspn/storage/gspn/GSPN.cpp b/src/storm-gspn/storage/gspn/GSPN.cpp
index ce0d47d44..34967daee 100644
--- a/src/storm-gspn/storage/gspn/GSPN.cpp
+++ b/src/storm-gspn/storage/gspn/GSPN.cpp
@@ -27,8 +27,8 @@ namespace storm {
return tId;
}
- GSPN::GSPN(std::string const& name, std::vector<Place> const& places, std::vector<ImmediateTransition<WeightType>> const& itransitions, std::vector<TimedTransition<RateType>> const& ttransitions, std::vector<TransitionPartition> const& partitions)
- : name(name), places(places), immediateTransitions(itransitions), timedTransitions(ttransitions), partitions(partitions)
+ GSPN::GSPN(std::string const& name, std::vector<Place> const& places, std::vector<ImmediateTransition<WeightType>> const& itransitions, std::vector<TimedTransition<RateType>> const& ttransitions, std::vector<TransitionPartition> const& partitions, std::shared_ptr<storm::expressions::ExpressionManager> const& exprManager)
+ : name(name), places(places), immediateTransitions(itransitions), timedTransitions(ttransitions), partitions(partitions), exprManager(exprManager);
{
}
@@ -134,8 +134,13 @@ namespace storm {
return getImmediateTransition(id);
}
-
- void GSPN::setCapacities(std::unordered_map<std::string, uint64_t> const& mapping) {
+
+
+ std::shared_ptr<storm::expressions::ExpressionManager> const& GSPN::getExpressionManager() {
+ return exprManager;
+ }
+
+ void GSPN::setCapacities(std::unordered_map<std::string, uint64_t> const& mapping) {
for(auto const& entry : mapping) {
storm::gspn::Place* place = getPlace(entry.first);
STORM_LOG_THROW(place != nullptr, storm::exceptions::InvalidArgumentException, "No place with name " << entry.first);
diff --git a/src/storm-gspn/storage/gspn/GSPN.h b/src/storm-gspn/storage/gspn/GSPN.h
index 947769af3..19101ffe4 100644
--- a/src/storm-gspn/storage/gspn/GSPN.h
+++ b/src/storm-gspn/storage/gspn/GSPN.h
@@ -6,6 +6,8 @@
#include <memory>
#include <unordered_map>
+#include "storm/storage/expressions/ExpressionManager.h"
+
#include "storm-gspn/storage/gspn/ImmediateTransition.h"
#include "storm-gspn/storage/gspn/Marking.h"
#include "storm-gspn/storage/gspn/Place.h"
@@ -30,7 +32,7 @@ namespace storm {
GSPN(std::string const& name, std::vector<Place> const& places, std::vector<ImmediateTransition<WeightType>> const& itransitions,
- std::vector<TimedTransition<RateType>> const& ttransitions, std::vector<TransitionPartition> const& partitions);
+ std::vector<TimedTransition<RateType>> const& ttransitions, std::vector<TransitionPartition> const& partitions, std::shared_ptr<storm::expressions::ExpressionManager> const& exprManager);
/*!
* Returns the number of places in this gspn.
@@ -135,7 +137,13 @@ namespace storm {
* @return The name.
*/
std::string const& getName() const;
-
+
+ /*!
+ * Obtain the expression manager used for expressions over GSPNs.
+ *
+ * @return
+ */
+ std::shared_ptr<storm::expressions::ExpressionManager> const& getExpressionManager() const;
/**
* Set Capacities according to name->capacity map.
@@ -197,7 +205,10 @@ namespace storm {
std::vector<storm::gspn::TimedTransition<RateType>> timedTransitions;
std::vector<storm::gspn::TransitionPartition> partitions;
-
+
+ std::shared_ptr<storm::expressions::ExpressionManager> exprManager;
+
+ // Layout information
mutable std::map<uint64_t, LayoutInfo> placeLayout;
mutable std::map<uint64_t, LayoutInfo> transitionLayout;
diff --git a/src/storm-gspn/storage/gspn/GspnBuilder.cpp b/src/storm-gspn/storage/gspn/GspnBuilder.cpp
index a727ebebf..52833419a 100644
--- a/src/storm-gspn/storage/gspn/GspnBuilder.cpp
+++ b/src/storm-gspn/storage/gspn/GspnBuilder.cpp
@@ -164,6 +164,9 @@ namespace storm {
storm::gspn::GSPN* GspnBuilder::buildGspn() const {
+ std::shared_ptr<storm::expressions::ExpressionManager> exprManager(new storm::expressions::ExpressionManager());
+ exprManager->
+
std::vector<TransitionPartition> orderedPartitions;
for(auto const& priorityPartitions : partitions) {
for (auto const& partition : priorityPartitions.second) {
diff --git a/src/storm-gspn/storm-gspn.h b/src/storm-gspn/storm-gspn.h
index 095b82aca..de3811109 100644
--- a/src/storm-gspn/storm-gspn.h
+++ b/src/storm-gspn/storm-gspn.h
@@ -13,8 +13,7 @@ namespace storm {
* Builds JANI model from GSPN.
*/
storm::jani::Model* buildJani(storm::gspn::GSPN const& gspn) {
- std::shared_ptr<storm::expressions::ExpressionManager> exprManager(new storm::expressions::ExpressionManager());
- storm::builder::JaniGSPNBuilder builder(gspn, exprManager);
+ storm::builder::JaniGSPNBuilder builder(gspn);
return builder.build();
}
From 488aaeaa580063577aca3ea3e89dc89bd4951814 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@gmail.com>
Date: Mon, 6 Feb 2017 18:41:14 +0100
Subject: [PATCH 14/24] properties in storm-gspn
---
src/storm-gspn-cli/storm-gspn.cpp | 13 ++++++++++++-
src/storm-gspn/builder/JaniGSPNBuilder.cpp | 4 ++--
src/storm-gspn/builder/JaniGSPNBuilder.h | 7 +++----
src/storm-gspn/storage/gspn/GSPN.cpp | 4 ++--
src/storm-gspn/storage/gspn/GspnBuilder.cpp | 9 +++++----
src/storm/utility/storm.cpp | 2 +-
src/storm/utility/storm.h | 5 +++++
7 files changed, 30 insertions(+), 14 deletions(-)
diff --git a/src/storm-gspn-cli/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp
index fdf2594fc..b01824c50 100644
--- a/src/storm-gspn-cli/storm-gspn.cpp
+++ b/src/storm-gspn-cli/storm-gspn.cpp
@@ -14,6 +14,8 @@
#include "utility/storm.h"
#include "storm/cli/cli.h"
+#include "storm/parser/FormulaParser.h"
+
#include "storm/storage/expressions/ExpressionManager.h"
#include "storm/storage/jani/Model.h"
#include "storm/storage/jani/JSONExporter.h"
@@ -33,6 +35,7 @@
#include "storm/settings/modules/JaniExportSettings.h"
#include "storm/settings/modules/ResourceSettings.h"
+
/*!
* Initialize the settings manager.
*/
@@ -88,6 +91,14 @@ int main(const int argc, const char **argv) {
auto parser = storm::parser::GspnParser();
auto gspn = parser.parse(storm::settings::getModule<storm::settings::modules::GSPNSettings>().getGspnFilename());
+ std::string formulaString = "";
+ if (!storm::settings::getModule<storm::settings::modules::GeneralSettings>().isPropertySet()) {
+ formulaString = storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty();
+ }
+ boost::optional<std::set<std::string>> propertyFilter;
+ storm::parser::FormulaParser formulaParser(gspn->getExpressionManager());
+ std::vector<storm::jani::Property> properties = storm::parseProperties(formulaParser, formulaString, propertyFilter);
+
if (!gspn->isValid()) {
STORM_LOG_ERROR("The gspn is not valid.");
}
@@ -101,7 +112,7 @@ int main(const int argc, const char **argv) {
if(storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isJaniFileSet()) {
storm::jani::Model* model = storm::buildJani(*gspn);
- storm::exportJaniModel(*model, {}, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
+ storm::exportJaniModel(*model, properties, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
delete model;
}
diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.cpp b/src/storm-gspn/builder/JaniGSPNBuilder.cpp
index 386d2b0a2..d5e8846ea 100644
--- a/src/storm-gspn/builder/JaniGSPNBuilder.cpp
+++ b/src/storm-gspn/builder/JaniGSPNBuilder.cpp
@@ -19,10 +19,10 @@ namespace storm {
storm::jani::Variable* janiVar = nullptr;
if (!place.hasRestrictedCapacity()) {
// Effectively no capacity limit known
- janiVar = new storm::jani::UnboundedIntegerVariable(place.getName(), expressionManager->declareIntegerVariable(place.getName()), expressionManager->integer(place.getNumberOfInitialTokens()));
+ janiVar = new storm::jani::UnboundedIntegerVariable(place.getName(), expressionManager->getVariable(place.getName()), expressionManager->integer(place.getNumberOfInitialTokens()));
} else {
assert(place.hasRestrictedCapacity());
- janiVar = new storm::jani::BoundedIntegerVariable(place.getName(), expressionManager->declareIntegerVariable(place.getName()), expressionManager->integer(place.getNumberOfInitialTokens()), expressionManager->integer(0), expressionManager->integer(place.getCapacity()));
+ janiVar = new storm::jani::BoundedIntegerVariable(place.getName(), expressionManager->getVariable(place.getName()), expressionManager->integer(place.getNumberOfInitialTokens()), expressionManager->integer(0), expressionManager->integer(place.getCapacity()));
}
assert(janiVar != nullptr);
assert(vars.count(place.getID()) == 0);
diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.h b/src/storm-gspn/builder/JaniGSPNBuilder.h
index 791989009..474d04807 100644
--- a/src/storm-gspn/builder/JaniGSPNBuilder.h
+++ b/src/storm-gspn/builder/JaniGSPNBuilder.h
@@ -2,14 +2,15 @@
#include "storm-gspn/storage/gspn/GSPN.h"
#include "storm/storage/jani/Model.h"
+#include "storm/storage/jani/Property.h"
#include "storm/storage/expressions/ExpressionManager.h"
namespace storm {
namespace builder {
class JaniGSPNBuilder {
public:
- JaniGSPNBuilder(storm::gspn::GSPN const& gspn, std::shared_ptr<storm::expressions::ExpressionManager> const& expManager)
- : gspn(gspn), expressionManager(expManager) {
+ JaniGSPNBuilder(storm::gspn::GSPN const& gspn)
+ : gspn(gspn), expressionManager(gspn.getExpressionManager()) {
}
@@ -26,8 +27,6 @@ namespace storm {
private:
-
-
void addVariables(storm::jani::Model* model);
uint64_t addLocation(storm::jani::Automaton& automaton);
diff --git a/src/storm-gspn/storage/gspn/GSPN.cpp b/src/storm-gspn/storage/gspn/GSPN.cpp
index 34967daee..4a093b30e 100644
--- a/src/storm-gspn/storage/gspn/GSPN.cpp
+++ b/src/storm-gspn/storage/gspn/GSPN.cpp
@@ -28,7 +28,7 @@ namespace storm {
}
GSPN::GSPN(std::string const& name, std::vector<Place> const& places, std::vector<ImmediateTransition<WeightType>> const& itransitions, std::vector<TimedTransition<RateType>> const& ttransitions, std::vector<TransitionPartition> const& partitions, std::shared_ptr<storm::expressions::ExpressionManager> const& exprManager)
- : name(name), places(places), immediateTransitions(itransitions), timedTransitions(ttransitions), partitions(partitions), exprManager(exprManager);
+ : name(name), places(places), immediateTransitions(itransitions), timedTransitions(ttransitions), partitions(partitions), exprManager(exprManager)
{
}
@@ -136,7 +136,7 @@ namespace storm {
}
- std::shared_ptr<storm::expressions::ExpressionManager> const& GSPN::getExpressionManager() {
+ std::shared_ptr<storm::expressions::ExpressionManager> const& GSPN::getExpressionManager() const {
return exprManager;
}
diff --git a/src/storm-gspn/storage/gspn/GspnBuilder.cpp b/src/storm-gspn/storage/gspn/GspnBuilder.cpp
index 52833419a..5303a89c6 100644
--- a/src/storm-gspn/storage/gspn/GspnBuilder.cpp
+++ b/src/storm-gspn/storage/gspn/GspnBuilder.cpp
@@ -4,7 +4,6 @@
#include "storm/exceptions/IllegalFunctionCallException.h"
#include "storm/utility/macros.h"
-#include "storm/exceptions/IllegalFunctionCallException.h"
#include "storm/exceptions/InvalidArgumentException.h"
#include "Place.h"
@@ -165,7 +164,6 @@ namespace storm {
storm::gspn::GSPN* GspnBuilder::buildGspn() const {
std::shared_ptr<storm::expressions::ExpressionManager> exprManager(new storm::expressions::ExpressionManager());
- exprManager->
std::vector<TransitionPartition> orderedPartitions;
for(auto const& priorityPartitions : partitions) {
@@ -180,8 +178,11 @@ namespace storm {
}
std::reverse(orderedPartitions.begin(), orderedPartitions.end());
-
- GSPN* result = new GSPN(gspnName, places, immediateTransitions, timedTransitions, orderedPartitions);
+ for(auto const& placeEntry : placeNames) {
+ exprManager->declareIntegerVariable(placeEntry.first, false);
+ }
+
+ GSPN* result = new GSPN(gspnName, places, immediateTransitions, timedTransitions, orderedPartitions, exprManager);
result->setTransitionLayoutInfo(transitionLayout);
result->setPlaceLayoutInfo(placeLayout);
return result;
diff --git a/src/storm/utility/storm.cpp b/src/storm/utility/storm.cpp
index 1023d6aa6..f4d04bdcd 100644
--- a/src/storm/utility/storm.cpp
+++ b/src/storm/utility/storm.cpp
@@ -41,7 +41,7 @@ namespace storm{
}
}
- std::vector<storm::jani::Property> parseProperties(storm::parser::FormulaParser& formulaParser, std::string const& inputString, boost::optional<std::set<std::string>> const& propertyFilter = boost::none) {
+ std::vector<storm::jani::Property> parseProperties(storm::parser::FormulaParser& formulaParser, std::string const& inputString, boost::optional<std::set<std::string>> const& propertyFilter) {
// If the given property looks like a file (containing a dot and there exists a file with that name),
// we try to parse it as a file, otherwise we assume it's a property.
std::vector<storm::jani::Property> properties;
diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h
index 7e81f2a36..ef4785c1a 100644
--- a/src/storm/utility/storm.h
+++ b/src/storm/utility/storm.h
@@ -100,6 +100,10 @@
namespace storm {
+ namespace parser {
+ class FormulaParser;
+ }
+
template<typename ValueType>
std::shared_ptr<storm::models::sparse::Model<ValueType>> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile, boost::optional<std::string> const& stateRewardsFile = boost::none, boost::optional<std::string> const& transitionRewardsFile = boost::none, boost::optional<std::string> const& choiceLabelingFile = boost::none) {
return storm::parser::AutoParser<>::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "", choiceLabelingFile ? choiceLabelingFile.get() : "" );
@@ -109,6 +113,7 @@ namespace storm {
std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> parseJaniModel(std::string const& path);
storm::prism::Program parseProgram(std::string const& path);
std::vector<storm::jani::Property> substituteConstantsInProperties(std::vector<storm::jani::Property> const& properties, std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
+ std::vector<storm::jani::Property> parseProperties(storm::parser::FormulaParser& formulaParser, std::string const& inputString, boost::optional<std::set<std::string>> const& propertyFilter = boost::none);
std::vector<storm::jani::Property> parsePropertiesForExplicit(std::string const& inputString, boost::optional<std::set<std::string>> const& propertyFilter = boost::none);
std::vector<storm::jani::Property> parsePropertiesForPrismProgram(std::string const& inputString, storm::prism::Program const& program, boost::optional<std::set<std::string>> const& propertyFilter = boost::none);
std::vector<storm::jani::Property> parsePropertiesForJaniModel(std::string const& inputString, storm::jani::Model const& model, boost::optional<std::set<std::string>> const& propertyFilter = boost::none);
From 8fc0033bb223dc79ef0e437a877987132e071f2d Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@gmail.com>
Date: Mon, 6 Feb 2017 19:33:23 +0100
Subject: [PATCH 15/24] fix dft-to-gspn regarding properties, now compiles
again, and changed settings: Properties are now in IOSettings (should not
change usage)
---
src/storm-dft-cli/storm-dyftee.cpp | 11 +++---
src/storm-gspn-cli/storm-gspn.cpp | 4 +--
src/storm/cli/cli.cpp | 14 ++++----
.../settings/modules/GeneralSettings.cpp | 18 ----------
src/storm/settings/modules/GeneralSettings.h | 23 -------------
src/storm/settings/modules/IOSettings.cpp | 19 ++++++++++-
src/storm/settings/modules/IOSettings.h | 34 +++++++++++++++++--
7 files changed, 65 insertions(+), 58 deletions(-)
diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp
index fdc4a4d5e..308037d77 100644
--- a/src/storm-dft-cli/storm-dyftee.cpp
+++ b/src/storm-dft-cli/storm-dyftee.cpp
@@ -127,6 +127,7 @@ int main(const int argc, const char** argv) {
storm::settings::modules::DFTSettings const& dftSettings = storm::settings::getModule<storm::settings::modules::DFTSettings>();
storm::settings::modules::GeneralSettings const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
+ storm::settings::modules::IOSettings const& ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
if (!dftSettings.isDftFileSet() && !dftSettings.isDftJsonFileSet()) {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
}
@@ -147,9 +148,9 @@ int main(const int argc, const char** argv) {
uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId();
storm::handleGSPNExportSettings(*gspn);
-
- std::shared_ptr<storm::expressions::ExpressionManager> exprManager(new storm::expressions::ExpressionManager());
- storm::builder::JaniGSPNBuilder builder(*gspn, exprManager);
+
+ std::shared_ptr<storm::expressions::ExpressionManager> const& exprManager = gspn->getExpressionManager();
+ storm::builder::JaniGSPNBuilder builder(*gspn);
storm::jani::Model* model = builder.build();
storm::jani::Variable const& topfailedVar = builder.getPlaceVariable(toplevelFailedPlace);
@@ -203,9 +204,9 @@ int main(const int argc, const char** argv) {
std::string operatorType = "";
std::string targetFormula = "";
- if (generalSettings.isPropertySet()) {
+ if (ioSettings.isPropertySet()) {
STORM_LOG_THROW(!dftSettings.usePropExpectedTime() && !dftSettings.usePropProbability() && !dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given.");
- pctlFormula = generalSettings.getProperty();
+ pctlFormula = ioSettings.getProperty();
} else if (dftSettings.usePropExpectedTime()) {
STORM_LOG_THROW(!dftSettings.usePropProbability() && !dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given.");
operatorType = "T";
diff --git a/src/storm-gspn-cli/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp
index b01824c50..5ea31f30c 100644
--- a/src/storm-gspn-cli/storm-gspn.cpp
+++ b/src/storm-gspn-cli/storm-gspn.cpp
@@ -92,8 +92,8 @@ int main(const int argc, const char **argv) {
auto gspn = parser.parse(storm::settings::getModule<storm::settings::modules::GSPNSettings>().getGspnFilename());
std::string formulaString = "";
- if (!storm::settings::getModule<storm::settings::modules::GeneralSettings>().isPropertySet()) {
- formulaString = storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty();
+ if (!storm::settings::getModule<storm::settings::modules::IOSettings>().isPropertySet()) {
+ formulaString = storm::settings::getModule<storm::settings::modules::IOSettings>().getProperty();
}
boost::optional<std::set<std::string>> propertyFilter;
storm::parser::FormulaParser formulaParser(gspn->getExpressionManager());
diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp
index a8e02dd46..c5fb7ef8b 100644
--- a/src/storm/cli/cli.cpp
+++ b/src/storm/cli/cli.cpp
@@ -198,9 +198,9 @@ namespace storm {
}
boost::optional<std::set<std::string>> propertyFilter;
- std::string propertyFilterString = storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPropertyFilter();
+ std::string propertyFilterString = storm::settings::getModule<storm::settings::modules::IOSettings>().getPropertyFilter();
if (propertyFilterString != "all") {
- propertyFilter = storm::parsePropertyFilter(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPropertyFilter());
+ propertyFilter = storm::parsePropertyFilter(storm::settings::getModule<storm::settings::modules::IOSettings>().getPropertyFilter());
}
auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
@@ -245,9 +245,9 @@ namespace storm {
// Then proceed to parsing the properties (if given), since the model we are building may depend on the property.
STORM_LOG_TRACE("Parsing properties.");
- if (generalSettings.isPropertySet()) {
+ if (ioSettings.isPropertySet()) {
if (model.isJaniModel()) {
- properties = storm::parsePropertiesForJaniModel(generalSettings.getProperty(), model.asJaniModel(), propertyFilter);
+ properties = storm::parsePropertiesForJaniModel(ioSettings.getProperty(), model.asJaniModel(), propertyFilter);
if (labelRenaming) {
std::vector<storm::jani::Property> amendedProperties;
@@ -257,7 +257,7 @@ namespace storm {
properties = std::move(amendedProperties);
}
} else {
- properties = storm::parsePropertiesForPrismProgram(generalSettings.getProperty(), model.asPrismProgram(), propertyFilter);
+ properties = storm::parsePropertiesForPrismProgram(ioSettings.getProperty(), model.asPrismProgram(), propertyFilter);
}
constantDefinitions = model.parseConstantDefinitions(constantDefinitionString);
@@ -297,8 +297,8 @@ namespace storm {
// If the model is given in an explicit format, we parse the properties without allowing expressions
// in formulas.
std::vector<storm::jani::Property> properties;
- if (generalSettings.isPropertySet()) {
- properties = storm::parsePropertiesForExplicit(generalSettings.getProperty(), propertyFilter);
+ if (ioSettings.isPropertySet()) {
+ properties = storm::parsePropertiesForExplicit(ioSettings.getProperty(), propertyFilter);
}
buildAndCheckExplicitModel<double>(properties, true);
diff --git a/src/storm/settings/modules/GeneralSettings.cpp b/src/storm/settings/modules/GeneralSettings.cpp
index 373d20175..036eadeaa 100644
--- a/src/storm/settings/modules/GeneralSettings.cpp
+++ b/src/storm/settings/modules/GeneralSettings.cpp
@@ -26,8 +26,6 @@ namespace storm {
const std::string GeneralSettings::precisionOptionShortName = "eps";
const std::string GeneralSettings::configOptionName = "config";
const std::string GeneralSettings::configOptionShortName = "c";
- const std::string GeneralSettings::propertyOptionName = "prop";
- const std::string GeneralSettings::propertyOptionShortName = "prop";
const std::string GeneralSettings::bisimulationOptionName = "bisimulation";
const std::string GeneralSettings::bisimulationOptionShortName = "bisim";
const std::string GeneralSettings::parametricOptionName = "parametric";
@@ -43,11 +41,6 @@ namespace storm {
.addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to use.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, configOptionName, false, "If given, this file will be read and parsed for additional configuration settings.").setShortName(configOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the configuration.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
-
- this->addOption(storm::settings::OptionBuilder(moduleName, propertyOptionName, false, "Specifies the properties to be checked on the model.").setShortName(propertyOptionShortName)
- .addArgument(storm::settings::ArgumentBuilder::createStringArgument("property or filename", "The formula or the file containing the formulas.").build())
- .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filter", "The names of the properties to check.").setDefaultValueString("all").build())
- .build());
this->addOption(storm::settings::OptionBuilder(moduleName, parametricRegionOptionName, false, "Sets whether to use the parametric Region engine.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, bisimulationOptionName, false, "Sets whether to perform bisimulation minimization.").setShortName(bisimulationOptionShortName).build());
this->addOption(storm::settings::OptionBuilder(moduleName, parametricOptionName, false, "Sets whether to enable parametric model checking.").build());
@@ -81,18 +74,7 @@ namespace storm {
std::string GeneralSettings::getConfigFilename() const {
return this->getOption(configOptionName).getArgumentByName("filename").getValueAsString();
}
-
- bool GeneralSettings::isPropertySet() const {
- return this->getOption(propertyOptionName).getHasOptionBeenSet();
- }
-
- std::string GeneralSettings::getProperty() const {
- return this->getOption(propertyOptionName).getArgumentByName("property or filename").getValueAsString();
- }
- std::string GeneralSettings::getPropertyFilter() const {
- return this->getOption(propertyOptionName).getArgumentByName("filter").getValueAsString();
- }
bool GeneralSettings::isBisimulationSet() const {
return this->getOption(bisimulationOptionName).getHasOptionBeenSet();
diff --git a/src/storm/settings/modules/GeneralSettings.h b/src/storm/settings/modules/GeneralSettings.h
index 23ccfef2f..cac1c7ea0 100644
--- a/src/storm/settings/modules/GeneralSettings.h
+++ b/src/storm/settings/modules/GeneralSettings.h
@@ -70,27 +70,6 @@ namespace storm {
* @return The name of the file that is to be scanned for settings.
*/
std::string getConfigFilename() const;
-
- /*!
- * Retrieves whether the property option was set.
- *
- * @return True if the property option was set.
- */
- bool isPropertySet() const;
-
- /*!
- * Retrieves the property specified with the property option.
- *
- * @return The property specified with the property option.
- */
- std::string getProperty() const;
-
- /*!
- * Retrieves the property filter.
- *
- * @return The property filter.
- */
- std::string getPropertyFilter() const;
/*!
* Retrieves whether the option to perform bisimulation minimization is set.
@@ -146,8 +125,6 @@ namespace storm {
static const std::string precisionOptionShortName;
static const std::string configOptionName;
static const std::string configOptionShortName;
- static const std::string propertyOptionName;
- static const std::string propertyOptionShortName;
static const std::string bisimulationOptionName;
static const std::string bisimulationOptionShortName;
static const std::string parametricOptionName;
diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp
index bf8055c31..9f07c0219 100644
--- a/src/storm/settings/modules/IOSettings.cpp
+++ b/src/storm/settings/modules/IOSettings.cpp
@@ -40,6 +40,8 @@ namespace storm {
const std::string IOSettings::fullModelBuildOptionName = "buildfull";
const std::string IOSettings::janiPropertyOptionName = "janiproperty";
const std::string IOSettings::janiPropertyOptionShortName = "jprop";
+ const std::string IOSettings::propertyOptionName = "prop";
+ const std::string IOSettings::propertyOptionShortName = "prop";
IOSettings::IOSettings() : ModuleSettings(moduleName) {
@@ -59,7 +61,10 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, jitOptionName, false, "If set, the model is built using the JIT model builder.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, fullModelBuildOptionName, false, "If set, include all rewards and labels.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, noBuildOptionName, false, "If set, do not build the model.").build());
-
+ this->addOption(storm::settings::OptionBuilder(moduleName, propertyOptionName, false, "Specifies the properties to be checked on the model.").setShortName(propertyOptionShortName)
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("property or filename", "The formula or the file containing the formulas.").build())
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filter", "The names of the properties to check.").setDefaultValueString("all").build())
+ .build());
std::vector<std::string> explorationOrders = {"dfs", "bfs"};
this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the exploration order to choose.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(explorationOrders)).setDefaultValueString("bfs").build()).build());
@@ -207,6 +212,18 @@ namespace storm {
return this->getOption(noBuildOptionName).getHasOptionBeenSet();
}
+ bool IOSettings::isPropertySet() const {
+ return this->getOption(propertyOptionName).getHasOptionBeenSet();
+ }
+
+ std::string IOSettings::getProperty() const {
+ return this->getOption(propertyOptionName).getArgumentByName("property or filename").getValueAsString();
+ }
+
+ std::string IOSettings::getPropertyFilter() const {
+ return this->getOption(propertyOptionName).getArgumentByName("filter").getValueAsString();
+ }
+
void IOSettings::finalize() {
}
diff --git a/src/storm/settings/modules/IOSettings.h b/src/storm/settings/modules/IOSettings.h
index 3c34f94f7..711ec2d97 100644
--- a/src/storm/settings/modules/IOSettings.h
+++ b/src/storm/settings/modules/IOSettings.h
@@ -211,11 +211,39 @@ namespace storm {
* @return The string that defines the constants of a symbolic model.
*/
std::string getConstantDefinitionString() const;
-
+
+ /*!
+ * Retrieves whether the jani-property option was set
+ * @return
+ */
bool isJaniPropertiesSet() const;
-
+
+ /*!
+ * @return The names of the jani properties to check
+ */
std::vector<std::string> getJaniProperties() const;
+ /*!
+ * Retrieves whether the property option was set.
+ *
+ * @return True if the property option was set.
+ */
+ bool isPropertySet() const;
+
+ /*!
+ * Retrieves the property specified with the property option.
+ *
+ * @return The property specified with the property option.
+ */
+ std::string getProperty() const;
+
+ /*!
+ * Retrieves the property filter.
+ *
+ * @return The property filter.
+ */
+ std::string getPropertyFilter() const;
+
/*!
* Retrieves whether the PRISM compatibility mode was enabled.
*
@@ -266,6 +294,8 @@ namespace storm {
static const std::string noBuildOptionName;
static const std::string janiPropertyOptionName;
static const std::string janiPropertyOptionShortName;
+ static const std::string propertyOptionName;
+ static const std::string propertyOptionShortName;
};
} // namespace modules
From fa49ebb922d200ab5eb12b806e9124d86ed5b57c Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 6 Feb 2017 21:04:06 +0100
Subject: [PATCH 16/24] installing correct libcarl if built from shipped
version
---
CMakeLists.txt | 6 +++---
resources/3rdparty/CMakeLists.txt | 11 +++++------
src/storm/utility/storm-version.h | 2 +-
3 files changed, 9 insertions(+), 10 deletions(-)
diff --git a/CMakeLists.txt b/CMakeLists.txt
index f0d00bb29..cd51e1343 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -355,15 +355,15 @@ endif(DOXYGEN_FOUND)
# If storm is built from an archive, we need to skip the version detection based on git.
if (STORM_SOURCE STREQUAL "archive")
if (NOT DEFINED STORM_VERSION_MAJOR OR NOT DEFINED STORM_VERSION_MINOR OR NOT DEFINED STORM_VERSION_PATCH)
- message(FATAL_ERROR "storm - Building from archive requires setting a version via cmake.")
+ message(FATAL_ERROR "storm - building from archive requires setting a version via cmake.")
endif()
- message(STATUS "storm - Version is ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH} (building from archive).")
+ message(STATUS "storm - version is ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH} (building from archive).")
set(STORM_VERSION_COMMITS_AHEAD boost::none)
set(STORM_VERSION_GIT_HASH boost::none)
set(STORM_VERSION_DIRTY boost::none)
else()
if (DEFINED STORM_VERSION_MAJOR OR DEFINED STORM_VERSION_MINOR OR DEFINED STORM_VERSION_PATCH)
- message(FATAL_ERROR "storm - Building from git does not support setting a version via cmake.")
+ message(FATAL_ERROR "storm - building from git does not support setting a version via cmake.")
endif()
# Make a version file containing the current version from git.
diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt
index fcadfbdd8..9dcf30aed 100644
--- a/resources/3rdparty/CMakeLists.txt
+++ b/resources/3rdparty/CMakeLists.txt
@@ -229,7 +229,7 @@ if(USE_CARL)
BUILD_COMMAND make lib_carl
INSTALL_COMMAND make install
LOG_BUILD ON
- LOG_INSTALL ON
+ LOG_INSTALL ON
BUILD_BYPRODUCTS ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl${DYNAMIC_EXT}
)
include(${STORM_3RDPARTY_BINARY_DIR}/carl/carlConfig.cmake)
@@ -241,8 +241,7 @@ if(USE_CARL)
set(STORM_HAVE_CARL ON)
# install the carl dynamic library if we build it
- get_filename_component(STORM_CARL_DYLIB_FULL_PATH ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl${DYNAMIC_EXT} REALPATH)
- install(FILES ${STORM_CARL_DYLIB_FULL_PATH} DESTINATION lib)
+ install(FILES ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl.1.0.0${DYNAMIC_EXT} DESTINATION lib)
endif()
if(STORM_USE_CLN_NUMBERS AND NOT STORM_HAVE_CLN)
message(FATAL_ERROR "Cannot use CLN numbers if carl is build without")
@@ -267,7 +266,7 @@ if(USE_SMTRAT)
include_directories("${smtrat_INCLUDE_DIR}")
list(APPEND STORM_LINK_LIBRARIES ${smtrat_LIBRARIES})
else()
- message(FATAL_ERROR "StoRM - SMT-RAT was requested but not found")
+ message(FATAL_ERROR "storm - SMT-RAT was requested but not found")
endif()
endif()
@@ -287,7 +286,7 @@ if(USE_HYPRO)
include_directories("${hypro_INCLUDE_DIR}")
list(APPEND STORM_LINK_LIBRARIES ${hypro_LIBRARIES})
else()
- message(FATAL_ERROR "StoRM - HyPro was requested but not found")
+ message(FATAL_ERROR "storm - HyPro was requested but not found")
endif()
endif()
@@ -493,7 +492,7 @@ if(ENABLE_CUDA)
if(NOT STORM_CUDA_COMPILE_RESULT_TYPEALIGNMENT)
message(FATAL_ERROR "storm (CudaPlugin) - Could not test type alignment, there was an Error while compiling the file ${PROJECT_SOURCE_DIR}/cuda/CMakeAlignmentCheck.cpp: ${OUTPUT_TEST_VAR}")
elseif(STORM_CUDA_RUN_RESULT_TYPEALIGNMENT EQUAL 0)
- message(STATUS "StoRM (CudaPlugin) - Result of Type Alignment Check: OK.")
+ message(STATUS "storm (CudaPlugin) - Result of Type Alignment Check: OK.")
else()
message(FATAL_ERROR "storm (CudaPlugin) - Result of Type Alignment Check: FAILED (Code ${STORM_CUDA_RUN_RESULT_TYPEALIGNMENT})")
endif()
diff --git a/src/storm/utility/storm-version.h b/src/storm/utility/storm-version.h
index 5c2412670..12bad5c21 100644
--- a/src/storm/utility/storm-version.h
+++ b/src/storm/utility/storm-version.h
@@ -55,7 +55,7 @@ namespace storm {
sstream << " build from revision " << gitRevisionHash.get();
}
if (dirty && dirty.get() == 1) {
- sstream << " (DIRTY)";
+ sstream << " (dirty)";
}
sstream << "." << std::endl;
return sstream.str();
From a85f4fdc897f64626514c389311c6f8ec9464518 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 7 Feb 2017 18:52:42 +0100
Subject: [PATCH 17/24] replaced some StoRMs and Storms by storm, reworked
version output a bit
---
CMakeLists.txt | 6 +-
resources/3rdparty/CMakeLists.txt | 2 +-
resources/3rdparty/include_cpptemplate.cmake | 2 +-
resources/3rdparty/include_cudd.cmake | 4 +-
resources/3rdparty/include_glpk.cmake | 6 +-
resources/3rdparty/include_xerces.cmake | 8 +-
src/storm-dft-cli/CMakeLists.txt | 5 +-
src/storm-dft-cli/storm-dyftee.cpp | 8 +-
src/storm-dft/CMakeLists.txt | 3 +
src/storm-gspn-cli/CMakeLists.txt | 3 +
src/storm-gspn-cli/storm-gspn.cpp | 8 +-
src/storm-gspn/CMakeLists.txt | 3 +
src/storm-gspn/parser/GspnParser.cpp | 2 +-
src/storm-pgcl-cli/CMakeLists.txt | 5 +-
src/storm-pgcl-cli/storm-pgcl.cpp | 8 +-
src/storm-pgcl/CMakeLists.txt | 3 +
src/storm/CMakeLists.txt | 9 +-
.../jit/ExplicitJitJaniModelBuilder.cpp | 2 +-
src/storm/cli/cli.cpp | 113 +++++++++---------
src/storm/cli/cli.h | 4 +-
.../SMTMinimalCommandSetGenerator.h | 4 +-
src/storm/parser/JaniParser.cpp | 20 ++--
src/storm/settings/SettingsManager.cpp | 5 -
src/storm/settings/SettingsManager.h | 5 -
.../settings/modules/JitBuilderSettings.cpp | 4 +-
src/storm/solver/GlpkLpSolver.h | 50 ++++----
src/storm/solver/GurobiLpSolver.cpp | 50 ++++----
src/storm/solver/MathsatSmtSolver.cpp | 32 ++---
src/storm/solver/NativeLinearEquationSolver.h | 2 +-
.../TopologicalMinMaxLinearEquationSolver.cpp | 8 +-
.../TopologicalMinMaxLinearEquationSolver.h | 8 +-
src/storm/solver/Z3SmtSolver.cpp | 38 +++---
src/storm/storage/jani/JSONExporter.cpp | 2 +-
src/storm/storm.cpp | 8 +-
src/storm/utility/ExplicitExporter.cpp | 2 +-
src/storm/utility/storm-version.h | 5 +-
src/test/storm-test.cpp | 2 +-
37 files changed, 231 insertions(+), 218 deletions(-)
diff --git a/CMakeLists.txt b/CMakeLists.txt
index cd51e1343..ee5bf36be 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -25,8 +25,8 @@ option(STORM_DEVELOPER "Sets whether the development mode is used." OFF)
option(STORM_ALLWARNINGS "Compile with even more warnings" OFF)
option(STORM_USE_LTO "Sets whether link-time optimizations are enabled." ON)
MARK_AS_ADVANCED(STORM_USE_LTO)
-option(STORM_PORTABLE_RELEASE "Sets whether a release build needs to be portable to another machine." OFF)
-MARK_AS_ADVANCED(STORM_PORTABLE_RELEASE)
+option(STORM_PORTABLE "Sets whether a build needs to be portable." OFF)
+MARK_AS_ADVANCED(STORM_PORTABLE)
option(STORM_USE_POPCNT "Sets whether the popcnt instruction is going to be used." ON)
MARK_AS_ADVANCED(STORM_USE_POPCNT)
option(USE_BOOST_STATIC_LIBRARIES "Sets whether the Boost libraries should be linked statically." OFF)
@@ -239,7 +239,7 @@ if (STORM_USE_LTO)
endif()
# In release mode, we turn on even more optimizations if we do not have to provide a portable binary.
-if (NOT STORM_PORTABLE_RELEASE)
+if (NOT STORM_PORTABLE)
set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -march=native")
endif ()
diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt
index 9dcf30aed..64fc5d7b3 100644
--- a/resources/3rdparty/CMakeLists.txt
+++ b/resources/3rdparty/CMakeLists.txt
@@ -351,7 +351,7 @@ ExternalProject_Add(
DOWNLOAD_COMMAND ""
PREFIX "sylvan"
SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/sylvan
- CMAKE_ARGS -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER} -DSYLVAN_BUILD_TEST=Off -DSYLVAN_BUILD_EXAMPLES=Off -DCMAKE_BUILD_TYPE=Release -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DUSE_CARL=ON -Dcarl_INCLUDE_DIR=${carl_INCLUDE_DIR} -DSYLVAN_PORTABLE=${STORM_PORTABLE_RELEASE} -Dcarl_LIBRARIES=${carl_LIBRARIES}
+ CMAKE_ARGS -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER} -DSYLVAN_BUILD_TEST=Off -DSYLVAN_BUILD_EXAMPLES=Off -DCMAKE_BUILD_TYPE=Release -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DUSE_CARL=ON -Dcarl_INCLUDE_DIR=${carl_INCLUDE_DIR} -DSYLVAN_PORTABLE=${STORM_PORTABLE} -Dcarl_LIBRARIES=${carl_LIBRARIES}
BINARY_DIR ${STORM_3RDPARTY_BINARY_DIR}/sylvan
BUILD_IN_SOURCE 0
INSTALL_COMMAND ""
diff --git a/resources/3rdparty/include_cpptemplate.cmake b/resources/3rdparty/include_cpptemplate.cmake
index e6f341b31..3cf4f43b4 100644
--- a/resources/3rdparty/include_cpptemplate.cmake
+++ b/resources/3rdparty/include_cpptemplate.cmake
@@ -24,6 +24,6 @@ set(CPPTEMPLATE_INCLUDE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/cpptemplate)
set(CPPTEMPLATE_STATIC_LIBRARY ${STORM_3RDPARTY_BINARY_DIR}/cpptemplate/cpptemplate${STATIC_EXT})
add_dependencies(resources cpptemplate)
-message(STATUS "Storm - Linking with cpptemplate.")
+message(STATUS "storm - Linking with cpptemplate.")
add_imported_library(cpptempl STATIC ${CPPTEMPLATE_STATIC_LIBRARY} ${CPPTEMPLATE_INCLUDE_DIR})
list(APPEND STORM_DEP_TARGETS cpptempl_STATIC)
\ No newline at end of file
diff --git a/resources/3rdparty/include_cudd.cmake b/resources/3rdparty/include_cudd.cmake
index 1c03de839..8f17fb35b 100644
--- a/resources/3rdparty/include_cudd.cmake
+++ b/resources/3rdparty/include_cudd.cmake
@@ -17,7 +17,7 @@ endif()
set(CUDD_LIB_DIR ${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0/lib)
set(STORM_CUDD_FLAGS "CFLAGS=-O3 -w -DPIC -DHAVE_IEEE_754 -fno-common -ffast-math -fno-finite-math-only")
-if (NOT STORM_PORTABLE_RELEASE)
+if (NOT STORM_PORTABLE)
set(STORM_CUDD_FLAGS "${STORM_CUDD_FLAGS} -march=native")
endif()
@@ -54,4 +54,4 @@ else()
list(APPEND STORM_DEP_TARGETS cudd_STATIC)
endif()
-message(STATUS "Storm - Linking with CUDD ${CUDD_VERSION_STRING}.")
+message(STATUS "storm - Linking with CUDD ${CUDD_VERSION_STRING}.")
diff --git a/resources/3rdparty/include_glpk.cmake b/resources/3rdparty/include_glpk.cmake
index e7dc55149..1f1eed1f1 100644
--- a/resources/3rdparty/include_glpk.cmake
+++ b/resources/3rdparty/include_glpk.cmake
@@ -1,8 +1,8 @@
find_package(GLPK QUIET)
if(GLPK_FOUND)
- message (STATUS "Storm - Using system version of glpk.")
+ message (STATUS "storm - Using system version of glpk.")
else()
- message (STATUS "Storm - Using shipped version of glpk.")
+ message (STATUS "storm - Using shipped version of glpk.")
set(GLPK_LIB_DIR ${STORM_3RDPARTY_BINARY_DIR}/glpk-4.57/lib)
ExternalProject_Add(glpk_ext
DOWNLOAD_COMMAND ""
@@ -25,7 +25,7 @@ endif()
# Since there is a shipped version, always use GLPK
set(STORM_HAVE_GLPK ON)
-message (STATUS "Storm - Linking with glpk ${GLPK_VERSION_STRING}")
+message (STATUS "storm - Linking with glpk ${GLPK_VERSION_STRING}")
add_imported_library(glpk SHARED ${GLPK_LIBRARIES} ${GLPK_INCLUDE_DIR})
list(APPEND STORM_DEP_TARGETS glpk_SHARED)
\ No newline at end of file
diff --git a/resources/3rdparty/include_xerces.cmake b/resources/3rdparty/include_xerces.cmake
index 4a464835d..d7ed7e1f9 100644
--- a/resources/3rdparty/include_xerces.cmake
+++ b/resources/3rdparty/include_xerces.cmake
@@ -1,9 +1,9 @@
if(USE_XERCESC)
find_package(XercesC QUIET)
if(XercesC_FOUND)
- message(STATUS "Storm - Use system version of xerces.")
+ message(STATUS "storm - Use system version of xerces.")
else()
- message(STATUS "Storm - Use shipped version of xerces.")
+ message(STATUS "storm - Use shipped version of xerces.")
set(XercesC_LIB_DIR ${STORM_3RDPARTY_BINARY_DIR}/xercesc-3.1.2/lib)
ExternalProject_Add(
xercesc
@@ -31,7 +31,7 @@ if(USE_XERCESC)
add_dependencies(resources xercesc)
endif()
- message (STATUS "Storm - Linking with xercesc.")
+ message (STATUS "storm - Linking with xercesc.")
set(STORM_HAVE_XERCES ON)
include_directories(${XercesC_INCLUDE_DIRS})
if(APPLE)
@@ -44,5 +44,5 @@ if(USE_XERCESC)
list(APPEND STORM_GSPN_LINK_LIBRARIES ${XercesC_LIBRARIES} ${COREFOUNDATION_LIBRARY} ${CORESERVICES_LIBRARY} ${CURL_LIBRARIES})
else()
set(STORM_HAVE_XERCES OFF)
- message (WARNING "Storm - Building without Xerces disables parsing XML formats (for GSPNs)")
+ message (WARNING "torm - Building without Xerces disables parsing XML formats (for GSPNs)")
endif(USE_XERCESC)
diff --git a/src/storm-dft-cli/CMakeLists.txt b/src/storm-dft-cli/CMakeLists.txt
index f44c57103..515022607 100644
--- a/src/storm-dft-cli/CMakeLists.txt
+++ b/src/storm-dft-cli/CMakeLists.txt
@@ -1,4 +1,7 @@
# Create storm-dft.
add_executable(storm-dft-cli ${PROJECT_SOURCE_DIR}/src/storm-dft-cli/storm-dyftee.cpp)
target_link_libraries(storm-dft-cli storm-dft) # Adding headers for xcode
-set_target_properties(storm-dft-cli PROPERTIES OUTPUT_NAME "storm-dft")
\ No newline at end of file
+set_target_properties(storm-dft-cli PROPERTIES OUTPUT_NAME "storm-dft")
+
+# installation
+install(TARGETS storm-dft-cli RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
\ No newline at end of file
diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp
index 308037d77..5f4cdaee4 100644
--- a/src/storm-dft-cli/storm-dyftee.cpp
+++ b/src/storm-dft-cli/storm-dyftee.cpp
@@ -80,7 +80,7 @@ void analyzeWithSMT(std::string filename) {
* Initialize the settings manager.
*/
void initializeSettings() {
- storm::settings::mutableManager().setName("StoRM-DyFTeE", "storm-dft");
+ storm::settings::mutableManager().setName("storm-DyFTeE", "storm-dft");
// Register all known settings modules.
storm::settings::addModule<storm::settings::modules::GeneralSettings>();
@@ -117,7 +117,7 @@ void initializeSettings() {
int main(const int argc, const char** argv) {
try {
storm::utility::setUp();
- storm::cli::printHeader("StoRM-DyFTeE", argc, argv);
+ storm::cli::printHeader("storm-DyFTeE", argc, argv);
initializeSettings();
bool optionsCorrect = storm::cli::parseOptions(argc, argv);
@@ -250,10 +250,10 @@ int main(const int argc, const char** argv) {
storm::utility::cleanUp();
return 0;
} catch (storm::exceptions::BaseException const& exception) {
- STORM_LOG_ERROR("An exception caused StoRM-DyFTeE to terminate. The message of the exception is: " << exception.what());
+ STORM_LOG_ERROR("An exception caused storm-DyFTeE to terminate. The message of the exception is: " << exception.what());
return 1;
} catch (std::exception const& exception) {
- STORM_LOG_ERROR("An unexpected exception occurred and caused StoRM-DyFTeE to terminate. The message of this exception is: " << exception.what());
+ STORM_LOG_ERROR("An unexpected exception occurred and caused storm-DyFTeE to terminate. The message of this exception is: " << exception.what());
return 2;
}
}
diff --git a/src/storm-dft/CMakeLists.txt b/src/storm-dft/CMakeLists.txt
index 10d9b8508..16fa40e48 100644
--- a/src/storm-dft/CMakeLists.txt
+++ b/src/storm-dft/CMakeLists.txt
@@ -11,3 +11,6 @@ file(GLOB_RECURSE STORM_DFT_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-dft/*/*.h)
# Create storm-pgcl.
add_library(storm-dft SHARED ${STORM_DFT_SOURCES} ${STORM_DFT_HEADERS})
target_link_libraries(storm-dft storm storm-gspn ${STORM_DFT_LINK_LIBRARIES})
+
+# installation
+install(TARGETS storm-dft RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
diff --git a/src/storm-gspn-cli/CMakeLists.txt b/src/storm-gspn-cli/CMakeLists.txt
index 343b8acc8..2898325f3 100644
--- a/src/storm-gspn-cli/CMakeLists.txt
+++ b/src/storm-gspn-cli/CMakeLists.txt
@@ -1,3 +1,6 @@
add_executable(storm-gspn-cli ${PROJECT_SOURCE_DIR}/src/storm-gspn-cli/storm-gspn.cpp)
target_link_libraries(storm-gspn-cli storm-gspn) # Adding headers for xcode
set_target_properties(storm-gspn-cli PROPERTIES OUTPUT_NAME "storm-gspn")
+
+# installation
+install(TARGETS storm-gspn-cli RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
\ No newline at end of file
diff --git a/src/storm-gspn-cli/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp
index 5ea31f30c..2dd98e645 100644
--- a/src/storm-gspn-cli/storm-gspn.cpp
+++ b/src/storm-gspn-cli/storm-gspn.cpp
@@ -40,7 +40,7 @@
* Initialize the settings manager.
*/
void initializeSettings() {
- storm::settings::mutableManager().setName("StoRM-GSPN", "storm-gspn");
+ storm::settings::mutableManager().setName("storm-GSPN", "storm-gspn");
// Register all known settings modules.
storm::settings::addModule<storm::settings::modules::GeneralSettings>();
@@ -75,7 +75,7 @@ std::unordered_map<std::string, uint64_t> parseCapacitiesList(std::string const&
int main(const int argc, const char **argv) {
try {
storm::utility::setUp();
- storm::cli::printHeader("StoRM-GSPN", argc, argv);
+ storm::cli::printHeader("storm-GSPN", argc, argv);
initializeSettings();
bool optionsCorrect = storm::cli::parseOptions(argc, argv);
@@ -147,10 +147,10 @@ int main(const int argc, const char **argv) {
storm::utility::cleanUp();
return 0;
} catch (storm::exceptions::BaseException const& exception) {
- STORM_LOG_ERROR("An exception caused StoRM to terminate. The message of the exception is: " << exception.what());
+ STORM_LOG_ERROR("An exception caused storm to terminate. The message of the exception is: " << exception.what());
return 1;
} catch (std::exception const& exception) {
- STORM_LOG_ERROR("An unexpected exception occurred and caused StoRM to terminate. The message of this exception is: " << exception.what());
+ STORM_LOG_ERROR("An unexpected exception occurred and caused storm to terminate. The message of this exception is: " << exception.what());
return 2;
}
}
diff --git a/src/storm-gspn/CMakeLists.txt b/src/storm-gspn/CMakeLists.txt
index a5478280d..564b696bd 100644
--- a/src/storm-gspn/CMakeLists.txt
+++ b/src/storm-gspn/CMakeLists.txt
@@ -11,3 +11,6 @@ file(GLOB_RECURSE STORM_GSPN_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-gspn/*/*.h)
# Create storm-pgcl.
add_library(storm-gspn SHARED ${STORM_GSPN_SOURCES} ${STORM_GSPN_HEADERS})
target_link_libraries(storm-gspn storm ${STORM_GSPN_LINK_LIBRARIES})
+
+# installation
+install(TARGETS storm-gspn RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
\ No newline at end of file
diff --git a/src/storm-gspn/parser/GspnParser.cpp b/src/storm-gspn/parser/GspnParser.cpp
index b92b6f006..cf5c698f0 100644
--- a/src/storm-gspn/parser/GspnParser.cpp
+++ b/src/storm-gspn/parser/GspnParser.cpp
@@ -81,7 +81,7 @@ namespace storm {
delete errHandler;
xercesc::XMLPlatformUtils::Terminate();
#else
- STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Storm is not compiled with XML support: " << filename << " can not be parsed");
+ STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "storm is not compiled with XML support: " << filename << " can not be parsed");
#endif
}
}
diff --git a/src/storm-pgcl-cli/CMakeLists.txt b/src/storm-pgcl-cli/CMakeLists.txt
index d8884639e..0f051a1b4 100644
--- a/src/storm-pgcl-cli/CMakeLists.txt
+++ b/src/storm-pgcl-cli/CMakeLists.txt
@@ -1,3 +1,6 @@
add_executable(storm-pgcl-cli ${PROJECT_SOURCE_DIR}/src/storm-pgcl-cli/storm-pgcl.cpp)
target_link_libraries(storm-pgcl-cli storm-pgcl)
-set_target_properties(storm-pgcl-cli PROPERTIES OUTPUT_NAME "storm-pgcl")
\ No newline at end of file
+set_target_properties(storm-pgcl-cli PROPERTIES OUTPUT_NAME "storm-pgcl")
+
+# installation
+install(TARGETS storm-pgcl-cli RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
\ No newline at end of file
diff --git a/src/storm-pgcl-cli/storm-pgcl.cpp b/src/storm-pgcl-cli/storm-pgcl.cpp
index 37accc430..6a6707177 100644
--- a/src/storm-pgcl-cli/storm-pgcl.cpp
+++ b/src/storm-pgcl-cli/storm-pgcl.cpp
@@ -25,7 +25,7 @@
* Initialize the settings manager.
*/
void initializeSettings() {
- storm::settings::mutableManager().setName("StoRM-PGCL", "storm-pgcl");
+ storm::settings::mutableManager().setName("storm-PGCL", "storm-pgcl");
// Register all known settings modules.
storm::settings::addModule<storm::settings::modules::GeneralSettings>();
@@ -59,7 +59,7 @@ void programGraphToDotFile(storm::ppg::ProgramGraph const& prog) {
int main(const int argc, const char** argv) {
try {
storm::utility::setUp();
- storm::cli::printHeader("StoRM-PGCL", argc, argv);
+ storm::cli::printHeader("storm-PGCL", argc, argv);
initializeSettings();
bool optionsCorrect = storm::cli::parseOptions(argc, argv);
@@ -96,10 +96,10 @@ int main(const int argc, const char** argv) {
}
}catch (storm::exceptions::BaseException const& exception) {
- STORM_LOG_ERROR("An exception caused StoRM-PGCL to terminate. The message of the exception is: " << exception.what());
+ STORM_LOG_ERROR("An exception caused storm-PGCL to terminate. The message of the exception is: " << exception.what());
return 1;
} catch (std::exception const& exception) {
- STORM_LOG_ERROR("An unexpected exception occurred and caused StoRM-PGCL to terminate. The message of this exception is: " << exception.what());
+ STORM_LOG_ERROR("An unexpected exception occurred and caused storm-PGCL to terminate. The message of this exception is: " << exception.what());
return 2;
}
}
diff --git a/src/storm-pgcl/CMakeLists.txt b/src/storm-pgcl/CMakeLists.txt
index bd1ffc932..e20a99483 100644
--- a/src/storm-pgcl/CMakeLists.txt
+++ b/src/storm-pgcl/CMakeLists.txt
@@ -11,3 +11,6 @@ file(GLOB_RECURSE STORM_PGCL_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-pgcl/*/*.h)
# Create storm-pgcl.
add_library(storm-pgcl SHARED ${STORM_PGCL_SOURCES} ${STORM_PGCL_HEADERS})
target_link_libraries(storm-pgcl storm)
+
+# installation
+install(TARGETS storm-pgcl RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
\ No newline at end of file
diff --git a/src/storm/CMakeLists.txt b/src/storm/CMakeLists.txt
index d9135dcb9..1a722e207 100644
--- a/src/storm/CMakeLists.txt
+++ b/src/storm/CMakeLists.txt
@@ -20,11 +20,11 @@ set(STORM_MAIN_SOURCES ${STORM_MAIN_FILE})
# Add custom additional include or link directories
if (ADDITIONAL_INCLUDE_DIRS)
- message(STATUS "StoRM - Using additional include directories ${ADDITIONAL_INCLUDE_DIRS}")
+ message(STATUS "storm - Using additional include directories ${ADDITIONAL_INCLUDE_DIRS}")
include_directories(${ADDITIONAL_INCLUDE_DIRS})
endif(ADDITIONAL_INCLUDE_DIRS)
if (ADDITIONAL_LINK_DIRS)
- message(STATUS "StoRM - Using additional link directories ${ADDITIONAL_LINK_DIRS}")
+ message(STATUS "storm - Using additional link directories ${ADDITIONAL_LINK_DIRS}")
link_directories(${ADDITIONAL_LINK_DIRS})
endif(ADDITIONAL_LINK_DIRS)
@@ -68,5 +68,6 @@ add_custom_target(copy_storm_headers DEPENDS ${STORM_OUTPUT_HEADERS} ${STORM_LIB
add_dependencies(storm copy_storm_headers)
add_dependencies(storm copy_resources_headers)
-# install command
-install(TARGETS storm-main storm RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
\ No newline at end of file
+# installation
+install(TARGETS storm RUNTIME DESTINATION bin LIBRARY DESTINATION lib)
+install(TARGETS storm-main RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
index 3c6789324..ce2bd80c1 100644
--- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
+++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
@@ -324,7 +324,7 @@ namespace storm {
template <typename ValueType, typename RewardModelType>
bool ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::checkStormHeadersAvailable() const {
bool result = true;
- std::string problem = "Unable to compile program using Storm headers. Is Storm's include directory '" + stormIncludeDirectory + "' set correctly? Does the directory contain all the headers (in particular 'storm-config.h'?";
+ std::string problem = "Unable to compile program using storm headers. Is storm's include directory '" + stormIncludeDirectory + "' set correctly? Does the directory contain all the headers (in particular 'storm-config.h')?";
try {
std::string program = R"(
#include "storm/builder/RewardModelInformation.h"
diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp
index c5fb7ef8b..efdb54d42 100644
--- a/src/storm/cli/cli.cpp
+++ b/src/storm/cli/cli.cpp
@@ -47,92 +47,95 @@ namespace storm {
char temp[512];
return (GetCurrentDir(temp, 512 - 1) ? std::string(temp) : std::string(""));
}
-
- void printHeader(const std::string name, const int argc, const char* argv[]) {
- std::cout << name << std::endl;
- std::cout << "---------------" << std::endl << std::endl;
-
-
- std::cout << storm::utility::StormVersion::longVersionString() << std::endl;
+
+ void printHeader(std::string const& name, const int argc, const char* argv[]) {
+ STORM_PRINT(name << " " << storm::utility::StormVersion::shortVersionString() << std::endl << std::endl);
+
+ // "Compute" the command line argument string with which storm was invoked.
+ std::stringstream commandStream;
+ for (int i = 1; i < argc; ++i) {
+ commandStream << argv[i] << " ";
+ }
+
+ std::string command = commandStream.str();
+
+ if (!command.empty()) {
+ STORM_PRINT("Command line arguments: " << commandStream.str() << std::endl);
+ STORM_PRINT("Current working directory: " << getCurrentWorkingDirectory() << std::endl << std::endl);
+ }
+ }
+
+ void printVersion(std::string const& name) {
+ STORM_PRINT(storm::utility::StormVersion::longVersionString() << std::endl);
+ STORM_PRINT(storm::utility::StormVersion::buildInfo() << std::endl);
+
#ifdef STORM_HAVE_INTELTBB
- std::cout << "Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " << TBB_INTERFACE_VERSION << ")." << std::endl;
+ STORM_PRINT("Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " << TBB_INTERFACE_VERSION << ")." << std::endl);
#endif
#ifdef STORM_HAVE_GLPK
- std::cout << "Linked with GNU Linear Programming Kit v" << GLP_MAJOR_VERSION << "." << GLP_MINOR_VERSION << "." << std::endl;
+ STORM_PRINT("Linked with GNU Linear Programming Kit v" << GLP_MAJOR_VERSION << "." << GLP_MINOR_VERSION << "." << std::endl);
#endif
#ifdef STORM_HAVE_GUROBI
- std::cout << "Linked with Gurobi Optimizer v" << GRB_VERSION_MAJOR << "." << GRB_VERSION_MINOR << "." << GRB_VERSION_TECHNICAL << "." << std::endl;
+ STORM_PRINT("Linked with Gurobi Optimizer v" << GRB_VERSION_MAJOR << "." << GRB_VERSION_MINOR << "." << GRB_VERSION_TECHNICAL << "." << std::endl);
#endif
#ifdef STORM_HAVE_Z3
unsigned int z3Major, z3Minor, z3BuildNumber, z3RevisionNumber;
Z3_get_version(&z3Major, &z3Minor, &z3BuildNumber, &z3RevisionNumber);
- std::cout << "Linked with Microsoft Z3 Optimizer v" << z3Major << "." << z3Minor << " Build " << z3BuildNumber << " Rev " << z3RevisionNumber << "." << std::endl;
+ STORM_PRINT("Linked with Microsoft Z3 Optimizer v" << z3Major << "." << z3Minor << " Build " << z3BuildNumber << " Rev " << z3RevisionNumber << "." << std::endl);
#endif
#ifdef STORM_HAVE_MSAT
char* msatVersion = msat_get_version();
- std::cout << "Linked with " << msatVersion << "." << std::endl;
+ STORM_PRINT("Linked with " << msatVersion << "." << std::endl);
msat_free(msatVersion);
#endif
#ifdef STORM_HAVE_SMTRAT
- std::cout << "Linked with SMT-RAT " << SMTRAT_VERSION << "." << std::endl;
+ STORM_PRINT("Linked with SMT-RAT " << SMTRAT_VERSION << "." << std::endl);
#endif
#ifdef STORM_HAVE_CARL
- std::cout << "Linked with CARL." << std::endl;
// TODO get version string
+ STORM_PRINT("Linked with CARL." << std::endl);
#endif
-
+
#ifdef STORM_HAVE_CUDA
int deviceCount = 0;
cudaError_t error_id = cudaGetDeviceCount(&deviceCount);
-
- if (error_id == cudaSuccess)
- {
- std::cout << "Compiled with CUDA support, ";
+
+ if (error_id == cudaSuccess) {
+ STORM_PRINT("Compiled with CUDA support, ");
// This function call returns 0 if there are no CUDA capable devices.
- if (deviceCount == 0)
- {
- std::cout<< "but there are no available device(s) that support CUDA." << std::endl;
- } else
- {
- std::cout << "detected " << deviceCount << " CUDA Capable device(s):" << std::endl;
+ if (deviceCount == 0){
+ STORM_PRINT("but there are no available device(s) that support CUDA." << std::endl);
+ } else {
+ STORM_PRINT("detected " << deviceCount << " CUDA capable device(s):" << std::endl);
}
-
+
int dev, driverVersion = 0, runtimeVersion = 0;
-
- for (dev = 0; dev < deviceCount; ++dev)
- {
+
+ for (dev = 0; dev < deviceCount; ++dev) {
cudaSetDevice(dev);
cudaDeviceProp deviceProp;
cudaGetDeviceProperties(&deviceProp, dev);
-
- std::cout << "CUDA Device " << dev << ": \"" << deviceProp.name << "\"" << std::endl;
-
+
+ STORM_PRINT("CUDA device " << dev << ": \"" << deviceProp.name << "\"" << std::endl);
+
// Console log
cudaDriverGetVersion(&driverVersion);
cudaRuntimeGetVersion(&runtimeVersion);
- std::cout << " CUDA Driver Version / Runtime Version " << driverVersion / 1000 << "." << (driverVersion % 100) / 10 << " / " << runtimeVersion / 1000 << "." << (runtimeVersion % 100) / 10 << std::endl;
- std::cout << " CUDA Capability Major/Minor version number: " << deviceProp.major<<"."<<deviceProp.minor <<std::endl;
+ STORM_PRINT(" CUDA Driver Version / Runtime Version " << driverVersion / 1000 << "." << (driverVersion % 100) / 10 << " / " << runtimeVersion / 1000 << "." << (runtimeVersion % 100) / 10 << std::endl);
+ STORM_PRINT(" CUDA Capability Major/Minor version number: " << deviceProp.major << "." << deviceProp.minor << std::endl);
}
- std::cout << std::endl;
+ STORM_PRINT(std::endl);
}
else {
- std::cout << "Compiled with CUDA support, but an error occured trying to find CUDA devices." << std::endl;
+ STORM_PRINT("Compiled with CUDA support, but an error occured trying to find CUDA devices." << std::endl);
}
#endif
-
- // "Compute" the command line argument string with which STORM was invoked.
- std::stringstream commandStream;
- for (int i = 1; i < argc; ++i) {
- commandStream << argv[i] << " ";
- }
- std::cout << "Command line arguments: " << commandStream.str() << std::endl;
- std::cout << "Current working directory: " << getCurrentWorkingDirectory() << std::endl << std::endl;
}
-
+
void showTimeAndMemoryStatistics(uint64_t wallclockMilliseconds) {
struct rusage ru;
getrusage(RUSAGE_SELF, &ru);
-
+
std::cout << std::endl << "Performance statistics:" << std::endl;
#ifdef MACOS
// For Mac OS, this is returned in bytes.
@@ -148,7 +151,7 @@ namespace storm {
std::cout << " * wallclock time: " << (wallclockMilliseconds/1000) << "." << std::setw(3) << std::setfill('0') << (wallclockMilliseconds % 1000) << "s" << std::endl;
}
}
-
+
bool parseOptions(const int argc, const char* argv[]) {
try {
storm::settings::mutableManager().setFromCommandLine(argc, argv);
@@ -172,7 +175,7 @@ namespace storm {
}
if (general.isVersionSet()) {
- storm::settings::manager().printVersion();
+ printVersion("storm");
return false;
}
@@ -183,20 +186,20 @@ namespace storm {
storm::utility::setLogLevel(l3pp::LogLevel::DEBUG);
}
if (debug.isTraceSet()) {
- storm::utility::setLogLevel(l3pp::LogLevel::TRACE);
+ storm::utility::setLogLevel(l3pp::LogLevel::TRACE);
}
if (debug.isLogfileSet()) {
storm::utility::initializeFileLogging();
}
return true;
}
-
+
void processOptions() {
STORM_LOG_TRACE("Processing options.");
if (storm::settings::getModule<storm::settings::modules::DebugSettings>().isLogfileSet()) {
storm::utility::initializeFileLogging();
}
-
+
boost::optional<std::set<std::string>> propertyFilter;
std::string propertyFilterString = storm::settings::getModule<storm::settings::modules::IOSettings>().getPropertyFilter();
if (propertyFilterString != "all") {
@@ -242,7 +245,7 @@ namespace storm {
// Get the string that assigns values to the unknown currently undefined constants in the model and formula.
std::string constantDefinitionString = ioSettings.getConstantDefinitionString();
std::map<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions;
-
+
// Then proceed to parsing the properties (if given), since the model we are building may depend on the property.
STORM_LOG_TRACE("Parsing properties.");
if (ioSettings.isPropertySet()) {
@@ -293,19 +296,19 @@ namespace storm {
}
} else if (ioSettings.isExplicitSet()) {
STORM_LOG_THROW(coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Only the sparse engine supports explicit model input.");
-
+
// If the model is given in an explicit format, we parse the properties without allowing expressions
// in formulas.
std::vector<storm::jani::Property> properties;
if (ioSettings.isPropertySet()) {
properties = storm::parsePropertiesForExplicit(ioSettings.getProperty(), propertyFilter);
}
-
+
buildAndCheckExplicitModel<double>(properties, true);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
}
}
-
+
}
}
diff --git a/src/storm/cli/cli.h b/src/storm/cli/cli.h
index f48d53f23..3fd41e914 100644
--- a/src/storm/cli/cli.h
+++ b/src/storm/cli/cli.h
@@ -8,7 +8,9 @@ namespace storm {
std::string getCurrentWorkingDirectory();
- void printHeader(std::string name, const int argc, const char* argv[]);
+ void printHeader(std::string const& name, const int argc, const char* argv[]);
+
+ void printVersion(std::string const& name);
void showTimeAndMemoryStatistics(uint64_t wallclockMilliseconds = 0);
diff --git a/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h b/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h
index e30aade7b..6359d04a6 100644
--- a/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h
+++ b/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h
@@ -1745,7 +1745,7 @@ namespace storm {
return commandSet;
#else
- throw storm::exceptions::NotImplementedException() << "This functionality is unavailable since StoRM has been compiled without support for Z3.";
+ throw storm::exceptions::NotImplementedException() << "This functionality is unavailable since storm has been compiled without support for Z3.";
#endif
}
@@ -1801,7 +1801,7 @@ namespace storm {
std::cout << std::endl << "-------------------------------------------" << std::endl;
#else
- throw storm::exceptions::NotImplementedException() << "This functionality is unavailable since StoRM has been compiled without support for Z3.";
+ throw storm::exceptions::NotImplementedException() << "This functionality is unavailable since storm has been compiled without support for Z3.";
#endif
}
diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp
index efe033d08..624260887 100644
--- a/src/storm/parser/JaniParser.cpp
+++ b/src/storm/parser/JaniParser.cpp
@@ -245,12 +245,12 @@ namespace storm {
}
}
}
- STORM_LOG_THROW(!(accTime && accSteps), storm::exceptions::NotSupportedException, "Storm does not allow to accumulate over both time and steps");
+ STORM_LOG_THROW(!(accTime && accSteps), storm::exceptions::NotSupportedException, "storm does not allow to accumulate over both time and steps");
if (propertyStructure.count("step-instant") > 0) {
storm::expressions::Expression stepInstantExpr = parseExpression(propertyStructure.at("step-instant"), "Step instant in " + context);
- STORM_LOG_THROW(!stepInstantExpr.containsVariables(), storm::exceptions::NotSupportedException, "Storm only allows constant step-instants");
+ STORM_LOG_THROW(!stepInstantExpr.containsVariables(), storm::exceptions::NotSupportedException, "storm only allows constant step-instants");
int64_t stepInstant = stepInstantExpr.evaluateAsInt();
STORM_LOG_THROW(stepInstant >= 0, storm::exceptions::InvalidJaniException, "Only non-negative step-instants are allowed");
if(!accTime && !accSteps) {
@@ -270,7 +270,7 @@ namespace storm {
}
} else if (propertyStructure.count("time-instant") > 0) {
storm::expressions::Expression timeInstantExpr = parseExpression(propertyStructure.at("time-instant"), "time instant in " + context);
- STORM_LOG_THROW(!timeInstantExpr.containsVariables(), storm::exceptions::NotSupportedException, "Storm only allows constant time-instants");
+ STORM_LOG_THROW(!timeInstantExpr.containsVariables(), storm::exceptions::NotSupportedException, "storm only allows constant time-instants");
double timeInstant = timeInstantExpr.evaluateAsDouble();
STORM_LOG_THROW(timeInstant >= 0, storm::exceptions::InvalidJaniException, "Only non-negative time-instants are allowed");
if(!accTime && !accSteps) {
@@ -292,7 +292,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Instant/Cumul. Reward for reward constraints not supported currently.");
}
- //STORM_LOG_THROW(!accTime && !accSteps, storm::exceptions::NotSupportedException, "Storm only allows accumulation if a step- or time-bound is given.");
+ //STORM_LOG_THROW(!accTime && !accSteps, storm::exceptions::NotSupportedException, "storm only allows accumulation if a step- or time-bound is given.");
if (rewExpr.isVariable()) {
std::string rewardName = rewExpr.getVariables().begin()->getName();
@@ -336,9 +336,9 @@ namespace storm {
}
if (propertyStructure.count("step-bounds") > 0) {
storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("step-bounds"));
- STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports step-bounded until with an upper bound");
+ STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "storm only supports step-bounded until with an upper bound");
if(pi.hasLowerBound()) {
- STORM_LOG_THROW(pi.lowerBound.evaluateAsInt() == 0, storm::exceptions::NotSupportedException, "Storm only supports step-bounded until without a (non-trivial) lower-bound");
+ STORM_LOG_THROW(pi.lowerBound.evaluateAsInt() == 0, storm::exceptions::NotSupportedException, "storm only supports step-bounded until without a (non-trivial) lower-bound");
}
int64_t upperBound = pi.upperBound.evaluateAsInt();
if(pi.upperBoundStrict) {
@@ -348,7 +348,7 @@ namespace storm {
return std::make_shared<storm::logic::BoundedUntilFormula const>(args[0], args[1], storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound), storm::logic::TimeBoundType::Steps);
} else if (propertyStructure.count("time-bounds") > 0) {
storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("time-bounds"));
- STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports time-bounded until with an upper bound.");
+ STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "storm only supports time-bounded until with an upper bound.");
double lowerBound = 0.0;
if(pi.hasLowerBound()) {
lowerBound = pi.lowerBound.evaluateAsDouble();
@@ -359,7 +359,7 @@ namespace storm {
return std::make_shared<storm::logic::BoundedUntilFormula const>(args[0], args[1], storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound), storm::logic::TimeBoundType::Time);
} else if (propertyStructure.count("reward-bounds") > 0 ) {
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by Storm");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by storm");
}
if (args[0]->isTrueFormula()) {
return std::make_shared<storm::logic::EventuallyFormula const>(args[1], storm::logic::FormulaContext::Reward);
@@ -372,9 +372,9 @@ namespace storm {
if (propertyStructure.count("step-bounds") > 0) {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Globally and step-bounds are not supported currently");
} else if (propertyStructure.count("time-bounds") > 0) {
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Globally and time bounds are not supported by Storm");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Globally and time bounds are not supported by storm");
} else if (propertyStructure.count("reward-bounds") > 0 ) {
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by Storm");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by storm");
}
return std::make_shared<storm::logic::GloballyFormula const>(args[1]);
diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp
index b5db92f3d..8fefca91c 100644
--- a/src/storm/settings/SettingsManager.cpp
+++ b/src/storm/settings/SettingsManager.cpp
@@ -257,11 +257,6 @@ namespace storm {
STORM_PRINT(std::endl);
}
- void SettingsManager::printVersion() const {
- STORM_PRINT(storm::utility::StormVersion::shortVersionString());
- STORM_PRINT(std::endl);
- }
-
uint_fast64_t SettingsManager::getPrintLengthOfLongestOption() const {
uint_fast64_t length = 0;
for (auto const& moduleName : this->moduleNames) {
diff --git a/src/storm/settings/SettingsManager.h b/src/storm/settings/SettingsManager.h
index 1ae89382e..201e7f896 100644
--- a/src/storm/settings/SettingsManager.h
+++ b/src/storm/settings/SettingsManager.h
@@ -80,11 +80,6 @@ namespace storm {
* @param maxLength The maximal length of an option name (necessary for proper alignment).
*/
void printHelpForModule(std::string const& moduleName, uint_fast64_t maxLength = 30) const;
-
- /*!
- * This function prints the version string to the command line.
- */
- void printVersion() const;
/*!
* Retrieves the only existing instance of a settings manager.
diff --git a/src/storm/settings/modules/JitBuilderSettings.cpp b/src/storm/settings/modules/JitBuilderSettings.cpp
index 2944ccee3..127434055 100644
--- a/src/storm/settings/modules/JitBuilderSettings.cpp
+++ b/src/storm/settings/modules/JitBuilderSettings.cpp
@@ -25,8 +25,8 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, doctorOptionName, false, "Show debugging information on why the jit-based model builder is not working on your system.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, compilerOptionName, false, "The compiler in the jit-based model builder.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the executable. Defaults to c++.").setDefaultValueString("c++").build()).build());
- this->addOption(storm::settings::OptionBuilder(moduleName, stormIncludeDirectoryOptionName, false, "The include directory of Storm.")
- .addArgument(storm::settings::ArgumentBuilder::createStringArgument("dir", "The directory that contains the headers of Storm.").build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, stormIncludeDirectoryOptionName, false, "The include directory of storm.")
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("dir", "The directory that contains the headers of storm.").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, boostIncludeDirectoryOptionName, false, "The include directory of boost.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("dir", "The directory containing the boost headers version >= 1.61.").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, carlIncludeDirectoryOptionName, false, "The include directory of carl.")
diff --git a/src/storm/solver/GlpkLpSolver.h b/src/storm/solver/GlpkLpSolver.h
index 35f94953a..63be0ede7 100644
--- a/src/storm/solver/GlpkLpSolver.h
+++ b/src/storm/solver/GlpkLpSolver.h
@@ -134,103 +134,103 @@ namespace storm {
class GlpkLpSolver : public LpSolver {
public:
GlpkLpSolver(std::string const& name, OptimizationDirection const& modelSense) {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
GlpkLpSolver(std::string const& name) : LpSolver(MINIMIZE) {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
GlpkLpSolver(OptimizationDirection const& modelSense) : LpSolver(modelSense) {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
GlpkLpSolver() : LpSolver(MINIMIZE) {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual ~GlpkLpSolver() {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual storm::expressions::Variable addBoundedContinuousVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual storm::expressions::Variable addLowerBoundedContinuousVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual storm::expressions::Variable addUpperBoundedContinuousVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual storm::expressions::Variable addUnboundedContinuousVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual storm::expressions::Variable addBoundedIntegerVariable(std::string const& name, double lowerBound, double upperBound, double objectiveFunctionCoefficient = 0) override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual storm::expressions::Variable addLowerBoundedIntegerVariable(std::string const& name, double lowerBound, double objectiveFunctionCoefficient = 0) override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual storm::expressions::Variable addUpperBoundedIntegerVariable(std::string const& name, double upperBound, double objectiveFunctionCoefficient = 0) override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual storm::expressions::Variable addUnboundedIntegerVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual storm::expressions::Variable addBinaryVariable(std::string const& name, double objectiveFunctionCoefficient = 0) override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual void update() const override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual void addConstraint(std::string const& name, storm::expressions::Expression const& constraint) override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual void optimize() const override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual bool isInfeasible() const override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual bool isUnbounded() const override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual bool isOptimal() const override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual double getContinuousValue(storm::expressions::Variable const& variable) const override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& variable) const override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual bool getBinaryValue(storm::expressions::Variable const& variable) const override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual double getObjectiveValue() const override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
virtual void writeModelToFile(std::string const& filename) const override {
- throw storm::exceptions::NotImplementedException() << "This version of StoRM was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for glpk. Yet, a method was called that requires this support. Please choose a version of support with glpk support.";
}
};
#endif
diff --git a/src/storm/solver/GurobiLpSolver.cpp b/src/storm/solver/GurobiLpSolver.cpp
index 2754cc292..d624f2cfb 100644
--- a/src/storm/solver/GurobiLpSolver.cpp
+++ b/src/storm/solver/GurobiLpSolver.cpp
@@ -357,19 +357,19 @@ namespace storm {
}
#else
GurobiLpSolver::GurobiLpSolver(std::string const&, OptimizationDirection const&) {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
GurobiLpSolver::GurobiLpSolver(std::string const&) {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
GurobiLpSolver::GurobiLpSolver(OptimizationDirection const&) {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
GurobiLpSolver::GurobiLpSolver() {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
GurobiLpSolver::~GurobiLpSolver() {
@@ -377,86 +377,86 @@ namespace storm {
}
storm::expressions::Variable GurobiLpSolver::addBoundedContinuousVariable(std::string const&, double, double, double) {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
storm::expressions::Variable GurobiLpSolver::addLowerBoundedContinuousVariable(std::string const&, double, double ) {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; }
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support."; }
storm::expressions::Variable GurobiLpSolver::addUpperBoundedContinuousVariable(std::string const&, double, double ) {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
storm::expressions::Variable GurobiLpSolver::addUnboundedContinuousVariable(std::string const&, double ) {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
storm::expressions::Variable GurobiLpSolver::addBoundedIntegerVariable(std::string const&, double, double, double) {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
storm::expressions::Variable GurobiLpSolver::addLowerBoundedIntegerVariable(std::string const&, double, double) {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
storm::expressions::Variable GurobiLpSolver::addUpperBoundedIntegerVariable(std::string const&, double, double) {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
storm::expressions::Variable GurobiLpSolver::addUnboundedIntegerVariable(std::string const&, double) {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
storm::expressions::Variable GurobiLpSolver::addBinaryVariable(std::string const&, double) {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
void GurobiLpSolver::update() const {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
void GurobiLpSolver::addConstraint(std::string const&, storm::expressions::Expression const&) {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
void GurobiLpSolver::optimize() const {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
bool GurobiLpSolver::isInfeasible() const {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
bool GurobiLpSolver::isUnbounded() const {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
bool GurobiLpSolver::isOptimal() const {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
double GurobiLpSolver::getContinuousValue(storm::expressions::Variable const&) const {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
int_fast64_t GurobiLpSolver::getIntegerValue(storm::expressions::Variable const&) const {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
bool GurobiLpSolver::getBinaryValue(storm::expressions::Variable const&) const {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
double GurobiLpSolver::getObjectiveValue() const {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
void GurobiLpSolver::writeModelToFile(std::string const&) const {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
void GurobiLpSolver::toggleOutput(bool) const {
- throw storm::exceptions::NotImplementedException() << "This version of Storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
+ throw storm::exceptions::NotImplementedException() << "This version of storm was compiled without support for Gurobi. Yet, a method was called that requires this support. Please choose a version of support with Gurobi support.";
}
#endif
diff --git a/src/storm/solver/MathsatSmtSolver.cpp b/src/storm/solver/MathsatSmtSolver.cpp
index ef362e12f..d7501ad53 100644
--- a/src/storm/solver/MathsatSmtSolver.cpp
+++ b/src/storm/solver/MathsatSmtSolver.cpp
@@ -107,7 +107,7 @@ namespace storm {
#ifdef STORM_HAVE_MSAT
msat_push_backtrack_point(env);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
@@ -115,7 +115,7 @@ namespace storm {
#ifdef STORM_HAVE_MSAT
msat_pop_backtrack_point(env);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
@@ -123,7 +123,7 @@ namespace storm {
#ifdef STORM_HAVE_MSAT
SmtSolver::pop(n);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
@@ -132,7 +132,7 @@ namespace storm {
#ifdef STORM_HAVE_MSAT
msat_reset_env(env);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
@@ -141,7 +141,7 @@ namespace storm {
#ifdef STORM_HAVE_MSAT
msat_assert_formula(env, expressionAdapter->translateExpression(e));
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
@@ -162,7 +162,7 @@ namespace storm {
}
return this->lastResult;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
@@ -190,7 +190,7 @@ namespace storm {
}
return this->lastResult;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
@@ -219,7 +219,7 @@ namespace storm {
}
return this->lastResult;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
#endif
@@ -230,7 +230,7 @@ namespace storm {
STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Unable to create model for formula that was not determined to be satisfiable.");
return this->convertMathsatModelToValuation();
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
@@ -239,7 +239,7 @@ namespace storm {
STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Unable to create model for formula that was not determined to be satisfiable.");
return std::shared_ptr<SmtSolver::ModelReference>(new MathsatModelReference(this->getManager(), env, *expressionAdapter));
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
@@ -279,7 +279,7 @@ namespace storm {
this->allSat(important, [&valuations](storm::expressions::SimpleValuation const& valuation) -> bool { valuations.push_back(valuation); return true; });
return valuations;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
@@ -379,7 +379,7 @@ namespace storm {
this->pop();
return static_cast<uint_fast64_t>(numberOfModels);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
@@ -405,7 +405,7 @@ namespace storm {
this->pop();
return static_cast<uint_fast64_t>(numberOfModels);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
@@ -426,7 +426,7 @@ namespace storm {
return unsatAssumptions;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
@@ -440,7 +440,7 @@ namespace storm {
}
msat_set_itp_group(env, groupIter->second);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
@@ -462,7 +462,7 @@ namespace storm {
return this->expressionAdapter->translateExpression(interpolant);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without MathSAT support.");
#endif
}
}
diff --git a/src/storm/solver/NativeLinearEquationSolver.h b/src/storm/solver/NativeLinearEquationSolver.h
index aeb0cc807..2a978cdbc 100644
--- a/src/storm/solver/NativeLinearEquationSolver.h
+++ b/src/storm/solver/NativeLinearEquationSolver.h
@@ -38,7 +38,7 @@ namespace storm {
};
/*!
- * A class that uses Storm's native matrix operations to implement the LinearEquationSolver interface.
+ * A class that uses storm's native matrix operations to implement the LinearEquationSolver interface.
*/
template<typename ValueType>
class NativeLinearEquationSolver : public LinearEquationSolver<ValueType> {
diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp
index c29b0452c..cb1cbd5f0 100644
--- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp
+++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.cpp
@@ -112,8 +112,8 @@ namespace storm {
STORM_LOG_WARN("Iterative solver did not converged after " << globalIterations << " iterations.");
}
#else
- STORM_LOG_ERROR("The useGpu Flag of a SCC was set, but this version of StoRM does not support CUDA acceleration. Internal Error!");
- throw storm::exceptions::InvalidStateException() << "The useGpu Flag of a SCC was set, but this version of StoRM does not support CUDA acceleration. Internal Error!";
+ STORM_LOG_ERROR("The useGpu Flag of a SCC was set, but this version of storm does not support CUDA acceleration. Internal Error!");
+ throw storm::exceptions::InvalidStateException() << "The useGpu Flag of a SCC was set, but this version of storm does not support CUDA acceleration. Internal Error!";
#endif
} else {
storm::storage::BitVector fullSystem(this->A.getRowGroupCount(), true);
@@ -213,8 +213,8 @@ namespace storm {
}
globalIterations += localIterations;
#else
- STORM_LOG_ERROR("The useGpu Flag of a SCC was set, but this version of StoRM does not support CUDA acceleration. Internal Error!");
- throw storm::exceptions::InvalidStateException() << "The useGpu Flag of a SCC was set, but this version of StoRM does not support CUDA acceleration. Internal Error!";
+ STORM_LOG_ERROR("The useGpu Flag of a SCC was set, but this version of storm does not support CUDA acceleration. Internal Error!");
+ throw storm::exceptions::InvalidStateException() << "The useGpu Flag of a SCC was set, but this version of storm does not support CUDA acceleration. Internal Error!";
#endif
} else {
//std::cout << "WARNING: Using CPU based TopoSolver! (double)" << std::endl;
diff --git a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h
index e706d48cd..c8af93f13 100644
--- a/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h
+++ b/src/storm/solver/TopologicalMinMaxLinearEquationSolver.h
@@ -73,7 +73,7 @@ namespace storm {
#ifdef STORM_HAVE_CUDA
return basicValueIteration_mvReduce_uint64_double_minimize(maxIterationCount, precision, relativePrecisionCheck, matrixRowIndices, columnIndicesAndValues, x, b, nondeterministicChoiceIndices, iterationCount);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without CUDA support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without CUDA support.");
#endif
}
template <>
@@ -92,7 +92,7 @@ namespace storm {
#ifdef STORM_HAVE_CUDA
return basicValueIteration_mvReduce_uint64_float_minimize(maxIterationCount, precision, relativePrecisionCheck, matrixRowIndices, columnIndicesAndValues, x, b, nondeterministicChoiceIndices, iterationCount);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without CUDA support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without CUDA support.");
#endif
}
@@ -116,7 +116,7 @@ namespace storm {
#ifdef STORM_HAVE_CUDA
return basicValueIteration_mvReduce_uint64_double_maximize(maxIterationCount, precision, relativePrecisionCheck, matrixRowIndices, columnIndicesAndValues, x, b, nondeterministicChoiceIndices, iterationCount);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without CUDA support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without CUDA support.");
#endif
}
template <>
@@ -135,7 +135,7 @@ namespace storm {
#ifdef STORM_HAVE_CUDA
return basicValueIteration_mvReduce_uint64_float_maximize(maxIterationCount, precision, relativePrecisionCheck, matrixRowIndices, columnIndicesAndValues, x, b, nondeterministicChoiceIndices, iterationCount);
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without CUDA support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without CUDA support.");
#endif
}
diff --git a/src/storm/solver/Z3SmtSolver.cpp b/src/storm/solver/Z3SmtSolver.cpp
index e033504ef..cb291bcb9 100644
--- a/src/storm/solver/Z3SmtSolver.cpp
+++ b/src/storm/solver/Z3SmtSolver.cpp
@@ -19,7 +19,7 @@ namespace storm {
z3::expr z3ExprValuation = model.eval(z3Expr, true);
return this->expressionAdapter.translateExpression(z3ExprValuation).isTrue();
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -30,7 +30,7 @@ namespace storm {
z3::expr z3ExprValuation = model.eval(z3Expr, true);
return this->expressionAdapter.translateExpression(z3ExprValuation).evaluateAsInt();
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -41,7 +41,7 @@ namespace storm {
z3::expr z3ExprValuation = model.eval(z3Expr, true);
return this->expressionAdapter.translateExpression(z3ExprValuation).evaluateAsDouble();
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -68,7 +68,7 @@ namespace storm {
#ifdef STORM_HAVE_Z3
this->solver->push();
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -77,7 +77,7 @@ namespace storm {
#ifdef STORM_HAVE_Z3
this->solver->pop();
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -86,7 +86,7 @@ namespace storm {
#ifdef STORM_HAVE_Z3
this->solver->pop(static_cast<unsigned int>(n));
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -95,7 +95,7 @@ namespace storm {
#ifdef STORM_HAVE_Z3
this->solver->reset();
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -104,7 +104,7 @@ namespace storm {
#ifdef STORM_HAVE_Z3
this->solver->add(expressionAdapter->translateExpression(assertion));
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -125,7 +125,7 @@ namespace storm {
}
return this->lastResult;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -152,7 +152,7 @@ namespace storm {
}
return this->lastResult;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -180,7 +180,7 @@ namespace storm {
}
return this->lastResult;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
#endif
@@ -190,7 +190,7 @@ namespace storm {
STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Unable to create model for formula that was not determined to be satisfiable.");
return this->convertZ3ModelToValuation(this->solver->get_model());
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -199,7 +199,7 @@ namespace storm {
STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException, "Unable to create model for formula that was not determined to be satisfiable.");
return std::shared_ptr<SmtSolver::ModelReference>(new Z3ModelReference(this->getManager(), this->solver->get_model(), *this->expressionAdapter));
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -234,7 +234,7 @@ namespace storm {
this->allSat(important, static_cast<std::function<bool(storm::expressions::SimpleValuation&)>>([&valuations](storm::expressions::SimpleValuation const& valuation) -> bool { valuations.push_back(valuation); return true; }));
return valuations;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -276,7 +276,7 @@ namespace storm {
this->pop();
return numberOfModels;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -317,7 +317,7 @@ namespace storm {
this->pop();
return numberOfModels;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -335,7 +335,7 @@ namespace storm {
return unsatAssumptions;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -346,7 +346,7 @@ namespace storm {
solver->set(paramObject);
return true;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
@@ -357,7 +357,7 @@ namespace storm {
solver->set(paramObject);
return true;
#else
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support.");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm is compiled without Z3 support.");
#endif
}
diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp
index ba6a54f8a..834ce8623 100644
--- a/src/storm/storage/jani/JSONExporter.cpp
+++ b/src/storm/storage/jani/JSONExporter.cpp
@@ -182,7 +182,7 @@ namespace storm {
}
boost::any FormulaToJaniJson::visit(storm::logic::CumulativeRewardFormula const&, boost::any const&) const {
- STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm currently does not support translating cummulative reward formulae");
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "storm currently does not support translating cummulative reward formulae");
}
boost::any FormulaToJaniJson::visit(storm::logic::EventuallyFormula const& f, boost::any const& data) const {
diff --git a/src/storm/storm.cpp b/src/storm/storm.cpp
index 20126f488..73c5a8a15 100644
--- a/src/storm/storm.cpp
+++ b/src/storm/storm.cpp
@@ -17,8 +17,8 @@ int main(const int argc, const char** argv) {
try {
storm::utility::Stopwatch totalTimer(true);
storm::utility::setUp();
- storm::cli::printHeader("Storm", argc, argv);
- storm::settings::initializeAll("Storm", "storm");
+ storm::cli::printHeader("storm", argc, argv);
+ storm::settings::initializeAll("storm", "storm");
bool optionsCorrect = storm::cli::parseOptions(argc, argv);
if (!optionsCorrect) {
return -1;
@@ -36,10 +36,10 @@ int main(const int argc, const char** argv) {
}
return 0;
} catch (storm::exceptions::BaseException const& exception) {
- STORM_LOG_ERROR("An exception caused Storm to terminate. The message of the exception is: " << exception.what());
+ STORM_LOG_ERROR("An exception caused storm to terminate. The message of the exception is: " << exception.what());
return 1;
} catch (std::exception const& exception) {
- STORM_LOG_ERROR("An unexpected exception occurred and caused Storm to terminate. The message of this exception is: " << exception.what());
+ STORM_LOG_ERROR("An unexpected exception occurred and caused storm to terminate. The message of this exception is: " << exception.what());
return 2;
}
}
diff --git a/src/storm/utility/ExplicitExporter.cpp b/src/storm/utility/ExplicitExporter.cpp
index 33e9bf3b3..1f40ab538 100644
--- a/src/storm/utility/ExplicitExporter.cpp
+++ b/src/storm/utility/ExplicitExporter.cpp
@@ -31,7 +31,7 @@ namespace storm {
exitRates = sparseModel->template as<storm::models::sparse::MarkovAutomaton<ValueType>>()->getExitRates();
}
- os << "// Exported by Storm" << std::endl;
+ os << "// Exported by storm" << std::endl;
os << "// Original model type: " << sparseModel->getType() << std::endl;
os << "@type: mdp" << std::endl;
os << "@parameters" << std::endl;
diff --git a/src/storm/utility/storm-version.h b/src/storm/utility/storm-version.h
index 12bad5c21..2cd72c00b 100644
--- a/src/storm/utility/storm-version.h
+++ b/src/storm/utility/storm-version.h
@@ -41,13 +41,13 @@ namespace storm {
static std::string shortVersionString() {
std::stringstream sstream;
- sstream << "Storm " << versionMajor << "." << versionMinor << "." << versionPatch;
+ sstream << versionMajor << "." << versionMinor << "." << versionPatch;
return sstream.str();
}
static std::string longVersionString() {
std::stringstream sstream;
- sstream << "version: " << versionMajor << "." << versionMinor << "." << versionPatch;
+ sstream << "Version " << versionMajor << "." << versionMinor << "." << versionPatch;
if (commitsAhead && commitsAhead.get() > 0) {
sstream << " (+" << commitsAhead.get() << " commits)";
}
@@ -57,7 +57,6 @@ namespace storm {
if (dirty && dirty.get() == 1) {
sstream << " (dirty)";
}
- sstream << "." << std::endl;
return sstream.str();
}
diff --git a/src/test/storm-test.cpp b/src/test/storm-test.cpp
index b63398a9b..a88084304 100644
--- a/src/test/storm-test.cpp
+++ b/src/test/storm-test.cpp
@@ -2,7 +2,7 @@
#include "storm/settings/SettingsManager.h"
int main(int argc, char **argv) {
- storm::settings::initializeAll("StoRM (Functional) Testing Suite", "test");
+ storm::settings::initializeAll("storm (Functional) Testing Suite", "test");
::testing::InitGoogleTest(&argc, argv);
return RUN_ALL_TESTS();
}
From 8b06e4fa6ed04d87fe32538a291837af044095b4 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 7 Feb 2017 18:58:35 +0100
Subject: [PATCH 18/24] added missing IOSettings module to storm-dft-cli
---
src/storm-dft-cli/storm-dyftee.cpp | 1 +
1 file changed, 1 insertion(+)
diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp
index 5f4cdaee4..c018108ec 100644
--- a/src/storm-dft-cli/storm-dyftee.cpp
+++ b/src/storm-dft-cli/storm-dyftee.cpp
@@ -87,6 +87,7 @@ void initializeSettings() {
storm::settings::addModule<storm::settings::modules::DFTSettings>();
storm::settings::addModule<storm::settings::modules::CoreSettings>();
storm::settings::addModule<storm::settings::modules::DebugSettings>();
+ storm::settings::addModule<storm::settings::modules::IOSettings>();
//storm::settings::addModule<storm::settings::modules::CounterexampleGeneratorSettings>();
//storm::settings::addModule<storm::settings::modules::CuddSettings>();
//storm::settings::addModule<storm::settings::modules::SylvanSettings>();
From c9f1b3217d81241e48e117dfc72b6817151a6749 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Wed, 8 Feb 2017 14:36:57 +0100
Subject: [PATCH 19/24] Jani parsing of ITE now gets local variables
---
src/storm/parser/JaniParser.cpp | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp
index 624260887..c47d59940 100644
--- a/src/storm/parser/JaniParser.cpp
+++ b/src/storm/parser/JaniParser.cpp
@@ -734,9 +734,9 @@ namespace storm {
STORM_LOG_THROW(expressionStructure.count("if") == 1, storm::exceptions::InvalidJaniException, "If operator required");
STORM_LOG_THROW(expressionStructure.count("else") == 1, storm::exceptions::InvalidJaniException, "Else operator required");
STORM_LOG_THROW(expressionStructure.count("then") == 1, storm::exceptions::InvalidJaniException, "If operator required");
- arguments.push_back(parseExpression(expressionStructure.at("if"), "if-formula in " + scopeDescription));
- arguments.push_back(parseExpression(expressionStructure.at("then"), "then-formula in " + scopeDescription));
- arguments.push_back(parseExpression(expressionStructure.at("else"), "else-formula in " + scopeDescription));
+ arguments.push_back(parseExpression(expressionStructure.at("if"), "if-formula in " + scopeDescription, localVars, returnNoneInitializedOnUnknownOperator));
+ arguments.push_back(parseExpression(expressionStructure.at("then"), "then-formula in " + scopeDescription, localVars, returnNoneInitializedOnUnknownOperator));
+ arguments.push_back(parseExpression(expressionStructure.at("else"), "else-formula in " + scopeDescription, localVars, returnNoneInitializedOnUnknownOperator));
ensureNumberOfArguments(3, arguments.size(), opstring, scopeDescription);
assert(arguments.size() == 3);
ensureBooleanType(arguments[0], opstring, 0, scopeDescription);
From 267eeca2e198be51e1bbdda189da29b76f7faee3 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Wed, 8 Feb 2017 15:15:22 +0100
Subject: [PATCH 20/24] Jani: better error message in ordered assignments
---
src/storm/storage/jani/OrderedAssignments.cpp | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/storm/storage/jani/OrderedAssignments.cpp b/src/storm/storage/jani/OrderedAssignments.cpp
index 9f8b166df..56657e2ce 100644
--- a/src/storm/storage/jani/OrderedAssignments.cpp
+++ b/src/storm/storage/jani/OrderedAssignments.cpp
@@ -26,7 +26,7 @@ namespace storm {
auto it = lowerBound(assignment, allAssignments);
if (it != allAssignments.end()) {
- STORM_LOG_THROW(assignment.getExpressionVariable() != (*it)->getExpressionVariable(), storm::exceptions::InvalidArgumentException, "Cannot add assignment as an assignment to this variable already exists.");
+ STORM_LOG_THROW(assignment.getExpressionVariable() != (*it)->getExpressionVariable(), storm::exceptions::InvalidArgumentException, "Cannot add assignment ('" << assignment.getAssignedExpression() << "') as an assignment ('" << (*it)->getAssignedExpression() << "') to variable '" << (*it)->getVariable().getName() << "' already exists.");
}
// Finally, insert the new element in the correct vectors.
From d3774f9958350a8747303b143919e9ea6818da74 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Wed, 8 Feb 2017 18:11:40 +0100
Subject: [PATCH 21/24] JANI: parse assignment index/level
---
src/storm/parser/JaniParser.cpp | 7 ++++++-
1 file changed, 6 insertions(+), 1 deletion(-)
diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp
index c47d59940..c8f0c15e8 100644
--- a/src/storm/parser/JaniParser.cpp
+++ b/src/storm/parser/JaniParser.cpp
@@ -1074,7 +1074,12 @@ namespace storm {
STORM_LOG_THROW(assignmentEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "' must have one value field");
storm::expressions::Expression assignmentExpr = parseExpression(assignmentEntry.at("value"), "assignment in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'", localVars);
// TODO check types
- assignments.emplace_back(lhs, assignmentExpr);
+ // index
+ uint64_t assignmentIndex = 0; // default.
+ if(assignmentEntry.count("index") > 0) {
+ assignmentIndex = getUnsignedInt(assignmentEntry.at("index"), "assignment index in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'");
+ }
+ assignments.emplace_back(lhs, assignmentExpr, assignmentIndex);
}
}
destinationLocationsAndProbabilities.emplace_back(locIds.at(targetLoc), probExpr);
From a21a0556ed3b245803cc3d8b27d21c42532cd661 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Wed, 8 Feb 2017 18:11:58 +0100
Subject: [PATCH 22/24] suppress warning during compilation
---
.../storage/expressions/UnaryNumericalFunctionExpression.cpp | 1 +
1 file changed, 1 insertion(+)
diff --git a/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp b/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp
index 9fdaa4d49..2382e1399 100644
--- a/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp
+++ b/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp
@@ -44,6 +44,7 @@ namespace storm {
case OperatorType::Ceil: return static_cast<int_fast64_t>(std::ceil(result)); break;
default:
STORM_LOG_ASSERT(false, "All other operator types should have been handled before.");
+ return 0;// Warning suppression.
}
}
}
From b83f57ebf3acd60e282e8223bd697d576423f2b0 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Wed, 8 Feb 2017 18:12:40 +0100
Subject: [PATCH 23/24] JANI assignment levels: we support index/levels other
than zero (although most builders wont support them)
---
src/storm/storage/jani/Assignment.cpp | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/storm/storage/jani/Assignment.cpp b/src/storm/storage/jani/Assignment.cpp
index ba0b41c2a..203d92933 100644
--- a/src/storm/storage/jani/Assignment.cpp
+++ b/src/storm/storage/jani/Assignment.cpp
@@ -9,7 +9,7 @@ namespace storm {
namespace jani {
Assignment::Assignment(storm::jani::Variable const& variable, storm::expressions::Expression const& expression, uint64_t level) : variable(variable), expression(expression), level(level) {
- STORM_LOG_THROW(level == 0, storm::exceptions::NotImplementedException, "Assignment levels other than 0 are currently not supported.");
+
}
bool Assignment::operator==(Assignment const& other) const {
From 0f8e00a80ed74522dd57fb622acebea081890c87 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@gmail.com>
Date: Wed, 8 Feb 2017 22:18:12 +0100
Subject: [PATCH 24/24] action reusal in syncvectors is not invalid jani, but
not properly supported. Changed error message accordingly, allows for changes
in model generators
---
src/storm/builder/DdJaniModelBuilder.cpp | 3 ++-
.../jit/ExplicitJitJaniModelBuilder.cpp | 3 ++-
.../generator/JaniNextStateGenerator.cpp | 4 +++-
src/storm/storage/jani/Model.cpp | 9 +++++++-
src/storm/storage/jani/Model.h | 6 +++++
.../storage/jani/ParallelComposition.cpp | 22 +++++++++++++++----
src/storm/storage/jani/ParallelComposition.h | 3 ++-
7 files changed, 41 insertions(+), 9 deletions(-)
diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp
index 33ee40758..2c308559c 100644
--- a/src/storm/builder/DdJaniModelBuilder.cpp
+++ b/src/storm/builder/DdJaniModelBuilder.cpp
@@ -1814,7 +1814,8 @@ namespace storm {
}
STORM_LOG_THROW(!model.usesAssignmentLevels(), storm::exceptions::InvalidSettingsException, "The symbolic JANI model builder currently does not support assignment levels.");
-
+ STORM_LOG_THROW(!model.reusesActionsInComposition(), storm::exceptions::InvalidSettingsException, "The symbolic JANI model builder currently does not support reusing actions in parallel composition");
+
storm::jani::Model preparedModel = model;
// Lift the transient edge destinations. We can do so, as we know that there are no assignment levels (because that's not supported anyway).
diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
index ce2bd80c1..15805419b 100644
--- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
+++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
@@ -131,7 +131,8 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The input model contains undefined constants that influence the graph structure of the underlying model, which is not allowed.");
}
#endif
-
+ STORM_LOG_THROW(!model.reusesActionsInComposition(), storm::exceptions::InvalidArgumentException, "The jit JANI model builder currently does not support reusing actions in parallel composition");
+
// Comment this in to print the JANI model for debugging purposes.
// this->model.makeStandardJaniCompliant();
// storm::jani::JsonExporter::toStream(this->model, std::vector<std::shared_ptr<storm::logic::Formula const>>(), std::cout, false);
diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp
index b5a3d420b..d53974178 100644
--- a/src/storm/generator/JaniNextStateGenerator.cpp
+++ b/src/storm/generator/JaniNextStateGenerator.cpp
@@ -28,7 +28,9 @@ namespace storm {
STORM_LOG_THROW(!model.hasNonGlobalTransientVariable(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support automata-local transient variables.");
STORM_LOG_THROW(!model.usesAssignmentLevels(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support assignment levels.");
STORM_LOG_THROW(!this->options.isBuildChoiceLabelsSet(), storm::exceptions::InvalidSettingsException, "JANI next-state generator cannot generate choice labels.");
-
+ STORM_LOG_THROW(!model.reusesActionsInComposition(), storm::exceptions::InvalidArgumentException, "The jit JANI model builder currently does not support reusing actions in parallel composition");
+
+
// Lift the transient edge destinations. We can do so, as we know that there are no assignment levels (because that's not supported anyway).
if (this->model.hasTransientEdgeDestinationAssignments()) {
this->model.liftTransientEdgeDestinationAssignments();
diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp
index 193e7388d..083b8f7fb 100644
--- a/src/storm/storage/jani/Model.cpp
+++ b/src/storm/storage/jani/Model.cpp
@@ -1132,7 +1132,14 @@ namespace storm {
return result;
}
-
+
+ bool Model::reusesActionsInComposition() const {
+ if(composition->isParallelComposition()) {
+ return composition->asParallelComposition().areActionsReused();
+ }
+ return false;
+ }
+
Model Model::createModelFromAutomaton(Automaton const& automaton) const {
// Copy the full model
Model newModel(*this);
diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h
index dffefef76..e942743bd 100644
--- a/src/storm/storage/jani/Model.h
+++ b/src/storm/storage/jani/Model.h
@@ -429,6 +429,12 @@ namespace storm {
bool isLinear() const;
void makeStandardJaniCompliant();
+
+ /*!
+ * Checks whether in the composition, actions are reused: That is, if the model is put in parallel composition and the same action potentially leads to multiple edges from the same state.
+ * @return
+ */
+ bool reusesActionsInComposition() const;
/// The name of the silent action.
static const std::string SILENT_ACTION_NAME;
diff --git a/src/storm/storage/jani/ParallelComposition.cpp b/src/storm/storage/jani/ParallelComposition.cpp
index d08ddaab4..1eaa0ff08 100644
--- a/src/storm/storage/jani/ParallelComposition.cpp
+++ b/src/storm/storage/jani/ParallelComposition.cpp
@@ -188,18 +188,32 @@ namespace storm {
std::size_t ParallelComposition::getNumberOfSynchronizationVectors() const {
return synchronizationVectors.size();
}
-
- void ParallelComposition::checkSynchronizationVectors() const {
+
+ bool ParallelComposition::areActionsReused() const {
for (uint_fast64_t inputIndex = 0; inputIndex < subcompositions.size(); ++ inputIndex) {
std::set<std::string> actions;
for (auto const& vector : synchronizationVectors) {
- STORM_LOG_THROW(vector.size() == this->subcompositions.size(), storm::exceptions::WrongFormatException, "Synchronization vectors must match parallel composition size.");
std::string const& action = vector.getInput(inputIndex);
if (action != SynchronizationVector::NO_ACTION_INPUT) {
- STORM_LOG_THROW(actions.find(action) == actions.end(), storm::exceptions::WrongFormatException, "Cannot use the same action ('" << action << "') multiple times as input for index " << inputIndex << " in synchronization vectors.");
+ return true;
actions.insert(action);
}
}
+ // And check recursively, in case we have nested parallel composition
+ if (subcompositions.at(inputIndex)->isParallelComposition()) {
+ if(subcompositions.at(inputIndex)->asParallelComposition().areActionsReused()) {
+ return true;
+ }
+ }
+ }
+ return false;
+ }
+
+ void ParallelComposition::checkSynchronizationVectors() const {
+ for (uint_fast64_t inputIndex = 0; inputIndex < subcompositions.size(); ++ inputIndex) {
+ for (auto const& vector : synchronizationVectors) {
+ STORM_LOG_THROW(vector.size() == this->subcompositions.size(), storm::exceptions::WrongFormatException, "Synchronization vectors must match parallel composition size.");
+ }
}
for (auto const& vector : synchronizationVectors) {
diff --git a/src/storm/storage/jani/ParallelComposition.h b/src/storm/storage/jani/ParallelComposition.h
index 3dbad1aa6..c3d41717c 100644
--- a/src/storm/storage/jani/ParallelComposition.h
+++ b/src/storm/storage/jani/ParallelComposition.h
@@ -124,7 +124,8 @@ namespace storm {
virtual boost::any accept(CompositionVisitor& visitor, boost::any const& data) const override;
virtual void write(std::ostream& stream) const override;
-
+
+ bool areActionsReused() const;
private:
/*!
* Checks the synchronization vectors for validity.