diff --git a/resources/3rdparty/sylvan/src/storm_wrapper.cpp b/resources/3rdparty/sylvan/src/storm_wrapper.cpp index edb31fda1..4678bec87 100644 --- a/resources/3rdparty/sylvan/src/storm_wrapper.cpp +++ b/resources/3rdparty/sylvan/src/storm_wrapper.cpp @@ -7,7 +7,7 @@ #include #include -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/constants.h" #include "storm/exceptions/InvalidOperationException.h" diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.hpp b/resources/3rdparty/sylvan/src/sylvan_obj.hpp index e9720c5a3..845349ad9 100755 --- a/resources/3rdparty/sylvan/src/sylvan_obj.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj.hpp @@ -23,7 +23,7 @@ #include #include -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace sylvan { diff --git a/src/storm-dft/builder/DftExplorationHeuristic.cpp b/src/storm-dft/builder/DftExplorationHeuristic.cpp index 0bcbd98ae..a8a11ae18 100644 --- a/src/storm-dft/builder/DftExplorationHeuristic.cpp +++ b/src/storm-dft/builder/DftExplorationHeuristic.cpp @@ -1,6 +1,6 @@ #include "DftExplorationHeuristic.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/macros.h" #include "storm/utility/constants.h" #include "storm/exceptions/NotImplementedException.h" diff --git a/src/storm-dft/storage/BucketPriorityQueue.cpp b/src/storm-dft/storage/BucketPriorityQueue.cpp index 89d7c7cce..3fccf05f9 100644 --- a/src/storm-dft/storage/BucketPriorityQueue.cpp +++ b/src/storm-dft/storage/BucketPriorityQueue.cpp @@ -1,6 +1,6 @@ #include "BucketPriorityQueue.h" #include "storm/utility/macros.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include diff --git a/src/storm-dft/storage/dft/elements/DFTElement.h b/src/storm-dft/storage/dft/elements/DFTElement.h index a27ba96b3..d5d82db5a 100644 --- a/src/storm-dft/storage/dft/elements/DFTElement.h +++ b/src/storm-dft/storage/dft/elements/DFTElement.h @@ -15,7 +15,7 @@ #include "../DFTState.h" #include "../DFTStateSpaceGenerationQueues.h" #include "storm/utility/constants.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" diff --git a/src/storm/abstraction/MenuGame.cpp b/src/storm/abstraction/MenuGame.cpp index 799003820..a62a5d769 100644 --- a/src/storm/abstraction/MenuGame.cpp +++ b/src/storm/abstraction/MenuGame.cpp @@ -10,7 +10,7 @@ #include "storm/models/symbolic/StandardRewardModel.h" #include "storm-config.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace abstraction { diff --git a/src/storm/abstraction/MenuGameAbstractor.cpp b/src/storm/abstraction/MenuGameAbstractor.cpp index 9a0071571..7ce40950b 100644 --- a/src/storm/abstraction/MenuGameAbstractor.cpp +++ b/src/storm/abstraction/MenuGameAbstractor.cpp @@ -10,7 +10,7 @@ #include "storm/utility/file.h" #include "storm-config.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace abstraction { diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index 75555bdcd..1e07ccd3e 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -16,7 +16,7 @@ #include "storm/settings/SettingsManager.h" #include "storm-config.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace abstraction { diff --git a/src/storm/abstraction/StateSetAbstractor.cpp b/src/storm/abstraction/StateSetAbstractor.cpp index 986589294..48e2042a9 100644 --- a/src/storm/abstraction/StateSetAbstractor.cpp +++ b/src/storm/abstraction/StateSetAbstractor.cpp @@ -8,7 +8,7 @@ #include "storm/utility/solver.h" #include "storm-config.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace abstraction { diff --git a/src/storm/abstraction/jani/AutomatonAbstractor.cpp b/src/storm/abstraction/jani/AutomatonAbstractor.cpp index e5f1e9b0b..b97ad6002 100644 --- a/src/storm/abstraction/jani/AutomatonAbstractor.cpp +++ b/src/storm/abstraction/jani/AutomatonAbstractor.cpp @@ -13,7 +13,7 @@ #include "storm/settings/SettingsManager.h" #include "storm-config.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/macros.h" diff --git a/src/storm/abstraction/jani/EdgeAbstractor.cpp b/src/storm/abstraction/jani/EdgeAbstractor.cpp index 980db0846..eaaafe266 100644 --- a/src/storm/abstraction/jani/EdgeAbstractor.cpp +++ b/src/storm/abstraction/jani/EdgeAbstractor.cpp @@ -17,7 +17,7 @@ #include "storm/utility/macros.h" #include "storm-config.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace abstraction { diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp index 816500023..b3c7a755a 100644 --- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp +++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp @@ -25,7 +25,7 @@ #include "storm/exceptions/NotSupportedException.h" #include "storm-config.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace abstraction { diff --git a/src/storm/abstraction/prism/CommandAbstractor.cpp b/src/storm/abstraction/prism/CommandAbstractor.cpp index cf116afcd..afc859e01 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.cpp +++ b/src/storm/abstraction/prism/CommandAbstractor.cpp @@ -17,7 +17,7 @@ #include "storm/utility/macros.h" #include "storm-config.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace abstraction { diff --git a/src/storm/abstraction/prism/ModuleAbstractor.cpp b/src/storm/abstraction/prism/ModuleAbstractor.cpp index 5670499ea..6ba51b062 100644 --- a/src/storm/abstraction/prism/ModuleAbstractor.cpp +++ b/src/storm/abstraction/prism/ModuleAbstractor.cpp @@ -12,7 +12,7 @@ #include "storm/settings/SettingsManager.h" #include "storm-config.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/macros.h" diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index e196c1510..4cb3d46eb 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -23,7 +23,7 @@ #include "storm/exceptions/NotSupportedException.h" #include "storm-config.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace abstraction { diff --git a/src/storm/adapters/AddExpressionAdapter.cpp b/src/storm/adapters/AddExpressionAdapter.cpp index 4ec8470e8..f792584a8 100644 --- a/src/storm/adapters/AddExpressionAdapter.cpp +++ b/src/storm/adapters/AddExpressionAdapter.cpp @@ -9,7 +9,7 @@ #include "storm/storage/dd/Bdd.h" #include "storm-config.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/constants.h" diff --git a/src/storm/adapters/EigenAdapter.h b/src/storm/adapters/EigenAdapter.h index 5fd1e832a..41d191c4f 100644 --- a/src/storm/adapters/EigenAdapter.h +++ b/src/storm/adapters/EigenAdapter.h @@ -3,7 +3,7 @@ #include #include "storm/utility/eigen.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/storage/SparseMatrix.h" diff --git a/src/storm/adapters/HyproAdapter.h b/src/storm/adapters/HyproAdapter.h index 7537b63eb..e8021d1d3 100644 --- a/src/storm/adapters/HyproAdapter.h +++ b/src/storm/adapters/HyproAdapter.h @@ -11,7 +11,7 @@ #include #include -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/storage/geometry/Halfspace.h" namespace storm { diff --git a/src/storm/adapters/CarlAdapter.h b/src/storm/adapters/RationalFunctionAdapter.h similarity index 96% rename from src/storm/adapters/CarlAdapter.h rename to src/storm/adapters/RationalFunctionAdapter.h index 642822b68..ba9858fe0 100644 --- a/src/storm/adapters/CarlAdapter.h +++ b/src/storm/adapters/RationalFunctionAdapter.h @@ -1,6 +1,6 @@ #pragma once -#include "storm/adapters/NumberAdapter.h" +#include "storm/adapters/RationalNumberAdapter.h" #include #include @@ -9,7 +9,6 @@ #include #include #include -#include namespace carl { // Define hash values for all polynomials and rational function. diff --git a/src/storm/adapters/NumberAdapter.h b/src/storm/adapters/RationalNumberAdapter.h similarity index 100% rename from src/storm/adapters/NumberAdapter.h rename to src/storm/adapters/RationalNumberAdapter.h diff --git a/src/storm/adapters/Smt2ExpressionAdapter.h b/src/storm/adapters/Smt2ExpressionAdapter.h index ad72269a6..c61566177 100644 --- a/src/storm/adapters/Smt2ExpressionAdapter.h +++ b/src/storm/adapters/Smt2ExpressionAdapter.h @@ -4,7 +4,7 @@ #include #include "storm-config.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/storage/expressions/Expressions.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/utility/macros.h" diff --git a/src/storm/analysis/GraphConditions.cpp b/src/storm/analysis/GraphConditions.cpp index 0a6b55e57..4f47f15a7 100644 --- a/src/storm/analysis/GraphConditions.cpp +++ b/src/storm/analysis/GraphConditions.cpp @@ -107,7 +107,6 @@ namespace storm { process(dtmc); } - template class ConstraintCollector; } -} \ No newline at end of file +} diff --git a/src/storm/analysis/GraphConditions.h b/src/storm/analysis/GraphConditions.h index 4bcf1a00a..bce7f9837 100644 --- a/src/storm/analysis/GraphConditions.h +++ b/src/storm/analysis/GraphConditions.h @@ -2,9 +2,11 @@ #include #include -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/models/sparse/Dtmc.h" +#include + namespace storm { namespace analysis { @@ -73,4 +75,4 @@ public: } -} \ No newline at end of file +} diff --git a/src/storm/api/bisimulation.h b/src/storm/api/bisimulation.h new file mode 100644 index 000000000..3981caee4 --- /dev/null +++ b/src/storm/api/bisimulation.h @@ -0,0 +1,52 @@ +#pragma once + +#include "storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h" +#include "storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h" + +namespace storm { + namespace api { + + template + std::shared_ptr performDeterministicSparseBisimulationMinimization(std::shared_ptr model, std::vector> const& formulas, storm::storage::BisimulationType type) { + typename storm::storage::DeterministicModelBisimulationDecomposition::Options options; + if (!formulas.empty()) { + options = typename storm::storage::DeterministicModelBisimulationDecomposition::Options(*model, formulas); + } + options.setType(type); + + storm::storage::DeterministicModelBisimulationDecomposition bisimulationDecomposition(*model, options); + bisimulationDecomposition.computeBisimulationDecomposition(); + return bisimulationDecomposition.getQuotient(); + } + + template + std::shared_ptr performNondeterministicSparseBisimulationMinimization(std::shared_ptr model, std::vector> const& formulas, storm::storage::BisimulationType type) { + typename storm::storage::DeterministicModelBisimulationDecomposition::Options options; + if (!formulas.empty()) { + options = typename storm::storage::NondeterministicModelBisimulationDecomposition::Options(*model, formulas); + } + options.setType(type); + + storm::storage::NondeterministicModelBisimulationDecomposition bisimulationDecomposition(*model, options); + bisimulationDecomposition.computeBisimulationDecomposition(); + return bisimulationDecomposition.getQuotient(); + } + + template + std::shared_ptr> performBisimulationMinimization(std::shared_ptr> const& model, std::vector> const& formulas, storm::storage::BisimulationType type = storm::storage::BisimulationType::Strong) { + + STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidSettingsException, "Bisimulation minimization is currently only available for DTMCs, CTMCs and MDPs."); + + model->reduceToStateBasedRewards(); + + if (model->isOfType(storm::models::ModelType::Dtmc)) { + return performDeterministicSparseBisimulationMinimization>(model->template as>(), formulas, type); + } else if (model->isOfType(storm::models::ModelType::Ctmc)) { + return performDeterministicSparseBisimulationMinimization>(model->template as>(), formulas, type); + } else { + return performNondeterministicSparseBisimulationMinimization>(model->template as>(), formulas, type); + } + } + + } +} diff --git a/src/storm/api/builder.h b/src/storm/api/builder.h new file mode 100644 index 000000000..50cf7006e --- /dev/null +++ b/src/storm/api/builder.h @@ -0,0 +1,103 @@ +#pragma once + +#include "storm/builder/DdPrismModelBuilder.h" +#include "storm/builder/DdJaniModelBuilder.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/IOSettings.h" +#include "storm/settings/modules/JitBuilderSettings.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/NotSupportedException.h" + +namespace storm { + namespace api { + + template + std::shared_ptr> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas) { + if (model.isPrismProgram()) { + typename storm::builder::DdPrismModelBuilder::Options options; + options = typename storm::builder::DdPrismModelBuilder::Options(formulas); + + storm::builder::DdPrismModelBuilder builder; + return builder.build(model.asPrismProgram(), options); + } else { + STORM_LOG_THROW(model.isJaniModel(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model for the given symbolic model description."); + typename storm::builder::DdJaniModelBuilder::Options options; + options = typename storm::builder::DdJaniModelBuilder::Options(formulas); + + storm::builder::DdJaniModelBuilder builder; + return builder.build(model.asJaniModel(), options); + } + } + + template<> + std::shared_ptr> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "CUDD does not support rational numbers."); + } + + template<> + std::shared_ptr> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "CUDD does not support rational functions."); + } + + template + std::shared_ptr> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool buildChoiceLabels = false) { + storm::builder::BuilderOptions options(formulas); + + if (storm::settings::getModule().isBuildFullModelSet()) { + options.setBuildAllLabels(); + options.setBuildAllRewardModels(); + options.clearTerminalStates(); + } + options.setBuildChoiceLabels(buildChoiceLabels); + + if (storm::settings::getModule().isJitSet()) { + STORM_LOG_THROW(model.isJaniModel(), storm::exceptions::NotSupportedException, "Cannot use JIT-based model builder for non-JANI model."); + + storm::builder::jit::ExplicitJitJaniModelBuilder builder(model.asJaniModel(), options); + + if (storm::settings::getModule().isDoctorSet()) { + bool result = builder.doctor(); + STORM_LOG_THROW(result, storm::exceptions::InvalidSettingsException, "The JIT-based model builder cannot be used on your system."); + STORM_LOG_INFO("The JIT-based model builder seems to be working."); + } + + return builder.build(); + } else { + std::shared_ptr> generator; + if (model.isPrismProgram()) { + generator = std::make_shared>(model.asPrismProgram(), options); + } else if (model.isJaniModel()) { + generator = std::make_shared>(model.asJaniModel(), options); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot build sparse model from this symbolic model description."); + } + storm::builder::ExplicitModelBuilder builder(generator); + return builder.build(); + } + } + + template + std::shared_ptr> buildExplicitModel(std::string const&, std::string const&, boost::optional const& = boost::none, boost::optional const& = boost::none, boost::optional const& = boost::none) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exact or parametric models with explicit input are not supported."); + } + + template<> + std::shared_ptr> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile, boost::optional const& stateRewardsFile, boost::optional const& transitionRewardsFile, boost::optional const& choiceLabelingFile) { + return storm::parser::AutoParser::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "", choiceLabelingFile ? choiceLabelingFile.get() : "" ); + } + + template + std::shared_ptr> buildExplicitDRNModel(std::string const& drnFile) { + return storm::parser::DirectEncodingParser::parseModel(drnFile); + } + + template<> + inline std::shared_ptr> buildExplicitDRNModel(std::string const&) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exact models with direct encoding are not supported."); + } + + + } +} diff --git a/src/storm/api/counterexamples.h b/src/storm/api/counterexamples.h new file mode 100644 index 000000000..b6c173ab0 --- /dev/null +++ b/src/storm/api/counterexamples.h @@ -0,0 +1,18 @@ +#pragma once + +#include "storm/counterexamples/MILPMinimalLabelSetGenerator.h" +#include "storm/counterexamples/SMTMinimalCommandSetGenerator.h" + +namespace storm { + namespace api { + + std::shared_ptr computePrismHighLevelCounterexampleMilp(storm::prism::Program const& program, std::shared_ptr> mdp, std::shared_ptr const& formula) { + return storm::counterexamples::MILPMinimalLabelSetGenerator::computeCounterexample(program, *mdp, formula); + } + + std::shared_ptr computePrismHighLevelCounterexampleMaxSmt(storm::prism::Program const& program, std::shared_ptr> mdp, std::shared_ptr const& formula) { + return storm::counterexamples::SMTMinimalCommandSetGenerator::computeCounterexample(program, *mdp, formula); + } + + } +} diff --git a/src/storm/api/export.h b/src/storm/api/export.h new file mode 100644 index 000000000..3aa202500 --- /dev/null +++ b/src/storm/api/export.h @@ -0,0 +1,70 @@ +#pragma once + +#include "storm/utility/macros.h" +#include "storm/exceptions/NotSupportedException.h" + +namespace storm { + namespace api { + + void exportJaniModel(storm::jani::Model const& model, std::vector const& properties, std::string const& filename) { + auto janiSettings = storm::settings::getModule(); + + if (janiSettings.isExportAsStandardJaniSet()) { + storm::jani::Model normalisedModel = model; + normalisedModel.makeStandardJaniCompliant(); + storm::jani::JsonExporter::toFile(normalisedModel, properties, filename); + } else { + storm::jani::JsonExporter::toFile(model, properties, filename); + } + } + + void exportJaniModelAsDot(storm::jani::Model const& model, std::string const& filename) { + std::ofstream out; + storm::utility::openFile(filename, out); + model.writeDotToStream(out); + storm::utility::closeFile(out); + } + + template + void exportParametricResultToFile(ValueType const& result, storm::analysis::ConstraintCollector const& constraintCollector, std::string const& path) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot export non-parametric result."); + } + + template <> + void exportParametricResultToFile(storm::RationalFunction const& result, storm::analysis::ConstraintCollector const& constraintCollector, std::string const& path) { + std::ofstream filestream; + storm::utility::openFile(path, filestream); + filestream << "!Parameters: "; + std::set vars = result.gatherVariables(); + std::copy(vars.begin(), vars.end(), std::ostream_iterator(filestream, "; ")); + filestream << std::endl; + filestream << "!Result: " << result << std::endl; + filestream << "!Well-formed Constraints: " << std::endl; + std::vector stringConstraints; + std::transform(constraintCollector.getWellformedConstraints().begin(), constraintCollector.getWellformedConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula const& c) -> std::string { return c.toString();}); + std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator(filestream, "\n")); + filestream << "!Graph-preserving Constraints: " << std::endl; + stringConstraints.clear(); + std::transform(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula const& c) -> std::string { return c.toString();}); + std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator(filestream, "\n")); + storm::utility::closeFile(filestream); + } + + template + void exportSparseModelAsDrn(std::shared_ptr> const& model, std::string const& filename, std::vector const& parameterNames) { + std::ofstream stream; + storm::utility::openFile(filename, stream); + storm::exporter::explicitExportSparseModel(stream, model, parameterNames); + storm::utility::closeFile(stream); + } + + template + void exportSparseModelAsDot(std::shared_ptr> const& model, std::string const& filename) { + std::ofstream stream; + storm::utility::openFile(filename, stream); + model->writeDotToStream(stream); + storm::utility::closeFile(stream); + } + + } +} diff --git a/src/storm/api/model_descriptions.cpp b/src/storm/api/model_descriptions.cpp new file mode 100644 index 000000000..bd1e399f3 --- /dev/null +++ b/src/storm/api/model_descriptions.cpp @@ -0,0 +1,25 @@ +#include "storm/api/model_descriptions.h" + +#include "storm/parser/PrismParser.h" +#include "storm/parser/JaniParser.h" + +#include "storm/storage/jani/Model.h" +#include "storm/storage/jani/Property.h" + +namespace storm { + namespace api { + + storm::prism::Program parseProgram(std::string const& filename) { + storm::prism::Program program = storm::parser::PrismParser::parse(filename).simplify().simplify(); + program.checkValidity(); + return program; + } + + std::pair> parseJaniModel(std::string const& filename) { + std::pair> modelAndFormulae = storm::parser::JaniParser::parse(filename); + modelAndFormulae.first.checkValid(); + return modelAndFormulae; + } + + } +} diff --git a/src/storm/api/model_descriptions.h b/src/storm/api/model_descriptions.h new file mode 100644 index 000000000..99ab5d24d --- /dev/null +++ b/src/storm/api/model_descriptions.h @@ -0,0 +1,22 @@ +#pragma once + +#include +#include + +namespace storm { + namespace prism { + class Program; + } + namespace jani { + class Model; + class Property; + } + + namespace api { + + storm::prism::Program parseProgram(std::string const& filename); + + std::pair> parseJaniModel(std::string const& filename); + + } +} diff --git a/src/storm/api/properties.cpp b/src/storm/api/properties.cpp new file mode 100644 index 000000000..3523c1019 --- /dev/null +++ b/src/storm/api/properties.cpp @@ -0,0 +1,96 @@ +#include "storm/api/properties.h" + +#include "storm/parser/FormulaParser.h" + +#include "storm/storage/SymbolicModelDescription.h" +#include "storm/storage/prism/Program.h" +#include "storm/storage/jani/Model.h" +#include "storm/storage/jani/Property.h" + +#include "storm/utility/cli.h" + +namespace storm { + namespace api { + + boost::optional> parsePropertyFilter(boost::optional const& propertyFilter) { + std::vector propertyNames = storm::utility::cli::parseCommaSeparatedStrings(propertyFilter.get()); + std::set propertyNameSet(propertyNames.begin(), propertyNames.end()); + return propertyNameSet; + } + + std::vector parseProperties(storm::parser::FormulaParser& formulaParser, std::string const& inputString, boost::optional> 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 properties; + if (inputString.find(".") != std::string::npos && std::ifstream(inputString).good()) { + properties = formulaParser.parseFromFile(inputString); + } else { + properties = formulaParser.parseFromString(inputString); + } + + return filterProperties(properties, propertyFilter); + } + + std::vector parseProperties(std::string const& inputString, boost::optional> const& propertyFilter) { + auto exprManager = std::make_shared(); + storm::parser::FormulaParser formulaParser(exprManager); + return parseProperties(formulaParser, inputString, propertyFilter); + } + + std::vector parsePropertiesForJaniModel(std::string const& inputString, storm::jani::Model const& model, boost::optional> const& propertyFilter) { + storm::parser::FormulaParser formulaParser(model.getManager().getSharedPointer()); + auto formulas = parseProperties(formulaParser, inputString, propertyFilter); + return substituteConstantsInProperties(formulas, model.getConstantsSubstitution()); + } + + std::vector parsePropertiesForPrismProgram(std::string const& inputString, storm::prism::Program const& program, boost::optional> const& propertyFilter) { + storm::parser::FormulaParser formulaParser(program); + auto formulas = parseProperties(formulaParser, inputString, propertyFilter); + return substituteConstantsInProperties(formulas, program.getConstantsSubstitution()); + } + + std::vector parsePropertiesForSymbolicModelDescription(std::string const& inputString, storm::storage::SymbolicModelDescription const& modelDescription, boost::optional> const& propertyFilter) { + std::vector result; + if (modelDescription.isPrismProgram()) { + result = storm::api::parsePropertiesForPrismProgram(inputString, modelDescription.asPrismProgram(), propertyFilter); + } else { + STORM_LOG_ASSERT(modelDescription.isJaniModel(), "Unknown model description type."); + result = storm::api::parsePropertiesForJaniModel(inputString, modelDescription.asJaniModel(), propertyFilter); + } + return result; + } + + std::vector substituteConstantsInProperties(std::vector const& properties, std::map const& substitution) { + std::vector preprocessedProperties; + for (auto const& property : properties) { + preprocessedProperties.emplace_back(property.substitute(substitution)); + } + return preprocessedProperties; + } + + std::vector filterProperties(std::vector const& properties, boost::optional> const& propertyFilter) { + if (propertyFilter) { + std::set const& propertyNameSet = propertyFilter.get(); + std::vector result; + std::set reducedPropertyNames; + for (auto const& property : properties) { + if (propertyNameSet.find(property.getName()) != propertyNameSet.end()) { + result.push_back(property); + reducedPropertyNames.insert(property.getName()); + } + } + + if (reducedPropertyNames.size() < propertyNameSet.size()) { + std::set missingProperties; + std::set_difference(propertyNameSet.begin(), propertyNameSet.end(), reducedPropertyNames.begin(), reducedPropertyNames.end(), std::inserter(missingProperties, missingProperties.begin())); + STORM_LOG_WARN("Filtering unknown properties " << boost::join(missingProperties, ", ") << "."); + } + + return result; + } else { + return properties; + } + } + + } +} diff --git a/src/storm/api/properties.h b/src/storm/api/properties.h new file mode 100644 index 000000000..5d2aa6c11 --- /dev/null +++ b/src/storm/api/properties.h @@ -0,0 +1,43 @@ +#pragma once + +#include +#include +#include +#include +#include + +namespace storm { + namespace parser { + class FormulaParser; + } + namespace jani { + class Property; + class Model; + } + namespace expressions { + class Variable; + class Expression; + } + namespace prism { + class Program; + } + namespace storage { + class SymbolicModelDescription; + } + + namespace api { + boost::optional> parsePropertyFilter(boost::optional const& propertyFilter); + + // Parsing properties. + std::vector parseProperties(storm::parser::FormulaParser& formulaParser, std::string const& inputString, boost::optional> const& propertyFilter = boost::none); + std::vector parseProperties(std::string const& inputString, boost::optional> const& propertyFilter = boost::none); + std::vector parsePropertiesForPrismProgram(std::string const& inputString, storm::prism::Program const& program, boost::optional> const& propertyFilter = boost::none); + std::vector parsePropertiesForJaniModel(std::string const& inputString, storm::jani::Model const& model, boost::optional> const& propertyFilter = boost::none); + std::vector parsePropertiesForSymbolicModelDescription(std::string const& inputString, storm::storage::SymbolicModelDescription const& modelDescription, boost::optional> const& propertyFilter = boost::none); + + // Process properties. + std::vector substituteConstantsInProperties(std::vector const& properties, std::map const& substitution); + std::vector filterProperties(std::vector const& properties, boost::optional> const& propertyFilter); + + } +} diff --git a/src/storm/api/storm.h b/src/storm/api/storm.h new file mode 100644 index 000000000..c2856da48 --- /dev/null +++ b/src/storm/api/storm.h @@ -0,0 +1,9 @@ +#pragma once + +#include "storm/api/model_descriptions.h" +#include "storm/api/properties.h" +#include "storm/api/builder.h" +#include "storm/api/bisimulation.h" +#include "storm/api/verification.h" +#include "storm/api/counterexamples.h" +#include "storm/api/export.h" diff --git a/src/storm/api/verification.h b/src/storm/api/verification.h new file mode 100644 index 000000000..f04a05772 --- /dev/null +++ b/src/storm/api/verification.h @@ -0,0 +1,365 @@ +#pragma once + +#include + +#include "storm/modelchecker/abstraction/GameBasedMdpModelChecker.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/NotSupportedException.h" +#include "storm/exceptions/NotImplementedException.h" + +namespace storm { + namespace api { + + template + storm::modelchecker::CheckTask createTask(std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) { + return storm::modelchecker::CheckTask(*formula, onlyInitialStatesRelevant); + } + + template + typename std::enable_if::value, std::unique_ptr>::type verifyWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, storm::modelchecker::CheckTask const& task) { + STORM_LOG_THROW(model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::DTMC || model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::MDP, storm::exceptions::NotSupportedException, "Can only treat DTMCs/MDPs using the abstraction refinement engine."); + + std::unique_ptr result; + if (model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::DTMC) { + storm::modelchecker::GameBasedMdpModelChecker> modelchecker(model); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); + } + } else { + storm::modelchecker::GameBasedMdpModelChecker> modelchecker(model); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); + } + } + return result; + } + + template + typename std::enable_if::value, std::unique_ptr>::type verifyWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const&, storm::modelchecker::CheckTask const&) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Abstraction-refinement engine does not support data type."); + } + + template + typename std::enable_if::value, std::unique_ptr>::type verifyWithExplorationEngine(storm::storage::SymbolicModelDescription const& model, storm::modelchecker::CheckTask const& task) { + STORM_LOG_THROW(model.isPrismProgram(), storm::exceptions::InvalidSettingsException, "Exploration engine is currently only applicable to PRISM models."); + storm::prism::Program const& program = model.asPrismProgram(); + STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Currently exploration-based verification is only available for DTMCs and MDPs."); + + std::unique_ptr result; + if (program.getModelType() == storm::prism::Program::ModelType::DTMC) { + storm::modelchecker::SparseExplorationModelChecker> checker(program); + if (checker.canHandle(task)) { + result = checker.check(task); + } + } else { + storm::modelchecker::SparseExplorationModelChecker> checker(program); + if (checker.canHandle(task)) { + result = checker.check(task); + } + } + return result; + } + + template + typename std::enable_if::value, std::unique_ptr>::type verifyWithExplorationEngine(storm::storage::SymbolicModelDescription const&, storm::modelchecker::CheckTask const&) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exploration engine does not support data type."); + } + + template + std::unique_ptr verifyWithSparseEngine(std::shared_ptr> const& dtmc, storm::modelchecker::CheckTask const& task) { + std::unique_ptr result; + if (storm::settings::getModule().getEquationSolver() == storm::solver::EquationSolverType::Elimination && storm::settings::getModule().isUseDedicatedModelCheckerSet()) { + storm::modelchecker::SparseDtmcEliminationModelChecker> modelchecker(*dtmc); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); + } + } else { + storm::modelchecker::SparseDtmcPrctlModelChecker> modelchecker(*dtmc); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); + } + } + return result; + } + + template + std::unique_ptr verifyWithSparseEngine(std::shared_ptr> const& ctmc, storm::modelchecker::CheckTask const& task) { + std::unique_ptr result; + storm::modelchecker::SparseCtmcCslModelChecker> modelchecker(*ctmc); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); + } + return result; + } + + template + typename std::enable_if::value, std::unique_ptr>::type verifyWithSparseEngine(std::shared_ptr> const& mdp, storm::modelchecker::CheckTask const& task) { + std::unique_ptr result; + storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(*mdp); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); + } + return result; + } + + template + typename std::enable_if::value, std::unique_ptr>::type verifyWithSparseEngine(std::shared_ptr> const&, storm::modelchecker::CheckTask const&) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sparse engine cannot verify MDPs with this data type."); + } + + template + typename std::enable_if::value, std::unique_ptr>::type verifyWithSparseEngine(std::shared_ptr> const& ma, storm::modelchecker::CheckTask const& task) { + std::unique_ptr result; + + // Close the MA, if it is not already closed. + if (!ma->isClosed()) { + STORM_LOG_WARN("Closing Markov automaton. Consider closing the MA before verification."); + ma->close(); + } + + storm::modelchecker::SparseMarkovAutomatonCslModelChecker> modelchecker(*ma); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); + } + return result; + } + + template + typename std::enable_if::value, std::unique_ptr>::type verifyWithSparseEngine(std::shared_ptr> const& ma, storm::modelchecker::CheckTask const& task) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sparse engine cannot verify MAs with this data type."); + } + + template + std::unique_ptr verifyWithSparseEngine(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { + std::unique_ptr result; + if (model->getType() == storm::models::ModelType::Dtmc) { + result = verifyWithSparseEngine(model->template as>(), task); + } else if (model->getType() == storm::models::ModelType::Mdp) { + result = verifyWithSparseEngine(model->template as>(), task); + } else if (model->getType() == storm::models::ModelType::Ctmc) { + result = verifyWithSparseEngine(model->template as>(), task); + } else if (model->getType() == storm::models::ModelType::MarkovAutomaton) { + result = verifyWithSparseEngine(model->template as>(), task); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type " << model->getType() << " is not supported."); + } + return result; + } + + template + std::unique_ptr verifyWithHybridEngine(std::shared_ptr> const& dtmc, storm::modelchecker::CheckTask const& task) { + std::unique_ptr result; + storm::modelchecker::HybridDtmcPrctlModelChecker> modelchecker(*dtmc); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); + } + return result; + } + + template + std::unique_ptr verifyWithHybridEngine(std::shared_ptr> const& ctmc, storm::modelchecker::CheckTask const& task) { + std::unique_ptr result; + storm::modelchecker::HybridCtmcCslModelChecker> modelchecker(*ctmc); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); + } + return result; + } + + template + typename std::enable_if::value, std::unique_ptr>::type verifyWithHybridEngine(std::shared_ptr> const& mdp, storm::modelchecker::CheckTask const& task) { + std::unique_ptr result; + storm::modelchecker::HybridMdpPrctlModelChecker> modelchecker(*mdp); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); + } + return result; + } + + template + typename std::enable_if::value, std::unique_ptr>::type verifyWithHybridEngine(std::shared_ptr> const&, storm::modelchecker::CheckTask const&) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Hybrid engine cannot verify MDPs with this data type."); + } + + template + std::unique_ptr verifyWithHybridEngine(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { + std::unique_ptr result; + if (model->getType() == storm::models::ModelType::Dtmc) { + result = verifyWithHybridEngine(model->template as>(), task); + } else if (model->getType() == storm::models::ModelType::Ctmc) { + result = verifyWithHybridEngine(model->template as>(), task); + } else if (model->getType() == storm::models::ModelType::Mdp) { + result = verifyWithHybridEngine(model->template as>(), task); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type is not supported by the hybrid engine."); + } + return result; + } + + template + std::unique_ptr verifyWithDdEngine(std::shared_ptr> const& dtmc, storm::modelchecker::CheckTask const& task) { + std::unique_ptr result; + storm::modelchecker::SymbolicDtmcPrctlModelChecker> modelchecker(*dtmc); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); + } + return result; + } + + template + typename std::enable_if::value, std::unique_ptr>::type verifyWithDdEngine(std::shared_ptr> const& mdp, storm::modelchecker::CheckTask const& task) { + std::unique_ptr result; + storm::modelchecker::SymbolicMdpPrctlModelChecker> modelchecker(*mdp); + if (modelchecker.canHandle(task)) { + result = modelchecker.check(task); + } + return result; + } + + template + typename std::enable_if::value, std::unique_ptr>::type verifyWithDdEngine(std::shared_ptr> const&, storm::modelchecker::CheckTask const&) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Dd engine cannot verify MDPs with this data type."); + } + + template + std::unique_ptr verifyWithDdEngine(std::shared_ptr> const& model, storm::modelchecker::CheckTask const& task) { + std::unique_ptr result; + if (model->getType() == storm::models::ModelType::Dtmc) { + result = verifyWithDdEngine(model->template as>(), task); + } else if (model->getType() == storm::models::ModelType::Mdp) { + result = verifyWithDdEngine(model->template as>(), task); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The model type is not supported by the dd engine."); + } + return result; + } + + template + std::unique_ptr verifyWithParameterLifting(std::shared_ptr>, std::shared_ptr const&) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter-lifting is unavailable for this data-type."); + } + + template<> + std::unique_ptr verifyWithParameterLifting(std::shared_ptr> markovModel, std::shared_ptr const& formula) { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Parameter-lifting is currently unavailable from the API."); +// storm::utility::Stopwatch parameterLiftingStopWatch(true); +// std::shared_ptr consideredFormula = formula; +// +// STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(markovModel, formula), "Could not validate whether parameter lifting is sound on the input model and the formula " << *formula); +// +// if (markovModel->isOfType(storm::models::ModelType::Ctmc) || markovModel->isOfType(storm::models::ModelType::MarkovAutomaton)) { +// STORM_PRINT_AND_LOG("Transforming continuous model to discrete model..."); +// storm::transformer::transformContinuousToDiscreteModelInPlace(markovModel, consideredFormula); +// STORM_PRINT_AND_LOG(" done!" << std::endl); +// markovModel->printModelInformationToStream(std::cout); +// } +// +// auto modelParameters = storm::models::sparse::getProbabilityParameters(*markovModel); +// auto rewParameters = storm::models::sparse::getRewardParameters(*markovModel); +// modelParameters.insert(rewParameters.begin(), rewParameters.end()); +// +// STORM_LOG_THROW(storm::settings::getModule().isParameterSpaceSet(), storm::exceptions::InvalidSettingsException, "Invoked Parameter lifting but no parameter space was defined."); +// auto parameterSpaceAsString = storm::settings::getModule().getParameterSpace(); +// auto parameterSpace = storm::storage::ParameterRegion::parseRegion(parameterSpaceAsString, modelParameters); +// auto refinementThreshold = storm::utility::convertNumber::CoefficientType>(storm::settings::getModule().getRefinementThreshold()); +// std::vector, storm::modelchecker::parametric::RegionCheckResult>> result; +// +// STORM_PRINT_AND_LOG("Performing parameter lifting for property " << *consideredFormula << " with parameter space " << parameterSpace.toString(true) << " and refinement threshold " << storm::utility::convertNumber(refinementThreshold) << " ..." << std::endl); +// +// storm::modelchecker::CheckTask task(*consideredFormula, true); +// std::string resultVisualization; +// +// if (markovModel->isOfType(storm::models::ModelType::Dtmc)) { +// if (storm::settings::getModule().isExactSet()) { +// storm::modelchecker::parametric::SparseDtmcRegionChecker , storm::RationalNumber> regionChecker(*markovModel->template as>()); +// regionChecker.specifyFormula(task); +// result = regionChecker.performRegionRefinement(parameterSpace, refinementThreshold); +// parameterLiftingStopWatch.stop(); +// if (modelParameters.size() == 2) { +// resultVisualization = regionChecker.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin())); +// } +// } else { +// storm::modelchecker::parametric::SparseDtmcRegionChecker , double, storm::RationalNumber> regionChecker(*markovModel->template as>()); +// regionChecker.specifyFormula(task); +// result = regionChecker.performRegionRefinement(parameterSpace, refinementThreshold); +// parameterLiftingStopWatch.stop(); +// if (modelParameters.size() == 2) { +// resultVisualization = regionChecker.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin())); +// } +// } +// } else if (markovModel->isOfType(storm::models::ModelType::Mdp)) { +// if (storm::settings::getModule().isExactSet()) { +// storm::modelchecker::parametric::SparseMdpRegionChecker, storm::RationalNumber> regionChecker(*markovModel->template as>()); +// regionChecker.specifyFormula(task); +// result = regionChecker.performRegionRefinement(parameterSpace, refinementThreshold); +// parameterLiftingStopWatch.stop(); +// if (modelParameters.size() == 2) { +// resultVisualization = regionChecker.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin())); +// } +// } else { +// storm::modelchecker::parametric::SparseMdpRegionChecker, double, storm::RationalNumber> regionChecker(*markovModel->template as>()); +// regionChecker.specifyFormula(task); +// result = regionChecker.performRegionRefinement(parameterSpace, refinementThreshold); +// parameterLiftingStopWatch.stop(); +// if (modelParameters.size() == 2) { +// resultVisualization = regionChecker.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin())); +// } +// } +// } else { +// STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to perform parameterLifting on the provided model type."); +// } +// +// +// auto satArea = storm::utility::zero::CoefficientType>(); +// auto unsatArea = storm::utility::zero::CoefficientType>(); +// uint_fast64_t numOfSatRegions = 0; +// uint_fast64_t numOfUnsatRegions = 0; +// for (auto const& res : result) { +// switch (res.second) { +// case storm::modelchecker::parametric::RegionCheckResult::AllSat: +// satArea += res.first.area(); +// ++numOfSatRegions; +// break; +// case storm::modelchecker::parametric::RegionCheckResult::AllViolated: +// unsatArea += res.first.area(); +// ++numOfUnsatRegions; +// break; +// default: +// STORM_LOG_ERROR("Unexpected result for region " << res.first.toString(true) << " : " << res.second << "."); +// break; +// } +// } +// typename storm::storage::ParameterRegion::CoefficientType satAreaFraction = satArea / parameterSpace.area(); +// typename storm::storage::ParameterRegion::CoefficientType unsatAreaFraction = unsatArea / parameterSpace.area(); +// STORM_PRINT_AND_LOG("Done! Found " << numOfSatRegions << " safe regions and " +// << numOfUnsatRegions << " unsafe regions." << std::endl); +// STORM_PRINT_AND_LOG(storm::utility::convertNumber(satAreaFraction) * 100 << "% of the parameter space is safe, and " +// << storm::utility::convertNumber(unsatAreaFraction) * 100 << "% of the parameter space is unsafe." << std::endl); +// STORM_PRINT_AND_LOG("Model checking with parameter lifting took " << parameterLiftingStopWatch << " seconds." << std::endl); +// STORM_PRINT_AND_LOG(resultVisualization); +// +// if (storm::settings::getModule().exportResultToFile()) { +// std::string path = storm::settings::getModule().exportResultPath(); +// STORM_PRINT_AND_LOG("Exporting result to path " << path << "." << std::endl); +// std::ofstream filestream; +// storm::utility::openFile(path, filestream); +// +// for (auto const& res : result) { +// switch (res.second) { +// case storm::modelchecker::parametric::RegionCheckResult::AllSat: +// filestream << "safe: " << res.first.toString(true) << std::endl; +// break; +// case storm::modelchecker::parametric::RegionCheckResult::AllViolated: +// filestream << "unsafe: " << res.first.toString(true) << std::endl; +// break; +// default: +// break; +// } +// } +// } +// } + } + + } +} diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index 6ea6e4470..6e56e9c68 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/src/storm/builder/DdJaniModelBuilder.cpp @@ -40,7 +40,7 @@ #include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/NotSupportedException.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace builder { diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp index b0749616d..410472354 100644 --- a/src/storm/builder/DdPrismModelBuilder.cpp +++ b/src/storm/builder/DdPrismModelBuilder.cpp @@ -26,7 +26,7 @@ #include "storm/settings/modules/CoreSettings.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace builder { diff --git a/src/storm/builder/RewardModelBuilder.cpp b/src/storm/builder/RewardModelBuilder.cpp index 75dece593..6db3c50fb 100644 --- a/src/storm/builder/RewardModelBuilder.cpp +++ b/src/storm/builder/RewardModelBuilder.cpp @@ -1,6 +1,6 @@ #include "storm/builder/RewardModelBuilder.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/models/sparse/StandardRewardModel.h" diff --git a/src/storm/builder/jit/Choice.cpp b/src/storm/builder/jit/Choice.cpp index 67078e9c8..9d4f42f2a 100644 --- a/src/storm/builder/jit/Choice.cpp +++ b/src/storm/builder/jit/Choice.cpp @@ -1,6 +1,6 @@ #include "storm/builder/jit/Choice.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/constants.h" diff --git a/src/storm/builder/jit/Distribution.cpp b/src/storm/builder/jit/Distribution.cpp index cd3534478..29a0a1075 100644 --- a/src/storm/builder/jit/Distribution.cpp +++ b/src/storm/builder/jit/Distribution.cpp @@ -1,6 +1,6 @@ #include "storm/builder/jit/Distribution.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace builder { diff --git a/src/storm/builder/jit/DistributionEntry.cpp b/src/storm/builder/jit/DistributionEntry.cpp index e00d9d2f7..352908d4e 100644 --- a/src/storm/builder/jit/DistributionEntry.cpp +++ b/src/storm/builder/jit/DistributionEntry.cpp @@ -1,6 +1,6 @@ #include "storm/builder/jit/DistributionEntry.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace builder { diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp index 3135fe4a0..48b83e965 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -372,7 +372,7 @@ namespace storm { std::string problem = "Unable to compile program using Carl data structures. Is Carls's include directory '" + carlIncludeDirectory + "' set correctly?"; try { std::string program = R"( -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" int main() { return 0; @@ -1651,10 +1651,10 @@ namespace storm { #include {% if exact %} -#include "storm/adapters/NumberAdapter.h" +#include "storm/adapters/RationalNumberAdapter.h" {% endif %} {% if parametric %} -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" {% endif %} #include "resources/3rdparty/sparsepp/sparsepp.h" diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h index 65321ad9f..9e4cea5f5 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h @@ -8,7 +8,7 @@ #include "cpptempl.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/storage/jani/Model.h" #include "storm/storage/jani/ParallelComposition.h" diff --git a/src/storm/builder/jit/JitModelBuilderInterface.cpp b/src/storm/builder/jit/JitModelBuilderInterface.cpp index 97446f196..3c79c64fe 100644 --- a/src/storm/builder/jit/JitModelBuilderInterface.cpp +++ b/src/storm/builder/jit/JitModelBuilderInterface.cpp @@ -1,6 +1,6 @@ #include "storm/builder/jit/JitModelBuilderInterface.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace builder { diff --git a/src/storm/builder/jit/StateBehaviour.cpp b/src/storm/builder/jit/StateBehaviour.cpp index 40cf06895..b732032cd 100644 --- a/src/storm/builder/jit/StateBehaviour.cpp +++ b/src/storm/builder/jit/StateBehaviour.cpp @@ -1,6 +1,6 @@ #include "storm/builder/jit/StateBehaviour.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/constants.h" diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp index 181a67480..644421c2c 100644 --- a/src/storm/cli/cli.cpp +++ b/src/storm/cli/cli.cpp @@ -1,11 +1,11 @@ -#include "cli.h" -#include "entrypoints.h" +#include "storm/cli/cli.h" +#include "storm/cli/entrypoints.h" -#include "../utility/storm.h" +#include "storm/utility/storm.h" #include "storm/storage/SymbolicModelDescription.h" - +#include "storm/models/ModelBase.h" #include "storm/settings/modules/DebugSettings.h" #include "storm/settings/modules/IOSettings.h" @@ -17,7 +17,18 @@ #include "storm/utility/resources.h" #include "storm/utility/file.h" #include "storm/utility/storm-version.h" +#include "storm/utility/cli.h" + +#include "storm/utility/initialize.h" +#include "storm/utility/Stopwatch.h" + +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/ResourceSettings.h" + +#include + +#include "storm/utility/macros.h" // Includes for the linked libraries and versions header. #ifdef STORM_HAVE_INTELTBB @@ -46,11 +57,29 @@ namespace storm { namespace cli { - std::string getCurrentWorkingDirectory() { - char temp[512]; - return (GetCurrentDir(temp, 512 - 1) ? std::string(temp) : std::string("")); + + int64_t process(const int argc, const char** argv) { + storm::utility::setUp(); + storm::cli::printHeader("Storm", argc, argv); + storm::settings::initializeAll("Storm", "storm"); + + storm::utility::Stopwatch totalTimer(true); + if (!storm::cli::parseOptions(argc, argv)) { + return -1; + } + + processOptions(); + + totalTimer.stop(); + if (storm::settings::getModule().isPrintTimeAndMemorySet()) { + storm::cli::printTimeAndMemoryStatistics(totalTimer.getTimeInMilliseconds()); + } + + storm::utility::cleanUp(); + return 0; } + void printHeader(std::string const& name, const int argc, const char* argv[]) { STORM_PRINT(name << " " << storm::utility::StormVersion::shortVersionString() << std::endl << std::endl); @@ -64,7 +93,7 @@ namespace storm { if (!command.empty()) { STORM_PRINT("Command line arguments: " << commandStream.str() << std::endl); - STORM_PRINT("Current working directory: " << getCurrentWorkingDirectory() << std::endl << std::endl); + STORM_PRINT("Current working directory: " << storm::utility::cli::getCurrentWorkingDirectory() << std::endl << std::endl); } } @@ -135,26 +164,6 @@ namespace storm { #endif } - 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. - uint64_t maximumResidentSizeInMegabytes = ru.ru_maxrss / 1024 / 1024; -#endif -#ifdef LINUX - // For Linux, this is returned in kilobytes. - uint64_t maximumResidentSizeInMegabytes = ru.ru_maxrss / 1024; -#endif - std::cout << " * peak memory usage: " << maximumResidentSizeInMegabytes << "MB" << std::endl; - std::cout << " * CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << "s" << std::endl; - if (wallclockMilliseconds != 0) { - 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); @@ -165,22 +174,33 @@ namespace storm { } storm::settings::modules::GeneralSettings const& general = storm::settings::getModule(); - storm::settings::modules::ResourceSettings const& resources = storm::settings::getModule(); - storm::settings::modules::DebugSettings const& debug = storm::settings::getModule(); - + + bool result = true; if (general.isHelpSet()) { storm::settings::manager().printHelp(storm::settings::getModule().getHelpModuleName()); - return false; - } - // If we were given a time limit, we put it in place now. - if (resources.isTimeoutSet()) { - storm::utility::resources::setCPULimit(resources.getTimeoutInSeconds()); + result = false; } if (general.isVersionSet()) { printVersion("storm"); - return false; + result = false;; } + + return result; + } + + void setResourceLimits() { + storm::settings::modules::ResourceSettings const& resources = storm::settings::getModule(); + + // If we were given a time limit, we put it in place now. + if (resources.isTimeoutSet()) { + storm::utility::resources::setCPULimit(resources.getTimeoutInSeconds()); + } + } + + void setLogLevel() { + storm::settings::modules::GeneralSettings const& general = storm::settings::getModule(); + storm::settings::modules::DebugSettings const& debug = storm::settings::getModule(); if (general.isVerboseSet()) { storm::utility::setLogLevel(l3pp::LogLevel::INFO); @@ -194,147 +214,603 @@ namespace storm { if (debug.isLogfileSet()) { storm::utility::initializeFileLogging(); } - return true; } - void processOptions() { - STORM_LOG_TRACE("Processing options."); - if (storm::settings::getModule().isLogfileSet()) { + void setFileLogging() { + storm::settings::modules::DebugSettings const& debug = storm::settings::getModule(); + if (debug.isLogfileSet()) { storm::utility::initializeFileLogging(); } - + } + + void setUrgentOptions() { + setResourceLimits(); + setLogLevel(); + setFileLogging(); + } + + void rest(); + + boost::optional> parsePropertyFilter(storm::settings::modules::IOSettings const& ioSettings) { boost::optional> propertyFilter; - std::string propertyFilterString = storm::settings::getModule().getPropertyFilter(); + std::string propertyFilterString = ioSettings.getPropertyFilter(); if (propertyFilterString != "all") { - propertyFilter = storm::parsePropertyFilter(storm::settings::getModule().getPropertyFilter()); + propertyFilter = storm::parsePropertyFilter(propertyFilterString); } + return propertyFilter; + } + + struct SymbolicInput { + // The symbolic model description. + boost::optional model; - auto coreSettings = storm::settings::getModule(); - auto generalSettings = storm::settings::getModule(); - auto ioSettings = storm::settings::getModule(); + // The properties to check. + std::vector properties; + }; + + void parseSymbolicModelDescription(storm::settings::modules::IOSettings const& ioSettings, SymbolicInput& input) { if (ioSettings.isPrismOrJaniInputSet()) { - storm::storage::SymbolicModelDescription model; - std::vector properties; - - STORM_LOG_TRACE("Parsing symbolic input."); - boost::optional> labelRenaming; if (ioSettings.isPrismInputSet()) { - model = storm::parseProgram(ioSettings.getPrismInputFilename()); - - bool transformToJani = ioSettings.isPrismToJaniSet(); - bool transformToJaniForJit = coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse && ioSettings.isJitSet(); - STORM_LOG_WARN_COND(transformToJani || !transformToJaniForJit, "The JIT-based model builder is only available for JANI models, automatically converting the PRISM input model."); - transformToJani |= transformToJaniForJit; + input.model = storm::api::parseProgram(ioSettings.getPrismInputFilename()); + } else { + auto janiInput = storm::api::parseJaniModel(ioSettings.getJaniInputFilename()); + input.model = janiInput.first; + auto const& janiPropertyInput = janiInput.second; - if (transformToJani) { - auto modelAndRenaming = model.toJaniWithLabelRenaming(true); - if (!modelAndRenaming.second.empty()) { - labelRenaming = modelAndRenaming.second; - } - model = modelAndRenaming.first; - } - } else if (ioSettings.isJaniInputSet()) { - auto input = storm::parseJaniModel(ioSettings.getJaniInputFilename()); - model = input.first; if (ioSettings.isJaniPropertiesSet()) { for (auto const& propName : ioSettings.getJaniProperties()) { - STORM_LOG_THROW(input.second.count(propName) == 1, storm::exceptions::InvalidArgumentException, "No property with name " << propName << " known."); - properties.push_back(input.second.at(propName)); + auto propertyIt = janiPropertyInput.find(propName); + STORM_LOG_THROW(propertyIt != janiPropertyInput.end(), storm::exceptions::InvalidArgumentException, "No JANI property with name '" << propName << "' is known."); + input.properties.emplace_back(propertyIt->second); } } - - if(ioSettings.isExportJaniDotSet()) { - std::ofstream out; - storm::utility::openFile(ioSettings.getExportJaniDotFilename(), out); - model.asJaniModel().writeDotToStream(out); - storm::utility::closeFile(out); - } - + } + } + } + + void parseProperties(storm::settings::modules::IOSettings const& ioSettings, SymbolicInput& input, boost::optional> const& propertyFilter) { + if (ioSettings.isPropertySet()) { + std::vector newProperties; + if (input.model) { + newProperties = storm::api::parsePropertiesForSymbolicModelDescription(ioSettings.getProperty(), input.model.get(), propertyFilter); + } else { + newProperties = storm::api::parseProperties(ioSettings.getProperty(), propertyFilter); } - // Get the string that assigns values to the unknown currently undefined constants in the model and formula. - std::string constantDefinitionString = ioSettings.getConstantDefinitionString(); - std::map constantDefinitions; + input.properties.insert(input.properties.end(), newProperties.begin(), newProperties.end()); + } + } + + SymbolicInput parseSymbolicInput() { + auto ioSettings = storm::settings::getModule(); + + // Parse the property filter, if any is given. + boost::optional> propertyFilter = parsePropertyFilter(ioSettings); + + SymbolicInput input; + parseSymbolicModelDescription(ioSettings, input); + parseProperties(ioSettings, input, propertyFilter); + + return input; + } + + SymbolicInput preprocessSymbolicInput(SymbolicInput const& input) { + auto ioSettings = storm::settings::getModule(); + auto coreSettings = storm::settings::getModule(); + + SymbolicInput output = input; + + // Substitute constant definitions in symbolic input. + std::string constantDefinitionString = ioSettings.getConstantDefinitionString(); + std::map constantDefinitions; + if (output.model) { + constantDefinitions = output.model.get().parseConstantDefinitions(constantDefinitionString); + output.model.get().preprocess(constantDefinitions); + } + if (!output.properties.empty()) { + output.properties = substituteConstantsInProperties(output.properties, constantDefinitions); + } + + // Check whether conversion for PRISM to JANI is requested or necessary. + if (input.model && input.model.get().isPrismProgram()) { + bool transformToJani = ioSettings.isPrismToJaniSet(); + bool transformToJaniForJit = coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse && ioSettings.isJitSet(); + STORM_LOG_WARN_COND(transformToJani || !transformToJaniForJit, "The JIT-based model builder is only available for JANI models, automatically converting the PRISM input model."); + transformToJani |= transformToJaniForJit; - // 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()) { - if (model.isJaniModel()) { - properties = storm::parsePropertiesForJaniModel(ioSettings.getProperty(), model.asJaniModel(), propertyFilter); - - if (labelRenaming) { - std::vector amendedProperties; - for (auto const& property : properties) { - amendedProperties.emplace_back(property.substituteLabels(labelRenaming.get())); - } - properties = std::move(amendedProperties); + if (transformToJani) { + SymbolicInput output; + + storm::prism::Program const& model = output.model.get().asPrismProgram(); + auto modelAndRenaming = model.toJaniWithLabelRenaming(true); + output.model = modelAndRenaming.first; + + if (!modelAndRenaming.second.empty()) { + std::map const& labelRenaming = modelAndRenaming.second; + std::vector amendedProperties; + for (auto const& property : output.properties) { + amendedProperties.emplace_back(property.substituteLabels(labelRenaming)); } + output.properties = std::move(amendedProperties); + } + } + } + + return output; + } + + void exportSymbolicInput(SymbolicInput const& input) { + auto ioSettings = storm::settings::getModule(); + if (input.model && input.model.get().isJaniModel()) { + storm::storage::SymbolicModelDescription const& model = input.model.get(); + if (ioSettings.isExportJaniDotSet()) { + storm::api::exportJaniModelAsDot(model.asJaniModel(), ioSettings.getExportJaniDotFilename()); + } + + if (model.isJaniModel() && storm::settings::getModule().isJaniFileSet()) { + storm::api::exportJaniModel(model.asJaniModel(), input.properties, storm::settings::getModule().getJaniFilename()); + } + } + } + + SymbolicInput parseAndPreprocessSymbolicInput() { + SymbolicInput input = parseSymbolicInput(); + input = preprocessSymbolicInput(input); + exportSymbolicInput(input); + return input; + } + + template + std::shared_ptr buildModelDd(SymbolicInput const& input) { + return storm::api::buildSymbolicModel(input.model.get(), extractFormulasFromProperties(input.properties)); + } + + template + std::shared_ptr buildModelSparse(SymbolicInput const& input) { + auto counterexampleGeneratorSettings = storm::settings::getModule(); + return storm::api::buildSparseModel(input.model.get(), extractFormulasFromProperties(input.properties), counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet()); + } + + template + std::shared_ptr buildModelExplicit(storm::settings::modules::IOSettings const& ioSettings) { + std::shared_ptr result; + if (ioSettings.isExplicitSet()) { + result = storm::api::buildExplicitModel(ioSettings.getTransitionFilename(), ioSettings.getLabelingFilename(), ioSettings.isStateRewardsSet() ? boost::optional(ioSettings.getStateRewardsFilename()) : boost::none, ioSettings.isTransitionRewardsSet() ? boost::optional(ioSettings.getTransitionRewardsFilename()) : boost::none, ioSettings.isChoiceLabelingSet() ? boost::optional(ioSettings.getChoiceLabelingFilename()) : boost::none); + } else { + result = storm::api::buildExplicitDRNModel(ioSettings.getExplicitDRNFilename()); + } + return result; + } + + template + std::shared_ptr buildModel(storm::settings::modules::CoreSettings::Engine const& engine, SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) { + storm::utility::Stopwatch modelBuildingWatch(true); + + std::shared_ptr result; + if (input.model) { + if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid) { + result = buildModelDd(input); + } else if (engine == storm::settings::modules::CoreSettings::Engine::Sparse) { + result = buildModelSparse(input); + } + } else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet()) { + STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Can only use sparse engine with explicit input."); + result = buildModelExplicit(ioSettings); + } + + modelBuildingWatch.stop(); + if (result) { + STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl); + } + + return result; + } + + template + std::shared_ptr> preprocessSparseMarkovAutomaton(std::shared_ptr> const& model) { + std::shared_ptr> result = model; + model->close(); + if (model->hasOnlyTrivialNondeterminism()) { + result = model->convertToCTMC(); + } + return result; + } + + template + std::shared_ptr> preprocessSparseModelBisimulation(std::shared_ptr> const& model, SymbolicInput const& input, storm::settings::modules::BisimulationSettings const& bisimulationSettings) { + storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong; + if (bisimulationSettings.isWeakBisimulationSet()) { + bisimType = storm::storage::BisimulationType::Weak; + } + + STORM_LOG_INFO("Performing bisimulation minimization..."); + return storm::api::performBisimulationMinimization(model, extractFormulasFromProperties(input.properties), bisimType); + } + + template + std::pair>, bool> preprocessSparseModel(std::shared_ptr> const& model, SymbolicInput const& input) { + auto generalSettings = storm::settings::getModule(); + auto bisimulationSettings = storm::settings::getModule(); + auto ioSettings = storm::settings::getModule(); + + std::pair>, bool> result = std::make_pair(model, false); + + if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) { + result.first = preprocessSparseMarkovAutomaton(result.first->template as>()); + result.second = true; + } + + if (generalSettings.isBisimulationSet()) { + result.first = preprocessSparseModelBisimulation(result.first, input, bisimulationSettings); + result.second = true; + } + + return result; + } + + template + void exportSparseModel(std::shared_ptr> const& model, SymbolicInput const& input) { + auto ioSettings = storm::settings::getModule(); + + if (ioSettings.isExportExplicitSet()) { + storm::api::exportSparseModelAsDrn(model, ioSettings.getExportExplicitFilename(), input.model ? input.model.get().getParameterNames() : std::vector()); + } + + if (ioSettings.isExportDotSet()) { + storm::api::exportSparseModelAsDot(model, ioSettings.getExportDotFilename()); + } + } + + template + void exportDdModel(std::shared_ptr> const& model, SymbolicInput const& input) { + // Intentionally left empty. + } + + template + void exportModel(std::shared_ptr const& model, SymbolicInput const& input) { + if (model->isSparseModel()) { + exportSparseModel(model->as>(), input); + } else { + exportDdModel(model->as>(), input); + } + } + + template + std::pair, bool> preprocessDdModel(std::shared_ptr> const& model, SymbolicInput const& input) { + return std::make_pair(model, false); + } + + template + std::pair, bool> preprocessModel(std::shared_ptr const& model, SymbolicInput const& input) { + storm::utility::Stopwatch preprocessingWatch(true); + + std::pair, bool> result = std::make_pair(model, false); + if (model->isSparseModel()) { + result = preprocessSparseModel(result.first->as>(), input); + } else { + STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type."); + result = preprocessDdModel(result.first->as>(), input); + } + + if (result.second) { + STORM_PRINT_AND_LOG(std::endl << "Time for model preprocessing: " << preprocessingWatch << "." << std::endl); + } + return result; + } + + void printComputingCounterexample(storm::jani::Property const& property) { + STORM_PRINT_AND_LOG("Computing counterexample for property " << *property.getRawFormula() << " ..." << std::endl); + } + + void printCounterexample(std::shared_ptr const& counterexample, storm::utility::Stopwatch* watch = nullptr) { + if (counterexample) { + STORM_PRINT_AND_LOG(counterexample << std::endl); + if (watch) { + STORM_PRINT_AND_LOG("Time for computation: " << *watch << "." << std::endl); + } + } else { + STORM_PRINT_AND_LOG(" failed." << std::endl); + } + } + + template + void generateCounterexamples(std::shared_ptr const& model, SymbolicInput const& input) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Counterexample generation is not supported for this data-type."); + } + + template <> + void generateCounterexamples(std::shared_ptr const& model, SymbolicInput const& input) { + typedef double ValueType; + + STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::NotSupportedException, "Counterexample generation is currently only supported for sparse models."); + auto sparseModel = model->as>(); + + STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "Counterexample is currently only supported for MDPs."); + auto mdp = sparseModel->template as>(); + + auto counterexampleSettings = storm::settings::getModule(); + if (counterexampleSettings.isMinimalCommandSetGenerationSet()) { + STORM_LOG_THROW(input.model && input.model.get().isPrismProgram(), storm::exceptions::NotSupportedException, "Minimal command set counterexamples are only supported for PRISM model input."); + storm::prism::Program const& program = input.model.get().asPrismProgram(); + + bool useMilp = counterexampleSettings.isUseMilpBasedMinimalCommandSetGenerationSet(); + for (auto const& property : input.properties) { + std::shared_ptr counterexample; + printComputingCounterexample(property); + storm::utility::Stopwatch watch(true); + if (useMilp) { + counterexample = storm::api::computePrismHighLevelCounterexampleMilp(program, mdp, property.getRawFormula()); } else { - properties = storm::parsePropertiesForPrismProgram(ioSettings.getProperty(), model.asPrismProgram(), propertyFilter); + counterexample = storm::api::computePrismHighLevelCounterexampleMaxSmt(program, mdp, property.getRawFormula()); } - - constantDefinitions = model.parseConstantDefinitions(constantDefinitionString); - properties = substituteConstantsInProperties(properties, constantDefinitions); - } else { - constantDefinitions = model.parseConstantDefinitions(constantDefinitionString); + watch.stop(); + printCounterexample(counterexample, &watch); } + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The selected counterexample formalism is unsupported."); + } + } + + template + void printFilteredResult(std::unique_ptr const& result, storm::modelchecker::FilterType ft) { + if (result->isQuantitative()) { + switch (ft) { + case storm::modelchecker::FilterType::VALUES: + STORM_PRINT_AND_LOG(*result); + break; + case storm::modelchecker::FilterType::SUM: + STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult().sum()); + break; + case storm::modelchecker::FilterType::AVG: + STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult().average()); + break; + case storm::modelchecker::FilterType::MIN: + STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult().getMin()); + break; + case storm::modelchecker::FilterType::MAX: + STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult().getMax()); + break; + case storm::modelchecker::FilterType::ARGMIN: + case storm::modelchecker::FilterType::ARGMAX: + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Outputting states is not supported."); + case storm::modelchecker::FilterType::EXISTS: + case storm::modelchecker::FilterType::FORALL: + case storm::modelchecker::FilterType::COUNT: + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Filter type only defined for qualitative results."); + } + } else { + switch (ft) { + case storm::modelchecker::FilterType::VALUES: + STORM_PRINT_AND_LOG(*result << std::endl); + break; + case storm::modelchecker::FilterType::EXISTS: + STORM_PRINT_AND_LOG(result->asQualitativeCheckResult().existsTrue()); + break; + case storm::modelchecker::FilterType::FORALL: + STORM_PRINT_AND_LOG(result->asQualitativeCheckResult().forallTrue()); + break; + case storm::modelchecker::FilterType::COUNT: + STORM_PRINT_AND_LOG(result->asQualitativeCheckResult().count()); + break; + case storm::modelchecker::FilterType::ARGMIN: + case storm::modelchecker::FilterType::ARGMAX: + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Outputting states is not supported."); + case storm::modelchecker::FilterType::SUM: + case storm::modelchecker::FilterType::AVG: + case storm::modelchecker::FilterType::MIN: + case storm::modelchecker::FilterType::MAX: + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Filter type only defined for quantitative results."); + } + } + STORM_PRINT_AND_LOG(std::endl); + } + + void printModelCheckingProperty(storm::jani::Property const& property) { + STORM_PRINT_AND_LOG(std::endl << "Model checking property " << *property.getRawFormula() << " ..." << std::endl); + } - if (model.isJaniModel() && storm::settings::getModule().isJaniFileSet()) { - exportJaniModel(model.asJaniModel(), properties, storm::settings::getModule().getJaniFilename()); + template + void printInitialStatesResult(std::unique_ptr const& result, storm::jani::Property const& property, storm::utility::Stopwatch* watch = nullptr) { + if (result) { + STORM_PRINT_AND_LOG("Result (initial states): "); + printFilteredResult(result, property.getFilter().getFilterType()); + if (watch) { + STORM_PRINT_AND_LOG("Time for model checking: " << *watch << "." << std::endl); } + } else { + STORM_PRINT_AND_LOG(" failed, property is unsupported by selected engine/settings." << std::endl); + } + } + + template + void verifyProperties(std::vector const& properties, std::function(std::shared_ptr const& formula)> const& verificationCallback, std::function const&)> const& postprocessingCallback = [](std::unique_ptr const&){}) { + for (auto const& property : properties) { + printModelCheckingProperty(property); + storm::utility::Stopwatch watch(true); + std::unique_ptr result = verificationCallback(property.getRawFormula()); + watch.stop(); + printInitialStatesResult(result, property, &watch); + postprocessingCallback(result); + } + } + + template + void verifyWithAbstractionRefinementEngine(SymbolicInput const& input) { + STORM_LOG_ASSERT(input.model, "Expected symbolic model description."); + verifyProperties(input.properties, [&input] (std::shared_ptr const& formula) { + return storm::api::verifyWithAbstractionRefinementEngine(input.model.get(), storm::api::createTask(formula, true)); + }); + } - model = model.preprocess(constantDefinitions); - + template + void verifyWithExplorationEngine(SymbolicInput const& input) { + STORM_LOG_ASSERT(input.model, "Expected symbolic model description."); + STORM_LOG_THROW((std::is_same::value), storm::exceptions::NotSupportedException, "Exploration does not support other data-types than floating points."); + verifyProperties(input.properties, [&input] (std::shared_ptr const& formula) { + return storm::api::verifyWithExplorationEngine(input.model.get(), storm::api::createTask(formula, true)); + }); + } + + template + void verifyWithSparseEngine(std::shared_ptr const& model, SymbolicInput const& input) { + auto sparseModel = model->as>(); + verifyProperties(input.properties, + [&sparseModel] (std::shared_ptr const& formula) { + std::unique_ptr result = storm::api::verifyWithSparseEngine(sparseModel, storm::api::createTask(formula, true)); + result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(sparseModel->getInitialStates())); + return result; + }, + [&sparseModel] (std::unique_ptr const& result) { + if (std::is_same::value && sparseModel->isOfType(storm::models::ModelType::Dtmc) && storm::settings::getModule().exportResultToFile()) { + auto dtmc = sparseModel->template as>(); + storm::api::exportParametricResultToFile(result->asExplicitQuantitativeCheckResult()[*sparseModel->getInitialStates().begin()], storm::analysis::ConstraintCollector(*dtmc), storm::settings::getModule().exportResultPath()); + } + }); + } + + template + void verifyWithHybridEngine(std::shared_ptr const& model, SymbolicInput const& input) { + verifyProperties(input.properties, [&model] (std::shared_ptr const& formula) { + auto symbolicModel = model->as>(); + std::unique_ptr result = storm::api::verifyWithHybridEngine(symbolicModel, storm::api::createTask(formula, true)); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(symbolicModel->getReachableStates(), symbolicModel->getInitialStates())); + return result; + }); + } + + template + void verifyWithDdEngine(std::shared_ptr const& model, SymbolicInput const& input) { + verifyProperties(input.properties, [&model] (std::shared_ptr const& formula) { + auto symbolicModel = model->as>(); + std::unique_ptr result = storm::api::verifyWithDdEngine(model->as>(), storm::api::createTask(formula, true)); + result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(symbolicModel->getReachableStates(), symbolicModel->getInitialStates())); + return result; + }); + } + + template + typename std::enable_if::value, void>::type verifySymbolicModel(std::shared_ptr const& model, SymbolicInput const& input, storm::settings::modules::CoreSettings const& coreSettings) { + bool hybrid = coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Hybrid; + if (hybrid) { + verifyWithHybridEngine(model, input); + } else { + verifyWithDdEngine(model, input); + } + } + template + typename std::enable_if::value, void>::type verifySymbolicModel(std::shared_ptr const& model, SymbolicInput const& input, storm::settings::modules::CoreSettings const& coreSettings) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "CUDD does not support the selected data-type."); + } + + template + void verifyModel(std::shared_ptr const& model, SymbolicInput const& input, storm::settings::modules::CoreSettings const& coreSettings) { + if (model->isSparseModel()) { + verifyWithSparseEngine(model, input); + } else { + STORM_LOG_ASSERT(model->isSymbolicModel(), "Unexpected model type."); + verifySymbolicModel(model, input, coreSettings); + } + } + + template + void processInputWithValueTypeAndDdlib(SymbolicInput const& input) { + auto coreSettings = storm::settings::getModule(); + + // For several engines, no model building step is performed, but the verification is started right away. + storm::settings::modules::CoreSettings::Engine engine = coreSettings.getEngine(); + if (engine == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement) { + verifyWithAbstractionRefinementEngine(input); + } else if (engine == storm::settings::modules::CoreSettings::Engine::Exploration) { + verifyWithExplorationEngine(input); + } else { + auto ioSettings = storm::settings::getModule(); - if (ioSettings.isNoBuildModelSet()) { - return; + std::shared_ptr model; + if (!ioSettings.isNoBuildModelSet()) { + model = buildModel(engine, input, ioSettings); } - STORM_LOG_TRACE("Building and checking symbolic model."); - if (generalSettings.isParametricSet()) { -#ifdef STORM_HAVE_CARL - buildAndCheckSymbolicModel(model, properties, true); -#else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No parameters are supported in this build."); -#endif - } else if (generalSettings.isExactSet()) { -#ifdef STORM_HAVE_CARL - buildAndCheckSymbolicModel(model, properties, true); -#else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No exact numbers are supported in this build."); -#endif - } else { - buildAndCheckSymbolicModel(model, properties, true); + if (model) { + model->printModelInformationToStream(std::cout); } - } else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet()) { - 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 properties; - if (ioSettings.isPropertySet()) { - properties = storm::parsePropertiesForExplicit(ioSettings.getProperty(), propertyFilter); + STORM_LOG_THROW(model || input.properties.empty(), storm::exceptions::InvalidSettingsException, "No input model."); + + if (model) { + auto preprocessingResult = preprocessModel(model, input); + if (preprocessingResult.second) { + model = preprocessingResult.first; + model->printModelInformationToStream(std::cout); + } } - - if (generalSettings.isParametricSet()) { + + if (model) { + exportModel(model, input); + + if (coreSettings.isCounterexampleSet()) { + generateCounterexamples(model, input); + } else { + verifyModel(model, input, coreSettings); + } + } + } + } + + template + void processInputWithValueType(SymbolicInput const& input) { + auto coreSettings = storm::settings::getModule(); + + if (coreSettings.getDdLibraryType() == storm::dd::DdType::CUDD) { + processInputWithValueTypeAndDdlib(input); + } else { + STORM_LOG_ASSERT(coreSettings.getDdLibraryType() == storm::dd::DdType::Sylvan, "Unknown DD library."); + processInputWithValueTypeAndDdlib(input); + } + } + + void processOptions() { + // Start by setting some urgent options (log levels, resources, etc.) + setUrgentOptions(); + + // Parse and preprocess symbolic input (PRISM, JANI, properties, etc.) + SymbolicInput symbolicInput = parseAndPreprocessSymbolicInput(); + + auto generalSettings = storm::settings::getModule(); + if (generalSettings.isParametricSet()) { #ifdef STORM_HAVE_CARL - buildAndCheckExplicitModel(properties, true); + processInputWithValueType(symbolicInput); #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No parameters are supported in this build."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No parameters are supported in this build."); #endif - } else if (generalSettings.isExactSet()) { + } else if (generalSettings.isExactSet()) { #ifdef STORM_HAVE_CARL - buildAndCheckExplicitModel(properties, true); + processInputWithValueType(symbolicInput); #else - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No exact numbers are supported in this build."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No exact numbers are supported in this build."); #endif - } else { - buildAndCheckExplicitModel(properties, true); - } } else { + processInputWithValueType(symbolicInput); + } + } - STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); + void printTimeAndMemoryStatistics(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. + uint64_t maximumResidentSizeInMegabytes = ru.ru_maxrss / 1024 / 1024; +#endif +#ifdef LINUX + // For Linux, this is returned in kilobytes. + uint64_t maximumResidentSizeInMegabytes = ru.ru_maxrss / 1024; +#endif + std::cout << " * peak memory usage: " << maximumResidentSizeInMegabytes << "MB" << std::endl; + std::cout << " * CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << "s" << std::endl; + if (wallclockMilliseconds != 0) { + std::cout << " * wallclock time: " << (wallclockMilliseconds/1000) << "." << std::setw(3) << std::setfill('0') << (wallclockMilliseconds % 1000) << "s" << std::endl; } } diff --git a/src/storm/cli/cli.h b/src/storm/cli/cli.h index 3fd41e914..4decbb02c 100644 --- a/src/storm/cli/cli.h +++ b/src/storm/cli/cli.h @@ -5,14 +5,17 @@ namespace storm { namespace cli { - - std::string getCurrentWorkingDirectory(); - + + /*! + * Processes the options and returns the exit code. + */ + int64_t process(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); + void printTimeAndMemoryStatistics(uint64_t wallclockMilliseconds = 0); /*! * Parses the given command line arguments. @@ -22,8 +25,9 @@ namespace storm { * @return True iff the program should continue to run after parsing the options. */ bool parseOptions(const int argc, const char* argv[]); - + void processOptions(); + } } diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h index 5c04891eb..001ec3992 100644 --- a/src/storm/cli/entrypoints.h +++ b/src/storm/cli/entrypoints.h @@ -9,6 +9,8 @@ #include "storm/utility/DirectEncodingExporter.h" #include "storm/utility/Stopwatch.h" +#include "storm/api/storm.h" + #include "storm/exceptions/NotImplementedException.h" #include "storm/exceptions/InvalidSettingsException.h" #include "storm/exceptions/UnexpectedException.h" @@ -125,7 +127,7 @@ namespace storm { STORM_PRINT_AND_LOG(std::endl << "Model checking property " << *property.getRawFormula() << " ..." << std::endl); std::cout.flush(); storm::utility::Stopwatch modelCheckingWatch(true); - std::unique_ptr result(storm::verifySymbolicModelWithAbstractionRefinementEngine(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); + std::unique_ptr result(storm::api::verifyWithAbstractionRefinementEngine(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); modelCheckingWatch.stop(); if (result) { STORM_PRINT_AND_LOG("Result (initial states): "); @@ -281,7 +283,7 @@ namespace storm { void buildAndCheckSymbolicModelWithSymbolicEngine(bool hybrid, storm::storage::SymbolicModelDescription const& model, std::vector const& properties, bool onlyInitialStatesRelevant = false) { // Start by building the model. storm::utility::Stopwatch modelBuildingWatch(true); - auto markovModel = buildSymbolicModel(model, extractFormulasFromProperties(properties)); + auto markovModel = storm::api::buildSymbolicModel(model, extractFormulasFromProperties(properties)); modelBuildingWatch.stop(); STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl << std::endl); @@ -311,7 +313,7 @@ namespace storm { auto formulas = extractFormulasFromProperties(properties); // Start by building the model. storm::utility::Stopwatch modelBuildingWatch(true); - std::shared_ptr markovModel = buildSparseModel(model, formulas); + std::shared_ptr markovModel = storm::api::buildSparseModel(model, formulas); modelBuildingWatch.stop(); STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl << std::endl); @@ -419,9 +421,9 @@ namespace storm { storm::utility::Stopwatch modelBuildingWatch(true); std::shared_ptr model; if (settings.isExplicitSet()) { - model = buildExplicitModel(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? boost::optional(settings.getStateRewardsFilename()) : boost::none, settings.isTransitionRewardsSet() ? boost::optional(settings.getTransitionRewardsFilename()) : boost::none, settings.isChoiceLabelingSet() ? boost::optional(settings.getChoiceLabelingFilename()) : boost::none); + model = api::buildExplicitModel(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? boost::optional(settings.getStateRewardsFilename()) : boost::none, settings.isTransitionRewardsSet() ? boost::optional(settings.getTransitionRewardsFilename()) : boost::none, settings.isChoiceLabelingSet() ? boost::optional(settings.getChoiceLabelingFilename()) : boost::none); } else { - model = buildExplicitDRNModel(settings.getExplicitDRNFilename()); + model = api::buildExplicitDRNModel(settings.getExplicitDRNFilename()); } modelBuildingWatch.stop(); STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl); diff --git a/src/storm/counterexamples/Counterexample.cpp b/src/storm/counterexamples/Counterexample.cpp new file mode 100644 index 000000000..4aba71b9c --- /dev/null +++ b/src/storm/counterexamples/Counterexample.cpp @@ -0,0 +1,12 @@ +#include "storm/counterexamples/Counterexample.h" + +namespace storm { + namespace counterexamples { + + std::ostream& operator<<(std::ostream& out, Counterexample const& counterexample) { + counterexample.writeToStream(out); + return out; + } + + } +} diff --git a/src/storm/counterexamples/Counterexample.h b/src/storm/counterexamples/Counterexample.h new file mode 100644 index 000000000..8cd93178d --- /dev/null +++ b/src/storm/counterexamples/Counterexample.h @@ -0,0 +1,16 @@ +#pragma once + +#include + +namespace storm { + namespace counterexamples { + + class Counterexample { + public: + virtual void writeToStream(std::ostream& out) const = 0; + }; + + std::ostream& operator<<(std::ostream& out, Counterexample const& counterexample); + + } +} diff --git a/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h b/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h index 537b844d6..d3ffa682f 100644 --- a/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h @@ -14,6 +14,8 @@ #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/InvalidStateException.h" +#include "storm/counterexamples/PrismHighLevelCounterexample.h" + #include "storm/utility/graph.h" #include "storm/utility/counterexamples.h" #include "storm/utility/solver.h" @@ -968,7 +970,7 @@ namespace storm { * @param formulaPtr A pointer to a safety formula. The outermost operator must be a probabilistic bound operator with a strict upper bound. The nested * formula can be either an unbounded until formula or an eventually formula. */ - static void computeCounterexample(storm::prism::Program const& program, storm::models::sparse::Mdp const& labeledMdp, std::shared_ptr const& formula) { + static std::shared_ptr computeCounterexample(storm::prism::Program const& program, storm::models::sparse::Mdp const& labeledMdp, std::shared_ptr const& formula) { std::cout << std::endl << "Generating minimal label counterexample for formula " << *formula << std::endl; STORM_LOG_THROW(formula->isProbabilityOperatorFormula(), storm::exceptions::InvalidPropertyException, "Counterexample generation does not support this kind of formula. Expecting a probability operator as the outermost formula element."); @@ -1013,10 +1015,7 @@ namespace storm { auto endTime = std::chrono::high_resolution_clock::now(); std::cout << std::endl << "Computed minimal label set of size " << usedLabelSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; - std::cout << "Resulting program:" << std::endl; - storm::prism::Program restrictedProgram = program.restrictCommands(usedLabelSet); - std::cout << restrictedProgram << std::endl; - std::cout << std::endl << "-------------------------------------------" << std::endl; + return std::make_shared(program.restrictCommands(usedLabelSet)); } }; diff --git a/src/storm/counterexamples/PrismHighLevelCounterexample.cpp b/src/storm/counterexamples/PrismHighLevelCounterexample.cpp new file mode 100644 index 000000000..ae0e7fb06 --- /dev/null +++ b/src/storm/counterexamples/PrismHighLevelCounterexample.cpp @@ -0,0 +1,16 @@ +#include "storm/counterexamples/PrismHighLevelCounterexample.h" + +namespace storm { + namespace counterexamples { + + PrismHighLevelCounterexample::PrismHighLevelCounterexample(storm::prism::Program const& program) : program(program) { + // Intentionally left empty. + } + + void PrismHighLevelCounterexample::writeToStream(std::ostream& out) const { + out << "High-level counterexample (PRISM program): " << std::endl; + out << program; + } + + } +} diff --git a/src/storm/counterexamples/PrismHighLevelCounterexample.h b/src/storm/counterexamples/PrismHighLevelCounterexample.h new file mode 100644 index 000000000..3e3de71c2 --- /dev/null +++ b/src/storm/counterexamples/PrismHighLevelCounterexample.h @@ -0,0 +1,21 @@ +#pragma once + +#include "storm/counterexamples/Counterexample.h" + +#include "storm/storage/prism/Program.h" + +namespace storm { + namespace counterexamples { + + class PrismHighLevelCounterexample : public Counterexample { + public: + PrismHighLevelCounterexample(storm::prism::Program const& program); + + void writeToStream(std::ostream& out) const override; + + private: + storm::prism::Program program; + }; + + } +} diff --git a/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h b/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h index 6359d04a6..6a8a77ab2 100644 --- a/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h @@ -6,6 +6,8 @@ #include "storm/solver/Z3SmtSolver.h" +#include "storm/counterexamples/PrismHighLevelCounterexample.h" + #include "storm/storage/prism/Program.h" #include "storm/storage/expressions/Expression.h" #include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" @@ -1583,7 +1585,6 @@ namespace storm { * Computes the minimal command set that is needed in the given MDP to exceed the given probability threshold for satisfying phi until psi. * * @param program The program that was used to build the MDP. - * @param constantDefinitionString A string defining the undefined constants in the given program. * @param labeledMdp The MDP in which to find the minimal command set. * @param phiStates A bit vector characterizing all phi states in the model. * @param psiStates A bit vector characterizing all psi states in the model. @@ -1593,7 +1594,7 @@ namespace storm { * @param checkThresholdFeasible If set, it is verified that the model can actually achieve/exceed the given probability value. If this check * is made and fails, an exception is thrown. */ - static boost::container::flat_set getMinimalCommandSet(storm::prism::Program program, std::string const& constantDefinitionString, storm::models::sparse::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeReachabilityEncoding = false) { + static boost::container::flat_set getMinimalCommandSet(storm::prism::Program program, storm::models::sparse::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeReachabilityEncoding = false) { #ifdef STORM_HAVE_Z3 // Set up all clocks used for time measurement. auto totalClock = std::chrono::high_resolution_clock::now(); @@ -1612,10 +1613,6 @@ namespace storm { auto analysisClock = std::chrono::high_resolution_clock::now(); decltype(std::chrono::high_resolution_clock::now() - analysisClock) totalAnalysisTime(0); - std::map constantDefinitions = storm::utility::cli::parseConstantDefinitionString(program.getManager(), constantDefinitionString); - storm::prism::Program preparedProgram = program.defineUndefinedConstants(constantDefinitions); - preparedProgram = preparedProgram.substituteConstants(); - // (0) Check whether the MDP is indeed labeled. if (!labeledMdp.hasChoiceLabeling()) { throw storm::exceptions::InvalidArgumentException() << "Minimal command set generation is impossible for unlabeled model."; @@ -1655,7 +1652,7 @@ namespace storm { STORM_LOG_DEBUG("Asserting cuts."); assertExplicitCuts(labeledMdp, psiStates, variableInformation, relevancyInformation, *solver); STORM_LOG_DEBUG("Asserted explicit cuts."); - assertSymbolicCuts(preparedProgram, labeledMdp, variableInformation, relevancyInformation, *solver); + assertSymbolicCuts(program, labeledMdp, variableInformation, relevancyInformation, *solver); STORM_LOG_DEBUG("Asserted symbolic cuts."); if (includeReachabilityEncoding) { assertReachabilityCuts(labeledMdp, psiStates, variableInformation, relevancyInformation, *solver); @@ -1749,7 +1746,7 @@ namespace storm { #endif } - static void computeCounterexample(storm::prism::Program program, std::string const& constantDefinitionString, storm::models::sparse::Mdp const& labeledMdp, std::shared_ptr const& formula) { + static std::shared_ptr computeCounterexample(storm::prism::Program program, storm::models::sparse::Mdp const& labeledMdp, std::shared_ptr const& formula) { #ifdef STORM_HAVE_Z3 std::cout << std::endl << "Generating minimal label counterexample for formula " << *formula << std::endl; @@ -1791,15 +1788,11 @@ namespace storm { // Delegate the actual computation work to the function of equal name. auto startTime = std::chrono::high_resolution_clock::now(); - auto labelSet = getMinimalCommandSet(program, constantDefinitionString, labeledMdp, phiStates, psiStates, threshold, strictBound, true, storm::settings::getModule().isEncodeReachabilitySet()); + auto labelSet = getMinimalCommandSet(program, labeledMdp, phiStates, psiStates, threshold, strictBound, true, storm::settings::getModule().isEncodeReachabilitySet()); auto endTime = std::chrono::high_resolution_clock::now(); std::cout << std::endl << "Computed minimal label set of size " << labelSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; - std::cout << "Resulting program:" << std::endl << std::endl; - storm::prism::Program restrictedProgram = program.restrictCommands(labelSet); - std::cout << restrictedProgram << std::endl; - std::cout << std::endl << "-------------------------------------------" << std::endl; - + return std::make_shared(program.restrictCommands(labelSet)); #else throw storm::exceptions::NotImplementedException() << "This functionality is unavailable since storm has been compiled without support for Z3."; #endif diff --git a/src/storm/generator/Choice.cpp b/src/storm/generator/Choice.cpp index cddf12f0f..feeb090ad 100644 --- a/src/storm/generator/Choice.cpp +++ b/src/storm/generator/Choice.cpp @@ -1,6 +1,6 @@ #include "storm/generator/Choice.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/constants.h" diff --git a/src/storm/generator/NextStateGenerator.cpp b/src/storm/generator/NextStateGenerator.cpp index 7f931051f..16212cbe8 100644 --- a/src/storm/generator/NextStateGenerator.cpp +++ b/src/storm/generator/NextStateGenerator.cpp @@ -1,6 +1,6 @@ #include "storm/generator/NextStateGenerator.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/logic/Formulas.h" diff --git a/src/storm/generator/StateBehavior.cpp b/src/storm/generator/StateBehavior.cpp index 54158970d..d7464b2cd 100644 --- a/src/storm/generator/StateBehavior.cpp +++ b/src/storm/generator/StateBehavior.cpp @@ -1,6 +1,6 @@ #include "storm/generator/StateBehavior.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace generator { diff --git a/src/storm/logic/OperatorFormula.cpp b/src/storm/logic/OperatorFormula.cpp index 6ee6a6270..3b0fbcd1c 100644 --- a/src/storm/logic/OperatorFormula.cpp +++ b/src/storm/logic/OperatorFormula.cpp @@ -1,6 +1,6 @@ #include "storm/logic/OperatorFormula.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/exceptions/InvalidOperationException.h" diff --git a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp index 399b0ed46..16574947f 100644 --- a/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/HybridCtmcCslModelChecker.cpp @@ -133,6 +133,7 @@ namespace storm { template class HybridCtmcCslModelChecker>; template class HybridCtmcCslModelChecker>; + template class HybridCtmcCslModelChecker>; } // namespace modelchecker } // namespace storm diff --git a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 1f5c9ee0d..5de82a7d1 100644 --- a/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseCtmcCslModelChecker.cpp @@ -15,7 +15,7 @@ #include "storm/logic/FragmentSpecification.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/InvalidPropertyException.h" diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index 1dff5b454..e0cd132ee 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -12,7 +12,7 @@ #include "storm/storage/StronglyConnectedComponentDecomposition.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/macros.h" #include "storm/utility/vector.h" diff --git a/src/storm/modelchecker/hints/ExplicitModelCheckerHint.cpp b/src/storm/modelchecker/hints/ExplicitModelCheckerHint.cpp index 8ad0015b4..b68ab9508 100644 --- a/src/storm/modelchecker/hints/ExplicitModelCheckerHint.cpp +++ b/src/storm/modelchecker/hints/ExplicitModelCheckerHint.cpp @@ -1,5 +1,5 @@ #include "storm/modelchecker/hints/ExplicitModelCheckerHint.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/macros.h" #include "storm/exceptions/InvalidOperationException.h" @@ -119,4 +119,4 @@ namespace storm { template class ExplicitModelCheckerHint; } -} \ No newline at end of file +} diff --git a/src/storm/modelchecker/hints/ModelCheckerHint.cpp b/src/storm/modelchecker/hints/ModelCheckerHint.cpp index 31f016857..50bb38ad0 100644 --- a/src/storm/modelchecker/hints/ModelCheckerHint.cpp +++ b/src/storm/modelchecker/hints/ModelCheckerHint.cpp @@ -1,6 +1,6 @@ #include "storm/modelchecker/hints/ModelCheckerHint.h" #include "storm/modelchecker/hints/ExplicitModelCheckerHint.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace modelchecker { @@ -31,4 +31,4 @@ namespace storm { template ExplicitModelCheckerHint& ModelCheckerHint::asExplicitModelCheckerHint(); } -} \ No newline at end of file +} diff --git a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp index 24b67bc03..86faf88a7 100644 --- a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp +++ b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.cpp @@ -1,6 +1,6 @@ #include "storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" diff --git a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.cpp b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.cpp index 99855e790..baac53b0e 100644 --- a/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.cpp +++ b/src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.cpp @@ -1,6 +1,6 @@ #include "storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp index e70f89bbc..9064acc97 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp @@ -2,7 +2,7 @@ #include -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/utility/macros.h" diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp index 01ea6f616..40d843f93 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp @@ -1,6 +1,6 @@ #include "storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/utility/macros.h" diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp index fcf6ca98e..74e646103 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp @@ -1,6 +1,6 @@ #include "storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp index 488e3667b..21e41614c 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp @@ -1,6 +1,6 @@ #include "storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp index d648ae593..c459ce7df 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp @@ -1,6 +1,6 @@ #include "storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp index 7ef64df2e..9276613b1 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp @@ -1,6 +1,6 @@ #include "storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp index 3087ef7a1..497bce790 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.cpp @@ -2,7 +2,7 @@ #include -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" diff --git a/src/storm/modelchecker/parametric/RegionChecker.cpp b/src/storm/modelchecker/parametric/RegionChecker.cpp index 3ded35806..163e28b7a 100644 --- a/src/storm/modelchecker/parametric/RegionChecker.cpp +++ b/src/storm/modelchecker/parametric/RegionChecker.cpp @@ -3,7 +3,7 @@ #include "storm/modelchecker/parametric/RegionChecker.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" diff --git a/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp index 87b4a02a4..b652f6e60 100644 --- a/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp @@ -1,6 +1,6 @@ #include "storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" @@ -256,4 +256,4 @@ namespace storm { } } -} \ No newline at end of file +} diff --git a/src/storm/modelchecker/parametric/SparseDtmcRegionChecker.cpp b/src/storm/modelchecker/parametric/SparseDtmcRegionChecker.cpp index c9a841964..97d9d1973 100644 --- a/src/storm/modelchecker/parametric/SparseDtmcRegionChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseDtmcRegionChecker.cpp @@ -1,6 +1,6 @@ #include "storm/modelchecker/parametric/SparseDtmcRegionChecker.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.h" #include "storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.h" diff --git a/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.cpp b/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.cpp index 9b8991689..1a7a004d4 100644 --- a/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.cpp @@ -1,6 +1,6 @@ #include "SparseInstantiationModelChecker.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -41,4 +41,4 @@ namespace storm { } } -} \ No newline at end of file +} diff --git a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp index d9e2610fe..6d9bc4d36 100644 --- a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp @@ -1,6 +1,6 @@ #include "storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" diff --git a/src/storm/modelchecker/parametric/SparseMdpRegionChecker.cpp b/src/storm/modelchecker/parametric/SparseMdpRegionChecker.cpp index 9ee9422ff..e61201415 100644 --- a/src/storm/modelchecker/parametric/SparseMdpRegionChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseMdpRegionChecker.cpp @@ -1,6 +1,6 @@ #include "storm/modelchecker/parametric/SparseMdpRegionChecker.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.h" #include "storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.h" diff --git a/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.cpp b/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.cpp index 1c8ffa269..8c9af8957 100644 --- a/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.cpp @@ -1,6 +1,6 @@ #include "SparseParameterLiftingModelChecker.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/logic/FragmentSpecification.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" @@ -91,4 +91,4 @@ namespace storm { } } -} \ No newline at end of file +} diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h index 0d4e603d5..357fb07b5 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h @@ -11,7 +11,7 @@ #include "storm/utility/solver.h" #include "storm/solver/SolveGoal.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace storage { diff --git a/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp b/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp index 89486ef3b..ac2b371bd 100644 --- a/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp +++ b/src/storm/modelchecker/propositional/SparsePropositionalModelChecker.cpp @@ -1,6 +1,6 @@ #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Ctmc.h" diff --git a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index dd467f6d0..77d482333 100644 --- a/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -4,7 +4,7 @@ #include #include -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/settings/modules/EliminationSettings.h" #include "storm/settings/modules/CoreSettings.h" diff --git a/src/storm/modelchecker/results/CheckResult.cpp b/src/storm/modelchecker/results/CheckResult.cpp index 45f286df0..bdcf68c8f 100644 --- a/src/storm/modelchecker/results/CheckResult.cpp +++ b/src/storm/modelchecker/results/CheckResult.cpp @@ -1,7 +1,7 @@ #include "storm/modelchecker/results/CheckResult.h" #include "storm-config.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" diff --git a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp index 9294cd627..83568b1c8 100644 --- a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp @@ -1,7 +1,7 @@ #include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/utility/macros.h" #include "storm/utility/vector.h" diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index 2614ef459..31bb67b5d 100644 --- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -7,7 +7,7 @@ #include "storm/utility/vector.h" #include "storm/exceptions/InvalidOperationException.h" #include "storm/exceptions/InvalidAccessException.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { diff --git a/src/storm/modelchecker/results/ParetoCurveCheckResult.cpp b/src/storm/modelchecker/results/ParetoCurveCheckResult.cpp index a76857576..26679181a 100644 --- a/src/storm/modelchecker/results/ParetoCurveCheckResult.cpp +++ b/src/storm/modelchecker/results/ParetoCurveCheckResult.cpp @@ -1,6 +1,6 @@ #include "storm/modelchecker/results/ParetoCurveCheckResult.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/vector.h" namespace storm { diff --git a/src/storm/modelchecker/results/QuantitativeCheckResult.cpp b/src/storm/modelchecker/results/QuantitativeCheckResult.cpp index f068ef7d6..2a7fc4211 100644 --- a/src/storm/modelchecker/results/QuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/QuantitativeCheckResult.cpp @@ -1,7 +1,7 @@ #include "storm/modelchecker/results/QuantitativeCheckResult.h" #include "storm-config.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/macros.h" #include "storm/exceptions/InvalidOperationException.h" diff --git a/src/storm/modelchecker/results/SymbolicParetoCurveCheckResult.cpp b/src/storm/modelchecker/results/SymbolicParetoCurveCheckResult.cpp index 37c8e3678..a2db3593a 100644 --- a/src/storm/modelchecker/results/SymbolicParetoCurveCheckResult.cpp +++ b/src/storm/modelchecker/results/SymbolicParetoCurveCheckResult.cpp @@ -1,7 +1,7 @@ #include "storm/modelchecker/results/SymbolicParetoCurveCheckResult.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "storm/utility/macros.h" #include "storm/storage/dd/DdManager.h" diff --git a/src/storm/models/sparse/Ctmc.cpp b/src/storm/models/sparse/Ctmc.cpp index a43aded44..6389ed7fb 100644 --- a/src/storm/models/sparse/Ctmc.cpp +++ b/src/storm/models/sparse/Ctmc.cpp @@ -1,6 +1,6 @@ #include "storm/models/sparse/Ctmc.h" #include "storm/models/sparse/StandardRewardModel.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/macros.h" namespace storm { diff --git a/src/storm/models/sparse/DeterministicModel.cpp b/src/storm/models/sparse/DeterministicModel.cpp index de37f1fa3..0756b69bb 100644 --- a/src/storm/models/sparse/DeterministicModel.cpp +++ b/src/storm/models/sparse/DeterministicModel.cpp @@ -1,7 +1,7 @@ #include "storm/models/sparse/DeterministicModel.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/utility/constants.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace models { diff --git a/src/storm/models/sparse/Dtmc.cpp b/src/storm/models/sparse/Dtmc.cpp index 319a06ee9..30b6d8ae2 100644 --- a/src/storm/models/sparse/Dtmc.cpp +++ b/src/storm/models/sparse/Dtmc.cpp @@ -1,6 +1,6 @@ #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/StandardRewardModel.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/exceptions/NotImplementedException.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/utility/constants.h" diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp index 88a77b43d..3f645b928 100644 --- a/src/storm/models/sparse/MarkovAutomaton.cpp +++ b/src/storm/models/sparse/MarkovAutomaton.cpp @@ -1,6 +1,6 @@ #include "storm/models/sparse/MarkovAutomaton.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/solver/stateelimination/StateEliminator.h" #include "storm/storage/FlexibleSparseMatrix.h" diff --git a/src/storm/models/sparse/Mdp.cpp b/src/storm/models/sparse/Mdp.cpp index 394ed75d4..a84d7ef01 100644 --- a/src/storm/models/sparse/Mdp.cpp +++ b/src/storm/models/sparse/Mdp.cpp @@ -3,7 +3,7 @@ #include "storm/exceptions/InvalidArgumentException.h" #include "storm/utility/constants.h" #include "storm/utility/vector.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/models/sparse/StandardRewardModel.h" diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp index d75065299..a923765cb 100644 --- a/src/storm/models/sparse/Model.cpp +++ b/src/storm/models/sparse/Model.cpp @@ -5,7 +5,7 @@ #include "storm/models/sparse/StandardRewardModel.h" #include "storm/utility/vector.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/NumberTraits.h" #include "storm/exceptions/IllegalArgumentException.h" diff --git a/src/storm/models/sparse/NondeterministicModel.cpp b/src/storm/models/sparse/NondeterministicModel.cpp index 7f221cabe..d0dfa056a 100644 --- a/src/storm/models/sparse/NondeterministicModel.cpp +++ b/src/storm/models/sparse/NondeterministicModel.cpp @@ -2,7 +2,7 @@ #include "storm/models/sparse/StandardRewardModel.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/exceptions/InvalidOperationException.h" diff --git a/src/storm/models/sparse/StandardRewardModel.cpp b/src/storm/models/sparse/StandardRewardModel.cpp index a4149709c..bffd8a7e9 100644 --- a/src/storm/models/sparse/StandardRewardModel.cpp +++ b/src/storm/models/sparse/StandardRewardModel.cpp @@ -4,7 +4,7 @@ #include "storm/exceptions/InvalidOperationException.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace models { diff --git a/src/storm/models/sparse/StandardRewardModel.h b/src/storm/models/sparse/StandardRewardModel.h index f0449ce52..2a3033ea7 100644 --- a/src/storm/models/sparse/StandardRewardModel.h +++ b/src/storm/models/sparse/StandardRewardModel.h @@ -5,7 +5,7 @@ #include "storm/storage/SparseMatrix.h" #include "storm/utility/OsDetection.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace models { diff --git a/src/storm/models/sparse/StochasticTwoPlayerGame.cpp b/src/storm/models/sparse/StochasticTwoPlayerGame.cpp index 6ac6f93e4..3b034653c 100644 --- a/src/storm/models/sparse/StochasticTwoPlayerGame.cpp +++ b/src/storm/models/sparse/StochasticTwoPlayerGame.cpp @@ -2,7 +2,7 @@ #include "storm/models/sparse/StandardRewardModel.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace models { diff --git a/src/storm/models/symbolic/Ctmc.cpp b/src/storm/models/symbolic/Ctmc.cpp index 543bc7d90..409a1fcd2 100644 --- a/src/storm/models/symbolic/Ctmc.cpp +++ b/src/storm/models/symbolic/Ctmc.cpp @@ -6,7 +6,7 @@ #include "storm/models/symbolic/StandardRewardModel.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace models { diff --git a/src/storm/models/symbolic/DeterministicModel.cpp b/src/storm/models/symbolic/DeterministicModel.cpp index a9d9c92df..4a2f629f8 100644 --- a/src/storm/models/symbolic/DeterministicModel.cpp +++ b/src/storm/models/symbolic/DeterministicModel.cpp @@ -6,7 +6,7 @@ #include "storm/models/symbolic/StandardRewardModel.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace models { diff --git a/src/storm/models/symbolic/Dtmc.cpp b/src/storm/models/symbolic/Dtmc.cpp index 3f7153ead..08ade71f9 100644 --- a/src/storm/models/symbolic/Dtmc.cpp +++ b/src/storm/models/symbolic/Dtmc.cpp @@ -6,7 +6,7 @@ #include "storm/models/symbolic/StandardRewardModel.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace models { diff --git a/src/storm/models/symbolic/Mdp.cpp b/src/storm/models/symbolic/Mdp.cpp index 20bd9ad2c..d9df2263b 100644 --- a/src/storm/models/symbolic/Mdp.cpp +++ b/src/storm/models/symbolic/Mdp.cpp @@ -6,7 +6,7 @@ #include "storm/models/symbolic/StandardRewardModel.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace models { diff --git a/src/storm/models/symbolic/Model.h b/src/storm/models/symbolic/Model.h index 5c9382831..0d2dac286 100644 --- a/src/storm/models/symbolic/Model.h +++ b/src/storm/models/symbolic/Model.h @@ -13,7 +13,7 @@ #include "storm/utility/OsDetection.h" #include "storm-config.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace dd { diff --git a/src/storm/models/symbolic/NondeterministicModel.cpp b/src/storm/models/symbolic/NondeterministicModel.cpp index eb8c1a73d..7856a942e 100644 --- a/src/storm/models/symbolic/NondeterministicModel.cpp +++ b/src/storm/models/symbolic/NondeterministicModel.cpp @@ -7,7 +7,7 @@ #include "storm/models/symbolic/StandardRewardModel.h" #include "storm-config.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace models { diff --git a/src/storm/models/symbolic/StandardRewardModel.cpp b/src/storm/models/symbolic/StandardRewardModel.cpp index 1507b6dfc..a91040069 100644 --- a/src/storm/models/symbolic/StandardRewardModel.cpp +++ b/src/storm/models/symbolic/StandardRewardModel.cpp @@ -4,7 +4,7 @@ #include "storm/storage/dd/Add.h" #include "storm/storage/dd/Bdd.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace models { diff --git a/src/storm/models/symbolic/StochasticTwoPlayerGame.cpp b/src/storm/models/symbolic/StochasticTwoPlayerGame.cpp index fdff99c36..346a6a396 100644 --- a/src/storm/models/symbolic/StochasticTwoPlayerGame.cpp +++ b/src/storm/models/symbolic/StochasticTwoPlayerGame.cpp @@ -7,7 +7,7 @@ #include "storm/models/symbolic/StandardRewardModel.h" #include "storm-config.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace models { diff --git a/src/storm/parser/AutoParser.cpp b/src/storm/parser/AutoParser.cpp index 9d3069738..dbc5fc493 100644 --- a/src/storm/parser/AutoParser.cpp +++ b/src/storm/parser/AutoParser.cpp @@ -10,7 +10,7 @@ #include "storm/utility/macros.h" #include "storm/exceptions/WrongFormatException.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/cstring.h" #include "storm/utility/OsDetection.h" diff --git a/src/storm/parser/DeterministicModelParser.cpp b/src/storm/parser/DeterministicModelParser.cpp index e962193c2..a99f40a68 100644 --- a/src/storm/parser/DeterministicModelParser.cpp +++ b/src/storm/parser/DeterministicModelParser.cpp @@ -9,7 +9,7 @@ #include "storm/parser/AtomicPropositionLabelingParser.h" #include "storm/parser/SparseStateRewardParser.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace parser { diff --git a/src/storm/parser/DeterministicSparseTransitionParser.cpp b/src/storm/parser/DeterministicSparseTransitionParser.cpp index ad56745bd..540371f74 100644 --- a/src/storm/parser/DeterministicSparseTransitionParser.cpp +++ b/src/storm/parser/DeterministicSparseTransitionParser.cpp @@ -16,7 +16,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/CoreSettings.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/macros.h" namespace storm { namespace parser { diff --git a/src/storm/parser/DirectEncodingParser.cpp b/src/storm/parser/DirectEncodingParser.cpp index 110c9ca32..0d1751d98 100644 --- a/src/storm/parser/DirectEncodingParser.cpp +++ b/src/storm/parser/DirectEncodingParser.cpp @@ -12,7 +12,7 @@ #include "storm/exceptions/NotSupportedException.h" #include "storm/settings/SettingsManager.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/constants.h" #include "storm/utility/macros.h" #include "storm/utility/file.h" diff --git a/src/storm/parser/ExpressionCreator.h b/src/storm/parser/ExpressionCreator.h index 06b5f5a60..bf454c552 100644 --- a/src/storm/parser/ExpressionCreator.h +++ b/src/storm/parser/ExpressionCreator.h @@ -4,7 +4,7 @@ #include "storm/parser/SpiritParserDefinitions.h" #include -#include "storm/adapters/NumberAdapter.h" +#include "storm/adapters/RationalNumberAdapter.h" namespace storm { diff --git a/src/storm/parser/ExpressionParser.h b/src/storm/parser/ExpressionParser.h index ebfa0517e..da3282b1b 100644 --- a/src/storm/parser/ExpressionParser.h +++ b/src/storm/parser/ExpressionParser.h @@ -6,7 +6,7 @@ #include "storm/parser/SpiritErrorHandler.h" #include "storm/storage/expressions/OperatorType.h" -#include "storm/adapters/NumberAdapter.h" +#include "storm/adapters/RationalNumberAdapter.h" namespace storm { namespace expressions { diff --git a/src/storm/parser/MarkovAutomatonParser.cpp b/src/storm/parser/MarkovAutomatonParser.cpp index d8a709cd9..bfc48c51e 100644 --- a/src/storm/parser/MarkovAutomatonParser.cpp +++ b/src/storm/parser/MarkovAutomatonParser.cpp @@ -6,7 +6,7 @@ #include "storm/exceptions/WrongFormatException.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace parser { diff --git a/src/storm/parser/NondeterministicModelParser.cpp b/src/storm/parser/NondeterministicModelParser.cpp index 5ea7952ba..64c256989 100644 --- a/src/storm/parser/NondeterministicModelParser.cpp +++ b/src/storm/parser/NondeterministicModelParser.cpp @@ -10,7 +10,7 @@ #include "storm/parser/SparseStateRewardParser.h" #include "storm/parser/SparseChoiceLabelingParser.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/macros.h" namespace storm { diff --git a/src/storm/parser/NondeterministicSparseTransitionParser.cpp b/src/storm/parser/NondeterministicSparseTransitionParser.cpp index f9a1947b9..cb941aec5 100644 --- a/src/storm/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/storm/parser/NondeterministicSparseTransitionParser.cpp @@ -13,7 +13,7 @@ #include "storm/utility/cstring.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/macros.h" namespace storm { namespace parser { diff --git a/src/storm/parser/SparseStateRewardParser.cpp b/src/storm/parser/SparseStateRewardParser.cpp index 3df355578..f42b4cbe8 100644 --- a/src/storm/parser/SparseStateRewardParser.cpp +++ b/src/storm/parser/SparseStateRewardParser.cpp @@ -7,7 +7,7 @@ #include "storm/utility/cstring.h" #include "storm/parser/MappedFile.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/macros.h" namespace storm { namespace parser { diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index 77c1e9150..a386dc94c 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/src/storm/settings/SettingsManager.cpp @@ -351,7 +351,7 @@ namespace storm { for (uint_fast64_t i = 0; i < argumentCache.size(); ++i) { ArgumentBase& argument = option->getArgument(i); bool conversionOk = argument.setFromStringValue(argumentCache[i]); - STORM_LOG_THROW(conversionOk, storm::exceptions::OptionParserException, "Conversion of value of argument '" << argument.getName() << "' to its type failed."); + STORM_LOG_THROW(conversionOk, storm::exceptions::OptionParserException, "Value '" << argumentCache[i] << "' is invalid for argument '" << argument.getName() << "' of option " << option->getModuleName() << ":" << option->getLongName() << "."); } // In case there are optional arguments that were not set, we set them to their default value. diff --git a/src/storm/solver/SmtlibSmtSolver.cpp b/src/storm/solver/SmtlibSmtSolver.cpp index a9da13e4e..8dcd37ddc 100644 --- a/src/storm/solver/SmtlibSmtSolver.cpp +++ b/src/storm/solver/SmtlibSmtSolver.cpp @@ -18,7 +18,7 @@ #include "storm/exceptions/IllegalFunctionCallException.h" #include "storm/utility/macros.h" #include "storm/utility/file.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/exceptions/UnexpectedException.h" namespace storm { diff --git a/src/storm/solver/SmtlibSmtSolver.h b/src/storm/solver/SmtlibSmtSolver.h index 5c4d86158..70e4c325f 100644 --- a/src/storm/solver/SmtlibSmtSolver.h +++ b/src/storm/solver/SmtlibSmtSolver.h @@ -7,7 +7,7 @@ #include "storm-config.h" #include "storm/solver/SmtSolver.h" #include "storm/adapters/Smt2ExpressionAdapter.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace solver { diff --git a/src/storm/solver/SmtratSmtSolver.h b/src/storm/solver/SmtratSmtSolver.h index a70721e45..3cb9b559c 100644 --- a/src/storm/solver/SmtratSmtSolver.h +++ b/src/storm/solver/SmtratSmtSolver.h @@ -7,7 +7,7 @@ #ifdef SMTRATDOESNTWORK // Does not compile with current version of smtrat. #include "lib/smtrat.h" -#include "../adapters/carlAdapter.h" +#include "../adapters/RationalFunctionAdapter.h" namespace storm { diff --git a/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp b/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp index 2fef23623..43fb7f0a2 100644 --- a/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicEliminationLinearEquationSolver.cpp @@ -5,7 +5,7 @@ #include "storm/utility/dd.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace solver { diff --git a/src/storm/solver/SymbolicLinearEquationSolver.cpp b/src/storm/solver/SymbolicLinearEquationSolver.cpp index 13c220418..0a80a3afc 100644 --- a/src/storm/solver/SymbolicLinearEquationSolver.cpp +++ b/src/storm/solver/SymbolicLinearEquationSolver.cpp @@ -14,7 +14,7 @@ #include "storm/utility/macros.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace solver { diff --git a/src/storm/solver/SymbolicLinearEquationSolver.h b/src/storm/solver/SymbolicLinearEquationSolver.h index a83054d5c..e3f68ee19 100644 --- a/src/storm/solver/SymbolicLinearEquationSolver.h +++ b/src/storm/solver/SymbolicLinearEquationSolver.h @@ -7,7 +7,7 @@ #include "storm/storage/expressions/Variable.h" #include "storm/storage/dd/DdType.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace dd { diff --git a/src/storm/solver/TerminationCondition.cpp b/src/storm/solver/TerminationCondition.cpp index 21aaf5a44..a30455564 100644 --- a/src/storm/solver/TerminationCondition.cpp +++ b/src/storm/solver/TerminationCondition.cpp @@ -1,7 +1,7 @@ #include "storm/solver/TerminationCondition.h" #include "storm/utility/vector.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/macros.h" diff --git a/src/storm/solver/stateelimination/DynamicStatePriorityQueue.cpp b/src/storm/solver/stateelimination/DynamicStatePriorityQueue.cpp index 8802fe837..e69339aed 100644 --- a/src/storm/solver/stateelimination/DynamicStatePriorityQueue.cpp +++ b/src/storm/solver/stateelimination/DynamicStatePriorityQueue.cpp @@ -1,6 +1,6 @@ #include "storm/solver/stateelimination/DynamicStatePriorityQueue.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/macros.h" #include "storm/utility/constants.h" diff --git a/src/storm/solver/stateelimination/StateEliminator.cpp b/src/storm/solver/stateelimination/StateEliminator.cpp index 1ebc02904..0dc48bcff 100644 --- a/src/storm/solver/stateelimination/StateEliminator.cpp +++ b/src/storm/solver/stateelimination/StateEliminator.cpp @@ -1,6 +1,6 @@ #include "storm/solver/stateelimination/StateEliminator.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/storage/BitVector.h" diff --git a/src/storm/solver/stateelimination/StaticStatePriorityQueue.cpp b/src/storm/solver/stateelimination/StaticStatePriorityQueue.cpp index 0ffcb8605..1a038d845 100644 --- a/src/storm/solver/stateelimination/StaticStatePriorityQueue.cpp +++ b/src/storm/solver/stateelimination/StaticStatePriorityQueue.cpp @@ -1,6 +1,6 @@ #include "storm/solver/stateelimination/StaticStatePriorityQueue.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace solver { diff --git a/src/storm/storage/Distribution.cpp b/src/storm/storage/Distribution.cpp index 3c0aebe1b..d918e4717 100644 --- a/src/storm/storage/Distribution.cpp +++ b/src/storm/storage/Distribution.cpp @@ -9,7 +9,7 @@ #include "storm/settings/SettingsManager.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace storage { diff --git a/src/storm/storage/FlexibleSparseMatrix.cpp b/src/storm/storage/FlexibleSparseMatrix.cpp index ef8ccf72d..1ee642c65 100644 --- a/src/storm/storage/FlexibleSparseMatrix.cpp +++ b/src/storm/storage/FlexibleSparseMatrix.cpp @@ -2,7 +2,7 @@ #include "storm/storage/SparseMatrix.h" #include "storm/storage/BitVector.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/macros.h" #include "storm/utility/constants.h" diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index d2bcead60..e03dd5902 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -9,7 +9,7 @@ #include "storm/storage/sparse/StateType.h" #include "storm/storage/SparseMatrix.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/storage/BitVector.h" #include "storm/utility/constants.h" diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h index cf9211849..234dec119 100644 --- a/src/storm/storage/SparseMatrix.h +++ b/src/storm/storage/SparseMatrix.h @@ -12,7 +12,7 @@ #include "storm/utility/OsDetection.h" #include "storm/utility/macros.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" // Forward declaration for adapter classes. namespace storm { diff --git a/src/storm/storage/StronglyConnectedComponentDecomposition.cpp b/src/storm/storage/StronglyConnectedComponentDecomposition.cpp index f38cd8b31..af98331a7 100644 --- a/src/storm/storage/StronglyConnectedComponentDecomposition.cpp +++ b/src/storm/storage/StronglyConnectedComponentDecomposition.cpp @@ -1,7 +1,7 @@ #include "storm/storage/StronglyConnectedComponentDecomposition.h" #include "storm/models/sparse/Model.h" #include "storm/models/sparse/StandardRewardModel.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace storage { diff --git a/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp b/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp index 39ad3db45..a90de5bb6 100644 --- a/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp @@ -6,7 +6,7 @@ #include #include -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/models/sparse/Dtmc.h" diff --git a/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp b/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp index 208c67997..1b1d3d0f1 100644 --- a/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp +++ b/src/storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp @@ -8,7 +8,7 @@ #include "storm/utility/macros.h" #include "storm/exceptions/IllegalFunctionCallException.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace storage { diff --git a/src/storm/storage/dd/Add.cpp b/src/storm/storage/dd/Add.cpp index a3d374d23..ea8a4407d 100644 --- a/src/storm/storage/dd/Add.cpp +++ b/src/storm/storage/dd/Add.cpp @@ -14,7 +14,7 @@ #include "storm/exceptions/InvalidOperationException.h" #include "storm-config.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace dd { diff --git a/src/storm/storage/dd/Add.h b/src/storm/storage/dd/Add.h index 86f443ce3..092c7e7ba 100644 --- a/src/storm/storage/dd/Add.h +++ b/src/storm/storage/dd/Add.h @@ -15,7 +15,7 @@ #include "storm/storage/dd/sylvan/SylvanAddIterator.h" #include "storm-config.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace dd { diff --git a/src/storm/storage/dd/Bdd.cpp b/src/storm/storage/dd/Bdd.cpp index d58758b6e..1b5f40172 100644 --- a/src/storm/storage/dd/Bdd.cpp +++ b/src/storm/storage/dd/Bdd.cpp @@ -17,7 +17,7 @@ #include "storm/exceptions/InvalidOperationException.h" #include "storm-config.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace dd { diff --git a/src/storm/storage/dd/DdManager.cpp b/src/storm/storage/dd/DdManager.cpp index b9f0df1be..ff4d83785 100644 --- a/src/storm/storage/dd/DdManager.cpp +++ b/src/storm/storage/dd/DdManager.cpp @@ -9,7 +9,7 @@ #include "storm/exceptions/NotSupportedException.h" #include "storm-config.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include #include diff --git a/src/storm/storage/dd/Odd.cpp b/src/storm/storage/dd/Odd.cpp index 0973fe7a4..af86aba1d 100644 --- a/src/storm/storage/dd/Odd.cpp +++ b/src/storm/storage/dd/Odd.cpp @@ -8,7 +8,7 @@ #include "storm/exceptions/InvalidArgumentException.h" #include "storm/utility/file.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace dd { diff --git a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h index 13b96d25a..cb11bcb5b 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanAdd.h @@ -13,7 +13,7 @@ #include "storm/storage/expressions/Variable.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm-config.h" namespace storm { diff --git a/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp index db205268f..83a7f26b7 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp +++ b/src/storm/storage/dd/sylvan/InternalSylvanBdd.cpp @@ -13,7 +13,7 @@ #include "storm/exceptions/InvalidOperationException.h" #include "storm/exceptions/NotSupportedException.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm-config.h" namespace storm { diff --git a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.h b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.h index 77846dbe4..24e3a354a 100644 --- a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.h +++ b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.h @@ -9,7 +9,7 @@ #include "storm/storage/dd/sylvan/InternalSylvanBdd.h" #include "storm/storage/dd/sylvan/InternalSylvanAdd.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm-config.h" namespace storm { diff --git a/src/storm/storage/dd/sylvan/SylvanAddIterator.cpp b/src/storm/storage/dd/sylvan/SylvanAddIterator.cpp index a9367fa7c..03afd7239 100644 --- a/src/storm/storage/dd/sylvan/SylvanAddIterator.cpp +++ b/src/storm/storage/dd/sylvan/SylvanAddIterator.cpp @@ -10,7 +10,7 @@ #include -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace dd { diff --git a/src/storm/storage/expressions/BaseExpression.h b/src/storm/storage/expressions/BaseExpression.h index 5f93766a5..93091e536 100644 --- a/src/storm/storage/expressions/BaseExpression.h +++ b/src/storm/storage/expressions/BaseExpression.h @@ -7,7 +7,7 @@ #include #include -#include "storm/adapters/NumberAdapter.h" +#include "storm/adapters/RationalNumberAdapter.h" #include "storm/storage/expressions/Type.h" #include "storm/utility/OsDetection.h" #include diff --git a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp index 0ed3dc746..2cd3c2f61 100644 --- a/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp +++ b/src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp @@ -1,7 +1,7 @@ #include #include -#include "storm/adapters/NumberAdapter.h" +#include "storm/adapters/RationalNumberAdapter.h" #include "storm/storage/expressions/BinaryNumericalFunctionExpression.h" #include "storm/storage/expressions/IntegerLiteralExpression.h" #include "storm/storage/expressions/RationalLiteralExpression.h" diff --git a/src/storm/storage/expressions/ExpressionEvaluator.h b/src/storm/storage/expressions/ExpressionEvaluator.h index 9308c912b..5d867e8be 100644 --- a/src/storm/storage/expressions/ExpressionEvaluator.h +++ b/src/storm/storage/expressions/ExpressionEvaluator.h @@ -3,7 +3,7 @@ #include -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/storage/expressions/Variable.h" #include "storm/storage/expressions/Expression.h" #include "storm/storage/expressions/ExprtkExpressionEvaluator.h" diff --git a/src/storm/storage/expressions/ExpressionEvaluatorBase.cpp b/src/storm/storage/expressions/ExpressionEvaluatorBase.cpp index d8ae7deaa..5071ab861 100644 --- a/src/storm/storage/expressions/ExpressionEvaluatorBase.cpp +++ b/src/storm/storage/expressions/ExpressionEvaluatorBase.cpp @@ -1,7 +1,7 @@ #include "storm/storage/expressions/ExpressionEvaluatorBase.h" #include "storm/storage/expressions/ExpressionManager.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace expressions { diff --git a/src/storm/storage/expressions/ExpressionManager.h b/src/storm/storage/expressions/ExpressionManager.h index 1ad82b939..3a80261b3 100644 --- a/src/storm/storage/expressions/ExpressionManager.h +++ b/src/storm/storage/expressions/ExpressionManager.h @@ -12,7 +12,7 @@ #include "storm/storage/expressions/Variable.h" #include "storm/storage/expressions/Expression.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/OsDetection.h" namespace storm { diff --git a/src/storm/storage/expressions/ExprtkExpressionEvaluator.cpp b/src/storm/storage/expressions/ExprtkExpressionEvaluator.cpp index 7cd49114d..42a405e49 100755 --- a/src/storm/storage/expressions/ExprtkExpressionEvaluator.cpp +++ b/src/storm/storage/expressions/ExprtkExpressionEvaluator.cpp @@ -1,7 +1,7 @@ #include "storm/storage/expressions/ExprtkExpressionEvaluator.h" #include "storm/storage/expressions/ExpressionManager.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/macros.h" #include "storm/exceptions/UnexpectedException.h" diff --git a/src/storm/storage/expressions/RationalLiteralExpression.h b/src/storm/storage/expressions/RationalLiteralExpression.h index b89505471..712dfca95 100644 --- a/src/storm/storage/expressions/RationalLiteralExpression.h +++ b/src/storm/storage/expressions/RationalLiteralExpression.h @@ -4,7 +4,7 @@ #include "storm/storage/expressions/BaseExpression.h" #include "storm/utility/OsDetection.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace expressions { diff --git a/src/storm/storage/expressions/ToCppVisitor.cpp b/src/storm/storage/expressions/ToCppVisitor.cpp index d336d0d40..b68de7132 100644 --- a/src/storm/storage/expressions/ToCppVisitor.cpp +++ b/src/storm/storage/expressions/ToCppVisitor.cpp @@ -2,7 +2,7 @@ #include "storm/storage/expressions/Expressions.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/macros.h" #include "storm/exceptions/NotSupportedException.h" diff --git a/src/storm/storage/expressions/ToRationalFunctionVisitor.h b/src/storm/storage/expressions/ToRationalFunctionVisitor.h index 6e90d36ce..25797322f 100644 --- a/src/storm/storage/expressions/ToRationalFunctionVisitor.h +++ b/src/storm/storage/expressions/ToRationalFunctionVisitor.h @@ -3,7 +3,7 @@ #include -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/storage/expressions/Expression.h" #include "storm/storage/expressions/Expressions.h" diff --git a/src/storm/storage/expressions/ToRationalNumberVisitor.h b/src/storm/storage/expressions/ToRationalNumberVisitor.h index 1f2b88f48..69f6e2b83 100644 --- a/src/storm/storage/expressions/ToRationalNumberVisitor.h +++ b/src/storm/storage/expressions/ToRationalNumberVisitor.h @@ -4,7 +4,7 @@ #include -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/storage/expressions/Expression.h" #include "storm/storage/expressions/Expressions.h" diff --git a/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp b/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp index 9e8290c02..3ed20d7b6 100644 --- a/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp +++ b/src/storm/storage/expressions/UnaryNumericalFunctionExpression.cpp @@ -2,7 +2,7 @@ #include -#include "storm/adapters/NumberAdapter.h" +#include "storm/adapters/RationalNumberAdapter.h" #include "storm/storage/expressions/UnaryNumericalFunctionExpression.h" #include "storm/storage/expressions/IntegerLiteralExpression.h" #include "storm/storage/expressions/RationalLiteralExpression.h" diff --git a/src/storm/storage/geometry/Polytope.cpp b/src/storm/storage/geometry/Polytope.cpp index 27a9cd046..a89b7247e 100644 --- a/src/storm/storage/geometry/Polytope.cpp +++ b/src/storm/storage/geometry/Polytope.cpp @@ -2,7 +2,7 @@ #include -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/adapters/HyproAdapter.h" #include "storm/storage/geometry/HyproPolytope.h" #include "storm/storage/geometry/NativePolytope.h" diff --git a/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneCollector.h b/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneCollector.h index 8aead0786..b9c1fc21c 100644 --- a/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneCollector.h +++ b/src/storm/storage/geometry/nativepolytopeconversion/HyperplaneCollector.h @@ -3,7 +3,7 @@ #include -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/adapters/EigenAdapter.h" namespace storm { @@ -61,4 +61,4 @@ namespace storm { } -#endif /* STORM_STORAGE_GEOMETRY_NATIVEPOLYTOPECONVERSION_HYPERPLANECOLLECTOR_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_GEOMETRY_NATIVEPOLYTOPECONVERSION_HYPERPLANECOLLECTOR_H_ */ diff --git a/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp b/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp index edd19d833..e4508b72c 100644 --- a/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp +++ b/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp @@ -2,7 +2,7 @@ #include #include -#include +#include #include "storm/utility/macros.h" #include "storm/utility/constants.h" diff --git a/src/storm/storage/geometry/nativepolytopeconversion/SubsetEnumerator.cpp b/src/storm/storage/geometry/nativepolytopeconversion/SubsetEnumerator.cpp index 81c8d9ff7..c6103bf9d 100644 --- a/src/storm/storage/geometry/nativepolytopeconversion/SubsetEnumerator.cpp +++ b/src/storm/storage/geometry/nativepolytopeconversion/SubsetEnumerator.cpp @@ -1,7 +1,7 @@ #include "SubsetEnumerator.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/eigen.h" namespace storm { @@ -95,4 +95,4 @@ namespace storm { template class SubsetEnumerator>; } } -} \ No newline at end of file +} diff --git a/src/storm/storage/jani/JSONExporter.h b/src/storm/storage/jani/JSONExporter.h index 1d3955536..e26cf287f 100644 --- a/src/storm/storage/jani/JSONExporter.h +++ b/src/storm/storage/jani/JSONExporter.h @@ -5,7 +5,7 @@ #include "storm/logic/FormulaVisitor.h" #include "Model.h" #include "storm/storage/jani/Property.h" -#include "storm/adapters/NumberAdapter.h" +#include "storm/adapters/RationalNumberAdapter.h" // JSON parser #include "json.hpp" namespace modernjson { diff --git a/src/storm/storage/jani/TemplateEdge.cpp b/src/storm/storage/jani/TemplateEdge.cpp index 959b7b7d1..987e4f6de 100644 --- a/src/storm/storage/jani/TemplateEdge.cpp +++ b/src/storm/storage/jani/TemplateEdge.cpp @@ -12,7 +12,7 @@ namespace storm { } TemplateEdge::TemplateEdge(storm::expressions::Expression const& guard, OrderedAssignments const& assignments, std::vector const& destinations) - : guard(guard), assignments(assignments), destinations(destinations) { + : guard(guard), destinations(destinations), assignments(assignments) { // Intentionally left empty. } diff --git a/src/storm/storm.cpp b/src/storm/storm.cpp index 20126f488..8e915d6e7 100644 --- a/src/storm/storm.cpp +++ b/src/storm/storm.cpp @@ -1,13 +1,7 @@ -// Include other headers. -#include -#include "storm/exceptions/BaseException.h" #include "storm/utility/macros.h" -#include "storm/cli/cli.h" -#include "storm/utility/initialize.h" -#include "storm/utility/Stopwatch.h" +#include "storm/exceptions/BaseException.h" -#include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/ResourceSettings.h" +#include "storm/cli/cli.h" /*! * Main entry point of the executable storm. @@ -15,26 +9,7 @@ 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"); - bool optionsCorrect = storm::cli::parseOptions(argc, argv); - if (!optionsCorrect) { - return -1; - } - - // From this point on we are ready to carry out the actual computations. - storm::cli::processOptions(); - - // All operations have now been performed, so we clean up everything and terminate. - storm::utility::cleanUp(); - totalTimer.stop(); - - if (storm::settings::getModule().isPrintTimeAndMemorySet()) { - storm::cli::showTimeAndMemoryStatistics(totalTimer.getTimeInMilliseconds()); - } - return 0; + return storm::cli::process(argc, argv); } catch (storm::exceptions::BaseException const& exception) { STORM_LOG_ERROR("An exception caused Storm to terminate. The message of the exception is: " << exception.what()); return 1; diff --git a/src/storm/transformer/ParameterLifter.cpp b/src/storm/transformer/ParameterLifter.cpp index 829631cff..43c76fd55 100644 --- a/src/storm/transformer/ParameterLifter.cpp +++ b/src/storm/transformer/ParameterLifter.cpp @@ -1,7 +1,7 @@ #include "storm/transformer/ParameterLifter.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/vector.h" diff --git a/src/storm/transformer/SparseParametricDtmcSimplifier.cpp b/src/storm/transformer/SparseParametricDtmcSimplifier.cpp index 972863b1b..a150efe9b 100644 --- a/src/storm/transformer/SparseParametricDtmcSimplifier.cpp +++ b/src/storm/transformer/SparseParametricDtmcSimplifier.cpp @@ -1,6 +1,6 @@ #include "storm/transformer/SparseParametricDtmcSimplifier.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/logic/CloneVisitor.h" #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" @@ -200,4 +200,4 @@ namespace storm { template class SparseParametricDtmcSimplifier>; } -} \ No newline at end of file +} diff --git a/src/storm/transformer/SparseParametricMdpSimplifier.cpp b/src/storm/transformer/SparseParametricMdpSimplifier.cpp index d84058637..a6d8bf99e 100644 --- a/src/storm/transformer/SparseParametricMdpSimplifier.cpp +++ b/src/storm/transformer/SparseParametricMdpSimplifier.cpp @@ -1,6 +1,6 @@ #include "storm/transformer/SparseParametricMdpSimplifier.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/logic/CloneVisitor.h" #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" @@ -298,4 +298,4 @@ namespace storm { template class SparseParametricMdpSimplifier>; } -} \ No newline at end of file +} diff --git a/src/storm/transformer/SparseParametricModelSimplifier.cpp b/src/storm/transformer/SparseParametricModelSimplifier.cpp index 744e07aa7..3dd6fbd56 100644 --- a/src/storm/transformer/SparseParametricModelSimplifier.cpp +++ b/src/storm/transformer/SparseParametricModelSimplifier.cpp @@ -1,6 +1,6 @@ #include "storm/transformer/SparseParametricModelSimplifier.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Mdp.h" @@ -149,4 +149,4 @@ namespace storm { template class SparseParametricModelSimplifier>; template class SparseParametricModelSimplifier>; } -} \ No newline at end of file +} diff --git a/src/storm/utility/ConstantsComparator.h b/src/storm/utility/ConstantsComparator.h index 5cb13d8fd..988d08538 100644 --- a/src/storm/utility/ConstantsComparator.h +++ b/src/storm/utility/ConstantsComparator.h @@ -1,7 +1,7 @@ #ifndef STORM_UTILITY_CONSTANTSCOMPARATOR_H_ #define STORM_UTILITY_CONSTANTSCOMPARATOR_H_ -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { namespace utility { diff --git a/src/storm/utility/DirectEncodingExporter.cpp b/src/storm/utility/DirectEncodingExporter.cpp index b82957c9c..e49e2ff1a 100644 --- a/src/storm/utility/DirectEncodingExporter.cpp +++ b/src/storm/utility/DirectEncodingExporter.cpp @@ -1,6 +1,6 @@ #include "DirectEncodingExporter.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/constants.h" #include "storm/utility/macros.h" #include "storm/exceptions/NotImplementedException.h" diff --git a/src/storm/utility/NumberTraits.h b/src/storm/utility/NumberTraits.h index 3d3d03387..c52dad448 100644 --- a/src/storm/utility/NumberTraits.h +++ b/src/storm/utility/NumberTraits.h @@ -1,6 +1,6 @@ #pragma once -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" namespace storm { template diff --git a/src/storm/utility/cli.cpp b/src/storm/utility/cli.cpp index 4798fd531..ded3f9a6a 100644 --- a/src/storm/utility/cli.cpp +++ b/src/storm/utility/cli.cpp @@ -8,6 +8,11 @@ namespace storm { namespace utility { namespace cli { + std::string getCurrentWorkingDirectory() { + char temp[512]; + return (GetCurrentDir(temp, 512 - 1) ? std::string(temp) : std::string("")); + } + std::map parseConstantDefinitionString(storm::expressions::ExpressionManager const& manager, std::string const& constantDefinitionString) { std::map constantDefinitions; std::set definedConstants; diff --git a/src/storm/utility/cli.h b/src/storm/utility/cli.h index 63909698d..07f00c9cc 100644 --- a/src/storm/utility/cli.h +++ b/src/storm/utility/cli.h @@ -9,6 +9,8 @@ namespace storm { namespace utility { namespace cli { + std::string getCurrentWorkingDirectory(); + std::map parseConstantDefinitionString(storm::expressions::ExpressionManager const& manager, std::string const& constantDefinitionString); std::vector parseCommaSeparatedStrings(std::string const& input); diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp index 138a44f51..7e0e5309c 100644 --- a/src/storm/utility/constants.cpp +++ b/src/storm/utility/constants.cpp @@ -9,7 +9,7 @@ #include "storm/exceptions/InvalidArgumentException.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/macros.h" namespace storm { diff --git a/src/storm/utility/dd.cpp b/src/storm/utility/dd.cpp index 26dde9bd5..b4b74a19a 100644 --- a/src/storm/utility/dd.cpp +++ b/src/storm/utility/dd.cpp @@ -4,7 +4,7 @@ #include "storm/storage/dd/Add.h" #include "storm/storage/dd/Bdd.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/macros.h" diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp index 7ff744662..fff71c741 100644 --- a/src/storm/utility/graph.cpp +++ b/src/storm/utility/graph.cpp @@ -2,7 +2,7 @@ #include "utility/OsDetection.h" #include "storm-config.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/storage/sparse/StateType.h" #include "storm/storage/dd/Bdd.h" diff --git a/src/storm/utility/parametric.h b/src/storm/utility/parametric.h index 7d51bf1ee..77a58e7f8 100644 --- a/src/storm/utility/parametric.h +++ b/src/storm/utility/parametric.h @@ -1,7 +1,7 @@ #ifndef STORM_UTILITY_PARAMETRIC_H #define STORM_UTILITY_PARAMETRIC_H -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include diff --git a/src/storm/utility/prism.cpp b/src/storm/utility/prism.cpp index 27e4b8847..1f2e00805 100644 --- a/src/storm/utility/prism.cpp +++ b/src/storm/utility/prism.cpp @@ -1,6 +1,6 @@ #include "storm/utility/prism.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/prism/Program.h" diff --git a/src/storm/utility/solver.h b/src/storm/utility/solver.h index 5748c60d2..4fbc0745e 100644 --- a/src/storm/utility/solver.h +++ b/src/storm/utility/solver.h @@ -7,7 +7,7 @@ #include #include -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/storage/sparse/StateType.h" #include "storm/storage/dd/DdType.h" diff --git a/src/storm/utility/stateelimination.h b/src/storm/utility/stateelimination.h index 7bfa81cb7..179e090c5 100644 --- a/src/storm/utility/stateelimination.h +++ b/src/storm/utility/stateelimination.h @@ -7,7 +7,7 @@ #include "storm/storage/sparse/StateType.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/settings/modules/EliminationSettings.h" diff --git a/src/storm/utility/storm.cpp b/src/storm/utility/storm.cpp index f4d04bdcd..07bb39118 100644 --- a/src/storm/utility/storm.cpp +++ b/src/storm/utility/storm.cpp @@ -29,17 +29,6 @@ namespace storm{ modelAndFormulae.first.checkValid(); return modelAndFormulae; } - - void exportJaniModel(storm::jani::Model const& model, std::vector const& properties, std::string const& filepath) { - STORM_LOG_TRACE("Exporting JANI model."); - if (storm::settings::getModule().isExportAsStandardJaniSet()) { - storm::jani::Model normalisedModel = model; - normalisedModel.makeStandardJaniCompliant(); - storm::jani::JsonExporter::toFile(normalisedModel, properties, filepath); - } else { - storm::jani::JsonExporter::toFile(model, properties, filepath); - } - } std::vector parseProperties(storm::parser::FormulaParser& formulaParser, std::string const& inputString, boost::optional> const& propertyFilter) { // If the given property looks like a file (containing a dot and there exists a file with that name), diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index 5c105b439..e92985b1a 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -95,7 +95,6 @@ #include "storm/analysis/GraphConditions.h" - // Headers related to exception handling. #include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/InvalidArgumentException.h" @@ -107,33 +106,14 @@ #include "storm/utility/Stopwatch.h" #include "storm/utility/file.h" +#include + namespace storm { namespace parser { class FormulaParser; } - - template - inline std::shared_ptr> buildExplicitModel(std::string const&, std::string const&, boost::optional const& = boost::none, boost::optional const& = boost::none, boost::optional const& = boost::none) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exact or parametric models with explicit input are not supported."); - } - - template<> - inline std::shared_ptr> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile, boost::optional const& stateRewardsFile, boost::optional const& transitionRewardsFile, boost::optional const& choiceLabelingFile) { - return storm::parser::AutoParser::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "", choiceLabelingFile ? choiceLabelingFile.get() : "" ); - } - - template - inline std::shared_ptr> buildExplicitDRNModel(std::string const& drnFile) { - return storm::parser::DirectEncodingParser::parseModel(drnFile); - } - - template<> - inline std::shared_ptr> buildExplicitDRNModel(std::string const&) { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exact models with direct encoding are not supported."); - } - std::vector> extractFormulasFromProperties(std::vector const& properties); std::pair> parseJaniModel(std::string const& path); storm::prism::Program parseProgram(std::string const& path); @@ -145,65 +125,6 @@ namespace storm { boost::optional> parsePropertyFilter(boost::optional const& propertyFilter); std::vector filterProperties(std::vector const& properties, boost::optional> const& propertyFilter); - template - std::shared_ptr> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas) { - storm::builder::BuilderOptions options(formulas); - - if (storm::settings::getModule().isBuildFullModelSet()) { - options.setBuildAllLabels(); - options.setBuildAllRewardModels(); - options.clearTerminalStates(); - } - - // Generate command labels if we are going to build a counterexample later. - if (storm::settings::getModule().isMinimalCommandSetGenerationSet()) { - options.setBuildChoiceLabels(true); - } - - if (storm::settings::getModule().isJitSet()) { - STORM_LOG_THROW(model.isJaniModel(), storm::exceptions::NotSupportedException, "Cannot use JIT-based model builder for non-JANI model."); - - storm::builder::jit::ExplicitJitJaniModelBuilder builder(model.asJaniModel(), options); - - if (storm::settings::getModule().isDoctorSet()) { - bool result = builder.doctor(); - STORM_LOG_THROW(result, storm::exceptions::InvalidSettingsException, "The JIT-based model builder cannot be used on your system."); - STORM_LOG_INFO("The JIT-based model builder seems to be working."); - } - - return builder.build(); - } else { - std::shared_ptr> generator; - if (model.isPrismProgram()) { - generator = std::make_shared>(model.asPrismProgram(), options); - } else if (model.isJaniModel()) { - generator = std::make_shared>(model.asJaniModel(), options); - } else { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot build sparse model from this symbolic model description."); - } - storm::builder::ExplicitModelBuilder builder(generator); - return builder.build(); - } - } - - template - std::shared_ptr> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas) { - if (model.isPrismProgram()) { - typename storm::builder::DdPrismModelBuilder::Options options; - options = typename storm::builder::DdPrismModelBuilder::Options(formulas); - - storm::builder::DdPrismModelBuilder builder; - return builder.build(model.asPrismProgram(), options); - } else { - STORM_LOG_THROW(model.isJaniModel(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model for the given symbolic model description."); - typename storm::builder::DdJaniModelBuilder::Options options; - options = typename storm::builder::DdJaniModelBuilder::Options(formulas); - - storm::builder::DdJaniModelBuilder builder; - return builder.build(model.asJaniModel(), options); - } - } - template std::shared_ptr performDeterministicSparseBisimulationMinimization(std::shared_ptr model, std::vector> const& formulas, storm::storage::BisimulationType type) { STORM_LOG_INFO("Performing bisimulation minimization... "); @@ -310,7 +231,7 @@ namespace storm { if (useMILP) { storm::counterexamples::MILPMinimalLabelSetGenerator::computeCounterexample(program, *mdp, formula); } else { - storm::counterexamples::SMTMinimalCommandSetGenerator::computeCounterexample(program, storm::settings::getModule().getConstantDefinitionString(), *mdp, formula); + storm::counterexamples::SMTMinimalCommandSetGenerator::computeCounterexample(program, *mdp, formula); } } else { @@ -758,27 +679,6 @@ namespace storm { return result; } - template - std::unique_ptr verifySymbolicModelWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, std::shared_ptr const& formula, bool onlyInitialStatesRelevant = false) { - - STORM_LOG_THROW(model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::DTMC || model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Can only treat DTMCs/MDPs using the abstraction refinement engine."); - - if (model.getModelType() == storm::storage::SymbolicModelDescription::ModelType::DTMC) { - storm::modelchecker::GameBasedMdpModelChecker> modelchecker(model); - storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); - return modelchecker.check(task); - } else { - storm::modelchecker::GameBasedMdpModelChecker> modelchecker(model); - storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); - return modelchecker.check(task); - } - } - - /** - * - */ - void exportJaniModel(storm::jani::Model const& model, std::vector const& properties, std::string const& filepath); - template void exportMatrixToFile(std::shared_ptr> model, std::string const& filepath) { STORM_LOG_THROW(model->getType() != storm::models::ModelType::Ctmc, storm::exceptions::NotImplementedException, "This functionality is not yet implemented." ); diff --git a/src/storm/utility/vector.h b/src/storm/utility/vector.h index 76fc58a5c..4931e5fad 100644 --- a/src/storm/utility/vector.h +++ b/src/storm/utility/vector.h @@ -10,7 +10,7 @@ #include #include #include -#include +#include #include diff --git a/src/test/abstraction/PrismMenuGameTest.cpp b/src/test/abstraction/PrismMenuGameTest.cpp index e95760b93..a200c1d68 100644 --- a/src/test/abstraction/PrismMenuGameTest.cpp +++ b/src/test/abstraction/PrismMenuGameTest.cpp @@ -17,7 +17,7 @@ #include "storm/utility/solver.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/AbstractionSettings.h" diff --git a/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp b/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp index 0314c3e56..3cd2910de 100644 --- a/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp +++ b/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp @@ -3,7 +3,7 @@ #ifdef STORM_HAVE_CARL -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/storm.h" diff --git a/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp b/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp index 81832d240..1cb6f61fd 100644 --- a/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp +++ b/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp @@ -3,7 +3,7 @@ #ifdef STORM_HAVE_CARL -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/storm.h" diff --git a/src/test/storage/SylvanDdTest.cpp b/src/test/storage/SylvanDdTest.cpp index 6c426fc4b..4b8ec2f38 100644 --- a/src/test/storage/SylvanDdTest.cpp +++ b/src/test/storage/SylvanDdTest.cpp @@ -1,7 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/storage/dd/DdManager.h" #include "storm/storage/dd/Add.h" diff --git a/src/test/utility/ModelInstantiatorTest.cpp b/src/test/utility/ModelInstantiatorTest.cpp index 646b51f2d..2f317a16d 100644 --- a/src/test/utility/ModelInstantiatorTest.cpp +++ b/src/test/utility/ModelInstantiatorTest.cpp @@ -3,7 +3,7 @@ #ifdef STORM_HAVE_CARL -#include "storm/adapters/CarlAdapter.h" +#include "storm/adapters/RationalFunctionAdapter.h" #include #include