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

Introduced JIT as a separate engine.

tempestpy_adaptions
Tim Quatmann 5 years ago
parent
d9176dc867
commit
17325419fb
6 changed files with 44 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. 9
      src/storm-cli-utilities/cli.cpp
  2. 25
      src/storm-cli-utilities/model-handling.h
  3. 6
      src/storm/settings/modules/BuildSettings.cpp
  4. 6
      src/storm/settings/modules/BuildSettings.h
  5. 28
      src/storm/utility/Engine.cpp
  6. 9
      src/storm/utility/Engine.h

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

@ -250,28 +250,27 @@ namespace storm {
auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
auto engine = coreSettings.getEngine();
auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
auto builderType = getBuilderType(engine, buildSettings.isJitSet());
// TODO: (end of method)
symbolicInput = preprocessSymbolicInput(symbolicInput, builderType);
symbolicInput = preprocessSymbolicInput(symbolicInput, storm::utility::getBuilderType(engine));
exportSymbolicInput(symbolicInput);
auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
if (generalSettings.isParametricSet()) {
#ifdef STORM_HAVE_CARL
processInputWithValueType<storm::RationalFunction>(symbolicInput);
processInputWithValueType<storm::RationalFunction>(symbolicInput, engine);
#else
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No parameters are supported in this build.");
#endif
} else if (generalSettings.isExactSet()) {
#ifdef STORM_HAVE_CARL
processInputWithValueType<storm::RationalNumber>(symbolicInput);
processInputWithValueType<storm::RationalNumber>(symbolicInput, engine);
#else
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No exact numbers are supported in this build.");
#endif
} else {
processInputWithValueType<double>(symbolicInput);
processInputWithValueType<double>(symbolicInput, engine);
}
}

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

