Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
explicit_models.h
Go to the documentation of this file.
1#pragma once
2
3#include <boost/optional.hpp>
4#include <memory>
5#include <string>
6#include <type_traits>
7
13
14namespace storm::api {
15
16template<typename ValueType>
17inline std::shared_ptr<storm::models::sparse::Model<ValueType>> buildExplicitModel(std::string const& transitionsFile, std::string const& labelingFile,
18 boost::optional<std::string> const& stateRewardsFile,
19 boost::optional<std::string> const& transitionRewardsFile,
20 boost::optional<std::string> const& choiceLabelingFile) {
21 if constexpr (std::is_same_v<ValueType, double>) {
22 return storm::parser::AutoParser<ValueType, ValueType>::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "",
23 transitionRewardsFile ? transitionRewardsFile.get() : "",
24 choiceLabelingFile ? choiceLabelingFile.get() : "");
25 }
26 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exact or parametric models with explicit input are not supported.");
27}
28
29template<typename ValueType>
30std::shared_ptr<storm::models::sparse::Model<ValueType>> buildExplicitDRNModel(
33}
34
35template<typename ValueType>
36std::shared_ptr<storm::models::sparse::Model<ValueType>> buildExplicitIMCAModel(std::string const& imcaFile) {
37 if constexpr (std::is_same_v<ValueType, double>) {
39 }
40 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exact models with direct encoding are not supported.");
41}
42
43} // namespace storm::api
static std::shared_ptr< storm::models::sparse::Model< ValueType, storm::models::sparse::StandardRewardModel< RewardValueType > > > parseModel(std::string const &transitionsFilename, std::string const &labelingFilename, std::string const &stateRewardFilename="", std::string const &transitionRewardFilename="", std::string const &choiceLabelingFilename="")
Checks the given files and parses the model within these files.
static std::shared_ptr< storm::models::sparse::Model< ValueType, RewardModelType > > parseModel(std::string const &fil, DirectEncodingParserOptions const &options=DirectEncodingParserOptions())
Load a model in DRN format from a file and create the model.
static std::shared_ptr< storm::models::sparse::MarkovAutomaton< ValueType > > parseImcaFile(std::string const &filename)
Parses the given file under the assumption that it contains a Markov automaton specified in the imca ...
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
std::shared_ptr< storm::models::sparse::Model< ValueType > > buildExplicitModel(std::string const &transitionsFile, std::string const &labelingFile, boost::optional< std::string > const &stateRewardsFile, boost::optional< std::string > const &transitionRewardsFile, boost::optional< std::string > const &choiceLabelingFile)
std::shared_ptr< storm::models::sparse::Model< ValueType > > buildExplicitDRNModel(std::string const &drnFile, storm::parser::DirectEncodingParserOptions const &options=storm::parser::DirectEncodingParserOptions())
std::shared_ptr< storm::models::sparse::Model< ValueType > > buildExplicitIMCAModel(std::string const &imcaFile)