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

fix dft-to-gspn regarding properties, now compiles again, and changed settings: Properties are now in IOSettings (should not change usage)

main
sjunges 8 years ago
parent
488aaeaa58
commit
8fc0033bb2
7 changed files with 65 additions and 58 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. 11
      src/storm-dft-cli/storm-dyftee.cpp
  2. 4
      src/storm-gspn-cli/storm-gspn.cpp
  3. 14
      src/storm/cli/cli.cpp
  4. 18
      src/storm/settings/modules/GeneralSettings.cpp
  5. 23
      src/storm/settings/modules/GeneralSettings.h
  6. 19
      src/storm/settings/modules/IOSettings.cpp
  7. 34
      src/storm/settings/modules/IOSettings.h

11
src/storm-dft-cli/storm-dyftee.cpp
View File

@ -127,6 +127,7 @@ int main(const int argc, const char** argv) {
storm::settings::modules::DFTSettings const& dftSettings = storm::settings::getModule<storm::settings::modules::DFTSettings>();
storm::settings::modules::GeneralSettings const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
storm::settings::modules::IOSettings const& ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
if (!dftSettings.isDftFileSet() && !dftSettings.isDftJsonFileSet()) {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
}
@ -147,9 +148,9 @@ int main(const int argc, const char** argv) {
uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId();
storm::handleGSPNExportSettings(*gspn);
std::shared_ptr<storm::expressions::ExpressionManager> exprManager(new storm::expressions::ExpressionManager());
storm::builder::JaniGSPNBuilder builder(*gspn, exprManager);
std::shared_ptr<storm::expressions::ExpressionManager> const& exprManager = gspn->getExpressionManager();
storm::builder::JaniGSPNBuilder builder(*gspn);
storm::jani::Model* model = builder.build();
storm::jani::Variable const& topfailedVar = builder.getPlaceVariable(toplevelFailedPlace);
@ -203,9 +204,9 @@ int main(const int argc, const char** argv) {
std::string operatorType = "";
std::string targetFormula = "";
if (generalSettings.isPropertySet()) {
if (ioSettings.isPropertySet()) {
STORM_LOG_THROW(!dftSettings.usePropExpectedTime() && !dftSettings.usePropProbability() && !dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given.");
pctlFormula = generalSettings.getProperty();
pctlFormula = ioSettings.getProperty();
} else if (dftSettings.usePropExpectedTime()) {
STORM_LOG_THROW(!dftSettings.usePropProbability() && !dftSettings.usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given.");
operatorType = "T";

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

@ -92,8 +92,8 @@ int main(const int argc, const char **argv) {
auto gspn = parser.parse(storm::settings::getModule<storm::settings::modules::GSPNSettings>().getGspnFilename());
std::string formulaString = "";
if (!storm::settings::getModule<storm::settings::modules::GeneralSettings>().isPropertySet()) {
formulaString = storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty();
if (!storm::settings::getModule<storm::settings::modules::IOSettings>().isPropertySet()) {
formulaString = storm::settings::getModule<storm::settings::modules::IOSettings>().getProperty();
}
boost::optional<std::set<std::string>> propertyFilter;
storm::parser::FormulaParser formulaParser(gspn->getExpressionManager());

14
src/storm/cli/cli.cpp
View File

@ -198,9 +198,9 @@ namespace storm {
}
boost::optional<std::set<std::string>> propertyFilter;
std::string propertyFilterString = storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPropertyFilter();
std::string propertyFilterString = storm::settings::getModule<storm::settings::modules::IOSettings>().getPropertyFilter();
if (propertyFilterString != "all") {
propertyFilter = storm::parsePropertyFilter(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPropertyFilter());
propertyFilter = storm::parsePropertyFilter(storm::settings::getModule<storm::settings::modules::IOSettings>().getPropertyFilter());
}
auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
@ -245,9 +245,9 @@ namespace storm {
// Then proceed to parsing the properties (if given), since the model we are building may depend on the property.
STORM_LOG_TRACE("Parsing properties.");
if (generalSettings.isPropertySet()) {
if (ioSettings.isPropertySet()) {
if (model.isJaniModel()) {
properties = storm::parsePropertiesForJaniModel(generalSettings.getProperty(), model.asJaniModel(), propertyFilter);
properties = storm::parsePropertiesForJaniModel(ioSettings.getProperty(), model.asJaniModel(), propertyFilter);
if (labelRenaming) {
std::vector<storm::jani::Property> amendedProperties;
@ -257,7 +257,7 @@ namespace storm {
properties = std::move(amendedProperties);
}
} else {
properties = storm::parsePropertiesForPrismProgram(generalSettings.getProperty(), model.asPrismProgram(), propertyFilter);
properties = storm::parsePropertiesForPrismProgram(ioSettings.getProperty(), model.asPrismProgram(), propertyFilter);
}
constantDefinitions = model.parseConstantDefinitions(constantDefinitionString);
@ -297,8 +297,8 @@ namespace storm {
// If the model is given in an explicit format, we parse the properties without allowing expressions
// in formulas.
std::vector<storm::jani::Property> properties;
if (generalSettings.isPropertySet()) {
properties = storm::parsePropertiesForExplicit(generalSettings.getProperty(), propertyFilter);
if (ioSettings.isPropertySet()) {
properties = storm::parsePropertiesForExplicit(ioSettings.getProperty(), propertyFilter);
}
buildAndCheckExplicitModel<double>(properties, true);

18
src/storm/settings/modules/GeneralSettings.cpp
View File

@ -26,8 +26,6 @@ namespace storm {
const std::string GeneralSettings::precisionOptionShortName = "eps";
const std::string GeneralSettings::configOptionName = "config";
const std::string GeneralSettings::configOptionShortName = "c";
const std::string GeneralSettings::propertyOptionName = "prop";
const std::string GeneralSettings::propertyOptionShortName = "prop";
const std::string GeneralSettings::bisimulationOptionName = "bisimulation";
const std::string GeneralSettings::bisimulationOptionShortName = "bisim";
const std::string GeneralSettings::parametricOptionName = "parametric";
@ -43,11 +41,6 @@ namespace storm {
.addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to use.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, configOptionName, false, "If given, this file will be read and parsed for additional configuration settings.").setShortName(configOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the configuration.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, propertyOptionName, false, "Specifies the properties to be checked on the model.").setShortName(propertyOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("property or filename", "The formula or the file containing the formulas.").build())
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filter", "The names of the properties to check.").setDefaultValueString("all").build())
.build());
this->addOption(storm::settings::OptionBuilder(moduleName, parametricRegionOptionName, false, "Sets whether to use the parametric Region engine.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, bisimulationOptionName, false, "Sets whether to perform bisimulation minimization.").setShortName(bisimulationOptionShortName).build());
this->addOption(storm::settings::OptionBuilder(moduleName, parametricOptionName, false, "Sets whether to enable parametric model checking.").build());
@ -81,18 +74,7 @@ namespace storm {
std::string GeneralSettings::getConfigFilename() const {
return this->getOption(configOptionName).getArgumentByName("filename").getValueAsString();
}
bool GeneralSettings::isPropertySet() const {
return this->getOption(propertyOptionName).getHasOptionBeenSet();
}
std::string GeneralSettings::getProperty() const {
return this->getOption(propertyOptionName).getArgumentByName("property or filename").getValueAsString();
}
std::string GeneralSettings::getPropertyFilter() const {
return this->getOption(propertyOptionName).getArgumentByName("filter").getValueAsString();
}
bool GeneralSettings::isBisimulationSet() const {
return this->getOption(bisimulationOptionName).getHasOptionBeenSet();

23
src/storm/settings/modules/GeneralSettings.h
View File

@ -70,27 +70,6 @@ namespace storm {
* @return The name of the file that is to be scanned for settings.
*/
std::string getConfigFilename() const;
/*!
* Retrieves whether the property option was set.
*
* @return True if the property option was set.
*/
bool isPropertySet() const;
/*!
* Retrieves the property specified with the property option.
*
* @return The property specified with the property option.
*/
std::string getProperty() const;
/*!
* Retrieves the property filter.
*
* @return The property filter.
*/
std::string getPropertyFilter() const;
/*!
* Retrieves whether the option to perform bisimulation minimization is set.
@ -146,8 +125,6 @@ namespace storm {
static const std::string precisionOptionShortName;
static const std::string configOptionName;
static const std::string configOptionShortName;
static const std::string propertyOptionName;
static const std::string propertyOptionShortName;
static const std::string bisimulationOptionName;
static const std::string bisimulationOptionShortName;
static const std::string parametricOptionName;

19
src/storm/settings/modules/IOSettings.cpp
View File

@ -40,6 +40,8 @@ namespace storm {
const std::string IOSettings::fullModelBuildOptionName = "buildfull";
const std::string IOSettings::janiPropertyOptionName = "janiproperty";
const std::string IOSettings::janiPropertyOptionShortName = "jprop";
const std::string IOSettings::propertyOptionName = "prop";
const std::string IOSettings::propertyOptionShortName = "prop";
IOSettings::IOSettings() : ModuleSettings(moduleName) {
@ -59,7 +61,10 @@ namespace storm {
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, noBuildOptionName, false, "If set, do not build the model.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, propertyOptionName, false, "Specifies the properties to be checked on the model.").setShortName(propertyOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("property or filename", "The formula or the file containing the formulas.").build())
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filter", "The names of the properties to check.").setDefaultValueString("all").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.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(explorationOrders)).setDefaultValueString("bfs").build()).build());
@ -207,6 +212,18 @@ namespace storm {
return this->getOption(noBuildOptionName).getHasOptionBeenSet();
}
bool IOSettings::isPropertySet() const {
return this->getOption(propertyOptionName).getHasOptionBeenSet();
}
std::string IOSettings::getProperty() const {
return this->getOption(propertyOptionName).getArgumentByName("property or filename").getValueAsString();
}
std::string IOSettings::getPropertyFilter() const {
return this->getOption(propertyOptionName).getArgumentByName("filter").getValueAsString();
}
void IOSettings::finalize() {
}

34
src/storm/settings/modules/IOSettings.h
View File

@ -211,11 +211,39 @@ namespace storm {
* @return The string that defines the constants of a symbolic model.
*/
std::string getConstantDefinitionString() const;
/*!
* Retrieves whether the jani-property option was set
* @return
*/
bool isJaniPropertiesSet() const;
/*!
* @return The names of the jani properties to check
*/
std::vector<std::string> getJaniProperties() const;
/*!
* Retrieves whether the property option was set.
*
* @return True if the property option was set.
*/
bool isPropertySet() const;
/*!
* Retrieves the property specified with the property option.
*
* @return The property specified with the property option.
*/
std::string getProperty() const;
/*!
* Retrieves the property filter.
*
* @return The property filter.
*/
std::string getPropertyFilter() const;
/*!
* Retrieves whether the PRISM compatibility mode was enabled.
*
@ -266,6 +294,8 @@ namespace storm {
static const std::string noBuildOptionName;
static const std::string janiPropertyOptionName;
static const std::string janiPropertyOptionShortName;
static const std::string propertyOptionName;
static const std::string propertyOptionShortName;
};
} // namespace modules

Write Preview
Loading…
Cancel
Save