Browse Source
Merge branch 'prismparser'
Merge branch 'prismparser'
Conflicts: CMakeLists.txt examples/dtmc/crowds/crowds15_5.pm examples/dtmc/crowds/crowds20_5.pm examples/dtmc/crowds/crowds5_5.pm examples/dtmc/die/die.pm examples/dtmc/synchronous_leader/leader3_5.pm src/parser/PrctlParser.cpp src/parser/PrctlParser.h src/storm.cpp src/utility/Settings.cpp test/parser/ParseMdpTest.cppmain
gereon
12 years ago
83 changed files with 6664 additions and 99 deletions
-
1.gitignore
-
50CMakeLists.txt
-
34examples/dtmc/crowds/crowds15_5.pm
-
44examples/dtmc/crowds/crowds20_5.pm
-
24examples/dtmc/crowds/crowds5_5.pm
-
55examples/dtmc/die/die.pm
-
22examples/dtmc/sync/sync.pm
-
28examples/dtmc/synchronous_leader/leader3_5.pm
-
563src/adapters/ExplicitModelAdapter.cpp
-
206src/adapters/ExplicitModelAdapter.h
-
231src/adapters/SymbolicExpressionAdapter.h
-
289src/adapters/SymbolicModelAdapter.h
-
23src/exceptions/ExpressionEvaluationException.h
-
23src/exceptions/NotImplementedException.h
-
53src/ir/Assignment.cpp
-
68src/ir/Assignment.h
-
45src/ir/BooleanVariable.cpp
-
51src/ir/BooleanVariable.h
-
75src/ir/Command.cpp
-
85src/ir/Command.h
-
25src/ir/IR.h
-
60src/ir/IntegerVariable.cpp
-
72src/ir/IntegerVariable.h
-
182src/ir/Module.cpp
-
171src/ir/Module.h
-
145src/ir/Program.cpp
-
151src/ir/Program.h
-
58src/ir/RewardModel.cpp
-
84src/ir/RewardModel.h
-
42src/ir/StateReward.cpp
-
65src/ir/StateReward.h
-
43src/ir/TransitionReward.cpp
-
68src/ir/TransitionReward.h
-
118src/ir/Update.cpp
-
104src/ir/Update.h
-
58src/ir/Variable.cpp
-
85src/ir/Variable.h
-
105src/ir/expressions/BaseExpression.h
-
91src/ir/expressions/BinaryBooleanFunctionExpression.h
-
46src/ir/expressions/BinaryExpression.h
-
112src/ir/expressions/BinaryNumericalFunctionExpression.h
-
98src/ir/expressions/BinaryRelationExpression.h
-
89src/ir/expressions/BooleanConstantExpression.h
-
62src/ir/expressions/BooleanLiteral.h
-
55src/ir/expressions/ConstantExpression.h
-
87src/ir/expressions/DoubleConstantExpression.h
-
62src/ir/expressions/DoubleLiteral.h
-
55src/ir/expressions/ExpressionVisitor.h
-
26src/ir/expressions/Expressions.h
-
85src/ir/expressions/IntegerConstantExpression.h
-
57src/ir/expressions/IntegerLiteral.h
-
81src/ir/expressions/UnaryBooleanFunctionExpression.h
-
39src/ir/expressions/UnaryExpression.h
-
99src/ir/expressions/UnaryNumericalFunctionExpression.h
-
146src/ir/expressions/VariableExpression.h
-
8src/models/Mdp.h
-
128src/parser/PrismParser.cpp
-
52src/parser/PrismParser.h
-
112src/parser/PrismParser/BaseGrammar.h
-
42src/parser/PrismParser/BooleanExpressionGrammar.cpp
-
44src/parser/PrismParser/BooleanExpressionGrammar.h
-
54src/parser/PrismParser/ConstBooleanExpressionGrammar.cpp
-
50src/parser/PrismParser/ConstBooleanExpressionGrammar.h
-
53src/parser/PrismParser/ConstDoubleExpressionGrammar.cpp
-
43src/parser/PrismParser/ConstDoubleExpressionGrammar.h
-
35src/parser/PrismParser/ConstIntegerExpressionGrammar.cpp
-
37src/parser/PrismParser/ConstIntegerExpressionGrammar.h
-
23src/parser/PrismParser/IdentifierGrammars.cpp
-
36src/parser/PrismParser/IdentifierGrammars.h
-
41src/parser/PrismParser/Includes.h
-
36src/parser/PrismParser/IntegerExpressionGrammar.cpp
-
40src/parser/PrismParser/IntegerExpressionGrammar.h
-
258src/parser/PrismParser/PrismGrammar.cpp
-
142src/parser/PrismParser/PrismGrammar.h
-
70src/parser/PrismParser/Tokens.h
-
171src/parser/PrismParser/VariableState.cpp
-
71src/parser/PrismParser/VariableState.h
-
28src/storm.cpp
-
195src/utility/CuddUtility.cpp
-
63src/utility/CuddUtility.h
-
1src/utility/Settings.cpp
-
2test/parser/ParseMdpTest.cpp
-
32test/parser/ParsePrismTest.cpp
@ -1,31 +1,24 @@ |
|||
dtmc |
|||
|
|||
module die |
|||
|
|||
// local state |
|||
s : [0..7] init 0; |
|||
// value of the die |
|||
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 -> (s'=7); |
|||
|
|||
endmodule |
|||
|
|||
rewards "coin_flips" |
|||
[] s<7 : 1; |
|||
endrewards |
|||
|
|||
label "one" = s=7&d=1; |
|||
label "two" = s=7&d=2; |
|||
label "three" = s=7&d=3; |
|||
label "four" = s=7&d=4; |
|||
label "five" = s=7&d=5; |
|||
label "six" = s=7&d=6; |
|||
label "done" = s=7; |
|||
// 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; |
|||
|
|||
[] 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; |
|||
endrewards |
|||
@ -0,0 +1,22 @@ |
|||
// A simple model using synchronization |
|||
dtmc |
|||
|
|||
module generator |
|||
|
|||
s : [0..2] init 0; |
|||
|
|||
[] s=0 -> 0.2 : (s'=1) + 0.8 : (s'=0); |
|||
[yield] s=1 -> 1 : (s'=2); |
|||
[] s=2 -> 0.5 : (s'=0) + 0.5 : (s'=2); |
|||
|
|||
endmodule |
|||
|
|||
module consumer |
|||
|
|||
t : [0..2] init 0; |
|||
|
|||
[] t=0 -> 0.8 : (t'=1) + 0.2 : (t'=0); |
|||
[yield] t=1 -> 1 : (t'=2); |
|||
[] t=2 -> 0.2 : (t'=0) + 0.8 : (t'=2); |
|||
|
|||
endmodule |
|||
@ -0,0 +1,563 @@ |
|||
#include "src/adapters/ExplicitModelAdapter.h"
|
|||
|
|||
#include "src/storage/SparseMatrix.h"
|
|||
#include "src/utility/Settings.h"
|
|||
#include "src/exceptions/WrongFileFormatException.h"
|
|||
|
|||
#include "src/ir/Program.h"
|
|||
#include "src/ir/RewardModel.h"
|
|||
#include "src/ir/StateReward.h"
|
|||
#include "src/ir/TransitionReward.h"
|
|||
|
|||
#include "src/models/AbstractModel.h"
|
|||
#include "src/models/Dtmc.h"
|
|||
#include "src/models/Ctmc.h"
|
|||
#include "src/models/Mdp.h"
|
|||
|
|||
typedef std::pair<std::vector<bool>, std::vector<int_fast64_t>> StateType; |
|||
|
|||
#include <sstream>
|
|||
|
|||
#include "log4cplus/logger.h"
|
|||
#include "log4cplus/loggingmacros.h"
|
|||
extern log4cplus::Logger logger; |
|||
|
|||
namespace storm { |
|||
|
|||
namespace adapters { |
|||
|
|||
ExplicitModelAdapter::ExplicitModelAdapter(storm::ir::Program program) : program(program), |
|||
booleanVariables(), integerVariables(), booleanVariableToIndexMap(), integerVariableToIndexMap(), |
|||
allStates(), stateToIndexMap(), numberOfTransitions(0), numberOfChoices(0), transitionRewards(nullptr), transitionMap() { |
|||
this->initializeVariables(); |
|||
storm::settings::Settings* s = storm::settings::instance(); |
|||
this->precision = s->get<double>("precision"); |
|||
} |
|||
|
|||
ExplicitModelAdapter::~ExplicitModelAdapter() { |
|||
this->clearInternalState(); |
|||
} |
|||
|
|||
std::shared_ptr<storm::models::AbstractModel> ExplicitModelAdapter::getModel(std::string const & rewardModelName) { |
|||
|
|||
|
|||
this->buildTransitionMap(); |
|||
|
|||
std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling = this->getStateLabeling(this->program.getLabels()); |
|||
std::shared_ptr<std::vector<double>> stateRewards = nullptr; |
|||
|
|||
this->rewardModel = nullptr; |
|||
if (rewardModelName != "") { |
|||
this->rewardModel = std::unique_ptr<storm::ir::RewardModel>(new storm::ir::RewardModel(this->program.getRewardModel(rewardModelName)));; |
|||
if (this->rewardModel != nullptr) { |
|||
if (this->rewardModel->hasStateRewards()) { |
|||
stateRewards = this->getStateRewards(this->rewardModel->getStateRewards()); |
|||
} |
|||
} |
|||
} |
|||
|
|||
switch (this->program.getModelType()) |
|||
{ |
|||
case storm::ir::Program::DTMC: |
|||
{ |
|||
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix = this->buildDeterministicMatrix(); |
|||
return std::shared_ptr<storm::models::AbstractModel>(new storm::models::Dtmc<double>(matrix, stateLabeling, stateRewards, this->transitionRewards)); |
|||
break; |
|||
} |
|||
case storm::ir::Program::CTMC: |
|||
{ |
|||
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix = this->buildDeterministicMatrix(); |
|||
return std::shared_ptr<storm::models::AbstractModel>(new storm::models::Ctmc<double>(matrix, stateLabeling, stateRewards, this->transitionRewards)); |
|||
break; |
|||
} |
|||
case storm::ir::Program::MDP: |
|||
{ |
|||
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix = this->buildNondeterministicMatrix(); |
|||
return std::shared_ptr<storm::models::AbstractModel>(new storm::models::Mdp<double>(matrix, stateLabeling, stateRewards, this->transitionRewards)); |
|||
break; |
|||
} |
|||
case storm::ir::Program::CTMDP: |
|||
// Todo
|
|||
//return std::shared_ptr<storm::models::AbstractModel>(new storm::models::Ctmdp<double>(matrix, stateLabeling, stateRewards, transitionRewardMatrix));
|
|||
break; |
|||
default: |
|||
LOG4CPLUS_ERROR(logger, "Error while creating model from probabilistic program: We can't handle this model type."); |
|||
throw storm::exceptions::WrongFileFormatException() << "Error while creating model from probabilistic program: We can't handle this model type."; |
|||
break; |
|||
} |
|||
|
|||
return std::shared_ptr<storm::models::AbstractModel>(nullptr); |
|||
} |
|||
|
|||
void ExplicitModelAdapter::setValue(StateType* const state, uint_fast64_t const index, bool const value) { |
|||
std::get<0>(*state)[index] = value; |
|||
} |
|||
|
|||
void ExplicitModelAdapter::setValue(StateType* const state, uint_fast64_t const index, int_fast64_t const value) { |
|||
std::get<1>(*state)[index] = value; |
|||
} |
|||
|
|||
std::string ExplicitModelAdapter::toString(StateType const * const state) { |
|||
std::stringstream ss; |
|||
for (unsigned int i = 0; i < state->first.size(); i++) ss << state->first[i] << "\t"; |
|||
for (unsigned int i = 0; i < state->second.size(); i++) ss << state->second[i] << "\t"; |
|||
return ss.str(); |
|||
} |
|||
|
|||
std::shared_ptr<std::vector<double>> ExplicitModelAdapter::getStateRewards(std::vector<storm::ir::StateReward> const & rewards) { |
|||
std::shared_ptr<std::vector<double>> results(new std::vector<double>(this->allStates.size())); |
|||
for (uint_fast64_t index = 0; index < this->allStates.size(); index++) { |
|||
for (auto reward: rewards) { |
|||
(*results)[index] = reward.getReward(this->allStates[index]); |
|||
} |
|||
} |
|||
return results; |
|||
} |
|||
|
|||
std::shared_ptr<storm::models::AtomicPropositionsLabeling> ExplicitModelAdapter::getStateLabeling(std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> labels) { |
|||
std::shared_ptr<storm::models::AtomicPropositionsLabeling> results(new storm::models::AtomicPropositionsLabeling(this->allStates.size(), labels.size())); |
|||
for (auto it: labels) { |
|||
results->addAtomicProposition(it.first); |
|||
} |
|||
for (uint_fast64_t index = 0; index < this->allStates.size(); index++) { |
|||
for (auto label: labels) { |
|||
if (label.second->getValueAsBool(this->allStates[index])) { |
|||
results->addAtomicPropositionToState(label.first, index); |
|||
} |
|||
} |
|||
} |
|||
return results; |
|||
} |
|||
|
|||
void ExplicitModelAdapter::initializeVariables() { |
|||
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(); |
|||
} |
|||
|
|||
this->booleanVariables.resize(numberOfBooleanVariables); |
|||
this->integerVariables.resize(numberOfIntegerVariables); |
|||
|
|||
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) { |
|||
storm::ir::BooleanVariable var = module.getBooleanVariable(j); |
|||
this->booleanVariables[var.getIndex()] = var; |
|||
this->booleanVariableToIndexMap[var.getName()] = var.getIndex(); |
|||
} |
|||
for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) { |
|||
storm::ir::IntegerVariable var = module.getIntegerVariable(j); |
|||
this->integerVariables[var.getIndex()] = var; |
|||
this->integerVariableToIndexMap[var.getName()] = var.getIndex(); |
|||
} |
|||
} |
|||
} |
|||
|
|||
/*!
|
|||
* Retrieves all active command labeled by some label, ordered by modules. |
|||
* |
|||
* This function will iterate over all modules and retrieve all commands that are labeled with the given action and active for the current state. |
|||
* The result will be a list of lists of commands. |
|||
* |
|||
* For each module that has appropriately labeled commands, there will be a list. |
|||
* If none of these commands is active, this list is empty. |
|||
* Note the difference between *no list* and *empty list*: Modules that produce no list are not relevant for this action while an empty list means, that it is not possible to do anything with this label. |
|||
* @param state Current state. |
|||
* @param action Action label. |
|||
* @return Active commands. |
|||
*/ |
|||
std::unique_ptr<std::list<std::list<storm::ir::Command>>> ExplicitModelAdapter::getActiveCommandsByAction(StateType const * state, std::string& action) { |
|||
std::unique_ptr<std::list<std::list<storm::ir::Command>>> res = std::unique_ptr<std::list<std::list<storm::ir::Command>>>(new std::list<std::list<storm::ir::Command>>()); |
|||
|
|||
// Iterate over all modules.
|
|||
for (uint_fast64_t i = 0; i < this->program.getNumberOfModules(); ++i) { |
|||
storm::ir::Module const& module = this->program.getModule(i); |
|||
|
|||
std::shared_ptr<std::set<uint_fast64_t>> ids = module.getCommandsByAction(action); |
|||
if (ids->size() == 0) continue; |
|||
std::list<storm::ir::Command> commands; |
|||
|
|||
// Look up commands by their id. Add, if guard holds.
|
|||
for (uint_fast64_t id : *ids) { |
|||
storm::ir::Command cmd = module.getCommand(id); |
|||
if (cmd.getGuard()->getValueAsBool(state)) { |
|||
commands.push_back(module.getCommand(id)); |
|||
} |
|||
} |
|||
res->push_back(commands); |
|||
} |
|||
// Sort the result in the vague hope that having small lists at the beginning will speed up the expanding.
|
|||
// This is how lambdas may look like in C++...
|
|||
res->sort([](const std::list<storm::ir::Command>& a, const std::list<storm::ir::Command>& b){ return a.size() < b.size(); }); |
|||
return res; |
|||
} |
|||
|
|||
/*!
|
|||
* Apply an update to the given state and return resulting state. |
|||
* @params state Current state. |
|||
* @params update Update to be applied. |
|||
* @return Resulting state. |
|||
*/ |
|||
StateType* ExplicitModelAdapter::applyUpdate(StateType const * const state, storm::ir::Update const& update) const { |
|||
return this->applyUpdate(state, state, update); |
|||
} |
|||
|
|||
StateType* ExplicitModelAdapter::applyUpdate(StateType const * const state, StateType const * const baseState, storm::ir::Update const& update) const { |
|||
StateType* newState = new StateType(*state); |
|||
for (auto assignedVariable : update.getBooleanAssignments()) { |
|||
setValue(newState, this->booleanVariableToIndexMap.at(assignedVariable.first), assignedVariable.second.getExpression()->getValueAsBool(baseState)); |
|||
} |
|||
for (auto assignedVariable : update.getIntegerAssignments()) { |
|||
setValue(newState, this->integerVariableToIndexMap.at(assignedVariable.first), assignedVariable.second.getExpression()->getValueAsInt(baseState)); |
|||
} |
|||
return newState; |
|||
} |
|||
|
|||
/*!
|
|||
* Generates all initial states and adds them to allStates. |
|||
*/ |
|||
void ExplicitModelAdapter::generateInitialStates() { |
|||
// Create a fresh state which can hold as many boolean and integer variables as there are.
|
|||
this->allStates.clear(); |
|||
this->allStates.push_back(new StateType()); |
|||
this->allStates[0]->first.resize(this->booleanVariables.size()); |
|||
this->allStates[0]->second.resize(this->integerVariables.size()); |
|||
|
|||
// Start with boolean variables.
|
|||
for (uint_fast64_t i = 0; i < this->booleanVariables.size(); ++i) { |
|||
// Check if an initial value is given
|
|||
if (this->booleanVariables[i].getInitialValue().get() == nullptr) { |
|||
// No initial value was given.
|
|||
uint_fast64_t size = this->allStates.size(); |
|||
for (uint_fast64_t pos = 0; pos < size; pos++) { |
|||
// Duplicate each state, one with true and one with false.
|
|||
this->allStates.push_back(new StateType(*this->allStates[pos])); |
|||
std::get<0>(*this->allStates[pos])[i] = false; |
|||
std::get<0>(*this->allStates[size + pos])[i] = true; |
|||
} |
|||
} else { |
|||
// Initial value was given.
|
|||
bool initialValue = this->booleanVariables[i].getInitialValue()->getValueAsBool(this->allStates[0]); |
|||
for (auto it : this->allStates) { |
|||
std::get<0>(*it)[i] = initialValue; |
|||
} |
|||
} |
|||
} |
|||
// Now process integer variables.
|
|||
for (uint_fast64_t i = 0; i < this->integerVariables.size(); ++i) { |
|||
// Check if an initial value was given.
|
|||
if (this->integerVariables[i].getInitialValue().get() == nullptr) { |
|||
// No initial value was given.
|
|||
uint_fast64_t size = this->allStates.size(); |
|||
int_fast64_t lower = this->integerVariables[i].getLowerBound()->getValueAsInt(this->allStates[0]); |
|||
int_fast64_t upper = this->integerVariables[i].getUpperBound()->getValueAsInt(this->allStates[0]); |
|||
|
|||
// Duplicate all states for all values in variable interval.
|
|||
for (int_fast64_t value = lower; value <= upper; value++) { |
|||
for (uint_fast64_t pos = 0; pos < size; pos++) { |
|||
// If value is lower bound, we reuse the existing state, otherwise we create a new one.
|
|||
if (value > lower) this->allStates.push_back(new StateType(*this->allStates[pos])); |
|||
// Set value to current state.
|
|||
std::get<1>(*this->allStates[(value - lower) * size + pos])[i] = value; |
|||
} |
|||
} |
|||
} else { |
|||
// Initial value was given.
|
|||
int_fast64_t initialValue = this->integerVariables[i].getInitialValue()->getValueAsInt(this->allStates[0]); |
|||
for (auto it : this->allStates) { |
|||
std::get<1>(*it)[i] = initialValue; |
|||
} |
|||
} |
|||
} |
|||
stateToIndexMap[this->allStates[0]] = 0; |
|||
LOG4CPLUS_DEBUG(logger, "Generated " << this->allStates.size() << " initial states."); |
|||
} |
|||
|
|||
/*!
|
|||
* Retrieves the state id of the given state. |
|||
* If the state has not been hit yet, it will be added to allStates and given a new id. |
|||
* In this case, the pointer must not be deleted, as it is used within allStates. |
|||
* If the state is already known, the pointer is deleted and the old state id is returned. |
|||
* Hence, the given state pointer should not be used afterwards. |
|||
* @param state Pointer to state, shall not be used afterwards. |
|||
* @returns State id of given state. |
|||
*/ |
|||
uint_fast64_t ExplicitModelAdapter::getOrAddStateId(StateType * state) { |
|||
// Check, if we already know this state at all.
|
|||
auto indexIt = this->stateToIndexMap.find(state); |
|||
if (indexIt == this->stateToIndexMap.end()) { |
|||
// No, add to allStates, initialize index.
|
|||
allStates.push_back(state); |
|||
stateToIndexMap[state] = allStates.size()-1; |
|||
return allStates.size()-1; |
|||
} else { |
|||
// Yes, obtain index and delete state object.
|
|||
delete state; |
|||
return indexIt->second; |
|||
} |
|||
} |
|||
|
|||
/*!
|
|||
* Expands all unlabeled transitions for a given state and adds them to the given list of results. |
|||
* @params state State to be explored. |
|||
* @params res Intermediate transition map. |
|||
*/ |
|||
void ExplicitModelAdapter::addUnlabeledTransitions(const uint_fast64_t stateID, std::list<std::pair<std::string, std::map<uint_fast64_t, double>>>& res) { |
|||
const StateType* state = this->allStates[stateID]; |
|||
// 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); |
|||
// Only consider unlabeled commands.
|
|||
if (command.getActionName() != "") continue; |
|||
// Omit, if command is not active.
|
|||
if (!command.getGuard()->getValueAsBool(state)) continue; |
|||
|
|||
// Add a new map and get pointer.
|
|||
res.emplace_back(); |
|||
std::map<uint_fast64_t, double>* states = &res.back().second; |
|||
double probSum = 0; |
|||
|
|||
// Iterate over all updates.
|
|||
for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) { |
|||
// Obtain new state id.
|
|||
storm::ir::Update const& update = command.getUpdate(k); |
|||
uint_fast64_t newStateId = this->getOrAddStateId(this->applyUpdate(state, update)); |
|||
|
|||
probSum += update.getLikelihoodExpression()->getValueAsDouble(state); |
|||
// Check, if we already know this state, add up probabilities for every state.
|
|||
auto stateIt = states->find(newStateId); |
|||
if (stateIt == states->end()) { |
|||
(*states)[newStateId] = update.getLikelihoodExpression()->getValueAsDouble(state); |
|||
this->numberOfTransitions++; |
|||
} else { |
|||
(*states)[newStateId] += update.getLikelihoodExpression()->getValueAsDouble(state); |
|||
} |
|||
} |
|||
if (std::abs(1 - probSum) > this->precision) { |
|||
LOG4CPLUS_ERROR(logger, "Sum of update probabilities should be one for command:\n\t" << command.toString()); |
|||
throw storm::exceptions::WrongFileFormatException() << "Sum of update probabilities should be one for command:\n\t" << command.toString(); |
|||
} |
|||
} |
|||
} |
|||
} |
|||
|
|||
/*!
|
|||
* Explores reachable state from given state by using labeled transitions. |
|||
* Found transitions are stored in given map. |
|||
* @param stateID State to be explored. |
|||
* @param res Intermediate transition map. |
|||
*/ |
|||
void ExplicitModelAdapter::addLabeledTransitions(const uint_fast64_t stateID, std::list<std::pair<std::string, std::map<uint_fast64_t, double>>>& res) { |
|||
// Create a copy of the current state, as we will free intermediate states...
|
|||
for (std::string action : this->program.getActions()) { |
|||
StateType* state = new StateType(*this->allStates[stateID]); |
|||
std::unique_ptr<std::list<std::list<storm::ir::Command>>> cmds = this->getActiveCommandsByAction(state, action); |
|||
|
|||
// Start with current state
|
|||
std::unordered_map<StateType*, double, StateHash, StateCompare> resultStates; |
|||
resultStates[state] = 1.0; |
|||
|
|||
for (std::list<storm::ir::Command> module : *cmds) { |
|||
if (resultStates.size() == 0) break; |
|||
std::unordered_map<StateType*, double, StateHash, StateCompare> newStates; |
|||
|
|||
// Iterate over all commands within this module.
|
|||
for (storm::ir::Command command : module) { |
|||
// Iterate over all updates of this command.
|
|||
double probSum = 0; |
|||
for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) { |
|||
storm::ir::Update const update = command.getUpdate(k); |
|||
|
|||
// Iterate over all resultStates.
|
|||
for (auto it : resultStates) { |
|||
// Apply the new update and get resulting state.
|
|||
StateType* newState = this->applyUpdate(it.first, this->allStates[stateID], update); |
|||
probSum += update.getLikelihoodExpression()->getValueAsDouble(it.first); |
|||
// Insert the new state into newStates array.
|
|||
// Take care of calculation of likelihood, combine identical states.
|
|||
auto s = newStates.find(newState); |
|||
if (s == newStates.end()) { |
|||
newStates[newState] = it.second * update.getLikelihoodExpression()->getValueAsDouble(it.first); |
|||
} else { |
|||
newStates[newState] += it.second * update.getLikelihoodExpression()->getValueAsDouble(it.first); |
|||
} |
|||
} |
|||
} |
|||
if (std::abs(1 - probSum) > this->precision) { |
|||
LOG4CPLUS_ERROR(logger, "Sum of update probabilities should be one for command:\n\t" << command.toString()); |
|||
throw storm::exceptions::WrongFileFormatException() << "Sum of update probabilities should be one for command:\n\t" << command.toString(); |
|||
} |
|||
} |
|||
for (auto it: resultStates) { |
|||
delete it.first; |
|||
} |
|||
// Move new states to resultStates.
|
|||
resultStates.clear(); |
|||
resultStates.insert(newStates.begin(), newStates.end()); |
|||
|
|||
} |
|||
|
|||
if (resultStates.size() > 0) { |
|||
res.push_back(std::make_pair(action, std::map<uint_fast64_t, double>())); |
|||
std::map<uint_fast64_t, double>* states = &res.back().second; |
|||
|
|||
// Now add our final result states to our global result.
|
|||
for (auto it : resultStates) { |
|||
uint_fast64_t newStateID = this->getOrAddStateId(it.first); |
|||
(*states)[newStateID] = it.second; |
|||
} |
|||
this->numberOfTransitions += states->size(); |
|||
} |
|||
} |
|||
|
|||
} |
|||
|
|||
/*!
|
|||
* Create matrix from intermediate mapping, assuming it is a dtmc model. |
|||
* @param intermediate Intermediate representation of transition mapping. |
|||
* @return result matrix. |
|||
*/ |
|||
std::shared_ptr<storm::storage::SparseMatrix<double>> ExplicitModelAdapter::buildDeterministicMatrix() { |
|||
// ***** ATTENTION *****
|
|||
// this->numberOfTransitions is meaningless, as we combine all choices into one for each state.
|
|||
// Hence, we compute the correct number of transitions now.
|
|||
uint_fast64_t numberOfTransitions = 0; |
|||
for (uint_fast64_t state = 0; state < this->allStates.size(); state++) { |
|||
// Collect all target nodes in a set to get number of distinct nodes.
|
|||
std::set<uint_fast64_t> set; |
|||
for (auto choice : transitionMap[state]) { |
|||
for (auto elem : choice.second) { |
|||
set.insert(elem.first); |
|||
} |
|||
} |
|||
numberOfTransitions += set.size(); |
|||
} |
|||
LOG4CPLUS_INFO(logger, "Building deterministic transition matrix: " << allStates.size() << " x " << allStates.size() << " with " << numberOfTransitions << " transitions."); |
|||
// Now build matrix.
|
|||
|
|||
std::shared_ptr<storm::storage::SparseMatrix<double>> result(new storm::storage::SparseMatrix<double>(allStates.size())); |
|||
result->initialize(numberOfTransitions); |
|||
if ((this->rewardModel != nullptr) && (this->rewardModel->hasTransitionRewards())) { |
|||
this->transitionRewards = std::shared_ptr<storm::storage::SparseMatrix<double>>(new storm::storage::SparseMatrix<double>(allStates.size())); |
|||
this->transitionRewards->initialize(numberOfTransitions); |
|||
} |
|||
for (uint_fast64_t state = 0; state < this->allStates.size(); state++) { |
|||
if (transitionMap[state].size() > 1) { |
|||
LOG4CPLUS_WARN(logger, "State " << state << " has " << transitionMap[state].size() << " overlapping guards in deterministic model."); |
|||
} |
|||
// Combine choices to one map.
|
|||
std::map<uint_fast64_t, double> map; |
|||
std::map<uint_fast64_t, double> rewardMap; |
|||
for (auto choice : transitionMap[state]) { |
|||
for (auto elem : choice.second) { |
|||
map[elem.first] += elem.second; |
|||
if ((this->rewardModel != nullptr) && (this->rewardModel->hasTransitionRewards())) { |
|||
for (auto reward : this->rewardModel->getTransitionRewards()) { |
|||
rewardMap[elem.first] += reward.getReward(choice.first, this->allStates[state]); |
|||
} |
|||
} |
|||
} |
|||
} |
|||
// Scale probabilities by number of choices.
|
|||
double factor = 1.0 / transitionMap[state].size(); |
|||
for (auto it : map) { |
|||
result->addNextValue(state, it.first, it.second * factor); |
|||
if ((this->rewardModel != nullptr) && (this->rewardModel->hasTransitionRewards())) { |
|||
this->transitionRewards->addNextValue(state, it.first, rewardMap[it.first] * factor); |
|||
} |
|||
} |
|||
|
|||
} |
|||
result->finalize(); |
|||
return result; |
|||
} |
|||
|
|||
/*!
|
|||
* Create matrix from intermediate mapping, assuming it is a mdp model. |
|||
* @param intermediate Intermediate representation of transition mapping. |
|||
* @param choices Overall number of choices for all nodes. |
|||
* @return result matrix. |
|||
*/ |
|||
std::shared_ptr<storm::storage::SparseMatrix<double>> ExplicitModelAdapter::buildNondeterministicMatrix() { |
|||
LOG4CPLUS_INFO(logger, "Building nondeterministic transition matrix: " << this->numberOfChoices << " x " << allStates.size() << " with " << this->numberOfTransitions << " transitions."); |
|||
std::shared_ptr<storm::storage::SparseMatrix<double>> result(new storm::storage::SparseMatrix<double>(this->numberOfChoices, allStates.size())); |
|||
result->initialize(this->numberOfTransitions); |
|||
if ((this->rewardModel != nullptr) && (this->rewardModel->hasTransitionRewards())) { |
|||
this->transitionRewards = std::shared_ptr<storm::storage::SparseMatrix<double>>(new storm::storage::SparseMatrix<double>(this->numberOfChoices, allStates.size())); |
|||
this->transitionRewards->initialize(this->numberOfTransitions); |
|||
} |
|||
// Build matrix.
|
|||
uint_fast64_t nextRow = 0; |
|||
for (uint_fast64_t state = 0; state < this->allStates.size(); state++) { |
|||
for (auto choice : transitionMap[state]) { |
|||
for (auto it : choice.second) { |
|||
result->addNextValue(nextRow, it.first, it.second); |
|||
if ((this->rewardModel != nullptr) && (this->rewardModel->hasTransitionRewards())) { |
|||
double rewardValue = 0; |
|||
for (auto reward : this->rewardModel->getTransitionRewards()) { |
|||
rewardValue = reward.getReward(choice.first, this->allStates[state]); |
|||
} |
|||
this->transitionRewards->addNextValue(nextRow, it.first, rewardValue); |
|||
} |
|||
} |
|||
nextRow++; |
|||
} |
|||
} |
|||
result->finalize(); |
|||
return result; |
|||
} |
|||
|
|||
/*!
|
|||
* Build matrix from model. Starts with all initial states and explores the reachable state space. |
|||
* While exploring, the transitions are stored in a temporary map. |
|||
* Afterwards, we transform this map into the actual matrix. |
|||
* @return result matrix. |
|||
*/ |
|||
void ExplicitModelAdapter::buildTransitionMap() { |
|||
LOG4CPLUS_DEBUG(logger, "Starting to create transition map from program..."); |
|||
this->clearInternalState(); |
|||
|
|||
this->generateInitialStates(); |
|||
for (uint_fast64_t curIndex = 0; curIndex < this->allStates.size(); curIndex++) |
|||
{ |
|||
this->addUnlabeledTransitions(curIndex, this->transitionMap[curIndex]); |
|||
this->addLabeledTransitions(curIndex, this->transitionMap[curIndex]); |
|||
|
|||
this->numberOfChoices += this->transitionMap[curIndex].size(); |
|||
if (this->transitionMap[curIndex].size() == 0) { |
|||
// This is a deadlock state.
|
|||
if (storm::settings::instance()->isSet("fix-deadlocks")) { |
|||
this->numberOfTransitions++; |
|||
this->numberOfChoices++; |
|||
this->transitionMap[curIndex].emplace_back(); |
|||
this->transitionMap[curIndex].back().second[curIndex] = 1; |
|||
} else { |
|||
LOG4CPLUS_ERROR(logger, "Error while creating sparse matrix from probabilistic program: found deadlock state."); |
|||
throw storm::exceptions::WrongFileFormatException() << "Error while creating sparse matrix from probabilistic program: found deadlock state."; |
|||
} |
|||
} |
|||
} |
|||
LOG4CPLUS_DEBUG(logger, "Finished creating transition map."); |
|||
} |
|||
|
|||
void ExplicitModelAdapter::clearInternalState() { |
|||
for (auto it : allStates) { |
|||
delete it; |
|||
} |
|||
allStates.clear(); |
|||
stateToIndexMap.clear(); |
|||
this->numberOfTransitions = 0; |
|||
this->numberOfChoices = 0; |
|||
this->transitionRewards = nullptr; |
|||
this->transitionMap.clear(); |
|||
} |
|||
|
|||
} // namespace adapters
|
|||
|
|||
} // namespace storm
|
|||
@ -0,0 +1,206 @@ |
|||
/* |
|||
* File: ExplicitModelAdapter.h |
|||
* Author: Gereon Kremer |
|||
* |
|||
* Created on March 15, 2013, 11:42 AM |
|||
*/ |
|||
|
|||
#ifndef EXPLICITMODELADAPTER_H |
|||
#define EXPLICITMODELADAPTER_H |
|||
|
|||
#include <memory> |
|||
#include <unordered_map> |
|||
#include <utility> |
|||
#include <vector> |
|||
#include <boost/functional/hash.hpp> |
|||
|
|||
#include "src/ir/Program.h" |
|||
#include "src/ir/StateReward.h" |
|||
#include "src/ir/TransitionReward.h" |
|||
|
|||
#include "src/models/AbstractModel.h" |
|||
#include "src/models/AtomicPropositionsLabeling.h" |
|||
#include "src/storage/SparseMatrix.h" |
|||
|
|||
namespace storm { |
|||
namespace adapters { |
|||
|
|||
/*! |
|||
* Model state, represented by the values of all variables. |
|||
*/ |
|||
typedef std::pair<std::vector<bool>, std::vector<int_fast64_t>> StateType; |
|||
|
|||
class StateHash { |
|||
public: |
|||
std::size_t operator()(StateType* state) const { |
|||
size_t seed = 0; |
|||
for (auto it : state->first) { |
|||
boost::hash_combine<bool>(seed, it); |
|||
} |
|||
for (auto it : state->second) { |
|||
boost::hash_combine<int_fast64_t>(seed, it); |
|||
} |
|||
return seed; |
|||
} |
|||
}; |
|||
|
|||
class StateCompare { |
|||
public: |
|||
bool operator()(StateType* state1, StateType* state2) const { |
|||
return *state1 == *state2; |
|||
} |
|||
}; |
|||
|
|||
class ExplicitModelAdapter { |
|||
public: |
|||
ExplicitModelAdapter(storm::ir::Program program); |
|||
~ExplicitModelAdapter(); |
|||
|
|||
std::shared_ptr<storm::models::AbstractModel> getModel(std::string const & rewardModelName = ""); |
|||
|
|||
private: |
|||
|
|||
double precision; |
|||
|
|||
// First some generic routines to operate on states. |
|||
|
|||
/*! |
|||
* Set some boolean variable in the given state object. |
|||
* @param state State to be changed. |
|||
* @param index Index of boolean variable. |
|||
* @param value New value. |
|||
*/ |
|||
static void setValue(StateType* const state, uint_fast64_t const index, bool const value); |
|||
/*! |
|||
* Set some integer variable in the given state object. |
|||
* @param state State to be changed. |
|||
* @param index Index of integer variable. |
|||
* @param value New value. |
|||
*/ |
|||
static void setValue(StateType* const state, uint_fast64_t const index, int_fast64_t const value); |
|||
static std::string toString(StateType const * const state); |
|||
/*! |
|||
* Apply an update to the given state and return the resulting new state object. |
|||
* This methods creates a copy of the given state. |
|||
* @params state Current state. |
|||
* @params update Update to be applied. |
|||
* @return Resulting state. |
|||
*/ |
|||
StateType* applyUpdate(StateType const * const state, storm::ir::Update const& update) const; |
|||
/*! |
|||
* Apply an update to a given state and return the resulting new state object. |
|||
* Updates are done using the variable values from a given baseState. |
|||
* @params state State to be updated. |
|||
* @params baseState State used for update variables. |
|||
* @params update Update to be applied. |
|||
* @return Resulting state. |
|||
*/ |
|||
StateType* applyUpdate(StateType const * const state, StateType const * const baseState, storm::ir::Update const& update) const; |
|||
|
|||
/*! |
|||
* Reads and combines variables from all program modules and stores them. |
|||
* Also creates a map to obtain a variable index from a variable map efficiently. |
|||
*/ |
|||
void initializeVariables(); |
|||
|
|||
std::shared_ptr<std::vector<double>> getStateRewards(std::vector<storm::ir::StateReward> const & rewards); |
|||
std::shared_ptr<storm::models::AtomicPropositionsLabeling> getStateLabeling(std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> labels); |
|||
|
|||
/*! |
|||
* Retrieves all active command labeled by some label, ordered by modules. |
|||
* |
|||
* This function will iterate over all modules and retrieve all commands that are labeled with the given action and active for the current state. |
|||
* The result will be a list of lists of commands. |
|||
* |
|||
* For each module that has appropriately labeled commands, there will be a list. |
|||
* If none of these commands is active, this list is empty. |
|||
* Note the difference between *no list* and *empty list*: Modules that produce no list are not relevant for this action while an empty list means, that it is not possible to do anything with this label. |
|||
* @param state Current state. |
|||
* @param action Action label. |
|||
* @return Active commands. |
|||
*/ |
|||
std::unique_ptr<std::list<std::list<storm::ir::Command>>> getActiveCommandsByAction(StateType const * state, std::string& action); |
|||
|
|||
/*! |
|||
* Generates all initial states and adds them to allStates. |
|||
*/ |
|||
void generateInitialStates(); |
|||
|
|||
/*! |
|||
* Retrieves the state id of the given state. |
|||
* If the state has not been hit yet, it will be added to allStates and given a new id. |
|||
* In this case, the pointer must not be deleted, as it is used within allStates. |
|||
* If the state is already known, the pointer is deleted and the old state id is returned. |
|||
* Hence, the given state pointer should not be used afterwards. |
|||
* @param state Pointer to state, shall not be used afterwards. |
|||
* @returns State id of given state. |
|||
*/ |
|||
uint_fast64_t getOrAddStateId(StateType * state); |
|||
|
|||
/*! |
|||
* Expands all unlabeled transitions for a given state and adds them to the given list of results. |
|||
* @params state State to be explored. |
|||
* @params res Intermediate transition map. |
|||
*/ |
|||
void addUnlabeledTransitions(const uint_fast64_t stateID, std::list<std::pair<std::string, std::map<uint_fast64_t, double>>>& res); |
|||
|
|||
/*! |
|||
* Explores reachable state from given state by using labeled transitions. |
|||
* Found transitions are stored in given map. |
|||
* @param stateID State to be explored. |
|||
* @param res Intermediate transition map. |
|||
*/ |
|||
void addLabeledTransitions(const uint_fast64_t stateID, std::list<std::pair<std::string, std::map<uint_fast64_t, double>>>& res); |
|||
|
|||
/*! |
|||
* Create matrix from intermediate mapping, assuming it is a dtmc model. |
|||
* @param intermediate Intermediate representation of transition mapping. |
|||
* @return result matrix. |
|||
*/ |
|||
std::shared_ptr<storm::storage::SparseMatrix<double>> buildDeterministicMatrix(); |
|||
|
|||
/*! |
|||
* Create matrix from intermediate mapping, assuming it is a mdp model. |
|||
* @param intermediate Intermediate representation of transition mapping. |
|||
* @param choices Overall number of choices for all nodes. |
|||
* @return result matrix. |
|||
*/ |
|||
std::shared_ptr<storm::storage::SparseMatrix<double>> buildNondeterministicMatrix(); |
|||
|
|||
/*! |
|||
* Build matrix from model. Starts with all initial states and explores the reachable state space. |
|||
* While exploring, the transitions are stored in a temporary map. |
|||
* Afterwards, we transform this map into the actual matrix. |
|||
* @return result matrix. |
|||
*/ |
|||
void buildTransitionMap(); |
|||
|
|||
void clearInternalState(); |
|||
|
|||
// Program that should be converted. |
|||
storm::ir::Program program; |
|||
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; |
|||
|
|||
// Members that are filled during the conversion. |
|||
std::unique_ptr<storm::ir::RewardModel> rewardModel; |
|||
std::vector<StateType*> allStates; |
|||
std::unordered_map<StateType*, uint_fast64_t, StateHash, StateCompare> stateToIndexMap; |
|||
uint_fast64_t numberOfTransitions; |
|||
uint_fast64_t numberOfChoices; |
|||
std::shared_ptr<storm::storage::SparseMatrix<double>> transitionRewards; |
|||
|
|||
/*! |
|||
* Maps a source node to a list of probability distributions over target nodes. |
|||
* Each such distribution corresponds to an unlabeled command or a feasible combination of labeled commands. |
|||
* Therefore, each distribution is represented by a label and a mapping from target nodes to their probabilities. |
|||
*/ |
|||
std::map<uint_fast64_t, std::list<std::pair<std::string, std::map<uint_fast64_t, double>>>> transitionMap; |
|||
}; |
|||
|
|||
} // namespace adapters |
|||
} // namespace storm |
|||
|
|||
#endif /* EXPLICITMODELADAPTER_H */ |
|||
@ -0,0 +1,231 @@ |
|||
/* |
|||
* SymbolicExpressionAdapter.h |
|||
* |
|||
* Created on: 27.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_ADAPTERS_SYMBOLICEXPRESSIONADAPTER_H_ |
|||
#define STORM_ADAPTERS_SYMBOLICEXPRESSIONADAPTER_H_ |
|||
|
|||
#include "src/ir/expressions/ExpressionVisitor.h" |
|||
#include "src/exceptions/ExpressionEvaluationException.h" |
|||
|
|||
#include "cuddObj.hh" |
|||
|
|||
#include <stack> |
|||
#include <iostream> |
|||
|
|||
namespace storm { |
|||
|
|||
namespace adapters { |
|||
|
|||
class SymbolicExpressionAdapter : public storm::ir::expressions::ExpressionVisitor { |
|||
public: |
|||
SymbolicExpressionAdapter(std::unordered_map<std::string, std::vector<ADD*>>& variableToDecisionDiagramVariableMap) : stack(), variableToDecisionDiagramVariableMap(variableToDecisionDiagramVariableMap) { |
|||
|
|||
} |
|||
|
|||
ADD* translateExpression(std::shared_ptr<storm::ir::expressions::BaseExpression> expression) { |
|||
expression->accept(this); |
|||
return stack.top(); |
|||
} |
|||
|
|||
virtual void visit(storm::ir::expressions::BaseExpression* expression) { |
|||
std::cout << expression->toString() << std::endl; |
|||
throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression " |
|||
<< " of abstract superclass type."; |
|||
} |
|||
|
|||
virtual void visit(storm::ir::expressions::BinaryBooleanFunctionExpression* expression) { |
|||
expression->getLeft()->accept(this); |
|||
expression->getRight()->accept(this); |
|||
|
|||
ADD* rightResult = stack.top(); |
|||
stack.pop(); |
|||
ADD* leftResult = stack.top(); |
|||
stack.pop(); |
|||
|
|||
switch(expression->getFunctionType()) { |
|||
case storm::ir::expressions::BinaryBooleanFunctionExpression::AND: |
|||
stack.push(new ADD(leftResult->Times(*rightResult))); |
|||
break; |
|||
case storm::ir::expressions::BinaryBooleanFunctionExpression::OR: |
|||
stack.push(new ADD(leftResult->Plus(*rightResult))); |
|||
break; |
|||
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Unknown boolean binary operator: '" << expression->getFunctionType() << "'."; |
|||
} |
|||
|
|||
// delete leftResult; |
|||
// delete rightResult; |
|||
} |
|||
|
|||
virtual void visit(storm::ir::expressions::BinaryNumericalFunctionExpression* expression) { |
|||
expression->getLeft()->accept(this); |
|||
expression->getRight()->accept(this); |
|||
|
|||
ADD* rightResult = stack.top(); |
|||
stack.pop(); |
|||
ADD* leftResult = stack.top(); |
|||
stack.pop(); |
|||
|
|||
switch(expression->getFunctionType()) { |
|||
case storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS: |
|||
stack.push(new ADD(leftResult->Plus(*rightResult))); |
|||
break; |
|||
case storm::ir::expressions::BinaryNumericalFunctionExpression::MINUS: |
|||
stack.push(new ADD(leftResult->Minus(*rightResult))); |
|||
break; |
|||
case storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES: |
|||
stack.push(new ADD(leftResult->Times(*rightResult))); |
|||
break; |
|||
case storm::ir::expressions::BinaryNumericalFunctionExpression::DIVIDE: |
|||
stack.push(new ADD(leftResult->Divide(*rightResult))); |
|||
break; |
|||
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Unknown boolean binary operator: '" << expression->getFunctionType() << "'."; |
|||
} |
|||
} |
|||
|
|||
virtual void visit(storm::ir::expressions::BinaryRelationExpression* expression) { |
|||
expression->getLeft()->accept(this); |
|||
expression->getRight()->accept(this); |
|||
|
|||
ADD* rightResult = stack.top(); |
|||
stack.pop(); |
|||
ADD* leftResult = stack.top(); |
|||
stack.pop(); |
|||
|
|||
switch(expression->getRelationType()) { |
|||
case storm::ir::expressions::BinaryRelationExpression::EQUAL: |
|||
stack.push(new ADD(leftResult->Equals(*rightResult))); |
|||
break; |
|||
case storm::ir::expressions::BinaryRelationExpression::NOT_EQUAL: |
|||
stack.push(new ADD(leftResult->NotEquals(*rightResult))); |
|||
break; |
|||
case storm::ir::expressions::BinaryRelationExpression::LESS: |
|||
stack.push(new ADD(leftResult->LessThan(*rightResult))); |
|||
break; |
|||
case storm::ir::expressions::BinaryRelationExpression::LESS_OR_EQUAL: |
|||
stack.push(new ADD(leftResult->LessThanOrEqual(*rightResult))); |
|||
break; |
|||
case storm::ir::expressions::BinaryRelationExpression::GREATER: |
|||
stack.push(new ADD(leftResult->GreaterThan(*rightResult))); |
|||
break; |
|||
case storm::ir::expressions::BinaryRelationExpression::GREATER_OR_EQUAL: |
|||
stack.push(new ADD(leftResult->GreaterThanOrEqual(*rightResult))); |
|||
break; |
|||
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Unknown boolean binary operator: '" << expression->getRelationType() << "'."; |
|||
} |
|||
} |
|||
|
|||
virtual void visit(storm::ir::expressions::BooleanConstantExpression* expression) { |
|||
if (!expression->isDefined()) { |
|||
throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Boolean constant '" << expression->getConstantName() << "' is undefined."; |
|||
} |
|||
|
|||
storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); |
|||
stack.push(new ADD(*cuddUtility->getConstant(expression->getValue() ? 1 : 0))); |
|||
} |
|||
|
|||
virtual void visit(storm::ir::expressions::BooleanLiteral* expression) { |
|||
storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); |
|||
stack.push(new ADD(*cuddUtility->getConstant(expression->getValueAsBool(nullptr) ? 1 : 0))); |
|||
} |
|||
|
|||
virtual void visit(storm::ir::expressions::DoubleConstantExpression* expression) { |
|||
if (expression->isDefined()) { |
|||
throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Double constant '" << expression->getConstantName() << "' is undefined."; |
|||
} |
|||
|
|||
storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); |
|||
stack.push(new ADD(*cuddUtility->getConstant(expression->getValue()))); |
|||
} |
|||
|
|||
virtual void visit(storm::ir::expressions::DoubleLiteral* expression) { |
|||
storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); |
|||
stack.push(new ADD(*cuddUtility->getConstant(expression->getValueAsDouble(nullptr)))); |
|||
} |
|||
|
|||
virtual void visit(storm::ir::expressions::IntegerConstantExpression* expression) { |
|||
if (!expression->isDefined()) { |
|||
throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Integer constant '" << expression->getConstantName() << "' is undefined."; |
|||
} |
|||
|
|||
storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); |
|||
stack.push(new ADD(*cuddUtility->getConstant(expression->getValue()))); |
|||
} |
|||
|
|||
virtual void visit(storm::ir::expressions::IntegerLiteral* expression) { |
|||
storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); |
|||
stack.push(new ADD(*cuddUtility->getConstant(expression->getValueAsInt(nullptr)))); |
|||
} |
|||
|
|||
virtual void visit(storm::ir::expressions::UnaryBooleanFunctionExpression* expression) { |
|||
expression->getChild()->accept(this); |
|||
|
|||
ADD* childResult = stack.top(); |
|||
stack.pop(); |
|||
|
|||
switch (expression->getFunctionType()) { |
|||
case storm::ir::expressions::UnaryBooleanFunctionExpression::NOT: |
|||
stack.push(new ADD(~(*childResult))); |
|||
break; |
|||
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Unknown boolean unary operator: '" << expression->getFunctionType() << "'."; |
|||
} |
|||
} |
|||
|
|||
virtual void visit(storm::ir::expressions::UnaryNumericalFunctionExpression* expression) { |
|||
expression->getChild()->accept(this); |
|||
|
|||
ADD* childResult = stack.top(); |
|||
stack.pop(); |
|||
|
|||
storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); |
|||
ADD* result = cuddUtility->getConstant(0); |
|||
switch(expression->getFunctionType()) { |
|||
case storm::ir::expressions::UnaryNumericalFunctionExpression::MINUS: |
|||
stack.push(new ADD(result->Minus(*childResult))); |
|||
break; |
|||
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Unknown numerical unary operator: '" << expression->getFunctionType() << "'."; |
|||
} |
|||
|
|||
} |
|||
|
|||
virtual void visit(storm::ir::expressions::VariableExpression* expression) { |
|||
storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); |
|||
|
|||
std::vector<ADD*> const& variables = variableToDecisionDiagramVariableMap[expression->getVariableName()]; |
|||
|
|||
ADD* result = cuddUtility->getConstant(0); |
|||
if (expression->getType() == storm::ir::expressions::BaseExpression::bool_) { |
|||
cuddUtility->setValueAtIndex(result, 1, variables, 1); |
|||
} else { |
|||
int64_t low = expression->getLowerBound()->getValueAsInt(nullptr); |
|||
int64_t high = expression->getUpperBound()->getValueAsInt(nullptr); |
|||
|
|||
for (uint_fast64_t i = low; i <= high; ++i) { |
|||
cuddUtility->setValueAtIndex(result, i - low, variables, i); |
|||
} |
|||
} |
|||
|
|||
stack.push(result); |
|||
} |
|||
|
|||
private: |
|||
std::stack<ADD*> stack; |
|||
std::unordered_map<std::string, std::vector<ADD*>>& variableToDecisionDiagramVariableMap; |
|||
}; |
|||
|
|||
} // namespace adapters |
|||
|
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_ADAPTERS_SYMBOLICEXPRESSIONADAPTER_H_ */ |
|||
@ -0,0 +1,289 @@ |
|||
/* |
|||
* SymbolicModelAdapter.h |
|||
* |
|||
* Created on: 25.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_ADAPTERS_SYMBOLICMODELADAPTER_H_ |
|||
#define STORM_ADAPTERS_SYMBOLICMODELADAPTER_H_ |
|||
|
|||
#include "src/exceptions/WrongFileFormatException.h" |
|||
|
|||
#include "src/utility/CuddUtility.h" |
|||
#include "SymbolicExpressionAdapter.h" |
|||
|
|||
#include "cuddObj.hh" |
|||
#include <iostream> |
|||
#include <unordered_map> |
|||
|
|||
namespace storm { |
|||
|
|||
namespace adapters { |
|||
|
|||
class SymbolicModelAdapter { |
|||
public: |
|||
|
|||
SymbolicModelAdapter() : cuddUtility(storm::utility::cuddUtilityInstance()), allDecisionDiagramVariables(), |
|||
allRowDecisionDiagramVariables(), allColumnDecisionDiagramVariables(), booleanRowDecisionDiagramVariables(), |
|||
integerRowDecisionDiagramVariables(), booleanColumnDecisionDiagramVariables(), integerColumnDecisionDiagramVariables(), |
|||
variableToRowDecisionDiagramVariableMap(), variableToColumnDecisionDiagramVariableMap(), |
|||
variableToIdentityDecisionDiagramMap(), |
|||
rowExpressionAdapter(variableToRowDecisionDiagramVariableMap), columnExpressionAdapter(variableToColumnDecisionDiagramVariableMap) { |
|||
|
|||
} |
|||
|
|||
void toMTBDD(storm::ir::Program const& program) { |
|||
LOG4CPLUS_INFO(logger, "Creating MTBDD representation for probabilistic program."); |
|||
createDecisionDiagramVariables(program); |
|||
createIdentityDecisionDiagrams(program); |
|||
|
|||
ADD* systemAdd = cuddUtility->getZero(); |
|||
for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { |
|||
storm::ir::Module const& module = program.getModule(i); |
|||
|
|||
ADD* moduleAdd = cuddUtility->getZero(); |
|||
for (uint_fast64_t j = 0; j < module.getNumberOfCommands(); ++j) { |
|||
storm::ir::Command const& command = module.getCommand(j); |
|||
|
|||
ADD* commandAdd = cuddUtility->getZero(); |
|||
|
|||
ADD* guard = rowExpressionAdapter.translateExpression(command.getGuard()); |
|||
if (*guard != *cuddUtility->getZero()) { |
|||
for (uint_fast64_t i = 0; i < command.getNumberOfUpdates(); ++i) { |
|||
ADD* updateAdd = cuddUtility->getOne(); |
|||
|
|||
storm::ir::Update const& update = command.getUpdate(i); |
|||
|
|||
std::map<std::string, storm::ir::Assignment> booleanAssignments = update.getBooleanAssignments(); |
|||
for (auto assignmentPair : booleanAssignments) { |
|||
ADD* updateExpr = rowExpressionAdapter.translateExpression(assignmentPair.second.getExpression()); |
|||
|
|||
ADD* temporary = cuddUtility->getZero(); |
|||
cuddUtility->setValueAtIndex(temporary, 0, variableToColumnDecisionDiagramVariableMap[assignmentPair.first], 0); |
|||
cuddUtility->setValueAtIndex(temporary, 1, variableToColumnDecisionDiagramVariableMap[assignmentPair.first], 1); |
|||
|
|||
ADD* result = new ADD(*updateExpr * *guard); |
|||
result = new ADD(result->Equals(*temporary)); |
|||
|
|||
*updateAdd = *updateAdd * *result; |
|||
} |
|||
|
|||
std::map<std::string, storm::ir::Assignment> integerAssignments = update.getIntegerAssignments(); |
|||
for (auto assignmentPair : integerAssignments) { |
|||
ADD* updateExpr = rowExpressionAdapter.translateExpression(assignmentPair.second.getExpression()); |
|||
|
|||
ADD* temporary = cuddUtility->getZero(); |
|||
|
|||
uint_fast64_t variableIndex = module.getIntegerVariableIndex(assignmentPair.first); |
|||
storm::ir::IntegerVariable integerVariable = module.getIntegerVariable(variableIndex); |
|||
int_fast64_t low = integerVariable.getLowerBound()->getValueAsInt(nullptr); |
|||
int_fast64_t high = integerVariable.getUpperBound()->getValueAsInt(nullptr); |
|||
|
|||
for (uint_fast64_t i = low; i <= high; ++i) { |
|||
cuddUtility->setValueAtIndex(temporary, i - low, variableToColumnDecisionDiagramVariableMap[assignmentPair.first], i); |
|||
} |
|||
|
|||
ADD* result = new ADD(*updateExpr * *guard); |
|||
result = new ADD(result->Equals(*temporary)); |
|||
*result *= *guard; |
|||
|
|||
*updateAdd = *updateAdd * *result; |
|||
} |
|||
for (uint_fast64_t i = 0; i < module.getNumberOfBooleanVariables(); ++i) { |
|||
storm::ir::BooleanVariable const& booleanVariable = module.getBooleanVariable(i); |
|||
|
|||
if (update.getBooleanAssignments().find(booleanVariable.getName()) == update.getBooleanAssignments().end()) { |
|||
*updateAdd = *updateAdd * *variableToIdentityDecisionDiagramMap[booleanVariable.getName()]; |
|||
} |
|||
} |
|||
for (uint_fast64_t i = 0; i < module.getNumberOfIntegerVariables(); ++i) { |
|||
storm::ir::IntegerVariable const& integerVariable = module.getIntegerVariable(i); |
|||
|
|||
if (update.getIntegerAssignments().find(integerVariable.getName()) == update.getIntegerAssignments().end()) { |
|||
*updateAdd = *updateAdd * *variableToIdentityDecisionDiagramMap[integerVariable.getName()]; |
|||
} |
|||
} |
|||
|
|||
*commandAdd += *updateAdd * *cuddUtility->getConstant(update.getLikelihoodExpression()->getValueAsDouble(nullptr)); |
|||
} |
|||
*moduleAdd += *commandAdd; |
|||
} else { |
|||
LOG4CPLUS_WARN(logger, "Guard " << command.getGuard()->toString() << " is unsatisfiable."); |
|||
} |
|||
} |
|||
*systemAdd += *moduleAdd; |
|||
} |
|||
|
|||
performReachability(program, systemAdd); |
|||
|
|||
LOG4CPLUS_INFO(logger, "Done creating MTBDD representation for probabilistic program."); |
|||
} |
|||
|
|||
private: |
|||
storm::utility::CuddUtility* cuddUtility; |
|||
|
|||
std::vector<ADD*> allDecisionDiagramVariables; |
|||
std::vector<ADD*> allRowDecisionDiagramVariables; |
|||
std::vector<ADD*> allColumnDecisionDiagramVariables; |
|||
std::vector<ADD*> booleanRowDecisionDiagramVariables; |
|||
std::vector<ADD*> integerRowDecisionDiagramVariables; |
|||
std::vector<ADD*> booleanColumnDecisionDiagramVariables; |
|||
std::vector<ADD*> integerColumnDecisionDiagramVariables; |
|||
std::unordered_map<std::string, std::vector<ADD*>> variableToRowDecisionDiagramVariableMap; |
|||
std::unordered_map<std::string, std::vector<ADD*>> variableToColumnDecisionDiagramVariableMap; |
|||
|
|||
std::unordered_map<std::string, ADD*> variableToIdentityDecisionDiagramMap; |
|||
|
|||
SymbolicExpressionAdapter rowExpressionAdapter; |
|||
SymbolicExpressionAdapter columnExpressionAdapter; |
|||
|
|||
ADD* getInitialStateDecisionDiagram(storm::ir::Program const& program) { |
|||
ADD* initialStates = cuddUtility->getOne(); |
|||
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) { |
|||
storm::ir::BooleanVariable const& booleanVariable = module.getBooleanVariable(j); |
|||
bool initialValue = booleanVariable.getInitialValue()->getValueAsBool(nullptr); |
|||
*initialStates *= *cuddUtility->getConstantEncoding(1, variableToRowDecisionDiagramVariableMap[booleanVariable.getName()]); |
|||
} |
|||
for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) { |
|||
storm::ir::IntegerVariable const& integerVariable = module.getIntegerVariable(j); |
|||
int_fast64_t initialValue = integerVariable.getInitialValue()->getValueAsInt(nullptr); |
|||
int_fast64_t low = integerVariable.getLowerBound()->getValueAsInt(nullptr); |
|||
*initialStates *= *cuddUtility->getConstantEncoding(initialValue - low, variableToRowDecisionDiagramVariableMap[integerVariable.getName()]); |
|||
} |
|||
} |
|||
|
|||
cuddUtility->dumpDotToFile(initialStates, "initstates.add"); |
|||
return initialStates; |
|||
} |
|||
|
|||
void performReachability(storm::ir::Program const& program, ADD* systemAdd) { |
|||
ADD* systemAdd01 = new ADD(systemAdd->GreaterThan(*cuddUtility->getZero())); |
|||
cuddUtility->dumpDotToFile(systemAdd01, "system01.add"); |
|||
|
|||
cuddUtility->dumpDotToFile(systemAdd, "reachtransold.add"); |
|||
ADD* reachableStates = getInitialStateDecisionDiagram(program); |
|||
cuddUtility->dumpDotToFile(reachableStates, "init.add"); |
|||
ADD* newReachableStates = new ADD(*reachableStates); |
|||
|
|||
ADD* rowCube = cuddUtility->getOne(); |
|||
for (auto variablePtr : allRowDecisionDiagramVariables) { |
|||
*rowCube *= *variablePtr; |
|||
} |
|||
|
|||
bool changed; |
|||
int iter = 0; |
|||
do { |
|||
changed = false; |
|||
*newReachableStates = *reachableStates * *systemAdd01; |
|||
newReachableStates = new ADD(newReachableStates->ExistAbstract(*rowCube)); |
|||
|
|||
cuddUtility->dumpDotToFile(newReachableStates, "reach1.add"); |
|||
|
|||
newReachableStates = cuddUtility->permuteVariables(newReachableStates, allColumnDecisionDiagramVariables, allRowDecisionDiagramVariables, allDecisionDiagramVariables.size()); |
|||
|
|||
*newReachableStates += *reachableStates; |
|||
newReachableStates = new ADD(newReachableStates->GreaterThan(*cuddUtility->getZero())); |
|||
|
|||
if (*newReachableStates != *reachableStates) changed = true; |
|||
*reachableStates = *newReachableStates; |
|||
} while (changed); |
|||
|
|||
*systemAdd *= *reachableStates; |
|||
std::cout << "got " << systemAdd->nodeCount() << " nodes" << std::endl; |
|||
std::cout << "and " << systemAdd->CountMinterm(allRowDecisionDiagramVariables.size() + allColumnDecisionDiagramVariables.size()) << std::endl; |
|||
} |
|||
|
|||
void createIdentityDecisionDiagrams(storm::ir::Program const& program) { |
|||
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) { |
|||
storm::ir::BooleanVariable const& booleanVariable = module.getBooleanVariable(j); |
|||
ADD* identity = cuddUtility->getZero(); |
|||
cuddUtility->setValueAtIndices(identity, 0, 0, |
|||
variableToRowDecisionDiagramVariableMap[booleanVariable.getName()], |
|||
variableToColumnDecisionDiagramVariableMap[booleanVariable.getName()], 1); |
|||
cuddUtility->setValueAtIndices(identity, 1, 1, |
|||
variableToRowDecisionDiagramVariableMap[booleanVariable.getName()], |
|||
variableToColumnDecisionDiagramVariableMap[booleanVariable.getName()], 1); |
|||
variableToIdentityDecisionDiagramMap[booleanVariable.getName()] = identity; |
|||
} |
|||
|
|||
for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) { |
|||
storm::ir::IntegerVariable const& integerVariable = module.getIntegerVariable(j); |
|||
|
|||
ADD* identity = cuddUtility->getZero(); |
|||
|
|||
int_fast64_t low = integerVariable.getLowerBound()->getValueAsInt(nullptr); |
|||
int_fast64_t high = integerVariable.getUpperBound()->getValueAsInt(nullptr); |
|||
|
|||
for (uint_fast64_t i = low; i <= high; ++i) { |
|||
cuddUtility->setValueAtIndices(identity, i - low, i - low, |
|||
variableToRowDecisionDiagramVariableMap[integerVariable.getName()], |
|||
variableToColumnDecisionDiagramVariableMap[integerVariable.getName()], 1); |
|||
} |
|||
variableToIdentityDecisionDiagramMap[integerVariable.getName()] = identity; |
|||
} |
|||
} |
|||
} |
|||
|
|||
void createDecisionDiagramVariables(storm::ir::Program const& program) { |
|||
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) { |
|||
storm::ir::BooleanVariable const& booleanVariable = module.getBooleanVariable(j); |
|||
|
|||
ADD* newRowDecisionDiagramVariable = cuddUtility->getNewAddVariable(); |
|||
variableToRowDecisionDiagramVariableMap[booleanVariable.getName()].push_back(newRowDecisionDiagramVariable); |
|||
booleanRowDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable); |
|||
allRowDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable); |
|||
allDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable); |
|||
|
|||
ADD* newColumnDecisionDiagramVariable = cuddUtility->getNewAddVariable(); |
|||
variableToColumnDecisionDiagramVariableMap[booleanVariable.getName()].push_back(newColumnDecisionDiagramVariable); |
|||
booleanColumnDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable); |
|||
allColumnDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable); |
|||
allDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable); |
|||
} |
|||
|
|||
for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) { |
|||
storm::ir::IntegerVariable const& integerVariable = module.getIntegerVariable(j); |
|||
uint_fast64_t integerRange = integerVariable.getUpperBound()->getValueAsInt(nullptr) - integerVariable.getLowerBound()->getValueAsInt(nullptr); |
|||
if (integerRange <= 0) { |
|||
throw storm::exceptions::WrongFileFormatException() << "Range of variable " |
|||
<< integerVariable.getName() << " is empty or negativ."; |
|||
} |
|||
uint_fast64_t numberOfDecisionDiagramVariables = static_cast<uint_fast64_t>(std::ceil(std::log2(integerRange))); |
|||
|
|||
std::vector<ADD*> allRowDecisionDiagramVariablesForVariable; |
|||
std::vector<ADD*> allColumnDecisionDiagramVariablesForVariable; |
|||
for (uint_fast64_t k = 0; k < numberOfDecisionDiagramVariables; ++k) { |
|||
ADD* newRowDecisionDiagramVariable = cuddUtility->getNewAddVariable(); |
|||
allRowDecisionDiagramVariablesForVariable.push_back(newRowDecisionDiagramVariable); |
|||
integerRowDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable); |
|||
allRowDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable); |
|||
allDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable); |
|||
|
|||
ADD* newColumnDecisionDiagramVariable = cuddUtility->getNewAddVariable(); |
|||
allColumnDecisionDiagramVariablesForVariable.push_back(newColumnDecisionDiagramVariable); |
|||
integerColumnDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable); |
|||
allColumnDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable); |
|||
allDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable); |
|||
} |
|||
variableToRowDecisionDiagramVariableMap[integerVariable.getName()] = allRowDecisionDiagramVariablesForVariable; |
|||
variableToColumnDecisionDiagramVariableMap[integerVariable.getName()] = allColumnDecisionDiagramVariablesForVariable; |
|||
} |
|||
} |
|||
} |
|||
}; |
|||
|
|||
} // namespace adapters |
|||
|
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_ADAPTERS_SYMBOLICMODELADAPTER_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_ */ |
|||
@ -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_ */ |
|||
@ -0,0 +1,53 @@ |
|||
/*
|
|||
* Assignment.cpp |
|||
* |
|||
* Created on: 12.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include "Assignment.h"
|
|||
|
|||
#include <sstream>
|
|||
|
|||
namespace storm { |
|||
|
|||
namespace ir { |
|||
|
|||
// Initializes all members with their default constructors.
|
|||
Assignment::Assignment() : variableName(), expression() { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
// Initializes all members according to the given values.
|
|||
Assignment::Assignment(std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> expression) |
|||
: variableName(variableName), expression(expression) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
Assignment::Assignment(const Assignment& assignment, const std::map<std::string, std::string>& renaming, const std::map<std::string,uint_fast64_t>& bools, const std::map<std::string,uint_fast64_t>& ints) |
|||
: variableName(assignment.variableName), expression(assignment.expression->clone(renaming, bools, ints)) { |
|||
if (renaming.count(assignment.variableName) > 0) { |
|||
this->variableName = renaming.at(assignment.variableName); |
|||
} |
|||
} |
|||
|
|||
// Returns the name of the variable associated with this assignment.
|
|||
std::string const& Assignment::getVariableName() const { |
|||
return variableName; |
|||
} |
|||
|
|||
// Returns the expression associated with this assignment.
|
|||
std::shared_ptr<storm::ir::expressions::BaseExpression> const& Assignment::getExpression() const { |
|||
return expression; |
|||
} |
|||
|
|||
// Build a string representation of the assignment.
|
|||
std::string Assignment::toString() const { |
|||
std::stringstream result; |
|||
result << "(" << variableName << "' = " << expression->toString() << ")"; |
|||
return result.str(); |
|||
} |
|||
|
|||
} // namespace ir
|
|||
|
|||
} // namespace storm
|
|||
@ -0,0 +1,68 @@ |
|||
/* |
|||
* Assignment.h |
|||
* |
|||
* Created on: 06.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_ASSIGNMENT_H_ |
|||
#define STORM_IR_ASSIGNMENT_H_ |
|||
|
|||
#include "expressions/BaseExpression.h" |
|||
|
|||
#include <memory> |
|||
|
|||
namespace storm { |
|||
|
|||
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 variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> expression); |
|||
|
|||
Assignment(const Assignment& assignment, const std::map<std::string, std::string>& renaming, const std::map<std::string,uint_fast64_t>& bools, const std::map<std::string,uint_fast64_t>& ints); |
|||
|
|||
/*! |
|||
* Retrieves the name of the variable that this assignment targets. |
|||
* @returns the name of the variable that this assignment targets. |
|||
*/ |
|||
std::string const& getVariableName() const; |
|||
|
|||
/*! |
|||
* Retrieves the expression that is assigned to the variable. |
|||
* @returns the expression that is assigned to the variable. |
|||
*/ |
|||
std::shared_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::shared_ptr<storm::ir::expressions::BaseExpression> expression; |
|||
}; |
|||
|
|||
} // namespace ir |
|||
|
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_ASSIGNMENT_H_ */ |
|||
@ -0,0 +1,45 @@ |
|||
/*
|
|||
* BooleanVariable.cpp |
|||
* |
|||
* Created on: 12.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include "BooleanVariable.h"
|
|||
|
|||
#include <sstream>
|
|||
|
|||
namespace storm { |
|||
|
|||
namespace ir { |
|||
|
|||
// Initializes all members with their default constructors.
|
|||
BooleanVariable::BooleanVariable() : Variable() { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
// Initializes all members according to the given values.
|
|||
BooleanVariable::BooleanVariable(uint_fast64_t index, std::string variableName, |
|||
std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue) |
|||
: Variable(index, variableName, initialValue) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
BooleanVariable::BooleanVariable(const BooleanVariable& var, const std::string& newName, const std::map<std::string, std::string>& renaming, const std::map<std::string,uint_fast64_t>& bools, const std::map<std::string,uint_fast64_t>& ints) |
|||
: Variable(var, newName, bools.at(newName), renaming, bools, ints) { |
|||
} |
|||
|
|||
// Build a string representation of the variable.
|
|||
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
|
|||
@ -0,0 +1,51 @@ |
|||
/* |
|||
* BooleanVariable.h |
|||
* |
|||
* Created on: 08.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_BOOLEANVARIABLE_H_ |
|||
#define STORM_IR_BOOLEANVARIABLE_H_ |
|||
|
|||
#include "src/ir/Variable.h" |
|||
#include <memory> |
|||
#include <map> |
|||
|
|||
namespace storm { |
|||
|
|||
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 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(uint_fast64_t index, std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>(nullptr)); |
|||
|
|||
|
|||
BooleanVariable(const BooleanVariable& var, const std::string& newName, const std::map<std::string, std::string>& renaming, const std::map<std::string,uint_fast64_t>& bools, const std::map<std::string,uint_fast64_t>& ints); |
|||
|
|||
/*! |
|||
* 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_ */ |
|||
@ -0,0 +1,75 @@ |
|||
/*
|
|||
* Command.cpp |
|||
* |
|||
* Created on: 12.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include "Command.h"
|
|||
|
|||
#include <sstream>
|
|||
#include <iostream>
|
|||
|
|||
namespace storm { |
|||
|
|||
namespace ir { |
|||
|
|||
// Initializes all members with their default constructors.
|
|||
Command::Command() : actionName(), guardExpression(), updates() { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
// Initializes all members according to the given values.
|
|||
Command::Command(std::string actionName, std::shared_ptr<storm::ir::expressions::BaseExpression> guardExpression, std::vector<storm::ir::Update> updates) |
|||
: actionName(actionName), guardExpression(guardExpression), updates(updates) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
Command::Command(const Command& cmd, const std::map<std::string, std::string>& renaming, const std::map<std::string,uint_fast64_t>& bools, const std::map<std::string,uint_fast64_t>& ints) |
|||
: actionName(cmd.actionName), guardExpression(cmd.guardExpression->clone(renaming, bools, ints)) { |
|||
if (renaming.count(this->actionName) > 0) { |
|||
this->actionName = renaming.at(this->actionName); |
|||
} |
|||
this->updates.reserve(cmd.updates.size()); |
|||
for (Update u : cmd.updates) { |
|||
this->updates.emplace_back(u, renaming, bools, ints); |
|||
} |
|||
} |
|||
|
|||
// Return the action name.
|
|||
std::string const& Command::getActionName() const { |
|||
return this->actionName; |
|||
} |
|||
|
|||
// 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; |
|||
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
|
|||
@ -0,0 +1,85 @@ |
|||
/* |
|||
* Command.h |
|||
* |
|||
* Created on: 06.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_COMMAND_H_ |
|||
#define STORM_IR_COMMAND_H_ |
|||
|
|||
#include "expressions/BaseExpression.h" |
|||
#include "Update.h" |
|||
|
|||
#include <vector> |
|||
#include <string> |
|||
#include <map> |
|||
|
|||
namespace storm { |
|||
|
|||
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 actionName the action name of the command. |
|||
* @param guardExpression the expression that defines the guard of the command. |
|||
*/ |
|||
Command(std::string actionName, std::shared_ptr<storm::ir::expressions::BaseExpression> guardExpression, std::vector<storm::ir::Update> updates); |
|||
|
|||
Command(const Command& cmd, const std::map<std::string, std::string>& renaming, const std::map<std::string,uint_fast64_t>& bools, const std::map<std::string,uint_fast64_t>& ints); |
|||
/*! |
|||
* Retrieves the action name of this command. |
|||
* @returns the action name of this command. |
|||
*/ |
|||
std::string const& getActionName() const; |
|||
|
|||
/*! |
|||
* 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. |
|||
*/ |
|||
std::string toString() const; |
|||
|
|||
private: |
|||
// The name of the command. |
|||
std::string actionName; |
|||
|
|||
// The expression that defines the guard of the command. |
|||
std::shared_ptr<storm::ir::expressions::BaseExpression> guardExpression; |
|||
|
|||
// The list of updates of the command. |
|||
std::vector<storm::ir::Update> updates; |
|||
}; |
|||
|
|||
} // namespace ir |
|||
|
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_COMMAND_H_ */ |
|||
@ -0,0 +1,25 @@ |
|||
/* |
|||
* 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_ */ |
|||
@ -0,0 +1,60 @@ |
|||
/*
|
|||
* IntegerVariable.cpp |
|||
* |
|||
* Created on: 12.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include "IntegerVariable.h"
|
|||
|
|||
#include <sstream>
|
|||
|
|||
#include <iostream>
|
|||
|
|||
namespace storm { |
|||
|
|||
namespace ir { |
|||
|
|||
// Initializes all members with their default constructors.
|
|||
IntegerVariable::IntegerVariable() : lowerBound(), upperBound() { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
// Initializes all members according to the given values.
|
|||
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) { |
|||
// TODO: This behaves like prism...
|
|||
if (this->getInitialValue() == nullptr) { |
|||
this->setInitialValue(lowerBound); |
|||
} |
|||
} |
|||
|
|||
IntegerVariable::IntegerVariable(const IntegerVariable& var, const std::string& newName, const std::map<std::string, std::string>& renaming, const std::map<std::string,uint_fast64_t>& bools, const std::map<std::string,uint_fast64_t>& ints) |
|||
: Variable(var, newName, ints.at(newName), renaming, bools, ints), lowerBound(var.lowerBound->clone(renaming, bools, ints)), upperBound(var.upperBound->clone(renaming, bools, ints)) { |
|||
} |
|||
|
|||
// Return lower bound for variable.
|
|||
std::shared_ptr<storm::ir::expressions::BaseExpression> IntegerVariable::getLowerBound() const { |
|||
return this->lowerBound; |
|||
} |
|||
|
|||
// Return upper bound for variable.
|
|||
std::shared_ptr<storm::ir::expressions::BaseExpression> IntegerVariable::getUpperBound() const { |
|||
return this->upperBound; |
|||
} |
|||
|
|||
|
|||
// Build a string representation of the variable.
|
|||
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
|
|||
@ -0,0 +1,72 @@ |
|||
/* |
|||
* IntegerVariable.h |
|||
* |
|||
* Created on: 08.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_INTEGERVARIABLE_H_ |
|||
#define STORM_IR_INTEGERVARIABLE_H_ |
|||
|
|||
#include "expressions/BaseExpression.h" |
|||
#include "src/ir/Variable.h" |
|||
#include <memory> |
|||
|
|||
namespace storm { |
|||
|
|||
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 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(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)); |
|||
|
|||
IntegerVariable(const IntegerVariable& var, const std::string& newName, const std::map<std::string, std::string>& renaming, const std::map<std::string,uint_fast64_t>& bools, const std::map<std::string,uint_fast64_t>& ints); |
|||
|
|||
/*! |
|||
* Retrieves the lower bound for this integer variable. |
|||
* @returns the lower bound for this integer variable. |
|||
*/ |
|||
std::shared_ptr<storm::ir::expressions::BaseExpression> getLowerBound() const; |
|||
|
|||
/*! |
|||
* Retrieves the upper bound for this integer variable. |
|||
* @returns the upper bound for this integer variable. |
|||
*/ |
|||
std::shared_ptr<storm::ir::expressions::BaseExpression> 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::shared_ptr<storm::ir::expressions::BaseExpression> lowerBound; |
|||
|
|||
// The upper bound of the domain of the variable. |
|||
std::shared_ptr<storm::ir::expressions::BaseExpression> upperBound; |
|||
}; |
|||
|
|||
} // namespace ir |
|||
|
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_INTEGERVARIABLE_H_ */ |
|||
@ -0,0 +1,182 @@ |
|||
/*
|
|||
* Module.cpp |
|||
* |
|||
* Created on: 12.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include "Module.h"
|
|||
|
|||
#include "src/exceptions/InvalidArgumentException.h"
|
|||
|
|||
#include <sstream>
|
|||
#include <iostream>
|
|||
|
|||
#include "log4cplus/logger.h"
|
|||
#include "log4cplus/loggingmacros.h"
|
|||
extern log4cplus::Logger logger; |
|||
|
|||
namespace storm { |
|||
|
|||
namespace ir { |
|||
|
|||
// Initializes all members with their default constructors.
|
|||
Module::Module() : moduleName(), booleanVariables(), integerVariables(), booleanVariablesToIndexMap(), |
|||
integerVariablesToIndexMap(), commands(), actions(), actionsToCommandIndexMap() { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
// Initializes all members according to the given values.
|
|||
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), actions(), actionsToCommandIndexMap() { |
|||
this->collectActions(); |
|||
} |
|||
|
|||
Module::Module(const Module& module, const std::string& moduleName, const std::map<std::string, std::string>& renaming, std::shared_ptr<VariableAdder> adder) |
|||
: moduleName(moduleName) { |
|||
LOG4CPLUS_TRACE(logger, "Start renaming " << module.moduleName << " to " << moduleName); |
|||
|
|||
// First step: Create new Variables via the adder.
|
|||
adder->performRenaming(renaming); |
|||
|
|||
// Second step: Get all indices of variables that are produced by the renaming.
|
|||
for (auto it: renaming) { |
|||
std::shared_ptr<expressions::VariableExpression> var = adder->getVariable(it.second); |
|||
if (var != nullptr) { |
|||
if (var->getType() == expressions::BaseExpression::bool_) { |
|||
this->booleanVariablesToIndexMap[it.second] = var->getVariableIndex(); |
|||
} else if (var->getType() == expressions::BaseExpression::int_) { |
|||
this->integerVariablesToIndexMap[it.second] = var->getVariableIndex(); |
|||
} |
|||
} |
|||
} |
|||
|
|||
// Third step: Create new Variable objects.
|
|||
this->booleanVariables.reserve(module.booleanVariables.size()); |
|||
for (BooleanVariable it: module.booleanVariables) { |
|||
if (renaming.count(it.getName()) > 0) { |
|||
this->booleanVariables.emplace_back(it, renaming.at(it.getName()), renaming, this->booleanVariablesToIndexMap, this->integerVariablesToIndexMap); |
|||
} else LOG4CPLUS_ERROR(logger, moduleName << "." << it.getName() << " was not renamed!"); |
|||
} |
|||
this->integerVariables.reserve(module.integerVariables.size()); |
|||
for (IntegerVariable it: module.integerVariables) { |
|||
if (renaming.count(it.getName()) > 0) { |
|||
this->integerVariables.emplace_back(it, renaming.at(it.getName()), renaming, this->booleanVariablesToIndexMap, this->integerVariablesToIndexMap); |
|||
} else LOG4CPLUS_ERROR(logger, moduleName << "." << it.getName() << " was not renamed!"); |
|||
} |
|||
|
|||
// Fourth step: Clone commands.
|
|||
this->commands.reserve(module.commands.size()); |
|||
for (Command cmd: module.commands) { |
|||
this->commands.emplace_back(cmd, renaming, this->booleanVariablesToIndexMap, this->integerVariablesToIndexMap); |
|||
} |
|||
this->collectActions(); |
|||
|
|||
LOG4CPLUS_TRACE(logger, "Finished renaming..."); |
|||
} |
|||
|
|||
// 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 index of the variable if it exists and throw exception otherwise.
|
|||
uint_fast64_t Module::getBooleanVariableIndex(std::string variableName) const { |
|||
auto it = booleanVariablesToIndexMap.find(variableName); |
|||
if (it != booleanVariablesToIndexMap.end()) { |
|||
return it->second; |
|||
} |
|||
throw storm::exceptions::InvalidArgumentException() << "Cannot retrieve index of unknown " |
|||
<< "boolean variable " << variableName << "."; |
|||
} |
|||
|
|||
// Return the index of the variable if it exists and throw exception otherwise.
|
|||
uint_fast64_t Module::getIntegerVariableIndex(std::string variableName) const { |
|||
auto it = integerVariablesToIndexMap.find(variableName); |
|||
if (it != integerVariablesToIndexMap.end()) { |
|||
return it->second; |
|||
} |
|||
throw storm::exceptions::InvalidArgumentException() << "Cannot retrieve index of unknown " |
|||
<< "variable " << variableName << "."; |
|||
} |
|||
|
|||
// 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.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(); |
|||
} |
|||
|
|||
// Return set of actions.
|
|||
std::set<std::string> const& Module::getActions() const { |
|||
return this->actions; |
|||
} |
|||
|
|||
// Return commands with given action.
|
|||
std::shared_ptr<std::set<uint_fast64_t>> const Module::getCommandsByAction(std::string const& action) const { |
|||
auto res = this->actionsToCommandIndexMap.find(action); |
|||
if (res == this->actionsToCommandIndexMap.end()) { |
|||
return std::shared_ptr<std::set<uint_fast64_t>>(new std::set<uint_fast64_t>()); |
|||
} else { |
|||
return res->second; |
|||
} |
|||
} |
|||
|
|||
void Module::collectActions() { |
|||
for (unsigned int id = 0; id < this->commands.size(); id++) { |
|||
std::string action = this->commands[id].getActionName(); |
|||
if (action != "") { |
|||
if (this->actionsToCommandIndexMap.count(action) == 0) { |
|||
this->actionsToCommandIndexMap[action] = std::shared_ptr<std::set<uint_fast64_t>>(new std::set<uint_fast64_t>()); |
|||
} |
|||
this->actionsToCommandIndexMap[action]->insert(id); |
|||
this->actions.insert(action); |
|||
} |
|||
} |
|||
} |
|||
|
|||
} // namespace ir
|
|||
|
|||
} // namespace storm
|
|||
@ -0,0 +1,171 @@ |
|||
/* |
|||
* Module.h |
|||
* |
|||
* Created on: 04.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_MODULE_H_ |
|||
#define STORM_IR_MODULE_H_ |
|||
|
|||
#include "BooleanVariable.h" |
|||
#include "IntegerVariable.h" |
|||
#include "expressions/VariableExpression.h" |
|||
#include "Command.h" |
|||
|
|||
#include <map> |
|||
#include <set> |
|||
#include <string> |
|||
#include <vector> |
|||
#include <memory> |
|||
|
|||
namespace storm { |
|||
|
|||
namespace ir { |
|||
|
|||
struct VariableAdder { |
|||
virtual uint_fast64_t addIntegerVariable(const std::string& name, const std::shared_ptr<storm::ir::expressions::BaseExpression> lower, const std::shared_ptr<storm::ir::expressions::BaseExpression> upper) = 0; |
|||
virtual uint_fast64_t addBooleanVariable(const std::string& name) = 0; |
|||
virtual std::shared_ptr<expressions::VariableExpression> getVariable(const std::string& name) = 0; |
|||
virtual void performRenaming(const std::map<std::string, std::string>& renaming) = 0; |
|||
}; |
|||
|
|||
/*! |
|||
* 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 a map of boolean variables. |
|||
* @param integerVariables a map of integer variables. |
|||
* @param commands the vector of 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); |
|||
|
|||
typedef uint_fast64_t (*addIntegerVariablePtr)(const std::string& name, const std::shared_ptr<storm::ir::expressions::BaseExpression> lower, const std::shared_ptr<storm::ir::expressions::BaseExpression> upper, const std::shared_ptr<storm::ir::expressions::BaseExpression> init); |
|||
typedef uint_fast64_t (*addBooleanVariablePtr)(const std::string& name, const std::shared_ptr<storm::ir::expressions::BaseExpression> init); |
|||
|
|||
/*! |
|||
* Special copy constructor, implementing the module renaming functionality. |
|||
* This will create a new module having all identifier renamed according to the given map. |
|||
* @param module Module to be copied. |
|||
* @param moduleName Name of the new module. |
|||
* @param renaming Renaming map. |
|||
*/ |
|||
Module(const Module& module, const std::string& moduleName, const std::map<std::string, std::string>& renaming, std::shared_ptr<VariableAdder> adder); |
|||
|
|||
/*! |
|||
* 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 the index of the boolean variable with the given name. |
|||
* @param variableName the name of the variable whose index to retrieve. |
|||
* @returns the index of the boolean variable with the given name. |
|||
*/ |
|||
uint_fast64_t getBooleanVariableIndex(std::string variableName) const; |
|||
|
|||
/*! |
|||
* Retrieves the index of the integer variable with the given name. |
|||
* @param variableName the name of the variable whose index to retrieve. |
|||
* @returns the index of the integer variable with the given name. |
|||
*/ |
|||
uint_fast64_t getIntegerVariableIndex(std::string variableName) 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. |
|||
* @returns a string representation of this variable. |
|||
*/ |
|||
std::string toString() const; |
|||
|
|||
/*! |
|||
* Retrieves the set of actions present in this module. |
|||
* @returns the set of actions present in this module. |
|||
*/ |
|||
std::set<std::string> const& getActions() const; |
|||
|
|||
/*! |
|||
* Retrieves the indices of all commands within this module that are labelled |
|||
* by the given action. |
|||
* @param action Name of the action. |
|||
* @returns Indices of all matching commands. |
|||
*/ |
|||
std::shared_ptr<std::set<uint_fast64_t>> const getCommandsByAction(std::string const& action) const; |
|||
|
|||
private: |
|||
|
|||
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> booleanVariablesToIndexMap; |
|||
|
|||
// A map of integer variable names to their index. |
|||
std::map<std::string, uint_fast64_t> integerVariablesToIndexMap; |
|||
|
|||
// 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. |
|||
std::map<std::string, std::shared_ptr<std::set<uint_fast64_t>>> actionsToCommandIndexMap; |
|||
}; |
|||
|
|||
} // namespace ir |
|||
|
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_MODULE_H_ */ |
|||
@ -0,0 +1,145 @@ |
|||
/*
|
|||
* Program.cpp |
|||
* |
|||
* Created on: 12.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include "Program.h"
|
|||
#include "exceptions/InvalidArgumentException.h"
|
|||
|
|||
#include <sstream>
|
|||
#include <iostream>
|
|||
|
|||
#include "log4cplus/logger.h"
|
|||
#include "log4cplus/loggingmacros.h"
|
|||
extern log4cplus::Logger logger; |
|||
|
|||
namespace storm { |
|||
|
|||
namespace ir { |
|||
|
|||
// Initializes all members with their default constructors.
|
|||
Program::Program() : modelType(UNDEFINED), booleanUndefinedConstantExpressions(), integerUndefinedConstantExpressions(), doubleUndefinedConstantExpressions(), modules(), rewards(), actions(), actionsToModuleIndexMap() { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
// Initializes all members according to the given values.
|
|||
Program::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) |
|||
: modelType(modelType), booleanUndefinedConstantExpressions(booleanUndefinedConstantExpressions), integerUndefinedConstantExpressions(integerUndefinedConstantExpressions), doubleUndefinedConstantExpressions(doubleUndefinedConstantExpressions), modules(modules), rewards(rewards), labels(labels), actionsToModuleIndexMap() { |
|||
// Build actionsToModuleIndexMap
|
|||
for (unsigned int id = 0; id < this->modules.size(); id++) { |
|||
for (auto action : this->modules[id].getActions()) { |
|||
if (this->actionsToModuleIndexMap.count(action) == 0) { |
|||
this->actionsToModuleIndexMap[action] = std::set<uint_fast64_t>(); |
|||
} |
|||
this->actionsToModuleIndexMap[action].insert(id); |
|||
this->actions.insert(action); |
|||
} |
|||
} |
|||
} |
|||
|
|||
Program::ModelType Program::getModelType() const { |
|||
return modelType; |
|||
} |
|||
|
|||
// Build a string representation of the program.
|
|||
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 element : booleanUndefinedConstantExpressions) { |
|||
result << "const bool " << element.first << " [" << element.second->toString() << "]" << ";" << std::endl; |
|||
} |
|||
for (auto element : integerUndefinedConstantExpressions) { |
|||
result << "const int " << element.first << " [" << element.second->toString() << "]" << ";" << std::endl; |
|||
} |
|||
for (auto element : doubleUndefinedConstantExpressions) { |
|||
result << "const double " << element.first << " [" << element.second->toString() << "]" << ";" << std::endl; |
|||
} |
|||
result << std::endl; |
|||
|
|||
for (auto module : modules) { |
|||
result << module.toString() << std::endl; |
|||
} |
|||
|
|||
for (auto rewardModel : rewards) { |
|||
result << rewardModel.first << ": " << rewardModel.second.toString() << std::endl; |
|||
} |
|||
|
|||
for (auto label : labels) { |
|||
result << "label " << label.first << " = " << label.second->toString() <<";" << std::endl; |
|||
} |
|||
|
|||
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]; |
|||
} |
|||
|
|||
// Return set of actions.
|
|||
std::set<std::string> const& Program::getActions() const { |
|||
return this->actions; |
|||
} |
|||
|
|||
// Return modules with given action.
|
|||
std::set<uint_fast64_t> const Program::getModulesByAction(std::string const& action) const { |
|||
auto res = this->actionsToModuleIndexMap.find(action); |
|||
if (res == this->actionsToModuleIndexMap.end()) { |
|||
return std::set<uint_fast64_t>(); |
|||
} else { |
|||
return res->second; |
|||
} |
|||
} |
|||
|
|||
storm::ir::RewardModel Program::getRewardModel(std::string const & name) const { |
|||
auto it = this->rewards.find(name); |
|||
if (it == this->rewards.end()) { |
|||
LOG4CPLUS_ERROR(logger, "The given reward model \"" << name << "\" does not exist. We will proceed without rewards."); |
|||
throw "Rewardmodel does not exist."; |
|||
} else { |
|||
return it->second; |
|||
} |
|||
} |
|||
|
|||
std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> Program::getLabels() const { |
|||
return this->labels; |
|||
} |
|||
|
|||
std::string Program::getVariableString() const { |
|||
std::map<unsigned int, std::string> bools; |
|||
std::map<unsigned int, std::string> ints; |
|||
unsigned maxInt = 0, maxBool = 0; |
|||
for (Module module: this->modules) { |
|||
for (unsigned int i = 0; i < module.getNumberOfBooleanVariables(); i++) { |
|||
storm::ir::BooleanVariable var = module.getBooleanVariable(i); |
|||
bools[var.getIndex()] = var.getName(); |
|||
if (var.getIndex() >= maxBool) maxBool = var.getIndex()+1; |
|||
} |
|||
for (unsigned int i = 0; i < module.getNumberOfIntegerVariables(); i++) { |
|||
storm::ir::IntegerVariable var = module.getIntegerVariable(i); |
|||
ints[var.getIndex()] = var.getName(); |
|||
if (var.getIndex() >= maxInt) maxInt = var.getIndex()+1; |
|||
} |
|||
} |
|||
std::stringstream ss; |
|||
for (unsigned int i = 0; i < maxBool; i++) ss << bools[i] << "\t"; |
|||
for (unsigned int i = 0; i < maxInt; i++) ss << ints[i] << "\t"; |
|||
return ss.str(); |
|||
} |
|||
|
|||
} // namespace ir
|
|||
|
|||
} // namepsace storm
|
|||
@ -0,0 +1,151 @@ |
|||
/* |
|||
* Program.h |
|||
* |
|||
* Created on: 04.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_PROGRAM_H_ |
|||
#define STORM_IR_PROGRAM_H_ |
|||
|
|||
#include "expressions/BaseExpression.h" |
|||
#include "expressions/BooleanConstantExpression.h" |
|||
#include "expressions/IntegerConstantExpression.h" |
|||
#include "expressions/DoubleConstantExpression.h" |
|||
#include "Module.h" |
|||
#include "RewardModel.h" |
|||
|
|||
#include <map> |
|||
#include <vector> |
|||
#include <memory> |
|||
#include <set> |
|||
|
|||
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 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::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 the model type of the model. |
|||
* @returns the type of the model. |
|||
*/ |
|||
ModelType getModelType() const; |
|||
|
|||
/*! |
|||
* Retrieves a string representation of this program. |
|||
* @returns a string representation of this program. |
|||
*/ |
|||
std::string toString() const; |
|||
|
|||
/*! |
|||
* Retrieves the set of actions present in this module. |
|||
* @returns the set of actions present in this module. |
|||
*/ |
|||
std::set<std::string> const& getActions() const; |
|||
|
|||
/*! |
|||
* Retrieved the indices of all Modules within this program that contain |
|||
* commands that are labelled with the given action. |
|||
* @param action Name of the action. |
|||
* @returns Indices of all matching modules. |
|||
*/ |
|||
std::set<uint_fast64_t> const getModulesByAction(std::string const& action) const; |
|||
|
|||
/*! |
|||
* Retrieve reward model with given name. |
|||
* @param name Name of the reward model. |
|||
* @return Reward model with given name. |
|||
*/ |
|||
storm::ir::RewardModel getRewardModel(std::string const & name) const; |
|||
|
|||
/*! |
|||
* Retrieves all labels. |
|||
* @return All labels. |
|||
*/ |
|||
std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> getLabels() const; |
|||
|
|||
std::string getVariableString() const; |
|||
|
|||
private: |
|||
// The type of the model. |
|||
ModelType modelType; |
|||
|
|||
// A map of undefined boolean constants to their expression nodes. |
|||
std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> booleanUndefinedConstantExpressions; |
|||
|
|||
// A map of undefined integer constants to their expressions nodes. |
|||
std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> integerUndefinedConstantExpressions; |
|||
|
|||
// A map of undefined double constants to their expressions nodes. |
|||
std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> doubleUndefinedConstantExpressions; |
|||
|
|||
// 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::shared_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; |
|||
}; |
|||
|
|||
} // namespace ir |
|||
|
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_PROGRAM_H_ */ |
|||
@ -0,0 +1,58 @@ |
|||
/*
|
|||
* RewardModel.cpp |
|||
* |
|||
* Created on: 12.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include "RewardModel.h"
|
|||
|
|||
#include <sstream>
|
|||
|
|||
namespace storm { |
|||
|
|||
namespace ir { |
|||
|
|||
// Initializes all members with their default constructors.
|
|||
RewardModel::RewardModel() : rewardModelName(), stateRewards(), transitionRewards() { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
// Initializes all members according to the given values.
|
|||
RewardModel::RewardModel(std::string rewardModelName, std::vector<storm::ir::StateReward> stateRewards, std::vector<storm::ir::TransitionReward> transitionRewards) : rewardModelName(rewardModelName), stateRewards(stateRewards), transitionRewards(transitionRewards) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
// Build a string representation of the reward model.
|
|||
std::string RewardModel::toString() const { |
|||
std::stringstream result; |
|||
result << "rewards \"" << rewardModelName << "\"" << std::endl; |
|||
for (auto reward : stateRewards) { |
|||
result << reward.toString() << std::endl; |
|||
} |
|||
for (auto 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> RewardModel::getStateRewards() const { |
|||
return this->stateRewards; |
|||
} |
|||
|
|||
bool RewardModel::hasTransitionRewards() const { |
|||
return this->transitionRewards.size() > 0; |
|||
} |
|||
|
|||
std::vector<storm::ir::TransitionReward> RewardModel::getTransitionRewards() const { |
|||
return this->transitionRewards; |
|||
} |
|||
|
|||
} // namespace ir
|
|||
|
|||
} // namespace storm
|
|||
@ -0,0 +1,84 @@ |
|||
/* |
|||
* RewardModel.h |
|||
* |
|||
* Created on: 04.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_REWARDMODEL_H_ |
|||
#define STORM_IR_REWARDMODEL_H_ |
|||
|
|||
#include "StateReward.h" |
|||
#include "TransitionReward.h" |
|||
|
|||
#include <string> |
|||
#include <vector> |
|||
|
|||
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 reward. |
|||
* @param transitionRewards A vector of transition-based reward. |
|||
*/ |
|||
RewardModel(std::string rewardModelName, std::vector<storm::ir::StateReward> stateRewards, std::vector<storm::ir::TransitionReward> transitionRewards); |
|||
|
|||
/*! |
|||
* Retrieves a string representation of this variable. |
|||
* @returns a string representation of this variable. |
|||
*/ |
|||
std::string toString() const; |
|||
|
|||
/*! |
|||
* Check, if there are any state rewards. |
|||
* @return True, iff there are any state rewards. |
|||
*/ |
|||
bool hasStateRewards() const; |
|||
|
|||
/*! |
|||
* Retrieve state rewards. |
|||
* @return State rewards. |
|||
*/ |
|||
std::vector<storm::ir::StateReward> getStateRewards() const; |
|||
|
|||
/*! |
|||
* Check, if there are any transition rewards. |
|||
* @return True, iff there are any transition rewards. |
|||
*/ |
|||
bool hasTransitionRewards() const; |
|||
|
|||
/*! |
|||
* Retrieve transition rewards. |
|||
* @return Transition rewards. |
|||
*/ |
|||
std::vector<storm::ir::TransitionReward> 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_ */ |
|||
@ -0,0 +1,42 @@ |
|||
/*
|
|||
* StateReward.cpp |
|||
* |
|||
* Created on: 12.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include "StateReward.h"
|
|||
|
|||
#include <sstream>
|
|||
|
|||
namespace storm { |
|||
|
|||
namespace ir { |
|||
|
|||
// Initializes all members with their default constructors.
|
|||
StateReward::StateReward() : statePredicate(), rewardValue() { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
// Initializes all members according to the given values.
|
|||
StateReward::StateReward(std::shared_ptr<storm::ir::expressions::BaseExpression> statePredicate, std::shared_ptr<storm::ir::expressions::BaseExpression> rewardValue) : statePredicate(statePredicate), rewardValue(rewardValue) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
// Build a string representation of the state reward.
|
|||
std::string StateReward::toString() const { |
|||
std::stringstream result; |
|||
result << "\t" << statePredicate->toString() << ": " << rewardValue->toString() << ";"; |
|||
return result.str(); |
|||
} |
|||
|
|||
double StateReward::getReward(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const * state) const { |
|||
if (this->statePredicate->getValueAsBool(state)) { |
|||
return this->rewardValue->getValueAsDouble(state); |
|||
} |
|||
return 0; |
|||
} |
|||
|
|||
} // namespace ir
|
|||
|
|||
} // namespace storm
|
|||
@ -0,0 +1,65 @@ |
|||
/* |
|||
* StateReward.h |
|||
* |
|||
* Created on: Jan 10, 2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_STATEREWARD_H_ |
|||
#define STORM_IR_STATEREWARD_H_ |
|||
|
|||
#include "expressions/BaseExpression.h" |
|||
|
|||
#include <memory> |
|||
|
|||
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::shared_ptr<storm::ir::expressions::BaseExpression> statePredicate, std::shared_ptr<storm::ir::expressions::BaseExpression> rewardValue); |
|||
|
|||
/*! |
|||
* Retrieves a string representation of this state reward. |
|||
* @returns a string representation of this state reward. |
|||
*/ |
|||
std::string toString() const; |
|||
|
|||
/*! |
|||
* Returns the reward for the given state. |
|||
* It the state fulfills the predicate, the reward value is returned, zero otherwise. |
|||
* @param state State object. |
|||
* @return Reward for given state. |
|||
*/ |
|||
double getReward(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const * state) const; |
|||
|
|||
private: |
|||
// The predicate that characterizes the states that obtain this reward. |
|||
std::shared_ptr<storm::ir::expressions::BaseExpression> statePredicate; |
|||
|
|||
// The expression that specifies the value of the reward obtained. |
|||
std::shared_ptr<storm::ir::expressions::BaseExpression> rewardValue; |
|||
}; |
|||
|
|||
} // namespace ir |
|||
|
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_STATEREWARD_H_ */ |
|||
@ -0,0 +1,43 @@ |
|||
/*
|
|||
* TransitionReward.cpp |
|||
* |
|||
* Created on: 12.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include "TransitionReward.h"
|
|||
|
|||
#include <sstream>
|
|||
|
|||
namespace storm { |
|||
|
|||
namespace ir { |
|||
|
|||
// Initializes all members with their default constructors.
|
|||
TransitionReward::TransitionReward() : commandName(), statePredicate(), rewardValue() { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
// Initializes all members according to the given values.
|
|||
TransitionReward::TransitionReward(std::string commandName, std::shared_ptr<storm::ir::expressions::BaseExpression> statePredicate, std::shared_ptr<storm::ir::expressions::BaseExpression> rewardValue) : commandName(commandName), statePredicate(statePredicate), rewardValue(rewardValue) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
// Build a string representation of the transition reward.
|
|||
std::string TransitionReward::toString() const { |
|||
std::stringstream result; |
|||
result << "\t[" << commandName << "] " << statePredicate->toString() << ": " << rewardValue->toString() << ";"; |
|||
return result.str(); |
|||
} |
|||
|
|||
double TransitionReward::getReward(std::string const & label, std::pair<std::vector<bool>, std::vector<int_fast64_t>> const * state) const { |
|||
if (this->commandName != label) return 0; |
|||
if (this->statePredicate->getValueAsBool(state)) { |
|||
return this->rewardValue->getValueAsDouble(state); |
|||
} |
|||
return 0; |
|||
} |
|||
|
|||
} // namespace ir
|
|||
|
|||
} // namespace storm
|
|||
@ -0,0 +1,68 @@ |
|||
/* |
|||
* TransitionReward.h |
|||
* |
|||
* Created on: Jan 10, 2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_TRANSITIONREWARD_H_ |
|||
#define STORM_IR_TRANSITIONREWARD_H_ |
|||
|
|||
#include "expressions/BaseExpression.h" |
|||
|
|||
#include <memory> |
|||
|
|||
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 commandName, std::shared_ptr<storm::ir::expressions::BaseExpression> statePredicate, std::shared_ptr<storm::ir::expressions::BaseExpression> rewardValue); |
|||
|
|||
/*! |
|||
* Retrieves a string representation of this transition reward. |
|||
* @returns a string representation of this transition reward. |
|||
*/ |
|||
std::string toString() const; |
|||
|
|||
/*! |
|||
* Retrieves reward for given transition. |
|||
* Returns reward value if source state fulfills predicate and the transition is labeled correctly, zero otherwise. |
|||
*/ |
|||
double getReward(std::string const & label, std::pair<std::vector<bool>, std::vector<int_fast64_t>> const * state) 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::shared_ptr<storm::ir::expressions::BaseExpression> statePredicate; |
|||
|
|||
// The expression specifying the value of the reward obtained along the transitions. |
|||
std::shared_ptr<storm::ir::expressions::BaseExpression> rewardValue; |
|||
}; |
|||
|
|||
} // namespace ir |
|||
|
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_TRANSITIONREWARD_H_ */ |
|||
@ -0,0 +1,118 @@ |
|||
/*
|
|||
* Update.cpp |
|||
* |
|||
* Created on: 12.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include "Update.h"
|
|||
|
|||
#include "src/exceptions/OutOfRangeException.h"
|
|||
|
|||
#include <sstream>
|
|||
|
|||
namespace storm { |
|||
|
|||
namespace ir { |
|||
|
|||
// Initializes all members with their default constructors.
|
|||
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> booleanAssignments, std::map<std::string, storm::ir::Assignment> integerAssignments) |
|||
: likelihoodExpression(likelihoodExpression), booleanAssignments(booleanAssignments), integerAssignments(integerAssignments) { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
Update::Update(const Update& update, const std::map<std::string, std::string>& renaming, const std::map<std::string,uint_fast64_t>& bools, const std::map<std::string,uint_fast64_t>& ints) { |
|||
for (auto it : update.booleanAssignments) { |
|||
if (renaming.count(it.first) > 0) { |
|||
this->booleanAssignments[renaming.at(it.first)] = Assignment(it.second, renaming, bools, ints); |
|||
} else { |
|||
this->booleanAssignments[it.first] = Assignment(it.second, renaming, bools, ints); |
|||
} |
|||
} |
|||
for (auto it : update.integerAssignments) { |
|||
if (renaming.count(it.first) > 0) { |
|||
this->integerAssignments[renaming.at(it.first)] = Assignment(it.second, renaming, bools, ints); |
|||
} else { |
|||
this->integerAssignments[it.first] = Assignment(it.second, renaming, bools, ints); |
|||
} |
|||
} |
|||
this->likelihoodExpression = update.likelihoodExpression->clone(renaming, bools, ints); |
|||
} |
|||
|
|||
// 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 : booleanAssignments) { |
|||
result << assignment.second.toString(); |
|||
if (i < booleanAssignments.size() - 1 || integerAssignments.size() > 0) { |
|||
result << " & "; |
|||
} |
|||
++i; |
|||
} |
|||
i = 0; |
|||
for (auto assignment : integerAssignments) { |
|||
result << assignment.second.toString(); |
|||
if (i < integerAssignments.size() - 1) { |
|||
result << " & "; |
|||
} |
|||
++i; |
|||
} |
|||
return result.str(); |
|||
} |
|||
|
|||
} // namespace ir
|
|||
|
|||
} // namespace storm
|
|||
@ -0,0 +1,104 @@ |
|||
/* |
|||
* Update.h |
|||
* |
|||
* Created on: 06.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_UPDATE_H_ |
|||
#define STORM_IR_UPDATE_H_ |
|||
|
|||
#include "expressions/BaseExpression.h" |
|||
#include "Assignment.h" |
|||
|
|||
#include <map> |
|||
#include <memory> |
|||
|
|||
namespace storm { |
|||
|
|||
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 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> booleanAssignments, std::map<std::string, storm::ir::Assignment> integerAssignments); |
|||
|
|||
Update(const Update& update, const std::map<std::string, std::string>& renaming, const std::map<std::string,uint_fast64_t>& bools, const std::map<std::string,uint_fast64_t>& ints); |
|||
|
|||
/*! |
|||
* 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. |
|||
* @returns a string representation of this update. |
|||
*/ |
|||
std::string toString() const; |
|||
|
|||
private: |
|||
// An expression specifying the likelihood of taking this update. |
|||
std::shared_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; |
|||
}; |
|||
|
|||
} // namespace ir |
|||
|
|||
} // namespace storm |
|||
|
|||
#endif /*STORM_IR_UPDATE_H_ */ |
|||
@ -0,0 +1,58 @@ |
|||
/*
|
|||
* Variable.cpp |
|||
* |
|||
* Created on: 12.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include "Variable.h"
|
|||
|
|||
#include <sstream>
|
|||
#include <map>
|
|||
#include <iostream>
|
|||
|
|||
namespace storm { |
|||
|
|||
namespace ir { |
|||
|
|||
// Initializes all members with their default constructors.
|
|||
Variable::Variable() : index(0), variableName(), initialValue() { |
|||
// Nothing to do here.
|
|||
} |
|||
|
|||
// Initializes all members according to the given values.
|
|||
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.
|
|||
} |
|||
|
|||
Variable::Variable(const Variable& var, const std::string& newName, const uint_fast64_t newIndex, const std::map<std::string, std::string>& renaming, const std::map<std::string,uint_fast64_t>& bools, const std::map<std::string,uint_fast64_t>& ints) { |
|||
this->index = newIndex; |
|||
this->variableName = newName; |
|||
if (var.initialValue != nullptr) { |
|||
this->initialValue = var.initialValue->clone(renaming, bools, ints); |
|||
} |
|||
} |
|||
|
|||
// Return the name of the variable.
|
|||
std::string const& Variable::getName() const { |
|||
return variableName; |
|||
} |
|||
|
|||
uint_fast64_t Variable::getIndex() const { |
|||
return index; |
|||
} |
|||
|
|||
// Return the expression for the initial value of the variable.
|
|||
std::shared_ptr<storm::ir::expressions::BaseExpression> const& Variable::getInitialValue() const { |
|||
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
|
|||
@ -0,0 +1,85 @@ |
|||
/* |
|||
* Variable.h |
|||
* |
|||
* Created on: 06.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_VARIABLE_H_ |
|||
#define STORM_IR_VARIABLE_H_ |
|||
|
|||
#include "expressions/BaseExpression.h" |
|||
|
|||
#include <string> |
|||
#include <memory> |
|||
|
|||
namespace storm { |
|||
|
|||
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 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(uint_fast64_t index, std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>()); |
|||
|
|||
/*! |
|||
* Creates a copy of the given Variable and gives it a new name. |
|||
* @param var Variable to copy. |
|||
* @param newName New name of this variable. |
|||
*/ |
|||
Variable(const Variable& var, const std::string& newName, const uint_fast64_t newIndex, const std::map<std::string, std::string>& renaming, const std::map<std::string,uint_fast64_t>& bools, const std::map<std::string,uint_fast64_t>& ints); |
|||
|
|||
/*! |
|||
* Retrieves the name of the variable. |
|||
* @returns the name of the variable. |
|||
*/ |
|||
std::string const& getName() const; |
|||
|
|||
/*! |
|||
* Retrieves the index of the variable. |
|||
* @returns the index of the variable. |
|||
*/ |
|||
uint_fast64_t getIndex() const; |
|||
|
|||
/*! |
|||
* Retrieves the expression defining the initial value of the variable. |
|||
* @returns the expression defining the initial value of the variable. |
|||
*/ |
|||
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; |
|||
|
|||
// The expression defining the initial value of the variable. |
|||
std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue; |
|||
}; |
|||
|
|||
} // namespace ir |
|||
|
|||
} // namespace storm |
|||
|
|||
|
|||
#endif /* STORM_IR_VARIABLE_H_ */ |
|||
@ -0,0 +1,105 @@ |
|||
/* |
|||
* Expression.h |
|||
* |
|||
* Created on: 03.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_EXPRESSIONS_BASEEXPRESSION_H_ |
|||
#define STORM_IR_EXPRESSIONS_BASEEXPRESSION_H_ |
|||
|
|||
#include "src/exceptions/ExpressionEvaluationException.h" |
|||
#include "src/exceptions/NotImplementedException.h" |
|||
|
|||
#include "ExpressionVisitor.h" |
|||
|
|||
#include <string> |
|||
#include <vector> |
|||
#include <map> |
|||
#include <memory> |
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
class BaseExpression { |
|||
|
|||
public: |
|||
enum ReturnType {undefined, bool_, int_, double_}; |
|||
|
|||
BaseExpression() : type(undefined) { |
|||
|
|||
} |
|||
|
|||
BaseExpression(ReturnType type) : type(type) { |
|||
|
|||
} |
|||
BaseExpression(const BaseExpression& be) |
|||
: type(be.type) { |
|||
} |
|||
|
|||
virtual ~BaseExpression() { |
|||
|
|||
} |
|||
|
|||
virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) = 0; |
|||
|
|||
virtual int_fast64_t 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."; |
|||
} |
|||
|
|||
virtual bool 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."; |
|||
} |
|||
|
|||
virtual double getValueAsDouble(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 'double'."; |
|||
} |
|||
throw storm::exceptions::NotImplementedException() << "Cannot evaluate expression of type '" |
|||
<< this->getTypeName() << " because evaluation implementation is missing."; |
|||
} |
|||
|
|||
virtual void accept(ExpressionVisitor* visitor) { |
|||
visitor->visit(this); |
|||
} |
|||
|
|||
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; |
|||
} |
|||
|
|||
virtual std::string dump(std::string prefix) const = 0; |
|||
|
|||
private: |
|||
ReturnType type; |
|||
}; |
|||
|
|||
} // namespace expressions |
|||
|
|||
} // namespace ir |
|||
|
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_EXPRESSIONS_BASEEXPRESSION_H_ */ |
|||
@ -0,0 +1,91 @@ |
|||
/* |
|||
* BinaryBooleanFunctionExpression.h |
|||
* |
|||
* Created on: 03.01.2013 |
|||
* Author: chris |
|||
*/ |
|||
|
|||
#ifndef STORM_IR_EXPRESSIONS_BINARYBOOLEANFUNCTIONEXPRESSION_H_ |
|||
#define STORM_IR_EXPRESSIONS_BINARYBOOLEANFUNCTIONEXPRESSION_H_ |
|||
|
|||
#include "src/ir/expressions/BinaryExpression.h" |
|||
|
|||
#include <memory> |
|||
#include <sstream> |
|||
|
|||
namespace storm { |
|||
|
|||
namespace ir { |
|||
|
|||
namespace expressions { |
|||
|
|||
class BinaryBooleanFunctionExpression : public BinaryExpression { |
|||
public: |
|||
enum FunctionType {AND, OR}; |
|||
|
|||
BinaryBooleanFunctionExpression(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right, FunctionType functionType) : BinaryExpression(bool_, left, right), functionType(functionType) { |
|||
|
|||
} |
|||
|
|||
virtual ~BinaryBooleanFunctionExpression() { |
|||
|
|||
} |
|||
|
|||
virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) { |
|||
return std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(this->getLeft()->clone(renaming, bools, ints), this->getRight()->clone(renaming, bools, ints), this->functionType)); |
|||
} |
|||
|
|||
virtual bool 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 << "'."; |
|||
} |
|||
} |
|||
|
|||
FunctionType getFunctionType() const { |
|||
return functionType; |
|||
} |
|||
|
|||
virtual void accept(ExpressionVisitor* visitor) { |
|||
visitor->visit(this); |
|||
} |
|||
|
|||
virtual std::string 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(); |
|||
} |
|||
|
|||
virtual std::string dump(std::string prefix) const { |
|||
std::stringstream result; |
|||
result << prefix << "BinaryBooleanFunctionExpression" << std::endl; |
|||
result << this->getLeft()->dump(prefix + "\t"); |
|||
switch (functionType) { |
|||
case AND: result << prefix << "&" << std::endl; break; |
|||
case OR: result << prefix << "|" << std::endl; break; |
|||
} |
|||
result << this->getRight()->dump(prefix + "\t"); |
|||
return result.str(); |
|||
} |
|||
|
|||
private: |
|||
FunctionType functionType; |
|||
}; |
|||
|
|||
} // namespace expressions |
|||
|
|||
} // namespace ir |
|||
|
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_EXPRESSIONS_BINARYBOOLEANFUNCTIONEXPRESSION_H_ */ |
|||
@ -0,0 +1,46 @@ |
|||
/* |
|||
* 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" |
|||
#include <memory> |
|||
#include <iostream> |
|||
|
|||
namespace storm { |
|||
|
|||
namespace ir { |
|||
|
|||
namespace expressions { |
|||
|
|||
class BinaryExpression : public BaseExpression { |
|||
public: |
|||
BinaryExpression(ReturnType type, std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right) |
|||
: BaseExpression(type), left(left), right(right) { |
|||
} |
|||
|
|||
std::shared_ptr<BaseExpression> const& getLeft() const { |
|||
return left; |
|||
} |
|||
|
|||
std::shared_ptr<BaseExpression> const& getRight() const { |
|||
return right; |
|||
} |
|||
|
|||
private: |
|||
std::shared_ptr<BaseExpression> left; |
|||
std::shared_ptr<BaseExpression> right; |
|||
}; |
|||
|
|||
} // namespace expressions |
|||
|
|||
} // namespace ir |
|||
|
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_EXPRESSIONS_BINARYEXPRESSION_H_ */ |
|||
@ -0,0 +1,112 @@ |
|||
/* |
|||
* BinaryFunctionExpression.h |
|||
* |
|||
* Created on: 03.01.2013 |
|||
* Author: chris |
|||
*/ |
|||
|
|||
#ifndef BINARYFUNCTIONEXPRESSION_H_ |
|||
#define BINARYFUNCTIONEXPRESSION_H_ |
|||
|
|||
#include "src/ir/expressions/BaseExpression.h" |
|||
|
|||
namespace storm { |
|||
|
|||
namespace ir { |
|||
|
|||
namespace expressions { |
|||
|
|||
class BinaryNumericalFunctionExpression : public BinaryExpression { |
|||
public: |
|||
enum FunctionType {PLUS, MINUS, TIMES, DIVIDE}; |
|||
|
|||
BinaryNumericalFunctionExpression(ReturnType type, std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right, FunctionType functionType) : BinaryExpression(type, left, right), functionType(functionType) { |
|||
|
|||
} |
|||
|
|||
virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) { |
|||
return std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(this->getType(), this->getLeft()->clone(renaming, bools, ints), this->getRight()->clone(renaming, bools, ints), this->functionType)); |
|||
} |
|||
|
|||
virtual ~BinaryNumericalFunctionExpression() { |
|||
|
|||
} |
|||
|
|||
FunctionType getFunctionType() const { |
|||
return functionType; |
|||
} |
|||
|
|||
virtual int_fast64_t 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; |
|||
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Unknown numeric binary operator: '" << functionType << "'."; |
|||
} |
|||
} |
|||
|
|||
virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
if (this->getType() != double_) { |
|||
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; |
|||
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Unknown numeric binary operator: '" << functionType << "'."; |
|||
} |
|||
} |
|||
|
|||
virtual void accept(ExpressionVisitor* visitor) { |
|||
visitor->visit(this); |
|||
} |
|||
|
|||
virtual std::string toString() const { |
|||
std::string result = this->getLeft()->toString(); |
|||
switch (functionType) { |
|||
case PLUS: result += " + "; break; |
|||
case MINUS: result += " - "; break; |
|||
case TIMES: result += " * "; break; |
|||
case DIVIDE: result += " / "; break; |
|||
} |
|||
result += this->getRight()->toString(); |
|||
return result; |
|||
} |
|||
|
|||
virtual std::string dump(std::string prefix) const { |
|||
std::stringstream result; |
|||
result << prefix << "BinaryNumericalFunctionExpression" << std::endl; |
|||
result << this->getLeft()->dump(prefix + "\t"); |
|||
switch (functionType) { |
|||
case PLUS: result << prefix << "+" << std::endl; break; |
|||
case MINUS: result << prefix << "-" << std::endl; break; |
|||
case TIMES: result << prefix << "*" << std::endl; break; |
|||
case DIVIDE: result << prefix << "/" << std::endl; break; |
|||
} |
|||
result << this->getRight()->dump(prefix + "\t"); |
|||
return result.str(); |
|||
} |
|||
private: |
|||
FunctionType functionType; |
|||
}; |
|||
|
|||
} |
|||
|
|||
} |
|||
|
|||
} |
|||
|
|||
#endif /* BINARYFUNCTIONEXPRESSION_H_ */ |
|||
@ -0,0 +1,98 @@ |
|||
/* |
|||
* BinaryRelationExpression.h |
|||
* |
|||
* Created on: 03.01.2013 |
|||
* Author: chris |
|||
*/ |
|||
|
|||
#ifndef BINARYRELATIONEXPRESSION_H_ |
|||
#define BINARYRELATIONEXPRESSION_H_ |
|||
|
|||
#include "src/ir/expressions/BinaryExpression.h" |
|||
#include <iostream> |
|||
|
|||
namespace storm { |
|||
|
|||
namespace ir { |
|||
|
|||
namespace expressions { |
|||
|
|||
class BinaryRelationExpression : public BinaryExpression { |
|||
public: |
|||
enum RelationType {EQUAL, NOT_EQUAL, LESS, LESS_OR_EQUAL, GREATER, GREATER_OR_EQUAL}; |
|||
|
|||
BinaryRelationExpression(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right, RelationType relationType) : BinaryExpression(bool_, left, right), relationType(relationType) { |
|||
} |
|||
|
|||
virtual ~BinaryRelationExpression() { |
|||
|
|||
} |
|||
|
|||
virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) { |
|||
return std::shared_ptr<BaseExpression>(new BinaryRelationExpression(this->getLeft()->clone(renaming, bools, ints), this->getRight()->clone(renaming, bools, ints), this->relationType)); |
|||
} |
|||
|
|||
virtual bool 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 << "'."; |
|||
} |
|||
} |
|||
|
|||
RelationType getRelationType() const { |
|||
return relationType; |
|||
} |
|||
|
|||
virtual void accept(ExpressionVisitor* visitor) { |
|||
visitor->visit(this); |
|||
} |
|||
|
|||
virtual std::string toString() const { |
|||
std::string 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; |
|||
} |
|||
virtual std::string dump(std::string prefix) const { |
|||
std::stringstream result; |
|||
result << prefix << "BinaryRelationExpression" << std::endl; |
|||
result << this->getLeft()->dump(prefix + "\t"); |
|||
switch (relationType) { |
|||
case EQUAL: result << prefix << "=" << std::endl; break; |
|||
case NOT_EQUAL: result << prefix << "!=" << std::endl; break; |
|||
case LESS: result << prefix << "<" << std::endl; break; |
|||
case LESS_OR_EQUAL: result << prefix << "<=" << std::endl; break; |
|||
case GREATER: result << prefix << ">" << std::endl; break; |
|||
case GREATER_OR_EQUAL: result << prefix << ">=" << std::endl; break; |
|||
} |
|||
result << this->getRight()->dump(prefix + "\t"); |
|||
return result.str(); |
|||
} |
|||
|
|||
private: |
|||
RelationType relationType; |
|||
}; |
|||
|
|||
} |
|||
|
|||
} |
|||
|
|||
} |
|||
|
|||
#endif /* BINARYRELATIONEXPRESSION_H_ */ |
|||
@ -0,0 +1,89 @@ |
|||
/* |
|||
* BooleanConstantExpression.h |
|||
* |
|||
* Created on: 04.01.2013 |
|||
* Author: chris |
|||
*/ |
|||
|
|||
#ifndef BOOLEANCONSTANTEXPRESSION_H_ |
|||
#define BOOLEANCONSTANTEXPRESSION_H_ |
|||
|
|||
#include "ConstantExpression.h" |
|||
|
|||
#include <boost/lexical_cast.hpp> |
|||
|
|||
namespace storm { |
|||
|
|||
namespace ir { |
|||
|
|||
namespace expressions { |
|||
|
|||
class BooleanConstantExpression : public ConstantExpression { |
|||
public: |
|||
BooleanConstantExpression(std::string constantName) : ConstantExpression(bool_, constantName) { |
|||
defined = false; |
|||
value = false; |
|||
} |
|||
BooleanConstantExpression(const BooleanConstantExpression& bce) |
|||
: ConstantExpression(bce), value(bce.value), defined(bce.defined) { |
|||
} |
|||
|
|||
virtual ~BooleanConstantExpression() { |
|||
|
|||
} |
|||
|
|||
virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) { |
|||
return std::shared_ptr<BaseExpression>(new BooleanConstantExpression(*this)); |
|||
} |
|||
|
|||
virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
if (!defined) { |
|||
throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Boolean constant '" << this->getConstantName() << "' is undefined."; |
|||
} else { |
|||
return value; |
|||
} |
|||
} |
|||
|
|||
virtual void accept(ExpressionVisitor* visitor) { |
|||
visitor->visit(this); |
|||
} |
|||
|
|||
virtual std::string toString() const { |
|||
std::string result = this->constantName; |
|||
if (defined) { |
|||
result += "[" + boost::lexical_cast<std::string>(value) + "]"; |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
virtual std::string dump(std::string prefix) const { |
|||
std::stringstream result; |
|||
result << prefix << "BooleanConstantExpression " << this->toString() << std::endl; |
|||
return result.str(); |
|||
} |
|||
|
|||
bool isDefined() { |
|||
return defined; |
|||
} |
|||
|
|||
bool getValue() { |
|||
return value; |
|||
} |
|||
|
|||
void define(bool value) { |
|||
defined = true; |
|||
this->value = value; |
|||
} |
|||
|
|||
bool value; |
|||
bool defined; |
|||
}; |
|||
|
|||
} |
|||
|
|||
} |
|||
|
|||
} |
|||
|
|||
#endif /* BOOLEANCONSTANTEXPRESSION_H_ */ |
|||
@ -0,0 +1,62 @@ |
|||
/* |
|||
* BooleanLiteral.h |
|||
* |
|||
* Created on: 03.01.2013 |
|||
* Author: chris |
|||
*/ |
|||
|
|||
#ifndef BOOLEANLITERAL_H_ |
|||
#define BOOLEANLITERAL_H_ |
|||
|
|||
#include "src/ir/expressions/BaseExpression.h" |
|||
|
|||
namespace storm { |
|||
namespace ir { |
|||
namespace expressions { |
|||
|
|||
class BooleanLiteral : public BaseExpression { |
|||
public: |
|||
bool value; |
|||
|
|||
BooleanLiteral(bool value) : BaseExpression(bool_), value(value) { |
|||
|
|||
} |
|||
|
|||
virtual ~BooleanLiteral() { |
|||
|
|||
} |
|||
|
|||
virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) { |
|||
return std::shared_ptr<BaseExpression>(new BooleanLiteral(this->value)); |
|||
} |
|||
|
|||
virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
return value; |
|||
} |
|||
|
|||
virtual void accept(ExpressionVisitor* visitor) { |
|||
visitor->visit(this); |
|||
} |
|||
|
|||
virtual std::string toString() const { |
|||
if (value) { |
|||
return std::string("true"); |
|||
} else { |
|||
return std::string("false"); |
|||
} |
|||
} |
|||
|
|||
virtual std::string dump(std::string prefix) const { |
|||
std::stringstream result; |
|||
result << prefix << "BooleanLiteral " << this->toString() << std::endl; |
|||
return result.str(); |
|||
} |
|||
}; |
|||
|
|||
} |
|||
|
|||
} |
|||
|
|||
} |
|||
|
|||
#endif /* BOOLEANLITERAL_H_ */ |
|||
@ -0,0 +1,55 @@ |
|||
/* |
|||
* ConstantExpression.h |
|||
* |
|||
* Created on: 03.01.2013 |
|||
* Author: chris |
|||
*/ |
|||
|
|||
#ifndef CONSTANTEXPRESSION_H_ |
|||
#define CONSTANTEXPRESSION_H_ |
|||
|
|||
#include "src/ir/expressions/BaseExpression.h" |
|||
|
|||
namespace storm { |
|||
|
|||
namespace ir { |
|||
|
|||
namespace expressions { |
|||
|
|||
class ConstantExpression : public BaseExpression { |
|||
public: |
|||
std::string constantName; |
|||
|
|||
ConstantExpression(ReturnType type, std::string constantName) : BaseExpression(type), constantName(constantName) { |
|||
} |
|||
ConstantExpression(const ConstantExpression& ce) |
|||
: BaseExpression(ce), constantName(ce.constantName) { |
|||
|
|||
} |
|||
|
|||
virtual ~ConstantExpression() { |
|||
|
|||
} |
|||
|
|||
std::string const& getConstantName() const { |
|||
return constantName; |
|||
} |
|||
|
|||
virtual std::string toString() const { |
|||
return constantName; |
|||
} |
|||
|
|||
virtual std::string dump(std::string prefix) const { |
|||
std::stringstream result; |
|||
result << prefix << "ConstantExpression " << this->toString() << std::endl; |
|||
return result.str(); |
|||
} |
|||
}; |
|||
|
|||
} |
|||
|
|||
} |
|||
|
|||
} |
|||
|
|||
#endif /* CONSTANTEXPRESSION_H_ */ |
|||
@ -0,0 +1,87 @@ |
|||
/* |
|||
* DoubleConstantExpression.h |
|||
* |
|||
* Created on: 04.01.2013 |
|||
* Author: chris |
|||
*/ |
|||
|
|||
#ifndef DOUBLECONSTANTEXPRESSION_H_ |
|||
#define DOUBLECONSTANTEXPRESSION_H_ |
|||
|
|||
#include "ConstantExpression.h" |
|||
|
|||
namespace storm { |
|||
|
|||
namespace ir { |
|||
|
|||
namespace expressions { |
|||
|
|||
class DoubleConstantExpression : public ConstantExpression { |
|||
public: |
|||
DoubleConstantExpression(std::string constantName) : ConstantExpression(double_, constantName), defined(false), value(0) { |
|||
} |
|||
|
|||
DoubleConstantExpression(const DoubleConstantExpression& dce) |
|||
: ConstantExpression(dce), defined(dce.defined), value(dce.value) { |
|||
} |
|||
|
|||
virtual ~DoubleConstantExpression() { |
|||
|
|||
} |
|||
|
|||
virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) { |
|||
return std::shared_ptr<BaseExpression>(new DoubleConstantExpression(*this)); |
|||
} |
|||
|
|||
virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
if (!defined) { |
|||
throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Double constant '" << this->getConstantName() << "' is undefined."; |
|||
} else { |
|||
return value; |
|||
} |
|||
} |
|||
|
|||
virtual void accept(ExpressionVisitor* visitor) { |
|||
visitor->visit(this); |
|||
} |
|||
|
|||
virtual std::string toString() const { |
|||
std::string result = this->constantName; |
|||
if (defined) { |
|||
result += "[" + boost::lexical_cast<std::string>(value) + "]"; |
|||
} |
|||
return result; |
|||
} |
|||
|
|||
virtual std::string dump(std::string prefix) const { |
|||
std::stringstream result; |
|||
result << prefix << "DoubleConstantExpression " << this->toString() << std::endl; |
|||
return result.str(); |
|||
} |
|||
|
|||
bool isDefined() { |
|||
return defined; |
|||
} |
|||
|
|||
double getValue() { |
|||
return value; |
|||
} |
|||
|
|||
void define(double value) { |
|||
defined = true; |
|||
this->value = value; |
|||
} |
|||
|
|||
private: |
|||
bool defined; |
|||
double value; |
|||
}; |
|||
|
|||
} |
|||
|
|||
} |
|||
|
|||
} |
|||
|
|||
#endif /* DOUBLECONSTANTEXPRESSION_H_ */ |
|||
@ -0,0 +1,62 @@ |
|||
/* |
|||
* DoubleLiteral.h |
|||
* |
|||
* Created on: 03.01.2013 |
|||
* Author: chris |
|||
*/ |
|||
|
|||
#ifndef DOUBLELITERAL_H_ |
|||
#define DOUBLELITERAL_H_ |
|||
|
|||
#include "src/ir/expressions/BaseExpression.h" |
|||
|
|||
#include "boost/lexical_cast.hpp" |
|||
|
|||
namespace storm { |
|||
|
|||
namespace ir { |
|||
|
|||
namespace expressions { |
|||
|
|||
class DoubleLiteral : public BaseExpression { |
|||
public: |
|||
double value; |
|||
|
|||
DoubleLiteral(double value) : BaseExpression(double_), value(value) { |
|||
|
|||
} |
|||
|
|||
virtual ~DoubleLiteral() { |
|||
|
|||
} |
|||
|
|||
virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) { |
|||
return std::shared_ptr<BaseExpression>(new DoubleLiteral(this->value)); |
|||
} |
|||
|
|||
virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
return value; |
|||
} |
|||
|
|||
virtual void accept(ExpressionVisitor* visitor) { |
|||
visitor->visit(this); |
|||
} |
|||
|
|||
virtual std::string toString() const { |
|||
return boost::lexical_cast<std::string>(value); |
|||
} |
|||
|
|||
virtual std::string dump(std::string prefix) const { |
|||
std::stringstream result; |
|||
result << prefix << "DoubleLiteral " << this->toString() << std::endl; |
|||
return result.str(); |
|||
} |
|||
}; |
|||
|
|||
} |
|||
|
|||
} |
|||
|
|||
} |
|||
|
|||
#endif /* DOUBLELITERAL_H_ */ |
|||
@ -0,0 +1,55 @@ |
|||
/* |
|||
* 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 BooleanLiteral; |
|||
class DoubleConstantExpression; |
|||
class DoubleLiteral; |
|||
class IntegerConstantExpression; |
|||
class IntegerLiteral; |
|||
class UnaryBooleanFunctionExpression; |
|||
class UnaryNumericalFunctionExpression; |
|||
class VariableExpression; |
|||
|
|||
class ExpressionVisitor { |
|||
public: |
|||
virtual void visit(BaseExpression* expression) = 0; |
|||
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(BooleanLiteral* expression) = 0; |
|||
virtual void visit(DoubleConstantExpression* expression) = 0; |
|||
virtual void visit(DoubleLiteral* expression) = 0; |
|||
virtual void visit(IntegerConstantExpression* expression) = 0; |
|||
virtual void visit(IntegerLiteral* 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_ */ |
|||
@ -0,0 +1,26 @@ |
|||
/* |
|||
* 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 "BooleanLiteral.h" |
|||
#include "DoubleLiteral.h" |
|||
#include "IntegerLiteral.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_ */ |
|||
@ -0,0 +1,85 @@ |
|||
/* |
|||
* IntegerConstantExpression.h |
|||
* |
|||
* Created on: 04.01.2013 |
|||
* Author: chris |
|||
*/ |
|||
|
|||
#ifndef INTEGERCONSTANTEXPRESSION_H_ |
|||
#define INTEGERCONSTANTEXPRESSION_H_ |
|||
|
|||
#include "ConstantExpression.h" |
|||
|
|||
namespace storm { |
|||
|
|||
namespace ir { |
|||
|
|||
namespace expressions { |
|||
|
|||
class IntegerConstantExpression : public ConstantExpression { |
|||
public: |
|||
IntegerConstantExpression(std::string constantName) : ConstantExpression(int_, constantName), defined(false), value(0) { |
|||
} |
|||
IntegerConstantExpression(const IntegerConstantExpression& ice) |
|||
: ConstantExpression(ice), defined(ice.defined), value(ice.value) { |
|||
} |
|||
|
|||
virtual ~IntegerConstantExpression() { |
|||
|
|||
} |
|||
|
|||
virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) { |
|||
return std::shared_ptr<BaseExpression>(new IntegerConstantExpression(*this)); |
|||
} |
|||
|
|||
virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
if (!defined) { |
|||
throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Integer constant '" << this->getConstantName() << "' is undefined."; |
|||
} else { |
|||
return value; |
|||
} |
|||
} |
|||
|
|||
virtual void accept(ExpressionVisitor* visitor) { |
|||
visitor->visit(this); |
|||
} |
|||
|
|||
virtual std::string toString() const { |
|||
std::string result = this->constantName; |
|||
if (defined) { |
|||
result += "[" + boost::lexical_cast<std::string>(value) + "]"; |
|||
} |
|||
return result; |
|||
} |
|||
virtual std::string dump(std::string prefix) const { |
|||
std::stringstream result; |
|||
result << prefix << "IntegerConstantExpression " << this->toString() << std::endl; |
|||
return result.str(); |
|||
} |
|||
|
|||
bool isDefined() { |
|||
return defined; |
|||
} |
|||
|
|||
int getValue() { |
|||
return value; |
|||
} |
|||
|
|||
void define(int_fast64_t value) { |
|||
defined = true; |
|||
this->value = value; |
|||
} |
|||
|
|||
private: |
|||
bool defined; |
|||
int_fast64_t value; |
|||
}; |
|||
|
|||
} |
|||
|
|||
} |
|||
|
|||
} |
|||
|
|||
#endif /* INTEGERCONSTANTEXPRESSION_H_ */ |
|||
@ -0,0 +1,57 @@ |
|||
/* |
|||
* IntegerLiteral.h |
|||
* |
|||
* Created on: 03.01.2013 |
|||
* Author: chris |
|||
*/ |
|||
|
|||
#ifndef INTEGERLITERAL_H_ |
|||
#define INTEGERLITERAL_H_ |
|||
|
|||
#include "src/ir/expressions/BaseExpression.h" |
|||
|
|||
namespace storm { |
|||
|
|||
namespace ir { |
|||
|
|||
namespace expressions { |
|||
|
|||
class IntegerLiteral : public BaseExpression { |
|||
public: |
|||
int_fast64_t value; |
|||
|
|||
IntegerLiteral(int_fast64_t value) : BaseExpression(int_), value(value) { |
|||
} |
|||
|
|||
virtual ~IntegerLiteral() { |
|||
} |
|||
|
|||
virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) { |
|||
return std::shared_ptr<BaseExpression>(new IntegerLiteral(this->value)); |
|||
} |
|||
|
|||
virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
return value; |
|||
} |
|||
|
|||
virtual void accept(ExpressionVisitor* visitor) { |
|||
visitor->visit(this); |
|||
} |
|||
|
|||
virtual std::string toString() const { |
|||
return boost::lexical_cast<std::string>(value); |
|||
} |
|||
virtual std::string dump(std::string prefix) const { |
|||
std::stringstream result; |
|||
result << prefix << "IntegerLiteral " << this->toString() << std::endl; |
|||
return result.str(); |
|||
} |
|||
}; |
|||
|
|||
} |
|||
|
|||
} |
|||
|
|||
} |
|||
|
|||
#endif /* INTEGERLITERAL_H_ */ |
|||
@ -0,0 +1,81 @@ |
|||
/* |
|||
* UnaryBooleanFunctionExpression.h |
|||
* |
|||
* Created on: 03.01.2013 |
|||
* Author: chris |
|||
*/ |
|||
|
|||
#ifndef UNARYBOOLEANFUNCTIONEXPRESSION_H_ |
|||
#define UNARYBOOLEANFUNCTIONEXPRESSION_H_ |
|||
|
|||
#include "src/ir/expressions/UnaryExpression.h" |
|||
|
|||
namespace storm { |
|||
|
|||
namespace ir { |
|||
|
|||
namespace expressions { |
|||
|
|||
class UnaryBooleanFunctionExpression : public UnaryExpression { |
|||
public: |
|||
enum FunctionType {NOT}; |
|||
|
|||
UnaryBooleanFunctionExpression(std::shared_ptr<BaseExpression> child, FunctionType functionType) : UnaryExpression(bool_, child), functionType(functionType) { |
|||
|
|||
} |
|||
|
|||
virtual ~UnaryBooleanFunctionExpression() { |
|||
|
|||
} |
|||
|
|||
virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) { |
|||
return std::shared_ptr<BaseExpression>(new UnaryBooleanFunctionExpression(this->getChild()->clone(renaming, bools, ints), this->functionType)); |
|||
} |
|||
|
|||
FunctionType getFunctionType() const { |
|||
return functionType; |
|||
} |
|||
|
|||
virtual bool 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 << "'."; |
|||
} |
|||
} |
|||
|
|||
virtual void accept(ExpressionVisitor* visitor) { |
|||
visitor->visit(this); |
|||
} |
|||
|
|||
virtual std::string toString() const { |
|||
std::string result = ""; |
|||
switch (functionType) { |
|||
case NOT: result += "!"; break; |
|||
} |
|||
result += "(" + this->getChild()->toString() + ")"; |
|||
|
|||
return result; |
|||
} |
|||
virtual std::string dump(std::string prefix) const { |
|||
std::stringstream result; |
|||
result << prefix << "UnaryBooleanFunctionExpression" << std::endl; |
|||
switch (functionType) { |
|||
case NOT: result << prefix << "!" << std::endl; break; |
|||
} |
|||
result << this->getChild()->dump(prefix + "\t"); |
|||
return result.str(); |
|||
} |
|||
|
|||
private: |
|||
FunctionType functionType; |
|||
}; |
|||
|
|||
} |
|||
|
|||
} |
|||
|
|||
} |
|||
|
|||
#endif /* UNARYBOOLEANFUNCTIONEXPRESSION_H_ */ |
|||
@ -0,0 +1,39 @@ |
|||
/* |
|||
* 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 { |
|||
|
|||
class UnaryExpression : public BaseExpression { |
|||
public: |
|||
UnaryExpression(ReturnType type, std::shared_ptr<BaseExpression> child) : BaseExpression(type), child(child) { |
|||
|
|||
} |
|||
|
|||
std::shared_ptr<BaseExpression> const& getChild() const { |
|||
return child; |
|||
} |
|||
|
|||
private: |
|||
std::shared_ptr<BaseExpression> child; |
|||
}; |
|||
|
|||
} // namespace expressions |
|||
|
|||
} // namespace ir |
|||
|
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_IR_EXPRESSIONS_UNARYEXPRESSION_H_ */ |
|||
@ -0,0 +1,99 @@ |
|||
/* |
|||
* UnaryFunctionExpression.h |
|||
* |
|||
* Created on: 03.01.2013 |
|||
* Author: chris |
|||
*/ |
|||
|
|||
#ifndef UNARYFUNCTIONEXPRESSION_H_ |
|||
#define UNARYFUNCTIONEXPRESSION_H_ |
|||
|
|||
#include "src/ir/expressions/UnaryExpression.h" |
|||
|
|||
namespace storm { |
|||
|
|||
namespace ir { |
|||
|
|||
namespace expressions { |
|||
|
|||
class UnaryNumericalFunctionExpression : public UnaryExpression { |
|||
public: |
|||
enum FunctionType {MINUS}; |
|||
|
|||
UnaryNumericalFunctionExpression(ReturnType type, std::shared_ptr<BaseExpression> child, FunctionType functionType) : UnaryExpression(type, child), functionType(functionType) { |
|||
|
|||
} |
|||
|
|||
virtual ~UnaryNumericalFunctionExpression() { |
|||
|
|||
} |
|||
|
|||
virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) { |
|||
return std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(this->getType(), this->getChild()->clone(renaming, bools, ints), this->functionType)); |
|||
} |
|||
|
|||
virtual int_fast64_t 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; |
|||
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Unknown numerical unary operator: '" << functionType << "'."; |
|||
} |
|||
} |
|||
|
|||
virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
if (this->getType() != double_) { |
|||
BaseExpression::getValueAsDouble(variableValues); |
|||
} |
|||
|
|||
double resultChild = this->getChild()->getValueAsDouble(variableValues); |
|||
switch(functionType) { |
|||
case MINUS: return -resultChild; break; |
|||
default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " |
|||
<< "Unknown numerical unary operator: '" << functionType << "'."; |
|||
} |
|||
} |
|||
|
|||
FunctionType getFunctionType() const { |
|||
return functionType; |
|||
} |
|||
|
|||
virtual void accept(ExpressionVisitor* visitor) { |
|||
visitor->visit(this); |
|||
} |
|||
|
|||
virtual std::string toString() const { |
|||
std::string result = ""; |
|||
switch (functionType) { |
|||
case MINUS: result += "-"; break; |
|||
} |
|||
result += this->getChild()->toString(); |
|||
|
|||
return result; |
|||
} |
|||
|
|||
virtual std::string dump(std::string prefix) const { |
|||
std::stringstream result; |
|||
result << prefix << "UnaryNumericalFunctionExpression" << std::endl; |
|||
switch (functionType) { |
|||
case MINUS: result << prefix << "-" << std::endl; break; |
|||
} |
|||
result << this->getChild()->dump(prefix + "\t"); |
|||
return result.str(); |
|||
} |
|||
|
|||
private: |
|||
FunctionType functionType; |
|||
}; |
|||
|
|||
} |
|||
|
|||
} |
|||
|
|||
} |
|||
|
|||
#endif /* UNARYFUNCTIONEXPRESSION_H_ */ |
|||
@ -0,0 +1,146 @@ |
|||
/* |
|||
* VariableExpression.h |
|||
* |
|||
* Created on: 03.01.2013 |
|||
* Author: chris |
|||
*/ |
|||
|
|||
#ifndef VARIABLEEXPRESSION_H_ |
|||
#define VARIABLEEXPRESSION_H_ |
|||
|
|||
#include "src/ir/expressions/BaseExpression.h" |
|||
|
|||
#include <memory> |
|||
#include <iostream> |
|||
|
|||
#include "log4cplus/logger.h" |
|||
#include "log4cplus/loggingmacros.h" |
|||
extern log4cplus::Logger logger; |
|||
|
|||
namespace storm { |
|||
|
|||
namespace ir { |
|||
|
|||
namespace expressions { |
|||
|
|||
class VariableExpression : public BaseExpression { |
|||
public: |
|||
VariableExpression(ReturnType type, uint_fast64_t index, std::string variableName, |
|||
std::shared_ptr<BaseExpression> lowerBound = std::shared_ptr<storm::ir::expressions::BaseExpression>(nullptr), |
|||
std::shared_ptr<BaseExpression> upperBound = std::shared_ptr<storm::ir::expressions::BaseExpression>(nullptr)) |
|||
: BaseExpression(type), index(index), variableName(variableName), |
|||
lowerBound(lowerBound), upperBound(upperBound) { |
|||
} |
|||
|
|||
virtual ~VariableExpression() { |
|||
} |
|||
|
|||
virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) { |
|||
std::shared_ptr<BaseExpression> lower = this->lowerBound, upper = this->upperBound; |
|||
if (lower != nullptr) lower = lower->clone(renaming, bools, ints); |
|||
if (upper != nullptr) upper = upper->clone(renaming, bools, ints); |
|||
if (renaming.count(this->variableName) > 0) { |
|||
std::string newName = renaming.at(this->variableName); |
|||
if (this->getType() == bool_) { |
|||
return std::shared_ptr<BaseExpression>(new VariableExpression(bool_, bools.at(newName), newName, lower, upper)); |
|||
} else if (this->getType() == int_) { |
|||
return std::shared_ptr<BaseExpression>(new VariableExpression(int_, ints.at(newName), newName, lower, upper)); |
|||
} else { |
|||
LOG4CPLUS_ERROR(logger, "ERROR: Renaming variable " << this->variableName << " that is neither bool nor int."); |
|||
return std::shared_ptr<BaseExpression>(nullptr); |
|||
} |
|||
} else { |
|||
return std::shared_ptr<BaseExpression>(new VariableExpression(this->getType(), this->index, this->variableName, lower, upper)); |
|||
} |
|||
} |
|||
|
|||
|
|||
virtual void accept(ExpressionVisitor* visitor) { |
|||
std::cout << "Visitor!" << std::endl; |
|||
visitor->visit(this); |
|||
} |
|||
|
|||
virtual std::string toString() const { |
|||
return this->variableName; |
|||
} |
|||
|
|||
virtual std::string dump(std::string prefix) const { |
|||
std::stringstream result; |
|||
result << prefix << this->variableName << " " << index << std::endl; |
|||
if (this->lowerBound != nullptr) { |
|||
result << prefix << "lower bound" << std::endl; |
|||
result << this->lowerBound->dump(prefix + "\t"); |
|||
} |
|||
if (this->upperBound != nullptr) { |
|||
result << prefix << "upper bound" << std::endl; |
|||
result << this->upperBound->dump(prefix + "\t"); |
|||
} |
|||
return result.str(); |
|||
} |
|||
|
|||
virtual int_fast64_t 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[index]; |
|||
} else { |
|||
throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression" |
|||
<< " involving variables without variable values."; |
|||
} |
|||
} |
|||
|
|||
virtual bool 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[index]; |
|||
} else { |
|||
throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression" |
|||
<< " involving variables without variable values."; |
|||
} |
|||
} |
|||
|
|||
virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const { |
|||
if (this->getType() != double_) { |
|||
BaseExpression::getValueAsDouble(variableValues); |
|||
} |
|||
|
|||
throw storm::exceptions::NotImplementedException() << "Cannot evaluate expression with " |
|||
<< " variable '" << variableName << "' of type double."; |
|||
} |
|||
|
|||
std::string const& getVariableName() const { |
|||
return variableName; |
|||
} |
|||
|
|||
std::shared_ptr<BaseExpression> const& getLowerBound() const { |
|||
return lowerBound; |
|||
} |
|||
|
|||
std::shared_ptr<BaseExpression> const& getUpperBound() const { |
|||
return upperBound; |
|||
} |
|||
|
|||
uint_fast64_t getVariableIndex() const { |
|||
return this->index; |
|||
} |
|||
|
|||
private: |
|||
uint_fast64_t index; |
|||
std::string variableName; |
|||
|
|||
std::shared_ptr<BaseExpression> lowerBound; |
|||
std::shared_ptr<BaseExpression> upperBound; |
|||
}; |
|||
|
|||
} |
|||
|
|||
} |
|||
|
|||
} |
|||
|
|||
#endif /* VARIABLEEXPRESSION_H_ */ |
|||
@ -0,0 +1,128 @@ |
|||
/*
|
|||
* PrismParser.cpp |
|||
* |
|||
* Created on: 11.01.2013 |
|||
* Author: chris |
|||
*/ |
|||
|
|||
#include "PrismParser.h"
|
|||
|
|||
#include "src/utility/OsDetection.h"
|
|||
|
|||
#include "src/parser/PrismParser/PrismGrammar.h"
|
|||
|
|||
// If the parser fails due to ill-formed data, this exception is thrown.
|
|||
#include "src/exceptions/WrongFileFormatException.h"
|
|||
|
|||
// Needed for file IO.
|
|||
#include <fstream>
|
|||
#include <iomanip>
|
|||
#include <limits>
|
|||
|
|||
#include "log4cplus/logger.h"
|
|||
#include "log4cplus/loggingmacros.h"
|
|||
extern log4cplus::Logger logger; |
|||
|
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
|
|||
/*!
|
|||
* Opens the given file for parsing, invokes the helper function to parse the actual content and |
|||
* closes the file properly, even if an exception is thrown in the parser. In this case, the |
|||
* exception is passed on to the caller. |
|||
*/ |
|||
storm::ir::Program PrismParser::parseFile(std::string const& filename) const { |
|||
// Open file and initialize result.
|
|||
std::ifstream inputFileStream(filename, std::ios::in); |
|||
storm::ir::Program result; |
|||
|
|||
// Now try to parse the contents of the file.
|
|||
try { |
|||
result = parse(inputFileStream, filename); |
|||
} catch(std::exception& e) { |
|||
// In case of an exception properly close the file before passing exception.
|
|||
inputFileStream.close(); |
|||
throw e; |
|||
} |
|||
|
|||
// Close the stream in case everything went smoothly and return result.
|
|||
inputFileStream.close(); |
|||
return result; |
|||
} |
|||
|
|||
/*!
|
|||
* Passes iterators to the input stream to the Boost spirit parser and thereby parses the input. |
|||
* If the parser throws an expectation failure exception, i.e. expected input different than the one |
|||
* provided, this is caught and displayed properly before the exception is passed on. |
|||
*/ |
|||
storm::ir::Program PrismParser::parse(std::istream& inputStream, std::string const& filename) const { |
|||
// Prepare iterators to input.
|
|||
// TODO: Right now, this parses the whole contents of the file into a string first.
|
|||
// While this is usually not necessary, because there exist adapters that make an input stream
|
|||
// iterable in both directions without storing it into a string, using the corresponding
|
|||
// Boost classes gives an awful output under valgrind and is thus disabled for the time being.
|
|||
std::string fileContent((std::istreambuf_iterator<char>(inputStream)), (std::istreambuf_iterator<char>())); |
|||
BaseIteratorType stringIteratorBegin = fileContent.begin(); |
|||
BaseIteratorType stringIteratorEnd = fileContent.end(); |
|||
PositionIteratorType positionIteratorBegin(stringIteratorBegin, stringIteratorEnd, filename); |
|||
PositionIteratorType positionIteratorBegin2(stringIteratorBegin, stringIteratorEnd, filename); |
|||
PositionIteratorType positionIteratorEnd; |
|||
|
|||
// Prepare resulting intermediate representation of input.
|
|||
storm::ir::Program result; |
|||
|
|||
// In order to instantiate the grammar, we have to pass the type of the skipping parser.
|
|||
// As this is more complex, we let Boost figure out the actual type for us.
|
|||
prism::PrismGrammar grammar; |
|||
try { |
|||
// Now parse the content using phrase_parse in order to be able to supply a skipping parser.
|
|||
// First run.
|
|||
LOG4CPLUS_INFO(logger, "Start parsing..."); |
|||
qi::phrase_parse(positionIteratorBegin, positionIteratorEnd, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result); |
|||
grammar.prepareForSecondRun(); |
|||
result = storm::ir::Program(); |
|||
LOG4CPLUS_INFO(logger, "Start second parsing run..."); |
|||
// Second run.
|
|||
qi::phrase_parse(positionIteratorBegin2, positionIteratorEnd, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result); |
|||
LOG4CPLUS_INFO(logger, "Finished parsing, here is the parsed program:" << std::endl << result.toString()); |
|||
// Reset grammars.
|
|||
grammar.resetGrammars(); |
|||
} catch(const qi::expectation_failure<PositionIteratorType>& e) { |
|||
// If the parser expected content different than the one provided, display information
|
|||
// about the location of the error.
|
|||
const boost::spirit::classic::file_position_base<std::string>& pos = e.first.get_position(); |
|||
|
|||
// Construct the error message including a caret display of the position in the
|
|||
// erroneous line.
|
|||
std::stringstream msg; |
|||
std::string line = e.first.get_currentline(); |
|||
while (line.find('\t') != std::string::npos) line.replace(line.find('\t'),1," "); |
|||
msg << pos.file << ", line " << pos.line << ", column " << pos.column |
|||
<< ": parse error: expected " << e.what_ << std::endl << "\t" |
|||
<< line << std::endl << "\t"; |
|||
int i = 0; |
|||
for (i = 1; i < pos.column; ++i) { |
|||
msg << "-"; |
|||
} |
|||
msg << "^"; |
|||
for (; i < 80; ++i) { |
|||
msg << "-"; |
|||
} |
|||
msg << std::endl; |
|||
|
|||
std::cerr << msg.str(); |
|||
|
|||
// Reset grammars in any case.
|
|||
grammar.resetGrammars(); |
|||
|
|||
// Now propagate exception.
|
|||
throw storm::exceptions::WrongFileFormatException() << msg.str(); |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
} // namespace parser
|
|||
|
|||
} // namespace storm
|
|||
@ -0,0 +1,52 @@ |
|||
/* * PrismParser.h |
|||
* |
|||
* Created on: Jan 3, 2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_PARSER_PRISMPARSER_H_ |
|||
#define STORM_PARSER_PRISMPARSER_H_ |
|||
|
|||
// All classes of the intermediate representation are used. |
|||
#include "src/ir/IR.h" |
|||
|
|||
// Used for file input. |
|||
#include <istream> |
|||
#include <memory> |
|||
|
|||
namespace storm { |
|||
|
|||
namespace parser { |
|||
|
|||
using namespace storm::ir; |
|||
using namespace storm::ir::expressions; |
|||
|
|||
/*! |
|||
* This class parses the format of the PRISM model checker into an intermediate representation. |
|||
*/ |
|||
class PrismParser { |
|||
public: |
|||
/*! |
|||
* Parses the given file into the intermediate representation assuming it complies with the |
|||
* PRISM syntax. |
|||
* @param filename the name of the file to parse. |
|||
* @return a shared pointer to the intermediate representation of the PRISM file. |
|||
*/ |
|||
storm::ir::Program parseFile(std::string const& filename) const; |
|||
|
|||
private: |
|||
/*! |
|||
* Parses the given input stream into the intermediate representation assuming it complies with |
|||
* the PRISM syntax. |
|||
* @param inputStream the input stream to parse. |
|||
* @param filename the name of the file the input stream belongs to. Used for diagnostics. |
|||
* @return a shared pointer to the intermediate representation of the PRISM file. |
|||
*/ |
|||
storm::ir::Program parse(std::istream& inputStream, std::string const& filename) const; |
|||
}; |
|||
|
|||
} // namespace parser |
|||
|
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_PARSER_PRISMPARSER_H_ */ |
|||
@ -0,0 +1,112 @@ |
|||
/* |
|||
* File: Keywords.h |
|||
* Author: nafur |
|||
* |
|||
* Created on April 10, 2013, 6:03 PM |
|||
*/ |
|||
|
|||
#ifndef BASEGRAMMAR_H |
|||
#define BASEGRAMMAR_H |
|||
|
|||
#include "Includes.h" |
|||
|
|||
#include "VariableState.h" |
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
namespace prism { |
|||
|
|||
template <typename T> |
|||
class BaseGrammar { |
|||
public: |
|||
BaseGrammar(std::shared_ptr<VariableState>& state) : state(state) {} |
|||
|
|||
static T& instance(std::shared_ptr<VariableState> state = nullptr) { |
|||
if (BaseGrammar::instanceObject == nullptr) { |
|||
BaseGrammar::instanceObject = std::shared_ptr<T>(new T(state)); |
|||
if (!state->firstRun) BaseGrammar::instanceObject->secondRun(); |
|||
} |
|||
return *BaseGrammar::instanceObject; |
|||
} |
|||
|
|||
static void resetInstance() { |
|||
BaseGrammar::instanceObject = nullptr; |
|||
} |
|||
|
|||
static void secondRun() { |
|||
if (BaseGrammar::instanceObject != nullptr) { |
|||
BaseGrammar::instanceObject->prepareSecondRun(); |
|||
} |
|||
} |
|||
|
|||
std::shared_ptr<BaseExpression> createBoolLiteral(const bool value) { |
|||
return std::shared_ptr<BooleanLiteral>(new BooleanLiteral(value)); |
|||
} |
|||
std::shared_ptr<BaseExpression> createDoubleLiteral(const double value) { |
|||
return std::shared_ptr<DoubleLiteral>(new DoubleLiteral(value)); |
|||
} |
|||
std::shared_ptr<BaseExpression> createIntLiteral(const int_fast64_t value) { |
|||
return std::shared_ptr<IntegerLiteral>(new IntegerLiteral(value)); |
|||
} |
|||
|
|||
std::shared_ptr<BaseExpression> createPlus(const std::shared_ptr<BaseExpression> left, bool addition, const std::shared_ptr<BaseExpression> right, BaseExpression::ReturnType type) { |
|||
if (addition) { |
|||
return std::shared_ptr<BinaryNumericalFunctionExpression>(new BinaryNumericalFunctionExpression(type, left, right, BinaryNumericalFunctionExpression::PLUS)); |
|||
} else { |
|||
return std::shared_ptr<BinaryNumericalFunctionExpression>(new BinaryNumericalFunctionExpression(type, left, right, BinaryNumericalFunctionExpression::MINUS)); |
|||
} |
|||
} |
|||
std::shared_ptr<BaseExpression> createDoublePlus(const std::shared_ptr<BaseExpression> left, bool addition, const std::shared_ptr<BaseExpression> right) { |
|||
return this->createPlus(left, addition, right, BaseExpression::double_); |
|||
} |
|||
std::shared_ptr<BaseExpression> createIntPlus(const std::shared_ptr<BaseExpression> left, bool addition, const std::shared_ptr<BaseExpression> right) { |
|||
return this->createPlus(left, addition, right, BaseExpression::int_); |
|||
} |
|||
|
|||
std::shared_ptr<BaseExpression> createIntMult(const std::shared_ptr<BaseExpression> left, const std::shared_ptr<BaseExpression> right) { |
|||
return std::shared_ptr<BinaryNumericalFunctionExpression>(new BinaryNumericalFunctionExpression(BaseExpression::int_, left, right, BinaryNumericalFunctionExpression::TIMES)); |
|||
} |
|||
std::shared_ptr<BaseExpression> createDoubleMult(const std::shared_ptr<BaseExpression> left, bool multiplication, const std::shared_ptr<BaseExpression> right) { |
|||
if (multiplication) { |
|||
return std::shared_ptr<BinaryNumericalFunctionExpression>(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::TIMES)); |
|||
} else { |
|||
return std::shared_ptr<BinaryNumericalFunctionExpression>(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::DIVIDE)); |
|||
} |
|||
} |
|||
|
|||
std::shared_ptr<BaseExpression> createRelation(std::shared_ptr<BaseExpression> left, BinaryRelationExpression::RelationType relationType, std::shared_ptr<BaseExpression> right) { |
|||
return std::shared_ptr<BinaryRelationExpression>(new BinaryRelationExpression(left, right, relationType)); |
|||
} |
|||
std::shared_ptr<BaseExpression> createNot(std::shared_ptr<BaseExpression> child) { |
|||
return std::shared_ptr<UnaryBooleanFunctionExpression>(new UnaryBooleanFunctionExpression(child, UnaryBooleanFunctionExpression::NOT)); |
|||
} |
|||
std::shared_ptr<BaseExpression> createAnd(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right) { |
|||
//std::cerr << "Creating " << left->toString() << " & " << right->toString() << std::endl; |
|||
return std::shared_ptr<BinaryBooleanFunctionExpression>(new BinaryBooleanFunctionExpression(left, right, BinaryBooleanFunctionExpression::AND)); |
|||
} |
|||
std::shared_ptr<BaseExpression> createOr(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right) { |
|||
return std::shared_ptr<BinaryBooleanFunctionExpression>(new BinaryBooleanFunctionExpression(left, right, BinaryBooleanFunctionExpression::OR)); |
|||
} |
|||
std::shared_ptr<BaseExpression> getBoolVariable(const std::string name) { |
|||
return state->getBooleanVariable(name); |
|||
} |
|||
std::shared_ptr<BaseExpression> getIntVariable(const std::string name) { |
|||
return state->getIntegerVariable(name); |
|||
} |
|||
|
|||
virtual void prepareSecondRun() {} |
|||
protected: |
|||
std::shared_ptr<VariableState> state; |
|||
|
|||
private: |
|||
static std::shared_ptr<T> instanceObject; |
|||
static bool inSecondRun; |
|||
}; |
|||
|
|||
template <typename T> |
|||
std::shared_ptr<T> BaseGrammar<T>::instanceObject; |
|||
} |
|||
} |
|||
} |
|||
#endif /* BASEGRAMMAR_H */ |
|||
|
|||
@ -0,0 +1,42 @@ |
|||
#include "BooleanExpressionGrammar.h"
|
|||
|
|||
#include "IntegerExpressionGrammar.h"
|
|||
#include "ConstBooleanExpressionGrammar.h"
|
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
namespace prism { |
|||
|
|||
BooleanExpressionGrammar::BooleanExpressionGrammar(std::shared_ptr<VariableState>& state) |
|||
: BooleanExpressionGrammar::base_type(booleanExpression), BaseGrammar(state) { |
|||
|
|||
booleanExpression %= orExpression; |
|||
booleanExpression.name("boolean expression"); |
|||
|
|||
orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = phoenix::bind(&BaseGrammar::createOr, this, qi::_val, qi::_1)]; |
|||
orExpression.name("boolean expression"); |
|||
|
|||
andExpression = notExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> notExpression)[qi::_val = phoenix::bind(&BaseGrammar::createAnd, this, qi::_val, qi::_1)]; |
|||
andExpression.name("boolean expression"); |
|||
|
|||
notExpression = atomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicBooleanExpression)[qi::_val = phoenix::bind(&BaseGrammar::createNot, this, qi::_1)]; |
|||
notExpression.name("boolean expression"); |
|||
|
|||
atomicBooleanExpression %= (relativeExpression | booleanVariableExpression | qi::lit("(") >> booleanExpression >> qi::lit(")") | ConstBooleanExpressionGrammar::instance(this->state)); |
|||
atomicBooleanExpression.name("boolean expression"); |
|||
|
|||
relativeExpression = (IntegerExpressionGrammar::instance(this->state) >> relations_ >> IntegerExpressionGrammar::instance(this->state))[qi::_val = phoenix::bind(&BaseGrammar::createRelation, this, qi::_1, qi::_2, qi::_3)]; |
|||
relativeExpression.name("relative expression"); |
|||
|
|||
booleanVariableExpression = IdentifierGrammar::instance(this->state)[qi::_val = phoenix::bind(&BaseGrammar::getBoolVariable, this, qi::_1)]; |
|||
booleanVariableExpression.name("boolean variable"); |
|||
} |
|||
|
|||
void BooleanExpressionGrammar::prepareSecondRun() { |
|||
booleanVariableExpression %= this->state->booleanVariables_; |
|||
booleanVariableExpression.name("boolean variable"); |
|||
} |
|||
|
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,44 @@ |
|||
/* |
|||
* File: BooleanExpressionGrammar.h |
|||
* Author: nafur |
|||
* |
|||
* Created on April 10, 2013, 6:27 PM |
|||
*/ |
|||
|
|||
#ifndef BOOLEANEXPRESSIONGRAMMAR_H |
|||
#define BOOLEANEXPRESSIONGRAMMAR_H |
|||
|
|||
#include "Includes.h" |
|||
#include "VariableState.h" |
|||
#include "IdentifierGrammars.h" |
|||
#include "Tokens.h" |
|||
|
|||
#include <iostream> |
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
namespace prism { |
|||
|
|||
class BooleanExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused>, public BaseGrammar<BooleanExpressionGrammar> { |
|||
public: |
|||
BooleanExpressionGrammar(std::shared_ptr<VariableState>& state); |
|||
virtual void prepareSecondRun(); |
|||
|
|||
private: |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused> booleanExpression; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> orExpression; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> andExpression; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> notExpression; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> atomicBooleanExpression; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> relativeExpression; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> booleanVariableExpression; |
|||
|
|||
storm::parser::prism::relationalOperatorStruct relations_; |
|||
}; |
|||
|
|||
|
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* BOOLEANEXPRESSIONGRAMMAR_H */ |
|||
@ -0,0 +1,54 @@ |
|||
#include "ConstBooleanExpressionGrammar.h"
|
|||
|
|||
#include "ConstIntegerExpressionGrammar.h"
|
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
namespace prism { |
|||
|
|||
std::shared_ptr<BaseExpression> ConstBooleanExpressionGrammar::createRelation(std::shared_ptr<BaseExpression> left, BinaryRelationExpression::RelationType relationType, std::shared_ptr<BaseExpression> right) { |
|||
return std::shared_ptr<BinaryRelationExpression>(new BinaryRelationExpression(left, right, relationType)); |
|||
} |
|||
std::shared_ptr<BaseExpression> ConstBooleanExpressionGrammar::createNot(std::shared_ptr<BaseExpression> child) { |
|||
return std::shared_ptr<UnaryBooleanFunctionExpression>(new UnaryBooleanFunctionExpression(child, UnaryBooleanFunctionExpression::NOT)); |
|||
} |
|||
std::shared_ptr<BaseExpression> ConstBooleanExpressionGrammar::createAnd(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right) { |
|||
return std::shared_ptr<BinaryBooleanFunctionExpression>(new BinaryBooleanFunctionExpression(left, right, BinaryBooleanFunctionExpression::AND)); |
|||
} |
|||
std::shared_ptr<BaseExpression> ConstBooleanExpressionGrammar::createOr(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right) { |
|||
return std::shared_ptr<BinaryBooleanFunctionExpression>(new BinaryBooleanFunctionExpression(left, right, BinaryBooleanFunctionExpression::OR)); |
|||
} |
|||
std::shared_ptr<BaseExpression> ConstBooleanExpressionGrammar::createLiteral(const bool value) { |
|||
return std::shared_ptr<BooleanLiteral>(new BooleanLiteral(value)); |
|||
} |
|||
|
|||
ConstBooleanExpressionGrammar::ConstBooleanExpressionGrammar(std::shared_ptr<VariableState>& state) |
|||
: ConstBooleanExpressionGrammar::base_type(constantBooleanExpression), BaseGrammar(state) { |
|||
|
|||
constantBooleanExpression %= constantOrExpression; |
|||
constantBooleanExpression.name("constant boolean expression"); |
|||
|
|||
constantOrExpression = constantAndExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> constantAndExpression)[qi::_val = phoenix::bind(&ConstBooleanExpressionGrammar::createOr, this, qi::_val, qi::_1)]; |
|||
constantOrExpression.name("constant boolean expression"); |
|||
|
|||
constantAndExpression = constantNotExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> constantNotExpression)[qi::_val = phoenix::bind(&ConstBooleanExpressionGrammar::createAnd, this, qi::_val, qi::_1)]; |
|||
constantAndExpression.name("constant boolean expression"); |
|||
|
|||
constantNotExpression = constantAtomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> constantAtomicBooleanExpression)[qi::_val = phoenix::bind(&ConstBooleanExpressionGrammar::createNot, this, qi::_1)]; |
|||
constantNotExpression.name("constant boolean expression"); |
|||
|
|||
constantAtomicBooleanExpression %= (constantRelativeExpression | qi::lit("(") >> constantBooleanExpression >> qi::lit(")") | booleanLiteralExpression | booleanConstantExpression); |
|||
constantAtomicBooleanExpression.name("constant boolean expression"); |
|||
|
|||
constantRelativeExpression = (ConstIntegerExpressionGrammar::instance(this->state) >> relations_ >> ConstIntegerExpressionGrammar::instance(this->state))[qi::_val = phoenix::bind(&ConstBooleanExpressionGrammar::createRelation, this, qi::_1, qi::_2, qi::_3)]; |
|||
constantRelativeExpression.name("constant boolean expression"); |
|||
|
|||
booleanConstantExpression %= (this->state->booleanConstants_ | booleanLiteralExpression); |
|||
booleanConstantExpression.name("boolean constant or literal"); |
|||
|
|||
booleanLiteralExpression = qi::bool_[qi::_val = phoenix::bind(&ConstBooleanExpressionGrammar::createLiteral, this, qi::_1)]; |
|||
booleanLiteralExpression.name("boolean literal"); |
|||
} |
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,50 @@ |
|||
/* |
|||
* File: ConstBooleanExpressionGrammar.h |
|||
* Author: nafur |
|||
* |
|||
* Created on April 10, 2013, 6:34 PM |
|||
*/ |
|||
|
|||
#ifndef CONSTBOOLEANEXPRESSIONGRAMMAR_H |
|||
#define CONSTBOOLEANEXPRESSIONGRAMMAR_H |
|||
|
|||
#include "Includes.h" |
|||
#include "VariableState.h" |
|||
#include "IdentifierGrammars.h" |
|||
#include "Tokens.h" |
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
namespace prism { |
|||
|
|||
class ConstBooleanExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused>, public BaseGrammar<ConstBooleanExpressionGrammar> { |
|||
public: |
|||
ConstBooleanExpressionGrammar(std::shared_ptr<VariableState>& state); |
|||
|
|||
|
|||
private: |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused> constantBooleanExpression; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantOrExpression; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantAndExpression; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantNotExpression; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantAtomicBooleanExpression; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantRelativeExpression; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> booleanConstantExpression; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> booleanLiteralExpression; |
|||
|
|||
storm::parser::prism::relationalOperatorStruct relations_; |
|||
|
|||
std::shared_ptr<BaseExpression> createRelation(std::shared_ptr<BaseExpression> left, BinaryRelationExpression::RelationType relationType, std::shared_ptr<BaseExpression> right); |
|||
std::shared_ptr<BaseExpression> createNot(std::shared_ptr<BaseExpression> child); |
|||
std::shared_ptr<BaseExpression> createAnd(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right); |
|||
std::shared_ptr<BaseExpression> createOr(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right); |
|||
std::shared_ptr<BaseExpression> createLiteral(const bool value); |
|||
}; |
|||
|
|||
|
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* CONSTBOOLEANEXPRESSIONGRAMMAR_H */ |
|||
|
|||
@ -0,0 +1,53 @@ |
|||
#include "ConstDoubleExpressionGrammar.h"
|
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
namespace prism { |
|||
|
|||
|
|||
std::shared_ptr<BaseExpression> ConstDoubleExpressionGrammar::createLiteral(double value) { |
|||
return std::shared_ptr<DoubleLiteral>(new DoubleLiteral(value)); |
|||
} |
|||
std::shared_ptr<BaseExpression> ConstDoubleExpressionGrammar::createPlus(const std::shared_ptr<BaseExpression> left, bool addition, const std::shared_ptr<BaseExpression> right) { |
|||
if (addition) { |
|||
return std::shared_ptr<BinaryNumericalFunctionExpression>(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::PLUS)); |
|||
} else { |
|||
return std::shared_ptr<BinaryNumericalFunctionExpression>(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::MINUS)); |
|||
} |
|||
} |
|||
std::shared_ptr<BaseExpression> ConstDoubleExpressionGrammar::createMult(const std::shared_ptr<BaseExpression> left, bool multiplication, const std::shared_ptr<BaseExpression> right) { |
|||
if (multiplication) { |
|||
return std::shared_ptr<BinaryNumericalFunctionExpression>(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::TIMES)); |
|||
} else { |
|||
return std::shared_ptr<BinaryNumericalFunctionExpression>(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::DIVIDE)); |
|||
} |
|||
} |
|||
|
|||
ConstDoubleExpressionGrammar::ConstDoubleExpressionGrammar(std::shared_ptr<VariableState>& state) |
|||
: ConstDoubleExpressionGrammar::base_type(constantDoubleExpression), BaseGrammar(state) { |
|||
|
|||
constantDoubleExpression %= constantDoublePlusExpression; |
|||
constantDoubleExpression.name("constant double expression"); |
|||
|
|||
constantDoublePlusExpression %= constantDoubleMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> constantDoubleMultExpression) |
|||
[qi::_val = phoenix::bind(&ConstDoubleExpressionGrammar::createPlus, this, qi::_val, qi::_a, qi::_1)]; |
|||
constantDoublePlusExpression.name("constant double expression"); |
|||
|
|||
constantDoubleMultExpression %= constantAtomicDoubleExpression[qi::_val = qi::_1] >> *((qi::lit("*")[qi::_a = true] | qi::lit("/")[qi::_a = false]) >> constantAtomicDoubleExpression) |
|||
[qi::_val = phoenix::bind(&ConstDoubleExpressionGrammar::createMult, this, qi::_val, qi::_a, qi::_1)]; |
|||
constantDoubleMultExpression.name("constant double expression"); |
|||
|
|||
constantAtomicDoubleExpression %= (qi::lit("(") >> constantDoubleExpression >> qi::lit(")") | doubleConstantExpression); |
|||
constantAtomicDoubleExpression.name("constant double expression"); |
|||
|
|||
doubleConstantExpression %= (this->state->doubleConstants_ | this->state->integerConstants_ | doubleLiteralExpression); |
|||
doubleConstantExpression.name("double constant or literal"); |
|||
|
|||
doubleLiteralExpression = qi::double_[qi::_val = phoenix::bind(&ConstDoubleExpressionGrammar::createLiteral, this, qi::_1)]; |
|||
doubleLiteralExpression.name("double literal"); |
|||
} |
|||
|
|||
|
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,43 @@ |
|||
/* |
|||
* File: ConstDoubleExpressionGrammar.h |
|||
* Author: nafur |
|||
* |
|||
* Created on April 10, 2013, 7:04 PM |
|||
*/ |
|||
|
|||
#ifndef CONSTDOUBLEEXPRESSIONGRAMMAR_H |
|||
#define CONSTDOUBLEEXPRESSIONGRAMMAR_H |
|||
|
|||
#include "Includes.h" |
|||
#include "VariableState.h" |
|||
#include "IdentifierGrammars.h" |
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
namespace prism { |
|||
|
|||
class ConstDoubleExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused>, public BaseGrammar<ConstDoubleExpressionGrammar> { |
|||
public: |
|||
ConstDoubleExpressionGrammar(std::shared_ptr<VariableState>& state); |
|||
|
|||
|
|||
private: |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused> constantDoubleExpression; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> constantDoublePlusExpression; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> constantDoubleMultExpression; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantAtomicDoubleExpression; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> doubleConstantExpression; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> doubleLiteralExpression; |
|||
|
|||
std::shared_ptr<BaseExpression> createLiteral(double value); |
|||
std::shared_ptr<BaseExpression> createPlus(const std::shared_ptr<BaseExpression> left, bool addition, const std::shared_ptr<BaseExpression> right); |
|||
std::shared_ptr<BaseExpression> createMult(const std::shared_ptr<BaseExpression> left, bool multiplication, const std::shared_ptr<BaseExpression> right); |
|||
}; |
|||
|
|||
|
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* CONSTDOUBLEEXPRESSIONGRAMMAR_H */ |
|||
|
|||
@ -0,0 +1,35 @@ |
|||
#include "ConstIntegerExpressionGrammar.h"
|
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
namespace prism { |
|||
|
|||
|
|||
ConstIntegerExpressionGrammar::ConstIntegerExpressionGrammar(std::shared_ptr<VariableState>& state) |
|||
: ConstIntegerExpressionGrammar::base_type(constantIntegerExpression), BaseGrammar(state) { |
|||
|
|||
constantIntegerExpression %= constantIntegerPlusExpression; |
|||
constantIntegerExpression.name("constant integer expression"); |
|||
|
|||
constantIntegerPlusExpression = constantIntegerMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> constantIntegerMultExpression) |
|||
[qi::_val = phoenix::bind(&BaseGrammar::createIntPlus, this, qi::_val, qi::_a, qi::_1)]; |
|||
constantIntegerPlusExpression.name("constant integer expression"); |
|||
|
|||
constantIntegerMultExpression %= constantAtomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicIntegerExpression) |
|||
[qi::_val = phoenix::bind(&BaseGrammar::createIntMult, this, qi::_val, qi::_1)]; |
|||
constantIntegerMultExpression.name("constant integer expression"); |
|||
|
|||
constantAtomicIntegerExpression %= (qi::lit("(") >> constantIntegerExpression >> qi::lit(")") | integerConstantExpression); |
|||
constantAtomicIntegerExpression.name("constant integer expression"); |
|||
|
|||
integerConstantExpression %= (this->state->integerConstants_ | integerLiteralExpression); |
|||
integerConstantExpression.name("integer constant or literal"); |
|||
|
|||
integerLiteralExpression = qi::int_[qi::_val = phoenix::bind(&BaseGrammar::createIntLiteral, this, qi::_1)]; |
|||
integerLiteralExpression.name("integer literal"); |
|||
|
|||
} |
|||
|
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,37 @@ |
|||
/* |
|||
* File: ConstIntegerExpressionGrammar.h |
|||
* Author: nafur |
|||
* |
|||
* Created on April 10, 2013, 6:02 PM |
|||
*/ |
|||
|
|||
#ifndef CONSTINTEGEREXPRESSIONGRAMMAR_H |
|||
#define CONSTINTEGEREXPRESSIONGRAMMAR_H |
|||
|
|||
#include "Includes.h" |
|||
#include "VariableState.h" |
|||
#include "IdentifierGrammars.h" |
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
namespace prism { |
|||
|
|||
class ConstIntegerExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused>, public BaseGrammar<ConstIntegerExpressionGrammar> { |
|||
public: |
|||
ConstIntegerExpressionGrammar(std::shared_ptr<VariableState>& state); |
|||
|
|||
private: |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused> constantIntegerExpression; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> constantIntegerPlusExpression; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantIntegerMultExpression; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantAtomicIntegerExpression; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerConstantExpression; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerLiteralExpression; |
|||
}; |
|||
|
|||
|
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* CONSTINTEGEREXPRESSIONGRAMMAR_H */ |
|||
@ -0,0 +1,23 @@ |
|||
#include "IdentifierGrammars.h"
|
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
namespace prism { |
|||
|
|||
IdentifierGrammar::IdentifierGrammar(std::shared_ptr<VariableState>& state) |
|||
: IdentifierGrammar::base_type(identifierName), BaseGrammar(state) { |
|||
|
|||
identifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&VariableState::isIdentifier, this->state.get(), qi::_1) ]; |
|||
identifierName.name("identifier"); |
|||
} |
|||
|
|||
FreeIdentifierGrammar::FreeIdentifierGrammar(std::shared_ptr<VariableState>& state) |
|||
: FreeIdentifierGrammar::base_type(freeIdentifierName), BaseGrammar(state) { |
|||
|
|||
freeIdentifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&VariableState::isFreeIdentifier, this->state.get(), qi::_1) ]; |
|||
freeIdentifierName.name("identifier"); |
|||
} |
|||
|
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,36 @@ |
|||
/* |
|||
* File: Keywords.h |
|||
* Author: nafur |
|||
* |
|||
* Created on April 10, 2013, 6:03 PM |
|||
*/ |
|||
|
|||
#ifndef IDENTIFIERGRAMMARS_H |
|||
#define IDENTIFIERGRAMMARS_H |
|||
|
|||
#include "Includes.h" |
|||
#include "BaseGrammar.h" |
|||
#include "VariableState.h" |
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
namespace prism { |
|||
|
|||
class IdentifierGrammar : public qi::grammar<Iterator, std::string(), Skipper, Unused>, public BaseGrammar<IdentifierGrammar> { |
|||
public: |
|||
IdentifierGrammar(std::shared_ptr<VariableState>& state); |
|||
private: |
|||
qi::rule<Iterator, std::string(), Skipper> identifierName; |
|||
}; |
|||
|
|||
class FreeIdentifierGrammar : public qi::grammar<Iterator, std::string(), Skipper, Unused>, public BaseGrammar<IdentifierGrammar> { |
|||
public: |
|||
FreeIdentifierGrammar(std::shared_ptr<VariableState>& state); |
|||
private: |
|||
qi::rule<Iterator, std::string(), Skipper> freeIdentifierName; |
|||
}; |
|||
} |
|||
} |
|||
} |
|||
#endif /* IDENTIFIERGRAMMARS_H */ |
|||
|
|||
@ -0,0 +1,41 @@ |
|||
/* |
|||
* File: BoostIncludes.h |
|||
* Author: nafur |
|||
* |
|||
* Created on April 10, 2013, 4:46 PM |
|||
*/ |
|||
|
|||
#ifndef BOOSTINCLUDES_H |
|||
#define BOOSTINCLUDES_H |
|||
|
|||
#define DEBUGPRISM |
|||
|
|||
// Used for Boost spirit. |
|||
#include <boost/typeof/typeof.hpp> |
|||
#include <boost/spirit/include/qi.hpp> |
|||
#include <boost/spirit/include/phoenix.hpp> |
|||
|
|||
// Include headers for spirit iterators. Needed for diagnostics and input stream iteration. |
|||
#include <boost/spirit/include/classic_position_iterator.hpp> |
|||
#include <boost/spirit/include/support_multi_pass.hpp> |
|||
|
|||
namespace qi = boost::spirit::qi; |
|||
namespace phoenix = boost::phoenix; |
|||
|
|||
typedef std::string::const_iterator BaseIteratorType; |
|||
typedef boost::spirit::classic::position_iterator2<BaseIteratorType> PositionIteratorType; |
|||
typedef PositionIteratorType Iterator; |
|||
typedef BOOST_TYPEOF(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol) Skipper; |
|||
typedef BOOST_TYPEOF(qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol | boost::spirit::ascii::space) Skipper2; |
|||
typedef boost::spirit::unused_type Unused; |
|||
|
|||
#include "src/ir/IR.h" |
|||
using namespace storm::ir; |
|||
using namespace storm::ir::expressions; |
|||
|
|||
#include "log4cplus/logger.h" |
|||
#include "log4cplus/loggingmacros.h" |
|||
extern log4cplus::Logger logger; |
|||
|
|||
#endif /* BOOSTINCLUDES_H */ |
|||
|
|||
@ -0,0 +1,36 @@ |
|||
#include "IntegerExpressionGrammar.h"
|
|||
|
|||
#include "IdentifierGrammars.h"
|
|||
#include "ConstIntegerExpressionGrammar.h"
|
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
namespace prism { |
|||
|
|||
IntegerExpressionGrammar::IntegerExpressionGrammar(std::shared_ptr<VariableState>& state) |
|||
: IntegerExpressionGrammar::base_type(integerExpression), BaseGrammar(state) { |
|||
|
|||
integerExpression %= integerPlusExpression; |
|||
integerExpression.name("integer expression"); |
|||
|
|||
integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> integerMultExpression)[qi::_val = phoenix::bind(&BaseGrammar::createIntPlus, this, qi::_val, qi::_a, qi::_1)]; |
|||
integerPlusExpression.name("integer expression"); |
|||
|
|||
integerMultExpression %= atomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicIntegerExpression[qi::_val = phoenix::bind(&BaseGrammar::createIntMult, this, qi::_val, qi::_1)]); |
|||
integerMultExpression.name("integer expression"); |
|||
|
|||
atomicIntegerExpression %= (integerVariableExpression | qi::lit("(") >> integerExpression >> qi::lit(")") | ConstIntegerExpressionGrammar::instance(this->state)); |
|||
atomicIntegerExpression.name("integer expression"); |
|||
|
|||
integerVariableExpression = IdentifierGrammar::instance(this->state)[qi::_val = phoenix::bind(&BaseGrammar::getIntVariable, this, qi::_1)]; |
|||
integerVariableExpression.name("integer variable"); |
|||
} |
|||
|
|||
void IntegerExpressionGrammar::prepareSecondRun() { |
|||
integerVariableExpression %= this->state->integerVariables_; |
|||
integerVariableExpression.name("integer variable"); |
|||
} |
|||
|
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,40 @@ |
|||
/* |
|||
* File: IntegerExpressionGrammar.h |
|||
* Author: nafur |
|||
* |
|||
* Created on April 10, 2013, 4:39 PM |
|||
*/ |
|||
|
|||
#ifndef INTEGEREXPRESSIONGRAMMAR_H |
|||
#define INTEGEREXPRESSIONGRAMMAR_H |
|||
|
|||
#include "src/ir/IR.h" |
|||
#include "VariableState.h" |
|||
#include "Includes.h" |
|||
#include "IdentifierGrammars.h" |
|||
|
|||
#include <memory> |
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
namespace prism { |
|||
|
|||
class IntegerExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused>, public BaseGrammar<IntegerExpressionGrammar> { |
|||
public: |
|||
IntegerExpressionGrammar(std::shared_ptr<VariableState>& state); |
|||
virtual void prepareSecondRun(); |
|||
|
|||
private: |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused> integerExpression; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> integerPlusExpression; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerMultExpression; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> atomicIntegerExpression; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerVariableExpression; |
|||
}; |
|||
|
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* INTEGEREXPRESSIONGRAMMAR_H */ |
|||
|
|||
@ -0,0 +1,258 @@ |
|||
/*
|
|||
* PrismGrammar.cpp |
|||
* |
|||
* Created on: 11.01.2013 |
|||
* Author: chris |
|||
*/ |
|||
|
|||
#include "PrismGrammar.h"
|
|||
|
|||
#include "src/utility/OsDetection.h"
|
|||
|
|||
#include "src/parser/PrismParser/Includes.h"
|
|||
#include "src/parser/PrismParser/BooleanExpressionGrammar.h"
|
|||
#include "src/parser/PrismParser/ConstBooleanExpressionGrammar.h"
|
|||
#include "src/parser/PrismParser/ConstDoubleExpressionGrammar.h"
|
|||
#include "src/parser/PrismParser/ConstIntegerExpressionGrammar.h"
|
|||
#include "src/parser/PrismParser/IntegerExpressionGrammar.h"
|
|||
#include "src/parser/PrismParser/IdentifierGrammars.h"
|
|||
#include "src/parser/PrismParser/VariableState.h"
|
|||
|
|||
// If the parser fails due to ill-formed data, this exception is thrown.
|
|||
#include "src/exceptions/WrongFileFormatException.h"
|
|||
|
|||
// Needed for file IO.
|
|||
#include <fstream>
|
|||
#include <iomanip>
|
|||
#include <limits>
|
|||
|
|||
#include "log4cplus/logger.h"
|
|||
#include "log4cplus/loggingmacros.h"
|
|||
extern log4cplus::Logger logger; |
|||
|
|||
// Some typedefs and namespace definitions to reduce code size.
|
|||
typedef std::string::const_iterator BaseIteratorType; |
|||
typedef boost::spirit::classic::position_iterator2<BaseIteratorType> PositionIteratorType; |
|||
namespace qi = boost::spirit::qi; |
|||
namespace phoenix = boost::phoenix; |
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
namespace prism { |
|||
|
|||
void dump(const std::string& s) { |
|||
std::cerr << "Dump: " << s << std::endl; |
|||
} |
|||
|
|||
std::shared_ptr<BaseExpression> PrismGrammar::addIntegerConstant(const std::string& name, const std::shared_ptr<BaseExpression> value) { |
|||
this->state->integerConstants_.add(name, value); |
|||
this->state->allConstantNames_.add(name, name); |
|||
return value; |
|||
} |
|||
|
|||
void PrismGrammar::addLabel(const std::string& name, std::shared_ptr<BaseExpression> value, std::map<std::string, std::shared_ptr<BaseExpression>>& mapping) { |
|||
this->state->labelNames_.add(name, name); |
|||
mapping[name] = value; |
|||
} |
|||
void PrismGrammar::addIntAssignment(const std::string& variable, std::shared_ptr<BaseExpression> value, std::map<std::string, Assignment>& mapping) { |
|||
//std::cout << "Adding int assignment for " << variable << std::endl;
|
|||
this->state->assignedLocalIntegerVariables_.add(variable, variable); |
|||
mapping[variable] = Assignment(variable, value); |
|||
} |
|||
void PrismGrammar::addBoolAssignment(const std::string& variable, std::shared_ptr<BaseExpression> value, std::map<std::string, Assignment>& mapping) { |
|||
//std::cout << "Adding bool assignment for " << variable << std::endl;
|
|||
this->state->assignedLocalBooleanVariables_.add(variable, variable); |
|||
mapping[variable] = Assignment(variable, value); |
|||
} |
|||
Module PrismGrammar::renameModule(const std::string& name, const std::string& oldname, std::map<std::string, std::string>& mapping) { |
|||
this->state->moduleNames_.add(name, name); |
|||
Module* old = this->state->moduleMap_.find(oldname); |
|||
if (old == nullptr) { |
|||
LOG4CPLUS_ERROR(logger, "Renaming module failed: module " << oldname << " does not exist!"); |
|||
throw "Renaming module failed"; |
|||
} |
|||
Module res(*old, name, mapping, this->state); |
|||
this->state->moduleMap_.at(name) = res; |
|||
return res; |
|||
} |
|||
Module PrismGrammar::createModule(const std::string name, std::vector<BooleanVariable>& bools, std::vector<IntegerVariable>& ints, std::map<std::string, uint_fast64_t>& boolids, std::map<std::string, uint_fast64_t> intids, std::vector<storm::ir::Command> commands) { |
|||
this->state->moduleNames_.add(name, name); |
|||
Module res(name, bools, ints, boolids, intids, commands); |
|||
this->state->moduleMap_.at(name) = res; |
|||
return res; |
|||
} |
|||
|
|||
void PrismGrammar::createIntegerVariable(const std::string name, std::shared_ptr<BaseExpression> lower, std::shared_ptr<BaseExpression> upper, std::shared_ptr<BaseExpression> init, std::vector<IntegerVariable>& vars, std::map<std::string, uint_fast64_t>& varids) { |
|||
//std::cout << "Creating int " << name << " = " << init << std::endl;
|
|||
uint_fast64_t id = this->state->addIntegerVariable(name, lower, upper); |
|||
vars.emplace_back(id, name, lower, upper, init); |
|||
varids[name] = id; |
|||
this->state->localIntegerVariables_.add(name, name); |
|||
} |
|||
void PrismGrammar::createBooleanVariable(const std::string name, std::shared_ptr<BaseExpression> init, std::vector<BooleanVariable>& vars, std::map<std::string, uint_fast64_t>& varids) { |
|||
//std::cout << "Creating bool " << name << std::endl;
|
|||
uint_fast64_t id = this->state->addBooleanVariable(name); |
|||
vars.emplace_back(id, name, init); |
|||
varids[name] = id; |
|||
this->state->localBooleanVariables_.add(name, name); |
|||
} |
|||
|
|||
StateReward createStateReward(std::shared_ptr<BaseExpression> guard, std::shared_ptr<BaseExpression> reward) { |
|||
return StateReward(guard, reward); |
|||
} |
|||
TransitionReward createTransitionReward(std::string label, std::shared_ptr<BaseExpression> guard, std::shared_ptr<BaseExpression> reward) { |
|||
return TransitionReward(label, guard, reward); |
|||
} |
|||
void createRewardModel(std::string name, std::vector<StateReward>& stateRewards, std::vector<TransitionReward>& transitionRewards, std::map<std::string, RewardModel>& mapping) { |
|||
mapping[name] = RewardModel(name, stateRewards, transitionRewards); |
|||
} |
|||
Update createUpdate(std::shared_ptr<BaseExpression> likelihood, std::map<std::string, Assignment>& bools, std::map<std::string, Assignment> ints) { |
|||
return Update(likelihood, bools, ints); |
|||
} |
|||
Command createCommand(std::string& label, std::shared_ptr<BaseExpression> guard, std::vector<Update>& updates) { |
|||
return Command(label, guard, updates); |
|||
} |
|||
Program createProgram( |
|||
Program::ModelType modelType, |
|||
std::map<std::string, std::shared_ptr<BooleanConstantExpression>> undefBoolConst, |
|||
std::map<std::string, std::shared_ptr<IntegerConstantExpression>> undefIntConst, |
|||
std::map<std::string, std::shared_ptr<DoubleConstantExpression>> undefDoubleConst, |
|||
std::vector<Module> modules, |
|||
std::map<std::string, RewardModel> rewards, |
|||
std::map<std::string, std::shared_ptr<BaseExpression>> labels) { |
|||
return Program(modelType, undefBoolConst, undefIntConst, undefDoubleConst, modules, rewards, labels); |
|||
} |
|||
|
|||
PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start), state(new VariableState()) { |
|||
|
|||
labelDefinition = (qi::lit("label") >> -qi::lit("\"") >> FreeIdentifierGrammar::instance(this->state) >> -qi::lit("\"") >> qi::lit("=") >> BooleanExpressionGrammar::instance(this->state) >> qi::lit(";")) |
|||
[phoenix::bind(&PrismGrammar::addLabel, this, qi::_1, qi::_2, qi::_r1)]; |
|||
labelDefinition.name("label declaration"); |
|||
labelDefinitionList %= *labelDefinition(qi::_r1); |
|||
labelDefinitionList.name("label declaration list"); |
|||
|
|||
// This block defines all entities that are needed for parsing a reward model.
|
|||
stateRewardDefinition = (BooleanExpressionGrammar::instance(this->state) > qi::lit(":") > ConstDoubleExpressionGrammar::instance(this->state) >> qi::lit(";"))[qi::_val = phoenix::bind(&createStateReward, qi::_1, qi::_2)]; |
|||
stateRewardDefinition.name("state reward definition"); |
|||
transitionRewardDefinition = (qi::lit("[") > -(commandName[qi::_a = qi::_1]) > qi::lit("]") > BooleanExpressionGrammar::instance(this->state) > qi::lit(":") > ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(";"))[qi::_val = phoenix::bind(&createTransitionReward, qi::_a, qi::_2, qi::_3)]; |
|||
transitionRewardDefinition.name("transition reward definition"); |
|||
rewardDefinition = (qi::lit("rewards") > qi::lit("\"") > FreeIdentifierGrammar::instance(this->state) > qi::lit("\"") > +(stateRewardDefinition[phoenix::push_back(qi::_a, qi::_1)] | transitionRewardDefinition[phoenix::push_back(qi::_b, qi::_1)]) >> qi::lit("endrewards")) |
|||
[phoenix::bind(&createRewardModel, qi::_1, qi::_a, qi::_b, qi::_r1)]; |
|||
rewardDefinition.name("reward definition"); |
|||
rewardDefinitionList = *rewardDefinition(qi::_r1); |
|||
rewardDefinitionList.name("reward definition list"); |
|||
|
|||
commandName %= this->state->commandNames_; |
|||
commandName.name("command name"); |
|||
unassignedLocalBooleanVariableName %= this->state->localBooleanVariables_ - this->state->assignedLocalBooleanVariables_; |
|||
unassignedLocalBooleanVariableName.name("unassigned local boolean variable"); |
|||
unassignedLocalIntegerVariableName %= this->state->localIntegerVariables_ - this->state->assignedLocalIntegerVariables_; |
|||
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("=") > IntegerExpressionGrammar::instance(this->state) > qi::lit(")"))[phoenix::bind(&PrismGrammar::addIntAssignment, this, qi::_1, qi::_2, qi::_r2)] | |
|||
(qi::lit("(") >> unassignedLocalBooleanVariableName > qi::lit("'") > qi::lit("=") > BooleanExpressionGrammar::instance(this->state) > qi::lit(")"))[phoenix::bind(&PrismGrammar::addBoolAssignment, this, qi::_1, qi::_2, qi::_r1)]; |
|||
assignmentDefinition.name("assignment"); |
|||
assignmentDefinitionList = assignmentDefinition(qi::_r1, qi::_r2) % "&"; |
|||
assignmentDefinitionList.name("assignment list"); |
|||
updateDefinition = ( |
|||
ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(":")[phoenix::clear(phoenix::ref(this->state->assignedLocalBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedLocalIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::bind(&createUpdate, qi::_1, qi::_a, qi::_b)]; |
|||
updateDefinition.name("update"); |
|||
updateListDefinition = +updateDefinition % "+"; |
|||
updateListDefinition.name("update list"); |
|||
commandDefinition = ( |
|||
qi::lit("[") > -( |
|||
(FreeIdentifierGrammar::instance(this->state)[phoenix::bind(this->state->commandNames_.add, qi::_1, qi::_1)] | commandName)[qi::_a = qi::_1] |
|||
) > qi::lit("]") > BooleanExpressionGrammar::instance(this->state) > qi::lit("->") > updateListDefinition > qi::lit(";") |
|||
)[qi::_val = phoenix::bind(&createCommand, qi::_a, qi::_2, qi::_3)]; |
|||
commandDefinition.name("command"); |
|||
|
|||
// This block defines all entities that are needed for parsing variable definitions.
|
|||
booleanVariableDefinition = (FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > ConstBooleanExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct<std::shared_ptr<BaseExpression>>(qi::_1)]) > qi::lit(";")) |
|||
[ |
|||
phoenix::bind(&PrismGrammar::createBooleanVariable, this, qi::_1, qi::_b, qi::_r1, qi::_r2) |
|||
]; |
|||
booleanVariableDefinition.name("boolean variable declaration"); |
|||
|
|||
integerVariableDefinition = (FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("[") > ConstIntegerExpressionGrammar::instance(this->state) > qi::lit("..") > ConstIntegerExpressionGrammar::instance(this->state) > qi::lit("]") > -(qi::lit("init") > ConstIntegerExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct<std::shared_ptr<BaseExpression>>(qi::_1)]) > qi::lit(";")) |
|||
[ |
|||
phoenix::bind(&PrismGrammar::createIntegerVariable, this, qi::_1, qi::_2, qi::_3, qi::_b, qi::_r1, qi::_r2) |
|||
]; |
|||
integerVariableDefinition.name("integer variable declaration"); |
|||
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") >> FreeIdentifierGrammar::instance(this->state)[phoenix::bind(&VariableState::startModule, *this->state)] |
|||
>> *(variableDefinition(qi::_a, qi::_b, qi::_c, qi::_d)) >> +commandDefinition > qi::lit("endmodule")) |
|||
[qi::_val = phoenix::bind(&PrismGrammar::createModule, this, qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2)]; |
|||
|
|||
moduleDefinition.name("module"); |
|||
moduleRenaming = (qi::lit("module") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") |
|||
> this->state->moduleNames_ > qi::lit("[") > *( |
|||
(IdentifierGrammar::instance(this->state) > qi::lit("=") > IdentifierGrammar::instance(this->state) >> -qi::lit(","))[phoenix::insert(qi::_a, phoenix::construct<std::pair<std::string,std::string>>(qi::_1, qi::_2))] |
|||
) > qi::lit("]") > qi::lit("endmodule")) |
|||
[qi::_val = phoenix::bind(&PrismGrammar::renameModule, this, qi::_1, qi::_2, qi::_a)]; |
|||
moduleRenaming.name("renamed module"); |
|||
moduleDefinitionList %= +(moduleDefinition | moduleRenaming); |
|||
moduleDefinitionList.name("module list"); |
|||
|
|||
// This block defines all entities that are needed for parsing constant definitions.
|
|||
definedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") > ConstBooleanExpressionGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(this->state->booleanConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; |
|||
definedBooleanConstantDefinition.name("defined boolean constant declaration"); |
|||
definedIntegerConstantDefinition = ( |
|||
qi::lit("const") >> qi::lit("int") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> |
|||
ConstIntegerExpressionGrammar::instance(this->state) >> qi::lit(";") |
|||
)[ qi::_val = phoenix::bind(&PrismGrammar::addIntegerConstant, this, qi::_1, qi::_2) ]; |
|||
definedIntegerConstantDefinition.name("defined integer constant declaration"); |
|||
definedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") > ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(this->state->doubleConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; |
|||
definedDoubleConstantDefinition.name("defined double constant declaration"); |
|||
undefinedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[qi::_a = phoenix::construct<std::shared_ptr<BooleanConstantExpression>>(phoenix::new_<BooleanConstantExpression>(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, std::shared_ptr<BooleanConstantExpression>>>(qi::_1, qi::_a)), phoenix::bind(this->state->booleanConstants_.add, qi::_1, qi::_a), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1)]; |
|||
undefinedBooleanConstantDefinition.name("undefined boolean constant declaration"); |
|||
undefinedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[qi::_a = phoenix::construct<std::shared_ptr<IntegerConstantExpression>>(phoenix::new_<IntegerConstantExpression>(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, std::shared_ptr<IntegerConstantExpression>>>(qi::_1, qi::_a)), phoenix::bind(this->state->integerConstants_.add, qi::_1, qi::_a), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1)]; |
|||
undefinedIntegerConstantDefinition.name("undefined integer constant declaration"); |
|||
undefinedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[qi::_a = phoenix::construct<std::shared_ptr<DoubleConstantExpression>>(phoenix::new_<DoubleConstantExpression>(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, std::shared_ptr<DoubleConstantExpression>>>(qi::_1, qi::_a)), phoenix::bind(this->state->doubleConstants_.add, qi::_1, qi::_a), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1)]; |
|||
undefinedDoubleConstantDefinition.name("undefined double constant declaration"); |
|||
definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition); |
|||
definedConstantDefinition.name("defined constant declaration"); |
|||
undefinedConstantDefinition = (undefinedBooleanConstantDefinition(qi::_r1) | undefinedIntegerConstantDefinition(qi::_r2) | undefinedDoubleConstantDefinition(qi::_r3)); |
|||
undefinedConstantDefinition.name("undefined constant declaration"); |
|||
constantDefinitionList = *(definedConstantDefinition | undefinedConstantDefinition(qi::_r1, qi::_r2, qi::_r3)); |
|||
constantDefinitionList.name("constant declaration list"); |
|||
|
|||
// This block defines all entities that are needed for parsing a program.
|
|||
modelTypeDefinition = modelType_; |
|||
modelTypeDefinition.name("model type"); |
|||
start = ( |
|||
modelTypeDefinition > |
|||
constantDefinitionList(qi::_a, qi::_b, qi::_c) > |
|||
moduleDefinitionList > |
|||
rewardDefinitionList(qi::_d) > |
|||
labelDefinitionList(qi::_e) |
|||
)[qi::_val = phoenix::bind(&createProgram, qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_d, qi::_e)]; |
|||
start.name("probabilistic program declaration"); |
|||
} |
|||
|
|||
void PrismGrammar::prepareForSecondRun() { |
|||
LOG4CPLUS_INFO(logger, "Preparing parser for second run."); |
|||
this->state->prepareForSecondRun(); |
|||
BooleanExpressionGrammar::secondRun(); |
|||
ConstBooleanExpressionGrammar::secondRun(); |
|||
ConstDoubleExpressionGrammar::secondRun(); |
|||
ConstIntegerExpressionGrammar::secondRun(); |
|||
IntegerExpressionGrammar::secondRun(); |
|||
} |
|||
|
|||
void PrismGrammar::resetGrammars() { |
|||
LOG4CPLUS_INFO(logger, "Resetting grammars."); |
|||
BooleanExpressionGrammar::resetInstance(); |
|||
ConstBooleanExpressionGrammar::resetInstance(); |
|||
ConstDoubleExpressionGrammar::resetInstance(); |
|||
ConstIntegerExpressionGrammar::resetInstance(); |
|||
IntegerExpressionGrammar::resetInstance(); |
|||
} |
|||
|
|||
} // namespace prism
|
|||
} // namespace parser
|
|||
} // namespace storm
|
|||
@ -0,0 +1,142 @@ |
|||
/* |
|||
* File: PrismGrammar.h |
|||
* Author: nafur |
|||
* |
|||
* Created on April 30, 2013, 5:20 PM |
|||
*/ |
|||
|
|||
#ifndef PRISMGRAMMAR_H |
|||
#define PRISMGRAMMAR_H |
|||
|
|||
// All classes of the intermediate representation are used. |
|||
#include "src/ir/IR.h" |
|||
#include "src/parser/PrismParser/Includes.h" |
|||
#include "src/parser/PrismParser/Tokens.h" |
|||
#include "src/parser/PrismParser/IdentifierGrammars.h" |
|||
#include "src/parser/PrismParser/VariableState.h" |
|||
#include "src/parser/PrismParser/ConstBooleanExpressionGrammar.h" |
|||
#include "src/parser/PrismParser/ConstDoubleExpressionGrammar.h" |
|||
#include "src/parser/PrismParser/ConstIntegerExpressionGrammar.h" |
|||
#include "src/parser/PrismParser/BooleanExpressionGrammar.h" |
|||
#include "src/parser/PrismParser/IntegerExpressionGrammar.h" |
|||
|
|||
// Used for file input. |
|||
#include <istream> |
|||
#include <memory> |
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
namespace prism { |
|||
|
|||
using namespace storm::ir; |
|||
using namespace storm::ir::expressions; |
|||
|
|||
/*! |
|||
* The Boost spirit grammar for the PRISM language. Returns the intermediate representation of |
|||
* the input that complies with the PRISM syntax. |
|||
*/ |
|||
class PrismGrammar : public qi::grammar< |
|||
Iterator, |
|||
Program(), |
|||
qi::locals< |
|||
std::map<std::string, std::shared_ptr<BooleanConstantExpression>>, |
|||
std::map<std::string, std::shared_ptr<IntegerConstantExpression>>, |
|||
std::map<std::string, std::shared_ptr<DoubleConstantExpression>>, |
|||
std::map<std::string, RewardModel>, |
|||
std::map<std::string, std::shared_ptr<BaseExpression>> |
|||
>, |
|||
Skipper> { |
|||
public: |
|||
PrismGrammar(); |
|||
void prepareForSecondRun(); |
|||
void resetGrammars(); |
|||
|
|||
private: |
|||
|
|||
std::shared_ptr<storm::parser::prism::VariableState> state; |
|||
|
|||
// The starting point of the grammar. |
|||
qi::rule< |
|||
Iterator, |
|||
Program(), |
|||
qi::locals< |
|||
std::map<std::string, std::shared_ptr<BooleanConstantExpression>>, |
|||
std::map<std::string, std::shared_ptr<IntegerConstantExpression>>, |
|||
std::map<std::string, std::shared_ptr<DoubleConstantExpression>>, |
|||
std::map<std::string, RewardModel>, |
|||
std::map<std::string, std::shared_ptr<BaseExpression>> |
|||
>, |
|||
Skipper> start; |
|||
qi::rule<Iterator, Program::ModelType(), Skipper> modelTypeDefinition; |
|||
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BooleanConstantExpression>>&, std::map<std::string, std::shared_ptr<IntegerConstantExpression>>&, std::map<std::string, std::shared_ptr<DoubleConstantExpression>>&), Skipper> constantDefinitionList; |
|||
qi::rule<Iterator, std::vector<Module>(), Skipper> moduleDefinitionList; |
|||
|
|||
// Rules for module definition. |
|||
qi::rule<Iterator, Module(), qi::locals<std::vector<BooleanVariable>, std::vector<IntegerVariable>, std::map<std::string, uint_fast64_t>, std::map<std::string, uint_fast64_t>>, Skipper> moduleDefinition; |
|||
qi::rule<Iterator, Module(), qi::locals<std::map<std::string, std::string>>, Skipper> moduleRenaming; |
|||
|
|||
// Rules for variable definitions. |
|||
qi::rule<Iterator, qi::unused_type(std::vector<BooleanVariable>&, std::vector<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<BooleanVariable>&, std::map<std::string, uint_fast64_t>&), qi::locals<uint_fast64_t, std::shared_ptr<BaseExpression>>, Skipper> booleanVariableDefinition; |
|||
qi::rule<Iterator, qi::unused_type(std::vector<IntegerVariable>&, std::map<std::string, uint_fast64_t>&), qi::locals<uint_fast64_t, std::shared_ptr<BaseExpression>>, Skipper> integerVariableDefinition; |
|||
|
|||
// Rules for command definitions. |
|||
qi::rule<Iterator, Command(), qi::locals<std::string>, Skipper> commandDefinition; |
|||
qi::rule<Iterator, std::vector<Update>(), Skipper> updateListDefinition; |
|||
qi::rule<Iterator, Update(), qi::locals<std::map<std::string, Assignment>, std::map<std::string, Assignment>>, Skipper> updateDefinition; |
|||
qi::rule<Iterator, qi::unused_type(std::map<std::string, Assignment>&, std::map<std::string, Assignment>&), Skipper> assignmentDefinitionList; |
|||
qi::rule<Iterator, qi::unused_type(std::map<std::string, Assignment>&, std::map<std::string, Assignment>&), Skipper> assignmentDefinition; |
|||
|
|||
// Rules for variable/command names. |
|||
qi::rule<Iterator, std::string(), Skipper> commandName; |
|||
qi::rule<Iterator, std::string(), Skipper> unassignedLocalBooleanVariableName; |
|||
qi::rule<Iterator, std::string(), Skipper> unassignedLocalIntegerVariableName; |
|||
|
|||
// Rules for reward definitions. |
|||
qi::rule<Iterator, qi::unused_type(std::map<std::string, RewardModel>&), Skipper> rewardDefinitionList; |
|||
qi::rule<Iterator, qi::unused_type(std::map<std::string, RewardModel>&), qi::locals<std::vector<StateReward>, std::vector<TransitionReward>>, Skipper> rewardDefinition; |
|||
qi::rule<Iterator, StateReward(), Skipper> stateRewardDefinition; |
|||
qi::rule<Iterator, TransitionReward(), qi::locals<std::string>, Skipper> transitionRewardDefinition; |
|||
|
|||
// Rules for label definitions. |
|||
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BaseExpression>>&), Skipper> labelDefinitionList; |
|||
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BaseExpression>>&), Skipper> labelDefinition; |
|||
|
|||
// Rules for constant definitions. |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantDefinition; |
|||
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BooleanConstantExpression>>&, std::map<std::string, std::shared_ptr<IntegerConstantExpression>>&, std::map<std::string, std::shared_ptr<DoubleConstantExpression>>&), Skipper> undefinedConstantDefinition; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedConstantDefinition; |
|||
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BooleanConstantExpression>>&), qi::locals<std::shared_ptr<BooleanConstantExpression>>, Skipper> undefinedBooleanConstantDefinition; |
|||
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<IntegerConstantExpression>>&), qi::locals<std::shared_ptr<IntegerConstantExpression>>, Skipper> undefinedIntegerConstantDefinition; |
|||
qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<DoubleConstantExpression>>&), qi::locals<std::shared_ptr<DoubleConstantExpression>>, Skipper> undefinedDoubleConstantDefinition; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedBooleanConstantDefinition; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedIntegerConstantDefinition; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedDoubleConstantDefinition; |
|||
|
|||
// Rules for variable recognition. |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> booleanVariableCreatorExpression; |
|||
qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<std::shared_ptr<BaseExpression>>, Skipper> integerVariableCreatorExpression; |
|||
|
|||
storm::parser::prism::keywordsStruct keywords_; |
|||
storm::parser::prism::modelTypeStruct modelType_; |
|||
storm::parser::prism::relationalOperatorStruct relations_; |
|||
|
|||
std::shared_ptr<BaseExpression> addIntegerConstant(const std::string& name, const std::shared_ptr<BaseExpression> value); |
|||
void addLabel(const std::string& name, std::shared_ptr<BaseExpression> value, std::map<std::string, std::shared_ptr<BaseExpression>>& mapping); |
|||
void addBoolAssignment(const std::string& variable, std::shared_ptr<BaseExpression> value, std::map<std::string, Assignment>& mapping); |
|||
void addIntAssignment(const std::string& variable, std::shared_ptr<BaseExpression> value, std::map<std::string, Assignment>& mapping); |
|||
Module renameModule(const std::string& name, const std::string& oldname, std::map<std::string, std::string>& mapping); |
|||
Module createModule(const std::string name, std::vector<BooleanVariable>& bools, std::vector<IntegerVariable>& ints, std::map<std::string, uint_fast64_t>& boolids, std::map<std::string, uint_fast64_t> intids, std::vector<storm::ir::Command> commands); |
|||
|
|||
void createIntegerVariable(const std::string name, std::shared_ptr<BaseExpression> lower, std::shared_ptr<BaseExpression> upper, std::shared_ptr<BaseExpression> init, std::vector<IntegerVariable>& vars, std::map<std::string, uint_fast64_t>& varids); |
|||
void createBooleanVariable(const std::string name, std::shared_ptr<BaseExpression> init, std::vector<BooleanVariable>& vars, std::map<std::string, uint_fast64_t>& varids); |
|||
}; |
|||
|
|||
|
|||
} // namespace prism |
|||
} // namespace parser |
|||
} // namespace storm |
|||
|
|||
|
|||
#endif /* PRISMGRAMMAR_H */ |
|||
|
|||
@ -0,0 +1,70 @@ |
|||
/* |
|||
* File: Tokens.h |
|||
* Author: nafur |
|||
* |
|||
* Created on April 19, 2013, 11:17 PM |
|||
*/ |
|||
|
|||
#ifndef TOKENS_H |
|||
#define TOKENS_H |
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
namespace prism { |
|||
|
|||
|
|||
// A structure mapping the textual representation of a model type to the model type |
|||
// representation of the intermediate representation. |
|||
struct modelTypeStruct : qi::symbols<char, Program::ModelType> { |
|||
modelTypeStruct() { |
|||
add |
|||
("dtmc", Program::ModelType::DTMC) |
|||
("ctmc", Program::ModelType::CTMC) |
|||
("mdp", Program::ModelType::MDP) |
|||
("ctmdp", Program::ModelType::CTMDP) |
|||
; |
|||
} |
|||
}; |
|||
|
|||
|
|||
// A structure defining the keywords that are not allowed to be chosen as identifiers. |
|||
struct keywordsStruct : qi::symbols<char, unsigned> { |
|||
keywordsStruct() { |
|||
add |
|||
("dtmc", 1) |
|||
("ctmc", 2) |
|||
("mdp", 3) |
|||
("ctmdp", 4) |
|||
("const", 5) |
|||
("int", 6) |
|||
("bool", 7) |
|||
("module", 8) |
|||
("endmodule", 9) |
|||
("rewards", 10) |
|||
("endrewards", 11) |
|||
("true", 12) |
|||
("false", 13) |
|||
; |
|||
} |
|||
}; |
|||
|
|||
// A structure mapping the textual representation of a binary relation to the representation |
|||
// of the intermediate representation. |
|||
struct relationalOperatorStruct : qi::symbols<char, BinaryRelationExpression::RelationType> { |
|||
relationalOperatorStruct() { |
|||
add |
|||
("=", BinaryRelationExpression::EQUAL) |
|||
("!=", BinaryRelationExpression::NOT_EQUAL) |
|||
("<", BinaryRelationExpression::LESS) |
|||
("<=", BinaryRelationExpression::LESS_OR_EQUAL) |
|||
(">", BinaryRelationExpression::GREATER) |
|||
(">=", BinaryRelationExpression::GREATER_OR_EQUAL) |
|||
; |
|||
} |
|||
}; |
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* TOKENS_H */ |
|||
|
|||
@ -0,0 +1,171 @@ |
|||
#include "VariableState.h"
|
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
namespace prism { |
|||
|
|||
using namespace storm::ir; |
|||
using namespace storm::ir::expressions; |
|||
|
|||
template<typename T> |
|||
struct SymbolDump { |
|||
SymbolDump(std::ostream& out) : out(out) {} |
|||
void operator() (std::basic_string<char> s, T elem) { |
|||
this->out << "\t" << s << " -> " << elem << std::endl; |
|||
} |
|||
private: |
|||
std::ostream& out; |
|||
}; |
|||
template<typename T> |
|||
std::ostream& operator<<(std::ostream& out, qi::symbols<char, T>& symbols) { |
|||
out << "Dumping symbol table" << std::endl; |
|||
SymbolDump<T> dump(out); |
|||
symbols.for_each(dump); |
|||
return out; |
|||
} |
|||
std::ostream& operator<<(std::ostream& out, VariableState::variableNamesStruct& symbols) { |
|||
SymbolDump<std::string> dump(out); |
|||
symbols.for_each(dump); |
|||
return out; |
|||
} |
|||
|
|||
|
|||
VariableState::VariableState(bool firstRun) |
|||
: firstRun(firstRun), keywords(), nextBooleanVariableIndex(0), nextIntegerVariableIndex(0) { |
|||
} |
|||
|
|||
uint_fast64_t VariableState::addBooleanVariable(const std::string& name) { |
|||
if (firstRun) { |
|||
std::shared_ptr<VariableExpression> varExpr = std::shared_ptr<VariableExpression>(new VariableExpression(storm::ir::expressions::BaseExpression::bool_, this->nextBooleanVariableIndex, name)); |
|||
LOG4CPLUS_TRACE(logger, "Adding boolean variable " << name << " with new id " << this->nextBooleanVariableIndex); |
|||
this->booleanVariables_.add(name, varExpr); |
|||
this->booleanVariableNames_.add(name, name); |
|||
this->nextBooleanVariableIndex++; |
|||
return varExpr->getVariableIndex(); |
|||
} else { |
|||
std::shared_ptr<VariableExpression> res = this->booleanVariables_.at(name); |
|||
if (res != nullptr) { |
|||
return res->getVariableIndex(); |
|||
} else { |
|||
LOG4CPLUS_ERROR(logger, "Boolean variable " << name << " was not created in first run."); |
|||
return 0; |
|||
} |
|||
} |
|||
} |
|||
|
|||
uint_fast64_t VariableState::addIntegerVariable(const std::string& name, const std::shared_ptr<storm::ir::expressions::BaseExpression> lower, const std::shared_ptr<storm::ir::expressions::BaseExpression> upper) { |
|||
if (firstRun) { |
|||
std::shared_ptr<VariableExpression> varExpr = std::shared_ptr<VariableExpression>(new VariableExpression(storm::ir::expressions::BaseExpression::int_, this->nextIntegerVariableIndex, name, lower, upper)); |
|||
LOG4CPLUS_TRACE(logger, "Adding integer variable " << name << " with new id " << this->nextIntegerVariableIndex); |
|||
this->integerVariables_.add(name, varExpr); |
|||
this->integerVariableNames_.add(name, name); |
|||
this->nextIntegerVariableIndex++; |
|||
return varExpr->getVariableIndex(); |
|||
} else { |
|||
std::shared_ptr<VariableExpression> res = this->integerVariables_.at(name); |
|||
if (res != nullptr) { |
|||
return res->getVariableIndex(); |
|||
} else { |
|||
|
|||
LOG4CPLUS_ERROR(logger, "Integer variable " << name << " was not created in first run."); |
|||
return 0; |
|||
} |
|||
} |
|||
} |
|||
|
|||
std::shared_ptr<VariableExpression> VariableState::getBooleanVariable(const std::string& name) { |
|||
std::shared_ptr<VariableExpression>* res = this->booleanVariables_.find(name); |
|||
if (res != nullptr) { |
|||
return *res; |
|||
} else { |
|||
if (firstRun) { |
|||
LOG4CPLUS_TRACE(logger, "Getting boolean variable " << name << ", was not yet created."); |
|||
return std::shared_ptr<VariableExpression>(new VariableExpression(BaseExpression::bool_, std::numeric_limits<uint_fast64_t>::max(), "bool", std::shared_ptr<BaseExpression>(nullptr), std::shared_ptr<BaseExpression>(nullptr))); |
|||
} else { |
|||
LOG4CPLUS_ERROR(logger, "Getting boolean variable " << name << ", but was not found. This variable does not exist."); |
|||
return std::shared_ptr<VariableExpression>(nullptr); |
|||
} |
|||
} |
|||
} |
|||
|
|||
std::shared_ptr<VariableExpression> VariableState::getIntegerVariable(const std::string& name) { |
|||
std::shared_ptr<VariableExpression>* res = this->integerVariables_.find(name); |
|||
if (res != nullptr) { |
|||
return *res; |
|||
} else { |
|||
if (firstRun) { |
|||
LOG4CPLUS_TRACE(logger, "Getting integer variable " << name << ", was not yet created."); |
|||
return std::shared_ptr<VariableExpression>(new VariableExpression(BaseExpression::int_, std::numeric_limits<uint_fast64_t>::max(), "int", std::shared_ptr<BaseExpression>(nullptr), std::shared_ptr<BaseExpression>(nullptr))); |
|||
} else { |
|||
LOG4CPLUS_ERROR(logger, "Getting integer variable " << name << ", but was not found. This variable does not exist."); |
|||
return std::shared_ptr<VariableExpression>(nullptr); |
|||
} |
|||
} |
|||
} |
|||
std::shared_ptr<VariableExpression> VariableState::getVariable(const std::string& name) { |
|||
std::shared_ptr<VariableExpression>* res = this->integerVariables_.find(name); |
|||
if (res != nullptr) { |
|||
return *res; |
|||
} else { |
|||
res = this->booleanVariables_.find(name); |
|||
if (res != nullptr) { |
|||
return *res; |
|||
} else { |
|||
return std::shared_ptr<VariableExpression>(nullptr); |
|||
} |
|||
} |
|||
} |
|||
|
|||
void VariableState::performRenaming(const std::map<std::string, std::string>& renaming) { |
|||
for (auto it: renaming) { |
|||
std::shared_ptr<VariableExpression>* original = this->integerVariables_.find(it.first); |
|||
if (original != nullptr) { |
|||
std::shared_ptr<VariableExpression>* next = this->integerVariables_.find(it.second); |
|||
if (next == nullptr) { |
|||
this->addIntegerVariable(it.second, (*original)->getLowerBound(), (*original)->getUpperBound()); |
|||
} |
|||
} |
|||
original = this->booleanVariables_.find(it.first); |
|||
if (original != nullptr) { |
|||
if (this->booleanVariables_.find(it.second) == nullptr) { |
|||
this->addBooleanVariable(it.second); |
|||
} |
|||
} |
|||
std::string* oldCmdName = this->commandNames_.find(it.first); |
|||
if (oldCmdName != nullptr) { |
|||
LOG4CPLUS_TRACE(logger, "Adding new command name " << it.second << " due to module renaming."); |
|||
this->commandNames_.at(it.second) = it.second; |
|||
} |
|||
} |
|||
} |
|||
|
|||
void VariableState::startModule() { |
|||
this->localBooleanVariables_.clear(); |
|||
this->localIntegerVariables_.clear(); |
|||
} |
|||
|
|||
bool VariableState::isFreeIdentifier(std::string& s) const { |
|||
if (this->integerVariableNames_.find(s) != nullptr) return false; |
|||
if (this->allConstantNames_.find(s) != nullptr) return false; |
|||
if (this->labelNames_.find(s) != nullptr) return false; |
|||
if (this->moduleNames_.find(s) != nullptr) return false; |
|||
if (this->keywords.find(s) != nullptr) return false; |
|||
return true; |
|||
} |
|||
bool VariableState::isIdentifier(std::string& s) const { |
|||
if (this->allConstantNames_.find(s) != nullptr) return false; |
|||
if (this->keywords.find(s) != nullptr) return false; |
|||
return true; |
|||
} |
|||
|
|||
void VariableState::prepareForSecondRun() { |
|||
integerConstants_.clear(); |
|||
booleanConstants_.clear(); |
|||
doubleConstants_.clear(); |
|||
allConstantNames_.clear(); |
|||
this->firstRun = false; |
|||
} |
|||
|
|||
} |
|||
} |
|||
} |
|||
@ -0,0 +1,71 @@ |
|||
/* |
|||
* File: VariableState.h |
|||
* Author: nafur |
|||
* |
|||
* Created on April 10, 2013, 4:43 PM |
|||
*/ |
|||
|
|||
#ifndef VARIABLESTATE_H |
|||
#define VARIABLESTATE_H |
|||
|
|||
#include "src/ir/IR.h" |
|||
#include "Includes.h" |
|||
#include "Tokens.h" |
|||
#include <iostream> |
|||
|
|||
namespace storm { |
|||
namespace parser { |
|||
namespace prism { |
|||
|
|||
using namespace storm::ir; |
|||
using namespace storm::ir::expressions; |
|||
|
|||
template<typename T> |
|||
std::ostream& operator<<(std::ostream& out, qi::symbols<char, T>& symbols); |
|||
|
|||
struct VariableState : public storm::ir::VariableAdder { |
|||
|
|||
public: |
|||
VariableState(bool firstRun = true); |
|||
|
|||
public: |
|||
bool firstRun; |
|||
keywordsStruct keywords; |
|||
|
|||
// 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<VariableExpression>> integerVariables_, booleanVariables_; |
|||
struct qi::symbols<char, std::shared_ptr<BaseExpression>> integerConstants_, booleanConstants_, doubleConstants_; |
|||
struct qi::symbols<char, Module> moduleMap_; |
|||
|
|||
// A structure representing the identity function over identifier names. |
|||
struct variableNamesStruct : qi::symbols<char, std::string> { } integerVariableNames_, booleanVariableNames_, commandNames_, labelNames_, allConstantNames_, moduleNames_, |
|||
localBooleanVariables_, localIntegerVariables_, assignedLocalBooleanVariables_, assignedLocalIntegerVariables_; |
|||
public: |
|||
uint_fast64_t addBooleanVariable(const std::string& name); |
|||
uint_fast64_t addIntegerVariable(const std::string& name, const std::shared_ptr<storm::ir::expressions::BaseExpression> lower, const std::shared_ptr<storm::ir::expressions::BaseExpression> upper); |
|||
|
|||
std::shared_ptr<VariableExpression> getBooleanVariable(const std::string& name); |
|||
std::shared_ptr<VariableExpression> getIntegerVariable(const std::string& name); |
|||
std::shared_ptr<VariableExpression> getVariable(const std::string& name); |
|||
|
|||
void performRenaming(const std::map<std::string, std::string>& renaming); |
|||
|
|||
void startModule(); |
|||
|
|||
bool isFreeIdentifier(std::string& s) const; |
|||
bool isIdentifier(std::string& s) const; |
|||
|
|||
void prepareForSecondRun(); |
|||
}; |
|||
|
|||
} |
|||
} |
|||
} |
|||
|
|||
#endif /* VARIABLESTATE_H */ |
|||
|
|||
@ -0,0 +1,195 @@ |
|||
/*
|
|||
* CuddUtility.cpp |
|||
* |
|||
* Created on: 26.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#include "CuddUtility.h"
|
|||
#include "src/exceptions/InvalidArgumentException.h"
|
|||
|
|||
#include "log4cplus/logger.h"
|
|||
#include "log4cplus/loggingmacros.h"
|
|||
|
|||
extern log4cplus::Logger logger; |
|||
|
|||
#include <stdio.h>
|
|||
#include <iostream>
|
|||
|
|||
namespace storm { |
|||
|
|||
namespace utility { |
|||
|
|||
storm::utility::CuddUtility* storm::utility::CuddUtility::instance = nullptr; |
|||
|
|||
ADD* CuddUtility::getNewAddVariable() { |
|||
ADD* result = new ADD(manager.addVar()); |
|||
allDecisionDiagramVariables.push_back(result); |
|||
return result; |
|||
} |
|||
|
|||
ADD* CuddUtility::getAddVariable(int index) const { |
|||
return new ADD(manager.addVar(index)); |
|||
} |
|||
|
|||
ADD* CuddUtility::getOne() const { |
|||
return new ADD(manager.addOne()); |
|||
} |
|||
|
|||
ADD* CuddUtility::getZero() const { |
|||
return new ADD(manager.addZero()); |
|||
} |
|||
|
|||
ADD* CuddUtility::getConstantEncoding(uint_fast64_t constant, std::vector<ADD*> const& variables) const { |
|||
if ((constant >> variables.size()) != 0) { |
|||
LOG4CPLUS_ERROR(logger, "Cannot create encoding for constant " << constant << " with " |
|||
<< variables.size() << " variables."); |
|||
throw storm::exceptions::InvalidArgumentException() << "Cannot create encoding" |
|||
<< " for constant " << constant << " with " << variables.size() |
|||
<< " variables."; |
|||
} |
|||
|
|||
// Determine whether the new ADD will be rooted by the first variable or its complement.
|
|||
ADD initialNode; |
|||
if ((constant & (1 << (variables.size() - 1))) != 0) { |
|||
initialNode = *variables[0]; |
|||
} else { |
|||
initialNode = ~(*variables[0]); |
|||
} |
|||
ADD* result = new ADD(initialNode); |
|||
|
|||
// Add (i.e. multiply) the other variables as well according to whether their bit is set or not.
|
|||
for (uint_fast64_t i = 1; i < variables.size(); ++i) { |
|||
if ((constant & (1 << (variables.size() - i - 1))) != 0) { |
|||
*result *= *variables[i]; |
|||
} else { |
|||
*result *= ~(*variables[i]); |
|||
} |
|||
} |
|||
|
|||
return result; |
|||
} |
|||
|
|||
void CuddUtility::setValueAtIndex(ADD* add, uint_fast64_t index, std::vector<ADD*> const& variables, double value) const { |
|||
if ((index >> variables.size()) != 0) { |
|||
LOG4CPLUS_ERROR(logger, "Cannot create encoding for index " << index << " with " |
|||
<< variables.size() << " variables."); |
|||
throw storm::exceptions::InvalidArgumentException() << "Cannot create encoding" |
|||
<< " for index " << index << " with " << variables.size() |
|||
<< " variables."; |
|||
} |
|||
|
|||
// Determine whether the new ADD will be rooted by the first variable or its complement.
|
|||
ADD initialNode; |
|||
if ((index & (1 << (variables.size() - 1))) != 0) { |
|||
initialNode = *variables[0]; |
|||
} else { |
|||
initialNode = ~(*variables[0]); |
|||
} |
|||
ADD* encoding = new ADD(initialNode); |
|||
|
|||
// Add (i.e. multiply) the other variables as well according to whether their bit is set or not.
|
|||
for (uint_fast64_t i = 1; i < variables.size(); ++i) { |
|||
if ((index & (1 << (variables.size() - i - 1))) != 0) { |
|||
*encoding *= *variables[i]; |
|||
} else { |
|||
*encoding *= ~(*variables[i]); |
|||
} |
|||
} |
|||
|
|||
*add = encoding->Ite(manager.constant(value), *add); |
|||
} |
|||
|
|||
void CuddUtility::setValueAtIndices(ADD* add, uint_fast64_t rowIndex, uint_fast64_t columnIndex, std::vector<ADD*> const& rowVariables, std::vector<ADD*> const& columnVariables, double value) const { |
|||
if ((rowIndex >> rowVariables.size()) != 0) { |
|||
LOG4CPLUS_ERROR(logger, "Cannot create encoding for index " << rowIndex << " with " |
|||
<< rowVariables.size() << " variables."); |
|||
throw storm::exceptions::InvalidArgumentException() << "Cannot create encoding" |
|||
<< " for index " << rowIndex << " with " << rowVariables.size() |
|||
<< " variables."; |
|||
} |
|||
if ((columnIndex >> columnVariables.size()) != 0) { |
|||
LOG4CPLUS_ERROR(logger, "Cannot create encoding for index " << columnIndex << " with " |
|||
<< columnVariables.size() << " variables."); |
|||
throw storm::exceptions::InvalidArgumentException() << "Cannot create encoding" |
|||
<< " for index " << columnIndex << " with " << columnVariables.size() |
|||
<< " variables."; |
|||
} |
|||
if (rowVariables.size() != columnVariables.size()) { |
|||
LOG4CPLUS_ERROR(logger, "Number of variables for indices encodings does not match."); |
|||
throw storm::exceptions::InvalidArgumentException() |
|||
<< "Number of variables for indices encodings does not match."; |
|||
} |
|||
|
|||
ADD initialNode; |
|||
if ((rowIndex & (1 << (rowVariables.size() - 1))) != 0) { |
|||
initialNode = *rowVariables[0]; |
|||
} else { |
|||
initialNode = ~(*rowVariables[0]); |
|||
} |
|||
ADD* encoding = new ADD(initialNode); |
|||
if ((columnIndex & (1 << (rowVariables.size() - 1))) != 0) { |
|||
*encoding *= *columnVariables[0]; |
|||
} else { |
|||
*encoding *= ~(*columnVariables[0]); |
|||
} |
|||
|
|||
for (uint_fast64_t i = 1; i < rowVariables.size(); ++i) { |
|||
if ((rowIndex & (1 << (rowVariables.size() - i - 1))) != 0) { |
|||
*encoding *= *rowVariables[i]; |
|||
} else { |
|||
*encoding *= ~(*rowVariables[i]); |
|||
} |
|||
if ((columnIndex & (1 << (columnVariables.size() - i - 1))) != 0) { |
|||
*encoding *= *columnVariables[i]; |
|||
} else { |
|||
*encoding *= ~(*columnVariables[i]); |
|||
} |
|||
} |
|||
|
|||
*add = encoding->Ite(manager.constant(value), *add); |
|||
} |
|||
|
|||
|
|||
ADD* CuddUtility::getConstant(double value) const { |
|||
return new ADD(manager.constant(value)); |
|||
} |
|||
|
|||
ADD* CuddUtility::permuteVariables(ADD* add, std::vector<ADD*> fromVariables, std::vector<ADD*> toVariables, uint_fast64_t totalNumberOfVariables) const { |
|||
std::vector<int> permutation; |
|||
permutation.resize(totalNumberOfVariables); |
|||
for (uint_fast64_t i = 0; i < totalNumberOfVariables; ++i) { |
|||
permutation[i] = i; |
|||
} |
|||
for (uint_fast64_t i = 0; i < fromVariables.size(); ++i) { |
|||
permutation[fromVariables[i]->NodeReadIndex()] = toVariables[i]->NodeReadIndex(); |
|||
} |
|||
return new ADD(add->Permute(&permutation[0])); |
|||
} |
|||
|
|||
void CuddUtility::dumpDotToFile(ADD* add, std::string filename) const { |
|||
std::vector<ADD> nodes; |
|||
nodes.push_back(*add); |
|||
|
|||
FILE* filePtr; |
|||
filePtr = fopen(filename.c_str(), "w"); |
|||
manager.DumpDot(nodes, 0, 0, filePtr); |
|||
fclose(filePtr); |
|||
} |
|||
|
|||
Cudd const& CuddUtility::getManager() const { |
|||
return manager; |
|||
} |
|||
|
|||
CuddUtility* cuddUtilityInstance() { |
|||
if (CuddUtility::instance == nullptr) { |
|||
CuddUtility::instance = new CuddUtility(); |
|||
} |
|||
return CuddUtility::instance; |
|||
} |
|||
|
|||
} // namespace utility
|
|||
|
|||
} // namespace storm
|
|||
|
|||
|
|||
@ -0,0 +1,63 @@ |
|||
/* |
|||
* CuddUtility.h |
|||
* |
|||
* Created on: 26.01.2013 |
|||
* Author: Christian Dehnert |
|||
*/ |
|||
|
|||
#ifndef STORM_UTILITY_CUDDUTILITY_H_ |
|||
#define STORM_UTILITY_CUDDUTILITY_H_ |
|||
|
|||
#include "cuddObj.hh" |
|||
|
|||
namespace storm { |
|||
|
|||
namespace utility { |
|||
|
|||
class CuddUtility { |
|||
public: |
|||
~CuddUtility() { |
|||
for (auto element : allDecisionDiagramVariables) { |
|||
delete element; |
|||
} |
|||
} |
|||
|
|||
ADD* getNewAddVariable(); |
|||
ADD* getAddVariable(int index) const; |
|||
|
|||
ADD* getOne() const; |
|||
ADD* getZero() const; |
|||
|
|||
ADD* getConstantEncoding(uint_fast64_t constant, std::vector<ADD*> const& variables) const; |
|||
|
|||
void setValueAtIndex(ADD* add, uint_fast64_t index, std::vector<ADD*> const& variables, double value) const; |
|||
void setValueAtIndices(ADD* add, uint_fast64_t rowIndex, uint_fast64_t columnIndex, std::vector<ADD*> const& rowVariables, std::vector<ADD*> const& columnVariables, double value) const; |
|||
|
|||
ADD* getConstant(double value) const; |
|||
|
|||
ADD* permuteVariables(ADD* add, std::vector<ADD*> fromVariables, std::vector<ADD*> toVariables, uint_fast64_t totalNumberOfVariables) const; |
|||
|
|||
void dumpDotToFile(ADD* add, std::string filename) const; |
|||
|
|||
Cudd const& getManager() const; |
|||
|
|||
friend CuddUtility* cuddUtilityInstance(); |
|||
|
|||
private: |
|||
CuddUtility() : manager(), allDecisionDiagramVariables() { |
|||
|
|||
} |
|||
|
|||
Cudd manager; |
|||
std::vector<ADD*> allDecisionDiagramVariables; |
|||
|
|||
static CuddUtility* instance; |
|||
}; |
|||
|
|||
CuddUtility* cuddUtilityInstance(); |
|||
|
|||
} // namespace utility |
|||
|
|||
} // namespace storm |
|||
|
|||
#endif /* STORM_UTILITY_CUDDUTILITY_H_ */ |
|||
@ -0,0 +1,32 @@ |
|||
#include "gtest/gtest.h"
|
|||
#include "storm-config.h"
|
|||
#include "src/parser/PrismParser.h"
|
|||
#include "src/utility/IoUtility.h"
|
|||
#include "src/ir/Program.h"
|
|||
#include "src/adapters/ExplicitModelAdapter.h"
|
|||
#include "src/models/Mdp.h"
|
|||
|
|||
TEST(ParsePrismTest, parseCrowds5_5) { |
|||
storm::parser::PrismParser parser; |
|||
storm::ir::Program program; |
|||
ASSERT_NO_THROW(program = parser.parseFile("examples/dtmc/crowds/crowds5_5.pm")); |
|||
storm::adapters::ExplicitModelAdapter adapter(program); |
|||
|
|||
std::shared_ptr<storm::models::Dtmc<double>> model = adapter.getModel()->as<storm::models::Dtmc<double>>(); |
|||
|
|||
ASSERT_EQ(model->getNumberOfStates(), (uint_fast64_t)8607); |
|||
ASSERT_EQ(model->getNumberOfTransitions(), (uint_fast64_t)15113); |
|||
} |
|||
|
|||
TEST(ParsePrismTest, parseTwoDice) { |
|||
storm::parser::PrismParser parser; |
|||
storm::ir::Program program; |
|||
ASSERT_NO_THROW(program = parser.parseFile("examples/mdp/two_dice/two_dice.nm")); |
|||
storm::adapters::ExplicitModelAdapter adapter(program); |
|||
|
|||
std::shared_ptr<storm::models::Mdp<double>> model = adapter.getModel()->as<storm::models::Mdp<double>>(); |
|||
|
|||
ASSERT_EQ(model->getNumberOfStates(), (uint_fast64_t)169); |
|||
ASSERT_EQ(model->getNumberOfChoices(), (uint_fast64_t)254); |
|||
ASSERT_EQ(model->getNumberOfTransitions(), (uint_fast64_t)436); |
|||
} |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue