diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp index 74750c350..ad32f6231 100644 --- a/src/storm-dft/api/storm-dft.cpp +++ b/src/storm-dft/api/storm-dft.cpp @@ -74,6 +74,7 @@ namespace storm { std::shared_ptr const& exprManager = gspn.getExpressionManager(); storm::jani::Variable const& topfailedVar = builder.getPlaceVariable(toplevelFailedPlace); storm::expressions::Expression targetExpression = exprManager->integer(1) == topfailedVar.getExpressionVariable().getExpression(); + storm::jani::Variable const& failedVar = builder.addTransientVariable(model.get(), "failed", targetExpression); STORM_LOG_TRACE("Target expression: " << targetExpression); auto evtlFormula = std::make_shared(targetExpression); diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.cpp b/src/storm-gspn/builder/JaniGSPNBuilder.cpp index 744b76eb4..00a75a83d 100644 --- a/src/storm-gspn/builder/JaniGSPNBuilder.cpp +++ b/src/storm-gspn/builder/JaniGSPNBuilder.cpp @@ -252,15 +252,18 @@ namespace storm { transientValue = transientValue && transitionDisabled; } } - + + return addTransientVariable(model, name, transientValue); + } + + storm::jani::Variable const& JaniGSPNBuilder::addTransientVariable(storm::jani::Model* model, std::string name, storm::expressions::Expression expression) { auto exprVar = expressionManager->declareBooleanVariable(name); auto const& janiVar = model->addVariable(*storm::jani::makeBooleanVariable(name, exprVar, expressionManager->boolean(false), true)); - storm::jani::Assignment assignment(janiVar, transientValue); + storm::jani::Assignment assignment(janiVar, expression); model->getAutomata().front().getLocations().front().addTransientAssignment(assignment); return janiVar; } - - + std::string getUniqueVarName(storm::expressions::ExpressionManager const& manager, std::string name) { std::string res = name; while (manager.hasVariable(res)) { @@ -300,4 +303,4 @@ namespace storm { } -} \ No newline at end of file +} diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.h b/src/storm-gspn/builder/JaniGSPNBuilder.h index 205f248e1..86d140c73 100644 --- a/src/storm-gspn/builder/JaniGSPNBuilder.h +++ b/src/storm-gspn/builder/JaniGSPNBuilder.h @@ -11,23 +11,26 @@ namespace storm { public: JaniGSPNBuilder(storm::gspn::GSPN const& gspn) : gspn(gspn), expressionManager(gspn.getExpressionManager()) { - + } - + virtual ~JaniGSPNBuilder() { // Intentionally left empty. } - - + storm::jani::Model* build(std::string const& automatonName = "gspn_automaton", bool buildStandardProperties = false); - + storm::jani::Variable const& getPlaceVariable(uint64_t placeId) const { return *vars.at(placeId); } - + std::vector const& getStandardProperties() const; - + /*! + * Add transient variable representing given expression. + */ + storm::jani::Variable const& addTransientVariable(storm::jani::Model* model, std::string name, storm::expressions::Expression expression); + private: void addVariables(storm::jani::Model* model); @@ -36,15 +39,16 @@ namespace storm { void addEdges(storm::jani::Automaton& automaton, uint64_t locId); storm::jani::Variable const& addDeadlockTransientVariable(storm::jani::Model* model, std::string name, bool ignoreCapacities = false, bool ignoreInhibitorArcs = false, bool ignoreEmptyPlaces = false); + void buildProperties(storm::jani::Model* model); - + const uint64_t janiVersion = 1; storm::gspn::GSPN const& gspn; std::map vars; std::shared_ptr expressionManager; - + std::vector standardProperties; - + }; } }