diff --git a/src/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/builder/jit/ExplicitJitJaniModelBuilder.cpp index 13a55275e..6efb68661 100644 --- a/src/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/src/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -13,6 +13,7 @@ #include "src/utility/macros.h" #include "src/utility/solver.h" +#include "src/exceptions/WrongFormatException.h" #include "src/exceptions/InvalidStateException.h" #include "src/exceptions/NotSupportedException.h" #include "src/exceptions/UnexpectedException.h" @@ -189,12 +190,9 @@ 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 %} @@ -226,18 +224,28 @@ namespace storm { while (!statesToExplore.empty()) { StateType currentState = statesToExplore.get(); IndexType currentIndex = getIndex(currentState); + + if (!isTerminalState(currentState)) { #ifndef NDEBUG - std::cout << "Exploring state " << currentState << ", id " << currentIndex << std::endl; + std::cout << "Exploring state " << currentState << ", id " << currentIndex << std::endl; #endif - behaviour.setExpanded(); - exploreNonSynchronizingEdges(currentState, currentIndex, behaviour, statesToExplore); - + behaviour.setExpanded(); + exploreNonSynchronizingEdges(currentState, currentIndex, behaviour, statesToExplore); + } + this->addStateBehaviour(currentIndex, behaviour); behaviour.clear(); } } + bool isTerminalState(StateType const& state) const { + {% for expression in terminalExpressions %}if ({$expression}) { + return true; + } + return false; + } + void exploreNonSynchronizingEdges(StateType const& sourceState, IndexType const& currentIndex, StateBehaviour& behaviour, StateSet& statesToExplore) { {% for edge in nonSynchronizingEdges %}if ({$edge.guard}) { Choice& choice = behaviour.addChoice(); @@ -309,6 +317,8 @@ namespace storm { modelData["nonSynchronizingEdges"] = cpptempl::make_data(nonSynchronizingEdges); cpptempl::data_list labels = generateLabels(); modelData["labels"] = cpptempl::make_data(labels); + cpptempl::data_list terminalExpressions = generateTerminalExpressions(); + modelData["terminalExpressions"] = cpptempl::make_data(terminalExpressions); modelData["deterministic_model"] = model.isDeterministicModel() ? "true" : "false"; modelData["discrete_time_model"] = model.isDiscreteTimeModel() ? "true" : "false"; return cpptempl::parse(sourceTemplate, modelData); @@ -505,6 +515,32 @@ namespace storm { return labels; } + template + cpptempl::data_list ExplicitJitJaniModelBuilder::generateTerminalExpressions() { + cpptempl::data_list terminalExpressions; + + for (auto const& terminalEntry : options.getTerminalStates()) { + LabelOrExpression const& labelOrExpression = terminalEntry.first; + if (labelOrExpression.isLabel()) { + auto const& variables = model.getGlobalVariables(); + STORM_LOG_THROW(variables.hasVariable(labelOrExpression.getLabel()), storm::exceptions::WrongFormatException, "Terminal label refers to unknown identifier '" << labelOrExpression.getLabel() << "'."); + auto const& variable = variables.getVariable(labelOrExpression.getLabel()); + STORM_LOG_THROW(variable.isBooleanVariable(), storm::exceptions::WrongFormatException, "Terminal label refers to non-boolean variable '" << variable.getName() << "."); + STORM_LOG_THROW(variable.isTransient(), storm::exceptions::WrongFormatException, "Terminal label refers to non-transient variable '" << variable.getName() << "."); + auto labelExpression = model.getLabelExpression(variable.asBooleanVariable(), locationVariables); + if (terminalEntry.second) { + labelExpression = !labelExpression; + } + terminalExpressions.push_back(expressionTranslator.translate(labelExpression, storm::expressions::ToCppTranslationOptions("state."))); + } else { + auto expression = terminalEntry.second ? labelOrExpression.getExpression() : !labelOrExpression.getExpression(); + terminalExpressions.push_back(expressionTranslator.translate(expression, storm::expressions::ToCppTranslationOptions("state."))); + } + } + + return terminalExpressions; + } + template cpptempl::data_list ExplicitJitJaniModelBuilder::generateNonSynchronizingEdges() { cpptempl::data_list edges; diff --git a/src/builder/jit/ExplicitJitJaniModelBuilder.h b/src/builder/jit/ExplicitJitJaniModelBuilder.h index 4c182db48..5cc26167f 100644 --- a/src/builder/jit/ExplicitJitJaniModelBuilder.h +++ b/src/builder/jit/ExplicitJitJaniModelBuilder.h @@ -53,6 +53,7 @@ namespace storm { cpptempl::data_list generateInitialStates(); cpptempl::data_map generateStateVariables(); cpptempl::data_list generateLabels(); + cpptempl::data_list generateTerminalExpressions(); cpptempl::data_list generateNonSynchronizingEdges(); cpptempl::data_map generateEdge(storm::jani::Edge const& edge); diff --git a/src/builder/jit/ModelComponentsBuilder.cpp b/src/builder/jit/ModelComponentsBuilder.cpp index 049db264d..64b6be403 100644 --- a/src/builder/jit/ModelComponentsBuilder.cpp +++ b/src/builder/jit/ModelComponentsBuilder.cpp @@ -51,6 +51,7 @@ namespace storm { 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 { transitionMatrixBuilder->addNextValue(currentRow, currentRowGroup, storm::utility::one()); + ++currentRow; } } ++currentRowGroup; diff --git a/src/utility/storm.h b/src/utility/storm.h index a1f6cbef7..9a2c7e080 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -114,6 +114,7 @@ namespace storm { if (storm::settings::getModule().isBuildFullModelSet()) { options.setBuildAllLabels(); options.setBuildAllRewardModels(); + options.clearTerminalStates(); } // Generate command labels if we are going to build a counterexample later.