Progress with SPARE implementation

Former-commit-id: 18343684fa

examples/dft/and_3_inputs.dft

@@ -1,5 +0,0 @@
-toplevel "A";
-"A" and "B" "C" "D";
-"B" lambda=0.5 dorm=0.2;
-"C" lambda=0.4 dorm=0.1;
-"D" lambda=0.3 dorm=0.05;

examples/dft/and_or_mix.dft

@@ -1,9 +0,0 @@
-toplevel "A";
-"A" and "B" "C";
-"B" or "BE1" "BE2";
-"C" and "BE3" "D";
-"D" or "BE1" "BE4";
-"BE1" lambda=0.5 dorm=0.3;
-"BE2" lambda=0.5 dorm=0.3;
-"BE3" lambda=0.5 dorm=0.3;
-"BE4" lambda=0.5 dorm=0.3;

examples/dft/be.dft

@@ -1,2 +0,0 @@
-toplevel "A";
-"A" lambda=0.5 dorm=0.3;

examples/dft/pand2.dft

@@ -1,6 +0,0 @@
-toplevel "A";
-"A" pand "B" "C" "D" "E";
-"B" lambda=0.4 dorm=0.3;
-"C" lambda=0.2 dorm=0.3;
-"D" lambda=0.1 dorm=0.3;
-"E" lambda=0.05 dorm=0.3;

examples/dft/pdep5.dft

@@ -1,5 +0,0 @@
-toplevel "A";
-"A" and "B" "C";
-"PDEP" pdep=0.2 "B" "C";
-"B" lambda=0.5 dorm=0;
-"C" lambda=0.5 dorm=0;

examples/dft/por2.dft

@@ -1,4 +0,0 @@
-toplevel "A";
-"A" por "B" "C";
-"B" lambda=0.4 dorm=0.0;
-"C" lambda=0.2 dorm=0.0;

examples/dft/por_mix.dft

@@ -1,6 +0,0 @@
-toplevel "A";
-"A" por "B" "C" "D";
-"B" and "C" "E";
-"C" lambda=0.2 dorm=0.0;
-"D" lambda=0.2 dorm=0.0;
-"E" lambda=0.2 dorm=0.0;

examples/dft/seq6.dft

@@ -1,7 +0,0 @@
-toplevel "A";
-"A" and "B" "C";
-"X" seq "B" "C"
-"B" lambda=0.5 dorm=0.3;
-"C" and "D" "E";
-"D" lambda=0.5 dorm=0.3;
-"E" lambda=0.5 dorm=0.3;

examples/dft/voting3.dft

@@ -1,11 +0,0 @@
-toplevel "A";
-"A" 5of9 "B" "C" "D" "E" "F" "G" "H" "I" "J";
-"B" lambda=0.1 dorm=0;
-"C" lambda=0.2 dorm=0;
-"D" lambda=0.3 dorm=0;
-"E" lambda=0.4 dorm=0;
-"F" lambda=0.5 dorm=0;
-"G" lambda=0.5 dorm=0;
-"H" lambda=0.5 dorm=0;
-"I" lambda=0.5 dorm=0;
-"J" lambda=0.5 dorm=0;

examples/dft/voting_mix.dft

@@ -1,9 +0,0 @@
-toplevel "A";
-"A" and "B" "F";
-"B" 2of3 "C" "D" "E";
-"C" lambda=0.1 dorm=0;
-"D" lambda=0.2 dorm=0;
-"E" lambda=0.3 dorm=0;
-"F" 2of3 "G" "H" "C";
-"G" lambda=0.4 dorm=0;
-"H" lambda=0.5 dorm=0;

src/transformations/dft/DftToGspnTransformator.cpp

