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

Incorporated more features for the portfolio engine.

tempestpy_adaptions
Tim Quatmann 5 years ago
parent
3b53e1e583
commit
f4820628a5
3 changed files with 58 additions and 6 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. 14
      src/storm/storage/jani/traverser/InformationCollector.cpp
  2. 2
      src/storm/storage/jani/traverser/InformationCollector.h
  3. 48
      src/storm/utility/Portfolio.cpp

14
src/storm/storage/jani/traverser/InformationCollector.cpp
View File

@ -1,6 +1,7 @@
#include "storm/storage/jani/traverser/InformationCollector.h"
#include "storm/storage/jani/traverser/JaniTraverser.h"
#include "storm/storage/jani/Model.h"
#include "storm/utility/constants.h"
namespace storm {
namespace jani {
@ -9,7 +10,13 @@ namespace storm {
public:
InformationObject collect(Model const& model) {
info = InformationObject();
domainSizesSum = 0;
this->traverse(model, boost::any());
if (info.stateDomainSize > 0) {
info.avgVarDomainSize = storm::utility::convertNumber<double>(domainSizesSum) / storm::utility::convertNumber<double>(info.nrVariables);
} else {
info.avgVarDomainSize = 0.0;
}
return info;
}
@ -22,6 +29,7 @@ namespace storm {
virtual void traverse(Automaton const& automaton, boost::any const& data) override {
info.nrLocations += automaton.getNumberOfLocations();
info.stateDomainSize *= automaton.getNumberOfLocations();
domainSizesSum += automaton.getNumberOfLocations();
info.nrEdges += automaton.getNumberOfEdges();
ConstJaniTraverser::traverse(automaton, data);
}
@ -34,6 +42,7 @@ namespace storm {
virtual void traverse(BooleanVariable const& variable, boost::any const& data) override {
if (!variable.isTransient()) {
info.stateDomainSize *= 2;
domainSizesSum += 2;
}
ConstJaniTraverser::traverse(variable, data);
}
@ -42,6 +51,7 @@ namespace storm {
if (!variable.isTransient()) {
if (variable.hasLowerBound() && variable.hasUpperBound() && !variable.getLowerBound().containsVariables() && !variable.getUpperBound().containsVariables()) {
info.stateDomainSize *= (variable.getUpperBound().evaluateAsInt() - variable.getLowerBound().evaluateAsInt());
domainSizesSum += (variable.getUpperBound().evaluateAsInt() - variable.getLowerBound().evaluateAsInt());
} else {
info.stateDomainSize = 0; // i.e. unknown
}
@ -80,13 +90,13 @@ namespace storm {
private:
InformationObject info;
uint64_t domainSizesSum;
};
}
InformationObject::InformationObject() : nrVariables(0), nrAutomata(0), nrEdges(0), nrLocations(0), stateDomainSize(1) {
InformationObject::InformationObject() : nrVariables(0), nrAutomata(0), nrEdges(0), nrLocations(0), stateDomainSize(1), avgVarDomainSize(0.0) {
// Intentionally left empty
}

2
src/storm/storage/jani/traverser/InformationCollector.h
View File

@ -19,6 +19,8 @@ namespace storm {
uint64_t nrLocations; /// The numer of all locations of all automata of the model
uint64_t stateDomainSize; /// The size of the domain of the states (i.e., the product of the range of all variables times the number of locations).
/// Here, 0 means that the state domain size is unknown.
double avgVarDomainSize; /// The average range of the domain a variable can have
/// Here, 0 means that the range of at least one non-transient variable is unknown.
};
InformationObject collectModelInformation(Model const& model);

48
src/storm/utility/Portfolio.cpp
View File

@ -1,8 +1,10 @@
#include "storm/utility/Portfolio.h"
#include <sstream>
#include "storm/storage/SymbolicModelDescription.h"
#include "storm/storage/jani/Property.h"
#include "storm/storage/jani/traverser/InformationCollector.h"
#include "storm/logic/Formula.h"
#include "storm/logic/FormulaInformation.h"
@ -38,9 +40,42 @@ namespace storm {
continuousTime = !model.isDiscreteTimeModel();
nondeterminism = !model.isDeterministicModel();
propertyType = getPropertyType(property);
numVariables = model.getTotalNumberOfNonTransientVariables();
numAutomata = model.getNumberOfAutomata();
numEdges = model.getNumberOfEdges();
auto modelInfo = model.getModelInformation();
numVariables = modelInfo.nrVariables;
numEdges = modelInfo.nrEdges;
numAutomata = modelInfo.nrAutomata;
stateDomainSize = modelInfo.stateDomainSize;
avgDomainSize = modelInfo.avgVarDomainSize;
stateEstimate = 0;
}
std::string toString() const {
std::stringstream str;
str << std::boolalpha << "continuous-time=" << continuousTime << "\tnondeterminism=" << nondeterminism << "\tpropertytype=";
switch (propertyType) {
case PropertyType::Unbounded:
str << "unbounded";
break;
case PropertyType::Bounded:
str << "bounded";
break;
case PropertyType::LongRun:
str << "longrun";
break;
}
str << "\tnumVariables=" << numVariables;
str << "\tnumEdges=" << numEdges;
str << "\tnumAutomata=" << numAutomata;
if (stateDomainSize > 0) {
str << "\tstateDomainSize=" << stateDomainSize;
}
if (avgDomainSize > 0.0) {
str << "\tavgDomainSize=" << avgDomainSize;
}
if (stateEstimate > 0) {
str << "\tstateEstimate=" << stateEstimate;
}
return str.str();
}
bool continuousTime;
@ -49,7 +84,9 @@ namespace storm {
uint64_t numVariables;
uint64_t numAutomata;
uint64_t numEdges;
uint64_t stateDomainSize;
uint64_t stateEstimate;
double avgDomainSize;
};
}
@ -60,6 +97,7 @@ namespace storm {
void Portfolio::predict(storm::jani::Model const& model, storm::jani::Property const& property) {
typedef pfinternal::PropertyType PropertyType;
auto f = pfinternal::Features(model, property);
STORM_LOG_INFO("Portfolio engine using features " << f.toString() << ".");
{ // Decision tree start
if (f.numEdges <= 618) {
@ -167,6 +205,8 @@ namespace storm {
typedef pfinternal::PropertyType PropertyType;
auto f = pfinternal::Features(model, property);
f.stateEstimate = stateEstimate;
STORM_LOG_INFO("Portfolio engine using features " << f.toString() << ".");
// TODO: Actually make use of the estimate
predict(model, property);
}

Write Preview
Loading…
Cancel
Save