Browse Source

Added macros that can be used for printing and warnings. Included Dennis' fix for model checking of Markov automata. Added check methods to the settings modules that check whether the specified options are non-contradictive.

Former-commit-id: 18c1687958
main
dehnert 11 years ago
parent
commit
1f1b60e6de
  1. 4
      src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
  2. 9
      src/settings/SettingsManager.cpp
  3. 5
      src/settings/SettingsManager.h
  4. 15
      src/settings/modules/CounterexampleGeneratorSettings.cpp
  5. 4
      src/settings/modules/CounterexampleGeneratorSettings.h
  6. 12
      src/settings/modules/GeneralSettings.cpp
  7. 2
      src/settings/modules/GeneralSettings.h
  8. 12
      src/settings/modules/GlpkSettings.cpp
  9. 9
      src/settings/modules/GlpkSettings.h
  10. 32
      src/settings/modules/GmmxxEquationSolverSettings.cpp
  11. 44
      src/settings/modules/GmmxxEquationSolverSettings.h
  12. 16
      src/settings/modules/GurobiSettings.cpp
  13. 16
      src/settings/modules/GurobiSettings.h
  14. 24
      src/settings/modules/NativeEquationSolverSettings.cpp
  15. 30
      src/settings/modules/NativeEquationSolverSettings.h
  16. 2
      src/utility/cli.h
  17. 34
      src/utility/macros.h

4
src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h

@ -494,7 +494,7 @@ namespace storm {
storm::expressions::Expression constraint = storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(state));
for (auto element : transitionMatrix.getRow(nondeterministicChoiceIndices[state])) {
constraint = constraint - storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(element.getColumn()));
constraint = constraint - storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(element.getColumn())) * storm::expressions::Expression::createDoubleLiteral(element.getValue());
}
constraint = constraint + storm::expressions::Expression::createDoubleLiteral(storm::utility::constantOne<ValueType>() / exitRates[state]) * storm::expressions::Expression::createDoubleVariable("k");
@ -512,7 +512,7 @@ namespace storm {
storm::expressions::Expression constraint = storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(state));
for (auto element : transitionMatrix.getRow(choice)) {
constraint = constraint - storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(element.getColumn()));
constraint = constraint - storm::expressions::Expression::createDoubleVariable(stateToVariableNameMap.at(element.getColumn())) * storm::expressions::Expression::createDoubleLiteral(element.getValue());
}
storm::expressions::Expression rightHandSide = storm::expressions::Expression::createDoubleLiteral(storm::utility::constantZero<ValueType>());

9
src/settings/SettingsManager.cpp

@ -110,6 +110,9 @@ namespace storm {
if (optionActive) {
setOptionsArguments(activeOptionName, activeOptionIsShortName ? this->shortNameToOptions : this->longNameToOptions, argumentCache);
}
// Finally check whether all modules are okay with the current settings.
this->checkAllModules();
}
void SettingsManager::setFromConfigurationFile(std::string const& configFilename) {
@ -325,6 +328,12 @@ namespace storm {
}
}
void SettingsManager::checkAllModules() const {
for (auto const& nameModulePair : this->modules) {
nameModulePair.second->check();
}
}
SettingsManager const& manager() {
return SettingsManager::manager();
}

5
src/settings/SettingsManager.h

