diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp
index 8ccdc12be..6c54dc226 100644
--- a/src/storm-dft-cli/storm-dyftee.cpp
+++ b/src/storm-dft-cli/storm-dyftee.cpp
@@ -4,6 +4,7 @@
#include "storm/cli/cli.h"
#include "storm/exceptions/BaseException.h"
+#include "storm/logic/Formula.h"
#include "storm/settings/modules/GeneralSettings.h"
#include "storm/settings/modules/CoreSettings.h"
@@ -71,20 +72,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);
- storm::transformations::dft::DftToGspnTransformator<ValueType> gspnTransformator(dft);
- gspnTransformator.transform();
- return gspnTransformator.obtainGSPN();
-}
/*!
* Initialize the settings manager.
@@ -140,15 +127,30 @@ int main(const int argc, const char** argv) {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
}
+
if (dftSettings.isTransformToGspn()) {
- storm::gspn::GSPN* gspn = transformDFT<double>(dftSettings.getDftFilename());
+
+ storm::parser::DFTGalileoParser<double> parser;
+ storm::storage::DFT<double> dft = 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);
- storm::jani::Model* model = storm::buildJani(*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);
+
+
+ auto evtlFormula = std::make_shared<storm::logic::AtomicExpressionFormula>(exprManager->integer(1) == topfailedVar.getExpressionVariable().getExpression());
+ 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);
storm::settings::modules::JaniExportSettings const& janiSettings = storm::settings::getModule<storm::settings::modules::JaniExportSettings>();
if (janiSettings.isJaniFileSet()) {
- storm::exportJaniModel(*model, {}, janiSettings.getJaniFilename());
+ storm::exportJaniModel(*model, {storm::jani::Property("time-bounded", tbUntil)}, janiSettings.getJaniFilename());
}
delete model;
diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp
index 5649754cd..355c6f440 100644
--- a/src/storm-dft/transformations/DftToGspnTransformator.cpp
+++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp
@@ -8,7 +8,7 @@ namespace storm {
// Prevent some magic constants
static constexpr const uint64_t defaultPriority = 0;
- static constexpr const uint64_t defaultCapacity = 0;
+ static constexpr const uint64_t defaultCapacity = 1;
template <typename ValueType>
DftToGspnTransformator<ValueType>::DftToGspnTransformator(storm::storage::DFT<ValueType> const& dft) : mDft(dft) {
@@ -27,6 +27,12 @@ namespace storm {
//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() {
@@ -133,6 +139,7 @@ namespace storm {
for(auto const& child : dftAnd->children()) {
assert(failedNodes.size() > child->id());
builder.addInputArc(failedNodes[child->id()], tAndFailed);
+ builder.addOutputArc(tAndFailed, failedNodes[child->id()]);
}
}
@@ -157,6 +164,7 @@ namespace storm {
}
assert(failedNodes.size() > child->id());
builder.addInputArc(failedNodes[child->id()], tNodeFailed);
+ builder.addOutputArc(tNodeFailed, failedNodes[child->id()]);
++i;
}
}
@@ -188,6 +196,7 @@ namespace storm {
builder.addOutputArc(tCollect, childInhibPlace);
builder.addInhibitionArc(childInhibPlace, tCollect);
builder.addInputArc(failedNodes[child->id()], tCollect);
+ builder.addOutputArc(tCollect, failedNodes[child->id()]);
++i;
}
}
@@ -212,12 +221,15 @@ namespace storm {
}
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.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);
}
}
diff --git a/src/storm-dft/transformations/DftToGspnTransformator.h b/src/storm-dft/transformations/DftToGspnTransformator.h
index e2812f738..2d763452d 100644
--- a/src/storm-dft/transformations/DftToGspnTransformator.h
+++ b/src/storm-dft/transformations/DftToGspnTransformator.h
@@ -33,6 +33,9 @@ namespace storm {
*/
gspn::GSPN* obtainGSPN();
+
+ uint64_t toplevelFailedPlaceId();
+
private:
/*
* Draw all elements of the GSPN.
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 305fa0129..196d29562 100644
--- a/src/storm-gspn/builder/JaniGSPNBuilder.h
+++ b/src/storm-gspn/builder/JaniGSPNBuilder.h
@@ -16,10 +16,6 @@ namespace storm {
}
- void setIgnoreWeights(bool ignore = true) {
- //ignoreWeights = ignore;
- }
-
storm::jani::Model* build() {
storm::jani::Model* model = new storm::jani::Model(gspn.getName(), storm::jani::ModelType::MA, janiVersion, expressionManager);
@@ -32,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;
@@ -86,7 +86,7 @@ namespace storm {
destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() >= inPlaceEntry.second);
}
for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) {
- destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() >= inhibPlaceEntry.second);
+ destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() < inhibPlaceEntry.second);
}
totalWeight = totalWeight + storm::expressions::ite(destguard, expressionManager->rational(trans.getWeight()), expressionManager->rational(0.0));
@@ -103,13 +103,13 @@ namespace storm {
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);
+ 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);
}
}
for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) {
- destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() > inhibPlaceEntry.second);
+ destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() < inhibPlaceEntry.second);
}
for (auto const& outputPlaceEntry : trans.getOutputPlaces()) {
if (trans.getInputPlaces().count(outputPlaceEntry.first) == 0) {
@@ -140,7 +140,7 @@ namespace storm {
}
}
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()) {
if (trans.getInputPlaces().count(outputPlaceEntry.first) == 0) {
diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h
index 6657a7d6d..343832e00 100644
--- a/src/storm/utility/storm.h
+++ b/src/storm/utility/storm.h
@@ -227,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();