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

Removed double whitespaces in outputs

main
Matthias Volk 6 years ago
parent
78d99328b6
commit
4ee31063a4
18 changed files with 56 additions and 56 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. 2
      src/storm-conv/settings/modules/ConversionInputSettings.cpp
  2. 2
      src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h
  3. 2
      src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
  4. 2
      src/storm-dft/parser/DFTJsonParser.cpp
  5. 4
      src/storm-pars/parser/ParameterRegionParser.cpp
  6. 64
      src/storm-parsers/parser/JaniParser.cpp
  7. 2
      src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp
  8. 2
      src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp
  9. 2
      src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp
  10. 2
      src/storm/settings/modules/IOSettings.cpp
  11. 2
      src/storm/solver/SymbolicNativeLinearEquationSolver.cpp
  12. 2
      src/storm/storage/jani/ArrayEliminator.cpp
  13. 2
      src/storm/storage/jani/Edge.cpp
  14. 2
      src/storm/transformer/EndComponentEliminator.h
  15. 10
      src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp
  16. 2
      src/test/storm/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp
  17. 4
      src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp
  18. 4
      src/test/storm/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp

2
src/storm-conv/settings/modules/ConversionInputSettings.cpp
View File

@ -43,7 +43,7 @@ namespace storm {
// Jani related
this->addOption(storm::settings::OptionBuilder(moduleName, janiInputOptionName, false, "Parses the model given in the JANI format.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the JANI input.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, janiPropertyOptionName, false, "Specifies the properties from the jani model (given by --" + janiInputOptionName + ") to be checked.").setShortName(janiPropertyOptionShortName)
this->addOption(storm::settings::OptionBuilder(moduleName, janiPropertyOptionName, false, "Specifies the properties from the jani model (given by --" + janiInputOptionName + ") to be checked.").setShortName(janiPropertyOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of properties to be checked").setDefaultValueString("").build()).build());
}

2
src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h
View File

@ -1690,7 +1690,7 @@ namespace storm {
for (uint64_t i = 0; i < maximalReachabilityProbability.size(); ++i) {
STORM_LOG_THROW((strictBound && maximalReachabilityProbability[i] >= propertyThreshold[i]) || (!strictBound && maximalReachabilityProbability[i] > propertyThreshold[i]), storm::exceptions::InvalidArgumentException, "Given probability threshold " << propertyThreshold[i] << " can not be " << (strictBound ? "achieved" : "exceeded") << " in model with maximal reachability probability of " << maximalReachabilityProbability[i] << ".");
std::cout << std::endl << "Maximal property value in model is " << maximalReachabilityProbability[i] << "." << std::endl << std::endl;
std::cout << std::endl << "Maximal property value in model is " << maximalReachabilityProbability[i] << "." << std::endl << std::endl;
}
}

2
src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
View File

@ -544,7 +544,7 @@ namespace storm {
storm::utility::openFile(filename, stream);
stream << "; time point variables" << std::endl;
for (auto const &timeVarEntry : timePointVariables) {
stream << "(declare-fun " << varNames[timeVarEntry.second] << "() Int)" << std::endl;
stream << "(declare-fun " << varNames[timeVarEntry.second] << "() Int)" << std::endl;
}
stream << "; claim variables" << std::endl;
for (auto const &claimVarEntry : claimVariables) {

2
src/storm-dft/parser/DFTJsonParser.cpp
View File

@ -126,7 +126,7 @@ namespace storm {
success = false;
}
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Type name: " << type << " not recognized.");
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Type name: " << type << " not recognized.");
success = false;
}

4
src/storm-pars/parser/ParameterRegionParser.cpp
View File

@ -12,9 +12,9 @@ namespace storm {
template<typename ParametricType>
void ParameterRegionParser<ParametricType>::parseParameterBoundaries(Valuation& lowerBoundaries, Valuation& upperBoundaries, std::string const& parameterBoundariesString, std::set<VariableType> const& consideredVariables) {
std::string::size_type positionOfFirstRelation = parameterBoundariesString.find("<=");
STORM_LOG_THROW(positionOfFirstRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a '<=' after the first number");
STORM_LOG_THROW(positionOfFirstRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a '<=' after the first number");
std::string::size_type positionOfSecondRelation = parameterBoundariesString.find("<=", positionOfFirstRelation+2);
STORM_LOG_THROW(positionOfSecondRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a '<=' after the parameter");
STORM_LOG_THROW(positionOfSecondRelation!=std::string::npos, storm::exceptions::InvalidArgumentException, "When parsing the region" << parameterBoundariesString << " I could not find a '<=' after the parameter");
std::string parameter = parameterBoundariesString.substr(positionOfFirstRelation+2,positionOfSecondRelation-(positionOfFirstRelation+2));

64
src/storm-parsers/parser/JaniParser.cpp
View File

@ -221,13 +221,13 @@ namespace storm {
}
std::vector<std::shared_ptr<storm::logic::Formula const>> JaniParser::parseUnaryFormulaArgument(storm::jani::Model& model, json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, Scope const& scope) {
STORM_LOG_THROW(propertyStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting operand for operator " << opstring << " in " << scope.description);
STORM_LOG_THROW(propertyStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting operand for operator " << opstring << " in " << scope.description);
return { parseFormula(model, propertyStructure.at("exp"), formulaContext, scope.refine("Operand of operator " + opstring)) };
}
std::vector<std::shared_ptr<storm::logic::Formula const>> JaniParser::parseBinaryFormulaArguments(storm::jani::Model& model, json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, Scope const& scope) {
STORM_LOG_THROW(propertyStructure.count("left") == 1, storm::exceptions::InvalidJaniException, "Expecting left operand for operator " << opstring << " in " << scope.description);
STORM_LOG_THROW(propertyStructure.count("right") == 1, storm::exceptions::InvalidJaniException, "Expecting right operand for operator " << opstring << " in " << scope.description);
STORM_LOG_THROW(propertyStructure.count("left") == 1, storm::exceptions::InvalidJaniException, "Expecting left operand for operator " << opstring << " in " << scope.description);
STORM_LOG_THROW(propertyStructure.count("right") == 1, storm::exceptions::InvalidJaniException, "Expecting right operand for operator " << opstring << " in " << scope.description);
return { parseFormula(model, propertyStructure.at("left"), formulaContext, scope.refine("Operand of operator " + opstring)), parseFormula(model, propertyStructure.at("right"), formulaContext, scope.refine("Operand of operator " + opstring)) };
}
@ -325,7 +325,7 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Forall and Exists are currently not supported in " << scope.description);
} else if (opString == "Emin" || opString == "Emax") {
STORM_LOG_WARN_COND(model.getJaniVersion() == 1, "Model not compliant: Contains Emin/Emax property in " << scope.description << ".");
STORM_LOG_THROW(propertyStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting reward-expression for operator " << opString << " in " << scope.description);
STORM_LOG_THROW(propertyStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting reward-expression for operator " << opString << " in " << scope.description);
storm::expressions::Expression rewExpr = parseExpression(propertyStructure.at("exp"), scope.refine("Reward expression"));
STORM_LOG_THROW(rewExpr.hasNumericalType(), storm::exceptions::InvalidJaniException, "Reward expression '" << rewExpr << "' does not have numerical type in " << scope.description);
std::string rewardName = rewExpr.toString();
@ -463,7 +463,7 @@ namespace storm {
for (auto const& rbStructure : propertyStructure.at("reward-bounds")) {
storm::jani::PropertyInterval pi = parsePropertyInterval(rbStructure.at("bounds"), scope.refine("reward-bounded until").clearVariables());
insertLowerUpperTimeBounds(lowerBounds, upperBounds, pi);
STORM_LOG_THROW(rbStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting reward-expression for operator " << opString << " in " << scope.description);
STORM_LOG_THROW(rbStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting reward-expression for operator " << opString << " in " << scope.description);
storm::expressions::Expression rewInstRewardModelExpression = parseExpression(rbStructure.at("exp"), scope.refine("Reward expression at reward-bounds"));
STORM_LOG_THROW(rewInstRewardModelExpression.hasNumericalType(), storm::exceptions::InvalidJaniException, "Reward expression '" << rewInstRewardModelExpression << "' does not have numerical type in " << scope.description);
storm::logic::RewardAccumulation boundRewardAccumulation = parseRewardAccumulation(rbStructure.at("accumulate"), scope.description);
@ -650,7 +650,7 @@ namespace storm {
std::string exprManagerName = name;
size_t valueCount = constantStructure.count("value");
storm::expressions::Expression definingExpression;
STORM_LOG_THROW(valueCount < 2, storm::exceptions::InvalidJaniException, "Value for constant '" + name + "' (scope: " + scope.description + ") must be given at most once.");
STORM_LOG_THROW(valueCount < 2, storm::exceptions::InvalidJaniException, "Value for constant '" + name + "' (scope: " + scope.description + ") must be given at most once.");
if (valueCount == 1) {
// Read initial value before; that makes creation later on a bit easier, and has as an additional benefit that we do not need to check whether the variable occurs also on the assignment.
definingExpression = parseExpression(constantStructure.at("value"), scope.refine("Value of constant " + name));
@ -701,14 +701,14 @@ namespace storm {
result.basicType = ParsedType::BasicType::Int;
result.expressionType = expressionManager->getIntegerType();
} else if(typeStructure == "clock") {
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported type 'clock' for variable '" << variableName << "' (scope: " << scope.description << ")");
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported type 'clock' for variable '" << variableName << "' (scope: " << scope.description << ").");
} else if(typeStructure == "continuous") {
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported type 'continuous' for variable ''" << variableName << "' (scope: " << scope.description << ")");
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported type 'continuous' for variable ''" << variableName << "' (scope: " << scope.description << ").");
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported type " << typeStructure.dump() << " for variable '" << variableName << "' (scope: " << scope.description << ")");
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported type " << typeStructure.dump() << " for variable '" << variableName << "' (scope: " << scope.description << ").");
}
} else if (typeStructure.is_object()) {
STORM_LOG_THROW(typeStructure.count("kind") == 1, storm::exceptions::InvalidJaniException, "For complex type as in variable " << variableName << "(scope: " << scope.description << ") kind must be given");
STORM_LOG_THROW(typeStructure.count("kind") == 1, storm::exceptions::InvalidJaniException, "For complex type as in variable " << variableName << "(scope: " << scope.description << ") kind must be given");
std::string kind = getString(typeStructure.at("kind"), "kind for complex type as in variable " + variableName + "(scope: " + scope.description + ") ");
if (kind == "bounded") {
STORM_LOG_THROW(typeStructure.count("lower-bound") + typeStructure.count("upper-bound") > 0, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << variableName << "(scope: " << scope.description << ") lower-bound or upper-bound must be given");
@ -726,7 +726,7 @@ namespace storm {
STORM_LOG_THROW(!lowerboundExpr.isInitialized() || lowerboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Lower bound for bounded integer variable " << variableName << "(scope: " << scope.description << ") must be integer-typed");
STORM_LOG_THROW(!upperboundExpr.isInitialized() || upperboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Upper bound for bounded integer variable " << variableName << "(scope: " << scope.description << ") must be integer-typed");
if (lowerboundExpr.isInitialized() && upperboundExpr.isInitialized() && !lowerboundExpr.containsVariables() && !upperboundExpr.containsVariables()) {
STORM_LOG_THROW(lowerboundExpr.evaluateAsInt() <= upperboundExpr.evaluateAsInt(), storm::exceptions::InvalidJaniException, "Lower bound must not be larger than upper bound for bounded integer variable " << variableName << "(scope: " << scope.description << ")");
STORM_LOG_THROW(lowerboundExpr.evaluateAsInt() <= upperboundExpr.evaluateAsInt(), storm::exceptions::InvalidJaniException, "Lower bound must not be larger than upper bound for bounded integer variable " << variableName << "(scope: " << scope.description << ").");
}
result.basicType = ParsedType::BasicType::Int;
result.expressionType = expressionManager->getIntegerType();
@ -735,13 +735,13 @@ namespace storm {
STORM_LOG_THROW(!lowerboundExpr.isInitialized() || lowerboundExpr.hasNumericalType(), storm::exceptions::InvalidJaniException, "Lower bound for bounded real variable " << variableName << "(scope: " << scope.description << ") must be numeric");
STORM_LOG_THROW(!upperboundExpr.isInitialized() || upperboundExpr.hasNumericalType(), storm::exceptions::InvalidJaniException, "Upper bound for bounded real variable " << variableName << "(scope: " << scope.description << ") must be numeric");
if (lowerboundExpr.isInitialized() && upperboundExpr.isInitialized() && !lowerboundExpr.containsVariables() && !upperboundExpr.containsVariables()) {
STORM_LOG_THROW(lowerboundExpr.evaluateAsRational() <= upperboundExpr.evaluateAsRational(), storm::exceptions::InvalidJaniException, "Lower bound must not be larger than upper bound for bounded integer variable " << variableName << "(scope: " << scope.description << ")");
STORM_LOG_THROW(lowerboundExpr.evaluateAsRational() <= upperboundExpr.evaluateAsRational(), storm::exceptions::InvalidJaniException, "Lower bound must not be larger than upper bound for bounded integer variable " << variableName << "(scope: " << scope.description << ").");
}
result.basicType = ParsedType::BasicType::Real;
result.expressionType = expressionManager->getRationalType();
result.bounds = std::make_pair(lowerboundExpr, upperboundExpr);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported base " << basictype << " for bounded variable " << variableName << "(scope: " << scope.description << ") ");
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported base " << basictype << " for bounded variable " << variableName << "(scope: " << scope.description << ").");
}
} else if (kind == "array") {
STORM_LOG_THROW(typeStructure.count("base") == 1, storm::exceptions::InvalidJaniException, "For array type as in variable " << variableName << "(scope: " << scope.description << ") base must be given");
@ -749,7 +749,7 @@ namespace storm {
parseType(*result.arrayBase, typeStructure.at("base"), variableName, scope);
result.expressionType = expressionManager->getArrayType(result.arrayBase->expressionType);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported kind " << kind << " for complex type of variable " << variableName << "(scope: " << scope.description << ") ");
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported kind " << kind << " for complex type of variable " << variableName << "(scope: " << scope.description << ").");
}
}
}
@ -767,7 +767,7 @@ namespace storm {
STORM_LOG_THROW(functionDefinitionStructure.count("parameters") == 1, storm::exceptions::InvalidJaniException, "Function definition '" + functionName + "' (scope: " + scope.description + ") must have exactly one list of parameters.");
for (auto const& parameterStructure : functionDefinitionStructure.at("parameters")) {
STORM_LOG_THROW(parameterStructure.count("name") == 1, storm::exceptions::InvalidJaniException, "Parameter declaration of parameter " + std::to_string(parameters.size()) + " of Function definition '" + functionName + "' (scope: " + scope.description + ") must have a name");
std::string parameterName = getString(parameterStructure.at("name"), "parameter-name of parameter " + std::to_string(parameters.size()) + " of Function definition '" + functionName + "' (scope: " + scope.description + ")");
std::string parameterName = getString(parameterStructure.at("name"), "parameter-name of parameter " + std::to_string(parameters.size()) + " of Function definition '" + functionName + "' (scope: " + scope.description + ").");
ParsedType parameterType;
STORM_LOG_THROW(parameterStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Parameter declaration of parameter " + std::to_string(parameters.size()) + " of Function definition '" + functionName + "' (scope: " + scope.description + ") must have exactly one type.");
parseType(parameterType, parameterStructure.at("type"), parameterName, scope.refine("parameter declaration of parameter " + std::to_string(parameters.size()) + " of function definition " + functionName));
@ -797,9 +797,9 @@ namespace storm {
std::string exprManagerName = namePrefix + name;
bool transientVar = defaultVariableTransient; // Default value for variables.
size_t tvarcount = variableStructure.count("transient");
STORM_LOG_THROW(tvarcount <= 1, storm::exceptions::InvalidJaniException, "Multiple definitions of transient not allowed in variable '" + name + "' (scope: " + scope.description + ") ");
STORM_LOG_THROW(tvarcount <= 1, storm::exceptions::InvalidJaniException, "Multiple definitions of transient not allowed in variable '" + name + "' (scope: " + scope.description + ").");
if(tvarcount == 1) {
transientVar = getBoolean(variableStructure.at("transient"), "transient-attribute in variable '" + name + "' (scope: " + scope.description + ") ");
transientVar = getBoolean(variableStructure.at("transient"), "transient-attribute in variable '" + name + "' (scope: " + scope.description + ").");
}
STORM_LOG_THROW(variableStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Variable '" + name + "' (scope: " + scope.description + ") must have a (single) type-declaration.");
ParsedType type;
@ -807,9 +807,9 @@ namespace storm {
size_t initvalcount = variableStructure.count("initial-value");
if(transientVar) {
STORM_LOG_THROW(initvalcount == 1, storm::exceptions::InvalidJaniException, "Initial value must be given once for transient variable '" + name + "' (scope: " + scope.description + ") "+ name + "' (scope: " + scope.description + ") ");
STORM_LOG_THROW(initvalcount == 1, storm::exceptions::InvalidJaniException, "Initial value must be given once for transient variable '" + name + "' (scope: " + scope.description + ") "+ name + "' (scope: " + scope.description + ").");
} else {
STORM_LOG_THROW(initvalcount <= 1, storm::exceptions::InvalidJaniException, "Initial value can be given at most one for variable " + name + "' (scope: " + scope.description + ")");
STORM_LOG_THROW(initvalcount <= 1, storm::exceptions::InvalidJaniException, "Initial value can be given at most one for variable " + name + "' (scope: " + scope.description + ").");
}
boost::optional<storm::expressions::Expression> initVal;
if (initvalcount == 1 && !variableStructure.at("initial-value").is_null()) {
@ -918,7 +918,7 @@ namespace storm {
return result;
}
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description, " << variableStructure.at("type").dump() << " for variable '" << name << "' (scope: " << scope.description << ")");
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description, " << variableStructure.at("type").dump() << " for variable '" << name << "' (scope: " << scope.description << ").");
}
/**
@ -1040,7 +1040,7 @@ namespace storm {
return storm::expressions::Expression(getVariableOrConstantExpression(ident, scope, auxiliaryVariables));
} else if (expressionStructure.is_object()) {
if (expressionStructure.count("distribution") == 1) {
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Distributions are not supported by storm expressions, cannot import " << expressionStructure.dump() << " in " << scope.description << ".");
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Distributions are not supported by storm expressions, cannot import " << expressionStructure.dump() << " in " << scope.description << ".");
}
if (expressionStructure.count("op") == 1) {
std::string opstring = getString(expressionStructure.at("op"), scope.description);
@ -1311,12 +1311,12 @@ namespace storm {
if(returnNoneInitializedOnUnknownOperator) {
return storm::expressions::Expression();
}
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown operator " << opstring << " in " << scope.description << ".");
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown operator " << opstring << " in " << scope.description << ".");
}
}
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "No supported operator declaration found for complex expressions as " << expressionStructure.dump() << " in " << scope.description << ".");
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "No supported operator declaration found for complex expressions as " << expressionStructure.dump() << " in " << scope.description << ".");
}
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "No supported expression found at " << expressionStructure.dump() << " in " << scope.description << ".");
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "No supported expression found at " << expressionStructure.dump() << " in " << scope.description << ".");
// Silly warning suppression.
return storm::expressions::Expression();
@ -1391,7 +1391,7 @@ namespace storm {
STORM_LOG_THROW(transientValueEntry.count("ref") == 1, storm::exceptions::InvalidJaniException, "Transient values in location " << locName << " need exactly one ref that is assigned to");
STORM_LOG_THROW(transientValueEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Transient values in location " << locName << " need exactly one assigned value");
storm::jani::LValue lValue = parseLValue(transientValueEntry.at("ref"), scope.refine("LHS of assignment in location " + locName));
STORM_LOG_THROW(lValue.isTransient(), storm::exceptions::InvalidJaniException, "Assigned non-transient variable " << lValue << " in location " + locName + " (automaton: '" + name + "')");
STORM_LOG_THROW(lValue.isTransient(), storm::exceptions::InvalidJaniException, "Assigned non-transient variable " << lValue << " in location " + locName + " (automaton: '" + name + "').");
storm::expressions::Expression rhs = parseExpression(transientValueEntry.at("value"), scope.refine("Assignment of lValue in location " + locName));
transientAssignments.emplace_back(lValue, rhs);
}
@ -1439,7 +1439,7 @@ namespace storm {
STORM_LOG_THROW(edgeEntry.count("guard") <= 1, storm::exceptions::InvalidJaniException, "Guard can be given at most once in edge from '" << sourceLoc << "' in automaton '" << name << "'");
storm::expressions::Expression guardExpr = expressionManager->boolean(true);
if (edgeEntry.count("guard") == 1) {
STORM_LOG_THROW(edgeEntry.at("guard").count("exp") == 1, storm::exceptions::InvalidJaniException, "Guard in edge from '" + sourceLoc + "' in automaton '" + name + "' must have one expression");
STORM_LOG_THROW(edgeEntry.at("guard").count("exp") == 1, storm::exceptions::InvalidJaniException, "Guard in edge from '" + sourceLoc + "' in automaton '" + name + "' must have one expression");
guardExpr = parseExpression(edgeEntry.at("guard").at("exp"), scope.refine("guard expression in edge from '" + sourceLoc));
STORM_LOG_THROW(guardExpr.hasBooleanType(), storm::exceptions::InvalidJaniException, "Guard " << guardExpr << " does not have Boolean type.");
}
@ -1448,13 +1448,13 @@ namespace storm {
// edge assignments
if (edgeEntry.count("assignments") > 0) {
STORM_LOG_THROW(edgeEntry.count("assignments") == 1, storm::exceptions::InvalidJaniException, "Multiple edge assignments in edge from '" + sourceLoc + "' in automaton '" + name + "'.");
STORM_LOG_THROW(edgeEntry.count("assignments") == 1, storm::exceptions::InvalidJaniException, "Multiple edge assignments in edge from '" + sourceLoc + "' in automaton '" + name + "'.");
for (auto const& assignmentEntry : edgeEntry.at("assignments")) {
// ref
STORM_LOG_THROW(assignmentEntry.count("ref") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' in automaton '" << name << "' must have one ref field");
STORM_LOG_THROW(assignmentEntry.count("ref") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' in automaton '" << name << "'must have one ref field");
storm::jani::LValue lValue = parseLValue(assignmentEntry.at("ref"), scope.refine("Assignment variable in edge from '" + sourceLoc + "' in automaton '" + name + "'"));
// value
STORM_LOG_THROW(assignmentEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' in automaton '" << name << "' must have one value field");
STORM_LOG_THROW(assignmentEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' in automaton '" << name << "' must have one value field");
storm::expressions::Expression assignmentExpr = parseExpression(assignmentEntry.at("value"), scope.refine("assignment in edge from '" + sourceLoc + "' in automaton '" + name + "'"));
// TODO check types
// index
@ -1482,7 +1482,7 @@ namespace storm {
probExpr = expressionManager->rational(1.0);
} else {
STORM_LOG_THROW(destEntry.at("probability").count("exp") == 1, storm::exceptions::InvalidJaniException, "Destination in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "' must have a probability expression.");
probExpr = parseExpression(destEntry.at("probability").at("exp"), scope.refine("probability expression in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'"));
probExpr = parseExpression(destEntry.at("probability").at("exp"), scope.refine("probability expression in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'"));
}
assert(probExpr.isInitialized());
STORM_LOG_THROW(probExpr.hasNumericalType(), storm::exceptions::InvalidJaniException, "Probability expression " << probExpr << " does not have a numerical type." );
@ -1493,10 +1493,10 @@ namespace storm {
if (assignmentDeclCount > 0) {
for (auto const& assignmentEntry : destEntry.at("assignments")) {
// ref
STORM_LOG_THROW(assignmentEntry.count("ref") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "' must have one ref field");
STORM_LOG_THROW(assignmentEntry.count("ref") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "' must have one ref field");
storm::jani::LValue lValue = parseLValue(assignmentEntry.at("ref"), scope.refine("Assignment variable in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'"));
// value
STORM_LOG_THROW(assignmentEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "' must have one value field");
STORM_LOG_THROW(assignmentEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "' must have one value field");
storm::expressions::Expression assignmentExpr = parseExpression(assignmentEntry.at("value"), scope.refine("assignment in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'"));
// TODO check types
// index

2
src/storm/modelchecker/multiobjective/pcaa/RewardBoundedMdpPcaaWeightVectorChecker.cpp
View File

@ -34,7 +34,7 @@ namespace storm {
template <class SparseMdpModelType>
RewardBoundedMdpPcaaWeightVectorChecker<SparseMdpModelType>::RewardBoundedMdpPcaaWeightVectorChecker(SparseMultiObjectivePreprocessorResult<SparseMdpModelType> const& preprocessorResult) : PcaaWeightVectorChecker<SparseMdpModelType>(preprocessorResult.objectives), swAll(true), rewardUnfolding(*preprocessorResult.preprocessedModel, preprocessorResult.objectives) {
STORM_LOG_THROW(preprocessorResult.rewardFinitenessType == SparseMultiObjectivePreprocessorResult<SparseMdpModelType>::RewardFinitenessType::AllFinite, storm::exceptions::NotSupportedException, "There is a scheduler that yields infinite reward for one objective. This is not supported.");
STORM_LOG_THROW(preprocessorResult.rewardFinitenessType == SparseMultiObjectivePreprocessorResult<SparseMdpModelType>::RewardFinitenessType::AllFinite, storm::exceptions::NotSupportedException, "There is a scheduler that yields infinite reward for one objective. This is not supported.");
STORM_LOG_THROW(preprocessorResult.preprocessedModel->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "The model has multiple initial states.");
// Update the objective bounds with what the reward unfolding can compute

2
src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp
View File

@ -67,7 +67,7 @@ namespace storm {
}
STORM_LOG_THROW(farestHalfspaceIndex<halfspaces.size(), storm::exceptions::UnexpectedException, "There is no seperating vector.");
STORM_LOG_DEBUG("Found separating weight vector: " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector<double>(halfspaces[farestHalfspaceIndex].normalVector())) << ".");
STORM_LOG_DEBUG("Found separating weight vector: " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector<double>(halfspaces[farestHalfspaceIndex].normalVector())) << ".");
return halfspaces[farestHalfspaceIndex].normalVector();
}

2
src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp
View File

@ -276,7 +276,7 @@ namespace storm {
STORM_LOG_THROW(SingleObjectiveMode, storm::exceptions::NotSupportedException, "Letting lower bounds approach infinity is only supported in single objective mode."); // It most likely also works with multiple objectives with the same shape. However, we haven't checked this yet.
STORM_LOG_THROW(objectives.front().formula->isProbabilityOperatorFormula(), storm::exceptions::NotSupportedException, "Letting lower bounds approach infinity is only supported for probability operator formulas");
auto const& probabilityOperatorFormula = objectives.front().formula->asProbabilityOperatorFormula();
STORM_LOG_THROW(probabilityOperatorFormula.getSubformula().isBoundedUntilFormula(), storm::exceptions::NotSupportedException, "Letting lower bounds approach infinity is only supported for bounded until probabilities.");
STORM_LOG_THROW(probabilityOperatorFormula.getSubformula().isBoundedUntilFormula(), storm::exceptions::NotSupportedException, "Letting lower bounds approach infinity is only supported for bounded until probabilities.");
STORM_LOG_THROW(!model.isNondeterministicModel() || (probabilityOperatorFormula.hasOptimalityType() && storm::solver::maximize(probabilityOperatorFormula.getOptimalityType())), storm::exceptions::NotSupportedException, "Letting lower bounds approach infinity is only supported for maximizing bounded until probabilities.");
STORM_LOG_THROW(upperBoundedDimensions.empty() || !probabilityOperatorFormula.getSubformula().asBoundedUntilFormula().hasMultiDimensionalSubformulas(), storm::exceptions::NotSupportedException, "Letting lower bounds approach infinity is only supported if the formula has either only lower bounds or if it has a single goal state."); // This would fail because the upper bounded dimension(s) might be satisfied already. One should erase epoch steps in the epoch model (after applying the goal-unfolding).

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

@ -90,7 +90,7 @@ namespace storm {
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the choice labels.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that this requires the model to be given as an symbolic model (i.e., via --" + prismInputOptionName + " or --" + janiInputOptionName + ").").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());
this->addOption(storm::settings::OptionBuilder(moduleName, janiPropertyOptionName, false, "Specifies the properties from the jani model (given by --" + janiInputOptionName + ") to be checked.").setShortName(janiPropertyOptionShortName)
this->addOption(storm::settings::OptionBuilder(moduleName, janiPropertyOptionName, false, "Specifies the properties from the jani model (given by --" + janiInputOptionName + ") to be checked.").setShortName(janiPropertyOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of properties to be checked").setDefaultValueString("").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, qvbsInputOptionName, false, "Selects a model from the Quantitative Verification Benchmark Set.").setShortName(qvbsInputOptionShortName)

2
src/storm/solver/SymbolicNativeLinearEquationSolver.cpp
View File

@ -49,7 +49,7 @@ namespace storm {
} else {
if (method != NativeLinearEquationSolverMethod::Power && method != NativeLinearEquationSolverMethod::RationalSearch && method != NativeLinearEquationSolverMethod::Jacobi) {
method = NativeLinearEquationSolverMethod::Jacobi;
STORM_LOG_INFO("The selected solution method is not supported in the dd engine. Falling back to '" + toString(method) + "'.");
STORM_LOG_INFO("The selected solution method is not supported in the dd engine. Falling back to '" + toString(method) + "'.");
}
STORM_LOG_WARN_COND_DEBUG(!env.solver().isForceSoundness(), "Sound computations are not supported in the Dd engine.");
}

2
src/storm/storage/jani/ArrayEliminator.cpp
View File

@ -110,7 +110,7 @@ namespace storm {
} else {
variables = "variables " + variables;
}
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unable to determine array size: Size of ConstructorArrayExpression '" << expression << "' still contains the " << variables << ".");
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unable to determine array size: Size of ConstructorArrayExpression '" << expression << "' still contains the " << variables << ".");
}
}

2
src/storm/storage/jani/Edge.cpp
View File

@ -182,7 +182,7 @@ namespace storm {
first = false;
stream << a;
}
stream << ", " << a;
stream << ", " << a;
}
}
stream << "]";

2
src/storm/transformer/EndComponentEliminator.h
View File

@ -89,7 +89,7 @@ namespace storm {
sinkRows.resize(result.newToOldRowMapping.size());
result.matrix = buildTransformedMatrix(originalMatrix, newRowGroupIndices, result.newToOldRowMapping, result.oldToNewStateMapping, sinkRows, addSelfLoopAtSinkStates);
STORM_LOG_DEBUG("EndComponentEliminator is done. Resulting matrix has " << result.matrix.getRowGroupCount() << " row groups.");
STORM_LOG_DEBUG("EndComponentEliminator is done. Resulting matrix has " << result.matrix.getRowGroupCount() << " row groups.");
return result;
}

10
src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp
View File

@ -82,7 +82,7 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_pareto_3Obj) {
storm::Environment env;
std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma";
std::string formulasAsString = "multi(Tmin=? [ F \"all_jobs_finished\" ], Pmax=? [ F<=0.2 \"half_of_jobs_finished\" ], Pmin=? [ F \"slowest_before_fastest\" ]) ";
std::string formulasAsString = "multi(Tmin=? [ F \"all_jobs_finished\" ], Pmax=? [ F<=0.2 \"half_of_jobs_finished\" ], Pmin=? [ F \"slowest_before_fastest\" ]) ";
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, "");
@ -113,8 +113,8 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_achievability_3Obj
storm::Environment env;
std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma";
std::string formulasAsString = "multi(T<=1.31 [ F \"all_jobs_finished\" ], P>=0.17 [ F<=0.2 \"half_of_jobs_finished\" ], P<=0.31 [ F \"slowest_before_fastest\" ]) "; //true
formulasAsString += "; multi(T<=1.29 [ F \"all_jobs_finished\" ], P>=0.18 [ F<=0.2 \"half_of_jobs_finished\" ], P<=0.29 [ F \"slowest_before_fastest\" ])"; //false
std::string formulasAsString = "multi(T<=1.31 [ F \"all_jobs_finished\" ], P>=0.17 [ F<=0.2 \"half_of_jobs_finished\" ], P<=0.31 [ F \"slowest_before_fastest\" ]) "; //true
formulasAsString += "; multi(T<=1.29 [ F \"all_jobs_finished\" ], P>=0.18 [ F<=0.2 \"half_of_jobs_finished\" ], P<=0.29 [ F \"slowest_before_fastest\" ])"; //false
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, "");
@ -135,8 +135,8 @@ TEST(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_quantitative_3Obj)
storm::Environment env;
std::string programFile = STORM_TEST_RESOURCES_DIR "/ma/jobscheduler.ma";
std::string formulasAsString = "multi(Tmin=? [ F \"all_jobs_finished\" ], P>=0.1797900683 [ F<=0.2 \"half_of_jobs_finished\" ], P<=0.3 [ F \"slowest_before_fastest\" ]) "; //quantitative
formulasAsString += "; multi(T<=1.26 [ F \"all_jobs_finished\" ], P>=0.2 [ F<=0.2 \"half_of_jobs_finished\" ], Pmin=? [ F \"slowest_before_fastest\" ])"; //false
std::string formulasAsString = "multi(Tmin=? [ F \"all_jobs_finished\" ], P>=0.1797900683 [ F<=0.2 \"half_of_jobs_finished\" ], P<=0.3 [ F \"slowest_before_fastest\" ]) "; //quantitative
formulasAsString += "; multi(T<=1.26 [ F \"all_jobs_finished\" ], P>=0.2 [ F<=0.2 \"half_of_jobs_finished\" ], Pmin=? [ F \"slowest_before_fastest\" ])"; //false
storm::prism::Program program = storm::api::parseProgram(programFile);
program = storm::utility::prism::preprocess(program, "");

2
src/test/storm/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp
View File

@ -61,7 +61,7 @@ TEST(SparseMdpCbMultiObjectiveModelCheckerTest, zeroconf) {
TEST(SparseMdpCbMultiObjectiveModelCheckerTest, team3with3objectives) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_team3.nm";
std::string formulasAsString = "multi(P>=0.75 [ F \"task1_compl\" ], R{\"w_1_total\"}>=2.210204082 [ C ], P>=0.5 [ F \"task2_compl\" ])"; // numerical
std::string formulasAsString = "multi(P>=0.75 [ F \"task1_compl\" ], R{\"w_1_total\"}>=2.210204082 [ C ], P>=0.5 [ F \"task2_compl\" ])"; // numerical
// programm, model, formula
storm::prism::Program program = storm::api::parseProgram(programFile);

4
src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp
View File

@ -165,7 +165,7 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_zeroconf_dl) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/zeroconf_dl_not_unfolded.nm";
std::string constantsDef = "N=1000,K=2,reset=true";
std::string formulasAsString = "Pmin=? [ F{\"t\"}<50 \"ipfound\" ]";
formulasAsString += "; \n Pmax=? [multi(F{\"t\"}<50 \"ipfound\", F{\"r\"}<=0 \"ipfound\") ]";
formulasAsString += "; \n Pmax=? [multi(F{\"t\"}<50 \"ipfound\", F{\"r\"}<=0 \"ipfound\") ]";
// programm, model, formula
storm::prism::Program program = storm::api::parseProgram(programFile);
@ -457,7 +457,7 @@ TEST(SparseMdpMultiDimensionalRewardUnfoldingTest, zeroconf_dl) {
std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/zeroconf_dl_not_unfolded.nm";
std::string constantsDef = "N=1000,K=2,reset=true";
std::string formulasAsString = "multi(Pmin=? [ F{\"t\"}<50 \"ipfound\" ])";
formulasAsString += "; \n multi(Pmax=? [multi(F{\"t\"}<50 \"ipfound\", F{\"r\"}<=0 \"ipfound\") ])";
formulasAsString += "; \n multi(Pmax=? [multi(F{\"t\"}<50 \"ipfound\", F{\"r\"}<=0 \"ipfound\") ])";
// programm, model, formula
storm::prism::Program program = storm::api::parseProgram(programFile);

4
src/test/storm/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp
View File

@ -65,7 +65,7 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, team3with3objectives) {
storm::Environment env;
std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_team3.nm";
std::string formulasAsString = "multi(Pmax=? [ F \"task1_compl\" ], R{\"w_1_total\"}>=2.210204082 [ C ], P>=0.5 [ F \"task2_compl\" ])"; // numerical
std::string formulasAsString = "multi(Pmax=? [ F \"task1_compl\" ], R{\"w_1_total\"}>=2.210204082 [ C ], P>=0.5 [ F \"task2_compl\" ])"; // numerical
// programm, model, formula
storm::prism::Program program = storm::api::parseProgram(programFile);
@ -83,7 +83,7 @@ TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, scheduler) {
storm::Environment env;
std::string programFile = STORM_TEST_RESOURCES_DIR "/mdp/multiobj_scheduler05.nm";
std::string formulasAsString = "multi(R{\"time\"}<= 11.778[ F \"tasks_complete\" ], R{\"energy\"}<=1.45 [ F \"tasks_complete\" ]) ";
std::string formulasAsString = "multi(R{\"time\"}<= 11.778[ F \"tasks_complete\" ], R{\"energy\"}<=1.45 [ F \"tasks_complete\" ]) ";
// programm, model, formula
storm::prism::Program program = storm::api::parseProgram(programFile);

Write Preview
Loading…
Cancel
Save