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

detect unsupported jani-features directly upon parsing the model.

tempestpy_adaptions
TimQu 6 years ago
parent
ae1987f64c
commit
101b49b898
7 changed files with 120 additions and 39 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. 70
      src/storm-cli-utilities/model-handling.h
  2. 19
      src/storm-parsers/api/model_descriptions.cpp
  3. 2
      src/storm-parsers/api/model_descriptions.h
  4. 12
      src/storm/api/builder.h
  5. 11
      src/storm/builder/BuilderType.h
  6. 33
      src/storm/storage/jani/Model.cpp
  7. 12
      src/storm/storage/jani/Model.h

70
src/storm-cli-utilities/model-handling.h
View File

@ -18,7 +18,8 @@
#include "storm/storage/SymbolicModelDescription.h"
#include "storm/storage/jani/Property.h"
#include "storm/logic/RewardAccumulationEliminationVisitor.h"
#include "storm/builder/BuilderType.h"
#include "storm/models/ModelBase.h"
@ -57,12 +58,13 @@ namespace storm {
boost::optional<std::vector<storm::jani::Property>> preprocessedProperties;
};
void parseSymbolicModelDescription(storm::settings::modules::IOSettings const& ioSettings, SymbolicInput& input) {
void parseSymbolicModelDescription(storm::settings::modules::IOSettings const& ioSettings, SymbolicInput& input, storm::builder::BuilderType const& builderType) {
if (ioSettings.isPrismOrJaniInputSet()) {
if (ioSettings.isPrismInputSet()) {
input.model = storm::api::parseProgram(ioSettings.getPrismInputFilename(), storm::settings::getModule<storm::settings::modules::BuildSettings>().isPrismCompatibilityEnabled());
} else {
auto janiInput = storm::api::parseJaniModel(ioSettings.getJaniInputFilename());
storm::jani::ModelFeatures supportedFeatures = storm::api::getSupportedJaniFeatures(builderType);
auto janiInput = storm::api::parseJaniModel(ioSettings.getJaniInputFilename(), supportedFeatures);
input.model = janiInput.first;
auto const& janiPropertyInput = janiInput.second;
@ -96,23 +98,21 @@ namespace storm {
}
}
SymbolicInput parseSymbolicInput() {
SymbolicInput parseSymbolicInput(storm::builder::BuilderType const& builderType) {
auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
// Parse the property filter, if any is given.
boost::optional<std::set<std::string>> propertyFilter = storm::api::parsePropertyFilter(ioSettings.getPropertyFilter());
SymbolicInput input;
parseSymbolicModelDescription(ioSettings, input);
parseSymbolicModelDescription(ioSettings, input, builderType);
parseProperties(ioSettings, input, propertyFilter);
return input;
}
SymbolicInput preprocessSymbolicInput(SymbolicInput const& input) {
SymbolicInput preprocessSymbolicInput(SymbolicInput const& input, storm::builder::BuilderType const& builderType) {
auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
SymbolicInput output = input;
@ -125,16 +125,12 @@ namespace storm {
}
if (!output.properties.empty()) {
output.properties = storm::api::substituteConstantsInProperties(output.properties, constantDefinitions);
if (output.model.is_initialized() && output.model->isJaniModel()) {
storm::logic::RewardAccumulationEliminationVisitor v(output.model->asJaniModel());
v.eliminateRewardAccumulations(output.properties);
}
}
// Check whether conversion for PRISM to JANI is requested or necessary.
if (input.model && input.model.get().isPrismProgram()) {
bool transformToJani = ioSettings.isPrismToJaniSet();
bool transformToJaniForJit = coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse && buildSettings.isJitSet();
bool transformToJaniForJit = builderType == storm::builder::BuilderType::Jit;
STORM_LOG_WARN_COND(transformToJani || !transformToJaniForJit, "The JIT-based model builder is only available for JANI models, automatically converting the PRISM input model.");
transformToJani |= transformToJaniForJit;
@ -154,25 +150,6 @@ namespace storm {
}
}
// Check whether transformations on the jani model are required
if (output.model && output.model.get().isJaniModel()) {
auto& janiModel = output.model.get().asJaniModel();
// Check if functions need to be eliminated
if (janiModel.getModelFeatures().hasFunctions()) {
if (!output.preprocessedProperties) {
output.preprocessedProperties = output.properties;
}
janiModel.substituteFunctions(output.preprocessedProperties.get());
}
// Check if arrays need to be eliminated. This should be done after! eliminating the functions
if (janiModel.getModelFeatures().hasArrays() && (coreSettings.getEngine() != storm::settings::modules::CoreSettings::Engine::Sparse || buildSettings.isJitSet())) {
if (!output.preprocessedProperties) {
output.preprocessedProperties = output.properties;
}
janiModel.eliminateArrays(output.preprocessedProperties.get());
}
}
return output;
}
@ -186,9 +163,29 @@ namespace storm {
}
}
storm::builder::BuilderType getBuilderType(storm::settings::modules::CoreSettings::Engine const& engine, bool useJit) {
if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid || engine == storm::settings::modules::CoreSettings::Engine::DdSparse || engine == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement) {
return storm::builder::BuilderType::Dd;
} else if (engine == storm::settings::modules::CoreSettings::Engine::Sparse) {
if (useJit) {
return storm::builder::BuilderType::Jit;
} else {
return storm::builder::BuilderType::Explicit;
}
} else if (engine == storm::settings::modules::CoreSettings::Engine::Exploration) {
return storm::builder::BuilderType::Explicit;
}
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to determine the model builder type.");
}
SymbolicInput parseAndPreprocessSymbolicInput() {
SymbolicInput input = parseSymbolicInput();
input = preprocessSymbolicInput(input);
// Get the used builder type to handle cases where preprocessing depends on it
auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
auto builderType = getBuilderType(coreSettings.getEngine(), buildSettings.isJitSet());
SymbolicInput input = parseSymbolicInput(builderType);
input = preprocessSymbolicInput(input, builderType);
exportSymbolicInput(input);
return input;
}
@ -251,9 +248,10 @@ namespace storm {
auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
std::shared_ptr<storm::models::ModelBase> result;
if (input.model) {
if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid || engine == storm::settings::modules::CoreSettings::Engine::DdSparse || engine == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement) {
auto builderType = getBuilderType(engine, buildSettings.isJitSet());
if (builderType == storm::builder::BuilderType::Dd) {
result = buildModelDd<DdType, ValueType>(input);
} else if (engine == storm::settings::modules::CoreSettings::Engine::Sparse) {
} else if (builderType == storm::builder::BuilderType::Explicit || builderType == storm::builder::BuilderType::Jit) {
result = buildModelSparse<ValueType>(input, buildSettings);
}
} else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet() || ioSettings.isExplicitIMCASet()) {

19
src/storm-parsers/api/model_descriptions.cpp
View File

@ -6,9 +6,9 @@
#include "storm/storage/jani/Model.h"
#include "storm/storage/jani/Property.h"
#include "storm/exceptions/NotSupportedException.h"
#include "storm/utility/macros.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/BuildSettings.h"
namespace storm {
namespace api {
@ -18,12 +18,25 @@ namespace storm {
program.checkValidity();
return program;
}
std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> parseJaniModel(std::string const& filename) {
storm::jani::ModelFeatures features;
// Add derived-operators and state-exit-rewards as these can be handled by all model builders
features.add(storm::jani::ModelFeature::DerivedOperators);
features.add(storm::jani::ModelFeature::StateExitRewards);
return parseJaniModel(filename, features);
}
std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> parseJaniModel(std::string const& filename, storm::jani::ModelFeatures const& allowedFeatures) {
std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> modelAndFormulae = storm::parser::JaniParser::parse(filename);
modelAndFormulae.first.checkValid();
// TODO: properties
auto nonEliminatedFeatures = modelAndFormulae.first.restrictToFeatures(allowedFeatures);
STORM_LOG_THROW(nonEliminatedFeatures.empty(), storm::exceptions::NotSupportedException, "The used model feature(s) " << nonEliminatedFeatures.toString() << " is/are not in the list of allowed features.");
return modelAndFormulae;
}
}
}

2
src/storm-parsers/api/model_descriptions.h
View File

@ -2,6 +2,7 @@
#include <string>
#include <map>
#include <storm/storage/jani/ModelFeatures.h>
namespace storm {
namespace prism {
@ -17,6 +18,7 @@ namespace storm {
storm::prism::Program parseProgram(std::string const& filename, bool prismCompatibility = false);
std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> parseJaniModel(std::string const& filename);
std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> parseJaniModel(std::string const& filename, storm::jani::ModelFeatures const& allowedFeatures);
}
}

12
src/storm/api/builder.h
View File

@ -5,6 +5,7 @@
#include "storm-parsers/parser/ImcaMarkovAutomatonParser.h"
#include "storm/storage/SymbolicModelDescription.h"
#include "storm/storage/jani/ModelFeatures.h"
#include "storm/storage/sparse/ModelComponents.h"
#include "storm/models/sparse/Dtmc.h"
@ -16,6 +17,7 @@
#include "storm/builder/DdPrismModelBuilder.h"
#include "storm/builder/DdJaniModelBuilder.h"
#include "storm/builder/BuilderType.h"
#include "storm/generator/PrismNextStateGenerator.h"
#include "storm/generator/JaniNextStateGenerator.h"
@ -29,6 +31,16 @@
namespace storm {
namespace api {
storm::jani::ModelFeatures getSupportedJaniFeatures(storm::builder::BuilderType const& builderType) {
storm::jani::ModelFeatures features;
features.add(storm::jani::ModelFeature::DerivedOperators);
features.add(storm::jani::ModelFeature::StateExitRewards);
if (builderType == storm::builder::BuilderType::Explicit) {
features.add(storm::jani::ModelFeature::Arrays);
}
return features;
}
template<storm::dd::DdType LibraryType, typename ValueType>
std::shared_ptr<storm::models::symbolic::Model<LibraryType, ValueType>> buildSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool buildFullModel = false) {
if (model.isPrismProgram()) {

11
src/storm/builder/BuilderType.h
View File

@ -0,0 +1,11 @@
#pragma once
namespace storm {
namespace builder {
enum class BuilderType {
Explicit,
Dd,
Jit
};
}
}

33
src/storm/storage/jani/Model.cpp
View File

@ -1031,6 +1031,39 @@ namespace storm {
}
}
ModelFeatures Model::restrictToFeatures(ModelFeatures const& modelFeatures) {
std::vector<Property> emptyPropertyVector;
return restrictToFeatures(modelFeatures, emptyPropertyVector);
}
ModelFeatures Model::restrictToFeatures(ModelFeatures const& features, std::vector<Property>& properties) {
ModelFeatures uncheckedFeatures = getModelFeatures();
// Check if functions need to be eliminated.
if (uncheckedFeatures.hasFunctions() && !features.hasFunctions()) {
substituteFunctions(properties);
}
uncheckedFeatures.remove(ModelFeature::Functions);
// Check if arrays need to be eliminated. This should be done after! eliminating the functions
if (uncheckedFeatures.hasArrays() && !features.hasArrays()) {
eliminateArrays(properties);
}
uncheckedFeatures.remove(ModelFeature::Arrays);
// There is no elimination for state exit rewards
if (features.hasStateExitRewards()) {
uncheckedFeatures.remove(ModelFeature::StateExitRewards);
}
// There is no elimination of derived operators
if (features.hasDerivedOperators()) {
uncheckedFeatures.remove(ModelFeature::DerivedOperators);
}
return uncheckedFeatures;
}
void Model::setInitialStatesRestriction(storm::expressions::Expression const& initialStatesRestriction) {
this->initialStatesRestriction = initialStatesRestriction;
}

12
src/storm/storage/jani/Model.h
View File

@ -423,6 +423,18 @@ namespace storm {
*/
void eliminateArrays(std::vector<Property>& properties);
/*!
* Attempts to eliminate all features of this model that are not in the given set of features.
* @return The model features that could not be eliminated.
*/
ModelFeatures restrictToFeatures(ModelFeatures const& modelFeatures);
/*!
* Attempts to eliminate all features of this model and the given properties that are not in the given set of features.
* @return The model features that could not be eliminated.
*/
ModelFeatures restrictToFeatures(ModelFeatures const& modelFeatures, std::vector<Property>& properties);
/*!
* Retrieves whether there is an expression restricting the legal initial values of the global variables.
*/

Write Preview
Loading…
Cancel
Save