sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

More general method for building GSPN-Jani properties

main
Matthias Volk 7 years ago
parent
cbd3880d87
commit
8c2a44494b
3 changed files with 59 additions and 49 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 11
      src/storm-gspn/api/storm-gspn.cpp
  2. 80
      src/storm-gspn/builder/JaniGSPNBuilder.cpp
  3. 17
      src/storm-gspn/builder/JaniGSPNBuilder.h

11
src/storm-gspn/api/storm-gspn.cpp
View File

@ -58,19 +58,20 @@ namespace storm {
gspn.writeStatsToStream(fs);
storm::utility::closeFile(fs);
}
if (exportSettings.isWriteToJaniSet()) {
auto const& jani = storm::settings::getModule<storm::settings::modules::JaniExportSettings>();
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;

80
src/storm-gspn/builder/JaniGSPNBuilder.cpp
View File

@ -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<storm::jani::Property> 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<storm::gspn::Transition const*> 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<storm::logic::AtomicExpressionFormula>(deadlockVar.getExpressionVariable().getExpression());
auto trueFormula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
auto maxReachDeadlock = std::make_shared<storm::logic::ProbabilityOperatorFormula>(
std::make_shared<storm::logic::EventuallyFormula>(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<storm::jani::Property> const& JaniGSPNBuilder::getStandardProperties(storm::jani::Model* model, std::shared_ptr<storm::logic::AtomicExpressionFormula> atomicFormula, std::string name, std::string description, bool maximal) {
std::vector<storm::jani::Property> 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<storm::logic::ProbabilityOperatorFormula>(
std::make_shared<storm::logic::EventuallyFormula>(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<storm::logic::ProbabilityOperatorFormula>(
std::make_shared<storm::logic::BoundedUntilFormula>(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<storm::logic::TimeOperatorFormula>(
std::make_shared<storm::logic::EventuallyFormula>(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<storm::logic::BooleanLiteralFormula>(true);
auto reachTimeBoundFormula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(
std::make_shared<storm::logic::BoundedUntilFormula>(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<storm::logic::TimeOperatorFormula>(
std::make_shared<storm::logic::EventuallyFormula>(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<storm::jani::Property> const& JaniGSPNBuilder::getDeadlockProperties(storm::jani::Model* model) {
auto const& deadlockVar = addDeadlockTransientVariable(model, getUniqueVarName(*expressionManager, "deadl"));
auto deadlockFormula = std::make_shared<storm::logic::AtomicExpressionFormula>(deadlockVar.getExpressionVariable().getExpression());
return getStandardProperties(model, deadlockFormula, "Deadlock", "a deadlock", true);
}
}
}

17
src/storm-gspn/builder/JaniGSPNBuilder.h
View File

@ -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<storm::jani::Property> const& getStandardProperties() const;
/*!
* Get standard properties (reachability, time bounded reachability, expected time) for a given atomic formula.
*/
std::vector<storm::jani::Property> const& getStandardProperties(storm::jani::Model* model, std::shared_ptr<storm::logic::AtomicExpressionFormula> atomicFormula, std::string name, std::string description, bool maximal);
/*!
* Get standard properties (reachability, time bounded reachability, expected time) for deadlocks.
*/
std::vector<storm::jani::Property> 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<uint64_t, storm::jani::Variable const*> vars;
std::shared_ptr<storm::expressions::ExpressionManager> expressionManager;
std::vector<storm::jani::Property> standardProperties;
};
}
}
Write Preview
Loading…
Cancel
Save