From 7f8a830b5a6675d9c4dcd2ed5d4927667b170a4e Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Wed, 16 May 2018 16:02:20 +0200
Subject: [PATCH] refined detection of trivial initial states restriction of
 JANI models

---
 src/storm/storage/jani/Automaton.cpp | 2 +-
 src/storm/storage/jani/Model.cpp     | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp
index 88f5f0489..060ae4e9b 100644
--- a/src/storm/storage/jani/Automaton.cpp
+++ b/src/storm/storage/jani/Automaton.cpp
@@ -328,7 +328,7 @@ namespace storm {
             storm::expressions::Expression result;
             
             // Add initial state restriction if there is one.
-            if (this->hasInitialStatesRestriction()) {
+            if (this->hasInitialStatesRestriction() && !this->getInitialStatesRestriction().isTrue()) {
                 result = this->getInitialStatesRestriction();
             }
             
diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp
index 8da333cb7..bec06e9b3 100644
--- a/src/storm/storage/jani/Model.cpp
+++ b/src/storm/storage/jani/Model.cpp
@@ -929,7 +929,7 @@ namespace storm {
         }
         
         bool Model::hasTrivialInitialStatesExpression() const {
-            if (this->hasInitialStatesRestriction()) {
+            if (this->hasInitialStatesRestriction() && !this->getInitialStatesRestriction().isTrue()) {
                 return false;
             }