From c06ae6528c47f6f5a089f4a55d98c1fa3ca94cb7 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Sat, 17 Sep 2016 13:49:18 +0200
Subject: [PATCH] builders from pgcl to jani updated
Former-commit-id: 0b75386a0e84783e92f420f461dc332cb4cc67b3 [formerly 29325b187e782ab910b80fa37b42d6b1c373a49e]
Former-commit-id: 99014d9b0ed6c98fd76cd044bb9b9054e5c1a6cd
---
src/builder/JaniProgramGraphBuilder.cpp | 62 +++++++++++++++++++++++++
src/builder/JaniProgramGraphBuilder.h | 36 ++++++++++++--
src/builder/ProgramGraphBuilder.cpp | 13 ++++--
src/builder/ProgramGraphBuilder.h | 17 ++++---
4 files changed, 113 insertions(+), 15 deletions(-)
diff --git a/src/builder/JaniProgramGraphBuilder.cpp b/src/builder/JaniProgramGraphBuilder.cpp
index 7ec2e1fb5..5ce712093 100644
--- a/src/builder/JaniProgramGraphBuilder.cpp
+++ b/src/builder/JaniProgramGraphBuilder.cpp
@@ -3,5 +3,67 @@
namespace storm {
namespace builder {
unsigned JaniProgramGraphBuilder::janiVersion = 1;
+
+ storm::jani::OrderedAssignments buildOrderedAssignments(storm::jani::Automaton& automaton, storm::ppg::DeterministicProgramAction const& act) {
+ std::vector<storm::jani::Assignment> vec;
+ uint64_t level = 0;
+ for(auto const& group : act) {
+ for(auto const& assignment : group) {
+ vec.emplace_back(automaton.getVariables().getVariable(act.getProgramGraph().getVariableName(assignment.first)) , assignment.second, level);
+ }
+ ++level;
+ }
+ return storm::jani::OrderedAssignments(vec);
+ }
+
+ std::vector<storm::jani::EdgeDestination> buildProbabilisticDestinations(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge ) {
+ storm::ppg::ProbabilisticProgramAction const& act = static_cast<storm::ppg::ProbabilisticProgramAction const&>(edge.getAction());
+ std::vector<storm::jani::EdgeDestination> vec;
+ //for(auto const& value : act ) {
+ // vec.emplace_back(
+ //}
+ return vec;
+ }
+
+ std::vector<storm::jani::EdgeDestination> JaniProgramGraphBuilder::buildDestinations(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge ) {
+ if (edge.getAction().isProbabilistic()) {
+ return buildProbabilisticDestinations(automaton, edge);
+ } else {
+ storm::jani::OrderedAssignments oa = buildOrderedAssignments(automaton, static_cast<storm::ppg::DeterministicProgramAction const&>(edge.getAction()));
+ storm::jani::EdgeDestination dest(edge.getTargetId(), expManager->rational(1.0), oa);
+ return {dest};
+ }
+ }
+
+
+
+ void JaniProgramGraphBuilder::addEdges(storm::jani::Automaton& automaton, storm::ppg::ProgramGraph const& pg, std::map<storm::ppg::ProgramLocationIdentifier, uint64_t> const& janiLocId) {
+ for(auto it = pg.locationBegin(); it != pg.locationEnd(); ++it) {
+ ppg::ProgramLocation const& loc = it->second;
+ if(loc.nrOutgoingEdgeGroups() == 1) {
+ for(auto const& edge : **(loc.begin())) {
+ storm::jani::Edge e(janiLocId.at(loc.id()), storm::jani::Model::silentActionIndex, boost::none, edge->getCondition(), buildDestinations(automaton, *edge));
+ automaton.addEdge(e);
+ }
+ } else {
+ if(loc.hasNonDeterminism())
+ {
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Combi of nondeterminism and probabilistic choices within a loc not supported yet");
+ } else {
+ std::vector<storm::jani::EdgeDestination> destinations;
+ for(auto const& eg : loc) {
+ // TODO add assignments
+ assert(eg->nrEdges() < 2); // Otherwise, non-determinism occurs.
+ assert(eg->nrEdges() > 0); // Empty edge groups should not occur in input.
+ uint64_t target = janiLocId.at((*eg->begin())->getTargetId());
+ destinations.emplace_back(target, eg->getProbability());
+ }
+ storm::jani::Edge e(janiLocId.at(it->second.id()), storm::jani::Model::silentActionIndex, boost::none, expManager->boolean(true), destinations);
+ automaton.addEdge(e);
+ }
+ }
+ }
+ }
+
}
}
\ No newline at end of file
diff --git a/src/builder/JaniProgramGraphBuilder.h b/src/builder/JaniProgramGraphBuilder.h
index 01f392e47..c45b91a00 100644
--- a/src/builder/JaniProgramGraphBuilder.h
+++ b/src/builder/JaniProgramGraphBuilder.h
@@ -1,8 +1,13 @@
+#include <string>
+
#include "src/storage/ppg/ProgramGraph.h"
#include "src/storage/jani/Model.h"
#include "src/storage/jani/Location.h"
+#include "src/storage/jani/EdgeDestination.h"
#include "src/storage/IntegerInterval.h"
+#include "src/exceptions/NotSupportedException.h"
+#include "src/utility/macros.h"
namespace storm {
namespace builder {
@@ -34,33 +39,54 @@ namespace storm {
storm::jani::Model* model = new storm::jani::Model(name, storm::jani::ModelType::MDP, janiVersion, expManager);
storm::jani::Automaton mainAutomaton("main");
addProcedureVariables(mainAutomaton, pg);
- addProcedureLocations(mainAutomaton, pg);
+ auto janiLocs = addProcedureLocations(mainAutomaton, pg);
+ addEdges(mainAutomaton, pg, janiLocs);
model->addAutomaton(mainAutomaton);
+ model->setStandardSystemComposition();
return model;
}
private:
+ std::string janiLocationName(storm::ppg::ProgramLocationIdentifier i) {
+ return "l" + std::to_string(i);
+ }
+
+
+
+ void addEdges(storm::jani::Automaton& automaton, storm::ppg::ProgramGraph const& pg, std::map<storm::ppg::ProgramLocationIdentifier, uint64_t> const& janiLocId);
+ std::vector<storm::jani::EdgeDestination> buildDestinations(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge );
+
+
void addProcedureVariables(storm::jani::Automaton& automaton, storm::ppg::ProgramGraph const& pg) {
for (auto const& v : pg.getVariables()) {
if(variableRestrictions.count(v.getIndex())) {
assert(false);
} else {
storm::jani::UnboundedIntegerVariable janiVar(v.getName(), v, expManager->integer(0), false);
- automaton.addUnboundedIntegerVariable(janiVar);
+ automaton.addVariable(janiVar);
}
}
}
- void addProcedureLocations(storm::jani::Automaton& automaton, storm::ppg::ProgramGraph const& pg) {
+ std::map<storm::ppg::ProgramLocationIdentifier, uint64_t> addProcedureLocations(storm::jani::Automaton& automaton, storm::ppg::ProgramGraph const& pg) {
+ std::map<storm::ppg::ProgramLocationIdentifier, uint64_t> result;
for(auto it = pg.locationBegin(); it != pg.locationEnd(); ++it) {
- storm::jani::Location janiLoc(std::to_string(it->second.id()));
- automaton.addLocation(janiLoc);
+ storm::jani::Location janiLoc(janiLocationName(it->second.id()));
+ result[it->second.id()] = automaton.addLocation(janiLoc);
+ if(it->second.isInitial()) {
+ automaton.addInitialLocation(result[it->second.id()]);
+ }
}
+ return result;
}
+ /// Restrictions on variables
std::map<uint64_t, storm::storage::IntegerInterval> variableRestrictions;
+ /// The expression manager
std::shared_ptr<storm::expressions::ExpressionManager> expManager;
+
+
};
}
}
\ No newline at end of file
diff --git a/src/builder/ProgramGraphBuilder.cpp b/src/builder/ProgramGraphBuilder.cpp
index 02aa89c12..269c611db 100644
--- a/src/builder/ProgramGraphBuilder.cpp
+++ b/src/builder/ProgramGraphBuilder.cpp
@@ -1,4 +1,5 @@
#include "ProgramGraphBuilder.h"
+#include "src/storage/pgcl/AssignmentStatement.h"
#include "src/storage/pgcl/ObserveStatement.h"
#include "src/storage/pgcl/LoopStatement.h"
#include "src/storage/pgcl/IfStatement.h"
@@ -9,8 +10,12 @@
namespace storm {
namespace builder {
void ProgramGraphBuilderVisitor::visit(storm::pgcl::AssignmentStatement const& s) {
- builder.currentLoc()->addProgramEdgeToAllGroups(builder.getAction(), builder.nextLocId());
-
+ if(s.isDeterministic()) {
+ builder.currentLoc()->addProgramEdgeToAllGroups(builder.addAction(s.getVariable(), boost::get<storm::expressions::Expression>(s.getExpression())), builder.nextLocId());
+ } else {
+ builder.currentLoc()->addProgramEdgeToAllGroups(builder.addAction(s.getVariable(), builder.getExpressionManager()->integer(2)), builder.nextLocId());
+
+ }
}
void ProgramGraphBuilderVisitor::visit(storm::pgcl::ObserveStatement const& s) {
builder.currentLoc()->addProgramEdgeToAllGroups(builder.noAction(), s.getCondition().getBooleanExpression(), builder.nextLocId());
@@ -58,11 +63,11 @@ namespace storm {
storm::ppg::ProgramLocation* beforeStatementLocation = builder.currentLoc();
builder.storeNextLocation(builder.nextLoc());
storm::ppg::ProgramLocation* bodyStart = builder.newLocation();
- beforeStatementLocation->addProgramEdgeGroup(s.getProbability());
+ beforeStatementLocation->addProgramEdgeGroup(s.getProbability())->addEdge(builder.nextLocId(), builder.noAction());
builder.buildBlock(*s.getLeftBranch());
builder.storeNextLocation(builder.nextLoc());
bodyStart = builder.newLocation();
- beforeStatementLocation->addProgramEdgeGroup(1 - s.getProbability());
+ beforeStatementLocation->addProgramEdgeGroup(1 - s.getProbability())->addEdge(builder.nextLocId(), builder.noAction());
builder.buildBlock(*s.getRightBranch());
}
}
diff --git a/src/builder/ProgramGraphBuilder.h b/src/builder/ProgramGraphBuilder.h
index 5cc61ada9..c92c50596 100644
--- a/src/builder/ProgramGraphBuilder.h
+++ b/src/builder/ProgramGraphBuilder.h
@@ -39,7 +39,7 @@ namespace storm {
~ProgramGraphBuilder() {
if(graph != nullptr) {
- // delete graph;
+ delete graph;
}
}
@@ -52,7 +52,7 @@ namespace storm {
return currentLoc();
}
- storm::ppg::ProgramLocation* storeNextLocation(storm::ppg::ProgramLocation* loc) {
+ void storeNextLocation(storm::ppg::ProgramLocation* loc) {
nextStack.push_back(loc);
}
@@ -64,18 +64,23 @@ namespace storm {
return nextLoc()->id();
}
- storm::ppg::ProgramActionIdentifier getAction() const {
- return graph->addAction();
+ storm::ppg::ProgramActionIdentifier addAction(storm::expressions::Variable const& var, storm::expressions::Expression const& expr) const {
+ storm::ppg::DeterministicProgramAction* action = graph->addDeterministicAction();
+ action->addAssignment(graph->getVariableId(var.getName()), expr);
+ return action->id();
}
storm::ppg::ProgramActionIdentifier noAction() const {
return noActionId;
}
+ std::shared_ptr<storm::expressions::ExpressionManager> const& getExpressionManager() const {
+ return program.getExpressionManager();
+ }
+
void buildBlock(storm::pgcl::PgclBlock const& block) {
-
ProgramGraphBuilderVisitor visitor(*this);
for(auto const& statement : block) {
std::cout << "Statement " << statement->getLocationNumber() << std::endl;
@@ -98,7 +103,7 @@ namespace storm {
: program(program)
{
graph = new storm::ppg::ProgramGraph(program.getExpressionManager(), program.getVariables());
- noActionId = getAction();
+ noActionId = graph->addDeterministicAction()->id();
}