diff --git a/src/storm-gspn-cli/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp index 70272e5b2..6b9c5e2ee 100644 --- a/src/storm-gspn-cli/storm-gspn.cpp +++ b/src/storm-gspn-cli/storm-gspn.cpp @@ -86,14 +86,16 @@ int main(const int argc, const char **argv) { if (!optionsCorrect) { return -1; } + + auto gspnSettings = storm::settings::getModule(); // parse gspn from file - if (!storm::settings::getModule().isGspnFileSet()) { + if (!gspnSettings.isGspnFileSet()) { return -1; } auto parser = storm::parser::GspnParser(); - auto gspn = parser.parse(storm::settings::getModule().getGspnFilename()); + auto gspn = parser.parse(gspnSettings.getGspnFilename()); std::string formulaString = ""; if (storm::settings::getModule().isPropertySet()) { @@ -107,11 +109,11 @@ int main(const int argc, const char **argv) { STORM_LOG_ERROR("The gspn is not valid."); } - if(storm::settings::getModule().isCapacitiesFileSet()) { - auto capacities = parseCapacitiesList(storm::settings::getModule().getCapacitiesFilename()); + if(gspnSettings.isCapacitiesFileSet()) { + auto capacities = parseCapacitiesList(gspnSettings.getCapacitiesFilename()); gspn->setCapacities(capacities); - } else if (storm::settings::getModule().isCapacitySet()) { - uint64_t capacity = storm::settings::getModule().getCapacity(); + } else if (gspnSettings.isCapacitySet()) { + uint64_t capacity = gspnSettings.getCapacity(); std::unordered_map capacities; for (auto const& place : gspn->getPlaces()) { capacities.emplace(place.getName(), capacity); diff --git a/src/storm-gspn/api/storm-gspn.cpp b/src/storm-gspn/api/storm-gspn.cpp index 45e579db1..b972b474c 100644 --- a/src/storm-gspn/api/storm-gspn.cpp +++ b/src/storm-gspn/api/storm-gspn.cpp @@ -63,10 +63,15 @@ namespace storm { storm::converter::JaniConversionOptions options(jani); storm::builder::JaniGSPNBuilder builder(gspn); - storm::jani::Model* model = builder.build(); + storm::jani::Model* model = builder.build("gspn_automaton", exportSettings.isAddJaniPropertiesSet()); storm::api::postprocessJani(*model, options); - storm::api::exportJaniToFile(*model, janiProperyGetter(builder), storm::settings::getModule().getWriteToJaniFilename()); + + auto properties = janiProperyGetter(builder); + if (exportSettings.isAddJaniPropertiesSet()) { + properties.insert(properties.end(), builder.getStandardProperties().begin(), builder.getStandardProperties().end()); + } + storm::api::exportJaniToFile(*model, properties, exportSettings.getWriteToJaniFilename()); delete model; } } diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.cpp b/src/storm-gspn/builder/JaniGSPNBuilder.cpp index cd81bb266..45a2a5ebc 100644 --- a/src/storm-gspn/builder/JaniGSPNBuilder.cpp +++ b/src/storm-gspn/builder/JaniGSPNBuilder.cpp @@ -1,9 +1,12 @@ #include "JaniGSPNBuilder.h" +#include + +#include "storm/logic/Formulas.h" namespace storm { namespace builder { - storm::jani::Model* JaniGSPNBuilder::build(std::string const& automatonName) { + storm::jani::Model* JaniGSPNBuilder::build(std::string const& automatonName, bool buildStandardProperties) { storm::jani::Model* model = new storm::jani::Model(gspn.getName(), storm::jani::ModelType::MA, janiVersion, expressionManager); storm::jani::Automaton mainAutomaton(automatonName, expressionManager->declareIntegerVariable("loc")); addVariables(model); @@ -11,8 +14,15 @@ namespace storm { addEdges(mainAutomaton, locId); model->addAutomaton(mainAutomaton); model->setStandardSystemComposition(); + if (buildStandardProperties) { + buildProperties(model); + } return model; } + + std::vector const& JaniGSPNBuilder::getStandardProperties() const { + return standardProperties; + } void JaniGSPNBuilder::addVariables(storm::jani::Model* model) { for (auto const& place : gspn.getPlaces()) { @@ -150,5 +160,116 @@ namespace storm { } } + + storm::jani::Variable const& JaniGSPNBuilder::addDeadlockTransientVariable(storm::jani::Model* model, std::string name, bool ignoreCapacities, bool ignoreInhibitorArcs, bool ignoreEmptyPlaces) { + + storm::expressions::Expression transientValue = expressionManager->boolean(true); + + // build the conjunction over all transitions + std::vector transitions; + transitions.reserve(gspn.getNumberOfImmediateTransitions() + gspn.getNumberOfTimedTransitions()); + for (auto const& t : gspn.getImmediateTransitions()) { + transitions.push_back(&t); + } + for (auto const& t : gspn.getTimedTransitions()) { + transitions.push_back(&t); + } + bool firstTransition = true; + for (auto const& transition : transitions) { + + // build the disjunction over all in/out places and inhibitor arcs + storm::expressions::Expression transitionDisabled = expressionManager->boolean(false); + bool firstPlace = true; + if (!ignoreEmptyPlaces) { + for (auto const& placeIdMult : transition->getInputPlaces()) { + storm::expressions::Expression placeBlocksTransition = (vars.at(placeIdMult.first)->getExpressionVariable() < expressionManager->integer(placeIdMult.second)); + if (firstPlace) { + transitionDisabled = placeBlocksTransition; + firstPlace = false; + } else { + transitionDisabled = transitionDisabled || placeBlocksTransition; + } + } + } + if (!ignoreInhibitorArcs) { + for (auto const& placeIdMult : transition->getInhibitionPlaces()) { + storm::expressions::Expression placeBlocksTransition = (vars.at(placeIdMult.first)->getExpressionVariable() >= expressionManager->integer(placeIdMult.second)); + if (firstPlace) { + transitionDisabled = placeBlocksTransition; + firstPlace = false; + } else { + transitionDisabled = transitionDisabled || placeBlocksTransition; + } + } + } + if (!ignoreCapacities) { + for (auto const& placeIdMult : transition->getOutputPlaces()) { + auto const& place = gspn.getPlace(placeIdMult.first); + if (place->hasRestrictedCapacity()) { + storm::expressions::Expression placeBlocksTransition = (vars.at(placeIdMult.first)->getExpressionVariable() + expressionManager->integer(placeIdMult.second) > expressionManager->integer(place->getCapacity())); + if (firstPlace) { + transitionDisabled = placeBlocksTransition; + firstPlace = false; + } else { + transitionDisabled = transitionDisabled || placeBlocksTransition; + } + } + } + } + + if (firstTransition) { + transientValue = transitionDisabled; + firstTransition = false; + } else { + transientValue = transientValue && transitionDisabled; + } + } + + 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); + 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)) { + res.append("_"); + } + return res; + } + + void JaniGSPNBuilder::buildProperties(storm::jani::Model* model) { + standardProperties.clear(); + + auto const& deadlockVar = addDeadlockTransientVariable(model, getUniqueVarName(*expressionManager, "deadl")); + auto deadlock = std::make_shared(deadlockVar.getExpressionVariable().getExpression()); + auto trueFormula = std::make_shared(true); + + auto maxReachDeadlock = std::make_shared( + std::make_shared(deadlock, storm::logic::FormulaContext::Probability), + storm::logic::OperatorInformation(storm::solver::OptimizationDirection::Maximize)); + standardProperties.emplace_back("MaxPrReachDeadlock", maxReachDeadlock, "The maximal probability to eventually reach a deadlock."); + + auto exprTB = expressionManager->declareIntegerVariable(getUniqueVarName(*expressionManager, "TIME_BOUND")); + auto janiTB = storm::jani::Constant(exprTB.getName(), exprTB); + model->addConstant(janiTB); + storm::logic::TimeBound tb(false, janiTB.getExpressionVariable().getExpression()); + storm::logic::TimeBoundReference tbr(storm::logic::TimeBoundType::Time); + auto maxReachDeadlockTimeBounded = std::make_shared( + std::make_shared(trueFormula, deadlock, boost::none, tb, tbr), + storm::logic::OperatorInformation(storm::solver::OptimizationDirection::Maximize)); + standardProperties.emplace_back("MaxPrReachDeadlockTB", maxReachDeadlockTimeBounded, "The maximal probability to reach a deadlock within 'TIME_BOUND' steps."); + + auto expTimeDeadlock = std::make_shared( + std::make_shared(deadlock, storm::logic::FormulaContext::Time), + storm::logic::OperatorInformation(storm::solver::OptimizationDirection::Maximize)); + standardProperties.emplace_back("MinExpTimeDeadlock", expTimeDeadlock, "The minimal expected time to reach a deadlock."); + + } + + } } \ No newline at end of file diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.h b/src/storm-gspn/builder/JaniGSPNBuilder.h index db890e36c..205f248e1 100644 --- a/src/storm-gspn/builder/JaniGSPNBuilder.h +++ b/src/storm-gspn/builder/JaniGSPNBuilder.h @@ -19,11 +19,13 @@ namespace storm { } - storm::jani::Model* build(std::string const& automatonName = "gspn_automaton"); + 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; private: @@ -33,11 +35,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; + }; } } diff --git a/src/storm-gspn/settings/modules/GSPNExportSettings.cpp b/src/storm-gspn/settings/modules/GSPNExportSettings.cpp index 295f963e2..895866cdf 100644 --- a/src/storm-gspn/settings/modules/GSPNExportSettings.cpp +++ b/src/storm-gspn/settings/modules/GSPNExportSettings.cpp @@ -20,6 +20,7 @@ namespace storm { const std::string GSPNExportSettings::writeToPnproOptionName = "to-pnpro"; const std::string GSPNExportSettings::writeToJsonOptionName = "to-json"; const std::string GSPNExportSettings::writeToJaniOptionName = "to-jani"; + const std::string GSPNExportSettings::addJaniPropertiesOptionName = "addprops"; const std::string GSPNExportSettings::writeStatsOptionName = "to-stats"; const std::string GSPNExportSettings::displayStatsOptionName = "show-stats"; @@ -32,6 +33,7 @@ namespace storm { 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, writeToJsonOptionName, false, "Destination for the json output").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, writeToJaniOptionName, false, "Destination for the jani output").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, addJaniPropertiesOptionName, false, "If set, a set of standard properties is added to the exported jani model.").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()); } @@ -76,6 +78,10 @@ namespace storm { return this->getOption(writeToJaniOptionName).getArgumentByName("filename").getValueAsString(); } + bool GSPNExportSettings::isAddJaniPropertiesSet() const { + return this->getOption(addJaniPropertiesOptionName).getHasOptionBeenSet(); + } + bool GSPNExportSettings::isDisplayStatsSet() const { return this->getOption(displayStatsOptionName).getHasOptionBeenSet(); } diff --git a/src/storm-gspn/settings/modules/GSPNExportSettings.h b/src/storm-gspn/settings/modules/GSPNExportSettings.h index fbe45a4eb..5ebb3ac5a 100644 --- a/src/storm-gspn/settings/modules/GSPNExportSettings.h +++ b/src/storm-gspn/settings/modules/GSPNExportSettings.h @@ -53,6 +53,11 @@ namespace storm { */ std::string getWriteToJaniFilename() const; + /*! + * Returns whether a set of standard properties is to be added when exporting to jani + */ + bool isAddJaniPropertiesSet() const; + bool isDisplayStatsSet() const; bool isWriteStatsToFileSet() const; @@ -71,6 +76,7 @@ namespace storm { static const std::string writeToPnproOptionName; static const std::string writeToJsonOptionName; static const std::string writeToJaniOptionName; + static const std::string addJaniPropertiesOptionName; static const std::string displayStatsOptionName; static const std::string writeStatsOptionName;