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

adapted property ctors with ShieldingExpression param

tempestpy_adaptions
Stefan Pranger 3 years ago
parent
9d4e654ec2
commit
b53a255365
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