diff --git a/src/storm/storage/jani/traverser/InformationCollector.cpp b/src/storm/storage/jani/traverser/InformationCollector.cpp index 834d1535d..58fe7fbc7 100644 --- a/src/storm/storage/jani/traverser/InformationCollector.cpp +++ b/src/storm/storage/jani/traverser/InformationCollector.cpp @@ -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(domainSizesSum) / storm::utility::convertNumber(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 } diff --git a/src/storm/storage/jani/traverser/InformationCollector.h b/src/storm/storage/jani/traverser/InformationCollector.h index 064534795..55a001768 100644 --- a/src/storm/storage/jani/traverser/InformationCollector.h +++ b/src/storm/storage/jani/traverser/InformationCollector.h @@ -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); diff --git a/src/storm/utility/Portfolio.cpp b/src/storm/utility/Portfolio.cpp index 2045ed153..c2687f679 100644 --- a/src/storm/utility/Portfolio.cpp +++ b/src/storm/utility/Portfolio.cpp @@ -1,8 +1,10 @@ #include "storm/utility/Portfolio.h" +#include + #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); }