From ae57574d85ef923d44f0cfeea76f9b00f36a863c Mon Sep 17 00:00:00 2001 From: sjunges <sebastian.junges@rwth-aachen.de> Date: Wed, 5 Oct 2016 22:22:22 +0200 Subject: [PATCH 01/30] first version of explicit format export [mdps/no rewards only currently] Former-commit-id: 078efab44d4311ebb12a03d66f30937534e16251 [formerly a1a444a014f5c8e2181dd24f959fbc57338257bf] Former-commit-id: 321bc64e6f1038b9131b39458db78b4ca1deb87b --- src/cli/entrypoints.h | 9 ++++ src/settings/modules/IOSettings.cpp | 12 ++++- src/settings/modules/IOSettings.h | 18 ++++++- src/storage/SymbolicModelDescription.cpp | 14 ++++++ src/storage/SymbolicModelDescription.h | 2 + src/utility/ExplicitExporter.cpp | 62 ++++++++++++++++++++++++ src/utility/ExplicitExporter.h | 15 ++++++ 7 files changed, 129 insertions(+), 3 deletions(-) create mode 100644 src/utility/ExplicitExporter.cpp create mode 100644 src/utility/ExplicitExporter.h diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index f4b009b7e..914a8153d 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -4,6 +4,7 @@ #include "src/utility/storm.h" #include "src/storage/SymbolicModelDescription.h" +#include "src/utility/ExplicitExporter.h" #include "src/exceptions/NotImplementedException.h" #include "src/exceptions/InvalidSettingsException.h" @@ -216,6 +217,14 @@ namespace storm { } else { verifySparseModel<ValueType>(sparseModel, formulas, onlyInitialStatesRelevant); } + + // And export if required. + if(storm::settings::getModule<storm::settings::modules::IOSettings>().isExportExplicitSet()) { + std::ofstream ofs; + ofs.open(storm::settings::getModule<storm::settings::modules::IOSettings>().getExportExplicitFilename(), std::ofstream::out); + storm::exporter::explicitExportSparseModel(ofs, sparseModel, model.getParameterNames()); + ofs.close(); + } } template<typename ValueType> diff --git a/src/settings/modules/IOSettings.cpp b/src/settings/modules/IOSettings.cpp index c174f1f51..cea559f4e 100644 --- a/src/settings/modules/IOSettings.cpp +++ b/src/settings/modules/IOSettings.cpp @@ -14,7 +14,7 @@ namespace storm { const std::string IOSettings::moduleName = "io"; const std::string IOSettings::exportDotOptionName = "exportdot"; - const std::string IOSettings::exportMatOptionName = "exportmat"; + const std::string IOSettings::exportExplicitOptionName = "exportexplicit"; const std::string IOSettings::explicitOptionName = "explicit"; const std::string IOSettings::explicitOptionShortName = "exp"; const std::string IOSettings::prismInputOptionName = "prism"; @@ -34,7 +34,7 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, prismCompatibilityOptionName, false, "Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportDotOptionName, "", "If given, the loaded model will be written to the specified file in the dot format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, exportMatOptionName, "", "If given, the loaded model will be written to the specified file in the mat format.") + this->addOption(storm::settings::OptionBuilder(moduleName, exportExplicitOptionName, "", "If given, the loaded model will be written to the specified file in the drn format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the file to which the model is to be writen.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, explicitOptionName, false, "Parses the model given in an explicit (sparse) representation.").setShortName(explicitOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("transition filename", "The name of the file from which to read the transitions.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()) @@ -66,6 +66,14 @@ namespace storm { std::string IOSettings::getExportDotFilename() const { return this->getOption(exportDotOptionName).getArgumentByName("filename").getValueAsString(); } + + bool IOSettings::isExportExplicitSet() const { + return this->getOption(exportExplicitOptionName).getHasOptionBeenSet(); + } + + std::string IOSettings::getExportExplicitFilename() const { + return this->getOption(exportExplicitOptionName).getArgumentByName("filename").getValueAsString(); + } bool IOSettings::isExplicitSet() const { return this->getOption(explicitOptionName).getHasOptionBeenSet(); diff --git a/src/settings/modules/IOSettings.h b/src/settings/modules/IOSettings.h index ae6ce6831..da4238e5c 100644 --- a/src/settings/modules/IOSettings.h +++ b/src/settings/modules/IOSettings.h @@ -35,6 +35,22 @@ namespace storm { */ std::string getExportDotFilename() const; + + /*! + * Retrieves whether the export-to-explicit option was set + * + * @return True if the export-to-explicit option was set + */ + bool isExportExplicitSet() const; + + + /*! + * Retrieves thename in which to write the model in explicit format, if the option was set. + * + * @return The name of the file in which to write the exported mode. + */ + std::string getExportExplicitFilename() const; + /*! * Retrieves whether the explicit option was set. * @@ -200,7 +216,7 @@ namespace storm { private: // Define the string names of the options as constants. static const std::string exportDotOptionName; - static const std::string exportMatOptionName; + static const std::string exportExplicitOptionName; static const std::string explicitOptionName; static const std::string explicitOptionShortName; static const std::string prismInputOptionName; diff --git a/src/storage/SymbolicModelDescription.cpp b/src/storage/SymbolicModelDescription.cpp index 4c144eff8..62440992d 100644 --- a/src/storage/SymbolicModelDescription.cpp +++ b/src/storage/SymbolicModelDescription.cpp @@ -57,6 +57,20 @@ namespace storm { return boost::get<storm::prism::Program>(modelDescription.get()); } + std::vector<std::string> SymbolicModelDescription::getParameterNames() const { + std::vector<std::string> result; + if(isJaniModel()) { + for(auto const& c : asJaniModel().getUndefinedConstants()) { + result.push_back(c.get().getName()); + } + } else { + for(auto const& c : asPrismProgram().getUndefinedConstants()) { + result.push_back(c.get().getName()); + } + } + return result; + } + SymbolicModelDescription SymbolicModelDescription::toJani(bool makeVariablesGlobal) const { if (this->isJaniModel()) { return *this; diff --git a/src/storage/SymbolicModelDescription.h b/src/storage/SymbolicModelDescription.h index 8b5b85d88..730578ac4 100644 --- a/src/storage/SymbolicModelDescription.h +++ b/src/storage/SymbolicModelDescription.h @@ -27,6 +27,8 @@ namespace storm { storm::jani::Model const& asJaniModel() const; storm::prism::Program const& asPrismProgram() const; + std::vector<std::string> getParameterNames() const; + SymbolicModelDescription toJani(bool makeVariablesGlobal = true) const; SymbolicModelDescription preprocess(std::string const& constantDefinitionString = "") const; diff --git a/src/utility/ExplicitExporter.cpp b/src/utility/ExplicitExporter.cpp new file mode 100644 index 000000000..77ff2aa1f --- /dev/null +++ b/src/utility/ExplicitExporter.cpp @@ -0,0 +1,62 @@ +#include "ExplicitExporter.h" + +#include "src/adapters/CarlAdapter.h" +#include "src/utility/macros.h" +#include "src/exceptions/NotImplementedException.h" +#include "src/models/sparse/Dtmc.h" +#include "src/models/sparse/Mdp.h" + +#include "src/models/sparse/StandardRewardModel.h" + + +namespace storm { + namespace exporter { + template<typename ValueType> + void explicitExportSparseModel(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel, std::vector<std::string> const& parameters) { + STORM_LOG_THROW(sparseModel->getType() == storm::models::ModelType::Mdp, storm::exceptions::NotImplementedException, "This functionality is not yet implemented." ); + std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp = sparseModel->template as<storm::models::sparse::Mdp<ValueType>>(); + + os << "// Exported by Storm" << std::endl; + os << "@type: mdp" << std::endl; + os << "@parameters" << std::endl; + for (auto const& p : parameters) { + os << p << " "; + } + os << std::endl; + os << "@nr_states" << std::endl << mdp->getNumberOfStates() << std::endl; + os << "@model" << std::endl; + storm::storage::SparseMatrix<ValueType> const& matrix = mdp->getTransitionMatrix(); + + for (typename storm::storage::SparseMatrix<ValueType>::index_type group = 0; group < matrix.getRowGroupCount(); ++group) { + os << "state " << group; + for(auto const& label : mdp->getStateLabeling().getLabelsOfState(group)) { + os << " " << label; + } + os << std::endl; + typename storm::storage::SparseMatrix<ValueType>::index_type start = matrix.getRowGroupIndices()[group]; + typename storm::storage::SparseMatrix<ValueType>::index_type end = matrix.getRowGroupIndices()[group + 1]; + + for (typename storm::storage::SparseMatrix<ValueType>::index_type i = start; i < end; ++i) { + // Print the actual row. + os << "\taction"; + if(mdp->hasChoiceLabeling()) { + //TODO + } + os << std::endl; + for(auto it = matrix.begin(i); it != matrix.end(i); ++it) { + os << "\t\t" << it->getColumn() << " : " << it->getValue() << std::endl; + } + + } + } + + } + + + + template void explicitExportSparseModel<double>(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<double>> sparseModel, std::vector<std::string> const& parameters); + + template void explicitExportSparseModel<storm::RationalNumber>(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> sparseModel, std::vector<std::string> const& parameters); + template void explicitExportSparseModel<storm::RationalFunction>(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> sparseModel, std::vector<std::string> const& parameters); + } +} \ No newline at end of file diff --git a/src/utility/ExplicitExporter.h b/src/utility/ExplicitExporter.h new file mode 100644 index 000000000..fd158f001 --- /dev/null +++ b/src/utility/ExplicitExporter.h @@ -0,0 +1,15 @@ +#pragma once +#include <iostream> +#include <memory> + +#include "src/models/sparse/Model.h" + +namespace storm { + namespace exporter { + + template<typename ValueType> + void explicitExportSparseModel(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel, std::vector<std::string> const& parameters); + + + } +} \ No newline at end of file From ec830adb19df7c4280ff55314810986170d162b2 Mon Sep 17 00:00:00 2001 From: sjunges <sebastian.junges@rwth-aachen.de> Date: Mon, 10 Oct 2016 16:58:43 +0200 Subject: [PATCH 02/30] added labels for error in pdtmc/brp Former-commit-id: 94e0376aa6628c54e5f8bad29f550f0b76d37dc7 [formerly a58bf3787e9e1816420e6ba5bf371d9394820f4e] Former-commit-id: c525fd395db9c98d8007caa9a505a5b9329501b6 --- examples/pdtmc/brp/brp.pm | 1 + examples/pdtmc/brp/brp16_2.pm | 2 ++ examples/pdtmc/brp_rewards2/brp_rewards16_2.pm | 2 ++ examples/pdtmc/brp_rewards4/brp_rewards16_2.pm | 2 ++ 4 files changed, 7 insertions(+) diff --git a/examples/pdtmc/brp/brp.pm b/examples/pdtmc/brp/brp.pm index 897f9909e..7a3cb325b 100644 --- a/examples/pdtmc/brp/brp.pm +++ b/examples/pdtmc/brp/brp.pm @@ -133,3 +133,4 @@ module channelL [TO_Ack] (l=2) -> (l'=0); endmodule + diff --git a/examples/pdtmc/brp/brp16_2.pm b/examples/pdtmc/brp/brp16_2.pm index 2e20b7de4..0fc99d05e 100644 --- a/examples/pdtmc/brp/brp16_2.pm +++ b/examples/pdtmc/brp/brp16_2.pm @@ -133,3 +133,5 @@ module channelL [TO_Ack] (l=2) -> (l'=0); endmodule + +label "error" = s=5; diff --git a/examples/pdtmc/brp_rewards2/brp_rewards16_2.pm b/examples/pdtmc/brp_rewards2/brp_rewards16_2.pm index 0b05d22fd..7145a77ae 100644 --- a/examples/pdtmc/brp_rewards2/brp_rewards16_2.pm +++ b/examples/pdtmc/brp_rewards2/brp_rewards16_2.pm @@ -144,3 +144,5 @@ rewards endrewards +label "target" = s=5; + diff --git a/examples/pdtmc/brp_rewards4/brp_rewards16_2.pm b/examples/pdtmc/brp_rewards4/brp_rewards16_2.pm index d756a90ec..ff62fea14 100644 --- a/examples/pdtmc/brp_rewards4/brp_rewards16_2.pm +++ b/examples/pdtmc/brp_rewards4/brp_rewards16_2.pm @@ -144,3 +144,5 @@ rewards endrewards + +label "target" = s=5; \ No newline at end of file From 236a2be0d3a6d2d84847200add8a333221512d6d Mon Sep 17 00:00:00 2001 From: sjunges <sebastian.junges@rwth-aachen.de> Date: Mon, 10 Oct 2016 16:59:14 +0200 Subject: [PATCH 03/30] pretty printing of rational functions, rewards in the drn format, option for full build Former-commit-id: 39676106c2fa94eac236ae822e0caeac18dff9f8 [formerly b80f259a87fddd440451c0fd43b3cc5c5b27a9af] Former-commit-id: e6f493d6f9155d50d87ab3bde7a1f6fc9b8aaae6 --- src/settings/modules/IOSettings.cpp | 8 ++++ src/settings/modules/IOSettings.h | 8 ++++ src/utility/ExplicitExporter.cpp | 60 +++++++++++++++++++++++++---- src/utility/constants.cpp | 31 ++++++++++++++- src/utility/constants.h | 4 ++ src/utility/storm.h | 8 ++++ 6 files changed, 110 insertions(+), 9 deletions(-) diff --git a/src/settings/modules/IOSettings.cpp b/src/settings/modules/IOSettings.cpp index cea559f4e..9568389d2 100644 --- a/src/settings/modules/IOSettings.cpp +++ b/src/settings/modules/IOSettings.cpp @@ -29,6 +29,7 @@ namespace storm { const std::string IOSettings::constantsOptionShortName = "const"; const std::string IOSettings::prismCompatibilityOptionName = "prismcompat"; const std::string IOSettings::prismCompatibilityOptionShortName = "pc"; + const std::string IOSettings::fullModelBuildOptionName = "buildfull"; IOSettings::IOSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, prismCompatibilityOptionName, false, "Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build()); @@ -44,6 +45,8 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, janiInputOptionName, false, "Parses the model given in the JANI format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the JANI input.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, prismToJaniOptionName, false, "If set, the input PRISM model is transformed to JANI.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, fullModelBuildOptionName, false, "If set, include all rewards and labels.").build()); + std::vector<std::string> explorationOrders = {"dfs", "bfs"}; this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName) @@ -57,6 +60,7 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the choice labels.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that this requires the model to be given as an symbolic model (i.e., via --" + prismInputOptionName + " or --" + janiInputOptionName + ").").setShortName(constantsOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build()); + } bool IOSettings::isExportDotSet() const { @@ -164,6 +168,10 @@ namespace storm { bool IOSettings::isPrismCompatibilityEnabled() const { return this->getOption(prismCompatibilityOptionName).getHasOptionBeenSet(); } + + bool IOSettings::isBuildFullModelSet() const { + return this->getOption(fullModelBuildOptionName).getHasOptionBeenSet(); + } void IOSettings::finalize() { } diff --git a/src/settings/modules/IOSettings.h b/src/settings/modules/IOSettings.h index da4238e5c..782d9880f 100644 --- a/src/settings/modules/IOSettings.h +++ b/src/settings/modules/IOSettings.h @@ -206,6 +206,13 @@ namespace storm { * @return True iff the PRISM compatibility mode was enabled. */ bool isPrismCompatibilityEnabled() const; + + /*! + * Retrieves whether the full model should be build, that is, the model including all labels and rewards. + * + * @return true iff the full model should be build. + */ + bool isBuildFullModelSet() const; bool check() const override; void finalize() override; @@ -231,6 +238,7 @@ namespace storm { static const std::string constantsOptionShortName; static const std::string prismCompatibilityOptionName; static const std::string prismCompatibilityOptionShortName; + static const std::string fullModelBuildOptionName; }; } // namespace modules diff --git a/src/utility/ExplicitExporter.cpp b/src/utility/ExplicitExporter.cpp index 77ff2aa1f..71d968aa0 100644 --- a/src/utility/ExplicitExporter.cpp +++ b/src/utility/ExplicitExporter.cpp @@ -1,6 +1,7 @@ #include "ExplicitExporter.h" #include "src/adapters/CarlAdapter.h" +#include "src/utility/constants.h" #include "src/utility/macros.h" #include "src/exceptions/NotImplementedException.h" #include "src/models/sparse/Dtmc.h" @@ -13,7 +14,7 @@ namespace storm { namespace exporter { template<typename ValueType> void explicitExportSparseModel(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel, std::vector<std::string> const& parameters) { - STORM_LOG_THROW(sparseModel->getType() == storm::models::ModelType::Mdp, storm::exceptions::NotImplementedException, "This functionality is not yet implemented." ); + STORM_LOG_THROW(sparseModel->getType() == storm::models::ModelType::Mdp || sparseModel->getType() == storm::models::ModelType::Dtmc , storm::exceptions::NotImplementedException, "This functionality is not yet implemented." ); std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp = sparseModel->template as<storm::models::sparse::Mdp<ValueType>>(); os << "// Exported by Storm" << std::endl; @@ -23,28 +24,71 @@ namespace storm { os << p << " "; } os << std::endl; - os << "@nr_states" << std::endl << mdp->getNumberOfStates() << std::endl; + os << "@nr_states" << std::endl << sparseModel->getNumberOfStates() << std::endl; os << "@model" << std::endl; - storm::storage::SparseMatrix<ValueType> const& matrix = mdp->getTransitionMatrix(); + storm::storage::SparseMatrix<ValueType> const& matrix = sparseModel->getTransitionMatrix(); for (typename storm::storage::SparseMatrix<ValueType>::index_type group = 0; group < matrix.getRowGroupCount(); ++group) { os << "state " << group; - for(auto const& label : mdp->getStateLabeling().getLabelsOfState(group)) { + + bool first = true; + for (auto const& rewardModelEntry : sparseModel->getRewardModels()) { + if (first) { + os << " ["; + first = false; + } else { + os << ", "; + } + + if(rewardModelEntry.second.hasStateRewards()) { + os << rewardModelEntry.second.getStateRewardVector().at(group); + } else { + os << "0"; + } + + } + if (!first) { + os << "]"; + } + + for(auto const& label : sparseModel->getStateLabeling().getLabelsOfState(group)) { os << " " << label; } os << std::endl; - typename storm::storage::SparseMatrix<ValueType>::index_type start = matrix.getRowGroupIndices()[group]; - typename storm::storage::SparseMatrix<ValueType>::index_type end = matrix.getRowGroupIndices()[group + 1]; + typename storm::storage::SparseMatrix<ValueType>::index_type start = matrix.hasTrivialRowGrouping() ? group : matrix.getRowGroupIndices()[group]; + typename storm::storage::SparseMatrix<ValueType>::index_type end = matrix.hasTrivialRowGrouping() ? group + 1 : matrix.getRowGroupIndices()[group + 1]; for (typename storm::storage::SparseMatrix<ValueType>::index_type i = start; i < end; ++i) { // Print the actual row. os << "\taction"; - if(mdp->hasChoiceLabeling()) { + bool first = true; + for (auto const& rewardModelEntry : sparseModel->getRewardModels()) { + if (first) { + os << " ["; + first = false; + } else { + os << ", "; + } + + if(rewardModelEntry.second.hasStateActionRewards()) { + os << storm::utility::to_string(rewardModelEntry.second.getStateActionRewardVector().at(i)); + } else { + os << "0"; + } + + } + if (!first) { + os << "]"; + } + + + + if(sparseModel->hasChoiceLabeling()) { //TODO } os << std::endl; for(auto it = matrix.begin(i); it != matrix.end(i); ++it) { - os << "\t\t" << it->getColumn() << " : " << it->getValue() << std::endl; + os << "\t\t" << it->getColumn() << " : " << storm::utility::to_string(it->getValue()) << std::endl; } } diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp index 6d954722a..b67d0783e 100644 --- a/src/utility/constants.cpp +++ b/src/utility/constants.cpp @@ -56,7 +56,31 @@ namespace storm { bool isInteger(uint_fast64_t const& number) { return true; } - + + template<typename ValueType> + std::string to_string(ValueType const& value) { + std::stringstream ss; + ss << value; + return ss.str(); + } + + template<> + std::string to_string(RationalFunction const& f) { + std::stringstream ss; + if (f.isConstant()) { + if (f.denominator().isOne()) { + ss << f.nominatorAsNumber(); + } else { + ss << f.nominatorAsNumber() << "/" << f.denominatorAsNumber(); + } + } else if (f.denominator().isOne()) { + ss << f.nominatorAsPolynomial().coefficient() * f.nominatorAsPolynomial().polynomial(); + } else { + ss << "(" << f.nominatorAsPolynomial() << ")/(" << f.denominatorAsPolynomial() << ")"; + } + return ss.str(); + } + #ifdef STORM_HAVE_CARL template<> bool isOne(storm::RationalNumber const& a) { @@ -275,6 +299,11 @@ namespace storm { template bool isInteger(float const& number); template float simplify(float value); + + template std::string to_string(float const& value); + template std::string to_string(double const& value); + template std::string to_string(storm::RationalNumber const& value); + template std::string to_string(storm::RationalFunction const& value); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float> matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& matrixEntry); diff --git a/src/utility/constants.h b/src/utility/constants.h index 66edb9f46..8bd7841e8 100644 --- a/src/utility/constants.h +++ b/src/utility/constants.h @@ -11,6 +11,7 @@ #include <limits> #include <cstdint> +#include <string> namespace storm { @@ -59,6 +60,9 @@ namespace storm { template<typename ValueType> bool isInteger(ValueType const& number); + + template<typename ValueType> + std::string to_string(ValueType const& value); } } diff --git a/src/utility/storm.h b/src/utility/storm.h index c5df89d64..cab5dcf71 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -108,7 +108,15 @@ namespace storm { template<typename ValueType> std::shared_ptr<storm::models::sparse::Model<ValueType>> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) { + + storm::generator::NextStateGeneratorOptions options(formulas); + + + if (storm::settings::getModule<storm::settings::modules::IOSettings>().isBuildFullModelSet()) { + options.setBuildAllLabels(); + options.setBuildAllRewardModels(); + } // Generate command labels if we are going to build a counterexample later. if (storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>().isMinimalCommandSetGenerationSet()) { From 011e3fbaa65c06f67a9ca1258bfc444848bd62a4 Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Wed, 12 Oct 2016 13:54:29 +0200 Subject: [PATCH 04/30] fixed bug that introduced transient variables in the state space Former-commit-id: b335cf0c0dae3be17160ec6ca44a29c72996b6f9 [formerly 84339f7943cc25252bd8ccd6addc84401e643d2c] Former-commit-id: 6f64020873265b23e9af9cc6c816045ec13d2ce8 --- src/generator/JaniNextStateGenerator.cpp | 4 ++- src/generator/VariableInformation.cpp | 36 +++++++++++++++--------- 2 files changed, 25 insertions(+), 15 deletions(-) diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index bc166cba3..10053d777 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -178,17 +178,19 @@ namespace storm { std::shared_ptr<storm::solver::SmtSolver::ModelReference> model = solver->getModel(); for (auto const& booleanVariable : this->variableInformation.booleanVariables) { bool variableValue = model->getBooleanValue(booleanVariable.variable); + std::cout << booleanVariable.variable.getName() << " has val " << variableValue << std::endl; storm::expressions::Expression localBlockingExpression = variableValue ? !booleanVariable.variable : booleanVariable.variable; blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression; initialState.set(booleanVariable.bitOffset, variableValue); } for (auto const& integerVariable : this->variableInformation.integerVariables) { int_fast64_t variableValue = model->getIntegerValue(integerVariable.variable); + std::cout << integerVariable.variable.getName() << " has val " << variableValue << std::endl; storm::expressions::Expression localBlockingExpression = integerVariable.variable != model->getManager().integer(variableValue); blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression; initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast<uint_fast64_t>(variableValue - integerVariable.lowerBound)); } - + // Gather iterators to the initial locations of all the automata. std::vector<std::set<uint64_t>::const_iterator> initialLocationsIterators; uint64_t currentLocationVariable = 0; diff --git a/src/generator/VariableInformation.cpp b/src/generator/VariableInformation.cpp index c1a00e4e6..3545f1e49 100644 --- a/src/generator/VariableInformation.cpp +++ b/src/generator/VariableInformation.cpp @@ -63,15 +63,19 @@ namespace storm { } for (auto const& variable : model.getGlobalVariables().getBooleanVariables()) { - booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset, true); - ++totalBitOffset; + if (!variable.isTransient()) { + booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset, true); + ++totalBitOffset; + } } for (auto const& variable : model.getGlobalVariables().getBoundedIntegerVariables()) { - int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt(); - int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt(); - uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1))); - integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true); - totalBitOffset += bitwidth; + if (!variable.isTransient()) { + int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt(); + int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt(); + uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1))); + integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true); + totalBitOffset += bitwidth; + } } for (auto const& automaton : model.getAutomata()) { uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(automaton.getNumberOfLocations()))); @@ -79,15 +83,19 @@ namespace storm { totalBitOffset += bitwidth; for (auto const& variable : automaton.getVariables().getBooleanVariables()) { - booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset); - ++totalBitOffset; + if (!variable.isTransient()) { + booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset); + ++totalBitOffset; + } } for (auto const& variable : automaton.getVariables().getBoundedIntegerVariables()) { - int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt(); - int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt(); - uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1))); - integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth); - totalBitOffset += bitwidth; + if (!variable.isTransient()) { + int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt(); + int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt(); + uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1))); + integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth); + totalBitOffset += bitwidth; + } } } From 91e6bb299923773a89fcb9ea649465f7a9283c7c Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Wed, 12 Oct 2016 15:14:47 +0200 Subject: [PATCH 05/30] fixed bug in DD-based JANI model generation related to transient edge assignments Former-commit-id: b2cf168189706f22201bf54c00cd0f822acbbd14 [formerly 0c50ca2d16cc56b2c1a12db38b6736d79e6780c7] Former-commit-id: 05686fd6f1b6198355e31940b5b764998047810a --- src/builder/DdJaniModelBuilder.cpp | 8 +++++--- src/generator/JaniNextStateGenerator.cpp | 2 -- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index 8b54e0eba..1b759cfc5 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -895,7 +895,6 @@ namespace storm { if (action.isInputEnabled()) { // If the action is input-enabled, we add self-loops to all states. transitions *= actionGuard.ite(action.transitions, encodeIndex(0, action.getLowestLocalNondeterminismVariable(), action.getHighestLocalNondeterminismVariable() - action.getLowestLocalNondeterminismVariable(), this->variables) * actionIdentityPair.second); - actionGuard.ite(action.transitions, encodeIndex(0, action.getLowestLocalNondeterminismVariable(), action.getHighestLocalNondeterminismVariable() - action.getLowestLocalNondeterminismVariable(), this->variables) * actionIdentityPair.second).exportToDot("this.dot"); } else { transitions *= action.transitions; } @@ -1107,7 +1106,8 @@ namespace storm { } // Add the source location and the guard. - transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd<ValueType>() * guard; + storm::dd::Add<Type, ValueType> sourceLocationAndGuard = this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd<ValueType>() * guard; + transitions *= sourceLocationAndGuard; // If we multiply the ranges of global variables, make sure everything stays within its bounds. if (!globalVariablesInSomeDestination.empty()) { @@ -1124,7 +1124,9 @@ namespace storm { // Finally treat the transient assignments. std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientEdgeAssignments; if (!this->transientVariables.empty()) { - performTransientAssignments(edge.getAssignments().getTransientAssignments(), [this, &transientEdgeAssignments, &guard] (storm::jani::Assignment const& assignment) { transientEdgeAssignments[assignment.getExpressionVariable()] = guard * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression()); } ); + performTransientAssignments(edge.getAssignments().getTransientAssignments(), [this, &transientEdgeAssignments, &guard, &sourceLocationAndGuard] (storm::jani::Assignment const& assignment) { + transientEdgeAssignments[assignment.getExpressionVariable()] = sourceLocationAndGuard * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression()); + } ); } return EdgeDd(isMarkovian, guard, guard * transitions, transientEdgeAssignments, globalVariablesInSomeDestination); diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index 10053d777..b2c786b77 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -178,14 +178,12 @@ namespace storm { std::shared_ptr<storm::solver::SmtSolver::ModelReference> model = solver->getModel(); for (auto const& booleanVariable : this->variableInformation.booleanVariables) { bool variableValue = model->getBooleanValue(booleanVariable.variable); - std::cout << booleanVariable.variable.getName() << " has val " << variableValue << std::endl; storm::expressions::Expression localBlockingExpression = variableValue ? !booleanVariable.variable : booleanVariable.variable; blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression; initialState.set(booleanVariable.bitOffset, variableValue); } for (auto const& integerVariable : this->variableInformation.integerVariables) { int_fast64_t variableValue = model->getIntegerValue(integerVariable.variable); - std::cout << integerVariable.variable.getName() << " has val " << variableValue << std::endl; storm::expressions::Expression localBlockingExpression = integerVariable.variable != model->getManager().integer(variableValue); blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression; initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast<uint_fast64_t>(variableValue - integerVariable.lowerBound)); From afb01572b962f5cf2e54593fd487d4c22a38d9cc Mon Sep 17 00:00:00 2001 From: sjunges <sebastian.junges@rwth-aachen.de> Date: Wed, 12 Oct 2016 21:11:45 +0200 Subject: [PATCH 06/30] support for ctmcs Former-commit-id: 114aff76bbbfecdb2f6f55e40d56522cb937511e [formerly da14316bc6f8abaca6c30bd997d87b0b889a4ac3] Former-commit-id: 51558945d4fac1cc796b19b157de9858417a2c94 --- src/utility/ExplicitExporter.cpp | 101 ++++++++++++++++++++----------- 1 file changed, 66 insertions(+), 35 deletions(-) diff --git a/src/utility/ExplicitExporter.cpp b/src/utility/ExplicitExporter.cpp index 71d968aa0..c29684fad 100644 --- a/src/utility/ExplicitExporter.cpp +++ b/src/utility/ExplicitExporter.cpp @@ -6,6 +6,8 @@ #include "src/exceptions/NotImplementedException.h" #include "src/models/sparse/Dtmc.h" #include "src/models/sparse/Mdp.h" +#include "src/models/sparse/Ctmc.h" +#include "src/models/sparse/MarkovAutomaton.h" #include "src/models/sparse/StandardRewardModel.h" @@ -14,10 +16,23 @@ namespace storm { namespace exporter { template<typename ValueType> void explicitExportSparseModel(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel, std::vector<std::string> const& parameters) { - STORM_LOG_THROW(sparseModel->getType() == storm::models::ModelType::Mdp || sparseModel->getType() == storm::models::ModelType::Dtmc , storm::exceptions::NotImplementedException, "This functionality is not yet implemented." ); - std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp = sparseModel->template as<storm::models::sparse::Mdp<ValueType>>(); - + bool embedded = false; + if(sparseModel->getType() == storm::models::ModelType::Ctmc || sparseModel->getType() == storm::models::ModelType::MarkovAutomaton) { + STORM_LOG_WARN("This format only supports discrete time models"); + embedded = true; + } + + STORM_LOG_THROW(embedded || sparseModel->getType() == storm::models::ModelType::Mdp || sparseModel->getType() == storm::models::ModelType::Dtmc , storm::exceptions::NotImplementedException, "This functionality is not yet implemented." ); + + std::vector<ValueType> exitRates; // Only for CTMCs and MAs. + if(sparseModel->getType() == storm::models::ModelType::Ctmc) { + exitRates = sparseModel->template as<storm::models::sparse::Ctmc<ValueType>>()->getExitRateVector(); + } else if(sparseModel->getType() == storm::models::ModelType::MarkovAutomaton) { + exitRates = sparseModel->template as<storm::models::sparse::MarkovAutomaton<ValueType>>()->getExitRates(); + } + os << "// Exported by Storm" << std::endl; + os << "// Original model type: " << sparseModel->getType() << std::endl; os << "@type: mdp" << std::endl; os << "@parameters" << std::endl; for (auto const& p : parameters) { @@ -31,24 +46,29 @@ namespace storm { for (typename storm::storage::SparseMatrix<ValueType>::index_type group = 0; group < matrix.getRowGroupCount(); ++group) { os << "state " << group; - bool first = true; - for (auto const& rewardModelEntry : sparseModel->getRewardModels()) { - if (first) { - os << " ["; - first = false; - } else { - os << ", "; + if (!embedded) { + bool first = true; + for (auto const& rewardModelEntry : sparseModel->getRewardModels()) { + if (first) { + os << " ["; + first = false; + } else { + os << ", "; + } + + if(rewardModelEntry.second.hasStateRewards()) { + os << rewardModelEntry.second.getStateRewardVector().at(group); + } else { + os << "0"; + } } - if(rewardModelEntry.second.hasStateRewards()) { - os << rewardModelEntry.second.getStateRewardVector().at(group); - } else { - os << "0"; + if (!first) { + os << "]"; } - - } - if (!first) { - os << "]"; + } else { + // We currently only support the expected time. + os << " [" << storm::utility::one<ValueType>()/exitRates.at(group) << "]"; } for(auto const& label : sparseModel->getStateLabeling().getLabelsOfState(group)) { @@ -61,24 +81,28 @@ namespace storm { for (typename storm::storage::SparseMatrix<ValueType>::index_type i = start; i < end; ++i) { // Print the actual row. os << "\taction"; - bool first = true; - for (auto const& rewardModelEntry : sparseModel->getRewardModels()) { - if (first) { - os << " ["; - first = false; - } else { - os << ", "; + if (!embedded) { + bool first = true; + for (auto const& rewardModelEntry : sparseModel->getRewardModels()) { + if (first) { + os << " ["; + first = false; + } else { + os << ", "; + } + + if(rewardModelEntry.second.hasStateActionRewards()) { + os << storm::utility::to_string(rewardModelEntry.second.getStateActionRewardVector().at(i)); + } else { + os << "0"; + } + } - - if(rewardModelEntry.second.hasStateActionRewards()) { - os << storm::utility::to_string(rewardModelEntry.second.getStateActionRewardVector().at(i)); - } else { - os << "0"; + if (!first) { + os << "]"; } - - } - if (!first) { - os << "]"; + } else { + // We currently only support the expected time. } @@ -87,8 +111,15 @@ namespace storm { //TODO } os << std::endl; + + for(auto it = matrix.begin(i); it != matrix.end(i); ++it) { - os << "\t\t" << it->getColumn() << " : " << storm::utility::to_string(it->getValue()) << std::endl; + ValueType prob = it->getValue(); + if(embedded) { + prob = prob / exitRates.at(group); + } + os << "\t\t" << it->getColumn() << " : "; + os << storm::utility::to_string(prob) << std::endl; } } From 40ea6eeecd85085f54d992c48b97d6cd015842b3 Mon Sep 17 00:00:00 2001 From: sjunges <sebastian.junges@rwth-aachen.de> Date: Wed, 12 Oct 2016 21:12:13 +0200 Subject: [PATCH 07/30] pctmc example Former-commit-id: 22aa41bdd1a81d86e40327220dfd43d3c4b407e1 [formerly ea552f454c9d0cb586541ae70e2339faa97ba0f8] Former-commit-id: 5231d96db57ed07ce82c515b8bddfc96c2901f72 --- examples/pctmc/polling6.sm | 83 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 83 insertions(+) create mode 100644 examples/pctmc/polling6.sm diff --git a/examples/pctmc/polling6.sm b/examples/pctmc/polling6.sm new file mode 100644 index 000000000..cb4faa90c --- /dev/null +++ b/examples/pctmc/polling6.sm @@ -0,0 +1,83 @@ +// polling example [IT90] +// gxn/dxp 26/01/00 + +ctmc + +const int N=6; + +const double mu; +const double gamma; + +//const double mu= 1; +//const double gamma= 200; +//const double lambda= mu/N; + +module server + + s : [1..6]; // station + a : [0..1]; // action: 0=polling, 1=serving + + [loop1a] (s=1)&(a=0) -> gamma : (s'=s+1); + [loop1b] (s=1)&(a=0) -> gamma : (a'=1); + [serve1] (s=1)&(a=1) -> mu : (s'=s+1)&(a'=0); + + [loop2a] (s=2)&(a=0) -> gamma : (s'=s+1); + [loop2b] (s=2)&(a=0) -> gamma : (a'=1); + [serve2] (s=2)&(a=1) -> mu : (s'=s+1)&(a'=0); + + [loop3a] (s=3)&(a=0) -> gamma : (s'=s+1); + [loop3b] (s=3)&(a=0) -> gamma : (a'=1); + [serve3] (s=3)&(a=1) -> mu : (s'=s+1)&(a'=0); + + [loop4a] (s=4)&(a=0) -> gamma : (s'=s+1); + [loop4b] (s=4)&(a=0) -> gamma : (a'=1); + [serve4] (s=4)&(a=1) -> mu : (s'=s+1)&(a'=0); + + [loop5a] (s=5)&(a=0) -> gamma : (s'=s+1); + [loop5b] (s=5)&(a=0) -> gamma : (a'=1); + [serve5] (s=5)&(a=1) -> mu : (s'=s+1)&(a'=0); + + [loop6a] (s=6)&(a=0) -> gamma : (s'=1); + [loop6b] (s=6)&(a=0) -> gamma : (a'=1); + [serve6] (s=6)&(a=1) -> mu : (s'=1)&(a'=0); + +endmodule + +module station1 + + s1 : [0..1]; + + [loop1a] (s1=0) -> 1 : (s1'=0); + [] (s1=0) -> mu/N : (s1'=1); + [loop1b] (s1=1) -> 1 : (s1'=1); + [serve1] (s1=1) -> 1 : (s1'=0); + +endmodule + +// construct further stations through renaming +module station2 = station1 [s1=s2, loop1a=loop2a, loop1b=loop2b, serve1=serve2] endmodule +module station3 = station1 [s1=s3, loop1a=loop3a, loop1b=loop3b, serve1=serve3] endmodule +module station4 = station1 [s1=s4, loop1a=loop4a, loop1b=loop4b, serve1=serve4] endmodule +module station5 = station1 [s1=s5, loop1a=loop5a, loop1b=loop5b, serve1=serve5] endmodule +module station6 = station1 [s1=s6, loop1a=loop6a, loop1b=loop6b, serve1=serve6] endmodule + +// cumulative rewards + +//rewards "waiting" // expected time the station 1 is waiting to be served +// s1=1 & !(s=1 & a=1) : 1; +//endrewards + +//rewards "served" // expected number of times station1 is served +// [serve1] true : 1; +//endrewards + +init +s = 1 & +a = 0 & +s1 = 0 & +s2 = 0 & +s3 = 0 & +s4 = 0 & +s5 = 0 & +s6 = 0 +endinit From ba0d81ca52172d4bd68fbf10c7a60a3714dc29d2 Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Wed, 12 Oct 2016 21:13:09 +0200 Subject: [PATCH 08/30] bugfix for PRISM program: only check initial values of variables if they have one Former-commit-id: c5c548bd62f28b1d2cdc70bb75f7c84d12233c62 [formerly c27c72bd59e9f07a05cb8e9c5f56b65906ff7a2f] Former-commit-id: 97acb66693b15d0464a7dbc15c70a13c73f60f10 --- src/storage/prism/Module.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp index 095ac3e11..0a4347396 100644 --- a/src/storage/prism/Module.cpp +++ b/src/storage/prism/Module.cpp @@ -196,12 +196,12 @@ namespace storm { bool Module::containsVariablesOnlyInUpdateProbabilities(std::set<storm::expressions::Variable> const& undefinedConstantVariables) const { for (auto const& booleanVariable : this->getBooleanVariables()) { - if (booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) { + if (booleanVariable.hasInitialValue() && booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) { return false; } } for (auto const& integerVariable : this->getIntegerVariables()) { - if (integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) { + if (integerVariable.hasInitialValue() && integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) { return false; } if (integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) { From aee1956950574f7eec41df0c4fde4ce6fa11b9ee Mon Sep 17 00:00:00 2001 From: sjunges <sebastian.junges@rwth-aachen.de> Date: Thu, 13 Oct 2016 15:03:57 +0200 Subject: [PATCH 09/30] progress towards JANI formula support, fix for gcc Former-commit-id: 66d87dbe8c40c58166f90e538fd647ac33955a12 [formerly ac7ce466a1c796d6356af6ba0bcdb03672a721c7] Former-commit-id: ec11ee9831b08c93c45f758ac62d4803b2b0545c --- src/storage/jani/JSONExporter.cpp | 197 ++++++++++++++++++++++++++++++ src/storage/jani/JSONExporter.h | 27 ++++ src/storage/jani/Property.cpp | 15 +-- src/storage/jani/Property.h | 32 +++-- src/storage/ppg/defines.h | 2 + 5 files changed, 257 insertions(+), 16 deletions(-) diff --git a/src/storage/jani/JSONExporter.cpp b/src/storage/jani/JSONExporter.cpp index 3493affe4..be30b82b8 100644 --- a/src/storage/jani/JSONExporter.cpp +++ b/src/storage/jani/JSONExporter.cpp @@ -6,6 +6,7 @@ #include "src/utility/macros.h" #include "src/exceptions/FileIoException.h" +#include "src/exceptions/NotSupportedException.h" #include "src/exceptions/InvalidJaniException.h" @@ -20,6 +21,8 @@ #include "src/storage/expressions/BinaryRelationExpression.h" #include "src/storage/expressions/VariableExpression.h" +#include "src/logic/Formulas.h" + #include "src/storage/jani/AutomatonComposition.h" #include "src/storage/jani/ParallelComposition.h" @@ -85,6 +88,200 @@ namespace storm { bool allowRecursion; }; + std::string comparisonTypeToJani(storm::logic::ComparisonType ct) { + switch(ct) { + case storm::logic::ComparisonType::Less: + return "<"; + case storm::logic::ComparisonType::LessEqual: + return "≤"; + case storm::logic::ComparisonType::Greater: + return ">"; + case storm::logic::ComparisonType::GreaterEqual: + return "≥"; + } + } + + modernjson::json numberToJson(storm::RationalNumber rn) { + modernjson::json numDecl; + if(carl::isOne(carl::getDenom(rn))) { + numDecl = modernjson::json(carl::toString(carl::getNum(rn))); + } else { + numDecl["op"] = "/"; + numDecl["left"] = carl::toString(carl::getNum(rn)); + numDecl["right"] = carl::toString(carl::getDenom(rn)); + } + return numDecl; + } + + + modernjson::json constructPropertyInterval(uint64_t lower, uint64_t upper) { + modernjson::json iDecl; + iDecl["lower"] = lower; + iDecl["upper"] = upper; + return iDecl; + } + + modernjson::json constructPropertyInterval(double lower, double upper) { + modernjson::json iDecl; + iDecl["lower"] = lower; + iDecl["upper"] = upper; + return iDecl; + } + + boost::any FormulaToJaniJson::visit(storm::logic::AtomicExpressionFormula const& f, boost::any const& data) const { + return ExpressionToJson::translate(f.getExpression()); + } + + boost::any FormulaToJaniJson::visit(storm::logic::AtomicLabelFormula const& f, boost::any const& data) const { + modernjson::json opDecl(f.isTrueFormula() ? "true" : "false"); + return opDecl; + } + boost::any FormulaToJaniJson::visit(storm::logic::BinaryBooleanStateFormula const& f, boost::any const& data) const{ + modernjson::json opDecl; + storm::logic::BinaryBooleanStateFormula::OperatorType op = f.getOperator(); + opDecl["op"] = op == storm::logic::BinaryBooleanStateFormula::OperatorType::And ? "∧" : "∨"; + opDecl["left"] = boost::any_cast<modernjson::json>(f.getLeftSubformula().accept(*this, boost::none)); + opDecl["right"] = boost::any_cast<modernjson::json>(f.getRightSubformula().accept(*this, boost::none)); + return opDecl; + } + boost::any FormulaToJaniJson::visit(storm::logic::BooleanLiteralFormula const& f, boost::any const& data) const { + modernjson::json opDecl(f.isTrueFormula() ? "true" : "false"); + return opDecl; + } + boost::any FormulaToJaniJson::visit(storm::logic::BoundedUntilFormula const& f, boost::any const& data) const { + modernjson::json opDecl; + opDecl["op"] = "U"; + opDecl["left"] = boost::any_cast<modernjson::json>(f.getLeftSubformula().accept(*this, boost::none)); + opDecl["right"] = boost::any_cast<modernjson::json>(f.getRightSubformula().accept(*this, boost::none)); + if(f.hasDiscreteTimeBound()) { + opDecl["step-bounds"] = constructPropertyInterval(0, f.getDiscreteTimeBound()); + } else { + opDecl["time-bounds"] = constructPropertyInterval(f.getIntervalBounds().first, f.getIntervalBounds().second); + } + return opDecl; + } + + boost::any FormulaToJaniJson::visit(storm::logic::ConditionalFormula const& f, boost::any const& data) const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani currently does not support conditional formulae"); + } + + boost::any FormulaToJaniJson::visit(storm::logic::CumulativeRewardFormula const& f, boost::any const& data) const { + + } + + boost::any FormulaToJaniJson::visit(storm::logic::EventuallyFormula const& f, boost::any const& data) const { + modernjson::json opDecl; + opDecl["op"] = "U"; + opDecl["left"] = boost::any_cast<modernjson::json>(f.getTrueFormula()->accept(*this, boost::none)); + opDecl["right"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none)); + return opDecl; + } + + boost::any FormulaToJaniJson::visit(storm::logic::TimeOperatorFormula const& f, boost::any const& data) const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani currently does not support conditional formulae"); + + } + + boost::any FormulaToJaniJson::visit(storm::logic::GloballyFormula const& f, boost::any const& data) const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani currently does not support conditional formulae"); + } + + boost::any FormulaToJaniJson::visit(storm::logic::InstantaneousRewardFormula const& f, boost::any const& data) const { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani currently does not support conditional formulae"); + } + + boost::any FormulaToJaniJson::visit(storm::logic::LongRunAverageOperatorFormula const& f, boost::any const& data) const { + modernjson::json opDecl; + if(f.hasBound()) { + auto bound = f.getBound(); + opDecl["op"] = comparisonTypeToJani(bound.comparisonType); + if(f.hasOptimalityType()) { + opDecl["left"]["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Smin" : "Smax"; + opDecl["left"]["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none)); + } else { + opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Smax" : "Smin"; + opDecl["left"]["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none)); + } + opDecl["right"] = numberToJson(bound.threshold); + } else { + if(f.hasOptimalityType()) { + opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Smin" : "Smax"; + opDecl["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none)); + + } else { + // TODO add checks + opDecl["op"] = "Pmin"; + opDecl["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none)); + } + } + return opDecl; + + } + + boost::any FormulaToJaniJson::visit(storm::logic::LongRunAverageRewardFormula const& f, boost::any const& data) const { + + } + + boost::any FormulaToJaniJson::visit(storm::logic::NextFormula const& f, boost::any const& data) const { + modernjson::json opDecl; + opDecl["op"] = "U"; + opDecl["left"] = boost::any_cast<modernjson::json>(f.getTrueFormula()->accept(*this, boost::none)); + opDecl["right"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none)); + opDecl["step-bounds"] = constructPropertyInterval((uint64_t)1, (uint64_t)1); + return opDecl; + } + + + + + boost::any FormulaToJaniJson::visit(storm::logic::ProbabilityOperatorFormula const& f, boost::any const& data) const { + modernjson::json opDecl; + + if(f.hasBound()) { + auto bound = f.getBound(); + opDecl["op"] = comparisonTypeToJani(bound.comparisonType); + if(f.hasOptimalityType()) { + opDecl["left"]["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Pmin" : "Pmax"; + opDecl["left"]["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none)); + } else { + opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Pmax" : "Pmin"; + opDecl["left"]["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none)); + } + opDecl["right"] = numberToJson(bound.threshold); + } else { + if(f.hasOptimalityType()) { + opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Pmin" : "Pmax"; + opDecl["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none)); + + } else { + // TODO add checks + opDecl["op"] = "Pmin"; + opDecl["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none)); + } + } + return opDecl; + } + + boost::any FormulaToJaniJson::visit(storm::logic::RewardOperatorFormula const& f, boost::any const& data) const { + + } + + boost::any FormulaToJaniJson::visit(storm::logic::UnaryBooleanStateFormula const& f, boost::any const& data) const { + modernjson::json opDecl; + storm::logic::UnaryBooleanStateFormula::OperatorType op = f.getOperator(); + assert(op == storm::logic::UnaryBooleanStateFormula::OperatorType::Not); + opDecl["op"] = "¬"; + opDecl["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none)); + return opDecl; + } + + boost::any FormulaToJaniJson::visit(storm::logic::UntilFormula const& f, boost::any const& data) const { + modernjson::json opDecl; + opDecl["op"] = "U"; + opDecl["left"] = boost::any_cast<modernjson::json>(f.getLeftSubformula().accept(*this, boost::none)); + opDecl["right"] = boost::any_cast<modernjson::json>(f.getRightSubformula().accept(*this, boost::none)); + return opDecl; + } std::string operatorTypeToJaniString(storm::expressions::OperatorType optype) { diff --git a/src/storage/jani/JSONExporter.h b/src/storage/jani/JSONExporter.h index 604a27a47..ff54de5e8 100644 --- a/src/storage/jani/JSONExporter.h +++ b/src/storage/jani/JSONExporter.h @@ -2,6 +2,7 @@ #include "src/storage/expressions/ExpressionVisitor.h" +#include "src/logic/FormulaVisitor.h" #include "Model.h" // JSON parser #include "json.hpp" @@ -28,6 +29,31 @@ namespace storm { }; + class FormulaToJaniJson : public storm::logic::FormulaVisitor { + public: + static modernjson::json translate(storm::logic::Formula const& formula); + virtual boost::any visit(storm::logic::AtomicExpressionFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::AtomicLabelFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::BinaryBooleanStateFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::BooleanLiteralFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::BoundedUntilFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::ConditionalFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::CumulativeRewardFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::EventuallyFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::TimeOperatorFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::GloballyFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::InstantaneousRewardFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::LongRunAverageOperatorFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::LongRunAverageRewardFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::NextFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::ProbabilityOperatorFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::RewardOperatorFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::UnaryBooleanStateFormula const& f, boost::any const& data) const; + virtual boost::any visit(storm::logic::UntilFormula const& f, boost::any const& data) const; + + + }; + class JsonExporter { JsonExporter() = default; @@ -37,6 +63,7 @@ namespace storm { private: void convertModel(storm::jani::Model const& model); + void convertProperty(storm::logic::Formula const& formula); void appendVariableDeclaration(storm::jani::Variable const& variable); modernjson::json finalize() { diff --git a/src/storage/jani/Property.cpp b/src/storage/jani/Property.cpp index 9b097757d..195aec571 100644 --- a/src/storage/jani/Property.cpp +++ b/src/storage/jani/Property.cpp @@ -1,11 +1,11 @@ #include "Property.h" namespace storm { namespace jani { - Property::Property(std::string const& name, std::shared_ptr<const storm::logic::Formula> const& formula, std::string const& comment) - : name(name), formula(formula), comment(comment) - { - - } +// Property::Property(std::string const& name, std::string const& comment) +// : name(name), formula(formula), comment(comment) +// { +// +// } std::string const& Property::getName() const { return this->name; @@ -14,10 +14,7 @@ namespace storm { std::string const& Property::getComment() const { return this->comment; } - - std::shared_ptr<storm::logic::Formula const> const& Property::getFormula() const { - return this->formula; - } + } } \ No newline at end of file diff --git a/src/storage/jani/Property.h b/src/storage/jani/Property.h index 30bddac60..c0f08bc56 100644 --- a/src/storage/jani/Property.h +++ b/src/storage/jani/Property.h @@ -4,6 +4,27 @@ namespace storm { namespace jani { + + enum class FilterType { MIN, MAX, SUM, AVG, COUNT, FORALL, EXISTS, ARGMIN, ARGMAX, VALUES }; + + + class PropertyExpression { + + }; + + class FilterExpression : public PropertyExpression { + std::shared_ptr<PropertyExpression> states; + std::shared_ptr<PropertyExpression> values; + FilterType ft; + }; + + class PathExpression : public PropertyExpression { + std::shared_ptr<PropertyExpression> leftStateExpression; + std::shared_ptr<PropertyExpression> rightStateExpression; + }; + + + class Property { /** * Constructs the property @@ -22,16 +43,13 @@ namespace storm { * @return the comment */ std::string const& getComment() const; - /** - * Get the formula - * @return the formula - */ - std::shared_ptr<storm::logic::Formula const> const& getFormula() const; - + + + private: std::string name; - std::shared_ptr<storm::logic::Formula const> formula; std::string comment; + PropertyExpression propertyExpression; }; } } diff --git a/src/storage/ppg/defines.h b/src/storage/ppg/defines.h index 548160ba9..d993e633e 100644 --- a/src/storage/ppg/defines.h +++ b/src/storage/ppg/defines.h @@ -1,6 +1,8 @@ #pragma once #include <cassert> #include <vector> +#include <cstdint> + namespace storm { namespace ppg { class ProgramGraph; From 6a80319c183a9825cb89960ca2bf8603e029de3f Mon Sep 17 00:00:00 2001 From: sjunges <sebastian.junges@rwth-aachen.de> Date: Thu, 13 Oct 2016 15:32:32 +0200 Subject: [PATCH 10/30] another Hwloc script Former-commit-id: cc5efdeb857264fd4c3351dd09063b763e36b623 [formerly 295c0c994ed500e72c1471c288fc22c4ca660ac4] Former-commit-id: fcaf78b967628407d13274a689861d02200259e9 --- resources/cmake/find_modules/FindHwloc.cmake | 206 ++++--------------- 1 file changed, 41 insertions(+), 165 deletions(-) diff --git a/resources/cmake/find_modules/FindHwloc.cmake b/resources/cmake/find_modules/FindHwloc.cmake index d1b5b488e..1db759375 100644 --- a/resources/cmake/find_modules/FindHwloc.cmake +++ b/resources/cmake/find_modules/FindHwloc.cmake @@ -1,179 +1,55 @@ -# FindHwloc -# ---------- +# Try to find hwloc libraries and headers. # -# Try to find Portable Hardware Locality (hwloc) libraries. -# http://www.open-mpi.org/software/hwloc +# Usage of this module: # -# You may declare HWLOC_ROOT environment variable to tell where -# your hwloc library is installed. +# find_package(hwloc) # -# Once done this will define:: +# Variables defined by this module: # -# Hwloc_FOUND - True if hwloc was found -# Hwloc_INCLUDE_DIRS - include directories for hwloc -# Hwloc_LIBRARIES - link against these libraries to use hwloc -# Hwloc_VERSION - version -# Hwloc_CFLAGS - include directories as compiler flags -# Hwloc_LDLFAGS - link paths and libs as compiler flags -# - -#============================================================================= -# Copyright 2014 Mikael Lepistö -# -# Distributed under the OSI-approved BSD License (the "License"); -# -# This software is distributed WITHOUT ANY WARRANTY; without even the -# implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. -# See the License for more information. -#============================================================================= - -if(WIN32) - find_path(Hwloc_INCLUDE_DIR - NAMES - hwloc.h - PATHS - ENV "PROGRAMFILES(X86)" - ENV HWLOC_ROOT - PATH_SUFFIXES - include - ) - - find_library(Hwloc_LIBRARY - NAMES - libhwloc.lib - PATHS - ENV "PROGRAMFILES(X86)" - ENV HWLOC_ROOT - PATH_SUFFIXES - lib - ) - - # - # Check if the found library can be used to linking - # - SET (_TEST_SOURCE "${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/linktest.c") - FILE (WRITE "${_TEST_SOURCE}" - " - #include <hwloc.h> - int main() - { - hwloc_topology_t topology; - int nbcores; - hwloc_topology_init(&topology); - hwloc_topology_load(topology); - nbcores = hwloc_get_nbobjs_by_type(topology, HWLOC_OBJ_CORE); - hwloc_topology_destroy(topology); - return 0; - } - " - ) - - TRY_COMPILE(_LINK_SUCCESS ${CMAKE_BINARY_DIR} "${_TEST_SOURCE}" - CMAKE_FLAGS - "-DINCLUDE_DIRECTORIES:STRING=${Hwloc_INCLUDE_DIR}" - CMAKE_FLAGS - "-DLINK_LIBRARIES:STRING=${Hwloc_LIBRARY}" - ) - - IF(NOT _LINK_SUCCESS) - if(CMAKE_SIZEOF_VOID_P EQUAL 8) - message(STATUS "You are building 64bit target.") - ELSE() - message(STATUS "You are building 32bit code. If you like to build x64 use e.g. -G 'Visual Studio 12 Win64' generator." ) - ENDIF() - message(FATAL_ERROR "Library found, but linking test program failed.") - ENDIF() - - # - # Resolve version if some compiled binary found... - # - find_program(HWLOC_INFO_EXECUTABLE - NAMES - hwloc-info - PATHS - ENV HWLOC_ROOT - PATH_SUFFIXES - bin - ) - - if(HWLOC_INFO_EXECUTABLE) - execute_process( - COMMAND ${HWLOC_INFO_EXECUTABLE} "--version" - OUTPUT_VARIABLE HWLOC_VERSION_LINE - OUTPUT_STRIP_TRAILING_WHITESPACE - ) - string(REGEX MATCH "([0-9]+.[0-9]+)$" - Hwloc_VERSION "${HWLOC_VERSION_LINE}") - unset(HWLOC_VERSION_LINE) - endif() - - # - # All good - # - - set(Hwloc_LIBRARIES ${Hwloc_LIBRARY}) - set(Hwloc_INCLUDE_DIRS ${Hwloc_INCLUDE_DIR}) - - include(FindPackageHandleStandardArgs) - find_package_handle_standard_args( - Hwloc - FOUND_VAR Hwloc_FOUND - REQUIRED_VARS Hwloc_LIBRARY Hwloc_INCLUDE_DIR - VERSION_VAR Hwloc_VERSION) - - mark_as_advanced( - Hwloc_INCLUDE_DIR - Hwloc_LIBRARY) - - foreach(arg ${Hwloc_INCLUDE_DIRS}) - set(Hwloc_CFLAGS "${Hwloc_CFLAGS} /I${arg}") - endforeach() +# HWLOC_FOUND System has hwloc libraries and headers +# HWLOC_LIBRARIES The hwloc library +# HWLOC_INCLUDE_DIRS The location of HWLOC headers - set(Hwloc_LDFLAGS "${Hwloc_LIBRARY}") +find_path( + HWLOC_PREFIX + NAMES include/hwloc.h +) -else() +if (NOT HWLOC_PREFIX AND NOT $ENV{HWLOC_BASE} STREQUAL "") + set(HWLOC_PREFIX $ENV{HWLOC_BASE}) +endif() - # Find with pkgconfig - find_package(PkgConfig) +message(STATUS "Searching for hwloc library in path " ${HWLOC_PREFIX}) - if(HWLOC_ROOT) - set(ENV{PKG_CONFIG_PATH} "${HWLOC_ROOT}/lib/pkgconfig") - else() - foreach(PREFIX ${CMAKE_PREFIX_PATH}) - set(PKG_CONFIG_PATH "${PKG_CONFIG_PATH}:${PREFIX}/lib/pkgconfig") - endforeach() - set(ENV{PKG_CONFIG_PATH} "${PKG_CONFIG_PATH}:$ENV{PKG_CONFIG_PATH}") - endif() +find_library( + HWLOC_LIBRARIES + NAMES hwloc + HINTS ${HWLOC_PREFIX}/lib +) - if(hwloc_FIND_REQUIRED) - set(_hwloc_OPTS "REQUIRED") - elseif(hwloc_FIND_QUIETLY) - set(_hwloc_OPTS "QUIET") - else() - set(_hwloc_output 1) - endif() +find_path( + HWLOC_INCLUDE_DIRS + NAMES hwloc.h + HINTS ${HWLOC_PREFIX}/include +) - if(hwloc_FIND_VERSION) - if(hwloc_FIND_VERSION_EXACT) - pkg_check_modules(Hwloc ${_hwloc_OPTS} hwloc=${hwloc_FIND_VERSION}) - else() - pkg_check_modules(Hwloc ${_hwloc_OPTS} hwloc>=${hwloc_FIND_VERSION}) - endif() - else() - pkg_check_modules(Hwloc ${_hwloc_OPTS} hwloc) - endif() +include(FindPackageHandleStandardArgs) - if(Hwloc_FOUND) - include(FindPackageHandleStandardArgs) - find_package_handle_standard_args(Hwloc DEFAULT_MSG Hwloc_LIBRARIES) +find_package_handle_standard_args( + HWLOC DEFAULT_MSG + HWLOC_LIBRARIES + HWLOC_INCLUDE_DIRS +) - if(NOT ${Hwloc_VERSION} VERSION_LESS 1.7.0) - set(Hwloc_GL_FOUND 1) - endif() +mark_as_advanced( + HWLOC_LIBRARIES + HWLOC_INCLUDE_DIRS +) - if(_hwloc_output) - message(STATUS - "Found hwloc ${Hwloc_VERSION} in ${Hwloc_INCLUDE_DIRS}:${Hwloc_LIBRARIES}") - endif() +if (HWLOC_FOUND) + if (NOT $ENV{HWLOC_LIB} STREQUAL "") +# set(HWLOC_LIBRARIES "$ENV{HWLOC_LIB}") endif() -endif() + message(STATUS "hwloc includes: " ${HWLOC_INCLUDE_DIRS}) + message(STATUS "hwloc libraries: " ${HWLOC_LIBRARIES}) +endif() \ No newline at end of file From ccfcbc0c69fc1349d2940e956d62039f698897e9 Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Thu, 13 Oct 2016 15:37:26 +0200 Subject: [PATCH 11/30] fixed hwloc issue even harder Former-commit-id: 5768663ab4880968d5562114aedea295ea2ec8a9 [formerly 47af70ccf358cd6c066f89ddb3229b1528963c8e] Former-commit-id: ef788dbb6af6a7f6855d5798d964ef13cdec1752 --- resources/3rdparty/CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 244e24057..dcc98e937 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -330,7 +330,7 @@ add_dependencies(resources sylvan) if(${OPERATING_SYSTEM} MATCHES "Linux") find_package(Hwloc QUIET REQUIRED) - if(Hwloc_FOUND) + if(HWLOC_FOUND) message(STATUS "StoRM - Linking with hwloc ${Hwloc_VERSION}") list(APPEND STORM_LINK_LIBRARIES ${Hwloc_LIBRARIES}) else() From 744216d5d2c2ae77a681dca3b5df23e0196888fd Mon Sep 17 00:00:00 2001 From: sjunges <sebastian.junges@rwth-aachen.de> Date: Thu, 13 Oct 2016 18:39:28 +0200 Subject: [PATCH 12/30] export formulae Former-commit-id: 4932938e383e1c8d2b09dd46591f070a43651380 [formerly 95b3269c755ac84aede16254a514be7d26a2aa24] Former-commit-id: 974a891cb6adfef1b39f9d94f1abdd63950dd7de --- src/cli/cli.cpp | 24 ++--- src/parser/JaniParser.cpp | 7 ++ src/storage/jani/JSONExporter.cpp | 158 ++++++++++++++++++++++++++++-- src/storage/jani/JSONExporter.h | 15 +-- src/storage/jani/Property.cpp | 10 +- src/storage/jani/Property.h | 29 +++--- 6 files changed, 200 insertions(+), 43 deletions(-) diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp index 2c5104123..db9829084 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -222,13 +222,23 @@ namespace storm { model = storm::parseJaniModel(ioSettings.getJaniInputFilename()).first; } + // Then proceed to parsing the properties (if given), since the model we are building may depend on the property. + std::vector<std::shared_ptr<storm::logic::Formula const>> formulas; + if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isPropertySet()) { + if (model.isJaniModel()) { + formulas = storm::parseFormulasForJaniModel(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), model.asJaniModel()); + } else { + formulas = storm::parseFormulasForPrismProgram(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), model.asPrismProgram()); + } + } + if(model.isJaniModel() && storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isJaniFileSet()) { if (storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isExportAsStandardJaniSet()) { storm::jani::Model normalisedModel = storm::jani::Model(model.asJaniModel()); normalisedModel.makeStandardJaniCompliant(); - storm::jani::JsonExporter::toFile(normalisedModel, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename()); + storm::jani::JsonExporter::toFile(normalisedModel, formulas, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename()); } else { - storm::jani::JsonExporter::toFile(model.asJaniModel(), storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename()); + storm::jani::JsonExporter::toFile(model.asJaniModel(), formulas, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename()); } } @@ -236,15 +246,7 @@ namespace storm { std::string constantDefinitionString = ioSettings.getConstantDefinitionString(); model = model.preprocess(constantDefinitionString); - // Then proceed to parsing the properties (if given), since the model we are building may depend on the property. - std::vector<std::shared_ptr<storm::logic::Formula const>> formulas; - if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isPropertySet()) { - if (model.isJaniModel()) { - formulas = storm::parseFormulasForJaniModel(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), model.asJaniModel()); - } else { - formulas = storm::parseFormulasForPrismProgram(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), model.asPrismProgram()); - } - } + if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isParametricSet()) { #ifdef STORM_HAVE_CARL diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index a49ab5548..97fc467e5 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -110,6 +110,13 @@ namespace storm { for (auto const& automataEntry : parsedStructure.at("automata")) { model.addAutomaton(parseAutomaton(automataEntry, model)); } + STORM_LOG_THROW(parsedStructure.count("restrict-initial") < 2, storm::exceptions::InvalidJaniException, "Model has multiple initial value restrictions"); + storm::expressions::Expression initialValueRestriction = expressionManager->boolean(true); + if(parsedStructure.count("restrict-initial") > 0) { + STORM_LOG_THROW(parsedStructure.at("restrict-initial").count("exp") == 1, storm::exceptions::InvalidJaniException, "Model needs an expression inside the initial restricion"); + initialValueRestriction = parseExpression(parsedStructure.at("restrict-initial").at("exp"), "Initial value restriction for automaton " + name); + } + model.setInitialStatesRestriction(initialValueRestriction); STORM_LOG_THROW(parsedStructure.count("system") == 1, storm::exceptions::InvalidJaniException, "Exactly one system description must be given"); std::shared_ptr<storm::jani::Composition> composition = parseComposition(parsedStructure.at("system")); model.setSystemComposition(composition); diff --git a/src/storage/jani/JSONExporter.cpp b/src/storage/jani/JSONExporter.cpp index be30b82b8..e6c1e9d60 100644 --- a/src/storage/jani/JSONExporter.cpp +++ b/src/storage/jani/JSONExporter.cpp @@ -9,6 +9,7 @@ #include "src/exceptions/NotSupportedException.h" #include "src/exceptions/InvalidJaniException.h" +#include "src/exceptions/NotImplementedException.h" #include "src/storage/expressions/RationalLiteralExpression.h" #include "src/storage/expressions/IntegerLiteralExpression.h" @@ -25,6 +26,7 @@ #include "src/storage/jani/AutomatonComposition.h" #include "src/storage/jani/ParallelComposition.h" +#include "src/storage/jani/Property.h" namespace storm { namespace jani { @@ -128,6 +130,11 @@ namespace storm { return iDecl; } + modernjson::json FormulaToJaniJson::translate(storm::logic::Formula const& formula, bool continuousTime) { + FormulaToJaniJson translator(continuousTime); + return boost::any_cast<modernjson::json>(formula.accept(translator)); + } + boost::any FormulaToJaniJson::visit(storm::logic::AtomicExpressionFormula const& f, boost::any const& data) const { return ExpressionToJson::translate(f.getExpression()); } @@ -178,16 +185,44 @@ namespace storm { } boost::any FormulaToJaniJson::visit(storm::logic::TimeOperatorFormula const& f, boost::any const& data) const { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani currently does not support conditional formulae"); - + modernjson::json opDecl; + std::vector<std::string> tvec; + tvec.push_back("time"); + if(f.hasBound()) { + auto bound = f.getBound(); + opDecl["op"] = comparisonTypeToJani(bound.comparisonType); + if(f.hasOptimalityType()) { + opDecl["left"]["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax"; + opDecl["left"]["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none)); + } else { + opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Emax" : "Emin"; + opDecl["left"]["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none)); + } + opDecl["left"]["exp"] = modernjson::json(1); + opDecl["left"]["accumulate"] = modernjson::json(tvec); + opDecl["right"] = numberToJson(bound.threshold); + } else { + if(f.hasOptimalityType()) { + opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax"; + opDecl["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none)); + + } else { + // TODO add checks + opDecl["op"] = "Pmin"; + opDecl["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none)); + } + opDecl["exp"] = modernjson::json(1); + opDecl["accumulate"] = modernjson::json(tvec); + } + return opDecl; } boost::any FormulaToJaniJson::visit(storm::logic::GloballyFormula const& f, boost::any const& data) const { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani currently does not support conditional formulae"); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support conversion of a globally formulae"); } boost::any FormulaToJaniJson::visit(storm::logic::InstantaneousRewardFormula const& f, boost::any const& data) const { - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani currently does not support conditional formulae"); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support conversion of an instanteneous reward formula"); } boost::any FormulaToJaniJson::visit(storm::logic::LongRunAverageOperatorFormula const& f, boost::any const& data) const { @@ -219,7 +254,30 @@ namespace storm { } boost::any FormulaToJaniJson::visit(storm::logic::LongRunAverageRewardFormula const& f, boost::any const& data) const { - +// modernjson::json opDecl; +// if(f.()) { +// auto bound = f.getBound(); +// opDecl["op"] = comparisonTypeToJani(bound.comparisonType); +// if(f.hasOptimalityType()) { +// opDecl["left"]["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Smin" : "Smax"; +// opDecl["left"]["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none)); +// } else { +// opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Smax" : "Smin"; +// opDecl["left"]["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none)); +// } +// opDecl["right"] = numberToJson(bound.threshold); +// } else { +// if(f.hasOptimalityType()) { +// opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Smin" : "Smax"; +// opDecl["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none)); +// +// } else { +// // TODO add checks +// opDecl["op"] = "Pmin"; +// opDecl["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none)); +// } +// } +// return opDecl; } boost::any FormulaToJaniJson::visit(storm::logic::NextFormula const& f, boost::any const& data) const { @@ -263,7 +321,40 @@ namespace storm { } boost::any FormulaToJaniJson::visit(storm::logic::RewardOperatorFormula const& f, boost::any const& data) const { - + modernjson::json opDecl; + std::vector<std::string> accvec; + if(continuous) { + accvec.push_back("time"); + } else { + accvec.push_back("steps"); + } + if(f.hasBound()) { + auto bound = f.getBound(); + opDecl["op"] = comparisonTypeToJani(bound.comparisonType); + if(f.hasOptimalityType()) { + opDecl["left"]["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax"; + opDecl["left"]["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none)); + } else { + opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Emax" : "Emin"; + opDecl["left"]["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none)); + } + opDecl["left"]["exp"] = f.hasRewardModelName() ? f.getRewardModelName() : "DEFAULT"; + opDecl["left"]["accumulate"] = modernjson::json(accvec); + opDecl["right"] = numberToJson(bound.threshold); + } else { + if(f.hasOptimalityType()) { + opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax"; + opDecl["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none)); + + } else { + // TODO add checks + opDecl["op"] = "Pmin"; + opDecl["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none)); + } + opDecl["exp"] = f.hasRewardModelName() ? f.getRewardModelName() : "DEFAULT"; + opDecl["accumulate"] = modernjson::json(accvec); + } + return opDecl; } boost::any FormulaToJaniJson::visit(storm::logic::UnaryBooleanStateFormula const& f, boost::any const& data) const { @@ -402,22 +493,23 @@ namespace storm { - void JsonExporter::toFile(storm::jani::Model const& janiModel, std::string const& filepath, bool checkValid) { + void JsonExporter::toFile(storm::jani::Model const& janiModel, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::string const& filepath, bool checkValid) { std::ofstream ofs; ofs.open (filepath, std::ofstream::out ); if(ofs.is_open()) { - toStream(janiModel, ofs, checkValid); + toStream(janiModel, formulas, ofs, checkValid); } else { STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Cannot open " << filepath); } } - void JsonExporter::toStream(storm::jani::Model const& janiModel, std::ostream& os, bool checkValid) { + void JsonExporter::toStream(storm::jani::Model const& janiModel, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::ostream& os, bool checkValid) { if(checkValid) { janiModel.checkValid(); } JsonExporter exporter; exporter.convertModel(janiModel); + exporter.convertProperties(formulas, !janiModel.isDiscreteTimeModel()); os << exporter.finalize().dump(4) << std::endl; } @@ -597,6 +689,54 @@ namespace storm { } + std::string janiFilterTypeString(storm::jani::FilterType const& ft) { + switch(ft) { + case storm::jani::FilterType::MIN: + return "min"; + case storm::jani::FilterType::MAX: + return "max"; + case storm::jani::FilterType::SUM: + return "sum"; + case storm::jani::FilterType::AVG: + return "avg"; + case storm::jani::FilterType::COUNT: + return "count"; + case storm::jani::FilterType::EXISTS: + return "∃"; + case storm::jani::FilterType::FORALL: + return "∀"; + case storm::jani::FilterType::ARGMIN: + return "argmin"; + case storm::jani::FilterType::ARGMAX: + return "argmax"; + case storm::jani::FilterType::VALUES: + return "values"; + + } + } + + modernjson::json convertFilterExpression(storm::jani::FilterExpression const& fe, bool continuousModel) { + modernjson::json propDecl; + propDecl["states"] = "initial"; + propDecl["fun"] = janiFilterTypeString(fe.getFilterType()); + propDecl["values"] = FormulaToJaniJson::translate(*fe.getFormula(), continuousModel); + return propDecl; + } + + + void JsonExporter::convertProperties( std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool continuousModel) { + std::vector<modernjson::json> properties; + uint64_t index = 0; + for(auto const& f : formulas) { + modernjson::json propDecl; + propDecl["name"] = "prop" + std::to_string(index); + propDecl["expression"] = convertFilterExpression(storm::jani::FilterExpression(f), continuousModel); + ++index; + properties.push_back(propDecl); + } + jsonStruct["properties"] = properties; + } + } } diff --git a/src/storage/jani/JSONExporter.h b/src/storage/jani/JSONExporter.h index ff54de5e8..55895364d 100644 --- a/src/storage/jani/JSONExporter.h +++ b/src/storage/jani/JSONExporter.h @@ -30,8 +30,9 @@ namespace storm { }; class FormulaToJaniJson : public storm::logic::FormulaVisitor { - public: - static modernjson::json translate(storm::logic::Formula const& formula); + + public: + static modernjson::json translate(storm::logic::Formula const& formula, bool continuousTime); virtual boost::any visit(storm::logic::AtomicExpressionFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::AtomicLabelFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::BinaryBooleanStateFormula const& f, boost::any const& data) const; @@ -51,19 +52,21 @@ namespace storm { virtual boost::any visit(storm::logic::UnaryBooleanStateFormula const& f, boost::any const& data) const; virtual boost::any visit(storm::logic::UntilFormula const& f, boost::any const& data) const; - + private: + FormulaToJaniJson(bool continuousModel) : continuous(continuousModel) { } + bool continuous; }; class JsonExporter { JsonExporter() = default; public: - static void toFile(storm::jani::Model const& janiModel, std::string const& filepath, bool checkValid = true); - static void toStream(storm::jani::Model const& janiModel, std::ostream& ostream, bool checkValid = false); + static void toFile(storm::jani::Model const& janiModel, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::string const& filepath, bool checkValid = true); + static void toStream(storm::jani::Model const& janiModel, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::ostream& ostream, bool checkValid = false); private: void convertModel(storm::jani::Model const& model); - void convertProperty(storm::logic::Formula const& formula); + void convertProperties(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool timeContinuousModel); void appendVariableDeclaration(storm::jani::Variable const& variable); modernjson::json finalize() { diff --git a/src/storage/jani/Property.cpp b/src/storage/jani/Property.cpp index 195aec571..28981f313 100644 --- a/src/storage/jani/Property.cpp +++ b/src/storage/jani/Property.cpp @@ -1,11 +1,11 @@ #include "Property.h" namespace storm { namespace jani { -// Property::Property(std::string const& name, std::string const& comment) -// : name(name), formula(formula), comment(comment) -// { -// -// } + Property::Property(std::string const& name, std::shared_ptr<storm::logic::Formula const> const& formula, std::string const& comment) + : name(name), filterExpression(FilterExpression(formula)), comment(comment) + { + + } std::string const& Property::getName() const { return this->name; diff --git a/src/storage/jani/Property.h b/src/storage/jani/Property.h index c0f08bc56..bde51865e 100644 --- a/src/storage/jani/Property.h +++ b/src/storage/jani/Property.h @@ -8,20 +8,25 @@ namespace storm { enum class FilterType { MIN, MAX, SUM, AVG, COUNT, FORALL, EXISTS, ARGMIN, ARGMAX, VALUES }; - class PropertyExpression { - - }; - class FilterExpression : public PropertyExpression { - std::shared_ptr<PropertyExpression> states; - std::shared_ptr<PropertyExpression> values; - FilterType ft; + class FilterExpression { + public: + explicit FilterExpression(std::shared_ptr<storm::logic::Formula const> formula) : values(formula) {} + + std::shared_ptr<storm::logic::Formula const> const& getFormula() const { + return values; + } + + FilterType getFilterType() const { + return ft; + } + private: + // For now, we assume that the states are always the initial states. + + std::shared_ptr<storm::logic::Formula const> values; + FilterType ft = FilterType::VALUES; }; - class PathExpression : public PropertyExpression { - std::shared_ptr<PropertyExpression> leftStateExpression; - std::shared_ptr<PropertyExpression> rightStateExpression; - }; @@ -49,7 +54,7 @@ namespace storm { private: std::string name; std::string comment; - PropertyExpression propertyExpression; + FilterExpression filterExpression; }; } } From 282be9612e139e42af481338cb5fcafe56f58e07 Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Fri, 14 Oct 2016 09:44:15 +0200 Subject: [PATCH 13/30] fixed typo in header inclusion Former-commit-id: 7039fe5a3555aca5ec2c8a240221d0d3a0050bfa [formerly 4050360481d33fd40c9f8be22e0b79dbf8d38c74] Former-commit-id: 266f1e06598d5828ae36611f3119ace055bb4cb2 --- src/storage/jani/Property.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/storage/jani/Property.h b/src/storage/jani/Property.h index bde51865e..dc6aab23b 100644 --- a/src/storage/jani/Property.h +++ b/src/storage/jani/Property.h @@ -1,6 +1,6 @@ #pragma once -#include "src/logic/formulas.h" +#include "src/logic/Formulas.h" namespace storm { namespace jani { From 6f663bde0ebd95fadebab7ea0b4f47672d750060 Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Fri, 14 Oct 2016 10:35:17 +0200 Subject: [PATCH 14/30] fixing hwloc entry in CMakeLists.txt Former-commit-id: 1359cb4b148859cf9d28a4ac25490fa99de291b8 [formerly 9a108db302551e3fbe9e5689bea7bdad465cebf0] Former-commit-id: ab87e2002eb66a4e915796119ef4d6db222a7874 --- resources/3rdparty/CMakeLists.txt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index dcc98e937..ffd5fc54c 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -331,8 +331,8 @@ add_dependencies(resources sylvan) if(${OPERATING_SYSTEM} MATCHES "Linux") find_package(Hwloc QUIET REQUIRED) if(HWLOC_FOUND) - message(STATUS "StoRM - Linking with hwloc ${Hwloc_VERSION}") - list(APPEND STORM_LINK_LIBRARIES ${Hwloc_LIBRARIES}) + message(STATUS "StoRM - Linking with hwloc ${HWLOC_VERSION}") + list(APPEND STORM_LINK_LIBRARIES ${HWLOC_LIBRARIES}) else() message(FATAL_ERROR "HWLOC is required but was not found.") endif() From 3ffc93f9b2157e3b23a661eba8c0405c916c6a90 Mon Sep 17 00:00:00 2001 From: sjunges <sebastian.junges@rwth-aachen.de> Date: Fri, 14 Oct 2016 10:38:43 +0200 Subject: [PATCH 15/30] label Former-commit-id: 88b6ce4560639a8bb7b117d27a59bee031a29c7e [formerly d698b1b83c6e5ac662f30f8a142c57a5c423338f] Former-commit-id: c1193042433bede64afe205c99f08de8b22f93b5 --- examples/pmdp/brp/brp.pm | 1 + 1 file changed, 1 insertion(+) diff --git a/examples/pmdp/brp/brp.pm b/examples/pmdp/brp/brp.pm index 2722cb0ee..a195980bf 100644 --- a/examples/pmdp/brp/brp.pm +++ b/examples/pmdp/brp/brp.pm @@ -137,3 +137,4 @@ module channelL endmodule +label "fatal" = s=5 & T; From 88ecb6090619395062e43a4c8f3b91a5edc96732 Mon Sep 17 00:00:00 2001 From: sjunges <sebastian.junges@rwth-aachen.de> Date: Fri, 14 Oct 2016 10:38:57 +0200 Subject: [PATCH 16/30] numbered actions Former-commit-id: 3b1e903ff98010a22ea708d0dd7b9a9dde17bdf9 [formerly df745fb1920d47dd20d213157a656b9cc75d4d79] Former-commit-id: 4700ce2d7021e5eed07b612441802373e7740a43 --- src/utility/ExplicitExporter.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/utility/ExplicitExporter.cpp b/src/utility/ExplicitExporter.cpp index c29684fad..bf9bcbf29 100644 --- a/src/utility/ExplicitExporter.cpp +++ b/src/utility/ExplicitExporter.cpp @@ -78,9 +78,10 @@ namespace storm { typename storm::storage::SparseMatrix<ValueType>::index_type start = matrix.hasTrivialRowGrouping() ? group : matrix.getRowGroupIndices()[group]; typename storm::storage::SparseMatrix<ValueType>::index_type end = matrix.hasTrivialRowGrouping() ? group + 1 : matrix.getRowGroupIndices()[group + 1]; + for (typename storm::storage::SparseMatrix<ValueType>::index_type i = start; i < end; ++i) { // Print the actual row. - os << "\taction"; + os << "\taction " << i - start; if (!embedded) { bool first = true; for (auto const& rewardModelEntry : sparseModel->getRewardModels()) { From 3626c044d39dabc5953e9a0a8e0291693fa18a3d Mon Sep 17 00:00:00 2001 From: sjunges <sebastian.junges@rwth-aachen.de> Date: Sat, 15 Oct 2016 00:50:11 +0200 Subject: [PATCH 17/30] several improvements towards jani-property support Former-commit-id: 3d56f22d99f3e051cc68dd08159761bea257e576 [formerly 1f527643abbb4e0bad9b609dc0f9835e7db51035] Former-commit-id: 75e40a9b69709b86cfe88a61c2c03554f4664718 --- src/parser/JaniParser.cpp | 173 ++++++++++++++++-- src/parser/JaniParser.h | 20 +- src/storage/jani/BooleanVariable.cpp | 5 +- src/storage/jani/BooleanVariable.h | 2 +- src/storage/jani/BoundedIntegerVariable.cpp | 9 +- src/storage/jani/BoundedIntegerVariable.h | 4 - src/storage/jani/JSONExporter.cpp | 7 +- src/storage/jani/Property.h | 1 + src/storage/jani/RealVariable.cpp | 2 +- src/storage/jani/RealVariable.h | 2 +- src/storage/jani/UnboundedIntegerVariable.cpp | 2 +- src/storage/jani/Variable.cpp | 2 +- src/storage/jani/Variable.h | 2 +- src/storage/prism/ToJaniConverter.cpp | 6 +- src/utility/storm.cpp | 4 +- src/utility/storm.h | 2 +- 16 files changed, 189 insertions(+), 54 deletions(-) diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index 97fc467e5..bc094f197 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -5,6 +5,8 @@ #include "src/storage/jani/ParallelComposition.h" #include "src/exceptions/FileIoException.h" #include "src/exceptions/InvalidJaniException.h" + +#include "src/exceptions/NotSupportedException.h" #include "src/exceptions/NotImplementedException.h" #include "src/storage/jani/ModelType.h" @@ -49,7 +51,7 @@ namespace storm { } - std::pair<storm::jani::Model, std::vector<storm::jani::Property>> JaniParser::parse(std::string const& path) { + std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> JaniParser::parse(std::string const& path) { JaniParser parser; parser.readFile(path); return parser.parseModel(); @@ -75,7 +77,7 @@ namespace storm { file.close(); } - std::pair<storm::jani::Model, std::vector<storm::jani::Property>> JaniParser::parseModel(bool parseProperties) { + std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> JaniParser::parseModel(bool parseProperties) { //jani-version STORM_LOG_THROW(parsedStructure.count("jani-version") == 1, storm::exceptions::InvalidJaniException, "Jani-version must be given exactly once."); uint64_t version = getUnsignedInt(parsedStructure.at("jani-version"), "jani version"); @@ -121,17 +123,87 @@ namespace storm { std::shared_ptr<storm::jani::Composition> composition = parseComposition(parsedStructure.at("system")); model.setSystemComposition(composition); STORM_LOG_THROW(parsedStructure.count("properties") <= 1, storm::exceptions::InvalidJaniException, "At most one list of properties can be given"); - PropertyVector properties; + std::map<std::string, storm::jani::Property> properties; if (parseProperties && parsedStructure.count("properties") == 1) { STORM_LOG_THROW(parsedStructure.at("properties").is_array(), storm::exceptions::InvalidJaniException, "Properties should be an array"); for(auto const& propertyEntry : parsedStructure.at("properties")) { - properties.push_back(this->parseProperty(propertyEntry)); + try { + auto prop = this->parseProperty(propertyEntry); + properties.emplace(prop.getName(), prop); + } catch (storm::exceptions::NotSupportedException const& ex) { + STORM_LOG_WARN("Cannot handle property " << ex.what()); + } catch (storm::exceptions::NotImplementedException const& ex) { + STORM_LOG_WARN("Cannot handle property " << ex.what()); + } } } return {model, properties}; } + + std::vector<std::shared_ptr<storm::logic::Formula const>> JaniParser::parseUnaryFormulaArgument(json const& propertyStructure, std::string const& opstring, std::string const& context) { + STORM_LOG_THROW(propertyStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting operand for operator " << opstring << " in " << context); + return { parseFormula(propertyStructure.at("exp"), "Operand of operator " + opstring) }; + } + + + std::vector<std::shared_ptr<storm::logic::Formula const>> JaniParser::parseBinaryFormulaArguments(json const& propertyStructure, std::string const& opstring, std::string const& context) { + STORM_LOG_THROW(propertyStructure.count("left") == 1, storm::exceptions::InvalidJaniException, "Expecting left operand for operator " << opstring << " in " << context); + STORM_LOG_THROW(propertyStructure.count("right") == 1, storm::exceptions::InvalidJaniException, "Expecting right operand for operator " << opstring << " in " << context); + return { parseFormula(propertyStructure.at("left"), "Operand of operator " + opstring), parseFormula(propertyStructure.at("right"), "Operand of operator " + opstring) }; + } + + + std::shared_ptr<storm::logic::Formula const> JaniParser::parseFormula(json const& propertyStructure, std::string const& context) { + storm::expressions::Expression expr = parseExpression(propertyStructure, "Expression in property", {}, true); + if(expr.isInitialized()) { + return std::make_shared<storm::logic::AtomicExpressionFormula>(expr); + } else if(propertyStructure.count("op") == 1) { + std::string opString = getString(propertyStructure.at("op"), "Operation description"); + + if(opString == "Pmin" || opString == "Pmax") { + std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseUnaryFormulaArgument(propertyStructure, opString, ""); + assert(args.size() == 1); + storm::logic::OperatorInformation opInfo; + opInfo.optimalityType = opString == "Pmin" ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize; + return std::make_shared<storm::logic::ProbabilityOperatorFormula>(args[0], opInfo); + + } else if (opString == "∀" || opString == "∃") { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Forall and Exists are currently not supported"); + } else if (opString == "Emin" || opString == "Emax") { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Emin and Emax are currently not supported"); + } else if (opString == "Smin" || opString == "Smax") { + std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseUnaryFormulaArgument(propertyStructure, opString, ""); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Smin and Smax are currently not supported"); + } else if (opString == "U") { + std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseBinaryFormulaArguments(propertyStructure, opString, ""); + if (propertyStructure.count("step-bounds") > 0) { + + } else if (propertyStructure.count("time-bounds") > 0) { + + } else if (propertyStructure.count("reward-bounds") > 0 ) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by Storm"); + } + return std::make_shared<storm::logic::UntilFormula const>(args[0], args[1]); + } else if (opString == "W") { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Weak until is not supported"); + } else if (opString == "∧" || opString == "∨") { + std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseBinaryFormulaArguments(propertyStructure, opString, ""); + assert(args.size() == 2); + storm::logic::BinaryBooleanStateFormula::OperatorType oper = opString == "∧" ? storm::logic::BinaryBooleanStateFormula::OperatorType::And : storm::logic::BinaryBooleanStateFormula::OperatorType::Or; + return std::make_shared<storm::logic::BinaryBooleanStateFormula const>(oper, args[0], args[1]); + } else if (opString == "¬") { + std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseUnaryFormulaArgument(propertyStructure, opString, ""); + assert(args.size() == 1); + return std::make_shared<storm::logic::UnaryBooleanStateFormula const>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, args[0]); + + } + + } + + } + storm::jani::Property JaniParser::parseProperty(json const& propertyStructure) { STORM_LOG_THROW(propertyStructure.count("name") == 1, storm::exceptions::InvalidJaniException, "Property must have a name"); // TODO check unique name @@ -140,8 +212,46 @@ namespace storm { if (propertyStructure.count("comment") > 0) { comment = getString(propertyStructure.at("comment"), "comment for property named '" + name + "'."); } + STORM_LOG_THROW(propertyStructure.count("expression") == 1, storm::exceptions::InvalidJaniException, "Property must have an expression"); + // Parse filter expression. + json const& expressionStructure = propertyStructure.at("expression"); - + STORM_LOG_THROW(expressionStructure.count("op") == 1, storm::exceptions::InvalidJaniException, "Expression in property must have an operation description"); + STORM_LOG_THROW(expressionStructure.at("op") == "filter", storm::exceptions::InvalidJaniException, "Top level operation of a property must be a filter"); + STORM_LOG_THROW(expressionStructure.count("fun") == 1, storm::exceptions::InvalidJaniException, "Filter must have a function descritpion"); + std::string funDescr = getString(expressionStructure.at("fun"), "Filter function in property named " + name); + storm::jani::FilterType ft; + if (funDescr == "min") { + ft = storm::jani::FilterType::MIN; + } else if (funDescr == "max") { + ft = storm::jani::FilterType::MAX; + } else if (funDescr == "sum") { + ft = storm::jani::FilterType::SUM; + } else if (funDescr == "avg") { + ft = storm::jani::FilterType::AVG; + } else if (funDescr == "count") { + ft = storm::jani::FilterType::COUNT; + } else if (funDescr == "∀") { + ft = storm::jani::FilterType::FORALL; + } else if (funDescr == "∃") { + ft = storm::jani::FilterType::EXISTS; + } else if (funDescr == "argmin") { + ft = storm::jani::FilterType::ARGMIN; + } else if (funDescr == "argmax") { + ft = storm::jani::FilterType::ARGMAX; + } else if (funDescr == "values") { + ft = storm::jani::FilterType::VALUES; + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown filter description " << funDescr << " in property named " << name); + } + + STORM_LOG_THROW(expressionStructure.count("states") == 1, storm::exceptions::InvalidJaniException, "Filter must have a states description"); + STORM_LOG_THROW(expressionStructure.at("states").is_string(), storm::exceptions::NotImplementedException, "We only support properties where the filter has a non-complex description of the states"); + std::string statesDescr = getString(expressionStructure.at("states"), "Filtered states in property named " + name); + STORM_LOG_THROW(statesDescr == "initial", storm::exceptions::NotImplementedException, "Only initial states are allowed as set of states we are interested in."); + STORM_LOG_THROW(expressionStructure.count("values") == 1, storm::exceptions::InvalidJaniException, "Values as input for a filter must be given"); + auto formula = parseFormula(expressionStructure.at("values"), "Values of property " + name); + return storm::jani::Property(name, formula, comment); } std::shared_ptr<storm::jani::Constant> JaniParser::parseConstant(json const& constantStructure, std::string const& scopeDescription) { @@ -236,7 +346,6 @@ namespace storm { boost::optional<storm::expressions::Expression> initVal; if(variableStructure.at("type").is_string()) { if(variableStructure.at("type") == "real") { - expressionManager->declareRationalVariable(name); if(initvalcount == 1) { if(variableStructure.at("initial-value").is_null()) { initVal = expressionManager->rational(defaultRationalInitialValue); @@ -247,7 +356,8 @@ namespace storm { return std::make_shared<storm::jani::RealVariable>(name, expressionManager->declareRationalVariable(exprManagerName), initVal.get(), transientVar); } - return std::make_shared<storm::jani::RealVariable>(name, expressionManager->declareRationalVariable(exprManagerName), transientVar); + assert(!transientVar); + return std::make_shared<storm::jani::RealVariable>(name, expressionManager->declareRationalVariable(exprManagerName)); } else if(variableStructure.at("type") == "bool") { if(initvalcount == 1) { if(variableStructure.at("initial-value").is_null()) { @@ -258,7 +368,8 @@ namespace storm { } return std::make_shared<storm::jani::BooleanVariable>(name, expressionManager->declareBooleanVariable(exprManagerName), initVal.get(), transientVar); } - return std::make_shared<storm::jani::BooleanVariable>(name, expressionManager->declareBooleanVariable(exprManagerName), transientVar); + assert(!transientVar); + return std::make_shared<storm::jani::BooleanVariable>(name, expressionManager->declareBooleanVariable(exprManagerName)); } else if(variableStructure.at("type") == "int") { if(initvalcount == 1) { if(variableStructure.at("initial-value").is_null()) { @@ -323,14 +434,14 @@ namespace storm { STORM_LOG_THROW(expected == actual, storm::exceptions::InvalidJaniException, "Operator " << opstring << " expects " << expected << " arguments, but got " << actual << " in " << errorInfo << "."); } - std::vector<storm::expressions::Expression> JaniParser::parseUnaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars) { - storm::expressions::Expression left = parseExpression(expressionDecl.at("exp"), "Left argument of operator " + opstring + " in " + scopeDescription, localVars); + std::vector<storm::expressions::Expression> JaniParser::parseUnaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars, bool returnNoneInitializedOnUnknownOperator) { + storm::expressions::Expression left = parseExpression(expressionDecl.at("exp"), "Argument of operator " + opstring + " in " + scopeDescription, localVars,returnNoneInitializedOnUnknownOperator); return {left}; } - std::vector<storm::expressions::Expression> JaniParser::parseBinaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars) { - storm::expressions::Expression left = parseExpression(expressionDecl.at("left"), "Left argument of operator " + opstring + " in " + scopeDescription, localVars); - storm::expressions::Expression right = parseExpression(expressionDecl.at("right"), "Right argument of operator " + opstring + " in " + scopeDescription, localVars); + std::vector<storm::expressions::Expression> JaniParser::parseBinaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars, bool returnNoneInitializedOnUnknownOperator) { + storm::expressions::Expression left = parseExpression(expressionDecl.at("left"), "Left argument of operator " + opstring + " in " + scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); + storm::expressions::Expression right = parseExpression(expressionDecl.at("right"), "Right argument of operator " + opstring + " in " + scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); return {left, right}; } /** @@ -366,7 +477,7 @@ namespace storm { } } - storm::expressions::Expression JaniParser::parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars) { + storm::expressions::Expression JaniParser::parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars, bool returnNoneInitializedOnUnknownOperator) { if(expressionStructure.is_boolean()) { if(expressionStructure.get<bool>()) { return expressionManager->boolean(true); @@ -389,31 +500,50 @@ namespace storm { if(expressionStructure.count("op") == 1) { std::string opstring = getString(expressionStructure.at("op"), scopeDescription); std::vector<storm::expressions::Expression> arguments = {}; - if(opstring == "?:") { + if(opstring == "ite") { + STORM_LOG_THROW(expressionStructure.count("if") == 1, storm::exceptions::InvalidJaniException, "If operator required"); + STORM_LOG_THROW(expressionStructure.count("else") == 1, storm::exceptions::InvalidJaniException, "Else operator required"); + STORM_LOG_THROW(expressionStructure.count("then") == 1, storm::exceptions::InvalidJaniException, "If operator required"); + arguments.push_back(parseExpression(expressionStructure.at("if"), "if-formula in " + scopeDescription)); + arguments.push_back(parseExpression(expressionStructure.at("then"), "then-formula in " + scopeDescription)); + arguments.push_back(parseExpression(expressionStructure.at("else"), "else-formula in " + scopeDescription)); ensureNumberOfArguments(3, arguments.size(), opstring, scopeDescription); assert(arguments.size() == 3); + ensureBooleanType(arguments[0], opstring, 0, scopeDescription); return storm::expressions::ite(arguments[0], arguments[1], arguments[2]); } else if (opstring == "∨") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); + if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { + return storm::expressions::Expression(); + } ensureBooleanType(arguments[0], opstring, 0, scopeDescription); ensureBooleanType(arguments[1], opstring, 1, scopeDescription); return arguments[0] || arguments[1]; } else if (opstring == "∧") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); + if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { + return storm::expressions::Expression(); + } ensureBooleanType(arguments[0], opstring, 0, scopeDescription); ensureBooleanType(arguments[1], opstring, 1, scopeDescription); return arguments[0] && arguments[1]; } else if (opstring == "⇒") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); + if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { + return storm::expressions::Expression(); + } ensureBooleanType(arguments[0], opstring, 0, scopeDescription); - ensureBooleanType(arguments[0], opstring, 1, scopeDescription); + ensureBooleanType(arguments[1], opstring, 1, scopeDescription); return (!arguments[0]) || arguments[1]; } else if (opstring == "¬") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 1); + if(!arguments[0].isInitialized()) { + return storm::expressions::Expression(); + } ensureBooleanType(arguments[0], opstring, 0, scopeDescription); return !arguments[0]; } else if (opstring == "=") { @@ -558,6 +688,9 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Opstring " + opstring + " is not supported by storm"); } else { + if(returnNoneInitializedOnUnknownOperator) { + return storm::expressions::Expression(); + } STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown operator " << opstring << " in " << scopeDescription << "."); } } diff --git a/src/parser/JaniParser.h b/src/parser/JaniParser.h index 8fa4e8277..1e87efe04 100644 --- a/src/parser/JaniParser.h +++ b/src/parser/JaniParser.h @@ -33,16 +33,16 @@ namespace storm { JaniParser() : expressionManager(new storm::expressions::ExpressionManager()) {} JaniParser(std::string const& jsonstring); - static std::pair<storm::jani::Model, PropertyVector> parse(std::string const& path); + static std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> parse(std::string const& path); protected: void readFile(std::string const& path); - std::pair<storm::jani::Model, PropertyVector> parseModel(bool parseProperties = true); + std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> parseModel(bool parseProperties = true); storm::jani::Property parseProperty(json const& propertyStructure); storm::jani::Automaton parseAutomaton(json const& automatonStructure, storm::jani::Model const& parentModel); std::shared_ptr<storm::jani::Variable> parseVariable(json const& variableStructure, std::string const& scopeDescription, bool prefWithScope = false); - storm::expressions::Expression parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>>()); + storm::expressions::Expression parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>>(), bool returnNoneOnUnknownOpString = false); private: std::shared_ptr<storm::jani::Constant> parseConstant(json const& constantStructure, std::string const& scopeDescription = "global"); @@ -51,13 +51,19 @@ namespace storm { * Helper for parsing the actions of a model. */ void parseActions(json const& actionStructure, storm::jani::Model& parentModel); - std::vector<storm::expressions::Expression> parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}); - std::vector<storm::expressions::Expression> parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}); - + std::shared_ptr<storm::logic::Formula const> parseFormula(json const& propertyStructure, std::string const& context); + std::vector<storm::expressions::Expression> parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}, bool returnNoneOnUnknownOpString = false); + std::vector<storm::expressions::Expression> parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}, bool returnNoneOnUnknownOpString = false); + + std::vector<std::shared_ptr<storm::logic::Formula const>> parseUnaryFormulaArgument(json const& propertyStructure, std::string const& opstring, std::string const& context); + std::vector<std::shared_ptr<storm::logic::Formula const>> parseBinaryFormulaArguments(json const& propertyStructure, std::string const& opstring, std::string const& context); + + + std::shared_ptr<storm::jani::Composition> parseComposition(json const& compositionStructure); storm::expressions::Variable getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}); - + /** * The overall structure currently under inspection. */ diff --git a/src/storage/jani/BooleanVariable.cpp b/src/storage/jani/BooleanVariable.cpp index 3eb63780b..ca2934f93 100644 --- a/src/storage/jani/BooleanVariable.cpp +++ b/src/storage/jani/BooleanVariable.cpp @@ -3,7 +3,7 @@ namespace storm { namespace jani { - BooleanVariable::BooleanVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : Variable(name, variable, transient) { + BooleanVariable::BooleanVariable(std::string const& name, storm::expressions::Variable const& variable) : Variable(name, variable) { // Intentionally left empty. } @@ -19,7 +19,8 @@ namespace storm { if (initValue) { return std::make_shared<BooleanVariable>(name, variable, initValue.get(), transient); } else { - return std::make_shared<BooleanVariable>(name, variable, transient); + assert(!transient); + return std::make_shared<BooleanVariable>(name, variable); } } diff --git a/src/storage/jani/BooleanVariable.h b/src/storage/jani/BooleanVariable.h index 7fe9603e0..7eeea85fd 100644 --- a/src/storage/jani/BooleanVariable.h +++ b/src/storage/jani/BooleanVariable.h @@ -11,7 +11,7 @@ namespace storm { /*! * Creates a Boolean variable with initial value */ - BooleanVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient=false); + BooleanVariable(std::string const& name, storm::expressions::Variable const& variable); /*! * Creates a Boolean variable with initial value diff --git a/src/storage/jani/BoundedIntegerVariable.cpp b/src/storage/jani/BoundedIntegerVariable.cpp index 37b458ba4..1d04c8166 100644 --- a/src/storage/jani/BoundedIntegerVariable.cpp +++ b/src/storage/jani/BoundedIntegerVariable.cpp @@ -13,11 +13,7 @@ namespace storm { // Intentionally left empty. } - BoundedIntegerVariable::BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) : Variable(name, variable, transient), lowerBound(lowerBound), upperBound(upperBound) { - // Intentionally left empty. - } - - BoundedIntegerVariable::BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) : Variable(name, variable), lowerBound(lowerBound), upperBound(upperBound) { + BoundedIntegerVariable::BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) : Variable(name, variable), lowerBound(lowerBound), upperBound(upperBound) { // Intentionally left empty. } @@ -56,7 +52,8 @@ namespace storm { if (initValue) { return std::make_shared<BoundedIntegerVariable>(name, variable, initValue.get(), transient, lowerBound.get(), upperBound.get()); } else { - return std::make_shared<BoundedIntegerVariable>(name, variable, transient, lowerBound.get(), upperBound.get()); + assert(!transient); + return std::make_shared<BoundedIntegerVariable>(name, variable, lowerBound.get(), upperBound.get()); } } } diff --git a/src/storage/jani/BoundedIntegerVariable.h b/src/storage/jani/BoundedIntegerVariable.h index 733024b3d..9b5350d0e 100644 --- a/src/storage/jani/BoundedIntegerVariable.h +++ b/src/storage/jani/BoundedIntegerVariable.h @@ -16,10 +16,6 @@ namespace storm { * Creates a bounded integer variable with transient set to false and an initial value. */ BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initValue, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound); - /*! - * Creates a bounded integer variable without initial value. - */ - BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound); /*! * Creates a bounded integer variable with transient set to false and no initial value. */ diff --git a/src/storage/jani/JSONExporter.cpp b/src/storage/jani/JSONExporter.cpp index e6c1e9d60..2eefbb774 100644 --- a/src/storage/jani/JSONExporter.cpp +++ b/src/storage/jani/JSONExporter.cpp @@ -140,7 +140,7 @@ namespace storm { } boost::any FormulaToJaniJson::visit(storm::logic::AtomicLabelFormula const& f, boost::any const& data) const { - modernjson::json opDecl(f.isTrueFormula() ? "true" : "false"); + modernjson::json opDecl(f.getLabel()); return opDecl; } boost::any FormulaToJaniJson::visit(storm::logic::BinaryBooleanStateFormula const& f, boost::any const& data) const{ @@ -152,7 +152,7 @@ namespace storm { return opDecl; } boost::any FormulaToJaniJson::visit(storm::logic::BooleanLiteralFormula const& f, boost::any const& data) const { - modernjson::json opDecl(f.isTrueFormula() ? "true" : "false"); + modernjson::json opDecl(f.isTrueFormula() ? true : false); return opDecl; } boost::any FormulaToJaniJson::visit(storm::logic::BoundedUntilFormula const& f, boost::any const& data) const { @@ -173,7 +173,7 @@ namespace storm { } boost::any FormulaToJaniJson::visit(storm::logic::CumulativeRewardFormula const& f, boost::any const& data) const { - + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm currently does not support translating cummulative reward formulae"); } boost::any FormulaToJaniJson::visit(storm::logic::EventuallyFormula const& f, boost::any const& data) const { @@ -718,6 +718,7 @@ namespace storm { modernjson::json convertFilterExpression(storm::jani::FilterExpression const& fe, bool continuousModel) { modernjson::json propDecl; propDecl["states"] = "initial"; + propDecl["op"] = "filter"; propDecl["fun"] = janiFilterTypeString(fe.getFilterType()); propDecl["values"] = FormulaToJaniJson::translate(*fe.getFormula(), continuousModel); return propDecl; diff --git a/src/storage/jani/Property.h b/src/storage/jani/Property.h index bde51865e..be35820a4 100644 --- a/src/storage/jani/Property.h +++ b/src/storage/jani/Property.h @@ -31,6 +31,7 @@ namespace storm { class Property { + public: /** * Constructs the property * @param name the name diff --git a/src/storage/jani/RealVariable.cpp b/src/storage/jani/RealVariable.cpp index 8880a9a0a..f06e87a5c 100644 --- a/src/storage/jani/RealVariable.cpp +++ b/src/storage/jani/RealVariable.cpp @@ -3,7 +3,7 @@ namespace storm { namespace jani { - RealVariable::RealVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : storm::jani::Variable(name, variable, transient) { + RealVariable::RealVariable(std::string const& name, storm::expressions::Variable const& variable) : storm::jani::Variable(name, variable) { // Intentionally left empty. } diff --git a/src/storage/jani/RealVariable.h b/src/storage/jani/RealVariable.h index 74c337ed9..1783b6fbf 100644 --- a/src/storage/jani/RealVariable.h +++ b/src/storage/jani/RealVariable.h @@ -10,7 +10,7 @@ namespace storm { /*! * Creates a real variable without initial value. */ - RealVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient=false); + RealVariable(std::string const& name, storm::expressions::Variable const& variable); /*! * Creates a real variable with initial value. diff --git a/src/storage/jani/UnboundedIntegerVariable.cpp b/src/storage/jani/UnboundedIntegerVariable.cpp index c646b09b1..6b541054e 100644 --- a/src/storage/jani/UnboundedIntegerVariable.cpp +++ b/src/storage/jani/UnboundedIntegerVariable.cpp @@ -7,7 +7,7 @@ namespace storm { // Intentionally left empty. } - UnboundedIntegerVariable::UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : Variable(name, variable, transient) { + UnboundedIntegerVariable::UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : Variable(name, variable) { // Intentionally left empty. } diff --git a/src/storage/jani/Variable.cpp b/src/storage/jani/Variable.cpp index 8551f14df..f2c7217ff 100644 --- a/src/storage/jani/Variable.cpp +++ b/src/storage/jani/Variable.cpp @@ -12,7 +12,7 @@ namespace storm { // Intentionally left empty. } - Variable::Variable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : name(name), variable(variable), transient(transient), init() { + Variable::Variable(std::string const& name, storm::expressions::Variable const& variable) : name(name), variable(variable), transient(false), init() { // Intentionally left empty. } diff --git a/src/storage/jani/Variable.h b/src/storage/jani/Variable.h index cbbe4aa69..2eea79679 100644 --- a/src/storage/jani/Variable.h +++ b/src/storage/jani/Variable.h @@ -25,7 +25,7 @@ namespace storm { /*! * Creates a new variable without initial value construct. */ - Variable(std::string const& name, storm::expressions::Variable const& variable, bool transient = false); + Variable(std::string const& name, storm::expressions::Variable const& variable); virtual ~Variable(); diff --git a/src/storage/prism/ToJaniConverter.cpp b/src/storage/prism/ToJaniConverter.cpp index 65289382a..e3bc3c569 100644 --- a/src/storage/prism/ToJaniConverter.cpp +++ b/src/storage/prism/ToJaniConverter.cpp @@ -47,7 +47,7 @@ namespace storm { storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression(), false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression())); variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); } else { - storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression())); + storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression())); variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); } } @@ -56,7 +56,7 @@ namespace storm { storm::jani::BooleanVariable const& createdVariable = janiModel.addVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression(), false)); variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); } else { - storm::jani::BooleanVariable const& createdVariable = janiModel.addVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable(), false)); + storm::jani::BooleanVariable const& createdVariable = janiModel.addVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable())); variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); } } @@ -100,7 +100,7 @@ namespace storm { std::vector<storm::jani::Assignment> transientLocationAssignments; for (auto const& rewardModel : program.getRewardModels()) { auto newExpressionVariable = manager->declareRationalVariable(rewardModel.getName().empty() ? "default" : rewardModel.getName()); - storm::jani::RealVariable const& newTransientVariable = janiModel.addVariable(storm::jani::RealVariable(rewardModel.getName(), newExpressionVariable, true)); + storm::jani::RealVariable const& newTransientVariable = janiModel.addVariable(storm::jani::RealVariable(rewardModel.getName().empty() ? "defaultReward" : rewardModel.getName(), newExpressionVariable, manager->rational(0.0), true)); if (rewardModel.hasStateRewards()) { storm::expressions::Expression transientLocationExpression; diff --git a/src/utility/storm.cpp b/src/utility/storm.cpp index d4fb44290..5e1b8104e 100644 --- a/src/utility/storm.cpp +++ b/src/utility/storm.cpp @@ -15,8 +15,8 @@ namespace storm { return program; } - std::pair<storm::jani::Model, std::vector<storm::jani::Property>> parseJaniModel(std::string const& path) { - std::pair<storm::jani::Model, std::vector<storm::jani::Property>> modelAndFormulae = storm::parser::JaniParser::parse(path); + std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> parseJaniModel(std::string const& path) { + std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> modelAndFormulae = storm::parser::JaniParser::parse(path); modelAndFormulae.first.checkValid(); return modelAndFormulae; } diff --git a/src/utility/storm.h b/src/utility/storm.h index c5df89d64..336d6e399 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -100,7 +100,7 @@ namespace storm { return storm::parser::AutoParser<>::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "", choiceLabelingFile ? choiceLabelingFile.get() : "" ); } - std::pair<storm::jani::Model, std::vector<storm::jani::Property>> parseJaniModel(std::string const& path); + std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> parseJaniModel(std::string const& path); storm::prism::Program parseProgram(std::string const& path); std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForExplicit(std::string const& inputString); std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForPrismProgram(std::string const& inputString, storm::prism::Program const& program); From ed970d78b1f6cd0005a2e758446e5975c949e054 Mon Sep 17 00:00:00 2001 From: sjunges <sebastian.junges@rwth-aachen.de> Date: Sun, 16 Oct 2016 12:32:30 +0200 Subject: [PATCH 18/30] property support for jani -- several changes throughout code, parser currently only supports probability properties Former-commit-id: d5db0cda02b446032ba8e5f0ee883e5b4b80fbc7 [formerly 66d55d7e43ac62517e897f3bac4e8d9c51a471e5] Former-commit-id: 1672b21b127acf4a5f70fa4793d4bfa6776a8784 --- src/cli/cli.cpp | 45 ++++-- src/cli/entrypoints.h | 144 ++++++++++++----- .../ExplicitQualitativeCheckResult.cpp | 41 +++++ .../results/ExplicitQualitativeCheckResult.h | 6 + .../ExplicitQuantitativeCheckResult.cpp | 59 +++++++ .../results/ExplicitQuantitativeCheckResult.h | 6 + src/modelchecker/results/FilterType.cpp | 32 ++++ src/modelchecker/results/FilterType.h | 14 ++ .../results/HybridQuantitativeCheckResult.cpp | 14 ++ .../results/HybridQuantitativeCheckResult.h | 9 +- .../results/QualitativeCheckResult.h | 4 + .../results/QuantitativeCheckResult.h | 12 +- .../SymbolicQualitativeCheckResult.cpp | 17 ++ .../results/SymbolicQualitativeCheckResult.h | 6 + .../SymbolicQuantitativeCheckResult.cpp | 12 ++ .../results/SymbolicQuantitativeCheckResult.h | 7 +- src/parser/CSVParser.cpp | 23 +++ src/parser/CSVParser.h | 12 ++ src/parser/JaniParser.cpp | 148 +++++++++++++++--- src/parser/JaniParser.h | 9 +- src/parser/KeyValueParser.cpp | 26 +++ src/parser/KeyValueParser.h | 7 + src/settings/modules/IOSettings.cpp | 14 ++ src/settings/modules/IOSettings.h | 6 + src/storage/jani/JSONExporter.cpp | 42 ++--- src/storage/jani/JSONExporter.h | 5 +- src/storage/jani/Property.cpp | 23 ++- src/storage/jani/Property.h | 44 +++++- src/utility/constants.cpp | 95 +++++++++++ src/utility/constants.h | 15 ++ src/utility/storm.cpp | 11 +- src/utility/storm.h | 1 + 32 files changed, 792 insertions(+), 117 deletions(-) create mode 100644 src/modelchecker/results/FilterType.cpp create mode 100644 src/modelchecker/results/FilterType.h create mode 100644 src/parser/CSVParser.cpp create mode 100644 src/parser/CSVParser.h create mode 100644 src/parser/KeyValueParser.cpp create mode 100644 src/parser/KeyValueParser.h diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp index db9829084..a1b20b546 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -213,22 +213,38 @@ namespace storm { auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>(); if (ioSettings.isPrismOrJaniInputSet()) { storm::storage::SymbolicModelDescription model; + std::vector<storm::jani::Property> properties; + if (ioSettings.isPrismInputSet()) { model = storm::parseProgram(ioSettings.getPrismInputFilename()); if (ioSettings.isPrismToJaniSet()) { model = model.toJani(true); } } else if (ioSettings.isJaniInputSet()) { - model = storm::parseJaniModel(ioSettings.getJaniInputFilename()).first; + 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)); + } + } + } // Then proceed to parsing the properties (if given), since the model we are building may depend on the property. - std::vector<std::shared_ptr<storm::logic::Formula const>> formulas; + uint64_t i = 0; if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isPropertySet()) { if (model.isJaniModel()) { - formulas = storm::parseFormulasForJaniModel(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), model.asJaniModel()); + for(auto const& formula : storm::parseFormulasForJaniModel(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), model.asJaniModel())) { + properties.emplace_back(std::to_string(i), formula); + ++i; + } } else { - formulas = storm::parseFormulasForPrismProgram(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), model.asPrismProgram()); + for(auto const& formula :storm::parseFormulasForPrismProgram(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), model.asPrismProgram())) { + properties.emplace_back(std::to_string(i), formula); + ++i; + } } } @@ -236,9 +252,9 @@ namespace storm { if (storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isExportAsStandardJaniSet()) { storm::jani::Model normalisedModel = storm::jani::Model(model.asJaniModel()); normalisedModel.makeStandardJaniCompliant(); - storm::jani::JsonExporter::toFile(normalisedModel, formulas, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename()); + storm::jani::JsonExporter::toFile(normalisedModel, formulasInProperties(properties), storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename()); } else { - storm::jani::JsonExporter::toFile(model.asJaniModel(), formulas, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename()); + storm::jani::JsonExporter::toFile(model.asJaniModel(), formulasInProperties(properties), storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename()); } } @@ -250,30 +266,35 @@ namespace storm { if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isParametricSet()) { #ifdef STORM_HAVE_CARL - buildAndCheckSymbolicModel<storm::RationalFunction>(model, formulas, true); + buildAndCheckSymbolicModel<storm::RationalFunction>(model, properties, true); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No parameters are supported in this build."); #endif } else if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isExactSet()) { #ifdef STORM_HAVE_CARL - buildAndCheckSymbolicModel<storm::RationalNumber>(model, formulas, true); + buildAndCheckSymbolicModel<storm::RationalNumber>(model, properties, true); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No exact numbers are supported in this build."); #endif } else { - buildAndCheckSymbolicModel<double>(model, formulas, true); + buildAndCheckSymbolicModel<double>(model, properties, true); } } else if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExplicitSet()) { STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::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<std::shared_ptr<storm::logic::Formula const>> formulas; + std::vector<storm::jani::Property> properties; if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isPropertySet()) { - formulas = storm::parseFormulasForExplicit(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty()); + uint64_t i = 0; + for(auto const& formula : storm::parseFormulasForExplicit(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty())) { + properties.emplace_back(std::to_string(i), formula); + ++i; + + } } - buildAndCheckExplicitModel<double>(formulas, true); + buildAndCheckExplicitModel<double>(properties, true); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); } diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index f4b009b7e..3d933038a 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -12,15 +12,72 @@ namespace storm { namespace cli { template<typename ValueType> - void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) { - for (auto const& formula : formulas) { - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, formula, onlyInitialStatesRelevant)); + void applyFilterFunctionAndOutput(std::unique_ptr<storm::modelchecker::CheckResult> const& result, storm::modelchecker::FilterType ft) { + + if(result->isQuantitative()) { + switch(ft) { + case storm::modelchecker::FilterType::VALUES: + std::cout << *result << std::endl; + return; + case storm::modelchecker::FilterType::SUM: + std::cout << result->asQuantitativeCheckResult<ValueType>().sum(); + return; + case storm::modelchecker::FilterType::AVG: + std::cout << result->asQuantitativeCheckResult<ValueType>().average(); + return; + case storm::modelchecker::FilterType::MIN: + std::cout << result->asQuantitativeCheckResult<ValueType>().getMin(); + return; + case storm::modelchecker::FilterType::MAX: + std::cout << result->asQuantitativeCheckResult<ValueType>().getMax(); + return; + case storm::modelchecker::FilterType::ARGMIN: + case storm::modelchecker::FilterType::ARGMAX: + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "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, "FilterType only defined for qualitative results"); + } + } else { + switch(ft) { + case storm::modelchecker::FilterType::VALUES: + std::cout << *result << std::endl; + return; + case storm::modelchecker::FilterType::EXISTS: + std::cout << result->asQualitativeCheckResult().existsTrue(); + return; + case storm::modelchecker::FilterType::FORALL: + std::cout << result->asQualitativeCheckResult().forallTrue(); + return; + case storm::modelchecker::FilterType::COUNT: + std::cout << result->asQualitativeCheckResult().count(); + return; + + case storm::modelchecker::FilterType::ARGMIN: + case storm::modelchecker::FilterType::ARGMAX: + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "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, "FilterType only defined for quantitative results"); + } + + } + } + + template<typename ValueType> + void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant = false) { + for (auto const& property : properties) { + std::cout << std::endl << "Model checking property: " << property << " ..."; + std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); if (result) { std::cout << " done." << std::endl; std::cout << "Result (initial states): "; result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); - std::cout << *result << std::endl; + applyFilterFunctionAndOutput<ValueType>(result, property.getFilter().getFilterType()); + std::cout << std::endl; } else { std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; } @@ -29,17 +86,18 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - inline void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant) { + inline void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant) { - for (auto const& formula : formulas) { + for (auto const& property : properties) { STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc || model->getType() == storm::models::ModelType::Ctmc, storm::exceptions::InvalidSettingsException, "Currently parametric verification is only available for DTMCs and CTMCs."); - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, formula, onlyInitialStatesRelevant)); + std::cout << std::endl << "Model checking property: " << property << " ..."; + std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); if (result) { std::cout << " done." << std::endl; std::cout << "Result (initial states): "; result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); - std::cout << *result << std::endl; + applyFilterFunctionAndOutput<storm::RationalFunction>(result, property.getFilter().getFilterType()); + std::cout << std::endl; } else { std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; } @@ -52,24 +110,24 @@ namespace storm { #endif template<storm::dd::DdType DdType> - void verifySymbolicModelWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) { + void verifySymbolicModelWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant = false) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Abstraction Refinement is not yet implemented."); } template<typename ValueType> - void verifySymbolicModelWithExplorationEngine(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) { + void verifySymbolicModelWithExplorationEngine(storm::storage::SymbolicModelDescription const& model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant = false) { 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."); - for (auto const& formula : formulas) { - std::cout << std::endl << "Model checking property: " << *formula << " ..."; + for (auto const& property : formulas) { + std::cout << std::endl << "Model checking property: " << property << " ..."; bool supportFormula; std::unique_ptr<storm::modelchecker::CheckResult> result; if(program.getModelType() == storm::prism::Program::ModelType::DTMC) { storm::modelchecker::SparseExplorationModelChecker<storm::models::sparse::Dtmc<ValueType>> checker(program); - storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant); + storm::modelchecker::CheckTask<storm::logic::Formula> task(*property.getFilter().getFormula(), onlyInitialStatesRelevant); supportFormula = checker.canHandle(task); if (supportFormula) { @@ -77,7 +135,7 @@ namespace storm { } } else if(program.getModelType() == storm::prism::Program::ModelType::MDP) { storm::modelchecker::SparseExplorationModelChecker<storm::models::sparse::Mdp<ValueType>> checker(program); - storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant); + storm::modelchecker::CheckTask<storm::logic::Formula> task(*property.getFilter().getFormula(), onlyInitialStatesRelevant); supportFormula = checker.canHandle(task); if (supportFormula) { @@ -94,7 +152,8 @@ namespace storm { if (result) { std::cout << " done." << std::endl; std::cout << "Result (initial states): "; - std::cout << *result << std::endl; + applyFilterFunctionAndOutput<ValueType>(result, property.getFilter().getFilterType()); + std::cout << std::endl; } else { std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; } @@ -103,22 +162,23 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - void verifySymbolicModelWithExplorationEngine<storm::RationalFunction>(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant) { + void verifySymbolicModelWithExplorationEngine<storm::RationalFunction>(storm::storage::SymbolicModelDescription const& model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant) { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Exploration-based verification does currently not support parametric models."); } #endif template<storm::dd::DdType DdType> - void verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) { - for (auto const& formula : formulas) { - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithHybridEngine(model, formula, onlyInitialStatesRelevant)); + void verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant = false) { + for (auto const& property : formulas) { + std::cout << std::endl << "Model checking property: " << property << " ..."; + std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithHybridEngine(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); if (result) { std::cout << " done." << std::endl; std::cout << "Result (initial states): "; result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(model->getReachableStates(), model->getInitialStates())); - std::cout << *result << std::endl; + applyFilterFunctionAndOutput<double>(result, property.getFilter().getFilterType()); + std::cout << std::endl; } else { std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; } @@ -126,15 +186,16 @@ namespace storm { } template<storm::dd::DdType DdType> - void verifySymbolicModelWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) { - for (auto const& formula : formulas) { - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithDdEngine(model, formula, onlyInitialStatesRelevant)); + void verifySymbolicModelWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant = false) { + for (auto const& property : formulas) { + std::cout << std::endl << "Model checking property: " << property << " ..."; + std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithDdEngine(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); if (result) { std::cout << " done." << std::endl; std::cout << "Result (initial states): "; result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(model->getReachableStates(), model->getInitialStates())); - std::cout << *result << std::endl; + applyFilterFunctionAndOutput<double>(result, property.getFilter().getFilterType()); + std::cout << std::endl; } else { std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; } @@ -182,23 +243,24 @@ namespace storm { } template<storm::dd::DdType LibraryType> - void buildAndCheckSymbolicModelWithSymbolicEngine(bool hybrid, storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) { + void buildAndCheckSymbolicModelWithSymbolicEngine(bool hybrid, storm::storage::SymbolicModelDescription const& model, std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant = false) { // Start by building the model. - auto markovModel = buildSymbolicModel<double, LibraryType>(model, formulas); + auto markovModel = buildSymbolicModel<double, LibraryType>(model, formulasInProperties(properties)); // Print some information about the model. markovModel->printModelInformationToStream(std::cout); // Then select the correct engine. if (hybrid) { - verifySymbolicModelWithHybridEngine(markovModel, formulas, onlyInitialStatesRelevant); + verifySymbolicModelWithHybridEngine(markovModel, properties, onlyInitialStatesRelevant); } else { - verifySymbolicModelWithDdEngine(markovModel, formulas, onlyInitialStatesRelevant); + verifySymbolicModelWithDdEngine(markovModel, properties, onlyInitialStatesRelevant); } } template<typename ValueType> - void buildAndCheckSymbolicModelWithSparseEngine(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) { + void buildAndCheckSymbolicModelWithSparseEngine(storm::storage::SymbolicModelDescription const& model, std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant = false) { + auto formulas = formulasInProperties(properties); // Start by building the model. std::shared_ptr<storm::models::ModelBase> markovModel = buildSparseModel<ValueType>(model, formulas); @@ -214,12 +276,12 @@ namespace storm { if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isCounterexampleSet()) { generateCounterexamples<ValueType>(model, sparseModel, formulas); } else { - verifySparseModel<ValueType>(sparseModel, formulas, onlyInitialStatesRelevant); + verifySparseModel<ValueType>(sparseModel, properties, onlyInitialStatesRelevant); } } template<typename ValueType> - void buildAndCheckSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) { + void buildAndCheckSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant = false) { if (storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement) { auto ddlib = storm::settings::getModule<storm::settings::modules::CoreSettings>().getDdLibraryType(); if (ddlib == storm::dd::DdType::CUDD) { @@ -247,35 +309,35 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - void buildAndCheckSymbolicModel<storm::RationalNumber>(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant) { + void buildAndCheckSymbolicModel<storm::RationalNumber>(storm::storage::SymbolicModelDescription const& model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant) { STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use this data type with an engine different than the sparse one."); buildAndCheckSymbolicModelWithSparseEngine<storm::RationalNumber>(model, formulas, onlyInitialStatesRelevant); } template<> - void buildAndCheckSymbolicModel<storm::RationalFunction>(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant) { + void buildAndCheckSymbolicModel<storm::RationalFunction>(storm::storage::SymbolicModelDescription const& model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant) { STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use this data type with an engine different than the sparse one."); buildAndCheckSymbolicModelWithSparseEngine<storm::RationalFunction>(model, formulas, onlyInitialStatesRelevant); } #endif template<typename ValueType> - void buildAndCheckExplicitModel(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) { + void buildAndCheckExplicitModel(std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant = false) { storm::settings::modules::IOSettings const& settings = storm::settings::getModule<storm::settings::modules::IOSettings>(); STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files."); std::shared_ptr<storm::models::ModelBase> model = buildExplicitModel<ValueType>(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? boost::optional<std::string>(settings.getStateRewardsFilename()) : boost::none, settings.isTransitionRewardsSet() ? boost::optional<std::string>(settings.getTransitionRewardsFilename()) : boost::none, settings.isChoiceLabelingSet() ? boost::optional<std::string>(settings.getChoiceLabelingFilename()) : boost::none); // Preprocess the model if needed. - BRANCH_ON_MODELTYPE(model, model, ValueType, storm::dd::DdType::CUDD, preprocessModel, formulas); + BRANCH_ON_MODELTYPE(model, model, ValueType, storm::dd::DdType::CUDD, preprocessModel, formulasInProperties(properties)); // Print some information about the model. model->printModelInformationToStream(std::cout); // Verify the model, if a formula was given. - if (!formulas.empty()) { + if (!properties.empty()) { STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidStateException, "Expected sparse model."); - verifySparseModel<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), formulas, onlyInitialStatesRelevant); + verifySparseModel<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), properties, onlyInitialStatesRelevant); } } } diff --git a/src/modelchecker/results/ExplicitQualitativeCheckResult.cpp b/src/modelchecker/results/ExplicitQualitativeCheckResult.cpp index aa86846fa..f5488122c 100644 --- a/src/modelchecker/results/ExplicitQualitativeCheckResult.cpp +++ b/src/modelchecker/results/ExplicitQualitativeCheckResult.cpp @@ -70,6 +70,47 @@ namespace storm { return *this; } + + bool ExplicitQualitativeCheckResult::existsTrue() const { + if (this->isResultForAllStates()) { + return !boost::get<vector_type>(truthValues).empty(); + } else { + for (auto& element : boost::get<map_type>(truthValues)) { + if(element.second) { + return true; + } + } + return false; + } + } + bool ExplicitQualitativeCheckResult::forallTrue() const { + if (this->isResultForAllStates()) { + return boost::get<vector_type>(truthValues).full(); + } else { + for (auto& element : boost::get<map_type>(truthValues)) { + if(!element.second) { + return false; + } + } + return true; + } + } + + uint64_t ExplicitQualitativeCheckResult::count() const { + if (this->isResultForAllStates()) { + return boost::get<vector_type>(truthValues).getNumberOfSetBits(); + } else { + uint64_t result = 0; + for (auto& element : boost::get<map_type>(truthValues)) { + if(element.second) { + ++result; + } + } + return result; + } + } + + bool ExplicitQualitativeCheckResult::operator[](storm::storage::sparse::state_type state) const { if (this->isResultForAllStates()) { return boost::get<vector_type>(truthValues).get(state); diff --git a/src/modelchecker/results/ExplicitQualitativeCheckResult.h b/src/modelchecker/results/ExplicitQualitativeCheckResult.h index 665675cfd..afb54b4be 100644 --- a/src/modelchecker/results/ExplicitQualitativeCheckResult.h +++ b/src/modelchecker/results/ExplicitQualitativeCheckResult.h @@ -47,6 +47,12 @@ namespace storm { vector_type const& getTruthValuesVector() const; map_type const& getTruthValuesVectorMap() const; + + virtual bool existsTrue() const override; + virtual bool forallTrue() const override; + virtual uint64_t count() const override; + + virtual std::ostream& writeToStream(std::ostream& out) const override; virtual void filter(QualitativeCheckResult const& filter) override; diff --git a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index 6233216d9..87ba9e0fa 100644 --- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -3,6 +3,7 @@ #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/storage/BitVector.h" #include "src/utility/macros.h" +#include "src/utility/constants.h" #include "src/utility/vector.h" #include "src/exceptions/InvalidOperationException.h" #include "src/exceptions/InvalidAccessException.h" @@ -81,6 +82,64 @@ namespace storm { } } + template<typename ValueType> + ValueType ExplicitQuantitativeCheckResult<ValueType>::getMin() const { + STORM_LOG_THROW(!values.empty(),storm::exceptions::InvalidOperationException, "Minimum of empty set is not defined"); + + if (this->isResultForAllStates()) { + return storm::utility::minimum(boost::get<vector_type>(values)); + } else { + return storm::utility::minimum(boost::get<map_type>(values)); + } + } + + + template<typename ValueType> + ValueType ExplicitQuantitativeCheckResult<ValueType>::getMax() const { + STORM_LOG_THROW(!values.empty(),storm::exceptions::InvalidOperationException, "Minimum of empty set is not defined"); + + if (this->isResultForAllStates()) { + return storm::utility::maximum(boost::get<vector_type>(values)); + } else { + return storm::utility::maximum(boost::get<map_type>(values)); + } + } + + template<typename ValueType> + ValueType ExplicitQuantitativeCheckResult<ValueType>::sum() const { + STORM_LOG_THROW(!values.empty(),storm::exceptions::InvalidOperationException, "Minimum of empty set is not defined"); + + ValueType sum = storm::utility::zero<ValueType>(); + if (this->isResultForAllStates()) { + for (auto& element : boost::get<vector_type>(values)) { + sum += element; + } + } else { + for (auto& element : boost::get<map_type>(values)) { + sum += element.second; + } + } + return sum; + } + + template<typename ValueType> + ValueType ExplicitQuantitativeCheckResult<ValueType>::average() const { + STORM_LOG_THROW(!values.empty(),storm::exceptions::InvalidOperationException, "Minimum of empty set is not defined"); + + ValueType sum = storm::utility::zero<ValueType>(); + if (this->isResultForAllStates()) { + for (auto& element : boost::get<vector_type>(values)) { + sum += element; + } + return sum / boost::get<vector_type>(values).size(); + } else { + for (auto& element : boost::get<map_type>(values)) { + sum += element.second; + } + return sum / boost::get<map_type>(values).size(); + } + } + template<typename ValueType> bool ExplicitQuantitativeCheckResult<ValueType>::hasScheduler() const { return static_cast<bool>(scheduler); diff --git a/src/modelchecker/results/ExplicitQuantitativeCheckResult.h b/src/modelchecker/results/ExplicitQuantitativeCheckResult.h index 639da4fa7..d2bb9f711 100644 --- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.h +++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.h @@ -53,6 +53,12 @@ namespace storm { virtual void oneMinus() override; + + virtual ValueType getMin() const override; + virtual ValueType getMax() const override; + virtual ValueType average() const override; + virtual ValueType sum() const override; + bool hasScheduler() const; void setScheduler(std::unique_ptr<storm::storage::Scheduler>&& scheduler); storm::storage::Scheduler const& getScheduler() const; diff --git a/src/modelchecker/results/FilterType.cpp b/src/modelchecker/results/FilterType.cpp new file mode 100644 index 000000000..3a15c8169 --- /dev/null +++ b/src/modelchecker/results/FilterType.cpp @@ -0,0 +1,32 @@ +#include "FilterType.h" + + +namespace storm { + namespace modelchecker { + + std::string toString(FilterType ft) { + switch(ft) { + case FilterType::ARGMAX: + return "the argmax"; + case FilterType::ARGMIN: + return "the argmin"; + case FilterType::AVG: + return "the average"; + case FilterType::COUNT: + return "the number of"; + case FilterType::EXISTS: + return "whether there exists a state in"; + case FilterType::FORALL: + return "whether for all states in"; + case FilterType::MAX: + return "the maximum"; + case FilterType::MIN: + return "the minumum"; + case FilterType::SUM: + return "the sum"; + case FilterType::VALUES: + return "the values"; + } + } + } +} \ No newline at end of file diff --git a/src/modelchecker/results/FilterType.h b/src/modelchecker/results/FilterType.h new file mode 100644 index 000000000..040b09084 --- /dev/null +++ b/src/modelchecker/results/FilterType.h @@ -0,0 +1,14 @@ +#pragma once +#include <string> + +namespace storm { + namespace modelchecker { + + enum class StateFilter { ARGMIN, ARGMAX }; + + enum class FilterType { MIN, MAX, SUM, AVG, COUNT, FORALL, EXISTS, ARGMIN, ARGMAX, VALUES }; + + std::string toString(FilterType); + bool isStateFilter(FilterType); + } +} \ No newline at end of file diff --git a/src/modelchecker/results/HybridQuantitativeCheckResult.cpp b/src/modelchecker/results/HybridQuantitativeCheckResult.cpp index a32095e40..62fe2c1dd 100644 --- a/src/modelchecker/results/HybridQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/HybridQuantitativeCheckResult.cpp @@ -5,9 +5,12 @@ #include "src/storage/dd/cudd/CuddAddIterator.h" #include "src/exceptions/InvalidOperationException.h" + +#include "src/exceptions/NotImplementedException.h" #include "src/utility/macros.h" #include "src/utility/constants.h" + namespace storm { namespace modelchecker { template<storm::dd::DdType Type, typename ValueType> @@ -164,6 +167,16 @@ namespace storm { return max; } + template<storm::dd::DdType Type, typename ValueType> + ValueType HybridQuantitativeCheckResult<Type, ValueType>::sum() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Sum not implemented for hybrid results"); + } + + template<storm::dd::DdType Type, typename ValueType> + ValueType HybridQuantitativeCheckResult<Type, ValueType>::average() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Average not implemented for hybrid results"); + } + template<storm::dd::DdType Type, typename ValueType> void HybridQuantitativeCheckResult<Type, ValueType>::oneMinus() { storm::dd::Add<Type> one = symbolicValues.getDdManager().template getAddOne<ValueType>(); @@ -175,6 +188,7 @@ namespace storm { } } + // Explicitly instantiate the class. template class HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>; template class HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>; diff --git a/src/modelchecker/results/HybridQuantitativeCheckResult.h b/src/modelchecker/results/HybridQuantitativeCheckResult.h index 8b7db1cea..16a802331 100644 --- a/src/modelchecker/results/HybridQuantitativeCheckResult.h +++ b/src/modelchecker/results/HybridQuantitativeCheckResult.h @@ -46,9 +46,14 @@ namespace storm { virtual void filter(QualitativeCheckResult const& filter) override; - virtual ValueType getMin() const; + virtual ValueType getMin() const override; - virtual ValueType getMax() const; + virtual ValueType getMax() const override; + + virtual ValueType sum() const override; + + virtual ValueType average() const override; + virtual void oneMinus() override; diff --git a/src/modelchecker/results/QualitativeCheckResult.h b/src/modelchecker/results/QualitativeCheckResult.h index 608e2c0d1..f4a89665b 100644 --- a/src/modelchecker/results/QualitativeCheckResult.h +++ b/src/modelchecker/results/QualitativeCheckResult.h @@ -12,6 +12,10 @@ namespace storm { virtual QualitativeCheckResult& operator|=(QualitativeCheckResult const& other); virtual void complement(); + virtual bool existsTrue() const = 0; + virtual bool forallTrue() const = 0; + virtual uint64_t count() const = 0; + virtual bool isQualitative() const override; }; } diff --git a/src/modelchecker/results/QuantitativeCheckResult.h b/src/modelchecker/results/QuantitativeCheckResult.h index bb268ae3f..2e9abe6a9 100644 --- a/src/modelchecker/results/QuantitativeCheckResult.h +++ b/src/modelchecker/results/QuantitativeCheckResult.h @@ -1,5 +1,4 @@ -#ifndef STORM_MODELCHECKER_QUANTITATIVECHECKRESULT_H_ -#define STORM_MODELCHECKER_QUANTITATIVECHECKRESULT_H_ +#pragma once #include "src/modelchecker/results/CheckResult.h" @@ -14,9 +13,16 @@ namespace storm { virtual void oneMinus() = 0; + + virtual ValueType getMin() const = 0; + + virtual ValueType getMax() const = 0; + + virtual ValueType average() const = 0; + virtual ValueType sum() const = 0; + virtual bool isQuantitative() const override; }; } } -#endif /* STORM_MODELCHECKER_QUANTITATIVECHECKRESULT_H_ */ \ No newline at end of file diff --git a/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp b/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp index 2275b942f..3468a13c9 100644 --- a/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp +++ b/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp @@ -3,6 +3,8 @@ #include "src/utility/macros.h" #include "src/exceptions/InvalidOperationException.h" +#include "src/exceptions/NotImplementedException.h" + namespace storm { namespace modelchecker { template <storm::dd::DdType Type> @@ -49,6 +51,21 @@ namespace storm { return truthValues; } + template <storm::dd::DdType Type> + bool SymbolicQualitativeCheckResult<Type>::existsTrue() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Exists not implemented for symbolic results"); + } + + template <storm::dd::DdType Type> + bool SymbolicQualitativeCheckResult<Type>::forallTrue() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Forall not implemented for symbolic results"); + } + + template <storm::dd::DdType Type> + uint64_t SymbolicQualitativeCheckResult<Type>::count() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Count not implemented for symbolic results"); + } + template <storm::dd::DdType Type> std::ostream& SymbolicQualitativeCheckResult<Type>::writeToStream(std::ostream& out) const { if (this->truthValues.isZero()) { diff --git a/src/modelchecker/results/SymbolicQualitativeCheckResult.h b/src/modelchecker/results/SymbolicQualitativeCheckResult.h index 3e94f5ee8..775b8c467 100644 --- a/src/modelchecker/results/SymbolicQualitativeCheckResult.h +++ b/src/modelchecker/results/SymbolicQualitativeCheckResult.h @@ -30,6 +30,12 @@ namespace storm { virtual QualitativeCheckResult& operator|=(QualitativeCheckResult const& other) override; virtual void complement() override; + + virtual bool existsTrue() const override; + virtual bool forallTrue() const override; + virtual uint64_t count() const override; + + storm::dd::Bdd<Type> const& getTruthValuesVector() const; virtual std::ostream& writeToStream(std::ostream& out) const override; diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp index 57f68bdf1..bde1407a4 100644 --- a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp @@ -5,6 +5,8 @@ #include "src/storage/dd/cudd/CuddAddIterator.h" #include "src/exceptions/InvalidOperationException.h" + +#include "src/exceptions/NotImplementedException.h" #include "src/utility/macros.h" #include "src/utility/constants.h" @@ -89,6 +91,16 @@ namespace storm { return this->values.getMax(); } + template<storm::dd::DdType Type, typename ValueType> + ValueType SymbolicQuantitativeCheckResult<Type, ValueType>::average() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Average not implemented for symbolic results"); + } + + template<storm::dd::DdType Type, typename ValueType> + ValueType SymbolicQuantitativeCheckResult<Type, ValueType>::sum() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Sum not implemented for symbolic results"); + } + template<storm::dd::DdType Type, typename ValueType> void SymbolicQuantitativeCheckResult<Type, ValueType>::oneMinus() { storm::dd::Add<Type> one = values.getDdManager().template getAddOne<ValueType>(); diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.h b/src/modelchecker/results/SymbolicQuantitativeCheckResult.h index fd03da786..36b0c4cce 100644 --- a/src/modelchecker/results/SymbolicQuantitativeCheckResult.h +++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.h @@ -35,9 +35,12 @@ namespace storm { virtual void filter(QualitativeCheckResult const& filter) override; - virtual ValueType getMin() const; + virtual ValueType getMin() const override; - virtual ValueType getMax() const; + virtual ValueType getMax() const override; + + virtual ValueType average() const override; + virtual ValueType sum() const override; virtual void oneMinus() override; diff --git a/src/parser/CSVParser.cpp b/src/parser/CSVParser.cpp new file mode 100644 index 000000000..04e26a3fa --- /dev/null +++ b/src/parser/CSVParser.cpp @@ -0,0 +1,23 @@ +#include "src/parser/CSVParser.h" +#include <boost/any.hpp> + +#include <boost/algorithm/string.hpp> +#include "src/utility/macros.h" +#include "src/exceptions/InvalidArgumentException.h" + + +namespace storm { + namespace parser { + + std::vector<std::string> parseCommaSeperatedValues(std::string const& input) { + std::vector<std::string> values; + std::vector<std::string> definitions; + boost::split(definitions, input, boost::is_any_of(",")); + for (auto& definition : definitions) { + boost::trim(definition); + values.push_back(definition); + } + return values; + } + } +} \ No newline at end of file diff --git a/src/parser/CSVParser.h b/src/parser/CSVParser.h new file mode 100644 index 000000000..ec21f2e80 --- /dev/null +++ b/src/parser/CSVParser.h @@ -0,0 +1,12 @@ +#include <vector> +#include <string> + +namespace storm { + namespace parser { + /** + * Given a string seperated by commas, returns the values. + */ + std::vector<std::string> parseCommaSeperatedValues(std::string const& input); + + } +} \ No newline at end of file diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index bc094f197..b6fe64bc6 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -10,6 +10,7 @@ #include "src/exceptions/NotImplementedException.h" #include "src/storage/jani/ModelType.h" +#include "src/modelchecker/results/FilterType.h" #include <iostream> #include <sstream> @@ -153,11 +154,41 @@ namespace storm { return { parseFormula(propertyStructure.at("left"), "Operand of operator " + opstring), parseFormula(propertyStructure.at("right"), "Operand of operator " + opstring) }; } - + storm::jani::PropertyInterval JaniParser::parsePropertyInterval(json const& piStructure) { + storm::jani::PropertyInterval pi; + if (piStructure.count("lower") > 0) { + pi.lowerBound = parseExpression(piStructure.at("lower"), "Lower bound for property interval"); + // TODO substitute constants. + STORM_LOG_THROW(!pi.lowerBound.containsVariables(), storm::exceptions::NotSupportedException, "Only constant expressions are supported as lower bounds"); + + + } + if (piStructure.count("lower-exclusive") > 0) { + STORM_LOG_THROW(pi.lowerBound.isInitialized(), storm::exceptions::InvalidJaniException, "Lower-exclusive can only be set if a lower bound is present"); + pi.lowerBoundStrict = piStructure.at("lower-exclusive"); + + } + if (piStructure.count("upper") > 0) { + pi.upperBound = parseExpression(piStructure.at("upper"), "Upper bound for property interval"); + // TODO substitute constants. + STORM_LOG_THROW(!pi.upperBound.containsVariables(), storm::exceptions::NotSupportedException, "Only constant expressions are supported as upper bounds"); + + } + if (piStructure.count("upper-exclusive") > 0) { + STORM_LOG_THROW(pi.lowerBound.isInitialized(), storm::exceptions::InvalidJaniException, "Lower-exclusive can only be set if a lower bound is present"); + pi.lowerBoundStrict = piStructure.at("upper-exclusive"); + } + STORM_LOG_THROW(pi.lowerBound.isInitialized() || pi.upperBound.isInitialized(), storm::exceptions::InvalidJaniException, "Bounded operators must be bounded"); + return pi; + + + } - std::shared_ptr<storm::logic::Formula const> JaniParser::parseFormula(json const& propertyStructure, std::string const& context) { - storm::expressions::Expression expr = parseExpression(propertyStructure, "Expression in property", {}, true); + std::shared_ptr<storm::logic::Formula const> JaniParser::parseFormula(json const& propertyStructure, std::string const& context, boost::optional<storm::logic::Bound<storm::RationalNumber>> bound) { + + storm::expressions::Expression expr = parseExpression(propertyStructure, "expression in property", {}, true); if(expr.isInitialized()) { + assert(bound == boost::none); return std::make_shared<storm::logic::AtomicExpressionFormula>(expr); } else if(propertyStructure.count("op") == 1) { std::string opString = getString(propertyStructure.at("op"), "Operation description"); @@ -167,9 +198,11 @@ namespace storm { assert(args.size() == 1); storm::logic::OperatorInformation opInfo; opInfo.optimalityType = opString == "Pmin" ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize; + opInfo.bound = bound; return std::make_shared<storm::logic::ProbabilityOperatorFormula>(args[0], opInfo); } else if (opString == "∀" || opString == "∃") { + assert(bound == boost::none); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Forall and Exists are currently not supported"); } else if (opString == "Emin" || opString == "Emax") { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Emin and Emax are currently not supported"); @@ -177,29 +210,84 @@ namespace storm { std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseUnaryFormulaArgument(propertyStructure, opString, ""); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Smin and Smax are currently not supported"); } else if (opString == "U") { + assert(bound == boost::none); std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseBinaryFormulaArguments(propertyStructure, opString, ""); if (propertyStructure.count("step-bounds") > 0) { - + storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("step-bounds")); + STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports step-bounded until with an upper bound"); + if(pi.hasLowerBound()) { + STORM_LOG_THROW(pi.lowerBound.evaluateAsInt() == 0, storm::exceptions::NotSupportedException, "Storm only supports step-bounded until without a (non-trivial) lower-bound"); + } + int64_t upperBound = pi.upperBound.evaluateAsInt(); + if(pi.upperBoundStrict) { + upperBound--; + } + STORM_LOG_THROW(upperBound >= 0, storm::exceptions::InvalidJaniException, "Step-bounds cannot be negative"); + return std::make_shared<storm::logic::BoundedUntilFormula const>(args[0], args[1], upperBound); } else if (propertyStructure.count("time-bounds") > 0) { + storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("time-bounds")); + STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports time-bounded until with an upper bound."); + double lowerBound = 0.0; + if(pi.hasLowerBound()) { + lowerBound = pi.lowerBound.evaluateAsDouble(); + } + double upperBound = pi.upperBound.evaluateAsDouble(); + STORM_LOG_THROW(lowerBound >= 0, storm::exceptions::InvalidJaniException, "(Lower) time-bounds cannot be negative"); + STORM_LOG_THROW(upperBound >= 0, storm::exceptions::InvalidJaniException, "(Upper) time-bounds cannot be negative"); + return std::make_shared<storm::logic::BoundedUntilFormula const>(args[0], args[1], upperBound); } else if (propertyStructure.count("reward-bounds") > 0 ) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by Storm"); } - return std::make_shared<storm::logic::UntilFormula const>(args[0], args[1]); + if (args[0]->isTrueFormula()) { + return std::make_shared<storm::logic::EventuallyFormula const>(args[1]); + } else { + return std::make_shared<storm::logic::UntilFormula const>(args[0], args[1]); + } } else if (opString == "W") { + assert(bound == boost::none); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Weak until is not supported"); } else if (opString == "∧" || opString == "∨") { + assert(bound == boost::none); std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseBinaryFormulaArguments(propertyStructure, opString, ""); assert(args.size() == 2); storm::logic::BinaryBooleanStateFormula::OperatorType oper = opString == "∧" ? storm::logic::BinaryBooleanStateFormula::OperatorType::And : storm::logic::BinaryBooleanStateFormula::OperatorType::Or; return std::make_shared<storm::logic::BinaryBooleanStateFormula const>(oper, args[0], args[1]); } else if (opString == "¬") { + assert(bound == boost::none); std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseUnaryFormulaArgument(propertyStructure, opString, ""); assert(args.size() == 1); return std::make_shared<storm::logic::UnaryBooleanStateFormula const>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, args[0]); + } else if (opString == "≥" || opString == "≤" || opString == "<" || opString == ">") { + assert(bound == boost::none); + storm::logic::ComparisonType ct; + if(opString == "≥") { + ct = storm::logic::ComparisonType::GreaterEqual; + } else if (opString == "≤") { + ct = storm::logic::ComparisonType::LessEqual; + } else if (opString == "<") { + ct = storm::logic::ComparisonType::Less; + } else if (opString == ">") { + ct = storm::logic::ComparisonType::Greater; + } + if (propertyStructure.at("left").count("op") > 0 && (propertyStructure.at("left").at("op") == "Pmin" || propertyStructure.at("left").at("op") == "Pmax" || propertyStructure.at("left").at("op") == "Emin" || propertyStructure.at("left").at("op") == "Emax" || propertyStructure.at("left").at("op") == "Smin" || propertyStructure.at("left").at("op") == "Smax")) { + auto expr = parseExpression(propertyStructure.at("right"), "Threshold for operator " + propertyStructure.at("left").at("op").get<std::string>()); + STORM_LOG_THROW(expr.getVariables().empty(), storm::exceptions::NotSupportedException, "Only constant thresholds supported"); + // TODO evaluate this expression directly as rational number + return parseFormula(propertyStructure.at("left"), "", storm::logic::Bound<storm::RationalNumber>(ct, storm::utility::convertNumber<storm::RationalNumber>(expr.evaluateAsDouble()))); + } else if(propertyStructure.at("right").count("op") > 0 && (propertyStructure.at("right").at("op") == "Pmin" || propertyStructure.at("right").at("op") == "Pmax" || propertyStructure.at("right").at("op") == "Emin" || propertyStructure.at("right").at("op") == "Emax" || propertyStructure.at("right").at("op") == "Smin" || propertyStructure.at("right").at("op") == "Smax")) { + auto expr = parseExpression(propertyStructure.at("left"), "Threshold for operator " + propertyStructure.at("right").at("op").get<std::string>()); + STORM_LOG_THROW(expr.getVariables().empty(), storm::exceptions::NotSupportedException, "Only constant thresholds supported"); + // TODO evaluate this expression directly as rational number + return parseFormula(propertyStructure.at("right"), "", storm::logic::Bound<storm::RationalNumber>(ct, storm::utility::convertNumber<storm::RationalNumber>(expr.evaluateAsDouble()))); + + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No complex comparisons are allowed."); + } + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown operator " << opString); } - } } @@ -220,38 +308,38 @@ namespace storm { STORM_LOG_THROW(expressionStructure.at("op") == "filter", storm::exceptions::InvalidJaniException, "Top level operation of a property must be a filter"); STORM_LOG_THROW(expressionStructure.count("fun") == 1, storm::exceptions::InvalidJaniException, "Filter must have a function descritpion"); std::string funDescr = getString(expressionStructure.at("fun"), "Filter function in property named " + name); - storm::jani::FilterType ft; + storm::modelchecker::FilterType ft; if (funDescr == "min") { - ft = storm::jani::FilterType::MIN; + ft = storm::modelchecker::FilterType::MIN; } else if (funDescr == "max") { - ft = storm::jani::FilterType::MAX; + ft = storm::modelchecker::FilterType::MAX; } else if (funDescr == "sum") { - ft = storm::jani::FilterType::SUM; + ft = storm::modelchecker::FilterType::SUM; } else if (funDescr == "avg") { - ft = storm::jani::FilterType::AVG; + ft = storm::modelchecker::FilterType::AVG; } else if (funDescr == "count") { - ft = storm::jani::FilterType::COUNT; + ft = storm::modelchecker::FilterType::COUNT; } else if (funDescr == "∀") { - ft = storm::jani::FilterType::FORALL; + ft = storm::modelchecker::FilterType::FORALL; } else if (funDescr == "∃") { - ft = storm::jani::FilterType::EXISTS; + ft = storm::modelchecker::FilterType::EXISTS; } else if (funDescr == "argmin") { - ft = storm::jani::FilterType::ARGMIN; + ft = storm::modelchecker::FilterType::ARGMIN; } else if (funDescr == "argmax") { - ft = storm::jani::FilterType::ARGMAX; + ft = storm::modelchecker::FilterType::ARGMAX; } else if (funDescr == "values") { - ft = storm::jani::FilterType::VALUES; + ft = storm::modelchecker::FilterType::VALUES; } else { STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown filter description " << funDescr << " in property named " << name); } STORM_LOG_THROW(expressionStructure.count("states") == 1, storm::exceptions::InvalidJaniException, "Filter must have a states description"); - STORM_LOG_THROW(expressionStructure.at("states").is_string(), storm::exceptions::NotImplementedException, "We only support properties where the filter has a non-complex description of the states"); - std::string statesDescr = getString(expressionStructure.at("states"), "Filtered states in property named " + name); + STORM_LOG_THROW(expressionStructure.at("states").count("op") > 0, storm::exceptions::NotImplementedException, "We only support properties where the filter has initial states"); + std::string statesDescr = getString(expressionStructure.at("states").at("op"), "Filtered states in property named " + name); STORM_LOG_THROW(statesDescr == "initial", storm::exceptions::NotImplementedException, "Only initial states are allowed as set of states we are interested in."); STORM_LOG_THROW(expressionStructure.count("values") == 1, storm::exceptions::InvalidJaniException, "Values as input for a filter must be given"); auto formula = parseFormula(expressionStructure.at("values"), "Values of property " + name); - return storm::jani::Property(name, formula, comment); + return storm::jani::Property(name, storm::jani::FilterExpression(formula, ft), comment); } std::shared_ptr<storm::jani::Constant> JaniParser::parseConstant(json const& constantStructure, std::string const& scopeDescription) { @@ -567,26 +655,38 @@ namespace storm { return arguments[0] != arguments[1]; } } else if (opstring == "<") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); + if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { + return storm::expressions::Expression(); + } ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] < arguments[1]; } else if (opstring == "≤") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); + if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { + return storm::expressions::Expression(); + } ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] <= arguments[1]; } else if (opstring == ">") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); + if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { + return storm::expressions::Expression(); + } ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] > arguments[1]; } else if (opstring == "≥") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); + if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { + return storm::expressions::Expression(); + } ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] >= arguments[1]; diff --git a/src/parser/JaniParser.h b/src/parser/JaniParser.h index 1e87efe04..df36cd43c 100644 --- a/src/parser/JaniParser.h +++ b/src/parser/JaniParser.h @@ -1,9 +1,11 @@ #pragma once #include <src/storage/jani/Constant.h> -#include <src/logic/Formula.h> +#include "src/logic/Formula.h" +#include "src/logic/Bound.h" #include "src/exceptions/FileIoException.h" #include "src/storage/expressions/ExpressionManager.h" + // JSON parser #include "json.hpp" @@ -16,6 +18,7 @@ namespace storm { class Variable; class Composition; class Property; + class PropertyInterval; } @@ -51,13 +54,13 @@ namespace storm { * Helper for parsing the actions of a model. */ void parseActions(json const& actionStructure, storm::jani::Model& parentModel); - std::shared_ptr<storm::logic::Formula const> parseFormula(json const& propertyStructure, std::string const& context); + std::shared_ptr<storm::logic::Formula const> parseFormula(json const& propertyStructure, std::string const& context, boost::optional<storm::logic::Bound<storm::RationalNumber>> bound = boost::none); std::vector<storm::expressions::Expression> parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}, bool returnNoneOnUnknownOpString = false); std::vector<storm::expressions::Expression> parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}, bool returnNoneOnUnknownOpString = false); std::vector<std::shared_ptr<storm::logic::Formula const>> parseUnaryFormulaArgument(json const& propertyStructure, std::string const& opstring, std::string const& context); std::vector<std::shared_ptr<storm::logic::Formula const>> parseBinaryFormulaArguments(json const& propertyStructure, std::string const& opstring, std::string const& context); - + storm::jani::PropertyInterval parsePropertyInterval(json const& piStructure); std::shared_ptr<storm::jani::Composition> parseComposition(json const& compositionStructure); diff --git a/src/parser/KeyValueParser.cpp b/src/parser/KeyValueParser.cpp new file mode 100644 index 000000000..a9ea96612 --- /dev/null +++ b/src/parser/KeyValueParser.cpp @@ -0,0 +1,26 @@ +#include "KeyValueParser.h" + +namespace storm { + namespace parser { + + std::unordered_map<std::string, std::string> parseKeyValueString(std::string const& keyValueString) { + std::unordered_map<std::string, std::string> keyValueMap; + std::vector<std::string> definitions; + boost::split(definitions, keyValueString, boost::is_any_of(",")); + for (auto& definition : definitions) { + boost::trim(definition); + + // Check whether the token could be a legal constant definition. + std::size_t positionOfAssignmentOperator = definition.find('='); + STORM_LOG_THROW(positionOfAssignmentOperator != std::string::npos, storm::exceptions::InvalidArgumentException, "Illegal key value string: syntax error."); + + // Now extract the variable name and the value from the string. + std::string key = definition.substr(0, positionOfAssignmentOperator); + boost::trim(key); + std::string value = definition.substr(positionOfAssignmentOperator + 1); + boost::trim(value); + keyValueMap.emplace(key, value); + } + } + } +} \ No newline at end of file diff --git a/src/parser/KeyValueParser.h b/src/parser/KeyValueParser.h new file mode 100644 index 000000000..3e32bd3ed --- /dev/null +++ b/src/parser/KeyValueParser.h @@ -0,0 +1,7 @@ +#pragma once + +namespace storm { + namespace parser { + std::unordered_map<std::string, std::string> parseKeyValueString(std::string const& keyValueString); + } +} \ No newline at end of file diff --git a/src/settings/modules/IOSettings.cpp b/src/settings/modules/IOSettings.cpp index c174f1f51..b6cf57dd3 100644 --- a/src/settings/modules/IOSettings.cpp +++ b/src/settings/modules/IOSettings.cpp @@ -7,6 +7,7 @@ #include "src/settings/ArgumentBuilder.h" #include "src/settings/Argument.h" #include "src/exceptions/InvalidSettingsException.h" +#include "src/parser/CSVParser.h" namespace storm { namespace settings { @@ -29,6 +30,8 @@ namespace storm { const std::string IOSettings::constantsOptionShortName = "const"; const std::string IOSettings::prismCompatibilityOptionName = "prismcompat"; const std::string IOSettings::prismCompatibilityOptionShortName = "pc"; + const std::string IOSettings::janiPropertyOptionName = "janiproperty"; + const std::string IOSettings::janiPropertyOptionShortName = "jprop"; IOSettings::IOSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, prismCompatibilityOptionName, false, "Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build()); @@ -57,6 +60,8 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the choice labels.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that this requires the model to be given as an symbolic model (i.e., via --" + prismInputOptionName + " or --" + janiInputOptionName + ").").setShortName(constantsOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, janiPropertyOptionName, false, "Specifies the properties from the jani model (given by --" + janiInputOptionName + ") to be checked.").setShortName(janiPropertyOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of properties to be checked").setDefaultValueString("").build()).build()); } bool IOSettings::isExportDotSet() const { @@ -153,6 +158,15 @@ namespace storm { return this->getOption(constantsOptionName).getArgumentByName("values").getValueAsString(); } + bool IOSettings::isJaniPropertiesSet() const { + return this->getOption(janiPropertyOptionName).getHasOptionBeenSet(); + } + + std::vector<std::string> IOSettings::getJaniProperties() const { + return storm::parser::parseCommaSeperatedValues(this->getOption(janiPropertyOptionName).getArgumentByName("values").getValueAsString()); + } + + bool IOSettings::isPrismCompatibilityEnabled() const { return this->getOption(prismCompatibilityOptionName).getHasOptionBeenSet(); } diff --git a/src/settings/modules/IOSettings.h b/src/settings/modules/IOSettings.h index ae6ce6831..5514af716 100644 --- a/src/settings/modules/IOSettings.h +++ b/src/settings/modules/IOSettings.h @@ -183,6 +183,10 @@ namespace storm { * @return The string that defines the constants of a symbolic model. */ std::string getConstantDefinitionString() const; + + bool isJaniPropertiesSet() const; + + std::vector<std::string> getJaniProperties() const; /*! * Retrieves whether the PRISM compatibility mode was enabled. @@ -215,6 +219,8 @@ namespace storm { static const std::string constantsOptionShortName; static const std::string prismCompatibilityOptionName; static const std::string prismCompatibilityOptionShortName; + static const std::string janiPropertyOptionName; + static const std::string janiPropertyOptionShortName; }; } // namespace modules diff --git a/src/storage/jani/JSONExporter.cpp b/src/storage/jani/JSONExporter.cpp index 2eefbb774..f70a76c62 100644 --- a/src/storage/jani/JSONExporter.cpp +++ b/src/storage/jani/JSONExporter.cpp @@ -105,13 +105,17 @@ namespace storm { modernjson::json numberToJson(storm::RationalNumber rn) { modernjson::json numDecl; - if(carl::isOne(carl::getDenom(rn))) { - numDecl = modernjson::json(carl::toString(carl::getNum(rn))); - } else { - numDecl["op"] = "/"; - numDecl["left"] = carl::toString(carl::getNum(rn)); - numDecl["right"] = carl::toString(carl::getDenom(rn)); - } + numDecl = storm::utility::convertNumber<double>(rn); +// if(carl::isOne(carl::getDenom(rn))) { +// numDecl = modernjson::json(carl::toString(carl::getNum(rn))); +// } else { +// numDecl["op"] = "/"; +// // TODO set json lib to work with arbitrary precision ints. +// assert(carl::toInt<int64_t>(carl::getNum(rn)) == carl::getNum(rn)); +// assert(carl::toInt<int64_t>(carl::getDenom(rn)) == carl::getDenom(rn)); +// numDecl["left"] = carl::toInt<int64_t>(carl::getNum(rn)); +// numDecl["right"] = carl::toInt<int64_t>(carl::getDenom(rn)); +// } return numDecl; } @@ -689,27 +693,27 @@ namespace storm { } - std::string janiFilterTypeString(storm::jani::FilterType const& ft) { + std::string janiFilterTypeString(storm::modelchecker::FilterType const& ft) { switch(ft) { - case storm::jani::FilterType::MIN: + case storm::modelchecker::FilterType::MIN: return "min"; - case storm::jani::FilterType::MAX: + case storm::modelchecker::FilterType::MAX: return "max"; - case storm::jani::FilterType::SUM: + case storm::modelchecker::FilterType::SUM: return "sum"; - case storm::jani::FilterType::AVG: + case storm::modelchecker::FilterType::AVG: return "avg"; - case storm::jani::FilterType::COUNT: + case storm::modelchecker::FilterType::COUNT: return "count"; - case storm::jani::FilterType::EXISTS: + case storm::modelchecker::FilterType::EXISTS: return "∃"; - case storm::jani::FilterType::FORALL: + case storm::modelchecker::FilterType::FORALL: return "∀"; - case storm::jani::FilterType::ARGMIN: + case storm::modelchecker::FilterType::ARGMIN: return "argmin"; - case storm::jani::FilterType::ARGMAX: + case storm::modelchecker::FilterType::ARGMAX: return "argmax"; - case storm::jani::FilterType::VALUES: + case storm::modelchecker::FilterType::VALUES: return "values"; } @@ -717,7 +721,7 @@ namespace storm { modernjson::json convertFilterExpression(storm::jani::FilterExpression const& fe, bool continuousModel) { modernjson::json propDecl; - propDecl["states"] = "initial"; + propDecl["states"]["op"] = "initial"; propDecl["op"] = "filter"; propDecl["fun"] = janiFilterTypeString(fe.getFilterType()); propDecl["values"] = FormulaToJaniJson::translate(*fe.getFormula(), continuousModel); diff --git a/src/storage/jani/JSONExporter.h b/src/storage/jani/JSONExporter.h index 55895364d..2159c26c5 100644 --- a/src/storage/jani/JSONExporter.h +++ b/src/storage/jani/JSONExporter.h @@ -4,9 +4,12 @@ #include "src/storage/expressions/ExpressionVisitor.h" #include "src/logic/FormulaVisitor.h" #include "Model.h" +#include "src/adapters/NumberAdapter.h" // JSON parser #include "json.hpp" -namespace modernjson = nlohmann; +namespace modernjson { + using json = nlohmann::basic_json<std::map, std::vector, std::string, bool, int64_t, uint64_t, double, std::allocator>; +}; namespace storm { namespace jani { diff --git a/src/storage/jani/Property.cpp b/src/storage/jani/Property.cpp index 28981f313..3e4243a3d 100644 --- a/src/storage/jani/Property.cpp +++ b/src/storage/jani/Property.cpp @@ -1,10 +1,23 @@ #include "Property.h" namespace storm { namespace jani { + + + + std::ostream& operator<<(std::ostream& os, FilterExpression const& fe) { + return os << "Obtain " << toString(fe.getFilterType()) << " the 'initial'-states with values described by '" << *fe.getFormula() << "'"; + } + Property::Property(std::string const& name, std::shared_ptr<storm::logic::Formula const> const& formula, std::string const& comment) - : name(name), filterExpression(FilterExpression(formula)), comment(comment) + : name(name), comment(comment), filterExpression(FilterExpression(formula)) { + } + + Property::Property(std::string const& name, FilterExpression const& fe, std::string const& comment) + : name(name), comment(comment), filterExpression(fe) + { + } std::string const& Property::getName() const { @@ -15,6 +28,14 @@ namespace storm { return this->comment; } + FilterExpression const& Property::getFilter() const { + return this->filterExpression; + } + + std::ostream& operator<<(std::ostream& os, Property const& p) { + return os << "(" << p.getName() << ") : " << p.getFilter(); + } + } } \ No newline at end of file diff --git a/src/storage/jani/Property.h b/src/storage/jani/Property.h index be35820a4..95ae41092 100644 --- a/src/storage/jani/Property.h +++ b/src/storage/jani/Property.h @@ -1,33 +1,52 @@ #pragma once #include "src/logic/formulas.h" +#include "src/modelchecker/results/FilterType.h" namespace storm { namespace jani { - enum class FilterType { MIN, MAX, SUM, AVG, COUNT, FORALL, EXISTS, ARGMIN, ARGMAX, VALUES }; - + /** + * Property intervals as per Jani Specification. + * Currently mainly used to help parsing. + */ + struct PropertyInterval { + storm::expressions::Expression lowerBound; + bool lowerBoundStrict = false; + storm::expressions::Expression upperBound; + bool upperBoundStrict = false; + + bool hasLowerBound() { + return lowerBound.isInitialized(); + } + + bool hasUpperBound() { + return upperBound.isInitialized(); + } + }; class FilterExpression { public: - explicit FilterExpression(std::shared_ptr<storm::logic::Formula const> formula) : values(formula) {} + explicit FilterExpression(std::shared_ptr<storm::logic::Formula const> formula, storm::modelchecker::FilterType ft = storm::modelchecker::FilterType::VALUES) : values(formula), ft(ft) {} + std::shared_ptr<storm::logic::Formula const> const& getFormula() const { return values; } - FilterType getFilterType() const { + storm::modelchecker::FilterType getFilterType() const { return ft; } private: // For now, we assume that the states are always the initial states. - std::shared_ptr<storm::logic::Formula const> values; - FilterType ft = FilterType::VALUES; + storm::modelchecker::FilterType ft; }; + std::ostream& operator<<(std::ostream& os, FilterExpression const& fe); + class Property { @@ -39,6 +58,13 @@ namespace storm { * @param comment An optional comment */ Property(std::string const& name, std::shared_ptr<storm::logic::Formula const> const& formula, std::string const& comment = ""); + /** + * Constructs the property + * @param name the name + * @param formula the formula representation + * @param comment An optional comment + */ + Property(std::string const& name, FilterExpression const& fe, std::string const& comment = ""); /** * Get the provided name * @return the name @@ -50,13 +76,15 @@ namespace storm { */ std::string const& getComment() const; - - + FilterExpression const& getFilter() const; private: std::string name; std::string comment; FilterExpression filterExpression; }; + + + std::ostream& operator<<(std::ostream& os, Property const& p); } } diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp index 6d954722a..d2542a2c2 100644 --- a/src/utility/constants.cpp +++ b/src/utility/constants.cpp @@ -5,7 +5,10 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" +#include "src/exceptions/InvalidArgumentException.h" + #include "src/adapters/CarlAdapter.h" +#include "src/utility/macros.h" namespace storm { namespace utility { @@ -143,6 +146,80 @@ namespace storm { return std::fabs(number); } + template<> + storm::RationalFunction minimum(std::vector<storm::RationalFunction> const& values) + { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum for rational functions is not defined"); + } + + template<typename ValueType> + ValueType minimum(std::vector<ValueType> const& values) { + assert(!values.empty()); + ValueType min = values.front(); + for (auto const& vt : values) { + if (vt < min) { + min = vt; + } + } + return min; + } + + template<> + storm::RationalFunction maximum(std::vector<storm::RationalFunction> const& values) + { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Maximum for rational functions is not defined"); + } + + + template<typename ValueType> + ValueType maximum(std::vector<ValueType> const& values) { + assert(!values.empty()); + ValueType max = values.front(); + for (auto const& vt : values) { + if (vt > max) { + max = vt; + } + } + return max; + } + + template<> + storm::RationalFunction minimum(std::map<uint64_t, storm::RationalFunction> const& values) + { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum for rational functions is not defined"); + } + + template< typename K, typename ValueType> + ValueType minimum(std::map<K, ValueType> const& values) { + assert(!values.empty()); + ValueType min = values.begin()->second; + for (auto const& vt : values) { + if (vt.second < min) { + min = vt.second; + } + } + return min; + } + + template<> + storm::RationalFunction maximum(std::map<uint64_t, storm::RationalFunction> const& values) + { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Maximum for rational functions is not defined"); + } + + + template<typename K, typename ValueType> + ValueType maximum(std::map<K, ValueType> const& values) { + assert(!values.empty()); + ValueType max = values.begin()->second; + for (auto const& vt : values) { + if (vt.second > max) { + max = vt.second; + } + } + return max; + } + #ifdef STORM_HAVE_CARL template<> RationalFunction& simplify(RationalFunction& value); @@ -317,6 +394,24 @@ namespace storm { template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>& matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>&& matrixEntry); + + template double minimum(std::vector<double> const&); + template double maximum(std::vector<double> const&); + + template storm::RationalNumber minimum(std::vector<storm::RationalNumber> const&); + template storm::RationalNumber maximum(std::vector<storm::RationalNumber> const&); + + template storm::RationalFunction minimum(std::vector<storm::RationalFunction> const&); + template storm::RationalFunction maximum(std::vector<storm::RationalFunction> const&); + + template double minimum(std::map<uint64_t, double> const&); + template double maximum(std::map<uint64_t, double> const&); + + template storm::RationalNumber minimum(std::map<uint64_t, storm::RationalNumber> const&); + template storm::RationalNumber maximum(std::map<uint64_t, storm::RationalNumber> const&); + + template storm::RationalFunction minimum(std::map<uint64_t, storm::RationalFunction> const&); + template storm::RationalFunction maximum(std::map<uint64_t, storm::RationalFunction> const&); #ifdef STORM_HAVE_CARL // Instantiations for rational number. template bool isOne(storm::RationalNumber const& value); diff --git a/src/utility/constants.h b/src/utility/constants.h index 66edb9f46..04fdf71c1 100644 --- a/src/utility/constants.h +++ b/src/utility/constants.h @@ -11,6 +11,8 @@ #include <limits> #include <cstdint> +#include <vector> +#include <map> namespace storm { @@ -45,6 +47,19 @@ namespace storm { template<typename ValueType> ValueType simplify(ValueType value); + template<typename ValueType> + ValueType minimum(std::vector<ValueType> const& values); + + template<typename ValueType> + ValueType maximum(std::vector<ValueType> const& values); + + template< typename K, typename ValueType> + ValueType minimum(std::map<K, ValueType> const& values); + + template<typename K, typename ValueType> + ValueType maximum(std::map<K, ValueType> const& values); + + template<typename IndexType, typename ValueType> storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry); diff --git a/src/utility/storm.cpp b/src/utility/storm.cpp index 5e1b8104e..700fe049e 100644 --- a/src/utility/storm.cpp +++ b/src/utility/storm.cpp @@ -7,7 +7,16 @@ #include "src/utility/macros.h" #include "src/storage/jani/Property.h" -namespace storm { +namespace storm{ + + std::vector<std::shared_ptr<storm::logic::Formula const>> formulasInProperties(std::vector<storm::jani::Property> const& properties) { + + std::vector<std::shared_ptr<storm::logic::Formula const>> formulas; + for (auto const& prop : properties) { + formulas.push_back(prop.getFilter().getFormula()); + } + return formulas; + } storm::prism::Program parseProgram(std::string const& path) { storm::prism::Program program = storm::parser::PrismParser::parse(path).simplify().simplify(); diff --git a/src/utility/storm.h b/src/utility/storm.h index 336d6e399..c20f0661d 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -100,6 +100,7 @@ namespace storm { return storm::parser::AutoParser<>::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "", choiceLabelingFile ? choiceLabelingFile.get() : "" ); } + std::vector<std::shared_ptr<storm::logic::Formula const>> formulasInProperties(std::vector<storm::jani::Property> const& properties); std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> parseJaniModel(std::string const& path); storm::prism::Program parseProgram(std::string const& path); std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForExplicit(std::string const& inputString); From 0796eea63268b5e46515f667af6cad6680d75c26 Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Mon, 17 Oct 2016 21:09:54 +0900 Subject: [PATCH 19/30] implemented the extended filter functions of JANI for the symbolic/hybrid check results Former-commit-id: 236ae3ea7fb14389837254f581eaa6f7ffbe665c [formerly c2418a22c7f94beda28fd30f25c0901861103745] Former-commit-id: 1a6a0759217b9d9402f139e69bdccbcf0ebbb5ff --- .../results/HybridQuantitativeCheckResult.cpp | 12 ++++++++---- .../results/HybridQuantitativeCheckResult.h | 3 +-- .../results/SymbolicQualitativeCheckResult.cpp | 15 ++++++++------- .../results/SymbolicQualitativeCheckResult.h | 7 +++++-- .../results/SymbolicQuantitativeCheckResult.cpp | 6 +++--- src/storage/expressions/ExpressionVisitor.h | 3 ++- 6 files changed, 27 insertions(+), 19 deletions(-) diff --git a/src/modelchecker/results/HybridQuantitativeCheckResult.cpp b/src/modelchecker/results/HybridQuantitativeCheckResult.cpp index 62fe2c1dd..2aeab204f 100644 --- a/src/modelchecker/results/HybridQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/HybridQuantitativeCheckResult.cpp @@ -57,7 +57,7 @@ namespace storm { template<storm::dd::DdType Type, typename ValueType> bool HybridQuantitativeCheckResult<Type, ValueType>::isResultForAllStates() const { - return true; + return (symbolicStates || explicitStates) == reachableStates; } template<storm::dd::DdType Type, typename ValueType> @@ -169,12 +169,16 @@ namespace storm { template<storm::dd::DdType Type, typename ValueType> ValueType HybridQuantitativeCheckResult<Type, ValueType>::sum() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Sum not implemented for hybrid results"); + ValueType sum = symbolicValues.sumAbstract(symbolicValues.getContainedMetaVariables()).getValue(); + for (auto const& value : explicitValues) { + sum += value; + } + return sum; } template<storm::dd::DdType Type, typename ValueType> ValueType HybridQuantitativeCheckResult<Type, ValueType>::average() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Average not implemented for hybrid results"); + return this->sum() / (symbolicStates || explicitStates).getNonZeroCount(); } template<storm::dd::DdType Type, typename ValueType> @@ -193,4 +197,4 @@ namespace storm { template class HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>; template class HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>; } -} \ No newline at end of file +} diff --git a/src/modelchecker/results/HybridQuantitativeCheckResult.h b/src/modelchecker/results/HybridQuantitativeCheckResult.h index 16a802331..43b1a39a4 100644 --- a/src/modelchecker/results/HybridQuantitativeCheckResult.h +++ b/src/modelchecker/results/HybridQuantitativeCheckResult.h @@ -54,7 +54,6 @@ namespace storm { virtual ValueType average() const override; - virtual void oneMinus() override; private: @@ -79,4 +78,4 @@ namespace storm { } } -#endif /* STORM_MODELCHECKER_HYBRIDQUANTITATIVECHECKRESULT_H_ */ \ No newline at end of file +#endif /* STORM_MODELCHECKER_HYBRIDQUANTITATIVECHECKRESULT_H_ */ diff --git a/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp b/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp index 3468a13c9..da97a38da 100644 --- a/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp +++ b/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp @@ -8,7 +8,7 @@ namespace storm { namespace modelchecker { template <storm::dd::DdType Type> - SymbolicQualitativeCheckResult<Type>::SymbolicQualitativeCheckResult(storm::dd::Bdd<Type> const& reachableStates, storm::dd::Bdd<Type> const& truthValues) : reachableStates(reachableStates), truthValues(truthValues) { + SymbolicQualitativeCheckResult<Type>::SymbolicQualitativeCheckResult(storm::dd::Bdd<Type> const& reachableStates, storm::dd::Bdd<Type> const& truthValues) : reachableStates(reachableStates), states(reachableStates), truthValues(truthValues) { // Intentionally left empty. } @@ -19,7 +19,7 @@ namespace storm { template <storm::dd::DdType Type> bool SymbolicQualitativeCheckResult<Type>::isResultForAllStates() const { - return true; + return reachableStates == states; } template <storm::dd::DdType Type> @@ -48,22 +48,22 @@ namespace storm { template <storm::dd::DdType Type> storm::dd::Bdd<Type> const& SymbolicQualitativeCheckResult<Type>::getTruthValuesVector() const { - return truthValues; + return this->truthValues; } template <storm::dd::DdType Type> bool SymbolicQualitativeCheckResult<Type>::existsTrue() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Exists not implemented for symbolic results"); + return !this->truthValues.isZero(); } template <storm::dd::DdType Type> bool SymbolicQualitativeCheckResult<Type>::forallTrue() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Forall not implemented for symbolic results"); + return this->truthValues == this->states; } template <storm::dd::DdType Type> uint64_t SymbolicQualitativeCheckResult<Type>::count() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Count not implemented for symbolic results"); + return this->truthValues.getNonZeroCount(); } template <storm::dd::DdType Type> @@ -80,9 +80,10 @@ namespace storm { void SymbolicQualitativeCheckResult<Type>::filter(QualitativeCheckResult const& filter) { STORM_LOG_THROW(filter.isSymbolicQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot filter symbolic check result with non-symbolic filter."); this->truthValues &= filter.asSymbolicQualitativeCheckResult<Type>().getTruthValuesVector(); + this->states &= filter.asSymbolicQualitativeCheckResult<Type>().getTruthValuesVector(); } template class SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>; template class SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>; } -} \ No newline at end of file +} diff --git a/src/modelchecker/results/SymbolicQualitativeCheckResult.h b/src/modelchecker/results/SymbolicQualitativeCheckResult.h index 775b8c467..db3ee1ab5 100644 --- a/src/modelchecker/results/SymbolicQualitativeCheckResult.h +++ b/src/modelchecker/results/SymbolicQualitativeCheckResult.h @@ -45,11 +45,14 @@ namespace storm { private: // The set of all reachable states. storm::dd::Bdd<Type> reachableStates; - + + // The set of states for which this check result contains values. + storm::dd::Bdd<Type> states; + // The values of the qualitative check result. storm::dd::Bdd<Type> truthValues; }; } } -#endif /* STORM_MODELCHECKER_SYMBOLICQUALITATIVECHECKRESULT_H_ */ \ No newline at end of file +#endif /* STORM_MODELCHECKER_SYMBOLICQUALITATIVECHECKRESULT_H_ */ diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp index bde1407a4..5bc712d2d 100644 --- a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp @@ -93,12 +93,12 @@ namespace storm { template<storm::dd::DdType Type, typename ValueType> ValueType SymbolicQuantitativeCheckResult<Type, ValueType>::average() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Average not implemented for symbolic results"); + return this->sum() / this->states.getNonZeroCount(); } template<storm::dd::DdType Type, typename ValueType> ValueType SymbolicQuantitativeCheckResult<Type, ValueType>::sum() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Sum not implemented for symbolic results"); + return this->values.sumAbstract(this->values.getContainedMetaVariables()).getValue(); } template<storm::dd::DdType Type, typename ValueType> @@ -111,4 +111,4 @@ namespace storm { template class SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>; template class SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>; } -} \ No newline at end of file +} diff --git a/src/storage/expressions/ExpressionVisitor.h b/src/storage/expressions/ExpressionVisitor.h index cfe2ce9b6..edbdc5d5a 100644 --- a/src/storage/expressions/ExpressionVisitor.h +++ b/src/storage/expressions/ExpressionVisitor.h @@ -2,6 +2,7 @@ #define STORM_STORAGE_EXPRESSIONS_EXPRESSIONVISITOR_H_ #include <boost/any.hpp> +#include <boost/none.hpp> namespace storm { namespace expressions { @@ -33,4 +34,4 @@ namespace storm { } } -#endif /* STORM_STORAGE_EXPRESSIONS_EXPRESSIONVISITOR_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_EXPRESSIONS_EXPRESSIONVISITOR_H_ */ From 9faa7539c52baa6a246b61a1a63ff6f96759b272 Mon Sep 17 00:00:00 2001 From: sjunges <sebastian.junges@rwth-aachen.de> Date: Wed, 19 Oct 2016 13:59:05 +0200 Subject: [PATCH 20/30] parser Former-commit-id: 6e1af26d2f14f19da335e5f9151976f2194daf48 [formerly 995647eeb7dd68d29d858d34c94f7cb1f7da235f] Former-commit-id: 0865990abf09daf1871adb770236d77ba923e839 --- src/parser/JaniParser.cpp | 130 +++++++++++++++++++++++++++--- src/storage/jani/JSONExporter.cpp | 2 + 2 files changed, 120 insertions(+), 12 deletions(-) diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index b6fe64bc6..db1819643 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -184,6 +184,7 @@ namespace storm { } + std::shared_ptr<storm::logic::Formula const> JaniParser::parseFormula(json const& propertyStructure, std::string const& context, boost::optional<storm::logic::Bound<storm::RationalNumber>> bound) { storm::expressions::Expression expr = parseExpression(propertyStructure, "expression in property", {}, true); @@ -205,7 +206,110 @@ namespace storm { assert(bound == boost::none); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Forall and Exists are currently not supported"); } else if (opString == "Emin" || opString == "Emax") { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Emin and Emax are currently not supported"); + std::shared_ptr<storm::logic::Formula const> reach; + if (propertyStructure.count("reach") > 0) { + reach = parseFormula(propertyStructure.at("reach"), "Reach-expression of operator " + opString); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Total reward is currently not supported"); + } + storm::logic::OperatorInformation opInfo; + opInfo.optimalityType = opString == "Emin" ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize; + opInfo.bound = bound; + + STORM_LOG_THROW(propertyStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting reward-expression for operator " << opString << " in " << context); + storm::expressions::Expression rewExpr = parseExpression(propertyStructure.at("exp"), "Reward expression in " + context); + + bool accTime = false; + bool accSteps = false; + if (propertyStructure.count("accumulate") > 0) { + STORM_LOG_THROW(propertyStructure.at("accumulate").is_array(), storm::exceptions::InvalidJaniException, "Accumulate should be an array"); + for(auto const& accEntry : propertyStructure.at("accumulate")) { + if (accEntry == "steps") { + accSteps = true; + } else if (accEntry == "time") { + accTime = true; + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "One may only accumulate either 'steps' or 'time', got " << accEntry.dump() << " in " << context); + } + } + } + STORM_LOG_THROW(!(accTime && accSteps), storm::exceptions::NotSupportedException, "Storm does not allow to accumulate over both time and steps"); + + + if (propertyStructure.count("step-instant") > 0) { + storm::expressions::Expression stepInstantExpr = parseExpression(propertyStructure.at("step-instant"), "Step instant in " + context); + STORM_LOG_THROW(!stepInstantExpr.containsVariables(), storm::exceptions::NotSupportedException, "Storm only allows constant step-instants"); + int64_t stepInstant = stepInstantExpr.evaluateAsInt(); + STORM_LOG_THROW(stepInstant >= 0, storm::exceptions::InvalidJaniException, "Only non-negative step-instants are allowed"); + if(!accTime && !accSteps) { + if (rewExpr.isVariable()) { + std::string rewardName = rewExpr.getVariables().begin()->getName(); + return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::InstantaneousRewardFormula>(static_cast<uint64_t>(stepInstant)), rewardName, opInfo); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Only simple reward expressions are currently supported"); + } + } else { + if (rewExpr.isVariable()) { + std::string rewardName = rewExpr.getVariables().begin()->getName(); + return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::CumulativeRewardFormula>(static_cast<uint64_t>(stepInstant)), rewardName, opInfo); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Only simple reward expressions are currently supported"); + } + } + } else if (propertyStructure.count("time-instant") > 0) { + storm::expressions::Expression timeInstantExpr = parseExpression(propertyStructure.at("time-instant"), "time instant in " + context); + STORM_LOG_THROW(!timeInstantExpr.containsVariables(), storm::exceptions::NotSupportedException, "Storm only allows constant time-instants"); + double timeInstant = timeInstantExpr.evaluateAsDouble(); + STORM_LOG_THROW(timeInstant >= 0, storm::exceptions::InvalidJaniException, "Only non-negative time-instants are allowed"); + if(!accTime && !accSteps) { + if (rewExpr.isVariable()) { + std::string rewardName = rewExpr.getVariables().begin()->getName(); + return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::InstantaneousRewardFormula>(timeInstant), rewardName, opInfo); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Only simple reward expressions are currently supported"); + } + } else { + if (rewExpr.isVariable()) { + std::string rewardName = rewExpr.getVariables().begin()->getName(); + return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::CumulativeRewardFormula>(timeInstant), rewardName, opInfo); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Only simple reward expressions are currently supported"); + } + } + } else if (propertyStructure.count("reward-instants") > 0) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Instant/Cumul. Reward for reward constraints not supported currently."); + } + + STORM_LOG_THROW(accTime || accSteps, storm::exceptions::NotSupportedException, "Storm only allows accumulation if a step- or time-bound is given."); + assert(!accTime && !accSteps); + + if (rewExpr.isVariable()) { + std::string rewardName = rewExpr.getVariables().begin()->getName(); + return std::make_shared<storm::logic::RewardOperatorFormula>(reach, rewardName, opInfo); + } else if (!rewExpr.containsVariables()) { + if(rewExpr.hasIntegerType()) { + if (rewExpr.evaluateAsInt() == 1) { + + return std::make_shared<storm::logic::TimeOperatorFormula>(reach, opInfo); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Expected steps/time only works with constant one."); + } + } else if (rewExpr.hasRationalType()){ + if (rewExpr.evaluateAsDouble() == 1.0) { + + return std::make_shared<storm::logic::TimeOperatorFormula>(reach, opInfo); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Expected steps/time only works with constant one."); + } + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Only numerical reward expressions are allowed"); + } + + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No complex reward expressions are supported at the moment"); + } + + } else if (opString == "Smin" || opString == "Smax") { std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseUnaryFormulaArgument(propertyStructure, opString, ""); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Smin and Smax are currently not supported"); @@ -917,16 +1021,18 @@ namespace storm { std::vector<storm::jani::Assignment> assignments; unsigned assignmentDeclCount = destEntry.count("assignments"); STORM_LOG_THROW(assignmentDeclCount < 2, storm::exceptions::InvalidJaniException, "Destination in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "' has multiple assignment lists"); - for(auto const& assignmentEntry : destEntry.at("assignments")) { - // ref - STORM_LOG_THROW(assignmentEntry.count("ref") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "' must have one ref field"); - std::string refstring = getString(assignmentEntry.at("ref"), "assignment in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'"); - storm::jani::Variable const& lhs = getLValue(refstring, parentModel.getGlobalVariables(), automaton.getVariables(), "Assignment variable in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'"); - // value - STORM_LOG_THROW(assignmentEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "' must have one value field"); - storm::expressions::Expression assignmentExpr = parseExpression(assignmentEntry.at("value"), "assignment in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'", localVars); - // TODO check types - assignments.emplace_back(lhs, assignmentExpr); + if (assignmentDeclCount > 0) { + for (auto const& assignmentEntry : destEntry.at("assignments")) { + // ref + STORM_LOG_THROW(assignmentEntry.count("ref") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "' must have one ref field"); + std::string refstring = getString(assignmentEntry.at("ref"), "assignment in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'"); + storm::jani::Variable const& lhs = getLValue(refstring, parentModel.getGlobalVariables(), automaton.getVariables(), "Assignment variable in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'"); + // value + STORM_LOG_THROW(assignmentEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "' must have one value field"); + storm::expressions::Expression assignmentExpr = parseExpression(assignmentEntry.at("value"), "assignment in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'", localVars); + // TODO check types + assignments.emplace_back(lhs, assignmentExpr); + } } edgeDestinations.emplace_back(locIds.at(targetLoc), probExpr, assignments); } @@ -945,7 +1051,7 @@ namespace storm { std::vector<std::string> inputs; for (auto const& syncInput : syncEntry.at("synchronise")) { if(syncInput.is_null()) { - // TODO handle null; + inputs.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); } else { inputs.push_back(syncInput); } diff --git a/src/storage/jani/JSONExporter.cpp b/src/storage/jani/JSONExporter.cpp index f70a76c62..9bca2d689 100644 --- a/src/storage/jani/JSONExporter.cpp +++ b/src/storage/jani/JSONExporter.cpp @@ -282,6 +282,8 @@ namespace storm { // } // } // return opDecl; + + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support conversion of an LRA reward formula"); } boost::any FormulaToJaniJson::visit(storm::logic::NextFormula const& f, boost::any const& data) const { From 435b3084cb3ce58e18839824ecc9a228f14bff4d Mon Sep 17 00:00:00 2001 From: sjunges <sebastian.junges@rwth-aachen.de> Date: Wed, 19 Oct 2016 19:21:05 +0200 Subject: [PATCH 21/30] Finally, Globally Former-commit-id: fa2ff942debbd67dfe6ef818b29d8ab8f88a706e [formerly 105d3af63147bd53e591b7d0329fbe363c7dc01e] Former-commit-id: 1560f7cfce335ce66278b63a4016b482b66da0b5 --- src/parser/JaniParser.cpp | 27 +++++++++++++++++++++++++-- 1 file changed, 25 insertions(+), 2 deletions(-) diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index db1819643..b328969d9 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -313,9 +313,17 @@ namespace storm { } else if (opString == "Smin" || opString == "Smax") { std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseUnaryFormulaArgument(propertyStructure, opString, ""); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Smin and Smax are currently not supported"); - } else if (opString == "U") { + } else if (opString == "U" || opString == "F") { assert(bound == boost::none); - std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseBinaryFormulaArguments(propertyStructure, opString, ""); + std::vector<std::shared_ptr<storm::logic::Formula const>> args; + if (opString == "U") { + args = parseBinaryFormulaArguments(propertyStructure, opString, ""); + } else { + assert(opString == "F"); + args = parseUnaryFormulaArgument(propertyStructure, opString, ""); + args.push_back(args[0]); + args[0] = storm::logic::BooleanLiteralFormula::getTrueFormula(); + } if (propertyStructure.count("step-bounds") > 0) { storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("step-bounds")); STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports step-bounded until with an upper bound"); @@ -348,9 +356,24 @@ namespace storm { } else { return std::make_shared<storm::logic::UntilFormula const>(args[0], args[1]); } + } else if (opString == "G") { + assert(bound == boost::none); + std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseUnaryFormulaArgument(propertyStructure, opString, "Subformula of globally operator " + context); + if (propertyStructure.count("step-bounds") > 0) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Globally and step-bounds are not supported currently"); + } else if (propertyStructure.count("time-bounds") > 0) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Globally and time bounds are not supported by Storm"); + } else if (propertyStructure.count("reward-bounds") > 0 ) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by Storm"); + } + return std::make_shared<storm::logic::GloballyFormula const>(args[1]); + } else if (opString == "W") { assert(bound == boost::none); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Weak until is not supported"); + } else if (opString == "R") { + assert(bound == boost::none); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Release is not supported"); } else if (opString == "∧" || opString == "∨") { assert(bound == boost::none); std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseBinaryFormulaArguments(propertyStructure, opString, ""); From ecc74595ba40e711af7bedf1f287d3cf881e2e7b Mon Sep 17 00:00:00 2001 From: sjunges <sebastian.junges@rwth-aachen.de> Date: Thu, 20 Oct 2016 01:40:59 +0200 Subject: [PATCH 22/30] several jani related fixes: IsInitialRestrictionSet(), FormulaContext, minor things Former-commit-id: f1a5b2edcf29739de8996cdd42a9456297860bb4 [formerly 6a9cb0a9886a5a2597d83e6fad14add828a08625] Former-commit-id: 11bf234fcc0662135aefef4d2e9eb025b25386b6 --- src/cli/cli.cpp | 4 ++ src/parser/JaniParser.cpp | 59 ++++++++++++++++++----------- src/parser/JaniParser.h | 12 ++++-- src/settings/modules/IOSettings.cpp | 7 +++- src/settings/modules/IOSettings.h | 6 +++ src/storage/jani/Automaton.cpp | 9 ++++- src/storm-pgcl.cpp | 4 +- 7 files changed, 71 insertions(+), 30 deletions(-) diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp index a1b20b546..2d0b467aa 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -258,6 +258,10 @@ namespace storm { } } + if (ioSettings.isNoBuildModelSet()) { + return; + } + // Get the string that assigns values to the unknown currently undefined constants in the model. std::string constantDefinitionString = ioSettings.getConstantDefinitionString(); model = model.preprocess(constantDefinitionString); diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index b328969d9..a149a9e92 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -142,16 +142,16 @@ namespace storm { } - std::vector<std::shared_ptr<storm::logic::Formula const>> JaniParser::parseUnaryFormulaArgument(json const& propertyStructure, std::string const& opstring, std::string const& context) { + std::vector<std::shared_ptr<storm::logic::Formula const>> JaniParser::parseUnaryFormulaArgument(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, std::string const& context) { STORM_LOG_THROW(propertyStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting operand for operator " << opstring << " in " << context); - return { parseFormula(propertyStructure.at("exp"), "Operand of operator " + opstring) }; + return { parseFormula(propertyStructure.at("exp"), formulaContext, "Operand of operator " + opstring) }; } - std::vector<std::shared_ptr<storm::logic::Formula const>> JaniParser::parseBinaryFormulaArguments(json const& propertyStructure, std::string const& opstring, std::string const& context) { + std::vector<std::shared_ptr<storm::logic::Formula const>> JaniParser::parseBinaryFormulaArguments(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, std::string const& context) { STORM_LOG_THROW(propertyStructure.count("left") == 1, storm::exceptions::InvalidJaniException, "Expecting left operand for operator " << opstring << " in " << context); STORM_LOG_THROW(propertyStructure.count("right") == 1, storm::exceptions::InvalidJaniException, "Expecting right operand for operator " << opstring << " in " << context); - return { parseFormula(propertyStructure.at("left"), "Operand of operator " + opstring), parseFormula(propertyStructure.at("right"), "Operand of operator " + opstring) }; + return { parseFormula(propertyStructure.at("left"), formulaContext, "Operand of operator " + opstring), parseFormula(propertyStructure.at("right"), formulaContext, "Operand of operator " + opstring) }; } storm::jani::PropertyInterval JaniParser::parsePropertyInterval(json const& piStructure) { @@ -185,8 +185,15 @@ namespace storm { } - std::shared_ptr<storm::logic::Formula const> JaniParser::parseFormula(json const& propertyStructure, std::string const& context, boost::optional<storm::logic::Bound<storm::RationalNumber>> bound) { - + std::shared_ptr<storm::logic::Formula const> JaniParser::parseFormula(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& context, boost::optional<storm::logic::Bound<storm::RationalNumber>> bound) { + if (propertyStructure.is_boolean()) { + return std::make_shared<storm::logic::BooleanLiteralFormula>(propertyStructure.get<bool>()); + } + if (propertyStructure.is_string()) { + if (labels.count(propertyStructure.get<std::string>()) > 0) { + return std::make_shared<storm::logic::AtomicLabelFormula>(propertyStructure.get<std::string>()); + } + } storm::expressions::Expression expr = parseExpression(propertyStructure, "expression in property", {}, true); if(expr.isInitialized()) { assert(bound == boost::none); @@ -195,7 +202,7 @@ namespace storm { std::string opString = getString(propertyStructure.at("op"), "Operation description"); if(opString == "Pmin" || opString == "Pmax") { - std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseUnaryFormulaArgument(propertyStructure, opString, ""); + std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseUnaryFormulaArgument(propertyStructure, storm::logic::FormulaContext::Probability, opString, ""); assert(args.size() == 1); storm::logic::OperatorInformation opInfo; opInfo.optimalityType = opString == "Pmin" ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize; @@ -206,9 +213,17 @@ namespace storm { assert(bound == boost::none); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Forall and Exists are currently not supported"); } else if (opString == "Emin" || opString == "Emax") { + bool time=false; + STORM_LOG_THROW(propertyStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting reward-expression for operator " << opString << " in " << context); + storm::expressions::Expression rewExpr = parseExpression(propertyStructure.at("exp"), "Reward expression in " + context); + if (rewExpr.isVariable()) { + time = false; + } else { + time = true; + } std::shared_ptr<storm::logic::Formula const> reach; if (propertyStructure.count("reach") > 0) { - reach = parseFormula(propertyStructure.at("reach"), "Reach-expression of operator " + opString); + reach = parseFormula(propertyStructure.at("reach"), time ? storm::logic::FormulaContext::Time : storm::logic::FormulaContext::Reward, "Reach-expression of operator " + opString); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Total reward is currently not supported"); } @@ -216,9 +231,6 @@ namespace storm { opInfo.optimalityType = opString == "Emin" ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize; opInfo.bound = bound; - STORM_LOG_THROW(propertyStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting reward-expression for operator " << opString << " in " << context); - storm::expressions::Expression rewExpr = parseExpression(propertyStructure.at("exp"), "Reward expression in " + context); - bool accTime = false; bool accSteps = false; if (propertyStructure.count("accumulate") > 0) { @@ -280,8 +292,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Instant/Cumul. Reward for reward constraints not supported currently."); } - STORM_LOG_THROW(accTime || accSteps, storm::exceptions::NotSupportedException, "Storm only allows accumulation if a step- or time-bound is given."); - assert(!accTime && !accSteps); + //STORM_LOG_THROW(!accTime && !accSteps, storm::exceptions::NotSupportedException, "Storm only allows accumulation if a step- or time-bound is given."); if (rewExpr.isVariable()) { std::string rewardName = rewExpr.getVariables().begin()->getName(); @@ -311,16 +322,15 @@ namespace storm { } else if (opString == "Smin" || opString == "Smax") { - std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseUnaryFormulaArgument(propertyStructure, opString, ""); STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Smin and Smax are currently not supported"); } else if (opString == "U" || opString == "F") { assert(bound == boost::none); std::vector<std::shared_ptr<storm::logic::Formula const>> args; if (opString == "U") { - args = parseBinaryFormulaArguments(propertyStructure, opString, ""); + args = parseBinaryFormulaArguments(propertyStructure, formulaContext, opString, ""); } else { assert(opString == "F"); - args = parseUnaryFormulaArgument(propertyStructure, opString, ""); + args = parseUnaryFormulaArgument(propertyStructure, formulaContext, opString, ""); args.push_back(args[0]); args[0] = storm::logic::BooleanLiteralFormula::getTrueFormula(); } @@ -352,13 +362,13 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by Storm"); } if (args[0]->isTrueFormula()) { - return std::make_shared<storm::logic::EventuallyFormula const>(args[1]); + return std::make_shared<storm::logic::EventuallyFormula const>(args[1], storm::logic::FormulaContext::Reward); } else { return std::make_shared<storm::logic::UntilFormula const>(args[0], args[1]); } } else if (opString == "G") { assert(bound == boost::none); - std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseUnaryFormulaArgument(propertyStructure, opString, "Subformula of globally operator " + context); + std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseUnaryFormulaArgument(propertyStructure, formulaContext, opString, "Subformula of globally operator " + context); if (propertyStructure.count("step-bounds") > 0) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Globally and step-bounds are not supported currently"); } else if (propertyStructure.count("time-bounds") > 0) { @@ -376,13 +386,13 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Release is not supported"); } else if (opString == "∧" || opString == "∨") { assert(bound == boost::none); - std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseBinaryFormulaArguments(propertyStructure, opString, ""); + std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseBinaryFormulaArguments(propertyStructure, formulaContext, opString, ""); assert(args.size() == 2); storm::logic::BinaryBooleanStateFormula::OperatorType oper = opString == "∧" ? storm::logic::BinaryBooleanStateFormula::OperatorType::And : storm::logic::BinaryBooleanStateFormula::OperatorType::Or; return std::make_shared<storm::logic::BinaryBooleanStateFormula const>(oper, args[0], args[1]); } else if (opString == "¬") { assert(bound == boost::none); - std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseUnaryFormulaArgument(propertyStructure, opString, ""); + std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseUnaryFormulaArgument(propertyStructure, formulaContext, opString, ""); assert(args.size() == 1); return std::make_shared<storm::logic::UnaryBooleanStateFormula const>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, args[0]); @@ -402,12 +412,12 @@ namespace storm { auto expr = parseExpression(propertyStructure.at("right"), "Threshold for operator " + propertyStructure.at("left").at("op").get<std::string>()); STORM_LOG_THROW(expr.getVariables().empty(), storm::exceptions::NotSupportedException, "Only constant thresholds supported"); // TODO evaluate this expression directly as rational number - return parseFormula(propertyStructure.at("left"), "", storm::logic::Bound<storm::RationalNumber>(ct, storm::utility::convertNumber<storm::RationalNumber>(expr.evaluateAsDouble()))); + return parseFormula(propertyStructure.at("left"), formulaContext, "", storm::logic::Bound<storm::RationalNumber>(ct, storm::utility::convertNumber<storm::RationalNumber>(expr.evaluateAsDouble()))); } else if(propertyStructure.at("right").count("op") > 0 && (propertyStructure.at("right").at("op") == "Pmin" || propertyStructure.at("right").at("op") == "Pmax" || propertyStructure.at("right").at("op") == "Emin" || propertyStructure.at("right").at("op") == "Emax" || propertyStructure.at("right").at("op") == "Smin" || propertyStructure.at("right").at("op") == "Smax")) { auto expr = parseExpression(propertyStructure.at("left"), "Threshold for operator " + propertyStructure.at("right").at("op").get<std::string>()); STORM_LOG_THROW(expr.getVariables().empty(), storm::exceptions::NotSupportedException, "Only constant thresholds supported"); // TODO evaluate this expression directly as rational number - return parseFormula(propertyStructure.at("right"), "", storm::logic::Bound<storm::RationalNumber>(ct, storm::utility::convertNumber<storm::RationalNumber>(expr.evaluateAsDouble()))); + return parseFormula(propertyStructure.at("right"),formulaContext, "", storm::logic::Bound<storm::RationalNumber>(ct, storm::utility::convertNumber<storm::RationalNumber>(expr.evaluateAsDouble()))); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No complex comparisons are allowed."); @@ -465,7 +475,7 @@ namespace storm { std::string statesDescr = getString(expressionStructure.at("states").at("op"), "Filtered states in property named " + name); STORM_LOG_THROW(statesDescr == "initial", storm::exceptions::NotImplementedException, "Only initial states are allowed as set of states we are interested in."); STORM_LOG_THROW(expressionStructure.count("values") == 1, storm::exceptions::InvalidJaniException, "Values as input for a filter must be given"); - auto formula = parseFormula(expressionStructure.at("values"), "Values of property " + name); + auto formula = parseFormula(expressionStructure.at("values"), storm::logic::FormulaContext::Undefined, "Values of property " + name); return storm::jani::Property(name, storm::jani::FilterExpression(formula, ft), comment); } @@ -581,6 +591,9 @@ namespace storm { initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") "); STORM_LOG_THROW(initVal.get().hasBooleanType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be a Boolean"); } + if(transientVar) { + labels.insert(name); + } return std::make_shared<storm::jani::BooleanVariable>(name, expressionManager->declareBooleanVariable(exprManagerName), initVal.get(), transientVar); } assert(!transientVar); diff --git a/src/parser/JaniParser.h b/src/parser/JaniParser.h index df36cd43c..438cb93d1 100644 --- a/src/parser/JaniParser.h +++ b/src/parser/JaniParser.h @@ -20,6 +20,10 @@ namespace storm { class Property; class PropertyInterval; } + + namespace logic { + enum class FormulaContext; + } namespace parser { @@ -54,12 +58,12 @@ namespace storm { * Helper for parsing the actions of a model. */ void parseActions(json const& actionStructure, storm::jani::Model& parentModel); - std::shared_ptr<storm::logic::Formula const> parseFormula(json const& propertyStructure, std::string const& context, boost::optional<storm::logic::Bound<storm::RationalNumber>> bound = boost::none); + std::shared_ptr<storm::logic::Formula const> parseFormula(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& context, boost::optional<storm::logic::Bound<storm::RationalNumber>> bound = boost::none); std::vector<storm::expressions::Expression> parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}, bool returnNoneOnUnknownOpString = false); std::vector<storm::expressions::Expression> parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}, bool returnNoneOnUnknownOpString = false); - std::vector<std::shared_ptr<storm::logic::Formula const>> parseUnaryFormulaArgument(json const& propertyStructure, std::string const& opstring, std::string const& context); - std::vector<std::shared_ptr<storm::logic::Formula const>> parseBinaryFormulaArguments(json const& propertyStructure, std::string const& opstring, std::string const& context); + std::vector<std::shared_ptr<storm::logic::Formula const>> parseUnaryFormulaArgument(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, std::string const& context); + std::vector<std::shared_ptr<storm::logic::Formula const>> parseBinaryFormulaArguments(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, std::string const& context); storm::jani::PropertyInterval parsePropertyInterval(json const& piStructure); @@ -75,6 +79,8 @@ namespace storm { * The expression manager to be used. */ std::shared_ptr<storm::expressions::ExpressionManager> expressionManager; + + std::set<std::string> labels = {}; bool allowRecursion = true; diff --git a/src/settings/modules/IOSettings.cpp b/src/settings/modules/IOSettings.cpp index 868237b1a..84d9b1238 100644 --- a/src/settings/modules/IOSettings.cpp +++ b/src/settings/modules/IOSettings.cpp @@ -30,6 +30,7 @@ namespace storm { const std::string IOSettings::constantsOptionShortName = "const"; const std::string IOSettings::prismCompatibilityOptionName = "prismcompat"; const std::string IOSettings::prismCompatibilityOptionShortName = "pc"; + const std::string IOSettings::noBuildOptionName = "nobuild"; const std::string IOSettings::fullModelBuildOptionName = "buildfull"; const std::string IOSettings::janiPropertyOptionName = "janiproperty"; const std::string IOSettings::janiPropertyOptionShortName = "jprop"; @@ -50,7 +51,7 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the JANI input.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, prismToJaniOptionName, false, "If set, the input PRISM model is transformed to JANI.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, fullModelBuildOptionName, false, "If set, include all rewards and labels.").build()); - + this->addOption(storm::settings::OptionBuilder(moduleName, noBuildOptionName, false, "If set, do not build the model.").build()); std::vector<std::string> explorationOrders = {"dfs", "bfs"}; this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName) @@ -186,6 +187,10 @@ namespace storm { bool IOSettings::isBuildFullModelSet() const { return this->getOption(fullModelBuildOptionName).getHasOptionBeenSet(); } + + bool IOSettings::isNoBuildModelSet() const { + return this->getOption(noBuildOptionName).getHasOptionBeenSet(); + } void IOSettings::finalize() { } diff --git a/src/settings/modules/IOSettings.h b/src/settings/modules/IOSettings.h index cedbda8aa..d2c2bef58 100644 --- a/src/settings/modules/IOSettings.h +++ b/src/settings/modules/IOSettings.h @@ -211,6 +211,11 @@ namespace storm { */ bool isPrismCompatibilityEnabled() const; + /** + * Retrieves whether no model should be build at all, in case one just want to translate models or parse a file + */ + bool isNoBuildModelSet() const; + /*! * Retrieves whether the full model should be build, that is, the model including all labels and rewards. * @@ -243,6 +248,7 @@ namespace storm { static const std::string prismCompatibilityOptionName; static const std::string prismCompatibilityOptionShortName; static const std::string fullModelBuildOptionName; + static const std::string noBuildOptionName; static const std::string janiPropertyOptionName; static const std::string janiPropertyOptionShortName; }; diff --git a/src/storage/jani/Automaton.cpp b/src/storage/jani/Automaton.cpp index 8e99f25c1..8ed71acbc 100644 --- a/src/storage/jani/Automaton.cpp +++ b/src/storage/jani/Automaton.cpp @@ -335,7 +335,14 @@ namespace storm { } bool Automaton::hasRestrictedInitialStates() const { - return hasInitialStatesRestriction() && !(getInitialStatesExpression().evaluateAsBool()); + if (!hasInitialStatesRestriction()) { + return false; + } + if (getInitialStatesExpression().containsVariables()) { + return true; + } else { + return !getInitialStatesExpression().evaluateAsBool(); + } } bool Automaton::hasInitialStatesRestriction() const { diff --git a/src/storm-pgcl.cpp b/src/storm-pgcl.cpp index 99ac1c960..a985e3a7b 100644 --- a/src/storm-pgcl.cpp +++ b/src/storm-pgcl.cpp @@ -37,9 +37,9 @@ void initializeSettings() { void handleJani(storm::jani::Model& model) { if (!storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isJaniFileSet()) { // For now, we have to have a jani file - storm::jani::JsonExporter::toStream(model, std::cout); + storm::jani::JsonExporter::toStream(model, {}, std::cout); } else { - storm::jani::JsonExporter::toFile(model, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename()); + storm::jani::JsonExporter::toFile(model, {}, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename()); } } From 489fd4f780db1deba3ed453f2800fe69d4f0e5a8 Mon Sep 17 00:00:00 2001 From: sjunges <sebastian.junges@rwth-aachen.de> Date: Thu, 20 Oct 2016 01:42:00 +0200 Subject: [PATCH 23/30] Die and TwoDie as in the Qapl talk Former-commit-id: 93f21ffea34b8fff4fae4ae6a41c2bb8f67b0ae1 [formerly 88343ceb7b65aeb964dbccc0765eae51faadc683] Former-commit-id: 1595b7eaac1932190e96f023350f97254cc52099 --- examples/pdtmc/die.pm | 35 ++++++++++++++++++++++++++++++++ examples/pdtmc/twodie.pm | 44 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 79 insertions(+) create mode 100644 examples/pdtmc/die.pm create mode 100644 examples/pdtmc/twodie.pm diff --git a/examples/pdtmc/die.pm b/examples/pdtmc/die.pm new file mode 100644 index 000000000..31290bd69 --- /dev/null +++ b/examples/pdtmc/die.pm @@ -0,0 +1,35 @@ +// Knuth's model of a fair die using only fair coins +dtmc + +const double p; +const double q; + +module die + + // local state + s : [0..7] init 0; + // value of the dice + d : [0..6] init 0; + + [] s=0 -> p : (s'=1) + 1-p : (s'=2); + [] s=1 -> q : (s'=3) + 1-q : (s'=4); + [] s=2 -> q : (s'=5) + 1-q : (s'=6); + [] s=3 -> p : (s'=1) + 1-p : (s'=7) & (d'=1); + [] s=4 -> p : (s'=7) & (d'=3) + 1-p : (s'=7) & (d'=2); + [] s=5 -> p : (s'=2) + 1-p : (s'=7) & (d'=6); + [] s=6 -> p : (s'=7) & (d'=6) + 1-p : (s'=7) & (d'=5); + [] s=7 -> 1: (s'=7); + +endmodule + +rewards "coin_flips" + [] s<7 : 1; +endrewards + +label "one" = s=7&d=1; +label "two" = s=7&d=2; +label "three" = s=7&d=3; +label "four" = s=7&d=4; +label "five" = s=7&d=5; +label "six" = s=7&d=6; +label "end" = s=7; diff --git a/examples/pdtmc/twodie.pm b/examples/pdtmc/twodie.pm new file mode 100644 index 000000000..d38f75496 --- /dev/null +++ b/examples/pdtmc/twodie.pm @@ -0,0 +1,44 @@ +// Knuth's model of a fair die using only fair coins +dtmc + +const double p; +const double q; + +module die1 + + // local state + s1 : [0..7] init 0; + // value of the dice + d1 : [0..6] init 0; + + [] s1=0 -> p : (s1'=1) + 1-p : (s1'=2); + [] s1=1 -> q : (s1'=3) + 1-q : (s1'=4); + [] s1=2 -> q : (s1'=5) + 1-q : (s1'=6); + [] s1=3 -> p : (s1'=1) + 1-p : (s1'=7) & (d1'=1); + [] s1=4 -> p : (s1'=7) & (d1'=3) + 1-p : (s1'=7) & (d1'=2); + [] s1=5 -> p : (s1'=2) + 1-p : (s1'=7) & (d1'=4); + [] s1=6 -> p : (s1'=7) & (d1'=6) + 1-p : (s1'=7) & (d1'=5); + [] s1=7 -> 1: (s1'=7); + +endmodule + +module die2 = die1 [ s1=s2, s2=s1, d1=d2 ] endmodule + +rewards "coin_flips" + [] s1<7 | s2<7 : 1; +endrewards + +label "two" = s1=7 & s2=7 & d1+d2=2; +label "three" = s1=7 & s2=7 & d1+d2=3; +label "four" = s1=7 & s2=7 & d1+d2=4; +label "five" = s1=7 & s2=7 & d1+d2=5; +label "six" = s1=7 & s2=7 & d1+d2=6; +label "seven" = s1=7 & s2=7 & d1+d2=7; +label "eight" = s1=7 & s2=7 & d1+d2=8; +label "nine" = s1=7 & s2=7 & d1+d2=9; +label "ten" = s1=7 & s2=7 & d1+d2=10; +label "eleven" = s1=7 & s2=7 & d1+d2=11; +label "twelve" = s1=7 & s2=7 & d1+d2=12; +label "same" = s1=7 & s2=7 & d1=d2; + +label "end" = s1=7 & s2=7; From bd2e7b075c51fa93f182fbbc60d5138a9a494df4 Mon Sep 17 00:00:00 2001 From: sjunges <sebastian.junges@rwth-aachen.de> Date: Thu, 20 Oct 2016 01:42:37 +0200 Subject: [PATCH 24/30] one can never have enough labels in prism files Former-commit-id: ec1751b34a926b41e6635e3d44a97dcdec0d3bd3 [formerly 7f1a1b2944b787698cf7143745438c4911c5ded3] Former-commit-id: af5e22c01e4d3b3b599773265f7c5411b9d15304 --- examples/pctmc/polling6.sm | 16 ++++++++++------ examples/pdtmc/brp/brp.pm | 2 ++ examples/pdtmc/brp_rewards2/brp_rewards2.pm | 3 ++- examples/pdtmc/brp_rewards4/brp_rewards4.pm | 3 +++ examples/pmdp/brp/brp.pm | 3 ++- examples/pmdp/coin2/coin2.pm | 5 ++++- examples/pmdp/coin4/coin4.pm | 3 +++ examples/pmdp/zeroconf/zeroconf.pm | 11 +++++++++++ 8 files changed, 37 insertions(+), 9 deletions(-) diff --git a/examples/pctmc/polling6.sm b/examples/pctmc/polling6.sm index cb4faa90c..686907565 100644 --- a/examples/pctmc/polling6.sm +++ b/examples/pctmc/polling6.sm @@ -63,13 +63,17 @@ module station6 = station1 [s1=s6, loop1a=loop6a, loop1b=loop6b, serve1=serve6] // cumulative rewards -//rewards "waiting" // expected time the station 1 is waiting to be served -// s1=1 & !(s=1 & a=1) : 1; -//endrewards +rewards "waiting" // expected time the station 1 is waiting to be served + s1=1 & !(s=1 & a=1) : 1; +endrewards -//rewards "served" // expected number of times station1 is served -// [serve1] true : 1; -//endrewards +rewards "served" // expected number of times station1 is served + [serve1] true : 1; +endrewards + +label "server1serving" = s=1 & a=1; +label "server5polling" = s=5 & a=0; +label "server5serving" = s=5 & a=1; init s = 1 & diff --git a/examples/pdtmc/brp/brp.pm b/examples/pdtmc/brp/brp.pm index 7a3cb325b..031bfe978 100644 --- a/examples/pdtmc/brp/brp.pm +++ b/examples/pdtmc/brp/brp.pm @@ -134,3 +134,5 @@ module channelL endmodule +label "fatal" = s=5 & T; +label "false_neg" = srep=1 & rrep=3 & recv; diff --git a/examples/pdtmc/brp_rewards2/brp_rewards2.pm b/examples/pdtmc/brp_rewards2/brp_rewards2.pm index b4cc546e1..a8e5eced1 100644 --- a/examples/pdtmc/brp_rewards2/brp_rewards2.pm +++ b/examples/pdtmc/brp_rewards2/brp_rewards2.pm @@ -143,4 +143,5 @@ rewards [TO_Ack] true : TOAck; endrewards - +label "fatal" = s=5 & T; +label "false_neg" = srep=1 & rrep=3 & recv; diff --git a/examples/pdtmc/brp_rewards4/brp_rewards4.pm b/examples/pdtmc/brp_rewards4/brp_rewards4.pm index 5617e839b..223993bc4 100644 --- a/examples/pdtmc/brp_rewards4/brp_rewards4.pm +++ b/examples/pdtmc/brp_rewards4/brp_rewards4.pm @@ -144,3 +144,6 @@ rewards endrewards + +label "fatal" = s=5 & T; +label "false_neg" = srep=1 & rrep=3 & recv; diff --git a/examples/pmdp/brp/brp.pm b/examples/pmdp/brp/brp.pm index a195980bf..0d76e95aa 100644 --- a/examples/pmdp/brp/brp.pm +++ b/examples/pmdp/brp/brp.pm @@ -136,5 +136,6 @@ module channelL endmodule - +label "error" = s=5; label "fatal" = s=5 & T; + diff --git a/examples/pmdp/coin2/coin2.pm b/examples/pmdp/coin2/coin2.pm index 8baa365f4..79a25b870 100644 --- a/examples/pmdp/coin2/coin2.pm +++ b/examples/pmdp/coin2/coin2.pm @@ -47,7 +47,10 @@ endmodule module process2 = process1[pc1=pc2,coin1=coin2,p1=p2] endmodule label "finished" = pc1=3 &pc2=3 ; -label "all_coins_equal_1" = coin1=1 &coin2=1 ; +label "all_coins_equal_0" = coin1=0 & coin2=0; +label "all_coins_equal_1" = coin1=1 & coin2=1; +label "agree" = coin1 = coin2; + rewards "steps" true : 1; endrewards diff --git a/examples/pmdp/coin4/coin4.pm b/examples/pmdp/coin4/coin4.pm index bdb4bd877..d3648919f 100644 --- a/examples/pmdp/coin4/coin4.pm +++ b/examples/pmdp/coin4/coin4.pm @@ -53,6 +53,9 @@ module process4 = process1[pc1=pc4,coin1=coin4,p1=p4] endmodule label "finished" = pc1=3 &pc2=3 &pc3=3 &pc4=3; label "all_coins_equal_1" = coin1=1 &coin2=1 &coin3=1 &coin4=1 ; +label "all_coins_equal_0" = coin1=0 & coin2=0 & coin3 = 0 & coin4 = 0; +label "agree" = coin1=coin2 & coin2=coin3 & coin3 = coin4; + rewards "steps" true : 1; endrewards diff --git a/examples/pmdp/zeroconf/zeroconf.pm b/examples/pmdp/zeroconf/zeroconf.pm index 9c71181f2..682db33d4 100644 --- a/examples/pmdp/zeroconf/zeroconf.pm +++ b/examples/pmdp/zeroconf/zeroconf.pm @@ -256,3 +256,14 @@ module host0 [] l=4 -> 1 : true; endmodule + +// reward structure +const double err; // cost associated with using a IP address already in use + +rewards + [time] true : 1; + [send] l=3 & mess=0 & y=CONSEC & probes=1 & ip=1 : err; +endrewards + +label "selected_ip" = l = 4; +label "selected_ip_in_use" = l = 4 & ip = 1; From 00db8794e6ea2e3c04b6f9430bbf4ef3bfaaa44f Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Sat, 22 Oct 2016 17:11:41 +0900 Subject: [PATCH 25/30] fixed bug in explicit jani model generator Former-commit-id: 445ee6a4ba17d2360d6d7c6b0833e7694e1c02b2 [formerly 702d0fb0de3dfdc024b8f6b50867c22504cbc98e] Former-commit-id: 0fb52d40d49233b78c5498e4c2d2972230f37857 --- src/generator/JaniNextStateGenerator.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index b2c786b77..80473c2f9 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -486,6 +486,8 @@ namespace storm { currentTargetStates = newTargetStates; newTargetStates = new boost::container::flat_map<CompressedState, ValueType>(); } + + ++locationVariableIt; } // At this point, we applied all commands of the current command combination and newTargetStates @@ -541,7 +543,6 @@ namespace storm { // Iterate over all automata. uint64_t automatonIndex = 0; for (auto const& automaton : model.getAutomata()) { - // If the automaton has no edge labeled with the given action, we can skip it. if (!automaton.hasEdgeLabeledWithActionIndex(actionIndex)) { continue; From cb97da887c1539c13c65d1c2654d6742fa75a8c3 Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Mon, 24 Oct 2016 15:20:15 +0200 Subject: [PATCH 26/30] went from deque to vector-based representation of splitter queue in bisimulation Former-commit-id: 70471926416ab789126995475aa6cfab4c17e7e4 --- .../BisimulationDecomposition.cpp | 8 +++--- .../bisimulation/BisimulationDecomposition.h | 4 +-- ...ministicModelBisimulationDecomposition.cpp | 8 +++--- ...erministicModelBisimulationDecomposition.h | 10 +++---- ...ministicModelBisimulationDecomposition.cpp | 26 +++---------------- ...erministicModelBisimulationDecomposition.h | 8 +++--- 6 files changed, 22 insertions(+), 42 deletions(-) diff --git a/src/storage/bisimulation/BisimulationDecomposition.cpp b/src/storage/bisimulation/BisimulationDecomposition.cpp index dbad8c633..bce19fd51 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.cpp +++ b/src/storage/bisimulation/BisimulationDecomposition.cpp @@ -231,7 +231,7 @@ namespace storm { template<typename ModelType, typename BlockDataType> void BisimulationDecomposition<ModelType, BlockDataType>::performPartitionRefinement() { // Insert all blocks into the splitter queue as a (potential) splitter. - std::deque<Block<BlockDataType>*> splitterQueue; + std::vector<Block<BlockDataType>*> splitterQueue; std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (std::unique_ptr<Block<BlockDataType>> const& block) { block->data().setSplitter(); splitterQueue.push_back(block.get()); } ); // Then perform the actual splitting until there are no more splitters. @@ -242,9 +242,9 @@ namespace storm { // Get and prepare the next splitter. // Sort the splitters according to their sizes to prefer small splitters. That is just a heuristic, but // tends to work well. - std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block<BlockDataType> const* b1, Block<BlockDataType> const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates(); } ); - Block<BlockDataType>* splitter = splitterQueue.front(); - splitterQueue.pop_front(); + std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block<BlockDataType> const* b1, Block<BlockDataType> const* b2) { return b1->getNumberOfStates() > b2->getNumberOfStates(); } ); + Block<BlockDataType>* splitter = splitterQueue.back(); + splitterQueue.pop_back(); splitter->data().setSplitter(false); // Now refine the partition using the current splitter. diff --git a/src/storage/bisimulation/BisimulationDecomposition.h b/src/storage/bisimulation/BisimulationDecomposition.h index 6507e3b07..e3322444c 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.h +++ b/src/storage/bisimulation/BisimulationDecomposition.h @@ -1,8 +1,6 @@ #ifndef STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_ #define STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_ -#include <deque> - #include "src/settings/SettingsManager.h" #include "src/settings/modules/BisimulationSettings.h" #include "src/storage/sparse/StateType.h" @@ -224,7 +222,7 @@ namespace storm { * @param splitter The splitter to use. * @param splitterQueue The queue into which to insert the newly discovered potential splitters. */ - virtual void refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) = 0; + virtual void refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue) = 0; /*! * Builds the quotient model based on the previously computed equivalence classes (stored in the blocks diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp index 3f70fd379..66b1a9ec5 100644 --- a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp @@ -157,7 +157,7 @@ namespace storm { } template<typename ModelType> - void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlocksOfSplitterStrong(std::list<Block<BlockDataType>*> const& predecessorBlocks, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) { + void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlocksOfSplitterStrong(std::list<Block<BlockDataType>*> const& predecessorBlocks, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue) { for (auto block : predecessorBlocks) { STORM_LOG_TRACE("Refining predecessor " << block->getId() << " of splitter"); @@ -378,7 +378,7 @@ namespace storm { } template<typename ModelType> - void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlockOfSplitterWeak(bisimulation::Block<BlockDataType>& block, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) { + void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlockOfSplitterWeak(bisimulation::Block<BlockDataType>& block, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue) { // First, we need to turn the one-step probabilities to go to the splitter to the conditional probabilities // for all non-silent states. computeConditionalProbabilitiesForNonSilentStates(block); @@ -416,7 +416,7 @@ namespace storm { } template<typename ModelType> - void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlocksOfSplitterWeak(bisimulation::Block<BlockDataType>& splitter, std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) { + void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlocksOfSplitterWeak(bisimulation::Block<BlockDataType>& splitter, std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue) { for (auto block : predecessorBlocks) { if (*block != splitter) { refinePredecessorBlockOfSplitterWeak(*block, splitterQueue); @@ -439,7 +439,7 @@ namespace storm { } template<typename ModelType> - void DeterministicModelBisimulationDecomposition<ModelType>::refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) { + void DeterministicModelBisimulationDecomposition<ModelType>::refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue) { STORM_LOG_TRACE("Refining partition based on splitter " << splitter.getId()); // The outline of the refinement is as follows. diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h index b9f2a2a5a..b4db574cb 100644 --- a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h +++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h @@ -39,11 +39,11 @@ namespace storm { virtual void buildQuotient() override; - virtual void refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) override; + virtual void refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue) override; private: // Refines the predecessor blocks wrt. strong bisimulation. - void refinePredecessorBlocksOfSplitterStrong(std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue); + void refinePredecessorBlocksOfSplitterStrong(std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue); /*! * Performs the necessary steps to compute a weak bisimulation on a DTMC. @@ -99,10 +99,10 @@ namespace storm { void updateSilentProbabilitiesBasedOnTransitions(bisimulation::Block<BlockDataType>& block); // Refines the predecessor blocks of the splitter wrt. weak bisimulation in DTMCs. - void refinePredecessorBlocksOfSplitterWeak(bisimulation::Block<BlockDataType>& splitter, std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue); + void refinePredecessorBlocksOfSplitterWeak(bisimulation::Block<BlockDataType>& splitter, std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue); // Refines the given block wrt to weak bisimulation in DTMCs. - void refinePredecessorBlockOfSplitterWeak(bisimulation::Block<BlockDataType>& block, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue); + void refinePredecessorBlockOfSplitterWeak(bisimulation::Block<BlockDataType>& block, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue); // Converts the one-step probabilities of going into the splitter into the conditional probabilities needed // for weak bisimulation (on DTMCs). @@ -127,4 +127,4 @@ namespace storm { } } -#endif /* STORM_STORAGE_BISIMULATION_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_BISIMULATION_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */ diff --git a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp index 64a7efe45..6fc317d3f 100644 --- a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp @@ -198,7 +198,7 @@ namespace storm { } template<typename ModelType> - void NondeterministicModelBisimulationDecomposition<ModelType>::updateQuotientDistributionsOfPredecessors(Block<BlockDataType> const& newBlock, Block<BlockDataType> const& oldBlock, std::deque<Block<BlockDataType>*>& splitterQueue) { + void NondeterministicModelBisimulationDecomposition<ModelType>::updateQuotientDistributionsOfPredecessors(Block<BlockDataType> const& newBlock, Block<BlockDataType> const& oldBlock, std::vector<Block<BlockDataType>*>& splitterQueue) { uint_fast64_t lastState = 0; bool lastStateInitialized = false; @@ -332,36 +332,23 @@ namespace storm { } template<typename ModelType> - bool NondeterministicModelBisimulationDecomposition<ModelType>::splitBlockAccordingToCurrentQuotientDistributions(Block<BlockDataType>& block, std::deque<Block<BlockDataType>*>& splitterQueue) { + bool NondeterministicModelBisimulationDecomposition<ModelType>::splitBlockAccordingToCurrentQuotientDistributions(Block<BlockDataType>& block, std::vector<Block<BlockDataType>*>& splitterQueue) { std::list<Block<BlockDataType>*> newBlocks; bool split = this->partition.splitBlock(block, [this] (storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) { bool result = quotientDistributionsLess(state1, state2); -// std::cout << state1 << " is " << (!result ? "not" : "") << " smaller than " << state2 << std::endl; return result; }, [this, &block, &splitterQueue, &newBlocks] (Block<BlockDataType>& newBlock) { newBlocks.push_back(&newBlock); - -// this->checkBlockStable(newBlock); -// this->checkDistributionsDifferent(block, block.getEndIndex()); -// this->checkQuotientDistributions(); }); - // The quotient distributions of the predecessors of block do not need to be updated, since the probability - // will go to the block with the same id as before. - -// std::cout << "partition after split: " << std::endl; -// this->partition.print(); - - // defer updating the quotient distributions until *after* all splits, because + // Defer updating the quotient distributions until *after* all splits, because // it otherwise influences the subsequent splits! for (auto el : newBlocks) { this->updateQuotientDistributionsOfPredecessors(*el, block, splitterQueue); } -// this->checkQuotientDistributions(); - return split; } @@ -369,11 +356,6 @@ namespace storm { bool NondeterministicModelBisimulationDecomposition<ModelType>::quotientDistributionsLess(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) const { STORM_LOG_TRACE("Comparing the quotient distributions of state " << state1 << " and " << state2 << "."); std::vector<uint_fast64_t> nondeterministicChoiceIndices = this->model.getTransitionMatrix().getRowGroupIndices(); - -// std::cout << "distributions of state " << state1 << std::endl; -// this->printDistributions(state1); -// std::cout << "distributions of state " << state2 << std::endl; -// this->printDistributions(state2); auto firstIt = orderedQuotientDistributions.begin() + nondeterministicChoiceIndices[state1]; auto firstIte = orderedQuotientDistributions.begin() + nondeterministicChoiceIndices[state1 + 1]; @@ -405,7 +387,7 @@ namespace storm { } template<typename ModelType> - void NondeterministicModelBisimulationDecomposition<ModelType>::refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) { + void NondeterministicModelBisimulationDecomposition<ModelType>::refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue) { if (!possiblyNeedsRefinement(splitter)) { return; } diff --git a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h index 18a6e8e58..6c25d6cf9 100644 --- a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h +++ b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h @@ -37,7 +37,7 @@ namespace storm { virtual void buildQuotient() override; - virtual void refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) override; + virtual void refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue) override; virtual void initialize() override; @@ -52,7 +52,7 @@ namespace storm { bool possiblyNeedsRefinement(bisimulation::Block<BlockDataType> const& block) const; // Splits the given block according to the current quotient distributions. - bool splitBlockAccordingToCurrentQuotientDistributions(bisimulation::Block<BlockDataType>& block, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue); + bool splitBlockAccordingToCurrentQuotientDistributions(bisimulation::Block<BlockDataType>& block, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue); // Retrieves whether the quotient distributions of state 1 are considered to be less than the ones of state 2. bool quotientDistributionsLess(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) const; @@ -62,7 +62,7 @@ namespace storm { // Updates the quotient distributions of the predecessors of the new block by taking the probability mass // away from the old block. - void updateQuotientDistributionsOfPredecessors(bisimulation::Block<BlockDataType> const& newBlock, bisimulation::Block<BlockDataType> const& oldBlock, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue); + void updateQuotientDistributionsOfPredecessors(bisimulation::Block<BlockDataType> const& newBlock, bisimulation::Block<BlockDataType> const& oldBlock, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue); bool checkQuotientDistributions() const; bool checkBlockStable(bisimulation::Block<BlockDataType> const& newBlock) const; @@ -81,4 +81,4 @@ namespace storm { } } -#endif /* STORM_STORAGE_BISIMULATION_NONDETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_BISIMULATION_NONDETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */ From 17384cd9e953f3143933f3cf2ef107f05b24ae50 Mon Sep 17 00:00:00 2001 From: dehnert <dehnert@cs.rwth-aachen.de> Date: Mon, 24 Oct 2016 16:45:14 +0200 Subject: [PATCH 27/30] fixed wrong include Former-commit-id: 46271a3866ea107c467e3284bc76888028a52ef5 [formerly 86b53e6740d320290b936504b55a3e04dd5b1369] Former-commit-id: 10466b1fdd58e954c822ecd3c9b660383765f5d2 --- src/storage/jani/Property.h | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/storage/jani/Property.h b/src/storage/jani/Property.h index 30f468d77..d4baa9d94 100644 --- a/src/storage/jani/Property.h +++ b/src/storage/jani/Property.h @@ -1,10 +1,8 @@ #pragma once -#include "src/logic/formulas.h" #include "src/modelchecker/results/FilterType.h" #include "src/logic/Formulas.h" - namespace storm { namespace jani { From ce9d7db67a1151357f85338e88e6a767679dff38 Mon Sep 17 00:00:00 2001 From: sjunges <sebastian.junges@rwth-aachen.de> Date: Thu, 27 Oct 2016 13:56:08 +0200 Subject: [PATCH 28/30] fixed knuths die in pdtmc Former-commit-id: f52f34571d095619a2cd12a611507b912a9595b8 [formerly 20c9ef124ae3b2bbceea0e61dcba2f46894fb03e] Former-commit-id: f6d23f46eb12a2cce806d8fe4f5d250f65714025 --- examples/pdtmc/die.pm | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/pdtmc/die.pm b/examples/pdtmc/die.pm index 31290bd69..a2a8f57b0 100644 --- a/examples/pdtmc/die.pm +++ b/examples/pdtmc/die.pm @@ -16,7 +16,7 @@ module die [] s=2 -> q : (s'=5) + 1-q : (s'=6); [] s=3 -> p : (s'=1) + 1-p : (s'=7) & (d'=1); [] s=4 -> p : (s'=7) & (d'=3) + 1-p : (s'=7) & (d'=2); - [] s=5 -> p : (s'=2) + 1-p : (s'=7) & (d'=6); + [] s=5 -> p : (s'=2) + 1-p : (s'=7) & (d'=4); [] s=6 -> p : (s'=7) & (d'=6) + 1-p : (s'=7) & (d'=5); [] s=7 -> 1: (s'=7); From d945cb279df4fa1cb04ea50a3a38c65d3a6c72e9 Mon Sep 17 00:00:00 2001 From: sjunges <sebastian.junges@rwth-aachen.de> Date: Wed, 2 Nov 2016 22:28:41 +0100 Subject: [PATCH 29/30] add derived operators to features, fixed composition export Former-commit-id: 4d57e83fdf4a6496c18723c128c4b569f0f004be [formerly f392ca29257e9f68a9c46ab2f412ed0676362c72] Former-commit-id: 555084f8b0e19850246c4f5c23dde2f8c8f19f67 --- src/storage/jani/JSONExporter.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/storage/jani/JSONExporter.cpp b/src/storage/jani/JSONExporter.cpp index 9bca2d689..7025b21b2 100644 --- a/src/storage/jani/JSONExporter.cpp +++ b/src/storage/jani/JSONExporter.cpp @@ -60,11 +60,7 @@ namespace storm { for (auto const& subcomp : composition.getSubcompositions()) { modernjson::json elemDecl; if (subcomp->isAutomaton()) { - modernjson::json autDecl; - autDecl["automaton"] = std::static_pointer_cast<AutomatonComposition>(subcomp)->getAutomatonName(); - std::vector<modernjson::json> elements; - elements.push_back(autDecl); - elemDecl["elements"] = elements; + elemDecl["automaton"] = std::static_pointer_cast<AutomatonComposition>(subcomp)->getAutomatonName(); } else { STORM_LOG_THROW(allowRecursion, storm::exceptions::InvalidJaniException, "Nesting composition " << *subcomp << " is not supported by JANI."); elemDecl = boost::any_cast<modernjson::json>(subcomp->accept(*this, boost::none)); @@ -691,10 +687,14 @@ namespace storm { jsonStruct["restrict-initial"]["exp"] = buildExpression(janiModel.getInitialStatesRestriction()); jsonStruct["automata"] = buildAutomataArray(janiModel.getAutomata(), janiModel.getActionIndexToNameMap()); jsonStruct["system"] = CompositionJsonExporter::translate(janiModel.getSystemComposition()); + std::vector<std::string> standardFeatureVector = {"derived-operators"}; + jsonStruct["features"] = standardFeatureVector; } + + std::string janiFilterTypeString(storm::modelchecker::FilterType const& ft) { switch(ft) { case storm::modelchecker::FilterType::MIN: From e0fd50cb9dc162ffece040092ce7a963c6f6898e Mon Sep 17 00:00:00 2001 From: sjunges <sebastian.junges@rwth-aachen.de> Date: Thu, 3 Nov 2016 11:42:32 +0100 Subject: [PATCH 30/30] Fixed export of sync input for no-action Former-commit-id: 7124276a8642c1f95c596afd69057ac0d668ba91 [formerly 1e63ff5245ec13fba0a78f4755eda9d053c3434f] Former-commit-id: 05f1f33c492935c4852d3882f5852887aaa2a8e7 --- src/storage/jani/JSONExporter.cpp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/storage/jani/JSONExporter.cpp b/src/storage/jani/JSONExporter.cpp index 7025b21b2..13512f554 100644 --- a/src/storage/jani/JSONExporter.cpp +++ b/src/storage/jani/JSONExporter.cpp @@ -71,7 +71,14 @@ namespace storm { std::vector<modernjson::json> synElems; for (auto const& syncs : composition.getSynchronizationVectors()) { modernjson::json syncDecl; - syncDecl["synchronise"] = syncs.getInput(); + syncDecl["synchronise"] = std::vector<std::string>(); + for (auto const& syncIn : syncs.getInput()) { + if (syncIn == SynchronizationVector::NO_ACTION_INPUT) { + syncDecl["synchronise"].push_back(nullptr); + } else { + syncDecl["synchronise"].push_back(syncIn); + } + } syncDecl["result"] = syncs.getOutput(); synElems.push_back(syncDecl); }