From 0f1c1f28ab25705f307ef01440b39631cd6015e4 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 24 Sep 2016 13:19:21 +0200 Subject: [PATCH] fixed bug related to input-enabling automata, tests now passing Former-commit-id: 98512a79f344e55c9614fbea161b00617e1c898a [formerly 176a5b5c3490364c5f5e916756822063fa211e2d] Former-commit-id: 33fac8df7a5cd0e0bac4f68762f1d085a4557583 --- src/builder/DdJaniModelBuilder.cpp | 33 +++-- src/storage/jani/ParallelComposition.cpp | 2 +- .../builder/DdJaniModelBuilderTest.cpp | 119 ++++++++++++++++++ test/functional/builder/SmallPrismTest.nm | 3 +- .../utility/ModelInstantiatorTest.cpp | 16 +-- 5 files changed, 151 insertions(+), 22 deletions(-) diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index ee1f0d669..a4dae2fbb 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -815,7 +815,7 @@ namespace storm { result.extendLocalNondeterminismVariables(actionDds.front().getLocalNondeterminismVariables()); } } - + return result; } @@ -831,9 +831,9 @@ namespace storm { auto const& action = actionIdentityPair.first; if (!action.isInputEnabled()) { allActionsInputEnabled = false; - break; } } + boost::optional> guardDisjunction; if (allActionsInputEnabled) { guardDisjunction = this->variables.manager->getBddZero(); @@ -845,7 +845,7 @@ namespace storm { std::map> globalVariableToWritingFragment; std::map> globalVariableToWritingFragmentWithoutNondeterminism; - storm::dd::Bdd guardConjunction = this->variables.manager->getBddOne(); + storm::dd::Bdd inputEnabledGuard = this->variables.manager->getBddOne(); storm::dd::Add transitions = this->variables.manager->template getAddOne(); std::map> transientEdgeAssignments; @@ -867,6 +867,7 @@ namespace storm { if (action.isInputEnabled()) { // If the action is input-enabled, we add self-loops to all states. transitions *= actionGuard.ite(action.transitions, encodeIndex(0, action.getLowestLocalNondeterminismVariable(), action.getHighestLocalNondeterminismVariable() - action.getLowestLocalNondeterminismVariable(), this->variables) * actionIdentityPair.second); + actionGuard.ite(action.transitions, encodeIndex(0, action.getLowestLocalNondeterminismVariable(), action.getHighestLocalNondeterminismVariable() - action.getLowestLocalNondeterminismVariable(), this->variables) * actionIdentityPair.second).exportToDot("this.dot"); } else { transitions *= action.transitions; } @@ -875,13 +876,13 @@ namespace storm { auto nondetVariables = std::set(this->variables.localNondeterminismVariables.begin() + action.getLowestLocalNondeterminismVariable(), this->variables.localNondeterminismVariables.begin() + action.getHighestLocalNondeterminismVariable()); for (auto const& entry : action.variableToWritingFragment) { - storm::dd::Bdd guardedWritingFragment = guardConjunction && entry.second; + storm::dd::Bdd guardedWritingFragment = inputEnabledGuard && entry.second; // Check whether there already is an entry for this variable in the mapping of global variables // to their writing fragments. auto globalFragmentIt = globalVariableToWritingFragment.find(entry.first); if (globalFragmentIt != globalVariableToWritingFragment.end()) { - // If it does, take the conjunction of the entries and also of their versions without nondeterminism + // If there is, take the conjunction of the entries and also of their versions without nondeterminism // variables. globalFragmentIt->second &= guardedWritingFragment; illegalFragment |= globalVariableToWritingFragmentWithoutNondeterminism[entry.first] && guardedWritingFragment.existsAbstract(nondetVariables); @@ -899,21 +900,30 @@ namespace storm { } // Now go through all fragments that are not written by the current action and join them with the - // guard of the current action. + // guard of the current action if the current action is not input enabled. for (auto& entry : globalVariableToWritingFragment) { - if (action.variableToWritingFragment.find(entry.first) == action.variableToWritingFragment.end()) { + if (action.variableToWritingFragment.find(entry.first) == action.variableToWritingFragment.end() && !action.isInputEnabled()) { entry.second &= actionGuard; } } - guardConjunction &= actionGuard; + if (!action.isInputEnabled()) { + inputEnabledGuard &= actionGuard; + } + } + + // If all actions were input-enabled, we need to constrain the transitions with the disjunction of all + // guards to make sure there are not transitions resulting from input enabledness alone. + if (allActionsInputEnabled) { + inputEnabledGuard &= guardDisjunction.get(); + transitions *= guardDisjunction.get().template toAdd(); } // Cut the union of the illegal fragments to the conjunction of the guards since only these states have // such a combined transition. - illegalFragment &= guardConjunction; + illegalFragment &= inputEnabledGuard; - return ActionDd(guardConjunction.template toAdd(), transitions * nonSynchronizingAutomataIdentities, transientEdgeAssignments, std::make_pair(lowestNondeterminismVariable, highestNondeterminismVariable), globalVariableToWritingFragment, illegalFragment); + return ActionDd(inputEnabledGuard.template toAdd(), transitions * nonSynchronizingAutomataIdentities, transientEdgeAssignments, std::make_pair(lowestNondeterminismVariable, highestNondeterminismVariable), globalVariableToWritingFragment, illegalFragment); } ActionDd combineUnsynchronizedActions(ActionDd action1, ActionDd action2, storm::dd::Add const& identity1, storm::dd::Add const& identity2) { @@ -951,6 +961,7 @@ namespace storm { } // Bring all actions to the same number of variables that encode the nondeterminism. + int i = 0; for (auto& action : actions) { storm::dd::Bdd nondeterminismEncodingBdd = this->variables.manager->getBddOne(); for (uint_fast64_t i = action.getHighestLocalNondeterminismVariable(); i < highestLocalNondeterminismVariable; ++i) { @@ -1454,6 +1465,7 @@ namespace storm { if (inputEnabledActionIndices.find(actionIndex) != inputEnabledActionIndices.end()) { actionDd.setIsInputEnabled(); } + result.actionIndexToAction[actionIndex] = actionDd; result.setLowestLocalNondeterminismVariable(std::max(result.getLowestLocalNondeterminismVariable(), actionDd.getLowestLocalNondeterminismVariable())); result.setHighestLocalNondeterminismVariable(std::max(result.getHighestLocalNondeterminismVariable(), actionDd.getHighestLocalNondeterminismVariable())); @@ -1509,7 +1521,6 @@ namespace storm { storm::dd::Add actionEncoding = encodeAction(action.first != storm::jani::Model::SILENT_ACTION_INDEX ? boost::optional(action.first) : boost::none, this->variables); storm::dd::Add missingNondeterminismEncoding = encodeIndex(0, action.second.getHighestLocalNondeterminismVariable(), numberOfUsedNondeterminismVariables - action.second.getHighestLocalNondeterminismVariable(), this->variables); storm::dd::Add extendedTransitions = actionEncoding * missingNondeterminismEncoding * action.second.transitions; - for (auto const& transientAssignment : action.second.transientEdgeAssignments) { addToTransientAssignmentMap(transientEdgeAssignments, transientAssignment.first, actionEncoding * missingNondeterminismEncoding * transientAssignment.second); } diff --git a/src/storage/jani/ParallelComposition.cpp b/src/storage/jani/ParallelComposition.cpp index 597518d37..aad0e2d3d 100644 --- a/src/storage/jani/ParallelComposition.cpp +++ b/src/storage/jani/ParallelComposition.cpp @@ -182,7 +182,7 @@ namespace storm { STORM_LOG_THROW(vector.size() == this->subcompositions.size(), storm::exceptions::WrongFormatException, "Synchronization vectors must match parallel composition size."); std::string const& action = vector.getInput(inputIndex); if (action != SynchronizationVector::NO_ACTION_INPUT) { - STORM_LOG_THROW(actions.find(action) == actions.end(), storm::exceptions::WrongFormatException, "Cannot use the same action multiple times as input in synchronization vectors."); + STORM_LOG_THROW(actions.find(action) == actions.end(), storm::exceptions::WrongFormatException, "Cannot use the same action ('" << action << "') multiple times as input for index " << inputIndex << " in synchronization vectors."); actions.insert(action); } } diff --git a/test/functional/builder/DdJaniModelBuilderTest.cpp b/test/functional/builder/DdJaniModelBuilderTest.cpp index 4f343ec88..20602d97f 100644 --- a/test/functional/builder/DdJaniModelBuilderTest.cpp +++ b/test/functional/builder/DdJaniModelBuilderTest.cpp @@ -366,6 +366,62 @@ TEST(DdJaniModelBuilderTest_Cudd, SynchronizationVectors) { EXPECT_THROW(newComposition = std::make_shared(automataCompositions, synchronizationVectors), storm::exceptions::WrongFormatException); } +TEST(DdJaniModelBuilderTest_Sylvan, SynchronizationVectors) { + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/SmallPrismTest.nm"); + storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + + storm::builder::DdJaniModelBuilder builder; + + // Start by checking the original composition. + std::shared_ptr> model = builder.build(janiModel); + EXPECT_EQ(7ul, model->getNumberOfStates()); + EXPECT_EQ(10ul, model->getNumberOfTransitions()); + + // Now we tweak it's system composition to check whether synchronization vectors work. + std::vector> automataCompositions; + automataCompositions.push_back(std::make_shared("one")); + automataCompositions.push_back(std::make_shared("two")); + automataCompositions.push_back(std::make_shared("three")); + + // First, make all actions non-synchronizing. + std::vector synchronizationVectors; + std::shared_ptr newComposition = std::make_shared(automataCompositions, synchronizationVectors); + janiModel.setSystemComposition(newComposition); + model = builder.build(janiModel); + EXPECT_EQ(24ul, model->getNumberOfStates()); + EXPECT_EQ(48ul, model->getNumberOfTransitions()); + + // Then, make only a, b and c synchronize. + std::vector inputVector; + inputVector.push_back("a"); + inputVector.push_back("b"); + inputVector.push_back("c"); + synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d")); + newComposition = std::make_shared(automataCompositions, synchronizationVectors); + janiModel.setSystemComposition(newComposition); + model = builder.build(janiModel); + EXPECT_EQ(7ul, model->getNumberOfStates()); + EXPECT_EQ(10ul, model->getNumberOfTransitions()); + + inputVector.clear(); + inputVector.push_back("c"); + inputVector.push_back("c"); + inputVector.push_back("a"); + synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d")); + newComposition = std::make_shared(automataCompositions, synchronizationVectors); + janiModel.setSystemComposition(newComposition); + model = builder.build(janiModel); + EXPECT_EQ(3ul, model->getNumberOfStates()); + EXPECT_EQ(3ul, model->getNumberOfTransitions()); + + inputVector.clear(); + inputVector.push_back("b"); + inputVector.push_back("c"); + inputVector.push_back("b"); + synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "e")); + EXPECT_THROW(newComposition = std::make_shared(automataCompositions, synchronizationVectors), storm::exceptions::WrongFormatException); +} + TEST(DdJaniModelBuilderTest_Sylvan, Composition) { storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm"); storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); @@ -416,3 +472,66 @@ TEST(DdJaniModelBuilderTest_Cudd, Composition) { EXPECT_EQ(21ul, mdp->getNumberOfChoices()); } +TEST(DdJaniModelBuilderTest_Cudd, InputEnabling) { + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/SmallPrismTest2.nm"); + storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + + storm::builder::DdJaniModelBuilder builder; + + // Make some automaton compositions input-enabled. + std::vector> automataCompositions; + automataCompositions.push_back(std::make_shared("one")); + automataCompositions.push_back(std::make_shared("two")); + automataCompositions.push_back(std::make_shared("three", std::set{"a"})); + + // Create the synchronization vectors. + std::vector synchronizationVectors; + std::vector inputVector; + inputVector.push_back("a"); + inputVector.push_back("b"); + inputVector.push_back("c"); + synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d")); + inputVector.clear(); + inputVector.push_back("c"); + inputVector.push_back("c"); + inputVector.push_back("a"); + synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d")); + + std::shared_ptr newComposition = std::make_shared(automataCompositions, synchronizationVectors); + janiModel.setSystemComposition(newComposition); + std::shared_ptr> model = builder.build(janiModel); + EXPECT_EQ(4ul, model->getNumberOfStates()); + EXPECT_EQ(5ul, model->getNumberOfTransitions()); +} + +TEST(DdJaniModelBuilderTest_Sylvan, InputEnabling) { + storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/SmallPrismTest2.nm"); + storm::jani::Model janiModel = modelDescription.toJani(true).preprocess().asJaniModel(); + + storm::builder::DdJaniModelBuilder builder; + + // Make some automaton compositions input-enabled. + std::vector> automataCompositions; + automataCompositions.push_back(std::make_shared("one")); + automataCompositions.push_back(std::make_shared("two")); + automataCompositions.push_back(std::make_shared("three", std::set{"a"})); + + // Create the synchronization vectors. + std::vector synchronizationVectors; + std::vector inputVector; + inputVector.push_back("a"); + inputVector.push_back("b"); + inputVector.push_back("c"); + synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d")); + inputVector.clear(); + inputVector.push_back("c"); + inputVector.push_back("c"); + inputVector.push_back("a"); + synchronizationVectors.push_back(storm::jani::SynchronizationVector(inputVector, "d")); + + std::shared_ptr newComposition = std::make_shared(automataCompositions, synchronizationVectors); + janiModel.setSystemComposition(newComposition); + std::shared_ptr> model = builder.build(janiModel); + EXPECT_EQ(4ul, model->getNumberOfStates()); + EXPECT_EQ(5ul, model->getNumberOfTransitions()); +} diff --git a/test/functional/builder/SmallPrismTest.nm b/test/functional/builder/SmallPrismTest.nm index 9d33b5c89..399635ee9 100644 --- a/test/functional/builder/SmallPrismTest.nm +++ b/test/functional/builder/SmallPrismTest.nm @@ -19,9 +19,8 @@ module two endmodule module three - s3 : [0 .. 1]; + s3 : [0 .. 2]; [c] s3=0 -> (s3'=1); endmodule -// (one || two || three)[(a, b, c) -> d, (c, c, a) -> a] diff --git a/test/functional/utility/ModelInstantiatorTest.cpp b/test/functional/utility/ModelInstantiatorTest.cpp index d1319613c..62cdb8c68 100644 --- a/test/functional/utility/ModelInstantiatorTest.cpp +++ b/test/functional/utility/ModelInstantiatorTest.cpp @@ -183,15 +183,15 @@ TEST(ModelInstantiatorTest, Brp_Rew) { } } ASSERT_TRUE(instantiated.hasUniqueRewardModel()); - EXPECT_FALSE(instantiated.getUniqueRewardModel()->second.hasStateRewards()); - EXPECT_FALSE(instantiated.getUniqueRewardModel()->second.hasTransitionRewards()); - EXPECT_TRUE(instantiated.getUniqueRewardModel()->second.hasStateActionRewards()); - ASSERT_TRUE(dtmc->getUniqueRewardModel()->second.hasStateActionRewards()); - std::size_t stateActionEntries = dtmc->getUniqueRewardModel()->second.getStateActionRewardVector().size(); - ASSERT_EQ(stateActionEntries, instantiated.getUniqueRewardModel()->second.getStateActionRewardVector().size()); + EXPECT_FALSE(instantiated.getUniqueRewardModel().hasStateRewards()); + EXPECT_FALSE(instantiated.getUniqueRewardModel().hasTransitionRewards()); + EXPECT_TRUE(instantiated.getUniqueRewardModel().hasStateActionRewards()); + ASSERT_TRUE(dtmc->getUniqueRewardModel().hasStateActionRewards()); + std::size_t stateActionEntries = dtmc->getUniqueRewardModel().getStateActionRewardVector().size(); + ASSERT_EQ(stateActionEntries, instantiated.getUniqueRewardModel().getStateActionRewardVector().size()); for(std::size_t i =0; igetUniqueRewardModel()->second.getStateActionRewardVector()[i].evaluate(valuation)); - EXPECT_EQ(evaluatedValue, instantiated.getUniqueRewardModel()->second.getStateActionRewardVector()[i]); + double evaluatedValue = carl::toDouble(dtmc->getUniqueRewardModel().getStateActionRewardVector()[i].evaluate(valuation)); + EXPECT_EQ(evaluatedValue, instantiated.getUniqueRewardModel().getStateActionRewardVector()[i]); } EXPECT_EQ(dtmc->getStateLabeling(), instantiated.getStateLabeling()); EXPECT_EQ(dtmc->getOptionalChoiceLabeling(), instantiated.getOptionalChoiceLabeling());