diff --git a/src/storm/utility/Portfolio.cpp b/src/storm/utility/Portfolio.cpp index 5ea49b720..c45f51d2b 100644 --- a/src/storm/utility/Portfolio.cpp +++ b/src/storm/utility/Portfolio.cpp @@ -3,21 +3,180 @@ #include "storm/storage/SymbolicModelDescription.h" #include "storm/storage/jani/Property.h" +#include "storm/logic/Formula.h" +#include "storm/logic/FormulaInformation.h" + #include "storm/utility/macros.h" #include "storm/exceptions/InvalidOperationException.h" namespace storm { namespace utility { - Portfolio::Portfolio() : engine(storm::utility::Engine::Unknown), bisimulation(false), exact(false) { + + namespace pfinternal { + enum class PropertyType{ + Bounded, + Unbounded, + LongRun + }; + + PropertyType getPropertyType(storm::jani::Property const& property) { + auto formulaInfo = property.getRawFormula()->info(); + if (formulaInfo.containsBoundedUntilFormula() || formulaInfo.containsNextFormula() || formulaInfo.containsCumulativeRewardFormula()) { + STORM_LOG_INFO("Assuming step or time bounded property:" << property); + return PropertyType::Bounded; + } else if (formulaInfo.containsLongRunFormula()) { + STORM_LOG_INFO("Assuming Long Run property:" << property); + return PropertyType::LongRun; + } else { + STORM_LOG_INFO("Unbounded property:" << property); + return PropertyType::Unbounded; + } + } + + struct Features { + Features(storm::storage::SymbolicModelDescription const& modelDescription, storm::jani::Property const& property) { + if (!modelDescription.isJaniModel()) { + initialize(modelDescription.toJani().asJaniModel(), property); + } else { + initialize(modelDescription.asJaniModel(), property); + } + } + + void initialize(storm::jani::Model const& model, storm::jani::Property const& property) { + continuousTime = !model.isDiscreteTimeModel(); + nondeterminism = !model.isDeterministicModel(); + propertyType = getPropertyType(property); + numVariables = model.getTotalNumberOfNonTransientVariables(); + numAutomata = model.getNumberOfAutomata(); + numEdges = model.getNumberOfEdges(); + } + + bool continuousTime; + bool nondeterminism; + PropertyType propertyType; + uint64_t numVariables; + uint64_t numAutomata; + uint64_t numEdges; + uint64_t stateEstimate; + }; + } + + Portfolio::Portfolio() : engine(storm::utility::Engine::Unknown), useBisimulation(false), useExact(false) { // Intentionally left empty } void Portfolio::predict(storm::storage::SymbolicModelDescription const& modelDescription, storm::jani::Property const& property) { - + typedef pfinternal::PropertyType PropertyType; + auto f = pfinternal::Features(modelDescription, property); + + { // Decision tree start + if (f.numEdges <= 618) { + if (!f.continuousTime) { + if (f.numVariables <= 3) { + exact(); + } else { // f.numVariables > 3 + if (f.propertyType == PropertyType::Bounded) { + if (f.numEdges <= 25) { + dd(); + } else { // f.numEdges > 25 + ddbisim(); + } + } else { // !(f.propertyType == PropertyType::Bounded) + if (f.numEdges <= 46) { + if (f.numVariables <= 8) { + hybrid(); + } else { // f.numVariables > 8 + if (f.numAutomata <= 1) { + ddbisim(); + } else { // f.numAutomata > 1 + if (f.numVariables <= 18) { + if (f.numEdges <= 36) { + if (f.numEdges <= 30) { + if (f.numAutomata <= 9) { + sparse(); + } else { // f.numAutomata > 9 + hybrid(); + } + } else { // f.numEdges > 30 + dd(); + } + } else { // f.numEdges > 36 + ddbisim(); + } + } else { // f.numVariables > 18 + hybrid(); + } + } + } + } else { // f.numEdges > 46 + if (!f.nondeterminism) { + if (f.numEdges <= 92) { + ddbisim(); + } else { // f.numEdges > 92 + dd(); + } + } else { // f.nondeterminism + if (f.numVariables <= 51) { + if (f.numAutomata <= 6) { + if (f.numAutomata <= 3) { + if (f.numEdges <= 85) { + sparse(); + } else { // f.numEdges > 85 + hybrid(); + } + } else { // f.numAutomata > 3 + hybrid(); + } + } else { // f.numAutomata > 6 + if (f.numAutomata <= 9) { + ddbisim(); + } else { // f.numAutomata > 9 + hybrid(); + } + } + } else { // f.numVariables > 51 + sparse(); + } + } + } + } + } + } else { // f.continuousTime + if (!f.nondeterminism) { + if (f.numAutomata <= 5) { + hybrid(); + } else { // f.numAutomata > 5 + if (f.numVariables <= 8) { + sparse(); + } else { // f.numVariables > 8 + if (f.numEdges <= 19) { + exact(); + } else { // f.numEdges > 19 + if (f.numVariables <= 21) { + hybrid(); + } else { // f.numVariables > 21 + sparse(); + } + } + } + } + } else { // f.nondeterminism + sparse(); + } + } + } else { // f.numEdges > 618 + sparse(); + } + } // Decision tree end + } void Portfolio::predict(storm::storage::SymbolicModelDescription const& modelDescription, storm::jani::Property const& property, uint64_t stateEstimate) { - + typedef pfinternal::PropertyType PropertyType; + auto f = pfinternal::Features(modelDescription, property); + f.stateEstimate = stateEstimate; + // TODO: Actually make use of the estimate + predict(modelDescription, property); } storm::utility::Engine Portfolio::getEngine() const { @@ -26,11 +185,41 @@ namespace storm { } bool Portfolio::enableBisimulation() const { - return bisimulation; + return useBisimulation; } bool Portfolio::enableExact() const { - return exact; + return useExact; + } + + void Portfolio::sparse() { + engine = storm::utility::Engine::Sparse; + useBisimulation = false; + useExact = false; + } + + void Portfolio::hybrid() { + engine = storm::utility::Engine::Hybrid; + useBisimulation = false; + useExact = false; + } + + void Portfolio::dd() { + engine = storm::utility::Engine::Dd; + useBisimulation = false; + useExact = false; + } + + void Portfolio::exact() { + engine = storm::utility::Engine::Sparse; + useBisimulation = false; + useExact = true; + } + + void Portfolio::ddbisim() { + engine = storm::utility::Engine::DdSparse; + useBisimulation = true; + useExact = false; } } diff --git a/src/storm/utility/Portfolio.h b/src/storm/utility/Portfolio.h index 17af90af7..8fceda6b8 100644 --- a/src/storm/utility/Portfolio.h +++ b/src/storm/utility/Portfolio.h @@ -34,9 +34,17 @@ namespace storm { bool enableExact() const; private: + + // some popular configs + void sparse(); + void hybrid(); + void dd(); + void exact(); + void ddbisim(); + storm::utility::Engine engine; - bool bisimulation; - bool exact; + bool useBisimulation; + bool useExact;