fixed bug related to input-enabling automata, tests now passing

Former-commit-id: 98512a79f3 [formerly 176a5b5c34]
Former-commit-id: 33fac8df7a

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<storm::dd::Bdd<Type>> guardDisjunction;
                 if (allActionsInputEnabled) {
                     guardDisjunction = this->variables.manager->getBddZero();
@@ -845,7 +845,7 @@ namespace storm {
                 std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> globalVariableToWritingFragment;
                 std::map<storm::expressions::Variable, storm::dd::Bdd<Type>> globalVariableToWritingFragmentWithoutNondeterminism;
                 
-                storm::dd::Bdd<Type> guardConjunction = this->variables.manager->getBddOne();
+                storm::dd::Bdd<Type> inputEnabledGuard = this->variables.manager->getBddOne();
                 storm::dd::Add<Type, ValueType> transitions = this->variables.manager->template getAddOne<ValueType>();
                 std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> 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<storm::expressions::Variable>(this->variables.localNondeterminismVariables.begin() + action.getLowestLocalNondeterminismVariable(), this->variables.localNondeterminismVariables.begin() + action.getHighestLocalNondeterminismVariable());
                     
                     for (auto const& entry : action.variableToWritingFragment) {
-                        storm::dd::Bdd<Type> guardedWritingFragment = guardConjunction && entry.second;
+                        storm::dd::Bdd<Type> 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<ValueType>();
                 }
                 
                 // 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<ValueType>(), transitions * nonSynchronizingAutomataIdentities, transientEdgeAssignments, std::make_pair(lowestNondeterminismVariable, highestNondeterminismVariable), globalVariableToWritingFragment, illegalFragment);
+                return ActionDd(inputEnabledGuard.template toAdd<ValueType>(), transitions * nonSynchronizingAutomataIdentities, transientEdgeAssignments, std::make_pair(lowestNondeterminismVariable, highestNondeterminismVariable), globalVariableToWritingFragment, illegalFragment);
             }
             
             ActionDd combineUnsynchronizedActions(ActionDd action1, ActionDd action2, storm::dd::Add<Type, ValueType> const& identity1, storm::dd::Add<Type, ValueType> 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<Type> 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<Type, ValueType> actionEncoding = encodeAction(action.first != storm::jani::Model::SILENT_ACTION_INDEX ? boost::optional<uint64_t>(action.first) : boost::none, this->variables);
                         storm::dd::Add<Type, ValueType> missingNondeterminismEncoding = encodeIndex(0, action.second.getHighestLocalNondeterminismVariable(), numberOfUsedNondeterminismVariables - action.second.getHighestLocalNondeterminismVariable(), this->variables);
                         storm::dd::Add<Type, ValueType> extendedTransitions = actionEncoding * missingNondeterminismEncoding * action.second.transitions;
-                        
                         for (auto const& transientAssignment : action.second.transientEdgeAssignments) {
                             addToTransientAssignmentMap(transientEdgeAssignments, transientAssignment.first, actionEncoding * missingNondeterminismEncoding * transientAssignment.second);
                         }

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);
                     }
                 }

test/functional/builder/DdJaniModelBuilderTest.cpp

@@ -366,6 +366,62 @@ TEST(DdJaniModelBuilderTest_Cudd, SynchronizationVectors) {
     EXPECT_THROW(newComposition = std::make_shared<storm::jani::ParallelComposition>(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<storm::dd::DdType::Sylvan, double> builder;
+    
+    // Start by checking the original composition.
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> 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<std::shared_ptr<storm::jani::Composition>> automataCompositions;
+    automataCompositions.push_back(std::make_shared<storm::jani::AutomatonComposition>("one"));
+    automataCompositions.push_back(std::make_shared<storm::jani::AutomatonComposition>("two"));
+    automataCompositions.push_back(std::make_shared<storm::jani::AutomatonComposition>("three"));
+    
+    // First, make all actions non-synchronizing.
+    std::vector<storm::jani::SynchronizationVector> synchronizationVectors;
+    std::shared_ptr<storm::jani::Composition> newComposition = std::make_shared<storm::jani::ParallelComposition>(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<std::string> 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<storm::jani::ParallelComposition>(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<storm::jani::ParallelComposition>(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<storm::jani::ParallelComposition>(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<storm::dd::DdType::CUDD, double> builder;
+    
+    // Make some automaton compositions input-enabled.
+    std::vector<std::shared_ptr<storm::jani::Composition>> automataCompositions;
+    automataCompositions.push_back(std::make_shared<storm::jani::AutomatonComposition>("one"));
+    automataCompositions.push_back(std::make_shared<storm::jani::AutomatonComposition>("two"));
+    automataCompositions.push_back(std::make_shared<storm::jani::AutomatonComposition>("three", std::set<std::string>{"a"}));
+
+    // Create the synchronization vectors.
+    std::vector<storm::jani::SynchronizationVector> synchronizationVectors;
+    std::vector<std::string> 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<storm::jani::Composition> newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors);
+    janiModel.setSystemComposition(newComposition);
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> 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<storm::dd::DdType::Sylvan, double> builder;
+    
+    // Make some automaton compositions input-enabled.
+    std::vector<std::shared_ptr<storm::jani::Composition>> automataCompositions;
+    automataCompositions.push_back(std::make_shared<storm::jani::AutomatonComposition>("one"));
+    automataCompositions.push_back(std::make_shared<storm::jani::AutomatonComposition>("two"));
+    automataCompositions.push_back(std::make_shared<storm::jani::AutomatonComposition>("three", std::set<std::string>{"a"}));
+    
+    // Create the synchronization vectors.
+    std::vector<storm::jani::SynchronizationVector> synchronizationVectors;
+    std::vector<std::string> 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<storm::jani::Composition> newComposition = std::make_shared<storm::jani::ParallelComposition>(automataCompositions, synchronizationVectors);
+    janiModel.setSystemComposition(newComposition);
+    std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = builder.build(janiModel);
+    EXPECT_EQ(4ul, model->getNumberOfStates());
+    EXPECT_EQ(5ul, model->getNumberOfTransitions());
+}

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]

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; i<stateActionEntries; ++i){
-            double evaluatedValue = carl::toDouble(dtmc->getUniqueRewardModel()->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());