Browse Source

Unified some method names.

Former-commit-id: 3cda728bf6
tempestpy_adaptions
dehnert 11 years ago
parent
commit
88a5be5b97
  1. 10
      src/adapters/ExplicitModelAdapter.h
  2. 2
      src/storage/expressions/IntegerLiteralExpression.h
  3. 18
      src/storage/prism/Constant.cpp
  4. 14
      src/storage/prism/Constant.h
  5. 12
      src/storage/prism/Formula.cpp
  6. 13
      src/storage/prism/Formula.h
  7. 4
      src/storage/prism/IntegerVariable.cpp
  8. 8
      src/storage/prism/IntegerVariable.h
  9. 10
      src/storage/prism/Label.cpp
  10. 8
      src/storage/prism/Label.h
  11. 20
      src/storage/prism/Program.cpp
  12. 6
      src/storage/prism/Variable.cpp
  13. 6
      src/storage/prism/Variable.h

10
src/adapters/ExplicitModelAdapter.h

@ -120,7 +120,7 @@ namespace storm {
LOG_THROW(definedConstants.find(constantName) == definedConstants.end(), storm::exceptions::InvalidArgumentException, "Illegally trying to define constant '" << constantName <<"' twice.");
definedConstants.insert(constantName);
if (constant.getConstantType() == storm::expressions::ExpressionReturnType::Bool) {
if (constant.getType() == storm::expressions::ExpressionReturnType::Bool) {
if (value == "true") {
constantDefinitions[constantName] = storm::expressions::Expression::createTrue();
} else if (value == "false") {
@ -128,10 +128,10 @@ namespace storm {
} else {
throw storm::exceptions::InvalidArgumentException() << "Illegal value for boolean constant: " << value << ".";
}
} else if (constant.getConstantType() == storm::expressions::ExpressionReturnType::Int) {
} else if (constant.getType() == storm::expressions::ExpressionReturnType::Int) {
int_fast64_t integerValue = std::stoi(value);
constantDefinitions[constantName] = storm::expressions::Expression::createIntegerLiteral(integerValue);
} else if (constant.getConstantType() == storm::expressions::ExpressionReturnType::Double) {
} else if (constant.getType() == storm::expressions::ExpressionReturnType::Double) {
double doubleValue = std::stod(value);
constantDefinitions[constantName] = storm::expressions::Expression::createDoubleLiteral(doubleValue);
}
@ -753,13 +753,13 @@ namespace storm {
// Initialize labeling.
for (auto const& label : labels) {
result.addAtomicProposition(label.getLabelName());
result.addAtomicProposition(label.getName());
}
for (uint_fast64_t index = 0; index < stateInformation.reachableStates.size(); index++) {
for (auto const& label : labels) {
// Add label to state, if the corresponding expression is true.
if (label.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates[index])) {
result.addAtomicPropositionToState(label.getLabelName(), index);
result.addAtomicPropositionToState(label.getName(), index);
}
}
}

2
src/storage/expressions/IntegerLiteralExpression.h

@ -18,7 +18,7 @@ namespace storm {
// Instantiate constructors and assignments with their default implementations.
IntegerLiteralExpression(IntegerLiteralExpression const& other) = default;
IntegerLiteralExpression& operator=(IntegerLiteralExpression const& other) = default;
#ifndef
#ifndef WINDOWS
IntegerLiteralExpression(IntegerLiteralExpression&&) = default;
IntegerLiteralExpression& operator=(IntegerLiteralExpression&&) = default;
#endif

18
src/storage/prism/Constant.cpp

@ -2,20 +2,20 @@
namespace storm {
namespace prism {
Constant::Constant(storm::expressions::ExpressionReturnType constantType, std::string const& constantName, storm::expressions::Expression const& expression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), constantType(constantType), constantName(constantName), defined(true), expression(expression) {
Constant::Constant(storm::expressions::ExpressionReturnType type, std::string const& name, storm::expressions::Expression const& expression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), type(type), name(name), defined(true), expression(expression) {
// Intentionally left empty.
}
Constant::Constant(storm::expressions::ExpressionReturnType constantType, std::string const& constantName, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), constantType(constantType), constantName(constantName), defined(false), expression() {
Constant::Constant(storm::expressions::ExpressionReturnType type, std::string const& name, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), type(type), name(name), defined(false), expression() {
// Intentionally left empty.
}
std::string const& Constant::getConstantName() const {
return this->constantName;
std::string const& Constant::getName() const {
return this->name;
}
storm::expressions::ExpressionReturnType Constant::getConstantType() const {
return this->constantType;
storm::expressions::ExpressionReturnType Constant::getType() const {
return this->type;
}
bool Constant::isDefined() const {
@ -27,18 +27,18 @@ namespace storm {
}
Constant Constant::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
return Constant(this->getConstantType(), this->getConstantName(), this->getExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber());
return Constant(this->getType(), this->getName(), this->getExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber());
}
std::ostream& operator<<(std::ostream& stream, Constant const& constant) {
stream << "const ";
switch (constant.getConstantType()) {
switch (constant.getType()) {
case storm::expressions::ExpressionReturnType::Undefined: stream << "undefined "; break;
case storm::expressions::ExpressionReturnType::Bool: stream << "bool "; break;
case storm::expressions::ExpressionReturnType::Int: stream << "int "; break;
case storm::expressions::ExpressionReturnType::Double: stream << "double "; break;
}
stream << constant.getConstantName();
stream << constant.getName();
if (constant.isDefined()) {
stream << " = " << constant.getExpression();
}

14
src/storage/prism/Constant.h

@ -14,13 +14,13 @@ namespace storm {
/*!
* Creates a constant with the given type, name and defining expression.
*
* @param constantType The type of the constant.
* @param constantName The name of the constant.
* @param type The type of the constant.
* @param name The name of the constant.
* @param expression The expression that defines the constant.
* @param filename The filename in which the transition reward is defined.
* @param lineNumber The line number in which the transition reward is defined.
*/
Constant(storm::expressions::ExpressionReturnType constantType, std::string const& constantName, storm::expressions::Expression const& expression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
Constant(storm::expressions::ExpressionReturnType type, std::string const& name, storm::expressions::Expression const& expression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
/*!
* Creates an undefined constant with the given type and name.
@ -46,14 +46,14 @@ namespace storm {
*
* @return The name of the constant.
*/
std::string const& getConstantName() const;
std::string const& getName() const;
/*!
* Retrieves the type of the constant.
*
* @return The type of the constant;
*/
storm::expressions::ExpressionReturnType getConstantType() const;
storm::expressions::ExpressionReturnType getType() const;
/*!
* Retrieves whether the constant is defined, i.e., whether there is an expression defining its value.
@ -82,10 +82,10 @@ namespace storm {
private:
// The type of the constant.
storm::expressions::ExpressionReturnType constantType;
storm::expressions::ExpressionReturnType type;
// The name of the constant.
std::string constantName;
std::string name;
// A flag that stores whether or not the constant is defined.
bool defined;

12
src/storage/prism/Formula.cpp

@ -2,28 +2,28 @@
namespace storm {
namespace prism {
Formula::Formula(std::string const& formulaName, storm::expressions::Expression const& expression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), formulaName(formulaName), expression(expression) {
Formula::Formula(std::string const& name, storm::expressions::Expression const& expression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), name(name), expression(expression) {
// Intentionally left empty.
}
std::string const& Formula::getFormulaName() const {
return this->formulaName;
std::string const& Formula::getName() const {
return this->name;
}
storm::expressions::Expression const& Formula::getExpression() const {
return this->expression;
}
storm::expressions::ExpressionReturnType Formula::getReturnType() const {
storm::expressions::ExpressionReturnType Formula::getType() const {
return this->getExpression().getReturnType();
}
Formula Formula::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
return Formula(this->getFormulaName(), this->getExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber());
return Formula(this->getName(), this->getExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber());
}
std::ostream& operator<<(std::ostream& stream, Formula const& formula) {
stream << "formula " << formula.getFormulaName() << " = " << formula.getExpression() << ";";
stream << "formula " << formula.getName() << " = " << formula.getExpression() << ";";
return stream;
}
}

13
src/storage/prism/Formula.h

@ -14,13 +14,12 @@ namespace storm {
/*!
* Creates a formula with the given name and expression.
*
* @param formulaName The name of the label.
* @param expression The predicate that needs to hold before taking a transition with the previously
* specified name in order to obtain the reward.
* @param name The name of the formula.
* @param expression The expression associated with this formula.
* @param filename The filename in which the transition reward is defined.
* @param lineNumber The line number in which the transition reward is defined.
*/
Formula(std::string const& formulaName, storm::expressions::Expression const& expression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
Formula(std::string const& name, storm::expressions::Expression const& expression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
// Create default implementations of constructors/assignment.
Formula() = default;
@ -36,7 +35,7 @@ namespace storm {
*
* @return The name that is associated with this formula.
*/
std::string const& getFormulaName() const;
std::string const& getName() const;
/*!
* Retrieves the expression that is associated with this formula.
@ -50,7 +49,7 @@ namespace storm {
*
* @return The return type of the formula.
*/
storm::expressions::ExpressionReturnType getReturnType() const;
storm::expressions::ExpressionReturnType getType() const;
/*!
* Substitutes all identifiers in the expression of the formula according to the given map.
@ -64,7 +63,7 @@ namespace storm {
private:
// The name of the formula.
std::string formulaName;
std::string name;
// A predicate that needs to be satisfied by states for the label to be attached.
storm::expressions::Expression expression;

4
src/storage/prism/IntegerVariable.cpp

@ -2,11 +2,11 @@
namespace storm {
namespace prism {
IntegerVariable::IntegerVariable(std::string const& variableName, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, std::string const& filename, uint_fast64_t lineNumber) : Variable(variableName, lowerBoundExpression, true, filename, lineNumber), lowerBoundExpression(lowerBoundExpression), upperBoundExpression(upperBoundExpression) {
IntegerVariable::IntegerVariable(std::string const& name, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, std::string const& filename, uint_fast64_t lineNumber) : Variable(name, lowerBoundExpression, true, filename, lineNumber), lowerBoundExpression(lowerBoundExpression), upperBoundExpression(upperBoundExpression) {
// Intentionally left empty.
}
IntegerVariable::IntegerVariable(std::string const& variableName, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression, std::string const& filename, uint_fast64_t lineNumber) : Variable(variableName, initialValueExpression, false, filename, lineNumber), lowerBoundExpression(lowerBoundExpression), upperBoundExpression(upperBoundExpression) {
IntegerVariable::IntegerVariable(std::string const& name, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression, std::string const& filename, uint_fast64_t lineNumber) : Variable(name, initialValueExpression, false, filename, lineNumber), lowerBoundExpression(lowerBoundExpression), upperBoundExpression(upperBoundExpression) {
// Intentionally left empty.
}

8
src/storage/prism/IntegerVariable.h

@ -22,25 +22,25 @@ namespace storm {
/*!
* Creates an integer variable with the given name and a default initial value.
*
* @param variableName The name of the variable.
* @param name The name of the variable.
* @param lowerBoundExpression A constant expression defining the lower bound of the domain of the variable.
* @param upperBoundExpression A constant expression defining the upper bound of the domain of the variable.
* @param filename The filename in which the variable is defined.
* @param lineNumber The line number in which the variable is defined.
*/
IntegerVariable(std::string const& variableName, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
IntegerVariable(std::string const& name, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
/*!
* Creates an integer variable with the given name and the given initial value expression.
*
* @param variableName The name of the variable.
* @param name The name of the variable.
* @param lowerBoundExpression A constant expression defining the lower bound of the domain of the variable.
* @param upperBoundExpression A constant expression defining the upper bound of the domain of the variable.
* @param initialValueExpression A constant expression that defines the initial value of the variable.
* @param filename The filename in which the variable is defined.
* @param lineNumber The line number in which the variable is defined.
*/
IntegerVariable(std::string const& variableName, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
IntegerVariable(std::string const& name, storm::expressions::Expression const& lowerBoundExpression, storm::expressions::Expression const& upperBoundExpression, storm::expressions::Expression const& initialValueExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
/*!
* Retrieves an expression defining the lower bound for this integer variable.

10
src/storage/prism/Label.cpp

@ -2,12 +2,12 @@
namespace storm {
namespace prism {
Label::Label(std::string const& labelName, storm::expressions::Expression const& statePredicateExpression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), labelName(labelName), statePredicateExpression(statePredicateExpression) {
Label::Label(std::string const& name, storm::expressions::Expression const& statePredicateExpression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), name(name), statePredicateExpression(statePredicateExpression) {
// Intentionally left empty.
}
std::string const& Label::getLabelName() const {
return this->labelName;
std::string const& Label::getName() const {
return this->name;
}
storm::expressions::Expression const& Label::getStatePredicateExpression() const {
@ -15,11 +15,11 @@ namespace storm {
}
Label Label::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
return Label(this->getLabelName(), this->getStatePredicateExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber());
return Label(this->getName(), this->getStatePredicateExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber());
}
std::ostream& operator<<(std::ostream& stream, Label const& label) {
stream << "label \"" << label.getLabelName() << "\" = " << label.getStatePredicateExpression() << ";";
stream << "label \"" << label.getName() << "\" = " << label.getStatePredicateExpression() << ";";
return stream;
}
}

8
src/storage/prism/Label.h

@ -14,13 +14,13 @@ namespace storm {
/*!
* Creates a label with the given name and state predicate expression.
*
* @param labelName The name of the label.
* @param name The name of the label.
* @param statePredicateExpression The predicate that needs to hold before taking a transition with the previously
* specified name in order to obtain the reward.
* @param filename The filename in which the transition reward is defined.
* @param lineNumber The line number in which the transition reward is defined.
*/
Label(std::string const& labelName, storm::expressions::Expression const& statePredicateExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
Label(std::string const& name, storm::expressions::Expression const& statePredicateExpression, std::string const& filename = "", uint_fast64_t lineNumber = 0);
// Create default implementations of constructors/assignment.
Label() = default;
@ -36,7 +36,7 @@ namespace storm {
*
* @return The name that is associated with this label.
*/
std::string const& getLabelName() const;
std::string const& getName() const;
/*!
* Retrieves the state predicate expression that is associated with this label.
@ -57,7 +57,7 @@ namespace storm {
private:
// The name of the label.
std::string labelName;
std::string name;
// A predicate that needs to be satisfied by states for the label to be attached.
storm::expressions::Expression statePredicateExpression;

20
src/storage/prism/Program.cpp

@ -169,7 +169,7 @@ namespace storm {
void Program::createMappings() {
// Build the mappings for constants, global variables, formulas, modules, reward models and labels.
for (uint_fast64_t constantIndex = 0; constantIndex < this->getNumberOfConstants(); ++constantIndex) {
this->constantToIndexMap[this->getConstants()[constantIndex].getConstantName()] = constantIndex;
this->constantToIndexMap[this->getConstants()[constantIndex].getName()] = constantIndex;
}
for (uint_fast64_t globalVariableIndex = 0; globalVariableIndex < this->getNumberOfGlobalBooleanVariables(); ++globalVariableIndex) {
this->globalBooleanVariableToIndexMap[this->getGlobalBooleanVariables()[globalVariableIndex].getName()] = globalVariableIndex;
@ -178,7 +178,7 @@ namespace storm {
this->globalIntegerVariableToIndexMap[this->getGlobalIntegerVariables()[globalVariableIndex].getName()] = globalVariableIndex;
}
for (uint_fast64_t formulaIndex = 0; formulaIndex < this->getNumberOfFormulas(); ++formulaIndex) {
this->formulaToIndexMap[this->getFormulas()[formulaIndex].getFormulaName()] = formulaIndex;
this->formulaToIndexMap[this->getFormulas()[formulaIndex].getName()] = formulaIndex;
}
for (uint_fast64_t moduleIndex = 0; moduleIndex < this->getNumberOfModules(); ++moduleIndex) {
this->moduleToIndexMap[this->getModules()[moduleIndex].getName()] = moduleIndex;
@ -187,7 +187,7 @@ namespace storm {
this->rewardModelToIndexMap[this->getRewardModels()[rewardModelIndex].getName()] = rewardModelIndex;
}
for (uint_fast64_t labelIndex = 0; labelIndex < this->getNumberOfLabels(); ++labelIndex) {
this->labelToIndexMap[this->getLabels()[labelIndex].getLabelName()] = labelIndex;
this->labelToIndexMap[this->getLabels()[labelIndex].getName()] = labelIndex;
}
// Build the mapping from action names to module indices so that the lookup can later be performed quickly.
@ -226,25 +226,25 @@ namespace storm {
// defining expression
if (constant.isDefined()) {
// Make sure we are not trying to define an already defined constant.
LOG_THROW(constantDefinitions.find(constant.getConstantName()) == constantDefinitions.end(), storm::exceptions::InvalidArgumentException, "Illegally defining already defined constant '" << constant.getConstantName() << "'.");
LOG_THROW(constantDefinitions.find(constant.getName()) == constantDefinitions.end(), storm::exceptions::InvalidArgumentException, "Illegally defining already defined constant '" << constant.getName() << "'.");
// Now replace the occurrences of undefined constants in its defining expression.
newConstants.emplace_back(constant.getConstantType(), constant.getConstantName(), constant.getExpression().substitute<std::map>(constantDefinitions), constant.getFilename(), constant.getLineNumber());
newConstants.emplace_back(constant.getType(), constant.getName(), constant.getExpression().substitute<std::map>(constantDefinitions), constant.getFilename(), constant.getLineNumber());
} else {
auto const& variableExpressionPair = constantDefinitions.find(constant.getConstantName());
auto const& variableExpressionPair = constantDefinitions.find(constant.getName());
// If the constant is not defined by the mapping, we leave it like it is.
if (variableExpressionPair == constantDefinitions.end()) {
newConstants.emplace_back(constant);
} else {
// Otherwise, we add it to the defined constants and assign it the appropriate expression.
definedUndefinedConstants.insert(constant.getConstantName());
definedUndefinedConstants.insert(constant.getName());
// Make sure the type of the constant is correct.
LOG_THROW(variableExpressionPair->second.getReturnType() == constant.getConstantType(), storm::exceptions::InvalidArgumentException, "Illegal type of expression defining constant '" << constant.getConstantName() << "'.");
LOG_THROW(variableExpressionPair->second.getReturnType() == constant.getType(), storm::exceptions::InvalidArgumentException, "Illegal type of expression defining constant '" << constant.getName() << "'.");
// Now create the defined constant.
newConstants.emplace_back(constant.getConstantType(), constant.getConstantName(), variableExpressionPair->second, constant.getFilename(), constant.getLineNumber());
newConstants.emplace_back(constant.getType(), constant.getName(), variableExpressionPair->second, constant.getFilename(), constant.getLineNumber());
}
}
}
@ -267,7 +267,7 @@ namespace storm {
LOG_THROW(constant.isDefined(), storm::exceptions::InvalidArgumentException, "Cannot substitute constants in program that contains undefined constants.");
// Put the corresponding expression in the substitution.
constantSubstitution.emplace(constant.getConstantName(), constant.getExpression());
constantSubstitution.emplace(constant.getName(), constant.getExpression());
// If there is at least one more constant to come, we substitute the costants we have so far.
if (constantIndex + 1 < newConstants.size()) {

6
src/storage/prism/Variable.cpp

@ -4,16 +4,16 @@
namespace storm {
namespace prism {
Variable::Variable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression, bool defaultInitialValue, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variableName(variableName), initialValueExpression(initialValueExpression), defaultInitialValue(defaultInitialValue) {
Variable::Variable(std::string const& name, storm::expressions::Expression const& initialValueExpression, bool defaultInitialValue, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), name(name), initialValueExpression(initialValueExpression), defaultInitialValue(defaultInitialValue) {
// Nothing to do here.
}
Variable::Variable(Variable const& oldVariable, std::string const& newName, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variableName(newName), initialValueExpression(oldVariable.getInitialValueExpression().substitute<std::map>(renaming)), defaultInitialValue(oldVariable.hasDefaultInitialValue()) {
Variable::Variable(Variable const& oldVariable, std::string const& newName, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), name(newName), initialValueExpression(oldVariable.getInitialValueExpression().substitute<std::map>(renaming)), defaultInitialValue(oldVariable.hasDefaultInitialValue()) {
// Intentionally left empty.
}
std::string const& Variable::getName() const {
return variableName;
return this->name;
}
bool Variable::hasDefaultInitialValue() const {

6
src/storage/prism/Variable.h

@ -47,14 +47,14 @@ namespace storm {
/*!
* Creates a variable with the given name and initial value.
*
* @param variableName The name of the variable.
* @param name The name of the variable.
* @param initialValueExpression The constant expression that defines the initial value of the variable.
* @param hasDefaultInitialValue A flag indicating whether the initial value of the variable is its default
* value.
* @param filename The filename in which the variable is defined.
* @param lineNumber The line number in which the variable is defined.
*/
Variable(std::string const& variableName, storm::expressions::Expression const& initialValueExpression, bool defaultInitialValue, std::string const& filename = "", uint_fast64_t lineNumber = 0);
Variable(std::string const& name, storm::expressions::Expression const& initialValueExpression, bool defaultInitialValue, std::string const& filename = "", uint_fast64_t lineNumber = 0);
/*!
* Creates a copy of the given variable and performs the provided renaming.
@ -69,7 +69,7 @@ namespace storm {
private:
// The name of the variable.
std::string variableName;
std::string name;
// The constant expression defining the initial value of the variable.
storm::expressions::Expression initialValueExpression;

Loading…
Cancel
Save