@ -179,6 +179,11 @@ namespace storm {
*/
static void addOptionToMap(std::string const& name, std::shared_ptr<Option> const& option, std::unordered_map<std::string, std::vector<std::shared_ptr<Option>>>& optionMap);
/*!
* Checks all modules for consistency by calling their respective check method.
*/
void checkAllModules() const;
/*!
* Retrieves the (print) length of the longest option of all modules.
*

15
src/settings/modules/CounterexampleGeneratorSettings.cpp

@ -1,6 +1,7 @@
#include "src/settings/modules/CounterexampleGeneratorSettings.h"
#include "src/settings/SettingsManager.h"
#include "src/exceptions/InvalidSettingsException.h"
namespace storm {
namespace settings {
@ -19,7 +20,7 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, schedulerCutsOptionName, true, "Sets whether to add the scheduler cuts for MILP-based minimal command counterexample generation.").build());
}
bool CounterexampleGeneratorSettings::isMinimalCommandGenerationSet() const {
bool CounterexampleGeneratorSettings::isMinimalCommandSetGenerationSet() const {
return this->getOption(minimalCommandSetOptionName).getHasOptionBeenSet();
}
@ -40,6 +41,18 @@ namespace storm {
return this->getOption(schedulerCutsOptionName).getHasOptionBeenSet();
}
bool CounterexampleGeneratorSettings::check() const {
// Ensure that the model was given either symbolically or explicitly.
STORM_LOG_THROW(!isMinimalCommandSetGenerationSet() || storm::settings::generalSettings().isSymbolicSet(), storm::exceptions::InvalidSettingsException, "For the generation of a minimal command set, the model has to be specified symbolically.");
if (isMinimalCommandSetGenerationSet()) {
STORM_LOG_WARN_COND(isUseMaxSatBasedMinimalCommandSetGenerationSet() || !isEncodeReachabilitySet(), "Encoding reachability is only available for the MaxSat-based minimal command set generation, so selecting it has no effect.");
STORM_LOG_WARN_COND(isUseMilpBasedMinimalCommandSetGenerationSet() || !isUseSchedulerCutsSet(), "Using scheduler cuts is only available for the MaxSat-based minimal command set generation, so selecting it has no effect.");
}
return true;
}
} // namespace modules
} // namespace settings
} // namespace storm

4
src/settings/modules/CounterexampleGeneratorSettings.h

@ -24,7 +24,7 @@ namespace storm {
*
* @return True iff a minimal command set counterexample is to be generated.
*/
bool isMinimalCommandGenerationSet() const;
bool isMinimalCommandSetGenerationSet() const;
/*!
* Retrieves whether the MILP-based technique is to be used to generate a minimal command set
@ -58,6 +58,8 @@ namespace storm {
*/
bool isUseSchedulerCutsSet() const;
bool check() const override;
// The name of the module.
static const std::string moduleName;

12
src/settings/modules/GeneralSettings.cpp

@ -2,6 +2,7 @@
#include "src/settings/SettingsManager.h"
#include "src/settings/SettingMemento.h"
#include "src/exceptions/InvalidSettingsException.h"
namespace storm {
namespace settings {
@ -266,6 +267,17 @@ namespace storm {
return this->getOption(statisticsOptionName).getHasOptionBeenSet();
}
bool GeneralSettings::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.");
// Make sure that one "source" for properties is given.
uint_fast64_t propertySources = 0 + (isPctlPropertySet() ? 1 : 0) + (isPctlFileSet() ? 1 : 0) + (isCslPropertySet() ? + 1 : 0) + (isCslFileSet() ? 1 : 0) + (isLtlPropertySet() ? 1 : 0) + (isLtlFileSet() ? 1 : 0);
STORM_LOG_THROW(propertySources <= 1, storm::exceptions::InvalidSettingsException, "Please specify exactly one source of properties.");
return true;
}
} // namespace modules
} // namespace settings
} // namespace storm

2
src/settings/modules/GeneralSettings.h

