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(); if (ioSettings.isPrismOrJaniInputSet()) { storm::storage::SymbolicModelDescription model; + std::vector 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> formulas; + uint64_t i = 0; if (storm::settings::getModule().isPropertySet()) { if (model.isJaniModel()) { - formulas = storm::parseFormulasForJaniModel(storm::settings::getModule().getProperty(), model.asJaniModel()); + for(auto const& formula : storm::parseFormulasForJaniModel(storm::settings::getModule().getProperty(), model.asJaniModel())) { + properties.emplace_back(std::to_string(i), formula); + ++i; + } } else { - formulas = storm::parseFormulasForPrismProgram(storm::settings::getModule().getProperty(), model.asPrismProgram()); + for(auto const& formula :storm::parseFormulasForPrismProgram(storm::settings::getModule().getProperty(), model.asPrismProgram())) { + properties.emplace_back(std::to_string(i), formula); + ++i; + } } } @@ -236,9 +252,9 @@ namespace storm { if (storm::settings::getModule().isExportAsStandardJaniSet()) { storm::jani::Model normalisedModel = storm::jani::Model(model.asJaniModel()); normalisedModel.makeStandardJaniCompliant(); - storm::jani::JsonExporter::toFile(normalisedModel, formulas, storm::settings::getModule().getJaniFilename()); + storm::jani::JsonExporter::toFile(normalisedModel, formulasInProperties(properties), storm::settings::getModule().getJaniFilename()); } else { - storm::jani::JsonExporter::toFile(model.asJaniModel(), formulas, storm::settings::getModule().getJaniFilename()); + storm::jani::JsonExporter::toFile(model.asJaniModel(), formulasInProperties(properties), storm::settings::getModule().getJaniFilename()); } } @@ -250,30 +266,35 @@ namespace storm { if (storm::settings::getModule().isParametricSet()) { #ifdef STORM_HAVE_CARL - buildAndCheckSymbolicModel(model, formulas, true); + buildAndCheckSymbolicModel(model, properties, true); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No parameters are supported in this build."); #endif } else if (storm::settings::getModule().isExactSet()) { #ifdef STORM_HAVE_CARL - buildAndCheckSymbolicModel(model, formulas, true); + buildAndCheckSymbolicModel(model, properties, true); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No exact numbers are supported in this build."); #endif } else { - buildAndCheckSymbolicModel(model, formulas, true); + buildAndCheckSymbolicModel(model, properties, true); } } else if (storm::settings::getModule().isExplicitSet()) { STORM_LOG_THROW(storm::settings::getModule().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> formulas; + std::vector properties; if (storm::settings::getModule().isPropertySet()) { - formulas = storm::parseFormulasForExplicit(storm::settings::getModule().getProperty()); + uint64_t i = 0; + for(auto const& formula : storm::parseFormulasForExplicit(storm::settings::getModule().getProperty())) { + properties.emplace_back(std::to_string(i), formula); + ++i; + + } } - buildAndCheckExplicitModel(formulas, true); + buildAndCheckExplicitModel(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 - void verifySparseModel(std::shared_ptr> model, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { - for (auto const& formula : formulas) { - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr result(storm::verifySparseModel(model, formula, onlyInitialStatesRelevant)); + void applyFilterFunctionAndOutput(std::unique_ptr 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().sum(); + return; + case storm::modelchecker::FilterType::AVG: + std::cout << result->asQuantitativeCheckResult().average(); + return; + case storm::modelchecker::FilterType::MIN: + std::cout << result->asQuantitativeCheckResult().getMin(); + return; + case storm::modelchecker::FilterType::MAX: + std::cout << result->asQuantitativeCheckResult().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 + void verifySparseModel(std::shared_ptr> model, std::vector const& properties, bool onlyInitialStatesRelevant = false) { + for (auto const& property : properties) { + std::cout << std::endl << "Model checking property: " << property << " ..."; + std::unique_ptr 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(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> model, std::vector> const& formulas, bool onlyInitialStatesRelevant) { + inline void verifySparseModel(std::shared_ptr> model, std::vector 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 result(storm::verifySparseModel(model, formula, onlyInitialStatesRelevant)); + std::cout << std::endl << "Model checking property: " << property << " ..."; + std::unique_ptr 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(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 - void verifySymbolicModelWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { + void verifySymbolicModelWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, std::vector const& formulas, bool onlyInitialStatesRelevant = false) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Abstraction Refinement is not yet implemented."); } template - void verifySymbolicModelWithExplorationEngine(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { + void verifySymbolicModelWithExplorationEngine(storm::storage::SymbolicModelDescription const& model, std::vector 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 result; if(program.getModelType() == storm::prism::Program::ModelType::DTMC) { storm::modelchecker::SparseExplorationModelChecker> checker(program); - storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); + storm::modelchecker::CheckTask 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> checker(program); - storm::modelchecker::CheckTask task(*formula, onlyInitialStatesRelevant); + storm::modelchecker::CheckTask 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(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::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool onlyInitialStatesRelevant) { + void verifySymbolicModelWithExplorationEngine(storm::storage::SymbolicModelDescription const& model, std::vector const& formulas, bool onlyInitialStatesRelevant) { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Exploration-based verification does currently not support parametric models."); } #endif template - void verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { - for (auto const& formula : formulas) { - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr result(storm::verifySymbolicModelWithHybridEngine(model, formula, onlyInitialStatesRelevant)); + void verifySymbolicModelWithHybridEngine(std::shared_ptr> model, std::vector const& formulas, bool onlyInitialStatesRelevant = false) { + for (auto const& property : formulas) { + std::cout << std::endl << "Model checking property: " << property << " ..."; + std::unique_ptr 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(model->getReachableStates(), model->getInitialStates())); - std::cout << *result << std::endl; + applyFilterFunctionAndOutput(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 - void verifySymbolicModelWithDdEngine(std::shared_ptr> model, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { - for (auto const& formula : formulas) { - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr result(storm::verifySymbolicModelWithDdEngine(model, formula, onlyInitialStatesRelevant)); + void verifySymbolicModelWithDdEngine(std::shared_ptr> model, std::vector const& formulas, bool onlyInitialStatesRelevant = false) { + for (auto const& property : formulas) { + std::cout << std::endl << "Model checking property: " << property << " ..."; + std::unique_ptr 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(model->getReachableStates(), model->getInitialStates())); - std::cout << *result << std::endl; + applyFilterFunctionAndOutput(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 - void buildAndCheckSymbolicModelWithSymbolicEngine(bool hybrid, storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { + void buildAndCheckSymbolicModelWithSymbolicEngine(bool hybrid, storm::storage::SymbolicModelDescription const& model, std::vector const& properties, bool onlyInitialStatesRelevant = false) { // Start by building the model. - auto markovModel = buildSymbolicModel(model, formulas); + auto markovModel = buildSymbolicModel(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 - void buildAndCheckSymbolicModelWithSparseEngine(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { + void buildAndCheckSymbolicModelWithSparseEngine(storm::storage::SymbolicModelDescription const& model, std::vector const& properties, bool onlyInitialStatesRelevant = false) { + auto formulas = formulasInProperties(properties); // Start by building the model. std::shared_ptr markovModel = buildSparseModel(model, formulas); @@ -214,12 +276,12 @@ namespace storm { if (storm::settings::getModule().isCounterexampleSet()) { generateCounterexamples(model, sparseModel, formulas); } else { - verifySparseModel(sparseModel, formulas, onlyInitialStatesRelevant); + verifySparseModel(sparseModel, properties, onlyInitialStatesRelevant); } } template - void buildAndCheckSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { + void buildAndCheckSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector const& formulas, bool onlyInitialStatesRelevant = false) { if (storm::settings::getModule().getEngine() == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement) { auto ddlib = storm::settings::getModule().getDdLibraryType(); if (ddlib == storm::dd::DdType::CUDD) { @@ -247,35 +309,35 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - void buildAndCheckSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool onlyInitialStatesRelevant) { + void buildAndCheckSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector const& formulas, bool onlyInitialStatesRelevant) { STORM_LOG_THROW(storm::settings::getModule().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use this data type with an engine different than the sparse one."); buildAndCheckSymbolicModelWithSparseEngine(model, formulas, onlyInitialStatesRelevant); } template<> - void buildAndCheckSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas, bool onlyInitialStatesRelevant) { + void buildAndCheckSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector const& formulas, bool onlyInitialStatesRelevant) { STORM_LOG_THROW(storm::settings::getModule().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use this data type with an engine different than the sparse one."); buildAndCheckSymbolicModelWithSparseEngine(model, formulas, onlyInitialStatesRelevant); } #endif template - void buildAndCheckExplicitModel(std::vector> const& formulas, bool onlyInitialStatesRelevant = false) { + void buildAndCheckExplicitModel(std::vector const& properties, bool onlyInitialStatesRelevant = false) { storm::settings::modules::IOSettings const& settings = storm::settings::getModule(); STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files."); std::shared_ptr model = buildExplicitModel(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? boost::optional(settings.getStateRewardsFilename()) : boost::none, settings.isTransitionRewardsSet() ? boost::optional(settings.getTransitionRewardsFilename()) : boost::none, settings.isChoiceLabelingSet() ? boost::optional(settings.getChoiceLabelingFilename()) : boost::none); // 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(model->as>(), formulas, onlyInitialStatesRelevant); + verifySparseModel(model->as>(), 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(truthValues).empty(); + } else { + for (auto& element : boost::get(truthValues)) { + if(element.second) { + return true; + } + } + return false; + } + } + bool ExplicitQualitativeCheckResult::forallTrue() const { + if (this->isResultForAllStates()) { + return boost::get(truthValues).full(); + } else { + for (auto& element : boost::get(truthValues)) { + if(!element.second) { + return false; + } + } + return true; + } + } + + uint64_t ExplicitQualitativeCheckResult::count() const { + if (this->isResultForAllStates()) { + return boost::get(truthValues).getNumberOfSetBits(); + } else { + uint64_t result = 0; + for (auto& element : boost::get(truthValues)) { + if(element.second) { + ++result; + } + } + return result; + } + } + + bool ExplicitQualitativeCheckResult::operator[](storm::storage::sparse::state_type state) const { if (this->isResultForAllStates()) { return boost::get(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 + ValueType ExplicitQuantitativeCheckResult::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(values)); + } else { + return storm::utility::minimum(boost::get(values)); + } + } + + + template + ValueType ExplicitQuantitativeCheckResult::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(values)); + } else { + return storm::utility::maximum(boost::get(values)); + } + } + + template + ValueType ExplicitQuantitativeCheckResult::sum() const { + STORM_LOG_THROW(!values.empty(),storm::exceptions::InvalidOperationException, "Minimum of empty set is not defined"); + + ValueType sum = storm::utility::zero(); + if (this->isResultForAllStates()) { + for (auto& element : boost::get(values)) { + sum += element; + } + } else { + for (auto& element : boost::get(values)) { + sum += element.second; + } + } + return sum; + } + + template + ValueType ExplicitQuantitativeCheckResult::average() const { + STORM_LOG_THROW(!values.empty(),storm::exceptions::InvalidOperationException, "Minimum of empty set is not defined"); + + ValueType sum = storm::utility::zero(); + if (this->isResultForAllStates()) { + for (auto& element : boost::get(values)) { + sum += element; + } + return sum / boost::get(values).size(); + } else { + for (auto& element : boost::get(values)) { + sum += element.second; + } + return sum / boost::get(values).size(); + } + } + template bool ExplicitQuantitativeCheckResult::hasScheduler() const { return static_cast(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&& 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 + +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 @@ -164,6 +167,16 @@ namespace storm { return max; } + template + ValueType HybridQuantitativeCheckResult::sum() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Sum not implemented for hybrid results"); + } + + template + ValueType HybridQuantitativeCheckResult::average() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Average not implemented for hybrid results"); + } + template void HybridQuantitativeCheckResult::oneMinus() { storm::dd::Add one = symbolicValues.getDdManager().template getAddOne(); @@ -175,6 +188,7 @@ namespace storm { } } + // Explicitly instantiate the class. template class HybridQuantitativeCheckResult; template class HybridQuantitativeCheckResult; 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 @@ -49,6 +51,21 @@ namespace storm { return truthValues; } + template + bool SymbolicQualitativeCheckResult::existsTrue() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Exists not implemented for symbolic results"); + } + + template + bool SymbolicQualitativeCheckResult::forallTrue() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Forall not implemented for symbolic results"); + } + + template + uint64_t SymbolicQualitativeCheckResult::count() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Count not implemented for symbolic results"); + } + template std::ostream& SymbolicQualitativeCheckResult::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 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 + ValueType SymbolicQuantitativeCheckResult::average() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Average not implemented for symbolic results"); + } + + template + ValueType SymbolicQuantitativeCheckResult::sum() const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Sum not implemented for symbolic results"); + } + template void SymbolicQuantitativeCheckResult::oneMinus() { storm::dd::Add one = values.getDdManager().template getAddOne(); 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 + +#include +#include "src/utility/macros.h" +#include "src/exceptions/InvalidArgumentException.h" + + +namespace storm { + namespace parser { + + std::vector parseCommaSeperatedValues(std::string const& input) { + std::vector values; + std::vector 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 +#include + +namespace storm { + namespace parser { + /** + * Given a string seperated by commas, returns the values. + */ + std::vector 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 #include @@ -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 JaniParser::parseFormula(json const& propertyStructure, std::string const& context) { - storm::expressions::Expression expr = parseExpression(propertyStructure, "Expression in property", {}, true); + std::shared_ptr JaniParser::parseFormula(json const& propertyStructure, std::string const& context, boost::optional> bound) { + + storm::expressions::Expression expr = parseExpression(propertyStructure, "expression in property", {}, true); if(expr.isInitialized()) { + assert(bound == boost::none); return std::make_shared(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(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> 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> 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(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(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(args[0], args[1]); + if (args[0]->isTrueFormula()) { + return std::make_shared(args[1]); + } else { + return std::make_shared(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> 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(oper, args[0], args[1]); } else if (opString == "¬") { + assert(bound == boost::none); std::vector> args = parseUnaryFormulaArgument(propertyStructure, opString, ""); assert(args.size() == 1); return std::make_shared(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()); + 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(ct, storm::utility::convertNumber(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()); + 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(ct, storm::utility::convertNumber(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 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 -#include +#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 parseFormula(json const& propertyStructure, std::string const& context); + std::shared_ptr parseFormula(json const& propertyStructure, std::string const& context, boost::optional> bound = boost::none); std::vector parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars = {}, bool returnNoneOnUnknownOpString = false); std::vector parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars = {}, bool returnNoneOnUnknownOpString = false); std::vector> parseUnaryFormulaArgument(json const& propertyStructure, std::string const& opstring, std::string const& context); std::vector> parseBinaryFormulaArguments(json const& propertyStructure, std::string const& opstring, std::string const& context); - + storm::jani::PropertyInterval parsePropertyInterval(json const& piStructure); std::shared_ptr 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 parseKeyValueString(std::string const& keyValueString) { + std::unordered_map keyValueMap; + std::vector 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 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 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 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(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(carl::getNum(rn)) == carl::getNum(rn)); +// assert(carl::toInt(carl::getDenom(rn)) == carl::getDenom(rn)); +// numDecl["left"] = carl::toInt(carl::getNum(rn)); +// numDecl["right"] = carl::toInt(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; +}; 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 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 formula) : values(formula) {} + explicit FilterExpression(std::shared_ptr formula, storm::modelchecker::FilterType ft = storm::modelchecker::FilterType::VALUES) : values(formula), ft(ft) {} + std::shared_ptr 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 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 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 const& values) + { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum for rational functions is not defined"); + } + + template + ValueType minimum(std::vector 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 const& values) + { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Maximum for rational functions is not defined"); + } + + + template + ValueType maximum(std::vector 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 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 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 const& values) + { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Maximum for rational functions is not defined"); + } + + + template + ValueType maximum(std::map 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& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); + + template double minimum(std::vector const&); + template double maximum(std::vector const&); + + template storm::RationalNumber minimum(std::vector const&); + template storm::RationalNumber maximum(std::vector const&); + + template storm::RationalFunction minimum(std::vector const&); + template storm::RationalFunction maximum(std::vector const&); + + template double minimum(std::map const&); + template double maximum(std::map const&); + + template storm::RationalNumber minimum(std::map const&); + template storm::RationalNumber maximum(std::map const&); + + template storm::RationalFunction minimum(std::map const&); + template storm::RationalFunction maximum(std::map 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 #include +#include +#include namespace storm { @@ -45,6 +47,19 @@ namespace storm { template ValueType simplify(ValueType value); + template + ValueType minimum(std::vector const& values); + + template + ValueType maximum(std::vector const& values); + + template< typename K, typename ValueType> + ValueType minimum(std::map const& values); + + template + ValueType maximum(std::map const& values); + + template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& 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> formulasInProperties(std::vector const& properties) { + + std::vector> 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> formulasInProperties(std::vector const& properties); std::pair> parseJaniModel(std::string const& path); storm::prism::Program parseProgram(std::string const& path); std::vector> parseFormulasForExplicit(std::string const& inputString);