Engine.h

Go to the documentation of this file.

#pragma once
 
#include <ostream>
#include <vector>
 
#include "storm/builder/BuilderType.h"
#include "storm/models/ModelType.h"
#include "storm/storage/dd/DdType.h"
 
namespace storm {
 
// Forward Declarations
namespace jani {
class Property;
}
 
namespace logic {
class Formula;
}
namespace modelchecker {
template<typename FormulaType, typename ValueType>
class CheckTask;
}
namespace storage {
class SymbolicModelDescription;
}
 
namespace utility {
 
enum class Engine {
    // The last one should always be 'Unknown' to make sure that the getEngines() method below works.
    Sparse,
    Hybrid,
    Dd,
    DdSparse,
    Exploration,
    AbstractionRefinement,
    Automatic,
    Unknown
};
 
std::vector<Engine> getEngines();
 
std::string toString(Engine const& engine);
 
std::ostream& operator<<(std::ostream& os, Engine const& engine);
 
Engine engineFromString(std::string const& engineStr);
 
storm::builder::BuilderType getBuilderType(storm::utility::Engine const& engine);
 
template<typename ValueType>
bool canHandle(storm::utility::Engine const& engine, std::vector<storm::jani::Property> const& properties,
               storm::storage::SymbolicModelDescription const& modelDescription);
}  // namespace utility
}  // namespace storm