From 6102fd27ae469990bfaed50888c80011b7aba635 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 4 Oct 2018 10:26:32 +0200 Subject: [PATCH] Subsystembuilder can now handle deadlock states --- src/storm/transformer/SubsystemBuilder.cpp | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/storm/transformer/SubsystemBuilder.cpp b/src/storm/transformer/SubsystemBuilder.cpp index b8ba5f0e3..cfeba6b0e 100644 --- a/src/storm/transformer/SubsystemBuilder.cpp +++ b/src/storm/transformer/SubsystemBuilder.cpp @@ -65,7 +65,6 @@ namespace storm { result.keptActions = storm::storage::BitVector(originalModel.getTransitionMatrix().getRowCount(), false); for (auto subsysState : subsystemStates) { result.newToOldStateIndexMapping.push_back(subsysState); - bool stateHasOneChoiceLeft = false; for (uint_fast64_t row = subsystemActions.getNextSetIndex(originalModel.getTransitionMatrix().getRowGroupIndices()[subsysState]); row < originalModel.getTransitionMatrix().getRowGroupIndices()[subsysState+1]; row = subsystemActions.getNextSetIndex(row+1)) { bool allRowEntriesStayInSubsys = true; for (auto const& entry : originalModel.getTransitionMatrix().getRow(row)) { @@ -74,10 +73,8 @@ namespace storm { break; } } - stateHasOneChoiceLeft |= allRowEntriesStayInSubsys; result.keptActions.set(row, allRowEntriesStayInSubsys); } - STORM_LOG_THROW(stateHasOneChoiceLeft, storm::exceptions::InvalidArgumentException, "The subsystem would contain a deadlock state."); } // Transform the components of the model