Browse Source
split IOSettings in BuildSettings and IOSettings, refactored some dependencies on settings object away if it doesnt hurt too much, moved GSPN and PGCL settings to their own libs
tempestpy_adaptions
split IOSettings in BuildSettings and IOSettings, refactored some dependencies on settings object away if it doesnt hurt too much, moved GSPN and PGCL settings to their own libs
tempestpy_adaptions
sjunges
7 years ago
34 changed files with 340 additions and 417 deletions
-
37src/storm-cli-utilities/model-handling.h
-
4src/storm-gspn/settings/modules/GSPNExportSettings.cpp
-
0src/storm-gspn/settings/modules/GSPNExportSettings.h
-
2src/storm-gspn/settings/modules/GSPNSettings.cpp
-
0src/storm-gspn/settings/modules/GSPNSettings.h
-
34src/storm-pars-cli/storm-pars.cpp
-
2src/storm-pgcl-cli/storm-pgcl.cpp
-
2src/storm-pgcl/settings/modules/PGCLSettings.cpp
-
0src/storm-pgcl/settings/modules/PGCLSettings.h
-
8src/storm/api/model_descriptions.cpp
-
2src/storm/api/model_descriptions.h
-
6src/storm/builder/BuilderOptions.cpp
-
4src/storm/builder/ExplicitModelBuilder.cpp
-
4src/storm/parser/ImcaMarkovAutomatonParser.cpp
-
14src/storm/parser/PrismParser.cpp
-
8src/storm/parser/PrismParser.h
-
3src/storm/settings/SettingsManager.cpp
-
95src/storm/settings/modules/BuildSettings.cpp
-
84src/storm/settings/modules/BuildSettings.h
-
4src/storm/settings/modules/CoreSettings.h
-
104src/storm/settings/modules/IOSettings.cpp
-
81src/storm/settings/modules/IOSettings.h
-
1src/storm/solver/AbstractEquationSolver.cpp
-
20src/storm/storage/prism/Program.cpp
-
4src/storm/storage/prism/Program.h
-
26src/test/storm/builder/DdJaniModelBuilderTest.cpp
-
28src/test/storm/builder/DdPrismModelBuilderTest.cpp
-
14src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp
-
15src/test/storm/builder/ExplicitJitJaniModelBuilderTest.cpp
-
14src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp
-
25src/test/storm/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
-
45src/test/storm/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
-
25src/test/storm/modelchecker/NativeCtmcCslModelCheckerTest.cpp
-
42src/test/storm/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
@ -1,5 +1,5 @@ |
|||
#include "GSPNExportSettings.h"
|
|||
#include "JaniExportSettings.h"
|
|||
#include "storm-gspn/settings/modules/GSPNExportSettings.h"
|
|||
#include "storm/settings/modules/JaniExportSettings.h"
|
|||
|
|||
#include "storm/settings/SettingsManager.h"
|
|||
#include "storm/settings/SettingMemento.h"
|
|||
@ -1,4 +1,4 @@ |
|||
#include "GSPNSettings.h"
|
|||
#include "storm-gspn/settings/modules/GSPNSettings.h"
|
|||
|
|||
#include "storm/settings/SettingsManager.h"
|
|||
#include "storm/settings/SettingMemento.h"
|
|||
@ -1,4 +1,4 @@ |
|||
#include "storm/settings/modules/PGCLSettings.h"
|
|||
#include "PGCLSettings.h"
|
|||
|
|||
#include "storm/settings/SettingsManager.h"
|
|||
#include "storm/settings/SettingMemento.h"
|
|||
@ -0,0 +1,95 @@ |
|||
#include "storm/settings/modules/BuildSettings.h"
|
|||
|
|||
#include "storm/settings/SettingsManager.h"
|
|||
#include "storm/settings/SettingMemento.h"
|
|||
#include "storm/settings/Option.h"
|
|||
#include "storm/settings/OptionBuilder.h"
|
|||
#include "storm/settings/ArgumentBuilder.h"
|
|||
#include "storm/settings/Argument.h"
|
|||
#include "storm/exceptions/InvalidSettingsException.h"
|
|||
#include "storm/parser/CSVParser.h"
|
|||
|
|||
#include "storm/utility/macros.h"
|
|||
#include "storm/exceptions/IllegalArgumentValueException.h"
|
|||
|
|||
namespace storm { |
|||
namespace settings { |
|||
namespace modules { |
|||
|
|||
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"; |
|||
const std::string explorationChecksOptionShortName = "ec"; |
|||
const std::string prismCompatibilityOptionName = "prismcompat"; |
|||
const std::string prismCompatibilityOptionShortName = "pc"; |
|||
const std::string noBuildOptionName = "nobuild"; |
|||
const std::string fullModelBuildOptionName = "buildfull"; |
|||
const std::string buildChoiceLabelOptionName = "buildchoicelab"; |
|||
const std::string buildStateValuationsOptionName = "buildstateval"; |
|||
BuildSettings::BuildSettings() : ModuleSettings(moduleName) { |
|||
|
|||
std::vector<std::string> explorationOrders = {"dfs", "bfs"}; |
|||
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, 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").build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, buildStateValuationsOptionName, false, "If set, also build the state valuations").build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, noBuildOptionName, false, "If set, do not build the model.").build()); |
|||
|
|||
this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName) |
|||
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the exploration order to choose.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(explorationOrders)).setDefaultValueString("bfs").build()).build()); |
|||
this->addOption(storm::settings::OptionBuilder(moduleName, explorationChecksOptionName, false, "If set, additional checks (if available) are performed during model exploration to debug the model.").setShortName(explorationChecksOptionShortName).build()); |
|||
|
|||
} |
|||
|
|||
|
|||
bool BuildSettings::isJitSet() const { |
|||
return this->getOption(jitOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
bool BuildSettings::isExplorationOrderSet() const { |
|||
return this->getOption(explorationOrderOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
bool BuildSettings::isPrismCompatibilityEnabled() const { |
|||
return this->getOption(prismCompatibilityOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
bool BuildSettings::isBuildFullModelSet() const { |
|||
return this->getOption(fullModelBuildOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
bool BuildSettings::isNoBuildModelSet() const { |
|||
return this->getOption(noBuildOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
bool BuildSettings::isBuildChoiceLabelsSet() const { |
|||
return this->getOption(buildChoiceLabelOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
bool BuildSettings::isBuildStateValuationsSet() const { |
|||
return this->getOption(buildStateValuationsOptionName).getHasOptionBeenSet(); |
|||
} |
|||
|
|||
|
|||
storm::builder::ExplorationOrder BuildSettings::getExplorationOrder() const { |
|||
std::string explorationOrderAsString = this->getOption(explorationOrderOptionName).getArgumentByName("name").getValueAsString(); |
|||
if (explorationOrderAsString == "dfs") { |
|||
return storm::builder::ExplorationOrder::Dfs; |
|||
} else if (explorationOrderAsString == "bfs") { |
|||
return storm::builder::ExplorationOrder::Bfs; |
|||
} |
|||
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown exploration order '" << explorationOrderAsString << "'."); |
|||
} |
|||
|
|||
bool BuildSettings::isExplorationChecksSet() const { |
|||
return this->getOption(explorationChecksOptionName).getHasOptionBeenSet(); |
|||
} |
|||
} |
|||
|
|||
|
|||
} |
|||
} |
|||
@ -0,0 +1,84 @@ |
|||
#pragma once |
|||
|
|||
|
|||
#include "storm-config.h" |
|||
#include "storm/settings/modules/ModuleSettings.h" |
|||
#include "storm/builder/ExplorationOrder.h" |
|||
|
|||
namespace storm { |
|||
namespace settings { |
|||
namespace modules { |
|||
class BuildSettings : public ModuleSettings { |
|||
|
|||
public: |
|||
|
|||
/*! |
|||
* 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. |
|||
* |
|||
* @return True if the model exploration option was set. |
|||
*/ |
|||
bool isExplorationOrderSet() const; |
|||
|
|||
/*! |
|||
* Retrieves whether to perform additional checks during model exploration (e.g. out-of-bounds, etc.). |
|||
* |
|||
* @return True if additional checks are to be performed. |
|||
*/ |
|||
bool isExplorationChecksSet() const; |
|||
|
|||
/*! |
|||
* Retrieves the exploration order if it was set. |
|||
* |
|||
* @return The chosen exploration order. |
|||
*/ |
|||
storm::builder::ExplorationOrder getExplorationOrder() const; |
|||
|
|||
/*! |
|||
* Retrieves whether the PRISM compatibility mode was enabled. |
|||
* |
|||
* @return True iff the PRISM compatibility mode was enabled. |
|||
*/ |
|||
bool isPrismCompatibilityEnabled() const; |
|||
|
|||
/** |
|||
* Retrieves whether no model should be build at all, in case one just want to translate models or parse a file. |
|||
*/ |
|||
bool isNoBuildModelSet() const; |
|||
|
|||
/*! |
|||
* Retrieves whether the full model should be build, that is, the model including all labels and rewards. |
|||
* |
|||
* @return true iff the full model should be build. |
|||
*/ |
|||
bool isBuildFullModelSet() const; |
|||
|
|||
/*! |
|||
* Retrieves whether the choice labels should be build |
|||
* @return |
|||
*/ |
|||
bool isBuildChoiceLabelsSet() const; |
|||
|
|||
/*! |
|||
* Retrieves whether the choice labels should be build |
|||
* @return |
|||
*/ |
|||
bool isBuildStateValuationsSet() const; |
|||
|
|||
|
|||
// The name of the module. |
|||
static const std::string moduleName; |
|||
}; |
|||
} |
|||
} |
|||
} |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue