diff --git a/src/adapters/IntermediateRepresentationAdapter.h b/src/adapters/IntermediateRepresentationAdapter.h
new file mode 100644
index 000000000..d60325b11
--- /dev/null
+++ b/src/adapters/IntermediateRepresentationAdapter.h
@@ -0,0 +1,144 @@
+/*
+ * IntermediateRepresentationAdapter.h
+ *
+ * Created on: 13.01.2013
+ * Author: Christian Dehnert
+ */
+
+#ifndef STORM_IR_INTERMEDIATEREPRESENTATIONADAPTER_H_
+#define STORM_IR_INTERMEDIATEREPRESENTATIONADAPTER_H_
+
+#include <tuple>
+#include <unordered_map>
+#include <boost/functional/hash.hpp>
+#include <map>
+#include <queue>
+#include <iostream>
+
+typedef std::pair<std::vector<bool>, std::vector<int_fast64_t>> StateType;
+
+namespace storm {
+
+namespace adapters {
+
+class StateHash {
+public:
+ std::size_t operator()(StateType* state) const {
+ size_t seed = 0;
+ for (auto it = state->first.begin(); it != state->first.end(); ++it) {
+ boost::hash_combine<bool>(seed, *it);
+ }
+ for (auto it = state->second.begin(); it != state->second.end(); ++it) {
+ boost::hash_combine<int_fast64_t>(seed, *it);
+ }
+ return seed;
+ }
+};
+
+class IntermediateRepresentationAdapter {
+public:
+ template<class T>
+ static storm::storage::SquareSparseMatrix<T>* toSparseMatrix(storm::ir::Program const& program) {
+
+ uint_fast64_t numberOfIntegerVariables = 0;
+ uint_fast64_t numberOfBooleanVariables = 0;
+ for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
+ numberOfIntegerVariables += program.getModule(i).getNumberOfIntegerVariables();
+ numberOfBooleanVariables += program.getModule(i).getNumberOfBooleanVariables();
+ }
+
+ std::vector<storm::ir::BooleanVariable> booleanVariables;
+ std::vector<storm::ir::IntegerVariable> integerVariables;
+ booleanVariables.resize(numberOfBooleanVariables);
+ integerVariables.resize(numberOfIntegerVariables);
+
+ std::unordered_map<std::string, uint_fast64_t> booleanVariableToIndexMap;
+ std::unordered_map<std::string, uint_fast64_t> integerVariableToIndexMap;
+
+ uint_fast64_t nextBooleanVariableIndex = 0;
+ uint_fast64_t nextIntegerVariableIndex = 0;
+ for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
+ storm::ir::Module const& module = program.getModule(i);
+
+ for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) {
+ booleanVariables[nextBooleanVariableIndex] = module.getBooleanVariable(j);
+ booleanVariableToIndexMap[module.getBooleanVariable(j).getName()] = nextBooleanVariableIndex;
+ ++nextBooleanVariableIndex;
+ }
+ for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) {
+ integerVariables[nextIntegerVariableIndex] = module.getIntegerVariable(j);
+ integerVariableToIndexMap[module.getIntegerVariable(j).getName()] = nextIntegerVariableIndex;
+ ++nextIntegerVariableIndex;
+ }
+ }
+
+ StateType* initialState = new StateType(std::vector<bool>(), std::vector<int_fast64_t>());
+ std::get<0>(*initialState).resize(numberOfBooleanVariables);
+ std::get<1>(*initialState).resize(numberOfIntegerVariables);
+
+ for (uint_fast64_t i = 0; i < numberOfBooleanVariables; ++i) {
+ bool initialValue = booleanVariables[i].getInitialValue()->getValueAsBool(std::get<0>(*initialState), std::get<1>(*initialState));
+ std::get<0>(*initialState)[i] = initialValue;
+ }
+
+ for (uint_fast64_t i = 0; i < numberOfIntegerVariables; ++i) {
+ int_fast64_t initialValue = integerVariables[i].getInitialValue()->getValueAsInt(std::get<0>(*initialState), std::get<1>(*initialState));
+ std::get<1>(*initialState)[i] = initialValue;
+ }
+
+ std::cout << "Initial State:" << std::get<0>(*initialState) << " / " << std::get<1>(*initialState) << std::endl;
+
+ uint_fast64_t nextIndex = 1;
+ std::unordered_map<StateType*, uint_fast64_t, StateHash> stateToIndexMap;
+ std::vector<StateType*> allStates;
+ std::queue<StateType*> stateQueue;
+
+ allStates.push_back(initialState);
+ stateQueue.push(initialState);
+ stateToIndexMap[initialState] = 0;
+
+ while (!stateQueue.empty()) {
+ // Get first state in queue.
+ StateType* currentState = stateQueue.front();
+ stateQueue.pop();
+
+ // Iterate over all modules.
+ for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
+ storm::ir::Module const& module = program.getModule(i);
+
+ // Iterate over all commands.
+ for (uint_fast64_t j = 0; j < module.getNumberOfCommands(); ++j) {
+ storm::ir::Command const& command = module.getCommand(j);
+
+ // Check if this command is enabled in the current state.
+ if (command.getGuard()->getValueAsBool(std::get<0>(*currentState), std::get<1>(*currentState))) {
+ for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) {
+ storm::ir::Update const& update = command.getUpdate(k);
+
+ std::map<std::string, storm::ir::Assignment> const& booleanAssignmentMap = update.getBooleanAssignments();
+ for (auto assignedVariable : booleanAssignmentMap) {
+ // Check if the variable that is being assigned is a boolean or an integer.
+ // auto boolIt =
+
+ }
+ }
+ }
+ }
+ }
+ }
+
+ // Now free all the elements we allocated.
+ for (auto element : allStates) {
+ delete element;
+ }
+ return nullptr;
+ }
+
+};
+
+}
+
+}
+
+
+#endif /* STORM_IR_INTERMEDIATEREPRESENTATIONADAPTER_H_ */
diff --git a/src/exceptions/ExpressionEvaluationException.h b/src/exceptions/ExpressionEvaluationException.h
new file mode 100644
index 000000000..390991c1d
--- /dev/null
+++ b/src/exceptions/ExpressionEvaluationException.h
@@ -0,0 +1,23 @@
+/*
+ * ExpressionEvaluationException.h
+ *
+ * Created on: 12.01.2013
+ * Author: Christian Dehnert
+ */
+
+#ifndef STORM_EXCEPTIONS_EXPRESSIONEVALUATIONEXCEPTION_H_
+#define STORM_EXCEPTIONS_EXPRESSIONEVALUATIONEXCEPTION_H_
+
+#include "src/exceptions/BaseException.h"
+
+namespace storm {
+
+namespace exceptions {
+
+STORM_EXCEPTION_DEFINE_NEW(ExpressionEvaluationException)
+
+}
+
+}
+
+#endif /* STORM_EXCEPTIONS_EXPRESSIONEVALUATIONEXCEPTION_H_ */
diff --git a/src/exceptions/NotImplementedException.h b/src/exceptions/NotImplementedException.h
new file mode 100644
index 000000000..cf98d4d99
--- /dev/null
+++ b/src/exceptions/NotImplementedException.h
@@ -0,0 +1,23 @@
+/*
+ * NotImplementedException.h
+ *
+ * Created on: 12.01.2013
+ * Author: Christian Dehnert
+ */
+
+#ifndef STORM_EXCEPTIONS_NOTIMPLEMENTEDEXCEPTION_H_
+#define STORM_EXCEPTIONS_NOTIMPLEMENTEDEXCEPTION_H_
+
+#include "src/exceptions/BaseException.h"
+
+namespace storm {
+
+namespace exceptions {
+
+STORM_EXCEPTION_DEFINE_NEW(NotImplementedException)
+
+}
+
+}
+
+#endif /* STORM_EXCEPTIONS_NOTIMPLEMENTEDEXCEPTION_H_ */
diff --git a/src/ir/BooleanVariable.cpp b/src/ir/BooleanVariable.cpp
index e524d6753..b867a1aa1 100644
--- a/src/ir/BooleanVariable.cpp
+++ b/src/ir/BooleanVariable.cpp
@@ -19,16 +19,16 @@ BooleanVariable::BooleanVariable() : Variable() {
}
// Initializes all members according to the given values.
-BooleanVariable::BooleanVariable(std::string variableName,
+BooleanVariable::BooleanVariable(uint_fast64_t index, std::string variableName,
std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue)
- : Variable(variableName, initialValue) {
+ : Variable(index, variableName, initialValue) {
// Nothing to do here.
}
// Build a string representation of the variable.
std::string BooleanVariable::toString() const {
std::stringstream result;
- result << getVariableName() << ": bool";
+ result << this->getName() << ": bool";
if (this->getInitialValue() != nullptr) {
result << " init " << this->getInitialValue()->toString();
}
diff --git a/src/ir/BooleanVariable.h b/src/ir/BooleanVariable.h
index dc832399e..e12506b67 100644
--- a/src/ir/BooleanVariable.h
+++ b/src/ir/BooleanVariable.h
@@ -8,6 +8,8 @@
#ifndef STORM_IR_BOOLEANVARIABLE_H_
#define STORM_IR_BOOLEANVARIABLE_H_
+#include "expressions/BooleanLiteral.h"
+
#include "Variable.h"
#include <memory>
@@ -27,10 +29,11 @@ public:
/*!
* Creates a boolean variable with the given name and the given initial value.
+ * @param index a 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.
*/
- BooleanVariable(std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>());
+ BooleanVariable(uint_fast64_t index, std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>(new storm::ir::expressions::BooleanLiteral(false)));
/*!
* Retrieves a string representation of this variable.
diff --git a/src/ir/Command.cpp b/src/ir/Command.cpp
index 832fbb302..5cb4c6354 100644
--- a/src/ir/Command.cpp
+++ b/src/ir/Command.cpp
@@ -24,6 +24,21 @@ Command::Command(std::string commandName, std::shared_ptr<storm::ir::expressions
// Nothing to do here.
}
+// Return the expression for the guard.
+std::shared_ptr<storm::ir::expressions::BaseExpression> const& Command::getGuard() const {
+ return guardExpression;
+}
+
+// Return the number of updates.
+uint_fast64_t Command::getNumberOfUpdates() const {
+ return this->updates.size();
+}
+
+// Return the requested update.
+storm::ir::Update const& Command::getUpdate(uint_fast64_t index) const {
+ return this->updates[index];
+}
+
// Build a string representation of the command.
std::string Command::toString() const {
std::stringstream result;
diff --git a/src/ir/Command.h b/src/ir/Command.h
index 186d81058..2ac54b525 100644
--- a/src/ir/Command.h
+++ b/src/ir/Command.h
@@ -35,6 +35,24 @@ public:
*/
Command(std::string commandName, std::shared_ptr<storm::ir::expressions::BaseExpression> guardExpression, std::vector<storm::ir::Update> updates);
+ /*!
+ * Retrieves a reference to the guard of the command.
+ * @returns a reference to the guard of the command.
+ */
+ std::shared_ptr<storm::ir::expressions::BaseExpression> const& getGuard() const;
+
+ /*!
+ * Retrieves the number of updates associated with this command.
+ * @returns the number of updates associated with this command.
+ */
+ uint_fast64_t getNumberOfUpdates() const;
+
+ /*!
+ * Retrieves a reference to the update with the given index.
+ * @returns a reference to the update with the given index.
+ */
+ storm::ir::Update const& getUpdate(uint_fast64_t index) const;
+
/*!
* Retrieves a string representation of this command.
* @returns a string representation of this command.
diff --git a/src/ir/IntegerVariable.cpp b/src/ir/IntegerVariable.cpp
index 6b6724b1a..8374551a9 100644
--- a/src/ir/IntegerVariable.cpp
+++ b/src/ir/IntegerVariable.cpp
@@ -9,6 +9,8 @@
#include <sstream>
+#include <iostream>
+
namespace storm {
namespace ir {
@@ -19,14 +21,16 @@ IntegerVariable::IntegerVariable() : lowerBound(), upperBound() {
}
// Initializes all members according to the given values.
-IntegerVariable::IntegerVariable(std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> lowerBound, std::shared_ptr<storm::ir::expressions::BaseExpression> upperBound, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue) : Variable(variableName, initialValue), lowerBound(lowerBound), upperBound(upperBound) {
- // Nothing to do here.
+IntegerVariable::IntegerVariable(uint_fast64_t index, std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> lowerBound, std::shared_ptr<storm::ir::expressions::BaseExpression> upperBound, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue) : Variable(index, variableName, initialValue), lowerBound(lowerBound), upperBound(upperBound) {
+ if (this->getInitialValue() == nullptr) {
+ this->setInitialValue(lowerBound);
+ }
}
// Build a string representation of the variable.
std::string IntegerVariable::toString() const {
std::stringstream result;
- result << this->getVariableName() << ": [" << lowerBound->toString() << ".." << upperBound->toString() << "]";
+ result << this->getName() << ": [" << lowerBound->toString() << ".." << upperBound->toString() << "]";
if (this->getInitialValue() != nullptr) {
result << " init " + this->getInitialValue()->toString();
}
diff --git a/src/ir/IntegerVariable.h b/src/ir/IntegerVariable.h
index d687e2a04..86e2dfc1b 100644
--- a/src/ir/IntegerVariable.h
+++ b/src/ir/IntegerVariable.h
@@ -29,12 +29,13 @@ public:
/*!
* Creates an integer variable with the given name, lower and upper bounds and the given initial
* value.
+ * @param index A unique (among the variables of equal type) 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(std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> lowerBound, std::shared_ptr<storm::ir::expressions::BaseExpression> upperBound, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>());
+ IntegerVariable(uint_fast64_t index, std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> lowerBound, std::shared_ptr<storm::ir::expressions::BaseExpression> upperBound, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>(nullptr));
/*!
* Retrieves a string representation of this variable.
diff --git a/src/ir/Module.cpp b/src/ir/Module.cpp
index 5f28a8d13..f76a53b88 100644
--- a/src/ir/Module.cpp
+++ b/src/ir/Module.cpp
@@ -14,25 +14,62 @@ namespace storm {
namespace ir {
// Initializes all members with their default constructors.
-Module::Module() : moduleName(), booleanVariables(), integerVariables(), commands() {
+Module::Module() : moduleName(), booleanVariables(), integerVariables(), booleanVariablesToIndexMap(),
+ integerVariablesToIndexMap(), commands() {
// Nothing to do here.
}
// Initializes all members according to the given values.
-Module::Module(std::string moduleName, std::map<std::string, storm::ir::BooleanVariable> booleanVariables, std::map<std::string, storm::ir::IntegerVariable> integerVariables, std::vector<storm::ir::Command> commands)
- : moduleName(moduleName), booleanVariables(booleanVariables), integerVariables(integerVariables), commands(commands) {
+Module::Module(std::string moduleName, std::vector<storm::ir::BooleanVariable> booleanVariables,
+ std::vector<storm::ir::IntegerVariable> integerVariables,
+ std::map<std::string, uint_fast64_t> booleanVariableToIndexMap,
+ std::map<std::string, uint_fast64_t> integerVariableToIndexMap,
+ std::vector<storm::ir::Command> commands)
+ : moduleName(moduleName), booleanVariables(booleanVariables), integerVariables(integerVariables),
+ booleanVariablesToIndexMap(booleanVariableToIndexMap),
+ integerVariablesToIndexMap(integerVariableToIndexMap), commands(commands) {
// Nothing to do here.
}
+// Return the number of boolean variables.
+uint_fast64_t Module::getNumberOfBooleanVariables() const {
+ return this->booleanVariables.size();
+}
+
+// Return the requested boolean variable.
+storm::ir::BooleanVariable const& Module::getBooleanVariable(uint_fast64_t index) const {
+ return this->booleanVariables[index];
+}
+
+// Return the number of integer variables.
+uint_fast64_t Module::getNumberOfIntegerVariables() const {
+ return this->integerVariables.size();
+}
+
+// Return the requested integer variable.
+storm::ir::IntegerVariable const& Module::getIntegerVariable(uint_fast64_t index) const {
+ return this->integerVariables[index];
+}
+
+// Return the number of commands.
+uint_fast64_t Module::getNumberOfCommands() const {
+ return this->commands.size();
+}
+
+// Return the requested command.
+storm::ir::Command const& Module::getCommand(uint_fast64_t index) const {
+ return this->commands[index];
+}
+
// Build a string representation of the variable.
std::string Module::toString() const {
std::stringstream result;
result << "module " << moduleName << std::endl;
for (auto variable : booleanVariables) {
- result << "\t" << variable.second.toString() << std::endl;
+ result << "\t" << variable.toString() << std::endl;
}
for (auto variable : integerVariables) {
- result << "\t" << variable.second.toString() << std::endl;
+ result << "\t" << variable.toString() << std::endl;
}
for (auto command : commands) {
result << "\t" << command.toString() << std::endl;
diff --git a/src/ir/Module.h b/src/ir/Module.h
index ad0218730..0ed2ed010 100644
--- a/src/ir/Module.h
+++ b/src/ir/Module.h
@@ -37,7 +37,47 @@ public:
* @param integerVariables a map of integer variables.
* @param commands the vector of commands.
*/
- Module(std::string moduleName, std::map<std::string, storm::ir::BooleanVariable> booleanVariables, std::map<std::string, storm::ir::IntegerVariable> integerVariables, std::vector<storm::ir::Command> commands);
+ Module(std::string moduleName, std::vector<storm::ir::BooleanVariable> booleanVariables,
+ std::vector<storm::ir::IntegerVariable> integerVariables,
+ std::map<std::string, uint_fast64_t> booleanVariableToIndexMap,
+ std::map<std::string, uint_fast64_t> integerVariableToIndexMap,
+ std::vector<storm::ir::Command> commands);
+
+ /*!
+ * Retrieves the number of boolean variables in the module.
+ * @returns the number of boolean variables in the module.
+ */
+ uint_fast64_t getNumberOfBooleanVariables() const;
+
+ /*!
+ * Retrieves a reference to the boolean variable with the given index.
+ * @returns a reference to the boolean variable with the given index.
+ */
+ storm::ir::BooleanVariable const& getBooleanVariable(uint_fast64_t index) const;
+
+ /*!
+ * Retrieves the number of integer variables in the module.
+ * @returns the number of integer variables in the module.
+ */
+ uint_fast64_t getNumberOfIntegerVariables() const;
+
+ /*!
+ * Retrieves a reference to the integer variable with the given index.
+ * @returns a reference to the integer variable with the given index.
+ */
+ storm::ir::IntegerVariable const& getIntegerVariable(uint_fast64_t index) const;
+
+ /*!
+ * Retrieves the number of commands of this module.
+ * @returns the number of commands of this module.
+ */
+ uint_fast64_t getNumberOfCommands() const;
+
+ /*!
+ * Retrieves a reference to the command with the given index.
+ * @returns a reference to the command with the given index.
+ */
+ storm::ir::Command const& getCommand(uint_fast64_t index) const;
/*!
* Retrieves a string representation of this variable.
@@ -49,11 +89,17 @@ private:
// The name of the module.
std::string moduleName;
- // A map of boolean variable names to their details.
- std::map<std::string, storm::ir::BooleanVariable> booleanVariables;
+ // 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> booleanVariablesToIndexMap;
// A map of integer variable names to their details.
- std::map<std::string, storm::ir::IntegerVariable> integerVariables;
+ std::map<std::string, uint_fast64_t> integerVariablesToIndexMap;
// The commands associated with the module.
std::vector<storm::ir::Command> commands;
diff --git a/src/ir/Program.cpp b/src/ir/Program.cpp
index 5a250405e..e5dfa9ce3 100644
--- a/src/ir/Program.cpp
+++ b/src/ir/Program.cpp
@@ -62,6 +62,15 @@ std::string Program::toString() const {
return result.str();
}
+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];
+}
+
+
} // namespace ir
} // namepsace storm
diff --git a/src/ir/Program.h b/src/ir/Program.h
index 8fcd7c10f..8ea9b5b11 100644
--- a/src/ir/Program.h
+++ b/src/ir/Program.h
@@ -54,6 +54,18 @@ public:
*/
Program(ModelType modelType, std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> booleanUndefinedConstantExpressions, std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> integerUndefinedConstantExpressions, std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> doubleUndefinedConstantExpressions, std::vector<storm::ir::Module> modules, std::map<std::string, storm::ir::RewardModel> rewards, std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> labels);
+ /*!
+ * Retrieves the number of modules in the program.
+ * @returns 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.
+ */
+ storm::ir::Module const& getModule(uint_fast64_t index) const;
+
/*!
* Retrieves a string representation of this program.
* @returns a string representation of this program.
diff --git a/src/ir/Update.cpp b/src/ir/Update.cpp
index 4e59d46be..668b543da 100644
--- a/src/ir/Update.cpp
+++ b/src/ir/Update.cpp
@@ -7,6 +7,8 @@
#include "Update.h"
+#include "src/exceptions/OutOfRangeException.h"
+
#include <sstream>
namespace storm {
@@ -14,28 +16,81 @@ namespace storm {
namespace ir {
// Initializes all members with their default constructors.
-Update::Update() : likelihoodExpression(), assignments() {
+Update::Update() : likelihoodExpression(), booleanAssignments(), integerAssignments() {
// Nothing to do here.
}
// Initializes all members according to the given values.
-Update::Update(std::shared_ptr<storm::ir::expressions::BaseExpression> likelihoodExpression, std::map<std::string, storm::ir::Assignment> assignments)
- : likelihoodExpression(likelihoodExpression), assignments(assignments) {
+Update::Update(std::shared_ptr<storm::ir::expressions::BaseExpression> likelihoodExpression, std::map<std::string, storm::ir::Assignment> booleanAssignments, std::map<std::string, storm::ir::Assignment> integerAssignments)
+ : likelihoodExpression(likelihoodExpression), booleanAssignments(booleanAssignments), integerAssignments(integerAssignments) {
// Nothing to do here.
}
+// Return the expression for the likelihood of the update.
+std::shared_ptr<storm::ir::expressions::BaseExpression> const& Update::getLikelihoodExpression() const {
+ return likelihoodExpression;
+}
+
+// Return the number of assignments.
+uint_fast64_t Update::getNumberOfBooleanAssignments() const {
+ return booleanAssignments.size();
+}
+
+uint_fast64_t Update::getNumberOfIntegerAssignments() const {
+ return integerAssignments.size();
+}
+
+// Return the boolean variable name to assignment map.
+std::map<std::string, storm::ir::Assignment> const& Update::getBooleanAssignments() const {
+ return booleanAssignments;
+}
+
+// Return the integer variable name to assignment map.
+std::map<std::string, storm::ir::Assignment> const& Update::getIntegerAssignments() const {
+ return integerAssignments;
+}
+
+// Return the assignment for the boolean variable if it exists and throw an exception otherwise.
+storm::ir::Assignment const& Update::getBooleanAssignment(std::string variableName) const {
+ auto it = booleanAssignments.find(variableName);
+ if (it == booleanAssignments.end()) {
+ throw storm::exceptions::OutOfRangeException() << "Cannot find boolean assignment for variable '"
+ << variableName << "' in update " << this->toString() << ".";
+ }
+
+ return (*it).second;
+}
+
+// Return the assignment for the boolean variable if it exists and throw an exception otherwise.
+storm::ir::Assignment const& Update::getIntegerAssignment(std::string variableName) const {
+ auto it = integerAssignments.find(variableName);
+ if (it == integerAssignments.end()) {
+ throw storm::exceptions::OutOfRangeException() << "Cannot find integer assignment for variable '"
+ << variableName << "' in update " << this->toString() << ".";
+ }
+
+ return (*it).second;
+}
+
// Build a string representation of the update.
std::string Update::toString() const {
std::stringstream result;
result << likelihoodExpression->toString() << " : ";
uint_fast64_t i = 0;
- for (auto assignment : assignments) {
+ for (auto assignment : booleanAssignments) {
result << assignment.second.toString();
++i;
- if (i < assignments.size() - 1) {
+ if (i < booleanAssignments.size() - 1 || integerAssignments.size() > 0) {
+ result << " & ";
+ }
+ }
+ i = 0;
+ for (auto assignment : integerAssignments) {
+ result << assignment.second.toString();
+ ++i;
+ if (i < integerAssignments.size() - 1) {
result << " & ";
}
-
}
return result.str();
}
diff --git a/src/ir/Update.h b/src/ir/Update.h
index 1aeb1d125..54ddc5cd8 100644
--- a/src/ir/Update.h
+++ b/src/ir/Update.h
@@ -34,7 +34,49 @@ public:
* @param likelihoodExpression an expression specifying the likelihood of this update.
* @param assignments a map of variable names to their assignments.
*/
- Update(std::shared_ptr<storm::ir::expressions::BaseExpression> likelihoodExpression, std::map<std::string, storm::ir::Assignment> assignments);
+ Update(std::shared_ptr<storm::ir::expressions::BaseExpression> likelihoodExpression, std::map<std::string, storm::ir::Assignment> booleanAssignments, std::map<std::string, storm::ir::Assignment> integerAssignments);
+
+ /*!
+ * Retrieves the expression for the likelihood of this update.
+ * @returns the expression for the likelihood of this update.
+ */
+ std::shared_ptr<storm::ir::expressions::BaseExpression> const& getLikelihoodExpression() const;
+
+ /*!
+ * Retrieves the number of boolean assignments associated with this update.
+ * @returns the number of boolean assignments associated with this update.
+ */
+ uint_fast64_t getNumberOfBooleanAssignments() const;
+
+ /*!
+ * Retrieves the number of integer assignments associated with this update.
+ * @returns 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.
+ * @returns 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.
+ * @returns 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.
+ * @returns a reference to the assignment for the boolean variable with the given name.
+ */
+ storm::ir::Assignment const& getBooleanAssignment(std::string variableName) const;
+
+ /*!
+ * Retrieves a reference to the assignment for the integer variable with the given name.
+ * @returns a reference to the assignment for the integer variable with the given name.
+ */
+ storm::ir::Assignment const& getIntegerAssignment(std::string variableName) const;
/*!
* Retrieves a string representation of this update.
@@ -46,8 +88,11 @@ private:
// An expression specifying the likelihood of taking this update.
std::shared_ptr<storm::ir::expressions::BaseExpression> likelihoodExpression;
- // A mapping of variable names to their assignments in this update.
- std::map<std::string, storm::ir::Assignment> assignments;
+ // 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;
};
} // namespace ir
diff --git a/src/ir/Variable.cpp b/src/ir/Variable.cpp
index a735fa94d..d051b9ca1 100644
--- a/src/ir/Variable.cpp
+++ b/src/ir/Variable.cpp
@@ -14,17 +14,17 @@ namespace storm {
namespace ir {
// Initializes all members with their default constructors.
-Variable::Variable() : variableName(), initialValue() {
+Variable::Variable() : index(0), variableName(), initialValue() {
// Nothing to do here.
}
// Initializes all members according to the given values.
-Variable::Variable(std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue) : variableName(variableName), initialValue(initialValue) {
+Variable::Variable(uint_fast64_t index, std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue) : index(index), variableName(variableName), initialValue(initialValue) {
// Nothing to do here.
}
// Return the name of the variable.
-std::string const& Variable::getVariableName() const {
+std::string const& Variable::getName() const {
return variableName;
}
@@ -33,6 +33,12 @@ std::shared_ptr<storm::ir::expressions::BaseExpression> const& Variable::getInit
return initialValue;
}
+// Set the initial value expression to the one provided.
+void Variable::setInitialValue(std::shared_ptr<storm::ir::expressions::BaseExpression> const& initialValue) {
+ this->initialValue = initialValue;
+}
+
+
} // namespace ir
} // namespace storm
diff --git a/src/ir/Variable.h b/src/ir/Variable.h
index bbd567073..eed1e538c 100644
--- a/src/ir/Variable.h
+++ b/src/ir/Variable.h
@@ -28,16 +28,17 @@ public:
/*!
* Creates an untyped variable with the given name and initial value.
+ * @param index A 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(std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>());
+ Variable(uint_fast64_t index, std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>());
/*!
* Retrieves the name of the variable.
* @returns the name of the variable.
*/
- std::string const& getVariableName() const;
+ std::string const& getName() const;
/*!
* Retrieves the expression defining the initial value of the variable.
@@ -45,7 +46,16 @@ public:
*/
std::shared_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::shared_ptr<storm::ir::expressions::BaseExpression> const& initialValue);
+
private:
+ // A unique (among the variables of equal type) index for the variable
+ uint_fast64_t index;
+
// The name of the variable.
std::string variableName;
diff --git a/src/ir/expressions/BaseExpression.h b/src/ir/expressions/BaseExpression.h
index f2d848fb7..b88953dce 100644
--- a/src/ir/expressions/BaseExpression.h
+++ b/src/ir/expressions/BaseExpression.h
@@ -2,13 +2,17 @@
* Expression.h
*
* Created on: 03.01.2013
- * Author: chris
+ * Author: Christian Dehnert
*/
-#ifndef EXPRESSION_H_
-#define EXPRESSION_H_
+#ifndef STORM_IR_EXPRESSIONS_BASEEXPRESSION_H_
+#define STORM_IR_EXPRESSIONS_BASEEXPRESSION_H_
+
+#include "src/exceptions/ExpressionEvaluationException.h"
+#include "src/exceptions/NotImplementedException.h"
#include <string>
+#include <vector>
namespace storm {
@@ -19,19 +23,70 @@ namespace expressions {
class BaseExpression {
public:
+ enum ReturnType {undefined, bool_, int_, double_};
+
+ BaseExpression() : type(undefined) {
+
+ }
+
+ BaseExpression(ReturnType type) : type(type) {
+
+ }
+
virtual ~BaseExpression() {
}
- virtual std::string toString() const {
- return "expr here!";
+ virtual int_fast64_t getValueAsInt(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) 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.";
+ }
+
+ virtual bool getValueAsBool(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) 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.";
+ }
+
+ virtual double getValueAsDouble(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+ if (type != bool_) {
+ 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.";
}
+
+ virtual std::string toString() const = 0;
+
+ std::string 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");
+ }
+ }
+
+ ReturnType getType() const {
+ return type;
+ }
+
+private:
+ ReturnType type;
};
-}
+} // namespace expressions
-}
+} // namespace ir
-}
+} // namespace storm
-#endif /* EXPRESSION_H_ */
+#endif /* STORM_IR_EXPRESSIONS_BASEEXPRESSION_H_ */
diff --git a/src/ir/expressions/BinaryBooleanFunctionExpression.h b/src/ir/expressions/BinaryBooleanFunctionExpression.h
index bd388dc04..e26bd22f3 100644
--- a/src/ir/expressions/BinaryBooleanFunctionExpression.h
+++ b/src/ir/expressions/BinaryBooleanFunctionExpression.h
@@ -5,11 +5,13 @@
* Author: chris
*/
-#ifndef BINARYBOOLEANFUNCTIONEXPRESSION_H_
-#define BINARYBOOLEANFUNCTIONEXPRESSION_H_
+#ifndef STORM_IR_EXPRESSIONS_BINARYBOOLEANFUNCTIONEXPRESSION_H_
+#define STORM_IR_EXPRESSIONS_BINARYBOOLEANFUNCTIONEXPRESSION_H_
#include "src/ir/expressions/BaseExpression.h"
-#include <boost/fusion/include/adapt_struct.hpp>
+
+#include <memory>
+#include <sstream>
namespace storm {
@@ -19,38 +21,49 @@ namespace expressions {
class BinaryBooleanFunctionExpression : public BaseExpression {
public:
- enum FunctorType {AND, OR, XOR, IMPLIES} functor;
- std::shared_ptr<storm::ir::expressions::BaseExpression> left;
- std::shared_ptr<BaseExpression> right;
+ enum FunctionType {AND, OR};
+
+ BinaryBooleanFunctionExpression(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right, FunctionType functionType) : BaseExpression(bool_), left(left), right(right), functionType(functionType) {
- BinaryBooleanFunctionExpression(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right, FunctorType functor) {
- this->left = left;
- this->right = right;
- this->functor = functor;
}
virtual ~BinaryBooleanFunctionExpression() {
}
+ virtual bool getValueAsBool(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+ bool resultLeft = left->getValueAsBool(booleanVariableValues, integerVariableValues);
+ bool resultRight = right->getValueAsBool(booleanVariableValues, integerVariableValues);
+ 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 << "'.";
+ }
+ }
+
virtual std::string toString() const {
- std::string result = left->toString();
- switch (functor) {
- case AND: result += " & "; break;
- case OR: result += " | "; break;
- case XOR: result += " ^ "; break;
- case IMPLIES: result += " => "; break;
+ std::stringstream result;
+ result << left->toString();
+ switch (functionType) {
+ case AND: result << " & "; break;
+ case OR: result << " | "; break;
}
- result += right->toString();
+ result << right->toString();
- return result;
+ return result.str();
}
+
+private:
+ std::shared_ptr<BaseExpression> left;
+ std::shared_ptr<BaseExpression> right;
+ FunctionType functionType;
};
-}
+} // namespace expressions
-}
+} // namespace ir
-}
+} // namespace storm
-#endif /* BINARYBOOLEANFUNCTIONEXPRESSION_H_ */
+#endif /* STORM_IR_EXPRESSIONS_BINARYBOOLEANFUNCTIONEXPRESSION_H_ */
diff --git a/src/ir/expressions/BinaryNumericalFunctionExpression.h b/src/ir/expressions/BinaryNumericalFunctionExpression.h
index 5b928768e..28ba2b3f2 100644
--- a/src/ir/expressions/BinaryNumericalFunctionExpression.h
+++ b/src/ir/expressions/BinaryNumericalFunctionExpression.h
@@ -18,23 +18,53 @@ namespace expressions {
class BinaryNumericalFunctionExpression : public BaseExpression {
public:
- std::shared_ptr<BaseExpression> left;
- std::shared_ptr<BaseExpression> right;
- enum FunctorType {PLUS, MINUS, TIMES, DIVIDE} functor;
+ enum FunctionType {PLUS, MINUS, TIMES, DIVIDE};
+
+ BinaryNumericalFunctionExpression(ReturnType type, std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right, FunctionType functionType) : BaseExpression(type), left(left), right(right), functionType(functionType) {
- BinaryNumericalFunctionExpression(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right, FunctorType functor) {
- this->left = left;
- this->right = right;
- this->functor = functor;
}
virtual ~BinaryNumericalFunctionExpression() {
}
+ virtual int_fast64_t getValueAsInt(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+ if (this->getType() != int_) {
+ BaseExpression::getValueAsInt(booleanVariableValues, integerVariableValues);
+ }
+
+ int_fast64_t resultLeft = left->getValueAsInt(booleanVariableValues, integerVariableValues);
+ int_fast64_t resultRight = right->getValueAsInt(booleanVariableValues, integerVariableValues);
+ 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;
+ default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
+ << "Unknown numeric binary operator: '" << functionType << "'.";
+ }
+ }
+
+ virtual double getValueAsDouble(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+ if (this->getType() != double_) {
+ BaseExpression::getValueAsDouble(booleanVariableValues, integerVariableValues);
+ }
+
+ double resultLeft = left->getValueAsDouble(booleanVariableValues, integerVariableValues);
+ double resultRight = right->getValueAsDouble(booleanVariableValues, integerVariableValues);
+ 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;
+ default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
+ << "Unknown numeric binary operator: '" << functionType << "'.";
+ }
+ }
+
virtual std::string toString() const {
std::string result = left->toString();
- switch (functor) {
+ switch (functionType) {
case PLUS: result += " + "; break;
case MINUS: result += " - "; break;
case TIMES: result += " * "; break;
@@ -44,7 +74,10 @@ public:
return result;
}
-
+private:
+ std::shared_ptr<BaseExpression> left;
+ std::shared_ptr<BaseExpression> right;
+ FunctionType functionType;
};
}
diff --git a/src/ir/expressions/BinaryRelationExpression.h b/src/ir/expressions/BinaryRelationExpression.h
index 625b801f5..db834ea93 100644
--- a/src/ir/expressions/BinaryRelationExpression.h
+++ b/src/ir/expressions/BinaryRelationExpression.h
@@ -18,23 +18,33 @@ namespace expressions {
class BinaryRelationExpression : public BaseExpression {
public:
- std::shared_ptr<BaseExpression> left;
- std::shared_ptr<BaseExpression> right;
- enum RelationType {EQUAL, LESS, LESS_OR_EQUAL, GREATER, GREATER_OR_EQUAL} relation;
+ enum RelationType {EQUAL, LESS, LESS_OR_EQUAL, GREATER, GREATER_OR_EQUAL};
+
+ BinaryRelationExpression(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right, RelationType relationType) : BaseExpression(bool_), left(left), right(right), relationType(relationType) {
- BinaryRelationExpression(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right, RelationType relation) {
- this->left = left;
- this->right = right;
- this->relation = relation;
}
virtual ~BinaryRelationExpression() {
}
+ virtual bool getValueAsBool(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+ int_fast64_t resultLeft = left->getValueAsInt(booleanVariableValues, integerVariableValues);
+ int_fast64_t resultRight = right->getValueAsInt(booleanVariableValues, integerVariableValues);
+ switch(relationType) {
+ case 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 << "'.";
+ }
+ }
+
virtual std::string toString() const {
std::string result = left->toString();
- switch (relation) {
+ switch (relationType) {
case EQUAL: result += " = "; break;
case LESS: result += " < "; break;
case LESS_OR_EQUAL: result += " <= "; break;
@@ -46,6 +56,10 @@ public:
return result;
}
+private:
+ std::shared_ptr<BaseExpression> left;
+ std::shared_ptr<BaseExpression> right;
+ RelationType relationType;
};
}
diff --git a/src/ir/expressions/BooleanConstantExpression.h b/src/ir/expressions/BooleanConstantExpression.h
index a10c2363e..cfd6ae418 100644
--- a/src/ir/expressions/BooleanConstantExpression.h
+++ b/src/ir/expressions/BooleanConstantExpression.h
@@ -20,7 +20,7 @@ namespace expressions {
class BooleanConstantExpression : public ConstantExpression {
public:
- BooleanConstantExpression(std::string constantName) : ConstantExpression(constantName) {
+ BooleanConstantExpression(std::string constantName) : ConstantExpression(bool_, constantName) {
defined = false;
value = false;
}
@@ -29,6 +29,15 @@ public:
}
+ virtual bool getValueAsBool(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+ if (!defined) {
+ throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
+ << "Boolean constant '" << this->getConstantName() << "' is undefined.";
+ } else {
+ return value;
+ }
+ }
+
virtual std::string toString() const {
std::string result = this->constantName;
if (defined) {
diff --git a/src/ir/expressions/BooleanLiteral.h b/src/ir/expressions/BooleanLiteral.h
index 81950e52a..f7d4e9957 100644
--- a/src/ir/expressions/BooleanLiteral.h
+++ b/src/ir/expressions/BooleanLiteral.h
@@ -20,14 +20,18 @@ class BooleanLiteral : public BaseExpression {
public:
bool value;
- BooleanLiteral(bool value) {
- this->value = value;
+ BooleanLiteral(bool value) : BaseExpression(bool_), value(value) {
+
}
virtual ~BooleanLiteral() {
}
+ virtual bool getValueAsBool(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+ return value;
+ }
+
virtual std::string toString() const {
if (value) {
return std::string("true");
diff --git a/src/ir/expressions/ConstantExpression.h b/src/ir/expressions/ConstantExpression.h
index 239b3dc68..79c356dba 100644
--- a/src/ir/expressions/ConstantExpression.h
+++ b/src/ir/expressions/ConstantExpression.h
@@ -20,14 +20,18 @@ class ConstantExpression : public BaseExpression {
public:
std::string constantName;
- ConstantExpression(std::string constantName) {
- this->constantName = constantName;
+ ConstantExpression(ReturnType type, std::string constantName) : BaseExpression(type), constantName(constantName) {
+
}
virtual ~ConstantExpression() {
}
+ std::string const& getConstantName() const {
+ return constantName;
+ }
+
virtual std::string toString() const {
return constantName;
}
diff --git a/src/ir/expressions/DoubleConstantExpression.h b/src/ir/expressions/DoubleConstantExpression.h
index 3a7363a65..9ad1e61d6 100644
--- a/src/ir/expressions/DoubleConstantExpression.h
+++ b/src/ir/expressions/DoubleConstantExpression.h
@@ -18,15 +18,23 @@ namespace expressions {
class DoubleConstantExpression : public ConstantExpression {
public:
- DoubleConstantExpression(std::string constantName) : ConstantExpression(constantName) {
- defined = false;
- value = 0.0;
+ DoubleConstantExpression(std::string constantName) : ConstantExpression(double_, constantName), defined(false), value(0) {
+
}
virtual ~DoubleConstantExpression() {
}
+ virtual double getValueAsDouble(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+ if (!defined) {
+ throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
+ << "Double constant '" << this->getConstantName() << "' is undefined.";
+ } else {
+ return value;
+ }
+ }
+
virtual std::string toString() const {
std::string result = this->constantName;
if (defined) {
@@ -48,8 +56,9 @@ public:
this->value = value;
}
- double value;
+private:
bool defined;
+ double value;
};
}
diff --git a/src/ir/expressions/DoubleLiteral.h b/src/ir/expressions/DoubleLiteral.h
index dbdcf55ca..e7854cfa5 100644
--- a/src/ir/expressions/DoubleLiteral.h
+++ b/src/ir/expressions/DoubleLiteral.h
@@ -22,14 +22,18 @@ class DoubleLiteral : public BaseExpression {
public:
double value;
- DoubleLiteral(double value) {
- this->value = value;
+ DoubleLiteral(double value) : BaseExpression(double_), value(value) {
+
}
virtual ~DoubleLiteral() {
}
+ virtual double getValueAsDouble(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+ return value;
+ }
+
virtual std::string toString() const {
return boost::lexical_cast<std::string>(value);
}
diff --git a/src/ir/expressions/IntegerConstantExpression.h b/src/ir/expressions/IntegerConstantExpression.h
index 5ff4d7f87..5e7c46ee7 100644
--- a/src/ir/expressions/IntegerConstantExpression.h
+++ b/src/ir/expressions/IntegerConstantExpression.h
@@ -18,15 +18,23 @@ namespace expressions {
class IntegerConstantExpression : public ConstantExpression {
public:
- IntegerConstantExpression(std::string constantName) : ConstantExpression(constantName) {
- defined = false;
- value = 0;
+ IntegerConstantExpression(std::string constantName) : ConstantExpression(int_, constantName), defined(false), value(0) {
+
}
virtual ~IntegerConstantExpression() {
}
+ virtual int_fast64_t getValueAsInt(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+ if (!defined) {
+ throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
+ << "Integer constant '" << this->getConstantName() << "' is undefined.";
+ } else {
+ return value;
+ }
+ }
+
virtual std::string toString() const {
std::string result = this->constantName;
if (defined) {
@@ -43,13 +51,14 @@ public:
return value;
}
- void define(int value) {
+ void define(int_fast64_t value) {
defined = true;
this->value = value;
}
- int value;
+private:
bool defined;
+ int_fast64_t value;
};
}
diff --git a/src/ir/expressions/IntegerLiteral.h b/src/ir/expressions/IntegerLiteral.h
index aef509321..36c78a948 100644
--- a/src/ir/expressions/IntegerLiteral.h
+++ b/src/ir/expressions/IntegerLiteral.h
@@ -18,16 +18,20 @@ namespace expressions {
class IntegerLiteral : public BaseExpression {
public:
- int value;
+ int_fast64_t value;
+
+ IntegerLiteral(int_fast64_t value) : BaseExpression(int_), value(value) {
- IntegerLiteral(int value) {
- this->value = value;
}
virtual ~IntegerLiteral() {
}
+ virtual int_fast64_t getValueAsInt(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+ return value;
+ }
+
virtual std::string toString() const {
return boost::lexical_cast<std::string>(value);
}
diff --git a/src/ir/expressions/UnaryBooleanFunctionExpression.h b/src/ir/expressions/UnaryBooleanFunctionExpression.h
index 893169b51..b21a70f87 100644
--- a/src/ir/expressions/UnaryBooleanFunctionExpression.h
+++ b/src/ir/expressions/UnaryBooleanFunctionExpression.h
@@ -18,27 +18,38 @@ namespace expressions {
class UnaryBooleanFunctionExpression : public BaseExpression {
public:
- std::shared_ptr<BaseExpression> child;
- enum FunctorType {NOT} functor;
+ enum FunctionType {NOT};
+
+ UnaryBooleanFunctionExpression(std::shared_ptr<BaseExpression> child, FunctionType functionType) : BaseExpression(bool_), child(child), functionType(functionType) {
- UnaryBooleanFunctionExpression(std::shared_ptr<BaseExpression> child, FunctorType functor) {
- this->child = child;
- this->functor = functor;
}
virtual ~UnaryBooleanFunctionExpression() {
}
+ virtual bool getValueAsBool(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+ bool resultChild = child->getValueAsBool(booleanVariableValues, integerVariableValues);
+ switch(functionType) {
+ case NOT: return !resultChild; break;
+ default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
+ << "Unknown boolean unary operator: '" << functionType << "'.";
+ }
+ }
+
virtual std::string toString() const {
std::string result = "";
- switch (functor) {
+ switch (functionType) {
case NOT: result += "!"; break;
}
result += child->toString();
return result;
}
+
+private:
+ std::shared_ptr<BaseExpression> child;
+ FunctionType functionType;
};
}
diff --git a/src/ir/expressions/UnaryNumericalFunctionExpression.h b/src/ir/expressions/UnaryNumericalFunctionExpression.h
index f697f35eb..db5cb2945 100644
--- a/src/ir/expressions/UnaryNumericalFunctionExpression.h
+++ b/src/ir/expressions/UnaryNumericalFunctionExpression.h
@@ -18,27 +18,55 @@ namespace expressions {
class UnaryNumericalFunctionExpression : public BaseExpression {
public:
- std::shared_ptr<BaseExpression> child;
- enum FunctorType {MINUS} functor;
+ enum FunctionType {MINUS};
+
+ UnaryNumericalFunctionExpression(ReturnType type, std::shared_ptr<BaseExpression> child, FunctionType functionType) : BaseExpression(type), child(child), functionType(functionType) {
- UnaryNumericalFunctionExpression(std::shared_ptr<BaseExpression> child, FunctorType functor) {
- this->child = child;
- this->functor = functor;
}
virtual ~UnaryNumericalFunctionExpression() {
}
+ virtual int_fast64_t getValueAsInt(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+ if (this->getType() != int_) {
+ BaseExpression::getValueAsInt(booleanVariableValues, integerVariableValues);
+ }
+
+ int_fast64_t resultChild = child->getValueAsInt(booleanVariableValues, integerVariableValues);
+ switch(functionType) {
+ case MINUS: return -resultChild; break;
+ default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
+ << "Unknown numerical unary operator: '" << functionType << "'.";
+ }
+ }
+
+ virtual double getValueAsDouble(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+ if (this->getType() != double_) {
+ BaseExpression::getValueAsDouble(booleanVariableValues, integerVariableValues);
+ }
+
+ double resultChild = child->getValueAsDouble(booleanVariableValues, integerVariableValues);
+ switch(functionType) {
+ case MINUS: return -resultChild; break;
+ default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
+ << "Unknown numerical unary operator: '" << functionType << "'.";
+ }
+ }
+
virtual std::string toString() const {
std::string result = "";
- switch (functor) {
+ switch (functionType) {
case MINUS: result += "-"; break;
}
result += child->toString();
return result;
}
+
+private:
+ std::shared_ptr<BaseExpression> child;
+ FunctionType functionType;
};
}
diff --git a/src/ir/expressions/VariableExpression.h b/src/ir/expressions/VariableExpression.h
index a6a27fa43..02ca79a36 100644
--- a/src/ir/expressions/VariableExpression.h
+++ b/src/ir/expressions/VariableExpression.h
@@ -20,9 +20,7 @@ namespace expressions {
class VariableExpression : public BaseExpression {
public:
- std::string variableName;
-
- VariableExpression(std::string variableName) : variableName(variableName) {
+ VariableExpression(ReturnType type, uint_fast64_t index, std::string variableName) : BaseExpression(type), index(index), variableName(variableName) {
}
@@ -33,6 +31,35 @@ public:
virtual std::string toString() const {
return variableName;
}
+
+ virtual int_fast64_t getValueAsInt(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+ if (this->getType() != int_) {
+ BaseExpression::getValueAsInt(booleanVariableValues, integerVariableValues);
+ }
+
+ return integerVariableValues[index];
+ }
+
+ virtual bool getValueAsBool(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+ if (this->getType() != bool_) {
+ BaseExpression::getValueAsBool(booleanVariableValues, integerVariableValues);
+ }
+
+ return booleanVariableValues[index];
+ }
+
+ virtual double getValueAsDouble(std::vector<bool> const& booleanVariableValues, std::vector<int_fast64_t> const& integerVariableValues) const {
+ if (this->getType() != double_) {
+ BaseExpression::getValueAsDouble(booleanVariableValues, integerVariableValues);
+ }
+
+ throw storm::exceptions::NotImplementedException() << "Cannot evaluate expression with "
+ << " variable '" << variableName << "' of type double.";
+ }
+
+private:
+ uint_fast64_t index;
+ std::string variableName;
};
}
diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp
index 96ae88ca7..fe6c4fd8e 100644
--- a/src/parser/PrismParser.cpp
+++ b/src/parser/PrismParser.cpp
@@ -51,7 +51,7 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, storm::ir::Program(), q
* TODO: It should be ensured that updates of a command only refer to variables of the
* current module.
*/
- PrismGrammar() : PrismGrammar::base_type(start) {
+ PrismGrammar() : PrismGrammar::base_type(start), nextBooleanVariableIndex(0), nextIntegerVariableIndex(0) {
// This rule defines all identifiers that have not been previously used.
freeIdentifierName %= qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_'))) - booleanVariableNames_ - integerVariableNames_ - allConstantNames_ - labelNames_ - moduleNames_ - keywords_]];
freeIdentifierName.name("unused identifier");
@@ -87,9 +87,9 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, storm::ir::Program(), q
// This block defines all expressions of integral type.
atomicIntegerExpression %= (integerVariableExpression | qi::lit("(") >> integerExpression >> qi::lit(")") | integerConstantExpression);
atomicIntegerExpression.name("integer expression");
- integerMultExpression %= atomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicIntegerExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))];
+ integerMultExpression %= atomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicIntegerExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(storm::ir::expressions::BaseExpression::int_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))];
integerMultExpression.name("integer expression");
- integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> integerMultExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))];
+ integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> integerMultExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(storm::ir::expressions::BaseExpression::int_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))];
integerPlusExpression.name("integer expression");
integerExpression %= integerPlusExpression;
integerExpression.name("integer expression");
@@ -97,9 +97,9 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, storm::ir::Program(), q
// This block defines all expressions of integral type that are by syntax constant. That is, they are evaluable given the values for all constants.
constantAtomicIntegerExpression %= (qi::lit("(") >> constantIntegerExpression >> qi::lit(")") | integerConstantExpression);
constantAtomicIntegerExpression.name("constant integer expression");
- constantIntegerMultExpression %= constantAtomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicIntegerExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))];
+ constantIntegerMultExpression %= constantAtomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicIntegerExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(storm::ir::expressions::BaseExpression::int_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))];
constantIntegerMultExpression.name("constant integer expression");
- constantIntegerPlusExpression = constantIntegerMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> constantIntegerMultExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))];
+ constantIntegerPlusExpression = constantIntegerMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> constantIntegerMultExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(storm::ir::expressions::BaseExpression::int_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))];
constantIntegerPlusExpression.name("constant integer expression");
constantIntegerExpression %= constantIntegerPlusExpression;
constantIntegerExpression.name("constant integer expression");
@@ -107,9 +107,9 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, storm::ir::Program(), q
// This block defines all expressions of type double that are by syntax constant. That is, they are evaluable given the values for all constants.
constantAtomicDoubleExpression %= (qi::lit("(") >> constantDoubleExpression >> qi::lit(")") | doubleConstantExpression);
constantAtomicDoubleExpression.name("constant double expression");
- constantDoubleMultExpression %= constantAtomicDoubleExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicDoubleExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))];
+ constantDoubleMultExpression %= constantAtomicDoubleExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicDoubleExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(storm::ir::expressions::BaseExpression::double_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))];
constantDoubleMultExpression.name("constant double expression");
- constantDoublePlusExpression %= constantDoubleMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> constantDoubleMultExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))];
+ constantDoublePlusExpression %= constantDoubleMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> constantDoubleMultExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(storm::ir::expressions::BaseExpression::double_, qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))];
constantDoublePlusExpression.name("constant double expression");
constantDoubleExpression %= constantDoublePlusExpression;
constantDoubleExpression.name("constant double expression");
@@ -119,7 +119,7 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, storm::ir::Program(), q
relativeExpression.name("boolean expression");
atomicBooleanExpression %= (relativeExpression | booleanVariableExpression | qi::lit("(") >> booleanExpression >> qi::lit(")") | booleanConstantExpression);
atomicBooleanExpression.name("boolean expression");
- notExpression = atomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicBooleanExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::UnaryBooleanFunctionExpression>>(phoenix::new_<storm::ir::expressions::UnaryBooleanFunctionExpression>(qi::_1, storm::ir::expressions::UnaryBooleanFunctionExpression::FunctorType::NOT))];
+ notExpression = atomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicBooleanExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::UnaryBooleanFunctionExpression>>(phoenix::new_<storm::ir::expressions::UnaryBooleanFunctionExpression>(qi::_1, storm::ir::expressions::UnaryBooleanFunctionExpression::NOT))];
notExpression.name("boolean expression");
andExpression = notExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> notExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryBooleanFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::AND))];
andExpression.name("boolean expression");
@@ -133,7 +133,7 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, storm::ir::Program(), q
constantRelativeExpression.name("constant boolean expression");
constantAtomicBooleanExpression %= (constantRelativeExpression | qi::lit("(") >> constantBooleanExpression >> qi::lit(")") | booleanLiteralExpression | booleanConstantExpression);
constantAtomicBooleanExpression.name("constant boolean expression");
- constantNotExpression = constantAtomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> constantAtomicBooleanExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::UnaryBooleanFunctionExpression>>(phoenix::new_<storm::ir::expressions::UnaryBooleanFunctionExpression>(qi::_1, storm::ir::expressions::UnaryBooleanFunctionExpression::FunctorType::NOT))];
+ constantNotExpression = constantAtomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> constantAtomicBooleanExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::UnaryBooleanFunctionExpression>>(phoenix::new_<storm::ir::expressions::UnaryBooleanFunctionExpression>(qi::_1, storm::ir::expressions::UnaryBooleanFunctionExpression::NOT))];
constantNotExpression.name("constant boolean expression");
constantAndExpression = constantNotExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> constantNotExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryBooleanFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::AND))];
constantAndExpression.name("constant boolean expression");
@@ -175,11 +175,11 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, storm::ir::Program(), q
unassignedLocalIntegerVariableName.name("unassigned local integer variable");
// This block defines all entities that are needed for parsing a single command.
- assignmentDefinition = (qi::lit("(") >> unassignedLocalIntegerVariableName > qi::lit("'") > qi::lit("=") > integerExpression > qi::lit(")"))[phoenix::bind(assignedLocalIntegerVariables_.add, qi::_1, qi::_1), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, storm::ir::Assignment>>(qi::_1, phoenix::construct<storm::ir::Assignment>(qi::_1, qi::_2)))] | (qi::lit("(") > unassignedLocalBooleanVariableName > qi::lit("'") > qi::lit("=") > booleanExpression > qi::lit(")"))[phoenix::bind(assignedLocalBooleanVariables_.add, qi::_1, qi::_1), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, storm::ir::Assignment>>(qi::_1, phoenix::construct<storm::ir::Assignment>(qi::_1, qi::_2)))];
+ assignmentDefinition = (qi::lit("(") >> unassignedLocalIntegerVariableName > qi::lit("'") > qi::lit("=") > integerExpression > qi::lit(")"))[phoenix::bind(assignedLocalIntegerVariables_.add, qi::_1, qi::_1), phoenix::insert(qi::_r2, phoenix::construct<std::pair<std::string, storm::ir::Assignment>>(qi::_1, phoenix::construct<storm::ir::Assignment>(qi::_1, qi::_2)))] | (qi::lit("(") > unassignedLocalBooleanVariableName > qi::lit("'") > qi::lit("=") > booleanExpression > qi::lit(")"))[phoenix::bind(assignedLocalBooleanVariables_.add, qi::_1, qi::_1), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, storm::ir::Assignment>>(qi::_1, phoenix::construct<storm::ir::Assignment>(qi::_1, qi::_2)))];
assignmentDefinition.name("assignment");
- assignmentDefinitionList = assignmentDefinition(qi::_r1) % "&";
+ assignmentDefinitionList = assignmentDefinition(qi::_r1, qi::_r2) % "&";
assignmentDefinitionList.name("assignment list");
- updateDefinition = (constantDoubleExpression > qi::lit(":")[phoenix::clear(phoenix::ref(assignedLocalBooleanVariables_)), phoenix::clear(phoenix::ref(assignedLocalIntegerVariables_))] > assignmentDefinitionList(qi::_a))[qi::_val = phoenix::construct<storm::ir::Update>(qi::_1, qi::_a)];
+ updateDefinition = (constantDoubleExpression > qi::lit(":")[phoenix::clear(phoenix::ref(assignedLocalBooleanVariables_)), phoenix::clear(phoenix::ref(assignedLocalIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::construct<storm::ir::Update>(qi::_1, qi::_a, qi::_b)];
updateDefinition.name("update");
updateListDefinition = +updateDefinition % "+";
updateListDefinition.name("update list");
@@ -187,15 +187,15 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, storm::ir::Program(), q
commandDefinition.name("command");
// This block defines all entities that are neede for parsing variable definitions.
- booleanVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > constantBooleanExpression[qi::_b = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(qi::_1)]) > qi::lit(";"))[phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, storm::ir::BooleanVariable>>(qi::_1, phoenix::construct<storm::ir::BooleanVariable>(phoenix::val(qi::_1), qi::_b))), qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::VariableExpression>>(phoenix::new_<storm::ir::expressions::VariableExpression>(qi::_1)), phoenix::bind(booleanVariables_.add, qi::_1, qi::_a), phoenix::bind(booleanVariableNames_.add, qi::_1, qi::_1), phoenix::bind(localBooleanVariables_.add, qi::_1, qi::_1)];
+ booleanVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > constantBooleanExpression[qi::_b = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(qi::_1)]) > qi::lit(";"))[phoenix::push_back(qi::_r1, phoenix::construct<storm::ir::BooleanVariable>(phoenix::val(nextBooleanVariableIndex), phoenix::val(qi::_1), qi::_b)), phoenix::insert(qi::_r2, phoenix::construct<std::pair<std::string, uint_fast64_t>>(qi::_1, phoenix::val(nextBooleanVariableIndex))), qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::VariableExpression>>(phoenix::new_<storm::ir::expressions::VariableExpression>(storm::ir::expressions::BaseExpression::bool_, phoenix::val(nextBooleanVariableIndex), qi::_1)), phoenix::bind(booleanVariables_.add, qi::_1, qi::_a), phoenix::bind(booleanVariableNames_.add, qi::_1, qi::_1), phoenix::bind(localBooleanVariables_.add, qi::_1, qi::_1), phoenix::ref(nextBooleanVariableIndex)++];
booleanVariableDefinition.name("boolean variable declaration");
- integerVariableDefinition = (freeIdentifierName > qi::lit(":") > qi::lit("[") > constantIntegerExpression > qi::lit("..") > constantIntegerExpression > qi::lit("]") > -(qi::lit("init") > constantIntegerExpression[qi::_b = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(qi::_1)]) > qi::lit(";"))[phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, storm::ir::IntegerVariable>>(qi::_1, phoenix::construct<storm::ir::IntegerVariable>(qi::_1, qi::_2, qi::_3, qi::_b))), qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::VariableExpression>>(phoenix::new_<storm::ir::expressions::VariableExpression>(qi::_1)), phoenix::bind(integerVariables_.add, qi::_1, qi::_a), phoenix::bind(integerVariableNames_.add, qi::_1, qi::_1), phoenix::bind(localIntegerVariables_.add, qi::_1, qi::_1)];
+ integerVariableDefinition = (freeIdentifierName > qi::lit(":") > qi::lit("[") > constantIntegerExpression > qi::lit("..") > constantIntegerExpression > qi::lit("]") > -(qi::lit("init") > constantIntegerExpression[qi::_b = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(qi::_1)]) > qi::lit(";"))[phoenix::push_back(qi::_r1, phoenix::construct<storm::ir::IntegerVariable>(phoenix::val(nextIntegerVariableIndex), qi::_1, qi::_2, qi::_3, qi::_b)), phoenix::insert(qi::_r2, phoenix::construct<std::pair<std::string, uint_fast64_t>>(qi::_1, phoenix::val(nextIntegerVariableIndex))), qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::VariableExpression>>(phoenix::new_<storm::ir::expressions::VariableExpression>(storm::ir::expressions::BaseExpression::int_, phoenix::val(nextIntegerVariableIndex), qi::_1)), phoenix::bind(integerVariables_.add, qi::_1, qi::_a), phoenix::bind(integerVariableNames_.add, qi::_1, qi::_1), phoenix::bind(localIntegerVariables_.add, qi::_1, qi::_1), phoenix::ref(nextIntegerVariableIndex)++];
integerVariableDefinition.name("integer variable declaration");
- variableDefinition = (booleanVariableDefinition(qi::_r1) | integerVariableDefinition(qi::_r2));
+ variableDefinition = (booleanVariableDefinition(qi::_r1, qi::_r3) | integerVariableDefinition(qi::_r2, qi::_r4));
variableDefinition.name("variable declaration");
// This block defines all entities that are needed for parsing a module.
- moduleDefinition = (qi::lit("module")[phoenix::clear(phoenix::ref(localBooleanVariables_)), phoenix::clear(phoenix::ref(localIntegerVariables_))] > freeIdentifierName > *(variableDefinition(qi::_a, qi::_b)) > +commandDefinition > qi::lit("endmodule"))[phoenix::bind(moduleNames_.add, qi::_1, qi::_1), qi::_val = phoenix::construct<storm::ir::Module>(qi::_1, qi::_a, qi::_b, qi::_2)];
+ moduleDefinition = (qi::lit("module")[phoenix::clear(phoenix::ref(localBooleanVariables_)), phoenix::clear(phoenix::ref(localIntegerVariables_))] > freeIdentifierName > *(variableDefinition(qi::_a, qi::_b, qi::_c, qi::_d)) > +commandDefinition > qi::lit("endmodule"))[phoenix::bind(moduleNames_.add, qi::_1, qi::_1), qi::_val = phoenix::construct<storm::ir::Module>(qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2)];
moduleDefinition.name("module");
moduleDefinitionList %= +moduleDefinition;
moduleDefinitionList.name("module list");
@@ -234,19 +234,19 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, storm::ir::Program(), q
qi::rule<Iterator, std::vector<storm::ir::Module>(), Skipper> moduleDefinitionList;
// Rules for module definition.
- qi::rule<Iterator, storm::ir::Module(), qi::locals<std::map<std::string, storm::ir::BooleanVariable>, std::map<std::string, storm::ir::IntegerVariable>>, Skipper> moduleDefinition;
+ qi::rule<Iterator, storm::ir::Module(), qi::locals<std::vector<storm::ir::BooleanVariable>, std::vector<storm::ir::IntegerVariable>, std::map<std::string, uint_fast64_t>, std::map<std::string, uint_fast64_t>>, Skipper> moduleDefinition;
// Rules for variable definitions.
- qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::ir::BooleanVariable>&, std::map<std::string, storm::ir::IntegerVariable>&), Skipper> variableDefinition;
- qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::ir::BooleanVariable>&), qi::locals<std::shared_ptr<storm::ir::expressions::VariableExpression>, std::shared_ptr<storm::ir::expressions::BaseExpression>>, Skipper> booleanVariableDefinition;
- qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::ir::IntegerVariable>&), qi::locals<std::shared_ptr<storm::ir::expressions::VariableExpression>, std::shared_ptr<storm::ir::expressions::BaseExpression>>, Skipper> integerVariableDefinition;
+ qi::rule<Iterator, qi::unused_type(std::vector<storm::ir::BooleanVariable>&, std::vector<storm::ir::IntegerVariable>&, std::map<std::string, uint_fast64_t>&, std::map<std::string, uint_fast64_t>&), Skipper> variableDefinition;
+ qi::rule<Iterator, qi::unused_type(std::vector<storm::ir::BooleanVariable>&, std::map<std::string, uint_fast64_t>&), qi::locals<std::shared_ptr<storm::ir::expressions::VariableExpression>, std::shared_ptr<storm::ir::expressions::BaseExpression>>, Skipper> booleanVariableDefinition;
+ qi::rule<Iterator, qi::unused_type(std::vector<storm::ir::IntegerVariable>&, std::map<std::string, uint_fast64_t>&), qi::locals<std::shared_ptr<storm::ir::expressions::VariableExpression>, std::shared_ptr<storm::ir::expressions::BaseExpression>>, Skipper> integerVariableDefinition;
// Rules for command definitions.
qi::rule<Iterator, storm::ir::Command(), qi::locals<std::string>, Skipper> commandDefinition;
qi::rule<Iterator, std::vector<storm::ir::Update>(), Skipper> updateListDefinition;
- qi::rule<Iterator, storm::ir::Update(), qi::locals<std::map<std::string, storm::ir::Assignment>>, Skipper> updateDefinition;
- qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::ir::Assignment>&), Skipper> assignmentDefinitionList;
- qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::ir::Assignment>&), Skipper> assignmentDefinition;
+ qi::rule<Iterator, storm::ir::Update(), qi::locals<std::map<std::string, storm::ir::Assignment>, std::map<std::string, storm::ir::Assignment>>, Skipper> updateDefinition;
+ qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::ir::Assignment>&, std::map<std::string, storm::ir::Assignment>&), Skipper> assignmentDefinitionList;
+ qi::rule<Iterator, qi::unused_type(std::map<std::string, storm::ir::Assignment>&, std::map<std::string, storm::ir::Assignment>&), Skipper> assignmentDefinition;
// Rules for variable/command names.
qi::rule<Iterator, std::string(), Skipper> integerVariableName;
@@ -377,6 +377,10 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, storm::ir::Program(), q
}
} relations_;
+ // Used for indexing the variables.
+ uint_fast64_t nextBooleanVariableIndex;
+ uint_fast64_t nextIntegerVariableIndex;
+
// Structures mapping variable and constant names to the corresponding expression nodes of
// the intermediate representation.
struct qi::symbols<char, std::shared_ptr<storm::ir::expressions::BaseExpression>> integerVariables_, booleanVariables_;
diff --git a/src/storm.cpp b/src/storm.cpp
index c4c75d09a..678189be5 100644
--- a/src/storm.cpp
+++ b/src/storm.cpp
@@ -36,6 +36,7 @@
#include "log4cplus/fileappender.h"
#include "src/parser/PrismParser.h"
+#include "src/adapters/IntermediateRepresentationAdapter.h"
#include "src/exceptions/InvalidSettingsException.h"
@@ -241,7 +242,8 @@ int main(const int argc, const char* argv[]) {
// testChecking();
storm::parser::PrismParser parser;
- parser.parseFile("test.input");
+ std::shared_ptr<storm::ir::Program> program = parser.parseFile("test.input");
+ storm::storage::SquareSparseMatrix<double>* result = storm::adapters::IntermediateRepresentationAdapter::toSparseMatrix<double>(*program);
cleanUp();
return 0;
diff --git a/test.input b/test.input
index 5339a8416..700951a05 100644
--- a/test.input
+++ b/test.input
@@ -1,24 +1,24 @@
+// Knuth's model of a fair die using only fair coins
dtmc
module die
-// local state
-s : [0..7] init 0;
-// value of the dice
-d : [0..6] init 0;
+
+ // local state
+ s : [0..7] init 0;
+ // value of the dice
+ d : [0..6] init 0;
+
+ [] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2);
+ [] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4);
+ [] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6);
+ [] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1);
+ [] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3);
+ [] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5);
+ [] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6);
+ [] s=7 -> 1: (s'=7);
-[] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2);
-[] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4);
-[] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6);
-[] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1);
-[] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3);
-[] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5);
-[] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6);
-[] s=7 -> 1 : (s'=7);
endmodule
rewards "coin_flips"
[] s<7 : 1;
- s>3 : 1;
endrewards
-
-label test = s>2;