@ -313,6 +313,8 @@ namespace storm {
* @return True iff statistics are to be shown for counterexample generation.
*/
bool isShowStatisticsSet() const;
bool check() const override;
// The name of the module.
static const std::string moduleName;

12
src/settings/modules/GlpkSettings.cpp

@ -19,10 +19,22 @@ namespace storm {
return this->getOption(outputOptionName).getHasOptionBeenSet();
}
bool GlpkSettings::isIntegerToleranceSet() const {
return this->getOption(integerToleranceOption).getHasOptionBeenSet();
}
double GlpkSettings::getIntegerTolerance() const {
return this->getOption(integerToleranceOption).getArgumentByName("value").getValueAsDouble();
}
bool GlpkSettings::check() const {
if (isOutputSet() || isIntegerToleranceSet()) {
STORM_LOG_WARN_COND(storm::settings::generalSettings().getLpSolver() == storm::settings::modules::GeneralSettings::LpSolver::glpk, "glpk is not selected as the used LP solver, so setting options for glpk has no effect.");
}
return true;
}
} // namespace modules
} // namespace settings
} // namespace storm

9
src/settings/modules/GlpkSettings.h

@ -26,6 +26,13 @@ namespace storm {
*/
bool isOutputSet() const;
/*!
* Retrieves whether the integer tolerance has been set.
*
* @return True iff the integer tolerance has been set.
*/
bool isIntegerToleranceSet() const;
/*!
* Retrieves the integer tolerance to be used.
*
@ -33,6 +40,8 @@ namespace storm {
*/
double getIntegerTolerance() const;
bool check() const override;
// The name of the module.
static const std::string moduleName;

32
src/settings/modules/GmmxxEquationSolverSettings.cpp

@ -32,6 +32,10 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, false, "Sets whether the relative or the absolute error is considered for detecting convergence.").build());
}
bool GmmxxEquationSolverSettings::isLinearEquationSystemTechniqueSet() const {
return this->getOption(techniqueOptionName).getHasOptionBeenSet();
}
GmmxxEquationSolverSettings::LinearEquationTechnique GmmxxEquationSolverSettings::getLinearEquationSystemTechnique() const {
std::string linearEquationSystemTechniqueAsString = this->getOption(techniqueOptionName).getArgumentByName("name").getValueAsString();
if (linearEquationSystemTechniqueAsString == "bicgstab") {
@ -46,6 +50,10 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown solution technique '" << linearEquationSystemTechniqueAsString << "' selected.");
}
bool GmmxxEquationSolverSettings::isPreconditioningTechniqueSet() const {
return this->getOption(preconditionOptionName).getHasOptionBeenSet();
}
GmmxxEquationSolverSettings::PreconditioningTechnique GmmxxEquationSolverSettings::getPreconditioningTechnique() const {
std::string preconditioningTechniqueAsString = this->getOption(preconditionOptionName).getArgumentByName("name").getValueAsString();
if (preconditioningTechniqueAsString == "ilu") {
@ -58,22 +66,46 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown preconditioning technique '" << preconditioningTechniqueAsString << "' selected.");
}
bool GmmxxEquationSolverSettings::isRestartIterationCountSet() const {
return this->getOption(restartOptionName).getHasOptionBeenSet();
}
uint_fast64_t GmmxxEquationSolverSettings::getRestartIterationCount() const {
return this->getOption(restartOptionName).getArgumentByName("count").getValueAsUnsignedInteger();
}
bool GmmxxEquationSolverSettings::isMaximalIterationCountSet() const {
return this->getOption(maximalIterationsOptionName).getHasOptionBeenSet();
}
uint_fast64_t GmmxxEquationSolverSettings::getMaximalIterationCount() const {
return this->getOption(maximalIterationsOptionName).getArgumentByName("count").getValueAsUnsignedInteger();
}
bool GmmxxEquationSolverSettings::isPrecisionSet() const {
return this->getOption(precisionOptionName).getHasOptionBeenSet();
}
double GmmxxEquationSolverSettings::getPrecision() const {
return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble();
}
bool GmmxxEquationSolverSettings::isConvergenceCriterionSet() const {
return this->getOption(absoluteOptionName).getHasOptionBeenSet();
}
GmmxxEquationSolverSettings::ConvergenceCriterion GmmxxEquationSolverSettings::getConvergenceCriterion() const {
return this->getOption(absoluteOptionName).getHasOptionBeenSet() ? GmmxxEquationSolverSettings::ConvergenceCriterion::Absolute : GmmxxEquationSolverSettings::ConvergenceCriterion::Relative;
}
bool GmmxxEquationSolverSettings::check() const {
bool optionsSet = isLinearEquationSystemTechniqueSet() || isPreconditioningTechniqueSet() || isRestartIterationCountSet() | isMaximalIterationCountSet() || isPrecisionSet() || isConvergenceCriterionSet();
STORM_LOG_WARN_COND(storm::settings::generalSettings().getEquationSolver() == storm::settings::modules::GeneralSettings::EquationSolver::Gmmxx || !optionsSet, "gmm++ is not selected as the equation solver, so setting options for gmm++ has no effect.");
return true;
}
} // namespace modules
} // namespace settings
} // namespace storm

