sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Merge pull request 'Adapt Property Ctors with ShieldingExpression Parameter' (#44) from storm_prs_and_updates into main 

Reviewed-on: https://git.pranger.xyz/TEMPEST/tempest-devel/pulls/44
tempestpy_adaptions
Stefan Pranger 3 years ago
parent
d3e313dcb4 b53a255365
commit
f4fb0188be
2 changed files with 12 additions and 12 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 10
      src/storm-gspn/builder/JaniGSPNBuilder.cpp
  2. 14
      src/storm-pars-cli/storm-pars.cpp

10
src/storm-gspn/builder/JaniGSPNBuilder.cpp
View File

@ -139,7 +139,7 @@ namespace storm {
continue;
}
storm::expressions::Expression guard = expressionManager->boolean(true);
std::vector<storm::jani::Assignment> assignments;
for (auto const& inPlaceEntry : trans.getInputPlaces()) {
guard = guard && (vars[inPlaceEntry.first]->getExpressionVariable() >= inPlaceEntry.second);
@ -160,7 +160,7 @@ namespace storm {
std::shared_ptr<storm::jani::TemplateEdge> templateEdge = std::make_shared<storm::jani::TemplateEdge>(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<storm::logic::ProbabilityOperatorFormula>(
std::make_shared<storm::logic::EventuallyFormula>(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<storm::logic::ProbabilityOperatorFormula>(
std::make_shared<storm::logic::BoundedUntilFormula>(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<storm::logic::TimeOperatorFormula>(
std::make_shared<storm::logic::EventuallyFormula>(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;
}

14
src/storm-pars-cli/storm-pars.cpp
View File

@ -280,7 +280,7 @@ namespace storm {
result.model = storm::pars::simplifyModel<ValueType>(result.model, input);
result.changed = true;
}
if (result.model->isOfType(storm::models::ModelType::MarkovAutomaton)) {
result.model = storm::cli::preprocessSparseMarkovAutomaton(result.model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>());
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::models::sparse::Model<ValueType>>()), storm::api::extractFormulasFromProperties(input.properties));
result.model = transformResult.first;
@ -322,7 +322,7 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
PreprocessResult preprocessDdModel(std::shared_ptr<storm::models::symbolic::Model<DdType, ValueType>> const& model, SymbolicInput const& input, storm::cli::ModelProcessingInformation const& mpi) {
auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
PreprocessResult result(model, false);
if (mpi.engine == storm::utility::Engine::Hybrid) {
@ -668,7 +668,7 @@ namespace storm {
}
}
}
template <typename ValueType>
void verifyRegionsWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input, std::vector<storm::storage::ParameterRegion<ValueType>> 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<storm::settings::modules::CoreSettings>();
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;

Write Preview
Loading…
Cancel
Save