diff --git a/src/storm-gspn/api/storm-gspn.cpp b/src/storm-gspn/api/storm-gspn.cpp index 63da78250..8cbe42d3a 100644 --- a/src/storm-gspn/api/storm-gspn.cpp +++ b/src/storm-gspn/api/storm-gspn.cpp @@ -58,19 +58,20 @@ namespace storm { gspn.writeStatsToStream(fs); storm::utility::closeFile(fs); } - + if (exportSettings.isWriteToJaniSet()) { auto const& jani = storm::settings::getModule(); storm::converter::JaniConversionOptions options(jani); - + storm::builder::JaniGSPNBuilder builder(gspn); - storm::jani::Model* model = builder.build("gspn_automaton", exportSettings.isAddJaniPropertiesSet()); + storm::jani::Model* model = builder.build("gspn_automaton"); storm::api::postprocessJani(*model, options); - + auto properties = janiProperyGetter(builder); if (exportSettings.isAddJaniPropertiesSet()) { - properties.insert(properties.end(), builder.getStandardProperties().begin(), builder.getStandardProperties().end()); + auto deadlockProperties = builder.getDeadlockProperties(model); + properties.insert(properties.end(), deadlockProperties.begin(), deadlockProperties.end()); } storm::api::exportJaniToFile(*model, properties, exportSettings.getWriteToJaniFilename(), jani.isCompactJsonSet()); delete model; diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.cpp b/src/storm-gspn/builder/JaniGSPNBuilder.cpp index 00a75a83d..6eedf8458 100644 --- a/src/storm-gspn/builder/JaniGSPNBuilder.cpp +++ b/src/storm-gspn/builder/JaniGSPNBuilder.cpp @@ -8,7 +8,7 @@ namespace storm { namespace builder { - storm::jani::Model* JaniGSPNBuilder::build(std::string const& automatonName, bool buildStandardProperties) { + storm::jani::Model* JaniGSPNBuilder::build(std::string const& automatonName) { storm::jani::ModelType modelType = storm::jani::ModelType::MA; if (gspn.getNumberOfTimedTransitions() == 0) { storm::jani::ModelType modelType = storm::jani::ModelType::MDP; @@ -22,15 +22,8 @@ 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()) { @@ -188,11 +181,10 @@ 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()); @@ -204,7 +196,7 @@ namespace storm { } 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; @@ -244,7 +236,7 @@ namespace storm { } } } - + if (firstTransition) { transientValue = transitionDisabled; firstTransition = false; @@ -271,36 +263,50 @@ namespace storm { } 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."); - + + std::vector const& JaniGSPNBuilder::getStandardProperties(storm::jani::Model* model, std::shared_ptr atomicFormula, std::string name, std::string description, bool maximal) { + std::vector standardProperties; + std::string dirShort = maximal ? "Max" : "Min"; + std::string dirLong = maximal ? "maximal" : "minimal"; + storm::solver::OptimizationDirection optimizationDirection = maximal ? storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize; + + // Build reachability property + auto reachFormula = std::make_shared( + std::make_shared(atomicFormula, storm::logic::FormulaContext::Probability), + storm::logic::OperatorInformation(optimizationDirection)); + standardProperties.emplace_back(dirShort + "PrReach" + name, reachFormula, "The " + dirLong + " probability to eventually reach " + description + "."); + + // Build time bounded reachability property + // Add variable for time bound auto exprTB = expressionManager->declareRationalVariable(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."); - + + auto trueFormula = std::make_shared(true); + auto reachTimeBoundFormula = std::make_shared( + std::make_shared(trueFormula, atomicFormula, boost::none, tb, tbr), + storm::logic::OperatorInformation(optimizationDirection)); + standardProperties.emplace_back(dirShort + "PrReach" + name + "TB", reachTimeBoundFormula, "The " + dirLong + " probability to reach " + description + " within 'TIME_BOUND' steps."); + + // Use complementary direction for expected time + dirShort = maximal ? "Min" : "Max"; + dirLong = maximal ? "minimal" : "maximal"; + optimizationDirection = maximal ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize; + + // Build expected time property + auto expTimeFormula = std::make_shared( + std::make_shared(atomicFormula, storm::logic::FormulaContext::Time), + storm::logic::OperatorInformation(optimizationDirection)); + standardProperties.emplace_back(dirShort + "ExpTime" + name, expTimeFormula, "The " + dirLong + " expected time to reach " + description + "."); + } + + std::vector const& JaniGSPNBuilder::getDeadlockProperties(storm::jani::Model* model) { + auto const& deadlockVar = addDeadlockTransientVariable(model, getUniqueVarName(*expressionManager, "deadl")); + auto deadlockFormula = std::make_shared(deadlockVar.getExpressionVariable().getExpression()); + return getStandardProperties(model, deadlockFormula, "Deadlock", "a deadlock", true); } - } } diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.h b/src/storm-gspn/builder/JaniGSPNBuilder.h index 86d140c73..8a5d07405 100644 --- a/src/storm-gspn/builder/JaniGSPNBuilder.h +++ b/src/storm-gspn/builder/JaniGSPNBuilder.h @@ -18,13 +18,21 @@ namespace storm { // Intentionally left empty. } - storm::jani::Model* build(std::string const& automatonName = "gspn_automaton", bool buildStandardProperties = false); + storm::jani::Model* build(std::string const& automatonName = "gspn_automaton"); storm::jani::Variable const& getPlaceVariable(uint64_t placeId) const { return *vars.at(placeId); } - std::vector const& getStandardProperties() const; + /*! + * Get standard properties (reachability, time bounded reachability, expected time) for a given atomic formula. + */ + std::vector const& getStandardProperties(storm::jani::Model* model, std::shared_ptr atomicFormula, std::string name, std::string description, bool maximal); + + /*! + * Get standard properties (reachability, time bounded reachability, expected time) for deadlocks. + */ + std::vector const& getDeadlockProperties(storm::jani::Model* model); /*! * Add transient variable representing given expression. @@ -40,15 +48,10 @@ namespace storm { 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; - }; } }