Browse Source

fixed two issues in jit builder: a) respect environment variable (instead of c++); b) casting integer variables to doubles when evaluating label expressions to avoid integer division

tempestpy_adaptions
dehnert 8 years ago
parent
commit
64ddf12558
  1. 4
      src/storm-dft-cli/storm-dyftee.cpp
  2. 10
      src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
  3. 1
      src/storm/settings/SettingsManager.cpp

4
src/storm-dft-cli/storm-dyftee.cpp

@ -48,7 +48,7 @@ void analyzeDFT(std::string filename, std::string property, bool symred, bool al
storm::parser::DFTGalileoParser<ValueType> parser;
storm::storage::DFT<ValueType> dft = parser.parseDFT(filename);
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::parseFormulasForExplicit(property);
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForExplicit(property));
STORM_LOG_ASSERT(formulas.size() == 1, "Wrong number of formulas.");
storm::modelchecker::DFTModelChecker<ValueType> modelChecker;
@ -156,7 +156,7 @@ int main(const int argc, const char** argv) {
storm::expressions::Expression targetExpression = exprManager->integer(1) == topfailedVar.getExpressionVariable().getExpression();
auto evtlFormula = std::make_shared<storm::logic::AtomicExpressionFormula>(targetExpression);
auto tbFormula = std::make_shared<storm::logic::BoundedUntilFormula>(std::make_shared<storm::logic::BooleanLiteralFormula>(true), evtlFormula, 0.0, 10.0);
auto tbFormula = std::make_shared<storm::logic::BoundedUntilFormula>(std::make_shared<storm::logic::BooleanLiteralFormula>(true), evtlFormula, storm::logic::TimeBound(false, exprManager->integer(0)), storm::logic::TimeBound(false, exprManager->integer(10)), storm::logic::TimeBoundType::Time);
auto tbUntil = std::make_shared<storm::logic::ProbabilityOperatorFormula>(tbFormula);
auto evFormula = std::make_shared<storm::logic::EventuallyFormula>(evtlFormula, storm::logic::FormulaContext::Time);

10
src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp

@ -50,8 +50,14 @@ namespace storm {
if (settings.isCompilerSet()) {
compiler = settings.getCompiler();
} else {
const char* cxxEnv = std::getenv("CXX");
if (cxxEnv != nullptr) {
compiler = std::string(cxxEnv);
}
if (compiler.empty()) {
compiler = "c++";
}
}
if (settings.isCompilerFlagsSet()) {
compilerFlags = settings.getCompilerFlags();
} else {
@ -1509,7 +1515,7 @@ namespace storm {
if (this->options.isBuildAllLabelsSet() || this->options.getLabelNames().find(variable.getName()) != this->options.getLabelNames().end()) {
cpptempl::data_map label;
label["name"] = variable.getName();
label["predicate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(model.getLabelExpression(variable.asBooleanVariable(), parallelAutomata)), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName));
label["predicate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(model.getLabelExpression(variable.asBooleanVariable(), parallelAutomata)), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastDouble));
labels.push_back(label);
}
}
@ -1518,7 +1524,7 @@ namespace storm {
for (auto const& expression : this->options.getExpressionLabels()) {
cpptempl::data_map label;
label["name"] = expression.toString();
label["predicate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(expression), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName));
label["predicate"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(expression), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastDouble));
labels.push_back(label);
}

1
src/storm/settings/SettingsManager.cpp

@ -349,6 +349,7 @@ namespace storm {
void SettingsManager::setOptionArguments(std::string const& optionName, std::shared_ptr<Option> option, std::vector<std::string> const& argumentCache) {
STORM_LOG_THROW(argumentCache.size() <= option->getArgumentCount(), storm::exceptions::OptionParserException, "Too many arguments for option '" << optionName << "'.");
STORM_LOG_THROW(!option->getHasOptionBeenSet(), storm::exceptions::OptionParserException, "Option '" << optionName << "' is set multiple times.");
// Now set the provided argument values one by one.
for (uint_fast64_t i = 0; i < argumentCache.size(); ++i) {

Loading…
Cancel
Save