From f76760441ee7034067b2035df3e7445c0da9efd2 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 30 Sep 2016 16:01:55 +0200 Subject: [PATCH] added check to symbolic JANI model builder Former-commit-id: ef32d63e2f79d6034ff0d8185998cb496329cb1e [formerly d41759397f0aa7e4afbd9f733480e71ded1227c1] Former-commit-id: 36b407f68474cd817599bd08a62605236c25b025 --- src/builder/DdJaniModelBuilder.cpp | 2 ++ src/storage/SymbolicModelDescription.cpp | 4 +++- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index 0c467b3f1..325cfb3a5 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/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."); diff --git a/src/storage/SymbolicModelDescription.cpp b/src/storage/SymbolicModelDescription.cpp index ccbb7c25b..4c144eff8 100644 --- a/src/storage/SymbolicModelDescription.cpp +++ b/src/storage/SymbolicModelDescription.cpp @@ -73,8 +73,10 @@ namespace storm { std::map 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()) {