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

Do not perform the conversion from a prism program to a jani model twice.

main
Tim Quatmann 5 years ago
parent
9962da7453
commit
c6b984ca51
6 changed files with 85 additions and 72 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. 4
      src/storm-cli-utilities/cli.cpp
  2. 96
      src/storm-cli-utilities/model-handling.h
  3. 4
      src/storm-pars-cli/storm-pars.cpp
  4. 4
      src/storm-pomdp-cli/storm-pomdp.cpp
  5. 20
      src/storm/utility/Portfolio.cpp
  6. 9
      src/storm/utility/Portfolio.h

4
src/storm-cli-utilities/cli.cpp
View File

@ -246,10 +246,10 @@ namespace storm {
SymbolicInput symbolicInput = parseSymbolicInput();
// Obtain settings for model processing
ModelProcessingInformation mpi = getModelProcessingInformation(symbolicInput);
ModelProcessingInformation mpi;
// Preprocess the symbolic input
symbolicInput = preprocessSymbolicInput(symbolicInput, mpi.engine);
std::tie(symbolicInput, mpi) = preprocessSymbolicInput(symbolicInput);
// Export symbolic input (if requested)
exportSymbolicInput(symbolicInput);

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

@ -156,6 +156,9 @@ namespace storm {
// If set, bisimulation will be applied.
bool applyBisimulation;
// If set, a transformation to Jani will be enforced
bool transformToJani;
// Which data type is to be used for numbers ...
enum class ValueType {
FinitePrecision,
@ -175,16 +178,17 @@ namespace storm {
void getModelProcessingInformationPortfolio(SymbolicInput const& input, ModelProcessingInformation& mpi) {
auto hints = storm::settings::getModule<storm::settings::modules::HintSettings>();
STORM_LOG_THROW(input.model.is_initialized(), storm::exceptions::InvalidArgumentException, "Portfolio engine requires a symbolic model (PRISM or JANI.");
STORM_LOG_THROW(input.model.is_initialized(), storm::exceptions::InvalidArgumentException, "Portfolio engine requires a JANI input model.");
STORM_LOG_THROW(input.model->isJaniModel(), storm::exceptions::InvalidArgumentException, "Portfolio engine requires a JANI input model.");
std::vector<storm::jani::Property> const& properties = input.preprocessedProperties.is_initialized() ? input.preprocessedProperties.get() : input.properties;
STORM_LOG_THROW(!properties.empty(), storm::exceptions::InvalidArgumentException, "Portfolio engine requires a property.");
STORM_LOG_WARN_COND(properties.size() == 1, "Portfolio engine does not support decisions based on multiple properties. Only the first property will be considered.");
storm::utility::Portfolio pf;
if (hints.isNumberStatesSet()) {
pf.predict(input.model.get(), properties.front(), hints.getNumberStates());
pf.predict(input.model->asJaniModel(), properties.front(), hints.getNumberStates());
} else {
pf.predict(input.model.get(), properties.front());
pf.predict(input.model->asJaniModel(), properties.front());
}
mpi.engine = pf.getEngine();
@ -202,8 +206,14 @@ namespace storm {
<< std::noboolalpha << std::endl);
}
ModelProcessingInformation getModelProcessingInformation(SymbolicInput const& input) {
/*!
* Sets the model processing information based on the given input.
* Finding the right model processing information might require a conversion to jani.
* In this case, the jani conversion is stored in the transformedJaniInput pointer (unless it is null)
*/
ModelProcessingInformation getModelProcessingInformation(SymbolicInput const& input, std::shared_ptr<SymbolicInput> const& transformedJaniInput = nullptr) {
ModelProcessingInformation mpi;
auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
@ -224,10 +234,29 @@ namespace storm {
}
// Since the remaining settings could depend on the ones above, we need apply the portfolio engine now.
bool usePortfolio = mpi.engine == storm::utility::Engine::Portfolio;
bool usePortfolio = input.model.is_initialized() && mpi.engine == storm::utility::Engine::Portfolio;
if (usePortfolio) {
if (input.model->isJaniModel()) {
// This can potentially overwrite the settings above, but will not overwrite settings that were explicitly set by the user (e.g. we will not disable bisimulation or disable exact arithmetic)
getModelProcessingInformationPortfolio(input, mpi);
} else {
// Transform Prism to jani first
STORM_LOG_ASSERT(input.model->isPrismProgram(), "Unexpected type of input.");
SymbolicInput janiInput;
janiInput.properties = input.properties;
storm::prism::Program const& prog = input.model.get().asPrismProgram();
auto modelAndProperties = prog.toJani(input.preprocessedProperties.is_initialized() ? input.preprocessedProperties.get() : input.properties);
janiInput.model = modelAndProperties.first;
if (!modelAndProperties.second.empty()) {
janiInput.preprocessedProperties = std::move(modelAndProperties.second);
}
// This can potentially overwrite the settings above, but will not overwrite settings that were explicitly set by the user (e.g. we will not disable bisimulation or disable exact arithmetic)
getModelProcessingInformationPortfolio(janiInput, mpi);
if (transformedJaniInput) {
// We cache the transformation result.
*transformedJaniInput = std::move(janiInput);
}
}
}
// Check whether these settings are compatible with the provided input.
@ -256,6 +285,14 @@ namespace storm {
}
}
// Set whether a transformation to jani is required or necessary
mpi.transformToJani = ioSettings.isPrismToJaniSet();
auto builderType = storm::utility::getBuilderType(mpi.engine);
bool transformToJaniForJit = builderType == storm::builder::BuilderType::Jit;
STORM_LOG_WARN_COND(mpi.transformToJani || !transformToJaniForJit, "The JIT-based model builder is only available for JANI models, automatically converting the PRISM input model.");
bool transformToJaniForDdMA = (builderType == storm::builder::BuilderType::Dd) && (input.model->getModelType() == storm::storage::SymbolicModelDescription::ModelType::MA);
STORM_LOG_WARN_COND(mpi.transformToJani || !transformToJaniForDdMA, "Dd-based model builder for Markov Automata is only available for JANI models, automatically converting the PRISM input model.");
mpi.transformToJani |= (transformToJaniForJit || transformToJaniForDdMA);
// Set the Valuetype used during model building
mpi.buildValueType = mpi.verificationValueType;
@ -294,17 +331,11 @@ namespace storm {
}
}
SymbolicInput preprocessSymbolicInput(SymbolicInput const& input, storm::utility::Engine const& engine) {
std::pair<SymbolicInput, ModelProcessingInformation> preprocessSymbolicInput(SymbolicInput const& input) {
auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
auto builderType = storm::utility::getBuilderType(engine);
SymbolicInput output = input;
if (output.model && output.model.get().isJaniModel()) {
storm::jani::ModelFeatures supportedFeatures = storm::api::getSupportedJaniFeatures(builderType);
storm::api::simplifyJaniModel(output.model.get().asJaniModel(), output.properties, supportedFeatures);
}
// Substitute constant definitions in symbolic input.
std::string constantDefinitionString = ioSettings.getConstantDefinitionString();
std::map<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions;
@ -315,25 +346,22 @@ namespace storm {
if (!output.properties.empty()) {
output.properties = storm::api::substituteConstantsInProperties(output.properties, constantDefinitions);
}
ensureNoUndefinedPropertyConstants(output.properties);
auto transformedJani = std::make_shared<SymbolicInput>();
ModelProcessingInformation mpi = getModelProcessingInformation(output, transformedJani);
// Check whether conversion for PRISM to JANI is requested or necessary.
if (input.model && input.model.get().isPrismProgram()) {
bool transformToJani = ioSettings.isPrismToJaniSet();
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.");
bool transformToJaniForDdMA = (builderType == storm::builder::BuilderType::Dd) && (input.model->getModelType() == storm::storage::SymbolicModelDescription::ModelType::MA);
STORM_LOG_WARN_COND(transformToJani || !transformToJaniForDdMA, "Dd-based model builder for Markov Automata is only available for JANI models, automatically converting the PRISM input model.");
transformToJani |= (transformToJaniForJit || transformToJaniForDdMA);
auto builderType = storm::utility::getBuilderType(mpi.engine);
if (transformToJani) {
// Check whether conversion for PRISM to JANI is requested or necessary.
if (output.model && output.model.get().isPrismProgram()) {
if (mpi.transformToJani) {
if (transformedJani->model) {
// Use the cached transformation if possible
output = std::move(*transformedJani);
} else {
storm::prism::Program const& model = output.model.get().asPrismProgram();
auto modelAndProperties = model.toJani(output.properties);
// Remove functions here
modelAndProperties.first.substituteFunctions();
output.model = modelAndProperties.first;
if (!modelAndProperties.second.empty()) {
@ -341,8 +369,14 @@ namespace storm {
}
}
}
}
return output;
if (output.model && output.model.get().isJaniModel()) {
storm::jani::ModelFeatures supportedFeatures = storm::api::getSupportedJaniFeatures(builderType);
storm::api::simplifyJaniModel(output.model.get().asJaniModel(), output.properties, supportedFeatures);
}
return {output, mpi};
}
void exportSymbolicInput(SymbolicInput const& input) {
@ -355,16 +389,6 @@ namespace storm {
}
}
SymbolicInput parseAndPreprocessSymbolicInput(storm::utility::Engine const& engine) {
// Get the used builder type to handle cases where preprocessing depends on it
auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
SymbolicInput input = parseSymbolicInput();
input = preprocessSymbolicInput(input, engine);
exportSymbolicInput(input);
return input;
}
std::vector<std::shared_ptr<storm::logic::Formula const>> createFormulasToRespect(std::vector<storm::jani::Property> const& properties) {
std::vector<std::shared_ptr<storm::logic::Formula const>> result = storm::api::extractFormulasFromProperties(properties);

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

@ -783,8 +783,8 @@ namespace storm {
// Parse and preprocess symbolic input (PRISM, JANI, properties, etc.)
auto symbolicInput = storm::cli::parseSymbolicInput();
auto mpi = storm::cli::getModelProcessingInformation(symbolicInput);
symbolicInput = storm::cli::preprocessSymbolicInput(symbolicInput, mpi.engine);
storm::cli::ModelProcessingInformation mpi;
std::tie(symbolicInput, mpi) = storm::cli::preprocessSymbolicInput(symbolicInput);
processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, storm::RationalFunction>(symbolicInput, mpi);
}

4
src/storm-pomdp-cli/storm-pomdp.cpp
View File

@ -99,8 +99,8 @@ int main(const int argc, const char** argv) {
auto const& pomdpSettings = storm::settings::getModule<storm::settings::modules::POMDPSettings>();
auto symbolicInput = storm::cli::parseSymbolicInput();
auto mpi = storm::cli::getModelProcessingInformation(symbolicInput);
symbolicInput = storm::cli::preprocessSymbolicInput(symbolicInput, mpi.engine);
storm::cli::ModelProcessingInformation mpi;
std::tie(symbolicInput, mpi) = storm::cli::preprocessSymbolicInput(symbolicInput);
// We should not export here if we are going to do some processing first.
auto model = storm::cli::buildPreprocessExportModelWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, storm::RationalNumber>(symbolicInput, mpi);

20
src/storm/utility/Portfolio.cpp
View File

@ -34,15 +34,7 @@ namespace storm {
}
struct Features {
Features(storm::storage::SymbolicModelDescription const& modelDescription, storm::jani::Property const& property) {
if (!modelDescription.isJaniModel()) {
initialize(modelDescription.toJani().asJaniModel(), property);
} else {
initialize(modelDescription.asJaniModel(), property);
}
}
void initialize(storm::jani::Model const& model, storm::jani::Property const& property) {
Features(storm::jani::Model const& model, storm::jani::Property const& property) {
continuousTime = !model.isDiscreteTimeModel();
nondeterminism = !model.isDeterministicModel();
propertyType = getPropertyType(property);
@ -65,9 +57,9 @@ namespace storm {
// Intentionally left empty
}
void Portfolio::predict(storm::storage::SymbolicModelDescription const& modelDescription, storm::jani::Property const& property) {
void Portfolio::predict(storm::jani::Model const& model, storm::jani::Property const& property) {
typedef pfinternal::PropertyType PropertyType;
auto f = pfinternal::Features(modelDescription, property);
auto f = pfinternal::Features(model, property);
{ // Decision tree start
if (f.numEdges <= 618) {
@ -171,12 +163,12 @@ namespace storm {
}
void Portfolio::predict(storm::storage::SymbolicModelDescription const& modelDescription, storm::jani::Property const& property, uint64_t stateEstimate) {
void Portfolio::predict(storm::jani::Model const& model, storm::jani::Property const& property, uint64_t stateEstimate) {
typedef pfinternal::PropertyType PropertyType;
auto f = pfinternal::Features(modelDescription, property);
auto f = pfinternal::Features(model, property);
f.stateEstimate = stateEstimate;
// TODO: Actually make use of the estimate
predict(modelDescription, property);
predict(model, property);
}
storm::utility::Engine Portfolio::getEngine() const {

9
src/storm/utility/Portfolio.h
View File

@ -5,13 +5,10 @@
namespace storm {
namespace jani {
class Model;
class Property;
}
namespace storage {
class SymbolicModelDescription;
}
namespace utility {
class Portfolio {
public:
@ -20,13 +17,13 @@ namespace storm {
/*!
* Predicts "good" settings for the provided model checking query
*/
void predict(storm::storage::SymbolicModelDescription const& modelDescription, storm::jani::Property const& property);
void predict(storm::jani::Model const& model, storm::jani::Property const& property);
/*!
* Predicts "good" settings for the provided model checking query
* @param stateEstimate A hint that gives a (rough) estimate for the number of states.
*/
void predict(storm::storage::SymbolicModelDescription const& modelDescription, storm::jani::Property const& property, uint64_t stateEstimate);
void predict(storm::jani::Model const& model, storm::jani::Property const& property, uint64_t stateEstimate);
/// Retrieve "good" settings after calling predict.
storm::utility::Engine getEngine() const;

Write Preview
Loading…
Cancel
Save