Browse Source

refined detection of trivial initial states restriction of JANI models

main
dehnert 7 years ago
parent
commit
7f8a830b5a
  1. 2
      src/storm/storage/jani/Automaton.cpp
  2. 2
      src/storm/storage/jani/Model.cpp

2
src/storm/storage/jani/Automaton.cpp

@ -328,7 +328,7 @@ namespace storm {
storm::expressions::Expression result; storm::expressions::Expression result;
// Add initial state restriction if there is one. // Add initial state restriction if there is one.
if (this->hasInitialStatesRestriction()) {
if (this->hasInitialStatesRestriction() && !this->getInitialStatesRestriction().isTrue()) {
result = this->getInitialStatesRestriction(); result = this->getInitialStatesRestriction();
} }

2
src/storm/storage/jani/Model.cpp

@ -929,7 +929,7 @@ namespace storm {
} }
bool Model::hasTrivialInitialStatesExpression() const { bool Model::hasTrivialInitialStatesExpression() const {
if (this->hasInitialStatesRestriction()) {
if (this->hasInitialStatesRestriction() && !this->getInitialStatesRestriction().isTrue()) {
return false; return false;
} }

Loading…
Cancel
Save