From d6b7331a5c00b3b28f603e8967551d380f7bfe6e Mon Sep 17 00:00:00 2001 From: Mavo Date: Fri, 29 Jan 2016 10:28:20 +0100 Subject: [PATCH] Fixed problem with multiple transitions to one state Former-commit-id: 2fe612028ea89b1fde6e7b68955a3761eb6fdf45 --- examples/dft/pand_param.dft | 6 ++++++ examples/dft/tripple_pand.dft | 9 +++++++++ examples/dft/tripple_pand2.dft | 8 ++++++++ examples/dft/tripple_pand2_c.dft | 6 ++++++ examples/dft/tripple_pand_c.dft | 7 +++++++ src/builder/ExplicitDFTModelBuilder.cpp | 20 +++++++++++--------- 6 files changed, 47 insertions(+), 9 deletions(-) create mode 100644 examples/dft/pand_param.dft create mode 100644 examples/dft/tripple_pand.dft create mode 100644 examples/dft/tripple_pand2.dft create mode 100644 examples/dft/tripple_pand2_c.dft create mode 100644 examples/dft/tripple_pand_c.dft 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