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

Added transformation for 2-input-POR 

Former-commit-id: 890be90f62
main
mdeutschen 9 years ago
committed by Sebastian Junges
parent
c80bcf8f6b
commit
07baef9a7c
3 changed files with 59 additions and 4 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      examples/dft/por2.dft
  2. 57
      src/transformations/dft/DftToGspnTransformator.cpp
  3. 2
      src/transformations/dft/DftToGspnTransformator.h

4
examples/dft/por2.dft
View File

@ -0,0 +1,4 @@
toplevel "A";
"A" por "B" "C";
"B" lambda=0.4 dorm=0.0;
"C" lambda=0.2 dorm=0.0;

57
src/transformations/dft/DftToGspnTransformator.cpp
View File

@ -171,7 +171,7 @@ namespace storm {
mGspn.addPlace(placePANDFailed);
storm::gspn::Place placePANDFailsave;
placePANDFailsave.setName(dftPand->name() + "_failsave");
placePANDFailsave.setName(dftPand->name() + STR_FAILSAVE);
placePANDFailsave.setNumberOfInitialTokens(0);
mGspn.addPlace(placePANDFailsave);
@ -185,12 +185,14 @@ namespace storm {
mGspn.addImmediateTransition(immediateTransitionPANDFailing);
storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionPANDFailsave;
immediateTransitionPANDFailsave.setName(dftPand->name() + "_failsaving");
immediateTransitionPANDFailsave.setName(dftPand->name() + STR_FAILSAVING);
immediateTransitionPANDFailsave.setPriority(1);
immediateTransitionPANDFailsave.setWeight(0.0);
immediateTransitionPANDFailsave.setInhibitionArcMultiplicity(placePANDFailsave, 1);
immediateTransitionPANDFailsave.setOutputArcMultiplicity(placePANDFailsave, 1);
mGspn.addImmediateTransition(immediateTransitionPANDFailsave);
// TODO: Extend for more than 2 children.
}
template <typename ValueType>
@ -200,7 +202,34 @@ namespace storm {
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawPOR(std::shared_ptr<storm::storage::DFTPor<ValueType> const> dftPor) {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a POR is not yet implemented.");
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(1);
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(1);
immediateTransitionPORFailsave.setWeight(0.0);
immediateTransitionPORFailsave.setInhibitionArcMultiplicity(placePORFailsave, 1);
immediateTransitionPORFailsave.setOutputArcMultiplicity(placePORFailsave, 1);
mGspn.addImmediateTransition(immediateTransitionPORFailsave);
// TODO: Extend for more than 2 children.
}
template <typename ValueType>
@ -279,7 +308,7 @@ namespace storm {
{
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 pandEntry2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + STR_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.
@ -302,7 +331,27 @@ namespace storm {
case storm::storage::DFTElementType::SPARE:
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 if (children[1] == child) { // Current element is secondary child.
porEntry2.second->setInputArcMultiplicity(childExit.second, 1);
porEntry2.second->setOutputArcMultiplicity(childExit.second, 1);
}
}
break;
}
case storm::storage::DFTElementType::SEQ:
break;
case storm::storage::DFTElementType::MUTEX:

2
src/transformations/dft/DftToGspnTransformator.h
View File

@ -36,6 +36,8 @@ namespace storm {
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.
/*!
* Write Gspn to file or console.

Write Preview
Loading…
Cancel
Save