44
src/settings/modules/GmmxxEquationSolverSettings.h

@ -28,6 +28,13 @@ namespace storm {
*/
GmmxxEquationSolverSettings(storm::settings::SettingsManager& settingsManager);
/*!
* Retrieves whether the linear equation system technique has been set.
*
* @return True iff the linear equation system technique has been set.
*/
bool isLinearEquationSystemTechniqueSet() const;
/*!
* Retrieves the technique that is to be used for solving systems of linear equations.
*
@ -35,6 +42,13 @@ namespace storm {
*/
LinearEquationTechnique getLinearEquationSystemTechnique() const;
/*!
* Retrieves whether the preconditioning technique has been set.
*
* @return True iff the preconditioning technique has been set.
*/
bool isPreconditioningTechniqueSet() const;
/*!
* Retrieves the technique that is to be used for preconditioning solving systems of linear equations.
*
@ -42,6 +56,13 @@ namespace storm {
*/
PreconditioningTechnique getPreconditioningTechnique() const;
/*!
* Retrieves whether the restart iteration count has been set.
*
* @return True iff the restart iteration count has been set.
*/
bool isRestartIterationCountSet() const;
/*!
* Retrieves the number of iterations after which restarted techniques are to be restarted.
*
@ -49,6 +70,13 @@ namespace storm {
*/
uint_fast64_t getRestartIterationCount() const;
/*!
* Retrieves whether the maximal iteration count has been set.
*
* @return True iff the maximal iteration count has been set.
*/
bool isMaximalIterationCountSet() const;
/*!
* Retrieves the maximal number of iterations to perform until giving up on converging.
*
@ -56,6 +84,13 @@ namespace storm {
*/
uint_fast64_t getMaximalIterationCount() const;
/*!
* Retrieves whether the precision has been set.
*
* @return True iff the precision has been set.
*/
bool isPrecisionSet() const;
/*!
* Retrieves the precision that is used for detecting convergence.
*
@ -63,6 +98,13 @@ namespace storm {
*/
double getPrecision() const;
/*!
* Retrieves whether the convergence criterion has been set.
*
* @return True iff the convergence criterion has been set.
*/
bool isConvergenceCriterionSet() const;
/*!
* Retrieves the selected convergence criterion.
*
@ -70,6 +112,8 @@ namespace storm {
*/
ConvergenceCriterion getConvergenceCriterion() const;
bool check() const override;
// The name of the module.
static const std::string moduleName;

16
src/settings/modules/GurobiSettings.cpp

@ -19,10 +19,18 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, integerToleranceOption, true, "Sets Gurobi's precision for integer variables.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
}
bool GurobiSettings::isIntegerToleranceSet() const {
return this->getOption(integerToleranceOption).getHasOptionBeenSet();
}
double GurobiSettings::getIntegerTolerance() const {
return this->getOption(integerToleranceOption).getArgumentByName("value").getValueAsDouble();
}
bool GurobiSettings::isNumberOfThreadsSet() const {
return this->getOption(threadsOption).getHasOptionBeenSet();
}
uint_fast64_t GurobiSettings::getNumberOfThreads() const {
return this->getOption(threadsOption).getArgumentByName("count").getValueAsUnsignedInteger();
}
@ -31,6 +39,14 @@ namespace storm {
return this->getOption(outputOption).getHasOptionBeenSet();
}
bool GurobiSettings::check() const {
if (isOutputSet() || isIntegerToleranceSet() || isNumberOfThreadsSet()) {
STORM_LOG_WARN_COND(storm::settings::generalSettings().getLpSolver() == storm::settings::modules::GeneralSettings::LpSolver::Gurobi, "Gurobi is not selected as the used LP solver, so setting options for Gurobi has no effect.");
}
return true;
}
} // namespace modules
} // namespace settings
} // namespace storm