@@ -241,7 +241,7 @@ namespace storm {
 						mGspn.addPlace(placeChildClaimed);
 						
 						storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionSpareChildActivating;
-						immediateTransitionSpareChildActivating.setName(dftSpare->children()[i]->name() + STR_ACTIVATING);
+						immediateTransitionSpareChildActivating.setName(children[i]->name() + STR_ACTIVATING);
 						immediateTransitionSpareChildActivating.setPriority(priority);
 						immediateTransitionSpareChildActivating.setWeight(0.0);
 						immediateTransitionSpareChildActivating.setInputArcMultiplicity(placeChildClaimed, 1);
@@ -256,13 +256,27 @@ namespace storm {
 					placeSPAREClaimedChild.setNumberOfInitialTokens(0);
 					mGspn.addPlace(placeSPAREClaimedChild);
 					
+					storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionChildClaiming;
+					immediateTransitionChildClaiming.setName(children[i]->name() + "_claiming");
+					immediateTransitionChildClaiming.setPriority(priority + 1); // Higher priority needed!
+					immediateTransitionChildClaiming.setWeight(0.0);
+					immediateTransitionChildClaiming.setInhibitionArcMultiplicity(placeChildClaimedExist.second, 1);
+					immediateTransitionChildClaiming.setOutputArcMultiplicity(placeChildClaimedExist.second, 1);
+					immediateTransitionChildClaiming.setOutputArcMultiplicity(placeSPAREClaimedChild, 1);
+					mGspn.addImmediateTransition(immediateTransitionChildClaiming);
+					
 					storm::gspn::Place placeSPAREChildConsumed;
-					placeSPAREChildConsumed.setName(children[i]->name() + "_consumed"); // TODO: If its the last child, this label must be "SPARE_failed".
+					if (i < children.size() - 1) {
+						placeSPAREChildConsumed.setName(children[i]->name() + "_consumed");
+					}
+					else {
+						placeSPAREChildConsumed.setName(dftSpare->name() + STR_FAILED);
+					}
 					placeSPAREChildConsumed.setNumberOfInitialTokens(0);
 					mGspn.addPlace(placeSPAREChildConsumed);
 					
 					storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionChildConsuming1;
-					immediateTransitionChildConsuming1.setName(dftSpare->children()[i]->name() + "_consuming1");
+					immediateTransitionChildConsuming1.setName(children[i]->name() + "_consuming1");
 					immediateTransitionChildConsuming1.setPriority(priority);
 					immediateTransitionChildConsuming1.setWeight(0.0);
 					immediateTransitionChildConsuming1.setOutputArcMultiplicity(placeSPAREChildConsumed, 1);
@@ -271,7 +285,7 @@ namespace storm {
 					mGspn.addImmediateTransition(immediateTransitionChildConsuming1);
 					
 					storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionChildConsuming2;
-					immediateTransitionChildConsuming2.setName(dftSpare->children()[i]->name() + "_consuming2");
+					immediateTransitionChildConsuming2.setName(children[i]->name() + "_consuming2");
 					immediateTransitionChildConsuming2.setPriority(priority);
 					immediateTransitionChildConsuming2.setWeight(0.0);
 					immediateTransitionChildConsuming2.setOutputArcMultiplicity(placeSPAREChildConsumed, 1);
@@ -734,6 +748,20 @@ namespace storm {
 				}
 			}
 			
+			template <typename ValueType>
+            std::vector<int> DftToGspnTransformator<ValueType>::getAllBEIDsOfElement(std::vector<int> ids, std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement) {
+				std::vector<int> newIds;
+				
+				if (dftElement->type() == storm::storage::DFTElementType::BE) {
+					newIds.push_back(dftElement->id());
+				}
+				else {
+					// TODO: Check all children: If they are BEs, add them to the list. Else, check the children again.
+				}
+				
+				return newIds;
+			}
+			
 			template <typename ValueType>
             void DftToGspnTransformator<ValueType>::writeGspn(bool toFile) {
                 if (toFile) {

src/transformations/dft/DftToGspnTransformator.h

@@ -199,6 +199,13 @@ namespace storm {
 				  * @param dftElement The element whose priority shall be determined.
 				  */
 				 uint_fast64_t getPriority(uint_fast64_t priority, std::shared_ptr<storm::storage::DFTElement<ValueType> const> dFTElement);
+				 
+				 /*
+				  * Return all ids of BEs, that are successors of the given element.
+				  * 
+				  * @param dftElement The element which 
+				  */
+				 std::vector<int> getAllBEIDsOfElement(std::vector<int> ids, std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement);
             };
         }
     }