diff --git a/src/builder/JaniProgramGraphBuilder.cpp b/src/builder/JaniProgramGraphBuilder.cpp index 5ce712093..1549b4988 100644 --- a/src/builder/JaniProgramGraphBuilder.cpp +++ b/src/builder/JaniProgramGraphBuilder.cpp @@ -1,4 +1,5 @@ #include "JaniProgramGraphBuilder.h" +#include "src/storage/jani/EdgeDestination.h" namespace storm { namespace builder { @@ -16,12 +17,13 @@ namespace storm { return storm::jani::OrderedAssignments(vec); } - std::vector buildProbabilisticDestinations(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge ) { + std::vector JaniProgramGraphBuilder::buildProbabilisticDestinations(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge ) { storm::ppg::ProbabilisticProgramAction const& act = static_cast(edge.getAction()); std::vector vec; - //for(auto const& value : act ) { - // vec.emplace_back( - //} + for(auto const& assign : act ) { + storm::jani::Assignment assignment(automaton.getVariables().getVariable(act.getVariableName()), expManager->integer(assign.value) ,0); + vec.emplace_back(janiLocId.at(edge.getTargetId()), assign.probability, assignment); + } return vec; } @@ -30,22 +32,67 @@ namespace storm { return buildProbabilisticDestinations(automaton, edge); } else { storm::jani::OrderedAssignments oa = buildOrderedAssignments(automaton, static_cast(edge.getAction())); - storm::jani::EdgeDestination dest(edge.getTargetId(), expManager->rational(1.0), oa); + storm::jani::EdgeDestination dest(janiLocId.at(edge.getTargetId()), expManager->rational(1.0), oa); return {dest}; } } + storm::expressions::Expression simplifyExpression(storm::expressions::Expression const& in) { + // TODO use bound restrictions etc. + return in.simplify(); + } + std::pair, storm::expressions::Expression> JaniProgramGraphBuilder::addVariableChecks(storm::ppg::ProgramEdge const& edge) { + std::vector edges; + storm::expressions::Expression newGuard; + newGuard = expManager->boolean(true); + if (edge.getAction().isProbabilistic()) { + + } else { + storm::ppg::DeterministicProgramAction const& act = static_cast(edge.getAction()); + STORM_LOG_THROW(act.nrLevels() <= 1, storm::exceptions::NotSupportedException, "Multi-level assignments with user variable bounds not supported"); + for(auto const& group : act) { + for(auto const& assignment : group) { + if (isUserRestricted(assignment.first)) { + assert(variableRestrictions.count(assignment.first) == 1); + storm::storage::IntegerInterval const& bound = variableRestrictions.at(assignment.first); + if (!assignment.second.containsVariables()) { + // Constant assignments can be checked statically. + // TODO we might still want to allow assignments which go out of bounds. + STORM_LOG_THROW(bound.contains(assignment.second.evaluateAsInt()), storm::exceptions::NotSupportedException, "User provided bounds must contain all constant expressions"); + } else { + // TODO currently only fully bounded restrictions are supported; + assert(variableRestrictions.at(assignment.first).hasLeftBound() && variableRestrictions.at(assignment.first).hasRightBound()); + storm::expressions::Expression newCondition = simplifyExpression(edge.getCondition() && (assignment.second > bound.getRightBound().get() || assignment.second < bound.getLeftBound().get())); + storm::jani::EdgeDestination dest(varOutOfBoundsLocations.at(assignment.first), expManager->rational(1.0), storm::jani::OrderedAssignments()); + storm::jani::Edge e(janiLocId.at(edge.getSourceId()), storm::jani::Model::silentActionIndex, boost::none, newCondition, {dest}); + edges.push_back(e); + newGuard = newGuard && assignment.second <= bound.getRightBound().get() && assignment.second >= bound.getLeftBound().get(); + } + } + } + } + } + return {edges, newGuard}; + } - void JaniProgramGraphBuilder::addEdges(storm::jani::Automaton& automaton, storm::ppg::ProgramGraph const& pg, std::map const& janiLocId) { - for(auto it = pg.locationBegin(); it != pg.locationEnd(); ++it) { + + void JaniProgramGraphBuilder::addEdges(storm::jani::Automaton& automaton) { + for(auto it = programGraph.locationBegin(); it != programGraph.locationEnd(); ++it) { ppg::ProgramLocation const& loc = it->second; - if(loc.nrOutgoingEdgeGroups() == 1) { + if (loc.nrOutgoingEdgeGroups() == 0) { + // TODO deadlock! + } else 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)); + std::pair, storm::expressions::Expression> checks = addVariableChecks(*edge); + for(auto const& check : checks.first) { + automaton.addEdge(check); + } + storm::jani::Edge e(janiLocId.at(loc.id()), storm::jani::Model::silentActionIndex, boost::none, simplifyExpression(edge->getCondition() && checks.second), buildDestinations(automaton, *edge)); automaton.addEdge(e); } } else { + // We have probabilistic branching if(loc.hasNonDeterminism()) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Combi of nondeterminism and probabilistic choices within a loc not supported yet"); diff --git a/src/builder/JaniProgramGraphBuilder.h b/src/builder/JaniProgramGraphBuilder.h index c45b91a00..5bbce1d15 100644 --- a/src/builder/JaniProgramGraphBuilder.h +++ b/src/builder/JaniProgramGraphBuilder.h @@ -24,7 +24,7 @@ namespace storm { public: static unsigned janiVersion; - JaniProgramGraphBuilder() { + JaniProgramGraphBuilder(storm::ppg::ProgramGraph const& pg) : programGraph(pg) { } @@ -33,14 +33,20 @@ namespace storm { //} + void restrictAllVariables(int64_t from, int64_t to) { + for (auto const& v : programGraph.getVariables()) { + variableRestrictions.emplace(v.first, storm::storage::IntegerInterval(from, to)); + } + } - storm::jani::Model* build(storm::ppg::ProgramGraph const& pg, std::string const& name = "program_graph") { - expManager = pg.getExpressionManager(); + storm::jani::Model* build(std::string const& name = "program_graph") { + expManager = programGraph.getExpressionManager(); storm::jani::Model* model = new storm::jani::Model(name, storm::jani::ModelType::MDP, janiVersion, expManager); storm::jani::Automaton mainAutomaton("main"); - addProcedureVariables(mainAutomaton, pg); - auto janiLocs = addProcedureLocations(mainAutomaton, pg); - addEdges(mainAutomaton, pg, janiLocs); + addProcedureVariables(mainAutomaton); + janiLocId = addProcedureLocations(mainAutomaton); + addVariableOoBLocations(mainAutomaton); + addEdges(mainAutomaton); model->addAutomaton(mainAutomaton); model->setStandardSystemComposition(); return model; @@ -51,40 +57,77 @@ namespace storm { return "l" + std::to_string(i); } + std::string janiVariableOutOfBoundsLocationName(storm::ppg::ProgramVariableIdentifier i) { + return "oob-" + programGraph.getVariableName(i); + } - void addEdges(storm::jani::Automaton& automaton, storm::ppg::ProgramGraph const& pg, std::map const& janiLocId); + void addEdges(storm::jani::Automaton& automaton); std::vector buildDestinations(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge ); - + /** + * Helper for probabilistic assignments + */ + std::vector buildProbabilisticDestinations(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge ); + + std::pair, storm::expressions::Expression> addVariableChecks(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); + bool isUserRestricted(storm::ppg::ProgramVariableIdentifier i) { + return variableRestrictions.count(i) == 1; + } + + void addProcedureVariables(storm::jani::Automaton& automaton) { + for (auto const& v : programGraph.getVariables()) { + if(variableRestrictions.count(v.first) == 1) { + storm::storage::IntegerInterval const& bounds = variableRestrictions.at(v.first); + if (bounds.hasLeftBound()) { + if (bounds.hasRightBound()) { + storm::jani::BoundedIntegerVariable janiVar(v.second.getName(), v.second, expManager->integer(0), false, expManager->integer(bounds.getLeftBound().get()), expManager->integer(bounds.getRightBound().get())); + automaton.addVariable(janiVar); + } else { + // Not yet supported. + assert(false); + } + } else { + // Not yet supported. + assert(false); + } } else { - storm::jani::UnboundedIntegerVariable janiVar(v.getName(), v, expManager->integer(0), false); + storm::jani::UnboundedIntegerVariable janiVar(v.second.getName(), v.second, expManager->integer(0), false); automaton.addVariable(janiVar); } } } - std::map addProcedureLocations(storm::jani::Automaton& automaton, storm::ppg::ProgramGraph const& pg) { + std::map addProcedureLocations(storm::jani::Automaton& automaton) { std::map result; - for(auto it = pg.locationBegin(); it != pg.locationEnd(); ++it) { + for (auto it = programGraph.locationBegin(); it != programGraph.locationEnd(); ++it) { storm::jani::Location janiLoc(janiLocationName(it->second.id())); result[it->second.id()] = automaton.addLocation(janiLoc); - if(it->second.isInitial()) { + if (it->second.isInitial()) { automaton.addInitialLocation(result[it->second.id()]); } } return result; } + void addVariableOoBLocations(storm::jani::Automaton& automaton) { + for(auto const& restr : variableRestrictions) { + storm::jani::Location janiLoc(janiVariableOutOfBoundsLocationName(restr.first)); + uint64_t locId = automaton.addLocation(janiLoc); + varOutOfBoundsLocations[restr.first] = locId; + + } + } + /// Restrictions on variables std::map variableRestrictions; + /// Locations for variables that would have gone ot o + std::map varOutOfBoundsLocations; + std::map janiLocId; /// The expression manager std::shared_ptr expManager; - + /// The program graph to be translated + storm::ppg::ProgramGraph const& programGraph; }; diff --git a/src/builder/ProgramGraphBuilder.cpp b/src/builder/ProgramGraphBuilder.cpp index 269c611db..c23276168 100644 --- a/src/builder/ProgramGraphBuilder.cpp +++ b/src/builder/ProgramGraphBuilder.cpp @@ -13,7 +13,7 @@ namespace storm { if(s.isDeterministic()) { builder.currentLoc()->addProgramEdgeToAllGroups(builder.addAction(s.getVariable(), boost::get(s.getExpression())), builder.nextLocId()); } else { - builder.currentLoc()->addProgramEdgeToAllGroups(builder.addAction(s.getVariable(), builder.getExpressionManager()->integer(2)), builder.nextLocId()); + builder.currentLoc()->addProgramEdgeToAllGroups(builder.addAction(s.getVariable(), boost::get(s.getExpression())), builder.nextLocId()); } } @@ -24,16 +24,19 @@ namespace storm { storm::expressions::Expression elseCondition; storm::ppg::ProgramLocation* beforeStatementLocation = builder.currentLoc(); builder.storeNextLocation(builder.nextLoc()); - storm::ppg::ProgramLocation* bodyStart = builder.newLocation(); + storm::ppg::ProgramLocation* ifbodyStart = builder.newLocation(); builder.buildBlock(*s.getIfBody()); + storm::ppg::ProgramLocation* elsebodyStart; if(s.hasElse()) { builder.storeNextLocation(builder.nextLoc()); - bodyStart = builder.newLocation(); + elsebodyStart = builder.newLocation(); builder.buildBlock(*s.getElseBody()); } - beforeStatementLocation->addProgramEdgeToAllGroups(builder.noAction(), s.getCondition().getBooleanExpression(), bodyStart->id()); + beforeStatementLocation->addProgramEdgeToAllGroups(builder.noAction(), s.getCondition().getBooleanExpression(), ifbodyStart->id()); + elseCondition = !s.getCondition().getBooleanExpression(); if(s.hasElse()) { - elseCondition = !s.getCondition().getBooleanExpression(); + beforeStatementLocation->addProgramEdgeToAllGroups(builder.noAction(), elseCondition, elsebodyStart->id()); + } else { beforeStatementLocation->addProgramEdgeToAllGroups(builder.noAction(), elseCondition, builder.nextLocId()); } diff --git a/src/builder/ProgramGraphBuilder.h b/src/builder/ProgramGraphBuilder.h index c92c50596..9c856704b 100644 --- a/src/builder/ProgramGraphBuilder.h +++ b/src/builder/ProgramGraphBuilder.h @@ -3,6 +3,7 @@ #include "src/storage/pgcl/PgclProgram.h" #include "src/storage/ppg/ProgramGraph.h" #include "src/storage/pgcl/AbstractStatementVisitor.h" +#include "src/storage/pgcl/UniformExpression.h" namespace storm { namespace builder { @@ -38,7 +39,7 @@ namespace storm { } ~ProgramGraphBuilder() { - if(graph != nullptr) { + if (graph != nullptr) { delete graph; } } @@ -70,6 +71,12 @@ namespace storm { return action->id(); } + storm::ppg::ProgramActionIdentifier addAction(storm::expressions::Variable const& var, storm::pgcl::UniformExpression const& expr) const { + storm::ppg::ProbabilisticProgramAction* action = graph->addUniformProbabilisticAction(graph->getVariableId(var.getName()), expr.getBegin(), expr.getEnd()); + return action->id(); + + } + storm::ppg::ProgramActionIdentifier noAction() const { return noActionId; } @@ -82,9 +89,8 @@ namespace storm { void buildBlock(storm::pgcl::PgclBlock const& block) { ProgramGraphBuilderVisitor visitor(*this); - for(auto const& statement : block) { - std::cout << "Statement " << statement->getLocationNumber() << std::endl; - if(!statement->isLast()) { + for (auto const& statement : block) { + if (!statement->isLast()) { nextStack.push_back(graph->addLocation(false)); } assert(!currentStack.empty()); @@ -103,7 +109,7 @@ namespace storm { : program(program) { graph = new storm::ppg::ProgramGraph(program.getExpressionManager(), program.getVariables()); - noActionId = graph->addDeterministicAction()->id(); + noActionId = graph->getNoActionId(); } @@ -112,7 +118,7 @@ namespace storm { // Terminal state. nextStack.push_back(graph->addLocation(false)); // Observe Violated State. - if(program.hasObserve()) { + if (program.hasObserve()) { observeFailedState = graph->addLocation(); } buildBlock(program); diff --git a/src/settings/modules/PGCLSettings.cpp b/src/settings/modules/PGCLSettings.cpp index e8187ced0..051b23375 100644 --- a/src/settings/modules/PGCLSettings.cpp +++ b/src/settings/modules/PGCLSettings.cpp @@ -18,10 +18,17 @@ namespace storm { const std::string PGCLSettings::pgclFileOptionShortName = "pgcl"; const std::string PGCLSettings::pgclToJaniOptionName = "to-jani"; const std::string PGCLSettings::pgclToJaniOptionShortName = "tj"; + const std::string PGCLSettings::programGraphToDotOptionName = "draw-program-graph"; + const std::string PGCLSettings::programGraphToDotShortOptionName = "pg"; + const std::string PGCLSettings::programVariableRestrictionsOptionName = "variable-restrictions"; + const std::string PGCLSettings::programVariableRestrictionShortOptionName = "rvar"; + PGCLSettings::PGCLSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, pgclFileOptionName, false, "Parses the pgcl program.").setShortName(pgclFileOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, pgclToJaniOptionName, false, "Transform to JANI.").setShortName(pgclToJaniOptionShortName).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, programGraphToDotOptionName, false, "Destination for the program graph dot output.").setShortName(programGraphToDotShortOptionName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, programVariableRestrictionsOptionName, false, "Restrictions of program variables").setShortName(programVariableRestrictionShortOptionName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("descriptio", "description of the variable restrictions").build()).build()); } bool PGCLSettings::isPgclFileSet() const { @@ -36,6 +43,22 @@ namespace storm { return this->getOption(pgclToJaniOptionName).getHasOptionBeenSet(); } + bool PGCLSettings::isProgramGraphToDotSet() const { + return this->getOption(programGraphToDotOptionName).getHasOptionBeenSet(); + } + + std::string PGCLSettings::getProgramGraphDotOutputFilename() const { + return this->getOption(programGraphToDotOptionName).getArgumentByName("filename").getValueAsString(); + } + + bool PGCLSettings::isProgramVariableRestrictionSet() const { + return this->getOption(programVariableRestrictionsOptionName).getHasOptionBeenSet(); + } + + std::string PGCLSettings::getProgramVariableRestrictions() const { + return this->getOption(programVariableRestrictionsOptionName).getArgumentByName("description").getValueAsString(); + } + void PGCLSettings::finalize() { } diff --git a/src/settings/modules/PGCLSettings.h b/src/settings/modules/PGCLSettings.h index c894a36a4..fe8bb2b17 100644 --- a/src/settings/modules/PGCLSettings.h +++ b/src/settings/modules/PGCLSettings.h @@ -25,10 +25,31 @@ namespace storm { std::string getPgclFilename() const; /** - * + * Whether the pgcl should be transformed to Jani */ bool isToJaniSet() const; + /** + * Whether the program graph should be drawn (dot output) + */ + bool isProgramGraphToDotSet() const; + + /** + * Destination where to write dot output of the program graph. + */ + std::string getProgramGraphDotOutputFilename() const ; + + /** + * Is program variable restriction string given + */ + bool isProgramVariableRestrictionSet() const; + + /** + * String for program variable restrictions + */ + std::string getProgramVariableRestrictions() const; + + bool check() const override; void finalize() override; @@ -39,6 +60,10 @@ namespace storm { static const std::string pgclFileOptionShortName; static const std::string pgclToJaniOptionName; static const std::string pgclToJaniOptionShortName; + static const std::string programGraphToDotOptionName; + static const std::string programGraphToDotShortOptionName; + static const std::string programVariableRestrictionsOptionName; + static const std::string programVariableRestrictionShortOptionName; }; } diff --git a/src/storage/IntegerInterval.h b/src/storage/IntegerInterval.h index 6f59be238..4459b1569 100644 --- a/src/storage/IntegerInterval.h +++ b/src/storage/IntegerInterval.h @@ -7,33 +7,47 @@ namespace storm { class IntegerInterval { public: - explicit IntegerInterval(uint64_t v) : leftBound(v), rightBound(v) { + explicit IntegerInterval(int64_t v) : leftBound(v), rightBound(v) { } - IntegerInterval(uint64_t lb, uint64_t rb) : leftBound(lb), rightBound(rb) { + IntegerInterval(int64_t lb, int64_t rb) : leftBound(lb), rightBound(rb) { } - bool hasLeftBound() { + bool hasLeftBound() const { return leftBound != boost::none; } - bool hasRightBound() { + bool hasRightBound() const { return rightBound != boost::none; } - boost::optional getLeftBound() { + bool contains(int64_t val) const { + if (hasLeftBound()) { + if (val < leftBound.get()) { + return false; + } + } + if (hasRightBound()) { + if (val > rightBound.get()) { + return false; + } + } + return true; + } + + boost::optional getLeftBound() const { return leftBound; } - boost::optional getRightBound() { + boost::optional getRightBound() const { return rightBound; } private: - boost::optional leftBound; - boost::optional rightBound; + boost::optional leftBound; + boost::optional rightBound; }; diff --git a/src/storage/pgcl/CompoundStatement.h b/src/storage/pgcl/CompoundStatement.h index bc075685c..0dd51a5d4 100755 --- a/src/storage/pgcl/CompoundStatement.h +++ b/src/storage/pgcl/CompoundStatement.h @@ -1,12 +1,4 @@ -/* - * File: CompoundStatement.h - * Author: Lukas Westhofen - * - * Created on 11. April 2015, 17:41 - */ - -#ifndef COMPOUNDSTATEMENT_H -#define COMPOUNDSTATEMENT_H +#pragma once #include "src/storage/pgcl/Statement.h" @@ -27,6 +19,3 @@ namespace storm { }; } } - -#endif /* COMPOUNDSTATEMENT_H */ - diff --git a/src/storage/ppg/ProgramAction.cpp b/src/storage/ppg/ProgramAction.cpp index 9f3d8a66f..6b70607be 100644 --- a/src/storage/ppg/ProgramAction.cpp +++ b/src/storage/ppg/ProgramAction.cpp @@ -4,12 +4,16 @@ namespace storm { namespace ppg { - ProbabilisticProgramAction::ProbabilisticProgramAction(ProgramGraph* graph, ProgramActionIdentifier actId, int64_t from, int64_t to) : ProgramAction(graph, actId) { + ProbabilisticProgramAction::ProbabilisticProgramAction(ProgramGraph* graph, ProgramActionIdentifier actId, ProgramVariableIdentifier var, int64_t from, int64_t to) : ProgramAction(graph, actId), var(var) { 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); } } + + std::string const& ProbabilisticProgramAction::getVariableName() const { + return getProgramGraph().getVariableName(var); + } } } \ No newline at end of file diff --git a/src/storage/ppg/ProgramAction.h b/src/storage/ppg/ProgramAction.h index 5b44030ff..4220a207d 100644 --- a/src/storage/ppg/ProgramAction.h +++ b/src/storage/ppg/ProgramAction.h @@ -49,12 +49,14 @@ namespace storm { * 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); + ProbabilisticProgramAction(ProgramGraph* graph, ProgramActionIdentifier actId, ProgramVariableIdentifier var, int64_t from, int64_t to); bool isProbabilistic() const override{ return true; } + std::string const& getVariableName() const; + iterator begin() { return values.begin(); } @@ -74,6 +76,7 @@ namespace storm { private: // TODO not the smartest representation (but at least it is internal!) std::vector values; + ProgramVariableIdentifier var; }; @@ -107,7 +110,7 @@ namespace storm { } private: - std::unordered_map map; + std::unordered_map map; }; class DeterministicProgramAction : public ProgramAction { @@ -120,9 +123,7 @@ namespace storm { } - - - void addAssignment(uint64_t varIndex, storm::expressions::Expression const& expr, uint64_t level=0) { + void addAssignment(ProgramVariableIdentifier varIndex, storm::expressions::Expression const& expr, uint64_t level=0) { if(assignments.size() <= level) { assignments.resize(level+1); } @@ -130,6 +131,10 @@ namespace storm { assignments[level][varIndex] = expr; } + size_t nrLevels() const { + return assignments.size(); + } + iterator begin() { return assignments.begin(); } diff --git a/src/storage/ppg/ProgramEdge.cpp b/src/storage/ppg/ProgramEdge.cpp index 4b5647d34..e76a2649b 100644 --- a/src/storage/ppg/ProgramEdge.cpp +++ b/src/storage/ppg/ProgramEdge.cpp @@ -4,8 +4,16 @@ namespace storm { namespace ppg { + ProgramLocationIdentifier ProgramEdge::getSourceId() const { + return group->getSourceId(); + } + ProgramAction const& ProgramEdge::getAction() const { return group->getGraph().getAction(action); } + + bool ProgramEdge::hasNoAction() const { + return action == group->getGraph().getNoActionId(); + } } } \ No newline at end of file diff --git a/src/storage/ppg/ProgramEdge.h b/src/storage/ppg/ProgramEdge.h index 0cbef21a9..312e7b224 100644 --- a/src/storage/ppg/ProgramEdge.h +++ b/src/storage/ppg/ProgramEdge.h @@ -15,7 +15,7 @@ namespace storm { // Intentionally left empty. } - + ProgramLocationIdentifier getSourceId() const; ProgramLocationIdentifier getTargetId() const { return target; } @@ -24,7 +24,11 @@ namespace storm { return condition; } + bool hasNoAction() const; ProgramAction const& getAction() const; + ProgramActionIdentifier getActionId() const { + return action; + } virtual ~ProgramEdge() { // Intentionally left empty. diff --git a/src/storage/ppg/ProgramEdgeGroup.h b/src/storage/ppg/ProgramEdgeGroup.h index 9736c658f..235ee694a 100644 --- a/src/storage/ppg/ProgramEdgeGroup.h +++ b/src/storage/ppg/ProgramEdgeGroup.h @@ -53,6 +53,14 @@ namespace storm { return *graph; } + ProgramLocationIdentifier getSourceId() const { + return sourceId; + } + + ProgramEdgeGroupIdentifier getId() const { + return groupId; + } + private: /// Pointer to the graph; not owned. ProgramGraph* graph; diff --git a/src/storage/ppg/ProgramGraph.cpp b/src/storage/ppg/ProgramGraph.cpp index e83667d3b..b6e951aca 100644 --- a/src/storage/ppg/ProgramGraph.cpp +++ b/src/storage/ppg/ProgramGraph.cpp @@ -1,2 +1,48 @@ #include "ProgramGraph.h" + + +namespace storm { + namespace ppg { + void ProgramGraph::printDot(std::ostream& os) const { + os << "digraph ppg {" << std::endl; + + for (auto const& loc : locations) { + os << "\tl" << loc.first << "[label=" << loc.first << "];"<< std::endl; + } + os << std::endl; + for (auto const& loc : locations) { + if (loc.second.nrOutgoingEdgeGroups() > 1) { + for (auto const& edgegroup : loc.second) { + os << "\teg" << edgegroup->getId() << "[shape=circle];"<< std::endl; + } + } + } + os << std::endl; + for (auto const& loc : locations) { + for (auto const& edgegroup : loc.second) { + + if (loc.second.nrOutgoingEdgeGroups() > 1) { + os << "\tl" << loc.first << " -> eg" << edgegroup->getId() << ";" << std::endl; + for (auto const& edge : *edgegroup) { + os << "\teg" << edgegroup->getId() << " -> l" << edge->getTargetId(); + if (!edge->hasNoAction()) { + os << " [label=\"" << edge->getActionId() << "\"]"; + } + os << ";" << std::endl; + } + } else { + for (auto const& edge : *edgegroup) { + os << "\tl" << loc.first << " -> l" << edge->getTargetId(); + if (!edge->hasNoAction()) { + os << " [label=\"" << edge->getActionId() << "\"]"; + } + os << ";" << std::endl; + } + } + } + } + os << "}" << std::endl; + } + } +} \ No newline at end of file diff --git a/src/storage/ppg/ProgramGraph.h b/src/storage/ppg/ProgramGraph.h index 7dc505298..1b83eac1f 100644 --- a/src/storage/ppg/ProgramGraph.h +++ b/src/storage/ppg/ProgramGraph.h @@ -21,8 +21,12 @@ namespace storm { using EdgeGroupIterator = ProgramLocation::EdgeGroupIterator; using ConstLocationIterator = std::unordered_map::const_iterator; - ProgramGraph(std::shared_ptr const& expManager, std::vector const& variables) : expManager(expManager), variables(variables) { - + ProgramGraph(std::shared_ptr const& expManager, std::vector const& variables) : expManager(expManager), variables() { + for(auto const& v : variables) { + this->variables.emplace(v.getIndex(), v); + } + // No Action: + deterministicActions.emplace(noActionId, DeterministicProgramAction(this, noActionId)); } ProgramGraph(ProgramGraph const&) = delete; @@ -36,6 +40,12 @@ namespace storm { return &(deterministicActions.emplace(newId, DeterministicProgramAction(this, newId)).first->second); } + ProbabilisticProgramAction* addUniformProbabilisticAction(ProgramVariableIdentifier var, int64_t from, int64_t to) { + ProgramActionIdentifier newId = freeActionIndex(); + assert(!hasAction(newId)); + return &(probabilisticActions.emplace(newId, ProbabilisticProgramAction(this, newId, var, from, to)).first->second); + } + ProgramLocation* addLocation(bool isInitial = false) { ProgramLocationIdentifier newId = freeLocationIndex(); assert(!hasLocation(newId)); @@ -86,6 +96,10 @@ namespace storm { } + ProgramActionIdentifier getNoActionId() const { + return noActionId; + } + std::vector addProgramEdgeToAllGroups(ProgramLocationIdentifier sourceId, ProgramActionIdentifier action, storm::expressions::Expression const& condition, ProgramLocationIdentifier targetId) { assert(hasLocation(sourceId)); return addProgramEdgeToAllGroups(getLocation(sourceId), action, condition, targetId); @@ -94,12 +108,10 @@ 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; + if(v.second.getName() == varName) { + return v.first; } - ++res; } assert(false); } @@ -110,7 +122,7 @@ namespace storm { bool hasVariable(std::string const& varName) const { for(auto const& v : variables) { - if(v.getName() == varName) { + if(v.second.getName() == varName) { return true; } } @@ -160,7 +172,7 @@ namespace storm { return locations.end(); } - std::vector const& getVariables() const { + std::unordered_map const& getVariables() const { return variables; } @@ -178,6 +190,7 @@ namespace storm { os << "Number of actions: " << nrActions() << std::endl; } + void printDot(std::ostream& os) const; protected: ProgramLocation& getLocation(ProgramLocationIdentifier id) { @@ -207,7 +220,7 @@ namespace storm { std::unordered_map probabilisticActions; std::unordered_map locations; storm::expressions::Expression initialValueRestriction; - std::vector variables; + std::unordered_map variables; std::shared_ptr expManager; private: @@ -215,7 +228,8 @@ namespace storm { ProgramEdgeGroupIdentifier newEdgeGroupId = 0; ProgramLocationIdentifier newLocationId = 0; ProgramEdgeIdentifier newEdgeId = 0; - ProgramActionIdentifier newActionId = 0; + ProgramActionIdentifier newActionId = 1; + ProgramActionIdentifier noActionId = 0; }; } diff --git a/src/storm-pgcl.cpp b/src/storm-pgcl.cpp index 906402e8b..b9d97b391 100644 --- a/src/storm-pgcl.cpp +++ b/src/storm-pgcl.cpp @@ -11,22 +11,14 @@ #include "src/builder/JaniProgramGraphBuilder.h" #include "src/storage/jani/JSONExporter.h" +#include "src/exceptions/FileIoException.h" + #include "src/settings/modules/GeneralSettings.h" #include "src/settings/modules/PGCLSettings.h" #include "src/settings/modules/CoreSettings.h" #include "src/settings/modules/DebugSettings.h" #include "src/settings/modules/JaniExportSettings.h" -//#include "src/settings/modules/CounterexampleGeneratorSettings.h" -//#include "src/settings/modules/CuddSettings.h" -//#include "src/settings/modules/SylvanSettings.h" -#include "src/settings/modules/GmmxxEquationSolverSettings.h" -#include "src/settings/modules/NativeEquationSolverSettings.h" -//#include "src/settings/modules/BisimulationSettings.h" -//#include "src/settings/modules/GlpkSettings.h" -//#include "src/settings/modules/GurobiSettings.h" -//#include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h" -//#include "src/settings/modules/ParametricSettings.h" -#include "src/settings/modules/EliminationSettings.h" + /*! * Initialize the settings manager. @@ -39,23 +31,12 @@ void initializeSettings() { storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); - //storm::settings::addModule(); - //storm::settings::addModule(); - //storm::settings::addModule(); - storm::settings::addModule(); - storm::settings::addModule(); - //storm::settings::addModule(); - //storm::settings::addModule(); - //storm::settings::addModule(); - //storm::settings::addModule(); - //storm::settings::addModule(); - storm::settings::addModule(); storm::settings::addModule(); } int handleJani(storm::jani::Model& model) { - if(!storm::settings::getModule().isJaniFileSet()) { + if (!storm::settings::getModule().isJaniFileSet()) { // For now, we have to have a jani file storm::jani::JsonExporter::toStream(model, std::cout); } else { @@ -63,6 +44,17 @@ int handleJani(storm::jani::Model& model) { } } +void programGraphToDotFile(storm::ppg::ProgramGraph const& prog) { + std::string filepath = storm::settings::getModule().getProgramGraphDotOutputFilename(); + std::ofstream ofs; + ofs.open(filepath, std::ofstream::out ); + if (ofs.is_open()) { + prog.printDot(ofs); + } else { + STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Cannot open " << filepath); + } +} + int main(const int argc, const char** argv) { try { storm::utility::setUp(); @@ -74,17 +66,20 @@ int main(const int argc, const char** argv) { return -1; } - if(!storm::settings::getModule().isPgclFileSet()) { + if (!storm::settings::getModule().isPgclFileSet()) { return -1; } storm::pgcl::PgclProgram prog = storm::parser::PgclParser::parse(storm::settings::getModule().getPgclFilename()); - std::cout << prog << std::endl; storm::ppg::ProgramGraph* progGraph = storm::builder::ProgramGraphBuilder::build(prog); progGraph->printInfo(std::cout); - if(storm::settings::getModule().isToJaniSet()) { - storm::builder::JaniProgramGraphBuilder builder; - storm::jani::Model* model = builder.build(*progGraph); + if (storm::settings::getModule().isProgramGraphToDotSet()) { + programGraphToDotFile(*progGraph); + } + if (storm::settings::getModule().isToJaniSet()) { + storm::builder::JaniProgramGraphBuilder builder(*progGraph); + builder.restrictAllVariables(0, 120); + storm::jani::Model* model = builder.build(); delete progGraph; handleJani(*model); delete model;