16
src/settings/modules/GurobiSettings.h

@ -19,6 +19,13 @@ namespace storm {
*/
GurobiSettings(storm::settings::SettingsManager& settingsManager);
/*!
* Retrieves whether the integer tolerance has been set.
*
* @return True iff the integer tolerance has been set.
*/
bool isIntegerToleranceSet() const;
/*!
* Retrieves the integer tolerance to be used.
*
@ -26,6 +33,13 @@ namespace storm {
*/
double getIntegerTolerance() const;
/*!
* Retrieves whether the number of threads has been set.
*
* @return True iff the number of threads has been set.
*/
bool isNumberOfThreadsSet() const;
/*!
* Retrieves the maximal number of threads Gurobi is allowed to use.
*
@ -40,6 +54,8 @@ namespace storm {
*/
bool isOutputSet() const;
bool check() const override;
// The name of the module.
static const std::string moduleName;

24
src/settings/modules/NativeEquationSolverSettings.cpp

@ -24,6 +24,10 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, false, "Sets whether the relative or the absolute error is considered for detecting convergence.").build());
}
bool NativeEquationSolverSettings::isLinearEquationSystemTechniqueSet() const {
return this->getOption(techniqueOptionName).getHasOptionBeenSet();
}
NativeEquationSolverSettings::LinearEquationTechnique NativeEquationSolverSettings::getLinearEquationSystemTechnique() const {
std::string linearEquationSystemTechniqueAsString = this->getOption(techniqueOptionName).getArgumentByName("name").getValueAsString();
if (linearEquationSystemTechniqueAsString == "jacobi") {
@ -32,18 +36,38 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown solution technique '" << linearEquationSystemTechniqueAsString << "' selected.");
}
bool NativeEquationSolverSettings::isMaximalIterationCountSet() const {
return this->getOption(maximalIterationsOptionName).getHasOptionBeenSet();
}
uint_fast64_t NativeEquationSolverSettings::getMaximalIterationCount() const {
return this->getOption(maximalIterationsOptionName).getArgumentByName("count").getValueAsUnsignedInteger();
}
bool NativeEquationSolverSettings::isPrecisionSet() const {
return this->getOption(precisionOptionName).getHasOptionBeenSet();
}
double NativeEquationSolverSettings::getPrecision() const {
return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble();
}
bool NativeEquationSolverSettings::isConvergenceCriterionSet() const {
return this->getOption(absoluteOptionName).getHasOptionBeenSet();
}
NativeEquationSolverSettings::ConvergenceCriterion NativeEquationSolverSettings::getConvergenceCriterion() const {
return this->getOption(absoluteOptionName).getHasOptionBeenSet() ? NativeEquationSolverSettings::ConvergenceCriterion::Absolute : NativeEquationSolverSettings::ConvergenceCriterion::Relative;
}
bool NativeEquationSolverSettings::check() const {
bool optionSet = isLinearEquationSystemTechniqueSet() || isMaximalIterationCountSet() || isPrecisionSet() || isConvergenceCriterionSet();
STORM_LOG_WARN_COND(storm::settings::generalSettings().getEquationSolver() == storm::settings::modules::GeneralSettings::EquationSolver::Native || !optionSet, "Native is not selected as the equation solver, so setting options for native has no effect.");
return true;
}
} // namespace modules
} // namespace settings
} // namespace storm

