sjunges
9 years ago
45 changed files with 1679 additions and 224 deletions
-
60src/storm-dft-cli/storm-dyftee.cpp
-
2src/storm-dft/CMakeLists.txt
-
1src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
-
18src/storm-dft/parser/DFTGalileoParser.cpp
-
5src/storm-dft/parser/DFTGalileoParser.h
-
167src/storm-dft/parser/DFTJsonParser.cpp
-
48src/storm-dft/parser/DFTJsonParser.h
-
14src/storm-dft/settings/modules/DFTSettings.cpp
-
16src/storm-dft/settings/modules/DFTSettings.h
-
11src/storm-dft/storage/dft/DFT.cpp
-
19src/storm-dft/storage/dft/DFT.h
-
78src/storm-dft/storage/dft/DFTBuilder.cpp
-
63src/storm-dft/storage/dft/DFTBuilder.h
-
23src/storm-dft/storage/dft/DFTIsomorphism.h
-
15src/storm-dft/storage/dft/DFTLayoutInfo.h
-
14src/storm-dft/storage/dft/DFTState.cpp
-
3src/storm-dft/storage/dft/elements/DFTBE.h
-
46src/storm-dft/storage/dft/elements/DFTDependency.h
-
4src/storm-dft/storage/dft/elements/DFTElement.cpp
-
15src/storm-dft/storage/dft/elements/DFTPand.h
-
17src/storm-dft/storage/dft/elements/DFTPor.h
-
9src/storm-dft/storage/dft/elements/DFTRestriction.h
-
629src/storm-dft/transformations/DftToGspnTransformator.cpp
-
163src/storm-dft/transformations/DftToGspnTransformator.h
-
4src/storm-gspn-cli/storm-gspn.cpp
-
169src/storm-gspn/builder/JaniGSPNBuilder.h
-
58src/storm-gspn/storage/gspn/GSPN.cpp
-
23src/storm-gspn/storage/gspn/GSPN.h
-
16src/storm-gspn/storage/gspn/GspnBuilder.cpp
-
14src/storm-gspn/storage/gspn/GspnBuilder.h
-
17src/storm-gspn/storage/gspn/PlacementInfo.h
-
3src/storm-gspn/storage/gspn/Transition.h
-
60src/storm-gspn/storm-gspn.h
-
11src/storm/cli/cli.cpp
-
2src/storm/generator/NextStateGenerator.cpp
-
16src/storm/settings/modules/GSPNExportSettings.cpp
-
11src/storm/settings/modules/GSPNExportSettings.h
-
2src/storm/storage/BitVector.cpp
-
6src/storm/storage/expressions/Expression.cpp
-
10src/storm/storage/jani/JSONExporter.cpp
-
8src/storm/storage/jani/JSONExporter.h
-
9src/storm/storage/jani/OrderedAssignments.cpp
-
2src/storm/storage/jani/OrderedAssignments.h
-
11src/storm/utility/storm.cpp
-
11src/storm/utility/storm.h
@ -0,0 +1,167 @@ |
|||||
|
#include "DFTJsonParser.h"
|
||||
|
|
||||
|
#include <iostream>
|
||||
|
#include <fstream>
|
||||
|
#include <boost/algorithm/string.hpp>
|
||||
|
#include <boost/lexical_cast.hpp>
|
||||
|
#include <boost/algorithm/string/replace.hpp>
|
||||
|
#include "storm/storage/expressions/ExpressionManager.h"
|
||||
|
#include "storm/exceptions/NotImplementedException.h"
|
||||
|
#include "storm/exceptions/FileIoException.h"
|
||||
|
#include "storm/exceptions/NotSupportedException.h"
|
||||
|
#include "storm/utility/macros.h"
|
||||
|
|
||||
|
namespace storm { |
||||
|
namespace parser { |
||||
|
|
||||
|
template<typename ValueType> |
||||
|
storm::storage::DFT<ValueType> DFTJsonParser<ValueType>::parseJson(const std::string& filename) { |
||||
|
readFile(filename); |
||||
|
storm::storage::DFT<ValueType> dft = builder.build(); |
||||
|
STORM_LOG_DEBUG("Elements:" << std::endl << dft.getElementsString()); |
||||
|
STORM_LOG_DEBUG("Spare Modules:" << std::endl << dft.getSpareModulesString()); |
||||
|
return dft; |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType> |
||||
|
std::string DFTJsonParser<ValueType>::stripQuotsFromName(std::string const& name) { |
||||
|
size_t firstQuots = name.find("\""); |
||||
|
size_t secondQuots = name.find("\"", firstQuots+1); |
||||
|
|
||||
|
if(firstQuots == std::string::npos) { |
||||
|
return name; |
||||
|
} else { |
||||
|
STORM_LOG_THROW(secondQuots != std::string::npos, storm::exceptions::FileIoException, "No ending quotation mark found in " << name); |
||||
|
return name.substr(firstQuots+1,secondQuots-1); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType> |
||||
|
std::string DFTJsonParser<ValueType>::getString(json const& structure, std::string const& errorInfo) { |
||||
|
STORM_LOG_THROW(structure.is_string(), storm::exceptions::FileIoException, "Expected a string in " << errorInfo << ", got '" << structure.dump() << "'"); |
||||
|
return structure.front(); |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType> |
||||
|
std::string DFTJsonParser<ValueType>::parseNodeIdentifier(std::string const& name) { |
||||
|
return boost::replace_all_copy(name, "'", "__prime__"); |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType> |
||||
|
void DFTJsonParser<ValueType>::readFile(const std::string& filename) { |
||||
|
STORM_LOG_DEBUG("Parsing from JSON"); |
||||
|
|
||||
|
std::ifstream file; |
||||
|
file.exceptions ( std::ifstream::failbit ); |
||||
|
try { |
||||
|
file.open(filename); |
||||
|
} |
||||
|
catch (std::ifstream::failure e) { |
||||
|
STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Exception during file opening on " << filename << "."); |
||||
|
return; |
||||
|
} |
||||
|
file.exceptions( std::ifstream::goodbit ); |
||||
|
|
||||
|
json parsedJson; |
||||
|
parsedJson << file; |
||||
|
file.close(); |
||||
|
|
||||
|
// Start by building mapping from ids to names
|
||||
|
std::map<std::string, std::string> nameMapping; |
||||
|
for (auto& element: parsedJson) { |
||||
|
if (element.at("classes") != "") { |
||||
|
json data = element.at("data"); |
||||
|
std::string id = data.at("id"); |
||||
|
std::string name = data.at("name"); |
||||
|
nameMapping[id] = name; |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
// TODO: avoid hack
|
||||
|
std::string toplevelId = nameMapping["1"]; |
||||
|
|
||||
|
for (auto& element : parsedJson) { |
||||
|
bool success = true; |
||||
|
if (element.at("classes") == "") { |
||||
|
continue; |
||||
|
} |
||||
|
json data = element.at("data"); |
||||
|
std::string name = data.at("name"); |
||||
|
std::vector<std::string> childNames; |
||||
|
if (data.count("children") > 0) { |
||||
|
for (auto& child : data.at("children")) { |
||||
|
childNames.push_back(nameMapping[child]); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
std::string type = getString(element.at("classes"), "classes"); |
||||
|
|
||||
|
if(type == "and") { |
||||
|
success = builder.addAndElement(name, childNames); |
||||
|
} else if (type == "or") { |
||||
|
success = builder.addOrElement(name, childNames); |
||||
|
} else if (type == "pand") { |
||||
|
success = builder.addPandElement(name, childNames); |
||||
|
} else if (type == "por") { |
||||
|
success = builder.addPorElement(name, childNames); |
||||
|
} else if (type == "spare") { |
||||
|
success = builder.addSpareElement(name, childNames); |
||||
|
} else if (type == "seq") { |
||||
|
success = builder.addSequenceEnforcer(name, childNames); |
||||
|
} else if (type== "fdep") { |
||||
|
success = builder.addDepElement(name, childNames, storm::utility::one<ValueType>()); |
||||
|
} else if (type== "pdep") { |
||||
|
ValueType probability = parseRationalExpression(data.at("prob")); |
||||
|
success = builder.addDepElement(name, childNames, probability); |
||||
|
} else if (type == "be") { |
||||
|
ValueType failureRate = parseRationalExpression(data.at("rate")); |
||||
|
ValueType dormancyFactor = parseRationalExpression(data.at("dorm")); |
||||
|
success = builder.addBasicElement(name, failureRate, dormancyFactor); |
||||
|
} else { |
||||
|
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Type name: " << type << " not recognized."); |
||||
|
success = false; |
||||
|
} |
||||
|
|
||||
|
// Set layout positions
|
||||
|
json position = element.at("position"); |
||||
|
double x = position.at("x"); |
||||
|
double y = position.at("y"); |
||||
|
builder.addLayoutInfo(name, x / 7, y / 7); |
||||
|
STORM_LOG_THROW(success, storm::exceptions::FileIoException, "Error while adding element '" << element << "'."); |
||||
|
} |
||||
|
|
||||
|
if(!builder.setTopLevel(toplevelId)) { |
||||
|
STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Top level id unknown."); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType> |
||||
|
ValueType DFTJsonParser<ValueType>::parseRationalExpression(std::string const& expr) { |
||||
|
STORM_LOG_ASSERT(false, "Specialized method should be called."); |
||||
|
return 0; |
||||
|
} |
||||
|
|
||||
|
template<> |
||||
|
double DFTJsonParser<double>::parseRationalExpression(std::string const& expr) { |
||||
|
return boost::lexical_cast<double>(expr); |
||||
|
} |
||||
|
|
||||
|
// Explicitly instantiate the class.
|
||||
|
template class DFTJsonParser<double>; |
||||
|
|
||||
|
#ifdef STORM_HAVE_CARL
|
||||
|
template<> |
||||
|
storm::RationalFunction DFTJsonParser<storm::RationalFunction>::parseRationalExpression(std::string const& expr) { |
||||
|
STORM_LOG_TRACE("Translating expression: " << expr); |
||||
|
storm::expressions::Expression expression = parser.parseFromString(expr); |
||||
|
STORM_LOG_TRACE("Expression: " << expression); |
||||
|
storm::RationalFunction rationalFunction = evaluator.asRational(expression); |
||||
|
STORM_LOG_TRACE("Parsed expression: " << rationalFunction); |
||||
|
return rationalFunction; |
||||
|
} |
||||
|
|
||||
|
template class DFTJsonParser<RationalFunction>; |
||||
|
#endif
|
||||
|
|
||||
|
} |
||||
|
} |
||||
@ -0,0 +1,48 @@ |
|||||
|
#pragma once |
||||
|
|
||||
|
#include <map> |
||||
|
|
||||
|
#include "storm/storage/expressions/ExpressionManager.h" |
||||
|
#include "storm/parser/ExpressionParser.h" |
||||
|
#include "storm/storage/expressions/ExpressionEvaluator.h" |
||||
|
|
||||
|
#include "storm-dft/storage/dft/DFT.h" |
||||
|
#include "storm-dft/storage/dft/DFTBuilder.h" |
||||
|
|
||||
|
// JSON parser |
||||
|
#include "json.hpp" |
||||
|
|
||||
|
using json = nlohmann::json; |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace parser { |
||||
|
|
||||
|
template<typename ValueType> |
||||
|
class DFTJsonParser { |
||||
|
storm::storage::DFTBuilder<ValueType> builder; |
||||
|
|
||||
|
std::shared_ptr<storm::expressions::ExpressionManager> manager; |
||||
|
|
||||
|
storm::parser::ExpressionParser parser; |
||||
|
|
||||
|
storm::expressions::ExpressionEvaluator<ValueType> evaluator; |
||||
|
|
||||
|
std::unordered_map<std::string, storm::expressions::Expression> identifierMapping; |
||||
|
|
||||
|
public: |
||||
|
DFTJsonParser() : manager(new storm::expressions::ExpressionManager()), parser(*manager), evaluator(*manager) { |
||||
|
} |
||||
|
|
||||
|
storm::storage::DFT<ValueType> parseJson(std::string const& filename); |
||||
|
|
||||
|
private: |
||||
|
void readFile(std::string const& filename); |
||||
|
|
||||
|
std::string stripQuotsFromName(std::string const& name); |
||||
|
std::string parseNodeIdentifier(std::string const& name); |
||||
|
std::string getString(json const& structure, std::string const& errorInfo); |
||||
|
|
||||
|
ValueType parseRationalExpression(std::string const& expr); |
||||
|
}; |
||||
|
} |
||||
|
} |
||||
@ -0,0 +1,15 @@ |
|||||
|
#pragma once |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace storage { |
||||
|
struct DFTLayoutInfo { |
||||
|
DFTLayoutInfo() {}; |
||||
|
DFTLayoutInfo(double x, double y) : x(x), y(y) {}; |
||||
|
|
||||
|
// x location |
||||
|
double x = 0.0; |
||||
|
// y location |
||||
|
double y = 0.0; |
||||
|
}; |
||||
|
} |
||||
|
} |
||||
@ -0,0 +1,629 @@ |
|||||
|
#include "DftToGspnTransformator.h"
|
||||
|
#include "storm/exceptions/NotImplementedException.h"
|
||||
|
#include <memory>
|
||||
|
|
||||
|
namespace storm { |
||||
|
namespace transformations { |
||||
|
namespace dft { |
||||
|
|
||||
|
// Prevent some magic constants
|
||||
|
static constexpr const uint64_t defaultPriority = 1; |
||||
|
static constexpr const uint64_t defaultCapacity = 1; |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
DftToGspnTransformator<ValueType>::DftToGspnTransformator(storm::storage::DFT<ValueType> const& dft) : mDft(dft) { |
||||
|
// Intentionally left empty.
|
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void DftToGspnTransformator<ValueType>::transform() { |
||||
|
|
||||
|
builder.setGspnName("DftToGspnTransformation"); |
||||
|
|
||||
|
// Loop through every DFT element and draw them as a GSPN.
|
||||
|
drawGSPNElements(); |
||||
|
|
||||
|
// Draw restrictions into the GSPN (i.e. SEQ or MUTEX).
|
||||
|
//drawGSPNRestrictions();
|
||||
|
} |
||||
|
|
||||
|
template<typename ValueType> |
||||
|
uint64_t DftToGspnTransformator<ValueType>::toplevelFailedPlaceId() { |
||||
|
assert(failedNodes.size() > mDft.getTopLevelIndex()); |
||||
|
return failedNodes[mDft.getTopLevelIndex()]; |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void DftToGspnTransformator<ValueType>::drawGSPNElements() { |
||||
|
|
||||
|
|
||||
|
// Loop through every DFT element and draw them as a GSPN.
|
||||
|
for (std::size_t i = 0; i < mDft.nrElements(); i++) { |
||||
|
auto dftElement = mDft.getElement(i); |
||||
|
bool isRepresentative = mDft.isRepresentative(i); |
||||
|
|
||||
|
// Check which type the element is and call the corresponding drawing-function.
|
||||
|
switch (dftElement->type()) { |
||||
|
case storm::storage::DFTElementType::AND: |
||||
|
drawAND(std::static_pointer_cast<storm::storage::DFTAnd<ValueType> const>(dftElement), isRepresentative); |
||||
|
break; |
||||
|
case storm::storage::DFTElementType::OR: |
||||
|
drawOR(std::static_pointer_cast<storm::storage::DFTOr<ValueType> const>(dftElement), isRepresentative); |
||||
|
break; |
||||
|
case storm::storage::DFTElementType::VOT: |
||||
|
drawVOT(std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(dftElement), isRepresentative); |
||||
|
break; |
||||
|
case storm::storage::DFTElementType::PAND: |
||||
|
drawPAND(std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(dftElement), isRepresentative); |
||||
|
break; |
||||
|
case storm::storage::DFTElementType::SPARE: |
||||
|
drawSPARE(std::static_pointer_cast<storm::storage::DFTSpare<ValueType> const>(dftElement), isRepresentative); |
||||
|
break; |
||||
|
case storm::storage::DFTElementType::POR: |
||||
|
drawPOR(std::static_pointer_cast<storm::storage::DFTPor<ValueType> const>(dftElement), isRepresentative); |
||||
|
break; |
||||
|
case storm::storage::DFTElementType::SEQ: |
||||
|
drawSeq(std::static_pointer_cast<storm::storage::DFTSeq<ValueType> const>(dftElement)); |
||||
|
break; |
||||
|
case storm::storage::DFTElementType::MUTEX: |
||||
|
// No method call needed here. MUTEX only consists of restrictions, which are handled later.
|
||||
|
break; |
||||
|
case storm::storage::DFTElementType::BE: |
||||
|
drawBE(std::static_pointer_cast<storm::storage::DFTBE<ValueType> const>(dftElement), isRepresentative); |
||||
|
break; |
||||
|
case storm::storage::DFTElementType::CONSTF: |
||||
|
drawCONSTF(dftElement, isRepresentative); |
||||
|
break; |
||||
|
case storm::storage::DFTElementType::CONSTS: |
||||
|
drawCONSTS(dftElement, isRepresentative); |
||||
|
break; |
||||
|
case storm::storage::DFTElementType::PDEP: |
||||
|
drawPDEP(std::static_pointer_cast<storm::storage::DFTDependency<ValueType> const>(dftElement)); |
||||
|
break; |
||||
|
default: |
||||
|
STORM_LOG_ASSERT(false, "DFT type unknown."); |
||||
|
break; |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void DftToGspnTransformator<ValueType>::drawBE(std::shared_ptr<storm::storage::DFTBE<ValueType> const> dftBE, bool isRepresentative) { |
||||
|
uint64_t beActive = builder.addPlace(defaultCapacity, isBEActive(dftBE) ? 1 : 0, dftBE->name() + STR_ACTIVATED); |
||||
|
activeNodes.emplace(dftBE->id(), beActive); |
||||
|
uint64_t beFailed = builder.addPlace(defaultCapacity, 0, dftBE->name() + STR_FAILED); |
||||
|
|
||||
|
double xcenter = mDft.getElementLayoutInfo(dftBE->id()).x; |
||||
|
double ycenter = mDft.getElementLayoutInfo(dftBE->id()).y; |
||||
|
builder.setPlaceLayoutInfo(beActive, storm::gspn::LayoutInfo(xcenter - 3.0, ycenter)); |
||||
|
builder.setPlaceLayoutInfo(beFailed, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter)); |
||||
|
|
||||
|
|
||||
|
uint64_t disabledNode = 0; |
||||
|
if (!smart || dftBE->nrRestrictions() > 0) { |
||||
|
disabledNode = addDisabledPlace(dftBE); |
||||
|
} |
||||
|
|
||||
|
uint64_t unavailableNode = 0; |
||||
|
if (!smart || isRepresentative) { |
||||
|
unavailableNode = addUnavailableNode(dftBE, storm::gspn::LayoutInfo(xcenter+9.0, ycenter)); |
||||
|
} |
||||
|
|
||||
|
assert(failedNodes.size() == dftBE->id()); |
||||
|
failedNodes.push_back(beFailed); |
||||
|
uint64_t tActive = builder.addTimedTransition(defaultPriority, dftBE->activeFailureRate(), dftBE->name() + "_activeFailing"); |
||||
|
builder.setTransitionLayoutInfo(tActive, storm::gspn::LayoutInfo(xcenter, ycenter + 3.0)); |
||||
|
builder.addInputArc(beActive, tActive); |
||||
|
builder.addInhibitionArc(beFailed, tActive); |
||||
|
builder.addOutputArc(tActive, beActive); |
||||
|
builder.addOutputArc(tActive, beFailed); |
||||
|
uint64_t tPassive = builder.addTimedTransition(defaultPriority, dftBE->passiveFailureRate(), dftBE->name() + "_passiveFailing"); |
||||
|
builder.setTransitionLayoutInfo(tPassive, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0)); |
||||
|
builder.addInhibitionArc(beActive, tPassive); |
||||
|
builder.addInhibitionArc(beFailed, tPassive); |
||||
|
builder.addOutputArc(tPassive, beFailed); |
||||
|
|
||||
|
if (!smart || dftBE->nrRestrictions() > 0) { |
||||
|
builder.addInhibitionArc(disabledNode, tActive); |
||||
|
builder.addInhibitionArc(disabledNode, tPassive); |
||||
|
} |
||||
|
|
||||
|
if (!smart || isRepresentative) { |
||||
|
builder.addOutputArc(tActive, unavailableNode); |
||||
|
builder.addOutputArc(tPassive, unavailableNode); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void DftToGspnTransformator<ValueType>::drawAND(std::shared_ptr<storm::storage::DFTAnd<ValueType> const> dftAnd, bool isRepresentative) { |
||||
|
uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftAnd->name() + STR_FAILED); |
||||
|
assert(failedNodes.size() == dftAnd->id()); |
||||
|
failedNodes.push_back(nodeFailed); |
||||
|
|
||||
|
double xcenter = mDft.getElementLayoutInfo(dftAnd->id()).x; |
||||
|
double ycenter = mDft.getElementLayoutInfo(dftAnd->id()).y; |
||||
|
builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter, ycenter-3.0)); |
||||
|
|
||||
|
uint64_t unavailableNode = 0; |
||||
|
if (isRepresentative) { |
||||
|
unavailableNode = addUnavailableNode(dftAnd, storm::gspn::LayoutInfo(xcenter+6.0, ycenter-3.0)); |
||||
|
} |
||||
|
|
||||
|
|
||||
|
uint64_t tAndFailed = builder.addImmediateTransition( getFailPriority(dftAnd) , 0.0, dftAnd->name() + STR_FAILING ); |
||||
|
builder.setTransitionLayoutInfo(tAndFailed, storm::gspn::LayoutInfo(xcenter, ycenter+3.0)); |
||||
|
builder.addInhibitionArc(nodeFailed, tAndFailed); |
||||
|
builder.addOutputArc(tAndFailed, nodeFailed); |
||||
|
if (isRepresentative) { |
||||
|
builder.addOutputArc(tAndFailed, unavailableNode); |
||||
|
} |
||||
|
for(auto const& child : dftAnd->children()) { |
||||
|
assert(failedNodes.size() > child->id()); |
||||
|
builder.addInputArc(failedNodes[child->id()], tAndFailed); |
||||
|
builder.addOutputArc(tAndFailed, failedNodes[child->id()]); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void DftToGspnTransformator<ValueType>::drawOR(std::shared_ptr<storm::storage::DFTOr<ValueType> const> dftOr, bool isRepresentative) { |
||||
|
uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftOr->name() + STR_FAILED); |
||||
|
assert(failedNodes.size() == dftOr->id()); |
||||
|
failedNodes.push_back(nodeFailed); |
||||
|
|
||||
|
double xcenter = mDft.getElementLayoutInfo(dftOr->id()).x; |
||||
|
double ycenter = mDft.getElementLayoutInfo(dftOr->id()).y; |
||||
|
builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter, ycenter-3.0)); |
||||
|
|
||||
|
uint64_t unavailableNode = 0; |
||||
|
if (isRepresentative) { |
||||
|
unavailableNode = addUnavailableNode(dftOr, storm::gspn::LayoutInfo(xcenter+6.0, ycenter-3.0)); |
||||
|
} |
||||
|
|
||||
|
uint64_t i = 0; |
||||
|
for (auto const& child : dftOr->children()) { |
||||
|
uint64_t tNodeFailed = builder.addImmediateTransition( getFailPriority(dftOr), 0.0, dftOr->name() + STR_FAILING + std::to_string(i) ); |
||||
|
builder.setTransitionLayoutInfo(tNodeFailed, storm::gspn::LayoutInfo(xcenter-5.0+i*3.0, ycenter+3.0)); |
||||
|
builder.addInhibitionArc(nodeFailed, tNodeFailed); |
||||
|
builder.addOutputArc(tNodeFailed, nodeFailed); |
||||
|
if (isRepresentative) { |
||||
|
builder.addOutputArc(tNodeFailed, unavailableNode); |
||||
|
} |
||||
|
assert(failedNodes.size() > child->id()); |
||||
|
builder.addInputArc(failedNodes[child->id()], tNodeFailed); |
||||
|
builder.addOutputArc(tNodeFailed, failedNodes[child->id()]); |
||||
|
++i; |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void DftToGspnTransformator<ValueType>::drawVOT(std::shared_ptr<storm::storage::DFTVot<ValueType> const> dftVot, bool isRepresentative) { |
||||
|
// TODO: finish layouting
|
||||
|
uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftVot->name() + STR_FAILED); |
||||
|
assert(failedNodes.size() == dftVot->id()); |
||||
|
failedNodes.push_back(nodeFailed); |
||||
|
|
||||
|
double xcenter = mDft.getElementLayoutInfo(dftVot->id()).x; |
||||
|
double ycenter = mDft.getElementLayoutInfo(dftVot->id()).y; |
||||
|
builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter, ycenter-3.0)); |
||||
|
|
||||
|
uint64_t unavailableNode = 0; |
||||
|
if (isRepresentative) { |
||||
|
unavailableNode = addUnavailableNode(dftVot, storm::gspn::LayoutInfo(xcenter+6.0, ycenter-3.0)); |
||||
|
} |
||||
|
|
||||
|
uint64_t nodeCollector = builder.addPlace(dftVot->nrChildren(), 0, dftVot->name() + "_collector"); |
||||
|
builder.setPlaceLayoutInfo(nodeCollector, storm::gspn::LayoutInfo(xcenter, ycenter)); |
||||
|
|
||||
|
uint64_t tNodeFailed = builder.addImmediateTransition(getFailPriority(dftVot), 0.0, dftVot->name() + STR_FAILING); |
||||
|
builder.addOutputArc(tNodeFailed, nodeFailed); |
||||
|
if (isRepresentative) { |
||||
|
builder.addOutputArc(tNodeFailed, unavailableNode); |
||||
|
} |
||||
|
builder.addInhibitionArc(nodeFailed, tNodeFailed); |
||||
|
builder.addInputArc(nodeCollector, tNodeFailed, dftVot->threshold()); |
||||
|
builder.addOutputArc(tNodeFailed, nodeCollector, dftVot->threshold()); |
||||
|
uint64_t i = 0; |
||||
|
for (auto const& child : dftVot->children()) { |
||||
|
uint64_t childInhibPlace = builder.addPlace(1, 0, dftVot->name() + "_child_fail_inhib" + std::to_string(i)); |
||||
|
uint64_t tCollect = builder.addImmediateTransition(getFailPriority(dftVot), 0.0, dftVot->name() + "_child_collect" + std::to_string(i)); |
||||
|
builder.addOutputArc(tCollect, nodeCollector); |
||||
|
builder.addOutputArc(tCollect, childInhibPlace); |
||||
|
builder.addInhibitionArc(childInhibPlace, tCollect); |
||||
|
builder.addInputArc(failedNodes[child->id()], tCollect); |
||||
|
builder.addOutputArc(tCollect, failedNodes[child->id()]); |
||||
|
++i; |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void DftToGspnTransformator<ValueType>::drawPAND(std::shared_ptr<storm::storage::DFTPand<ValueType> const> dftPand, bool isRepresentative) { |
||||
|
uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftPand->name() + STR_FAILED); |
||||
|
assert(failedNodes.size() == dftPand->id()); |
||||
|
failedNodes.push_back(nodeFailed); |
||||
|
|
||||
|
double xcenter = mDft.getElementLayoutInfo(dftPand->id()).x; |
||||
|
double ycenter = mDft.getElementLayoutInfo(dftPand->id()).y; |
||||
|
builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter+3.0, ycenter-3.0)); |
||||
|
|
||||
|
uint64_t unavailableNode = 0; |
||||
|
if (!smart || isRepresentative) { |
||||
|
unavailableNode = addUnavailableNode(dftPand, storm::gspn::LayoutInfo(xcenter+9.0, ycenter-3.0)); |
||||
|
} |
||||
|
|
||||
|
uint64_t tNodeFailed = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILING); |
||||
|
builder.setTransitionLayoutInfo(tNodeFailed, storm::gspn::LayoutInfo(xcenter+3.0, ycenter+3.0)); |
||||
|
builder.addInhibitionArc(nodeFailed, tNodeFailed); |
||||
|
builder.addOutputArc(tNodeFailed, nodeFailed); |
||||
|
if (!smart || isRepresentative) { |
||||
|
builder.addOutputArc(tNodeFailed, nodeFailed); |
||||
|
} |
||||
|
|
||||
|
if(dftPand->isInclusive()) { |
||||
|
// Inclusive PAND
|
||||
|
uint64_t nodeFS = builder.addPlace(defaultCapacity, 0, dftPand->name() + STR_FAILSAVE); |
||||
|
builder.setPlaceLayoutInfo(nodeFS, storm::gspn::LayoutInfo(xcenter-3.0, ycenter-3.0)); |
||||
|
|
||||
|
builder.addInhibitionArc(nodeFS, tNodeFailed); |
||||
|
for(auto const& child : dftPand->children()) { |
||||
|
builder.addInputArc(failedNodes[child->id()], tNodeFailed); |
||||
|
builder.addOutputArc(tNodeFailed, failedNodes[child->id()]); |
||||
|
} |
||||
|
for (uint64_t j = 1; j < dftPand->nrChildren(); ++j) { |
||||
|
uint64_t tfs = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILSAVING + std::to_string(j)); |
||||
|
builder.setTransitionLayoutInfo(tfs, storm::gspn::LayoutInfo(xcenter-6.0+j*3.0, ycenter+3.0)); |
||||
|
|
||||
|
builder.addInputArc(failedNodes[dftPand->children().at(j)->id()], tfs); |
||||
|
builder.addOutputArc(tfs, failedNodes[dftPand->children().at(j)->id()]); |
||||
|
builder.addInhibitionArc(failedNodes[dftPand->children().at(j-1)->id()], tfs); |
||||
|
builder.addOutputArc(tfs, nodeFS); |
||||
|
builder.addInhibitionArc(nodeFS, tfs); |
||||
|
|
||||
|
} |
||||
|
} else { |
||||
|
// Exclusive PAND
|
||||
|
uint64_t fi = 0; |
||||
|
uint64_t tn = 0; |
||||
|
for(uint64_t j = 0; j < dftPand->nrChildren(); ++j) { |
||||
|
auto const& child = dftPand->children()[j]; |
||||
|
if (j > 0) { |
||||
|
builder.addInhibitionArc(failedNodes.at(child->id()), tn); |
||||
|
} |
||||
|
if (j != dftPand->nrChildren() - 1) { |
||||
|
tn = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILING + "_" +std::to_string(j)); |
||||
|
builder.setTransitionLayoutInfo(tn, storm::gspn::LayoutInfo(xcenter-3.0, ycenter+3.0)); |
||||
|
} else { |
||||
|
tn = tNodeFailed; |
||||
|
} |
||||
|
builder.addInputArc(failedNodes.at(child->id()), tn); |
||||
|
builder.addOutputArc(tn, failedNodes.at(child->id())); |
||||
|
if (j > 0) { |
||||
|
builder.addInputArc(fi, tn); |
||||
|
} |
||||
|
if (j != dftPand->nrChildren() - 1) { |
||||
|
fi = builder.addPlace(defaultCapacity, 0, dftPand->name() + "_F_" + std::to_string(j)); |
||||
|
builder.setPlaceLayoutInfo(fi, storm::gspn::LayoutInfo(xcenter-3.0+j*3.0, ycenter)); |
||||
|
builder.addOutputArc(tn, fi); |
||||
|
} |
||||
|
|
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
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); |
||||
|
|
||||
|
double xcenter = mDft.getElementLayoutInfo(dftPor->id()).x; |
||||
|
double ycenter = mDft.getElementLayoutInfo(dftPor->id()).y; |
||||
|
builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter+3.0, ycenter-3.0)); |
||||
|
|
||||
|
uint64_t unavailableNode = 0; |
||||
|
if (!smart || isRepresentative) { |
||||
|
unavailableNode = addUnavailableNode(dftPor, storm::gspn::LayoutInfo(xcenter+9.0, ycenter-3.0)); |
||||
|
} |
||||
|
|
||||
|
uint64_t tfail = builder.addImmediateTransition(getFailPriority(dftPor), 0.0, dftPor->name() + STR_FAILING); |
||||
|
builder.setTransitionLayoutInfo(tfail, storm::gspn::LayoutInfo(xcenter+3.0, ycenter+3.0)); |
||||
|
builder.addOutputArc(tfail, nodeFailed); |
||||
|
builder.addInhibitionArc(nodeFailed, tfail); |
||||
|
|
||||
|
builder.addInputArc(failedNodes.at(dftPor->children().front()->id()), tfail); |
||||
|
builder.addOutputArc(tfail, failedNodes.at(dftPor->children().front()->id())); |
||||
|
|
||||
|
if(!smart || isRepresentative) { |
||||
|
builder.addOutputArc(tfail, unavailableNode); |
||||
|
} |
||||
|
|
||||
|
if(dftPor->isInclusive()) { |
||||
|
// Inclusive POR
|
||||
|
uint64_t nodeFS = builder.addPlace(defaultCapacity, 0, dftPor->name() + STR_FAILSAVE); |
||||
|
builder.setPlaceLayoutInfo(nodeFS, storm::gspn::LayoutInfo(xcenter-3.0, ycenter-3.0)); |
||||
|
|
||||
|
builder.addInhibitionArc(nodeFS, 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.setTransitionLayoutInfo(tfailsf, storm::gspn::LayoutInfo(xcenter-3.0+j*3.0, ycenter+3.0)); |
||||
|
builder.addInputArc(failedNodes.at(child->id()), tfailsf); |
||||
|
builder.addOutputArc(tfailsf, failedNodes.at(child->id())); |
||||
|
builder.addOutputArc(tfailsf, nodeFS); |
||||
|
builder.addInhibitionArc(nodeFS, tfailsf); |
||||
|
builder.addInhibitionArc(failedNodes.at(dftPor->children().front()->id()), tfailsf); |
||||
|
} |
||||
|
|
||||
|
++j; |
||||
|
} |
||||
|
} else { |
||||
|
// Exclusive POR
|
||||
|
uint64_t j = 0; |
||||
|
for (auto const& child : dftPor->children()) { |
||||
|
if(j > 0) { |
||||
|
builder.addInhibitionArc(failedNodes.at(child->id()), tfail); |
||||
|
} |
||||
|
++j; |
||||
|
} |
||||
|
|
||||
|
} |
||||
|
|
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void DftToGspnTransformator<ValueType>::drawSPARE(std::shared_ptr<storm::storage::DFTSpare<ValueType> const> dftSpare, bool isRepresentative) { |
||||
|
|
||||
|
uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftSpare->name() + STR_FAILED); |
||||
|
failedNodes.push_back(nodeFailed); |
||||
|
|
||||
|
double xcenter = mDft.getElementLayoutInfo(dftSpare->id()).x; |
||||
|
double ycenter = mDft.getElementLayoutInfo(dftSpare->id()).y; |
||||
|
builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter+10.0, ycenter-8.0)); |
||||
|
|
||||
|
uint64_t unavailableNode = 0; |
||||
|
if (isRepresentative) { |
||||
|
unavailableNode = addUnavailableNode(dftSpare, storm::gspn::LayoutInfo(xcenter+16.0, ycenter-8.0)); |
||||
|
} |
||||
|
uint64_t spareActive = builder.addPlace(defaultCapacity, isBEActive(dftSpare) ? 1 : 0, dftSpare->name() + STR_ACTIVATED); |
||||
|
builder.setPlaceLayoutInfo(spareActive, storm::gspn::LayoutInfo(xcenter-20.0, ycenter-8.0)); |
||||
|
activeNodes.emplace(dftSpare->id(), spareActive); |
||||
|
|
||||
|
|
||||
|
std::vector<uint64_t> cucNodes; |
||||
|
std::vector<uint64_t> considerNodes; |
||||
|
std::vector<uint64_t> nextclTransitions; |
||||
|
std::vector<uint64_t> nextconsiderTransitions; |
||||
|
uint64_t j = 0; |
||||
|
for(auto const& child : dftSpare->children()) { |
||||
|
if (j > 0) { |
||||
|
size_t nodeConsider = builder.addPlace(defaultCapacity, 0, dftSpare->name()+ "_consider_" + child->name()); |
||||
|
considerNodes.push_back(nodeConsider); |
||||
|
builder.setPlaceLayoutInfo(nodeConsider, storm::gspn::LayoutInfo(xcenter-15.0+j*14.0, ycenter-8.0)); |
||||
|
|
||||
|
builder.addOutputArc(nextclTransitions.back(), considerNodes.back(), 1); |
||||
|
if (j > 1) { |
||||
|
builder.addOutputArc(nextconsiderTransitions.back(), considerNodes.back()); |
||||
|
} |
||||
|
|
||||
|
uint64_t tnextconsider = builder.addImmediateTransition(getFailPriority(dftSpare), 0.0, dftSpare->name() + "_cannot_claim_" + child->name()); |
||||
|
builder.setTransitionLayoutInfo(tnextconsider, storm::gspn::LayoutInfo(xcenter-7.0+j*14.0, ycenter-8.0)); |
||||
|
builder.addInputArc(considerNodes.back(), tnextconsider); |
||||
|
builder.addInputArc(unavailableNodes.at(child->id()), tnextconsider); |
||||
|
nextconsiderTransitions.push_back(tnextconsider); |
||||
|
|
||||
|
} |
||||
|
size_t nodeCUC = builder.addPlace(defaultCapacity, j == 0 ? 1 : 0, dftSpare->name() + "_claimed_" + child->name()); |
||||
|
cucNodes.push_back(nodeCUC); |
||||
|
builder.setPlaceLayoutInfo(nodeCUC, storm::gspn::LayoutInfo(xcenter-9.0+j*14.0, ycenter+5.0)); |
||||
|
if (j > 0) { |
||||
|
uint64 tclaim = builder.addImmediateTransition(getFailPriority(dftSpare), 0.0, dftSpare->name() + "_claim_" + child->name()); |
||||
|
builder.setTransitionLayoutInfo(tclaim, storm::gspn::LayoutInfo(xcenter-9.0+j*14.0, ycenter)); |
||||
|
builder.addInhibitionArc(unavailableNodes.at(child->id()), tclaim); |
||||
|
builder.addInputArc(considerNodes.back(), tclaim); |
||||
|
builder.addOutputArc(tclaim, cucNodes.back()); |
||||
|
} |
||||
|
uint64_t tnextcl = builder.addImmediateTransition(getFailPriority(dftSpare), 0.0, dftSpare->name() + "_next_claim_" + std::to_string(j)); |
||||
|
builder.setTransitionLayoutInfo(tnextcl, storm::gspn::LayoutInfo(xcenter-3.0+j*14.0, ycenter+5.0)); |
||||
|
builder.addInputArc(cucNodes.back(), tnextcl); |
||||
|
builder.addInputArc(failedNodes.at(child->id()), tnextcl); |
||||
|
builder.addOutputArc(tnextcl, failedNodes.at(child->id())); |
||||
|
nextclTransitions.push_back(tnextcl); |
||||
|
++j; |
||||
|
for (uint64_t k : mDft.module(child->id())) { |
||||
|
|
||||
|
uint64_t tactive = builder.addImmediateTransition(defaultPriority+1, 0.0, dftSpare->name() + "_activate_" + std::to_string(j) + "_" + std::to_string(k)); |
||||
|
builder.addInputArc(cucNodes.back(), tactive); |
||||
|
builder.addOutputArc(tactive, cucNodes.back()); |
||||
|
builder.addInputArc(spareActive, tactive); |
||||
|
builder.addOutputArc(tactive, activeNodes.at(k)); |
||||
|
builder.addInhibitionArc(activeNodes.at(k), tactive); |
||||
|
} |
||||
|
|
||||
|
|
||||
|
} |
||||
|
builder.addOutputArc(nextconsiderTransitions.back(), nodeFailed); |
||||
|
builder.addOutputArc(nextclTransitions.back(), nodeFailed); |
||||
|
|
||||
|
if (isRepresentative) { |
||||
|
builder.addOutputArc(nextconsiderTransitions.back(), unavailableNode); |
||||
|
builder.addOutputArc(nextclTransitions.back(), unavailableNode); |
||||
|
} |
||||
|
|
||||
|
|
||||
|
|
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void DftToGspnTransformator<ValueType>::drawCONSTF(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftConstF, bool isRepresentative) { |
||||
|
failedNodes.push_back(builder.addPlace(defaultCapacity, 1, dftConstF->name() + STR_FAILED)); |
||||
|
uint64_t unavailableNode = 0; |
||||
|
if (isRepresentative) { |
||||
|
// TODO set position
|
||||
|
unavailableNode = addUnavailableNode(dftConstF, storm::gspn::LayoutInfo(0, 0), false); |
||||
|
} |
||||
|
|
||||
|
} |
||||
|
//
|
||||
|
template <typename ValueType> |
||||
|
void DftToGspnTransformator<ValueType>::drawCONSTS(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftConstS, bool isRepresentative) { |
||||
|
// 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);
|
||||
|
} |
||||
|
//
|
||||
|
template <typename ValueType> |
||||
|
void DftToGspnTransformator<ValueType>::drawPDEP(std::shared_ptr<storm::storage::DFTDependency<ValueType> const> dftDependency) { |
||||
|
double xcenter = mDft.getElementLayoutInfo(dftDependency->id()).x;; |
||||
|
double ycenter = mDft.getElementLayoutInfo(dftDependency->id()).y;; |
||||
|
|
||||
|
uint64_t coinPlace = builder.addPlace(defaultCapacity, 1, dftDependency->name() + "_coin"); |
||||
|
builder.setPlaceLayoutInfo(coinPlace, storm::gspn::LayoutInfo(xcenter-5.0, ycenter+2.0)); |
||||
|
uint64_t t1 = builder.addImmediateTransition(defaultPriority, 0.0, dftDependency->name() + "_start_flip"); |
||||
|
|
||||
|
builder.addInputArc(coinPlace, t1); |
||||
|
builder.addInputArc(failedNodes.at(dftDependency->triggerEvent()->id()), t1); |
||||
|
builder.addOutputArc(t1, failedNodes.at(dftDependency->triggerEvent()->id())); |
||||
|
uint64_t forwardPlace = builder.addPlace(defaultCapacity, 0, dftDependency->name() + "_forward"); |
||||
|
builder.setPlaceLayoutInfo(forwardPlace, storm::gspn::LayoutInfo(xcenter+1.0, ycenter+2.0)); |
||||
|
|
||||
|
if (!smart || dftDependency->probability() < 1.0) { |
||||
|
uint64_t flipPlace = builder.addPlace(defaultCapacity, 0, dftDependency->name() + "_flip"); |
||||
|
builder.addOutputArc(t1, flipPlace); |
||||
|
|
||||
|
builder.setPlaceLayoutInfo(flipPlace, storm::gspn::LayoutInfo(xcenter-2.0, ycenter+2.0)); |
||||
|
uint64_t t2 = builder.addImmediateTransition(defaultPriority + 1, dftDependency->probability(), "_win_flip"); |
||||
|
builder.addInputArc(flipPlace, t2); |
||||
|
builder.addOutputArc(t2, forwardPlace); |
||||
|
if (dftDependency->probability() < 1.0) { |
||||
|
uint64_t t3 = builder.addImmediateTransition(defaultPriority + 1, 1 - dftDependency->probability(), "_loose_flip"); |
||||
|
builder.addInputArc(flipPlace, t3); |
||||
|
} |
||||
|
} else { |
||||
|
builder.addOutputArc(t1, forwardPlace); |
||||
|
} |
||||
|
for(auto const& depEv : dftDependency->dependentEvents()) { |
||||
|
uint64_t tx = builder.addImmediateTransition(defaultPriority, 0.0, dftDependency->name() + "_propagate_" + depEv->name()); |
||||
|
builder.addInputArc(forwardPlace, tx); |
||||
|
builder.addOutputArc(tx, forwardPlace); |
||||
|
builder.addOutputArc(tx, failedNodes.at(depEv->id())); |
||||
|
builder.addInhibitionArc(failedNodes.at(depEv->id()), tx); |
||||
|
if (!smart || depEv->nrRestrictions() > 0) { |
||||
|
builder.addInhibitionArc(disabledNodes.at(depEv->id()), tx); |
||||
|
} |
||||
|
if (!smart || mDft.isRepresentative(depEv->id())) { |
||||
|
builder.addOutputArc(tx, unavailableNodes.at(depEv->id())); |
||||
|
} |
||||
|
|
||||
|
} |
||||
|
|
||||
|
|
||||
|
|
||||
|
|
||||
|
|
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void DftToGspnTransformator<ValueType>::drawSeq(std::shared_ptr<storm::storage::DFTSeq<ValueType> const> dftSeq) { |
||||
|
STORM_LOG_THROW(dftSeq->allChildrenBEs(), storm::exceptions::NotImplementedException, "Sequence enforcers with gates as children are currently not supported"); |
||||
|
uint64_t j = 0; |
||||
|
uint64_t tEnable = 0; |
||||
|
uint64_t nextPlace = 0; |
||||
|
for(auto const& child : dftSeq->children()) { |
||||
|
nextPlace = builder.addPlace(defaultCapacity, j==0 ? 1 : 0, dftSeq->name() + "_next_" + child->name()); |
||||
|
if (j>0) { |
||||
|
builder.addOutputArc(tEnable, nextPlace); |
||||
|
} |
||||
|
tEnable = builder.addImmediateTransition(defaultPriority + 1, 0.0, dftSeq->name() + "_unblock_" +child->name() ); |
||||
|
builder.addInputArc(nextPlace, tEnable); |
||||
|
builder.addInputArc(disabledNodes.at(child->id()), tEnable); |
||||
|
if (j>0) { |
||||
|
builder.addInputArc(failedNodes.at(dftSeq->children().at(j-1)->id()), tEnable); |
||||
|
} |
||||
|
++j; |
||||
|
} |
||||
|
|
||||
|
} |
||||
|
|
||||
|
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 unavailableNode = builder.addPlace(defaultCapacity, initialAvailable ? 0 : 1, dftElement->name() + "_unavailable"); |
||||
|
assert(unavailableNode != 0); |
||||
|
unavailableNodes.emplace(dftElement->id(), unavailableNode); |
||||
|
builder.setPlaceLayoutInfo(unavailableNode, layoutInfo); |
||||
|
return unavailableNode; |
||||
|
} |
||||
|
|
||||
|
template<typename ValueType> |
||||
|
uint64_t DftToGspnTransformator<ValueType>::addDisabledPlace(std::shared_ptr<const storm::storage::DFTBE<ValueType> > dftBe) { |
||||
|
uint64_t disabledNode = builder.addPlace(dftBe->nrRestrictions(), dftBe->nrRestrictions(), dftBe->name() + "_dabled"); |
||||
|
disabledNodes.emplace(dftBe->id(), disabledNode); |
||||
|
return disabledNode; |
||||
|
} |
||||
|
//
|
||||
|
|
||||
|
template <typename ValueType> |
||||
|
bool DftToGspnTransformator<ValueType>::isBEActive(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement) |
||||
|
{ |
||||
|
// If element is the top element, return true.
|
||||
|
if (dftElement->id() == mDft.getTopLevelIndex()) { |
||||
|
return true; |
||||
|
} |
||||
|
else { // Else look at all parents.
|
||||
|
auto parents = dftElement->parents(); |
||||
|
std::vector<bool> pathValidities; |
||||
|
|
||||
|
for (std::size_t i = 0; i < parents.size(); i++) { |
||||
|
// Add all parents to the vector, except if the parent is a SPARE and the current element is an inactive child of the SPARE.
|
||||
|
if (parents[i]->type() == storm::storage::DFTElementType::SPARE) { |
||||
|
auto children = std::static_pointer_cast<storm::storage::DFTSpare<ValueType> const>(parents[i])->children(); |
||||
|
if (children[0]->id() != dftElement->id()) { |
||||
|
continue; |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
pathValidities.push_back(isBEActive(parents[i])); |
||||
|
} |
||||
|
|
||||
|
// Check all vector entries. If one is true, a "valid" path has been found.
|
||||
|
for (std::size_t i = 0; i < pathValidities.size(); i++) { |
||||
|
if (pathValidities[i]) { |
||||
|
return true; |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
// No "valid" path found. BE is inactive.
|
||||
|
return false; |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
uint64_t DftToGspnTransformator<ValueType>::getFailPriority(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement) |
||||
|
{ |
||||
|
return mDft.maxRank() - dftElement->rank() + 2; |
||||
|
} |
||||
|
|
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void DftToGspnTransformator<ValueType>::drawGSPNRestrictions() { |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
gspn::GSPN* DftToGspnTransformator<ValueType>::obtainGSPN() { |
||||
|
return builder.buildGspn(); |
||||
|
} |
||||
|
|
||||
|
// Explicitly instantiate the class.
|
||||
|
template class DftToGspnTransformator<double>; |
||||
|
|
||||
|
|
||||
|
#ifdef STORM_HAVE_CARL
|
||||
|
// template class DftToGspnTransformator<storm::RationalFunction>;
|
||||
|
#endif
|
||||
|
|
||||
|
} // namespace dft
|
||||
|
} // namespace transformations
|
||||
|
} // namespace storm
|
||||
|
|
||||
|
|
||||
@ -0,0 +1,163 @@ |
|||||
|
#pragma once |
||||
|
|
||||
|
#include "storm-dft/storage/dft/DFT.h" |
||||
|
#include "storm-gspn/storage/gspn/GSPN.h" |
||||
|
#include "storm-gspn/storage/gspn/GspnBuilder.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace transformations { |
||||
|
namespace dft { |
||||
|
|
||||
|
/*! |
||||
|
* Transformator for DFT -> GSPN. |
||||
|
*/ |
||||
|
template<typename ValueType> |
||||
|
class DftToGspnTransformator { |
||||
|
|
||||
|
public: |
||||
|
/*! |
||||
|
* Constructor. |
||||
|
* |
||||
|
* @param dft DFT |
||||
|
*/ |
||||
|
DftToGspnTransformator(storm::storage::DFT<ValueType> const& dft); |
||||
|
|
||||
|
/*! |
||||
|
* Transform the DFT to a GSPN. |
||||
|
*/ |
||||
|
void transform(); |
||||
|
|
||||
|
/*! |
||||
|
* Extract Gspn by building |
||||
|
* |
||||
|
*/ |
||||
|
gspn::GSPN* obtainGSPN(); |
||||
|
|
||||
|
|
||||
|
uint64_t toplevelFailedPlaceId(); |
||||
|
|
||||
|
private: |
||||
|
/* |
||||
|
* Draw all elements of the GSPN. |
||||
|
*/ |
||||
|
void drawGSPNElements(); |
||||
|
/* |
||||
|
* Draw restrictions between the elements of the GSPN (i.e. SEQ or MUTEX). |
||||
|
*/ |
||||
|
void drawGSPNRestrictions(); |
||||
|
|
||||
|
/* |
||||
|
* Draw a Petri net Basic Event. |
||||
|
* |
||||
|
* @param dftBE The Basic Event. |
||||
|
*/ |
||||
|
void drawBE(std::shared_ptr<storm::storage::DFTBE<ValueType> const> dftBE, bool isRepresentative); |
||||
|
|
||||
|
/* |
||||
|
* Draw a Petri net AND. |
||||
|
* |
||||
|
* @param dftAnd The AND gate. |
||||
|
*/ |
||||
|
void drawAND(std::shared_ptr<storm::storage::DFTAnd<ValueType> const> dftAnd, bool isRepresentative); |
||||
|
|
||||
|
/* |
||||
|
* Draw a Petri net OR. |
||||
|
* |
||||
|
* @param dftOr The OR gate. |
||||
|
*/ |
||||
|
void drawOR(std::shared_ptr<storm::storage::DFTOr<ValueType> const> dftOr, bool isRepresentative); |
||||
|
|
||||
|
/* |
||||
|
* Draw a Petri net VOT. |
||||
|
* |
||||
|
* @param dftVot The VOT gate. |
||||
|
*/ |
||||
|
void drawVOT(std::shared_ptr<storm::storage::DFTVot<ValueType> const> dftVot, bool isRepresentative); |
||||
|
|
||||
|
/* |
||||
|
* Draw a Petri net PAND. |
||||
|
* This PAND is inklusive (children are allowed to fail simultaneously and the PAND will fail nevertheless). |
||||
|
* |
||||
|
* @param dftPand The PAND gate. |
||||
|
*/ |
||||
|
void drawPAND(std::shared_ptr<storm::storage::DFTPand<ValueType> const> dftPand, bool isRepresentative); |
||||
|
|
||||
|
/* |
||||
|
* Draw a Petri net SPARE. |
||||
|
* |
||||
|
* @param dftSpare The SPARE gate. |
||||
|
*/ |
||||
|
void drawSPARE(std::shared_ptr<storm::storage::DFTSpare<ValueType> const> dftSpare, bool isRepresentative); |
||||
|
|
||||
|
/* |
||||
|
* Draw a Petri net POR. |
||||
|
* This POR is inklusive (children are allowed to fail simultaneously and the POR will fail nevertheless). |
||||
|
* |
||||
|
* @param dftPor The POR gate. |
||||
|
*/ |
||||
|
void drawPOR(std::shared_ptr<storm::storage::DFTPor<ValueType> const> dftPor, bool isRepresentative); |
||||
|
|
||||
|
/* |
||||
|
* 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, bool isRepresentative); |
||||
|
|
||||
|
/* |
||||
|
* 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, bool isRepresentative); |
||||
|
|
||||
|
/* |
||||
|
* Draw a Petri net PDEP (FDEP is included with a firerate of 1). |
||||
|
*/ |
||||
|
void drawPDEP(std::shared_ptr<storm::storage::DFTDependency<ValueType> const> dftDependency); |
||||
|
|
||||
|
|
||||
|
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). |
||||
|
* |
||||
|
* @param dFTElement DFT element. |
||||
|
*/ |
||||
|
bool isBEActive(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dFTElement); |
||||
|
|
||||
|
/* |
||||
|
* Get the priority of the element. |
||||
|
* The priority is two times the length of the shortest path to the top event. |
||||
|
* |
||||
|
* @param priority The priority of the gate. Top Event has priority 0, its children 2, its grandchildren 4, ... |
||||
|
* |
||||
|
* @param dftElement The element whose priority shall be determined. |
||||
|
*/ |
||||
|
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 addDisabledPlace(std::shared_ptr<storm::storage::DFTBE<ValueType> const> dftBe); |
||||
|
|
||||
|
storm::storage::DFT<ValueType> const& mDft; |
||||
|
storm::gspn::GspnBuilder builder; |
||||
|
std::vector<uint64_t> failedNodes; |
||||
|
std::map<uint64_t, uint64_t> unavailableNodes; |
||||
|
std::map<uint64_t, uint64_t> activeNodes; |
||||
|
std::map<uint64_t, uint64_t> disabledNodes; |
||||
|
bool smart = true; |
||||
|
|
||||
|
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. |
||||
|
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. |
||||
|
|
||||
|
|
||||
|
}; |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
|
||||
@ -0,0 +1,17 @@ |
|||||
|
#pragma once |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace gspn { |
||||
|
struct LayoutInfo { |
||||
|
LayoutInfo() {}; |
||||
|
LayoutInfo(double x, double y, double rotation = 0.0) : x(x), y(y), rotation(rotation) {}; |
||||
|
|
||||
|
// x location |
||||
|
double x = 0.0; |
||||
|
// y location |
||||
|
double y = 0.0; |
||||
|
// degrees |
||||
|
double rotation = 0.0; |
||||
|
}; |
||||
|
} |
||||
|
} |
||||
@ -0,0 +1,60 @@ |
|||||
|
#pragma once |
||||
|
|
||||
|
#include "storm/storage/jani/Model.h" |
||||
|
|
||||
|
#include "storm-gspn/builder/JaniGSPNBuilder.h" |
||||
|
#include "storm-gspn/storage/gspn/GSPN.h" |
||||
|
|
||||
|
#include "storm/settings/modules/GSPNExportSettings.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
/** |
||||
|
* Builds JANI model from GSPN. |
||||
|
*/ |
||||
|
storm::jani::Model* buildJani(storm::gspn::GSPN const& gspn) { |
||||
|
std::shared_ptr<storm::expressions::ExpressionManager> exprManager(new storm::expressions::ExpressionManager()); |
||||
|
storm::builder::JaniGSPNBuilder builder(gspn, exprManager); |
||||
|
return builder.build(); |
||||
|
} |
||||
|
|
||||
|
void handleGSPNExportSettings(storm::gspn::GSPN const& gspn) { |
||||
|
storm::settings::modules::GSPNExportSettings const& exportSettings = storm::settings::getModule<storm::settings::modules::GSPNExportSettings>(); |
||||
|
if (exportSettings.isWriteToDotSet()) { |
||||
|
std::ofstream fs; |
||||
|
fs.open(exportSettings.getWriteToDotFilename()); |
||||
|
gspn.writeDotToStream(fs); |
||||
|
fs.close(); |
||||
|
} |
||||
|
|
||||
|
if (exportSettings.isWriteToPnproSet()) { |
||||
|
std::ofstream fs; |
||||
|
fs.open(exportSettings.getWriteToPnproFilename()); |
||||
|
gspn.toPnpro(fs); |
||||
|
fs.close(); |
||||
|
} |
||||
|
|
||||
|
if (exportSettings.isWriteToPnmlSet()) { |
||||
|
std::ofstream fs; |
||||
|
fs.open(exportSettings.getWriteToPnmlFilename()); |
||||
|
gspn.toPnml(fs); |
||||
|
fs.close(); |
||||
|
} |
||||
|
|
||||
|
if (exportSettings.isDisplayStatsSet()) { |
||||
|
std::cout << "============GSPN Statistics==============" << std::endl; |
||||
|
gspn.writeStatsToStream(std::cout); |
||||
|
std::cout << "=========================================" << std::endl; |
||||
|
} |
||||
|
|
||||
|
if (exportSettings.isWriteStatsToFileSet()) { |
||||
|
std::ofstream fs; |
||||
|
fs.open(exportSettings.getWriteStatsFilename()); |
||||
|
gspn.writeStatsToStream(fs); |
||||
|
fs.close(); |
||||
|
} |
||||
|
|
||||
|
|
||||
|
|
||||
|
} |
||||
|
|
||||
|
} |
||||
Reference in new issue
xxxxxxxxxx