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

Moved dynamic behavior computation from builder to DFT and added SEQ and SPARE cases

tempestpy_adaptions
Alexander Bork 6 years ago
parent
aa150fc2e3
commit
589555c75f
5 changed files with 170 additions and 92 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. 13
      src/storm-dft-cli/storm-dft.cpp
  2. 86
      src/storm-dft/builder/DFTBuilder.cpp
  3. 2
      src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
  4. 156
      src/storm-dft/storage/dft/DFT.cpp
  5. 5
      src/storm-dft/storage/dft/DFT.h

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

@ -92,6 +92,17 @@ void processOptions() {
}
#ifdef STORM_HAVE_Z3
if(debug.isTestSet()){
dft->setDynamicBehaviorInfo();
for(size_t i = 0; i < dft->nrElements(); ++i){
if(dft->getDynamicBehavior()[i]) {
STORM_LOG_DEBUG("Element " << dft->getElement(i)->name() << " has dynamic behavior");
} else {
STORM_LOG_DEBUG("Element " << dft->getElement(i)->name() << " has static behavior");
}
}
}
if (faultTreeSettings.solveWithSMT()) {
dft = dftTransformator.transformUniqueFailedBe(*dft);
if (dft->getDependencies().size() > 0) {
@ -100,6 +111,8 @@ void processOptions() {
}
// Solve with SMT
STORM_LOG_DEBUG("Running DFT analysis with use of SMT");
// Set dynamic behavior vector
dft->setDynamicBehaviorInfo();
storm::api::analyzeDFTSMT(*dft, true, debug.isTestSet());
return;
}

86
src/storm-dft/builder/DFTBuilder.cpp
View File

@ -97,7 +97,7 @@ namespace storm {
}
STORM_LOG_THROW(!mTopLevelIdentifier.empty(), storm::exceptions::WrongFormatException, "No top level element defined.");
storm::storage::DFT<ValueType> dft(elems, mElements[mTopLevelIdentifier], computeHasDynamicBehavior(elems));
storm::storage::DFT<ValueType> dft(elems, mElements[mTopLevelIdentifier]);
// Set layout info
for (auto& elem : mElements) {
@ -135,90 +135,6 @@ namespace storm {
return elem->rank();
}
template<typename ValueType>
std::vector<bool> DFTBuilder<ValueType>::computeHasDynamicBehavior(DFTElementVector elements) {
std::vector<bool> dynamicBehaviorVector(elements.size());
// Initialize with false
std::fill(dynamicBehaviorVector.begin(), dynamicBehaviorVector.end(), false);
std::queue<DFTElementPointer> elementQueue;
// deal with all dynamic elements
for (auto const &element : elements) {
switch (element->type()) {
case storage::DFTElementType::PAND:
case storage::DFTElementType::POR:
// TODO check SPAREs, SEQs, MUTEXs
case storage::DFTElementType::SPARE:
case storage::DFTElementType::SEQ:
case storage::DFTElementType::MUTEX: {
auto gate = std::static_pointer_cast<storm::storage::DFTGate<ValueType>>(element);
dynamicBehaviorVector[gate->id()] = true;
for (auto const &child : gate->children()) {
// only enqueue static children
if (!dynamicBehaviorVector.at(child->id())) {
elementQueue.push(child);
}
}
break;
}
default: {
break;
}
}
}
// propagate dynamic behavior
while (!elementQueue.empty()) {
DFTElementPointer currentElement = elementQueue.front();
elementQueue.pop();
switch (currentElement->type()) {
// Static Gates
case storage::DFTElementType::AND:
case storage::DFTElementType::OR:
case storage::DFTElementType::VOT: {
// check all parents and if one has dynamic behavior, propagate it
dynamicBehaviorVector[currentElement->id()] = true;
auto gate = std::static_pointer_cast<storm::storage::DFTGate<ValueType>>(currentElement);
for (auto const &child : gate->children()) {
// only enqueue static children
if (!dynamicBehaviorVector.at(child->id())) {
elementQueue.push(child);
}
}
break;
}
//BEs
case storage::DFTElementType::BE_EXP:
case storage::DFTElementType::BE_CONST:
case storage::DFTElementType::BE: {
auto be = std::static_pointer_cast<storm::storage::DFTBE<ValueType>>(currentElement);
dynamicBehaviorVector[be->id()] = true;
// add all ingoing dependencies to queue
for (auto const &dep : be->ingoingDependencies()) {
if (!dynamicBehaviorVector.at(dep->id())) {
elementQueue.push(dep);
}
}
break;
}
case storage::DFTElementType::PDEP: {
auto dep = std::static_pointer_cast<storm::storage::DFTDependency<ValueType>>(currentElement);
dynamicBehaviorVector[dep->id()] = true;
// add all ingoing dependencies to queue
auto trigger = dep->triggerEvent();
if (!dynamicBehaviorVector.at(trigger->id())) {
elementQueue.push(trigger);
}
break;
}
default:
break;
}
}
return dynamicBehaviorVector;
}
template<typename ValueType>
bool DFTBuilder<ValueType>::addRestriction(std::string const& name, std::vector<std::string> const& children, storm::storage::DFTElementType tp) {
if (children.size() <= 1) {

2
src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
View File

@ -948,7 +948,7 @@ namespace storm {
dep1Index = dft.getDependencies().at(i);
for (size_t j = i + 1; j < dft.getDependencies().size(); ++j) {
dep2Index = dft.getDependencies().at(j);
if (dft.getDynamicBehavior()[dep1Index] || dft.getDynamicBehavior()[dep2Index]) {
if (dft.getDynamicBehavior()[dep1Index] && dft.getDynamicBehavior()[dep2Index]) {
if (dft.getDependency(dep1Index)->triggerEvent() ==
dft.getDependency(dep2Index)->triggerEvent()) {
STORM_LOG_DEBUG("Conflict between " << dft.getElement(dep1Index)->name() << " and "

156
src/storm-dft/storage/dft/DFT.cpp
View File

@ -17,12 +17,15 @@ namespace storm {
namespace storage {
template<typename ValueType>
DFT<ValueType>::DFT(DFTElementVector const &elements, DFTElementPointer const &tle,
std::vector<bool> const &dynamicBehavior) :
mElements(elements), mNrOfBEs(0), mNrOfSpares(0), mTopLevelIndex(tle->id()), mMaxSpareChildCount(0),
mDynamicBehavior(dynamicBehavior) {
DFT<ValueType>::DFT(DFTElementVector const &elements, DFTElementPointer const &tle) :
mElements(elements), mNrOfBEs(0), mNrOfSpares(0), mTopLevelIndex(tle->id()), mMaxSpareChildCount(0) {
// Check that ids correspond to indices in the element vector
STORM_LOG_ASSERT(elementIndicesCorrect(), "Ids incorrect.");
// Initialize dynamic behavior vector with TRUE to preserve correct behavior
// We don't directly call setDynamicBehaviorInfo to not slow down DFT generation if possible
mDynamicBehavior = std::vector<bool>(mElements.size());
std::fill(mDynamicBehavior.begin(), mDynamicBehavior.end(), true);
size_t nrRepresentatives = 0;
for (auto& elem : mElements) {
@ -88,6 +91,151 @@ namespace storm {
mStateVectorSize = nrElements() * 2 + mNrOfSpares * usageInfoBits + nrRepresentatives;
}
template<typename ValueType>
void DFT<ValueType>::setDynamicBehaviorInfo() {
std::vector<bool> dynamicBehaviorVector(mElements.size());
std::queue <DFTElementPointer> elementQueue;
// deal with all dynamic elements
for (auto const &element : mElements) {
switch (element->type()) {
case storage::DFTElementType::PAND:
case storage::DFTElementType::POR:
case storage::DFTElementType::MUTEX: {
auto gate = std::static_pointer_cast<storm::storage::DFTChildren<ValueType>>(element);
dynamicBehaviorVector[gate->id()] = true;
for (auto const &child : gate->children()) {
// only enqueue static children
if (!dynamicBehaviorVector.at(child->id())) {
elementQueue.push(child);
}
}
break;
}
// TODO different cases
case storage::DFTElementType::SPARE: {
auto spare = std::static_pointer_cast<storm::storage::DFTSpare<ValueType>>(element);
// Iterate over all children (representatives of spare modules)
for (auto const &child : spare->children()) {
// Case 1: Shared Module
// If child only has one parent, it is this SPARE -> nothing to check
if (child->nrParents() > 1) {
// TODO make more efficient by directly setting ALL spares which share a module to be dynamic
for (auto const &parent : child->parents()) {
if (parent->isSpareGate() and parent->id() != spare->id()) {
dynamicBehaviorVector[spare->id()] = true;
break; // inner loop
}
}
}
// Case 2: Triggering outside events
// If the SPARE was already detected to have dynamic behavior, do not proceed
if (!dynamicBehaviorVector[spare->id()]) {
for (auto const &memberID : module(child->id())) {
// Iterate over all members of the module child represents
auto member = getElement(memberID);
for (auto const dep : member->outgoingDependencies()) {
// If the member has outgoing dependencies, check if those trigger something outside the module
for (auto const depEvent : dep->dependentEvents()) {
// If a dependent event is not found in the module, SPARE is dynamic
if (std::find(module(child->id()).begin(), module(child->id()).end(),
depEvent->id()) == module(child->id()).end()) {
dynamicBehaviorVector[spare->id()] = true;
break; //depEvent-loop
}
}
if (dynamicBehaviorVector[spare->id()]) { break; } //dependency-loop
}
if (dynamicBehaviorVector[spare->id()]) { break; } //module-loop
}
}
if (dynamicBehaviorVector[spare->id()]) { break; } //child-loop
}
// if during the computation, dynamic behavior was detected, add children to queue
if (dynamicBehaviorVector[spare->id()]) {
for (auto const &child : spare->children()) {
// only enqueue static children
if (!dynamicBehaviorVector.at(child->id())) {
elementQueue.push(child);
}
}
}
break;
}
case storage::DFTElementType::SEQ: {
auto seq = std::static_pointer_cast<storm::storage::DFTSeq<ValueType>>(element);
// A SEQ only has dynamic behavior if not all children are BEs
if (!seq->allChildrenBEs()) {
dynamicBehaviorVector[seq->id()] = true;
for (auto const &child : seq->children()) {
// only enqueue static children
if (!dynamicBehaviorVector.at(child->id())) {
elementQueue.push(child);
}
}
}
break;
}
default: {
break;
}
}
}
// propagate dynamic behavior
while (!elementQueue.empty()) {
DFTElementPointer currentElement = elementQueue.front();
elementQueue.pop();
switch (currentElement->type()) {
// Static Gates
case storage::DFTElementType::AND:
case storage::DFTElementType::OR:
case storage::DFTElementType::VOT: {
// check all parents and if one has dynamic behavior, propagate it
dynamicBehaviorVector[currentElement->id()] = true;
auto gate = std::static_pointer_cast<storm::storage::DFTGate<ValueType>>(currentElement);
for (auto const &child : gate->children()) {
// only enqueue static children
if (!dynamicBehaviorVector.at(child->id())) {
elementQueue.push(child);
}
}
break;
}
//BEs
case storage::DFTElementType::BE_EXP:
case storage::DFTElementType::BE_CONST:
case storage::DFTElementType::BE: {
auto be = std::static_pointer_cast<storm::storage::DFTBE<ValueType>>(currentElement);
dynamicBehaviorVector[be->id()] = true;
// add all ingoing dependencies to queue
for (auto const &dep : be->ingoingDependencies()) {
if (!dynamicBehaviorVector.at(dep->id())) {
elementQueue.push(dep);
}
}
break;
}
case storage::DFTElementType::PDEP: {
auto dep = std::static_pointer_cast<storm::storage::DFTDependency<ValueType>>(currentElement);
dynamicBehaviorVector[dep->id()] = true;
// add all ingoing dependencies to queue
auto trigger = dep->triggerEvent();
if (!dynamicBehaviorVector.at(trigger->id())) {
elementQueue.push(trigger);
}
break;
}
default:
break;
}
}
mDynamicBehavior = dynamicBehaviorVector;
}
template<typename ValueType>
DFTStateGenerationInfo DFT<ValueType>::buildStateGenerationInfo(storm::storage::DFTIndependentSymmetries const& symmetries) const {
DFTStateGenerationInfo generationInfo(nrElements(), mMaxSpareChildCount);

5
src/storm-dft/storage/dft/DFT.h
View File

@ -70,8 +70,7 @@ namespace storm {
std::vector<bool> mDynamicBehavior;
public:
DFT(DFTElementVector const &elements, DFTElementPointer const &tle,
std::vector<bool> const &dynamicBehavior);
DFT(DFTElementVector const &elements, DFTElementPointer const &tle);
DFTStateGenerationInfo buildStateGenerationInfo(storm::storage::DFTIndependentSymmetries const& symmetries) const;
@ -82,6 +81,8 @@ namespace storm {
DFT<ValueType> optimize() const;
void copyElements(std::vector<size_t> elements, storm::builder::DFTBuilder<ValueType> builder) const;
void setDynamicBehaviorInfo();
size_t stateBitVectorSize() const {
// Ensure multiple of 64
Write Preview
Loading…
Cancel
Save