Browse Source

POR[inclusive] support seems to be working now

main
Sebastian Junges 8 years ago
parent
commit
80d578d130
  1. 14
      src/storm-dft/transformations/DftToGspnTransformator.cpp

14
src/storm-dft/transformations/DftToGspnTransformator.cpp

@ -233,6 +233,8 @@ namespace storm {
unavailableNode = addUnavailableNode(dftPand);
}
if(dftPand->isInclusive()) {
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);
@ -254,6 +256,9 @@ namespace storm {
builder.addInhibitionArc(nodeFS, tfs);
}
} else {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "NOt yet implemented");
}
}
//
template <typename ValueType>
@ -318,6 +323,7 @@ namespace storm {
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawPOR(std::shared_ptr<storm::storage::DFTPor<ValueType> const> dftPor, bool isRepresentative) {
uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftPor->name() + STR_FAILED);
failedNodes.push_back(nodeFailed);
uint64_t nodeFS = builder.addPlace(defaultCapacity, 0, dftPor->name() + STR_FAILSAVE);
@ -329,11 +335,15 @@ namespace storm {
builder.addInhibitionArc(nodeFailed, tfail);
uint64_t j = 0;
for (auto const& child : dftPor->children()) {
if(j > 0) {
uint64_t tfailsf = builder.addImmediateTransition(getFailPriority(dftPor), 0.0, dftPor->name() + STR_FAILSAVING + std::to_string(j));
builder.addInputArc(failedNodes.at(child->id()), tfailsf);
builder.addOutputArc(tfailsf, failedNodes.at(child->id()));
// TODO
// builder.addInhibitionArc(<#const uint_fast64_t &from#>, <#const uint_fast64_t &to#>)
builder.addOutputArc(tfailsf, nodeFS);
builder.addInhibitionArc(nodeFS, tfailsf);
builder.addInhibitionArc(failedNodes.at(dftPor->children().front()->id()), tfailsf);
}
++j;
}
}

Loading…
Cancel
Save