30
src/settings/modules/NativeEquationSolverSettings.h

@ -25,6 +25,13 @@ namespace storm {
*/
NativeEquationSolverSettings(storm::settings::SettingsManager& settingsManager);
/*!
* Retrieves whether the linear equation system technique has been set.
*
* @return True iff the linear equation system technique has been set.
*/
bool isLinearEquationSystemTechniqueSet() const;
/*!
* Retrieves the technique that is to be used for solving systems of linear equations.
*
@ -32,6 +39,13 @@ namespace storm {
*/
LinearEquationTechnique getLinearEquationSystemTechnique() const;
/*!
* Retrieves whether the maximal iteration count has been set.
*
* @return True iff the maximal iteration count has been set.
*/
bool isMaximalIterationCountSet() const;
/*!
* Retrieves the maximal number of iterations to perform until giving up on converging.
*
@ -39,6 +53,13 @@ namespace storm {
*/
uint_fast64_t getMaximalIterationCount() const;
/*!
* Retrieves whether the precision has been set.
*
* @return True iff the precision has been set.
*/
bool isPrecisionSet() const;
/*!
* Retrieves the precision that is used for detecting convergence.
*
@ -46,6 +67,13 @@ namespace storm {
*/
double getPrecision() const;
/*!
* Retrieves whether the convergence criterion has been set.
*
* @return True iff the convergence criterion has been set.
*/
bool isConvergenceCriterionSet() const;
/*!
* Retrieves the selected convergence criterion.
*
@ -53,6 +81,8 @@ namespace storm {
*/
ConvergenceCriterion getConvergenceCriterion() const;
bool check() const override;
// The name of the module.
static const std::string moduleName;

2
src/utility/cli.h

@ -259,7 +259,7 @@ namespace storm {
}
void generateCounterexample(std::shared_ptr<storm::models::AbstractModel<double>> model, std::shared_ptr<storm::properties::prctl::AbstractPrctlFormula<double>> const& formula) {
if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandGenerationSet()) {
if (storm::settings::counterexampleGeneratorSettings().isMinimalCommandSetGenerationSet()) {
STORM_LOG_THROW(model->getType() == storm::models::MDP, storm::exceptions::InvalidTypeException, "Minimal command set generation is only available for MDPs.");
STORM_LOG_THROW(storm::settings::generalSettings().isSymbolicSet(), storm::exceptions::InvalidSettingsException, "Minimal command set generation is only available for symbolic models.");

34
src/utility/macros.h

@ -44,14 +44,48 @@ extern log4cplus::Logger logger;
LOG4CPLUS_WARN(logger, message); \
} while (false)
#define STORM_LOG_WARN_COND(cond, message) \
{ \
if (!(cond)) { \
LOG4CPLUS_WARN(logger, message); \
} \
} while (false)
#define STORM_LOG_INFO(message) \
{ \
LOG4CPLUS_INFO(logger, message); \
} while (false)
#define STORM_LOG_INFO_COND(cond, message) \
{ \
if (!(cond)) { \
LOG4CPLUS_INFO(logger, message); \
} \
} while (false)
#define STORM_LOG_ERROR(message) \
{ \
LOG4CPLUS_ERROR(logger, message); \
} while (false)
#define STORM_LOG_ERROR_COND(cond, message) \
{ \
if (!(cond)) { \
LOG4CPLUS_ERROR(logger, message); \
} \
} while (false)
/*!
* Define the macros that print information and optionally also log it.
*/
#define STORM_PRINT(message) \
{ \
STORM_LOG_INFO(message); \
}
#define STORM_PRINT_AND_LOG(message) \
{ \
STORM_PRINT(message); \
}
#endif /* STORM_UTILITY_MACROS_H_ */
Loading…
Cancel
Save