From e89e08975410ba28b3bafdee96fdc5f567935926 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 13 Feb 2015 10:30:50 +0100
Subject: [PATCH] Removed parametric main files.
Former-commit-id: 526f0754bb9679678c3e4fee6bda44b1d165345e
---
src/stormParametric.cpp | 146 ----------------------------------------
src/stormParametric.h | 33 ---------
2 files changed, 179 deletions(-)
delete mode 100644 src/stormParametric.cpp
delete mode 100644 src/stormParametric.h
diff --git a/src/stormParametric.cpp b/src/stormParametric.cpp
deleted file mode 100644
index bcc7e0d02..000000000
--- a/src/stormParametric.cpp
+++ /dev/null
@@ -1,146 +0,0 @@
-// Include generated headers.
-#include "storm-config.h"
-
-#include <tuple>
-#include <sstream>
-
-// Include other headers.
-#include "src/exceptions/BaseException.h"
-#include "src/utility/macros.h"
-#include "src/utility/cli.h"
-#include "src/utility/export.h"
-#include "src/modelchecker/reachability/CollectConstraints.h"
-
-//#include "src/modelchecker/reachability/DirectEncoding.h"
-#include "src/storage/DeterministicModelBisimulationDecomposition.h"
-#include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
-#include "src/storage/parameters.h"
-#include "src/models/Dtmc.h"
-
-template<typename ValueType>
-void printApproximateResult(ValueType const& value) {
- // Intentionally left empty.
-}
-
-template<>
-void printApproximateResult(storm::RationalFunction const& value) {
- if (value.isConstant()) {
- STORM_PRINT_AND_LOG(" (approximately " << std::setprecision(30) << carl::toDouble(value.constantPart()) << ")" << std::endl);
- }
-}
-
-template<typename ValueType>
-void check() {
- // From this point on we are ready to carry out the actual computations.
- // Program Translation Time Measurement, Start
- std::chrono::high_resolution_clock::time_point programTranslationStart = std::chrono::high_resolution_clock::now();
-
- if (storm::settings::generalSettings().isSymbolicSet()) {
- std::string programFile = storm::settings::generalSettings().getSymbolicModelFilename();
- std::string constants = storm::settings::generalSettings().getConstantDefinitionString();
- storm::prism::Program program = storm::parser::PrismParser::parse(programFile);
-
- boost::optional<std::shared_ptr<storm::logic::Formula>> formula;
- if (storm::settings::generalSettings().isPropertySet()) {
- formula = storm::parser::FormulaParser(program.getManager().getSharedPointer()).parseFromString(storm::settings::generalSettings().getProperty());
- }
-
- typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options options;
- if (formula) {
- options = typename storm::builder::ExplicitPrismModelBuilder<ValueType>::Options(*formula.get());
- }
- options.addConstantDefinitionsFromString(program, storm::settings::generalSettings().getConstantDefinitionString());
-
- std::shared_ptr<storm::models::AbstractModel<ValueType>> model = storm::builder::ExplicitPrismModelBuilder<ValueType>::translateProgram(program, options);
-
- // Convert the transition rewards to state rewards if necessary.
- if (model->hasTransitionRewards()) {
- model->convertTransitionRewardsToStateRewards();
- }
-
- // Program Translation Time Measurement, End
- std::chrono::high_resolution_clock::time_point programTranslationEnd = std::chrono::high_resolution_clock::now();
- std::cout << "Parsing and translating the model took " << std::chrono::duration_cast<std::chrono::milliseconds>(programTranslationEnd - programTranslationStart).count() << "ms." << std::endl << std::endl;
-
- model->printModelInformationToStream(std::cout);
-
- if (formula) {
- STORM_LOG_THROW(model->getType() == storm::models::DTMC, storm::exceptions::InvalidArgumentException, "The given model is not a DTMC and, hence, not currently supported.");
- std::shared_ptr<storm::models::Dtmc<ValueType>> dtmc = model->template as<storm::models::Dtmc<ValueType>>();
-
- storm::modelchecker::SparseDtmcEliminationModelChecker<ValueType> modelchecker(*dtmc);
- STORM_LOG_THROW(modelchecker.canHandle(*formula.get()), storm::exceptions::InvalidPropertyException, "Model checker cannot handle the property: '" << *formula.get() << "'.");
-
- std::cout << "Checking formula " << *formula.get() << std::endl;
-
- // Perform bisimulation minimization if requested.
- if (storm::settings::generalSettings().isBisimulationSet()) {
- typename storm::storage::DeterministicModelBisimulationDecomposition<ValueType>::Options options(*dtmc, *formula.get());
- options.weak = storm::settings::bisimulationSettings().isWeakBisimulationSet();
-
- storm::storage::DeterministicModelBisimulationDecomposition<ValueType> bisimulationDecomposition(*dtmc, options);
- *dtmc = std::move(*bisimulationDecomposition.getQuotient()->template as<storm::models::Dtmc<ValueType>>());
-
- dtmc->printModelInformationToStream(std::cout);
- }
-
- STORM_LOG_THROW(dtmc, storm::exceptions::InvalidStateException, "Preprocessing went wrong.");
-
- storm::modelchecker::reachability::CollectConstraints<ValueType> constraintCollector;
- constraintCollector(*dtmc);
-
- std::unique_ptr<storm::modelchecker::CheckResult> result = modelchecker.check(*formula.get());
- ValueType valueFunction = result->asExplicitQuantitativeCheckResult<ValueType>()[*model->getInitialStates().begin()];
-
- if (storm::settings::parametricSettings().exportResultToFile()) {
- storm::utility::exportParametricMcResult(valueFunction, constraintCollector);
- }
-
- // Report the result.
- STORM_PRINT_AND_LOG(std::endl << "Result (initial state): ");
- result->writeToStream(std::cout, model->getInitialStates());
- if (std::is_same<ValueType, storm::RationalFunction>::value) {
- printApproximateResult(valueFunction);
- }
- std::cout << std::endl;
-
- // Generate derivatives for sensitivity analysis if requested.
- if (std::is_same<ValueType, storm::RationalFunction>::value && storm::settings::parametricSettings().isDerivativesSet()) {
- auto allVariables = valueFunction.gatherVariables();
-
- if (!allVariables.empty()) {
- std::map<storm::Variable, storm::RationalFunction> derivatives;
- for (auto const& variable : allVariables) {
- derivatives[variable] = valueFunction.derivative(variable);
- }
-
- std::cout << std::endl << "Derivatives (variable; derivative):" << std::endl;
- for (auto const& variableDerivativePair : derivatives) {
- std::cout << "(" << variableDerivativePair.first << "; " << variableDerivativePair.second << ")" << std::endl;
- }
- }
- }
- }
- }
-}
-
-/*!
- * Main entry point of the executable pstorm.
- */
-int main(const int argc, const char** argv) {
- try {
- storm::utility::cli::setUp();
- storm::utility::cli::printHeader(argc, argv);
- bool optionsCorrect = storm::utility::cli::parseOptions(argc, argv);
-
- check<storm::RationalFunction>();
-
- // All operations have now been performed, so we clean up everything and terminate.
- storm::utility::cli::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());
- } 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());
- }
-}
diff --git a/src/stormParametric.h b/src/stormParametric.h
deleted file mode 100644
index cba7e8fe0..000000000
--- a/src/stormParametric.h
+++ /dev/null
@@ -1,33 +0,0 @@
-//
-//
-//
-//#pragma once
-//#include "storage/prism/Program.h"
-//#include "models/AbstractModel.h"
-//#include "storage/parameters.h"
-//
-//namespace storm
-//{
-// class ParametricStormEntryPoint
-// {
-// private:
-// std::string const& mConstants;
-// storm::prism::Program const& mProgram;
-// std::shared_ptr<storm::models::AbstractModel<RationalFunction>> mModel;
-// public:
-// ParametricStormEntryPoint(std::string const& constants, storm::prism::Program const& program) :
-// mConstants(constants),
-// mProgram(program)
-// {
-//
-// }
-//
-// void createModel();
-// std::string reachabilityToSmt2(std::string const&);
-//
-// virtual ~ParametricStormEntryPoint() {}
-//
-// };
-// void storm_parametric(std::string const& constants, storm::prism::Program const&);
-//}
-//