diff --git a/src/transformations/dft/DftToGspnTransformator.cpp b/src/transformations/dft/DftToGspnTransformator.cpp
index 87df6a89e..68114bf94 100644
--- a/src/transformations/dft/DftToGspnTransformator.cpp
+++ b/src/transformations/dft/DftToGspnTransformator.cpp
@@ -5,6 +5,10 @@
namespace storm {
namespace transformations {
namespace dft {
+
+ // Prevent some magic constants
+ static constexpr const uint64_t defaultPriority = 0;
+ static constexpr const uint64_t defaultCapacity = 0;
template <typename ValueType>
DftToGspnTransformator<ValueType>::DftToGspnTransformator(storm::storage::DFT<ValueType> const& dft) : mDft(dft) {
@@ -13,8 +17,8 @@ namespace storm {
template <typename ValueType>
void DftToGspnTransformator<ValueType>::transform() {
- mGspn = storm::gspn::GSPN();
- mGspn.setName("DftToGspnTransformation");
+
+ builder.setGspnName("DftToGspnTransformation");
// Loop through every DFT element and draw them as a GSPN.
drawGSPNElements();
@@ -85,538 +89,512 @@ namespace storm {
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawBE(std::shared_ptr<storm::storage::DFTBE<ValueType> const> dftBE) {
- uint_fast64_t priority = getPriority(0, dftBE);
-
- storm::gspn::Place placeBEActivated;
- placeBEActivated.setName(dftBE->name() + STR_ACTIVATED);
- placeBEActivated.setNumberOfInitialTokens(isBEActive(dftBE) ? 1 : 0);
- mGspn.addPlace(placeBEActivated);
-
- storm::gspn::Place placeBEFailed;
- placeBEFailed.setName(dftBE->name() + STR_FAILED);
- placeBEFailed.setNumberOfInitialTokens(0);
- mGspn.addPlace(placeBEFailed);
-
- storm::gspn::TimedTransition<double> timedTransitionActiveFailure;
- timedTransitionActiveFailure.setName(dftBE->name() + "_activeFailing");
- timedTransitionActiveFailure.setPriority(priority);
- timedTransitionActiveFailure.setRate(dftBE->activeFailureRate());
- timedTransitionActiveFailure.setInputArcMultiplicity(placeBEActivated, 1);
- timedTransitionActiveFailure.setInhibitionArcMultiplicity(placeBEFailed, 1);
- timedTransitionActiveFailure.setOutputArcMultiplicity(placeBEActivated, 1);
- timedTransitionActiveFailure.setOutputArcMultiplicity(placeBEFailed, 1);
- mGspn.addTimedTransition(timedTransitionActiveFailure);
-
- storm::gspn::TimedTransition<double> timedTransitionPassiveFailure;
- timedTransitionPassiveFailure.setName(dftBE->name() + "_passiveFailing");
- timedTransitionPassiveFailure.setPriority(priority);
- timedTransitionPassiveFailure.setRate(dftBE->passiveFailureRate());
- timedTransitionPassiveFailure.setInhibitionArcMultiplicity(placeBEActivated, 1);
- timedTransitionPassiveFailure.setInhibitionArcMultiplicity(placeBEFailed, 1);
- timedTransitionPassiveFailure.setOutputArcMultiplicity(placeBEFailed, 1);
- mGspn.addTimedTransition(timedTransitionPassiveFailure);
- }
+ uint64_t beActive = builder.addPlace(defaultCapacity, isBEActive(dftBE) ? 1 : 0, dftBE->name() + STR_ACTIVATED);
+ uint64_t beFailed = builder.addPlace(defaultCapacity, 0, dftBE->name() + STR_FAILED);
+ assert(failedNodes.size() == dftBE->id());
+ failedNodes.push_back(beFailed);
+ uint64_t tActive = builder.addTimedTransition(defaultPriority, dftBE->activeFailureRate(), dftBE->name() + "_activeFailing");
+ builder.addInputArc(beActive, tActive);
+ builder.addInhibitionArc(beFailed, tActive);
+ builder.addOutputArc(tActive, beActive);
+ builder.addOutputArc(tActive, beFailed);
+ uint64_t tPassive = builder.addTimedTransition(defaultPriority, dftBE->passiveFailureRate(), dftBE->name() + "_passiveFailing");
+ builder.addInhibitionArc(beActive, tPassive);
+ builder.addInhibitionArc(beFailed, tPassive);
+ builder.addOutputArc(tActive, beFailed);
+ }
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawAND(std::shared_ptr<storm::storage::DFTAnd<ValueType> const> dftAnd) {
- storm::gspn::Place placeANDFailed;
- placeANDFailed.setName(dftAnd->name() + STR_FAILED);
- placeANDFailed.setNumberOfInitialTokens(0);
- mGspn.addPlace(placeANDFailed);
-
- storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionANDFailing;
- immediateTransitionANDFailing.setName(dftAnd->name() + STR_FAILING);
- immediateTransitionANDFailing.setPriority(getPriority(0, dftAnd));
- immediateTransitionANDFailing.setWeight(0.0);
- immediateTransitionANDFailing.setInhibitionArcMultiplicity(placeANDFailed, 1);
- immediateTransitionANDFailing.setOutputArcMultiplicity(placeANDFailed, 1);
- mGspn.addImmediateTransition(immediateTransitionANDFailing);
+ uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftAnd->name() + STR_FAILED);
+ assert(failedNodes.size() == dftAnd->id());
+ failedNodes.push_back(nodeFailed);
+ uint64_t tAndFailed = builder.addImmediateTransition( getFailPriority(dftAnd) , 0.0, dftAnd->name() + STR_FAILING );
+ builder.addInhibitionArc(nodeFailed, tAndFailed);
+ builder.addOutputArc(tAndFailed, nodeFailed);
+ for(auto const& child : dftAnd->children()) {
+ assert(failedNodes.size() > child->id());
+ builder.addInputArc(failedNodes[child->id()], tAndFailed);
+ }
+
}
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawOR(std::shared_ptr<storm::storage::DFTOr<ValueType> const> dftOr) {
- uint_fast64_t priority = getPriority(0, dftOr);
-
- storm::gspn::Place placeORFailed;
- placeORFailed.setName(dftOr->name() + STR_FAILED);
- placeORFailed.setNumberOfInitialTokens(0);
- mGspn.addPlace(placeORFailed);
-
- auto children = dftOr->children();
- for (std::size_t i = 0; i < dftOr->nrChildren(); i++) {
- storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionORFailing;
- immediateTransitionORFailing.setName(dftOr->name() + "_" + children[i]->name() + STR_FAILING);
- immediateTransitionORFailing.setPriority(priority);
- immediateTransitionORFailing.setWeight(0.0);
- immediateTransitionORFailing.setInhibitionArcMultiplicity(placeORFailed, 1);
- immediateTransitionORFailing.setOutputArcMultiplicity(placeORFailed, 1);
- mGspn.addImmediateTransition(immediateTransitionORFailing);
- }
+ uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftOr->name() + STR_FAILED);
+ assert(failedNodes.size() == dftOr->id());
+ failedNodes.push_back(nodeFailed);
+ uint64_t i = 0;
+ for (auto const& child : dftOr->children()) {
+ uint64_t tNodeFailed = builder.addImmediateTransition( getFailPriority(dftOr) , 0.0, dftOr->name() + STR_FAILING + std::to_string(i) );
+ builder.addInhibitionArc(nodeFailed, tNodeFailed);
+ builder.addOutputArc(tNodeFailed, nodeFailed);
+ assert(failedNodes.size() > child->id());
+ builder.addInputArc(failedNodes[child->id()], tNodeFailed);
+ ++i;
+ }
}
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawVOT(std::shared_ptr<storm::storage::DFTVot<ValueType> const> dftVot) {
- uint_fast64_t priority = getPriority(0, dftVot);
-
- storm::gspn::Place placeVOTFailed;
- placeVOTFailed.setName(dftVot->name() + STR_FAILED);
- placeVOTFailed.setNumberOfInitialTokens(0);
- mGspn.addPlace(placeVOTFailed);
-
- storm::gspn::Place placeVOTCollector;
- placeVOTCollector.setName(dftVot->name() + "_collector");
- placeVOTCollector.setNumberOfInitialTokens(0);
- mGspn.addPlace(placeVOTCollector);
-
- storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionVOTFailing;
- immediateTransitionVOTFailing.setName(dftVot->name() + STR_FAILING);
- immediateTransitionVOTFailing.setPriority(priority);
- immediateTransitionVOTFailing.setWeight(0.0);
- immediateTransitionVOTFailing.setInhibitionArcMultiplicity(placeVOTFailed, 1);
- immediateTransitionVOTFailing.setOutputArcMultiplicity(placeVOTFailed, 1);
- immediateTransitionVOTFailing.setOutputArcMultiplicity(placeVOTCollector, dftVot->threshold()); // Custom threshold.
- immediateTransitionVOTFailing.setInputArcMultiplicity(placeVOTCollector, dftVot->threshold()); // Custom threshold.
- mGspn.addImmediateTransition(immediateTransitionVOTFailing);
-
- auto children = dftVot->children();
-
- // Draw transition/place for every child.
- for (std::size_t i = 0; i < children.size(); i++) {
- storm::gspn::Place placeChildInhibit;
- placeChildInhibit.setName(dftVot->name() + "_" + children[i]->name() + "_inhibitor");
- placeChildInhibit.setNumberOfInitialTokens(0);
- mGspn.addPlace(placeChildInhibit);
-
- storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionCollecting;
- immediateTransitionCollecting.setName(dftVot->name() + "_" + children[i]->name() + "_collecting");
- immediateTransitionCollecting.setPriority(priority);
- immediateTransitionCollecting.setWeight(0.0);
- immediateTransitionCollecting.setInhibitionArcMultiplicity(placeChildInhibit, 1);
- immediateTransitionCollecting.setOutputArcMultiplicity(placeChildInhibit, 1);
- immediateTransitionCollecting.setOutputArcMultiplicity(placeVOTCollector, 1);
- mGspn.addImmediateTransition(immediateTransitionCollecting);
- }
+ uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftVot->name() + STR_FAILED);
+ assert(failedNodes.size() == dftVot->id());
+ failedNodes.push_back(nodeFailed);
+ uint64_t nodeCollector = builder.addPlace(dftVot->nrChildren(), 0, dftVot->name() + "_collector");
+ uint64_t tNodeFailed = builder.addImmediateTransition(getFailPriority(dftVot), 0.0, dftVot->name() + STR_FAILING);
+ builder.addOutputArc(tNodeFailed, nodeFailed);
+ builder.addInhibitionArc(nodeFailed, tNodeFailed);
+ builder.addInputArc(nodeCollector, tNodeFailed, dftVot->threshold());
+ builder.addOutputArc(tNodeFailed, nodeCollector, dftVot->threshold());
+ uint64_t i = 0;
+ for (auto const& child : dftVot->children()) {
+ uint64_t childInhibPlace = builder.addPlace(1, 0, dftVot->name() + "_child_fail_inhib" + std::to_string(i));
+ uint64_t tCollect = builder.addImmediateTransition(getFailPriority(dftVot), 0.0, dftVot->name() + "_child_collect" + std::to_string(i));
+ builder.addOutputArc(tCollect, nodeCollector);
+ builder.addOutputArc(tCollect, childInhibPlace);
+ builder.addInhibitionArc(childInhibPlace, tCollect);
+ builder.addInputArc(failedNodes[child->id()], tCollect);
+ ++i;
+ }
}
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawPAND(std::shared_ptr<storm::storage::DFTPand<ValueType> const> dftPand) {
- uint_fast64_t priority = getPriority(0, dftPand);
-
- storm::gspn::Place placePANDFailed;
- placePANDFailed.setName(dftPand->name() + STR_FAILED);
- placePANDFailed.setNumberOfInitialTokens(0);
- mGspn.addPlace(placePANDFailed);
-
- storm::gspn::Place placePANDFailsave;
- placePANDFailsave.setName(dftPand->name() + STR_FAILSAVE);
- placePANDFailsave.setNumberOfInitialTokens(0);
- mGspn.addPlace(placePANDFailsave);
-
- storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionPANDFailing;
- immediateTransitionPANDFailing.setName(dftPand->name() + STR_FAILING);
- immediateTransitionPANDFailing.setPriority(priority);
- immediateTransitionPANDFailing.setWeight(0.0);
- immediateTransitionPANDFailing.setInhibitionArcMultiplicity(placePANDFailed, 1);
- immediateTransitionPANDFailing.setInhibitionArcMultiplicity(placePANDFailsave, 1);
- immediateTransitionPANDFailing.setOutputArcMultiplicity(placePANDFailed, 1);
- mGspn.addImmediateTransition(immediateTransitionPANDFailing);
-
- for (std::size_t i = 0; i < dftPand->nrChildren() -1; i++) {
- storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionPANDFailsave;
- immediateTransitionPANDFailsave.setName(dftPand->name() + "_" + std::to_string(i) + STR_FAILSAVING);
- immediateTransitionPANDFailsave.setPriority(priority);
- immediateTransitionPANDFailsave.setWeight(0.0);
- immediateTransitionPANDFailsave.setInhibitionArcMultiplicity(placePANDFailsave, 1);
- immediateTransitionPANDFailsave.setOutputArcMultiplicity(placePANDFailsave, 1);
- mGspn.addImmediateTransition(immediateTransitionPANDFailsave);
- }
+ uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftPand->name() + STR_FAILED);
+ assert(failedNodes.size() == dftPand->id());
+ failedNodes.push_back(nodeFailed);
+ uint64_t nodeFS = builder.addPlace(defaultCapacity, 0, dftPand->name() + STR_FAILSAVE);
+ uint64_t tNodeFailed = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILING);
+ builder.addInhibitionArc(nodeFailed, tNodeFailed);
+ builder.addInhibitionArc(nodeFS, tNodeFailed);
+ builder.addOutputArc(tNodeFailed, nodeFailed);
+ for(auto const& child : dftPand->children()) {
+ builder.addInputArc(failedNodes[child->id()], tNodeFailed);
+ }
+ for (uint64_t j = 1; j < dftPand->nrChildren(); ++j) {
+ uint64_t tfs = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILSAVING + std::to_string(j));
+ builder.addInputArc(failedNodes[dftPand->children().at(j)->id()], tfs);
+ builder.addInhibitionArc(failedNodes[dftPand->children().at(j-1)->id()], tfs);
+ builder.addOutputArc(tfs, nodeFS);
+
+ }
+
+//
+// storm::gspn::Place placePANDFailed;
+// placePANDFailed.setName(dftPand->name() + STR_FAILED);
+// placePANDFailed.setNumberOfInitialTokens(0);
+// mGspn.addPlace(placePANDFailed);
+//
+// storm::gspn::Place placePANDFailsave;
+// placePANDFailsave.setName(dftPand->name() + STR_FAILSAVE);
+// placePANDFailsave.setNumberOfInitialTokens(0);
+// mGspn.addPlace(placePANDFailsave);
+//
+// storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionPANDFailing;
+// immediateTransitionPANDFailing.setName(dftPand->name() + STR_FAILING);
+// immediateTransitionPANDFailing.setPriority(priority);
+// immediateTransitionPANDFailing.setWeight(0.0);
+// immediateTransitionPANDFailing.setInhibitionArcMultiplicity(placePANDFailed, 1);
+// immediateTransitionPANDFailing.setInhibitionArcMultiplicity(placePANDFailsave, 1);
+// immediateTransitionPANDFailing.setOutputArcMultiplicity(placePANDFailed, 1);
+// mGspn.addImmediateTransition(immediateTransitionPANDFailing);
+//
+// for (std::size_t i = 0; i < dftPand->nrChildren() -1; i++) {
+// storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionPANDFailsave;
+// immediateTransitionPANDFailsave.setName(dftPand->name() + "_" + std::to_string(i) + STR_FAILSAVING);
+// immediateTransitionPANDFailsave.setPriority(priority);
+// immediateTransitionPANDFailsave.setWeight(0.0);
+// immediateTransitionPANDFailsave.setInhibitionArcMultiplicity(placePANDFailsave, 1);
+// immediateTransitionPANDFailsave.setOutputArcMultiplicity(placePANDFailsave, 1);
+// mGspn.addImmediateTransition(immediateTransitionPANDFailsave);
+// }
}
-
+//
template <typename ValueType>
- void DftToGspnTransformator<ValueType>::drawSPARE(std::shared_ptr<storm::storage::DFTSpare<ValueType> const> dftSpare) {
- uint_fast64_t priority = getPriority(0, dftSpare);
-
- // This codeblock can be removed later, when I am 100% sure it is not needed anymore.
- /*
- storm::gspn::Place placeSPAREActivated;
- placeSPAREActivated.setName(dftSpare->name() + STR_ACTIVATED);
- placeSPAREActivated.setNumberOfInitialTokens(isBEActive(dftSpare));
- mGspn.addPlace(placeSPAREActivated);
-
- storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionPCActivating;
- immediateTransitionPCActivating.setName(dftSpare->children()[0]->name() + STR_ACTIVATING);
- immediateTransitionPCActivating.setPriority(priority);
- immediateTransitionPCActivating.setWeight(0.0);
- immediateTransitionPCActivating.setInputArcMultiplicity(placeSPAREActivated, 1);
- immediateTransitionPCActivating.setOutputArcMultiplicity(placeSPAREActivated, 1);
- mGspn.addImmediateTransition(immediateTransitionPCActivating);
- */
-
- auto children = dftSpare->children();
-
- // Draw places and transitions that belong to each spare child.
- for (std::size_t i = 1; i < children.size(); i++) {
- auto placeChildClaimedPreexist = mGspn.getPlace(children[i]->name() + "_claimed");
-
- if (!placeChildClaimedPreexist.first) { // Only draw this place if it doesn't exist jet.
- storm::gspn::Place placeChildClaimed;
- placeChildClaimed.setName(children[i]->name() + "_claimed");
- placeChildClaimed.setNumberOfInitialTokens(0);
- mGspn.addPlace(placeChildClaimed);
-
- storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionSpareChildActivating;
- immediateTransitionSpareChildActivating.setName(children[i]->name() + STR_ACTIVATING);
- immediateTransitionSpareChildActivating.setPriority(priority);
- immediateTransitionSpareChildActivating.setWeight(0.0);
- immediateTransitionSpareChildActivating.setInputArcMultiplicity(placeChildClaimed, 1);
- immediateTransitionSpareChildActivating.setOutputArcMultiplicity(placeChildClaimed, 1);
- mGspn.addImmediateTransition(immediateTransitionSpareChildActivating);
- }
-
- auto placeChildClaimedExist = mGspn.getPlace(children[i]->name() + "_claimed");
-
- storm::gspn::Place placeSPAREClaimedChild;
- placeSPAREClaimedChild.setName(dftSpare->name() + "_claimed_" + children[i]->name());
- placeSPAREClaimedChild.setNumberOfInitialTokens(0);
- mGspn.addPlace(placeSPAREClaimedChild);
-
- storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionChildClaiming;
- immediateTransitionChildClaiming.setName(dftSpare->name() + "_claiming_" + children[i]->name());
- 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;
- if (i < children.size() - 1) {
- placeSPAREChildConsumed.setName(dftSpare->name() + "_" + 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->name() + "_" + children[i]->name() + "_consuming1");
- immediateTransitionChildConsuming1.setPriority(priority);
- immediateTransitionChildConsuming1.setWeight(0.0);
- immediateTransitionChildConsuming1.setOutputArcMultiplicity(placeSPAREChildConsumed, 1);
- immediateTransitionChildConsuming1.setInhibitionArcMultiplicity(placeSPAREChildConsumed, 1);
- immediateTransitionChildConsuming1.setInhibitionArcMultiplicity(placeSPAREClaimedChild, 1);
- mGspn.addImmediateTransition(immediateTransitionChildConsuming1);
-
- storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionChildConsuming2;
- immediateTransitionChildConsuming2.setName(dftSpare->name() + "_" + children[i]->name() + "_consuming2");
- immediateTransitionChildConsuming2.setPriority(priority);
- immediateTransitionChildConsuming2.setWeight(0.0);
- immediateTransitionChildConsuming2.setOutputArcMultiplicity(placeSPAREChildConsumed, 1);
- immediateTransitionChildConsuming2.setInhibitionArcMultiplicity(placeSPAREChildConsumed, 1);
- immediateTransitionChildConsuming2.setOutputArcMultiplicity(placeSPAREClaimedChild, 1);
- immediateTransitionChildConsuming2.setInputArcMultiplicity(placeSPAREClaimedChild, 1);
- mGspn.addImmediateTransition(immediateTransitionChildConsuming2);
- }
-
- // Draw connections between all spare childs.
- for (std::size_t i = 1; i < children.size() - 1; i++) {
- auto placeSPAREChildConsumed = mGspn.getPlace(dftSpare->name() + "_" + children[i]->name() + "_consumed");
- auto immediateTransitionChildClaiming = mGspn.getImmediateTransition(dftSpare->name() + "_claiming_" + children[i + 1]->name());
- auto immediateTransitionChildConsuming1 = mGspn.getImmediateTransition(dftSpare->name() + "_" + children[i + 1]->name() + "_consuming1");
-
- immediateTransitionChildClaiming.second->setOutputArcMultiplicity(placeSPAREChildConsumed.second, 1);
- immediateTransitionChildClaiming.second->setInputArcMultiplicity(placeSPAREChildConsumed.second, 1);
-
- immediateTransitionChildConsuming1.second->setOutputArcMultiplicity(placeSPAREChildConsumed.second, 1);
- immediateTransitionChildConsuming1.second->setInputArcMultiplicity(placeSPAREChildConsumed.second, 1);
- }
+ void DftToGspnTransformator<ValueType>::drawSPARE(std::shared_ptr<storm::storage::DFTSpare<ValueType> const> dftSpare) {
+// uint_fast64_t priority = getPriority(0, dftSpare);
+//
+// // This codeblock can be removed later, when I am 100% sure it is not needed anymore.
+// /*
+// storm::gspn::Place placeSPAREActivated;
+// placeSPAREActivated.setName(dftSpare->name() + STR_ACTIVATED);
+// placeSPAREActivated.setNumberOfInitialTokens(isBEActive(dftSpare));
+// mGspn.addPlace(placeSPAREActivated);
+//
+// storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionPCActivating;
+// immediateTransitionPCActivating.setName(dftSpare->children()[0]->name() + STR_ACTIVATING);
+// immediateTransitionPCActivating.setPriority(priority);
+// immediateTransitionPCActivating.setWeight(0.0);
+// immediateTransitionPCActivating.setInputArcMultiplicity(placeSPAREActivated, 1);
+// immediateTransitionPCActivating.setOutputArcMultiplicity(placeSPAREActivated, 1);
+// mGspn.addImmediateTransition(immediateTransitionPCActivating);
+// */
+//
+// auto children = dftSpare->children();
+//
+// // Draw places and transitions that belong to each spare child.
+// for (std::size_t i = 1; i < children.size(); i++) {
+// auto placeChildClaimedPreexist = mGspn.getPlace(children[i]->name() + "_claimed");
+//
+// if (!placeChildClaimedPreexist.first) { // Only draw this place if it doesn't exist jet.
+// storm::gspn::Place placeChildClaimed;
+// placeChildClaimed.setName(children[i]->name() + "_claimed");
+// placeChildClaimed.setNumberOfInitialTokens(0);
+// mGspn.addPlace(placeChildClaimed);
+//
+// storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionSpareChildActivating;
+// immediateTransitionSpareChildActivating.setName(children[i]->name() + STR_ACTIVATING);
+// immediateTransitionSpareChildActivating.setPriority(priority);
+// immediateTransitionSpareChildActivating.setWeight(0.0);
+// immediateTransitionSpareChildActivating.setInputArcMultiplicity(placeChildClaimed, 1);
+// immediateTransitionSpareChildActivating.setOutputArcMultiplicity(placeChildClaimed, 1);
+// mGspn.addImmediateTransition(immediateTransitionSpareChildActivating);
+// }
+//
+// auto placeChildClaimedExist = mGspn.getPlace(children[i]->name() + "_claimed");
+//
+// storm::gspn::Place placeSPAREClaimedChild;
+// placeSPAREClaimedChild.setName(dftSpare->name() + "_claimed_" + children[i]->name());
+// placeSPAREClaimedChild.setNumberOfInitialTokens(0);
+// mGspn.addPlace(placeSPAREClaimedChild);
+//
+// storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionChildClaiming;
+// immediateTransitionChildClaiming.setName(dftSpare->name() + "_claiming_" + children[i]->name());
+// 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;
+// if (i < children.size() - 1) {
+// placeSPAREChildConsumed.setName(dftSpare->name() + "_" + 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->name() + "_" + children[i]->name() + "_consuming1");
+// immediateTransitionChildConsuming1.setPriority(priority);
+// immediateTransitionChildConsuming1.setWeight(0.0);
+// immediateTransitionChildConsuming1.setOutputArcMultiplicity(placeSPAREChildConsumed, 1);
+// immediateTransitionChildConsuming1.setInhibitionArcMultiplicity(placeSPAREChildConsumed, 1);
+// immediateTransitionChildConsuming1.setInhibitionArcMultiplicity(placeSPAREClaimedChild, 1);
+// mGspn.addImmediateTransition(immediateTransitionChildConsuming1);
+//
+// storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionChildConsuming2;
+// immediateTransitionChildConsuming2.setName(dftSpare->name() + "_" + children[i]->name() + "_consuming2");
+// immediateTransitionChildConsuming2.setPriority(priority);
+// immediateTransitionChildConsuming2.setWeight(0.0);
+// immediateTransitionChildConsuming2.setOutputArcMultiplicity(placeSPAREChildConsumed, 1);
+// immediateTransitionChildConsuming2.setInhibitionArcMultiplicity(placeSPAREChildConsumed, 1);
+// immediateTransitionChildConsuming2.setOutputArcMultiplicity(placeSPAREClaimedChild, 1);
+// immediateTransitionChildConsuming2.setInputArcMultiplicity(placeSPAREClaimedChild, 1);
+// mGspn.addImmediateTransition(immediateTransitionChildConsuming2);
+// }
+//
+// // Draw connections between all spare childs.
+// for (std::size_t i = 1; i < children.size() - 1; i++) {
+// auto placeSPAREChildConsumed = mGspn.getPlace(dftSpare->name() + "_" + children[i]->name() + "_consumed");
+// auto immediateTransitionChildClaiming = mGspn.getImmediateTransition(dftSpare->name() + "_claiming_" + children[i + 1]->name());
+// auto immediateTransitionChildConsuming1 = mGspn.getImmediateTransition(dftSpare->name() + "_" + children[i + 1]->name() + "_consuming1");
+//
+// immediateTransitionChildClaiming.second->setOutputArcMultiplicity(placeSPAREChildConsumed.second, 1);
+// immediateTransitionChildClaiming.second->setInputArcMultiplicity(placeSPAREChildConsumed.second, 1);
+//
+// immediateTransitionChildConsuming1.second->setOutputArcMultiplicity(placeSPAREChildConsumed.second, 1);
+// immediateTransitionChildConsuming1.second->setInputArcMultiplicity(placeSPAREChildConsumed.second, 1);
+// }
}
-
+//
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawPOR(std::shared_ptr<storm::storage::DFTPor<ValueType> const> dftPor) {
- uint_fast64_t priority = getPriority(0, dftPor);
-
- storm::gspn::Place placePORFailed;
- placePORFailed.setName(dftPor->name() + STR_FAILED);
- placePORFailed.setNumberOfInitialTokens(0);
- mGspn.addPlace(placePORFailed);
-
- storm::gspn::Place placePORFailsave;
- placePORFailsave.setName(dftPor->name() + STR_FAILSAVE);
- placePORFailsave.setNumberOfInitialTokens(0);
- mGspn.addPlace(placePORFailsave);
-
- storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionPORFailing;
- immediateTransitionPORFailing.setName(dftPor->name() + STR_FAILING);
- immediateTransitionPORFailing.setPriority(priority);
- immediateTransitionPORFailing.setWeight(0.0);
- immediateTransitionPORFailing.setInhibitionArcMultiplicity(placePORFailed, 1);
- immediateTransitionPORFailing.setInhibitionArcMultiplicity(placePORFailsave, 1);
- immediateTransitionPORFailing.setOutputArcMultiplicity(placePORFailed, 1);
- mGspn.addImmediateTransition(immediateTransitionPORFailing);
-
- storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionPORFailsave;
- immediateTransitionPORFailsave.setName(dftPor->name() + STR_FAILSAVING);
- immediateTransitionPORFailsave.setPriority(priority);
- immediateTransitionPORFailsave.setWeight(0.0);
- immediateTransitionPORFailsave.setInhibitionArcMultiplicity(placePORFailsave, 1);
- immediateTransitionPORFailsave.setOutputArcMultiplicity(placePORFailsave, 1);
- mGspn.addImmediateTransition(immediateTransitionPORFailsave);
+// uint_fast64_t priority = getPriority(0, dftPor);
+//
+// storm::gspn::Place placePORFailed;
+// placePORFailed.setName(dftPor->name() + STR_FAILED);
+// placePORFailed.setNumberOfInitialTokens(0);
+// mGspn.addPlace(placePORFailed);
+//
+// storm::gspn::Place placePORFailsave;
+// placePORFailsave.setName(dftPor->name() + STR_FAILSAVE);
+// placePORFailsave.setNumberOfInitialTokens(0);
+// mGspn.addPlace(placePORFailsave);
+//
+// storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionPORFailing;
+// immediateTransitionPORFailing.setName(dftPor->name() + STR_FAILING);
+// immediateTransitionPORFailing.setPriority(priority);
+// immediateTransitionPORFailing.setWeight(0.0);
+// immediateTransitionPORFailing.setInhibitionArcMultiplicity(placePORFailed, 1);
+// immediateTransitionPORFailing.setInhibitionArcMultiplicity(placePORFailsave, 1);
+// immediateTransitionPORFailing.setOutputArcMultiplicity(placePORFailed, 1);
+// mGspn.addImmediateTransition(immediateTransitionPORFailing);
+//
+// storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionPORFailsave;
+// immediateTransitionPORFailsave.setName(dftPor->name() + STR_FAILSAVING);
+// immediateTransitionPORFailsave.setPriority(priority);
+// immediateTransitionPORFailsave.setWeight(0.0);
+// immediateTransitionPORFailsave.setInhibitionArcMultiplicity(placePORFailsave, 1);
+// immediateTransitionPORFailsave.setOutputArcMultiplicity(placePORFailsave, 1);
+// mGspn.addImmediateTransition(immediateTransitionPORFailsave);
}
-
+//
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawCONSTF(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftConstF) {
- storm::gspn::Place placeCONSTFFailed;
- placeCONSTFFailed.setName(dftConstF->name() + STR_FAILED);
- placeCONSTFFailed.setNumberOfInitialTokens(1);
- mGspn.addPlace(placeCONSTFFailed);
+// storm::gspn::Place placeCONSTFFailed;
+// placeCONSTFFailed.setName(dftConstF->name() + STR_FAILED);
+// placeCONSTFFailed.setNumberOfInitialTokens(1);
+// mGspn.addPlace(placeCONSTFFailed);
}
-
+//
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawCONSTS(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftConstS) {
- storm::gspn::Place placeCONSTSFailed;
- placeCONSTSFailed.setName(dftConstS->name() + STR_FAILED);
- placeCONSTSFailed.setNumberOfInitialTokens(0);
- placeCONSTSFailed.setCapacity(0); // It cannot contain a token, because it cannot fail.
- mGspn.addPlace(placeCONSTSFailed);
+// storm::gspn::Place placeCONSTSFailed;
+// placeCONSTSFailed.setName(dftConstS->name() + STR_FAILED);
+// placeCONSTSFailed.setNumberOfInitialTokens(0);
+// placeCONSTSFailed.setCapacity(0); // It cannot contain a token, because it cannot fail.
+// mGspn.addPlace(placeCONSTSFailed);
}
-
+//
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawPDEP(std::shared_ptr<storm::storage::DFTDependency<ValueType> const>(dftDependency)) {
- // Only draw dependency, if it wasn't drawn before.
- std::string gateName = dftDependency->name().substr(0, dftDependency->name().find("_"));
- auto exists = mGspn.getPlace(gateName + STR_FAILED);
- if (!exists.first) {
- storm::gspn::Place placeDEPFailed;
- placeDEPFailed.setName(gateName + STR_FAILED);
- placeDEPFailed.setNumberOfInitialTokens(0);
- mGspn.addPlace(placeDEPFailed);
-
- storm::gspn::TimedTransition<double> timedTransitionDEPFailure;
- timedTransitionDEPFailure.setName(gateName + STR_FAILING);
- timedTransitionDEPFailure.setPriority(getPriority(0, dftDependency));
- timedTransitionDEPFailure.setRate(dftDependency->probability());
- timedTransitionDEPFailure.setOutputArcMultiplicity(placeDEPFailed, 1);
- timedTransitionDEPFailure.setInhibitionArcMultiplicity(placeDEPFailed, 1);
- mGspn.addTimedTransition(timedTransitionDEPFailure);
- }
+// // Only draw dependency, if it wasn't drawn before.
+// std::string gateName = dftDependency->name().substr(0, dftDependency->name().find("_"));
+// auto exists = mGspn.getPlace(gateName + STR_FAILED);
+// if (!exists.first) {
+// storm::gspn::Place placeDEPFailed;
+// placeDEPFailed.setName(gateName + STR_FAILED);
+// placeDEPFailed.setNumberOfInitialTokens(0);
+// mGspn.addPlace(placeDEPFailed);
+//
+// storm::gspn::TimedTransition<double> timedTransitionDEPFailure;
+// timedTransitionDEPFailure.setName(gateName + STR_FAILING);
+// timedTransitionDEPFailure.setPriority(getPriority(0, dftDependency));
+// timedTransitionDEPFailure.setRate(dftDependency->probability());
+// timedTransitionDEPFailure.setOutputArcMultiplicity(placeDEPFailed, 1);
+// timedTransitionDEPFailure.setInhibitionArcMultiplicity(placeDEPFailed, 1);
+// mGspn.addTimedTransition(timedTransitionDEPFailure);
+// }
}
-
+//
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawGSPNConnections() {
- // Check for every element, if they have parents (all will have at least 1, except the top event).
- for (std::size_t i = 0; i < mDft.nrElements(); i++) {
- auto child = mDft.getElement(i);
- auto parents = child->parentIds();
-
- // Draw a connection to every parent.
- for (std::size_t j = 0; j < parents.size(); j++) {
- // Check the type of the parent and act accordingly (every parent gate has different entry points...).
- switch (mDft.getElement(parents[j])->type()) {
- case storm::storage::DFTElementType::AND:
- {
- auto andEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + STR_FAILING);
- auto childExit = mGspn.getPlace(child->name() + STR_FAILED);
- if (andEntry.first && childExit.first) { // Only add arcs if the objects have been found.
- andEntry.second->setInputArcMultiplicity(childExit.second, 1);
- andEntry.second->setOutputArcMultiplicity(childExit.second, 1);
- }
- break;
- }
- case storm::storage::DFTElementType::OR:
- {
- auto orEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + child->name() + STR_FAILING);
- auto childExit = mGspn.getPlace(child->name() + STR_FAILED);
- if (orEntry.first && childExit.first) { // Only add arcs if the objects have been found.
- orEntry.second->setInputArcMultiplicity(childExit.second, 1);
- orEntry.second->setOutputArcMultiplicity(childExit.second, 1);
- }
- break;
- }
- case storm::storage::DFTElementType::VOT:
- {
- auto childExit = mGspn.getPlace(child->name() + STR_FAILED);
- auto parentEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + child->name() + "_collecting");
-
- if (childExit.first && parentEntry.first) { // Only add arcs if the objects have been found.
- parentEntry.second->setInputArcMultiplicity(childExit.second, 1);
- parentEntry.second->setOutputArcMultiplicity(childExit.second, 1);
- }
-
- break;
- }
- case storm::storage::DFTElementType::PAND:
- {
- auto children = std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(mDft.getElement(parents[j]))->children();
- auto childExit = mGspn.getPlace(child->name() + STR_FAILED);
- auto pandEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + STR_FAILING);
-
- if (childExit.first && pandEntry.first) { // Only add arcs if the objects have been found.
- pandEntry.second->setInputArcMultiplicity(childExit.second, 1);
- pandEntry.second->setOutputArcMultiplicity(childExit.second, 1);
-
- if (children[0] == child) { // Current element is primary child.
- auto pandEntry2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_0" + STR_FAILSAVING);
-
- if (pandEntry2.first) {
- pandEntry2.second->setInhibitionArcMultiplicity(childExit.second, 1);
- }
- }
- else { // Current element is not the primary child.
- for (std::size_t k = 1; k < children.size(); k++) {
- if (children[k] == child) {
- auto pandEntry2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + std::to_string((k - 1)) + STR_FAILSAVING);
- auto pandEntry3 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + std::to_string((k)) + STR_FAILSAVING);
-
- if (pandEntry2.first) {
- pandEntry2.second->setInputArcMultiplicity(childExit.second, 1);
- pandEntry2.second->setOutputArcMultiplicity(childExit.second, 1);
- }
-
- if (pandEntry3.first) {
- pandEntry3.second->setInhibitionArcMultiplicity(childExit.second, 1);
- }
-
- continue;
- }
- }
- }
- }
-
- break;
- }
- case storm::storage::DFTElementType::SPARE:
- {
- // Check if current child is a primary or spare child.
- auto children = std::static_pointer_cast<storm::storage::DFTSpare<ValueType> const>(mDft.getElement(parents[j]))->children();
-
- if (child == children[0]) { // Primary child.
- auto spareExit = mGspn.getImmediateTransition(child->name() + STR_ACTIVATING);
-
- std::vector<int> ids = getAllBEIDsOfElement(child);
- for (std::size_t k = 0; k < ids.size(); k++) {
- auto childEntry = mGspn.getPlace(mDft.getElement(ids[k])->name() + STR_ACTIVATED);
-
- if (spareExit.first && childEntry.first) { // Only add arcs if the objects have been found.
- spareExit.second->setInhibitionArcMultiplicity(childEntry.second, 1);
- spareExit.second->setOutputArcMultiplicity(childEntry.second, 1);
- }
- }
-
- // Draw lines from "primary child_failed" to SPARE.
- auto childExit = mGspn.getPlace(child->name() + STR_FAILED);
- auto spareEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_claiming_" + children[1]->name());
- auto spareEntry2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + children[1]->name() + "_consuming1");
-
- if (childExit.first && spareEntry.first && spareEntry2.first) { // Only add arcs if the objects have been found.
- spareEntry.second->setInputArcMultiplicity(childExit.second, 1);
- spareEntry.second->setOutputArcMultiplicity(childExit.second, 1);
-
- spareEntry2.second->setInputArcMultiplicity(childExit.second, 1);
- spareEntry2.second->setOutputArcMultiplicity(childExit.second, 1);
- }
- }
- else { // A spare child.
- auto spareExit = mGspn.getImmediateTransition(child->name() + STR_ACTIVATING);
- auto spareExit2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_claiming_" + child->name());
-
- std::vector<int> ids = getAllBEIDsOfElement(child);
- for (std::size_t k = 0; k < ids.size(); k++) {
- auto childEntry = mGspn.getPlace(mDft.getElement(ids[k])->name() + STR_ACTIVATED);
-
- if (spareExit.first && spareExit2.first && childEntry.first) { // Only add arcs if the objects have been found.
- if (!spareExit.second->existsInhibitionArc(childEntry.second)) {
- spareExit.second->setInhibitionArcMultiplicity(childEntry.second, 1);
- }
- if (!spareExit.second->existsOutputArc(childEntry.second)) {
- spareExit.second->setOutputArcMultiplicity(childEntry.second, 1);
- }
- if (!spareExit2.second->existsInhibitionArc(childEntry.second)) {
- spareExit2.second->setInhibitionArcMultiplicity(childEntry.second, 1);
- }
- }
- }
-
- auto childExit = mGspn.getPlace(child->name() + STR_FAILED);
- auto spareEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_claiming_" + child->name());
- auto spareEntry2 = mGspn.getImmediateTransition(child->name() + STR_ACTIVATING);
- auto spareEntry3 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + child->name() + "_consuming2");
-
- if (childExit.first && spareEntry.first && spareEntry2.first && spareEntry3.first) { // Only add arcs if the objects have been found.
- spareEntry.second->setInhibitionArcMultiplicity(childExit.second, 1);
-
- if (!spareEntry2.second->existsInhibitionArc(childExit.second)) {
- spareEntry2.second->setInhibitionArcMultiplicity(childExit.second, 1);
- }
-
- spareEntry3.second->setInputArcMultiplicity(childExit.second, 1);
- spareEntry3.second->setOutputArcMultiplicity(childExit.second, 1);
- }
- }
-
- break;
- }
- case storm::storage::DFTElementType::POR:
- {
- auto children = std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(mDft.getElement(parents[j]))->children();
- auto porEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + STR_FAILING);
- auto porEntry2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + STR_FAILSAVING);
- auto childExit = mGspn.getPlace(child->name() + STR_FAILED);
-
- if (porEntry.first && porEntry2.first && childExit.first) { // Only add arcs if the objects have been found.
- if (children[0] == child) { // Current element is primary child.
- porEntry.second->setInputArcMultiplicity(childExit.second, 1);
- porEntry.second->setOutputArcMultiplicity(childExit.second, 1);
- porEntry2.second->setInhibitionArcMultiplicity(childExit.second, 1);
-
- }
- else { // Current element is not the primary child.
- porEntry2.second->setInputArcMultiplicity(childExit.second, 1);
- porEntry2.second->setOutputArcMultiplicity(childExit.second, 1);
- }
- }
-
- break;
- }
- case storm::storage::DFTElementType::SEQ:
- {
- // Sequences are realized with restrictions. Nothing to do here.
- break;
- }
- case storm::storage::DFTElementType::MUTEX:
- {
- // MUTEX are realized with restrictions. Nothing to do here.
- break;
- }
- case storm::storage::DFTElementType::BE:
- {
- // The parent is never a Basic Event.
- break;
- }
- case storm::storage::DFTElementType::CONSTF:
- {
- // The parent is never a Basic Event.
- break;
- }
- case storm::storage::DFTElementType::CONSTS:
- {
- // The parent is never a Basic Event.
- break;
- }
- case storm::storage::DFTElementType::PDEP:
- {
- // The parent is never a DEP. Hence the connections must be drawn somewhere else.
- break;
- }
- default:
- {
- STORM_LOG_ASSERT(false, "DFT type unknown.");
- break;
- }
- }
- }
- }
+// // Check for every element, if they have parents (all will have at least 1, except the top event).
+// for (std::size_t i = 0; i < mDft.nrElements(); i++) {
+// auto child = mDft.getElement(i);
+// auto parents = child->parentIds();
+//
+// // Draw a connection to every parent.
+// for (std::size_t j = 0; j < parents.size(); j++) {
+// // Check the type of the parent and act accordingly (every parent gate has different entry points...).
+// switch (mDft.getElement(parents[j])->type()) {
+// case storm::storage::DFTElementType::AND:
+// {
+// auto andEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + STR_FAILING);
+// auto childExit = mGspn.getPlace(child->name() + STR_FAILED);
+// if (andEntry.first && childExit.first) { // Only add arcs if the objects have been found.
+// andEntry.second->setInputArcMultiplicity(childExit.second, 1);
+// andEntry.second->setOutputArcMultiplicity(childExit.second, 1);
+// }
+// break;
+// }
+// case storm::storage::DFTElementType::OR:
+// {
+// auto orEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + child->name() + STR_FAILING);
+// auto childExit = mGspn.getPlace(child->name() + STR_FAILED);
+// if (orEntry.first && childExit.first) { // Only add arcs if the objects have been found.
+// orEntry.second->setInputArcMultiplicity(childExit.second, 1);
+// orEntry.second->setOutputArcMultiplicity(childExit.second, 1);
+// }
+// break;
+// }
+// case storm::storage::DFTElementType::VOT:
+// {
+// auto childExit = mGspn.getPlace(child->name() + STR_FAILED);
+// auto parentEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + child->name() + "_collecting");
+//
+// if (childExit.first && parentEntry.first) { // Only add arcs if the objects have been found.
+// parentEntry.second->setInputArcMultiplicity(childExit.second, 1);
+// parentEntry.second->setOutputArcMultiplicity(childExit.second, 1);
+// }
+//
+// break;
+// }
+// case storm::storage::DFTElementType::PAND:
+// {
+// auto children = std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(mDft.getElement(parents[j]))->children();
+// auto childExit = mGspn.getPlace(child->name() + STR_FAILED);
+// auto pandEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + STR_FAILING);
+//
+// if (childExit.first && pandEntry.first) { // Only add arcs if the objects have been found.
+// pandEntry.second->setInputArcMultiplicity(childExit.second, 1);
+// pandEntry.second->setOutputArcMultiplicity(childExit.second, 1);
+//
+// if (children[0] == child) { // Current element is primary child.
+// auto pandEntry2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_0" + STR_FAILSAVING);
+//
+// if (pandEntry2.first) {
+// pandEntry2.second->setInhibitionArcMultiplicity(childExit.second, 1);
+// }
+// }
+// else { // Current element is not the primary child.
+// for (std::size_t k = 1; k < children.size(); k++) {
+// if (children[k] == child) {
+// auto pandEntry2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + std::to_string((k - 1)) + STR_FAILSAVING);
+// auto pandEntry3 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + std::to_string((k)) + STR_FAILSAVING);
+//
+// if (pandEntry2.first) {
+// pandEntry2.second->setInputArcMultiplicity(childExit.second, 1);
+// pandEntry2.second->setOutputArcMultiplicity(childExit.second, 1);
+// }
+//
+// if (pandEntry3.first) {
+// pandEntry3.second->setInhibitionArcMultiplicity(childExit.second, 1);
+// }
+//
+// continue;
+// }
+// }
+// }
+// }
+//
+// break;
+// }
+// case storm::storage::DFTElementType::SPARE:
+// {
+// // Check if current child is a primary or spare child.
+// auto children = std::static_pointer_cast<storm::storage::DFTSpare<ValueType> const>(mDft.getElement(parents[j]))->children();
+//
+// if (child == children[0]) { // Primary child.
+// auto spareExit = mGspn.getImmediateTransition(child->name() + STR_ACTIVATING);
+//
+// std::vector<int> ids = getAllBEIDsOfElement(child);
+// for (std::size_t k = 0; k < ids.size(); k++) {
+// auto childEntry = mGspn.getPlace(mDft.getElement(ids[k])->name() + STR_ACTIVATED);
+//
+// if (spareExit.first && childEntry.first) { // Only add arcs if the objects have been found.
+// spareExit.second->setInhibitionArcMultiplicity(childEntry.second, 1);
+// spareExit.second->setOutputArcMultiplicity(childEntry.second, 1);
+// }
+// }
+//
+// // Draw lines from "primary child_failed" to SPARE.
+// auto childExit = mGspn.getPlace(child->name() + STR_FAILED);
+// auto spareEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_claiming_" + children[1]->name());
+// auto spareEntry2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + children[1]->name() + "_consuming1");
+//
+// if (childExit.first && spareEntry.first && spareEntry2.first) { // Only add arcs if the objects have been found.
+// spareEntry.second->setInputArcMultiplicity(childExit.second, 1);
+// spareEntry.second->setOutputArcMultiplicity(childExit.second, 1);
+//
+// spareEntry2.second->setInputArcMultiplicity(childExit.second, 1);
+// spareEntry2.second->setOutputArcMultiplicity(childExit.second, 1);
+// }
+// }
+// else { // A spare child.
+// auto spareExit = mGspn.getImmediateTransition(child->name() + STR_ACTIVATING);
+// auto spareExit2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_claiming_" + child->name());
+//
+// std::vector<int> ids = getAllBEIDsOfElement(child);
+// for (std::size_t k = 0; k < ids.size(); k++) {
+// auto childEntry = mGspn.getPlace(mDft.getElement(ids[k])->name() + STR_ACTIVATED);
+//
+// if (spareExit.first && spareExit2.first && childEntry.first) { // Only add arcs if the objects have been found.
+// if (!spareExit.second->existsInhibitionArc(childEntry.second)) {
+// spareExit.second->setInhibitionArcMultiplicity(childEntry.second, 1);
+// }
+// if (!spareExit.second->existsOutputArc(childEntry.second)) {
+// spareExit.second->setOutputArcMultiplicity(childEntry.second, 1);
+// }
+// if (!spareExit2.second->existsInhibitionArc(childEntry.second)) {
+// spareExit2.second->setInhibitionArcMultiplicity(childEntry.second, 1);
+// }
+// }
+// }
+//
+// auto childExit = mGspn.getPlace(child->name() + STR_FAILED);
+// auto spareEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_claiming_" + child->name());
+// auto spareEntry2 = mGspn.getImmediateTransition(child->name() + STR_ACTIVATING);
+// auto spareEntry3 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + child->name() + "_consuming2");
+//
+// if (childExit.first && spareEntry.first && spareEntry2.first && spareEntry3.first) { // Only add arcs if the objects have been found.
+// spareEntry.second->setInhibitionArcMultiplicity(childExit.second, 1);
+//
+// if (!spareEntry2.second->existsInhibitionArc(childExit.second)) {
+// spareEntry2.second->setInhibitionArcMultiplicity(childExit.second, 1);
+// }
+//
+// spareEntry3.second->setInputArcMultiplicity(childExit.second, 1);
+// spareEntry3.second->setOutputArcMultiplicity(childExit.second, 1);
+// }
+// }
+//
+// break;
+// }
+// case storm::storage::DFTElementType::POR:
+// {
+// auto children = std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(mDft.getElement(parents[j]))->children();
+// auto porEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + STR_FAILING);
+// auto porEntry2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + STR_FAILSAVING);
+// auto childExit = mGspn.getPlace(child->name() + STR_FAILED);
+//
+// if (porEntry.first && porEntry2.first && childExit.first) { // Only add arcs if the objects have been found.
+// if (children[0] == child) { // Current element is primary child.
+// porEntry.second->setInputArcMultiplicity(childExit.second, 1);
+// porEntry.second->setOutputArcMultiplicity(childExit.second, 1);
+// porEntry2.second->setInhibitionArcMultiplicity(childExit.second, 1);
+//
+// }
+// else { // Current element is not the primary child.
+// porEntry2.second->setInputArcMultiplicity(childExit.second, 1);
+// porEntry2.second->setOutputArcMultiplicity(childExit.second, 1);
+// }
+// }
+//
+// break;
+// }
+// case storm::storage::DFTElementType::SEQ:
+// {
+// // Sequences are realized with restrictions. Nothing to do here.
+// break;
+// }
+// case storm::storage::DFTElementType::MUTEX:
+// {
+// // MUTEX are realized with restrictions. Nothing to do here.
+// break;
+// }
+// case storm::storage::DFTElementType::BE:
+// {
+// // The parent is never a Basic Event.
+// break;
+// }
+// case storm::storage::DFTElementType::CONSTF:
+// {
+// // The parent is never a Basic Event.
+// break;
+// }
+// case storm::storage::DFTElementType::CONSTS:
+// {
+// // The parent is never a Basic Event.
+// break;
+// }
+// case storm::storage::DFTElementType::PDEP:
+// {
+// // The parent is never a DEP. Hence the connections must be drawn somewhere else.
+// break;
+// }
+// default:
+// {
+// STORM_LOG_ASSERT(false, "DFT type unknown.");
+// break;
+// }
+// }
+// }
+// }
}
template <typename ValueType>
@@ -655,205 +633,183 @@ namespace storm {
}
template <typename ValueType>
- uint_fast64_t DftToGspnTransformator<ValueType>::getPriority(uint_fast64_t priority, std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement)
+ uint64_t DftToGspnTransformator<ValueType>::getFailPriority(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement)
{
- // If element is the top element, return current priority.
- if (dftElement->id() == mDft.getTopLevelIndex()) {
- return priority;
- }
- else { // Else look at all parents.
- auto parents = dftElement->parents();
- std::vector<uint_fast64_t> pathLengths;
-
- // If the element has no parents, return.
- if (parents.size() == 0) {
- return UINT_FAST64_MAX / 2; // High enough value so that this priority is never used as the shortest path to the top event.
- }
-
- // Check priorities of all parents.
- for (std::size_t i = 0; i < parents.size(); i++) {
- pathLengths.push_back(getPriority(priority + 2, parents[i]));
- }
-
- // And only use the path to the parent with the lowest priority.
- return *std::min_element(pathLengths.begin(), pathLengths.end());
- }
-
- return priority;
+ return mDft.maxRank() - dftElement->rank();
}
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawGSPNDependencies() {
- for (std::size_t i = 0; i < mDft.nrElements(); i++) {
- auto dftElement = mDft.getElement(i);
-
- if (dftElement->isDependency()) {
- std::string gateName = dftElement->name().substr(0, dftElement->name().find("_"));
- auto depEntry = mGspn.getTimedTransition(gateName + STR_FAILING);
- auto trigger = mGspn.getPlace(std::static_pointer_cast<storm::storage::DFTDependency<ValueType> const>(dftElement)->nameTrigger() + STR_FAILED);
-
- if (depEntry.first && trigger.first) { // Only add arcs if the objects have been found.
- if (!depEntry.second->existsInputArc(trigger.second)) {
- depEntry.second->setInputArcMultiplicity(trigger.second, 1);
- }
- if (!depEntry.second->existsOutputArc(trigger.second)){
- depEntry.second->setOutputArcMultiplicity(trigger.second, 1);
- }
- }
-
- auto dependent = mGspn.getPlace(std::static_pointer_cast<storm::storage::DFTDependency<ValueType> const>(dftElement)->nameDependent() + STR_FAILED);
-
- if (dependent.first) { // Only add arcs if the objects have been found.
- depEntry.second->setOutputArcMultiplicity(dependent.second, 1);
- }
- }
- }
+// for (std::size_t i = 0; i < mDft.nrElements(); i++) {
+// auto dftElement = mDft.getElement(i);
+//
+// if (dftElement->isDependency()) {
+// std::string gateName = dftElement->name().substr(0, dftElement->name().find("_"));
+// auto depEntry = mGspn.getTimedTransition(gateName + STR_FAILING);
+// auto trigger = mGspn.getPlace(std::static_pointer_cast<storm::storage::DFTDependency<ValueType> const>(dftElement)->nameTrigger() + STR_FAILED);
+//
+// if (depEntry.first && trigger.first) { // Only add arcs if the objects have been found.
+// if (!depEntry.second->existsInputArc(trigger.second)) {
+// depEntry.second->setInputArcMultiplicity(trigger.second, 1);
+// }
+// if (!depEntry.second->existsOutputArc(trigger.second)){
+// depEntry.second->setOutputArcMultiplicity(trigger.second, 1);
+// }
+// }
+//
+// auto dependent = mGspn.getPlace(std::static_pointer_cast<storm::storage::DFTDependency<ValueType> const>(dftElement)->nameDependent() + STR_FAILED);
+//
+// if (dependent.first) { // Only add arcs if the objects have been found.
+// depEntry.second->setOutputArcMultiplicity(dependent.second, 1);
+// }
+// }
+// }
}
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawGSPNRestrictions() {
- for (std::size_t i = 0; i < mDft.nrElements(); i++) {
- auto dftElement = mDft.getElement(i);
-
- if (dftElement->isRestriction()) {
- switch (dftElement->type()) {
- case storm::storage::DFTElementType::SEQ:
- {
- auto children = mDft.getRestriction(i)->children();
-
- for (std::size_t j = 0; j < children.size() - 1; j++) {
- auto suppressor = mGspn.getPlace(children[j]->name() + STR_FAILED);
-
- switch (children[j + 1]->type()) {
- case storm::storage::DFTElementType::BE: // If suppressed is a BE, add 2 arcs to timed transitions.
- {
- auto suppressedActive = mGspn.getTimedTransition(children[j + 1]->name() + "_activeFailing");
- auto suppressedPassive = mGspn.getTimedTransition(children[j + 1]->name() + "_passiveFailing");
-
- if (suppressor.first && suppressedActive.first && suppressedPassive.first) { // Only add arcs if the objects have been found.
- suppressedActive.second->setInputArcMultiplicity(suppressor.second, 1);
- suppressedActive.second->setOutputArcMultiplicity(suppressor.second, 1);
- suppressedPassive.second->setInputArcMultiplicity(suppressor.second, 1);
- suppressedPassive.second->setOutputArcMultiplicity(suppressor.second, 1);
- }
- break;
- }
- default: // If supressed is not a BE, add single arc to immediate transition.
- {
- auto suppressed = mGspn.getImmediateTransition(children[j + 1]->name() + STR_FAILING);
-
- if (suppressor.first && suppressed.first) { // Only add arcs if the objects have been found.
- suppressed.second->setInputArcMultiplicity(suppressor.second, 1);
- suppressed.second->setOutputArcMultiplicity(suppressor.second, 1);
- }
- break;
- }
- }
- }
- break;
- }
- case storm::storage::DFTElementType::MUTEX:
- {
- // MUTEX is not implemented by the DFTGalileoParser yet. Nothing to do here.
- STORM_LOG_ASSERT(false, "MUTEX is not supported by DftToGspnTransformator.");
- break;
- }
- default:
- {
- break;
- }
- }
- }
- }
+// for (std::size_t i = 0; i < mDft.nrElements(); i++) {
+// auto dftElement = mDft.getElement(i);
+//
+// if (dftElement->isRestriction()) {
+// switch (dftElement->type()) {
+// case storm::storage::DFTElementType::SEQ:
+// {
+// auto children = mDft.getRestriction(i)->children();
+//
+// for (std::size_t j = 0; j < children.size() - 1; j++) {
+// auto suppressor = mGspn.getPlace(children[j]->name() + STR_FAILED);
+//
+// switch (children[j + 1]->type()) {
+// case storm::storage::DFTElementType::BE: // If suppressed is a BE, add 2 arcs to timed transitions.
+// {
+// auto suppressedActive = mGspn.getTimedTransition(children[j + 1]->name() + "_activeFailing");
+// auto suppressedPassive = mGspn.getTimedTransition(children[j + 1]->name() + "_passiveFailing");
+//
+// if (suppressor.first && suppressedActive.first && suppressedPassive.first) { // Only add arcs if the objects have been found.
+// suppressedActive.second->setInputArcMultiplicity(suppressor.second, 1);
+// suppressedActive.second->setOutputArcMultiplicity(suppressor.second, 1);
+// suppressedPassive.second->setInputArcMultiplicity(suppressor.second, 1);
+// suppressedPassive.second->setOutputArcMultiplicity(suppressor.second, 1);
+// }
+// break;
+// }
+// default: // If supressed is not a BE, add single arc to immediate transition.
+// {
+// auto suppressed = mGspn.getImmediateTransition(children[j + 1]->name() + STR_FAILING);
+//
+// if (suppressor.first && suppressed.first) { // Only add arcs if the objects have been found.
+// suppressed.second->setInputArcMultiplicity(suppressor.second, 1);
+// suppressed.second->setOutputArcMultiplicity(suppressor.second, 1);
+// }
+// break;
+// }
+// }
+// }
+// break;
+// }
+// case storm::storage::DFTElementType::MUTEX:
+// {
+// // MUTEX is not implemented by the DFTGalileoParser yet. Nothing to do here.
+// STORM_LOG_ASSERT(false, "MUTEX is not supported by DftToGspnTransformator.");
+// break;
+// }
+// default:
+// {
+// break;
+// }
+// }
+// }
+// }
}
template <typename ValueType>
std::vector<int> DftToGspnTransformator<ValueType>::getAllBEIDsOfElement(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement) {
- std::vector<int> ids;
-
- switch (dftElement->type()) {
- case storm::storage::DFTElementType::AND:
- {
- auto children = std::static_pointer_cast<storm::storage::DFTAnd<ValueType> const>(dftElement)->children();
-
- for (std::size_t i = 0; i < children.size(); i++) {
- std::vector<int> newIds = getAllBEIDsOfElement(children[i]);
- ids.insert(ids.end(), newIds.begin(), newIds.end());
- }
- break;
- }
- case storm::storage::DFTElementType::OR:
- {
- auto children = std::static_pointer_cast<storm::storage::DFTOr<ValueType> const>(dftElement)->children();
-
- for (std::size_t i = 0; i < children.size(); i++) {
- std::vector<int> newIds = getAllBEIDsOfElement(children[i]);
- ids.insert(ids.end(), newIds.begin(), newIds.end());
- }
- break;
- }
- case storm::storage::DFTElementType::VOT:
- {
- auto children = std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(dftElement)->children();
-
- for (std::size_t i = 0; i < children.size(); i++) {
- std::vector<int> newIds = getAllBEIDsOfElement(children[i]);
- ids.insert(ids.end(), newIds.begin(), newIds.end());
- }
- break;
- }
- case storm::storage::DFTElementType::PAND:
- {
- auto children = std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(dftElement)->children();
-
- for (std::size_t i = 0; i < children.size(); i++) {
- std::vector<int> newIds = getAllBEIDsOfElement(children[i]);
- ids.insert(ids.end(), newIds.begin(), newIds.end());
- }
- break;
- }
- case storm::storage::DFTElementType::SPARE:
- {
- auto children = std::static_pointer_cast<storm::storage::DFTSpare<ValueType> const>(dftElement)->children();
-
- // Only regard the primary child of a SPARE. The spare childs are not allowed to be listed here.
- for (std::size_t i = 0; i < 1; i++) {
- std::vector<int> newIds = getAllBEIDsOfElement(children[i]);
- ids.insert(ids.end(), newIds.begin(), newIds.end());
- }
- break;
- }
- case storm::storage::DFTElementType::POR:
- {
- auto children = std::static_pointer_cast<storm::storage::DFTPor<ValueType> const>(dftElement)->children();
-
- for (std::size_t i = 0; i < children.size(); i++) {
- std::vector<int> newIds = getAllBEIDsOfElement(children[i]);
- ids.insert(ids.end(), newIds.begin(), newIds.end());
- }
- break;
- }
- case storm::storage::DFTElementType::BE:
- case storm::storage::DFTElementType::CONSTF:
- case storm::storage::DFTElementType::CONSTS:
- {
- ids.push_back(dftElement->id());
- break;
- }
- case storm::storage::DFTElementType::SEQ:
- case storm::storage::DFTElementType::MUTEX:
- case storm::storage::DFTElementType::PDEP:
- {
- break;
- }
- default:
- {
- STORM_LOG_ASSERT(false, "DFT type unknown.");
- break;
- }
- }
-
- return ids;
+// std::vector<int> ids;
+//
+// switch (dftElement->type()) {
+// case storm::storage::DFTElementType::AND:
+// {
+// auto children = std::static_pointer_cast<storm::storage::DFTAnd<ValueType> const>(dftElement)->children();
+//
+// for (std::size_t i = 0; i < children.size(); i++) {
+// std::vector<int> newIds = getAllBEIDsOfElement(children[i]);
+// ids.insert(ids.end(), newIds.begin(), newIds.end());
+// }
+// break;
+// }
+// case storm::storage::DFTElementType::OR:
+// {
+// auto children = std::static_pointer_cast<storm::storage::DFTOr<ValueType> const>(dftElement)->children();
+//
+// for (std::size_t i = 0; i < children.size(); i++) {
+// std::vector<int> newIds = getAllBEIDsOfElement(children[i]);
+// ids.insert(ids.end(), newIds.begin(), newIds.end());
+// }
+// break;
+// }
+// case storm::storage::DFTElementType::VOT:
+// {
+// auto children = std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(dftElement)->children();
+//
+// for (std::size_t i = 0; i < children.size(); i++) {
+// std::vector<int> newIds = getAllBEIDsOfElement(children[i]);
+// ids.insert(ids.end(), newIds.begin(), newIds.end());
+// }
+// break;
+// }
+// case storm::storage::DFTElementType::PAND:
+// {
+// auto children = std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(dftElement)->children();
+//
+// for (std::size_t i = 0; i < children.size(); i++) {
+// std::vector<int> newIds = getAllBEIDsOfElement(children[i]);
+// ids.insert(ids.end(), newIds.begin(), newIds.end());
+// }
+// break;
+// }
+// case storm::storage::DFTElementType::SPARE:
+// {
+// auto children = std::static_pointer_cast<storm::storage::DFTSpare<ValueType> const>(dftElement)->children();
+//
+// // Only regard the primary child of a SPARE. The spare childs are not allowed to be listed here.
+// for (std::size_t i = 0; i < 1; i++) {
+// std::vector<int> newIds = getAllBEIDsOfElement(children[i]);
+// ids.insert(ids.end(), newIds.begin(), newIds.end());
+// }
+// break;
+// }
+// case storm::storage::DFTElementType::POR:
+// {
+// auto children = std::static_pointer_cast<storm::storage::DFTPor<ValueType> const>(dftElement)->children();
+//
+// for (std::size_t i = 0; i < children.size(); i++) {
+// std::vector<int> newIds = getAllBEIDsOfElement(children[i]);
+// ids.insert(ids.end(), newIds.begin(), newIds.end());
+// }
+// break;
+// }
+// case storm::storage::DFTElementType::BE:
+// case storm::storage::DFTElementType::CONSTF:
+// case storm::storage::DFTElementType::CONSTS:
+// {
+// ids.push_back(dftElement->id());
+// break;
+// }
+// case storm::storage::DFTElementType::SEQ:
+// case storm::storage::DFTElementType::MUTEX:
+// case storm::storage::DFTElementType::PDEP:
+// {
+// break;
+// }
+// default:
+// {
+// STORM_LOG_ASSERT(false, "DFT type unknown.");
+// break;
+// }
+// }
+//
+// return ids;
}
template <typename ValueType>
@@ -862,16 +818,21 @@ namespace storm {
// Writing to file
std::ofstream file;
file.open("gspn.dot");
- mGspn.writeDotToStream(file);
+ storm::gspn::GSPN* gspn = builder.buildGspn();
+ gspn->writeDotToStream(file);
+ delete gspn;
file.close();
} else {
// Writing to console
- mGspn.writeDotToStream(std::cout);
+ storm::gspn::GSPN* gspn = builder.buildGspn();
+ gspn->writeDotToStream(std::cout);
+ delete gspn;
}
}
// Explicitly instantiate the class.
template class DftToGspnTransformator<double>;
+
#ifdef STORM_HAVE_CARL
// template class DftToGspnTransformator<storm::RationalFunction>;
diff --git a/src/transformations/dft/DftToGspnTransformator.h b/src/transformations/dft/DftToGspnTransformator.h
index 162cb7001..3b29f40d6 100644
--- a/src/transformations/dft/DftToGspnTransformator.h
+++ b/src/transformations/dft/DftToGspnTransformator.h
@@ -1,8 +1,8 @@
-#ifndef DFTTOGSPNTRANSFORMATOR_H
-#define DFTTOGSPNTRANSFORMATOR_H
+#pragma once
#include <src/storage/dft/DFT.h>
#include "src/storage/gspn/GSPN.h"
+#include "src/storage/gspn/GspnBuilder.h"
namespace storm {
namespace transformations {
@@ -28,17 +28,6 @@ namespace storm {
void transform();
private:
-
- storm::storage::DFT<ValueType> const& mDft;
- storm::gspn::GSPN mGspn;
-
- static constexpr const char* STR_FAILING = "_failing"; // Name standard for transitions that point towards a place, which in turn indicates the failure of a gate.
- static constexpr const char* STR_FAILED = "_failed"; // Name standard for place which indicates the failure of a gate.
- static constexpr const char* STR_FAILSAVING = "_failsaving"; // Name standard for transition that point towards a place, which in turn indicates the failsave state of a gate.
- static constexpr const char* STR_FAILSAVE = "_failsave"; // Name standard for place which indicates the failsave state of a gate.
- static constexpr const char* STR_ACTIVATED = "_activated"; // Name standard for place which indicates the activity.
- static constexpr const char* STR_ACTIVATING = "_activating"; // Name standard for transition that point towards a place, which in turn indicates its activity.
-
/*!
* Write Gspn to file or console.
*
@@ -152,7 +141,7 @@ 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);
+ uint64_t getFailPriority(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dFTElement);
/*
* Return all ids of BEs, that are successors of the given element and that are not the spare childs of a SPARE.
@@ -160,9 +149,22 @@ namespace storm {
* @param dftElement The element which
*/
std::vector<int> getAllBEIDsOfElement(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement);
+
+
+ storm::storage::DFT<ValueType> const& mDft;
+ storm::gspn::GspnBuilder builder;
+ std::vector<uint64_t> failedNodes;
+
+ static constexpr const char* STR_FAILING = "_failing"; // Name standard for transitions that point towards a place, which in turn indicates the failure of a gate.
+ static constexpr const char* STR_FAILED = "_failed"; // Name standard for place which indicates the failure of a gate.
+ static constexpr const char* STR_FAILSAVING = "_failsaving"; // Name standard for transition that point towards a place, which in turn indicates the failsave state of a gate.
+ static constexpr const char* STR_FAILSAVE = "_failsave"; // Name standard for place which indicates the failsave state of a gate.
+ static constexpr const char* STR_ACTIVATED = "_activated"; // Name standard for place which indicates the activity.
+ static constexpr const char* STR_ACTIVATING = "_activating"; // Name standard for transition that point towards a place, which in turn indicates its activity.
+
+
};
}
}
}
-#endif /* DFTTOGSPNTRANSFORMATOR_H*/