diff --git a/examples/dft/pand_param.dft b/examples/dft/pand_param.dft new file mode 100644 index 000000000..9a0b3d211 --- /dev/null +++ b/examples/dft/pand_param.dft @@ -0,0 +1,6 @@ +param x; +param y; +toplevel "A"; +"A" pand "B" "C"; +"B" lambda=x dorm=0.3; +"C" lambda=y dorm=0.3; diff --git a/examples/dft/tripple_pand.dft b/examples/dft/tripple_pand.dft new file mode 100644 index 000000000..7b38cf0f1 --- /dev/null +++ b/examples/dft/tripple_pand.dft @@ -0,0 +1,9 @@ +toplevel "A"; +"A" pand "B" "BE4"; +"B" pand "C" "BE3"; +"C" pand "BE1" "BE2"; +"BE1" lambda=0.5 dorm=3; +"BE2" lambda=0.5 dorm=3; +"BE3" lambda=0.5 dorm=3; +"BE4" lambda=0.5 dorm=3; + diff --git a/examples/dft/tripple_pand2.dft b/examples/dft/tripple_pand2.dft new file mode 100644 index 000000000..4e6ef460f --- /dev/null +++ b/examples/dft/tripple_pand2.dft @@ -0,0 +1,8 @@ +toplevel "A"; +"A" pand "B" "C"; +"B" pand "BE1" "BE2"; +"C" pand "BE2" "BE3"; +"BE1" lambda=0.5 dorm=3; +"BE2" lambda=0.5 dorm=3; +"BE3" lambda=0.5 dorm=3; + diff --git a/examples/dft/tripple_pand2_c.dft b/examples/dft/tripple_pand2_c.dft new file mode 100644 index 000000000..1c6001ea4 --- /dev/null +++ b/examples/dft/tripple_pand2_c.dft @@ -0,0 +1,6 @@ +toplevel "A"; +"A" pand "BE1" "BE2" "BE3"; +"BE1" lambda=0.5 dorm=3; +"BE2" lambda=0.5 dorm=3; +"BE3" lambda=0.5 dorm=3; + diff --git a/examples/dft/tripple_pand_c.dft b/examples/dft/tripple_pand_c.dft new file mode 100644 index 000000000..bfb8daa1c --- /dev/null +++ b/examples/dft/tripple_pand_c.dft @@ -0,0 +1,7 @@ +toplevel "A"; +"A" pand "BE1" "BE2" "BE3" "BE4"; +"BE1" lambda=0.5 dorm=3; +"BE2" lambda=0.5 dorm=3; +"BE3" lambda=0.5 dorm=3; +"BE4" lambda=0.5 dorm=3; + diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp index c0c596b02..0d37e795f 100644 --- a/src/builder/ExplicitDFTModelBuilder.cpp +++ b/src/builder/ExplicitDFTModelBuilder.cpp @@ -62,12 +62,8 @@ namespace storm { } } - // TODO Matthias: initialize - modelComponents.rewardModels; - modelComponents.choiceLabeling; - std::shared_ptr> model; - model = std::shared_ptr>(new storm::models::sparse::Ctmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling))); + model = std::shared_ptr>(new storm::models::sparse::Ctmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling))); model->printModelInformationToStream(std::cout); return model; } @@ -149,10 +145,16 @@ namespace storm { } // Set transition - ValueType prob = nextBE.first->activeFailureRate(); - auto resultInsert = outgoingTransitions.insert(std::make_pair(it->getId(), prob)); - assert(resultInsert.second); - sum += prob; + ValueType rate = nextBE.first->activeFailureRate(); + auto resultFind = outgoingTransitions.find(it->getId()); + if (resultFind != outgoingTransitions.end()) { + // Add to existing transition + resultFind->second += rate; + } else { + // Insert new transition + outgoingTransitions.insert(std::make_pair(it->getId(), rate)); + } + sum += rate; } // end while failing BE // Add all transitions