From b71574d478bcfbfe95a1f6b7ff497d8627e29a61 Mon Sep 17 00:00:00 2001 From: sjunges Date: Sun, 12 Feb 2017 22:14:23 +0100 Subject: [PATCH] make Jitbuilder compile if multiple levels are present... --- src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp index 3c029aee0..9844a64af 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -138,7 +138,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The input model contains undefined constants that influence the graph structure of the underlying model, which is not allowed."); } #endif - STORM_LOG_THROW(!model.reusesActionsInComposition(), storm::exceptions::InvalidArgumentException, "The jit JANI model builder currently does not support reusing actions in parallel composition"); + //STORM_LOG_THROW(!model.reusesActionsInComposition(), storm::exceptions::InvalidArgumentException, "The jit JANI model builder currently does not support reusing actions in parallel composition"); // Comment this in to print the JANI model for debugging purposes. // this->model.makeStandardJaniCompliant(); @@ -1014,6 +1014,7 @@ namespace storm { ++position; } bool generateLevelCode = lowestLevel != highestLevel; + uint64_t indentLevel = 4; indent(vectorSource, indentLevel - 4) << "void performSynchronizedDestinations_" << synchronizationVectorIndex << "(StateType const& in, StateBehaviour& behaviour, StateSet& statesToExplore, "; @@ -1078,11 +1079,11 @@ namespace storm { indent(vectorSource, indentLevel + 1 + index) << "for (auto const& destination" << index << " : edge" << index << ") {" << std::endl; if (generateLevelCode) { if (index == 0) { - indent(vectorSource, indentLevel + 2 + index) << "lowestLevel = edge0.lowestLevel();" << std::endl; - indent(vectorSource, indentLevel + 2 + index) << "highestLevel = edge0.highestLevel();" << std::endl; + indent(vectorSource, indentLevel + 2 + index) << "lowestLevel = destination" << index << ".lowestLevel();" << std::endl; + indent(vectorSource, indentLevel + 2 + index) << "highestLevel = destination" << index << ".highestLevel();" << std::endl; } else { - indent(vectorSource, indentLevel + 2 + index) << "lowestLevel = std::min(lowestLevel, edge0.lowestLevel());" << std::endl; - indent(vectorSource, indentLevel + 2 + index) << "highestLevel = std::max(highestLevel, edge0.highestLevel());" << std::endl; + indent(vectorSource, indentLevel + 2 + index) << "lowestLevel = std::min(lowestLevel, destination" << index << ".lowestLevel());" << std::endl; + indent(vectorSource, indentLevel + 2 + index) << "highestLevel = std::max(highestLevel, destination" << index << ".highestLevel());" << std::endl; } } }