diff --git a/src/adapters/CarlAdapter.h b/src/adapters/CarlAdapter.h
index 1fb6ca9c0..abfedf126 100644
--- a/src/adapters/CarlAdapter.h
+++ b/src/adapters/CarlAdapter.h
@@ -1,12 +1,10 @@
-/**
- * @file: extendedCarl.h
- * @author: Sebastian Junges
- *
- * @since March 18, 2014
- */
+#ifndef STORM_ADAPTERS_CARLADAPTER_H_
+#define STORM_ADAPTERS_CARLADAPTER_H_
-#ifndef STORM_ADAPTERS_EXTENDEDCARL_H_
-#define STORM_ADAPTERS_EXTENDEDCARL_H_
+// Include config to know whether CARL is available or not.
+#include "storm-config.h"
+
+#ifdef STORM_HAVE_CARL
#include <cln/cln.h>
#include <carl/core/MultivariatePolynomial.h>
@@ -15,29 +13,35 @@
#include <carl/core/Constraint.h>
#include <carl/core/FactorizedPolynomial.h>
-namespace carl
-{
+namespace carl {
+ // Define hash values for all polynomials and rational function.
template<typename C, typename O, typename P>
- inline size_t hash_value(carl::MultivariatePolynomial<C,O,P> const& p)
- {
+ inline size_t hash_value(carl::MultivariatePolynomial<C,O,P> const& p) {
std::hash<carl::MultivariatePolynomial<C,O,P>> h;
return h(p);
}
template<typename Pol>
- inline size_t hash_value(carl::RationalFunction<Pol> const& f)
- {
- std::hash<Pol> h;
- return h(f.nominator()) ^ h(f.denominator());
- }
-
- template<typename Pol>
- inline size_t hash_value(carl::FactorizedPolynomial<Pol> const& p)
- {
+ inline size_t hash_value(carl::FactorizedPolynomial<Pol> const& p) {
std::hash<FactorizedPolynomial<Pol>> h;
return h(p);
}
+
+ template<typename Pol>
+ inline size_t hash_value(carl::RationalFunction<Pol> const& f) {
+ std::hash<Pol> h;
+ return h(f.nominator()) ^ h(f.denominator());
+ }
+}
+
+namespace storm {
+ typedef carl::Variable Variable;
+ typedef carl::MultivariatePolynomial<cln::cl_RA> RawPolynomial;
+ typedef carl::FactorizedPolynomial<RawPolynomial> Polynomial;
+ typedef carl::CompareRelation CompareRelation;
+ typedef carl::RationalFunction<Polynomial> RationalFunction;
}
+#endif
-#endif
\ No newline at end of file
+#endif /* STORM_ADAPTERS_CARLADAPTER_H_ */
\ No newline at end of file
diff --git a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp
index 1d3056426..57eefb270 100644
--- a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp
+++ b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp
@@ -1,7 +1,6 @@
#include "src/modelchecker/propositional/SparsePropositionalModelChecker.h"
-#include "storm-config.h"
-#include "src/storage/parameters.h"
+#include "src/adapters/CarlAdapter.h"
#include "src/models/Dtmc.h"
#include "src/models/Mdp.h"
@@ -54,7 +53,7 @@ namespace storm {
template storm::models::Mdp<double> const& SparsePropositionalModelChecker<double>::getModelAs() const;
template class SparsePropositionalModelChecker<double>;
-#ifdef PARAMETRIC_SYSTEMS
+#ifdef STORM_HAVE_CARL
template storm::models::Dtmc<storm::RationalFunction> const& SparsePropositionalModelChecker<storm::RationalFunction>::getModelAs() const;
template storm::models::Mdp<storm::RationalFunction> const& SparsePropositionalModelChecker<storm::RationalFunction>::getModelAs() const;
template class SparsePropositionalModelChecker<storm::RationalFunction>;
diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
index 4769ba873..8e9564ad6 100644
--- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
+++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
@@ -3,9 +3,7 @@
#include <algorithm>
#include <chrono>
-#ifdef PARAMETRIC_SYSTEMS
-#include "src/storage/parameters.h"
-#endif
+#include "src/adapters/CarlAdapter.h"
#include "src/storage/StronglyConnectedComponentDecomposition.h"
@@ -1021,8 +1019,8 @@ namespace storm {
template class SparseDtmcEliminationModelChecker<double>;
-#ifdef PARAMETRIC_SYSTEMS
- template class SparseDtmcEliminationModelChecker<RationalFunction>;
+#ifdef STORM_HAVE_CARL
+ template class SparseDtmcEliminationModelChecker<storm::RationalFunction>;
#endif
} // namespace modelchecker
} // namespace storm
diff --git a/src/modelchecker/results/CheckResult.cpp b/src/modelchecker/results/CheckResult.cpp
index 735e6c021..22bb96ee9 100644
--- a/src/modelchecker/results/CheckResult.cpp
+++ b/src/modelchecker/results/CheckResult.cpp
@@ -1,7 +1,7 @@
#include "src/modelchecker/results/CheckResult.h"
#include "storm-config.h"
-#include "src/storage/parameters.h"
+#include "src/adapters/CarlAdapter.h"
#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
@@ -90,7 +90,7 @@ namespace storm {
template ExplicitQuantitativeCheckResult<double>& CheckResult::asExplicitQuantitativeCheckResult();
template ExplicitQuantitativeCheckResult<double> const& CheckResult::asExplicitQuantitativeCheckResult() const;
-#ifdef PARAMETRIC_SYSTEMS
+#ifdef STORM_HAVE_CARL
template QuantitativeCheckResult<storm::RationalFunction>& CheckResult::asQuantitativeCheckResult();
template QuantitativeCheckResult<storm::RationalFunction> const& CheckResult::asQuantitativeCheckResult() const;
template ExplicitQuantitativeCheckResult<storm::RationalFunction>& CheckResult::asExplicitQuantitativeCheckResult();
diff --git a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
index d1c5aebae..90d7b09ef 100644
--- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
+++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
@@ -4,10 +4,7 @@
#include "src/storage/BitVector.h"
#include "src/utility/macros.h"
#include "src/exceptions/InvalidOperationException.h"
-
-// Include the configuration to check whether rational functions are available.
-#include "storm-config.h"
-#include "src/storage/parameters.h"
+#include "src/adapters/CarlAdapter.h"
namespace storm {
namespace modelchecker {
@@ -231,7 +228,7 @@ namespace storm {
template class ExplicitQuantitativeCheckResult<double>;
-#ifdef PARAMETRIC_SYSTEMS
+#ifdef STORM_HAVE_CARL
template class ExplicitQuantitativeCheckResult<storm::RationalFunction>;
#endif
}
diff --git a/src/modelchecker/results/QuantitativeCheckResult.cpp b/src/modelchecker/results/QuantitativeCheckResult.cpp
index 0b6e2c9d2..40d97d99e 100644
--- a/src/modelchecker/results/QuantitativeCheckResult.cpp
+++ b/src/modelchecker/results/QuantitativeCheckResult.cpp
@@ -1,7 +1,7 @@
#include "src/modelchecker/results/QuantitativeCheckResult.h"
#include "storm-config.h"
-#include "src/storage/parameters.h"
+#include "src/adapters/CarlAdapter.h"
#include "src/utility/macros.h"
#include "src/exceptions/InvalidOperationException.h"
@@ -15,7 +15,7 @@ namespace storm {
template class QuantitativeCheckResult<double>;
-#ifdef PARAMETRIC_SYSTEMS
+#ifdef STORM_HAVE_CARL
template class QuantitativeCheckResult<storm::RationalFunction>;
#endif
}
diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp
index d361c4de5..d38cf4305 100644
--- a/src/settings/modules/GeneralSettings.cpp
+++ b/src/settings/modules/GeneralSettings.cpp
@@ -41,6 +41,7 @@ namespace storm {
const std::string GeneralSettings::statisticsOptionShortName = "stats";
const std::string GeneralSettings::bisimulationOptionName = "bisimulation";
const std::string GeneralSettings::bisimulationOptionShortName = "bisim";
+ const std::string GeneralSettings::parametricOptionName = "parametric";
GeneralSettings::GeneralSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
this->addOption(storm::settings::OptionBuilder(moduleName, helpOptionName, false, "Shows all available options, arguments and descriptions.").setShortName(helpOptionShortName)
@@ -84,6 +85,7 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that Note that this requires the model to be given as an symbolic model (i.e., via --" + symbolicOptionName + ").").setShortName(constantsOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, statisticsOptionName, false, "Sets whether to display statistics if available.").setShortName(statisticsOptionShortName).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, parametricOptionName, false, "Sets whether to use the parametric engine.").build());
}
bool GeneralSettings::isHelpSet() const {
@@ -239,6 +241,14 @@ namespace storm {
return this->getOption(statisticsOptionName).getHasOptionBeenSet();
}
+ bool GeneralSettings::isBisimulationSet() const {
+ return this->getOption(bisimulationOptionName).getHasOptionBeenSet();
+ }
+
+ bool GeneralSettings::isParametricSet() const {
+ return this->getOption(parametricOptionName).getHasOptionBeenSet();
+ }
+
bool GeneralSettings::check() const {
// Ensure that the model was given either symbolically or explicitly.
STORM_LOG_THROW(!isSymbolicSet() || !isExplicitSet(), storm::exceptions::InvalidSettingsException, "The model may be either given in an explicit or a symbolic format, but not both.");
@@ -250,10 +260,6 @@ namespace storm {
return true;
}
- bool GeneralSettings::isBisimulationSet() const {
- return this->getOption(bisimulationOptionName).getHasOptionBeenSet();
- }
-
} // namespace modules
} // namespace settings
} // namespace storm
\ No newline at end of file
diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h
index 583bf7e3b..e0d84e894 100644
--- a/src/settings/modules/GeneralSettings.h
+++ b/src/settings/modules/GeneralSettings.h
@@ -286,6 +286,13 @@ namespace storm {
*/
bool isBisimulationSet() const;
+ /*!
+ * Retrieves whether the option enabling parametric model checking is set.
+ *
+ * @return True iff the option was set.
+ */
+ bool isParametricSet() const;
+
bool check() const override;
// The name of the module.
@@ -325,6 +332,7 @@ namespace storm {
static const std::string statisticsOptionShortName;
static const std::string bisimulationOptionName;
static const std::string bisimulationOptionShortName;
+ static const std::string parametricOptionName;
};
} // namespace modules
diff --git a/src/storage/DeterministicModelBisimulationDecomposition.cpp b/src/storage/DeterministicModelBisimulationDecomposition.cpp
index 33d2589da..ba1e52efa 100644
--- a/src/storage/DeterministicModelBisimulationDecomposition.cpp
+++ b/src/storage/DeterministicModelBisimulationDecomposition.cpp
@@ -6,7 +6,7 @@
#include <iomanip>
#include <boost/iterator/transform_iterator.hpp>
-#include "src/storage/parameters.h"
+#include "src/adapters/CarlAdapter.h"
#include "src/modelchecker/propositional/SparsePropositionalModelChecker.h"
#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
@@ -1488,7 +1488,7 @@ namespace storm {
template class DeterministicModelBisimulationDecomposition<double>;
-#ifdef PARAMETRIC_SYSTEMS
+#ifdef STORM_HAVE_CARL
template class DeterministicModelBisimulationDecomposition<storm::RationalFunction>;
#endif
}
diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp
index c191ba9e0..9fcdb856e 100644
--- a/src/storage/SparseMatrix.cpp
+++ b/src/storage/SparseMatrix.cpp
@@ -8,7 +8,7 @@
#endif
#include "src/storage/SparseMatrix.h"
-#include "src/storage/parameters.h"
+#include "src/adapters/CarlAdapter.h"
#include "src/exceptions/InvalidStateException.h"
#include "src/utility/macros.h"
@@ -986,7 +986,7 @@ namespace storm {
template class SparseMatrixBuilder<int>;
template class SparseMatrix<int>;
template std::ostream& operator<<(std::ostream& out, SparseMatrix<int> const& matrix);
-#ifdef PARAMETRIC_SYSTEMS
+#ifdef STORM_HAVE_CARL
template class MatrixEntry<typename SparseMatrix<RationalFunction>::index_type, RationalFunction>;
template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, RationalFunction> const& entry);
template class SparseMatrixBuilder<RationalFunction>;
diff --git a/src/storage/StronglyConnectedComponentDecomposition.cpp b/src/storage/StronglyConnectedComponentDecomposition.cpp
index f510f478c..692fdd9d7 100644
--- a/src/storage/StronglyConnectedComponentDecomposition.cpp
+++ b/src/storage/StronglyConnectedComponentDecomposition.cpp
@@ -1,6 +1,6 @@
#include "src/storage/StronglyConnectedComponentDecomposition.h"
#include "src/models/AbstractModel.h"
-#include "src/storage/parameters.h"
+#include "src/adapters/CarlAdapter.h"
namespace storm {
namespace storage {
@@ -211,11 +211,9 @@ namespace storm {
// Explicitly instantiate the SCC decomposition.
template class StronglyConnectedComponentDecomposition<double>;
- #ifdef PARAMETRIC_SYSTEMS
- template class StronglyConnectedComponentDecomposition<Polynomial>;
- template class StronglyConnectedComponentDecomposition<RationalFunction>;
- #endif
-
-
+#ifdef STORM_HAVE_CARL
+ template class StronglyConnectedComponentDecomposition<storm::Polynomial>;
+ template class StronglyConnectedComponentDecomposition<storm::RationalFunction>;
+#endif
} // namespace storage
} // namespace storm
\ No newline at end of file
diff --git a/src/storage/expressions/ExpressionEvaluator.h b/src/storage/expressions/ExpressionEvaluator.h
index 5229807f0..d9fa1653b 100644
--- a/src/storage/expressions/ExpressionEvaluator.h
+++ b/src/storage/expressions/ExpressionEvaluator.h
@@ -3,7 +3,7 @@
#include <unordered_map>
-#include "src/storage/parameters.h"
+#include "src/adapters/CarlAdapter.h"
#include "src/storage/expressions/Variable.h"
#include "src/storage/expressions/Expression.h"
#include "src/storage/expressions/ExprtkExpressionEvaluator.h"
diff --git a/src/storage/expressions/ExpressionEvaluatorBase.cpp b/src/storage/expressions/ExpressionEvaluatorBase.cpp
index a750946e3..e707a48ca 100644
--- a/src/storage/expressions/ExpressionEvaluatorBase.cpp
+++ b/src/storage/expressions/ExpressionEvaluatorBase.cpp
@@ -1,7 +1,7 @@
#include "src/storage/expressions/ExpressionEvaluatorBase.h"
#include "src/storage/expressions/ExpressionManager.h"
-#include "src/storage/parameters.h"
+#include "src/adapters/CarlAdapter.h"
namespace storm {
namespace expressions {
@@ -17,7 +17,7 @@ namespace storm {
template class ExpressionEvaluatorBase<double>;
#ifdef STORM_HAVE_CARL
- template class ExpressionEvaluatorBase<RationalFunction>;
+ template class ExpressionEvaluatorBase<storm::RationalFunction>;
#endif
}
}
\ No newline at end of file
diff --git a/src/storage/expressions/ExprtkExpressionEvaluator.cpp b/src/storage/expressions/ExprtkExpressionEvaluator.cpp
index 11799faa5..b621b64a6 100644
--- a/src/storage/expressions/ExprtkExpressionEvaluator.cpp
+++ b/src/storage/expressions/ExprtkExpressionEvaluator.cpp
@@ -1,7 +1,7 @@
#include "src/storage/expressions/ExprtkExpressionEvaluator.h"
#include "src/storage/expressions/ExpressionManager.h"
-#include "src/storage/parameters.h"
+#include "src/adapters/CarlAdapter.h"
#include "src/utility/macros.h"
namespace storm {
diff --git a/src/storage/expressions/ToRationalFunctionVisitor.h b/src/storage/expressions/ToRationalFunctionVisitor.h
index 51cc96761..4ad74acc9 100644
--- a/src/storage/expressions/ToRationalFunctionVisitor.h
+++ b/src/storage/expressions/ToRationalFunctionVisitor.h
@@ -1,7 +1,7 @@
#ifndef STORM_STORAGE_EXPRESSIONS_TORATIONALFUNCTIONVISITOR_H_
#define STORM_STORAGE_EXPRESSIONS_TORATIONALFUNCTIONVISITOR_H_
-#include "src/storage/parameters.h"
+#include "src/adapters/CarlAdapter.h"
#include "src/storage/expressions/Expression.h"
#include "src/storage/expressions/Expressions.h"
#include "src/storage/expressions/ExpressionVisitor.h"
diff --git a/src/utility/ConstantsComparator.cpp b/src/utility/ConstantsComparator.cpp
index 0c189adaf..ac05599a0 100644
--- a/src/utility/ConstantsComparator.cpp
+++ b/src/utility/ConstantsComparator.cpp
@@ -79,7 +79,7 @@ namespace storm {
return true;
}
-#ifdef PARAMETRIC_SYSTEMS
+#ifdef STORM_HAVE_CARL
template<>
RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent) {
return carl::pow(value, exponent);
@@ -182,7 +182,7 @@ namespace storm {
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>& matrixEntry);
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>&& matrixEntry);
-#ifdef PARAMETRIC_SYSTEMS
+#ifdef STORM_HAVE_CARL
template class ConstantsComparator<RationalFunction>;
template class ConstantsComparator<Polynomial>;
diff --git a/src/utility/ConstantsComparator.h b/src/utility/ConstantsComparator.h
index 5d77504e0..2c45c9f8f 100644
--- a/src/utility/ConstantsComparator.h
+++ b/src/utility/ConstantsComparator.h
@@ -13,12 +13,7 @@
#include <cstdint>
#include "src/settings/SettingsManager.h"
-
-#include "storm-config.h"
-
-#ifdef PARAMETRIC_SYSTEMS
-#include "src/storage/parameters.h"
-#endif
+#include "src/adapters/CarlAdapter.h"
namespace storm {
@@ -81,7 +76,7 @@ namespace storm {
double precision;
};
-#ifdef PARAMETRIC_SYSTEMS
+#ifdef STORM_HAVE_CARL
template<>
RationalFunction& simplify(RationalFunction& value);
diff --git a/src/utility/PrismUtility.h b/src/utility/PrismUtility.h
index 5f5e716d3..7d76dd5f4 100644
--- a/src/utility/PrismUtility.h
+++ b/src/utility/PrismUtility.h
@@ -225,7 +225,7 @@ namespace storm {
constantDefinitions[variable] = program.getManager().rational(doubleValue);
}
} else {
- throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: unknown undefined constant " << constantName << ".";
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal constant definition string: unknown undefined constant " << constantName << ".");
}
}
}
diff --git a/src/utility/cli.h b/src/utility/cli.h
index 1961fc738..f82da0994 100644
--- a/src/utility/cli.h
+++ b/src/utility/cli.h
@@ -274,58 +274,59 @@ namespace storm {
}
// Customize model-building.
- typename storm::builder::ExplicitPrismModelBuilder<double>::Options options;
+ typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options options;
if (formula) {
- options = storm::builder::ExplicitPrismModelBuilder<double>::Options(*formula.get());
+ options = typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options(*formula.get());
}
options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString());
// Then, build the model from the symbolic description.
- result = storm::builder::ExplicitPrismModelBuilder<double>::translateProgram(program, options);
+ result = storm::builder::ExplicitPrismModelBuilder<ValueType>::translateProgram(program, options);
return result;
}
template<typename ValueType>
std::shared_ptr<storm::models::AbstractModel<ValueType>> preprocessModel(std::shared_ptr<storm::models::AbstractModel<ValueType>> model, boost::optional<std::shared_ptr<storm::logic::Formula>> const& formula) {
if (storm::settings::generalSettings().isBisimulationSet()) {
- STORM_LOG_THROW(model->getType() == storm::models::DTMC, storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs.");
- std::shared_ptr<storm::models::Dtmc<double>> dtmc = model->template as<storm::models::Dtmc<double>>();
+ STORM_LOG_THROW(model->getType() == storm::models::DTMC || model->getType() == storm::models::CTMC, storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs.");
+ std::shared_ptr<storm::models::Dtmc<ValueType>> dtmc = model->template as<storm::models::Dtmc<ValueType>>();
if (dtmc->hasTransitionRewards()) {
dtmc->convertTransitionRewardsToStateRewards();
}
std::cout << "Performing bisimulation minimization... ";
- typename storm::storage::DeterministicModelBisimulationDecomposition<double>::Options options;
+ typename storm::storage::DeterministicModelBisimulationDecomposition<ValueType>::Options options;
if (formula) {
- options = storm::storage::DeterministicModelBisimulationDecomposition<double>::Options(*model, *formula.get());
+ options = typename storm::storage::DeterministicModelBisimulationDecomposition<ValueType>::Options(*model, *formula.get());
}
if (storm::settings::bisimulationSettings().isWeakBisimulationSet()) {
options.weak = true;
options.bounded = false;
}
- storm::storage::DeterministicModelBisimulationDecomposition<double> bisimulationDecomposition(*dtmc, options);
+ storm::storage::DeterministicModelBisimulationDecomposition<ValueType> bisimulationDecomposition(*dtmc, options);
model = bisimulationDecomposition.getQuotient();
std::cout << "done." << std::endl << std::endl;
}
return model;
}
- void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::AbstractModel<double>> model, std::shared_ptr<storm::logic::Formula> const& formula) {
+ template<typename ValueType>
+ void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::AbstractModel<ValueType>> model, std::shared_ptr<storm::logic::Formula> formula) {
if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandSetGenerationSet()) {
STORM_LOG_THROW(model->getType() == storm::models::MDP, storm::exceptions::InvalidTypeException, "Minimal command set generation is only available for MDPs.");
STORM_LOG_THROW(storm::settings::generalSettings().isSymbolicSet(), storm::exceptions::InvalidSettingsException, "Minimal command set generation is only available for symbolic models.");
- std::shared_ptr<storm::models::Mdp<double>> mdp = model->as<storm::models::Mdp<double>>();
+ std::shared_ptr<storm::models::Mdp<ValueType>> mdp = model->template as<storm::models::Mdp<ValueType>>();
// Determine whether we are required to use the MILP-version or the SAT-version.
bool useMILP = storm::settings::counterexampleGeneratorSettings().isUseMilpBasedMinimalCommandSetGenerationSet();
if (useMILP) {
- storm::counterexamples::MILPMinimalLabelSetGenerator<double>::computeCounterexample(program, *mdp, formula);
+ storm::counterexamples::MILPMinimalLabelSetGenerator<ValueType>::computeCounterexample(program, *mdp, formula);
} else {
- storm::counterexamples::SMTMinimalCommandSetGenerator<double>::computeCounterexample(program, storm::settings::generalSettings().getConstantDefinitionString(), *mdp, formula);
+ storm::counterexamples::SMTMinimalCommandSetGenerator<ValueType>::computeCounterexample(program, storm::settings::generalSettings().getConstantDefinitionString(), *mdp, formula);
}
} else {
@@ -333,12 +334,119 @@ namespace storm {
}
}
+ template<>
+ void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::AbstractModel<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula> formula) {
+ STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model.");
+ }
+
+ template<typename ValueType>
+ void verifyModel(boost::optional<storm::prism::Program> const& program, std::shared_ptr<storm::models::AbstractModel<ValueType>> model, std::shared_ptr<storm::logic::Formula> formula) {
+ storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
+
+ // If we were requested to generate a counterexample, we now do so.
+ if (settings.isCounterexampleSet()) {
+ STORM_LOG_THROW(program, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for non-symbolic model.");
+ generateCounterexample<ValueType>(program.get(), model, formula);
+ } else {
+ std::cout << std::endl << "Model checking property: " << *formula << " ...";
+ std::unique_ptr<storm::modelchecker::CheckResult> result;
+ if (model->getType() == storm::models::DTMC) {
+ std::shared_ptr<storm::models::Dtmc<ValueType>> dtmc = model->template as<storm::models::Dtmc<ValueType>>();
+ storm::modelchecker::SparseDtmcEliminationModelChecker<ValueType> modelchecker(*dtmc);
+ if (modelchecker.canHandle(*formula.get())) {
+ result = modelchecker.check(*formula.get());
+ } else {
+ storm::modelchecker::SparseDtmcPrctlModelChecker<ValueType> modelchecker2(*dtmc);
+ if (modelchecker2.canHandle(*formula.get())) {
+ modelchecker2.check(*formula.get());
+ }
+ }
+ } else if (model->getType() == storm::models::MDP) {
+ std::shared_ptr<storm::models::Mdp<ValueType>> mdp = model->template as<storm::models::Mdp<ValueType>>();
+ storm::modelchecker::SparseMdpPrctlModelChecker<ValueType> modelchecker(*mdp);
+ result = modelchecker.check(*formula.get());
+ }
+
+ if (result) {
+ std::cout << " done." << std::endl;
+ std::cout << "Result (initial states): ";
+ result->writeToStream(std::cout, model->getInitialStates());
+ std::cout << std::endl << std::endl;
+ } else {
+ std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
+ }
+ }
+ }
+
+ template<>
+ void verifyModel(boost::optional<storm::prism::Program> const& program, std::shared_ptr<storm::models::AbstractModel<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula> formula) {
+ storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
+
+ STORM_LOG_THROW(model->getType() == storm::models::DTMC, storm::exceptions::InvalidSettingsException, "Currently parametric verification is only available for DTMCs.");
+ std::shared_ptr<storm::models::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::Dtmc<storm::RationalFunction>>();
+
+ std::cout << std::endl << "Model checking property: " << *formula << " ...";
+ std::unique_ptr<storm::modelchecker::CheckResult> result;
+
+ storm::modelchecker::SparseDtmcEliminationModelChecker<storm::RationalFunction> modelchecker(*dtmc);
+ if (modelchecker.canHandle(*formula.get())) {
+ result = modelchecker.check(*formula.get());
+ } else {
+ STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The parametric engine currently does not support this property.");
+ }
+
+ if (result) {
+ std::cout << " done." << std::endl;
+ std::cout << "Result (initial states): ";
+ result->writeToStream(std::cout, model->getInitialStates());
+ std::cout << std::endl << std::endl;
+ } else {
+ std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
+ }
+ }
+
+ template<typename ValueType>
+ void buildAndCheckSymbolicModel(boost::optional<storm::prism::Program> const& program, boost::optional<std::shared_ptr<storm::logic::Formula>> formula) {
+ // Now we are ready to actually build the model.
+ STORM_LOG_THROW(program, storm::exceptions::InvalidStateException, "Program has not been successfully parsed.");
+ std::shared_ptr<storm::models::AbstractModel<ValueType>> model = buildSymbolicModel<ValueType>(program.get(), formula);
+
+ // Preprocess the model if needed.
+ model = preprocessModel<ValueType>(model, formula);
+
+ // Print some information about the model.
+ model->printModelInformationToStream(std::cout);
+
+ // Verify the model, if a formula was given.
+ if (formula) {
+ verifyModel<ValueType>(program, model, formula.get());
+ }
+ }
+
+ template<typename ValueType>
+ void buildAndCheckExplicitModel(boost::optional<std::shared_ptr<storm::logic::Formula>> formula) {
+ storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
+
+ STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files.");
+ std::shared_ptr<storm::models::AbstractModel<ValueType>> model = buildExplicitModel<ValueType>(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional<std::string>(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional<std::string>());
+
+ // Preprocess the model if needed.
+ model = preprocessModel<ValueType>(model, formula);
+
+ // Print some information about the model.
+ model->printModelInformationToStream(std::cout);
+
+ // Verify the model, if a formula was given.
+ if (formula) {
+ verifyModel<ValueType>(boost::optional<storm::prism::Program>(), model, formula.get());
+ }
+ }
+
void processOptions() {
if (storm::settings::debugSettings().isLogfileSet()) {
initializeFileLogging();
}
- std::chrono::high_resolution_clock::time_point totalTimeStart = std::chrono::high_resolution_clock::now();
storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
// If we have to build the model from a symbolic representation, we need to parse the representation first.
@@ -360,82 +468,16 @@ namespace storm {
}
}
- // Now we are ready to actually build the model.
- std::chrono::high_resolution_clock::time_point buildingTimeStart = std::chrono::high_resolution_clock::now();
- std::shared_ptr<storm::models::AbstractModel<double>> model;
- if (settings.isExplicitSet()) {
- model = buildExplicitModel<double>(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? settings.getStateRewardsFilename() : boost::optional<std::string>(), settings.isTransitionRewardsSet() ? settings.getTransitionRewardsFilename() : boost::optional<std::string>());
- } else if (settings.isSymbolicSet()) {
- STORM_LOG_THROW(program, storm::exceptions::InvalidStateException, "Program has not been successfully parsed.");
- model = buildSymbolicModel<double>(program.get(), formula);
- } else {
- STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
- }
- std::chrono::high_resolution_clock::time_point buildingTimeEnd = std::chrono::high_resolution_clock::now();
-
- // Now, we can do the preprocessing on the model, if it was requested.
- std::chrono::high_resolution_clock::time_point preprocessingTimeStart = std::chrono::high_resolution_clock::now();
- model = preprocessModel(model, formula);
- std::chrono::high_resolution_clock::time_point preprocessingTimeEnd = std::chrono::high_resolution_clock::now();
-
- // Print some information about the model.
- model->printModelInformationToStream(std::cout);
-
- std::chrono::high_resolution_clock::time_point checkingTimeStart = std::chrono::high_resolution_clock::now();
- // If we were requested to generate a counterexample, we now do so.
- if (settings.isCounterexampleSet()) {
- STORM_LOG_THROW(settings.isPropertySet(), storm::exceptions::InvalidSettingsException, "Unable to generate counterexample without a property.");
- STORM_LOG_THROW(program, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for non-symbolic model.");
- generateCounterexample(program.get(), model, formula.get());
- } else if (formula) {
- std::cout << std::endl << "Model checking property: " << *formula.get() << " ...";
- std::unique_ptr<storm::modelchecker::CheckResult> result;
- if (model->getType() == storm::models::DTMC) {
- std::shared_ptr<storm::models::Dtmc<double>> dtmc = model->as<storm::models::Dtmc<double>>();
- storm::modelchecker::SparseDtmcEliminationModelChecker<double> modelchecker(*dtmc);
- if (modelchecker.canHandle(*formula.get())) {
- result = modelchecker.check(*formula.get());
- } else {
- storm::modelchecker::SparseDtmcPrctlModelChecker<double> modelchecker2(*dtmc);
- if (modelchecker2.canHandle(*formula.get())) {
- modelchecker2.check(*formula.get());
- }
- }
- } else if (model->getType() == storm::models::MDP) {
- std::shared_ptr<storm::models::Mdp<double>> mdp = model->as<storm::models::Mdp<double>>();
- storm::modelchecker::SparseMdpPrctlModelChecker<double> modelchecker(*mdp);
- result = modelchecker.check(*formula.get());
- }
- if (result) {
- std::cout << " done." << std::endl;
- std::cout << "Result (initial states): ";
- result->writeToStream(std::cout, model->getInitialStates());
- std::cout << std::endl << std::endl;
+ if (settings.isSymbolicSet()) {
+ if (settings.isParametricSet()) {
+ buildAndCheckSymbolicModel<storm::RationalFunction>(program.get(), formula);
} else {
- std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
+ buildAndCheckSymbolicModel<double>(program.get(), formula);
}
- }
- std::chrono::high_resolution_clock::time_point checkingTimeEnd = std::chrono::high_resolution_clock::now();
- std::chrono::high_resolution_clock::time_point totalTimeEnd = std::chrono::high_resolution_clock::now();
-
- if (storm::settings::generalSettings().isShowStatisticsSet()) {
- std::chrono::high_resolution_clock::duration totalTime = totalTimeEnd - totalTimeStart;
- std::chrono::milliseconds totalTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(totalTime);
- std::chrono::high_resolution_clock::duration buildingTime = buildingTimeEnd - buildingTimeStart;
- std::chrono::milliseconds buildingTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(buildingTime);
- std::chrono::high_resolution_clock::duration preprocessingTime = preprocessingTimeEnd - preprocessingTimeStart;
- std::chrono::milliseconds preprocessingTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(preprocessingTime);
- std::chrono::high_resolution_clock::duration checkingTime = checkingTimeEnd - checkingTimeStart;
- std::chrono::milliseconds checkingTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(checkingTime);
-
- STORM_PRINT_AND_LOG(std::endl);
- STORM_PRINT_AND_LOG("Time breakdown:" << std::endl);
- STORM_PRINT_AND_LOG(" * time for building: " << buildingTimeInMilliseconds.count() << "ms" << std::endl);
- STORM_PRINT_AND_LOG(" * time for preprocessing: " << preprocessingTimeInMilliseconds.count() << "ms" << std::endl);
- STORM_PRINT_AND_LOG(" * time for checking: " << checkingTimeInMilliseconds.count() << "ms" << std::endl);
- STORM_PRINT_AND_LOG("------------------------------------------" << std::endl);
- STORM_PRINT_AND_LOG(" * total time: " << totalTimeInMilliseconds.count() << "ms" << std::endl);
- STORM_PRINT_AND_LOG(std::endl);
+ } else if (settings.isExplicitSet()) {
+ buildAndCheckExplicitModel<double>(formula);
+ } else {
+ STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
}
}
}