From b53a255365f7e829a22c007329cd03b7ef173de9 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Fri, 6 Aug 2021 15:52:25 +0200 Subject: [PATCH] adapted property ctors with ShieldingExpression param --- src/storm-gspn/builder/JaniGSPNBuilder.cpp | 10 +++++----- src/storm-pars-cli/storm-pars.cpp | 14 +++++++------- 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.cpp b/src/storm-gspn/builder/JaniGSPNBuilder.cpp index cf9496495..3c66576cf 100644 --- a/src/storm-gspn/builder/JaniGSPNBuilder.cpp +++ b/src/storm-gspn/builder/JaniGSPNBuilder.cpp @@ -139,7 +139,7 @@ namespace storm { continue; } storm::expressions::Expression guard = expressionManager->boolean(true); - + std::vector assignments; for (auto const& inPlaceEntry : trans.getInputPlaces()) { guard = guard && (vars[inPlaceEntry.first]->getExpressionVariable() >= inPlaceEntry.second); @@ -160,7 +160,7 @@ namespace storm { std::shared_ptr templateEdge = std::make_shared(guard); automaton.registerTemplateEdge(templateEdge); - + storm::expressions::Expression rate = expressionManager->rational(trans.getRate()); if (trans.hasInfiniteServerSemantics() || (trans.hasKServerSemantics() && !trans.hasSingleServerSemantics())) { STORM_LOG_THROW(trans.hasKServerSemantics() || !trans.getInputPlaces().empty(), storm::exceptions::InvalidModelException, "Unclear semantics: Found a transition with infinite-server semantics and without input place."); @@ -281,7 +281,7 @@ namespace storm { auto reachFormula = std::make_shared( std::make_shared(atomicFormula, storm::logic::FormulaContext::Probability), storm::logic::OperatorInformation(optimizationDirection)); - standardProperties.emplace_back(dirShort + "PrReach" + name, reachFormula, emptySet, "The " + dirLong + " probability to eventually reach " + description + "."); + standardProperties.emplace_back(dirShort + "PrReach" + name, reachFormula, emptySet, nullptr, "The " + dirLong + " probability to eventually reach " + description + "."); // Build time bounded reachability property // Add variable for time bound @@ -295,7 +295,7 @@ namespace storm { auto reachTimeBoundFormula = std::make_shared( std::make_shared(trueFormula, atomicFormula, boost::none, tb, tbr), storm::logic::OperatorInformation(optimizationDirection)); - standardProperties.emplace_back(dirShort + "PrReach" + name + "TB", reachTimeBoundFormula, emptySet, "The " + dirLong + " probability to reach " + description + " within 'TIME_BOUND' steps."); + standardProperties.emplace_back(dirShort + "PrReach" + name + "TB", reachTimeBoundFormula, emptySet, nullptr, "The " + dirLong + " probability to reach " + description + " within 'TIME_BOUND' steps."); // Use complementary direction for expected time dirShort = maximal ? "Min" : "Max"; @@ -306,7 +306,7 @@ namespace storm { auto expTimeFormula = std::make_shared( std::make_shared(atomicFormula, storm::logic::FormulaContext::Time), storm::logic::OperatorInformation(optimizationDirection)); - standardProperties.emplace_back(dirShort + "ExpTime" + name, expTimeFormula, emptySet, "The " + dirLong + " expected time to reach " + description + "."); + standardProperties.emplace_back(dirShort + "ExpTime" + name, expTimeFormula, emptySet, nullptr, "The " + dirLong + " expected time to reach " + description + "."); return standardProperties; } diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp index 837ed4304..edc0c4507 100644 --- a/src/storm-pars-cli/storm-pars.cpp +++ b/src/storm-pars-cli/storm-pars.cpp @@ -280,7 +280,7 @@ namespace storm { result.model = storm::pars::simplifyModel(result.model, input); result.changed = true; } - + if (result.model->isOfType(storm::models::ModelType::MarkovAutomaton)) { result.model = storm::cli::preprocessSparseMarkovAutomaton(result.model->template as>()); result.changed = true; @@ -302,7 +302,7 @@ namespace storm { result.formulas = eliminationResult.second; result.changed = true; } - + if (parametricSettings.transformContinuousModel() && (model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::MarkovAutomaton))) { auto transformResult = storm::api::transformContinuousToDiscreteTimeSparseModel(std::move(*model->template as>()), storm::api::extractFormulasFromProperties(input.properties)); result.model = transformResult.first; @@ -322,7 +322,7 @@ namespace storm { template PreprocessResult preprocessDdModel(std::shared_ptr> const& model, SymbolicInput const& input, storm::cli::ModelProcessingInformation const& mpi) { auto bisimulationSettings = storm::settings::getModule(); - + PreprocessResult result(model, false); if (mpi.engine == storm::utility::Engine::Hybrid) { @@ -668,7 +668,7 @@ namespace storm { } } } - + template void verifyRegionsWithSparseEngine(std::shared_ptr> const& model, SymbolicInput const& input, std::vector> const& regions, storm::api::MonotonicitySetting monotonicitySettings = storm::api::MonotonicitySetting(), uint64_t monThresh = 0) { STORM_LOG_ASSERT(!regions.empty(), "Can not analyze an empty set of regions."); @@ -822,7 +822,7 @@ namespace storm { auto formula = preprocessingResult.formulas.get().at(i); STORM_LOG_ASSERT(i < input.properties.size(), "Index " << i << " greater than number of properties."); storm::jani::Property property = input.properties.at(i); - newProperties.push_back(storm::jani::Property(property.getName(), formula, property.getUndefinedConstants(), property.getComment())); + newProperties.push_back(storm::jani::Property(property.getName(), formula, property.getUndefinedConstants(), nullptr, property.getComment())); } input.properties = newProperties; } @@ -870,11 +870,11 @@ namespace storm { void processOptions() { // Start by setting some urgent options (log levels, resources, etc.) storm::cli::setUrgentOptions(); - + auto coreSettings = storm::settings::getModule(); auto engine = coreSettings.getEngine(); STORM_LOG_WARN_COND(engine != storm::utility::Engine::Dd || engine != storm::utility::Engine::Hybrid || coreSettings.getDdLibraryType() == storm::dd::DdType::Sylvan, "The selected DD library does not support parametric models. Switching to Sylvan..."); - + // Parse and preprocess symbolic input (PRISM, JANI, properties, etc.) auto symbolicInput = storm::cli::parseSymbolicInput(); storm::cli::ModelProcessingInformation mpi;