From 137aa163f2a0a026f31a4401737158c9d512ee26 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 21 Nov 2016 15:14:43 +0100 Subject: [PATCH] fixed jit builder to not ignore locations --- .../jit/ExplicitJitJaniModelBuilder.cpp | 58 ++++++++++++++----- .../builder/jit/ExplicitJitJaniModelBuilder.h | 4 +- .../generator/JaniNextStateGenerator.cpp | 2 +- 3 files changed, 45 insertions(+), 19 deletions(-) diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp index 31b80d3c8..7e8397d9d 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -560,16 +560,20 @@ namespace storm { lowerBounds[variable.getExpressionVariable()] = lowerBound; if (lowerBound != 0) { - lowerBoundShiftSubstitution[variable.getExpressionVariable()] = variable.getExpressionVariable() + model.getManager().integer(lowerBound); + lowerBoundShiftSubstitution[variable.getExpressionVariable()] = variable.getExpressionVariable() - model.getManager().integer(-lowerBound); } uint64_t range = static_cast(upperBound - lowerBound + 1); uint64_t numberOfBits = static_cast(std::ceil(std::log2(range))); result["name"] = registerVariable(variable.getExpressionVariable(), variable.isTransient()); + result["original_name"] = variable.getExpressionVariable().getName(); result["numberOfBits"] = std::to_string(numberOfBits); if (variable.hasInitExpression()) { result["init"] = asString(variable.getInitExpression().evaluateAsInt() - lowerBound); } + + result["lower"] = asString(lowerBound); + result["upper"] = asString(upperBound); return result; } @@ -740,6 +744,10 @@ namespace storm { storm::expressions::Expression blockingExpression; std::shared_ptr model = solver->getModel(); for (auto const& variable : this->model.getGlobalVariables().getBooleanVariables()) { + if (variable.isTransient()) { + continue; + } + storm::expressions::Variable const& expressionVariable = variable.getExpressionVariable(); bool variableValue = model->getBooleanValue(expressionVariable); initialStateAssignment.push_back(generateAssignment(variable, variableValue)); @@ -748,6 +756,10 @@ namespace storm { blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression; } for (auto const& variable : this->model.getGlobalVariables().getBoundedIntegerVariables()) { + if (variable.isTransient()) { + continue; + } + storm::expressions::Variable const& expressionVariable = variable.getExpressionVariable(); int_fast64_t variableValue = model->getIntegerValue(expressionVariable); initialStateAssignment.push_back(generateAssignment(variable, variableValue)); @@ -758,6 +770,10 @@ namespace storm { for (auto const& automatonRef : parallelAutomata) { storm::jani::Automaton const& automaton = automatonRef.get(); for (auto const& variable : automaton.getVariables().getBooleanVariables()) { + if (variable.isTransient()) { + continue; + } + storm::expressions::Variable const& expressionVariable = variable.getExpressionVariable(); bool variableValue = model->getBooleanValue(expressionVariable); initialStateAssignment.push_back(generateAssignment(variable, variableValue)); @@ -766,6 +782,10 @@ namespace storm { blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression; } for (auto const& variable : automaton.getVariables().getBoundedIntegerVariables()) { + if (variable.isTransient()) { + continue; + } + storm::expressions::Variable const& expressionVariable = variable.getExpressionVariable(); int_fast64_t variableValue = model->getIntegerValue(expressionVariable); initialStateAssignment.push_back(generateAssignment(variable, variableValue)); @@ -1285,7 +1305,7 @@ namespace storm { uint64_t destinationIndex = 0; std::set transientVariablesInDestinations; for (auto const& destination : edge.getDestinations()) { - destinations.push_back(generateDestination(destinationIndex, destination, edge.getOptionalRate())); + destinations.push_back(generateDestination(automaton, destinationIndex, destination, edge.getOptionalRate())); for (auto const& assignment : destination.getOrderedAssignments().getAllAssignments()) { if (assignment.isTransient()) { @@ -1302,7 +1322,7 @@ namespace storm { ++destinationIndex; } - edgeData["guard"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(edge.getGuard()), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); + edgeData["guard"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(edge.getGuard()) && getLocationVariable(automaton) == model.getManager().integer(edge.getSourceLocationIndex()), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)); edgeData["destinations"] = cpptempl::make_data(destinations); edgeData["name"] = automaton.getName() + "_" + std::to_string(edgeIndex); edgeData["transient_assignments"] = cpptempl::make_data(edgeAssignments); @@ -1322,10 +1342,10 @@ namespace storm { } template - cpptempl::data_map ExplicitJitJaniModelBuilder::generateDestination(uint64_t destinationIndex, storm::jani::EdgeDestination const& destination, boost::optional const& rate) { + cpptempl::data_map ExplicitJitJaniModelBuilder::generateDestination(storm::jani::Automaton const& automaton, uint64_t destinationIndex, storm::jani::EdgeDestination const& destination, boost::optional const& rate) { cpptempl::data_map destinationData; - cpptempl::data_list levels = generateLevels(destination.getOrderedAssignments()); + cpptempl::data_list levels = generateLevels(automaton, destination.getLocationIndex(), destination.getOrderedAssignments()); destinationData["name"] = asString(destinationIndex); destinationData["levels"] = cpptempl::make_data(levels); storm::expressions::Expression expressionToTranslate = rate ? shiftVariablesWrtLowerBound(rate.get() * destination.getProbability()) : shiftVariablesWrtLowerBound(destination.getProbability()); @@ -1348,12 +1368,12 @@ namespace storm { } template - cpptempl::data_list ExplicitJitJaniModelBuilder::generateLevels(storm::jani::OrderedAssignments const& orderedAssignments) { + cpptempl::data_list ExplicitJitJaniModelBuilder::generateLevels(storm::jani::Automaton const& automaton, uint64_t destinationLocationIndex, storm::jani::OrderedAssignments const& orderedAssignments) { cpptempl::data_list levels; auto const& assignments = orderedAssignments.getAllAssignments(); if (!assignments.empty()) { - int_fast64_t currentLevel = assignments.begin()->getLevel(); + int64_t currentLevel = assignments.front().getLevel(); cpptempl::data_list nonTransientAssignmentData; cpptempl::data_list transientAssignmentData; @@ -1379,10 +1399,21 @@ namespace storm { // Close the last (open) level. cpptempl::data_map level; + nonTransientAssignmentData.push_back(generateLocationAssignment(automaton, destinationLocationIndex)); level["non_transient_assignments"] = cpptempl::make_data(nonTransientAssignmentData); level["transient_assignments"] = cpptempl::make_data(transientAssignmentData); level["index"] = asString(currentLevel); levels.push_back(level); + } else { + // Create (an otherwise) empty level to perform the location assignment. + cpptempl::data_map level; + cpptempl::data_list nonTransientAssignmentData; + cpptempl::data_list transientAssignmentData; + nonTransientAssignmentData.push_back(generateLocationAssignment(automaton, destinationLocationIndex)); + level["non_transient_assignments"] = cpptempl::make_data(nonTransientAssignmentData); + level["transient_assignments"] = cpptempl::make_data(transientAssignmentData); + level["index"] = asString(0); + levels.push_back(level); } return levels; @@ -1397,7 +1428,7 @@ namespace storm { // Check if the variable has a non-zero lower bound and, if so, shift it appropriately. auto it = lowerBounds.find(variable.getExpressionVariable()); if (it != lowerBounds.end()) { - result["value"] = asString(value) + " - " + asString(it->second); + result["value"] = asString(value) + " + " + asString(-it->second); } else { result["value"] = asString(value); } @@ -1430,13 +1461,7 @@ namespace storm { } if (lowerBoundIt != lowerBounds.end()) { - if (lowerBoundIt->second < 0) { - result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()) + model.getManager().integer(lowerBoundIt->second), options); - } else if (lowerBoundIt->second == 0) { - result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()), options); - } else { - result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()) - model.getManager().integer(lowerBoundIt->second), options); - } + result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()) + model.getManager().integer(-lowerBoundIt->second), options); } else { result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()), options); } @@ -1633,7 +1658,8 @@ namespace storm { {% for variable in nontransient_variables.boolean %}bool {$variable.name} : 1; {% endfor %} // Bounded integer variables. - {% for variable in nontransient_variables.boundedInteger %}uint64_t {$variable.name} : {$variable.numberOfBits}; + {% for variable in nontransient_variables.boundedInteger %}// {$variable.original_name}: [{$variable.lower} ... {$variable.upper}] + uint64_t {$variable.name} : {$variable.numberOfBits}; {% endfor %} // Unbounded integer variables. {% for variable in nontransient_variables.unboundedInteger %}int64_t {$variable.name}; diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h index ca3f6b3c2..e3c4c0b94 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h @@ -100,9 +100,9 @@ namespace storm { // Functions related to the generation of edge data. void generateEdges(cpptempl::data_map& modelData); cpptempl::data_map generateSynchronizationVector(cpptempl::data_map& modelData, storm::jani::ParallelComposition const& parallelComposition, storm::jani::SynchronizationVector const& synchronizationVector, uint64_t synchronizationVectorIndex); - cpptempl::data_list generateLevels(storm::jani::OrderedAssignments const& assignments); + cpptempl::data_list generateLevels(storm::jani::Automaton const& automaton, uint64_t destinationLocationIndex, storm::jani::OrderedAssignments const& assignments); cpptempl::data_map generateEdge(storm::jani::Automaton const& automaton, uint64_t edgeIndex, storm::jani::Edge const& edge); - cpptempl::data_map generateDestination(uint64_t destinationIndex, storm::jani::EdgeDestination const& destination, boost::optional const& rate = boost::none); + cpptempl::data_map generateDestination(storm::jani::Automaton const& automaton, uint64_t destinationIndex, storm::jani::EdgeDestination const& destination, boost::optional const& rate = boost::none); template cpptempl::data_map generateAssignment(storm::jani::Variable const& variable, ValueTypePrime value) const; cpptempl::data_map generateLocationAssignment(storm::jani::Automaton const& automaton, uint64_t value) const; diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index b03dba70c..42372b291 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -25,7 +25,6 @@ namespace storm { JaniNextStateGenerator::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator(model.getExpressionManager(), options), model(model), rewardVariables(), hasStateActionRewards(false) { STORM_LOG_THROW(model.hasStandardComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions."); STORM_LOG_THROW(!model.hasNonGlobalTransientVariable(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support automata-local transient variables."); - STORM_LOG_THROW(!model.hasTransientEdgeDestinationAssignments(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support transient edge destination assignments."); STORM_LOG_THROW(!model.usesAssignmentLevels(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support assignment levels."); STORM_LOG_THROW(!this->options.isBuildChoiceLabelsSet(), storm::exceptions::InvalidSettingsException, "JANI next-state generator cannot generate choice labels."); @@ -33,6 +32,7 @@ namespace storm { if (this->model.hasTransientEdgeDestinationAssignments()) { this->model.liftTransientEdgeDestinationAssignments(); } + STORM_LOG_THROW(!this->model.hasTransientEdgeDestinationAssignments(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support transient edge destination assignments."); // Only after checking validity of the program, we initialize the variable information. this->checkValid();