Mavo
9 years ago
18 changed files with 419 additions and 337 deletions
-
7src/builder/ExplicitPrismModelBuilder.cpp
-
13src/cli/cli.cpp
-
2src/cli/entrypoints.h
-
6src/settings/SettingsManager.cpp
-
9src/settings/SettingsManager.h
-
4src/settings/modules/CounterexampleGeneratorSettings.cpp
-
151src/settings/modules/IOSettings.cpp
-
194src/settings/modules/IOSettings.h
-
127src/settings/modules/MarkovChainSettings.cpp
-
156src/settings/modules/MarkovChainSettings.h
-
6src/storage/prism/Program.cpp
-
7src/utility/storm.h
-
6test/functional/builder/DdPrismModelBuilderTest.cpp
-
4test/functional/builder/ExplicitPrismModelBuilderTest.cpp
-
12test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
-
20test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
-
12test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
-
20test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
@ -0,0 +1,151 @@ |
|||||
|
#include "src/settings/modules/IOSettings.h"
|
||||
|
|
||||
|
#include "src/settings/SettingsManager.h"
|
||||
|
#include "src/settings/SettingMemento.h"
|
||||
|
#include "src/settings/Option.h"
|
||||
|
#include "src/settings/OptionBuilder.h"
|
||||
|
#include "src/settings/ArgumentBuilder.h"
|
||||
|
#include "src/settings/Argument.h"
|
||||
|
#include "src/exceptions/InvalidSettingsException.h"
|
||||
|
|
||||
|
namespace storm { |
||||
|
namespace settings { |
||||
|
namespace modules { |
||||
|
|
||||
|
const std::string IOSettings::moduleName = "io"; |
||||
|
const std::string IOSettings::exportDotOptionName = "exportdot"; |
||||
|
const std::string IOSettings::exportMatOptionName = "exportmat"; |
||||
|
const std::string IOSettings::explicitOptionName = "explicit"; |
||||
|
const std::string IOSettings::explicitOptionShortName = "exp"; |
||||
|
const std::string IOSettings::symbolicOptionName = "symbolic"; |
||||
|
const std::string IOSettings::symbolicOptionShortName = "s"; |
||||
|
const std::string IOSettings::explorationOrderOptionName = "explorder"; |
||||
|
const std::string IOSettings::explorationOrderOptionShortName = "eo"; |
||||
|
const std::string IOSettings::transitionRewardsOptionName = "transrew"; |
||||
|
const std::string IOSettings::stateRewardsOptionName = "staterew"; |
||||
|
const std::string IOSettings::choiceLabelingOptionName = "choicelab"; |
||||
|
const std::string IOSettings::constantsOptionName = "constants"; |
||||
|
const std::string IOSettings::constantsOptionShortName = "const"; |
||||
|
const std::string IOSettings::prismCompatibilityOptionName = "prismcompat"; |
||||
|
const std::string IOSettings::prismCompatibilityOptionShortName = "pc"; |
||||
|
|
||||
|
IOSettings::IOSettings() : ModuleSettings(moduleName) { |
||||
|
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, exportDotOptionName, "", "If given, the loaded model will be written to the specified file in the dot format.") |
||||
|
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build()); |
||||
|
this->addOption(storm::settings::OptionBuilder(moduleName, exportMatOptionName, "", "If given, the loaded model will be written to the specified file in the mat format.") |
||||
|
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the file to which the model is to be writen.").build()).build()); |
||||
|
this->addOption(storm::settings::OptionBuilder(moduleName, explicitOptionName, false, "Parses the model given in an explicit (sparse) representation.").setShortName(explicitOptionShortName) |
||||
|
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("transition filename", "The name of the file from which to read the transitions.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()) |
||||
|
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("labeling filename", "The name of the file from which to read the state labeling.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); |
||||
|
this->addOption(storm::settings::OptionBuilder(moduleName, symbolicOptionName, false, "Parses the model given in a symbolic representation.").setShortName(symbolicOptionShortName) |
||||
|
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the symbolic model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); |
||||
|
|
||||
|
std::vector<std::string> explorationOrders = {"dfs", "bfs"}; |
||||
|
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. Available are: dfs and bfs.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(explorationOrders)).setDefaultValueString("bfs").build()).build()); |
||||
|
|
||||
|
this->addOption(storm::settings::OptionBuilder(moduleName, transitionRewardsOptionName, false, "If given, the transition rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").") |
||||
|
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the transition rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); |
||||
|
this->addOption(storm::settings::OptionBuilder(moduleName, stateRewardsOptionName, false, "If given, the state rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").") |
||||
|
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the state rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); |
||||
|
this->addOption(storm::settings::OptionBuilder(moduleName, choiceLabelingOptionName, false, "If given, the choice labels are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").") |
||||
|
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the choice labels.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); |
||||
|
this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that Note that this requires the model to be given as an symbolic model (i.e., via --" + symbolicOptionName + ").").setShortName(constantsOptionShortName) |
||||
|
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build()); |
||||
|
} |
||||
|
|
||||
|
bool IOSettings::isExportDotSet() const { |
||||
|
return this->getOption(exportDotOptionName).getHasOptionBeenSet(); |
||||
|
} |
||||
|
|
||||
|
std::string IOSettings::getExportDotFilename() const { |
||||
|
return this->getOption(exportDotOptionName).getArgumentByName("filename").getValueAsString(); |
||||
|
} |
||||
|
|
||||
|
bool IOSettings::isExplicitSet() const { |
||||
|
return this->getOption(explicitOptionName).getHasOptionBeenSet(); |
||||
|
} |
||||
|
|
||||
|
std::string IOSettings::getTransitionFilename() const { |
||||
|
return this->getOption(explicitOptionName).getArgumentByName("transition filename").getValueAsString(); |
||||
|
} |
||||
|
|
||||
|
std::string IOSettings::getLabelingFilename() const { |
||||
|
return this->getOption(explicitOptionName).getArgumentByName("labeling filename").getValueAsString(); |
||||
|
} |
||||
|
|
||||
|
bool IOSettings::isSymbolicSet() const { |
||||
|
return this->getOption(symbolicOptionName).getHasOptionBeenSet(); |
||||
|
} |
||||
|
|
||||
|
std::string IOSettings::getSymbolicModelFilename() const { |
||||
|
return this->getOption(symbolicOptionName).getArgumentByName("filename").getValueAsString(); |
||||
|
} |
||||
|
|
||||
|
bool IOSettings::isExplorationOrderSet() const { |
||||
|
return this->getOption(explorationOrderOptionName).getHasOptionBeenSet(); |
||||
|
} |
||||
|
|
||||
|
storm::builder::ExplorationOrder IOSettings::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 IOSettings::isTransitionRewardsSet() const { |
||||
|
return this->getOption(transitionRewardsOptionName).getHasOptionBeenSet(); |
||||
|
} |
||||
|
|
||||
|
std::string IOSettings::getTransitionRewardsFilename() const { |
||||
|
return this->getOption(transitionRewardsOptionName).getArgumentByName("filename").getValueAsString(); |
||||
|
} |
||||
|
|
||||
|
bool IOSettings::isStateRewardsSet() const { |
||||
|
return this->getOption(stateRewardsOptionName).getHasOptionBeenSet(); |
||||
|
} |
||||
|
|
||||
|
std::string IOSettings::getStateRewardsFilename() const { |
||||
|
return this->getOption(stateRewardsOptionName).getArgumentByName("filename").getValueAsString(); |
||||
|
} |
||||
|
|
||||
|
bool IOSettings::isChoiceLabelingSet() const { |
||||
|
return this->getOption(choiceLabelingOptionName).getHasOptionBeenSet(); |
||||
|
} |
||||
|
|
||||
|
std::string IOSettings::getChoiceLabelingFilename() const { |
||||
|
return this->getOption(choiceLabelingOptionName).getArgumentByName("filename").getValueAsString(); |
||||
|
} |
||||
|
|
||||
|
std::unique_ptr<storm::settings::SettingMemento> IOSettings::overridePrismCompatibilityMode(bool stateToSet) { |
||||
|
return this->overrideOption(prismCompatibilityOptionName, stateToSet); |
||||
|
} |
||||
|
|
||||
|
bool IOSettings::isConstantsSet() const { |
||||
|
return this->getOption(constantsOptionName).getHasOptionBeenSet(); |
||||
|
} |
||||
|
|
||||
|
std::string IOSettings::getConstantDefinitionString() const { |
||||
|
return this->getOption(constantsOptionName).getArgumentByName("values").getValueAsString(); |
||||
|
} |
||||
|
|
||||
|
bool IOSettings::isPrismCompatibilityEnabled() const { |
||||
|
return this->getOption(prismCompatibilityOptionName).getHasOptionBeenSet(); |
||||
|
} |
||||
|
|
||||
|
void IOSettings::finalize() { |
||||
|
} |
||||
|
|
||||
|
bool IOSettings::check() const { |
||||
|
// Ensure that the model was given either symbolically or explicitly.
|
||||
|
STORM_LOG_THROW(!isSymbolicSet() || !isExplicitSet(), storm::exceptions::InvalidSettingsException, "The model may be either given in an explicit or a symbolic format, but not both."); |
||||
|
return true; |
||||
|
} |
||||
|
|
||||
|
} // namespace modules
|
||||
|
} // namespace settings
|
||||
|
} // namespace storm
|
||||
@ -0,0 +1,194 @@ |
|||||
|
#ifndef STORM_SETTINGS_MODULES_IOSETTINGS_H_ |
||||
|
#define STORM_SETTINGS_MODULES_IOSETTINGS_H_ |
||||
|
|
||||
|
#include "storm-config.h" |
||||
|
#include "src/settings/modules/ModuleSettings.h" |
||||
|
|
||||
|
#include "src/builder/ExplorationOrder.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace settings { |
||||
|
namespace modules { |
||||
|
|
||||
|
/*! |
||||
|
* This class represents the markov chain settings. |
||||
|
*/ |
||||
|
class IOSettings : public ModuleSettings { |
||||
|
public: |
||||
|
|
||||
|
/*! |
||||
|
* Creates a new set of IO settings. |
||||
|
*/ |
||||
|
IOSettings(); |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves whether the export-to-dot option was set. |
||||
|
* |
||||
|
* @return True if the export-to-dot option was set. |
||||
|
*/ |
||||
|
bool isExportDotSet() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves the name in which to write the model in dot format, if the export-to-dot option was set. |
||||
|
* |
||||
|
* @return The name of the file in which to write the exported model. |
||||
|
*/ |
||||
|
std::string getExportDotFilename() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves whether the explicit option was set. |
||||
|
* |
||||
|
* @return True if the explicit option was set. |
||||
|
*/ |
||||
|
bool isExplicitSet() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves the name of the file that contains the transitions if the model was given using the explicit |
||||
|
* option. |
||||
|
* |
||||
|
* @return The name of the file that contains the transitions. |
||||
|
*/ |
||||
|
std::string getTransitionFilename() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves the name of the file that contains the state labeling if the model was given using the |
||||
|
* explicit option. |
||||
|
* |
||||
|
* @return The name of the file that contains the state labeling. |
||||
|
*/ |
||||
|
std::string getLabelingFilename() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves whether the symbolic option was set. |
||||
|
* |
||||
|
* @return True if the symbolic option was set. |
||||
|
*/ |
||||
|
bool isSymbolicSet() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves the name of the file that contains the symbolic model specification if the model was given |
||||
|
* using the symbolic option. |
||||
|
* |
||||
|
* @return The name of the file that contains the symbolic model specification. |
||||
|
*/ |
||||
|
std::string getSymbolicModelFilename() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves whether the model exploration order was set. |
||||
|
* |
||||
|
* @return True if the model exploration option was set. |
||||
|
*/ |
||||
|
bool isExplorationOrderSet() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves the exploration order if it was set. |
||||
|
* |
||||
|
* @return The chosen exploration order. |
||||
|
*/ |
||||
|
storm::builder::ExplorationOrder getExplorationOrder() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves whether the transition reward option was set. |
||||
|
* |
||||
|
* @return True if the transition reward option was set. |
||||
|
*/ |
||||
|
bool isTransitionRewardsSet() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves the name of the file that contains the transition rewards if the model was given using the |
||||
|
* explicit option. |
||||
|
* |
||||
|
* @return The name of the file that contains the transition rewards. |
||||
|
*/ |
||||
|
std::string getTransitionRewardsFilename() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves whether the state reward option was set. |
||||
|
* |
||||
|
* @return True if the state reward option was set. |
||||
|
*/ |
||||
|
bool isStateRewardsSet() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves the name of the file that contains the state rewards if the model was given using the |
||||
|
* explicit option. |
||||
|
* |
||||
|
* @return The name of the file that contains the state rewards. |
||||
|
*/ |
||||
|
std::string getStateRewardsFilename() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves whether the choice labeling option was set. |
||||
|
* |
||||
|
* @return True iff the choice labeling option was set. |
||||
|
*/ |
||||
|
bool isChoiceLabelingSet() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves the name of the file that contains the choice labeling |
||||
|
* if the model was given using the explicit option. |
||||
|
* |
||||
|
* @return The name of the file that contains the choice labeling. |
||||
|
*/ |
||||
|
std::string getChoiceLabelingFilename() const; |
||||
|
|
||||
|
/*! |
||||
|
* Overrides the option to enable the PRISM compatibility mode by setting it to the specified value. As |
||||
|
* soon as the returned memento goes out of scope, the original value is restored. |
||||
|
* |
||||
|
* @param stateToSet The value that is to be set for the option. |
||||
|
* @return The memento that will eventually restore the original value. |
||||
|
*/ |
||||
|
std::unique_ptr<storm::settings::SettingMemento> overridePrismCompatibilityMode(bool stateToSet); |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves whether the export-to-dot option was set. |
||||
|
* |
||||
|
* @return True if the export-to-dot option was set. |
||||
|
*/ |
||||
|
bool isConstantsSet() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves the string that defines the constants of a symbolic model (given via the symbolic option). |
||||
|
* |
||||
|
* @return The string that defines the constants of a symbolic model. |
||||
|
*/ |
||||
|
std::string getConstantDefinitionString() const; |
||||
|
|
||||
|
/*! |
||||
|
* Retrieves whether the PRISM compatibility mode was enabled. |
||||
|
* |
||||
|
* @return True iff the PRISM compatibility mode was enabled. |
||||
|
*/ |
||||
|
bool isPrismCompatibilityEnabled() const; |
||||
|
|
||||
|
bool check() const override; |
||||
|
void finalize() override; |
||||
|
|
||||
|
// The name of the module. |
||||
|
static const std::string moduleName; |
||||
|
|
||||
|
private: |
||||
|
// Define the string names of the options as constants. |
||||
|
static const std::string exportDotOptionName; |
||||
|
static const std::string exportMatOptionName; |
||||
|
static const std::string explicitOptionName; |
||||
|
static const std::string explicitOptionShortName; |
||||
|
static const std::string symbolicOptionName; |
||||
|
static const std::string symbolicOptionShortName; |
||||
|
static const std::string explorationOrderOptionName; |
||||
|
static const std::string explorationOrderOptionShortName; |
||||
|
static const std::string transitionRewardsOptionName; |
||||
|
static const std::string stateRewardsOptionName; |
||||
|
static const std::string choiceLabelingOptionName; |
||||
|
static const std::string constantsOptionName; |
||||
|
static const std::string constantsOptionShortName; |
||||
|
static const std::string prismCompatibilityOptionName; |
||||
|
static const std::string prismCompatibilityOptionShortName; |
||||
|
}; |
||||
|
|
||||
|
} // namespace modules |
||||
|
} // namespace settings |
||||
|
} // namespace storm |
||||
|
|
||||
|
#endif /* STORM_SETTINGS_MODULES_IOSETTINGS_H_ */ |
||||
Write
Preview
Loading…
Cancel
Save
Reference in new issue