From 15d13bc06d86a50b43e5ab7b5991d9c3011cf708 Mon Sep 17 00:00:00 2001 From: masawei Date: Tue, 21 Jan 2014 00:58:29 +0100 Subject: [PATCH] Refactored the AutoParser. - Devided the AutoParser.h into .h and .cpp - The AutoParser now is a stateless class |- This resulted in changes to the interface between the parsers and the rest of the project. |- The main() now directly acquires a shared_ptr to an AbstractModel from the call of the AutoParser and keeps ownership of it. |- Additionally, the division into .h and .cpp lead to a move of includes from the header to the source. This caused several tests to need some model header to be included. |- Tests are still showing green (except those needing Gurobi, which I do not have). Next up: Parser.h/.cpp, then comments and making things look nice.) Former-commit-id: f59b7405e5dda9971064bb36ba023ca3aef9dd86 --- .../PathBasedSubsystemGenerator.h | 2 +- src/parser/AutoParser.cpp | 94 ++++++++++ src/parser/AutoParser.h | 163 ++++-------------- src/storm.cpp | 47 ++--- .../GmmxxDtmcPrctlModelCheckerTest.cpp | 18 +- .../SparseMdpPrctlModelCheckerTest.cpp | 24 +-- .../MaximalEndComponentDecompositionTest.cpp | 15 +- ...glyConnectedComponentDecompositionTest.cpp | 11 +- test/performance/graph/GraphTest.cpp | 20 ++- .../GmmxxDtmcPrctModelCheckerTest.cpp | 14 +- .../SparseMdpPrctlModelCheckerTest.cpp | 14 +- .../MaximalEndComponentDecompositionTest.cpp | 11 +- ...glyConnectedComponentDecompositionTest.cpp | 20 ++- 13 files changed, 234 insertions(+), 219 deletions(-) create mode 100644 src/parser/AutoParser.cpp 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 computeCriticalSubsystem(storm::models::Dtmc& model, storm::property::prctl::AbstractStateFormula const& stateFormula) { + static storm::models::Dtmc computeCriticalSubsystem(storm::models::Dtmc & model, storm::property::prctl::AbstractStateFormula 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> 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> model; + switch (type) { + case storm::models::DTMC: { + model.reset(new storm::models::Dtmc(std::move(DeterministicModelParser::parseDtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); + break; + } + case storm::models::CTMC: { + model.reset(new storm::models::Ctmc(std::move(DeterministicModelParser::parseCtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); + break; + } + case storm::models::MDP: { + model.reset(new storm::models::Mdp(std::move(NondeterministicModelParser::parseMdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); + break; + } + case storm::models::CTMDP: { + model.reset(new storm::models::Ctmdp(std::move(NondeterministicModelParser::parseCtmdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); + break; + } + case storm::models::MA: { + model.reset(new storm::models::MarkovAutomaton(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 -#include -#include #include -#include 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(). - */ -template -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(std::move(DeterministicModelParser::parseDtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); - break; - } - case storm::models::CTMC: { - this->model.reset(new storm::models::Ctmc(std::move(DeterministicModelParser::parseCtmc(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); - break; - } - case storm::models::MDP: { - this->model.reset(new storm::models::Mdp(std::move(NondeterministicModelParser::parseMdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); - break; - } - case storm::models::CTMDP: { - this->model.reset(new storm::models::Ctmdp(std::move(NondeterministicModelParser::parseCtmdp(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile)))); - break; - } - case storm::models::MA: { - this->model.reset(new storm::models::MarkovAutomaton(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() 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> 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 - std::shared_ptr getModel() { - return this->model->template as(); - } - - 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> 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* createPrctlModelChecker(storm::models::Dtmc& dtmc) { +storm::modelchecker::prctl::AbstractModelChecker* createPrctlModelChecker(storm::models::Dtmc 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* createPrctlModelChecke * @param mdp The Dtmc that the model checker will check * @return */ -storm::modelchecker::prctl::AbstractModelChecker* createPrctlModelChecker(storm::models::Mdp& mdp) { +storm::modelchecker::prctl::AbstractModelChecker* createPrctlModelChecker(storm::models::Mdp const & mdp) { // Create the appropriate model checker. return new storm::modelchecker::prctl::SparseMdpPrctlModelChecker(mdp); } @@ -259,13 +259,13 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker * * @param parser An AutoParser to get the model from. */ - void generateCounterExample(storm::parser::AutoParser parser) { + void generateCounterExample(std::shared_ptr> 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 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 model = *parser.getModel>(); + // 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 dtmc = *(model->as>()); LOG4CPLUS_INFO(logger, "Model is a DTMC."); // Get specified PRCTL formulas. @@ -346,10 +349,10 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker // 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 } // Generate counterexample - storm::models::Dtmc counterExample = storm::counterexamples::PathBasedSubsystemGenerator::computeCriticalSubsystem(*parser.getModel>(), stateForm); + storm::models::Dtmc counterExample = storm::counterexamples::PathBasedSubsystemGenerator::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 parser(chosenTransitionSystemFile, chosenLabelingFile, chosenStateRewardsFile, chosenTransitionRewardsFile); + std::shared_ptr> 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>()->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* modelchecker = nullptr; - parser.getModel>()->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>()); + modelchecker = createPrctlModelChecker(*model->as>()); checkPrctlFormulae(*modelchecker); break; case storm::models::MDP: LOG4CPLUS_INFO(logger, "Model is an MDP."); - modelchecker = createPrctlModelChecker(*parser.getModel>()); + modelchecker = createPrctlModelChecker(*model->as>()); 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> markovAutomaton = parser.getModel>(); - markovAutomaton->close(); - storm::modelchecker::csl::SparseMarkovAutomatonCslModelChecker mc(*markovAutomaton); + storm::models::MarkovAutomaton markovAutomaton = *model->as>(); + markovAutomaton.close(); + storm::modelchecker::csl::SparseMarkovAutomatonCslModelChecker 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 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> 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> dtmc = parser.getModel>(); + std::shared_ptr> dtmc = abstractModel->as>(); 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 parser(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.lab", "", ""); + std::shared_ptr> 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> dtmc = parser.getModel>(); + std::shared_ptr> dtmc = abstractModel->as>(); 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 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> 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> dtmc = parser.getModel>(); + ASSERT_EQ(abstractModel->getType(), storm::models::DTMC); + std::shared_ptr> dtmc = abstractModel->as>(); 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 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> 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> mdp = parser.getModel>(); + std::shared_ptr> mdp = abstractModel->as>(); 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 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> stateRewardMdp = stateRewardParser.getModel>(); + std::shared_ptr> stateRewardMdp = abstractModel->as>(); storm::modelchecker::prctl::SparseMdpPrctlModelChecker stateRewardModelChecker(*stateRewardMdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); @@ -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 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> stateAndTransitionRewardMdp = stateAndTransitionRewardParser.getModel>(); + std::shared_ptr> stateAndTransitionRewardMdp = abstractModel->as>(); storm::modelchecker::prctl::SparseMdpPrctlModelChecker stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::shared_ptr>(new storm::solver::NativeNondeterministicLinearEquationSolver())); @@ -152,11 +152,11 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) { TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { storm::settings::Settings* s = storm::settings::Settings::getInstance(); - storm::parser::AutoParser 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> 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> mdp = parser.getModel>(); + std::shared_ptr> mdp = abstractModel->as>(); 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 parser(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.lab", "", ""); + std::shared_ptr> 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> markovAutomaton = parser.getModel>(); + std::shared_ptr> markovAutomaton = abstractModel->as>(); storm::storage::MaximalEndComponentDecomposition mecDecomposition; ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition(*markovAutomaton)); @@ -72,9 +73,9 @@ TEST(MaximalEndComponentDecomposition, FullSystem1) { } TEST(MaximalEndComponentDecomposition, FullSystem2) { - storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny2.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny2.lab", "", ""); + std::shared_ptr> 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> markovAutomaton = parser.getModel>(); + std::shared_ptr> markovAutomaton = abstractModel->as>(); storm::storage::MaximalEndComponentDecomposition mecDecomposition; ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition(*markovAutomaton)); @@ -101,9 +102,9 @@ TEST(MaximalEndComponentDecomposition, FullSystem2) { } TEST(MaximalEndComponentDecomposition, Subsystem) { - storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.lab", "", ""); + std::shared_ptr> 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> markovAutomaton = parser.getModel>(); + std::shared_ptr> markovAutomaton = abstractModel->as>(); 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 parser(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny1.lab", "", ""); - std::shared_ptr> markovAutomaton = parser.getModel>(); + std::shared_ptr> 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> markovAutomaton = abstractModel->as>(); storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; @@ -22,8 +24,9 @@ TEST(StronglyConnectedComponentDecomposition, FullSystem1) { } TEST(StronglyConnectedComponentDecomposition, FullSystem2) { - storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny2.tra", STORM_CPP_BASE_PATH "/examples/ma/tiny/tiny2.lab", "", ""); - std::shared_ptr> markovAutomaton = parser.getModel>(); + std::shared_ptr> 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> markovAutomaton = abstractModel->as>(); storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*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 parser(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", ""); + std::shared_ptr> 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> dtmc = parser.getModel>(); + std::shared_ptr> dtmc = abstractModel->as>(); 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 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> dtmc2 = parser2.getModel>(); + std::shared_ptr> dtmc2 = abstractModel->as>(); 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 parser(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", ""); - std::shared_ptr> mdp = parser.getModel>(); + std::shared_ptr> 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> mdp = abstractModel->as>(); 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 parser2(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", "", ""); - std::shared_ptr> mdp2 = parser2.getModel>(); + 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> mdp2 = abstractModel->as>(); 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 parser(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", ""); + std::shared_ptr> 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> dtmc = parser.getModel>(); + std::shared_ptr> dtmc = abstractModel->as>(); 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 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> 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> dtmc = parser.getModel>(); + std::shared_ptr> dtmc = abstractModel->as>(); 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 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> 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> mdp = parser.getModel>(); + std::shared_ptr> mdp = abstractModel->as>(); 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 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> 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> mdp = parser.getModel>(); + std::shared_ptr> mdp = abstractModel->as>(); 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 parser(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", ""); - std::shared_ptr> mdp = parser.getModel>(); + std::shared_ptr> 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> mdp = abstractModel->as>(); storm::storage::MaximalEndComponentDecomposition mecDecomposition; ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition(*mdp)); @@ -15,12 +16,12 @@ TEST(MaximalEndComponentDecomposition, AsynchronousLeader) { } TEST(MaximalEndComponentDecomposition, Consensus) { - storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_4.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_4.lab", "", ""); - std::shared_ptr> mdp = parser.getModel>(); + std::shared_ptr> 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> mdp = abstractModel->as>(); storm::storage::MaximalEndComponentDecomposition mecDecomposition; ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition(*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 parser(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", ""); - std::shared_ptr> dtmc = parser.getModel>(); + std::shared_ptr> 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> dtmc = abstractModel->as>(); storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; @@ -22,8 +24,8 @@ TEST(StronglyConnectedComponentDecomposition, Crowds) { } TEST(StronglyConnectedComponentDecomposition, SynchronousLeader) { - storm::parser::AutoParser 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> dtmc = parser.getModel>(); + std::shared_ptr> 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> dtmc = abstractModel->as>(); storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; @@ -40,8 +42,8 @@ TEST(StronglyConnectedComponentDecomposition, SynchronousLeader) { } TEST(StronglyConnectedComponentDecomposition, AsynchronousLeader) { - storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", ""); - std::shared_ptr> mdp = parser.getModel>(); + std::shared_ptr> 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> mdp = abstractModel->as>(); storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; @@ -58,8 +60,8 @@ TEST(StronglyConnectedComponentDecomposition, AsynchronousLeader) { } TEST(StronglyConnectedComponentDecomposition, Consensus) { - storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_4.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_4.lab", "", ""); - std::shared_ptr> mdp = parser.getModel>(); + std::shared_ptr> 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> mdp = abstractModel->as>(); storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; @@ -73,4 +75,4 @@ TEST(StronglyConnectedComponentDecomposition, Consensus) { ASSERT_EQ(384, sccDecomposition.size()); mdp = nullptr; -} \ No newline at end of file +}