@ -218,25 +218,10 @@ namespace storm {
}
}
storm::builder::BuilderType getBuilderType(storm::utility::Engine const& engine, bool useJit) {
if (engine == storm::utility::Engine::Dd || engine == storm::utility::Engine::Hybrid || engine == storm::utility::Engine::DdSparse || engine == storm::utility::Engine::AbstractionRefinement) {
return storm::builder::BuilderType::Dd;
} else if (engine == storm::utility::Engine::Sparse) {
if (useJit) {
return storm::builder::BuilderType::Jit;
} else {
return storm::builder::BuilderType::Explicit;
}
} else if (engine == storm::utility::Engine::Exploration) {
return storm::builder::BuilderType::Explicit;
}
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to determine the model builder type.");
}
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>();
auto builderType = getBuilderType(engine, buildSettings.isJitSet());
auto builderType = storm::utility::getBuilderType(engine);
SymbolicInput input = parseSymbolicInput();
input = preprocessSymbolicInput(input, builderType);
@ -262,7 +247,7 @@ namespace storm {
}
template <typename ValueType>
std::shared_ptr<storm::models::ModelBase> buildModelSparse(SymbolicInput const& input, storm::settings::modules::BuildSettings const& buildSettings) {
std::shared_ptr<storm::models::ModelBase> buildModelSparse(SymbolicInput const& input, storm::settings::modules::BuildSettings const& buildSettings, bool useJit) {
storm::builder::BuilderOptions options(createFormulasToRespect(input.properties), input.model.get());
options.setBuildChoiceLabels(buildSettings.isBuildChoiceLabelsSet());
options.setBuildStateValuations(buildSettings.isBuildStateValuationsSet());
@ -286,7 +271,7 @@ namespace storm {
options.setBuildAllLabels(true);
options.setBuildAllRewardModels(true);
}
return storm::api::buildSparseModel<ValueType>(input.model.get(), options, buildSettings.isJitSet(), storm::settings::getModule<storm::settings::modules::JitBuilderSettings>().isDoctorSet());
return storm::api::buildSparseModel<ValueType>(input.model.get(), options, useJit, storm::settings::getModule<storm::settings::modules::JitBuilderSettings>().isDoctorSet());
}
template <typename ValueType>
@ -312,11 +297,11 @@ namespace storm {
auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
std::shared_ptr<storm::models::ModelBase> result;
if (input.model) {
auto builderType = getBuilderType(engine, buildSettings.isJitSet());
auto builderType = storm::utility::getBuilderType(engine);
if (builderType == storm::builder::BuilderType::Dd) {
result = buildModelDd<DdType, ValueType>(input);
} else if (builderType == storm::builder::BuilderType::Explicit || builderType == storm::builder::BuilderType::Jit) {
result = buildModelSparse<ValueType>(input, buildSettings);
result = buildModelSparse<ValueType>(input, buildSettings, builderType == storm::builder::BuilderType::Jit);
}
} else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet() || ioSettings.isExplicitIMCASet()) {
STORM_LOG_THROW(engine == storm::utility::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Can only use sparse engine with explicit input.");

6
src/storm/settings/modules/BuildSettings.cpp
View File

@ -18,7 +18,6 @@ namespace storm {
const std::string BuildSettings::moduleName = "build";
const std::string jitOptionName = "jit";
const std::string explorationOrderOptionName = "explorder";
const std::string explorationOrderOptionShortName = "eo";
const std::string explorationChecksOptionName = "explchecks";
@ -38,7 +37,6 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, prismCompatibilityOptionName, false, "Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build());
this->addOption(storm::settings::OptionBuilder(moduleName, dontFixDeadlockOptionName, false, "If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(dontFixDeadlockOptionShortName).setIsAdvanced().build());
this->addOption(storm::settings::OptionBuilder(moduleName, jitOptionName, false, "If set, the model is built using the JIT model builder.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, fullModelBuildOptionName, false, "If set, include all rewards and labels.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, buildChoiceLabelOptionName, false, "If set, also build the choice labels").setIsAdvanced().build());
this->addOption(storm::settings::OptionBuilder(moduleName, buildStateValuationsOptionName, false, "If set, also build the state valuations").setIsAdvanced().build());
@ -53,10 +51,6 @@ namespace storm {
.addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("number", "The number of bits.").addValidatorUnsignedInteger(ArgumentValidatorFactory::createUnsignedRangeValidatorExcluding(0,63)).setDefaultValueUnsignedInteger(32).build()).build());
}
bool BuildSettings::isJitSet() const {
return this->getOption(jitOptionName).getHasOptionBeenSet();
}
bool BuildSettings::isExplorationOrderSet() const {
return this->getOption(explorationOrderOptionName).getHasOptionBeenSet();
}

6
src/storm/settings/modules/BuildSettings.h
View File

@ -16,12 +16,6 @@ namespace storm {
* Creates a new set of core settings.
*/
BuildSettings();
/*!
* Retrieves whether the option to use the JIT builder is set.
*
* @return True iff the JIT builder is to be used.
*/
bool isJitSet() const;
/*!
* Retrieves whether the model exploration order was set.

28
src/storm/utility/Engine.cpp
View File

@ -19,6 +19,10 @@
#include "storm/storage/SymbolicModelDescription.h"
#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidArgumentException.h"
namespace storm {
namespace utility {
@ -41,6 +45,8 @@ namespace storm {
return "dd";
case Engine::DdSparse:
return "dd-to-sparse";
case Engine::Jit:
return "jit";
case Engine::Exploration:
return "expl";
case Engine::AbstractionRefinement:
@ -68,6 +74,28 @@ namespace storm {
return Engine::Unknown;
}
storm::builder::BuilderType getBuilderType(Engine const& engine) {
switch (engine) {
case Engine::Sparse:
return storm::builder::BuilderType::Explicit;
case Engine::Hybrid:
return storm::builder::BuilderType::Dd;
case Engine::Dd:
return storm::builder::BuilderType::Dd;
case Engine::DdSparse:
return storm::builder::BuilderType::Dd;
case Engine::Jit:
return storm::builder::BuilderType::Jit;
case Engine::Exploration:
return storm::builder::BuilderType::Explicit;
case Engine::AbstractionRefinement:
return storm::builder::BuilderType::Dd;
default:
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given engine has no builder type to it.");
return storm::builder::BuilderType::Explicit;
}
}
template <storm::dd::DdType ddType, typename ValueType>
bool canHandle(storm::utility::Engine const& engine, storm::models::ModelType const& modelType, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& checkTask) {
// Define types to improve readability

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

@ -5,6 +5,7 @@
#include "storm/models/ModelType.h"
#include "storm/storage/dd/DdType.h"
#include "storm/builder/BuilderType.h"
namespace storm {
@ -25,7 +26,7 @@ namespace storm {
/// An enumeration of all engines.
enum class Engine {
// The last one should always be 'Unknown' to make sure that the getEngines() method below works.
Sparse, Hybrid, Dd, DdSparse, Exploration, AbstractionRefinement, Unknown
Sparse, Hybrid, Dd, DdSparse, Jit, Exploration, AbstractionRefinement, Unknown
};
/*!
@ -49,6 +50,11 @@ namespace storm {
*/
Engine engineFromString(std::string const& engineStr);
/*!
* Returns the builder type used for the given engine.
*/
storm::builder::BuilderType getBuilderType(storm::utility::Engine const& engine);
/*!
* Returns false if the given model type and checkTask can certainly not be handled by the given engine.
* Notice that the set of handable model checking queries is only overapproximated, i.e. if this returns true,
@ -66,6 +72,5 @@ namespace storm {
*/
template <storm::dd::DdType ddType, typename ValueType>
bool canHandle(storm::utility::Engine const& engine, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& checkTask, storm::storage::SymbolicModelDescription const& modelDescription);
}
}
Write Preview
Loading…
Cancel
Save