From e8810a3be43f3438fb47f84740e85eedfc7071cb Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 26 Oct 2016 20:52:16 +0200 Subject: [PATCH] more work: up Former-commit-id: e7fa2351117c65dce1d3307880cce5556700091c [formerly 6323071a5b9401fc68eb2ca7a23bc4ecf1df8c20] Former-commit-id: 72073e0de4e86bf335b20e1ab6dd20ed82e10788 --- src/builder/jit/ExplicitJitJaniModelBuilder.cpp | 3 +++ src/builder/jit/ModelComponentsBuilder.cpp | 3 ++- src/builder/jit/StateBehaviour.cpp | 2 +- src/builder/jit/StateBehaviour.h | 2 +- 4 files changed, 7 insertions(+), 3 deletions(-) diff --git a/src/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/builder/jit/ExplicitJitJaniModelBuilder.cpp index e0f601ea2..13a55275e 100644 --- a/src/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/src/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -189,9 +189,12 @@ namespace storm { this->modelComponentsBuilder.registerLabel("init", stateIds.size()); this->modelComponentsBuilder.registerLabel("deadlock", stateIds.size()); + int stateCnt = 0; for (auto const& stateEntry : stateIds) { auto const& state = stateEntry.first; {% for label in labels %}if ({$label.predicate}) { + ++stateCnt; + std::cout << "state " << state << " with index " << stateEntry.second << " has label {$label.name} (" << stateCnt << ") " << std::endl; this->modelComponentsBuilder.addLabel(stateEntry.second, {$loop.index} - 1); } {% endfor %} diff --git a/src/builder/jit/ModelComponentsBuilder.cpp b/src/builder/jit/ModelComponentsBuilder.cpp index 6935b1cab..049db264d 100644 --- a/src/builder/jit/ModelComponentsBuilder.cpp +++ b/src/builder/jit/ModelComponentsBuilder.cpp @@ -9,6 +9,7 @@ #include "src/exceptions/WrongFormatException.h" #include "src/utility/macros.h" +#include "src/utility/constants.h" namespace storm { namespace builder { @@ -49,7 +50,7 @@ namespace storm { if (behaviour.isExpanded() && dontFixDeadlocks) { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating sparse matrix from JANI model: found deadlock state and fixing deadlocks was explicitly disabled."); } else { - // FIXME: fix deadlock + transitionMatrixBuilder->addNextValue(currentRow, currentRowGroup, storm::utility::one()); } } ++currentRowGroup; diff --git a/src/builder/jit/StateBehaviour.cpp b/src/builder/jit/StateBehaviour.cpp index 2a24d70ee..e054e4af3 100644 --- a/src/builder/jit/StateBehaviour.cpp +++ b/src/builder/jit/StateBehaviour.cpp @@ -62,7 +62,7 @@ namespace storm { } template - void StateBehaviour::setExpaned() { + void StateBehaviour::setExpanded() { expanded = true; } diff --git a/src/builder/jit/StateBehaviour.h b/src/builder/jit/StateBehaviour.h index a5dd5d839..7b49a8db5 100644 --- a/src/builder/jit/StateBehaviour.h +++ b/src/builder/jit/StateBehaviour.h @@ -23,7 +23,7 @@ namespace storm { void compress(); bool isExpanded() const; - void setExpaned(); + void setExpanded(); bool empty() const; std::size_t size() const;