diff --git a/src/counterexamples/PathBasedSubsystemGenerator.h b/src/counterexamples/PathBasedSubsystemGenerator.h
index 58678a390..11e24d00d 100644
--- a/src/counterexamples/PathBasedSubsystemGenerator.h
+++ b/src/counterexamples/PathBasedSubsystemGenerator.h
@@ -507,7 +507,7 @@ public:
/*!
*
*/
- static storm::models::Dtmc<T> computeCriticalSubsystem(storm::models::Dtmc<T>& model, storm::property::prctl::AbstractStateFormula<T> const& stateFormula) {
+ static storm::models::Dtmc<T> computeCriticalSubsystem(storm::models::Dtmc<T> & model, storm::property::prctl::AbstractStateFormula<T> const& stateFormula) {
//-------------------------------------------------------------
// 1. Strip and handle formulas
diff --git a/src/parser/AutoParser.cpp b/src/parser/AutoParser.cpp
new file mode 100644
index 000000000..ba9ec8323
--- /dev/null
+++ b/src/parser/AutoParser.cpp
@@ -0,0 +1,94 @@
+/*
+ * AutoParser.cpp
+ *
+ * Created on: Jan 20, 2014
+ * Author: Manuel S. Weiand
+ */
+
+#include "src/parser/AutoParser.h"
+
+#include "src/parser/Parser.h"
+
+#include "src/parser/DeterministicModelParser.h"
+#include "src/parser/NondeterministicModelParser.h"
+#include "src/parser/MarkovAutomatonParser.h"
+#include "src/exceptions/WrongFormatException.h"
+
+namespace storm {
+ namespace parser {
+
+ std::shared_ptr<storm::models::AbstractModel<double>> AutoParser::parseModel(std::string const & transitionSystemFile,
+ std::string const & labelingFile,
+ std::string const & stateRewardFile,
+ std::string const & transitionRewardFile) {
+
+ // Find and parse the model type hint.
+ storm::models::ModelType type = AutoParser::analyzeHint(transitionSystemFile);
+
+ // In case the hint string is unknown or could not be found, throw an exception.
+ if (type == storm::models::Unknown) {
+ LOG4CPLUS_ERROR(logger, "Could not determine file type of " << transitionSystemFile << ".");
+ LOG4CPLUS_ERROR(logger, "The first line of the file should contain a format hint. Please fix your file and try again.");
+ throw storm::exceptions::WrongFormatException() << "Could not determine type of file " << transitionSystemFile;
+ } else {
+ LOG4CPLUS_INFO(logger, "Model type seems to be " << type);
+ }
+
+ // Do the actual parsing.
+ std::shared_ptr<storm::models::AbstractModel<double>> model;
+ switch (type) {
+ case storm::models::DTMC: {
+ model.reset(new storm::models::Dtmc<double>(std::move(DeterministicModelParser::parseDtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))));
+ break;
+ }
+ case storm::models::CTMC: {
+ model.reset(new storm::models::Ctmc<double>(std::move(DeterministicModelParser::parseCtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))));
+ break;
+ }
+ case storm::models::MDP: {
+ model.reset(new storm::models::Mdp<double>(std::move(NondeterministicModelParser::parseMdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))));
+ break;
+ }
+ case storm::models::CTMDP: {
+ model.reset(new storm::models::Ctmdp<double>(std::move(NondeterministicModelParser::parseCtmdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))));
+ break;
+ }
+ case storm::models::MA: {
+ model.reset(new storm::models::MarkovAutomaton<double>(storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)));
+ break;
+ }
+ default:
+ LOG4CPLUS_WARN(logger, "Unknown/Unhandled Model Type which cannot be parsed."); // Unknown
+ }
+
+ return model;
+ }
+
+ storm::models::ModelType AutoParser::analyzeHint(const std::string& filename) {
+ storm::models::ModelType hintType = storm::models::Unknown;
+
+ // Find out the line endings used within the file.
+ storm::parser::SupportedLineEndingsEnum lineEndings = storm::parser::findUsedLineEndings(filename);
+
+ // Open the file.
+ MappedFile file(filename.c_str());
+ char* buf = file.data;
+
+ // Find and read in the hint.
+ char hint[128];
+ // %20s => The input hint can be AT MOST 120 chars long.
+ storm::parser::scanForModelHint(hint, sizeof(hint), buf, lineEndings);
+
+ for (char* c = hint; *c != '\0'; c++) *c = toupper(*c);
+
+ // Check if the hint value is known and store the appropriate enum value.
+ if (strncmp(hint, "DTMC", sizeof(hint)) == 0) hintType = storm::models::DTMC;
+ else if (strncmp(hint, "CTMC", sizeof(hint)) == 0) hintType = storm::models::CTMC;
+ else if (strncmp(hint, "MDP", sizeof(hint)) == 0) hintType = storm::models::MDP;
+ else if (strncmp(hint, "CTMDP", sizeof(hint)) == 0) hintType = storm::models::CTMDP;
+ else if (strncmp(hint, "MA", sizeof(hint)) == 0) hintType = storm::models::MA;
+
+ return hintType;
+ }
+ }
+}
diff --git a/src/parser/AutoParser.h b/src/parser/AutoParser.h
index 59082a135..d09897922 100644
--- a/src/parser/AutoParser.h
+++ b/src/parser/AutoParser.h
@@ -1,140 +1,49 @@
#ifndef STORM_PARSER_AUTOPARSER_H_
#define STORM_PARSER_AUTOPARSER_H_
-#include "src/parser/Parser.h"
#include "src/models/AbstractModel.h"
-#include "src/exceptions/WrongFormatException.h"
-#include "src/models/AbstractModel.h"
-#include "src/parser/DeterministicModelParser.h"
-#include "src/parser/NondeterministicModelParser.h"
-#include "src/parser/MarkovAutomatonParser.h"
-
-#include <memory>
-#include <iostream>
-#include <utility>
#include <string>
-#include <cctype>
namespace storm {
-
-namespace parser {
-
-/*!
- * @brief Checks the given files and parses the model within these files.
- *
- * This parser analyzes the format hint in the first line of the transition
- * file. If this is a valid format, it will use the parser for this format,
- * otherwise it will throw an exception.
- *
- * When the files are parsed successfully, the parsed ModelType and Model
- * can be obtained via getType() and getModel<ModelClass>().
- */
-template<class T>
-class AutoParser {
- public:
- AutoParser(std::string const & transitionSystemFile, std::string const & labelingFile,
- std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "") : model(nullptr) {
- storm::models::ModelType type = this->analyzeHint(transitionSystemFile);
-
- if (type == storm::models::Unknown) {
- LOG4CPLUS_ERROR(logger, "Could not determine file type of " << transitionSystemFile << ".");
- LOG4CPLUS_ERROR(logger, "The first line of the file should contain a format hint. Please fix your file and try again.");
- throw storm::exceptions::WrongFormatException() << "Could not determine type of file " << transitionSystemFile;
- } else {
- LOG4CPLUS_INFO(logger, "Model type seems to be " << type);
- }
-
- // Do actual parsing
- switch (type) {
- case storm::models::DTMC: {
- this->model.reset(new storm::models::Dtmc<double>(std::move(DeterministicModelParser::parseDtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))));
- break;
- }
- case storm::models::CTMC: {
- this->model.reset(new storm::models::Ctmc<double>(std::move(DeterministicModelParser::parseCtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))));
- break;
- }
- case storm::models::MDP: {
- this->model.reset(new storm::models::Mdp<double>(std::move(NondeterministicModelParser::parseMdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))));
- break;
- }
- case storm::models::CTMDP: {
- this->model.reset(new storm::models::Ctmdp<double>(std::move(NondeterministicModelParser::parseCtmdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile))));
- break;
- }
- case storm::models::MA: {
- this->model.reset(new storm::models::MarkovAutomaton<double>(storm::parser::MarkovAutomatonParser::parseMarkovAutomaton(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)));
- break;
- }
- default: ; // Unknown
- }
-
-
- if (!this->model) {
- LOG4CPLUS_WARN(logger, "Unknown/Unhandled Model Type. Model is still null.");
- }
- }
+ namespace parser {
+
+ class AutoParser {
+ public:
+
+ /*!
+ * Checks the given files and parses the model within these files.
+ *
+ * This parser analyzes the format hint in the first line of the transition
+ * file. If this is a valid format, it will use the parser for this format,
+ * otherwise it will throw an exception.
+ *
+ * When the files are parsed successfully, a shared pointer owning the resulting model is returned.
+ * The concrete model can be obtained using the as<Type>() member of the AbstractModel class.
+ *
+ * @param transitionsFilename The name of the file containing the transitions of the Markov automaton.
+ * @param labelingFilename The name of the file containing the labels for the states of the Markov automaton.
+ * @param stateRewardFilename The name of the file that contains the state reward of the Markov automaton.
+ * @param transitionRewardFilename The name of the file that contains the transition rewards of the Markov automaton.
+ * @return A shared_ptr containing the resulting model.
+ */
+ static std::shared_ptr<storm::models::AbstractModel<double>> parseModel(std::string const & transitionSystemFile,
+ std::string const & labelingFile,
+ std::string const & stateRewardFile = "",
+ std::string const & transitionRewardFile = "");
- /*!
- * @brief Returns the type of model that was parsed.
- */
- storm::models::ModelType getType() {
- if (this->model) {
- return this->model->getType();
- } else {
- return storm::models::Unknown;
- }
- }
+ private:
+
+ /*!
+ * Opens the given file and parses the file format hint.
+ *
+ * @param filename The path and name of the file that is to be analysed.
+ * @return The type of the model as an enum value.
+ */
+ static storm::models::ModelType analyzeHint(const std::string& filename);
+ };
- /*!
- * @brief Returns the model with the given type.
- */
- template <typename Model>
- std::shared_ptr<Model> getModel() {
- return this->model->template as<Model>();
- }
-
- private:
-
- /*!
- * @brief Open file and read file format hint.
- */
- storm::models::ModelType analyzeHint(const std::string& filename) {
- storm::models::ModelType hintType = storm::models::Unknown;
-
- // Parse the File and check for the Line Endings
- storm::parser::SupportedLineEndingsEnum lineEndings = storm::parser::findUsedLineEndings(filename);
-
- // Open file
- MappedFile file(filename.c_str());
- char* buf = file.data;
-
- // parse hint
- char hint[128];
- // %20s => The Input Hint can be AT MOST 120 chars long
- storm::parser::scanForModelHint(hint, sizeof(hint), buf, lineEndings);
-
- for (char* c = hint; *c != '\0'; c++) *c = toupper(*c);
-
- // check hint
- if (strncmp(hint, "DTMC", sizeof(hint)) == 0) hintType = storm::models::DTMC;
- else if (strncmp(hint, "CTMC", sizeof(hint)) == 0) hintType = storm::models::CTMC;
- else if (strncmp(hint, "MDP", sizeof(hint)) == 0) hintType = storm::models::MDP;
- else if (strncmp(hint, "CTMDP", sizeof(hint)) == 0) hintType = storm::models::CTMDP;
- else if (strncmp(hint, "MA", sizeof(hint)) == 0) hintType = storm::models::MA;
-
- return hintType;
- }
-
- /*!
- * @brief Pointer to a parser that has parsed the given transition system.
- */
- std::shared_ptr<storm::models::AbstractModel<T>> model;
-};
-
-} // namespace parser
-
+ } // namespace parser
} // namespace storm
#endif /* STORM_PARSER_AUTOPARSER_H_ */
diff --git a/src/storm.cpp b/src/storm.cpp
index 88ecafad4..cef1c793e 100644
--- a/src/storm.cpp
+++ b/src/storm.cpp
@@ -210,7 +210,7 @@ void cleanUp() {
* @param dtmc A reference to the DTMC for which the model checker is to be created.
* @return A pointer to the resulting model checker.
*/
-storm::modelchecker::prctl::AbstractModelChecker<double>* createPrctlModelChecker(storm::models::Dtmc<double>& dtmc) {
+storm::modelchecker::prctl::AbstractModelChecker<double>* createPrctlModelChecker(storm::models::Dtmc<double> const & dtmc) {
// Create the appropriate model checker.
storm::settings::Settings* s = storm::settings::Settings::getInstance();
std::string const chosenMatrixLibrary = s->getOptionByLongName("matrixLibrary").getArgument(0).getValueAsString();
@@ -230,7 +230,7 @@ storm::modelchecker::prctl::AbstractModelChecker<double>* createPrctlModelChecke
* @param mdp The Dtmc that the model checker will check
* @return
*/
-storm::modelchecker::prctl::AbstractModelChecker<double>* createPrctlModelChecker(storm::models::Mdp<double>& mdp) {
+storm::modelchecker::prctl::AbstractModelChecker<double>* createPrctlModelChecker(storm::models::Mdp<double> const & mdp) {
// Create the appropriate model checker.
return new storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double>(mdp);
}
@@ -259,13 +259,13 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker<double>
*
* @param parser An AutoParser to get the model from.
*/
- void generateCounterExample(storm::parser::AutoParser<double> parser) {
+ void generateCounterExample(std::shared_ptr<storm::models::AbstractModel<double>> model) {
LOG4CPLUS_INFO(logger, "Starting counterexample generation.");
LOG4CPLUS_INFO(logger, "Testing inputs...");
storm::settings::Settings* s = storm::settings::Settings::getInstance();
- //First test output directory.
+ // First test output directory.
std::string outPath = s->getOptionByLongName("counterExample").getArgument(0).getValueAsString();
if(outPath.back() != '/' && outPath.back() != '\\') {
LOG4CPLUS_ERROR(logger, "The output path is not valid.");
@@ -279,13 +279,16 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker<double>
testFile.close();
std::remove((outPath + "test.dot").c_str());
- //Differentiate between model types.
- if(parser.getType() != storm::models::DTMC) {
+ // Differentiate between model types.
+ if(model->getType() != storm::models::DTMC) {
LOG4CPLUS_ERROR(logger, "Counterexample generation for the selected model type is not supported.");
return;
}
- storm::models::Dtmc<double> model = *parser.getModel<storm::models::Dtmc<double>>();
+ // Get the Dtmc back from the AbstractModel
+ // Note that the ownership of the object referenced by dtmc lies at the main function.
+ // Thus, it must not be deleted.
+ storm::models::Dtmc<double> dtmc = *(model->as<storm::models::Dtmc<double>>());
LOG4CPLUS_INFO(logger, "Model is a DTMC.");
// Get specified PRCTL formulas.
@@ -346,10 +349,10 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker<double>
// Also raise the logger threshold for the log file, so that the model check infos aren't logged (useless and there are lots of them)
// Lower it again after the model check.
logger.getAppender("mainFileAppender")->setThreshold(log4cplus::WARN_LOG_LEVEL);
- storm::storage::BitVector result = stateForm.check(*createPrctlModelChecker(model));
+ storm::storage::BitVector result = stateForm.check(*createPrctlModelChecker(dtmc));
logger.getAppender("mainFileAppender")->setThreshold(log4cplus::INFO_LOG_LEVEL);
- if((result & model.getInitialStates()).getNumberOfSetBits() == model.getInitialStates().getNumberOfSetBits()) {
+ if((result & dtmc.getInitialStates()).getNumberOfSetBits() == dtmc.getInitialStates().getNumberOfSetBits()) {
std::cout << "Formula is satisfied. Can not generate counterexample.\n\n" << std::endl;
LOG4CPLUS_INFO(logger, "Formula is satisfied. Can not generate counterexample.");
delete formula;
@@ -357,7 +360,7 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker<double>
}
// Generate counterexample
- storm::models::Dtmc<double> counterExample = storm::counterexamples::PathBasedSubsystemGenerator<double>::computeCriticalSubsystem(*parser.getModel<storm::models::Dtmc<double>>(), stateForm);
+ storm::models::Dtmc<double> counterExample = storm::counterexamples::PathBasedSubsystemGenerator<double>::computeCriticalSubsystem(dtmc, stateForm);
LOG4CPLUS_INFO(logger, "Found counterexample.");
@@ -418,19 +421,19 @@ int main(const int argc, const char* argv[]) {
chosenTransitionRewardsFile = s->getOptionByLongName("transitionRewards").getArgument(0).getValueAsString();
}
- storm::parser::AutoParser<double> parser(chosenTransitionSystemFile, chosenLabelingFile, chosenStateRewardsFile, chosenTransitionRewardsFile);
+ std::shared_ptr<storm::models::AbstractModel<double>> model = storm::parser::AutoParser::parseModel(chosenTransitionSystemFile, chosenLabelingFile, chosenStateRewardsFile, chosenTransitionRewardsFile);
if (s->isSet("exportdot")) {
std::ofstream outputFileStream;
outputFileStream.open(s->getOptionByLongName("exportdot").getArgument(0).getValueAsString(), std::ofstream::out);
- parser.getModel<storm::models::AbstractModel<double>>()->writeDotToStream(outputFileStream);
+ model->writeDotToStream(outputFileStream);
outputFileStream.close();
}
//Should there be a counterexample generated in case the formula is not satisfied?
if(s->isSet("counterexample")) {
- generateCounterExample(parser);
+ generateCounterExample(model);
} else {
// Determine which engine is to be used to choose the right model checker.
@@ -438,17 +441,17 @@ int main(const int argc, const char* argv[]) {
// Depending on the model type, the appropriate model checking procedure is chosen.
storm::modelchecker::prctl::AbstractModelChecker<double>* modelchecker = nullptr;
- parser.getModel<storm::models::AbstractModel<double>>()->printModelInformationToStream(std::cout);
+ model->printModelInformationToStream(std::cout);
- switch (parser.getType()) {
+ switch (model->getType()) {
case storm::models::DTMC:
LOG4CPLUS_INFO(logger, "Model is a DTMC.");
- modelchecker = createPrctlModelChecker(*parser.getModel<storm::models::Dtmc<double>>());
+ modelchecker = createPrctlModelChecker(*model->as<storm::models::Dtmc<double>>());
checkPrctlFormulae(*modelchecker);
break;
case storm::models::MDP:
LOG4CPLUS_INFO(logger, "Model is an MDP.");
- modelchecker = createPrctlModelChecker(*parser.getModel<storm::models::Mdp<double>>());
+ modelchecker = createPrctlModelChecker(*model->as<storm::models::Mdp<double>>());
checkPrctlFormulae(*modelchecker);
break;
case storm::models::CTMC:
@@ -461,13 +464,13 @@ int main(const int argc, const char* argv[]) {
break;
case storm::models::MA: {
LOG4CPLUS_INFO(logger, "Model is a Markov automaton.");
- std::shared_ptr<storm::models::MarkovAutomaton<double>> markovAutomaton = parser.getModel<storm::models::MarkovAutomaton<double>>();
- markovAutomaton->close();
- storm::modelchecker::csl::SparseMarkovAutomatonCslModelChecker<double> mc(*markovAutomaton);
+ storm::models::MarkovAutomaton<double> markovAutomaton = *model->as<storm::models::MarkovAutomaton<double>>();
+ markovAutomaton.close();
+ storm::modelchecker::csl::SparseMarkovAutomatonCslModelChecker<double> mc(markovAutomaton);
// std::cout << mc.checkExpectedTime(true, markovAutomaton->getLabeledStates("goal")) << std::endl;
// std::cout << mc.checkExpectedTime(false, markovAutomaton->getLabeledStates("goal")) << std::endl;
- std::cout << mc.checkLongRunAverage(true, markovAutomaton->getLabeledStates("goal")) << std::endl;
- std::cout << mc.checkLongRunAverage(false, markovAutomaton->getLabeledStates("goal")) << std::endl;
+ std::cout << mc.checkLongRunAverage(true, markovAutomaton.getLabeledStates("goal")) << std::endl;
+ std::cout << mc.checkLongRunAverage(false, markovAutomaton.getLabeledStates("goal")) << std::endl;
// std::cout << mc.checkTimeBoundedEventually(true, markovAutomaton->getLabeledStates("goal"), 0, 1) << std::endl;
// std::cout << mc.checkTimeBoundedEventually(true, markovAutomaton->getLabeledStates("goal"), 1, 2) << std::endl;
break;
diff --git a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
index d724ef23d..fdff14a66 100644
--- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
@@ -11,11 +11,11 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) {
storm::settings::Settings* s = storm::settings::Settings::getInstance();
storm::settings::InternalOptionMemento deadlockOption("fixDeadlocks", true);
ASSERT_TRUE(s->isSet("fixDeadlocks"));
- storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.coin_flips.trans.rew");
+ std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.coin_flips.trans.rew");
- ASSERT_EQ(parser.getType(), storm::models::DTMC);
+ ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
- std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
+ std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
ASSERT_EQ(dtmc->getNumberOfStates(), 13ull);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 27ull);
@@ -67,11 +67,11 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
storm::settings::Settings* s = storm::settings::Settings::getInstance();
storm::settings::InternalOptionMemento deadlockOption("fixDeadlocks", true);
ASSERT_TRUE(s->isSet("fixDeadlocks"));
- storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.lab", "", "");
+ std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.lab", "", "");
- ASSERT_EQ(parser.getType(), storm::models::DTMC);
+ ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
- std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
+ std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
ASSERT_EQ(dtmc->getNumberOfStates(), 8607ull);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 22460ull);
@@ -113,10 +113,10 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
storm::settings::Settings* s = storm::settings::Settings::getInstance();
storm::settings::InternalOptionMemento deadlockOption("fixDeadlocks", true);
ASSERT_TRUE(s->isSet("fixDeadlocks"));
- storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.pick.trans.rew");
+ std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.pick.trans.rew");
- ASSERT_EQ(parser.getType(), storm::models::DTMC);
- std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
+ ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
+ std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
ASSERT_EQ(dtmc->getNumberOfStates(), 12400ull);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 28894ull);
diff --git a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
index 83b4afdb2..67fe2d63a 100644
--- a/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
@@ -8,11 +8,11 @@
TEST(SparseMdpPrctlModelCheckerTest, Dice) {
storm::settings::Settings* s = storm::settings::Settings::getInstance();
- storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew");
+ std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew");
- ASSERT_EQ(parser.getType(), storm::models::MDP);
+ ASSERT_EQ(abstractModel->getType(), storm::models::MDP);
- std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
+ std::shared_ptr<storm::models::Mdp<double>> mdp = abstractModel->as<storm::models::Mdp<double>>();
ASSERT_EQ(mdp->getNumberOfStates(), 169ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull);
@@ -97,11 +97,11 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
- storm::parser::AutoParser<double> stateRewardParser(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", "");
+ abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", "");
- ASSERT_EQ(stateRewardParser.getType(), storm::models::MDP);
+ ASSERT_EQ(abstractModel->getType(), storm::models::MDP);
- std::shared_ptr<storm::models::Mdp<double>> stateRewardMdp = stateRewardParser.getModel<storm::models::Mdp<double>>();
+ std::shared_ptr<storm::models::Mdp<double>> stateRewardMdp = abstractModel->as<storm::models::Mdp<double>>();
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp, std::shared_ptr<storm::solver::NativeNondeterministicLinearEquationSolver<double>>(new storm::solver::NativeNondeterministicLinearEquationSolver<double>()));
@@ -123,11 +123,11 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
- storm::parser::AutoParser<double> stateAndTransitionRewardParser(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew");
+ abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew");
- ASSERT_EQ(stateAndTransitionRewardParser.getType(), storm::models::MDP);
+ ASSERT_EQ(abstractModel->getType(), storm::models::MDP);
- std::shared_ptr<storm::models::Mdp<double>> stateAndTransitionRewardMdp = stateAndTransitionRewardParser.getModel<storm::models::Mdp<double>>();
+ std::shared_ptr<storm::models::Mdp<double>> stateAndTransitionRewardMdp = abstractModel->as<storm::models::Mdp<double>>();
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::shared_ptr<storm::solver::NativeNondeterministicLinearEquationSolver<double>>(new storm::solver::NativeNondeterministicLinearEquationSolver<double>()));
@@ -152,11 +152,11 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
storm::settings::Settings* s = storm::settings::Settings::getInstance();
- storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.trans.rew");
+ std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.trans.rew");
- ASSERT_EQ(parser.getType(), storm::models::MDP);
+ ASSERT_EQ(abstractModel->getType(), storm::models::MDP);
- std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
+ std::shared_ptr<storm::models::Mdp<double>> mdp = abstractModel->as<storm::models::Mdp<double>>();
ASSERT_EQ(mdp->getNumberOfStates(), 3172ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull);
diff --git a/test/functional/storage/MaximalEndComponentDecompositionTest.cpp b/test/functional/storage/MaximalEndComponentDecompositionTest.cpp
index cacb33843..1a6112148 100644
--- a/test/functional/storage/MaximalEndComponentDecompositionTest.cpp
+++ b/test/functional/storage/MaximalEndComponentDecompositionTest.cpp
@@ -2,11 +2,12 @@
#include "storm-config.h"
#include "src/parser/AutoParser.h"
#include "src/storage/MaximalEndComponentDecomposition.h"
+#include "src/models/MarkovAutomaton.h"
TEST(MaximalEndComponentDecomposition, FullSystem1) {
- storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.lab", "", "");
+ std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.lab", "", "");
- std::shared_ptr<storm::models::MarkovAutomaton<double>> markovAutomaton = parser.getModel<storm::models::MarkovAutomaton<double>>();
+ std::shared_ptr<storm::models::MarkovAutomaton<double>> markovAutomaton = abstractModel->as<storm::models::MarkovAutomaton<double>>();
storm::storage::MaximalEndComponentDecomposition<double> mecDecomposition;
ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition<double>(*markovAutomaton));
@@ -72,9 +73,9 @@ TEST(MaximalEndComponentDecomposition, FullSystem1) {
}
TEST(MaximalEndComponentDecomposition, FullSystem2) {
- storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny2.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny2.lab", "", "");
+ std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny2.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny2.lab", "", "");
- std::shared_ptr<storm::models::MarkovAutomaton<double>> markovAutomaton = parser.getModel<storm::models::MarkovAutomaton<double>>();
+ std::shared_ptr<storm::models::MarkovAutomaton<double>> markovAutomaton = abstractModel->as<storm::models::MarkovAutomaton<double>>();
storm::storage::MaximalEndComponentDecomposition<double> mecDecomposition;
ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition<double>(*markovAutomaton));
@@ -101,9 +102,9 @@ TEST(MaximalEndComponentDecomposition, FullSystem2) {
}
TEST(MaximalEndComponentDecomposition, Subsystem) {
- storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.lab", "", "");
+ std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.lab", "", "");
- std::shared_ptr<storm::models::MarkovAutomaton<double>> markovAutomaton = parser.getModel<storm::models::MarkovAutomaton<double>>();
+ std::shared_ptr<storm::models::MarkovAutomaton<double>> markovAutomaton = abstractModel->as<storm::models::MarkovAutomaton<double>>();
storm::storage::BitVector subsystem(markovAutomaton->getNumberOfStates(), true);
subsystem.set(7, false);
@@ -130,4 +131,4 @@ TEST(MaximalEndComponentDecomposition, Subsystem) {
// This case must never happen as the only two existing MEC contains 3.
ASSERT_TRUE(false);
}
-}
\ No newline at end of file
+}
diff --git a/test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp b/test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp
index 22f04d0d1..21939d1bf 100644
--- a/test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp
+++ b/test/functional/storage/StronglyConnectedComponentDecompositionTest.cpp
@@ -2,10 +2,12 @@
#include "storm-config.h"
#include "src/parser/AutoParser.h"
#include "src/storage/StronglyConnectedComponentDecomposition.h"
+#include "src/models/MarkovAutomaton.h"
TEST(StronglyConnectedComponentDecomposition, FullSystem1) {
- storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.lab", "", "");
- std::shared_ptr<storm::models::MarkovAutomaton<double>> markovAutomaton = parser.getModel<storm::models::MarkovAutomaton<double>>();
+ std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.lab", "", "");
+
+ std::shared_ptr<storm::models::MarkovAutomaton<double>> markovAutomaton = abstractModel->as<storm::models::MarkovAutomaton<double>>();
storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
@@ -22,8 +24,9 @@ TEST(StronglyConnectedComponentDecomposition, FullSystem1) {
}
TEST(StronglyConnectedComponentDecomposition, FullSystem2) {
- storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny2.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny2.lab", "", "");
- std::shared_ptr<storm::models::MarkovAutomaton<double>> markovAutomaton = parser.getModel<storm::models::MarkovAutomaton<double>>();
+ std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny2.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny2.lab", "", "");
+
+ std::shared_ptr<storm::models::MarkovAutomaton<double>> markovAutomaton = abstractModel->as<storm::models::MarkovAutomaton<double>>();
storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition<double>(*markovAutomaton, true, false));
diff --git a/test/performance/graph/GraphTest.cpp b/test/performance/graph/GraphTest.cpp
index b3355c398..e0fe1b9b4 100644
--- a/test/performance/graph/GraphTest.cpp
+++ b/test/performance/graph/GraphTest.cpp
@@ -4,11 +4,13 @@
#include "src/parser/AutoParser.h"
#include "src/utility/graph.h"
#include "src/storage/StronglyConnectedComponentDecomposition.h"
+#include "src/models/Mdp.h"
+#include "src/models/Dtmc.h"
TEST(GraphTest, PerformProb01) {
- storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", "");
+ std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", "");
- std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
+ std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
storm::storage::BitVector trueStates(dtmc->getNumberOfStates(), true);
LOG4CPLUS_WARN(logger, "Computing prob01 (3 times) for crowds/crowds20_5...");
@@ -31,9 +33,9 @@ TEST(GraphTest, PerformProb01) {
dtmc = nullptr;
- storm::parser::AutoParser<double> parser2(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.lab", "", "");
+ abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.lab", "", "");
- std::shared_ptr<storm::models::Dtmc<double>> dtmc2 = parser2.getModel<storm::models::Dtmc<double>>();
+ std::shared_ptr<storm::models::Dtmc<double>> dtmc2 = abstractModel->as<storm::models::Dtmc<double>>();
trueStates = storm::storage::BitVector(dtmc2->getNumberOfStates(), true);
LOG4CPLUS_WARN(logger, "Computing prob01 for synchronous_leader/leader6_8...");
@@ -47,8 +49,8 @@ TEST(GraphTest, PerformProb01) {
}
TEST(GraphTest, PerformProb01MinMax) {
- storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", "");
- std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
+ std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", "");
+ std::shared_ptr<storm::models::Mdp<double>> mdp = abstractModel->as<storm::models::Mdp<double>>();
storm::storage::BitVector trueStates(mdp->getNumberOfStates(), true);
LOG4CPLUS_WARN(logger, "Computing prob01min for asynchronous_leader/leader7...");
@@ -67,8 +69,8 @@ TEST(GraphTest, PerformProb01MinMax) {
mdp = nullptr;
- storm::parser::AutoParser<double> parser2(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", "", "");
- std::shared_ptr<storm::models::Mdp<double>> mdp2 = parser2.getModel<storm::models::Mdp<double>>();
+ abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", "", "");
+ std::shared_ptr<storm::models::Mdp<double>> mdp2 = abstractModel->as<storm::models::Mdp<double>>();
trueStates = storm::storage::BitVector(mdp2->getNumberOfStates(), true);
LOG4CPLUS_WARN(logger, "Computing prob01min for consensus/coin4_6...");
@@ -86,4 +88,4 @@ TEST(GraphTest, PerformProb01MinMax) {
ASSERT_EQ(prob01.second.getNumberOfSetBits(), 63616ull);
mdp2 = nullptr;
-}
\ No newline at end of file
+}
diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
index c9c309d60..809f602fb 100644
--- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
+++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
@@ -10,11 +10,11 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
storm::settings::Settings* s = storm::settings::Settings::getInstance();
storm::settings::InternalOptionMemento deadlockOption("fixDeadlocks", true);
ASSERT_TRUE(s->isSet("fixDeadlocks"));
- storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", "");
+ std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", "");
- ASSERT_EQ(parser.getType(), storm::models::DTMC);
+ ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
- std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
+ std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
ASSERT_EQ(dtmc->getNumberOfStates(), 2036647ull);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 8973900ull);
@@ -63,12 +63,12 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
storm::settings::Settings* s = storm::settings::Settings::getInstance();
storm::settings::InternalOptionMemento deadlockOption("fixDeadlocks", true);
ASSERT_TRUE(s->isSet("fixDeadlocks"));
- storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.pick.trans.rew");
+ std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.pick.trans.rew");
- ASSERT_EQ(parser.getType(), storm::models::DTMC);
+ ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
- std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
+ std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
ASSERT_EQ(dtmc->getNumberOfStates(), 1312334ull);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 2886810ull);
@@ -110,4 +110,4 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
ASSERT_LT(std::abs(result[0] - 1.025106273), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
-}
\ No newline at end of file
+}
diff --git a/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
index 4a8193d26..8f083f89f 100644
--- a/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
+++ b/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
@@ -8,11 +8,11 @@
TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
storm::settings::Settings* s = storm::settings::Settings::getInstance();
- storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew");
+ std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew");
- ASSERT_EQ(parser.getType(), storm::models::MDP);
+ ASSERT_EQ(abstractModel->getType(), storm::models::MDP);
- std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
+ std::shared_ptr<storm::models::Mdp<double>> mdp = abstractModel->as<storm::models::Mdp<double>>();
ASSERT_EQ(mdp->getNumberOfStates(), 2095783ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385ull);
@@ -79,11 +79,11 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
// Increase the maximal number of iterations, because the solver does not converge otherwise.
// This is done in the main cpp unit
- storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", "");
+ std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", "");
- ASSERT_EQ(parser.getType(), storm::models::MDP);
+ ASSERT_EQ(abstractModel->getType(), storm::models::MDP);
- std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
+ std::shared_ptr<storm::models::Mdp<double>> mdp = abstractModel->as<storm::models::Mdp<double>>();
ASSERT_EQ(mdp->getNumberOfStates(), 63616ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull);
@@ -168,4 +168,4 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
ASSERT_LT(std::abs(result[31168] - 2183.142422), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
-}
\ No newline at end of file
+}
diff --git a/test/performance/storage/MaximalEndComponentDecompositionTest.cpp b/test/performance/storage/MaximalEndComponentDecompositionTest.cpp
index a34a35091..ee5460fed 100644
--- a/test/performance/storage/MaximalEndComponentDecompositionTest.cpp
+++ b/test/performance/storage/MaximalEndComponentDecompositionTest.cpp
@@ -2,10 +2,11 @@
#include "storm-config.h"
#include "src/parser/AutoParser.h"
#include "src/storage/MaximalEndComponentDecomposition.h"
+#include "src/models/Mdp.h"
TEST(MaximalEndComponentDecomposition, AsynchronousLeader) {
- storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", "");
- std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
+ std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", "");
+ std::shared_ptr<storm::models::Mdp<double>> mdp = abstractModel->as<storm::models::Mdp<double>>();
storm::storage::MaximalEndComponentDecomposition<double> mecDecomposition;
ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition<double>(*mdp));
@@ -15,12 +16,12 @@ TEST(MaximalEndComponentDecomposition, AsynchronousLeader) {
}
TEST(MaximalEndComponentDecomposition, Consensus) {
- storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_4.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_4.lab", "", "");
- std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
+ std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_4.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_4.lab", "", "");
+ std::shared_ptr<storm::models::Mdp<double>> mdp = abstractModel->as<storm::models::Mdp<double>>();
storm::storage::MaximalEndComponentDecomposition<double> mecDecomposition;
ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition<double>(*mdp));
ASSERT_EQ(384, mecDecomposition.size());
mdp = nullptr;
-}
\ No newline at end of file
+}
diff --git a/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp b/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp
index b519c27be..83bc77de6 100644
--- a/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp
+++ b/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp
@@ -2,10 +2,12 @@
#include "storm-config.h"
#include "src/parser/AutoParser.h"
#include "src/storage/StronglyConnectedComponentDecomposition.h"
+#include "src/models/Mdp.h"
+#include "src/models/Dtmc.h"
TEST(StronglyConnectedComponentDecomposition, Crowds) {
- storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", "");
- std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
+ std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", "");
+ std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
@@ -22,8 +24,8 @@ TEST(StronglyConnectedComponentDecomposition, Crowds) {
}
TEST(StronglyConnectedComponentDecomposition, SynchronousLeader) {
- storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_9.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_9.lab", "", "");
- std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
+ std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_9.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_9.lab", "", "");
+ std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
@@ -40,8 +42,8 @@ TEST(StronglyConnectedComponentDecomposition, SynchronousLeader) {
}
TEST(StronglyConnectedComponentDecomposition, AsynchronousLeader) {
- storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", "");
- std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
+ std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", "");
+ std::shared_ptr<storm::models::Mdp<double>> mdp = abstractModel->as<storm::models::Mdp<double>>();
storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
@@ -58,8 +60,8 @@ TEST(StronglyConnectedComponentDecomposition, AsynchronousLeader) {
}
TEST(StronglyConnectedComponentDecomposition, Consensus) {
- storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_4.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_4.lab", "", "");
- std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
+ std::shared_ptr<storm::models::AbstractModel<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_4.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_4.lab", "", "");
+ std::shared_ptr<storm::models::Mdp<double>> mdp = abstractModel->as<storm::models::Mdp<double>>();
storm::storage::StronglyConnectedComponentDecomposition<double> sccDecomposition;
@@ -73,4 +75,4 @@ TEST(StronglyConnectedComponentDecomposition, Consensus) {
ASSERT_EQ(384, sccDecomposition.size());
mdp = nullptr;
-}
\ No newline at end of file
+}