diff --git a/src/storage/ppg/ProgramAction.cpp b/src/storage/ppg/ProgramAction.cpp
new file mode 100644
index 000000000..9f3d8a66f
--- /dev/null
+++ b/src/storage/ppg/ProgramAction.cpp
@@ -0,0 +1,15 @@
+#include "ProgramAction.h"
+#include "ProgramGraph.h"
+
+namespace storm {
+ namespace ppg {
+
+ ProbabilisticProgramAction::ProbabilisticProgramAction(ProgramGraph* graph, ProgramActionIdentifier actId, int64_t from, int64_t to) : ProgramAction(graph, actId) {
+ assert(from <= to);
+ storm::expressions::Expression prob = graph->getExpressionManager()->integer(1) / graph->getExpressionManager()->integer(to - from + 1);
+ for(int64_t i = from; i <= to; ++i) {
+ values.emplace_back(i, prob);
+ }
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/storage/ppg/ProgramAction.h b/src/storage/ppg/ProgramAction.h
new file mode 100644
index 000000000..5b44030ff
--- /dev/null
+++ b/src/storage/ppg/ProgramAction.h
@@ -0,0 +1,158 @@
+#pragma once
+#include "defines.h"
+#include "src/storage/expressions/Expression.h"
+#include "src/storage/expressions/Variable.h"
+#include "src/storage/expressions/ExpressionManager.h"
+
+namespace storm {
+ namespace ppg {
+
+ class ProgramAction {
+ public:
+ ProgramAction(ProgramGraph* graph, ProgramActionIdentifier id) : graph(graph), actId(id) {
+
+ }
+
+ ProgramActionIdentifier id() const {
+ return actId;
+ }
+
+ ProgramGraph const& getProgramGraph() const {
+ return *graph;
+ }
+
+ virtual bool isProbabilistic() const = 0;
+ private:
+ ProgramGraph* graph;
+ ProgramActionIdentifier actId;
+ };
+
+
+ struct ValueProbabilityPair {
+ ValueProbabilityPair(int64_t value, storm::expressions::Expression const& probability) : value(value), probability(probability) {
+ // Intentionally left empty.
+ }
+
+ int64_t value;
+ storm::expressions::Expression probability;
+ };
+
+ class ProbabilisticProgramAction : public ProgramAction {
+ public:
+ // TODO in the long run, we probably need own iterators for this.
+ using iterator = std::vector<ValueProbabilityPair>::iterator;
+ using const_iterator = std::vector<ValueProbabilityPair>::const_iterator;
+
+
+
+ /**
+ * Constructs a uniform assignment operation to a variable;
+ * Action assigns a variable according to a uniform distribution [from, to]
+ */
+ ProbabilisticProgramAction(ProgramGraph* graph, ProgramActionIdentifier actId, int64_t from, int64_t to);
+
+ bool isProbabilistic() const override{
+ return true;
+ }
+
+ iterator begin() {
+ return values.begin();
+ }
+
+ iterator end() {
+ return values.end();
+ }
+
+ const_iterator begin() const {
+ return values.begin();
+ }
+
+ const_iterator end() const {
+ return values.end();
+ }
+
+ private:
+ // TODO not the smartest representation (but at least it is internal!)
+ std::vector<ValueProbabilityPair> values;
+
+ };
+
+
+ struct AssignmentGroup {
+ using iterator = std::unordered_map<uint64_t, storm::expressions::Expression>::iterator;
+ using const_iterator = std::unordered_map<uint64_t, storm::expressions::Expression>::const_iterator;
+
+ storm::expressions::Expression& operator[](uint64_t varIndex) {
+ return map[varIndex];
+ }
+
+ bool hasVariable(uint64_t varIndex) const {
+ return map.count(varIndex) > 0;
+ }
+
+ iterator begin() {
+ return map.begin();
+ }
+
+ iterator end() {
+ return map.end();
+ }
+
+ const_iterator begin() const {
+ return map.begin();
+ }
+
+ const_iterator end() const {
+ return map.end();
+ }
+
+ private:
+ std::unordered_map<uint64_t, storm::expressions::Expression> map;
+ };
+
+ class DeterministicProgramAction : public ProgramAction {
+
+ public:
+ using iterator = std::vector<AssignmentGroup>::iterator;
+ using const_iterator = std::vector<AssignmentGroup>::const_iterator;
+
+ DeterministicProgramAction(ProgramGraph* graph, ProgramActionIdentifier actId) : ProgramAction(graph, actId) {
+
+ }
+
+
+
+ void addAssignment(uint64_t varIndex, storm::expressions::Expression const& expr, uint64_t level=0) {
+ if(assignments.size() <= level) {
+ assignments.resize(level+1);
+ }
+ assert(!assignments[level].hasVariable(varIndex));
+ assignments[level][varIndex] = expr;
+ }
+
+ iterator begin() {
+ return assignments.begin();
+ }
+
+ iterator end() {
+ return assignments.end();
+ }
+
+ const_iterator begin() const {
+ return assignments.begin();
+ }
+
+ const_iterator end() const {
+ return assignments.end();
+ }
+
+ bool isProbabilistic() const override{
+ return false;
+ }
+
+ protected:
+ std::vector<AssignmentGroup> assignments;
+ };
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/ppg/ProgramEdge.cpp b/src/storage/ppg/ProgramEdge.cpp
index 608da964d..4b5647d34 100644
--- a/src/storage/ppg/ProgramEdge.cpp
+++ b/src/storage/ppg/ProgramEdge.cpp
@@ -1,9 +1,11 @@
-//
-// ProgramEdge.cpp
-// storm
-//
-// Created by Sebastian Junges on 09/09/16.
-//
-//
-
#include "ProgramEdge.h"
+#include "ProgramGraph.h"
+
+namespace storm {
+ namespace ppg {
+
+ ProgramAction const& ProgramEdge::getAction() const {
+ return group->getGraph().getAction(action);
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/storage/ppg/ProgramEdge.h b/src/storage/ppg/ProgramEdge.h
index fa9d3b3db..0cbef21a9 100644
--- a/src/storage/ppg/ProgramEdge.h
+++ b/src/storage/ppg/ProgramEdge.h
@@ -5,6 +5,8 @@
namespace storm {
namespace ppg {
+ class ProgramAction;
+
class ProgramEdge {
public:
ProgramEdge(ProgramEdgeGroup* group, ProgramEdgeIdentifier id, ProgramActionIdentifier action, storm::expressions::Expression const& condition, ProgramLocationIdentifier targetId)
@@ -13,6 +15,17 @@ namespace storm {
// Intentionally left empty.
}
+
+ ProgramLocationIdentifier getTargetId() const {
+ return target;
+ }
+
+ storm::expressions::Expression const& getCondition() const {
+ return condition;
+ }
+
+ ProgramAction const& getAction() const;
+
virtual ~ProgramEdge() {
// Intentionally left empty.
}
diff --git a/src/storage/ppg/ProgramEdgeGroup.h b/src/storage/ppg/ProgramEdgeGroup.h
index 0c215de31..9736c658f 100644
--- a/src/storage/ppg/ProgramEdgeGroup.h
+++ b/src/storage/ppg/ProgramEdgeGroup.h
@@ -8,6 +8,8 @@ namespace storm {
class ProgramEdgeGroup {
public:
+ using const_iterator = std::vector<ProgramEdge*>::const_iterator;
+
ProgramEdgeGroup(ProgramGraph* graph, ProgramEdgeGroupIdentifier id, ProgramLocationIdentifier sourceId, storm::expressions::Expression const& probability)
: graph(graph), groupId(id), sourceId(sourceId), probability(probability)
{
@@ -31,6 +33,26 @@ namespace storm {
return edges.back();
}
+ const_iterator begin() const {
+ return edges.begin();
+ }
+
+ const_iterator end() const {
+ return edges.end();
+ }
+
+ size_t nrEdges() const {
+ return edges.size();
+ }
+
+ storm::expressions::Expression const& getProbability() const {
+ return probability;
+ }
+
+ ProgramGraph const& getGraph() const {
+ return *graph;
+ }
+
private:
/// Pointer to the graph; not owned.
ProgramGraph* graph;
diff --git a/src/storage/ppg/ProgramGraph.h b/src/storage/ppg/ProgramGraph.h
index 0dec3e610..7dc505298 100644
--- a/src/storage/ppg/ProgramGraph.h
+++ b/src/storage/ppg/ProgramGraph.h
@@ -8,19 +8,10 @@
#include "ProgramLocation.h"
#include "ProgramEdge.h"
#include "ProgramEdgeGroup.h"
+#include "ProgramAction.h"
namespace storm {
namespace ppg {
- struct ProgramAction {
- ProgramAction(ProgramGraph* graph, ProgramActionIdentifier actId) : graph(graph), actId(actId) {
-
- }
-
- ProgramGraph* graph;
- ProgramActionIdentifier actId;
- };
-
-
/**
* Program graph as based on Principles of Model Checking, Def 2.13
* Action effects are part of the action.
@@ -34,15 +25,15 @@ namespace storm {
}
+ ProgramGraph(ProgramGraph const&) = delete;
+
virtual ~ProgramGraph() {
- std::cout << "remove graph" << std::endl;
}
- ProgramActionIdentifier addAction() {
+ DeterministicProgramAction* addDeterministicAction() {
ProgramActionIdentifier newId = freeActionIndex();
assert(!hasAction(newId));
- actions.emplace(newId, ProgramAction(this, newId));
- return newId;
+ return &(deterministicActions.emplace(newId, DeterministicProgramAction(this, newId)).first->second);
}
ProgramLocation* addLocation(bool isInitial = false) {
@@ -101,12 +92,51 @@ namespace storm {
}
+ ProgramVariableIdentifier getVariableId(std::string const& varName) const {
+ // TODO consider holding a map for this.
+ uint64_t res = 0;
+ for(auto const& v : variables) {
+ if(v.getName() == varName) {
+ return res;
+ }
+ ++res;
+ }
+ assert(false);
+ }
+
+ std::string const& getVariableName(ProgramVariableIdentifier id) const {
+ return variables.at(id).getName();
+ }
+
+ bool hasVariable(std::string const& varName) const {
+ for(auto const& v : variables) {
+ if(v.getName() == varName) {
+ return true;
+ }
+ }
+ return false;
+ }
+
bool hasLocation(ProgramLocationIdentifier id) const {
return locations.count(id) == 1;
}
bool hasAction(ProgramActionIdentifier id) const {
- return actions.count(id) == 1;
+ return deterministicActions.count(id) == 1 || probabilisticActions.count(id);
+ }
+
+ ProgramAction const& getAction(ProgramActionIdentifier id) const {
+ assert(hasAction(id));
+ if(isDeterministicAction(id)) {
+ return deterministicActions.at(id);
+ } else {
+ return probabilisticActions.at(id);
+ }
+ }
+
+ bool isDeterministicAction(ProgramActionIdentifier id) const {
+ assert(hasAction(id));
+ return probabilisticActions.count(id) == 0;
}
size_t nrLocations() const {
@@ -117,6 +147,10 @@ namespace storm {
return variables.size();
}
+ size_t nrActions() const {
+ return variables.size();
+ }
+
ConstLocationIterator locationBegin() const {
return locations.begin();
@@ -141,6 +175,7 @@ namespace storm {
void printInfo(std::ostream& os) const {
os << "Number of variables: " << nrVariables() << std::endl;
os << "Number of locations: " << nrLocations() << std::endl;
+ os << "Number of actions: " << nrActions() << std::endl;
}
protected:
@@ -168,7 +203,8 @@ namespace storm {
return newEdgeGroupId++;
}
- std::unordered_map<ProgramActionIdentifier, ProgramAction> actions;
+ std::unordered_map<ProgramActionIdentifier, DeterministicProgramAction> deterministicActions;
+ std::unordered_map<ProgramActionIdentifier, ProbabilisticProgramAction> probabilisticActions;
std::unordered_map<ProgramLocationIdentifier, ProgramLocation> locations;
storm::expressions::Expression initialValueRestriction;
std::vector<storm::expressions::Variable> variables;
diff --git a/src/storage/ppg/ProgramLocation.h b/src/storage/ppg/ProgramLocation.h
index 8efde84c8..e88f0e85d 100644
--- a/src/storage/ppg/ProgramLocation.h
+++ b/src/storage/ppg/ProgramLocation.h
@@ -8,6 +8,7 @@ namespace storm {
class ProgramLocation {
public:
using EdgeGroupIterator = std::vector<ProgramEdgeGroup*>::iterator;
+ using const_iterator = std::vector<ProgramEdgeGroup*>::const_iterator;
ProgramLocation(ProgramGraph* graph, ProgramLocationIdentifier id, bool initial) : graph(graph), locId(id), init(initial){
// Intentionally left empty
@@ -38,10 +39,27 @@ namespace storm {
return edgeGroups.size();
}
+ bool hasNonDeterminism() const {
+ for(auto const& eg : edgeGroups) {
+ if(eg->nrEdges() > 1) return true;
+ }
+ return false;
+ }
+
+ const_iterator begin() const {
+ return edgeGroups.begin();
+ }
+
+ const_iterator end() const {
+ return edgeGroups.end();
+ }
+
+ // Todo rename?
EdgeGroupIterator getOutgoingEdgeGroupBegin() {
return edgeGroups.begin();
}
+ // Todo rename?
EdgeGroupIterator getOutgoingEdgeGroupEnd() {
return edgeGroups.end();
}
diff --git a/src/storage/ppg/defines.h b/src/storage/ppg/defines.h
index 6f64e9cfe..548160ba9 100644
--- a/src/storage/ppg/defines.h
+++ b/src/storage/ppg/defines.h
@@ -10,6 +10,7 @@ namespace storm {
using ProgramActionIdentifier = uint64_t;
using ProgramEdgeGroupIdentifier = uint64_t;
using ProgramEdgeIdentifier = uint64_t;
+ using ProgramVariableIdentifier = uint64_t;
}
}
\ No newline at end of file