added check to symbolic JANI model builder

Former-commit-id: ef32d63e2f [formerly d41759397f]
Former-commit-id: 36b407f684

src/builder/DdJaniModelBuilder.cpp

@@ -188,6 +188,8 @@ namespace storm {
                 this->model.getSystemComposition().accept(*this, boost::none);
                 STORM_LOG_THROW(automata.size() == this->model.getNumberOfAutomata(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model whose system composition refers to a subset of automata.");
                 
+                STORM_LOG_THROW(!this->model.hasTransientEdgeDestinationAssignments(), storm::exceptions::InvalidArgumentException, "The symbolic JANI model builder currently does not support transient edge destination assignments.");
+                
                 // Then, check that the model does not contain non-transient unbounded integer or non-transient real variables.
                 STORM_LOG_THROW(!this->model.getGlobalVariables().containsNonTransientUnboundedIntegerVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains non-transient global unbounded integer variables.");
                 STORM_LOG_THROW(!this->model.getGlobalVariables().containsNonTransientRealVariables(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model that contains global non-transient real variables.");

src/storage/SymbolicModelDescription.cpp

@@ -73,8 +73,10 @@ namespace storm {
                 std::map<storm::expressions::Variable, storm::expressions::Expression> substitution = storm::utility::jani::parseConstantDefinitionString(this->asJaniModel(), constantDefinitionString);
                 storm::jani::Model preparedModel = this->asJaniModel().defineUndefinedConstants(substitution).substituteConstants();
                 if (preparedModel.hasTransientEdgeDestinationAssignments()) {
-                    STORM_LOG_WARN("JANI model has transient edge-destinations assignments, which are currently not supported. Trying to lift these assignments to edges rather than destinations.");
                     preparedModel.liftTransientEdgeDestinationAssignments();
+                    if (preparedModel.hasTransientEdgeDestinationAssignments()) {
+                        STORM_LOG_WARN("JANI model has non-liftable transient edge-destinations assignments, which are currently not supported. Trying to lift these assignments to edges rather than destinations failed.");
+                    }
                 }
                 return SymbolicModelDescription(preparedModel);
             } else if (this->isPrismProgram()) {