From 32e3661bd23a7fb9838a932e244391e13873d98a Mon Sep 17 00:00:00 2001 From: Jip Spel Date: Tue, 12 Nov 2019 10:59:32 +0100 Subject: [PATCH] Fix adding same state twice to Order --- src/storm-pars/analysis/OrderExtender.cpp | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/src/storm-pars/analysis/OrderExtender.cpp b/src/storm-pars/analysis/OrderExtender.cpp index 636dd8913..ebf8dc1eb 100644 --- a/src/storm-pars/analysis/OrderExtender.cpp +++ b/src/storm-pars/analysis/OrderExtender.cpp @@ -196,7 +196,18 @@ namespace storm { order->addBetween(max, order->getTop(), order->getNode(min)); } assert (order->compare(max, min) == Order::ABOVE); - order->addBetween(state, max, min); + if (order->contains(state)) { + if (order->compare(max, state) == Order::UNKNOWN) { + order->addRelation(max, state); + } + if (order->compare(state, min) == Order::UNKNOWN) { + order->addRelation(state, min); + } + } else { + order->addBetween(state, max, min); + } + assert (order->compare(max, state) == Order::ABOVE); + assert (order->compare(state, min) == Order::ABOVE); } } }