From 170717a20574edb43c8299a17eb999059a8c036c Mon Sep 17 00:00:00 2001
From: mdeutschen <michael.deutschen@rwth-aachen.de>
Date: Mon, 8 Aug 2016 17:14:28 +0200
Subject: [PATCH] Added transformation for 2-input-PAND and untested CONSTF and
CONSTS
Former-commit-id: 478cc29fc58db56e9b754fd09e76cd85a864b2f2
---
.../dft/DftToGspnTransformator.cpp | 103 +++++++++++++++---
.../dft/DftToGspnTransformator.h | 17 +++
2 files changed, 106 insertions(+), 14 deletions(-)
diff --git a/src/transformations/dft/DftToGspnTransformator.cpp b/src/transformations/dft/DftToGspnTransformator.cpp
index 83fee7878..1ce3a5cf7 100644
--- a/src/transformations/dft/DftToGspnTransformator.cpp
+++ b/src/transformations/dft/DftToGspnTransformator.cpp
@@ -65,10 +65,10 @@ namespace storm {
drawBE(std::static_pointer_cast<storm::storage::DFTBE<ValueType> const>(dftElement));
break;
case storm::storage::DFTElementType::CONSTF:
- STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a CONSTF is not yet implemented.");
+ drawCONSTF(dftElement);
break;
case storm::storage::DFTElementType::CONSTS:
- STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a CONSTS is not yet implemented.");
+ drawCONSTS(dftElement);
break;
case storm::storage::DFTElementType::PDEP:
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a PDEP is not yet implemented.");
@@ -88,7 +88,7 @@ namespace storm {
mGspn.addPlace(placeBEActivated);
storm::gspn::Place placeBEFailed;
- placeBEFailed.setName(dftBE->name() + "_failed");
+ placeBEFailed.setName(dftBE->name() + STR_FAILED);
placeBEFailed.setNumberOfInitialTokens(0);
mGspn.addPlace(placeBEFailed);
@@ -115,12 +115,12 @@ namespace storm {
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawAND(std::shared_ptr<storm::storage::DFTAnd<ValueType> const> dftAnd) {
storm::gspn::Place placeANDFailed;
- placeANDFailed.setName(dftAnd->name() + "_failed");
+ placeANDFailed.setName(dftAnd->name() + STR_FAILED);
placeANDFailed.setNumberOfInitialTokens(0);
mGspn.addPlace(placeANDFailed);
storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionANDFailing;
- immediateTransitionANDFailing.setName(dftAnd->name() + "_failing");
+ immediateTransitionANDFailing.setName(dftAnd->name() + STR_FAILING);
immediateTransitionANDFailing.setPriority(1);
immediateTransitionANDFailing.setWeight(0.0);
immediateTransitionANDFailing.setInhibitionArcMultiplicity(placeANDFailed, 1);
@@ -131,14 +131,14 @@ namespace storm {
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawOR(std::shared_ptr<storm::storage::DFTOr<ValueType> const> dftOr) {
storm::gspn::Place placeORFailed;
- placeORFailed.setName(dftOr->name() + "_failed");
+ 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() + "_failing");
+ immediateTransitionORFailing.setName(dftOr->name() + "_" + children[i]->name() + STR_FAILING);
immediateTransitionORFailing.setPriority(1);
immediateTransitionORFailing.setWeight(0.0);
immediateTransitionORFailing.setInhibitionArcMultiplicity(placeORFailed, 1);
@@ -153,13 +153,41 @@ namespace storm {
}
template <typename ValueType>
- void DftToGspnTransformator<ValueType>::drawPAND(std::shared_ptr<storm::storage::DFTPand<ValueType> const> dftPand) {
- STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a PAND is not yet implemented.");
+ void DftToGspnTransformator<ValueType>::drawPAND(std::shared_ptr<storm::storage::DFTPand<ValueType> const> 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() + "_failsave");
+ placePANDFailsave.setNumberOfInitialTokens(0);
+ mGspn.addPlace(placePANDFailsave);
+
+ storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionPANDFailing;
+ immediateTransitionPANDFailing.setName(dftPand->name() + STR_FAILING);
+ immediateTransitionPANDFailing.setPriority(1);
+ immediateTransitionPANDFailing.setWeight(0.0);
+ immediateTransitionPANDFailing.setInhibitionArcMultiplicity(placePANDFailed, 1);
+ immediateTransitionPANDFailing.setInhibitionArcMultiplicity(placePANDFailsave, 1);
+ immediateTransitionPANDFailing.setOutputArcMultiplicity(placePANDFailed, 1);
+ mGspn.addImmediateTransition(immediateTransitionPANDFailing);
+
+ storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionPANDFailsave;
+ immediateTransitionPANDFailsave.setName(dftPand->name() + "_failsaving");
+ immediateTransitionPANDFailsave.setPriority(1);
+ immediateTransitionPANDFailsave.setWeight(0.0);
+ immediateTransitionPANDFailsave.setInhibitionArcMultiplicity(placePANDFailsave, 1);
+ immediateTransitionPANDFailsave.setOutputArcMultiplicity(placePANDFailsave, 1);
+ mGspn.addImmediateTransition(immediateTransitionPANDFailsave);
+
+ // TODO: Are PANDs with more than two children possible?
}
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawSPARE(std::shared_ptr<storm::storage::DFTSpare<ValueType> const> dftSpare) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a SPARE is not yet implemented.");
+ // TODO: What are the codewords for SPAREs in a *.dft file? hsp, wsp and csp?
}
template <typename ValueType>
@@ -167,6 +195,25 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a POR is not yet implemented.");
}
+ 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);
+ // TODO: What is the codeword for CONSTF in a *.dft file?
+ }
+
+ 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);
+ // TODO: What is the codeword for CONSTS in a *.dft file?
+ }
+
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).
@@ -180,8 +227,8 @@ namespace storm {
switch (mDft.getElement(parents[j])->type()) {
case storm::storage::DFTElementType::AND:
{
- auto andEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_failing");
- auto childExit = mGspn.getPlace(child->name() + "_failed");
+ 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);
@@ -190,8 +237,8 @@ namespace storm {
}
case storm::storage::DFTElementType::OR:
{
- auto orEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + child->name() + "_failing");
- auto childExit = mGspn.getPlace(child->name() + "_failed");
+ 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);
@@ -201,7 +248,29 @@ namespace storm {
case storm::storage::DFTElementType::VOT:
break;
case storm::storage::DFTElementType::PAND:
+ {
+ auto children = std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(mDft.getElement(parents[j]))->children();
+ auto pandEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + STR_FAILING);
+ auto pandEntry2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_failsaving");
+ auto childExit = mGspn.getPlace(child->name() + STR_FAILED);
+
+ if (pandEntry.first && pandEntry2.first && childExit.first) { // Only add arcs if the objects have been found.
+ if (children[0] == child) { // Current element is primary child.
+ pandEntry.second->setInputArcMultiplicity(childExit.second, 1);
+ pandEntry.second->setOutputArcMultiplicity(childExit.second, 1);
+ pandEntry2.second->setInhibitionArcMultiplicity(childExit.second, 1);
+
+ }
+ else if (children[1] == child) { // Current element is secondary child.
+ pandEntry.second->setInputArcMultiplicity(childExit.second, 1);
+ pandEntry.second->setOutputArcMultiplicity(childExit.second, 1);
+ pandEntry2.second->setInputArcMultiplicity(childExit.second, 1);
+ pandEntry2.second->setOutputArcMultiplicity(childExit.second, 1);
+ }
+ }
+
break;
+ }
case storm::storage::DFTElementType::SPARE:
break;
case storm::storage::DFTElementType::POR:
@@ -212,13 +281,19 @@ namespace storm {
break;
case storm::storage::DFTElementType::BE:
{
- // The parent is never a Basic Event.
+ // The parent is never a Basic Event (Except for SPAREs?).
break;
}
case storm::storage::DFTElementType::CONSTF:
+ {
+ // The parent is never a Basic Event (Except for SPAREs?).
break;
+ }
case storm::storage::DFTElementType::CONSTS:
+ {
+ // The parent is never a Basic Event (Except for SPAREs?).
break;
+ }
case storm::storage::DFTElementType::PDEP:
break;
default:
diff --git a/src/transformations/dft/DftToGspnTransformator.h b/src/transformations/dft/DftToGspnTransformator.h
index ce87472ea..21ba259ab 100644
--- a/src/transformations/dft/DftToGspnTransformator.h
+++ b/src/transformations/dft/DftToGspnTransformator.h
@@ -31,6 +31,9 @@ namespace storm {
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.
/*!
* Write Gspn to file or console.
@@ -98,6 +101,20 @@ namespace storm {
* @param dftPor The POR gate.
*/
void drawPOR(std::shared_ptr<storm::storage::DFTPor<ValueType> const> dftPor);
+
+ /*
+ * Draw a Petri net CONSTF (Constant Failure, a Basic Event that has already failed).
+ *
+ * @param dftPor The CONSTF Basic Event.
+ */
+ void drawCONSTF(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftConstF);
+
+ /*
+ * Draw a Petri net CONSTS (Constant Save, a Basic Event that cannot fail).
+ *
+ * @param dftPor The CONSTS Basic Event.
+ */
+ void drawCONSTS(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftConstS);
};
}
}