diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 0f277386d..7239a9676 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -6,6 +6,7 @@ add_custom_target(binaries) add_subdirectory(storm) add_subdirectory(storm-counterexamples) +add_subdirectory(storm-parsers) add_subdirectory(storm-cli-utilities) add_subdirectory(storm-pgcl) add_subdirectory(storm-pgcl-cli) diff --git a/src/storm-cli-utilities/CMakeLists.txt b/src/storm-cli-utilities/CMakeLists.txt index 5e37b5db4..de4c0fde1 100644 --- a/src/storm-cli-utilities/CMakeLists.txt +++ b/src/storm-cli-utilities/CMakeLists.txt @@ -17,7 +17,7 @@ set_target_properties(storm-cli-utilities PROPERTIES DEFINE_SYMBOL "") list(APPEND STORM_TARGETS storm-cli-utilities) set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) -target_link_libraries(storm-cli-utilities PUBLIC storm storm-counterexamples) +target_link_libraries(storm-cli-utilities PUBLIC storm storm-counterexamples storm-parsers) # Install storm headers to include directory. foreach(HEADER ${STORM_CLI_UTIL_HEADERS}) diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index b57818c08..41faf8732 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -3,6 +3,7 @@ #include "storm/api/storm.h" #include "storm-counterexamples/api/counterexamples.h" +#include "storm-parsers/api/storm-parsers.h" #include "storm/utility/resources.h" #include "storm/utility/file.h" diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index ce31be5b8..395985f7e 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -7,6 +7,8 @@ #include "storm/settings/modules/ResourceSettings.h" #include "storm/settings/modules/GeneralSettings.h" + +#include "storm-parsers/api/storm-parsers.h" #include "storm/utility/initialize.h" #include "storm-cli-utilities/cli.h" diff --git a/src/storm-dft/parser/DFTGalileoParser.h b/src/storm-dft/parser/DFTGalileoParser.h index c56540edd..f956d8cb9 100644 --- a/src/storm-dft/parser/DFTGalileoParser.h +++ b/src/storm-dft/parser/DFTGalileoParser.h @@ -3,12 +3,12 @@ #include <map> #include "storm/storage/expressions/ExpressionManager.h" -#include "storm/parser/ExpressionParser.h" +#include "storm-parsers/parser/ExpressionParser.h" #include "storm/storage/expressions/ExpressionEvaluator.h" #include "storm-dft/storage/dft/DFT.h" #include "storm-dft/builder/DFTBuilder.h" -#include "storm/parser/ValueParser.h" +#include "storm-parsers/parser/ValueParser.h" namespace storm { diff --git a/src/storm-dft/parser/DFTJsonParser.h b/src/storm-dft/parser/DFTJsonParser.h index 5517d85e1..3b6812a76 100644 --- a/src/storm-dft/parser/DFTJsonParser.h +++ b/src/storm-dft/parser/DFTJsonParser.h @@ -3,7 +3,7 @@ #include <map> #include "storm/storage/expressions/ExpressionManager.h" -#include "storm/parser/ExpressionParser.h" +#include "storm-parsers/parser/ExpressionParser.h" #include "storm/storage/expressions/ExpressionEvaluator.h" #include "storm-dft/storage/dft/DFT.h" diff --git a/src/storm-gspn-cli/storm-gspn.cpp b/src/storm-gspn-cli/storm-gspn.cpp index 602b353a0..99d60b0d7 100644 --- a/src/storm-gspn-cli/storm-gspn.cpp +++ b/src/storm-gspn-cli/storm-gspn.cpp @@ -14,7 +14,7 @@ #include "api/storm.h" #include "storm-cli-utilities/cli.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/jani/Model.h" diff --git a/src/storm-gspn/builder/ExplicitGspnModelBuilder.cpp b/src/storm-gspn/builder/ExplicitGspnModelBuilder.cpp index 1960a623a..23ba78594 100644 --- a/src/storm-gspn/builder/ExplicitGspnModelBuilder.cpp +++ b/src/storm-gspn/builder/ExplicitGspnModelBuilder.cpp @@ -5,7 +5,7 @@ //#include "storm/utility/macros.h" //#include "storm/exceptions/NotImplementedException.h" //#include "storm/storage/expressions/ExpressionManager.h" -//#include "storm/parser/FormulaParser.h" +//#include "storm-parsers/parser/FormulaParser.h" //#include "storm/storage/expressions/ExpressionEvaluator.h" // //namespace storm { diff --git a/src/storm-parsers/CMakeLists.txt b/src/storm-parsers/CMakeLists.txt new file mode 100644 index 000000000..d459345e4 --- /dev/null +++ b/src/storm-parsers/CMakeLists.txt @@ -0,0 +1,42 @@ +file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-parsers/*.h ${PROJECT_SOURCE_DIR}/src/storm-parsers/*.cpp) + +register_source_groups_from_filestructure("${ALL_FILES}" storm-parsers) + + + +file(GLOB_RECURSE STORM_PARSER_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-parsers/*/*.cpp) +file(GLOB_RECURSE STORM_PARSER_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-parsers/*/*.h) + + +# Disable Debug compiler flags for PrismParser to lessen memory consumption during compilation +SET_SOURCE_FILES_PROPERTIES(${PROJECT_SOURCE_DIR}/src/storm-parsers/parser/PrismParser.cpp PROPERTIES COMPILE_FLAGS -g0) +# Create storm-dft. +add_library(storm-parsers SHARED ${STORM_PARSER_SOURCES} ${STORM_PARSER_HEADERS}) + +# Remove define symbol for shared libstorm. +set_target_properties(storm-parsers PROPERTIES DEFINE_SYMBOL "") +#add_dependencies(storm resources) +list(APPEND STORM_TARGETS storm-parsers) +set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE) + +target_link_libraries(storm-parsers PUBLIC storm) + +# Install storm headers to include directory. +foreach(HEADER ${STORM_PARSER_HEADERS}) + string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER}) + string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH}) + string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH}) + add_custom_command( + OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} + COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY} + COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME} + DEPENDS ${HEADER} + ) + list(APPEND STORM_PARSER_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}") +endforeach() +add_custom_target(copy_storm_parser_headers DEPENDS ${STORM_PARSER_OUTPUT_HEADERS} ${STORM_PARSER_HEADERS}) +add_dependencies(storm-parsers copy_storm_parser_headers) + +# installation +install(TARGETS storm-parsers EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL) + diff --git a/src/storm/api/model_descriptions.cpp b/src/storm-parsers/api/model_descriptions.cpp similarity index 88% rename from src/storm/api/model_descriptions.cpp rename to src/storm-parsers/api/model_descriptions.cpp index 76ce24116..a440dffef 100644 --- a/src/storm/api/model_descriptions.cpp +++ b/src/storm-parsers/api/model_descriptions.cpp @@ -1,7 +1,7 @@ -#include "storm/api/model_descriptions.h" +#include "model_descriptions.h" -#include "storm/parser/PrismParser.h" -#include "storm/parser/JaniParser.h" +#include "storm-parsers/parser/PrismParser.h" +#include "storm-parsers/parser/JaniParser.h" #include "storm/storage/jani/Model.h" #include "storm/storage/jani/Property.h" diff --git a/src/storm/api/model_descriptions.h b/src/storm-parsers/api/model_descriptions.h similarity index 100% rename from src/storm/api/model_descriptions.h rename to src/storm-parsers/api/model_descriptions.h diff --git a/src/storm-parsers/api/properties.cpp b/src/storm-parsers/api/properties.cpp new file mode 100644 index 000000000..d5349544d --- /dev/null +++ b/src/storm-parsers/api/properties.cpp @@ -0,0 +1,71 @@ + + +#include "storm-parsers/parser/FormulaParser.h" +#include "storm/api/properties.h" + + +#include "storm/storage/SymbolicModelDescription.h" +#include "storm/storage/prism/Program.h" +#include "storm/storage/jani/Model.h" +#include "storm/storage/jani/Property.h" + +#include "storm/logic/Formula.h" + +#include "storm/utility/cli.h" + + +namespace storm { + namespace api { + + boost::optional <std::set<std::string>> parsePropertyFilter(std::string const &propertyFilter) { + if (propertyFilter == "all") { + return boost::none; + } + std::vector <std::string> propertyNames = storm::utility::cli::parseCommaSeparatedStrings(propertyFilter); + std::set <std::string> propertyNameSet(propertyNames.begin(), propertyNames.end()); + return propertyNameSet; + } + + std::vector <storm::jani::Property> parseProperties(storm::parser::FormulaParser &formulaParser, std::string const &inputString, boost::optional <std::set<std::string>> const &propertyFilter) { + // If the given property is a file, we parse it as a file, otherwise we assume it's a property. + std::vector <storm::jani::Property> properties; + if (std::ifstream(inputString).good()) { + STORM_LOG_INFO("Loading properties from file: " << inputString << std::endl); + properties = formulaParser.parseFromFile(inputString); + } else { + properties = formulaParser.parseFromString(inputString); + } + + return filterProperties(properties, propertyFilter); + } + + std::vector <storm::jani::Property> parseProperties(std::string const &inputString, boost::optional <std::set<std::string>> const &propertyFilter) { + auto exprManager = std::make_shared<storm::expressions::ExpressionManager>(); + storm::parser::FormulaParser formulaParser(exprManager); + return parseProperties(formulaParser, inputString, propertyFilter); + } + + std::vector <storm::jani::Property> parsePropertiesForJaniModel(std::string const &inputString, storm::jani::Model const &model, boost::optional <std::set<std::string>> const &propertyFilter) { + storm::parser::FormulaParser formulaParser(model.getManager().getSharedPointer()); + auto formulas = parseProperties(formulaParser, inputString, propertyFilter); + return substituteConstantsInProperties(formulas, model.getConstantsSubstitution()); + } + + std::vector <storm::jani::Property> parsePropertiesForPrismProgram(std::string const &inputString, storm::prism::Program const &program, boost::optional <std::set<std::string>> const &propertyFilter) { + storm::parser::FormulaParser formulaParser(program); + auto formulas = parseProperties(formulaParser, inputString, propertyFilter); + return substituteConstantsInProperties(formulas, program.getConstantsSubstitution()); + } + + std::vector <storm::jani::Property> parsePropertiesForSymbolicModelDescription(std::string const &inputString, storm::storage::SymbolicModelDescription const &modelDescription, boost::optional <std::set<std::string>> const &propertyFilter) { + std::vector <storm::jani::Property> result; + if (modelDescription.isPrismProgram()) { + result = storm::api::parsePropertiesForPrismProgram(inputString, modelDescription.asPrismProgram(), propertyFilter); + } else { + STORM_LOG_ASSERT(modelDescription.isJaniModel(), "Unknown model description type."); + result = storm::api::parsePropertiesForJaniModel(inputString, modelDescription.asJaniModel(), propertyFilter); + } + return result; + } + } +} \ No newline at end of file diff --git a/src/storm-parsers/api/properties.h b/src/storm-parsers/api/properties.h new file mode 100644 index 000000000..81d37d965 --- /dev/null +++ b/src/storm-parsers/api/properties.h @@ -0,0 +1,43 @@ +#pragma once + +#include <string> +#include <set> +#include <map> +#include <vector> +#include <memory> +#include <boost/optional.hpp> + +namespace storm { + namespace parser { + class FormulaParser; + } + namespace jani { + class Property; + class Model; + } + namespace expressions { + class Variable; + class Expression; + } + namespace prism { + class Program; + } + namespace storage { + class SymbolicModelDescription; + } + namespace logic { + class Formula; + } + + namespace api { + boost::optional<std::set<std::string>> parsePropertyFilter(std::string const& propertyFilter); + + // Parsing properties. + std::vector<storm::jani::Property> parseProperties(storm::parser::FormulaParser& formulaParser, std::string const& inputString, boost::optional<std::set<std::string>> const& propertyFilter = boost::none); + std::vector<storm::jani::Property> parseProperties(std::string const& inputString, boost::optional<std::set<std::string>> const& propertyFilter = boost::none); + std::vector<storm::jani::Property> parsePropertiesForPrismProgram(std::string const& inputString, storm::prism::Program const& program, boost::optional<std::set<std::string>> const& propertyFilter = boost::none); + std::vector<storm::jani::Property> parsePropertiesForJaniModel(std::string const& inputString, storm::jani::Model const& model, boost::optional<std::set<std::string>> const& propertyFilter = boost::none); + std::vector<storm::jani::Property> parsePropertiesForSymbolicModelDescription(std::string const& inputString, storm::storage::SymbolicModelDescription const& modelDescription, boost::optional<std::set<std::string>> const& propertyFilter = boost::none); + + } +} diff --git a/src/storm-parsers/api/storm-parsers.h b/src/storm-parsers/api/storm-parsers.h new file mode 100644 index 000000000..b88188976 --- /dev/null +++ b/src/storm-parsers/api/storm-parsers.h @@ -0,0 +1,4 @@ +#pragma once + +#include "storm-parsers/api/model_descriptions.h" +#include "storm-parsers/api/properties.h" \ No newline at end of file diff --git a/src/storm/parser/AtomicPropositionLabelingParser.cpp b/src/storm-parsers/parser/AtomicPropositionLabelingParser.cpp similarity index 98% rename from src/storm/parser/AtomicPropositionLabelingParser.cpp rename to src/storm-parsers/parser/AtomicPropositionLabelingParser.cpp index 4d55b4fe8..a8afc93d7 100644 --- a/src/storm/parser/AtomicPropositionLabelingParser.cpp +++ b/src/storm-parsers/parser/AtomicPropositionLabelingParser.cpp @@ -5,14 +5,14 @@ * Author: Gereon Kremer */ -#include "storm/parser/AtomicPropositionLabelingParser.h" +#include "storm-parsers/parser/AtomicPropositionLabelingParser.h" #include <cstring> #include <string> #include <iostream> #include "storm/utility/cstring.h" -#include "storm/parser/MappedFile.h" +#include "storm-parsers/parser/MappedFile.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/FileIoException.h" diff --git a/src/storm/parser/AtomicPropositionLabelingParser.h b/src/storm-parsers/parser/AtomicPropositionLabelingParser.h similarity index 100% rename from src/storm/parser/AtomicPropositionLabelingParser.h rename to src/storm-parsers/parser/AtomicPropositionLabelingParser.h diff --git a/src/storm/parser/AutoParser.cpp b/src/storm-parsers/parser/AutoParser.cpp similarity index 95% rename from src/storm/parser/AutoParser.cpp rename to src/storm-parsers/parser/AutoParser.cpp index 896c4215e..9e96af5e6 100644 --- a/src/storm/parser/AutoParser.cpp +++ b/src/storm-parsers/parser/AutoParser.cpp @@ -1,12 +1,12 @@ -#include "storm/parser/AutoParser.h" +#include "storm-parsers/parser/AutoParser.h" #include "storm/models/sparse/StandardRewardModel.h" -#include "storm/parser/MappedFile.h" +#include "storm-parsers/parser/MappedFile.h" -#include "storm/parser/DeterministicModelParser.h" -#include "storm/parser/NondeterministicModelParser.h" -#include "storm/parser/MarkovAutomatonParser.h" +#include "storm-parsers/parser/DeterministicModelParser.h" +#include "storm-parsers/parser/NondeterministicModelParser.h" +#include "storm-parsers/parser/MarkovAutomatonParser.h" #include "storm/utility/macros.h" #include "storm/exceptions/WrongFormatException.h" diff --git a/src/storm/parser/AutoParser.h b/src/storm-parsers/parser/AutoParser.h similarity index 100% rename from src/storm/parser/AutoParser.h rename to src/storm-parsers/parser/AutoParser.h diff --git a/src/storm/parser/DeterministicModelParser.cpp b/src/storm-parsers/parser/DeterministicModelParser.cpp similarity index 95% rename from src/storm/parser/DeterministicModelParser.cpp rename to src/storm-parsers/parser/DeterministicModelParser.cpp index cfe5a16df..6b81c0630 100644 --- a/src/storm/parser/DeterministicModelParser.cpp +++ b/src/storm-parsers/parser/DeterministicModelParser.cpp @@ -1,13 +1,13 @@ -#include "storm/parser/DeterministicModelParser.h" +#include "storm-parsers/parser/DeterministicModelParser.h" #include <string> #include <vector> #include "storm/models/sparse/StandardRewardModel.h" -#include "storm/parser/DeterministicSparseTransitionParser.h" -#include "storm/parser/SparseItemLabelingParser.h" -#include "storm/parser/SparseStateRewardParser.h" +#include "storm-parsers/parser/DeterministicSparseTransitionParser.h" +#include "storm-parsers/parser/SparseItemLabelingParser.h" +#include "storm-parsers/parser/SparseStateRewardParser.h" #include "storm/adapters/RationalFunctionAdapter.h" diff --git a/src/storm/parser/DeterministicModelParser.h b/src/storm-parsers/parser/DeterministicModelParser.h similarity index 100% rename from src/storm/parser/DeterministicModelParser.h rename to src/storm-parsers/parser/DeterministicModelParser.h diff --git a/src/storm/parser/DeterministicSparseTransitionParser.cpp b/src/storm-parsers/parser/DeterministicSparseTransitionParser.cpp similarity index 99% rename from src/storm/parser/DeterministicSparseTransitionParser.cpp rename to src/storm-parsers/parser/DeterministicSparseTransitionParser.cpp index 540371f74..229cc3c2e 100644 --- a/src/storm/parser/DeterministicSparseTransitionParser.cpp +++ b/src/storm-parsers/parser/DeterministicSparseTransitionParser.cpp @@ -1,4 +1,4 @@ -#include "storm/parser/DeterministicSparseTransitionParser.h" +#include "storm-parsers/parser/DeterministicSparseTransitionParser.h" #include <cstdio> #include <cstring> @@ -9,7 +9,7 @@ #include "storm/utility/constants.h" #include "storm/utility/cstring.h" -#include "storm/parser/MappedFile.h" +#include "storm-parsers/parser/MappedFile.h" #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/InvalidArgumentException.h" diff --git a/src/storm/parser/DeterministicSparseTransitionParser.h b/src/storm-parsers/parser/DeterministicSparseTransitionParser.h similarity index 100% rename from src/storm/parser/DeterministicSparseTransitionParser.h rename to src/storm-parsers/parser/DeterministicSparseTransitionParser.h diff --git a/src/storm/parser/DirectEncodingParser.cpp b/src/storm-parsers/parser/DirectEncodingParser.cpp similarity index 99% rename from src/storm/parser/DirectEncodingParser.cpp rename to src/storm-parsers/parser/DirectEncodingParser.cpp index 93d8a60f2..da4cd5228 100644 --- a/src/storm/parser/DirectEncodingParser.cpp +++ b/src/storm-parsers/parser/DirectEncodingParser.cpp @@ -1,4 +1,4 @@ -#include "storm/parser/DirectEncodingParser.h" +#include "storm-parsers/parser/DirectEncodingParser.h" #include <iostream> #include <string> diff --git a/src/storm/parser/DirectEncodingParser.h b/src/storm-parsers/parser/DirectEncodingParser.h similarity index 97% rename from src/storm/parser/DirectEncodingParser.h rename to src/storm-parsers/parser/DirectEncodingParser.h index 456445e1c..f025b8dfc 100644 --- a/src/storm/parser/DirectEncodingParser.h +++ b/src/storm-parsers/parser/DirectEncodingParser.h @@ -1,7 +1,7 @@ #ifndef STORM_PARSER_DIRECTENCODINGPARSER_H_ #define STORM_PARSER_DIRECTENCODINGPARSER_H_ -#include "storm/parser/ValueParser.h" +#include "storm-parsers/parser/ValueParser.h" #include "storm/models/sparse/Model.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/storage/sparse/ModelComponents.h" diff --git a/src/storm/parser/ExpressionCreator.cpp b/src/storm-parsers/parser/ExpressionCreator.cpp similarity index 100% rename from src/storm/parser/ExpressionCreator.cpp rename to src/storm-parsers/parser/ExpressionCreator.cpp diff --git a/src/storm/parser/ExpressionCreator.h b/src/storm-parsers/parser/ExpressionCreator.h similarity index 98% rename from src/storm/parser/ExpressionCreator.h rename to src/storm-parsers/parser/ExpressionCreator.h index 20bcc5854..814dc964a 100644 --- a/src/storm/parser/ExpressionCreator.h +++ b/src/storm-parsers/parser/ExpressionCreator.h @@ -1,7 +1,7 @@ #pragma once #include <memory> // Very ugly, but currently we would like to have the symbol table here. -#include "storm/parser/SpiritParserDefinitions.h" +#include "storm-parsers/parser/SpiritParserDefinitions.h" #include <boost/optional.hpp> #include "storm/adapters/RationalNumberAdapter.h" diff --git a/src/storm/parser/ExpressionParser.cpp b/src/storm-parsers/parser/ExpressionParser.cpp similarity index 99% rename from src/storm/parser/ExpressionParser.cpp rename to src/storm-parsers/parser/ExpressionParser.cpp index 64e185b54..d1d6dcaf0 100644 --- a/src/storm/parser/ExpressionParser.cpp +++ b/src/storm-parsers/parser/ExpressionParser.cpp @@ -1,10 +1,10 @@ -#include "storm/parser/ExpressionParser.h" +#include "storm-parsers/parser/ExpressionParser.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/InvalidTypeException.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/utility/constants.h" -#include "storm/parser/ExpressionCreator.h" +#include "storm-parsers/parser/ExpressionCreator.h" #include "storm/storage/expressions/Expression.h" diff --git a/src/storm/parser/ExpressionParser.h b/src/storm-parsers/parser/ExpressionParser.h similarity index 99% rename from src/storm/parser/ExpressionParser.h rename to src/storm-parsers/parser/ExpressionParser.h index cb415c53e..4fa075adc 100644 --- a/src/storm/parser/ExpressionParser.h +++ b/src/storm-parsers/parser/ExpressionParser.h @@ -2,8 +2,8 @@ #include <sstream> -#include "storm/parser/SpiritParserDefinitions.h" -#include "storm/parser/SpiritErrorHandler.h" +#include "storm-parsers/parser/SpiritParserDefinitions.h" +#include "storm-parsers/parser/SpiritErrorHandler.h" #include "storm/storage/expressions/OperatorType.h" #include "storm/adapters/RationalNumberAdapter.h" diff --git a/src/storm/parser/FormulaParser.cpp b/src/storm-parsers/parser/FormulaParser.cpp similarity index 98% rename from src/storm/parser/FormulaParser.cpp rename to src/storm-parsers/parser/FormulaParser.cpp index d8b9c2df2..0f44d469b 100644 --- a/src/storm/parser/FormulaParser.cpp +++ b/src/storm-parsers/parser/FormulaParser.cpp @@ -1,8 +1,8 @@ -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include <fstream> -#include "storm/parser/SpiritErrorHandler.h" +#include "storm-parsers/parser/SpiritErrorHandler.h" #include "storm/storage/prism/Program.h" diff --git a/src/storm/parser/FormulaParser.h b/src/storm-parsers/parser/FormulaParser.h similarity index 96% rename from src/storm/parser/FormulaParser.h rename to src/storm-parsers/parser/FormulaParser.h index d9c06fa92..49c78a720 100644 --- a/src/storm/parser/FormulaParser.h +++ b/src/storm-parsers/parser/FormulaParser.h @@ -3,8 +3,8 @@ #include <sstream> -#include "storm/parser/SpiritParserDefinitions.h" -#include "storm/parser/ExpressionParser.h" +#include "storm-parsers/parser/SpiritParserDefinitions.h" +#include "storm-parsers/parser/ExpressionParser.h" #include "storm/storage/jani/Property.h" #include "storm/storage/expressions/Expression.h" #include "storm/utility/macros.h" diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp similarity index 100% rename from src/storm/parser/FormulaParserGrammar.cpp rename to src/storm-parsers/parser/FormulaParserGrammar.cpp diff --git a/src/storm/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h similarity index 99% rename from src/storm/parser/FormulaParserGrammar.h rename to src/storm-parsers/parser/FormulaParserGrammar.h index dd9a3a06f..c9d5ae020 100644 --- a/src/storm/parser/FormulaParserGrammar.h +++ b/src/storm-parsers/parser/FormulaParserGrammar.h @@ -3,11 +3,11 @@ #include <memory> #include <fstream> -#include "storm/parser/SpiritErrorHandler.h" +#include "storm-parsers/parser/SpiritErrorHandler.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/storage/jani/Property.h" #include "storm/logic/Formulas.h" -#include "storm/parser/ExpressionParser.h" +#include "storm-parsers/parser/ExpressionParser.h" #include "storm/modelchecker/results/FilterType.h" diff --git a/src/storm/parser/ImcaMarkovAutomatonParser.cpp b/src/storm-parsers/parser/ImcaMarkovAutomatonParser.cpp similarity index 99% rename from src/storm/parser/ImcaMarkovAutomatonParser.cpp rename to src/storm-parsers/parser/ImcaMarkovAutomatonParser.cpp index f55d09219..0cbf917f1 100644 --- a/src/storm/parser/ImcaMarkovAutomatonParser.cpp +++ b/src/storm-parsers/parser/ImcaMarkovAutomatonParser.cpp @@ -1,4 +1,4 @@ -#include "storm/parser/ImcaMarkovAutomatonParser.h" +#include "storm-parsers/parser/ImcaMarkovAutomatonParser.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/BuildSettings.h" diff --git a/src/storm/parser/ImcaMarkovAutomatonParser.h b/src/storm-parsers/parser/ImcaMarkovAutomatonParser.h similarity index 98% rename from src/storm/parser/ImcaMarkovAutomatonParser.h rename to src/storm-parsers/parser/ImcaMarkovAutomatonParser.h index f2820242e..b5c7beded 100644 --- a/src/storm/parser/ImcaMarkovAutomatonParser.h +++ b/src/storm-parsers/parser/ImcaMarkovAutomatonParser.h @@ -7,7 +7,7 @@ #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/generator/StateBehavior.h" -#include "storm/parser/SpiritErrorHandler.h" +#include "storm-parsers/parser/SpiritErrorHandler.h" namespace storm { namespace parser { diff --git a/src/storm/parser/JaniParser.cpp b/src/storm-parsers/parser/JaniParser.cpp similarity index 100% rename from src/storm/parser/JaniParser.cpp rename to src/storm-parsers/parser/JaniParser.cpp diff --git a/src/storm/parser/JaniParser.h b/src/storm-parsers/parser/JaniParser.h similarity index 100% rename from src/storm/parser/JaniParser.h rename to src/storm-parsers/parser/JaniParser.h diff --git a/src/storm/parser/KeyValueParser.cpp b/src/storm-parsers/parser/KeyValueParser.cpp similarity index 100% rename from src/storm/parser/KeyValueParser.cpp rename to src/storm-parsers/parser/KeyValueParser.cpp diff --git a/src/storm/parser/KeyValueParser.h b/src/storm-parsers/parser/KeyValueParser.h similarity index 100% rename from src/storm/parser/KeyValueParser.h rename to src/storm-parsers/parser/KeyValueParser.h diff --git a/src/storm/parser/MappedFile.cpp b/src/storm-parsers/parser/MappedFile.cpp similarity index 98% rename from src/storm/parser/MappedFile.cpp rename to src/storm-parsers/parser/MappedFile.cpp index 5b9f02714..d28e8e927 100644 --- a/src/storm/parser/MappedFile.cpp +++ b/src/storm-parsers/parser/MappedFile.cpp @@ -5,7 +5,7 @@ * Author: Manuel Sascha Weiand */ -#include "storm/parser/MappedFile.h" +#include "storm-parsers/parser/MappedFile.h" #include <fstream> #include <cstring> diff --git a/src/storm/parser/MappedFile.h b/src/storm-parsers/parser/MappedFile.h similarity index 100% rename from src/storm/parser/MappedFile.h rename to src/storm-parsers/parser/MappedFile.h diff --git a/src/storm/parser/MarkovAutomatonParser.cpp b/src/storm-parsers/parser/MarkovAutomatonParser.cpp similarity index 100% rename from src/storm/parser/MarkovAutomatonParser.cpp rename to src/storm-parsers/parser/MarkovAutomatonParser.cpp diff --git a/src/storm/parser/MarkovAutomatonParser.h b/src/storm-parsers/parser/MarkovAutomatonParser.h similarity index 96% rename from src/storm/parser/MarkovAutomatonParser.h rename to src/storm-parsers/parser/MarkovAutomatonParser.h index 763ece141..1f2087674 100644 --- a/src/storm/parser/MarkovAutomatonParser.h +++ b/src/storm-parsers/parser/MarkovAutomatonParser.h @@ -2,7 +2,7 @@ #define STORM_PARSER_MARKOVAUTOMATONPARSER_H_ #include "storm/models/sparse/MarkovAutomaton.h" -#include "storm/parser/MarkovAutomatonSparseTransitionParser.h" +#include "storm-parsers/parser/MarkovAutomatonSparseTransitionParser.h" namespace storm { namespace parser { diff --git a/src/storm/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/storm-parsers/parser/MarkovAutomatonSparseTransitionParser.cpp similarity index 99% rename from src/storm/parser/MarkovAutomatonSparseTransitionParser.cpp rename to src/storm-parsers/parser/MarkovAutomatonSparseTransitionParser.cpp index 25b62a2e2..9acd151b0 100644 --- a/src/storm/parser/MarkovAutomatonSparseTransitionParser.cpp +++ b/src/storm-parsers/parser/MarkovAutomatonSparseTransitionParser.cpp @@ -4,7 +4,7 @@ #include "storm/settings/modules/CoreSettings.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/FileIoException.h" -#include "storm/parser/MappedFile.h" +#include "storm-parsers/parser/MappedFile.h" #include "storm/utility/cstring.h" #include "storm/utility/constants.h" #include "storm/utility/macros.h" diff --git a/src/storm/parser/MarkovAutomatonSparseTransitionParser.h b/src/storm-parsers/parser/MarkovAutomatonSparseTransitionParser.h similarity index 100% rename from src/storm/parser/MarkovAutomatonSparseTransitionParser.h rename to src/storm-parsers/parser/MarkovAutomatonSparseTransitionParser.h diff --git a/src/storm/parser/NondeterministicModelParser.cpp b/src/storm-parsers/parser/NondeterministicModelParser.cpp similarity index 93% rename from src/storm/parser/NondeterministicModelParser.cpp rename to src/storm-parsers/parser/NondeterministicModelParser.cpp index c107803eb..b26626fb0 100644 --- a/src/storm/parser/NondeterministicModelParser.cpp +++ b/src/storm-parsers/parser/NondeterministicModelParser.cpp @@ -1,13 +1,13 @@ -#include "storm/parser/NondeterministicModelParser.h" +#include "storm-parsers/parser/NondeterministicModelParser.h" #include <string> #include <vector> #include "storm/models/sparse/StandardRewardModel.h" -#include "storm/parser/NondeterministicSparseTransitionParser.h" -#include "storm/parser/SparseItemLabelingParser.h" -#include "storm/parser/SparseStateRewardParser.h" +#include "storm-parsers/parser/NondeterministicSparseTransitionParser.h" +#include "storm-parsers/parser/SparseItemLabelingParser.h" +#include "storm-parsers/parser/SparseStateRewardParser.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/macros.h" diff --git a/src/storm/parser/NondeterministicModelParser.h b/src/storm-parsers/parser/NondeterministicModelParser.h similarity index 100% rename from src/storm/parser/NondeterministicModelParser.h rename to src/storm-parsers/parser/NondeterministicModelParser.h diff --git a/src/storm/parser/NondeterministicSparseTransitionParser.cpp b/src/storm-parsers/parser/NondeterministicSparseTransitionParser.cpp similarity index 99% rename from src/storm/parser/NondeterministicSparseTransitionParser.cpp rename to src/storm-parsers/parser/NondeterministicSparseTransitionParser.cpp index cb941aec5..56b00070c 100644 --- a/src/storm/parser/NondeterministicSparseTransitionParser.cpp +++ b/src/storm-parsers/parser/NondeterministicSparseTransitionParser.cpp @@ -1,8 +1,8 @@ -#include "storm/parser/NondeterministicSparseTransitionParser.h" +#include "storm-parsers/parser/NondeterministicSparseTransitionParser.h" #include <string> -#include "storm/parser/MappedFile.h" +#include "storm-parsers/parser/MappedFile.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/CoreSettings.h" #include "storm/exceptions/FileIoException.h" diff --git a/src/storm/parser/NondeterministicSparseTransitionParser.h b/src/storm-parsers/parser/NondeterministicSparseTransitionParser.h similarity index 100% rename from src/storm/parser/NondeterministicSparseTransitionParser.h rename to src/storm-parsers/parser/NondeterministicSparseTransitionParser.h diff --git a/src/storm/parser/PrismParser.cpp b/src/storm-parsers/parser/PrismParser.cpp similarity index 99% rename from src/storm/parser/PrismParser.cpp rename to src/storm-parsers/parser/PrismParser.cpp index ca59981cb..5d76736f7 100644 --- a/src/storm/parser/PrismParser.cpp +++ b/src/storm-parsers/parser/PrismParser.cpp @@ -1,4 +1,4 @@ -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/storage/prism/Compositions.h" @@ -11,7 +11,7 @@ #include "storm/storage/expressions/ExpressionManager.h" -#include "storm/parser/ExpressionParser.h" +#include "storm-parsers/parser/ExpressionParser.h" namespace storm { namespace parser { diff --git a/src/storm/parser/PrismParser.h b/src/storm-parsers/parser/PrismParser.h similarity index 99% rename from src/storm/parser/PrismParser.h rename to src/storm-parsers/parser/PrismParser.h index fe7f0bc83..38a112e9d 100644 --- a/src/storm/parser/PrismParser.h +++ b/src/storm-parsers/parser/PrismParser.h @@ -6,8 +6,8 @@ #include <memory> #include <iomanip> -#include "storm/parser/SpiritParserDefinitions.h" -#include "storm/parser/SpiritErrorHandler.h" +#include "storm-parsers/parser/SpiritParserDefinitions.h" +#include "storm-parsers/parser/SpiritErrorHandler.h" #include "storm/storage/prism/Program.h" #include "storm/storage/expressions/Expression.h" diff --git a/src/storm/parser/ReadValues.h b/src/storm-parsers/parser/ReadValues.h similarity index 100% rename from src/storm/parser/ReadValues.h rename to src/storm-parsers/parser/ReadValues.h diff --git a/src/storm/parser/SparseChoiceLabelingParser.cpp b/src/storm-parsers/parser/SparseChoiceLabelingParser.cpp similarity index 97% rename from src/storm/parser/SparseChoiceLabelingParser.cpp rename to src/storm-parsers/parser/SparseChoiceLabelingParser.cpp index b51e8b97c..452045319 100644 --- a/src/storm/parser/SparseChoiceLabelingParser.cpp +++ b/src/storm-parsers/parser/SparseChoiceLabelingParser.cpp @@ -1,10 +1,10 @@ -#include "storm/parser/SparseChoiceLabelingParser.h" +#include "storm-parsers/parser/SparseChoiceLabelingParser.h" #include "storm/utility/macros.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/OutOfRangeException.h" #include "storm/exceptions/FileIoException.h" -#include "storm/parser/MappedFile.h" +#include "storm-parsers/parser/MappedFile.h" #include "storm/utility/cstring.h" namespace storm { diff --git a/src/storm/parser/SparseChoiceLabelingParser.h b/src/storm-parsers/parser/SparseChoiceLabelingParser.h similarity index 100% rename from src/storm/parser/SparseChoiceLabelingParser.h rename to src/storm-parsers/parser/SparseChoiceLabelingParser.h diff --git a/src/storm/parser/SparseItemLabelingParser.cpp b/src/storm-parsers/parser/SparseItemLabelingParser.cpp similarity index 99% rename from src/storm/parser/SparseItemLabelingParser.cpp rename to src/storm-parsers/parser/SparseItemLabelingParser.cpp index 2e98e4673..9e5e7b154 100644 --- a/src/storm/parser/SparseItemLabelingParser.cpp +++ b/src/storm-parsers/parser/SparseItemLabelingParser.cpp @@ -1,11 +1,11 @@ -#include "storm/parser/SparseItemLabelingParser.h" +#include "storm-parsers/parser/SparseItemLabelingParser.h" #include <cstring> #include <string> #include <iostream> #include "storm/utility/cstring.h" -#include "storm/parser/MappedFile.h" +#include "storm-parsers/parser/MappedFile.h" #include "storm/utility/macros.h" #include "storm/exceptions/WrongFormatException.h" diff --git a/src/storm/parser/SparseItemLabelingParser.h b/src/storm-parsers/parser/SparseItemLabelingParser.h similarity index 98% rename from src/storm/parser/SparseItemLabelingParser.h rename to src/storm-parsers/parser/SparseItemLabelingParser.h index 4b901ab82..97c30cc25 100644 --- a/src/storm/parser/SparseItemLabelingParser.h +++ b/src/storm-parsers/parser/SparseItemLabelingParser.h @@ -4,7 +4,7 @@ #include <cstdint> #include <boost/optional.hpp> -#include "storm/parser/MappedFile.h" +#include "storm-parsers/parser/MappedFile.h" #include "storm/models/sparse/StateLabeling.h" #include "storm/models/sparse/ChoiceLabeling.h" diff --git a/src/storm/parser/SparseStateRewardParser.cpp b/src/storm-parsers/parser/SparseStateRewardParser.cpp similarity index 96% rename from src/storm/parser/SparseStateRewardParser.cpp rename to src/storm-parsers/parser/SparseStateRewardParser.cpp index f42b4cbe8..acb67e9fb 100644 --- a/src/storm/parser/SparseStateRewardParser.cpp +++ b/src/storm-parsers/parser/SparseStateRewardParser.cpp @@ -1,11 +1,11 @@ #include <iostream> -#include "storm/parser/SparseStateRewardParser.h" +#include "storm-parsers/parser/SparseStateRewardParser.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/OutOfRangeException.h" #include "storm/exceptions/FileIoException.h" #include "storm/utility/cstring.h" -#include "storm/parser/MappedFile.h" +#include "storm-parsers/parser/MappedFile.h" #include "storm/adapters/RationalFunctionAdapter.h" #include "storm/utility/macros.h" diff --git a/src/storm/parser/SparseStateRewardParser.h b/src/storm-parsers/parser/SparseStateRewardParser.h similarity index 100% rename from src/storm/parser/SparseStateRewardParser.h rename to src/storm-parsers/parser/SparseStateRewardParser.h diff --git a/src/storm/parser/SpiritErrorHandler.h b/src/storm-parsers/parser/SpiritErrorHandler.h similarity index 95% rename from src/storm/parser/SpiritErrorHandler.h rename to src/storm-parsers/parser/SpiritErrorHandler.h index 34280e422..ab64008bc 100644 --- a/src/storm/parser/SpiritErrorHandler.h +++ b/src/storm-parsers/parser/SpiritErrorHandler.h @@ -1,6 +1,6 @@ #pragma once -#include "storm/parser/SpiritParserDefinitions.h" +#include "storm-parsers/parser/SpiritParserDefinitions.h" #include "storm/utility/macros.h" #include "storm/exceptions/WrongFormatException.h" diff --git a/src/storm/parser/SpiritParserDefinitions.h b/src/storm-parsers/parser/SpiritParserDefinitions.h similarity index 100% rename from src/storm/parser/SpiritParserDefinitions.h rename to src/storm-parsers/parser/SpiritParserDefinitions.h diff --git a/src/storm/parser/ValueParser.cpp b/src/storm-parsers/parser/ValueParser.cpp similarity index 96% rename from src/storm/parser/ValueParser.cpp rename to src/storm-parsers/parser/ValueParser.cpp index 17495b0d9..61cd5c0ac 100644 --- a/src/storm/parser/ValueParser.cpp +++ b/src/storm-parsers/parser/ValueParser.cpp @@ -1,4 +1,4 @@ -#include "storm/parser/ValueParser.h" +#include "storm-parsers/parser/ValueParser.h" #include "storm/exceptions/NotSupportedException.h" diff --git a/src/storm/parser/ValueParser.h b/src/storm-parsers/parser/ValueParser.h similarity index 97% rename from src/storm/parser/ValueParser.h rename to src/storm-parsers/parser/ValueParser.h index db948b75e..626857a3e 100644 --- a/src/storm/parser/ValueParser.h +++ b/src/storm-parsers/parser/ValueParser.h @@ -2,7 +2,7 @@ #define STORM_PARSER_VALUEPARSER_H_ #include "storm/storage/expressions/ExpressionManager.h" -#include "storm/parser/ExpressionParser.h" +#include "storm-parsers/parser/ExpressionParser.h" #include "storm/storage/expressions/ExpressionEvaluator.h" #include "storm/exceptions/WrongFormatException.h" diff --git a/src/storm-pgcl/parser/PgclParser.h b/src/storm-pgcl/parser/PgclParser.h index dfd75a810..0e31094b9 100755 --- a/src/storm-pgcl/parser/PgclParser.h +++ b/src/storm-pgcl/parser/PgclParser.h @@ -5,9 +5,9 @@ #include <memory> #include <iomanip> // Includes files for building and parsing the PGCL program -#include "storm/parser/SpiritParserDefinitions.h" -#include "storm/parser/SpiritErrorHandler.h" -#include "storm/parser/ExpressionParser.h" +#include "storm-parsers/parser/SpiritParserDefinitions.h" +#include "storm-parsers/parser/SpiritErrorHandler.h" +#include "storm-parsers/parser/ExpressionParser.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/expressions/Expression.h" #include "storm-pgcl/storage/pgcl/PgclProgram.h" diff --git a/src/storm/CMakeLists.txt b/src/storm/CMakeLists.txt index 6a8cda64e..dcd1bb9f9 100644 --- a/src/storm/CMakeLists.txt +++ b/src/storm/CMakeLists.txt @@ -28,8 +28,6 @@ if (ADDITIONAL_LINK_DIRS) link_directories(${ADDITIONAL_LINK_DIRS}) endif(ADDITIONAL_LINK_DIRS) -# Disable Debug compiler flags for PrismParser to lessen memory consumption during compilation -SET_SOURCE_FILES_PROPERTIES(${PROJECT_SOURCE_DIR}/src/storm/parser/PrismParser.cpp PROPERTIES COMPILE_FLAGS -g0) ############################################################################### ## diff --git a/src/storm/api/builder.h b/src/storm/api/builder.h index 715e6e1ac..8aa2e2e17 100644 --- a/src/storm/api/builder.h +++ b/src/storm/api/builder.h @@ -1,8 +1,8 @@ #pragma once -#include "storm/parser/AutoParser.h" -#include "storm/parser/DirectEncodingParser.h" -#include "storm/parser/ImcaMarkovAutomatonParser.h" +#include "storm-parsers/parser/AutoParser.h" +#include "storm-parsers/parser/DirectEncodingParser.h" +#include "storm-parsers/parser/ImcaMarkovAutomatonParser.h" #include "storm/storage/SymbolicModelDescription.h" diff --git a/src/storm/api/properties.cpp b/src/storm/api/properties.cpp index 163679013..e5010d8b9 100644 --- a/src/storm/api/properties.cpp +++ b/src/storm/api/properties.cpp @@ -1,6 +1,5 @@ #include "storm/api/properties.h" -#include "storm/parser/FormulaParser.h" #include "storm/storage/SymbolicModelDescription.h" #include "storm/storage/prism/Program.h" @@ -13,57 +12,7 @@ namespace storm { namespace api { - - boost::optional<std::set<std::string>> parsePropertyFilter(std::string const& propertyFilter) { - if (propertyFilter == "all") { - return boost::none; - } - std::vector<std::string> propertyNames = storm::utility::cli::parseCommaSeparatedStrings(propertyFilter); - std::set<std::string> propertyNameSet(propertyNames.begin(), propertyNames.end()); - return propertyNameSet; - } - std::vector<storm::jani::Property> parseProperties(storm::parser::FormulaParser& formulaParser, std::string const& inputString, boost::optional<std::set<std::string>> const& propertyFilter) { - // If the given property is a file, we parse it as a file, otherwise we assume it's a property. - std::vector<storm::jani::Property> properties; - if (std::ifstream(inputString).good()) { - STORM_LOG_INFO("Loading properties from file: " << inputString << std::endl); - properties = formulaParser.parseFromFile(inputString); - } else { - properties = formulaParser.parseFromString(inputString); - } - - return filterProperties(properties, propertyFilter); - } - - std::vector<storm::jani::Property> parseProperties(std::string const& inputString, boost::optional<std::set<std::string>> const& propertyFilter) { - auto exprManager = std::make_shared<storm::expressions::ExpressionManager>(); - storm::parser::FormulaParser formulaParser(exprManager); - return parseProperties(formulaParser, inputString, propertyFilter); - } - - std::vector<storm::jani::Property> parsePropertiesForJaniModel(std::string const& inputString, storm::jani::Model const& model, boost::optional<std::set<std::string>> const& propertyFilter) { - storm::parser::FormulaParser formulaParser(model.getManager().getSharedPointer()); - auto formulas = parseProperties(formulaParser, inputString, propertyFilter); - return substituteConstantsInProperties(formulas, model.getConstantsSubstitution()); - } - - std::vector<storm::jani::Property> parsePropertiesForPrismProgram(std::string const& inputString, storm::prism::Program const& program, boost::optional<std::set<std::string>> const& propertyFilter) { - storm::parser::FormulaParser formulaParser(program); - auto formulas = parseProperties(formulaParser, inputString, propertyFilter); - return substituteConstantsInProperties(formulas, program.getConstantsSubstitution()); - } - - std::vector<storm::jani::Property> parsePropertiesForSymbolicModelDescription(std::string const& inputString, storm::storage::SymbolicModelDescription const& modelDescription, boost::optional<std::set<std::string>> const& propertyFilter) { - std::vector<storm::jani::Property> result; - if (modelDescription.isPrismProgram()) { - result = storm::api::parsePropertiesForPrismProgram(inputString, modelDescription.asPrismProgram(), propertyFilter); - } else { - STORM_LOG_ASSERT(modelDescription.isJaniModel(), "Unknown model description type."); - result = storm::api::parsePropertiesForJaniModel(inputString, modelDescription.asJaniModel(), propertyFilter); - } - return result; - } std::vector<storm::jani::Property> substituteConstantsInProperties(std::vector<storm::jani::Property> const& properties, std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) { std::vector<storm::jani::Property> preprocessedProperties; diff --git a/src/storm/api/properties.h b/src/storm/api/properties.h index c52073105..c0c878f48 100644 --- a/src/storm/api/properties.h +++ b/src/storm/api/properties.h @@ -8,9 +8,7 @@ #include <boost/optional.hpp> namespace storm { - namespace parser { - class FormulaParser; - } + namespace jani { class Property; class Model; @@ -30,14 +28,6 @@ namespace storm { } namespace api { - boost::optional<std::set<std::string>> parsePropertyFilter(std::string const& propertyFilter); - - // Parsing properties. - std::vector<storm::jani::Property> parseProperties(storm::parser::FormulaParser& formulaParser, std::string const& inputString, boost::optional<std::set<std::string>> const& propertyFilter = boost::none); - std::vector<storm::jani::Property> parseProperties(std::string const& inputString, boost::optional<std::set<std::string>> const& propertyFilter = boost::none); - std::vector<storm::jani::Property> parsePropertiesForPrismProgram(std::string const& inputString, storm::prism::Program const& program, boost::optional<std::set<std::string>> const& propertyFilter = boost::none); - std::vector<storm::jani::Property> parsePropertiesForJaniModel(std::string const& inputString, storm::jani::Model const& model, boost::optional<std::set<std::string>> const& propertyFilter = boost::none); - std::vector<storm::jani::Property> parsePropertiesForSymbolicModelDescription(std::string const& inputString, storm::storage::SymbolicModelDescription const& modelDescription, boost::optional<std::set<std::string>> const& propertyFilter = boost::none); // Process properties. std::vector<storm::jani::Property> substituteConstantsInProperties(std::vector<storm::jani::Property> const& properties, std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution); diff --git a/src/storm/api/storm.h b/src/storm/api/storm.h index d8f6aed82..0048bc315 100644 --- a/src/storm/api/storm.h +++ b/src/storm/api/storm.h @@ -1,6 +1,5 @@ #pragma once -#include "storm/api/model_descriptions.h" #include "storm/api/properties.h" #include "storm/api/builder.h" #include "storm/api/bisimulation.h" diff --git a/src/test/storm-pars/CMakeLists.txt b/src/test/storm-pars/CMakeLists.txt index 0f2793553..28c5a391d 100644 --- a/src/test/storm-pars/CMakeLists.txt +++ b/src/test/storm-pars/CMakeLists.txt @@ -13,7 +13,7 @@ foreach (testsuite modelchecker utility) file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp) add_executable (test-pars-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp) - target_link_libraries(test-pars-${testsuite} storm-pars) + target_link_libraries(test-pars-${testsuite} storm-pars storm-parsers) target_link_libraries(test-pars-${testsuite} ${STORM_TEST_LINK_LIBRARIES}) add_dependencies(test-pars-${testsuite} test-resources) diff --git a/src/test/storm-pars/modelchecker/ParametricDtmcPrctlModelCheckerTest.cpp b/src/test/storm-pars/modelchecker/ParametricDtmcPrctlModelCheckerTest.cpp index cf30285c5..91e08d2cf 100644 --- a/src/test/storm-pars/modelchecker/ParametricDtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm-pars/modelchecker/ParametricDtmcPrctlModelCheckerTest.cpp @@ -2,13 +2,13 @@ #include "storm-config.h" #include "test/storm_gtest.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/Formulas.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" -#include "storm/parser/AutoParser.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/AutoParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/api/builder.h" diff --git a/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp b/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp index dd6d59cf8..94bedf559 100644 --- a/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp +++ b/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp @@ -8,6 +8,8 @@ #include "storm-pars/api/storm-pars.h" #include "storm/api/storm.h" +#include "storm-parsers/api/storm-parsers.h" + #include "storm/environment/solver/MinMaxSolverEnvironment.h" namespace { diff --git a/src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp b/src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp index 3d3c97caa..48e71fd0b 100644 --- a/src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp +++ b/src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp @@ -8,6 +8,8 @@ #include "storm-pars/api/storm-pars.h" #include "storm/api/storm.h" +#include "storm-parsers/api/storm-parsers.h" + #include "storm/environment/solver/MinMaxSolverEnvironment.h" namespace { diff --git a/src/test/storm-pars/modelchecker/SymbolicParametricDtmcPrctlModelCheckerTest.cpp b/src/test/storm-pars/modelchecker/SymbolicParametricDtmcPrctlModelCheckerTest.cpp index de5e6f849..f23a23e4a 100644 --- a/src/test/storm-pars/modelchecker/SymbolicParametricDtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm-pars/modelchecker/SymbolicParametricDtmcPrctlModelCheckerTest.cpp @@ -1,7 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/Formulas.h" #include "storm/utility/solver.h" #include "storm/storage/SymbolicModelDescription.h" @@ -9,7 +9,7 @@ #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h" #include "storm/solver/SymbolicEliminationLinearEquationSolver.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/builder/DdPrismModelBuilder.h" #include "storm/models/symbolic/StandardRewardModel.h" #include "storm/models/symbolic/Dtmc.h" diff --git a/src/test/storm-pars/utility/ModelInstantiatorTest.cpp b/src/test/storm-pars/utility/ModelInstantiatorTest.cpp index 1873a4436..fa7bb16eb 100644 --- a/src/test/storm-pars/utility/ModelInstantiatorTest.cpp +++ b/src/test/storm-pars/utility/ModelInstantiatorTest.cpp @@ -13,6 +13,7 @@ #include "storm-pars/utility/ModelInstantiator.h" #include "storm/api/storm.h" +#include "storm-parsers/api/storm-parsers.h" #include "storm/models/sparse/Model.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Mdp.h" diff --git a/src/test/storm/CMakeLists.txt b/src/test/storm/CMakeLists.txt index 0ae2fc509..c745943b4 100644 --- a/src/test/storm/CMakeLists.txt +++ b/src/test/storm/CMakeLists.txt @@ -13,7 +13,7 @@ foreach (testsuite abstraction adapter builder logic modelchecker parser permiss file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp) add_executable (test-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp) - target_link_libraries(test-${testsuite} storm) + target_link_libraries(test-${testsuite} storm storm-parsers) target_link_libraries(test-${testsuite} ${STORM_TEST_LINK_LIBRARIES}) add_dependencies(test-${testsuite} test-resources) diff --git a/src/test/storm/abstraction/PrismMenuGameTest.cpp b/src/test/storm/abstraction/PrismMenuGameTest.cpp index a200c1d68..96c484d99 100644 --- a/src/test/storm/abstraction/PrismMenuGameTest.cpp +++ b/src/test/storm/abstraction/PrismMenuGameTest.cpp @@ -3,7 +3,7 @@ #ifdef STORM_HAVE_MSAT -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/abstraction/MenuGameRefiner.h" #include "storm/abstraction/prism/PrismMenuGameAbstractor.h" diff --git a/src/test/storm/builder/DdJaniModelBuilderTest.cpp b/src/test/storm/builder/DdJaniModelBuilderTest.cpp index fa657a96f..1515b83e3 100644 --- a/src/test/storm/builder/DdJaniModelBuilderTest.cpp +++ b/src/test/storm/builder/DdJaniModelBuilderTest.cpp @@ -10,7 +10,7 @@ #include "storm/storage/jani/Compositions.h" #include "storm/models/symbolic/StandardRewardModel.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/builder/DdJaniModelBuilder.h" #include "storm/settings/SettingMemento.h" diff --git a/src/test/storm/builder/DdPrismModelBuilderTest.cpp b/src/test/storm/builder/DdPrismModelBuilderTest.cpp index 1ff4a79fe..a56aa1e12 100644 --- a/src/test/storm/builder/DdPrismModelBuilderTest.cpp +++ b/src/test/storm/builder/DdPrismModelBuilderTest.cpp @@ -8,7 +8,7 @@ #include "storm/models/symbolic/Ctmc.h" #include "storm/models/symbolic/Mdp.h" #include "storm/models/symbolic/StandardRewardModel.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/builder/DdPrismModelBuilder.h" TEST(DdPrismModelBuilderTest_Sylvan, Dtmc) { diff --git a/src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp b/src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp index 4f21c3a64..95b690e96 100644 --- a/src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp +++ b/src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp @@ -3,7 +3,7 @@ #include "storm/models/sparse/StandardRewardModel.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/settings/SettingMemento.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/builder/ExplicitModelBuilder.h" #include "storm/generator/JaniNextStateGenerator.h" #include "storm/storage/jani/Model.h" diff --git a/src/test/storm/builder/ExplicitJitJaniModelBuilderTest.cpp b/src/test/storm/builder/ExplicitJitJaniModelBuilderTest.cpp index 334735b02..c5c0eec05 100644 --- a/src/test/storm/builder/ExplicitJitJaniModelBuilderTest.cpp +++ b/src/test/storm/builder/ExplicitJitJaniModelBuilderTest.cpp @@ -3,7 +3,7 @@ #include "storm/models/sparse/StandardRewardModel.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/settings/SettingMemento.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/builder/jit/ExplicitJitJaniModelBuilder.h" #include "storm/storage/jani/Model.h" diff --git a/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp b/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp index 8e5929618..65e1dff1d 100644 --- a/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp +++ b/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp @@ -2,7 +2,7 @@ #include "storm-config.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/models/sparse/MarkovAutomaton.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/builder/ExplicitModelBuilder.h" diff --git a/src/test/storm/logic/FragmentCheckerTest.cpp b/src/test/storm/logic/FragmentCheckerTest.cpp index c846f7f68..5adf50028 100644 --- a/src/test/storm/logic/FragmentCheckerTest.cpp +++ b/src/test/storm/logic/FragmentCheckerTest.cpp @@ -1,6 +1,6 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/FragmentChecker.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/storage/expressions/ExpressionManager.h" diff --git a/src/test/storm/modelchecker/ConditionalDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/ConditionalDtmcPrctlModelCheckerTest.cpp index c0972c474..fd124f456 100644 --- a/src/test/storm/modelchecker/ConditionalDtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/ConditionalDtmcPrctlModelCheckerTest.cpp @@ -2,12 +2,12 @@ #include "test/storm_gtest.h" #include "storm-config.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/Formulas.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/api/builder.h" #include "storm/storage/expressions/ExpressionManager.h" diff --git a/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp index f2a790b9b..1b83be1c6 100644 --- a/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/CtmcCslModelCheckerTest.cpp @@ -3,9 +3,10 @@ #include "storm-config.h" #include "storm/api/builder.h" -#include "storm/api/model_descriptions.h" +#include "storm-parsers/api/model_descriptions.h" #include "storm/api/properties.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/api/properties.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/Formulas.h" #include "storm/solver/EigenLinearEquationSolver.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -18,7 +19,7 @@ #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "storm/modelchecker/results/QualitativeCheckResult.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/settings/modules/CoreSettings.h" #include "storm/environment/solver/NativeSolverEnvironment.h" diff --git a/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp index ad6654ff4..f7f3b72a1 100644 --- a/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/DtmcPrctlModelCheckerTest.cpp @@ -3,9 +3,10 @@ #include "storm-config.h" #include "storm/api/builder.h" -#include "storm/api/model_descriptions.h" +#include "storm-parsers/api/model_descriptions.h" #include "storm/api/properties.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/api/properties.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/Formulas.h" #include "storm/solver/EigenLinearEquationSolver.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -19,7 +20,7 @@ #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "storm/modelchecker/results/QualitativeCheckResult.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/settings/modules/CoreSettings.h" #include "storm/environment/solver/NativeSolverEnvironment.h" diff --git a/src/test/storm/modelchecker/ExplicitDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/ExplicitDtmcPrctlModelCheckerTest.cpp index 06b90270b..025bc8c45 100644 --- a/src/test/storm/modelchecker/ExplicitDtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/ExplicitDtmcPrctlModelCheckerTest.cpp @@ -1,7 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/Formulas.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" @@ -9,8 +9,8 @@ #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/SettingMemento.h" -#include "storm/parser/AutoParser.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/AutoParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/builder/ExplicitModelBuilder.h" #include "storm/storage/expressions/ExpressionManager.h" diff --git a/src/test/storm/modelchecker/ExplicitMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/ExplicitMdpPrctlModelCheckerTest.cpp index 91db98302..b295c397b 100644 --- a/src/test/storm/modelchecker/ExplicitMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/ExplicitMdpPrctlModelCheckerTest.cpp @@ -1,7 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/Formulas.h" #include "storm/solver/StandardMinMaxLinearEquationSolver.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -10,8 +10,8 @@ #include "storm/environment/solver/MinMaxSolverEnvironment.h" -#include "storm/parser/AutoParser.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/AutoParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/builder/ExplicitModelBuilder.h" TEST(ExplicitMdpPrctlModelCheckerTest, Dice) { diff --git a/src/test/storm/modelchecker/GameBasedDtmcModelCheckerTest.cpp b/src/test/storm/modelchecker/GameBasedDtmcModelCheckerTest.cpp index 2a4f64c4d..3511aabec 100644 --- a/src/test/storm/modelchecker/GameBasedDtmcModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/GameBasedDtmcModelCheckerTest.cpp @@ -1,13 +1,13 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/Formulas.h" #include "storm/utility/solver.h" #include "storm/modelchecker/abstraction/GameBasedMdpModelChecker.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/builder/DdPrismModelBuilder.h" #include "storm/models/symbolic/StandardRewardModel.h" #include "storm/models/symbolic/Dtmc.h" diff --git a/src/test/storm/modelchecker/GameBasedMdpModelCheckerTest.cpp b/src/test/storm/modelchecker/GameBasedMdpModelCheckerTest.cpp index 960cc56bc..225bf81b4 100644 --- a/src/test/storm/modelchecker/GameBasedMdpModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/GameBasedMdpModelCheckerTest.cpp @@ -1,7 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/Formulas.h" #include "storm/models/symbolic/StandardRewardModel.h" #include "storm/models/sparse/Model.h" @@ -13,6 +13,8 @@ #include "storm/api/storm.h" +#include "storm-parsers/api/storm-parsers.h" + #if defined STORM_HAVE_MSAT TEST(GameBasedMdpModelCheckerTest, Dice_Cudd) { #else diff --git a/src/test/storm/modelchecker/LraDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/LraDtmcPrctlModelCheckerTest.cpp index 59c589cb1..c964628b9 100644 --- a/src/test/storm/modelchecker/LraDtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/LraDtmcPrctlModelCheckerTest.cpp @@ -2,7 +2,7 @@ #include "storm-config.h" #include "test/storm_gtest.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/settings/SettingMemento.h" #include "storm/logic/Formulas.h" #include "storm/solver/NativeLinearEquationSolver.h" @@ -17,7 +17,7 @@ #include "storm/environment/solver/EigenSolverEnvironment.h" #include "storm/environment/solver/GmmxxSolverEnvironment.h" -#include "storm/parser/AutoParser.h" +#include "storm-parsers/parser/AutoParser.h" #include "storm/builder/ExplicitModelBuilder.h" namespace { diff --git a/src/test/storm/modelchecker/LraMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/LraMdpPrctlModelCheckerTest.cpp index ed3abb16b..b05ebfb76 100644 --- a/src/test/storm/modelchecker/LraMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/LraMdpPrctlModelCheckerTest.cpp @@ -1,7 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/Formulas.h" #include "storm/solver/StandardMinMaxLinearEquationSolver.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -12,7 +12,7 @@ #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/NativeEquationSolverSettings.h" -#include "storm/parser/AutoParser.h" +#include "storm-parsers/parser/AutoParser.h" TEST(LraMdpPrctlModelCheckerTest, LRA_SingleMec) { storm::storage::SparseMatrixBuilder<double> matrixBuilder; diff --git a/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp index e0741fa30..feb90d438 100644 --- a/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/MdpPrctlModelCheckerTest.cpp @@ -4,8 +4,9 @@ #include "test/storm_gtest.h" #include "storm/api/builder.h" -#include "storm/api/model_descriptions.h" +#include "storm-parsers/api/model_descriptions.h" #include "storm/api/properties.h" +#include "storm-parsers/api/properties.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/symbolic/Mdp.h" diff --git a/src/test/storm/modelchecker/SchedulerGenerationMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/SchedulerGenerationMdpPrctlModelCheckerTest.cpp index 751a28ed2..6f82d6a47 100644 --- a/src/test/storm/modelchecker/SchedulerGenerationMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/SchedulerGenerationMdpPrctlModelCheckerTest.cpp @@ -1,7 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/Formulas.h" #include "storm/solver/StandardMinMaxLinearEquationSolver.h" #include "storm/models/sparse/StandardRewardModel.h" @@ -12,8 +12,8 @@ #include "storm/environment/solver/MinMaxSolverEnvironment.h" -#include "storm/parser/AutoParser.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/AutoParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/builder/ExplicitModelBuilder.h" namespace { diff --git a/src/test/storm/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp b/src/test/storm/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp index 00c8b88e5..ed182bf2c 100644 --- a/src/test/storm/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp @@ -1,7 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/Formulas.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" @@ -10,7 +10,7 @@ #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/SettingMemento.h" -#include "storm/parser/AutoParser.h" +#include "storm-parsers/parser/AutoParser.h" TEST(SparseDtmcEliminationModelCheckerTest, Die) { std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/die.tra", STORM_TEST_RESOURCES_DIR "/lab/die.lab", "", STORM_TEST_RESOURCES_DIR "/rew/die.coin_flips.trans.rew"); diff --git a/src/test/storm/modelchecker/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp b/src/test/storm/modelchecker/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp index 36ca41ff0..3a20c997b 100644 --- a/src/test/storm/modelchecker/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp +++ b/src/test/storm/modelchecker/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp @@ -7,6 +7,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/utility/constants.h" #include "storm/api/storm.h" +#include "storm-parsers/api/storm-parsers.h" #include "storm/environment/Environment.h" TEST(SparseDtmcMultiDimensionalRewardUnfoldingTest, cost_bounded_die) { diff --git a/src/test/storm/modelchecker/SparseExplorationModelCheckerTest.cpp b/src/test/storm/modelchecker/SparseExplorationModelCheckerTest.cpp index a1645e2a0..dc7d7a55a 100644 --- a/src/test/storm/modelchecker/SparseExplorationModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/SparseExplorationModelCheckerTest.cpp @@ -4,8 +4,8 @@ #include "storm/logic/Formulas.h" #include "storm/modelchecker/exploration/SparseExplorationModelChecker.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" -#include "storm/parser/PrismParser.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/PrismParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/ExplorationSettings.h" diff --git a/src/test/storm/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp index e5843b4e1..4970fff9d 100644 --- a/src/test/storm/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/SparseMaCbMultiObjectiveModelCheckerTest.cpp @@ -9,6 +9,7 @@ #include "storm/settings/modules/MultiObjectiveSettings.h" #include "storm/settings/SettingsManager.h" #include "storm/api/storm.h" +#include "storm-parsers/api/storm-parsers.h" #include "storm/environment/Environment.h" diff --git a/src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp index d2c116358..58c8e7494 100644 --- a/src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp @@ -14,6 +14,7 @@ #include "storm/settings/modules/MultiObjectiveSettings.h" #include "storm/settings/SettingsManager.h" #include "storm/api/storm.h" +#include "storm-parsers/api/storm-parsers.h" #include "storm/environment/Environment.h" diff --git a/src/test/storm/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp index 7b2479ec3..f353092af 100644 --- a/src/test/storm/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/SparseMdpCbMultiObjectiveModelCheckerTest.cpp @@ -7,6 +7,7 @@ #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/SettingsManager.h" #include "storm/api/storm.h" +#include "storm-parsers/api/storm-parsers.h" #include "storm/environment/Environment.h" diff --git a/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp b/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp index 3f73da77e..4880564b0 100644 --- a/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp +++ b/src/test/storm/modelchecker/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp @@ -10,6 +10,7 @@ #include "storm/settings/SettingsManager.h" #include "storm/utility/constants.h" #include "storm/api/storm.h" +#include "storm-parsers/api/storm-parsers.h" #include "storm/environment/Environment.h" #include "storm/environment/solver/MinMaxSolverEnvironment.h" diff --git a/src/test/storm/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp index 947cbde55..8e4cb084c 100644 --- a/src/test/storm/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp @@ -10,6 +10,7 @@ #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/SettingsManager.h" #include "storm/api/storm.h" +#include "storm-parsers/api/storm-parsers.h" #include "storm/environment/Environment.h" TEST(SparseMdpPcaaMultiObjectiveModelCheckerTest, consensus) { diff --git a/src/test/storm/parser/AutoParserTest.cpp b/src/test/storm/parser/AutoParserTest.cpp index 0ddd14894..96aa9cc60 100644 --- a/src/test/storm/parser/AutoParserTest.cpp +++ b/src/test/storm/parser/AutoParserTest.cpp @@ -2,7 +2,7 @@ #include "storm-config.h" #include "storm/models/sparse/StandardRewardModel.h" -#include "storm/parser/AutoParser.h" +#include "storm-parsers/parser/AutoParser.h" #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/WrongFormatException.h" diff --git a/src/test/storm/parser/DeterministicModelParserTest.cpp b/src/test/storm/parser/DeterministicModelParserTest.cpp index b2f7ac9c2..bd5b0bf69 100644 --- a/src/test/storm/parser/DeterministicModelParserTest.cpp +++ b/src/test/storm/parser/DeterministicModelParserTest.cpp @@ -2,7 +2,7 @@ #include "storm-config.h" #include "storm/models/sparse/StandardRewardModel.h" -#include "storm/parser/DeterministicModelParser.h" +#include "storm-parsers/parser/DeterministicModelParser.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Ctmc.h" #include "storm/exceptions/FileIoException.h" diff --git a/src/test/storm/parser/DeterministicSparseTransitionParserTest.cpp b/src/test/storm/parser/DeterministicSparseTransitionParserTest.cpp index bd8e9e2f2..737d8ff04 100644 --- a/src/test/storm/parser/DeterministicSparseTransitionParserTest.cpp +++ b/src/test/storm/parser/DeterministicSparseTransitionParserTest.cpp @@ -8,7 +8,7 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/DeterministicSparseTransitionParser.h" +#include "storm-parsers/parser/DeterministicSparseTransitionParser.h" #include "storm/storage/SparseMatrix.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/CoreSettings.h" diff --git a/src/test/storm/parser/DirectEncodingParserTest.cpp b/src/test/storm/parser/DirectEncodingParserTest.cpp index 93bd34e04..c5716195b 100644 --- a/src/test/storm/parser/DirectEncodingParserTest.cpp +++ b/src/test/storm/parser/DirectEncodingParserTest.cpp @@ -1,7 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/DirectEncodingParser.h" +#include "storm-parsers/parser/DirectEncodingParser.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/MarkovAutomaton.h" diff --git a/src/test/storm/parser/FormulaParserTest.cpp b/src/test/storm/parser/FormulaParserTest.cpp index 6269a082c..fd1206947 100644 --- a/src/test/storm/parser/FormulaParserTest.cpp +++ b/src/test/storm/parser/FormulaParserTest.cpp @@ -1,6 +1,6 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/FragmentSpecification.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/storage/expressions/ExpressionManager.h" diff --git a/src/test/storm/parser/MappedFileTest.cpp b/src/test/storm/parser/MappedFileTest.cpp index f33ee3aa2..362cbc899 100644 --- a/src/test/storm/parser/MappedFileTest.cpp +++ b/src/test/storm/parser/MappedFileTest.cpp @@ -9,7 +9,7 @@ #include "storm-config.h" #include <string> -#include "storm/parser/MappedFile.h" +#include "storm-parsers/parser/MappedFile.h" #include "storm/utility/cstring.h" #include "storm/utility/file.h" #include "storm/exceptions/FileIoException.h" diff --git a/src/test/storm/parser/MarkovAutomatonParserTest.cpp b/src/test/storm/parser/MarkovAutomatonParserTest.cpp index c31787087..3eb2dc3f7 100644 --- a/src/test/storm/parser/MarkovAutomatonParserTest.cpp +++ b/src/test/storm/parser/MarkovAutomatonParserTest.cpp @@ -1,7 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/MarkovAutomatonParser.h" +#include "storm-parsers/parser/MarkovAutomatonParser.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/OutOfRangeException.h" diff --git a/src/test/storm/parser/MarkovAutomatonSparseTransitionParserTest.cpp b/src/test/storm/parser/MarkovAutomatonSparseTransitionParserTest.cpp index 461b28a95..f29a5689d 100644 --- a/src/test/storm/parser/MarkovAutomatonSparseTransitionParserTest.cpp +++ b/src/test/storm/parser/MarkovAutomatonSparseTransitionParserTest.cpp @@ -12,9 +12,9 @@ #include <vector> -#include "storm/parser/MarkovAutomatonSparseTransitionParser.h" +#include "storm-parsers/parser/MarkovAutomatonSparseTransitionParser.h" #include "storm/utility/cstring.h" -#include "storm/parser/MarkovAutomatonParser.h" +#include "storm-parsers/parser/MarkovAutomatonParser.h" #include "storm/settings/SettingMemento.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/FileIoException.h" diff --git a/src/test/storm/parser/NondeterministicModelParserTest.cpp b/src/test/storm/parser/NondeterministicModelParserTest.cpp index b700c56f4..8ed57b2b7 100644 --- a/src/test/storm/parser/NondeterministicModelParserTest.cpp +++ b/src/test/storm/parser/NondeterministicModelParserTest.cpp @@ -1,7 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/NondeterministicModelParser.h" +#include "storm-parsers/parser/NondeterministicModelParser.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/exceptions/FileIoException.h" diff --git a/src/test/storm/parser/NondeterministicSparseTransitionParserTest.cpp b/src/test/storm/parser/NondeterministicSparseTransitionParserTest.cpp index 77344834a..9c740144f 100644 --- a/src/test/storm/parser/NondeterministicSparseTransitionParserTest.cpp +++ b/src/test/storm/parser/NondeterministicSparseTransitionParserTest.cpp @@ -8,7 +8,7 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/NondeterministicSparseTransitionParser.h" +#include "storm-parsers/parser/NondeterministicSparseTransitionParser.h" #include "storm/storage/SparseMatrix.h" #include "storm/settings/SettingMemento.h" diff --git a/src/test/storm/parser/PrismParserTest.cpp b/src/test/storm/parser/PrismParserTest.cpp index c86d90f63..4fe5735f5 100644 --- a/src/test/storm/parser/PrismParserTest.cpp +++ b/src/test/storm/parser/PrismParserTest.cpp @@ -1,6 +1,6 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" TEST(PrismParser, StandardModelTest) { storm::prism::Program result; diff --git a/src/test/storm/parser/SparseItemLabelingParserTest.cpp b/src/test/storm/parser/SparseItemLabelingParserTest.cpp index 695b6837b..2f5cf3c0b 100644 --- a/src/test/storm/parser/SparseItemLabelingParserTest.cpp +++ b/src/test/storm/parser/SparseItemLabelingParserTest.cpp @@ -1,7 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" #include "storm/models/sparse/StateLabeling.h" -#include "storm/parser/SparseItemLabelingParser.h" +#include "storm-parsers/parser/SparseItemLabelingParser.h" #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/OutOfRangeException.h" diff --git a/src/test/storm/parser/SparseStateRewardParserTest.cpp b/src/test/storm/parser/SparseStateRewardParserTest.cpp index d92203210..53524b3cd 100644 --- a/src/test/storm/parser/SparseStateRewardParserTest.cpp +++ b/src/test/storm/parser/SparseStateRewardParserTest.cpp @@ -10,7 +10,7 @@ #include <cmath> -#include "storm/parser/SparseStateRewardParser.h" +#include "storm-parsers/parser/SparseStateRewardParser.h" #include "storm/exceptions/FileIoException.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/OutOfRangeException.h" diff --git a/src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp b/src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp index 20707d33e..a6b0a34fd 100644 --- a/src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp +++ b/src/test/storm/permissiveschedulers/MilpPermissiveSchedulerTest.cpp @@ -1,8 +1,8 @@ #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/PrismParser.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/PrismParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/logic/Formulas.h" #include "storm/permissivesched/PermissiveSchedulers.h" diff --git a/src/test/storm/permissiveschedulers/SmtPermissiveSchedulerTest.cpp b/src/test/storm/permissiveschedulers/SmtPermissiveSchedulerTest.cpp index b19f82618..1b873a935 100644 --- a/src/test/storm/permissiveschedulers/SmtPermissiveSchedulerTest.cpp +++ b/src/test/storm/permissiveschedulers/SmtPermissiveSchedulerTest.cpp @@ -1,8 +1,8 @@ #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/PrismParser.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/PrismParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/logic/Formulas.h" #include "storm/permissivesched/PermissiveSchedulers.h" #include "storm/builder/ExplicitModelBuilder.h" diff --git a/src/test/storm/storage/DeterministicModelBisimulationDecompositionTest.cpp b/src/test/storm/storage/DeterministicModelBisimulationDecompositionTest.cpp index 3ebeca7a5..3341b1fe7 100644 --- a/src/test/storm/storage/DeterministicModelBisimulationDecompositionTest.cpp +++ b/src/test/storm/storage/DeterministicModelBisimulationDecompositionTest.cpp @@ -1,7 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/AutoParser.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/AutoParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/storage/bisimulation/DeterministicModelBisimulationDecomposition.h" #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/StandardRewardModel.h" diff --git a/src/test/storm/storage/JaniModelTest.cpp b/src/test/storm/storage/JaniModelTest.cpp index 7c7f393b3..c7a6b5c11 100644 --- a/src/test/storm/storage/JaniModelTest.cpp +++ b/src/test/storm/storage/JaniModelTest.cpp @@ -1,6 +1,6 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/utility/solver.h" diff --git a/src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp b/src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp index 6e9718e6b..b30b5259b 100644 --- a/src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp +++ b/src/test/storm/storage/MaximalEndComponentDecompositionTest.cpp @@ -1,13 +1,13 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/AutoParser.h" +#include "storm-parsers/parser/AutoParser.h" #include "storm/storage/MaximalEndComponentDecomposition.h" #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/builder/ExplicitModelBuilder.h" #include "storm/storage/SymbolicModelDescription.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" TEST(MaximalEndComponentDecomposition, FullSystem1) { std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/tiny1.tra", STORM_TEST_RESOURCES_DIR "/lab/tiny1.lab", "", ""); diff --git a/src/test/storm/storage/NondeterministicModelBisimulationDecompositionTest.cpp b/src/test/storm/storage/NondeterministicModelBisimulationDecompositionTest.cpp index 596938852..d77fa8d64 100644 --- a/src/test/storm/storage/NondeterministicModelBisimulationDecompositionTest.cpp +++ b/src/test/storm/storage/NondeterministicModelBisimulationDecompositionTest.cpp @@ -1,8 +1,8 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/PrismParser.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/PrismParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/builder/ExplicitModelBuilder.h" diff --git a/src/test/storm/storage/PrismProgramTest.cpp b/src/test/storm/storage/PrismProgramTest.cpp index 8525f03e2..e860fa997 100644 --- a/src/test/storm/storage/PrismProgramTest.cpp +++ b/src/test/storm/storage/PrismProgramTest.cpp @@ -1,6 +1,6 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/utility/solver.h" diff --git a/src/test/storm/storage/StronglyConnectedComponentDecompositionTest.cpp b/src/test/storm/storage/StronglyConnectedComponentDecompositionTest.cpp index e447d2ec0..821b721a7 100644 --- a/src/test/storm/storage/StronglyConnectedComponentDecompositionTest.cpp +++ b/src/test/storm/storage/StronglyConnectedComponentDecompositionTest.cpp @@ -1,6 +1,6 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/AutoParser.h" +#include "storm-parsers/parser/AutoParser.h" #include "storm/storage/SparseMatrix.h" #include "storm/storage/StronglyConnectedComponentDecomposition.h" #include "storm/models/sparse/StandardRewardModel.h" diff --git a/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp b/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp index d339bd027..64d2906d1 100644 --- a/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp +++ b/src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp @@ -1,8 +1,8 @@ #include "gtest/gtest.h" #include "storm-config.h" -#include "storm/parser/PrismParser.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/PrismParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/builder/DdPrismModelBuilder.h" @@ -19,7 +19,7 @@ #include "storm/solver/SymbolicMinMaxLinearEquationSolver.h" #include "storm/logic/Formulas.h" -#include "storm/parser/FormulaParser.h" +#include "storm-parsers/parser/FormulaParser.h" #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/StandardRewardModel.h" diff --git a/src/test/storm/utility/GraphTest.cpp b/src/test/storm/utility/GraphTest.cpp index ac646d99a..3098297c0 100644 --- a/src/test/storm/utility/GraphTest.cpp +++ b/src/test/storm/utility/GraphTest.cpp @@ -2,7 +2,7 @@ #include "storm-config.h" #include "storm/storage/SymbolicModelDescription.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/models/symbolic/Dtmc.h" #include "storm/models/symbolic/Mdp.h" #include "storm/models/symbolic/StandardRewardModel.h" diff --git a/src/test/storm/utility/KSPTest.cpp b/src/test/storm/utility/KSPTest.cpp index 5ac954314..dfe14e817 100644 --- a/src/test/storm/utility/KSPTest.cpp +++ b/src/test/storm/utility/KSPTest.cpp @@ -3,7 +3,7 @@ #include "storm/builder/ExplicitModelBuilder.h" #include "storm/models/sparse/Dtmc.h" -#include "storm/parser/PrismParser.h" +#include "storm-parsers/parser/PrismParser.h" #include "storm/storage/SymbolicModelDescription.h" #include "storm/utility/graph.h" #include "storm/utility/shortestPaths.h"