diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp
index 6ed375d79..f246438fe 100644
--- a/src/storm-dft-cli/storm-dyftee.cpp
+++ b/src/storm-dft-cli/storm-dyftee.cpp
@@ -3,7 +3,8 @@
#include "storm/utility/storm.h"
#include "storm/cli/cli.h"
#include "storm/exceptions/BaseException.h"
-#include "storm/utility/macros.h"
+
+#include "storm/logic/Formula.h"
#include "storm/settings/modules/GeneralSettings.h"
#include "storm/settings/modules/CoreSettings.h"
@@ -14,17 +15,22 @@
#include "storm/settings/modules/EliminationSettings.h"
#include "storm-dft/parser/DFTGalileoParser.h"
+#include "storm-dft/parser/DFTJsonParser.h"
#include "storm-dft/modelchecker/dft/DFTModelChecker.h"
#include "storm-dft/modelchecker/dft/DFTASFChecker.h"
+#include "storm-dft/transformations/DftToGspnTransformator.h"
+
#include "storm-dft/settings/modules/DFTSettings.h"
#include "storm-gspn/storage/gspn/GSPN.h"
+#include "storm-gspn/storm-gspn.h"
#include "storm/settings/modules/GSPNSettings.h"
#include "storm/settings/modules/GSPNExportSettings.h"
#include <boost/lexical_cast.hpp>
+#include <memory>
/*!
* Load DFT from filename, build corresponding Model and check against given property.
@@ -68,17 +74,6 @@ void analyzeWithSMT(std::string filename) {
//std::cout << "SMT result: " << sat << std::endl;
}
-/*!
- * Load DFT from filename and transform into a GSPN.
- *
- * @param filename Path to DFT file in Galileo format.
- *
- */
-template <typename ValueType>
-storm::gspn::GSPN transformDFT(std::string filename) {
- storm::parser::DFTGalileoParser<ValueType> parser;
- storm::storage::DFT<ValueType> dft = parser.parseDFT(filename);
-}
/*!
* Initialize the settings manager.
@@ -107,6 +102,7 @@ void initializeSettings() {
// For translation into JANI via GSPN.
storm::settings::addModule<storm::settings::modules::GSPNSettings>();
storm::settings::addModule<storm::settings::modules::GSPNExportSettings>();
+ storm::settings::addModule<storm::settings::modules::JaniExportSettings>();
}
/*!
@@ -129,14 +125,48 @@ int main(const int argc, const char** argv) {
storm::settings::modules::DFTSettings const& dftSettings = storm::settings::getModule<storm::settings::modules::DFTSettings>();
storm::settings::modules::GeneralSettings const& generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
- if (!dftSettings.isDftFileSet()) {
+ if (!dftSettings.isDftFileSet() && !dftSettings.isDftJsonFileSet()) {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
}
+
if (dftSettings.isTransformToGspn()) {
- // For now we only transform the DFT to a GSPN and then exit
- transformDFT<double>(dftSettings.getDftFilename());
+ std::shared_ptr<storm::storage::DFT<double>> dft;
+ if (dftSettings.isDftJsonFileSet()) {
+ storm::parser::DFTJsonParser<double> parser;
+ dft = std::make_shared<storm::storage::DFT<double>>(parser.parseJson(dftSettings.getDftJsonFilename()));
+ } else {
+ storm::parser::DFTGalileoParser<double> parser(true, false);
+ dft = std::make_shared<storm::storage::DFT<double>>(parser.parseDFT(dftSettings.getDftFilename()));
+ }
+ storm::transformations::dft::DftToGspnTransformator<double> gspnTransformator(*dft);
+ gspnTransformator.transform();
+ storm::gspn::GSPN* gspn = gspnTransformator.obtainGSPN();
+ uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId();
+
+ storm::handleGSPNExportSettings(*gspn);
+
+ std::shared_ptr<storm::expressions::ExpressionManager> exprManager(new storm::expressions::ExpressionManager());
+ storm::builder::JaniGSPNBuilder builder(*gspn, exprManager);
+ storm::jani::Model* model = builder.build();
+ storm::jani::Variable const& topfailedVar = builder.getPlaceVariable(toplevelFailedPlace);
+
+
+ storm::expressions::Expression targetExpression = exprManager->integer(1) == topfailedVar.getExpressionVariable().getExpression();
+ auto evtlFormula = std::make_shared<storm::logic::AtomicExpressionFormula>(targetExpression);
+ auto tbFormula = std::make_shared<storm::logic::BoundedUntilFormula>(std::make_shared<storm::logic::BooleanLiteralFormula>(true), evtlFormula, 0.0, 10.0);
+ auto tbUntil = std::make_shared<storm::logic::ProbabilityOperatorFormula>(tbFormula);
+
+ auto evFormula = std::make_shared<storm::logic::EventuallyFormula>(evtlFormula, storm::logic::FormulaContext::Time);
+ auto rewFormula = std::make_shared<storm::logic::TimeOperatorFormula>(evFormula, storm::logic::OperatorInformation(), storm::logic::RewardMeasureType::Expectation);
+
+ storm::settings::modules::JaniExportSettings const& janiSettings = storm::settings::getModule<storm::settings::modules::JaniExportSettings>();
+ if (janiSettings.isJaniFileSet()) {
+ storm::exportJaniModel(*model, {storm::jani::Property("time-bounded", tbUntil), storm::jani::Property("mttf", rewFormula)}, janiSettings.getJaniFilename());
+ }
+ delete model;
+ delete gspn;
storm::utility::cleanUp();
return 0;
}
diff --git a/src/storm-dft/CMakeLists.txt b/src/storm-dft/CMakeLists.txt
index df0c067e0..10d9b8508 100644
--- a/src/storm-dft/CMakeLists.txt
+++ b/src/storm-dft/CMakeLists.txt
@@ -10,4 +10,4 @@ file(GLOB_RECURSE STORM_DFT_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-dft/*/*.h)
# Create storm-pgcl.
add_library(storm-dft SHARED ${STORM_DFT_SOURCES} ${STORM_DFT_HEADERS})
-target_link_libraries(storm-dft storm ${STORM_DFT_LINK_LIBRARIES})
+target_link_libraries(storm-dft storm storm-gspn ${STORM_DFT_LINK_LIBRARIES})
diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
index ae4144ee7..2de46e599 100644
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
@@ -8,6 +8,7 @@
#include "storm-dft/storage/dft/DFTIsomorphism.h"
#include "storm-dft/settings/modules/DFTSettings.h"
+
namespace storm {
namespace modelchecker {
diff --git a/src/storm-dft/parser/DFTGalileoParser.cpp b/src/storm-dft/parser/DFTGalileoParser.cpp
index 776eb64d9..f872f4526 100644
--- a/src/storm-dft/parser/DFTGalileoParser.cpp
+++ b/src/storm-dft/parser/DFTGalileoParser.cpp
@@ -4,6 +4,7 @@
#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"
@@ -34,6 +35,11 @@ namespace storm {
return name.substr(firstQuots+1,secondQuots-1);
}
}
+
+ template<typename ValueType>
+ std::string DFTGalileoParser<ValueType>::parseNodeIdentifier(std::string const& name) {
+ return boost::replace_all_copy(name, "'", "__prime__");
+ }
template<typename ValueType>
void DFTGalileoParser<ValueType>::readFile(const std::string& filename) {
@@ -84,11 +90,11 @@ namespace storm {
} else {
std::vector<std::string> tokens;
boost::split(tokens, line, boost::is_any_of(" "));
- std::string name(stripQuotsFromName(tokens[0]));
+ std::string name(parseNodeIdentifier(stripQuotsFromName(tokens[0])));
std::vector<std::string> childNames;
for(unsigned i = 2; i < tokens.size(); ++i) {
- childNames.push_back(stripQuotsFromName(tokens[i]));
+ childNames.push_back(parseNodeIdentifier(stripQuotsFromName(tokens[i])));
}
if(tokens[1] == "and") {
success = builder.addAndElement(name, childNames);
@@ -104,8 +110,16 @@ namespace storm {
success = builder.addVotElement(name, threshold, childNames);
} else if (tokens[1] == "pand") {
success = builder.addPandElement(name, childNames);
+ } else if (tokens[1] == "pand-inc") {
+ success = builder.addPandElement(name, childNames, true);
+ } else if (tokens[1] == "pand-ex") {
+ success = builder.addPandElement(name, childNames, false);
} else if (tokens[1] == "por") {
success = builder.addPorElement(name, childNames);
+ } else if (tokens[1] == "por-ex") {
+ success = builder.addPorElement(name, childNames, false);
+ } else if (tokens[1] == "por-inc") {
+ success = builder.addPorElement(name, childNames, true);
} else if (tokens[1] == "wsp" || tokens[1] == "csp") {
success = builder.addSpareElement(name, childNames);
} else if (tokens[1] == "seq") {
diff --git a/src/storm-dft/parser/DFTGalileoParser.h b/src/storm-dft/parser/DFTGalileoParser.h
index 3f19683ff..c2a35bc50 100644
--- a/src/storm-dft/parser/DFTGalileoParser.h
+++ b/src/storm-dft/parser/DFTGalileoParser.h
@@ -26,7 +26,7 @@ namespace storm {
std::unordered_map<std::string, storm::expressions::Expression> identifierMapping;
public:
- DFTGalileoParser() : manager(new storm::expressions::ExpressionManager()), parser(*manager), evaluator(*manager) {
+ DFTGalileoParser(bool defaultInclusive = true, bool binaryDependencies = true) : builder(defaultInclusive, binaryDependencies), manager(new storm::expressions::ExpressionManager()), parser(*manager), evaluator(*manager) {
}
storm::storage::DFT<ValueType> parseDFT(std::string const& filename);
@@ -35,8 +35,11 @@ namespace storm {
void readFile(std::string const& filename);
std::string stripQuotsFromName(std::string const& name);
+ std::string parseNodeIdentifier(std::string const& name);
ValueType parseRationalExpression(std::string const& expr);
+
+ bool defaultInclusive;
};
}
}
diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp
new file mode 100644
index 000000000..9a5c5d047
--- /dev/null
+++ b/src/storm-dft/parser/DFTJsonParser.cpp
@@ -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
+
+ }
+}
diff --git a/src/storm-dft/parser/DFTJsonParser.h b/src/storm-dft/parser/DFTJsonParser.h
new file mode 100644
index 000000000..cf2e83826
--- /dev/null
+++ b/src/storm-dft/parser/DFTJsonParser.h
@@ -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);
+ };
+ }
+}
diff --git a/src/storm-dft/settings/modules/DFTSettings.cpp b/src/storm-dft/settings/modules/DFTSettings.cpp
index 5bf705d8a..898360c4b 100644
--- a/src/storm-dft/settings/modules/DFTSettings.cpp
+++ b/src/storm-dft/settings/modules/DFTSettings.cpp
@@ -16,6 +16,8 @@ namespace storm {
const std::string DFTSettings::moduleName = "dft";
const std::string DFTSettings::dftFileOptionName = "dftfile";
const std::string DFTSettings::dftFileOptionShortName = "dft";
+ const std::string DFTSettings::dftJsonFileOptionName = "dftfile-json";
+ const std::string DFTSettings::dftJsonFileOptionShortName = "dftjson";
const std::string DFTSettings::symmetryReductionOptionName = "symmetryreduction";
const std::string DFTSettings::symmetryReductionOptionShortName = "symred";
const std::string DFTSettings::modularisationOptionName = "modularisation";
@@ -37,6 +39,8 @@ namespace storm {
DFTSettings::DFTSettings() : ModuleSettings(moduleName) {
this->addOption(storm::settings::OptionBuilder(moduleName, dftFileOptionName, false, "Parses the model given in the Galileo format.").setShortName(dftFileOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the DFT model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, dftJsonFileOptionName, false, "Parses the model given in the Cytoscape JSON format.").setShortName(dftJsonFileOptionShortName)
+ .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file from which to read the DFT model.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, symmetryReductionOptionName, false, "Exploit symmetric structure of model.").setShortName(symmetryReductionOptionShortName).build());
this->addOption(storm::settings::OptionBuilder(moduleName, modularisationOptionName, false, "Use modularisation (not applicable for expected time).").build());
this->addOption(storm::settings::OptionBuilder(moduleName, disableDCOptionName, false, "Disable Dont Care propagation.").build());
@@ -60,7 +64,15 @@ namespace storm {
std::string DFTSettings::getDftFilename() const {
return this->getOption(dftFileOptionName).getArgumentByName("filename").getValueAsString();
}
-
+
+ bool DFTSettings::isDftJsonFileSet() const {
+ return this->getOption(dftJsonFileOptionName).getHasOptionBeenSet();
+ }
+
+ std::string DFTSettings::getDftJsonFilename() const {
+ return this->getOption(dftJsonFileOptionName).getArgumentByName("filename").getValueAsString();
+ }
+
bool DFTSettings::useSymmetryReduction() const {
return this->getOption(symmetryReductionOptionName).getHasOptionBeenSet();
}
diff --git a/src/storm-dft/settings/modules/DFTSettings.h b/src/storm-dft/settings/modules/DFTSettings.h
index 1b1b097f9..c1a9df7e5 100644
--- a/src/storm-dft/settings/modules/DFTSettings.h
+++ b/src/storm-dft/settings/modules/DFTSettings.h
@@ -34,6 +34,20 @@ namespace storm {
*/
std::string getDftFilename() const;
+ /*!
+ * Retrieves whether the dft file option for Json was set.
+ *
+ * @return True if the dft file option was set.
+ */
+ bool isDftJsonFileSet() const;
+
+ /*!
+ * Retrieves the name of the json file that contains the dft specification.
+ *
+ * @return The name of the json file that contains the dft specification.
+ */
+ std::string getDftJsonFilename() const;
+
/*!
* Retrieves whether the option to use symmetry reduction is set.
*
@@ -144,6 +158,8 @@ namespace storm {
// Define the string names of the options as constants.
static const std::string dftFileOptionName;
static const std::string dftFileOptionShortName;
+ static const std::string dftJsonFileOptionName;
+ static const std::string dftJsonFileOptionShortName;
static const std::string symmetryReductionOptionName;
static const std::string symmetryReductionOptionShortName;
static const std::string modularisationOptionName;
diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp
index 8f19119a2..e38c40ce1 100644
--- a/src/storm-dft/storage/dft/DFT.cpp
+++ b/src/storm-dft/storage/dft/DFT.cpp
@@ -174,7 +174,8 @@ namespace storm {
std::shared_ptr<DFTDependency<ValueType> const> dependency = getDependency(idDependency);
visitQueue.push(dependency->id());
visitQueue.push(dependency->triggerEvent()->id());
- visitQueue.push(dependency->dependentEvent()->id());
+ STORM_LOG_THROW(dependency->dependentEvents().size() == 1, storm::exceptions::NotSupportedException, "Direct state generation does not support n-ary dependencies. Consider rewriting them by setting the binary dependency flag.");
+ visitQueue.push(dependency->dependentEvents()[0]->id());
}
stateIndex = performStateGenerationInfoDFS(generationInfo, visitQueue, visited, stateIndex);
@@ -284,7 +285,13 @@ namespace storm {
template<typename ValueType>
uint64_t DFT<ValueType>::maxRank() const {
- return mElements.back()->rank();
+ uint64_t max = 0;
+ for (auto const& e : mElements) {
+ if(e->rank() > max) {
+ max = e->rank();
+ }
+ }
+ return max;
}
template<typename ValueType>
diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h
index 9ef232a65..4c904ec5c 100644
--- a/src/storm-dft/storage/dft/DFT.h
+++ b/src/storm-dft/storage/dft/DFT.h
@@ -15,7 +15,7 @@
#include "storm-dft/storage/dft/DFTElements.h"
#include "storm-dft/storage/dft/SymmetricUnits.h"
#include "storm-dft/storage/dft/DFTStateGenerationInfo.h"
-
+#include "storm-dft/storage/dft/DFTLayoutInfo.h"
namespace storm {
namespace storage {
@@ -63,7 +63,8 @@ namespace storm {
std::vector<size_t> mTopModule;
std::map<size_t, size_t> mRepresentants; // id element -> id representative
std::vector<std::vector<size_t>> mSymmetries;
-
+ std::map<size_t, DFTLayoutInfo> mLayoutInfo;
+
public:
DFT(DFTElementVector const& elements, DFTElementPointer const& tle);
@@ -263,7 +264,19 @@ namespace storm {
std::vector<size_t> immediateFailureCauses(size_t index) const;
std::vector<size_t> findModularisationRewrite() const;
-
+
+ void setElementLayoutInfo(size_t id, DFTLayoutInfo const& layoutInfo) {
+ mLayoutInfo[id] = layoutInfo;
+ }
+
+ DFTLayoutInfo const& getElementLayoutInfo(size_t id) const {
+ if(mLayoutInfo.count(id) == 0) {
+ STORM_LOG_WARN("Layout info for element with id " << id << " not found");
+ return DFTLayoutInfo();
+ }
+ return mLayoutInfo.at(id);
+ }
+
private:
std::pair<std::vector<size_t>, std::vector<size_t>> getSortedParentAndOutDepIds(size_t index) const;
diff --git a/src/storm-dft/storage/dft/DFTBuilder.cpp b/src/storm-dft/storage/dft/DFTBuilder.cpp
index 612008226..70df810cf 100644
--- a/src/storm-dft/storage/dft/DFTBuilder.cpp
+++ b/src/storm-dft/storage/dft/DFTBuilder.cpp
@@ -25,9 +25,11 @@ namespace storm {
if (itFind != mElements.end()) {
// Child found
DFTElementPointer childElement = itFind->second;
- STORM_LOG_ASSERT(!childElement->isDependency(), "Child is dependency.");
- gate->pushBackChild(childElement);
- childElement->addParent(gate);
+ STORM_LOG_TRACE("Ignore functional dependency " << child << " in gate " << gate->name());
+ if(!childElement->isDependency()) {
+ gate->pushBackChild(childElement);
+ childElement->addParent(gate);
+ }
} else {
// Child not found -> find first dependent event to assure that child is dependency
// TODO: Not sure whether this is the intended behaviour?
@@ -50,17 +52,31 @@ namespace storm {
}
}
- // Initialize dependencies
- for (auto& dependency : mDependencies) {
- DFTGatePointer triggerEvent = std::static_pointer_cast<DFTGate<ValueType>>(mElements[dependency->nameTrigger()]);
- STORM_LOG_ASSERT(mElements[dependency->nameDependent()]->isBasicElement(), "Dependent element is not BE.");
- std::shared_ptr<DFTBE<ValueType>> dependentEvent = std::static_pointer_cast<DFTBE<ValueType>>(mElements[dependency->nameDependent()]);
- dependency->initialize(triggerEvent, dependentEvent);
- triggerEvent->addOutgoingDependency(dependency);
- dependentEvent->addIngoingDependency(dependency);
+ for(auto& elem : mDependencyChildNames) {
+ bool first = true;
+ std::vector<std::shared_ptr<DFTBE<ValueType>>> dependencies;
+ for(auto const& childName : elem.second) {
+ auto itFind = mElements.find(childName);
+ STORM_LOG_ASSERT(itFind != mElements.end(), "Child '" << childName << "' not found");
+ DFTElementPointer childElement = itFind->second;
+ if (!first) {
+ dependencies.push_back(std::static_pointer_cast<DFTBE<ValueType>>(childElement));
+ } else {
+ elem.first->setTriggerElement(std::static_pointer_cast<DFTGate<ValueType>>(childElement));
+ childElement->addOutgoingDependency(elem.first);
+ }
+ first = false;
+ }
+ if (binaryDependencies) {
+ assert(dependencies.size() == 1);
+ }
+ elem.first->setDependentEvents(dependencies);
+ for (auto& dependency : dependencies) {
+ dependency->addIngoingDependency(elem.first);
+ }
+
}
-
-
+
// Sort elements topologically
// compute rank
@@ -73,8 +89,18 @@ namespace storm {
for(DFTElementPointer e : elems) {
e->setId(id++);
}
+
STORM_LOG_ASSERT(!mTopLevelIdentifier.empty(), "No top level element.");
- return DFT<ValueType>(elems, mElements[mTopLevelIdentifier]);
+ DFT<ValueType> dft(elems, mElements[mTopLevelIdentifier]);
+
+ // Set layout info
+ for (auto& elem : mElements) {
+ if(mLayoutInfo.count(elem.first) > 0) {
+ dft.setElementLayoutInfo(elem.second->id(), mLayoutInfo.at(elem.first));
+ }
+ }
+
+ return dft;
}
template<typename ValueType>
@@ -144,10 +170,10 @@ namespace storm {
element = std::make_shared<DFTOr<ValueType>>(mNextId++, name);
break;
case DFTElementType::PAND:
- element = std::make_shared<DFTPand<ValueType>>(mNextId++, name);
+ element = std::make_shared<DFTPand<ValueType>>(mNextId++, name, pandDefaultInclusive);
break;
case DFTElementType::POR:
- element = std::make_shared<DFTPor<ValueType>>(mNextId++, name);
+ element = std::make_shared<DFTPor<ValueType>>(mNextId++, name, porDefaultInclusive);
break;
case DFTElementType::SPARE:
element = std::make_shared<DFTSpare<ValueType>>(mNextId++, name);
@@ -175,10 +201,24 @@ namespace storm {
} else if(visited[n] == topoSortColour::WHITE) {
if(n->isGate()) {
visited[n] = topoSortColour::GREY;
- for(DFTElementPointer const& c : std::static_pointer_cast<DFTGate<ValueType>>(n)->children()) {
+ for (DFTElementPointer const& c : std::static_pointer_cast<DFTGate<ValueType>>(n)->children()) {
+ topoVisit(c, visited, L);
+ }
+ }
+ // TODO restrictions and dependencies have no parents, so this can be done more efficiently.
+ if(n->isRestriction()) {
+ visited[n] = topoSortColour::GREY;
+ for (DFTElementPointer const& c : std::static_pointer_cast<DFTRestriction<ValueType>>(n)->children()) {
topoVisit(c, visited, L);
}
}
+ if(n->isDependency()) {
+ visited[n] = topoSortColour::GREY;
+ for (DFTElementPointer const& c : std::static_pointer_cast<DFTDependency<ValueType>>(n)->dependentEvents()) {
+ topoVisit(c, visited, L);
+ }
+ topoVisit(std::static_pointer_cast<DFTDependency<ValueType>>(n)->triggerEvent(), visited, L);
+ }
visited[n] = topoSortColour::BLACK;
L.push_back(n);
}
@@ -240,7 +280,9 @@ namespace storm {
{
DFTDependencyPointer dependency = std::static_pointer_cast<DFTDependency<ValueType>>(element);
children.push_back(dependency->triggerEvent()->name());
- children.push_back(dependency->dependentEvent()->name());
+ for(auto const& depEv : dependency->dependentEvents()) {
+ children.push_back(depEv->name());
+ }
addDepElement(element->name(), children, dependency->probability());
break;
}
diff --git a/src/storm-dft/storage/dft/DFTBuilder.h b/src/storm-dft/storage/dft/DFTBuilder.h
index f9a11d52b..636b5e5a1 100644
--- a/src/storm-dft/storage/dft/DFTBuilder.h
+++ b/src/storm-dft/storage/dft/DFTBuilder.h
@@ -7,7 +7,7 @@
#include "storm-dft/storage/dft/DFTElements.h"
#include "storm-dft/storage/dft/elements/DFTRestriction.h"
-
+#include "storm-dft/storage/dft/DFTLayoutInfo.h"
namespace storm {
namespace storage {
@@ -31,11 +31,13 @@ namespace storm {
std::unordered_map<std::string, DFTElementPointer> mElements;
std::unordered_map<DFTElementPointer, std::vector<std::string>> mChildNames;
std::unordered_map<DFTRestrictionPointer, std::vector<std::string>> mRestrictionChildNames;
+ std::unordered_map<DFTDependencyPointer, std::vector<std::string>> mDependencyChildNames;
std::vector<DFTDependencyPointer> mDependencies;
std::vector<DFTRestrictionPointer> mRestrictions;
+ std::unordered_map<std::string, DFTLayoutInfo> mLayoutInfo;
public:
- DFTBuilder() {
+ DFTBuilder(bool defaultInclusive = true, bool binaryDependencies = true) : pandDefaultInclusive(defaultInclusive), porDefaultInclusive(defaultInclusive), binaryDependencies(binaryDependencies) {
}
@@ -51,10 +53,26 @@ namespace storm {
return addStandardGate(name, children, DFTElementType::PAND);
}
+ bool addPandElement(std::string const& name, std::vector<std::string> const& children, bool inclusive) {
+ bool tmpDefault = pandDefaultInclusive;
+ pandDefaultInclusive = inclusive;
+ bool result = addStandardGate(name, children, DFTElementType::PAND);
+ pandDefaultInclusive = tmpDefault;
+ return result;
+ }
+
bool addPorElement(std::string const& name, std::vector<std::string> const& children) {
return addStandardGate(name, children, DFTElementType::POR);
}
+ bool addPorElement(std::string const& name, std::vector<std::string> const& children, bool inclusive) {
+ bool tmpDefault = porDefaultInclusive;
+ porDefaultInclusive = inclusive;
+ bool result = addStandardGate(name, children, DFTElementType::POR);
+ pandDefaultInclusive = tmpDefault;
+ return result;
+ }
+
bool addSpareElement(std::string const& name, std::vector<std::string> const& children) {
return addStandardGate(name, children, DFTElementType::SPARE);
}
@@ -84,7 +102,7 @@ namespace storm {
//TODO Matthias: collect constraints for SMT solving
//0 <= probability <= 1
- if (!storm::utility::isOne(probability) && children.size() > 2) {
+ if (binaryDependencies && !storm::utility::isOne(probability) && children.size() > 2) {
// Introduce additional element for first capturing the proabilistic dependency
std::string nameAdditional = name + "_additional";
addBasicElement(nameAdditional, storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>());
@@ -97,16 +115,27 @@ namespace storm {
return true;
} else {
// Add dependencies
- for (size_t i = 1; i < children.size(); ++i) {
- std::string nameDep = name + "_" + std::to_string(i);
- if(mElements.count(nameDep) != 0) {
- // Element with that name already exists.
- STORM_LOG_ERROR("Element with name: " << nameDep << " already exists.");
- return false;
+ if(binaryDependencies) {
+ for (size_t i = 1; i < children.size(); ++i) {
+ std::string nameDep = name + "_" + std::to_string(i);
+ if (mElements.count(nameDep) != 0) {
+ // Element with that name already exists.
+ STORM_LOG_ERROR("Element with name: " << nameDep << " already exists.");
+ return false;
+ }
+ STORM_LOG_ASSERT(storm::utility::isOne(probability) || children.size() == 2,
+ "PDep with multiple children supported.");
+ DFTDependencyPointer element = std::make_shared<DFTDependency<ValueType>>(mNextId++,
+ nameDep,
+ probability);
+ mElements[element->name()] = element;
+ mDependencyChildNames[element] = {trigger, children[i]};
+ mDependencies.push_back(element);
}
- STORM_LOG_ASSERT(storm::utility::isOne(probability) || children.size() == 2, "PDep with multiple children supported.");
- DFTDependencyPointer element = std::make_shared<DFTDependency<ValueType>>(mNextId++, nameDep, trigger, children[i], probability);
+ } else {
+ DFTDependencyPointer element = std::make_shared<DFTDependency<ValueType>>(mNextId++, name, probability);
mElements[element->name()] = element;
+ mDependencyChildNames[element] = children;
mDependencies.push_back(element);
}
return true;
@@ -147,6 +176,11 @@ namespace storm {
mElements[name] = std::make_shared<DFTBE<ValueType>>(mNextId++, name, failureRate, dormancyFactor);
return true;
}
+
+ void addLayoutInfo(std::string const& name, double x, double y) {
+ STORM_LOG_ASSERT(mElements.count(name) > 0, "Element '" << name << "' not found.");
+ mLayoutInfo[name] = storm::storage::DFTLayoutInfo(x, y);
+ }
bool setTopLevel(std::string const& tle) {
mTopLevelIdentifier = tle;
@@ -187,6 +221,13 @@ namespace storm {
DFTElementVector topoSort();
+ // If true, the standard gate adders make a pand inclusive, and exclusive otherwise.
+ bool pandDefaultInclusive;
+ // If true, the standard gate adders make a pand inclusive, and exclusive otherwise.
+ bool porDefaultInclusive;
+
+ bool binaryDependencies;
+
};
}
}
diff --git a/src/storm-dft/storage/dft/DFTIsomorphism.h b/src/storm-dft/storage/dft/DFTIsomorphism.h
index 86625c975..081b76f0b 100644
--- a/src/storm-dft/storage/dft/DFTIsomorphism.h
+++ b/src/storm-dft/storage/dft/DFTIsomorphism.h
@@ -258,7 +258,8 @@ namespace storage {
}
void colourize(std::shared_ptr<const DFTDependency<ValueType>> const& dep) {
- depColour[dep->id()] = std::pair<ValueType, ValueType>(dep->probability(), dep->dependentEvent()->activeFailureRate());
+ // TODO this can be improved for n-ary dependencies.
+ depColour[dep->id()] = std::pair<ValueType, ValueType>(dep->probability(), dep->dependentEvents()[0]->activeFailureRate());
}
void colourize(std::shared_ptr<const DFTRestriction<ValueType>> const& restr) {
@@ -486,10 +487,26 @@ namespace storage {
STORM_LOG_ASSERT(dft.isDependency(indexpair.second), "Element is no dependency.");
auto const& lDep = dft.getDependency(indexpair.first);
auto const& rDep = dft.getDependency(indexpair.second);
+
if(bijection.at(lDep->triggerEvent()->id()) != rDep->triggerEvent()->id()) {
return false;
- }
- if(bijection.at(lDep->dependentEvent()->id()) != rDep->dependentEvent()->id()) {
+ }
+
+ std::set<size_t> dependenciesLeftMapped;
+ for (auto const& depEv : lDep->dependentEvents()) {
+ if (bleft.has(depEv->id())) {
+ dependenciesLeftMapped.insert(bijection.at(depEv->id()));
+ }
+ }
+
+ std::set<size_t> dependenciesRight;
+ for (auto const& depEv : rDep->dependentEvents()) {
+ if (bright.has(depEv->id())) {
+ dependenciesRight.insert(depEv->id());
+ }
+ }
+
+ if (dependenciesLeftMapped != dependenciesRight) {
return false;
}
} else if(dft.isRestriction(indexpair.first)) {
diff --git a/src/storm-dft/storage/dft/DFTLayoutInfo.h b/src/storm-dft/storage/dft/DFTLayoutInfo.h
new file mode 100644
index 000000000..c61de0f6d
--- /dev/null
+++ b/src/storm-dft/storage/dft/DFTLayoutInfo.h
@@ -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;
+ };
+ }
+}
diff --git a/src/storm-dft/storage/dft/DFTState.cpp b/src/storm-dft/storage/dft/DFTState.cpp
index 78c0937d8..ec6509944 100644
--- a/src/storm-dft/storage/dft/DFTState.cpp
+++ b/src/storm-dft/storage/dft/DFTState.cpp
@@ -57,7 +57,8 @@ namespace storm {
for (size_t dependencyId : mDft.getDependencies()) {
std::shared_ptr<DFTDependency<ValueType> const> dependency = mDft.getDependency(dependencyId);
STORM_LOG_ASSERT(dependencyId == dependency->id(), "Ids do not match.");
- if (hasFailed(dependency->triggerEvent()->id()) && getElementState(dependency->dependentEvent()->id()) == DFTElementState::Operational) {
+ assert(dependency->dependentEvents().size() == 1);
+ if (hasFailed(dependency->triggerEvent()->id()) && getElementState(dependency->dependentEvents()[0]->id()) == DFTElementState::Operational) {
mFailableDependencies.push_back(dependencyId);
STORM_LOG_TRACE("New dependency failure: " << dependency->toString());
}
@@ -198,8 +199,9 @@ namespace storm {
for (auto dependency : mDft.getElement(id)->outgoingDependencies()) {
STORM_LOG_ASSERT(dependency->triggerEvent()->id() == id, "Ids do not match.");
- if (getElementState(dependency->dependentEvent()->id()) == DFTElementState::Operational) {
- STORM_LOG_ASSERT(!isFailsafe(dependency->dependentEvent()->id()), "Dependent event is failsafe.");
+ assert(dependency->dependentEvents().size() == 1);
+ if (getElementState(dependency->dependentEvents()[0]->id()) == DFTElementState::Operational) {
+ STORM_LOG_ASSERT(!isFailsafe(dependency->dependentEvents()[0]->id()), "Dependent event is failsafe.");
mFailableDependencies.push_back(dependency->id());
STORM_LOG_TRACE("New dependency failure: " << dependency->toString());
}
@@ -213,7 +215,8 @@ namespace storm {
STORM_LOG_ASSERT(hasFailed(id), "Element has not failed.");
for (auto dependency : mDft.getBasicElement(id)->ingoingDependencies()) {
- STORM_LOG_ASSERT(dependency->dependentEvent()->id() == id, "Ids do not match.");
+ assert(dependency->dependentEvents().size() == 1);
+ STORM_LOG_ASSERT(dependency->dependentEvents()[0]->id() == id, "Ids do not match.");
setDependencyDontCare(dependency->id());
}
}
@@ -244,7 +247,8 @@ namespace storm {
// Consider failure due to dependency
STORM_LOG_ASSERT(index < nrFailableDependencies(), "Index invalid.");
std::shared_ptr<DFTDependency<ValueType> const> dependency = mDft.getDependency(mFailableDependencies[index]);
- std::pair<std::shared_ptr<DFTBE<ValueType> const>,bool> res(mDft.getBasicElement(dependency->dependentEvent()->id()), true);
+ assert(dependency->dependentEvents().size() == 1);
+ std::pair<std::shared_ptr<DFTBE<ValueType> const>,bool> res(mDft.getBasicElement(dependency->dependentEvents()[0]->id()), true);
mFailableDependencies.erase(mFailableDependencies.begin() + index);
setFailed(res.first->id());
setDependencySuccessful(dependency->id());
diff --git a/src/storm-dft/storage/dft/elements/DFTBE.h b/src/storm-dft/storage/dft/elements/DFTBE.h
index 216227af6..3be82d9f1 100644
--- a/src/storm-dft/storage/dft/elements/DFTBE.h
+++ b/src/storm-dft/storage/dft/elements/DFTBE.h
@@ -38,7 +38,8 @@ namespace storm {
}
bool addIngoingDependency(DFTDependencyPointer const& e) {
- STORM_LOG_ASSERT(e->dependentEvent()->id() == this->id(), "Ids do not match.");
+ // TODO write this assertion for n-ary dependencies, probably by addign a method to the dependencies to support this.
+ //STORM_LOG_ASSERT(e->dependentEvent()->id() == this->id(), "Ids do not match.");
if(std::find(mIngoingDependencies.begin(), mIngoingDependencies.end(), e) != mIngoingDependencies.end()) {
return false;
}
diff --git a/src/storm-dft/storage/dft/elements/DFTDependency.h b/src/storm-dft/storage/dft/elements/DFTDependency.h
index 2c5b7d0cc..7d11bae2a 100644
--- a/src/storm-dft/storage/dft/elements/DFTDependency.h
+++ b/src/storm-dft/storage/dft/elements/DFTDependency.h
@@ -12,35 +12,28 @@ namespace storm {
using DFTBEPointer = std::shared_ptr<DFTBE<ValueType>>;
protected:
- std::string mNameTrigger;
- std::string mNameDependent;
ValueType mProbability;
DFTGatePointer mTriggerEvent;
- DFTBEPointer mDependentEvent;
+ std::vector<DFTBEPointer> mDependentEvents;
public:
- DFTDependency(size_t id, std::string const& name, std::string const& trigger, std::string const& dependent, ValueType probability) :
- DFTElement<ValueType>(id, name), mNameTrigger(trigger), mNameDependent(dependent), mProbability(probability)
+ DFTDependency(size_t id, std::string const& name, ValueType probability) :
+ DFTElement<ValueType>(id, name), mProbability(probability)
{
}
virtual ~DFTDependency() {}
- void initialize(DFTGatePointer triggerEvent, DFTBEPointer dependentEvent) {
- STORM_LOG_ASSERT(triggerEvent->name() == mNameTrigger, "Name does not match.");
- STORM_LOG_ASSERT(dependentEvent->name() == mNameDependent, "Name does not match.");
+ void setTriggerElement(DFTGatePointer const& triggerEvent) {
mTriggerEvent = triggerEvent;
- mDependentEvent = dependentEvent;
- }
- std::string nameTrigger() const {
- return mNameTrigger;
}
- std::string nameDependent() const {
- return mNameDependent;
+ void setDependentEvents(std::vector<DFTBEPointer> const& dependentEvents) {
+ mDependentEvents = dependentEvents;
}
+
ValueType const& probability() const {
return mProbability;
}
@@ -50,9 +43,9 @@ namespace storm {
return mTriggerEvent;
}
- DFTBEPointer const& dependentEvent() const {
- STORM_LOG_ASSERT(mDependentEvent, "Dependent element does not exists.");
- return mDependentEvent;
+ std::vector<DFTBEPointer> const& dependentEvents() const {
+ STORM_LOG_ASSERT(mDependentEvents.size() > 0, "Dependent element does not exists.");
+ return mDependentEvents;
}
DFTElementType type() const override {
@@ -76,9 +69,11 @@ namespace storm {
virtual std::vector<size_t> independentUnit() const override {
std::set<size_t> unit = {this->mId};
- mDependentEvent->extendUnit(unit);
- if(unit.count(mTriggerEvent->id()) != 0) {
- return {};
+ for(auto const& depEv : mDependentEvents) {
+ depEv->extendUnit(unit);
+ if(unit.count(mTriggerEvent->id()) != 0) {
+ return {};
+ }
}
return std::vector<size_t>(unit.begin(), unit.end());
}
@@ -90,7 +85,10 @@ namespace storm {
// Parent in the subdft, ie it is *not* a subdft
return;
}
- mDependentEvent->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
+ for (auto const& depEv : mDependentEvents) {
+ depEv->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
+ if (elemsInSubtree.empty()) return;
+ }
if(elemsInSubtree.empty()) {
// Parent in the subdft, ie it is *not* a subdft
return;
@@ -102,7 +100,11 @@ namespace storm {
virtual std::string toString() const override {
std::stringstream stream;
bool fdep = storm::utility::isOne(mProbability);
- stream << "{" << this->name() << "} " << (fdep ? "FDEP" : "PDEP") << "(" << mTriggerEvent->name() << " => " << mDependentEvent->name() << ")";
+ stream << "{" << this->name() << "} " << (fdep ? "FDEP" : "PDEP") << "(" << mTriggerEvent->name() << " => { ";
+ for(auto const& depEv : mDependentEvents) {
+ stream << depEv->name() << " ";
+ }
+ stream << "}";
if (!fdep) {
stream << " with probability " << mProbability;
}
diff --git a/src/storm-dft/storage/dft/elements/DFTElement.cpp b/src/storm-dft/storage/dft/elements/DFTElement.cpp
index 61a087bdb..287af8e98 100644
--- a/src/storm-dft/storage/dft/elements/DFTElement.cpp
+++ b/src/storm-dft/storage/dft/elements/DFTElement.cpp
@@ -14,8 +14,10 @@ namespace storm {
}
// Check that no outgoing dependencies can be triggered anymore
+ // Notice that n-ary dependencies are supported via rewriting them during build-time
for (DFTDependencyPointer dependency : mOutgoingDependencies) {
- if (state.isOperational(dependency->dependentEvent()->id()) && state.isOperational(dependency->triggerEvent()->id())) {
+ assert(dependency->dependentEvents().size() == 1);
+ if (state.isOperational(dependency->dependentEvents()[0]->id()) && state.isOperational(dependency->triggerEvent()->id())) {
return false;
}
}
diff --git a/src/storm-dft/storage/dft/elements/DFTPand.h b/src/storm-dft/storage/dft/elements/DFTPand.h
index bb18efe72..21cda29a9 100644
--- a/src/storm-dft/storage/dft/elements/DFTPand.h
+++ b/src/storm-dft/storage/dft/elements/DFTPand.h
@@ -7,11 +7,13 @@ namespace storm {
class DFTPand : public DFTGate<ValueType> {
public:
- DFTPand(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
- DFTGate<ValueType>(id, name, children)
+ DFTPand(size_t id, std::string const& name, bool inclusive, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
+ DFTGate<ValueType>(id, name, children),
+ inclusive(inclusive)
{}
void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+ assert(inclusive);
if(state.isOperational(this->mId)) {
bool childOperationalBefore = false;
for(auto const& child : this->mChildren)
@@ -31,6 +33,7 @@ namespace storm {
}
void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+ assert(inclusive);
STORM_LOG_ASSERT(this->hasFailsafeChild(state), "No failsafe child.");
if(state.isOperational(this->mId)) {
this->failsafe(state, queues);
@@ -42,9 +45,15 @@ namespace storm {
return DFTElementType::PAND;
}
+ bool isInclusive() const {
+ return inclusive;
+ }
+
std::string typestring() const override {
- return "PAND";
+ return inclusive ? "PAND-inc" : "PAND-ex";
}
+ protected:
+ bool inclusive;
};
template<typename ValueType>
diff --git a/src/storm-dft/storage/dft/elements/DFTPor.h b/src/storm-dft/storage/dft/elements/DFTPor.h
index 6e2fe731c..857e19714 100644
--- a/src/storm-dft/storage/dft/elements/DFTPor.h
+++ b/src/storm-dft/storage/dft/elements/DFTPor.h
@@ -6,12 +6,14 @@ namespace storm {
template<typename ValueType>
class DFTPor : public DFTGate<ValueType> {
public:
- DFTPor(size_t id, std::string const& name, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
- DFTGate<ValueType>(id, name, children)
+ DFTPor(size_t id, std::string const& name, bool inclusive, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children = {}) :
+ DFTGate<ValueType>(id, name, children),
+ inclusive(inclusive)
{}
void checkFails(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
- if(state.isOperational(this->mId)) {
+ assert(inclusive);
+ if(state.isOperational(this->mId)) {
if (state.hasFailed(this->mChildren.front()->id())) {
// First child has failed before others
this->fail(state, queues);
@@ -28,6 +30,7 @@ namespace storm {
}
void checkFailsafe(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
+ assert(inclusive);
if (state.isFailsafe(this->mChildren.front()->id())) {
this->failsafe(state, queues);
this->childrenDontCare(state, queues);
@@ -39,8 +42,14 @@ namespace storm {
}
std::string typestring() const override {
- return "POR";
+ return inclusive ? "POR-inc" : "POR-ex";
}
+
+ bool isInclusive() const {
+ return inclusive;
+ }
+ protected:
+ bool inclusive;
};
template<typename ValueType>
diff --git a/src/storm-dft/storage/dft/elements/DFTRestriction.h b/src/storm-dft/storage/dft/elements/DFTRestriction.h
index f4a03f688..195a217bb 100644
--- a/src/storm-dft/storage/dft/elements/DFTRestriction.h
+++ b/src/storm-dft/storage/dft/elements/DFTRestriction.h
@@ -36,6 +36,15 @@ namespace storm {
virtual bool isSeqEnforcer() const {
return false;
}
+
+ bool allChildrenBEs() const {
+ for(auto const& elem : mChildren) {
+ if (!elem->isBasicElement()) {
+ return false;
+ }
+ }
+ return true;
+ }
virtual std::string typestring() const = 0;
diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp
new file mode 100644
index 000000000..8c3ef0448
--- /dev/null
+++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp
@@ -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
+
+
diff --git a/src/storm-dft/transformations/DftToGspnTransformator.h b/src/storm-dft/transformations/DftToGspnTransformator.h
new file mode 100644
index 000000000..4ec911b23
--- /dev/null
+++ b/src/storm-dft/transformations/DftToGspnTransformator.h
@@ -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.
+
+
+ };
+ }
+ }
+}
+
diff --git a/src/storm-gspn-cli/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp
index b973d046d..17b45222d 100644
--- a/src/storm-gspn-cli/storm-gspn.cpp
+++ b/src/storm-gspn-cli/storm-gspn.cpp
@@ -66,9 +66,7 @@ std::unordered_map<std::string, uint64_t> parseCapacitiesList(std::string const&
}
void handleJani(storm::gspn::GSPN const& gspn) {
- std::shared_ptr<storm::expressions::ExpressionManager> exprManager(new storm::expressions::ExpressionManager());
- storm::builder::JaniGSPNBuilder builder(gspn, exprManager);
- storm::jani::Model* model = builder.build();
+
storm::jani::JsonExporter::toFile(*model, {}, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
delete model;
}
diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.h b/src/storm-gspn/builder/JaniGSPNBuilder.h
index 76517a3a1..196d29562 100644
--- a/src/storm-gspn/builder/JaniGSPNBuilder.h
+++ b/src/storm-gspn/builder/JaniGSPNBuilder.h
@@ -9,17 +9,11 @@ namespace storm {
class JaniGSPNBuilder {
public:
JaniGSPNBuilder(storm::gspn::GSPN const& gspn, std::shared_ptr<storm::expressions::ExpressionManager> const& expManager) : gspn(gspn), expressionManager(expManager) {
- gspn.writeDotToStream(std::cout);
+
}
virtual ~JaniGSPNBuilder() {
- for (auto const& varEntry : vars) {
- delete varEntry.second;
- }
- }
-
- void setIgnoreWeights(bool ignore = true) {
- ignoreWeights = ignore;
+
}
@@ -34,6 +28,10 @@ namespace storm {
return model;
}
+ storm::jani::Variable const& getPlaceVariable(uint64_t placeId) {
+ return *vars.at(placeId);
+ }
+
void addVariables(storm::jani::Model* model) {
for (auto const& place : gspn.getPlaces()) {
storm::jani::Variable* janiVar = nullptr;
@@ -46,8 +44,8 @@ namespace storm {
}
assert(janiVar != nullptr);
assert(vars.count(place.getID()) == 0);
- vars[place.getID()] = janiVar;
- model->addVariable(*janiVar);
+ vars[place.getID()] = &model->addVariable(*janiVar);
+ delete janiVar;
}
}
@@ -59,95 +57,76 @@ namespace storm {
void addEdges(storm::jani::Automaton& automaton, uint64_t locId) {
- storm::expressions::Expression guard = expressionManager->boolean(true);
- for (auto const& trans : gspn.getImmediateTransitions()) {
- if (ignoreWeights || trans.noWeightAttached()) {
- std::vector<storm::jani::Assignment> assignments;
+ uint64_t lastPriority = -1;
+ storm::expressions::Expression lastPriorityGuard = expressionManager->boolean(false);
+ storm::expressions::Expression priorityGuard = expressionManager->boolean(true);
+ // TODO here there is something to fix if we add transition partitions.
+
+ for (auto const& partition : gspn.getPartitions()) {
+ storm::expressions::Expression guard = expressionManager->boolean(false);
+ std::vector<storm::jani::EdgeDestination> weightedDestinations;
+
+ assert(lastPriority >= partition.priority);
+ if (lastPriority > partition.priority) {
+ priorityGuard = priorityGuard && !lastPriorityGuard;
+ lastPriority = partition.priority;
+ } else {
+ assert(lastPriority == partition.priority);
+ }
+
+ // Compute enabled weight expression.
+ storm::expressions::Expression totalWeight = expressionManager->rational(0.0);
+ for (auto const& transId : partition.transitions) {
+ auto const& trans = gspn.getImmediateTransitions()[transId];
+ if (trans.noWeightAttached()) {
+ continue;
+ }
+ storm::expressions::Expression destguard = expressionManager->boolean(true);
for (auto const& inPlaceEntry : trans.getInputPlaces()) {
- guard = guard && (vars[inPlaceEntry.first]->getExpressionVariable() > inPlaceEntry.second);
- assignments.emplace_back( *vars[inPlaceEntry.first], (vars[inPlaceEntry.first])->getExpressionVariable() - inPlaceEntry.second);
+ destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() >= inPlaceEntry.second);
}
for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) {
- guard = guard && (vars[inhibPlaceEntry.first]->getExpressionVariable() > inhibPlaceEntry.second);
- }
- for (auto const& outputPlaceEntry : trans.getOutputPlaces()) {
- assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second );
+ destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() < inhibPlaceEntry.second);
}
- storm::jani::OrderedAssignments oa(assignments);
- storm::jani::EdgeDestination dest(locId, expressionManager->integer(1), oa);
- storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, boost::none, guard, {dest});
- automaton.addEdge(e);
+ totalWeight = totalWeight + storm::expressions::ite(destguard, expressionManager->rational(trans.getWeight()), expressionManager->rational(0.0));
+
}
+ totalWeight = totalWeight.simplify();
- }
- if(!ignoreWeights) {
- uint64_t lastPriority;
- storm::expressions::Expression lastPriorityGuard = expressionManager->boolean(false);
- storm::expressions::Expression priorityGuard = expressionManager->boolean(true);
- // TODO here there is something to fix if we add transition partitions.
- for (auto const& partition : gspn.getPartitions()) {
- storm::expressions::Expression guard = expressionManager->boolean(false);
- std::vector<storm::jani::EdgeDestination> weightedDestinations;
-
-
- assert(lastPriority <= partition.priority);
- if (lastPriority < partition.priority) {
- priorityGuard = priorityGuard && !lastPriorityGuard;
- lastPriority = partition.priority;
- } else {
- assert(lastPriority == partition.priority);
+ for (auto const& transId : partition.transitions) {
+ auto const& trans = gspn.getImmediateTransitions()[transId];
+ if (trans.noWeightAttached()) {
+ std::cout << "ERROR -- no weights attached at transition" << std::endl;
+ continue;
}
-
- // Compute enabled weight expression.
- storm::expressions::Expression totalWeight = expressionManager->rational(0.0);
- for (auto const& transId : partition.transitions) {
- auto const& trans = gspn.getImmediateTransitions()[transId];
- if (trans.noWeightAttached()) {
- continue;
- }
- storm::expressions::Expression destguard = expressionManager->boolean(true);
- for (auto const& inPlaceEntry : trans.getInputPlaces()) {
- destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() > inPlaceEntry.second);
- }
- for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) {
- destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() > inhibPlaceEntry.second);
+ storm::expressions::Expression destguard = expressionManager->boolean(true);
+ std::vector<storm::jani::Assignment> assignments;
+ for (auto const& inPlaceEntry : trans.getInputPlaces()) {
+ destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() >= inPlaceEntry.second);
+ if (trans.getOutputPlaces().count(inPlaceEntry.first) == 0) {
+ assignments.emplace_back( *vars[inPlaceEntry.first], (vars[inPlaceEntry.first])->getExpressionVariable() - inPlaceEntry.second);
}
- totalWeight = totalWeight + storm::expressions::ite(destguard, expressionManager->rational(trans.getWeight()), expressionManager->rational(0.0));
-
}
- totalWeight = totalWeight.simplify();
-
-
- for (auto const& transId : partition.transitions) {
- auto const& trans = gspn.getImmediateTransitions()[transId];
- if (trans.noWeightAttached()) {
- continue;
- }
- storm::expressions::Expression destguard = expressionManager->boolean(true);
- std::vector<storm::jani::Assignment> assignments;
- for (auto const& inPlaceEntry : trans.getInputPlaces()) {
- destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() > inPlaceEntry.second);
- assignments.emplace_back( *vars[inPlaceEntry.first], (vars[inPlaceEntry.first]->getExpressionVariable() - inPlaceEntry.second) );
- }
- for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) {
- destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() > inhibPlaceEntry.second);
- }
- for (auto const& outputPlaceEntry : trans.getOutputPlaces()) {
- assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first]->getExpressionVariable() + outputPlaceEntry.second) );
+ for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) {
+ destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() < inhibPlaceEntry.second);
+ }
+ for (auto const& outputPlaceEntry : trans.getOutputPlaces()) {
+ if (trans.getInputPlaces().count(outputPlaceEntry.first) == 0) {
+ assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second );
+ } else {
+ assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second - trans.getInputPlaces().at(outputPlaceEntry.first));
}
- destguard = destguard.simplify();
- guard = guard || destguard;
- storm::jani::OrderedAssignments oa(assignments);
- storm::jani::EdgeDestination dest(locId, storm::expressions::ite(destguard, (expressionManager->rational(trans.getWeight()) / totalWeight), expressionManager->rational(0.0)), oa);
- weightedDestinations.push_back(dest);
}
- storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, boost::none, (priorityGuard && guard).simplify(), weightedDestinations);
- automaton.addEdge(e);
- lastPriorityGuard = lastPriorityGuard || guard;
+ destguard = destguard.simplify();
+ guard = guard || destguard;
+ storm::jani::OrderedAssignments oa(assignments);
+ storm::jani::EdgeDestination dest(locId, storm::expressions::ite(destguard, (expressionManager->rational(trans.getWeight()) / totalWeight), expressionManager->rational(0.0)), oa);
+ weightedDestinations.push_back(dest);
}
-
-
+ storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, boost::none, (priorityGuard && guard).simplify(), weightedDestinations);
+ automaton.addEdge(e);
+ lastPriorityGuard = lastPriorityGuard || guard;
}
for (auto const& trans : gspn.getTimedTransitions()) {
@@ -155,27 +134,33 @@ namespace storm {
std::vector<storm::jani::Assignment> assignments;
for (auto const& inPlaceEntry : trans.getInputPlaces()) {
- guard = guard && (vars[inPlaceEntry.first]->getExpressionVariable() > inPlaceEntry.second);
- assignments.emplace_back( *vars[inPlaceEntry.first], (vars[inPlaceEntry.first]->getExpressionVariable() - inPlaceEntry.second) );
+ guard = guard && (vars[inPlaceEntry.first]->getExpressionVariable() >= inPlaceEntry.second);
+ if (trans.getOutputPlaces().count(inPlaceEntry.first) == 0) {
+ assignments.emplace_back( *vars[inPlaceEntry.first], (vars[inPlaceEntry.first])->getExpressionVariable() - inPlaceEntry.second);
+ }
}
for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) {
- guard = guard && (vars[inhibPlaceEntry.first]->getExpressionVariable() > inhibPlaceEntry.second);
+ guard = guard && (vars[inhibPlaceEntry.first]->getExpressionVariable() < inhibPlaceEntry.second);
}
for (auto const& outputPlaceEntry : trans.getOutputPlaces()) {
- assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first]->getExpressionVariable() + outputPlaceEntry.second) );
+ if (trans.getInputPlaces().count(outputPlaceEntry.first) == 0) {
+ assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second );
+ } else {
+ assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first])->getExpressionVariable() + outputPlaceEntry.second - trans.getInputPlaces().at(outputPlaceEntry.first));
+ }
}
storm::jani::OrderedAssignments oa(assignments);
storm::jani::EdgeDestination dest(locId, expressionManager->integer(1), oa);
storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, expressionManager->rational(trans.getRate()), guard, {dest});
automaton.addEdge(e);
+
}
}
private:
- bool ignoreWeights;
const uint64_t janiVersion = 1;
storm::gspn::GSPN const& gspn;
- std::map<uint64_t, storm::jani::Variable*> vars;
+ std::map<uint64_t, storm::jani::Variable const*> vars;
std::shared_ptr<storm::expressions::ExpressionManager> expressionManager;
};
diff --git a/src/storm-gspn/storage/gspn/GSPN.cpp b/src/storm-gspn/storage/gspn/GSPN.cpp
index 5a7f819de..ce0d47d44 100644
--- a/src/storm-gspn/storage/gspn/GSPN.cpp
+++ b/src/storm-gspn/storage/gspn/GSPN.cpp
@@ -36,6 +36,14 @@ namespace storm {
uint64_t GSPN::getNumberOfPlaces() const {
return places.size();
}
+
+ uint64_t GSPN::getNumberOfImmediateTransitions() const {
+ return immediateTransitions.size();
+ }
+
+ uint64_t GSPN::getNumberOfTimedTransitions() const {
+ return timedTransitions.size();
+ }
std::vector<storm::gspn::TimedTransition<GSPN::RateType>> const& GSPN::getTimedTransitions() const {
return this->timedTransitions;
@@ -368,6 +376,20 @@ namespace storm {
return result;
}
+
+ void GSPN::setPlaceLayoutInfo(uint64_t placeId, LayoutInfo const& layout) const {
+ placeLayout[placeId] = layout;
+ }
+ void GSPN::setTransitionLayoutInfo(uint64_t transitionId, LayoutInfo const& layout) const {
+ transitionLayout[transitionId] = layout;
+ }
+
+ void GSPN::setPlaceLayoutInfo(std::map<uint64_t, LayoutInfo> const& placeLayout) const {
+ this->placeLayout = placeLayout;
+ }
+ void GSPN::setTransitionLayoutInfo(std::map<uint64_t, LayoutInfo> const& transitionLayout) const {
+ this->transitionLayout = transitionLayout;
+ }
void GSPN::toPnpro(std::ostream &stream) const {
auto space = " ";
@@ -382,8 +404,14 @@ namespace storm {
for (auto& place : places) {
stream << space3 << "<place marking=\"" << place.getNumberOfInitialTokens() <<"\" ";
stream << "name =\"" << place.getName() << "\" ";
- stream << "x=\"" << x << "\" ";
- stream << "y=\"1\" ";
+ if (placeLayout.count(place.getID()) > 0) {
+ stream << "x=\"" << placeLayout.at(place.getID()).x << "\" ";
+ stream << "y=\"" << placeLayout.at(place.getID()).y << "\" ";
+ } else {
+ stream << "x=\"" << x << "\" ";
+ stream << "y=\"1\" ";
+
+ }
stream << "/>" << std::endl;
x = x + 3;
}
@@ -392,16 +420,28 @@ namespace storm {
stream << space3 << "<transition name=\"" << trans.getName() << "\" ";
stream << "type=\"EXP\" ";
stream << "nservers-x=\"" << trans.getRate() << "\" ";
- stream << "x=\"" << x << "\" ";
- stream << "y=\"4\" ";
+ if (transitionLayout.count(trans.getID()) > 0) {
+ stream << "x=\"" << transitionLayout.at(trans.getID()).x << "\" ";
+ stream << "y=\"" << transitionLayout.at(trans.getID()).y << "\" ";
+ } else {
+ stream << "x=\"" << x << "\" ";
+ stream << "y=\"4\" ";
+
+ }
stream << "/>" << std::endl;
x = x + 3;
}
for (auto& trans : immediateTransitions) {
stream << space3 << "<transition name=\"" << trans.getName() << "\" ";
stream << "type=\"IMM\" ";
- stream << "x=\"" << x << "\" ";
- stream << "y=\"4\" ";
+ stream << "priority=\"" << trans.getPriority() << "\" ";
+ if (transitionLayout.count(trans.getID()) > 0) {
+ stream << "x=\"" << transitionLayout.at(trans.getID()).x << "\" ";
+ stream << "y=\"" << transitionLayout.at(trans.getID()).y << "\" ";
+ } else {
+ stream << "x=\"" << x << "\" ";
+ stream << "y=\"4\" ";
+ }
stream << "/>" << std::endl;
x = x + 3;
}
@@ -565,6 +605,12 @@ namespace storm {
stream << space << "</net>" << std::endl;
stream << "</pnml>" << std::endl;
}
+
+ void GSPN::writeStatsToStream(std::ostream& stream) const {
+ stream << "Number of places: " << getNumberOfPlaces() << std::endl;
+ stream << "Number of timed transitions: " << getNumberOfTimedTransitions() << std::endl;
+ stream << "Number of immediate transitions: " << getNumberOfImmediateTransitions() << std::endl;
+ }
}
}
diff --git a/src/storm-gspn/storage/gspn/GSPN.h b/src/storm-gspn/storage/gspn/GSPN.h
index 7086a6c1c..947769af3 100644
--- a/src/storm-gspn/storage/gspn/GSPN.h
+++ b/src/storm-gspn/storage/gspn/GSPN.h
@@ -11,6 +11,7 @@
#include "storm-gspn/storage/gspn/Place.h"
#include "storm-gspn/storage/gspn/TimedTransition.h"
#include "storm-gspn/storage/gspn/TransitionPartition.h"
+#include "storm-gspn/storage/gspn/PlacementInfo.h"
namespace storm {
namespace gspn {
@@ -37,6 +38,10 @@ namespace storm {
* @return The number of places.
*/
uint64_t getNumberOfPlaces() const;
+
+ uint64_t getNumberOfImmediateTransitions() const;
+
+ uint64_t getNumberOfTimedTransitions() const;
/*!
*
@@ -136,7 +141,13 @@ namespace storm {
* Set Capacities according to name->capacity map.
*/
void setCapacities(std::unordered_map<std::string, uint64_t> const& mapping);
-
+
+ void setPlaceLayoutInfo(uint64_t placeId, LayoutInfo const& layout) const;
+ void setTransitionLayoutInfo(uint64_t transitionId, LayoutInfo const& layout) const;
+ void setPlaceLayoutInfo(std::map<uint64_t, LayoutInfo> const& placeLayout) const;
+ void setTransitionLayoutInfo(std::map<uint64_t, LayoutInfo> const& transitionLayout) const;
+
+
/*!
* Performe some checks
* - testPlaces()
@@ -146,9 +157,11 @@ namespace storm {
*/
bool isValid() const;
// TODO doc
- void toPnpro(std::ostream &stream) const;
+ void toPnpro(std::ostream& stream) const;
// TODO doc
- void toPnml(std::ostream &stream) const;
+ void toPnml(std::ostream& stream) const;
+
+ void writeStatsToStream(std::ostream& stream) const;
private:
storm::gspn::Place* getPlace(uint64_t id);
storm::gspn::Place* getPlace(std::string const& name);
@@ -185,6 +198,10 @@ namespace storm {
std::vector<storm::gspn::TransitionPartition> partitions;
+ mutable std::map<uint64_t, LayoutInfo> placeLayout;
+ mutable std::map<uint64_t, LayoutInfo> transitionLayout;
+
+
};
}
}
diff --git a/src/storm-gspn/storage/gspn/GspnBuilder.cpp b/src/storm-gspn/storage/gspn/GspnBuilder.cpp
index 9cb662eb7..e0bbd76fd 100644
--- a/src/storm-gspn/storage/gspn/GspnBuilder.cpp
+++ b/src/storm-gspn/storage/gspn/GspnBuilder.cpp
@@ -23,6 +23,15 @@ namespace storm {
places.push_back(place);
return newId;
}
+
+
+ void GspnBuilder::setPlaceLayoutInfo(uint64_t placeId, LayoutInfo const& layoutInfo) {
+ placeLayout[placeId] = layoutInfo;
+ }
+
+ void GspnBuilder::setTransitionLayoutInfo(uint64_t transitionId, LayoutInfo const& layoutInfo) {
+ transitionLayout[transitionId] = layoutInfo;
+ }
uint_fast64_t GspnBuilder::addImmediateTransition(uint_fast64_t const& priority, double const& weight, std::string const& name) {
auto trans = storm::gspn::ImmediateTransition<double>();
@@ -35,7 +44,7 @@ namespace storm {
if(partitions.count(priority) == 0) {
TransitionPartition newPart;
newPart.priority = priority;
- partitions.at(priority).push_back(newPart);
+ partitions[priority].push_back(newPart);
}
if(storm::utility::isZero(weight)) {
@@ -164,7 +173,10 @@ namespace storm {
}
std::reverse(orderedPartitions.begin(), orderedPartitions.end());
- return new GSPN(gspnName, places, immediateTransitions, timedTransitions, orderedPartitions);
+ GSPN* result = new GSPN(gspnName, places, immediateTransitions, timedTransitions, orderedPartitions);
+ result->setTransitionLayoutInfo(transitionLayout);
+ result->setPlaceLayoutInfo(placeLayout);
+ return result;
}
}
}
diff --git a/src/storm-gspn/storage/gspn/GspnBuilder.h b/src/storm-gspn/storage/gspn/GspnBuilder.h
index 2f63ba719..79fb2e712 100644
--- a/src/storm-gspn/storage/gspn/GspnBuilder.h
+++ b/src/storm-gspn/storage/gspn/GspnBuilder.h
@@ -20,29 +20,32 @@ namespace storm {
/**
* Add a place to the gspn.
- * @param id The id must be unique for the gspn.
* @param name The name must be unique for the gspn.
* @param capacity The capacity is the limit of tokens in the place.
* A capacity of -1 indicates an unbounded place.
* @param initialTokens The number of inital tokens in the place.
*/
uint_fast64_t addPlace(int_fast64_t const& capacity = 1, uint_fast64_t const& initialTokens = 0, std::string const& name = "");
+
+ void setPlaceLayoutInfo(uint64_t placeId, LayoutInfo const& layoutInfo);
/**
* Adds an immediate transition to the gspn.
- * @param id The id must be unique for the gspn.
* @param priority The priority for the transtion.
* @param weight The weight for the transition.
*/
uint_fast64_t addImmediateTransition(uint_fast64_t const& priority = 0, WeightType const& weight = 0, std::string const& name = "");
-
+
+
/**
* Adds an timed transition to the gspn.
- * @param id The name id be unique for the gspn.
* @param priority The priority for the transtion.
* @param weight The weight for the transition.
*/
uint_fast64_t addTimedTransition(uint_fast64_t const &priority, RateType const& rate, std::string const& name = "");
+
+ void setTransitionLayoutInfo(uint64_t transitionId, LayoutInfo const& layoutInfo);
+
/**
* Adds an new input arc from a place to an transition.
@@ -112,6 +115,9 @@ namespace storm {
// set containing all places
std::vector<storm::gspn::Place> places;
+
+ std::map<uint64_t, LayoutInfo> placeLayout;
+ std::map<uint64_t, LayoutInfo> transitionLayout;
};
}
}
diff --git a/src/storm-gspn/storage/gspn/PlacementInfo.h b/src/storm-gspn/storage/gspn/PlacementInfo.h
new file mode 100644
index 000000000..e59218686
--- /dev/null
+++ b/src/storm-gspn/storage/gspn/PlacementInfo.h
@@ -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;
+ };
+ }
+}
\ No newline at end of file
diff --git a/src/storm-gspn/storage/gspn/Transition.h b/src/storm-gspn/storage/gspn/Transition.h
index d61affaea..9deab2fb0 100644
--- a/src/storm-gspn/storage/gspn/Transition.h
+++ b/src/storm-gspn/storage/gspn/Transition.h
@@ -168,6 +168,9 @@ namespace storm {
void setID(uint64_t const& id) {
this->id = id;
}
+
+
+ uint64_t getID() const { return id; }
private:
// maps place ids connected to this transition with an input arc to the corresponding multiplicity
diff --git a/src/storm-gspn/storm-gspn.h b/src/storm-gspn/storm-gspn.h
new file mode 100644
index 000000000..63b0746f1
--- /dev/null
+++ b/src/storm-gspn/storm-gspn.h
@@ -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();
+ }
+
+
+
+ }
+
+}
\ No newline at end of file
diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp
index 7ba6cc09e..cfa8c66d1 100644
--- a/src/storm/cli/cli.cpp
+++ b/src/storm/cli/cli.cpp
@@ -12,7 +12,7 @@
#include "storm/settings/modules/JaniExportSettings.h"
#include "storm/utility/storm-version.h"
-#include "storm/storage/jani/JSONExporter.h"
+
// Includes for the linked libraries and versions header.
@@ -253,14 +253,7 @@ namespace storm {
}
if (model.isJaniModel() && storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isJaniFileSet()) {
- STORM_LOG_TRACE("Exporting JANI model.");
- if (storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isExportAsStandardJaniSet()) {
- storm::jani::Model normalisedModel = storm::jani::Model(model.asJaniModel());
- normalisedModel.makeStandardJaniCompliant();
- storm::jani::JsonExporter::toFile(normalisedModel, formulasInProperties(properties), storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
- } else {
- storm::jani::JsonExporter::toFile(model.asJaniModel(), formulasInProperties(properties), storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
- }
+ exportJaniModel(model.asJaniModel(), properties, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
}
if (ioSettings.isNoBuildModelSet()) {
diff --git a/src/storm/generator/NextStateGenerator.cpp b/src/storm/generator/NextStateGenerator.cpp
index 588edb70a..7f931051f 100644
--- a/src/storm/generator/NextStateGenerator.cpp
+++ b/src/storm/generator/NextStateGenerator.cpp
@@ -119,7 +119,7 @@ namespace storm {
result.getChoices().front().add(choice);
// Swap the choice to the end to indicate it can be removed (if it's not already there).
- if (index != result.getNumberOfChoices() - 1) {
+ if (index != result.getNumberOfChoices() - 1 - numberOfChoicesToDelete) {
choice = std::move(result.getChoices()[result.getNumberOfChoices() - 1 - numberOfChoicesToDelete]);
}
++numberOfChoicesToDelete;
diff --git a/src/storm/settings/modules/GSPNExportSettings.cpp b/src/storm/settings/modules/GSPNExportSettings.cpp
index 9be15c75e..8a5c315dc 100644
--- a/src/storm/settings/modules/GSPNExportSettings.cpp
+++ b/src/storm/settings/modules/GSPNExportSettings.cpp
@@ -19,6 +19,8 @@ namespace storm {
const std::string GSPNExportSettings::writeToPnmlOptionName = "to-pnml";
const std::string GSPNExportSettings::writeToPnproOptionName = "to-pnpro";
+ const std::string GSPNExportSettings::writeStatsOptionName = "to-stats";
+ const std::string GSPNExportSettings::displayStatsOptionName = "show-stats";
//const std::string GSPNExportSettings::janiFileOptionShortName = "dotoutput";
@@ -27,6 +29,8 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, writeToDotOptionName, false, "Destination for the dot output.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, writeToPnmlOptionName, false, "Destination for the pnml output").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, writeToPnproOptionName, false, "Destination for the pnpro output").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, writeStatsOptionName, false, "Destination for the stats file").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, displayStatsOptionName, false, "Print stats to stdout").build());
}
bool GSPNExportSettings::isWriteToDotSet() const {
@@ -54,6 +58,18 @@ namespace storm {
}
+ bool GSPNExportSettings::isDisplayStatsSet() const {
+ return this->getOption(displayStatsOptionName).getHasOptionBeenSet();
+ }
+
+ bool GSPNExportSettings::isWriteStatsToFileSet() const {
+ return this->getOption(writeStatsOptionName).getHasOptionBeenSet();
+ }
+
+ std::string GSPNExportSettings::getWriteStatsFilename() const {
+ return this->getOption(writeStatsOptionName).getArgumentByName("filename").getValueAsString();
+ }
+
void GSPNExportSettings::finalize() {
}
diff --git a/src/storm/settings/modules/GSPNExportSettings.h b/src/storm/settings/modules/GSPNExportSettings.h
index 3db836cf7..554cce223 100644
--- a/src/storm/settings/modules/GSPNExportSettings.h
+++ b/src/storm/settings/modules/GSPNExportSettings.h
@@ -15,7 +15,7 @@ namespace storm {
GSPNExportSettings();
/**
- * Retrievew whether the pgcl file option was set
+ * Retrieve whether the pgcl file option was set
*/
bool isWriteToDotSet() const;
@@ -38,6 +38,12 @@ namespace storm {
*/
std::string getWriteToPnproFilename() const;
+ bool isDisplayStatsSet() const;
+
+ bool isWriteStatsToFileSet() const;
+
+ std::string getWriteStatsFilename() const;
+
bool check() const override;
void finalize() override;
@@ -48,6 +54,9 @@ namespace storm {
static const std::string writeToDotOptionName;
static const std::string writeToPnmlOptionName;
static const std::string writeToPnproOptionName;
+ static const std::string displayStatsOptionName;
+ static const std::string writeStatsOptionName;
+
//static const std::string writeToDotOptionShortName;
};
diff --git a/src/storm/storage/BitVector.cpp b/src/storm/storage/BitVector.cpp
index 89113d718..a0004263a 100644
--- a/src/storm/storage/BitVector.cpp
+++ b/src/storm/storage/BitVector.cpp
@@ -486,7 +486,7 @@ namespace storm {
void BitVector::setFromInt(uint_fast64_t bitIndex, uint_fast64_t numberOfBits, uint64_t value) {
STORM_LOG_ASSERT(numberOfBits <= 64, "Number of bits must be <= 64.");
- STORM_LOG_ASSERT(numberOfBits == 64 || (value >> numberOfBits) == 0, "Integer value too large to fit in the given number of bits.");
+ STORM_LOG_ASSERT(numberOfBits == 64 || (value >> numberOfBits) == 0, "Integer value ("<< value << ") too large to fit in the given number of bits (" << numberOfBits << ").");
uint64_t bucket = bitIndex >> 6;
uint64_t bitIndexInBucket = bitIndex & mod64mask;
diff --git a/src/storm/storage/expressions/Expression.cpp b/src/storm/storage/expressions/Expression.cpp
index 9dbd46986..c9ca8a320 100644
--- a/src/storm/storage/expressions/Expression.cpp
+++ b/src/storm/storage/expressions/Expression.cpp
@@ -235,6 +235,12 @@ namespace storm {
Expression operator&&(Expression const& first, Expression const& second) {
assertSameManager(first.getBaseExpression(), second.getBaseExpression());
+ if (first.isTrue()) {
+ return second;
+ }
+ if (second.isTrue()) {
+ return first;
+ }
return Expression(std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(first.getBaseExpression().getManager(), first.getType().logicalConnective(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryBooleanFunctionExpression::OperatorType::And)));
}
diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp
index 7548fd323..889496265 100644
--- a/src/storm/storage/jani/JSONExporter.cpp
+++ b/src/storm/storage/jani/JSONExporter.cpp
@@ -516,7 +516,7 @@ namespace storm {
- void JsonExporter::toFile(storm::jani::Model const& janiModel, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::string const& filepath, bool checkValid) {
+ void JsonExporter::toFile(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::string const& filepath, bool checkValid) {
std::ofstream ofs;
ofs.open (filepath, std::ofstream::out );
if(ofs.is_open()) {
@@ -526,7 +526,7 @@ namespace storm {
}
}
- void JsonExporter::toStream(storm::jani::Model const& janiModel, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::ostream& os, bool checkValid) {
+ void JsonExporter::toStream(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::ostream& os, bool checkValid) {
if(checkValid) {
janiModel.checkValid();
}
@@ -759,13 +759,13 @@ namespace storm {
}
- void JsonExporter::convertProperties( std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::jani::Model const& model) {
+ void JsonExporter::convertProperties( std::vector<storm::jani::Property> const& formulas, storm::jani::Model const& model) {
std::vector<modernjson::json> properties;
uint64_t index = 0;
for(auto const& f : formulas) {
modernjson::json propDecl;
- propDecl["name"] = "prop" + std::to_string(index);
- propDecl["expression"] = convertFilterExpression(storm::jani::FilterExpression(f), model);
+ propDecl["name"] = f.getName();
+ propDecl["expression"] = convertFilterExpression(f.getFilter(), model);
++index;
properties.push_back(propDecl);
}
diff --git a/src/storm/storage/jani/JSONExporter.h b/src/storm/storage/jani/JSONExporter.h
index 1008ec097..1eceb5d2e 100644
--- a/src/storm/storage/jani/JSONExporter.h
+++ b/src/storm/storage/jani/JSONExporter.h
@@ -4,6 +4,7 @@
#include "storm/storage/expressions/ExpressionVisitor.h"
#include "storm/logic/FormulaVisitor.h"
#include "Model.h"
+#include "storm/storage/jani/Property.h"
#include "storm/adapters/NumberAdapter.h"
// JSON parser
#include "json.hpp"
@@ -66,12 +67,13 @@ namespace storm {
JsonExporter() = default;
public:
- static void toFile(storm::jani::Model const& janiModel, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::string const& filepath, bool checkValid = true);
- static void toStream(storm::jani::Model const& janiModel, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::ostream& ostream, bool checkValid = false);
+ static void toFile(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::string const& filepath, bool checkValid = true);
+ static void toStream(storm::jani::Model const& janiModel, std::vector<storm::jani::Property> const& formulas, std::ostream& ostream, bool checkValid = false);
+
private:
void convertModel(storm::jani::Model const& model);
- void convertProperties(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::jani::Model const& model);
+ void convertProperties(std::vector<storm::jani::Property> const& formulas, storm::jani::Model const& model);
void appendVariableDeclaration(storm::jani::Variable const& variable);
modernjson::json finalize() {
diff --git a/src/storm/storage/jani/OrderedAssignments.cpp b/src/storm/storage/jani/OrderedAssignments.cpp
index 667952719..18f0aebae 100644
--- a/src/storm/storage/jani/OrderedAssignments.cpp
+++ b/src/storm/storage/jani/OrderedAssignments.cpp
@@ -141,5 +141,14 @@ namespace storm {
return std::lower_bound(assignments.begin(), assignments.end(), assignment, storm::jani::AssignmentPartialOrderByLevelAndVariable());
}
+ std::ostream& operator<<(std::ostream& stream, OrderedAssignments const& assignments) {
+ stream << "[";
+ for(auto const& e : assignments.allAssignments) {
+ stream << *e << std::endl;
+ }
+ stream << "]";
+ return stream;
+ }
+
}
}
diff --git a/src/storm/storage/jani/OrderedAssignments.h b/src/storm/storage/jani/OrderedAssignments.h
index 789b1014a..999b9d95f 100644
--- a/src/storm/storage/jani/OrderedAssignments.h
+++ b/src/storm/storage/jani/OrderedAssignments.h
@@ -109,6 +109,8 @@ namespace storm {
*/
void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
+ friend std::ostream& operator<<(std::ostream& stream, OrderedAssignments const& assignments);
+
private:
static std::vector<std::shared_ptr<Assignment>>::const_iterator lowerBound(Assignment const& assignment, std::vector<std::shared_ptr<Assignment>> const& assignments);
diff --git a/src/storm/utility/storm.cpp b/src/storm/utility/storm.cpp
index 40ab41b91..9a0e6faba 100644
--- a/src/storm/utility/storm.cpp
+++ b/src/storm/utility/storm.cpp
@@ -30,6 +30,17 @@ namespace storm{
modelAndFormulae.first.checkValid();
return modelAndFormulae;
}
+
+ void exportJaniModel(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::string const& filepath) {
+ STORM_LOG_TRACE("Exporting JANI model.");
+ if (storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isExportAsStandardJaniSet()) {
+ storm::jani::Model normalisedModel = model;
+ normalisedModel.makeStandardJaniCompliant();
+ storm::jani::JsonExporter::toFile(normalisedModel, properties, filepath);
+ } else {
+ storm::jani::JsonExporter::toFile(model, properties, filepath);
+ }
+ }
/**
* Helper
diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h
index cee49998b..343832e00 100644
--- a/src/storm/utility/storm.h
+++ b/src/storm/utility/storm.h
@@ -23,6 +23,7 @@
#include "storm/settings/modules/RegionSettings.h"
#include "storm/settings/modules/EliminationSettings.h"
#include "storm/settings/modules/JitBuilderSettings.h"
+#include "storm/settings/modules/JaniExportSettings.h"
// Formula headers.
#include "storm/logic/Formulas.h"
@@ -55,6 +56,7 @@
#include "storm/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h"
#include "storm/storage/ModelFormulasPair.h"
#include "storm/storage/SymbolicModelDescription.h"
+#include "storm/storage/jani/JSONExporter.h"
// Headers for model checking.
#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
@@ -225,6 +227,7 @@ namespace storm {
std::shared_ptr<storm::models::ModelBase> preprocessModel(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
if (model->getType() == storm::models::ModelType::MarkovAutomaton && model->isSparseModel()) {
std::shared_ptr<storm::models::sparse::MarkovAutomaton<typename ModelType::ValueType>> ma = model->template as<storm::models::sparse::MarkovAutomaton<typename ModelType::ValueType>>();
+ ma->close();
if (ma->hasOnlyTrivialNondeterminism()) {
// Markov automaton can be converted into CTMC.
model = ma->convertToCTMC();
@@ -575,7 +578,13 @@ namespace storm {
}
return result;
}
-
+
+
+ /**
+ *
+ */
+ void exportJaniModel(storm::jani::Model const& model, std::vector<storm::jani::Property> const& properties, std::string const& filepath);
+
template<typename ValueType>
void exportMatrixToFile(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::string const& filepath) {
STORM_LOG_THROW(model->getType() != storm::models::ModelType::Ctmc, storm::exceptions::NotImplementedException, "This functionality is not yet implemented." );