From e7dc0a049b1dba2dff4223fa7ef74db0746b0902 Mon Sep 17 00:00:00 2001 From: sjunges Date: Fri, 30 Sep 2016 01:05:59 +0200 Subject: [PATCH] towards nice pgcl - jani support Former-commit-id: 4465a9566a0d8a6913ef69c740e599ffe765a88d [formerly c5fd489dabdbbee94b53f6fd184bf9433185e9c2] Former-commit-id: 34f78bdd4f854987d4ddeabd63ee59355e88f114 --- src/builder/JaniProgramGraphBuilder.cpp | 13 ++++- src/builder/JaniProgramGraphBuilder.h | 30 ++++++---- src/builder/ProgramGraphBuilder.h | 6 +- src/storage/pgcl/PgclProgram.cpp | 9 ++- src/storage/pgcl/PgclProgram.h | 9 ++- src/storage/pgcl/VariableDeclaration.cpp | 1 + src/storage/pgcl/VariableDeclaration.h | 36 ++++++++++++ src/storage/ppg/ProgramAction.h | 19 +++++++ src/storage/ppg/ProgramEdgeGroup.h | 9 +++ src/storage/ppg/ProgramGraph.cpp | 71 ++++++++++++++++++++++-- src/storage/ppg/ProgramGraph.h | 60 ++++++++++++++++++-- src/storage/ppg/ProgramLocation.h | 4 ++ src/storm-pgcl.cpp | 2 +- 13 files changed, 235 insertions(+), 34 deletions(-) create mode 100644 src/storage/pgcl/VariableDeclaration.cpp create mode 100644 src/storage/pgcl/VariableDeclaration.h diff --git a/src/builder/JaniProgramGraphBuilder.cpp b/src/builder/JaniProgramGraphBuilder.cpp index 72fce66d7..41d6cba65 100644 --- a/src/builder/JaniProgramGraphBuilder.cpp +++ b/src/builder/JaniProgramGraphBuilder.cpp @@ -47,7 +47,13 @@ namespace storm { storm::expressions::Expression newGuard; newGuard = expManager->boolean(true); if (edge.getAction().isProbabilistic()) { - + // No check necessary currently, but at least we should statically check that the bounds are okay. + storm::ppg::ProbabilisticProgramAction const& act = static_cast(edge.getAction()); + if (isUserRestrictedVariable(act.getVariableIdentifier())) { + storm::storage::IntegerInterval const& bound = variableRestrictions.at(act.getVariableIdentifier()); + storm::storage::IntegerInterval supportInterval = act.getSupportInterval(); + STORM_LOG_THROW(bound.contains(supportInterval), storm::exceptions::NotSupportedException, "User provided bounds must contain all constant expressions"); + } } 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"); @@ -81,7 +87,10 @@ namespace storm { for(auto it = programGraph.locationBegin(); it != programGraph.locationEnd(); ++it) { ppg::ProgramLocation const& loc = it->second; if (loc.nrOutgoingEdgeGroups() == 0) { - // TODO deadlock! + storm::jani::OrderedAssignments oa; + storm::jani::EdgeDestination dest(janiLocId.at(loc.id()), expManager->integer(1), oa); + storm::jani::Edge e(janiLocId.at(loc.id()), storm::jani::Model::SILENT_ACTION_INDEX, boost::none, expManager->boolean(true), {dest}); + automaton.addEdge(e); } else if (loc.nrOutgoingEdgeGroups() == 1) { for(auto const& edge : **(loc.begin())) { std::pair, storm::expressions::Expression> checks = addVariableChecks(*edge); diff --git a/src/builder/JaniProgramGraphBuilder.h b/src/builder/JaniProgramGraphBuilder.h index 72a1b9320..0e20e7d84 100644 --- a/src/builder/JaniProgramGraphBuilder.h +++ b/src/builder/JaniProgramGraphBuilder.h @@ -25,7 +25,7 @@ namespace storm { static unsigned janiVersion; JaniProgramGraphBuilder(storm::ppg::ProgramGraph const& pg) : programGraph(pg) { - transients = programGraph.transientVariables(); + rewards = programGraph.rewardVariables(); } virtual ~JaniProgramGraphBuilder() { @@ -41,7 +41,9 @@ 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)); + if(v.second.hasIntegerType()) { + variableRestrictions.emplace(v.first, storm::storage::IntegerInterval(from, to)); + } } } @@ -78,25 +80,29 @@ namespace storm { std::pair, storm::expressions::Expression> addVariableChecks(storm::ppg::ProgramEdge const& edge); bool isUserRestrictedVariable(storm::ppg::ProgramVariableIdentifier i) { - return variableRestrictions.count(i) == 1 && !isTransientVariable(i); + return variableRestrictions.count(i) == 1 && !isRewardVariable(i); } bool isRestrictedVariable(storm::ppg::ProgramVariableIdentifier i) { // Might be different from user restricted in near future. - return variableRestrictions.count(i) == 1 && !isTransientVariable(i); + return variableRestrictions.count(i) == 1 && !isRewardVariable(i); } - bool isTransientVariable(storm::ppg::ProgramVariableIdentifier i) { - return std::find(transients.begin(), transients.end(), i) != transients.end(); + bool isRewardVariable(storm::ppg::ProgramVariableIdentifier i) { + return std::find(rewards.begin(), rewards.end(), i) != rewards.end(); } void addProcedureVariables(storm::jani::Model& model, storm::jani::Automaton& automaton) { for (auto const& v : programGraph.getVariables()) { - if(isRestrictedVariable(v.first) && !isTransientVariable(v.first)) { + if (v.second.hasBooleanType()) { + storm::jani::BooleanVariable* janiVar = new storm::jani::BooleanVariable(v.second.getName(), v.second, programGraph.getInitialValue(v.first), false); + automaton.addVariable(*janiVar); + variables.emplace(v.first, janiVar); + } else if (isRestrictedVariable(v.first) && !isRewardVariable(v.first)) { storm::storage::IntegerInterval const& bounds = variableRestrictions.at(v.first); if (bounds.hasLeftBound()) { if (bounds.hasRightBound()) { - storm::jani::BoundedIntegerVariable* janiVar = new storm::jani::BoundedIntegerVariable (v.second.getName(), v.second, expManager->integer(0), false, expManager->integer(bounds.getLeftBound().get()), expManager->integer(bounds.getRightBound().get())); + storm::jani::BoundedIntegerVariable* janiVar = new storm::jani::BoundedIntegerVariable (v.second.getName(), v.second, programGraph.getInitialValue(v.first), false, expManager->integer(bounds.getLeftBound().get()), expManager->integer(bounds.getRightBound().get())); variables.emplace(v.first, janiVar); automaton.addVariable(*janiVar); } else { @@ -108,8 +114,8 @@ namespace storm { assert(false); } } else { - storm::jani::UnboundedIntegerVariable* janiVar = new storm::jani::UnboundedIntegerVariable(v.second.getName(), v.second, expManager->integer(0), isTransientVariable(v.first)); - if(isTransientVariable(v.first)) { + storm::jani::UnboundedIntegerVariable* janiVar = new storm::jani::UnboundedIntegerVariable(v.second.getName(), v.second, programGraph.getInitialValue(v.first), isRewardVariable(v.first)); + if(isRewardVariable(v.first)) { model.addVariable(*janiVar); } else { automaton.addVariable(*janiVar); @@ -134,7 +140,7 @@ namespace storm { void addVariableOoBLocations(storm::jani::Automaton& automaton) { for(auto const& restr : variableRestrictions) { - if(!isTransientVariable(restr.first)) { + if(!isRewardVariable(restr.first)) { storm::jani::Location janiLoc(janiVariableOutOfBoundsLocationName(restr.first)); uint64_t locId = automaton.addLocation(janiLoc); varOutOfBoundsLocations[restr.first] = locId; @@ -143,7 +149,7 @@ namespace storm { } } /// Transient variables - std::vector transients; + std::vector rewards; /// Restrictions on variables std::map variableRestrictions; /// Locations for variables that would have gone ot o diff --git a/src/builder/ProgramGraphBuilder.h b/src/builder/ProgramGraphBuilder.h index 9c856704b..90f78f112 100644 --- a/src/builder/ProgramGraphBuilder.h +++ b/src/builder/ProgramGraphBuilder.h @@ -108,7 +108,7 @@ namespace storm { ProgramGraphBuilder(storm::pgcl::PgclProgram const& program) : program(program) { - graph = new storm::ppg::ProgramGraph(program.getExpressionManager(), program.getVariables()); + graph = new storm::ppg::ProgramGraph(program.getExpressionManager(), program.getVariableDeclarations()); noActionId = graph->getNoActionId(); } @@ -116,10 +116,10 @@ namespace storm { void run() { currentStack.push_back(graph->addLocation(true)); // Terminal state. - nextStack.push_back(graph->addLocation(false)); + nextStack.push_back(graph->addLocation(false, true)); // Observe Violated State. if (program.hasObserve()) { - observeFailedState = graph->addLocation(); + observeFailedState = graph->addLocation(false, false, true); } buildBlock(program); } diff --git a/src/storage/pgcl/PgclProgram.cpp b/src/storage/pgcl/PgclProgram.cpp index 93a599bf6..d0bba935e 100755 --- a/src/storage/pgcl/PgclProgram.cpp +++ b/src/storage/pgcl/PgclProgram.cpp @@ -4,11 +4,12 @@ namespace storm { namespace pgcl { - PgclProgram::PgclProgram(vector const& statements, vector const& locationToStatement, std::vector const& parameters, std::shared_ptr expressions, bool hasLoop, bool hasNondet, bool hasObserve) : + PgclProgram::PgclProgram(std::vector variables, vector const& statements, vector const& locationToStatement, std::vector const& parameters, std::shared_ptr expressions, bool hasLoop, bool hasNondet, bool hasObserve) : PgclBlock(statements, expressions, hasLoop, hasNondet, hasObserve), - locationToStatement(locationToStatement) + locationToStatement(locationToStatement),variables(variables) { + // Intentionally left empty. } @@ -24,6 +25,10 @@ namespace storm { return vars; } + + std::vector const& PgclProgram::getVariableDeclarations() const { + return variables; + } std::ostream& operator<<(std::ostream& stream, PgclProgram& program) { storm::pgcl::StatementPrinterVisitor printer(stream); diff --git a/src/storage/pgcl/PgclProgram.h b/src/storage/pgcl/PgclProgram.h index 8c6bffc57..79d755a66 100755 --- a/src/storage/pgcl/PgclProgram.h +++ b/src/storage/pgcl/PgclProgram.h @@ -2,6 +2,7 @@ #include #include "Block.h" +#include "VariableDeclaration.h" #include "src/storage/pgcl/Statement.h" #include "src/storage/pgcl/StatementPrinterVisitor.h" #include "src/storage/expressions/ExpressionManager.h" @@ -36,7 +37,7 @@ namespace storm { * statement. * @param hasParam Whether the program is parameterized. */ - PgclProgram(vector const& statements, vector const& locationToStatement, std::vector const& parameters, std::shared_ptr expressions, bool hasLoop, bool hasNondet, bool hasObserve); + PgclProgram(std::vector variables, vector const& statements, vector const& locationToStatement, std::vector const& parameters, std::shared_ptr expressions, bool hasLoop, bool hasNondet, bool hasObserve); PgclProgram(const PgclProgram & orig) = default; @@ -48,6 +49,9 @@ namespace storm { vector getLocationToStatementVector(); std::vector getVariables() const; + std::vector const& getVariableDeclarations() const; + + private: /** @@ -56,7 +60,8 @@ namespace storm { * recursion is resolved here. */ vector locationToStatement; - }; + std::vector variables; + }; /** * Prints every statement of the program along with their location * numbers. diff --git a/src/storage/pgcl/VariableDeclaration.cpp b/src/storage/pgcl/VariableDeclaration.cpp new file mode 100644 index 000000000..241437821 --- /dev/null +++ b/src/storage/pgcl/VariableDeclaration.cpp @@ -0,0 +1 @@ +#include "VariableDeclaration.h" diff --git a/src/storage/pgcl/VariableDeclaration.h b/src/storage/pgcl/VariableDeclaration.h new file mode 100644 index 000000000..a2f7b8d37 --- /dev/null +++ b/src/storage/pgcl/VariableDeclaration.h @@ -0,0 +1,36 @@ +#pragma once + +#include "src/storage/expressions/Expression.h" +#include "src/storage/expressions/Variable.h" + +namespace storm { + namespace pgcl { + class VariableDeclaration { + public: + + VariableDeclaration(storm::expressions::Variable const& var, storm::expressions::Expression const& exp) + : variable(var), initialValue(exp) + { + // Not implemented. + } + + storm::expressions::Variable const& getVariable() const { + return variable; + } + + storm::expressions::Expression const& getInitialValueExpression() const { + return initialValue; + } + + private: + storm::expressions::Variable variable; + storm::expressions::Expression initialValue; + + }; + } +} + + + + + diff --git a/src/storage/ppg/ProgramAction.h b/src/storage/ppg/ProgramAction.h index 4220a207d..6241645b9 100644 --- a/src/storage/ppg/ProgramAction.h +++ b/src/storage/ppg/ProgramAction.h @@ -1,5 +1,6 @@ #pragma once #include "defines.h" +#include "src/storage/IntegerInterval.h" #include "src/storage/expressions/Expression.h" #include "src/storage/expressions/Variable.h" #include "src/storage/expressions/ExpressionManager.h" @@ -57,6 +58,24 @@ namespace storm { std::string const& getVariableName() const; + ProgramVariableIdentifier getVariableIdentifier() const { + return var; + } + + storm::storage::IntegerInterval getSupportInterval() const { + assert(!values.empty()); + int64_t min = values.front().value; + int64_t max = values.front().value; + for (auto const& valEntry : values) { + if (valEntry.value < min) { + min = valEntry.value; + } else if (valEntry.value > max) { + max = valEntry.value; + } + } + return storm::storage::IntegerInterval(min, max); + } + iterator begin() { return values.begin(); } diff --git a/src/storage/ppg/ProgramEdgeGroup.h b/src/storage/ppg/ProgramEdgeGroup.h index 235ee694a..13d63df99 100644 --- a/src/storage/ppg/ProgramEdgeGroup.h +++ b/src/storage/ppg/ProgramEdgeGroup.h @@ -8,6 +8,7 @@ namespace storm { class ProgramEdgeGroup { public: + using iterator = std::vector::iterator; using const_iterator = std::vector::const_iterator; ProgramEdgeGroup(ProgramGraph* graph, ProgramEdgeGroupIdentifier id, ProgramLocationIdentifier sourceId, storm::expressions::Expression const& probability) @@ -33,6 +34,14 @@ namespace storm { return edges.back(); } + iterator begin() { + return edges.begin(); + } + + iterator end() { + return edges.end(); + } + const_iterator begin() const { return edges.begin(); } diff --git a/src/storage/ppg/ProgramGraph.cpp b/src/storage/ppg/ProgramGraph.cpp index 169c880f7..1b1388eda 100644 --- a/src/storage/ppg/ProgramGraph.cpp +++ b/src/storage/ppg/ProgramGraph.cpp @@ -5,7 +5,7 @@ namespace storm { namespace ppg { - std::vector ProgramGraph::transientVariables() const { + std::vector ProgramGraph::noeffectVariables() const { std::vector transientCandidates = variablesNotInGuards(); bool removedCandidate = true; // tmp while(removedCandidate && !transientCandidates.empty()) { @@ -29,6 +29,58 @@ namespace storm { return transientCandidates; } + std::pair ProgramGraph::checkIfRewardVariableHelper(storm::expressions::Variable const& var, std::unordered_map const& detActions) const { + bool pos = true; + bool first = true; + for (auto const& act : detActions) { + for (auto const& group : act.second) { + for (auto const& assignment : group) { + if (assignment.first == var.getIndex()) { + //storm::expressions::Expression expr = (assignment.second - var.getExpression()).simplify(); + if(!assignment.second.isLinear()) { + return {false, true}; + } + auto const& vars = assignment.second.getVariables(); + if(vars.empty() || vars.size() > 1) { + return {false, true}; + } + if(vars.begin()->getIndex() == assignment.first) { + std::map eta0; + std::map eta1; + eta0.emplace(var, expManager->integer(0)); + eta1.emplace(var, expManager->integer(1)); + if(assignment.second.substitute(eta1).evaluateAsInt() - assignment.second.substitute(eta0).evaluateAsInt() != 1) { + return {false, true}; + } + if(assignment.second.substitute(eta0).evaluateAsInt() < 0) { + if(!first && pos) { + return {false, true}; + } + pos = false; + } + first = false; + } + } + } + } + } + return {true, pos}; + } + + std::vector ProgramGraph::rewardVariables() const { + std::vector rewardCandidates = noeffectVariables(); + std::vector result; + for (auto const& var : rewardCandidates) { + if(variables.at(var).hasIntegerType()) { + // TODO add some checks here; refine the evaluate as int stuff. + if(initialValues.at(var).evaluateAsInt() == 0 && checkIfRewardVariableHelper(variables.at(var), this->deterministicActions).first) { + result.push_back(var); + } + } + } + return result; + } + std::vector ProgramGraph::variablesNotInGuards() const { std::vector result; std::set contained; @@ -36,11 +88,6 @@ namespace storm { for (auto const& edgegroup : loc.second) { for (auto const& edge : *edgegroup) { auto conditionVars = edge->getCondition().getVariables(); - std::cout << "Guard " << edge->getCondition() << " contains "; - for (auto const& cv : conditionVars) { - std::cout << cv.getName() << ", "; - } - std::cout << std::endl; contained.insert(conditionVars.begin(), conditionVars.end()); } } @@ -54,6 +101,18 @@ namespace storm { return result; } +// void ProgramGraph::mergeActions() { +// auto initialLocs = initialLocations(); +// assert(initialLocs.size() == 1); +// // For now, we only follow the unique path. +// ProgramLocationIdentifier currentLocId = initialLocs.front(); +// while(locations.at(currentLocId).hasUniqueSuccessor()) { +// auto& edgeGroup = **locations.at(currentLocId()).begin(); +// auto& edge = **edgeGroup.begin(); +// +// } +// } + void ProgramGraph::printDot(std::ostream& os) const { os << "digraph ppg {" << std::endl; diff --git a/src/storage/ppg/ProgramGraph.h b/src/storage/ppg/ProgramGraph.h index e2028f28c..99ab9a940 100644 --- a/src/storage/ppg/ProgramGraph.h +++ b/src/storage/ppg/ProgramGraph.h @@ -10,6 +10,8 @@ #include "ProgramEdgeGroup.h" #include "ProgramAction.h" +#include "src/storage/pgcl/VariableDeclaration.h" + namespace storm { namespace ppg { /** @@ -21,9 +23,10 @@ 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() { + ProgramGraph(std::shared_ptr const& expManager, std::vector const& variables) : variables(), expManager(expManager) { for(auto const& v : variables) { - this->variables.emplace(v.getIndex(), v); + this->variables.emplace(v.getVariable().getIndex(), v.getVariable()); + this->initialValues.emplace(v.getVariable().getIndex(), v.getInitialValueExpression()); } // No Action: deterministicActions.emplace(noActionId, DeterministicProgramAction(this, noActionId)); @@ -46,9 +49,10 @@ namespace storm { return &(probabilisticActions.emplace(newId, ProbabilisticProgramAction(this, newId, var, from, to)).first->second); } - ProgramLocation* addLocation(bool isInitial = false) { + ProgramLocation* addLocation(bool isInitial = false, bool successfulTermination = false, bool aborted = false, std::vector const& labels = {}) { ProgramLocationIdentifier newId = freeLocationIndex(); assert(!hasLocation(newId)); + locationLabels[newId] = labels; return &(locations.emplace(newId, ProgramLocation(this, newId, isInitial)).first->second); } @@ -92,10 +96,26 @@ namespace storm { } return res; - } + + bool hasLabel(ProgramLocationIdentifier loc, std::string const& label) const { + return std::find(locationLabels.at(loc).begin(), locationLabels.at(loc).end(), label) != locationLabels.at(loc).end(); + } + + bool hasSuccessfulTerminationLabel(ProgramLocationIdentifier loc) const { + return hasLabel(loc, succesfulTerminationLabel); + } + + bool hasAbortLabel(ProgramLocationIdentifier loc) const { + return hasLabel(loc, abortLabel); + } + + bool hasTerminationLabel(ProgramLocationIdentifier loc) const { + return hasSuccessfulTerminationLabel(loc) || hasAbortLabel(loc); + } + ProgramActionIdentifier getNoActionId() const { return noActionId; } @@ -163,6 +183,11 @@ namespace storm { return variables.size(); } + storm::expressions::Expression getInitialValue(ProgramVariableIdentifier v) const { + return initialValues.at(v); + } + + void collectInitialValues(); ConstLocationIterator locationBegin() const { return locations.begin(); @@ -180,7 +205,10 @@ namespace storm { return expManager; } - std::vector transientVariables() const; + std::vector noeffectVariables() const; + + std::vector rewardVariables() const; + void checkValid() { @@ -195,11 +223,25 @@ namespace storm { void printDot(std::ostream& os) const; protected: + + std::vector initialLocationIdentifiers() const { + std::vector result; + for (auto const& loc : locations) { + if(loc.second.isInitial()) { + result.push_back(loc.first); + } + } + return result; + } + /** * Returns the set of variables which do not occur in guards. */ std::vector variablesNotInGuards() const; + std::pair checkIfRewardVariableHelper(storm::expressions::Variable const& var, std::unordered_map const& detActions) const; + + ProgramLocation& getLocation(ProgramLocationIdentifier id) { return locations.at(id); } @@ -228,7 +270,10 @@ namespace storm { std::unordered_map locations; storm::expressions::Expression initialValueRestriction; std::unordered_map variables; - + /// + std::unordered_map initialValues; + // If heavily used, then it might be better to use a bitvector and a seperate list for the names. + std::unordered_map> locationLabels; std::shared_ptr expManager; private: // Helper for IDs, may be changed later. @@ -237,6 +282,9 @@ namespace storm { ProgramEdgeIdentifier newEdgeId = 0; ProgramActionIdentifier newActionId = 1; ProgramActionIdentifier noActionId = 0; + std::string succesfulTerminationLabel = "__ret0__"; + std::string abortLabel = "__ret1__"; + }; } diff --git a/src/storage/ppg/ProgramLocation.h b/src/storage/ppg/ProgramLocation.h index e88f0e85d..48b92dfed 100644 --- a/src/storage/ppg/ProgramLocation.h +++ b/src/storage/ppg/ProgramLocation.h @@ -46,6 +46,10 @@ namespace storm { return false; } + bool hasUniqueSuccessor() const { + return nrOutgoingEdgeGroups() == 1 && !hasNonDeterminism(); + } + const_iterator begin() const { return edgeGroups.begin(); } diff --git a/src/storm-pgcl.cpp b/src/storm-pgcl.cpp index 729e12588..66e227d75 100644 --- a/src/storm-pgcl.cpp +++ b/src/storm-pgcl.cpp @@ -34,7 +34,7 @@ void initializeSettings() { storm::settings::addModule(); } -int handleJani(storm::jani::Model& model) { +void handleJani(storm::jani::Model& model) { if (!storm::settings::getModule().isJaniFileSet()) { // For now, we have to have a jani file storm::jani::JsonExporter::toStream(model, std::cout);