sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Minor fixes

main
Matthias Volk 7 years ago
parent
ca0d76e502
commit
e4e467622f
3 changed files with 30 additions and 31 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 3
      src/storm-dft-cli/storm-dft.cpp
  2. 15
      src/storm-dft/transformations/DftToGspnTransformator.cpp
  3. 11
      src/storm-dft/transformations/DftToGspnTransformator.h

3
src/storm-dft-cli/storm-dft.cpp
View File

@ -107,7 +107,8 @@ void processOptions() {
std::shared_ptr<storm::storage::DFT<double>> dft = loadDFT<double>(); std::shared_ptr<storm::storage::DFT<double>> dft = loadDFT<double>();
// Transform to GSPN // Transform to GSPN
storm::transformations::dft::DftToGspnTransformator<double> gspnTransformator(*dft); storm::transformations::dft::DftToGspnTransformator<double> gspnTransformator(*dft);
gspnTransformator.transform();
bool smart = false;
gspnTransformator.transform(smart);
storm::gspn::GSPN* gspn = gspnTransformator.obtainGSPN(); storm::gspn::GSPN* gspn = gspnTransformator.obtainGSPN();
uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId(); uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId();

15
src/storm-dft/transformations/DftToGspnTransformator.cpp
View File

@ -16,14 +16,15 @@ namespace storm {
} }
template <typename ValueType> template <typename ValueType>
void DftToGspnTransformator<ValueType>::transform() {
void DftToGspnTransformator<ValueType>::transform(bool smart) {
this->smart = smart;
builder.setGspnName("DftToGspnTransformation"); builder.setGspnName("DftToGspnTransformation");
// Loop through every DFT element and draw them as a GSPN. // Loop through every DFT element and draw them as a GSPN.
drawGSPNElements(); drawGSPNElements();
// Draw restrictions into the GSPN (i.e. SEQ or MUTEX). // Draw restrictions into the GSPN (i.e. SEQ or MUTEX).
// TODO
//drawGSPNRestrictions(); //drawGSPNRestrictions();
} }
@ -36,7 +37,6 @@ namespace storm {
template <typename ValueType> template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawGSPNElements() { void DftToGspnTransformator<ValueType>::drawGSPNElements() {
// Loop through every DFT element and draw them as a GSPN. // Loop through every DFT element and draw them as a GSPN.
for (std::size_t i = 0; i < mDft.nrElements(); i++) { for (std::size_t i = 0; i < mDft.nrElements(); i++) {
auto dftElement = mDft.getElement(i); auto dftElement = mDft.getElement(i);
@ -81,7 +81,7 @@ namespace storm {
drawPDEP(std::static_pointer_cast<storm::storage::DFTDependency<ValueType> const>(dftElement)); drawPDEP(std::static_pointer_cast<storm::storage::DFTDependency<ValueType> const>(dftElement));
break; break;
default: default:
STORM_LOG_ASSERT(false, "DFT type unknown.");
STORM_LOG_ASSERT(false, "DFT type " << dftElement->type() << " unknown.");
break; break;
} }
} }
@ -548,7 +548,7 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
uint64_t DftToGspnTransformator<ValueType>::addUnavailableNode(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement, storm::gspn::LayoutInfo const& layoutInfo, bool initialAvailable) { uint64_t DftToGspnTransformator<ValueType>::addUnavailableNode(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement, storm::gspn::LayoutInfo const& layoutInfo, bool initialAvailable) {
uint64_t unavailableNode = builder.addPlace(defaultCapacity, initialAvailable ? 0 : 1, dftElement->name() + "_unavailable");
uint64_t unavailableNode = builder.addPlace(defaultCapacity, initialAvailable ? 0 : 1, dftElement->name() + "_unavail");
assert(unavailableNode != 0); assert(unavailableNode != 0);
unavailableNodes.emplace(dftElement->id(), unavailableNode); unavailableNodes.emplace(dftElement->id(), unavailableNode);
builder.setPlaceLayoutInfo(unavailableNode, layoutInfo); builder.setPlaceLayoutInfo(unavailableNode, layoutInfo);
@ -561,11 +561,9 @@ namespace storm {
disabledNodes.emplace(dftBe->id(), disabledNode); disabledNodes.emplace(dftBe->id(), disabledNode);
return disabledNode; return disabledNode;
} }
//
template <typename ValueType> template <typename ValueType>
bool DftToGspnTransformator<ValueType>::isBEActive(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement)
{
bool DftToGspnTransformator<ValueType>::isBEActive(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement) {
// If element is the top element, return true. // If element is the top element, return true.
if (dftElement->id() == mDft.getTopLevelIndex()) { if (dftElement->id() == mDft.getTopLevelIndex()) {
return true; return true;
@ -607,6 +605,7 @@ namespace storm {
template <typename ValueType> template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawGSPNRestrictions() { void DftToGspnTransformator<ValueType>::drawGSPNRestrictions() {
// TODO
} }
template <typename ValueType> template <typename ValueType>

11
src/storm-dft/transformations/DftToGspnTransformator.h
View File

@ -25,7 +25,7 @@ namespace storm {
/*! /*!
* Transform the DFT to a GSPN. * Transform the DFT to a GSPN.
*/ */
void transform();
void transform(bool smart = true);
/*! /*!
* Extract Gspn by building * Extract Gspn by building
@ -41,6 +41,7 @@ namespace storm {
* Draw all elements of the GSPN. * Draw all elements of the GSPN.
*/ */
void drawGSPNElements(); void drawGSPNElements();
/* /*
* Draw restrictions between the elements of the GSPN (i.e. SEQ or MUTEX). * Draw restrictions between the elements of the GSPN (i.e. SEQ or MUTEX).
*/ */
@ -118,6 +119,7 @@ namespace storm {
void drawSeq(std::shared_ptr<storm::storage::DFTSeq<ValueType> const> dftSeq); void drawSeq(std::shared_ptr<storm::storage::DFTSeq<ValueType> const> dftSeq);
/* /*
* Return true if BE is active (corresponding place contains one initial token) or false if BE is inactive (corresponding place contains no initial token). * Return true if BE is active (corresponding place contains one initial token) or false if BE is inactive (corresponding place contains no initial token).
* *
@ -135,7 +137,6 @@ namespace storm {
*/ */
uint64_t getFailPriority(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dFTElement); uint64_t getFailPriority(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dFTElement);
uint64_t addUnavailableNode(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement, storm::gspn::LayoutInfo const& layoutInfo, bool initialAvailable = true); uint64_t addUnavailableNode(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement, storm::gspn::LayoutInfo const& layoutInfo, bool initialAvailable = true);
uint64_t addDisabledPlace(std::shared_ptr<storm::storage::DFTBE<ValueType> const> dftBe); uint64_t addDisabledPlace(std::shared_ptr<storm::storage::DFTBE<ValueType> const> dftBe);
@ -146,16 +147,14 @@ namespace storm {
std::map<uint64_t, uint64_t> unavailableNodes; std::map<uint64_t, uint64_t> unavailableNodes;
std::map<uint64_t, uint64_t> activeNodes; std::map<uint64_t, uint64_t> activeNodes;
std::map<uint64_t, uint64_t> disabledNodes; std::map<uint64_t, uint64_t> disabledNodes;
bool smart = true;
bool smart;
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_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_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_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_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. static constexpr const char* STR_ACTIVATING = "_activating"; // Name standard for transition that point towards a place, which in turn indicates its activity.
static constexpr const char* STR_ACTIVATED = "_active"; // Name standard for place which indicates the activity.
}; };
} }
} }

Write Preview
Loading…
Cancel
Save