Browse Source
Merge branch 'master' into philippTopologicalRevival
Merge branch 'master' into philippTopologicalRevival
Conflicts:
CMakeLists.txt
src/storm.cpp
Former-commit-id: 16c8e8734a
main
PBerger
11 years ago
305 changed files with 18870 additions and 11052 deletions
-
4.gitignore
-
25CMakeLists.txt
-
0StormCPackConfig.cmake
-
4examples/dtmc/synchronous_leader/leader4_8.pm
-
4examples/dtmc/synchronous_leader/leader5_8.pm
-
4examples/dtmc/synchronous_leader/leader6_8.pm
-
9resources/3rdparty/cudd-2.5.0/CMakeLists.txt
-
3resources/3rdparty/cudd-2.5.0/src/cudd/cudd.h
-
261resources/3rdparty/cudd-2.5.0/src/cudd/cuddAddAbs.c
-
19resources/3rdparty/cudd-2.5.0/src/cudd/cuddExport.c
-
2resources/3rdparty/cudd-2.5.0/src/cudd/cuddInt.h
-
65resources/3rdparty/cudd-2.5.0/src/cudd/cuddSat.c
-
33resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.cc
-
7resources/3rdparty/cudd-2.5.0/src/obj/cuddObj.hh
-
2resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-lbtt.lex.cpp
-
2resources/3rdparty/ltl2dstar-0.5.1/src/parsers/nba-parser-promela.lex.cpp
-
298src/adapters/ExplicitModelAdapter.h
-
4src/adapters/GmmxxAdapter.h
-
2src/adapters/SymbolicModelAdapter.h
-
367src/counterexamples/MILPMinimalLabelSetGenerator.h
-
146src/counterexamples/PathBasedSubsystemGenerator.h
-
2src/counterexamples/SMTMinimalCommandSetGenerator.h
-
31src/exceptions/ExceptionMacros.h
-
17src/exceptions/InvalidOperationException.h
-
18src/exceptions/InvalidTypeException.h
-
63src/ir/Assignment.cpp
-
98src/ir/Assignment.h
-
49src/ir/BooleanVariable.cpp
-
70src/ir/BooleanVariable.h
-
94src/ir/Command.cpp
-
134src/ir/Command.h
-
25src/ir/IR.h
-
72src/ir/IntegerVariable.cpp
-
98src/ir/IntegerVariable.h
-
200src/ir/Module.cpp
-
230src/ir/Module.h
-
300src/ir/Program.cpp
-
318src/ir/Program.h
-
53src/ir/RewardModel.cpp
-
88src/ir/RewardModel.h
-
60src/ir/StateReward.cpp
-
85src/ir/StateReward.h
-
65src/ir/TransitionReward.cpp
-
99src/ir/TransitionReward.h
-
130src/ir/Update.cpp
-
152src/ir/Update.h
-
74src/ir/Variable.cpp
-
124src/ir/Variable.h
-
85src/ir/expressions/BaseExpression.cpp
-
172src/ir/expressions/BaseExpression.h
-
67src/ir/expressions/BinaryBooleanFunctionExpression.cpp
-
69src/ir/expressions/BinaryBooleanFunctionExpression.h
-
52src/ir/expressions/BinaryExpression.cpp
-
66src/ir/expressions/BinaryExpression.h
-
96src/ir/expressions/BinaryNumericalFunctionExpression.cpp
-
72src/ir/expressions/BinaryNumericalFunctionExpression.h
-
75src/ir/expressions/BinaryRelationExpression.cpp
-
69src/ir/expressions/BinaryRelationExpression.h
-
45src/ir/expressions/BooleanConstantExpression.cpp
-
49src/ir/expressions/BooleanConstantExpression.h
-
49src/ir/expressions/BooleanLiteralExpression.cpp
-
55src/ir/expressions/BooleanLiteralExpression.h
-
132src/ir/expressions/ConstantExpression.h
-
45src/ir/expressions/DoubleConstantExpression.cpp
-
49src/ir/expressions/DoubleConstantExpression.h
-
49src/ir/expressions/DoubleLiteralExpression.cpp
-
55src/ir/expressions/DoubleLiteralExpression.h
-
49src/ir/expressions/ExpressionVisitor.h
-
26src/ir/expressions/Expressions.h
-
48src/ir/expressions/IntegerConstantExpression.cpp
-
51src/ir/expressions/IntegerConstantExpression.h
-
53src/ir/expressions/IntegerLiteralExpression.cpp
-
57src/ir/expressions/IntegerLiteralExpression.h
-
62src/ir/expressions/UnaryBooleanFunctionExpression.cpp
-
68src/ir/expressions/UnaryBooleanFunctionExpression.h
-
39src/ir/expressions/UnaryExpression.cpp
-
55src/ir/expressions/UnaryExpression.h
-
86src/ir/expressions/UnaryNumericalFunctionExpression.cpp
-
70src/ir/expressions/UnaryNumericalFunctionExpression.h
-
120src/ir/expressions/VariableExpression.cpp
-
98src/ir/expressions/VariableExpression.h
-
2src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
-
78src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
-
2src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
-
2src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
-
6src/models/AbstractDeterministicModel.h
-
2src/models/AbstractModel.h
-
4src/models/AbstractNondeterministicModel.h
-
12src/models/Dtmc.h
-
14src/models/MarkovAutomaton.h
-
305src/parser/AtomicPropositionLabelingParser.cpp
-
36src/parser/AtomicPropositionLabelingParser.h
-
101src/parser/AutoParser.cpp
-
171src/parser/AutoParser.h
-
2src/parser/CslParser.h
-
80src/parser/DeterministicModelParser.cpp
-
151src/parser/DeterministicModelParser.h
-
465src/parser/DeterministicSparseTransitionParser.cpp
-
99src/parser/DeterministicSparseTransitionParser.h
-
400src/parser/ExpressionParser.cpp
@ -0,0 +1,31 @@ |
|||
#ifndef STORM_EXCEPTIONS_EXCEPTIONMACROS_H_ |
|||
#define STORM_EXCEPTIONS_EXCEPTIONMACROS_H_ |
|||
|
|||
#include <cassert> |
|||
|
|||
#include "log4cplus/logger.h" |
|||
#include "log4cplus/loggingmacros.h" |
|||
|
|||
extern log4cplus::Logger logger; |
|||
|
|||
#ifndef NDEBUG |
|||
#define LOG_ASSERT(cond, message) \ |
|||
{ \ |
|||
if (!(cond)) { \ |
|||
LOG4CPLUS_ERROR(logger, message); \ |
|||
assert(cond); \ |
|||
} \ |
|||
} while (false) |
|||
#else |
|||
#define LOG_ASSERT(cond, message) /* empty */ |
|||
#endif |
|||
|
|||
#define LOG_THROW(cond, exception, message) \ |
|||
{ \ |
|||
if (!(cond)) { \ |
|||
LOG4CPLUS_ERROR(logger, message); \ |
|||
throw exception() << message; \ |
|||
} \ |
|||
} while (false) |
|||
|
|||
#endif /* STORM_EXCEPTIONS_EXCEPTIONMACROS_H_ */ |
|||
@ -0,0 +1,17 @@ |
|||
#ifndef STORM_EXCEPTIONS_INVALIDOPERATIONEXCEPTION_H_ |
|||
#define STORM_EXCEPTIONS_INVALIDOPERATIONEXCEPTION_H_ |
|||
|
|||
#include "src/exceptions/BaseException.h" |
|||
|
|||
namespace storm { |
|||
|
|||
namespace exceptions { |
|||
|
|||
/*! |
|||
* @brief This exception is thrown when an operation is invalid in this context |
|||
*/ |
|||
STORM_EXCEPTION_DEFINE_NEW(InvalidOperationException) |
|||
|
|||
} // namespace exceptions |
|||
} // namespace storm |
|||
#endif // STORM_EXCEPTIONS_INVALIDOPERATIONEXCEPTION_H_ |
|||
@ -0,0 +1,18 @@ |
|||
#ifndef STORM_EXCEPTIONS_INVALIDTYPEEXCEPTION_H_ |
|||
#define STORM_EXCEPTIONS_INVALIDTYPEEXCEPTION_H_ |
|||
|
|||
#include "src/exceptions/BaseException.h" |
|||
|
|||
namespace storm { |
|||
|
|||
namespace exceptions { |
|||
|
|||
/*! |
|||
* @brief This exception is thrown when a type is invalid in this context |
|||
*/ |
|||
STORM_EXCEPTION_DEFINE_NEW(InvalidTypeException) |
|||
|
|||
} // namespace exceptions |
|||
|
|||
} // namespace storm |
|||
#endif // STORM_EXCEPTIONS_INVALIDTYPEEXCEPTION_H_ |
|||
@ -1,63 +0,0 @@ |
|||
/*
|
|||
* Assignment.cpp |
|||
* |
|||
* Created on: 12.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include <sstream>
|
|||
|
|||
#include "Assignment.h"
|
|||
#include "src/parser/prismparser/VariableState.h"
|
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
|
|||
Assignment::Assignment() : variableName(), expression() { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
Assignment::Assignment(std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& expression) |
|||
: variableName(variableName), expression(std::move(expression)) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
Assignment::Assignment(Assignment const& oldAssignment, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) |
|||
: variableName(oldAssignment.variableName), expression(oldAssignment.expression->clone(renaming, variableState)) { |
|||
auto renamingPair = renaming.find(oldAssignment.variableName); |
|||
if (renamingPair != renaming.end()) { |
|||
this->variableName = renamingPair->second; |
|||
} |
|||
} |
|||
|
|||
Assignment::Assignment(Assignment const& otherAssignment) : variableName(otherAssignment.variableName), expression() { |
|||
if (otherAssignment.expression != nullptr) { |
|||
expression = otherAssignment.expression->clone(); |
|||
} |
|||
} |
|||
|
|||
Assignment& Assignment::operator=(Assignment const& otherAssignment) { |
|||
if (this != &otherAssignment) { |
|||
this->variableName = otherAssignment.variableName; |
|||
this->expression = otherAssignment.expression->clone(); |
|||
} |
|||
|
|||
return *this; |
|||
} |
|||
|
|||
std::string const& Assignment::getVariableName() const { |
|||
return variableName; |
|||
} |
|||
|
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> const& Assignment::getExpression() const { |
|||
return expression; |
|||
} |
|||
|
|||
std::string Assignment::toString() const { |
|||
std::stringstream result; |
|||
result << "(" << variableName << "' = " << expression->toString() << ")"; |
|||
return result.str(); |
|||
} |
|||
|
|||
} // namespace ir
|
|||
} // namespace storm
|
|||
@ -1,98 +0,0 @@ |
|||
/* |
|||
* Assignment.h |
|||
* |
|||
* Created on: 06.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_ASSIGNMENT_H_ |
|||
#define STORM_IR_ASSIGNMENT_H_ |
|||
|
|||
#include <memory> |
|||
|
|||
#include "expressions/BaseExpression.h" |
|||
|
|||
namespace storm { |
|||
|
|||
namespace parser { |
|||
namespace prism { |
|||
class VariableState; |
|||
} // namespace prismparser |
|||
} // namespace parser |
|||
|
|||
namespace ir { |
|||
|
|||
/*! |
|||
* A class representing the assignment of an expression to a variable. |
|||
*/ |
|||
class Assignment { |
|||
public: |
|||
/*! |
|||
* Default constructor. Creates an empty assignment. |
|||
*/ |
|||
Assignment(); |
|||
|
|||
/*! |
|||
* Constructs an assignment using the given variable name and expression. |
|||
* |
|||
* @param variableName The variable that this assignment targets. |
|||
* @param expression The expression to assign to the variable. |
|||
*/ |
|||
Assignment(std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& expression); |
|||
|
|||
/*! |
|||
* Creates a copy of the given assignment and performs the provided renaming. |
|||
* |
|||
* @param oldAssignment The assignment to copy. |
|||
* @param renaming A mapping from names that are to be renamed to the names they are to be |
|||
* replaced with. |
|||
* @param variableState An object knowing about the variables in the system. |
|||
*/ |
|||
Assignment(Assignment const& oldAssignment, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState); |
|||
|
|||
/*! |
|||
* Performs a deep-copy of the given assignment. |
|||
* |
|||
* @param otherAssignment The assignment to copy. |
|||
*/ |
|||
Assignment(Assignment const& otherAssignment); |
|||
|
|||
/*! |
|||
* Performs a deep-copy of the given assignment and assigns it to the current one. |
|||
* |
|||
* @param otherAssignment The assignment to assign. |
|||
*/ |
|||
Assignment& operator=(Assignment const& otherAssignment); |
|||
|
|||
/*! |
|||
* Retrieves the name of the variable that this assignment targets. |
|||
* |
|||
* @return The name of the variable that this assignment targets. |
|||
*/ |
|||
std::string const& getVariableName() const; |
|||
|
|||
/*! |
|||
* Retrieves the expression that is assigned to the variable. |
|||
* |
|||
* @return The expression that is assigned to the variable. |
|||
*/ |
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> const& getExpression() const; |
|||
|
|||
/*! |
|||
* Retrieves a string representation of this assignment. |
|||
* @returns a string representation of this assignment. |
|||
*/ |
|||
std::string toString() const; |
|||
|
|||
private: |
|||
// The name of the variable that this assignment targets. |
|||
std::string variableName; |
|||
|
|||
// The expression that is assigned to the variable. |
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> expression; |
|||
}; |
|||
|
|||
} // namespace ir |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_ASSIGNMENT_H_ */ |
|||
@ -1,49 +0,0 @@ |
|||
/*
|
|||
* BooleanVariable.cpp |
|||
* |
|||
* Created on: 12.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include <sstream>
|
|||
|
|||
#include "BooleanVariable.h"
|
|||
#include "src/parser/prismparser/VariableState.h"
|
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
|
|||
BooleanVariable::BooleanVariable() : Variable() { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
BooleanVariable::BooleanVariable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue) |
|||
: Variable(localIndex, globalIndex, variableName, std::move(initialValue)) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
BooleanVariable::BooleanVariable(BooleanVariable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) |
|||
: Variable(oldVariable, newName, newGlobalIndex, renaming, variableState) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
BooleanVariable& BooleanVariable::operator=(BooleanVariable const& otherVariable) { |
|||
if (this != &otherVariable) { |
|||
Variable::operator=(otherVariable); |
|||
} |
|||
|
|||
return *this; |
|||
} |
|||
|
|||
std::string BooleanVariable::toString() const { |
|||
std::stringstream result; |
|||
result << this->getName() << ": bool"; |
|||
if (this->getInitialValue() != nullptr) { |
|||
result << " init " << this->getInitialValue()->toString(); |
|||
} |
|||
result << ";"; |
|||
return result.str(); |
|||
} |
|||
|
|||
} // namespace ir
|
|||
} // namespace storm
|
|||
@ -1,70 +0,0 @@ |
|||
/* |
|||
* BooleanVariable.h |
|||
* |
|||
* Created on: 08.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_BOOLEANVARIABLE_H_ |
|||
#define STORM_IR_BOOLEANVARIABLE_H_ |
|||
|
|||
#include <memory> |
|||
#include <map> |
|||
|
|||
#include "src/ir/Variable.h" |
|||
|
|||
namespace storm { |
|||
|
|||
namespace parser { |
|||
namespace prism { |
|||
class VariableState; |
|||
} // namespace prismparser |
|||
} // namespace parser |
|||
|
|||
namespace ir { |
|||
|
|||
/*! |
|||
* A class representing a boolean variable. |
|||
*/ |
|||
class BooleanVariable : public Variable { |
|||
public: |
|||
/*! |
|||
* Default constructor. Creates a boolean variable without a name. |
|||
*/ |
|||
BooleanVariable(); |
|||
|
|||
/*! |
|||
* Creates a boolean variable with the given name and the given initial value. |
|||
* |
|||
* @param localIndex A module-local unique index for the variable. |
|||
* @param globalIndex A globally unique index for the variable. |
|||
* @param variableName The name of the variable. |
|||
* @param initialValue The expression that defines the initial value of the variable. |
|||
*/ |
|||
BooleanVariable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue = nullptr); |
|||
|
|||
/*! |
|||
* Creates a copy of the given boolean variable and performs the provided renaming. |
|||
* |
|||
* @param oldVariable The variable to copy. |
|||
* @param newName New name of this variable. |
|||
* @param newGlobalIndex The new global index of the variable. |
|||
* @param renaming A mapping from names that are to be renamed to the names they are to be |
|||
* replaced with. |
|||
* @param variableState An object knowing about the variables in the system. |
|||
*/ |
|||
BooleanVariable(BooleanVariable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState); |
|||
|
|||
BooleanVariable& operator=(BooleanVariable const& otherVariable); |
|||
|
|||
/*! |
|||
* Retrieves a string representation of this variable. |
|||
* @returns a string representation of this variable. |
|||
*/ |
|||
std::string toString() const; |
|||
}; |
|||
|
|||
} // namespace ir |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_BOOLEANVARIABLE_H_ */ |
|||
@ -1,94 +0,0 @@ |
|||
/*
|
|||
* Command.cpp |
|||
* |
|||
* Created on: 12.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include <sstream>
|
|||
#include <iostream>
|
|||
|
|||
#include "Command.h"
|
|||
#include "src/parser/prismparser/VariableState.h"
|
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
|
|||
Command::Command() : actionName(), guardExpression(), updates(), globalIndex() { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
Command::Command(uint_fast64_t globalIndex, std::string const& actionName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& guardExpression, std::vector<storm::ir::Update> const& updates) |
|||
: actionName(actionName), guardExpression(std::move(guardExpression)), updates(updates), globalIndex(globalIndex) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
Command::Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState& variableState) |
|||
: actionName(oldCommand.getActionName()), guardExpression(oldCommand.guardExpression->clone(renaming, variableState)), globalIndex(newGlobalIndex) { |
|||
auto renamingPair = renaming.find(this->actionName); |
|||
if (renamingPair != renaming.end()) { |
|||
this->actionName = renamingPair->second; |
|||
} |
|||
this->updates.reserve(oldCommand.getNumberOfUpdates()); |
|||
for (Update const& update : oldCommand.updates) { |
|||
this->updates.emplace_back(update, variableState.getNextGlobalUpdateIndex(), renaming, variableState); |
|||
variableState.nextGlobalUpdateIndex++; |
|||
} |
|||
} |
|||
|
|||
Command::Command(Command const& otherCommand) : actionName(otherCommand.actionName), guardExpression(), updates(otherCommand.updates), globalIndex(otherCommand.globalIndex) { |
|||
if (otherCommand.guardExpression != nullptr) { |
|||
guardExpression = otherCommand.guardExpression->clone(); |
|||
} |
|||
} |
|||
|
|||
Command& Command::operator=(Command const& otherCommand) { |
|||
if (this != &otherCommand) { |
|||
this->actionName = otherCommand.actionName; |
|||
this->guardExpression = otherCommand.guardExpression->clone(); |
|||
this->updates = otherCommand.updates; |
|||
this->globalIndex = otherCommand.globalIndex; |
|||
} |
|||
|
|||
return *this; |
|||
} |
|||
|
|||
std::string const& Command::getActionName() const { |
|||
return this->actionName; |
|||
} |
|||
|
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> const& Command::getGuard() const { |
|||
return guardExpression; |
|||
} |
|||
|
|||
uint_fast64_t Command::getNumberOfUpdates() const { |
|||
return this->updates.size(); |
|||
} |
|||
|
|||
storm::ir::Update const& Command::getUpdate(uint_fast64_t index) const { |
|||
return this->updates[index]; |
|||
} |
|||
|
|||
std::vector<storm::ir::Update> const& Command::getUpdates() const { |
|||
return this->updates; |
|||
} |
|||
|
|||
uint_fast64_t Command::getGlobalIndex() const { |
|||
return this->globalIndex; |
|||
} |
|||
|
|||
std::string Command::toString() const { |
|||
std::stringstream result; |
|||
result << "[" << actionName << "] " << guardExpression->toString() << " -> "; |
|||
for (uint_fast64_t i = 0; i < updates.size(); ++i) { |
|||
result << updates[i].toString(); |
|||
if (i < updates.size() - 1) { |
|||
result << " + "; |
|||
} |
|||
} |
|||
result << ";"; |
|||
return result.str(); |
|||
} |
|||
|
|||
} // namespace ir
|
|||
} // namespace storm
|
|||
@ -1,134 +0,0 @@ |
|||
/* |
|||
* Command.h |
|||
* |
|||
* Created on: 06.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_COMMAND_H_ |
|||
#define STORM_IR_COMMAND_H_ |
|||
|
|||
#include <vector> |
|||
#include <string> |
|||
#include <map> |
|||
|
|||
#include "expressions/BaseExpression.h" |
|||
#include "Update.h" |
|||
|
|||
namespace storm { |
|||
|
|||
namespace parser { |
|||
namespace prism { |
|||
class VariableState; |
|||
} // namespace prismparser |
|||
} // namespace parser |
|||
|
|||
namespace ir { |
|||
|
|||
/*! |
|||
* A class representing a command. |
|||
*/ |
|||
class Command { |
|||
public: |
|||
/*! |
|||
* Default constructor. Creates a a command without name, guard and updates. |
|||
*/ |
|||
Command(); |
|||
|
|||
/*! |
|||
* Creates a command with the given name, guard and updates. |
|||
* |
|||
* @param globalIndex The global index of the command. |
|||
* @param actionName The action name of the command. |
|||
* @param guardExpression the expression that defines the guard of the command. |
|||
* @param updates A list of updates that is associated with this command. |
|||
*/ |
|||
Command(uint_fast64_t globalIndex, std::string const& actionName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& guardExpression, std::vector<storm::ir::Update> const& updates); |
|||
|
|||
/*! |
|||
* Creates a copy of the given command and performs the provided renaming. |
|||
* |
|||
* @param oldCommand The command to copy. |
|||
* @param newGlobalIndex The global index of the copy of the command. |
|||
* @param renaming A mapping from names that are to be renamed to the names they are to be |
|||
* replaced with. |
|||
* @param variableState An object knowing about the variables in the system. |
|||
*/ |
|||
Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState& variableState); |
|||
|
|||
/*! |
|||
* Performs a deep-copy of the given command. |
|||
* |
|||
* @param otherCommand The command to copy. |
|||
*/ |
|||
Command(Command const& otherCommand); |
|||
|
|||
Command& operator=(Command const& otherCommand); |
|||
|
|||
/*! |
|||
* Retrieves the action name of this command. |
|||
* |
|||
* @return The action name of this command. |
|||
*/ |
|||
std::string const& getActionName() const; |
|||
|
|||
/*! |
|||
* Retrieves a reference to the guard of the command. |
|||
* |
|||
* @return A reference to the guard of the command. |
|||
*/ |
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> const& getGuard() const; |
|||
|
|||
/*! |
|||
* Retrieves the number of updates associated with this command. |
|||
* |
|||
* @return The number of updates associated with this command. |
|||
*/ |
|||
uint_fast64_t getNumberOfUpdates() const; |
|||
|
|||
/*! |
|||
* Retrieves a reference to the update with the given index. |
|||
* |
|||
* @return A reference to the update with the given index. |
|||
*/ |
|||
storm::ir::Update const& getUpdate(uint_fast64_t index) const; |
|||
|
|||
/*! |
|||
* Retrieves a vector of all updates associated with this command. |
|||
* |
|||
* @return A vector of updates associated with this command. |
|||
*/ |
|||
std::vector<storm::ir::Update> const& getUpdates() const; |
|||
|
|||
/*! |
|||
* Retrieves the global index of the command, that is, a unique index over all modules. |
|||
* |
|||
* @return The global index of the command. |
|||
*/ |
|||
uint_fast64_t getGlobalIndex() const; |
|||
|
|||
/*! |
|||
* Retrieves a string representation of this command. |
|||
* |
|||
* @return A string representation of this command. |
|||
*/ |
|||
std::string toString() const; |
|||
|
|||
private: |
|||
// The name of the command. |
|||
std::string actionName; |
|||
|
|||
// The expression that defines the guard of the command. |
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> guardExpression; |
|||
|
|||
// The list of updates of the command. |
|||
std::vector<storm::ir::Update> updates; |
|||
|
|||
// The global index of the command. |
|||
uint_fast64_t globalIndex; |
|||
}; |
|||
|
|||
} // namespace ir |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_COMMAND_H_ */ |
|||
@ -1,25 +0,0 @@ |
|||
/* |
|||
* IR.h |
|||
* |
|||
* Created on: 06.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_IR_H_ |
|||
#define STORM_IR_IR_H_ |
|||
|
|||
// Bundle all headers to make it easy to include them. |
|||
#include "expressions/Expressions.h" |
|||
#include "Assignment.h" |
|||
#include "Update.h" |
|||
#include "Command.h" |
|||
#include "Variable.h" |
|||
#include "BooleanVariable.h" |
|||
#include "IntegerVariable.h" |
|||
#include "Module.h" |
|||
#include "StateReward.h" |
|||
#include "TransitionReward.h" |
|||
#include "RewardModel.h" |
|||
#include "Program.h" |
|||
|
|||
#endif /* STORM_IR_IR_H_ */ |
|||
@ -1,72 +0,0 @@ |
|||
/*
|
|||
* IntegerVariable.cpp |
|||
* |
|||
* Created on: 12.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include <sstream>
|
|||
#include <iostream>
|
|||
|
|||
#include "IntegerVariable.h"
|
|||
#include "src/parser/prismparser/VariableState.h"
|
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
|
|||
IntegerVariable::IntegerVariable() : lowerBound(), upperBound() { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
IntegerVariable::IntegerVariable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& lowerBound, std::unique_ptr<storm::ir::expressions::BaseExpression>&& upperBound, std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue) |
|||
: Variable(localIndex, globalIndex, variableName, std::move(initialValue)), lowerBound(std::move(lowerBound)), upperBound(std::move(upperBound)) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
IntegerVariable::IntegerVariable(IntegerVariable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) |
|||
: Variable(oldVariable, newName, newGlobalIndex, renaming, variableState), lowerBound(oldVariable.lowerBound->clone(renaming, variableState)), upperBound(oldVariable.upperBound->clone(renaming, variableState)) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
IntegerVariable::IntegerVariable(IntegerVariable const& otherVariable) : Variable(otherVariable.getLocalIndex(), otherVariable.getGlobalIndex(), otherVariable.getName(), nullptr), lowerBound(), upperBound() { |
|||
if (otherVariable.getInitialValue() != nullptr) { |
|||
setInitialValue(otherVariable.getInitialValue()->clone()); |
|||
} |
|||
if (otherVariable.lowerBound != nullptr) { |
|||
lowerBound = otherVariable.lowerBound->clone(); |
|||
} |
|||
if (otherVariable.upperBound != nullptr) { |
|||
upperBound = otherVariable.upperBound->clone(); |
|||
} |
|||
} |
|||
|
|||
IntegerVariable& IntegerVariable::operator=(IntegerVariable const& otherVariable) { |
|||
if (this != &otherVariable) { |
|||
Variable::operator=(otherVariable); |
|||
this->lowerBound = otherVariable.lowerBound->clone(); |
|||
this->upperBound = otherVariable.upperBound->clone(); |
|||
} |
|||
|
|||
return *this; |
|||
} |
|||
|
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> const& IntegerVariable::getLowerBound() const { |
|||
return this->lowerBound; |
|||
} |
|||
|
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> const& IntegerVariable::getUpperBound() const { |
|||
return this->upperBound; |
|||
} |
|||
|
|||
std::string IntegerVariable::toString() const { |
|||
std::stringstream result; |
|||
result << this->getName() << ": [" << lowerBound->toString() << ".." << upperBound->toString() << "]"; |
|||
if (this->getInitialValue() != nullptr) { |
|||
result << " init " + this->getInitialValue()->toString(); |
|||
} |
|||
result << ";"; |
|||
return result.str(); |
|||
} |
|||
|
|||
} // namespace ir
|
|||
} // namespace storm
|
|||
@ -1,98 +0,0 @@ |
|||
/* |
|||
* IntegerVariable.h |
|||
* |
|||
* Created on: 08.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_INTEGERVARIABLE_H_ |
|||
#define STORM_IR_INTEGERVARIABLE_H_ |
|||
|
|||
#include <memory> |
|||
|
|||
#include "src/ir/Variable.h" |
|||
#include "expressions/BaseExpression.h" |
|||
|
|||
namespace storm { |
|||
|
|||
namespace parser { |
|||
namespace prism { |
|||
class VariableState; |
|||
} // namespace prismparser |
|||
} // namespace parser |
|||
|
|||
namespace ir { |
|||
|
|||
/*! |
|||
* A class representing an integer variable. |
|||
*/ |
|||
class IntegerVariable : public Variable { |
|||
public: |
|||
/*! |
|||
* Default constructor. Creates an integer variable without a name and lower and upper bounds. |
|||
*/ |
|||
IntegerVariable(); |
|||
|
|||
/*! |
|||
* Creates a boolean variable with the given name and the given initial value. |
|||
* |
|||
* @param localIndex A module-local unique index for the variable. |
|||
* @param globalIndex A globally unique index for the variable. |
|||
* @param variableName The name of the variable. |
|||
* @param lowerBound the lower bound of the domain of the variable. |
|||
* @param upperBound the upper bound of the domain of the variable. |
|||
* @param initialValue the expression that defines the initial value of the variable. |
|||
*/ |
|||
IntegerVariable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& lowerBound, std::unique_ptr<storm::ir::expressions::BaseExpression>&& upperBound, std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue = nullptr); |
|||
|
|||
/*! |
|||
* Creates a copy of the given integer variable and performs the provided renaming. |
|||
* |
|||
* @param oldVariable The variable to copy. |
|||
* @param newName New name of this variable. |
|||
* @param newGlobalIndex The new global index of the variable. |
|||
* @param renaming A mapping from names that are to be renamed to the names they are to be |
|||
* replaced with. |
|||
* @param variableState An object knowing about the variables in the system. |
|||
*/ |
|||
IntegerVariable(IntegerVariable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState); |
|||
|
|||
/*! |
|||
* Performs a deep-copy of the given variable. |
|||
* |
|||
* @param otherVariable The variable to copy. |
|||
*/ |
|||
IntegerVariable(IntegerVariable const& otherVariable); |
|||
|
|||
IntegerVariable& operator=(IntegerVariable const& otherVariable); |
|||
|
|||
/*! |
|||
* Retrieves the lower bound for this integer variable. |
|||
* @returns the lower bound for this integer variable. |
|||
*/ |
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> const& getLowerBound() const; |
|||
|
|||
/*! |
|||
* Retrieves the upper bound for this integer variable. |
|||
* @returns the upper bound for this integer variable. |
|||
*/ |
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> const& getUpperBound() const; |
|||
|
|||
/*! |
|||
* Retrieves a string representation of this variable. |
|||
* @returns a string representation of this variable. |
|||
*/ |
|||
std::string toString() const; |
|||
|
|||
private: |
|||
// The lower bound of the domain of the variable. |
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> lowerBound; |
|||
|
|||
// The upper bound of the domain of the variable. |
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> upperBound; |
|||
}; |
|||
|
|||
} // namespace ir |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_INTEGERVARIABLE_H_ */ |
|||
@ -1,200 +0,0 @@ |
|||
/*
|
|||
* Module.cpp |
|||
* |
|||
* Created on: 12.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include <sstream>
|
|||
#include <iostream>
|
|||
#include "utility/OsDetection.h"
|
|||
|
|||
#include "Module.h"
|
|||
#include "src/parser/prismparser/VariableState.h"
|
|||
#include "src/exceptions/OutOfRangeException.h"
|
|||
#include "src/exceptions/InvalidArgumentException.h"
|
|||
|
|||
#include "log4cplus/logger.h"
|
|||
#include "log4cplus/loggingmacros.h"
|
|||
extern log4cplus::Logger logger; |
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
|
|||
Module::Module() : moduleName(), booleanVariables(), integerVariables(), booleanVariableToLocalIndexMap(), |
|||
integerVariableToLocalIndexMap(), commands(), actions(), actionsToCommandIndexMap() { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
Module::Module(std::string const& moduleName, |
|||
std::vector<storm::ir::BooleanVariable> const& booleanVariables, |
|||
std::vector<storm::ir::IntegerVariable> const& integerVariables, |
|||
std::map<std::string, uint_fast64_t> const& booleanVariableToLocalIndexMap, |
|||
std::map<std::string, uint_fast64_t> const& integerVariableToLocalIndexMap, |
|||
std::vector<storm::ir::Command> const& commands) |
|||
: moduleName(moduleName), booleanVariables(booleanVariables), integerVariables(integerVariables), |
|||
booleanVariableToLocalIndexMap(booleanVariableToLocalIndexMap), |
|||
integerVariableToLocalIndexMap(integerVariableToLocalIndexMap), commands(commands), actions(), actionsToCommandIndexMap() { |
|||
// Initialize the internal mappings for fast information retrieval.
|
|||
this->collectActions(); |
|||
} |
|||
|
|||
Module::Module(Module const& oldModule, std::string const& newModuleName, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState& variableState) |
|||
: moduleName(newModuleName), booleanVariableToLocalIndexMap(oldModule.booleanVariableToLocalIndexMap), integerVariableToLocalIndexMap(oldModule.integerVariableToLocalIndexMap) { |
|||
LOG4CPLUS_TRACE(logger, "Start renaming " << oldModule.getName() << " to " << moduleName << "."); |
|||
|
|||
// Iterate over boolean variables and rename them. If a variable was not renamed, this is an error and an exception
|
|||
// is thrown.
|
|||
this->booleanVariables.reserve(oldModule.getNumberOfBooleanVariables()); |
|||
for (BooleanVariable const& booleanVariable : oldModule.booleanVariables) { |
|||
auto renamingPair = renaming.find(booleanVariable.getName()); |
|||
if (renamingPair == renaming.end()) { |
|||
LOG4CPLUS_ERROR(logger, "Boolean variable " << moduleName << "." << booleanVariable.getName() << " was not renamed."); |
|||
throw storm::exceptions::InvalidArgumentException() << "Boolean variable " << moduleName << "." << booleanVariable.getName() << " was not renamed."; |
|||
} else { |
|||
uint_fast64_t globalIndex = variableState.addBooleanVariable(renamingPair->second); |
|||
this->booleanVariables.emplace_back(booleanVariable, renamingPair->second, globalIndex, renaming, variableState); |
|||
} |
|||
} |
|||
// Now do the same for the integer variables.
|
|||
this->integerVariables.reserve(oldModule.getNumberOfIntegerVariables()); |
|||
for (IntegerVariable const& integerVariable : oldModule.integerVariables) { |
|||
auto renamingPair = renaming.find(integerVariable.getName()); |
|||
if (renamingPair == renaming.end()) { |
|||
LOG4CPLUS_ERROR(logger, "Integer variable " << moduleName << "." << integerVariable.getName() << " was not renamed."); |
|||
throw storm::exceptions::InvalidArgumentException() << "Integer variable " << moduleName << "." << integerVariable.getName() << " was not renamed."; |
|||
} else { |
|||
uint_fast64_t globalIndex = variableState.addIntegerVariable(renamingPair->second); |
|||
this->integerVariables.emplace_back(integerVariable, renamingPair->second, globalIndex, renaming, variableState); |
|||
} |
|||
} |
|||
|
|||
// Now we are ready to clone all commands and rename them if requested.
|
|||
this->commands.reserve(oldModule.getNumberOfCommands()); |
|||
for (Command const& command : oldModule.commands) { |
|||
this->commands.emplace_back(command, variableState.getNextGlobalCommandIndex(), renaming, variableState); |
|||
variableState.nextGlobalCommandIndex++; |
|||
} |
|||
this->collectActions(); |
|||
|
|||
LOG4CPLUS_TRACE(logger, "Finished renaming..."); |
|||
} |
|||
|
|||
uint_fast64_t Module::getNumberOfBooleanVariables() const { |
|||
return this->booleanVariables.size(); |
|||
} |
|||
|
|||
storm::ir::BooleanVariable const& Module::getBooleanVariable(uint_fast64_t index) const { |
|||
return this->booleanVariables[index]; |
|||
} |
|||
|
|||
storm::ir::BooleanVariable const& Module::getBooleanVariable(std::string const& variableName) const { |
|||
uint_fast64_t index = this->getBooleanVariableIndex(variableName); |
|||
return this->booleanVariables[index]; |
|||
} |
|||
|
|||
uint_fast64_t Module::getNumberOfIntegerVariables() const { |
|||
return this->integerVariables.size(); |
|||
} |
|||
|
|||
storm::ir::IntegerVariable const& Module::getIntegerVariable(uint_fast64_t index) const { |
|||
return this->integerVariables[index]; |
|||
} |
|||
|
|||
storm::ir::IntegerVariable const& Module::getIntegerVariable(std::string const& variableName) const { |
|||
uint_fast64_t index = this->getIntegerVariableIndex(variableName); |
|||
return this->integerVariables[index]; |
|||
} |
|||
|
|||
uint_fast64_t Module::getNumberOfCommands() const { |
|||
return this->commands.size(); |
|||
} |
|||
|
|||
uint_fast64_t Module::getBooleanVariableIndex(std::string const& variableName) const { |
|||
auto it = booleanVariableToLocalIndexMap.find(variableName); |
|||
if (it != booleanVariableToLocalIndexMap.end()) { |
|||
return it->second; |
|||
} |
|||
LOG4CPLUS_ERROR(logger, "Cannot retrieve index of unknown boolean variable " << variableName << "."); |
|||
throw storm::exceptions::InvalidArgumentException() << "Cannot retrieve index of unknown boolean variable " << variableName << "."; |
|||
} |
|||
|
|||
uint_fast64_t Module::getIntegerVariableIndex(std::string const& variableName) const { |
|||
auto it = integerVariableToLocalIndexMap.find(variableName); |
|||
if (it != integerVariableToLocalIndexMap.end()) { |
|||
return it->second; |
|||
} |
|||
LOG4CPLUS_ERROR(logger, "Cannot retrieve index of unknown integer variable " << variableName << "."); |
|||
throw storm::exceptions::InvalidArgumentException() << "Cannot retrieve index of unknown integer variable " << variableName << "."; |
|||
} |
|||
|
|||
storm::ir::Command const& Module::getCommand(uint_fast64_t index) const { |
|||
return this->commands[index]; |
|||
} |
|||
|
|||
std::string const& Module::getName() const { |
|||
return this->moduleName; |
|||
} |
|||
|
|||
std::string Module::toString() const { |
|||
std::stringstream result; |
|||
result << "module " << moduleName << std::endl; |
|||
for (auto variable : booleanVariables) { |
|||
result << "\t" << variable.toString() << std::endl; |
|||
} |
|||
for (auto variable : integerVariables) { |
|||
result << "\t" << variable.toString() << std::endl; |
|||
} |
|||
for (auto command : commands) { |
|||
result << "\t" << command.toString() << std::endl; |
|||
} |
|||
result << "endmodule" << std::endl; |
|||
return result.str(); |
|||
} |
|||
|
|||
std::set<std::string> const& Module::getActions() const { |
|||
return this->actions; |
|||
} |
|||
|
|||
bool Module::hasAction(std::string const& action) const { |
|||
auto const& actionEntry = this->actions.find(action); |
|||
if (actionEntry != this->actions.end()) { |
|||
return true; |
|||
} |
|||
return false; |
|||
} |
|||
|
|||
std::set<uint_fast64_t> const& Module::getCommandsByAction(std::string const& action) const { |
|||
auto actionsCommandSetPair = this->actionsToCommandIndexMap.find(action); |
|||
if (actionsCommandSetPair != this->actionsToCommandIndexMap.end()) { |
|||
return actionsCommandSetPair->second; |
|||
} |
|||
LOG4CPLUS_ERROR(logger, "Action name '" << action << "' does not exist in module."); |
|||
throw storm::exceptions::OutOfRangeException() << "Action name '" << action << "' does not exist in module."; |
|||
} |
|||
|
|||
void Module::collectActions() { |
|||
for (unsigned int id = 0; id < this->commands.size(); id++) { |
|||
std::string const& action = this->commands[id].getActionName(); |
|||
if (action != "") { |
|||
if (this->actionsToCommandIndexMap.find(action) == this->actionsToCommandIndexMap.end()) { |
|||
this->actionsToCommandIndexMap.emplace(action, std::set<uint_fast64_t>()); |
|||
} |
|||
this->actionsToCommandIndexMap[action].insert(id); |
|||
this->actions.insert(action); |
|||
} |
|||
} |
|||
} |
|||
|
|||
void Module::restrictCommands(boost::container::flat_set<uint_fast64_t> const& indexSet) { |
|||
std::vector<storm::ir::Command> newCommands; |
|||
for (auto const& command : commands) { |
|||
if (indexSet.find(command.getGlobalIndex()) != indexSet.end()) { |
|||
newCommands.push_back(std::move(command)); |
|||
} |
|||
} |
|||
commands = std::move(newCommands); |
|||
} |
|||
|
|||
} // namespace ir
|
|||
} // namespace storm
|
|||
@ -1,230 +0,0 @@ |
|||
/* |
|||
* Module.h |
|||
* |
|||
* Created on: 04.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_MODULE_H_ |
|||
#define STORM_IR_MODULE_H_ |
|||
|
|||
#include "utility/OsDetection.h" |
|||
#include <boost/container/flat_set.hpp> |
|||
|
|||
#ifdef LINUX |
|||
#include <boost/container/map.hpp> |
|||
#endif |
|||
#include <map> |
|||
|
|||
#include <set> |
|||
#include <string> |
|||
#include <vector> |
|||
#include <memory> |
|||
|
|||
#include "BooleanVariable.h" |
|||
#include "IntegerVariable.h" |
|||
#include "Command.h" |
|||
#include "expressions/VariableExpression.h" |
|||
|
|||
namespace storm { |
|||
|
|||
namespace parser { |
|||
namespace prism { |
|||
class VariableState; |
|||
} // namespace prismparser |
|||
} // namespace parser |
|||
|
|||
namespace ir { |
|||
|
|||
/*! |
|||
* A class representing a module. |
|||
*/ |
|||
class Module { |
|||
public: |
|||
/*! |
|||
* Default constructor. Creates an empty module. |
|||
*/ |
|||
Module(); |
|||
|
|||
/*! |
|||
* Creates a module with the given name, variables and commands. |
|||
* |
|||
* @param moduleName The name of the module. |
|||
* @param booleanVariables The boolean variables defined by the module. |
|||
* @param integerVariables The integer variables defined by the module. |
|||
* @param booleanVariableToLocalIndexMap A mapping of boolean variables to local (i.e. module-local) indices. |
|||
* @param integerVariableToLocalIndexMap A mapping of integer variables to local (i.e. module-local) indices. |
|||
* @param commands The commands of the module. |
|||
*/ |
|||
Module(std::string const& moduleName, std::vector<storm::ir::BooleanVariable> const& booleanVariables, |
|||
std::vector<storm::ir::IntegerVariable> const& integerVariables, |
|||
std::map<std::string, uint_fast64_t> const& booleanVariableToLocalIndexMap, |
|||
std::map<std::string, uint_fast64_t> const& integerVariableToLocalIndexMap, |
|||
std::vector<storm::ir::Command> const& commands); |
|||
|
|||
/*! |
|||
* Special copy constructor, implementing the module renaming functionality. |
|||
* This will create a new module having all identifiers renamed according to the given map. |
|||
* |
|||
* @param oldModule The module to be copied. |
|||
* @param newModuleName The name of the new module. |
|||
* @param renaming A mapping of identifiers to the new identifiers they are to be replaced with. |
|||
* @param variableState An object knowing about the variables in the system. |
|||
*/ |
|||
Module(Module const& oldModule, std::string const& newModuleName, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState& variableState); |
|||
|
|||
/*! |
|||
* Retrieves the number of boolean variables in the module. |
|||
* |
|||
* @return the number of boolean variables in the module. |
|||
*/ |
|||
uint_fast64_t getNumberOfBooleanVariables() const; |
|||
|
|||
/*! |
|||
* Retrieves a reference to the boolean variable with the given index. |
|||
* |
|||
* @return A reference to the boolean variable with the given index. |
|||
*/ |
|||
storm::ir::BooleanVariable const& getBooleanVariable(uint_fast64_t index) const; |
|||
|
|||
/*! |
|||
* Retrieves a reference to the boolean variable with the given name. |
|||
* |
|||
* @return A reference to the boolean variable with the given name. |
|||
*/ |
|||
storm::ir::BooleanVariable const& getBooleanVariable(std::string const& variableName) const; |
|||
|
|||
/*! |
|||
* Retrieves the number of integer variables in the module. |
|||
* |
|||
* @return The number of integer variables in the module. |
|||
*/ |
|||
uint_fast64_t getNumberOfIntegerVariables() const; |
|||
|
|||
/*! |
|||
* Retrieves a reference to the integer variable with the given index. |
|||
* |
|||
* @return A reference to the integer variable with the given index. |
|||
*/ |
|||
storm::ir::IntegerVariable const& getIntegerVariable(uint_fast64_t index) const; |
|||
|
|||
/*! |
|||
* Retrieves a reference to the boolean variable with the given name. |
|||
* |
|||
* @return A reference to the boolean variable with the given name. |
|||
*/ |
|||
storm::ir::IntegerVariable const& getIntegerVariable(std::string const& variableName) const; |
|||
|
|||
/*! |
|||
* Retrieves the number of commands of this module. |
|||
* |
|||
* @return the number of commands of this module. |
|||
*/ |
|||
uint_fast64_t getNumberOfCommands() const; |
|||
|
|||
/*! |
|||
* Retrieves the index of the boolean variable with the given name. |
|||
* |
|||
* @param variableName The name of the boolean variable whose index to retrieve. |
|||
* @return The index of the boolean variable with the given name. |
|||
*/ |
|||
uint_fast64_t getBooleanVariableIndex(std::string const& variableName) const; |
|||
|
|||
/*! |
|||
* Retrieves the index of the integer variable with the given name. |
|||
* |
|||
* @param variableName The name of the integer variable whose index to retrieve. |
|||
* @return The index of the integer variable with the given name. |
|||
*/ |
|||
uint_fast64_t getIntegerVariableIndex(std::string const& variableName) const; |
|||
|
|||
/*! |
|||
* Retrieves a reference to the command with the given index. |
|||
* |
|||
* @return A reference to the command with the given index. |
|||
*/ |
|||
storm::ir::Command const& getCommand(uint_fast64_t index) const; |
|||
|
|||
/*! |
|||
* Retrieves the name of the module. |
|||
* |
|||
* @return The name of the module. |
|||
*/ |
|||
std::string const& getName() const; |
|||
|
|||
/*! |
|||
* Retrieves a string representation of this module. |
|||
* |
|||
* @return a string representation of this module. |
|||
*/ |
|||
std::string toString() const; |
|||
|
|||
/*! |
|||
* Retrieves the set of actions present in this module. |
|||
* |
|||
* @return the set of actions present in this module. |
|||
*/ |
|||
std::set<std::string> const& getActions() const; |
|||
|
|||
/*! |
|||
* Retrieves whether or not this module contains a command labeled with the given action. |
|||
* |
|||
* @param action The action name to look for in this module. |
|||
* @return True if the module has at least one command labeled with the given action. |
|||
*/ |
|||
bool hasAction(std::string const& action) const; |
|||
|
|||
/*! |
|||
* Retrieves the indices of all commands within this module that are labelled by the given action. |
|||
* |
|||
* @param action The action with which the commands have to be labelled. |
|||
* @return A set of indices of commands that are labelled with the given action. |
|||
*/ |
|||
std::set<uint_fast64_t> const& getCommandsByAction(std::string const& action) const; |
|||
|
|||
/*! |
|||
* Deletes all commands with indices not in the given set from the module. |
|||
* |
|||
* @param indexSet The set of indices for which to keep the commands. |
|||
*/ |
|||
void restrictCommands(boost::container::flat_set<uint_fast64_t> const& indexSet); |
|||
private: |
|||
|
|||
/*! |
|||
* Computes the locally maintained mappings for fast data retrieval. |
|||
*/ |
|||
void collectActions(); |
|||
|
|||
// The name of the module. |
|||
std::string moduleName; |
|||
|
|||
// A list of boolean variables. |
|||
std::vector<storm::ir::BooleanVariable> booleanVariables; |
|||
|
|||
// A list of integer variables. |
|||
std::vector<storm::ir::IntegerVariable> integerVariables; |
|||
|
|||
// A map of boolean variable names to their index. |
|||
std::map<std::string, uint_fast64_t> booleanVariableToLocalIndexMap; |
|||
|
|||
// A map of integer variable names to their index. |
|||
std::map<std::string, uint_fast64_t> integerVariableToLocalIndexMap; |
|||
|
|||
// The commands associated with the module. |
|||
std::vector<storm::ir::Command> commands; |
|||
|
|||
// The set of actions present in this module. |
|||
std::set<std::string> actions; |
|||
|
|||
// A map of actions to the set of commands labeled with this action. |
|||
#ifdef LINUX |
|||
boost::container::map<std::string, std::set<uint_fast64_t>> actionsToCommandIndexMap; |
|||
#else |
|||
std::map<std::string, std::set<uint_fast64_t>> actionsToCommandIndexMap; |
|||
#endif |
|||
}; |
|||
|
|||
} // namespace ir |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_MODULE_H_ */ |
|||
@ -1,300 +0,0 @@ |
|||
/*
|
|||
* Program.cpp |
|||
* |
|||
* Created on: 12.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include <sstream>
|
|||
#include <iostream>
|
|||
|
|||
#include "Program.h"
|
|||
#include "exceptions/InvalidArgumentException.h"
|
|||
#include "src/exceptions/OutOfRangeException.h"
|
|||
|
|||
#include "log4cplus/logger.h"
|
|||
#include "log4cplus/loggingmacros.h"
|
|||
extern log4cplus::Logger logger; |
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
|
|||
Program::Program() : modelType(UNDEFINED), booleanUndefinedConstantExpressions(), integerUndefinedConstantExpressions(), doubleUndefinedConstantExpressions(), modules(), rewards(), actions(), actionsToModuleIndexMap(), variableToModuleIndexMap() { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
Program::Program(ModelType modelType, |
|||
std::map<std::string, std::unique_ptr<storm::ir::expressions::BooleanConstantExpression>> const& booleanUndefinedConstantExpressions, |
|||
std::map<std::string, std::unique_ptr<storm::ir::expressions::IntegerConstantExpression>> const& integerUndefinedConstantExpressions, |
|||
std::map<std::string, std::unique_ptr<storm::ir::expressions::DoubleConstantExpression>> const& doubleUndefinedConstantExpressions, |
|||
std::vector<BooleanVariable> const& globalBooleanVariables, |
|||
std::vector<IntegerVariable> const& globalIntegerVariables, |
|||
std::map<std::string, uint_fast64_t> const& globalBooleanVariableToIndexMap, |
|||
std::map<std::string, uint_fast64_t> const& globalIntegerVariableToIndexMap, |
|||
std::vector<storm::ir::Module> const& modules, |
|||
std::map<std::string, storm::ir::RewardModel> const& rewards, |
|||
std::map<std::string, std::unique_ptr<storm::ir::expressions::BaseExpression>> const& labels) |
|||
: modelType(modelType), globalBooleanVariables(globalBooleanVariables), globalIntegerVariables(globalIntegerVariables), |
|||
globalBooleanVariableToIndexMap(globalBooleanVariableToIndexMap), globalIntegerVariableToIndexMap(globalIntegerVariableToIndexMap), |
|||
modules(modules), rewards(rewards), actionsToModuleIndexMap(), variableToModuleIndexMap() { |
|||
|
|||
// Perform a deep-copy of the maps.
|
|||
for (auto const& booleanUndefinedConstant : booleanUndefinedConstantExpressions) { |
|||
this->booleanUndefinedConstantExpressions[booleanUndefinedConstant.first] = std::unique_ptr<storm::ir::expressions::BooleanConstantExpression>(new storm::ir::expressions::BooleanConstantExpression(*booleanUndefinedConstant.second)); |
|||
} |
|||
for (auto const& integerUndefinedConstant : integerUndefinedConstantExpressions) { |
|||
this->integerUndefinedConstantExpressions[integerUndefinedConstant.first] = std::unique_ptr<storm::ir::expressions::IntegerConstantExpression>(new storm::ir::expressions::IntegerConstantExpression(*integerUndefinedConstant.second)); |
|||
} |
|||
for (auto const& doubleUndefinedConstant : doubleUndefinedConstantExpressions) { |
|||
this->doubleUndefinedConstantExpressions[doubleUndefinedConstant.first] = std::unique_ptr<storm::ir::expressions::DoubleConstantExpression>(new storm::ir::expressions::DoubleConstantExpression(*doubleUndefinedConstant.second)); |
|||
} |
|||
for (auto const& label : labels) { |
|||
this->labels[label.first] = label.second->clone(); |
|||
} |
|||
|
|||
// Now build the mapping from action names to module indices so that the lookup can later be performed quickly.
|
|||
for (unsigned int moduleIndex = 0; moduleIndex < this->modules.size(); moduleIndex++) { |
|||
Module const& module = this->modules[moduleIndex]; |
|||
|
|||
for (auto const& action : module.getActions()) { |
|||
if (this->actionsToModuleIndexMap.count(action) == 0) { |
|||
this->actionsToModuleIndexMap[action] = std::set<uint_fast64_t>(); |
|||
} |
|||
this->actionsToModuleIndexMap[action].insert(moduleIndex); |
|||
this->actions.insert(action); |
|||
} |
|||
|
|||
// Put in the appropriate entries for the mapping from variable names to module index.
|
|||
for (uint_fast64_t booleanVariableIndex = 0; booleanVariableIndex < module.getNumberOfBooleanVariables(); ++booleanVariableIndex) { |
|||
this->variableToModuleIndexMap[module.getBooleanVariable(booleanVariableIndex).getName()] = moduleIndex; |
|||
} |
|||
for (uint_fast64_t integerVariableIndex = 0; integerVariableIndex < module.getNumberOfIntegerVariables(); ++integerVariableIndex) { |
|||
this->variableToModuleIndexMap[module.getIntegerVariable(integerVariableIndex).getName()] = moduleIndex; |
|||
} |
|||
} |
|||
} |
|||
|
|||
Program::Program(Program const& otherProgram) : modelType(otherProgram.modelType), globalBooleanVariables(otherProgram.globalBooleanVariables), |
|||
globalIntegerVariables(otherProgram.globalIntegerVariables), globalBooleanVariableToIndexMap(otherProgram.globalBooleanVariableToIndexMap), |
|||
globalIntegerVariableToIndexMap(otherProgram.globalIntegerVariableToIndexMap), modules(otherProgram.modules), rewards(otherProgram.rewards), |
|||
actions(otherProgram.actions), actionsToModuleIndexMap(), variableToModuleIndexMap() { |
|||
// Perform deep-copy of the maps.
|
|||
for (auto const& booleanUndefinedConstant : otherProgram.booleanUndefinedConstantExpressions) { |
|||
this->booleanUndefinedConstantExpressions[booleanUndefinedConstant.first] = std::unique_ptr<storm::ir::expressions::BooleanConstantExpression>(new storm::ir::expressions::BooleanConstantExpression(*booleanUndefinedConstant.second)); |
|||
} |
|||
for (auto const& integerUndefinedConstant : otherProgram.integerUndefinedConstantExpressions) { |
|||
this->integerUndefinedConstantExpressions[integerUndefinedConstant.first] = std::unique_ptr<storm::ir::expressions::IntegerConstantExpression>(new storm::ir::expressions::IntegerConstantExpression(*integerUndefinedConstant.second)); |
|||
} |
|||
for (auto const& doubleUndefinedConstant : otherProgram.doubleUndefinedConstantExpressions) { |
|||
this->doubleUndefinedConstantExpressions[doubleUndefinedConstant.first] = std::unique_ptr<storm::ir::expressions::DoubleConstantExpression>(new storm::ir::expressions::DoubleConstantExpression(*doubleUndefinedConstant.second)); |
|||
} |
|||
for (auto const& label : otherProgram.labels) { |
|||
this->labels[label.first] = label.second->clone(); |
|||
} |
|||
} |
|||
|
|||
Program& Program::operator=(Program const& otherProgram) { |
|||
if (this != &otherProgram) { |
|||
this->modelType = otherProgram.modelType; |
|||
this->globalBooleanVariables = otherProgram.globalBooleanVariables; |
|||
this->globalIntegerVariables = otherProgram.globalIntegerVariables; |
|||
this->globalBooleanVariableToIndexMap = otherProgram.globalBooleanVariableToIndexMap; |
|||
this->globalIntegerVariableToIndexMap = otherProgram.globalIntegerVariableToIndexMap; |
|||
this->modules = otherProgram.modules; |
|||
this->rewards = otherProgram.rewards; |
|||
this->actions = otherProgram.actions; |
|||
this->actionsToModuleIndexMap = otherProgram.actionsToModuleIndexMap; |
|||
this->variableToModuleIndexMap = otherProgram.variableToModuleIndexMap; |
|||
|
|||
// Perform deep-copy of the maps.
|
|||
for (auto const& booleanUndefinedConstant : otherProgram.booleanUndefinedConstantExpressions) { |
|||
this->booleanUndefinedConstantExpressions[booleanUndefinedConstant.first] = std::unique_ptr<storm::ir::expressions::BooleanConstantExpression>(new storm::ir::expressions::BooleanConstantExpression(*booleanUndefinedConstant.second)); |
|||
} |
|||
for (auto const& integerUndefinedConstant : otherProgram.integerUndefinedConstantExpressions) { |
|||
this->integerUndefinedConstantExpressions[integerUndefinedConstant.first] = std::unique_ptr<storm::ir::expressions::IntegerConstantExpression>(new storm::ir::expressions::IntegerConstantExpression(*integerUndefinedConstant.second)); |
|||
} |
|||
for (auto const& doubleUndefinedConstant : otherProgram.doubleUndefinedConstantExpressions) { |
|||
this->doubleUndefinedConstantExpressions[doubleUndefinedConstant.first] = std::unique_ptr<storm::ir::expressions::DoubleConstantExpression>(new storm::ir::expressions::DoubleConstantExpression(*doubleUndefinedConstant.second)); |
|||
} |
|||
for (auto const& label : otherProgram.labels) { |
|||
this->labels[label.first] = label.second->clone(); |
|||
} |
|||
} |
|||
|
|||
return *this; |
|||
} |
|||
|
|||
Program::ModelType Program::getModelType() const { |
|||
return modelType; |
|||
} |
|||
|
|||
std::string Program::toString() const { |
|||
std::stringstream result; |
|||
switch (modelType) { |
|||
case UNDEFINED: result << "undefined"; break; |
|||
case DTMC: result << "dtmc"; break; |
|||
case CTMC: result << "ctmc"; break; |
|||
case MDP: result << "mdp"; break; |
|||
case CTMDP: result << "ctmdp"; break; |
|||
} |
|||
result << std::endl; |
|||
|
|||
for (auto const& element : booleanUndefinedConstantExpressions) { |
|||
result << "const bool " << element.second->toString() << ";" << std::endl; |
|||
} |
|||
for (auto const& element : integerUndefinedConstantExpressions) { |
|||
result << "const int " << element.second->toString() << ";" << std::endl; |
|||
} |
|||
for (auto const& element : doubleUndefinedConstantExpressions) { |
|||
result << "const double " << element.second->toString() << ";" << std::endl; |
|||
} |
|||
result << std::endl; |
|||
|
|||
for (auto const& element : globalBooleanVariables) { |
|||
result << "global " << element.toString() << std::endl; |
|||
} |
|||
for (auto const& element : globalIntegerVariables) { |
|||
result << "global " << element.toString() << std::endl; |
|||
} |
|||
result << std::endl; |
|||
|
|||
for (auto const& module : modules) { |
|||
result << module.toString() << std::endl; |
|||
} |
|||
|
|||
for (auto const& rewardModel : rewards) { |
|||
result << rewardModel.second.toString() << std::endl; |
|||
} |
|||
|
|||
for (auto const& label : labels) { |
|||
result << "label \"" << label.first << "\" = " << label.second->toString() <<";" << std::endl; |
|||
} |
|||
|
|||
return result.str(); |
|||
} |
|||
|
|||
storm::ir::BooleanVariable const& Program::getGlobalBooleanVariable(uint_fast64_t index) const { |
|||
return this->globalBooleanVariables[index]; |
|||
} |
|||
|
|||
storm::ir::IntegerVariable const& Program::getGlobalIntegerVariable(uint_fast64_t index) const { |
|||
return this->globalIntegerVariables[index]; |
|||
} |
|||
|
|||
uint_fast64_t Program::getNumberOfModules() const { |
|||
return this->modules.size(); |
|||
} |
|||
|
|||
storm::ir::Module const& Program::getModule(uint_fast64_t index) const { |
|||
return this->modules[index]; |
|||
} |
|||
|
|||
std::set<std::string> const& Program::getActions() const { |
|||
return this->actions; |
|||
} |
|||
|
|||
std::set<uint_fast64_t> const& Program::getModulesByAction(std::string const& action) const { |
|||
auto actionModuleSetPair = this->actionsToModuleIndexMap.find(action); |
|||
if (actionModuleSetPair == this->actionsToModuleIndexMap.end()) { |
|||
LOG4CPLUS_ERROR(logger, "Action name '" << action << "' does not exist."); |
|||
throw storm::exceptions::OutOfRangeException() << "Action name '" << action << "' does not exist."; |
|||
} |
|||
return actionModuleSetPair->second; |
|||
} |
|||
|
|||
uint_fast64_t Program::getModuleIndexForVariable(std::string const& variableName) const { |
|||
auto variableNameToModuleIndexPair = this->variableToModuleIndexMap.find(variableName); |
|||
if (variableNameToModuleIndexPair != this->variableToModuleIndexMap.end()) { |
|||
return variableNameToModuleIndexPair->second; |
|||
} |
|||
throw storm::exceptions::OutOfRangeException() << "Variable '" << variableName << "' does not exist."; |
|||
} |
|||
|
|||
uint_fast64_t Program::getNumberOfGlobalBooleanVariables() const { |
|||
return this->globalBooleanVariables.size(); |
|||
} |
|||
|
|||
uint_fast64_t Program::getNumberOfGlobalIntegerVariables() const { |
|||
return this->globalIntegerVariables.size(); |
|||
} |
|||
|
|||
storm::ir::RewardModel const& Program::getRewardModel(std::string const& name) const { |
|||
auto nameRewardModelPair = this->rewards.find(name); |
|||
if (nameRewardModelPair == this->rewards.end()) { |
|||
LOG4CPLUS_ERROR(logger, "Reward model '" << name << "' does not exist."); |
|||
throw storm::exceptions::OutOfRangeException() << "Reward model '" << name << "' does not exist."; |
|||
} |
|||
return nameRewardModelPair->second; |
|||
} |
|||
|
|||
std::map<std::string, std::unique_ptr<storm::ir::expressions::BaseExpression>> const& Program::getLabels() const { |
|||
return this->labels; |
|||
} |
|||
|
|||
bool Program::hasUndefinedBooleanConstant(std::string const& constantName) const { |
|||
return this->booleanUndefinedConstantExpressions.find(constantName) != this->booleanUndefinedConstantExpressions.end(); |
|||
} |
|||
|
|||
std::unique_ptr<storm::ir::expressions::BooleanConstantExpression> const& Program::getUndefinedBooleanConstantExpression(std::string const& constantName) const { |
|||
auto constantExpressionPair = this->booleanUndefinedConstantExpressions.find(constantName); |
|||
if (constantExpressionPair != this->booleanUndefinedConstantExpressions.end()) { |
|||
return constantExpressionPair->second; |
|||
} else { |
|||
throw storm::exceptions::InvalidArgumentException() << "Unknown undefined boolean constant " << constantName << "."; |
|||
} |
|||
} |
|||
|
|||
bool Program::hasUndefinedIntegerConstant(std::string const& constantName) const { |
|||
return this->integerUndefinedConstantExpressions.find(constantName) != this->integerUndefinedConstantExpressions.end(); |
|||
} |
|||
|
|||
std::unique_ptr<storm::ir::expressions::IntegerConstantExpression> const& Program::getUndefinedIntegerConstantExpression(std::string const& constantName) const { |
|||
auto constantExpressionPair = this->integerUndefinedConstantExpressions.find(constantName); |
|||
if (constantExpressionPair != this->integerUndefinedConstantExpressions.end()) { |
|||
return constantExpressionPair->second; |
|||
} else { |
|||
throw storm::exceptions::InvalidArgumentException() << "Unknown undefined integer constant " << constantName << "."; |
|||
} |
|||
} |
|||
|
|||
bool Program::hasUndefinedDoubleConstant(std::string const& constantName) const { |
|||
return this->doubleUndefinedConstantExpressions.find(constantName) != this->doubleUndefinedConstantExpressions.end(); |
|||
} |
|||
|
|||
std::unique_ptr<storm::ir::expressions::DoubleConstantExpression> const& Program::getUndefinedDoubleConstantExpression(std::string const& constantName) const { |
|||
auto constantExpressionPair = this->doubleUndefinedConstantExpressions.find(constantName); |
|||
if (constantExpressionPair != this->doubleUndefinedConstantExpressions.end()) { |
|||
return constantExpressionPair->second; |
|||
} else { |
|||
throw storm::exceptions::InvalidArgumentException() << "Unknown undefined double constant " << constantName << "."; |
|||
} |
|||
} |
|||
|
|||
std::map<std::string, std::unique_ptr<storm::ir::expressions::BooleanConstantExpression>> const& Program::getBooleanUndefinedConstantExpressionsMap() const { |
|||
return this->booleanUndefinedConstantExpressions; |
|||
} |
|||
|
|||
std::map<std::string, std::unique_ptr<storm::ir::expressions::IntegerConstantExpression>> const& Program::getIntegerUndefinedConstantExpressionsMap() const { |
|||
return this->integerUndefinedConstantExpressions; |
|||
} |
|||
|
|||
std::map<std::string, std::unique_ptr<storm::ir::expressions::DoubleConstantExpression>> const& Program::getDoubleUndefinedConstantExpressionsMap() const { |
|||
return this->doubleUndefinedConstantExpressions; |
|||
} |
|||
|
|||
uint_fast64_t Program::getGlobalIndexOfBooleanVariable(std::string const& variableName) const { |
|||
return this->globalBooleanVariableToIndexMap.at(variableName); |
|||
} |
|||
|
|||
uint_fast64_t Program::getGlobalIndexOfIntegerVariable(std::string const& variableName) const { |
|||
return this->globalIntegerVariableToIndexMap.at(variableName); |
|||
} |
|||
|
|||
void Program::restrictCommands(boost::container::flat_set<uint_fast64_t> const& indexSet) { |
|||
for (auto& module : modules) { |
|||
module.restrictCommands(indexSet); |
|||
} |
|||
} |
|||
|
|||
} // namespace ir
|
|||
} // namepsace storm
|
|||
@ -1,318 +0,0 @@ |
|||
/* |
|||
* Program.h |
|||
* |
|||
* Created on: 04.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_PROGRAM_H_ |
|||
#define STORM_IR_PROGRAM_H_ |
|||
|
|||
#include <map> |
|||
#include <vector> |
|||
#include <memory> |
|||
#include <set> |
|||
#include <boost/container/flat_set.hpp> |
|||
|
|||
#include "expressions/BaseExpression.h" |
|||
#include "expressions/BooleanConstantExpression.h" |
|||
#include "expressions/IntegerConstantExpression.h" |
|||
#include "expressions/DoubleConstantExpression.h" |
|||
#include "Module.h" |
|||
#include "RewardModel.h" |
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
|
|||
/*! |
|||
* A class representing a program. |
|||
*/ |
|||
class Program { |
|||
public: |
|||
|
|||
/*! |
|||
* An enum for the different model types. |
|||
*/ |
|||
enum ModelType {UNDEFINED, DTMC, CTMC, MDP, CTMDP}; |
|||
|
|||
/*! |
|||
* Default constructor. Creates an empty program. |
|||
*/ |
|||
Program(); |
|||
|
|||
/*! |
|||
* Creates a program with the given model type, undefined constants, modules, rewards and labels. |
|||
* |
|||
* @param modelType The type of the model that this program gives rise to. |
|||
* @param booleanUndefinedConstantExpressions A map of undefined boolean constants to their |
|||
* expression nodes. |
|||
* @param integerUndefinedConstantExpressions A map of undefined integer constants to their |
|||
* expression nodes. |
|||
* @param doubleUndefinedConstantExpressions A map of undefined double constants to their |
|||
* expression nodes. |
|||
* @param globalBooleanVariables A list of global boolean variables. |
|||
* @param globalIntegerVariables A list of global integer variables. |
|||
* @param globalBooleanVariableToIndexMap A mapping from global boolean variable names to the index in the |
|||
* list of global boolean variables. |
|||
* @param globalIntegerVariableToIndexMap A mapping from global integer variable names to the index in the |
|||
* list of global integer variables. |
|||
* @param modules The modules of the program. |
|||
* @param rewards The reward models of the program. |
|||
* @param labels The labels defined for this model. |
|||
*/ |
|||
Program(ModelType modelType, |
|||
std::map<std::string, std::unique_ptr<storm::ir::expressions::BooleanConstantExpression>> const& booleanUndefinedConstantExpressions, |
|||
std::map<std::string, std::unique_ptr<storm::ir::expressions::IntegerConstantExpression>> const& integerUndefinedConstantExpressions, |
|||
std::map<std::string, std::unique_ptr<storm::ir::expressions::DoubleConstantExpression>> const& doubleUndefinedConstantExpressions, |
|||
std::vector<BooleanVariable> const& globalBooleanVariables, |
|||
std::vector<IntegerVariable> const& globalIntegerVariables, |
|||
std::map<std::string, uint_fast64_t> const& globalBooleanVariableToIndexMap, |
|||
std::map<std::string, uint_fast64_t> const& globalIntegerVariableToIndexMap, |
|||
std::vector<storm::ir::Module> const& modules, |
|||
std::map<std::string, storm::ir::RewardModel> const& rewards, |
|||
std::map<std::string, std::unique_ptr<storm::ir::expressions::BaseExpression>> const& labels); |
|||
|
|||
/*! |
|||
* Performs a deep-copy of the given program. |
|||
* |
|||
* @param otherProgram The program to copy. |
|||
*/ |
|||
Program(Program const& otherProgram); |
|||
|
|||
/*! |
|||
* Performs a deep-copy of the given program and assigns it to the current one. |
|||
* |
|||
* @param otherProgram The program to assign. |
|||
*/ |
|||
Program& operator=(Program const& otherProgram); |
|||
|
|||
/*! |
|||
* Retrieves the number of modules in the program. |
|||
* |
|||
* @return The number of modules in the program. |
|||
*/ |
|||
uint_fast64_t getNumberOfModules() const; |
|||
|
|||
/*! |
|||
* Retrieves a reference to the module with the given index. |
|||
* |
|||
* @param index The index of the module to retrieve. |
|||
* @return The module with the given index. |
|||
*/ |
|||
storm::ir::Module const& getModule(uint_fast64_t index) const; |
|||
|
|||
/*! |
|||
* Retrieves the model type of the model. |
|||
* |
|||
* @return The type of the model. |
|||
*/ |
|||
ModelType getModelType() const; |
|||
|
|||
/*! |
|||
* Retrieves a string representation of this program. |
|||
* |
|||
* @return A string representation of this program. |
|||
*/ |
|||
std::string toString() const; |
|||
|
|||
/*! |
|||
* Retrieves a reference to the global boolean variable with the given index. |
|||
* |
|||
* @return A reference to the global boolean variable with the given index. |
|||
*/ |
|||
storm::ir::BooleanVariable const& getGlobalBooleanVariable(uint_fast64_t index) const; |
|||
|
|||
/*! |
|||
* Retrieves a reference to the global integer variable with the given index. |
|||
* |
|||
* @return A reference to the global integer variable with the given index. |
|||
*/ |
|||
storm::ir::IntegerVariable const& getGlobalIntegerVariable(uint_fast64_t index) const; |
|||
|
|||
/*! |
|||
* Retrieves the set of actions present in this module. |
|||
* |
|||
* @return The set of actions present in this module. |
|||
*/ |
|||
std::set<std::string> const& getActions() const; |
|||
|
|||
/*! |
|||
* Retrieves the indices of all modules within this program that contain commands that are labelled with the given |
|||
* action. |
|||
* |
|||
* @param action The name of the action the modules are supposed to possess. |
|||
* @return A set of indices of all matching modules. |
|||
*/ |
|||
std::set<uint_fast64_t> const& getModulesByAction(std::string const& action) const; |
|||
|
|||
/*! |
|||
* Retrieves the index of the module in which the given variable name was declared. |
|||
* |
|||
* @param variableName The name of the variable to search. |
|||
* @return The index of the module in which the given variable name was declared. |
|||
*/ |
|||
uint_fast64_t getModuleIndexForVariable(std::string const& variableName) const; |
|||
|
|||
/*! |
|||
* Retrieves the number of global boolean variables of the program. |
|||
* |
|||
* @return The number of global boolean variables of the program. |
|||
*/ |
|||
uint_fast64_t getNumberOfGlobalBooleanVariables() const; |
|||
|
|||
/*! |
|||
* Retrieves the number of global integer variables of the program. |
|||
* |
|||
* @return The number of global integer variables of the program. |
|||
*/ |
|||
uint_fast64_t getNumberOfGlobalIntegerVariables() const; |
|||
|
|||
/*! |
|||
* Retrieves the reward model with the given name. |
|||
* |
|||
* @param name The name of the reward model to return. |
|||
* @return The reward model with the given name. |
|||
*/ |
|||
storm::ir::RewardModel const& getRewardModel(std::string const& name) const; |
|||
|
|||
/*! |
|||
* Retrieves all labels that are defined by the probabilitic program. |
|||
* |
|||
* @return A set of labels that are defined in the program. |
|||
*/ |
|||
std::map<std::string, std::unique_ptr<storm::ir::expressions::BaseExpression>> const& getLabels() const; |
|||
|
|||
/*! |
|||
* Retrieves whether the given constant name is an undefined boolean constant of the program. |
|||
* |
|||
* @return True if the given constant name is an undefined boolean constant of the program. |
|||
*/ |
|||
bool hasUndefinedBooleanConstant(std::string const& constantName) const; |
|||
|
|||
/*! |
|||
* Retrieves the expression associated with the given undefined boolean constant. |
|||
* |
|||
* @param constantName The name of the undefined boolean constant for which to retrieve the expression. |
|||
* @return The expression associated with the given undefined boolean constant. |
|||
*/ |
|||
std::unique_ptr<storm::ir::expressions::BooleanConstantExpression> const& getUndefinedBooleanConstantExpression(std::string const& constantName) const; |
|||
|
|||
/*! |
|||
* Retrieves whether the given constant name is an undefined integer constant of the program. |
|||
* |
|||
* @return True if the given constant name is an undefined integer constant of the program. |
|||
*/ |
|||
bool hasUndefinedIntegerConstant(std::string const& constantName) const; |
|||
|
|||
/*! |
|||
* Retrieves the expression associated with the given undefined integer constant. |
|||
* |
|||
* @param constantName The name of the undefined integer constant for which to retrieve the expression. |
|||
* @return The expression associated with the given undefined integer constant. |
|||
*/ |
|||
std::unique_ptr<storm::ir::expressions::IntegerConstantExpression> const& getUndefinedIntegerConstantExpression(std::string const& constantName) const; |
|||
|
|||
/*! |
|||
* Retrieves whether the given constant name is an undefined double constant of the program. |
|||
* |
|||
* @return True if the given constant name is an undefined double constant of the program. |
|||
*/ |
|||
bool hasUndefinedDoubleConstant(std::string const& constantName) const; |
|||
|
|||
/*! |
|||
* Retrieves the expression associated with the given undefined double constant. |
|||
* |
|||
* @param constantName The name of the undefined double constant for which to retrieve the expression. |
|||
* @return The expression associated with the given undefined double constant. |
|||
*/ |
|||
std::unique_ptr<storm::ir::expressions::DoubleConstantExpression> const& getUndefinedDoubleConstantExpression(std::string const& constantName) const; |
|||
|
|||
/*! |
|||
* Retrieves the mapping of undefined boolean constant names to their expression objects. |
|||
* |
|||
* @return The mapping of undefined boolean constant names to their expression objects. |
|||
*/ |
|||
std::map<std::string, std::unique_ptr<storm::ir::expressions::BooleanConstantExpression>> const& getBooleanUndefinedConstantExpressionsMap() const; |
|||
|
|||
/*! |
|||
* Retrieves the mapping of undefined integer constant names to their expression objects. |
|||
* |
|||
* @return The mapping of undefined integer constant names to their expression objects. |
|||
*/ |
|||
std::map<std::string, std::unique_ptr<storm::ir::expressions::IntegerConstantExpression>> const& getIntegerUndefinedConstantExpressionsMap() const; |
|||
|
|||
/*! |
|||
* Retrieves the mapping of undefined double constant names to their expression objects. |
|||
* |
|||
* @return The mapping of undefined double constant names to their expression objects. |
|||
*/ |
|||
std::map<std::string, std::unique_ptr<storm::ir::expressions::DoubleConstantExpression>> const& getDoubleUndefinedConstantExpressionsMap() const; |
|||
|
|||
/*! |
|||
* Retrieves the global index of the given boolean variable. |
|||
* |
|||
* @param variableName The name of the boolean variable whose index to retrieve. |
|||
*/ |
|||
uint_fast64_t getGlobalIndexOfBooleanVariable(std::string const& variableName) const; |
|||
|
|||
/*! |
|||
* Retrieves the global index of the integer boolean variable. |
|||
* |
|||
* @param variableName The name of the integer variable whose index to retrieve. |
|||
*/ |
|||
uint_fast64_t getGlobalIndexOfIntegerVariable(std::string const& variableName) const; |
|||
|
|||
/*! |
|||
* Deletes all commands with indices not in the given set from the program. |
|||
* |
|||
* @param indexSet The set of indices for which to keep the commands. |
|||
*/ |
|||
void restrictCommands(boost::container::flat_set<uint_fast64_t> const& indexSet); |
|||
private: |
|||
// The type of the model. |
|||
ModelType modelType; |
|||
|
|||
// A map of undefined boolean constants to their expression nodes. |
|||
std::map<std::string, std::unique_ptr<storm::ir::expressions::BooleanConstantExpression>> booleanUndefinedConstantExpressions; |
|||
|
|||
// A map of undefined integer constants to their expressions nodes. |
|||
std::map<std::string, std::unique_ptr<storm::ir::expressions::IntegerConstantExpression>> integerUndefinedConstantExpressions; |
|||
|
|||
// A map of undefined double constants to their expressions nodes. |
|||
std::map<std::string, std::unique_ptr<storm::ir::expressions::DoubleConstantExpression>> doubleUndefinedConstantExpressions; |
|||
|
|||
// A list of global boolean variables. |
|||
std::vector<BooleanVariable> globalBooleanVariables; |
|||
|
|||
// A list of global integer variables. |
|||
std::vector<IntegerVariable> globalIntegerVariables; |
|||
|
|||
// A mapping from global boolean variable names to their indices. |
|||
std::map<std::string, uint_fast64_t> globalBooleanVariableToIndexMap; |
|||
|
|||
// A mapping from global integer variable names to their indices. |
|||
std::map<std::string, uint_fast64_t> globalIntegerVariableToIndexMap; |
|||
|
|||
// The modules associated with the program. |
|||
std::vector<storm::ir::Module> modules; |
|||
|
|||
// The reward models associated with the program. |
|||
std::map<std::string, storm::ir::RewardModel> rewards; |
|||
|
|||
// The labels that are defined for this model. |
|||
std::map<std::string, std::unique_ptr<storm::ir::expressions::BaseExpression>> labels; |
|||
|
|||
// The set of actions present in this program. |
|||
std::set<std::string> actions; |
|||
|
|||
// A map of actions to the set of modules containing commands labelled with this action. |
|||
std::map<std::string, std::set<uint_fast64_t>> actionsToModuleIndexMap; |
|||
|
|||
// A mapping from variable names to the modules in which they were declared. |
|||
std::map<std::string, uint_fast64_t> variableToModuleIndexMap; |
|||
}; |
|||
|
|||
} // namespace ir |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_PROGRAM_H_ */ |
|||
@ -1,53 +0,0 @@ |
|||
/*
|
|||
* RewardModel.cpp |
|||
* |
|||
* Created on: 12.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include <sstream>
|
|||
|
|||
#include "RewardModel.h"
|
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
|
|||
RewardModel::RewardModel() : rewardModelName(), stateRewards(), transitionRewards() { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
RewardModel::RewardModel(std::string const& rewardModelName, std::vector<storm::ir::StateReward> const& stateRewards, std::vector<storm::ir::TransitionReward> const& transitionRewards) : rewardModelName(rewardModelName), stateRewards(stateRewards), transitionRewards(transitionRewards) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
std::string RewardModel::toString() const { |
|||
std::stringstream result; |
|||
result << "rewards \"" << rewardModelName << "\"" << std::endl; |
|||
for (auto const& reward : stateRewards) { |
|||
result << reward.toString() << std::endl; |
|||
} |
|||
for (auto const& reward : transitionRewards) { |
|||
result << reward.toString() << std::endl; |
|||
} |
|||
result << "endrewards" << std::endl; |
|||
return result.str(); |
|||
} |
|||
|
|||
bool RewardModel::hasStateRewards() const { |
|||
return this->stateRewards.size() > 0; |
|||
} |
|||
|
|||
std::vector<storm::ir::StateReward> const& RewardModel::getStateRewards() const { |
|||
return this->stateRewards; |
|||
} |
|||
|
|||
bool RewardModel::hasTransitionRewards() const { |
|||
return this->transitionRewards.size() > 0; |
|||
} |
|||
|
|||
std::vector<storm::ir::TransitionReward> const& RewardModel::getTransitionRewards() const { |
|||
return this->transitionRewards; |
|||
} |
|||
|
|||
} // namespace ir
|
|||
} // namespace storm
|
|||
@ -1,88 +0,0 @@ |
|||
/* |
|||
* RewardModel.h |
|||
* |
|||
* Created on: 04.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_REWARDMODEL_H_ |
|||
#define STORM_IR_REWARDMODEL_H_ |
|||
|
|||
#include <string> |
|||
#include <vector> |
|||
|
|||
#include "StateReward.h" |
|||
#include "TransitionReward.h" |
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
|
|||
/*! |
|||
* A class representing a reward model. |
|||
*/ |
|||
class RewardModel { |
|||
public: |
|||
/*! |
|||
* Default constructor. Creates an empty reward model. |
|||
*/ |
|||
RewardModel(); |
|||
|
|||
/*! |
|||
* Creates a reward module with the given name, state and transition rewards. |
|||
* |
|||
* @param rewardModelName The name of the reward model. |
|||
* @param stateRewards A vector of state-based rewards. |
|||
* @param transitionRewards A vector of transition-based rewards. |
|||
*/ |
|||
RewardModel(std::string const& rewardModelName, std::vector<storm::ir::StateReward> const& stateRewards, std::vector<storm::ir::TransitionReward> const& transitionRewards); |
|||
|
|||
/*! |
|||
* Retrieves a string representation of this reward model. |
|||
* |
|||
* @return a string representation of this reward model. |
|||
*/ |
|||
std::string toString() const; |
|||
|
|||
/*! |
|||
* Check, if there are any state rewards. |
|||
* |
|||
* @return True, iff there are any state rewards. |
|||
*/ |
|||
bool hasStateRewards() const; |
|||
|
|||
/*! |
|||
* Retrieves a vector of state rewards associated with this reward model. |
|||
* |
|||
* @return A vector containing the state rewards associated with this reward model. |
|||
*/ |
|||
std::vector<storm::ir::StateReward> const& getStateRewards() const; |
|||
|
|||
/*! |
|||
* Check, if there are any transition rewards. |
|||
* |
|||
* @return True, iff there are any transition rewards associated with this reward model. |
|||
*/ |
|||
bool hasTransitionRewards() const; |
|||
|
|||
/*! |
|||
* Retrieves a vector of transition rewards associated with this reward model. |
|||
* |
|||
* @return A vector of transition rewards associated with this reward model. |
|||
*/ |
|||
std::vector<storm::ir::TransitionReward> const& getTransitionRewards() const; |
|||
|
|||
private: |
|||
// The name of the reward model. |
|||
std::string rewardModelName; |
|||
|
|||
// The state-based rewards associated with this reward model. |
|||
std::vector<storm::ir::StateReward> stateRewards; |
|||
|
|||
// The transition-based rewards associated with this reward model. |
|||
std::vector<storm::ir::TransitionReward> transitionRewards; |
|||
}; |
|||
|
|||
} // namespace ir |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_REWARDMODEL_H_ */ |
|||
@ -1,60 +0,0 @@ |
|||
/*
|
|||
* StateReward.cpp |
|||
* |
|||
* Created on: 12.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include <sstream>
|
|||
|
|||
#include "StateReward.h"
|
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
|
|||
StateReward::StateReward() : statePredicate(), rewardValue() { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
StateReward::StateReward(std::unique_ptr<storm::ir::expressions::BaseExpression>&& statePredicate, std::unique_ptr<storm::ir::expressions::BaseExpression>&& rewardValue) : statePredicate(std::move(statePredicate)), rewardValue(std::move(rewardValue)) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
StateReward::StateReward(StateReward const& otherReward) { |
|||
if (otherReward.statePredicate != nullptr) { |
|||
statePredicate = otherReward.statePredicate->clone(); |
|||
} |
|||
if (otherReward.rewardValue != nullptr) { |
|||
rewardValue = otherReward.rewardValue->clone(); |
|||
} |
|||
} |
|||
|
|||
StateReward& StateReward::operator=(StateReward const& otherReward) { |
|||
if (this != & otherReward) { |
|||
if (otherReward.statePredicate != nullptr) { |
|||
this->statePredicate = otherReward.statePredicate->clone(); |
|||
} |
|||
if (otherReward.rewardValue != nullptr) { |
|||
this->rewardValue = otherReward.rewardValue->clone(); |
|||
} |
|||
} |
|||
|
|||
return *this; |
|||
} |
|||
|
|||
std::string StateReward::toString() const { |
|||
std::stringstream result; |
|||
result << "\t" << statePredicate->toString() << ": " << rewardValue->toString() << ";"; |
|||
return result.str(); |
|||
} |
|||
|
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> const& StateReward::getStatePredicate() const { |
|||
return this->statePredicate; |
|||
} |
|||
|
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> const& StateReward::getRewardValue() const { |
|||
return this->rewardValue; |
|||
} |
|||
|
|||
} // namespace ir
|
|||
} // namespace storm
|
|||
@ -1,85 +0,0 @@ |
|||
/* |
|||
* StateReward.h |
|||
* |
|||
* Created on: Jan 10, 2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_STATEREWARD_H_ |
|||
#define STORM_IR_STATEREWARD_H_ |
|||
|
|||
#include <memory> |
|||
|
|||
#include "expressions/BaseExpression.h" |
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
|
|||
/*! |
|||
* A class representing a state reward. |
|||
*/ |
|||
class StateReward { |
|||
public: |
|||
/*! |
|||
* Default constructor. Creates an empty state reward. |
|||
*/ |
|||
StateReward(); |
|||
|
|||
/*! |
|||
* Creates a state reward for the states satisfying the given expression with the value given |
|||
* by a second expression. |
|||
* |
|||
* @param statePredicate The predicate that states earning this state-based reward need to |
|||
* satisfy. |
|||
* @param rewardValue An expression specifying the values of the rewards to attach to the |
|||
* states. |
|||
*/ |
|||
StateReward(std::unique_ptr<storm::ir::expressions::BaseExpression>&& statePredicate, std::unique_ptr<storm::ir::expressions::BaseExpression>&& rewardValue); |
|||
|
|||
/*! |
|||
* Performs a deep-copy of the given reward. |
|||
* |
|||
* @param otherReward The reward to copy. |
|||
*/ |
|||
StateReward(StateReward const& otherReward); |
|||
|
|||
/*! |
|||
* Performs a deep-copy of the given reward and assigns it to the current one. |
|||
* |
|||
* @param otherReward The reward to assign. |
|||
*/ |
|||
StateReward& operator=(StateReward const& otherReward); |
|||
|
|||
/*! |
|||
* Retrieves a string representation of this state reward. |
|||
* |
|||
* @return A string representation of this state reward. |
|||
*/ |
|||
std::string toString() const; |
|||
|
|||
/*! |
|||
* Retrieves the state predicate that is associated with this state reward. |
|||
* |
|||
* @return The state predicate that is associated with this state reward. |
|||
*/ |
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> const& getStatePredicate() const; |
|||
|
|||
/*! |
|||
* Retrieves the reward value associated with this state reward. |
|||
* |
|||
* @return The reward value associated with this state reward. |
|||
*/ |
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> const& getRewardValue() const; |
|||
|
|||
private: |
|||
// The predicate that characterizes the states that obtain this reward. |
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> statePredicate; |
|||
|
|||
// The expression that specifies the value of the reward obtained. |
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> rewardValue; |
|||
}; |
|||
|
|||
} // namespace ir |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_STATEREWARD_H_ */ |
|||
@ -1,65 +0,0 @@ |
|||
/*
|
|||
* TransitionReward.cpp |
|||
* |
|||
* Created on: 12.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include <sstream>
|
|||
|
|||
#include "TransitionReward.h"
|
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
|
|||
TransitionReward::TransitionReward() : commandName(), statePredicate(), rewardValue() { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
TransitionReward::TransitionReward(std::string const& commandName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& statePredicate, std::unique_ptr<storm::ir::expressions::BaseExpression>&& rewardValue) : commandName(commandName), statePredicate(std::move(statePredicate)), rewardValue(std::move(rewardValue)) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
TransitionReward::TransitionReward(TransitionReward const& otherReward) : commandName(otherReward.commandName), statePredicate(), rewardValue() { |
|||
if (otherReward.statePredicate != nullptr) { |
|||
statePredicate = otherReward.statePredicate->clone(); |
|||
} |
|||
if (otherReward.rewardValue != nullptr) { |
|||
rewardValue = otherReward.rewardValue->clone(); |
|||
} |
|||
} |
|||
|
|||
TransitionReward& TransitionReward::operator=(TransitionReward const& otherReward) { |
|||
if (this != &otherReward) { |
|||
this->commandName = otherReward.commandName; |
|||
if (otherReward.statePredicate != nullptr) { |
|||
this->statePredicate = otherReward.statePredicate->clone(); |
|||
} |
|||
if (otherReward.rewardValue != nullptr) { |
|||
this->rewardValue = otherReward.rewardValue->clone(); |
|||
} |
|||
} |
|||
|
|||
return *this; |
|||
} |
|||
|
|||
std::string TransitionReward::toString() const { |
|||
std::stringstream result; |
|||
result << "\t[" << commandName << "] " << statePredicate->toString() << ": " << rewardValue->toString() << ";"; |
|||
return result.str(); |
|||
} |
|||
|
|||
std::string const& TransitionReward::getActionName() const { |
|||
return this->commandName; |
|||
} |
|||
|
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> const& TransitionReward::getStatePredicate() const { |
|||
return this->statePredicate; |
|||
} |
|||
|
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> const& TransitionReward::getRewardValue() const { |
|||
return this->rewardValue; |
|||
} |
|||
|
|||
} // namespace ir
|
|||
} // namespace storm
|
|||
@ -1,99 +0,0 @@ |
|||
/* |
|||
* TransitionReward.h |
|||
* |
|||
* Created on: Jan 10, 2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_TRANSITIONREWARD_H_ |
|||
#define STORM_IR_TRANSITIONREWARD_H_ |
|||
|
|||
#include <memory> |
|||
|
|||
#include "expressions/BaseExpression.h" |
|||
|
|||
namespace storm { |
|||
|
|||
namespace ir { |
|||
|
|||
/*! |
|||
* A class representing a transition reward. |
|||
*/ |
|||
class TransitionReward { |
|||
public: |
|||
/*! |
|||
* Default constructor. Creates an empty transition reward. |
|||
*/ |
|||
TransitionReward(); |
|||
|
|||
/*! |
|||
* Creates a transition reward for the transitions with the given name emanating from states |
|||
* satisfying the given expression with the value given by another expression. |
|||
* |
|||
* @param commandName The name of the command that obtains this reward. |
|||
* @param statePredicate The predicate that needs to hold before taking a transition with the |
|||
* previously specified name in order to obtain the reward. |
|||
* @param rewardValue An expression specifying the values of the rewards to attach to the |
|||
* transitions. |
|||
*/ |
|||
TransitionReward(std::string const& commandName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& statePredicate, std::unique_ptr<storm::ir::expressions::BaseExpression>&& rewardValue); |
|||
|
|||
/*! |
|||
* Performs a deep-copy of the given transition reward. |
|||
* |
|||
* @param otherReward The transition reward to copy. |
|||
*/ |
|||
TransitionReward(TransitionReward const& otherReward); |
|||
|
|||
/*! |
|||
* Performs a deep-copy of the given transition reward and assigns it to the current one. |
|||
* |
|||
* @param otherReward The reward to assign. |
|||
*/ |
|||
TransitionReward& operator=(TransitionReward const& otherReward); |
|||
|
|||
/*! |
|||
* Retrieves a string representation of this transition reward. |
|||
* |
|||
* @return A string representation of this transition reward. |
|||
*/ |
|||
std::string toString() const; |
|||
|
|||
/*! |
|||
* Retrieves the action name that is associated with this transition reward. |
|||
* |
|||
* @return The action name that is associated with this transition reward. |
|||
*/ |
|||
std::string const& getActionName() const; |
|||
|
|||
/*! |
|||
* Retrieves the state predicate that is associated with this state reward. |
|||
* |
|||
* @return The state predicate that is associated with this state reward. |
|||
*/ |
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> const& getStatePredicate() const; |
|||
|
|||
/*! |
|||
* Retrieves the reward value associated with this state reward. |
|||
* |
|||
* @return The reward value associated with this state reward. |
|||
*/ |
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> const& getRewardValue() const; |
|||
|
|||
private: |
|||
// The name of the command this transition-based reward is attached to. |
|||
std::string commandName; |
|||
|
|||
// A predicate that needs to be satisfied by states for the reward to be obtained (by taking |
|||
// a corresponding command transition). |
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> statePredicate; |
|||
|
|||
// The expression specifying the value of the reward obtained along the transitions. |
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> rewardValue; |
|||
}; |
|||
|
|||
} // namespace ir |
|||
|
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_TRANSITIONREWARD_H_ */ |
|||
@ -1,130 +0,0 @@ |
|||
/*
|
|||
* Update.cpp |
|||
* |
|||
* Created on: 12.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include <sstream>
|
|||
|
|||
#include "Update.h"
|
|||
#include "src/parser/prismparser/VariableState.h"
|
|||
#include "src/exceptions/OutOfRangeException.h"
|
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
|
|||
Update::Update() : likelihoodExpression(), booleanAssignments(), integerAssignments(), globalIndex() { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
Update::Update(uint_fast64_t globalIndex, std::unique_ptr<storm::ir::expressions::BaseExpression>&& likelihoodExpression, std::map<std::string, storm::ir::Assignment> const& booleanAssignments, std::map<std::string, storm::ir::Assignment> const& integerAssignments) |
|||
: likelihoodExpression(std::move(likelihoodExpression)), booleanAssignments(booleanAssignments), integerAssignments(integerAssignments), globalIndex(globalIndex) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
Update::Update(Update const& update, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState& variableState) : globalIndex(newGlobalIndex) { |
|||
for (auto const& variableAssignmentPair : update.booleanAssignments) { |
|||
if (renaming.count(variableAssignmentPair.first) > 0) { |
|||
this->booleanAssignments[renaming.at(variableAssignmentPair.first)] = Assignment(variableAssignmentPair.second, renaming, variableState); |
|||
} else { |
|||
this->booleanAssignments[variableAssignmentPair.first] = Assignment(variableAssignmentPair.second, renaming, variableState); |
|||
} |
|||
} |
|||
for (auto const& variableAssignmentPair : update.integerAssignments) { |
|||
if (renaming.count(variableAssignmentPair.first) > 0) { |
|||
this->integerAssignments[renaming.at(variableAssignmentPair.first)] = Assignment(variableAssignmentPair.second, renaming, variableState); |
|||
} else { |
|||
this->integerAssignments[variableAssignmentPair.first] = Assignment(variableAssignmentPair.second, renaming, variableState); |
|||
} |
|||
} |
|||
this->likelihoodExpression = update.likelihoodExpression->clone(renaming, variableState); |
|||
} |
|||
|
|||
Update::Update(Update const& otherUpdate) : likelihoodExpression(), booleanAssignments(otherUpdate.booleanAssignments), integerAssignments(otherUpdate.integerAssignments), globalIndex(otherUpdate.globalIndex) { |
|||
if (otherUpdate.likelihoodExpression != nullptr) { |
|||
likelihoodExpression = otherUpdate.likelihoodExpression->clone(); |
|||
} |
|||
} |
|||
|
|||
Update& Update::operator=(Update const& otherUpdate) { |
|||
if (this != &otherUpdate) { |
|||
if (otherUpdate.likelihoodExpression != nullptr) { |
|||
this->likelihoodExpression = otherUpdate.likelihoodExpression->clone(); |
|||
} |
|||
this->booleanAssignments = otherUpdate.booleanAssignments; |
|||
this->integerAssignments = otherUpdate.integerAssignments; |
|||
this->globalIndex = otherUpdate.globalIndex; |
|||
} |
|||
|
|||
return *this; |
|||
} |
|||
|
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> const& Update::getLikelihoodExpression() const { |
|||
return likelihoodExpression; |
|||
} |
|||
|
|||
uint_fast64_t Update::getNumberOfBooleanAssignments() const { |
|||
return booleanAssignments.size(); |
|||
} |
|||
|
|||
uint_fast64_t Update::getNumberOfIntegerAssignments() const { |
|||
return integerAssignments.size(); |
|||
} |
|||
|
|||
std::map<std::string, storm::ir::Assignment> const& Update::getBooleanAssignments() const { |
|||
return booleanAssignments; |
|||
} |
|||
|
|||
std::map<std::string, storm::ir::Assignment> const& Update::getIntegerAssignments() const { |
|||
return integerAssignments; |
|||
} |
|||
|
|||
storm::ir::Assignment const& Update::getBooleanAssignment(std::string const& variableName) const { |
|||
auto variableAssignmentPair = booleanAssignments.find(variableName); |
|||
if (variableAssignmentPair == booleanAssignments.end()) { |
|||
throw storm::exceptions::OutOfRangeException() << "Cannot find boolean assignment for variable '" |
|||
<< variableName << "' in update " << this->toString() << "."; |
|||
} |
|||
|
|||
return variableAssignmentPair->second; |
|||
} |
|||
|
|||
storm::ir::Assignment const& Update::getIntegerAssignment(std::string const& variableName) const { |
|||
auto variableAssignmentPair = integerAssignments.find(variableName); |
|||
if (variableAssignmentPair == integerAssignments.end()) { |
|||
throw storm::exceptions::OutOfRangeException() << "Cannot find integer assignment for variable '" |
|||
<< variableName << "' in update " << this->toString() << "."; |
|||
} |
|||
|
|||
return variableAssignmentPair->second; |
|||
} |
|||
|
|||
uint_fast64_t Update::getGlobalIndex() const { |
|||
return this->globalIndex; |
|||
} |
|||
|
|||
std::string Update::toString() const { |
|||
std::stringstream result; |
|||
result << likelihoodExpression->toString() << " : "; |
|||
uint_fast64_t i = 0; |
|||
for (auto const& assignment : booleanAssignments) { |
|||
result << assignment.second.toString(); |
|||
if (i < booleanAssignments.size() - 1 || integerAssignments.size() > 0) { |
|||
result << " & "; |
|||
} |
|||
++i; |
|||
} |
|||
i = 0; |
|||
for (auto const& assignment : integerAssignments) { |
|||
result << assignment.second.toString(); |
|||
if (i < integerAssignments.size() - 1) { |
|||
result << " & "; |
|||
} |
|||
++i; |
|||
} |
|||
return result.str(); |
|||
} |
|||
|
|||
} // namespace ir
|
|||
} // namespace storm
|
|||
@ -1,152 +0,0 @@ |
|||
/* |
|||
* Update.h |
|||
* |
|||
* Created on: 06.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_UPDATE_H_ |
|||
#define STORM_IR_UPDATE_H_ |
|||
|
|||
#include <map> |
|||
#include <memory> |
|||
|
|||
#include "expressions/BaseExpression.h" |
|||
#include "Assignment.h" |
|||
|
|||
namespace storm { |
|||
|
|||
namespace parser { |
|||
namespace prism { |
|||
class VariableState; |
|||
} // namespace prismparser |
|||
} // namespace parser |
|||
|
|||
namespace ir { |
|||
|
|||
/*! |
|||
* A class representing an update of a command. |
|||
*/ |
|||
class Update { |
|||
public: |
|||
/*! |
|||
* Default constructor. Creates an empty update. |
|||
*/ |
|||
Update(); |
|||
|
|||
/*! |
|||
* Creates an update with the given expression specifying the likelihood and the mapping of |
|||
* variable to their assignments. |
|||
* |
|||
* @param globalIndex The global index of the update. |
|||
* @param likelihoodExpression An expression specifying the likelihood of this update. |
|||
* @param assignments A map of variable names to their assignments. |
|||
*/ |
|||
Update(uint_fast64_t globalIndex, std::unique_ptr<storm::ir::expressions::BaseExpression>&& likelihoodExpression, std::map<std::string, storm::ir::Assignment> const& booleanAssignments, std::map<std::string, storm::ir::Assignment> const& integerAssignments); |
|||
|
|||
/*! |
|||
* Creates a copy of the given update and performs the provided renaming. |
|||
* |
|||
* @param update The update that is to be copied. |
|||
* @param newGlobalIndex The global index of the resulting update. |
|||
* @param renaming A mapping from names that are to be renamed to the names they are to be |
|||
* replaced with. |
|||
* @param variableState An object knowing about the variables in the system. |
|||
*/ |
|||
Update(Update const& update, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState& variableState); |
|||
|
|||
/*! |
|||
* Peforms a deep-copy of the given update. |
|||
* |
|||
* @param otherUpdate The update to copy. |
|||
*/ |
|||
Update(Update const& otherUpdate); |
|||
|
|||
/*! |
|||
* Performs a deep-copy of the given update and assigns it to the current one. |
|||
* |
|||
* @param otherUpdate The update to assign. |
|||
*/ |
|||
Update& operator=(Update const& otherUpdate); |
|||
|
|||
/*! |
|||
* Retrieves the expression for the likelihood of this update. |
|||
* |
|||
* @return The expression for the likelihood of this update. |
|||
*/ |
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> const& getLikelihoodExpression() const; |
|||
|
|||
/*! |
|||
* Retrieves the number of boolean assignments associated with this update. |
|||
* |
|||
* @return The number of boolean assignments associated with this update. |
|||
*/ |
|||
uint_fast64_t getNumberOfBooleanAssignments() const; |
|||
|
|||
/*! |
|||
* Retrieves the number of integer assignments associated with this update. |
|||
* |
|||
* @return The number of integer assignments associated with this update. |
|||
*/ |
|||
uint_fast64_t getNumberOfIntegerAssignments() const; |
|||
|
|||
/*! |
|||
* Retrieves a reference to the map of boolean variable names to their respective assignments. |
|||
* |
|||
* @return A reference to the map of boolean variable names to their respective assignments. |
|||
*/ |
|||
std::map<std::string, storm::ir::Assignment> const& getBooleanAssignments() const; |
|||
|
|||
/*! |
|||
* Retrieves a reference to the map of integer variable names to their respective assignments. |
|||
* |
|||
* @return A reference to the map of integer variable names to their respective assignments. |
|||
*/ |
|||
std::map<std::string, storm::ir::Assignment> const& getIntegerAssignments() const; |
|||
|
|||
/*! |
|||
* Retrieves a reference to the assignment for the boolean variable with the given name. |
|||
* |
|||
* @return A reference to the assignment for the boolean variable with the given name. |
|||
*/ |
|||
storm::ir::Assignment const& getBooleanAssignment(std::string const& variableName) const; |
|||
|
|||
/*! |
|||
* Retrieves a reference to the assignment for the integer variable with the given name. |
|||
* |
|||
* @return A reference to the assignment for the integer variable with the given name. |
|||
*/ |
|||
storm::ir::Assignment const& getIntegerAssignment(std::string const& variableName) const; |
|||
|
|||
/*! |
|||
* Retrieves the global index of the update, that is, a unique index over all modules. |
|||
* |
|||
* @return The global index of the update. |
|||
*/ |
|||
uint_fast64_t getGlobalIndex() const; |
|||
|
|||
/*! |
|||
* Retrieves a string representation of this update. |
|||
* |
|||
* @return A string representation of this update. |
|||
*/ |
|||
std::string toString() const; |
|||
|
|||
private: |
|||
// An expression specifying the likelihood of taking this update. |
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> likelihoodExpression; |
|||
|
|||
// A mapping of boolean variable names to their assignments in this update. |
|||
std::map<std::string, storm::ir::Assignment> booleanAssignments; |
|||
|
|||
// A mapping of integer variable names to their assignments in this update. |
|||
std::map<std::string, storm::ir::Assignment> integerAssignments; |
|||
|
|||
// The global index of the update. |
|||
uint_fast64_t globalIndex; |
|||
}; |
|||
|
|||
} // namespace ir |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_UPDATE_H_ */ |
|||
@ -1,74 +0,0 @@ |
|||
/*
|
|||
* Variable.cpp |
|||
* |
|||
* Created on: 12.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include <sstream>
|
|||
#include <map>
|
|||
#include <iostream>
|
|||
|
|||
#include "Variable.h"
|
|||
#include "src/parser/prismparser/VariableState.h"
|
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
|
|||
Variable::Variable() : localIndex(0), globalIndex(0), variableName(), initialValue() { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
Variable::Variable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue) |
|||
: localIndex(localIndex), globalIndex(globalIndex), variableName(variableName), initialValue(std::move(initialValue)) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
Variable::Variable(Variable const& otherVariable) : localIndex(otherVariable.localIndex), globalIndex(otherVariable.globalIndex), variableName(otherVariable.variableName), initialValue() { |
|||
if (otherVariable.initialValue != nullptr) { |
|||
initialValue = otherVariable.initialValue->clone(); |
|||
} |
|||
} |
|||
|
|||
Variable::Variable(Variable const& var, std::string const& newName, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) |
|||
: localIndex(var.getLocalIndex()), globalIndex(newGlobalIndex), variableName(newName), initialValue() { |
|||
if (var.initialValue != nullptr) { |
|||
this->initialValue = var.initialValue->clone(renaming, variableState); |
|||
} |
|||
} |
|||
|
|||
Variable& Variable::operator=(Variable const& otherVariable) { |
|||
if (this != &otherVariable) { |
|||
this->localIndex = otherVariable.localIndex; |
|||
this->globalIndex = otherVariable.globalIndex; |
|||
this->variableName = otherVariable.variableName; |
|||
if (otherVariable.initialValue != nullptr) { |
|||
this->initialValue = otherVariable.initialValue->clone(); |
|||
} |
|||
} |
|||
|
|||
return *this; |
|||
} |
|||
|
|||
std::string const& Variable::getName() const { |
|||
return variableName; |
|||
} |
|||
|
|||
uint_fast64_t Variable::getGlobalIndex() const { |
|||
return globalIndex; |
|||
} |
|||
|
|||
uint_fast64_t Variable::getLocalIndex() const { |
|||
return localIndex; |
|||
} |
|||
|
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> const& Variable::getInitialValue() const { |
|||
return initialValue; |
|||
} |
|||
|
|||
void Variable::setInitialValue(std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue) { |
|||
this->initialValue = std::move(initialValue); |
|||
} |
|||
|
|||
} // namespace ir
|
|||
} // namespace storm
|
|||
@ -1,124 +0,0 @@ |
|||
/* |
|||
* Variable.h |
|||
* |
|||
* Created on: 06.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_VARIABLE_H_ |
|||
#define STORM_IR_VARIABLE_H_ |
|||
|
|||
#include <string> |
|||
#include <memory> |
|||
|
|||
#include "expressions/BaseExpression.h" |
|||
|
|||
namespace storm { |
|||
|
|||
namespace parser { |
|||
namespace prism { |
|||
class VariableState; |
|||
} // namespace prismparser |
|||
} // namespace parser |
|||
|
|||
namespace ir { |
|||
|
|||
/*! |
|||
* A class representing a untyped variable. |
|||
*/ |
|||
class Variable { |
|||
public: |
|||
/*! |
|||
* Default constructor. Creates an unnamed, untyped variable without initial value. |
|||
*/ |
|||
Variable(); |
|||
|
|||
/*! |
|||
* Creates an untyped variable with the given name and initial value. |
|||
* |
|||
* @param localIndex A module-local index for the variable. |
|||
* @param globalIndex A globally unique (among the variables of equal type) index for the variable. |
|||
* @param variableName the name of the variable. |
|||
* @param initialValue the expression that defines the initial value of the variable. |
|||
*/ |
|||
Variable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue = nullptr); |
|||
|
|||
/*! |
|||
* Creates a copy of the given variable and performs the provided renaming. |
|||
* |
|||
* @param oldVariable The variable to copy. |
|||
* @param newName New name of this variable. |
|||
* @param newGlobalIndex The new global index of the variable. |
|||
* @param renaming A mapping from names that are to be renamed to the names they are to be |
|||
* replaced with. |
|||
* @param variableState An object knowing about the variables in the system. |
|||
*/ |
|||
Variable(Variable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState); |
|||
|
|||
/*! |
|||
* Creates a deep-copy of the given variable. |
|||
* |
|||
* @param otherVariable The variable to copy. |
|||
*/ |
|||
Variable(Variable const& otherVariable); |
|||
|
|||
/*! |
|||
* Creates a deep-copy of the given variable and assigns it to the current one. |
|||
*/ |
|||
Variable& operator=(Variable const& otherVariable); |
|||
|
|||
/*! |
|||
* Retrieves the name of the variable. |
|||
* |
|||
* @return The name of the variable. |
|||
*/ |
|||
std::string const& getName() const; |
|||
|
|||
/*! |
|||
* Retrieves the global index of the variable, i.e. the index in all variables of equal type |
|||
* of all modules. |
|||
* |
|||
* @return The global index of the variable. |
|||
*/ |
|||
uint_fast64_t getGlobalIndex() const; |
|||
|
|||
/*! |
|||
* Retrieves the global index of the variable, i.e. the index in all variables of equal type in |
|||
* the same module. |
|||
* |
|||
* @return The local index of the variable. |
|||
*/ |
|||
uint_fast64_t getLocalIndex() const; |
|||
|
|||
/*! |
|||
* Retrieves the expression defining the initial value of the variable. |
|||
* |
|||
* @return The expression defining the initial value of the variable. |
|||
*/ |
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> const& getInitialValue() const; |
|||
|
|||
/*! |
|||
* Sets the initial value to the given expression. |
|||
* |
|||
* @param initialValue The new initial value. |
|||
*/ |
|||
void setInitialValue(std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue); |
|||
|
|||
private: |
|||
// A unique (among the variables of equal type) index for the variable inside its module. |
|||
uint_fast64_t localIndex; |
|||
|
|||
// A unique (among the variables of equal type) index for the variable over all modules. |
|||
uint_fast64_t globalIndex; |
|||
|
|||
// The name of the variable. |
|||
std::string variableName; |
|||
|
|||
// The expression defining the initial value of the variable. |
|||
std::unique_ptr<storm::ir::expressions::BaseExpression> initialValue; |
|||
}; |
|||
|
|||
} // namespace ir |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_VARIABLE_H_ */ |
|||
@ -1,85 +0,0 @@ |
|||
/*
|
|||
* BaseExpression.cpp |
|||
* |
|||
* Created on: 10.06.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include "BaseExpression.h"
|
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
BaseExpression::BaseExpression() : type(undefined) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
BaseExpression::BaseExpression(ReturnType type) : type(type) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
BaseExpression::BaseExpression(BaseExpression const& baseExpression) : type(baseExpression.type) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
BaseExpression::~BaseExpression() { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
std::unique_ptr<BaseExpression> BaseExpression::substitute(std::unique_ptr<BaseExpression>&& expression, std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution) { |
|||
BaseExpression* result = expression->performSubstitution(substitution); |
|||
|
|||
if (result != expression.get()) { |
|||
return std::unique_ptr<BaseExpression>(result); |
|||
} else { |
|||
return std::move(expression); |
|||
} |
|||
} |
|||
|
|||
int_fast64_t BaseExpression::getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
if (type != int_) { |
|||
throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression of type '" |
|||
<< this->getTypeName() << "' as 'int'."; |
|||
} |
|||
throw storm::exceptions::NotImplementedException() << "Cannot evaluate expression of type '" |
|||
<< this->getTypeName() << " because evaluation implementation is missing."; |
|||
} |
|||
|
|||
bool BaseExpression::getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
if (type != bool_) { |
|||
throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression of type '" |
|||
<< this->getTypeName() << "' as 'bool'."; |
|||
} |
|||
throw storm::exceptions::NotImplementedException() << "Cannot evaluate expression of type '" |
|||
<< this->getTypeName() << " because evaluation implementation is missing."; |
|||
} |
|||
|
|||
double BaseExpression::getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
if (type != double_ && type != int_) { |
|||
throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression of type '" |
|||
<< this->getTypeName() << "' as 'double'."; |
|||
} |
|||
throw storm::exceptions::NotImplementedException() << "Cannot evaluate expression of type '" |
|||
<< this->getTypeName() << " because evaluation implementation is missing."; |
|||
} |
|||
|
|||
std::string BaseExpression::getTypeName() const { |
|||
switch(type) { |
|||
case bool_: return std::string("bool"); |
|||
case int_: return std::string("int"); |
|||
case double_: return std::string("double"); |
|||
default: return std::string("undefined"); |
|||
} |
|||
} |
|||
|
|||
BaseExpression::ReturnType BaseExpression::getType() const { |
|||
return type; |
|||
} |
|||
|
|||
BaseExpression* BaseExpression::performSubstitution(std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution) { |
|||
return this; |
|||
} |
|||
|
|||
} // namespace expressions
|
|||
} // namespace ir
|
|||
} // namespace storm
|
|||
@ -1,172 +0,0 @@ |
|||
/* |
|||
* BaseExpression.h |
|||
* |
|||
* Created on: 03.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_EXPRESSIONS_BASEEXPRESSION_H_ |
|||
#define STORM_IR_EXPRESSIONS_BASEEXPRESSION_H_ |
|||
|
|||
#include <string> |
|||
#include <vector> |
|||
#include <map> |
|||
#include <memory> |
|||
|
|||
#include "src/exceptions/ExpressionEvaluationException.h" |
|||
#include "src/exceptions/NotImplementedException.h" |
|||
#include "ExpressionVisitor.h" |
|||
|
|||
namespace storm { |
|||
|
|||
// Forward-declare VariableState. |
|||
namespace parser { |
|||
namespace prism { |
|||
class VariableState; |
|||
} // namespace prismparser |
|||
} // namespace parser |
|||
|
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
/*! |
|||
* The base class for all expressions. |
|||
*/ |
|||
class BaseExpression { |
|||
public: |
|||
// Forward declare friend classes to allow access to substitute. |
|||
friend class BinaryExpression; |
|||
friend class UnaryExpression; |
|||
|
|||
/*! |
|||
* Each node in an expression tree has a uniquely defined type from this enum. |
|||
*/ |
|||
enum ReturnType {undefined, bool_, int_, double_}; |
|||
|
|||
/*! |
|||
* Creates an expression with undefined type. |
|||
*/ |
|||
BaseExpression(); |
|||
|
|||
/*! |
|||
* Creates an expression with the given type. |
|||
* |
|||
* @param type The type of the expression. |
|||
*/ |
|||
BaseExpression(ReturnType type); |
|||
|
|||
/*! |
|||
* Copy-constructs from the given expression. |
|||
* |
|||
* @param baseExpression The expression to copy. |
|||
*/ |
|||
BaseExpression(BaseExpression const& baseExpression); |
|||
|
|||
/*! |
|||
* Destructor. |
|||
*/ |
|||
virtual ~BaseExpression(); |
|||
|
|||
/*! |
|||
* Performes a deep-copy of the expression. |
|||
* |
|||
* @return A deep-copy of the expression. |
|||
*/ |
|||
virtual std::unique_ptr<BaseExpression> clone() const = 0; |
|||
|
|||
/*! |
|||
* Copies the expression tree underneath (including) the current node and performs the provided renaming. |
|||
* |
|||
* @param renaming A mapping from identifier names to strings they are to be replaced with. |
|||
* @param variableState An object knowing about the global variable state. |
|||
*/ |
|||
virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const = 0; |
|||
|
|||
/*! |
|||
* Performs the given substitution by replacing each variable in the given expression that is a key in |
|||
* the map by a copy of the mapped expression. |
|||
* |
|||
* @param expression The expression in which to perform the substitution. |
|||
* @param substitution The substitution to apply. |
|||
* @return The resulting expression. |
|||
*/ |
|||
static std::unique_ptr<BaseExpression> substitute(std::unique_ptr<BaseExpression>&& expression, std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution); |
|||
|
|||
/*! |
|||
* Retrieves the value of the expression as an integer given the provided variable valuation. |
|||
* |
|||
* @param variableValues The variable valuation under which to evaluate the expression. If set to null, |
|||
* constant expressions can be evaluated without variable values. However, upon encountering a variable |
|||
* expression an expression is thrown, because evaluation is impossible without the variable values then. |
|||
* @return The value of the expression as an integer. |
|||
*/ |
|||
virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const; |
|||
|
|||
/*! |
|||
* Retrieves the value of the expression as a boolean given the provided variable valuation. |
|||
* |
|||
* @param variableValues The variable valuation under which to evaluate the expression. If set to null, |
|||
* constant expressions can be evaluated without variable values. However, upon encountering a variable |
|||
* expression an expression is thrown, because evaluation is impossible without the variable values then. |
|||
* @return The value of the expression as a boolean. |
|||
*/ |
|||
virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const; |
|||
|
|||
/*! |
|||
* Retrieves the value of the expression as a double given the provided variable valuation. |
|||
* |
|||
* @param variableValues The variable valuation under which to evaluate the expression. If set to null, |
|||
* constant expressions can be evaluated without variable values. However, upon encountering a variable |
|||
* expression an expression is thrown, because evaluation is impossible without the variable values then. |
|||
* @return The value of the expression as a double. |
|||
*/ |
|||
virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const; |
|||
|
|||
/*! |
|||
* Acceptor method for visitor pattern. |
|||
* |
|||
* @param visitor The visitor that is supposed to visit each node of the expression tree. |
|||
*/ |
|||
virtual void accept(ExpressionVisitor* visitor) = 0; |
|||
|
|||
/*! |
|||
* Retrieves a string representation of the expression tree underneath the current node. |
|||
* |
|||
* @return A string representation of the expression tree underneath the current node. |
|||
*/ |
|||
virtual std::string toString() const = 0; |
|||
|
|||
/*! |
|||
* Retrieves a string representation of the type to which this node evaluates. |
|||
* |
|||
* @return A string representation of the type to which this node evaluates. |
|||
*/ |
|||
std::string getTypeName() const; |
|||
|
|||
/*! |
|||
* Retrieves the type to which the node evaluates. |
|||
* |
|||
* @return The type to which the node evaluates. |
|||
*/ |
|||
ReturnType getType() const; |
|||
|
|||
protected: |
|||
/*! |
|||
* Performs the given substitution on the expression, i.e. replaces all variables whose names are keys |
|||
* of the map by a copy of the expression they are associated with in the map. This is intended as a helper |
|||
* function for substitute. |
|||
* |
|||
* @param substitution The substitution to perform |
|||
*/ |
|||
virtual BaseExpression* performSubstitution(std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution); |
|||
|
|||
private: |
|||
// The type to which this node evaluates. |
|||
ReturnType type; |
|||
}; |
|||
|
|||
} // namespace expressions |
|||
} // namespace ir |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_EXPRESSIONS_BASEEXPRESSION_H_ */ |
|||
@ -1,67 +0,0 @@ |
|||
/*
|
|||
* BinaryBooleanFunctionExpression.cpp |
|||
* |
|||
* Created on: 10.06.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include <sstream>
|
|||
|
|||
#include "BinaryBooleanFunctionExpression.h"
|
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
BinaryBooleanFunctionExpression::BinaryBooleanFunctionExpression(std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right, FunctionType functionType) |
|||
: BinaryExpression(bool_, std::move(left), std::move(right)), functionType(functionType) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
BinaryBooleanFunctionExpression::BinaryBooleanFunctionExpression(BinaryBooleanFunctionExpression const& binaryBooleanFunctionExpression) |
|||
: BinaryExpression(binaryBooleanFunctionExpression), functionType(binaryBooleanFunctionExpression.functionType) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
std::unique_ptr<BaseExpression> BinaryBooleanFunctionExpression::clone() const { |
|||
return std::unique_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(this->getLeft()->clone(), this->getRight()->clone(), functionType)); |
|||
} |
|||
|
|||
std::unique_ptr<BaseExpression> BinaryBooleanFunctionExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const { |
|||
return std::unique_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(this->getLeft()->clone(renaming, variableState), this->getRight()->clone(renaming, variableState), this->functionType)); |
|||
} |
|||
|
|||
bool BinaryBooleanFunctionExpression::getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
bool resultLeft = this->getLeft()->getValueAsBool(variableValues); |
|||
bool resultRight = this->getRight()->getValueAsBool(variableValues); |
|||
switch(functionType) { |
|||
case AND: return resultLeft & resultRight; break; |
|||
case OR: return resultLeft | resultRight; break; |
|||
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Unknown boolean binary operator: '" << functionType << "'."; |
|||
} |
|||
} |
|||
|
|||
BinaryBooleanFunctionExpression::FunctionType BinaryBooleanFunctionExpression::getFunctionType() const { |
|||
return functionType; |
|||
} |
|||
|
|||
void BinaryBooleanFunctionExpression::accept(ExpressionVisitor* visitor) { |
|||
visitor->visit(this); |
|||
} |
|||
|
|||
std::string BinaryBooleanFunctionExpression::toString() const { |
|||
std::stringstream result; |
|||
result << "(" << this->getLeft()->toString(); |
|||
switch (functionType) { |
|||
case AND: result << " & "; break; |
|||
case OR: result << " | "; break; |
|||
} |
|||
result << this->getRight()->toString() << ")"; |
|||
|
|||
return result.str(); |
|||
} |
|||
|
|||
} // namespace expressions
|
|||
} // namespace ir
|
|||
} // namespace storm
|
|||
@ -1,69 +0,0 @@ |
|||
/* |
|||
* BinaryBooleanFunctionExpression.h |
|||
* |
|||
* Created on: 03.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_EXPRESSIONS_BINARYBOOLEANFUNCTIONEXPRESSION_H_ |
|||
#define STORM_IR_EXPRESSIONS_BINARYBOOLEANFUNCTIONEXPRESSION_H_ |
|||
|
|||
#include "BinaryExpression.h" |
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
/*! |
|||
* A class representing a binary function expression of boolean type. |
|||
*/ |
|||
class BinaryBooleanFunctionExpression : public BinaryExpression { |
|||
public: |
|||
/*! |
|||
* An enum type specifying the different functions applicable. |
|||
*/ |
|||
enum FunctionType {AND, OR}; |
|||
|
|||
/*! |
|||
* Creates a binary boolean function expression tree node with the given children and function type. |
|||
* |
|||
* @param left The left child of the node. |
|||
* @param right The right child of the node. |
|||
* @param functionType The operator that is to be applied to the two children. |
|||
*/ |
|||
BinaryBooleanFunctionExpression(std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right, FunctionType functionType); |
|||
|
|||
/*! |
|||
* Copy-constructs from the given expression. |
|||
* |
|||
* @param binaryBooleanFunctionExpression The expression to copy. |
|||
*/ |
|||
BinaryBooleanFunctionExpression(BinaryBooleanFunctionExpression const& binaryBooleanFunctionExpression); |
|||
|
|||
virtual std::unique_ptr<BaseExpression> clone() const override; |
|||
|
|||
virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override; |
|||
|
|||
virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override; |
|||
|
|||
/*! |
|||
* Retrieves the operator that is associated with this node. |
|||
* |
|||
* @param The operator that is associated with this node. |
|||
*/ |
|||
FunctionType getFunctionType() const; |
|||
|
|||
virtual void accept(ExpressionVisitor* visitor) override; |
|||
|
|||
virtual std::string toString() const override; |
|||
|
|||
private: |
|||
// The operator that is associated with this node. |
|||
FunctionType functionType; |
|||
}; |
|||
|
|||
} // namespace expressions |
|||
} // namespace ir |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_EXPRESSIONS_BINARYBOOLEANFUNCTIONEXPRESSION_H_ */ |
|||
@ -1,52 +0,0 @@ |
|||
/*
|
|||
* BinaryBooleanFunctionExpression.cpp |
|||
* |
|||
* Created on: 10.06.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include "BinaryExpression.h"
|
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
BinaryExpression::BinaryExpression(ReturnType type, std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right) |
|||
: BaseExpression(type), left(std::move(left)), right(std::move(right)) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
BinaryExpression::BinaryExpression(BinaryExpression const& binaryExpression) : BaseExpression(binaryExpression.getType()), left(binaryExpression.left->clone()), right(binaryExpression.right->clone()) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
BaseExpression* BinaryExpression::performSubstitution(std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution) { |
|||
// Get the new left successor recursively.
|
|||
BaseExpression* newLeftSuccessor = left->performSubstitution(substitution); |
|||
|
|||
// If the left successor changed, we need to update it. If it did not change, this must not be executed,
|
|||
// because assigning to the unique_ptr will destroy the current successor immediately.
|
|||
if (newLeftSuccessor != left.get()) { |
|||
left = std::unique_ptr<BaseExpression>(newLeftSuccessor); |
|||
} |
|||
|
|||
// Now do the same thing for the right successor.
|
|||
BaseExpression* newRightSuccessor = right->performSubstitution(substitution); |
|||
if (newRightSuccessor != right.get()) { |
|||
right = std::unique_ptr<BaseExpression>(newRightSuccessor); |
|||
} |
|||
|
|||
return this; |
|||
} |
|||
|
|||
std::unique_ptr<BaseExpression> const& BinaryExpression::getLeft() const { |
|||
return left; |
|||
} |
|||
|
|||
std::unique_ptr<BaseExpression> const& BinaryExpression::getRight() const { |
|||
return right; |
|||
} |
|||
|
|||
} // namespace expressions
|
|||
} // namespace ir
|
|||
} // namespace storm
|
|||
@ -1,66 +0,0 @@ |
|||
/* |
|||
* BinaryExpression.h |
|||
* |
|||
* Created on: 27.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_EXPRESSIONS_BINARYEXPRESSION_H_ |
|||
#define STORM_IR_EXPRESSIONS_BINARYEXPRESSION_H_ |
|||
|
|||
#include "src/ir/expressions/BaseExpression.h" |
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
/*! |
|||
* A class representing a generic binary expression. |
|||
*/ |
|||
class BinaryExpression : public BaseExpression { |
|||
public: |
|||
/*! |
|||
* Constructs a binary expression with the given type and children. |
|||
* @param type The type of the binary expression. |
|||
* @param left The left child of the binary expression. |
|||
* @param right The right child of the binary expression. |
|||
*/ |
|||
BinaryExpression(ReturnType type, std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right); |
|||
|
|||
/*! |
|||
* Copy-constructs from the given expression. |
|||
* |
|||
* @param binaryExpression The expression to copy. |
|||
*/ |
|||
BinaryExpression(BinaryExpression const& binaryExpression); |
|||
|
|||
/*! |
|||
* Retrieves the left child of the expression node. |
|||
* |
|||
* @return The left child of the expression node. |
|||
*/ |
|||
std::unique_ptr<BaseExpression> const& getLeft() const; |
|||
|
|||
/*! |
|||
* Retrieves the right child of the expression node. |
|||
* |
|||
* @return The right child of the expression node. |
|||
*/ |
|||
std::unique_ptr<BaseExpression> const& getRight() const; |
|||
|
|||
protected: |
|||
virtual BaseExpression* performSubstitution(std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution) override; |
|||
|
|||
private: |
|||
// The left child of the binary expression. |
|||
std::unique_ptr<BaseExpression> left; |
|||
|
|||
// The right child of the binary expression. |
|||
std::unique_ptr<BaseExpression> right; |
|||
}; |
|||
|
|||
} // namespace expressions |
|||
} // namespace ir |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_EXPRESSIONS_BINARYEXPRESSION_H_ */ |
|||
@ -1,96 +0,0 @@ |
|||
/*
|
|||
* BinaryBooleanFunctionExpression.cpp |
|||
* |
|||
* Created on: 10.06.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include <sstream>
|
|||
#include <algorithm>
|
|||
|
|||
#include "BinaryNumericalFunctionExpression.h"
|
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
BinaryNumericalFunctionExpression::BinaryNumericalFunctionExpression(ReturnType type, std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right, FunctionType functionType) |
|||
: BinaryExpression(type, std::move(left), std::move(right)), functionType(functionType) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
BinaryNumericalFunctionExpression::BinaryNumericalFunctionExpression(BinaryNumericalFunctionExpression const& binaryNumericalFunctionExpression) |
|||
: BinaryExpression(binaryNumericalFunctionExpression), functionType(binaryNumericalFunctionExpression.functionType) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
std::unique_ptr<BaseExpression> BinaryNumericalFunctionExpression::clone() const { |
|||
return std::unique_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(this->getType(), this->getLeft()->clone(), this->getRight()->clone(), functionType)); |
|||
} |
|||
|
|||
std::unique_ptr<BaseExpression> BinaryNumericalFunctionExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const { |
|||
return std::unique_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(this->getType(), this->getLeft()->clone(renaming, variableState), this->getRight()->clone(renaming, variableState), this->functionType)); |
|||
} |
|||
|
|||
BinaryNumericalFunctionExpression::FunctionType BinaryNumericalFunctionExpression::getFunctionType() const { |
|||
return functionType; |
|||
} |
|||
|
|||
int_fast64_t BinaryNumericalFunctionExpression::getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
if (this->getType() != int_) { |
|||
BaseExpression::getValueAsInt(variableValues); |
|||
} |
|||
|
|||
int_fast64_t resultLeft = this->getLeft()->getValueAsInt(variableValues); |
|||
int_fast64_t resultRight = this->getRight()->getValueAsInt(variableValues); |
|||
switch(functionType) { |
|||
case PLUS: return resultLeft + resultRight; break; |
|||
case MINUS: return resultLeft - resultRight; break; |
|||
case TIMES: return resultLeft * resultRight; break; |
|||
case DIVIDE: return resultLeft / resultRight; break; |
|||
case MIN: return std::min(resultLeft, resultRight); break; |
|||
case MAX: return std::max(resultLeft, resultRight); break; |
|||
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Unknown numeric binary operator: '" << functionType << "'."; |
|||
} |
|||
} |
|||
|
|||
double BinaryNumericalFunctionExpression::getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
if (this->getType() != double_ && this->getType() != int_) { |
|||
BaseExpression::getValueAsDouble(variableValues); |
|||
} |
|||
|
|||
double resultLeft = this->getLeft()->getValueAsDouble(variableValues); |
|||
double resultRight = this->getRight()->getValueAsDouble(variableValues); |
|||
switch(functionType) { |
|||
case PLUS: return resultLeft + resultRight; break; |
|||
case MINUS: return resultLeft - resultRight; break; |
|||
case TIMES: return resultLeft * resultRight; break; |
|||
case DIVIDE: return resultLeft / resultRight; break; |
|||
case MIN: return std::min(resultLeft, resultRight); break; |
|||
case MAX: return std::max(resultLeft, resultRight); break; |
|||
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Unknown numeric binary operator: '" << functionType << "'."; |
|||
} |
|||
} |
|||
|
|||
void BinaryNumericalFunctionExpression::accept(ExpressionVisitor* visitor) { |
|||
visitor->visit(this); |
|||
} |
|||
|
|||
std::string BinaryNumericalFunctionExpression::toString() const { |
|||
std::stringstream result; |
|||
switch (functionType) { |
|||
case PLUS: result << "(" << this->getLeft()->toString() << " + " << this->getRight()->toString() << ")"; break; |
|||
case MINUS: result << "(" << this->getLeft()->toString() << " - " << this->getRight()->toString() << ")"; break; |
|||
case TIMES: result << "(" << this->getLeft()->toString() << " * " << this->getRight()->toString() << ")"; break; |
|||
case DIVIDE: result << "(" << this->getLeft()->toString() << " / " << this->getRight()->toString() << ")"; break; |
|||
case MIN: result << "min(" << this->getLeft()->toString() << ", " << this->getRight()->toString() << ")"; break; |
|||
case MAX: result << "max(" << this->getLeft()->toString() << ", " << this->getRight()->toString() << ")"; break; |
|||
} |
|||
return result.str(); |
|||
} |
|||
|
|||
} // namespace expressions
|
|||
} // namespace ir
|
|||
} // namespace storm
|
|||
@ -1,72 +0,0 @@ |
|||
/* |
|||
* BinaryFunctionExpression.h |
|||
* |
|||
* Created on: 03.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_EXPRESSIONS_BINARYFUNCTIONEXPRESSION_H_ |
|||
#define STORM_IR_EXPRESSIONS_BINARYFUNCTIONEXPRESSION_H_ |
|||
|
|||
#include "src/ir/expressions/BinaryExpression.h" |
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
/*! |
|||
* A class representing a binary function expression of numerical type. |
|||
*/ |
|||
class BinaryNumericalFunctionExpression : public BinaryExpression { |
|||
public: |
|||
/*! |
|||
* An enum type specifying the different functions applicable. |
|||
*/ |
|||
enum FunctionType {PLUS, MINUS, TIMES, DIVIDE, MIN, MAX}; |
|||
|
|||
/*! |
|||
* Creates a binary numerical function expression with the given type, children and function type. |
|||
* |
|||
* @param type The type of the expression tree node. |
|||
* @param left The left child of the expression tree node. |
|||
* @param right The right child of the expression tree node. |
|||
* @param functionType The function that is applied to the children of this node. |
|||
*/ |
|||
BinaryNumericalFunctionExpression(ReturnType type, std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right, FunctionType functionType); |
|||
|
|||
/*! |
|||
* Performs a deep-copy of the given expression. |
|||
* |
|||
* @param binaryNumericalFunctionExpression The expression to copy. |
|||
*/ |
|||
BinaryNumericalFunctionExpression(BinaryNumericalFunctionExpression const& binaryNumericalFunctionExpression); |
|||
|
|||
virtual std::unique_ptr<BaseExpression> clone() const override; |
|||
|
|||
virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override; |
|||
|
|||
/*! |
|||
* Retrieves the operator that is associated with this node. |
|||
* |
|||
* @param The operator that is associated with this node. |
|||
*/ |
|||
FunctionType getFunctionType() const; |
|||
|
|||
virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override; |
|||
|
|||
virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override; |
|||
|
|||
virtual void accept(ExpressionVisitor* visitor) override; |
|||
|
|||
virtual std::string toString() const override; |
|||
|
|||
private: |
|||
// The operator that is associated with this node. |
|||
FunctionType functionType; |
|||
}; |
|||
|
|||
} // namespace expressions |
|||
} // namespace ir |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_EXPRESSIONS_BINARYFUNCTIONEXPRESSION_H_ */ |
|||
@ -1,75 +0,0 @@ |
|||
/*
|
|||
* BinaryBooleanFunctionExpression.cpp |
|||
* |
|||
* Created on: 10.06.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include <sstream>
|
|||
|
|||
#include "BinaryRelationExpression.h"
|
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
BinaryRelationExpression::BinaryRelationExpression(std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right, RelationType relationType) |
|||
: BinaryExpression(bool_, std::move(left), std::move(right)), relationType(relationType) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
BinaryRelationExpression::BinaryRelationExpression(BinaryRelationExpression const& binaryRelationExpression) |
|||
: BinaryExpression(binaryRelationExpression), relationType(binaryRelationExpression.relationType) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
std::unique_ptr<BaseExpression> BinaryRelationExpression::clone() const { |
|||
return std::unique_ptr<BaseExpression>(new BinaryRelationExpression(this->getLeft()->clone(), this->getRight()->clone(), relationType)); |
|||
} |
|||
|
|||
std::unique_ptr<BaseExpression> BinaryRelationExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const { |
|||
return std::unique_ptr<BaseExpression>(new BinaryRelationExpression(this->getLeft()->clone(renaming, variableState), this->getRight()->clone(renaming, variableState), this->relationType)); |
|||
} |
|||
|
|||
bool BinaryRelationExpression::getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
int_fast64_t resultLeft = this->getLeft()->getValueAsInt(variableValues); |
|||
int_fast64_t resultRight = this->getRight()->getValueAsInt(variableValues); |
|||
switch(relationType) { |
|||
case EQUAL: return resultLeft == resultRight; break; |
|||
case NOT_EQUAL: return resultLeft != resultRight; break; |
|||
case LESS: return resultLeft < resultRight; break; |
|||
case LESS_OR_EQUAL: return resultLeft <= resultRight; break; |
|||
case GREATER: return resultLeft > resultRight; break; |
|||
case GREATER_OR_EQUAL: return resultLeft >= resultRight; break; |
|||
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Unknown boolean binary relation: '" << relationType << "'."; |
|||
} |
|||
} |
|||
|
|||
BinaryRelationExpression::RelationType BinaryRelationExpression::getRelationType() const { |
|||
return relationType; |
|||
} |
|||
|
|||
void BinaryRelationExpression::accept(ExpressionVisitor* visitor) { |
|||
visitor->visit(this); |
|||
} |
|||
|
|||
std::string BinaryRelationExpression::toString() const { |
|||
std::stringstream result; |
|||
result << "(" << this->getLeft()->toString(); |
|||
switch (relationType) { |
|||
case EQUAL: result << " = "; break; |
|||
case NOT_EQUAL: result << " != "; break; |
|||
case LESS: result << " < "; break; |
|||
case LESS_OR_EQUAL: result << " <= "; break; |
|||
case GREATER: result << " > "; break; |
|||
case GREATER_OR_EQUAL: result << " >= "; break; |
|||
} |
|||
result << this->getRight()->toString() << ")"; |
|||
|
|||
return result.str(); |
|||
} |
|||
|
|||
} // namespace expressions
|
|||
} // namespace ir
|
|||
} // namespace storm
|
|||
@ -1,69 +0,0 @@ |
|||
/* |
|||
* BinaryRelationExpression.h |
|||
* |
|||
* Created on: 03.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_EXPRESSIONS_BINARYRELATIONEXPRESSION_H_ |
|||
#define STORM_IR_EXPRESSIONS_BINARYRELATIONEXPRESSION_H_ |
|||
|
|||
#include "src/ir/expressions/BinaryExpression.h" |
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
/*! |
|||
* A class representing a binary relation expression of boolean type. |
|||
*/ |
|||
class BinaryRelationExpression : public BinaryExpression { |
|||
public: |
|||
/*! |
|||
* An enum type specifying the different relations applicable. |
|||
*/ |
|||
enum RelationType {EQUAL, NOT_EQUAL, LESS, LESS_OR_EQUAL, GREATER, GREATER_OR_EQUAL}; |
|||
|
|||
/*! |
|||
* Creates a binary relation expression tree node with the given children and relation type. |
|||
* |
|||
* @param left The left child of the binary expression. |
|||
* @param right The right child of the binary expression. |
|||
* @param relationType The type of the relation associated with this node. |
|||
*/ |
|||
BinaryRelationExpression(std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right, RelationType relationType); |
|||
|
|||
/*! |
|||
* Copy-constructs from the given expression. |
|||
* |
|||
* @param binaryRelationExpression The expression to copy. |
|||
*/ |
|||
BinaryRelationExpression(BinaryRelationExpression const& binaryRelationExpression); |
|||
|
|||
virtual std::unique_ptr<BaseExpression> clone() const override; |
|||
|
|||
virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override; |
|||
|
|||
virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override; |
|||
|
|||
/*! |
|||
* Retrieves the relation that is associated with this node. |
|||
* |
|||
* @param The relation that is associated with this node. |
|||
*/ |
|||
RelationType getRelationType() const; |
|||
|
|||
virtual void accept(ExpressionVisitor* visitor) override; |
|||
|
|||
virtual std::string toString() const override; |
|||
|
|||
private: |
|||
// The relation operator associated with this node. |
|||
RelationType relationType; |
|||
}; |
|||
|
|||
} // namespace expressions |
|||
} // namespace ir |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_EXPRESSIONS_BINARYRELATIONEXPRESSION_H_ */ |
|||
@ -1,45 +0,0 @@ |
|||
/*
|
|||
* BooleanConstantExpression.cpp |
|||
* |
|||
* Created on: 10.06.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include "BooleanConstantExpression.h"
|
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
BooleanConstantExpression::BooleanConstantExpression(std::string const& constantName) : ConstantExpression<bool>(bool_, constantName) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
BooleanConstantExpression::BooleanConstantExpression(BooleanConstantExpression const& booleanConstantExpression) : ConstantExpression(booleanConstantExpression) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
std::unique_ptr<BaseExpression> BooleanConstantExpression::clone() const { |
|||
return std::unique_ptr<BaseExpression>(new BooleanConstantExpression(*this)); |
|||
} |
|||
|
|||
std::unique_ptr<BaseExpression> BooleanConstantExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const { |
|||
return std::unique_ptr<BaseExpression>(new BooleanConstantExpression(*this)); |
|||
} |
|||
|
|||
bool BooleanConstantExpression::getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
if (!this->isDefined()) { |
|||
throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Boolean constant '" << this->getConstantName() << "' is undefined."; |
|||
} else { |
|||
return this->getValue(); |
|||
} |
|||
} |
|||
|
|||
void BooleanConstantExpression::accept(ExpressionVisitor* visitor) { |
|||
visitor->visit(this); |
|||
} |
|||
|
|||
} // namespace expressions
|
|||
} // namespace ir
|
|||
} // namespace storm
|
|||
@ -1,49 +0,0 @@ |
|||
/* |
|||
* BooleanConstantExpression.h |
|||
* |
|||
* Created on: 04.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_EXPRESSIONS_BOOLEANCONSTANTEXPRESSION_H_ |
|||
#define STORM_IR_EXPRESSIONS_BOOLEANCONSTANTEXPRESSION_H_ |
|||
|
|||
#include "ConstantExpression.h" |
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
/*! |
|||
* A class representing a boolean constant expression. |
|||
*/ |
|||
class BooleanConstantExpression : public ConstantExpression<bool> { |
|||
public: |
|||
/*! |
|||
* Creates a boolean constant expression with the given constant name. |
|||
* |
|||
* @param constantName The name of the constant to use. |
|||
*/ |
|||
BooleanConstantExpression(std::string const& constantName); |
|||
|
|||
/*! |
|||
* Copy-constructs from the given expression. |
|||
* |
|||
* @param booleanConstantExpression The expression to copy. |
|||
*/ |
|||
BooleanConstantExpression(BooleanConstantExpression const& booleanConstantExpression); |
|||
|
|||
virtual std::unique_ptr<BaseExpression> clone() const override; |
|||
|
|||
virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override; |
|||
|
|||
virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override; |
|||
|
|||
virtual void accept(ExpressionVisitor* visitor) override; |
|||
}; |
|||
|
|||
} // namespace expressions |
|||
} // namespace ir |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_EXPRESSIONS_BOOLEANCONSTANTEXPRESSION_H_ */ |
|||
@ -1,49 +0,0 @@ |
|||
/*
|
|||
* BooleanLiteralExpression.cpp |
|||
* |
|||
* Created on: 04.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include "BooleanLiteralExpression.h"
|
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
BooleanLiteralExpression::BooleanLiteralExpression(bool value) : BaseExpression(bool_), value(value) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
BooleanLiteralExpression::BooleanLiteralExpression(BooleanLiteralExpression const& booleanLiteralExpression) |
|||
: BaseExpression(booleanLiteralExpression), value(booleanLiteralExpression.value) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
std::unique_ptr<BaseExpression> BooleanLiteralExpression::clone() const { |
|||
return std::unique_ptr<BaseExpression>(new BooleanLiteralExpression(*this)); |
|||
} |
|||
|
|||
std::unique_ptr<BaseExpression> BooleanLiteralExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const { |
|||
return std::unique_ptr<BaseExpression>(new BooleanLiteralExpression(this->value)); |
|||
} |
|||
|
|||
bool BooleanLiteralExpression::getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
return value; |
|||
} |
|||
|
|||
void BooleanLiteralExpression::accept(ExpressionVisitor* visitor) { |
|||
visitor->visit(this); |
|||
} |
|||
|
|||
std::string BooleanLiteralExpression::toString() const { |
|||
if (value) { |
|||
return std::string("true"); |
|||
} else { |
|||
return std::string("false"); |
|||
} |
|||
} |
|||
|
|||
} // namespace expressions
|
|||
} // namespace ir
|
|||
} // namespace storm
|
|||
@ -1,55 +0,0 @@ |
|||
/* |
|||
* BooleanLiteralExpression.h |
|||
* |
|||
* Created on: 03.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_EXPRESSIONS_BOOLEANLITERALEXPRESSION_H_ |
|||
#define STORM_IR_EXPRESSIONS_BOOLEANLITERALEXPRESSION_H_ |
|||
|
|||
#include "src/ir/expressions/BaseExpression.h" |
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
/*! |
|||
* A class representing a boolean literal. |
|||
*/ |
|||
class BooleanLiteralExpression : public BaseExpression { |
|||
public: |
|||
/*! |
|||
* Creates a boolean literal expression with the given value. |
|||
* |
|||
* @param value The value for the boolean literal. |
|||
*/ |
|||
BooleanLiteralExpression(bool value); |
|||
|
|||
/*! |
|||
* Copy-constructs from the given expression. |
|||
* |
|||
* @param booleanLiteralExpression The expression to copy. |
|||
*/ |
|||
BooleanLiteralExpression(BooleanLiteralExpression const& booleanLiteralExpression); |
|||
|
|||
virtual std::unique_ptr<BaseExpression> clone() const override; |
|||
|
|||
virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override; |
|||
|
|||
virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override; |
|||
|
|||
virtual void accept(ExpressionVisitor* visitor) override; |
|||
|
|||
virtual std::string toString() const override; |
|||
|
|||
private: |
|||
// The value of the boolean literal. |
|||
bool value; |
|||
}; |
|||
|
|||
} // namespace expressions |
|||
} // namespace ir |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_EXPRESSIONS_BOOLEANLITERALEXPRESSION_H_ */ |
|||
@ -1,132 +0,0 @@ |
|||
/* |
|||
* ConstantExpression.h |
|||
* |
|||
* Created on: 03.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_EXPRESSIONS_CONSTANTEXPRESSION_H_ |
|||
#define STORM_IR_EXPRESSIONS_CONSTANTEXPRESSION_H_ |
|||
|
|||
#include "BaseExpression.h" |
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
// A struct for storing whether the constant was defined and if so, what value it holds. |
|||
template<class T> |
|||
struct ConstantDefinitionStruct { |
|||
/*! |
|||
* Constructs a structure indicating that the constant has been defined with the given value. |
|||
* |
|||
* @param value The value with which the constant was defined. |
|||
*/ |
|||
ConstantDefinitionStruct(T value) : value(value), defined(true) { |
|||
// Nothing to do here. |
|||
} |
|||
|
|||
/*! |
|||
* Constructs a structure indicating that the constant has not yet been defined. |
|||
* |
|||
* @param value The value with which the constant was defined. |
|||
*/ |
|||
ConstantDefinitionStruct() : value(), defined(false) { |
|||
// Nothing to do here. |
|||
} |
|||
|
|||
T value; |
|||
bool defined; |
|||
}; |
|||
|
|||
/*! |
|||
* A class representing a generic constant expression. |
|||
*/ |
|||
template<class T> |
|||
class ConstantExpression : public BaseExpression { |
|||
public: |
|||
/*! |
|||
* Constructs a constant expression of the given type with the given constant name. |
|||
* |
|||
* @param type The type of the constant. |
|||
* @param constantName The name of the constant. |
|||
*/ |
|||
ConstantExpression(ReturnType type, std::string const& constantName) : BaseExpression(type), constantName(constantName), valueStructPointer(new ConstantDefinitionStruct<T>()) { |
|||
// Nothing to do here. |
|||
} |
|||
|
|||
/*! |
|||
* Copy-constructs from the given expression. |
|||
* |
|||
* @param constantExpression The expression to copy. |
|||
*/ |
|||
ConstantExpression(ConstantExpression const& constantExpression) : BaseExpression(constantExpression), constantName(constantExpression.constantName), valueStructPointer(constantExpression.valueStructPointer) { |
|||
// Nothing to do here. |
|||
} |
|||
|
|||
/*! |
|||
* Retrieves the name of the constant. |
|||
* |
|||
* @return The name of the constant. |
|||
*/ |
|||
std::string const& getConstantName() const { |
|||
return constantName; |
|||
} |
|||
|
|||
virtual std::string toString() const override { |
|||
std::stringstream result; |
|||
if (this->valueStructPointer->defined) { |
|||
result << this->valueStructPointer->value; |
|||
} else { |
|||
result << this->getConstantName(); |
|||
} |
|||
return result.str(); |
|||
} |
|||
|
|||
/*! |
|||
* Retrieves whether the constant is defined or not. |
|||
* |
|||
* @return True if the constant is defined. |
|||
*/ |
|||
bool isDefined() const { |
|||
return this->valueStructPointer->defined; |
|||
} |
|||
|
|||
/*! |
|||
* Retrieves the value of the constant if it is defined. |
|||
*/ |
|||
T getValue() const { |
|||
return this->valueStructPointer->value; |
|||
} |
|||
|
|||
/*! |
|||
* Defines the constant using the given value. |
|||
* |
|||
* @param value The value to use for defining the constant. |
|||
*/ |
|||
void define(T value) { |
|||
this->valueStructPointer->defined = true; |
|||
this->valueStructPointer->value = value; |
|||
} |
|||
|
|||
/*! |
|||
* Undefines the value that was previously set for this constant (if any). |
|||
*/ |
|||
void undefine() { |
|||
this->valueStructPointer->defined = false; |
|||
this->valueStructPointer->value = T(); |
|||
} |
|||
|
|||
private: |
|||
// The name of the constant. |
|||
std::string constantName; |
|||
|
|||
// The definedness status and (if applicable) the value of the constant. |
|||
std::shared_ptr<ConstantDefinitionStruct<T>> valueStructPointer; |
|||
}; |
|||
|
|||
} // namespace expressions |
|||
} // namespace ir |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_EXPRESSIONS_CONSTANTEXPRESSION_H_ */ |
|||
@ -1,45 +0,0 @@ |
|||
/*
|
|||
* DoubleConstantExpression.cpp |
|||
* |
|||
* Created on: 10.06.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include "DoubleConstantExpression.h"
|
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
DoubleConstantExpression::DoubleConstantExpression(std::string const& constantName) : ConstantExpression<double>(double_, constantName) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
DoubleConstantExpression::DoubleConstantExpression(DoubleConstantExpression const& doubleConstantExpression) : ConstantExpression(doubleConstantExpression) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
std::unique_ptr<BaseExpression> DoubleConstantExpression::clone() const { |
|||
return std::unique_ptr<BaseExpression>(new DoubleConstantExpression(*this)); |
|||
} |
|||
|
|||
std::unique_ptr<BaseExpression> DoubleConstantExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const { |
|||
return std::unique_ptr<BaseExpression>(new DoubleConstantExpression(*this)); |
|||
} |
|||
|
|||
double DoubleConstantExpression::getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
if (!this->isDefined()) { |
|||
throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Double constant '" << this->getConstantName() << "' is undefined."; |
|||
} else { |
|||
return this->getValue(); |
|||
} |
|||
} |
|||
|
|||
void DoubleConstantExpression::accept(ExpressionVisitor* visitor) { |
|||
visitor->visit(this); |
|||
} |
|||
|
|||
} // namespace expressions
|
|||
} // namespace ir
|
|||
} // namespace storm
|
|||
@ -1,49 +0,0 @@ |
|||
/* |
|||
* DoubleConstantExpression.h |
|||
* |
|||
* Created on: 04.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_EXPRESSIONS_DOUBLECONSTANTEXPRESSION_H_ |
|||
#define STORM_IR_EXPRESSIONS_DOUBLECONSTANTEXPRESSION_H_ |
|||
|
|||
#include "ConstantExpression.h" |
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
/*! |
|||
* A class representing a constant expression of type double. |
|||
*/ |
|||
class DoubleConstantExpression : public ConstantExpression<double> { |
|||
public: |
|||
/*! |
|||
* Creates a double constant expression with the given constant name. |
|||
* |
|||
* @param constantName The name of the constant to use. |
|||
*/ |
|||
DoubleConstantExpression(std::string const& constantName); |
|||
|
|||
/*! |
|||
* Copy-constructs from the given expression. |
|||
* |
|||
* @param doubleConstantExpression The expression to copy. |
|||
*/ |
|||
DoubleConstantExpression(DoubleConstantExpression const& doubleConstantExpression); |
|||
|
|||
virtual std::unique_ptr<BaseExpression> clone() const override; |
|||
|
|||
virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override; |
|||
|
|||
virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override; |
|||
|
|||
virtual void accept(ExpressionVisitor* visitor) override; |
|||
}; |
|||
|
|||
} // namespace expressions |
|||
} // namespace ir |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_EXPRESSIONS_DOUBLECONSTANTEXPRESSION_H_ */ |
|||
@ -1,49 +0,0 @@ |
|||
/*
|
|||
* DoubleLiteralExpression.cpp |
|||
* |
|||
* Created on: 10.06.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include <sstream>
|
|||
|
|||
#include "DoubleLiteralExpression.h"
|
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
DoubleLiteralExpression::DoubleLiteralExpression(double value) : BaseExpression(double_), value(value) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
DoubleLiteralExpression::DoubleLiteralExpression(DoubleLiteralExpression const& doubleLiteralExpression) |
|||
: BaseExpression(doubleLiteralExpression), value(doubleLiteralExpression.value) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
std::unique_ptr<BaseExpression> DoubleLiteralExpression::clone() const { |
|||
return std::unique_ptr<BaseExpression>(new DoubleLiteralExpression(*this)); |
|||
} |
|||
|
|||
std::unique_ptr<BaseExpression> DoubleLiteralExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const { |
|||
return std::unique_ptr<BaseExpression>(new DoubleLiteralExpression(this->value)); |
|||
} |
|||
|
|||
double DoubleLiteralExpression::getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
return value; |
|||
} |
|||
|
|||
void DoubleLiteralExpression::accept(ExpressionVisitor* visitor) { |
|||
visitor->visit(this); |
|||
} |
|||
|
|||
std::string DoubleLiteralExpression::toString() const { |
|||
std::stringstream result; |
|||
result << value; |
|||
return result.str(); |
|||
} |
|||
|
|||
} // namespace expressions
|
|||
} // namespace ir
|
|||
} // namespace storm
|
|||
@ -1,55 +0,0 @@ |
|||
/* |
|||
* DoubleLiteralExpression.h |
|||
* |
|||
* Created on: 03.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_EXPRESSIONS_DOUBLELITERALEXPRESSION_H_ |
|||
#define STORM_IR_EXPRESSIONS_DOUBLELITERALEXPRESSION_H_ |
|||
|
|||
#include "src/ir/expressions/BaseExpression.h" |
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
/*! |
|||
* A class representing a double literal. |
|||
*/ |
|||
class DoubleLiteralExpression : public BaseExpression { |
|||
public: |
|||
/*! |
|||
* Creates a double literal expression with the given value. |
|||
* |
|||
* @param value The value for the double literal. |
|||
*/ |
|||
DoubleLiteralExpression(double value); |
|||
|
|||
/*! |
|||
* Copy-constructs from the given expression. |
|||
* |
|||
* @param doubleLiteralExpression The expression to copy. |
|||
*/ |
|||
DoubleLiteralExpression(DoubleLiteralExpression const& doubleLiteralExpression); |
|||
|
|||
virtual std::unique_ptr<BaseExpression> clone() const override; |
|||
|
|||
virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override; |
|||
|
|||
virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override; |
|||
|
|||
virtual void accept(ExpressionVisitor* visitor) override; |
|||
|
|||
virtual std::string toString() const override; |
|||
|
|||
private: |
|||
// The value of the double literal. |
|||
double value; |
|||
}; |
|||
|
|||
} // namespace expressions |
|||
} // namespace ir |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_EXPRESSIONS_DOUBLELITERALEXPRESSION_H_ */ |
|||
@ -1,49 +0,0 @@ |
|||
/* |
|||
* ExpressionVisitor.h |
|||
* |
|||
* Created on: 26.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_EXPRESSIONS_EXPRESSIONVISITOR_H_ |
|||
#define STORM_IR_EXPRESSIONS_EXPRESSIONVISITOR_H_ |
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
class BaseExpression; |
|||
class BinaryBooleanFunctionExpression; |
|||
class BinaryNumericalFunctionExpression; |
|||
class BinaryRelationExpression; |
|||
class BooleanConstantExpression; |
|||
class BooleanLiteralExpression; |
|||
class DoubleConstantExpression; |
|||
class DoubleLiteralExpression; |
|||
class IntegerConstantExpression; |
|||
class IntegerLiteralExpression; |
|||
class UnaryBooleanFunctionExpression; |
|||
class UnaryNumericalFunctionExpression; |
|||
class VariableExpression; |
|||
|
|||
class ExpressionVisitor { |
|||
public: |
|||
virtual void visit(BinaryBooleanFunctionExpression* expression) = 0; |
|||
virtual void visit(BinaryNumericalFunctionExpression* expression) = 0; |
|||
virtual void visit(BinaryRelationExpression* expression) = 0; |
|||
virtual void visit(BooleanConstantExpression* expression) = 0; |
|||
virtual void visit(BooleanLiteralExpression* expression) = 0; |
|||
virtual void visit(DoubleConstantExpression* expression) = 0; |
|||
virtual void visit(DoubleLiteralExpression* expression) = 0; |
|||
virtual void visit(IntegerConstantExpression* expression) = 0; |
|||
virtual void visit(IntegerLiteralExpression* expression) = 0; |
|||
virtual void visit(UnaryBooleanFunctionExpression* expression) = 0; |
|||
virtual void visit(UnaryNumericalFunctionExpression* expression) = 0; |
|||
virtual void visit(VariableExpression* expression) = 0; |
|||
}; |
|||
|
|||
} // namespace expressions |
|||
} // namespace ir |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_EXPRESSIONS_EXPRESSIONVISITOR_H_ */ |
|||
@ -1,26 +0,0 @@ |
|||
/* |
|||
* Expressions.h |
|||
* |
|||
* Created on: 03.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_EXPRESSIONS_EXPRESSIONS_H_ |
|||
#define STORM_IR_EXPRESSIONS_EXPRESSIONS_H_ |
|||
|
|||
#include "BaseExpression.h" |
|||
#include "BinaryBooleanFunctionExpression.h" |
|||
#include "BinaryNumericalFunctionExpression.h" |
|||
#include "BinaryRelationExpression.h" |
|||
#include "BooleanLiteralExpression.h" |
|||
#include "DoubleLiteralExpression.h" |
|||
#include "IntegerLiteralExpression.h" |
|||
#include "UnaryBooleanFunctionExpression.h" |
|||
#include "UnaryNumericalFunctionExpression.h" |
|||
#include "VariableExpression.h" |
|||
#include "ConstantExpression.h" |
|||
#include "BooleanConstantExpression.h" |
|||
#include "IntegerConstantExpression.h" |
|||
#include "DoubleConstantExpression.h" |
|||
|
|||
#endif /* STORM_IR_EXPRESSIONS_EXPRESSIONS_H_ */ |
|||
@ -1,48 +0,0 @@ |
|||
/*
|
|||
* IntegerConstantExpression.cpp |
|||
* |
|||
* Created on: 10.06.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include "IntegerConstantExpression.h"
|
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
IntegerConstantExpression::IntegerConstantExpression(std::string const& constantName) : ConstantExpression(int_, constantName) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
IntegerConstantExpression::IntegerConstantExpression(IntegerConstantExpression const& integerConstantExpression) : ConstantExpression(integerConstantExpression) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
std::unique_ptr<BaseExpression> IntegerConstantExpression::clone() const { |
|||
return std::unique_ptr<BaseExpression>(new IntegerConstantExpression(*this)); |
|||
} |
|||
|
|||
std::unique_ptr<BaseExpression> IntegerConstantExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const { |
|||
return std::unique_ptr<BaseExpression>(new IntegerConstantExpression(*this)); |
|||
} |
|||
|
|||
double IntegerConstantExpression::getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
return static_cast<double>(getValueAsInt(variableValues)); |
|||
} |
|||
|
|||
int_fast64_t IntegerConstantExpression::getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
if (!this->isDefined()) { |
|||
throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Integer constant '" << this->getConstantName() << "' is undefined."; |
|||
} else { |
|||
return this->getValue(); |
|||
} |
|||
} |
|||
|
|||
void IntegerConstantExpression::accept(ExpressionVisitor* visitor) { |
|||
visitor->visit(this); |
|||
} |
|||
} // namespace expressions
|
|||
} // namespace ir
|
|||
} // namespace storm
|
|||
@ -1,51 +0,0 @@ |
|||
/* |
|||
* IntegerConstantExpression.h |
|||
* |
|||
* Created on: 04.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_EXPRESSIONS_INTEGERCONSTANTEXPRESSION_H_ |
|||
#define STORM_IR_EXPRESSIONS_INTEGERCONSTANTEXPRESSION_H_ |
|||
|
|||
#include "ConstantExpression.h" |
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
/*! |
|||
* A class representing a constant expression of type integer. |
|||
*/ |
|||
class IntegerConstantExpression : public ConstantExpression<int_fast64_t> { |
|||
public: |
|||
/*! |
|||
* Creates an integer constant expression with the given constant name. |
|||
* |
|||
* @param constantName The name of the constant to use. |
|||
*/ |
|||
IntegerConstantExpression(std::string const& constantName); |
|||
|
|||
/*! |
|||
* Copy-constructs from the given expression. |
|||
* |
|||
* @param integerConstantExpression The expression to copy. |
|||
*/ |
|||
IntegerConstantExpression(IntegerConstantExpression const& integerConstantExpression); |
|||
|
|||
virtual std::unique_ptr<BaseExpression> clone() const override; |
|||
|
|||
virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override; |
|||
|
|||
virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override; |
|||
|
|||
virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override; |
|||
|
|||
virtual void accept(ExpressionVisitor* visitor) override; |
|||
}; |
|||
|
|||
} // namespace expressions |
|||
} // namespace ir |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_EXPRESSIONS_INTEGERCONSTANTEXPRESSION_H_ */ |
|||
@ -1,53 +0,0 @@ |
|||
/*
|
|||
* IntegerLiteralExpression.cpp |
|||
* |
|||
* Created on: 03.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include <sstream>
|
|||
|
|||
#include "IntegerLiteralExpression.h"
|
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
IntegerLiteralExpression::IntegerLiteralExpression(int_fast64_t value) : BaseExpression(int_), value(value) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
IntegerLiteralExpression::IntegerLiteralExpression(IntegerLiteralExpression const& integerLiteralExpression) |
|||
: BaseExpression(integerLiteralExpression), value(integerLiteralExpression.value) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
std::unique_ptr<BaseExpression> IntegerLiteralExpression::clone() const { |
|||
return std::unique_ptr<BaseExpression>(new IntegerLiteralExpression(*this)); |
|||
} |
|||
|
|||
std::unique_ptr<BaseExpression> IntegerLiteralExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const { |
|||
return std::unique_ptr<BaseExpression>(new IntegerLiteralExpression(this->value)); |
|||
} |
|||
|
|||
double IntegerLiteralExpression::getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
return static_cast<double>(value); |
|||
} |
|||
|
|||
int_fast64_t IntegerLiteralExpression::getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
return value; |
|||
} |
|||
|
|||
void IntegerLiteralExpression::accept(ExpressionVisitor* visitor) { |
|||
visitor->visit(this); |
|||
} |
|||
|
|||
std::string IntegerLiteralExpression::toString() const { |
|||
std::stringstream result; |
|||
result << value; |
|||
return result.str(); |
|||
} |
|||
|
|||
} // namespace expressions
|
|||
} // namespace ir
|
|||
} // namespace storm
|
|||
@ -1,57 +0,0 @@ |
|||
/* |
|||
* IntegerLiteralExpression.h |
|||
* |
|||
* Created on: 03.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_EXPRESSIONS_INTEGERLITERALEXPRESSION_H_ |
|||
#define STORM_IR_EXPRESSIONS_INTEGERLITERALEXPRESSION_H_ |
|||
|
|||
#include "src/ir/expressions/BaseExpression.h" |
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
/*! |
|||
* A class representing an integer literal. |
|||
*/ |
|||
class IntegerLiteralExpression : public BaseExpression { |
|||
public: |
|||
/*! |
|||
* Creates an integer literal expression with the given value. |
|||
* |
|||
* @param value The value for the integer literal. |
|||
*/ |
|||
IntegerLiteralExpression(int_fast64_t value); |
|||
|
|||
/*! |
|||
* Copy-constructs from the given expression. |
|||
* |
|||
* @param integerLiteralExpression The expression to copy. |
|||
*/ |
|||
IntegerLiteralExpression(IntegerLiteralExpression const& integerLiteralExpression); |
|||
|
|||
virtual std::unique_ptr<BaseExpression> clone() const override; |
|||
|
|||
virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override; |
|||
|
|||
virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override; |
|||
|
|||
virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override; |
|||
|
|||
virtual void accept(ExpressionVisitor* visitor) override; |
|||
|
|||
virtual std::string toString() const override; |
|||
|
|||
private: |
|||
// The value of the double literal. |
|||
int_fast64_t value; |
|||
}; |
|||
|
|||
} // namespace expressions |
|||
} // namespace ir |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_EXPRESSIONS_INTEGERLITERALEXPRESSION_H_ */ |
|||
@ -1,62 +0,0 @@ |
|||
/*
|
|||
* UnaryBooleanFunctionExpression.cpp |
|||
* |
|||
* Created on: 10.06.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include <sstream>
|
|||
|
|||
#include "UnaryBooleanFunctionExpression.h"
|
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
UnaryBooleanFunctionExpression::UnaryBooleanFunctionExpression(std::unique_ptr<BaseExpression>&& child, FunctionType functionType) : UnaryExpression(bool_, std::move(child)), functionType(functionType) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
UnaryBooleanFunctionExpression::UnaryBooleanFunctionExpression(UnaryBooleanFunctionExpression const& unaryBooleanFunctionExpression) : UnaryExpression(unaryBooleanFunctionExpression), functionType(unaryBooleanFunctionExpression.functionType) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
std::unique_ptr<BaseExpression> UnaryBooleanFunctionExpression::clone() const { |
|||
return std::unique_ptr<BaseExpression>(new UnaryBooleanFunctionExpression(this->getChild()->clone(), functionType)); |
|||
} |
|||
|
|||
std::unique_ptr<BaseExpression> UnaryBooleanFunctionExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const { |
|||
return std::unique_ptr<BaseExpression>(new UnaryBooleanFunctionExpression(this->getChild()->clone(renaming, variableState), this->functionType)); |
|||
} |
|||
|
|||
UnaryBooleanFunctionExpression::FunctionType UnaryBooleanFunctionExpression::getFunctionType() const { |
|||
return functionType; |
|||
} |
|||
|
|||
bool UnaryBooleanFunctionExpression::getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
bool resultChild = this->getChild()->getValueAsBool(variableValues); |
|||
switch(functionType) { |
|||
case NOT: return !resultChild; break; |
|||
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Unknown boolean unary operator: '" << functionType << "'."; |
|||
} |
|||
} |
|||
|
|||
void UnaryBooleanFunctionExpression::accept(ExpressionVisitor* visitor) { |
|||
visitor->visit(this); |
|||
} |
|||
|
|||
std::string UnaryBooleanFunctionExpression::toString() const { |
|||
std::stringstream result; |
|||
result << "("; |
|||
switch (functionType) { |
|||
case NOT: result << "!"; break; |
|||
} |
|||
result << this->getChild()->toString() << ")"; |
|||
|
|||
return result.str(); |
|||
} |
|||
|
|||
} // namespace expressions
|
|||
} // namespace ir
|
|||
} // namespace storm
|
|||
@ -1,68 +0,0 @@ |
|||
/* |
|||
* UnaryBooleanFunctionExpression.h |
|||
* |
|||
* Created on: 03.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_EXPRESSIONS_UNARYBOOLEANFUNCTIONEXPRESSION_H_ |
|||
#define STORM_IR_EXPRESSIONS_UNARYBOOLEANFUNCTIONEXPRESSION_H_ |
|||
|
|||
#include "UnaryExpression.h" |
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
/*! |
|||
* A class representing a unary function expression of boolean type. |
|||
*/ |
|||
class UnaryBooleanFunctionExpression : public UnaryExpression { |
|||
public: |
|||
/*! |
|||
* An enum type specifying the different functions applicable. |
|||
*/ |
|||
enum FunctionType {NOT}; |
|||
|
|||
/*! |
|||
* Creates a unary boolean function expression tree node with the given child and function type. |
|||
* |
|||
* @param child The child of the node. |
|||
* @param functionType The operator that is to be applied to the two children. |
|||
*/ |
|||
UnaryBooleanFunctionExpression(std::unique_ptr<BaseExpression>&& child, FunctionType functionType); |
|||
|
|||
/*! |
|||
* Copy-constructs from the given expression. |
|||
* |
|||
* @param unaryBooleanFunctionExpression The expression to copy. |
|||
*/ |
|||
UnaryBooleanFunctionExpression(UnaryBooleanFunctionExpression const& unaryBooleanFunctionExpression); |
|||
|
|||
virtual std::unique_ptr<BaseExpression> clone() const override; |
|||
|
|||
virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override; |
|||
|
|||
/*! |
|||
* Retrieves the operator that is associated with this node. |
|||
* |
|||
* @param The operator that is associated with this node. |
|||
*/ |
|||
FunctionType getFunctionType() const; |
|||
|
|||
virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override; |
|||
|
|||
virtual void accept(ExpressionVisitor* visitor) override; |
|||
|
|||
virtual std::string toString() const override; |
|||
|
|||
private: |
|||
// The operator that is associated with this node. |
|||
FunctionType functionType; |
|||
}; |
|||
|
|||
} // namespace expressions |
|||
} // namespace ir |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_EXPRESSIONS_UNARYBOOLEANFUNCTIONEXPRESSION_H_ */ |
|||
@ -1,39 +0,0 @@ |
|||
/*
|
|||
* UnaryExpression.cpp |
|||
* |
|||
* Created on: 27.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include "UnaryExpression.h"
|
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
UnaryExpression::UnaryExpression(ReturnType type, std::unique_ptr<BaseExpression>&& child) : BaseExpression(type), child(std::move(child)) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
UnaryExpression::UnaryExpression(UnaryExpression const& unaryExpression) : BaseExpression(unaryExpression), child(unaryExpression.child->clone()) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
std::unique_ptr<BaseExpression> const& UnaryExpression::getChild() const { |
|||
return child; |
|||
} |
|||
|
|||
BaseExpression* UnaryExpression::performSubstitution(std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution) { |
|||
BaseExpression* newChild = child->performSubstitution(substitution); |
|||
|
|||
// Only update the child if it changed, because otherwise the child gets destroyed.
|
|||
if (newChild != child.get()) { |
|||
child = std::unique_ptr<BaseExpression>(newChild); |
|||
} |
|||
|
|||
return this; |
|||
} |
|||
|
|||
} // namespace expressions
|
|||
} // namespace ir
|
|||
} // namespace storm
|
|||
@ -1,55 +0,0 @@ |
|||
/* |
|||
* UnaryExpression.h |
|||
* |
|||
* Created on: 27.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_EXPRESSIONS_UNARYEXPRESSION_H_ |
|||
#define STORM_IR_EXPRESSIONS_UNARYEXPRESSION_H_ |
|||
|
|||
#include "BaseExpression.h" |
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
/*! |
|||
* A class representing a generic unary expression. |
|||
*/ |
|||
class UnaryExpression : public BaseExpression { |
|||
public: |
|||
/*! |
|||
* Constructs a unary expression with the given type and child. |
|||
* @param type The type of the unary expression. |
|||
* @param right The child of the unary expression. |
|||
*/ |
|||
UnaryExpression(ReturnType type, std::unique_ptr<BaseExpression>&& child); |
|||
|
|||
/*! |
|||
* Copy-constructs from the given expression. |
|||
* |
|||
* @param unaryExpression The expression to copy. |
|||
*/ |
|||
UnaryExpression(UnaryExpression const& unaryExpression); |
|||
|
|||
/*! |
|||
* Retrieves the child of the expression node. |
|||
* |
|||
* @return The child of the expression node. |
|||
*/ |
|||
std::unique_ptr<BaseExpression> const& getChild() const; |
|||
|
|||
protected: |
|||
virtual BaseExpression* performSubstitution(std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution) override; |
|||
|
|||
private: |
|||
// The left child of the unary expression. |
|||
std::unique_ptr<BaseExpression> child; |
|||
}; |
|||
|
|||
} // namespace expressions |
|||
} // namespace ir |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_EXPRESSIONS_UNARYEXPRESSION_H_ */ |
|||
@ -1,86 +0,0 @@ |
|||
/*
|
|||
* UnaryFunctionExpression.h |
|||
* |
|||
* Created on: 03.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include <cmath>
|
|||
|
|||
#include "UnaryNumericalFunctionExpression.h"
|
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
UnaryNumericalFunctionExpression::UnaryNumericalFunctionExpression(ReturnType type, std::unique_ptr<BaseExpression>&& child, FunctionType functionType) : UnaryExpression(type, std::move(child)), functionType(functionType) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
UnaryNumericalFunctionExpression::UnaryNumericalFunctionExpression(UnaryNumericalFunctionExpression const& unaryNumericalFunctionExpression) : UnaryExpression(unaryNumericalFunctionExpression), functionType(unaryNumericalFunctionExpression.functionType) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
std::unique_ptr<BaseExpression> UnaryNumericalFunctionExpression::clone() const { |
|||
return std::unique_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(this->getType(), this->getChild()->clone(), functionType)); |
|||
} |
|||
|
|||
std::unique_ptr<BaseExpression> UnaryNumericalFunctionExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const { |
|||
return std::unique_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(this->getType(), this->getChild()->clone(renaming, variableState), this->functionType)); |
|||
} |
|||
|
|||
int_fast64_t UnaryNumericalFunctionExpression::getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
if (this->getType() != int_) { |
|||
BaseExpression::getValueAsInt(variableValues); |
|||
} |
|||
|
|||
int_fast64_t resultChild = this->getChild()->getValueAsInt(variableValues); |
|||
switch(functionType) { |
|||
case MINUS: return -resultChild; break; |
|||
case FLOOR: return static_cast<int_fast64_t>(std::floor(resultChild)); break; |
|||
case CEIL: return static_cast<int_fast64_t>(std::ceil(resultChild)); break; |
|||
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Unknown numerical unary operator: '" << functionType << "'."; |
|||
} |
|||
} |
|||
|
|||
double UnaryNumericalFunctionExpression::getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
if (this->getType() != double_ && this->getType() != int_) { |
|||
BaseExpression::getValueAsDouble(variableValues); |
|||
} |
|||
|
|||
double resultChild = this->getChild()->getValueAsDouble(variableValues); |
|||
switch(functionType) { |
|||
case MINUS: return -resultChild; break; |
|||
case FLOOR: return std::floor(resultChild); break; |
|||
case CEIL: return std::ceil(resultChild); break; |
|||
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Unknown numerical unary operator: '" << functionType << "'."; |
|||
} |
|||
} |
|||
|
|||
UnaryNumericalFunctionExpression::FunctionType UnaryNumericalFunctionExpression::getFunctionType() const { |
|||
return functionType; |
|||
} |
|||
|
|||
void UnaryNumericalFunctionExpression::accept(ExpressionVisitor* visitor) { |
|||
visitor->visit(this); |
|||
} |
|||
|
|||
std::string UnaryNumericalFunctionExpression::toString() const { |
|||
std::stringstream result; |
|||
result << "("; |
|||
switch (functionType) { |
|||
case MINUS: result << "-"; break; |
|||
case FLOOR: result << "floor("; break; |
|||
case CEIL: result << "ceil("; break; |
|||
} |
|||
result << this->getChild()->toString() << ")"; |
|||
|
|||
return result.str(); |
|||
} |
|||
|
|||
} // namespace expressions
|
|||
} // namespace ir
|
|||
} // namespace storm
|
|||
|
|||
@ -1,70 +0,0 @@ |
|||
/* |
|||
* UnaryFunctionExpression.h |
|||
* |
|||
* Created on: 03.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_EXPRESSIONS_UNARYFUNCTIONEXPRESSION_H_ |
|||
#define STORM_IR_EXPRESSIONS_UNARYFUNCTIONEXPRESSION_H_ |
|||
|
|||
#include "UnaryExpression.h" |
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
/*! |
|||
* A class representing a unary function expression of numerical type. |
|||
*/ |
|||
class UnaryNumericalFunctionExpression : public UnaryExpression { |
|||
public: |
|||
/*! |
|||
* An enum type specifying the different functions applicable. |
|||
*/ |
|||
enum FunctionType {MINUS, FLOOR, CEIL}; |
|||
|
|||
/*! |
|||
* Creates a unary numerical function expression tree node with the given child and function type. |
|||
* |
|||
* @param child The child of the node. |
|||
* @param functionType The operator that is to be applied to the two children. |
|||
*/ |
|||
UnaryNumericalFunctionExpression(ReturnType type, std::unique_ptr<BaseExpression>&& child, FunctionType functionType); |
|||
|
|||
/*! |
|||
* Copy-constructs from the given expression. |
|||
* |
|||
* @param unaryNumericalFunctionExpression The expression to copy. |
|||
*/ |
|||
UnaryNumericalFunctionExpression(UnaryNumericalFunctionExpression const& unaryNumericalFunctionExpression); |
|||
|
|||
virtual std::unique_ptr<BaseExpression> clone() const override; |
|||
|
|||
virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override; |
|||
|
|||
virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override; |
|||
|
|||
virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override; |
|||
|
|||
/*! |
|||
* Retrieves the operator that is associated with this node. |
|||
* |
|||
* @param The operator that is associated with this node. |
|||
*/ |
|||
FunctionType getFunctionType() const; |
|||
|
|||
virtual void accept(ExpressionVisitor* visitor) override; |
|||
|
|||
virtual std::string toString() const override; |
|||
|
|||
private: |
|||
// The operator that is associated with this node. |
|||
FunctionType functionType; |
|||
}; |
|||
|
|||
} // namespace expressions |
|||
} // namespace ir |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_EXPRESSIONS_UNARYFUNCTIONEXPRESSION_H_ */ |
|||
@ -1,120 +0,0 @@ |
|||
/*
|
|||
* VariableExpression.cpp |
|||
* |
|||
* Created on: 10.06.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include "VariableExpression.h"
|
|||
#include "src/parser/prismparser/VariableState.h"
|
|||
#include "src/exceptions/ExpressionEvaluationException.h"
|
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
VariableExpression::VariableExpression(ReturnType type, std::string const& variableName) : BaseExpression(type), globalIndex(0), variableName(variableName) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
VariableExpression::VariableExpression(ReturnType type, uint_fast64_t globalIndex, std::string const& variableName) |
|||
: BaseExpression(type), globalIndex(globalIndex), variableName(variableName) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
VariableExpression::VariableExpression(VariableExpression const& variableExpression) : BaseExpression(variableExpression), globalIndex(variableExpression.globalIndex), variableName(variableExpression.variableName) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
std::unique_ptr<BaseExpression> VariableExpression::clone() const { |
|||
return std::unique_ptr<BaseExpression>(new VariableExpression(*this)); |
|||
} |
|||
|
|||
std::unique_ptr<BaseExpression> VariableExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const { |
|||
// Perform the proper cloning.
|
|||
auto renamingPair = renaming.find(this->variableName); |
|||
if (renamingPair != renaming.end()) { |
|||
if (this->getType() == int_) { |
|||
return variableState.getIntegerVariableExpression(renamingPair->second)->clone(); |
|||
} else { |
|||
return variableState.getBooleanVariableExpression(renamingPair->second)->clone(); |
|||
} |
|||
} else { |
|||
if (this->getType() == int_) { |
|||
return variableState.getIntegerVariableExpression(this->variableName)->clone(); |
|||
} else { |
|||
return variableState.getBooleanVariableExpression(this->variableName)->clone(); |
|||
} |
|||
} |
|||
} |
|||
|
|||
BaseExpression* VariableExpression::performSubstitution(std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution) { |
|||
// If the name of the variable is a key of the map, we need to replace it.
|
|||
auto substitutionIterator = substitution.find(variableName); |
|||
|
|||
if (substitutionIterator != substitution.end()) { |
|||
std::unique_ptr<BaseExpression> expressionClone = substitutionIterator->second.get().clone(); |
|||
BaseExpression* rawPointer = expressionClone.release(); |
|||
return rawPointer; |
|||
} else { |
|||
// Otherwise, we don't need to replace anything.
|
|||
return this; |
|||
} |
|||
} |
|||
|
|||
void VariableExpression::accept(ExpressionVisitor* visitor) { |
|||
visitor->visit(this); |
|||
} |
|||
|
|||
std::string VariableExpression::toString() const { |
|||
return this->variableName; |
|||
} |
|||
|
|||
int_fast64_t VariableExpression::getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
if (this->getType() != int_) { |
|||
BaseExpression::getValueAsInt(variableValues); |
|||
} |
|||
|
|||
if (variableValues != nullptr) { |
|||
return variableValues->second[globalIndex]; |
|||
} else { |
|||
throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression involving variables without variable values."; |
|||
} |
|||
} |
|||
|
|||
bool VariableExpression::getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
if (this->getType() != bool_) { |
|||
BaseExpression::getValueAsBool(variableValues); |
|||
} |
|||
|
|||
if (variableValues != nullptr) { |
|||
return variableValues->first[globalIndex]; |
|||
} else { |
|||
throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression involving variables without variable values."; |
|||
} |
|||
} |
|||
|
|||
double VariableExpression::getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
if (this->getType() != double_ && this->getType() != int_) { |
|||
BaseExpression::getValueAsDouble(variableValues); |
|||
} |
|||
|
|||
// Because only int variables can deliver a double value, we only need to check them.
|
|||
if (variableValues != nullptr) { |
|||
return static_cast<double>(variableValues->second[globalIndex]); |
|||
} else { |
|||
throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression with variable '" << variableName << "' of type double."; |
|||
} |
|||
} |
|||
|
|||
std::string const& VariableExpression::getVariableName() const { |
|||
return variableName; |
|||
} |
|||
|
|||
uint_fast64_t VariableExpression::getGlobalVariableIndex() const { |
|||
return this->globalIndex; |
|||
} |
|||
|
|||
} // namespace expressions
|
|||
} // namespace ir
|
|||
} // namespace storm
|
|||
@ -1,98 +0,0 @@ |
|||
/* |
|||
* VariableExpression.h |
|||
* |
|||
* Created on: 03.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_EXPRESSIONS_VARIABLEEXPRESSION_H_ |
|||
#define STORM_IR_EXPRESSIONS_VARIABLEEXPRESSION_H_ |
|||
|
|||
#include "BaseExpression.h" |
|||
|
|||
namespace storm { |
|||
|
|||
// Forward-declare VariableState. |
|||
namespace parser { |
|||
namespace prismparser { |
|||
class VariableState; |
|||
} // namespace prismparser |
|||
} // namespace parser |
|||
|
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
/*! |
|||
* A class representing a variable in the expression tree. |
|||
*/ |
|||
class VariableExpression : public BaseExpression { |
|||
public: |
|||
/*! |
|||
* Creates a variable expression of the given type with the given name. As this variable has no indices |
|||
* it is only meant as a dummy and needs to be replaced with a "full" variable expression. |
|||
* |
|||
* @param type The type of the variable. |
|||
* @param variableName The name of the variable. |
|||
*/ |
|||
VariableExpression(ReturnType type, std::string const& variableName); |
|||
|
|||
/*! |
|||
* Creates a variable expression of the given type with the given name and indices. |
|||
* |
|||
* @param type The type of the variable. |
|||
* @param globalIndex The global (i.e. program-wide) index of the variable. |
|||
* @param variableName The name of the variable. |
|||
*/ |
|||
VariableExpression(ReturnType type, uint_fast64_t globalIndex, std::string const& variableName); |
|||
|
|||
/*! |
|||
* Copy-constructs from the given expression. |
|||
* |
|||
* @param variableExpression The expression to copy. |
|||
*/ |
|||
VariableExpression(VariableExpression const& variableExpression); |
|||
|
|||
virtual std::unique_ptr<BaseExpression> clone() const override; |
|||
|
|||
virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override; |
|||
|
|||
virtual void accept(ExpressionVisitor* visitor) override; |
|||
|
|||
virtual std::string toString() const override; |
|||
|
|||
virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override; |
|||
|
|||
virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override; |
|||
|
|||
virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override; |
|||
|
|||
/*! |
|||
* Retrieves the name of the variable. |
|||
* |
|||
* @return The name of the variable. |
|||
*/ |
|||
std::string const& getVariableName() const; |
|||
|
|||
/*! |
|||
* Retrieves the global (i.e. program-wide) index of the variable. |
|||
* |
|||
* @return The global index of the variable. |
|||
*/ |
|||
uint_fast64_t getGlobalVariableIndex() const; |
|||
|
|||
protected: |
|||
virtual BaseExpression* performSubstitution(std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution) override; |
|||
|
|||
private: |
|||
// The global index of the variable. |
|||
uint_fast64_t globalIndex; |
|||
|
|||
// The name of the variable. |
|||
std::string variableName; |
|||
}; |
|||
|
|||
} // namespace expressions |
|||
} // namespace ir |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_EXPRESSIONS_VARIABLEEXPRESSION_H_ */ |
|||
@ -1,23 +1,33 @@ |
|||
#ifndef STORM_PARSER_LABPARSER_H_ |
|||
#define STORM_PARSER_LABPARSER_H_ |
|||
#ifndef STORM_PARSER_ATOMICPROPOSITIONLABELINGPARSER_H_ |
|||
#define STORM_PARSER_ATOMICPROPOSITIONLABELINGPARSER_H_ |
|||
|
|||
#include "src/models/AtomicPropositionsLabeling.h" |
|||
#include <cstdint> |
|||
|
|||
#include "src/parser/Parser.h" |
|||
namespace storm { |
|||
namespace parser { |
|||
|
|||
#include <memory> |
|||
/*! |
|||
* This class can be used to parse a labeling file. |
|||
* |
|||
* Since the labeling is state based, the same label parser can be used for all models. |
|||
*/ |
|||
class AtomicPropositionLabelingParser { |
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
public: |
|||
|
|||
/*! |
|||
* Reads a label file and puts the result in an AtomicPropositionsLabeling object. |
|||
* |
|||
* @param stateCount The number of states of the model to be labeled. |
|||
* @param filename The path and name of the labeling (.lab) file. |
|||
* @return The parsed labeling as an AtomicPropositionsLabeling object. |
|||
*/ |
|||
static storm::models::AtomicPropositionsLabeling parseAtomicPropositionLabeling(uint_fast64_t stateCount, std::string const &filename); |
|||
|
|||
/*! |
|||
* @brief Load label file and return initialized AtomicPropositionsLabeling object. |
|||
* |
|||
*/ |
|||
storm::models::AtomicPropositionsLabeling AtomicPropositionLabelingParser(uint_fast64_t node_count, std::string const &filename); |
|||
}; |
|||
|
|||
} // namespace parser |
|||
} // namespace parser |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_PARSER_LABPARSER_H_ */ |
|||
#endif /* STORM_PARSER_ATOMICPROPOSITIONLABELINGPARSER_H_ */ |
|||
@ -0,0 +1,101 @@ |
|||
/*
|
|||
* AutoParser.cpp |
|||
* |
|||
* Created on: Jan 20, 2014 |
|||
* Author: Manuel S. Weiand |
|||
*/ |
|||
|
|||
#include "src/parser/AutoParser.h"
|
|||
|
|||
#include "src/parser/MappedFile.h"
|
|||
|
|||
#include "src/parser/DeterministicModelParser.h"
|
|||
#include "src/parser/NondeterministicModelParser.h"
|
|||
#include "src/parser/MarkovAutomatonParser.h"
|
|||
#include "src/exceptions/WrongFormatException.h"
|
|||
|
|||
#include "src/utility/cstring.h"
|
|||
#include "src/utility/OsDetection.h"
|
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
|
|||
using namespace storm::utility::cstring; |
|||
|
|||
std::shared_ptr<storm::models::AbstractModel<double>> AutoParser::parseModel(std::string const & transitionsFilename, |
|||
std::string const & labelingFilename, |
|||
std::string const & stateRewardFilename, |
|||
std::string const & transitionRewardFilename) { |
|||
|
|||
// Find and parse the model type hint.
|
|||
storm::models::ModelType type = AutoParser::analyzeHint(transitionsFilename); |
|||
|
|||
// In case the hint string is unknown or could not be found, throw an exception.
|
|||
if (type == storm::models::Unknown) { |
|||
LOG4CPLUS_ERROR(logger, "Could not determine file type of " << transitionsFilename << "."); |
|||
LOG4CPLUS_ERROR(logger, "The first line of the file should contain a format hint. Please fix your file and try again."); |
|||
throw storm::exceptions::WrongFormatException() << "Could not determine type of file " << transitionsFilename; |
|||
} else { |
|||
LOG4CPLUS_INFO(logger, "Model type seems to be " << type); |
|||
} |
|||
|
|||
// Do the actual parsing.
|
|||
std::shared_ptr<storm::models::AbstractModel<double>> model; |
|||
switch (type) { |
|||
case storm::models::DTMC: { |
|||
model.reset(new storm::models::Dtmc<double>(std::move(DeterministicModelParser::parseDtmc(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename)))); |
|||
break; |
|||
} |
|||
case storm::models::CTMC: { |
|||
model.reset(new storm::models::Ctmc<double>(std::move(DeterministicModelParser::parseCtmc(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename)))); |
|||
break; |
|||
} |
|||
case storm::models::MDP: { |
|||
model.reset(new storm::models::Mdp<double>(std::move(NondeterministicModelParser::parseMdp(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename)))); |
|||
break; |
|||
} |
|||
case storm::models::CTMDP: { |
|||
model.reset(new storm::models::Ctmdp<double>(std::move(NondeterministicModelParser::parseCtmdp(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename)))); |
|||
break; |
|||
} |
|||
case storm::models::MA: { |
|||
model.reset(new storm::models::MarkovAutomaton<double>(storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename))); |
|||
break; |
|||
} |
|||
default: |
|||
LOG4CPLUS_WARN(logger, "Unknown/Unhandled Model Type which cannot be parsed."); // Unknown
|
|||
} |
|||
|
|||
return model; |
|||
} |
|||
|
|||
storm::models::ModelType AutoParser::analyzeHint(std::string const & filename) { |
|||
storm::models::ModelType hintType = storm::models::Unknown; |
|||
|
|||
// Open the file.
|
|||
MappedFile file(filename.c_str()); |
|||
char* buf = file.getData(); |
|||
|
|||
// Find and read in the hint.
|
|||
char hint[65]; |
|||
// %60s => The input hint can be AT MOST 60 chars long.
|
|||
#ifdef WINDOWS
|
|||
sscanf_s(buf, "%60s", hint, sizeof(hint)); |
|||
#else
|
|||
sscanf(buf, "%60s", hint); |
|||
#endif
|
|||
|
|||
for (char* c = hint; *c != '\0'; c++) *c = toupper(*c); |
|||
|
|||
// Check if the hint value is known and store the appropriate enum value.
|
|||
if (strncmp(hint, "DTMC", sizeof(hint)) == 0) hintType = storm::models::DTMC; |
|||
else if (strncmp(hint, "CTMC", sizeof(hint)) == 0) hintType = storm::models::CTMC; |
|||
else if (strncmp(hint, "MDP", sizeof(hint)) == 0) hintType = storm::models::MDP; |
|||
else if (strncmp(hint, "CTMDP", sizeof(hint)) == 0) hintType = storm::models::CTMDP; |
|||
else if (strncmp(hint, "MA", sizeof(hint)) == 0) hintType = storm::models::MA; |
|||
|
|||
return hintType; |
|||
} |
|||
|
|||
} // namespace parser
|
|||
} // namespace storm
|
|||
@ -1,140 +1,63 @@ |
|||
#ifndef STORM_PARSER_AUTOPARSER_H_ |
|||
#define STORM_PARSER_AUTOPARSER_H_ |
|||
|
|||
#include "src/parser/Parser.h" |
|||
#include "src/models/AbstractModel.h" |
|||
|
|||
#include "src/exceptions/WrongFormatException.h" |
|||
#include "src/models/AbstractModel.h" |
|||
#include "src/parser/DeterministicModelParser.h" |
|||
#include "src/parser/NondeterministicModelParser.h" |
|||
#include "src/parser/MarkovAutomatonParser.h" |
|||
|
|||
#include <memory> |
|||
#include <iostream> |
|||
#include <utility> |
|||
#include <string> |
|||
#include <cctype> |
|||
|
|||
namespace storm { |
|||
|
|||
namespace parser { |
|||
|
|||
/*! |
|||
* @brief Checks the given files and parses the model within these files. |
|||
* |
|||
* This parser analyzes the format hint in the first line of the transition |
|||
* file. If this is a valid format, it will use the parser for this format, |
|||
* otherwise it will throw an exception. |
|||
* |
|||
* When the files are parsed successfully, the parsed ModelType and Model |
|||
* can be obtained via getType() and getModel<ModelClass>(). |
|||
*/ |
|||
template<class T> |
|||
class AutoParser { |
|||
public: |
|||
AutoParser(std::string const & transitionSystemFile, std::string const & labelingFile, |
|||
std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "") : model(nullptr) { |
|||
storm::models::ModelType type = this->analyzeHint(transitionSystemFile); |
|||
|
|||
if (type == storm::models::Unknown) { |
|||
LOG4CPLUS_ERROR(logger, "Could not determine file type of " << transitionSystemFile << "."); |
|||
LOG4CPLUS_ERROR(logger, "The first line of the file should contain a format hint. Please fix your file and try again."); |
|||
throw storm::exceptions::WrongFormatException() << "Could not determine type of file " << transitionSystemFile; |
|||
} else { |
|||
LOG4CPLUS_INFO(logger, "Model type seems to be " << type); |
|||
} |
|||
|
|||
// Do actual parsing |
|||
switch (type) { |
|||
case storm::models::DTMC: { |
|||
this->model.reset(new storm::models::Dtmc<double>(std::move(DeterministicModelParserAsDtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); |
|||
break; |
|||
} |
|||
case storm::models::CTMC: { |
|||
this->model.reset(new storm::models::Ctmc<double>(std::move(DeterministicModelParserAsCtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); |
|||
break; |
|||
} |
|||
case storm::models::MDP: { |
|||
this->model.reset(new storm::models::Mdp<double>(std::move(NondeterministicModelParserAsMdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); |
|||
break; |
|||
} |
|||
case storm::models::CTMDP: { |
|||
this->model.reset(new storm::models::Ctmdp<double>(std::move(NondeterministicModelParserAsCtmdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); |
|||
break; |
|||
} |
|||
case storm::models::MA: { |
|||
this->model.reset(new storm::models::MarkovAutomaton<double>(storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))); |
|||
break; |
|||
} |
|||
default: ; // Unknown |
|||
} |
|||
|
|||
|
|||
if (!this->model) { |
|||
LOG4CPLUS_WARN(logger, "Unknown/Unhandled Model Type. Model is still null."); |
|||
} |
|||
} |
|||
|
|||
/*! |
|||
* @brief Returns the type of model that was parsed. |
|||
*/ |
|||
storm::models::ModelType getType() { |
|||
if (this->model) { |
|||
return this->model->getType(); |
|||
} else { |
|||
return storm::models::Unknown; |
|||
} |
|||
} |
|||
|
|||
/*! |
|||
* @brief Returns the model with the given type. |
|||
*/ |
|||
template <typename Model> |
|||
std::shared_ptr<Model> getModel() { |
|||
return this->model->template as<Model>(); |
|||
} |
|||
/*! |
|||
* Contains all file parsers and helper classes. |
|||
* |
|||
* This namespace contains everything needed to load data files (like |
|||
* atomic propositions, transition systems, formulas, etc.) including |
|||
* methods for efficient file access (see MappedFile). |
|||
*/ |
|||
namespace parser { |
|||
|
|||
private: |
|||
|
|||
/*! |
|||
* @brief Open file and read file format hint. |
|||
* This class automatically chooses the correct parser for the given files and returns the corresponding model. |
|||
* The choice of the parser is made using the model hint at the beginning of the given transition file. |
|||
*/ |
|||
storm::models::ModelType analyzeHint(const std::string& filename) { |
|||
storm::models::ModelType hintType = storm::models::Unknown; |
|||
|
|||
// Parse the File and check for the Line Endings |
|||
storm::parser::SupportedLineEndingsEnum lineEndings = storm::parser::findUsedLineEndings(filename); |
|||
|
|||
// Open file |
|||
MappedFile file(filename.c_str()); |
|||
char* buf = file.data; |
|||
|
|||
// parse hint |
|||
char hint[128]; |
|||
// %20s => The Input Hint can be AT MOST 120 chars long |
|||
storm::parser::scanForModelHint(hint, sizeof(hint), buf, lineEndings); |
|||
|
|||
for (char* c = hint; *c != '\0'; c++) *c = toupper(*c); |
|||
|
|||
// check hint |
|||
if (strncmp(hint, "DTMC", sizeof(hint)) == 0) hintType = storm::models::DTMC; |
|||
else if (strncmp(hint, "CTMC", sizeof(hint)) == 0) hintType = storm::models::CTMC; |
|||
else if (strncmp(hint, "MDP", sizeof(hint)) == 0) hintType = storm::models::MDP; |
|||
else if (strncmp(hint, "CTMDP", sizeof(hint)) == 0) hintType = storm::models::CTMDP; |
|||
else if (strncmp(hint, "MA", sizeof(hint)) == 0) hintType = storm::models::MA; |
|||
|
|||
return hintType; |
|||
} |
|||
class AutoParser { |
|||
public: |
|||
|
|||
/*! |
|||
* Checks the given files and parses the model within these files. |
|||
* |
|||
* This parser analyzes the format hint in the first line of the transition file. |
|||
* If this is a valid format, it will use the parser for this format, otherwise it will throw an exception. |
|||
* |
|||
* When the files are parsed successfully, a shared pointer owning the resulting model is returned. |
|||
* The concrete model can be obtained using the as<Type>() member of the AbstractModel class. |
|||
* |
|||
* @note The number of states of the model is determined by the transitions file. |
|||
* The labeling file may therefore not contain labels of states that are not contained in the transitions file. |
|||
* |
|||
* @param transitionsFilename The path and name of the file containing the transitions of the model. |
|||
* @param labelingFilename The path and name of the file containing the labels for the states of the model. |
|||
* @param stateRewardFilename The path and name of the file that contains the state reward of the model. This file is optional. |
|||
* @param transitionRewardFilename The path and name of the file that contains the transition rewards of the model. This file is optional. |
|||
* @return A shared_ptr containing the resulting model. |
|||
*/ |
|||
static std::shared_ptr<storm::models::AbstractModel<double>> parseModel(std::string const & transitionsFilename, |
|||
std::string const & labelingFilename, |
|||
std::string const & stateRewardFilename = "", |
|||
std::string const & transitionRewardFilename = ""); |
|||
|
|||
private: |
|||
|
|||
/*! |
|||
* Opens the given file and parses the file format hint. |
|||
* |
|||
* @param filename The path and name of the file that is to be analysed. |
|||
* @return The type of the model as an enum value. |
|||
*/ |
|||
static storm::models::ModelType analyzeHint(std::string const & filename); |
|||
}; |
|||
|
|||
/*! |
|||
* @brief Pointer to a parser that has parsed the given transition system. |
|||
*/ |
|||
std::shared_ptr<storm::models::AbstractModel<T>> model; |
|||
}; |
|||
|
|||
} // namespace parser |
|||
|
|||
} // namespace parser |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_PARSER_AUTOPARSER_H_ */ |
|||
@ -1,23 +1,90 @@ |
|||
#ifndef STORM_PARSER_TRAPARSER_H_ |
|||
#define STORM_PARSER_TRAPARSER_H_ |
|||
#ifndef STORM_PARSER_DETERMINISTICSPARSETRANSITIONPARSER_H_ |
|||
#define STORM_PARSER_DETERMINISTICSPARSETRANSITIONPARSER_H_ |
|||
|
|||
#include "src/storage/SparseMatrix.h" |
|||
|
|||
#include "src/parser/Parser.h" |
|||
#include "src/utility/OsDetection.h" |
|||
namespace storm { |
|||
namespace parser { |
|||
|
|||
#include <memory> |
|||
/*! |
|||
* This class can be used to parse a file containing either transitions or transition rewards of a deterministic model. |
|||
* |
|||
* The file is parsed in two passes. |
|||
* The first pass tests the file format and collects statistical data needed for the second pass. |
|||
* The second pass then parses the file data and constructs a SparseMatrix representing it. |
|||
*/ |
|||
class DeterministicSparseTransitionParser { |
|||
public: |
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
|
|||
/*! |
|||
* @brief Load a deterministic transition system from file and create a |
|||
* sparse adjacency matrix whose entries represent the weights of the edges |
|||
*/ |
|||
storm::storage::SparseMatrix<double> DeterministicSparseTransitionParser(std::string const& filename, bool insertDiagonalEntriesIfMissing = true, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr); |
|||
|
|||
} // namespace parser |
|||
/*! |
|||
* A structure representing the result of the first pass of this parser. It contains the number of non-zero entries in the model and the highest state index. |
|||
*/ |
|||
struct FirstPassResult { |
|||
|
|||
/*! |
|||
* The default constructor. |
|||
* Constructs an empty FirstPassResult. |
|||
*/ |
|||
FirstPassResult() : numberOfNonzeroEntries(0), highestStateIndex(0) { |
|||
// Intentionally left empty. |
|||
} |
|||
|
|||
//! The total number of non-zero entries of the model. |
|||
uint_fast64_t numberOfNonzeroEntries; |
|||
|
|||
//! The highest state index that appears in the model. |
|||
uint_fast64_t highestStateIndex; |
|||
}; |
|||
|
|||
/*! |
|||
* Load a deterministic transition system from file and create a |
|||
* sparse adjacency matrix whose entries represent the weights of the edges. |
|||
* |
|||
* @param filename The path and name of the file to be parsed. |
|||
* @param insertDiagonalEntriesIfMissing A flag set iff entries on the primary diagonal of the matrix should be added in case they are missing in the parsed file. |
|||
* @return A SparseMatrix containing the parsed transition system. |
|||
*/ |
|||
static storm::storage::SparseMatrix<double> parseDeterministicTransitions(std::string const& filename); |
|||
|
|||
/*! |
|||
* Load the transition rewards for a deterministic transition system from file and create a |
|||
* sparse adjacency matrix whose entries represent the rewards of the respective transitions. |
|||
* |
|||
* @param filename The path and name of the file to be parsed. |
|||
* @param transitionMatrix The transition matrix of the model in which the reward matrix is to be used in. |
|||
* The dimensions (rows and columns) of the two matrices should match. |
|||
* @return A SparseMatrix containing the parsed transition rewards. |
|||
*/ |
|||
static storm::storage::SparseMatrix<double> parseDeterministicTransitionRewards(std::string const& filename, storm::storage::SparseMatrix<double> const & transitionMatrix); |
|||
|
|||
private: |
|||
|
|||
/* |
|||
* Performs the first pass on the input pointed to by the given buffer to obtain the number of |
|||
* transitions and the maximum node id. |
|||
* |
|||
* @param buffer The buffer that contains the input. |
|||
* @param insertDiagonalEntriesIfMissing A flag set iff entries on the primary diagonal of the matrix should be added in case they are missing in the parsed file. |
|||
* @return A structure representing the result of the first pass. |
|||
*/ |
|||
static FirstPassResult firstPass(char* buffer, bool insertDiagonalEntriesIfMissing = true); |
|||
|
|||
/* |
|||
* The main parsing routine. |
|||
* Opens the given file, calls the first pass and performs the second pass, parsing the content of the file into a SparseMatrix. |
|||
* |
|||
* @param filename The path and name of the file to be parsed. |
|||
* @param rewardFile A flag set iff the file to be parsed contains transition rewards. |
|||
* @param insertDiagonalEntriesIfMissing A flag set iff entries on the primary diagonal of the matrix should be added in case they are missing in the parsed file. |
|||
* @param transitionMatrix The transition matrix of the model in which the reward matrix is to be used in. |
|||
* The dimensions (rows and columns) of the two matrices should match. |
|||
* @return A SparseMatrix containing the parsed file contents. |
|||
*/ |
|||
static storm::storage::SparseMatrix<double> parse(std::string const& filename, bool isRewardFile, storm::storage::SparseMatrix<double> const & transitionMatrix); |
|||
|
|||
}; |
|||
|
|||
} // namespace parser |
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_PARSER_TRAPARSER_H_ */ |
|||
#endif /* STORM_PARSER_DETERMINISTICSPARSETRANSITIONPARSER_H_ */ |
|||
@ -0,0 +1,400 @@ |
|||
#include "src/parser/ExpressionParser.h"
|
|||
#include "src/exceptions/InvalidArgumentException.h"
|
|||
#include "src/exceptions/InvalidTypeException.h"
|
|||
#include "src/exceptions/WrongFormatException.h"
|
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
ExpressionParser::ExpressionParser(qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_) : ExpressionParser::base_type(expression), createExpressions(false), acceptDoubleLiterals(true), identifiers_(nullptr), invalidIdentifiers_(invalidIdentifiers_) { |
|||
identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][qi::_pass = phoenix::bind(&ExpressionParser::isValidIdentifier, phoenix::ref(*this), qi::_1)]; |
|||
identifier.name("identifier"); |
|||
|
|||
floorCeilExpression = ((qi::lit("floor")[qi::_a = true] | qi::lit("ceil")[qi::_a = false]) >> qi::lit("(") >> plusExpression >> qi::lit(")"))[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&ExpressionParser::createFloorExpression, phoenix::ref(*this), qi::_1)] .else_ [qi::_val = phoenix::bind(&ExpressionParser::createCeilExpression, phoenix::ref(*this), qi::_1)]]; |
|||
floorCeilExpression.name("floor/ceil expression"); |
|||
|
|||
minMaxExpression = ((qi::lit("min")[qi::_a = true] | qi::lit("max")[qi::_a = false]) >> qi::lit("(") >> plusExpression >> qi::lit(",") >> plusExpression >> qi::lit(")"))[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&ExpressionParser::createMinimumExpression, phoenix::ref(*this), qi::_1, qi::_2)] .else_ [qi::_val = phoenix::bind(&ExpressionParser::createMaximumExpression, phoenix::ref(*this), qi::_1, qi::_2)]]; |
|||
minMaxExpression.name("min/max expression"); |
|||
|
|||
identifierExpression = identifier[qi::_val = phoenix::bind(&ExpressionParser::getIdentifierExpression, phoenix::ref(*this), qi::_1)]; |
|||
identifierExpression.name("identifier expression"); |
|||
|
|||
literalExpression = qi::lit("true")[qi::_val = phoenix::bind(&ExpressionParser::createTrueExpression, phoenix::ref(*this))] | qi::lit("false")[qi::_val = phoenix::bind(&ExpressionParser::createFalseExpression, phoenix::ref(*this))] | strict_double[qi::_val = phoenix::bind(&ExpressionParser::createDoubleLiteralExpression, phoenix::ref(*this), qi::_1, qi::_pass)] | qi::int_[qi::_val = phoenix::bind(&ExpressionParser::createIntegerLiteralExpression, phoenix::ref(*this), qi::_1)]; |
|||
literalExpression.name("literal expression"); |
|||
|
|||
atomicExpression = minMaxExpression | floorCeilExpression | qi::lit("(") >> expression >> qi::lit(")") | literalExpression | identifierExpression; |
|||
atomicExpression.name("atomic expression"); |
|||
|
|||
unaryExpression = atomicExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicExpression)[qi::_val = phoenix::bind(&ExpressionParser::createNotExpression, phoenix::ref(*this), qi::_1)] | (qi::lit("-") >> atomicExpression)[qi::_val = phoenix::bind(&ExpressionParser::createMinusExpression, phoenix::ref(*this), qi::_1)]; |
|||
unaryExpression.name("unary expression"); |
|||
|
|||
powerExpression = unaryExpression[qi::_val = qi::_1] >> -(qi::lit("^") > expression)[qi::_val = phoenix::bind(&ExpressionParser::createPowerExpression, phoenix::ref(*this), qi::_val, qi::_1)]; |
|||
powerExpression.name("power expression"); |
|||
|
|||
multiplicationExpression = powerExpression[qi::_val = qi::_1] >> *((qi::lit("*")[qi::_a = true] | qi::lit("/")[qi::_a = false]) >> powerExpression[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&ExpressionParser::createMultExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [qi::_val = phoenix::bind(&ExpressionParser::createDivExpression, phoenix::ref(*this), qi::_val, qi::_1)]]); |
|||
multiplicationExpression.name("multiplication expression"); |
|||
|
|||
plusExpression = multiplicationExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> multiplicationExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&ExpressionParser::createPlusExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [qi::_val = phoenix::bind(&ExpressionParser::createMinusExpression, phoenix::ref(*this), qi::_val, qi::_1)]]; |
|||
plusExpression.name("plus expression"); |
|||
|
|||
relativeExpression = (plusExpression >> qi::lit(">=") >> plusExpression)[qi::_val = phoenix::bind(&ExpressionParser::createGreaterOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit(">") >> plusExpression)[qi::_val = phoenix::bind(&ExpressionParser::createGreaterExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<=") >> plusExpression)[qi::_val = phoenix::bind(&ExpressionParser::createLessOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<") >> plusExpression)[qi::_val = phoenix::bind(&ExpressionParser::createLessExpression, phoenix::ref(*this), qi::_1, qi::_2)] | plusExpression[qi::_val = qi::_1]; |
|||
relativeExpression.name("relative expression"); |
|||
|
|||
equalityExpression = relativeExpression[qi::_val = qi::_1] >> *((qi::lit("=")[qi::_a = true] | qi::lit("!=")[qi::_a = false]) >> relativeExpression)[phoenix::if_(qi::_a) [ qi::_val = phoenix::bind(&ExpressionParser::createEqualsExpression, phoenix::ref(*this), qi::_val, qi::_1) ] .else_ [ qi::_val = phoenix::bind(&ExpressionParser::createNotEqualsExpression, phoenix::ref(*this), qi::_val, qi::_1) ] ]; |
|||
equalityExpression.name("equality expression"); |
|||
|
|||
andExpression = equalityExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> equalityExpression)[qi::_val = phoenix::bind(&ExpressionParser::createAndExpression, phoenix::ref(*this), qi::_val, qi::_1)]; |
|||
andExpression.name("and expression"); |
|||
|
|||
orExpression = andExpression[qi::_val = qi::_1] >> *((qi::lit("|")[qi::_a = true] | qi::lit("=>")[qi::_a = false]) >> andExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&ExpressionParser::createOrExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [qi::_val = phoenix::bind(&ExpressionParser::createImpliesExpression, phoenix::ref(*this), qi::_val, qi::_1)] ]; |
|||
orExpression.name("or expression"); |
|||
|
|||
iteExpression = orExpression[qi::_val = qi::_1] >> -(qi::lit("?") > orExpression > qi::lit(":") > orExpression)[qi::_val = phoenix::bind(&ExpressionParser::createIteExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]; |
|||
iteExpression.name("if-then-else expression"); |
|||
|
|||
expression %= iteExpression; |
|||
expression.name("expression"); |
|||
|
|||
// Enable error reporting.
|
|||
qi::on_error<qi::fail>(expression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); |
|||
qi::on_error<qi::fail>(iteExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); |
|||
qi::on_error<qi::fail>(orExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); |
|||
qi::on_error<qi::fail>(andExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); |
|||
qi::on_error<qi::fail>(equalityExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); |
|||
qi::on_error<qi::fail>(relativeExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); |
|||
qi::on_error<qi::fail>(plusExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); |
|||
qi::on_error<qi::fail>(multiplicationExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); |
|||
qi::on_error<qi::fail>(unaryExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); |
|||
qi::on_error<qi::fail>(atomicExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); |
|||
qi::on_error<qi::fail>(literalExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); |
|||
qi::on_error<qi::fail>(identifierExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); |
|||
qi::on_error<qi::fail>(minMaxExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); |
|||
qi::on_error<qi::fail>(floorCeilExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); |
|||
} |
|||
|
|||
void ExpressionParser::setIdentifierMapping(qi::symbols<char, storm::expressions::Expression> const* identifiers_) { |
|||
if (identifiers_ != nullptr) { |
|||
this->createExpressions = true; |
|||
this->identifiers_ = identifiers_; |
|||
} else { |
|||
this->createExpressions = false; |
|||
this->identifiers_ = nullptr; |
|||
} |
|||
} |
|||
|
|||
void ExpressionParser::unsetIdentifierMapping() { |
|||
this->createExpressions = false; |
|||
this->identifiers_ = nullptr; |
|||
} |
|||
|
|||
void ExpressionParser::setAcceptDoubleLiterals(bool flag) { |
|||
this->acceptDoubleLiterals = flag; |
|||
} |
|||
|
|||
storm::expressions::Expression ExpressionParser::createIteExpression(storm::expressions::Expression e1, storm::expressions::Expression e2, storm::expressions::Expression e3) const { |
|||
if (this->createExpressions) { |
|||
try { |
|||
return e1.ite(e2, e3); |
|||
} catch (storm::exceptions::InvalidTypeException const& e) { |
|||
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); |
|||
} |
|||
} else { |
|||
return storm::expressions::Expression::createFalse(); |
|||
} |
|||
} |
|||
|
|||
storm::expressions::Expression ExpressionParser::createImpliesExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { |
|||
if (this->createExpressions) { |
|||
try { |
|||
return e1.implies(e2); |
|||
} catch (storm::exceptions::InvalidTypeException const& e) { |
|||
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); |
|||
} |
|||
} else { |
|||
return storm::expressions::Expression::createFalse(); |
|||
} |
|||
} |
|||
|
|||
storm::expressions::Expression ExpressionParser::createOrExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { |
|||
if (this->createExpressions) { |
|||
try { |
|||
return e1 || e2; |
|||
} catch (storm::exceptions::InvalidTypeException const& e) { |
|||
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); |
|||
} |
|||
} else { |
|||
return storm::expressions::Expression::createFalse(); |
|||
} |
|||
} |
|||
|
|||
storm::expressions::Expression ExpressionParser::createAndExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { |
|||
if (this->createExpressions) { |
|||
try{ |
|||
return e1 && e2; |
|||
} catch (storm::exceptions::InvalidTypeException const& e) { |
|||
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); |
|||
} |
|||
} else { |
|||
return storm::expressions::Expression::createFalse(); |
|||
} |
|||
} |
|||
|
|||
storm::expressions::Expression ExpressionParser::createGreaterExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { |
|||
if (this->createExpressions) { |
|||
try { |
|||
return e1 > e2; |
|||
} catch (storm::exceptions::InvalidTypeException const& e) { |
|||
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); |
|||
} |
|||
} else { |
|||
return storm::expressions::Expression::createFalse(); |
|||
} |
|||
} |
|||
|
|||
storm::expressions::Expression ExpressionParser::createGreaterOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { |
|||
if (this->createExpressions) { |
|||
try { |
|||
return e1 >= e2; |
|||
} catch (storm::exceptions::InvalidTypeException const& e) { |
|||
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); |
|||
} |
|||
} else { |
|||
return storm::expressions::Expression::createFalse(); |
|||
} |
|||
} |
|||
|
|||
storm::expressions::Expression ExpressionParser::createLessExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { |
|||
if (this->createExpressions) { |
|||
try { |
|||
return e1 < e2; |
|||
} catch (storm::exceptions::InvalidTypeException const& e) { |
|||
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); |
|||
} |
|||
} else { |
|||
return storm::expressions::Expression::createFalse(); |
|||
} |
|||
} |
|||
|
|||
storm::expressions::Expression ExpressionParser::createLessOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { |
|||
if (this->createExpressions) { |
|||
try { |
|||
return e1 <= e2; |
|||
} catch (storm::exceptions::InvalidTypeException const& e) { |
|||
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); |
|||
} |
|||
} else { |
|||
return storm::expressions::Expression::createFalse(); |
|||
} |
|||
} |
|||
|
|||
storm::expressions::Expression ExpressionParser::createEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { |
|||
if (this->createExpressions) { |
|||
try { |
|||
if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) { |
|||
return e1.iff(e2); |
|||
} else { |
|||
return e1 == e2; |
|||
} |
|||
} catch (storm::exceptions::InvalidTypeException const& e) { |
|||
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); |
|||
} |
|||
} else { |
|||
return storm::expressions::Expression::createFalse(); |
|||
} |
|||
} |
|||
|
|||
storm::expressions::Expression ExpressionParser::createNotEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { |
|||
if (this->createExpressions) { |
|||
try { |
|||
return e1 != e2; |
|||
} catch (storm::exceptions::InvalidTypeException const& e) { |
|||
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); |
|||
} |
|||
} else { |
|||
return storm::expressions::Expression::createFalse(); |
|||
} |
|||
} |
|||
|
|||
storm::expressions::Expression ExpressionParser::createPlusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { |
|||
if (this->createExpressions) { |
|||
try { |
|||
return e1 + e2; |
|||
} catch (storm::exceptions::InvalidTypeException const& e) { |
|||
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); |
|||
} |
|||
} else { |
|||
return storm::expressions::Expression::createFalse(); |
|||
} |
|||
} |
|||
|
|||
storm::expressions::Expression ExpressionParser::createMinusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { |
|||
if (this->createExpressions) { |
|||
try { |
|||
return e1 - e2; |
|||
} catch (storm::exceptions::InvalidTypeException const& e) { |
|||
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); |
|||
} |
|||
} else { |
|||
return storm::expressions::Expression::createFalse(); |
|||
} |
|||
} |
|||
|
|||
storm::expressions::Expression ExpressionParser::createMultExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { |
|||
if (this->createExpressions) { |
|||
try { |
|||
return e1 * e2; |
|||
} catch (storm::exceptions::InvalidTypeException const& e) { |
|||
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); |
|||
} |
|||
} else { |
|||
return storm::expressions::Expression::createFalse(); |
|||
} |
|||
} |
|||
|
|||
storm::expressions::Expression ExpressionParser::createPowerExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { |
|||
if (this->createExpressions) { |
|||
try { |
|||
return e1 ^ e2; |
|||
} catch (storm::exceptions::InvalidTypeException const& e) { |
|||
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); |
|||
} |
|||
} else { |
|||
return storm::expressions::Expression::createFalse(); |
|||
} |
|||
} |
|||
|
|||
storm::expressions::Expression ExpressionParser::createDivExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { |
|||
if (this->createExpressions) { |
|||
try { |
|||
return e1 / e2; |
|||
} catch (storm::exceptions::InvalidTypeException const& e) { |
|||
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); |
|||
} |
|||
} else { |
|||
return storm::expressions::Expression::createFalse(); |
|||
} |
|||
} |
|||
|
|||
storm::expressions::Expression ExpressionParser::createNotExpression(storm::expressions::Expression e1) const { |
|||
if (this->createExpressions) { |
|||
try { |
|||
return !e1; |
|||
} catch (storm::exceptions::InvalidTypeException const& e) { |
|||
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); |
|||
} |
|||
} else { |
|||
return storm::expressions::Expression::createFalse(); |
|||
} |
|||
} |
|||
|
|||
storm::expressions::Expression ExpressionParser::createMinusExpression(storm::expressions::Expression e1) const { |
|||
if (this->createExpressions) { |
|||
try { |
|||
return -e1; |
|||
} catch (storm::exceptions::InvalidTypeException const& e) { |
|||
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); |
|||
} |
|||
} else { |
|||
return storm::expressions::Expression::createFalse(); |
|||
} |
|||
} |
|||
|
|||
storm::expressions::Expression ExpressionParser::createTrueExpression() const { |
|||
if (this->createExpressions) { |
|||
return storm::expressions::Expression::createTrue(); |
|||
} else { |
|||
return storm::expressions::Expression::createFalse(); |
|||
} |
|||
} |
|||
|
|||
storm::expressions::Expression ExpressionParser::createFalseExpression() const { |
|||
return storm::expressions::Expression::createFalse(); |
|||
} |
|||
|
|||
storm::expressions::Expression ExpressionParser::createDoubleLiteralExpression(double value, bool& pass) const { |
|||
// If we are not supposed to accept double expressions, we reject it by setting pass to false.
|
|||
if (!this->acceptDoubleLiterals) { |
|||
pass = false; |
|||
} |
|||
|
|||
if (this->createExpressions) { |
|||
return storm::expressions::Expression::createDoubleLiteral(value); |
|||
} else { |
|||
return storm::expressions::Expression::createFalse(); |
|||
} |
|||
} |
|||
|
|||
storm::expressions::Expression ExpressionParser::createIntegerLiteralExpression(int value) const { |
|||
if (this->createExpressions) { |
|||
return storm::expressions::Expression::createIntegerLiteral(static_cast<int_fast64_t>(value)); |
|||
} else { |
|||
return storm::expressions::Expression::createFalse(); |
|||
} |
|||
} |
|||
|
|||
storm::expressions::Expression ExpressionParser::createMinimumExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { |
|||
if (this->createExpressions) { |
|||
try { |
|||
return storm::expressions::Expression::minimum(e1, e2); |
|||
} catch (storm::exceptions::InvalidTypeException const& e) { |
|||
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); |
|||
} |
|||
} else { |
|||
return storm::expressions::Expression::createFalse(); |
|||
} |
|||
} |
|||
|
|||
storm::expressions::Expression ExpressionParser::createMaximumExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const { |
|||
if (this->createExpressions) { |
|||
try { |
|||
return storm::expressions::Expression::maximum(e1, e2); |
|||
} catch (storm::exceptions::InvalidTypeException const& e) { |
|||
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); |
|||
} |
|||
} else { |
|||
return storm::expressions::Expression::createFalse(); |
|||
} |
|||
} |
|||
|
|||
storm::expressions::Expression ExpressionParser::createFloorExpression(storm::expressions::Expression e1) const { |
|||
if (this->createExpressions) { |
|||
try { |
|||
return e1.floor(); |
|||
} catch (storm::exceptions::InvalidTypeException const& e) { |
|||
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); |
|||
} |
|||
} else { |
|||
return storm::expressions::Expression::createFalse(); |
|||
} |
|||
} |
|||
|
|||
storm::expressions::Expression ExpressionParser::createCeilExpression(storm::expressions::Expression e1) const { |
|||
if (this->createExpressions) { |
|||
try { |
|||
return e1.ceil(); |
|||
} catch (storm::exceptions::InvalidTypeException const& e) { |
|||
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what()); |
|||
} |
|||
} else { |
|||
return storm::expressions::Expression::createFalse(); |
|||
} |
|||
} |
|||
|
|||
storm::expressions::Expression ExpressionParser::getIdentifierExpression(std::string const& identifier) const { |
|||
if (this->createExpressions) { |
|||
LOG_THROW(this->identifiers_ != nullptr, storm::exceptions::WrongFormatException, "Unable to substitute identifier expressions without given mapping."); |
|||
storm::expressions::Expression const* expression = this->identifiers_->find(identifier); |
|||
LOG_THROW(expression != nullptr, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": Undeclared identifier '" << identifier << "'."); |
|||
return *expression; |
|||
} else { |
|||
return storm::expressions::Expression::createFalse(); |
|||
} |
|||
} |
|||
|
|||
bool ExpressionParser::isValidIdentifier(std::string const& identifier) { |
|||
if (this->invalidIdentifiers_.find(identifier) != nullptr) { |
|||
return false; |
|||
} |
|||
return true; |
|||
} |
|||
} |
|||
} |
|||
Some files were not shown because too many files changed in this diff
Reference in new issue
xxxxxxxxxx