terminal states now supported by jit-based builder

Former-commit-id: bf4eb4654d [formerly 5d2f364967]
Former-commit-id: 84aa362762

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;
 #endif
                                         
                                             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<IndexType, ValueType>& behaviour, StateSet& statesToExplore) {
                                     {% for edge in nonSynchronizingEdges %}if ({$edge.guard}) {
                                         Choice<IndexType, ValueType>& 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 <typename ValueType, typename RewardModelType>
+            cpptempl::data_list ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::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 <typename ValueType, typename RewardModelType>
             cpptempl::data_list ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateNonSynchronizingEdges() {
                 cpptempl::data_list edges;

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);

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<ValueType>());
+                        ++currentRow;
                     }
                 }
                 ++currentRowGroup;

src/utility/storm.h

@@ -114,6 +114,7 @@ namespace storm {
         if (storm::settings::getModule<storm::settings::modules::IOSettings>().isBuildFullModelSet()) {
             options.setBuildAllLabels();
             options.setBuildAllRewardModels();
+            options.clearTerminalStates();
         }
 
         // Generate command labels if we are going to build a counterexample later.