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 -#include - -// 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 -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 -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> formula; - if (storm::settings::generalSettings().isPropertySet()) { - formula = storm::parser::FormulaParser(program.getManager().getSharedPointer()).parseFromString(storm::settings::generalSettings().getProperty()); - } - - typename storm::builder::ExplicitPrismModelBuilder::Options options; - if (formula) { - options = typename storm::builder::ExplicitPrismModelBuilder::Options(*formula.get()); - } - options.addConstantDefinitionsFromString(program, storm::settings::generalSettings().getConstantDefinitionString()); - - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder::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(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> dtmc = model->template as>(); - - storm::modelchecker::SparseDtmcEliminationModelChecker 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::Options options(*dtmc, *formula.get()); - options.weak = storm::settings::bisimulationSettings().isWeakBisimulationSet(); - - storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*dtmc, options); - *dtmc = std::move(*bisimulationDecomposition.getQuotient()->template as>()); - - dtmc->printModelInformationToStream(std::cout); - } - - STORM_LOG_THROW(dtmc, storm::exceptions::InvalidStateException, "Preprocessing went wrong."); - - storm::modelchecker::reachability::CollectConstraints constraintCollector; - constraintCollector(*dtmc); - - std::unique_ptr result = modelchecker.check(*formula.get()); - ValueType valueFunction = result->asExplicitQuantitativeCheckResult()[*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::value) { - printApproximateResult(valueFunction); - } - std::cout << std::endl; - - // Generate derivatives for sensitivity analysis if requested. - if (std::is_same::value && storm::settings::parametricSettings().isDerivativesSet()) { - auto allVariables = valueFunction.gatherVariables(); - - if (!allVariables.empty()) { - std::map 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(); - - // 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> 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&); -//} -//