sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

builders from pgcl to jani updated 

Former-commit-id: 0b75386a0e [formerly 29325b187e]
Former-commit-id: 99014d9b0e
tempestpy_adaptions
sjunges 8 years ago
parent
b3204a178a
commit
c06ae6528c
4 changed files with 113 additions and 15 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 62
      src/builder/JaniProgramGraphBuilder.cpp
  2. 36
      src/builder/JaniProgramGraphBuilder.h
  3. 13
      src/builder/ProgramGraphBuilder.cpp
  4. 17
      src/builder/ProgramGraphBuilder.h

62
src/builder/JaniProgramGraphBuilder.cpp
View File

@ -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);
}
}
}
}
}
}

36
src/builder/JaniProgramGraphBuilder.h
View File

@ -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;
};
}
}

13
src/builder/ProgramGraphBuilder.cpp
View File

@ -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());
}
}

17
src/builder/ProgramGraphBuilder.h
View File

@ -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();
}

Write Preview
Loading…
Cancel
Save