From caf79bd68d1a55846722357ac4f54a2d58fa7c64 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 23 Jul 2026 23:53:16 +0200 Subject: [PATCH 1/3] Moved preprocessing to Jani Model and Prism Program --- src/storm/builder/DdPrismModelBuilder.cpp | 1 - src/storm/builder/ExplicitModelBuilder.h | 3 -- .../SparseExplorationModelChecker.cpp | 1 - .../storage/SymbolicModelDescription.cpp | 15 +++------ src/storm/storage/jani/Model.cpp | 32 +++++++++++-------- src/storm/storage/jani/Model.h | 20 ++++++++++-- src/storm/storage/prism/Program.cpp | 21 +++++++----- src/storm/storage/prism/Program.h | 23 ++++++++++--- src/storm/utility/prism.cpp | 24 -------------- src/storm/utility/prism.h | 29 ----------------- 10 files changed, 73 insertions(+), 96 deletions(-) delete mode 100644 src/storm/utility/prism.cpp delete mode 100644 src/storm/utility/prism.h diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp index 09dabf6ffe..01a8bb0479 100644 --- a/src/storm/builder/DdPrismModelBuilder.cpp +++ b/src/storm/builder/DdPrismModelBuilder.cpp @@ -19,7 +19,6 @@ #include "storm/storage/prism/Compositions.h" #include "storm/storage/prism/Program.h" #include "storm/utility/dd.h" -#include "storm/utility/prism.h" namespace storm { namespace builder { diff --git a/src/storm/builder/ExplicitModelBuilder.h b/src/storm/builder/ExplicitModelBuilder.h index b43fbe32c5..9490570562 100644 --- a/src/storm/builder/ExplicitModelBuilder.h +++ b/src/storm/builder/ExplicitModelBuilder.h @@ -21,8 +21,6 @@ #include "storm/storage/sparse/ModelComponents.h" #include "storm/storage/sparse/StateStorage.h" -#include "storm/utility/prism.h" - #include "storm/builder/ExplorationOrder.h" #include "storm/generator/CompressedState.h" @@ -33,7 +31,6 @@ namespace storm { namespace builder { -using namespace storm::utility::prism; using namespace storm::generator; // Forward-declare classes. diff --git a/src/storm/modelchecker/exploration/SparseExplorationModelChecker.cpp b/src/storm/modelchecker/exploration/SparseExplorationModelChecker.cpp index 14cd562ba5..47c7cb552e 100644 --- a/src/storm/modelchecker/exploration/SparseExplorationModelChecker.cpp +++ b/src/storm/modelchecker/exploration/SparseExplorationModelChecker.cpp @@ -29,7 +29,6 @@ #include "storm/utility/constants.h" #include "storm/utility/graph.h" #include "storm/utility/macros.h" -#include "storm/utility/prism.h" #include "storm/exceptions/InvalidOperationException.h" #include "storm/exceptions/InvalidPropertyException.h" diff --git a/src/storm/storage/SymbolicModelDescription.cpp b/src/storm/storage/SymbolicModelDescription.cpp index 0cdb62a9d1..5b313517da 100644 --- a/src/storm/storage/SymbolicModelDescription.cpp +++ b/src/storm/storage/SymbolicModelDescription.cpp @@ -1,14 +1,12 @@ #include "storm/storage/SymbolicModelDescription.h" -#include "storm/utility/cli.h" -#include "storm/utility/prism.h" - #include "storm/storage/jani/Automaton.h" #include "storm/storage/jani/Model.h" #include "storm/storage/jani/Property.h" #include "storm/exceptions/InvalidOperationException.h" #include "storm/exceptions/InvalidTypeException.h" +#include "storm/utility/cli.h" #include "storm/utility/macros.h" namespace storm { @@ -159,20 +157,15 @@ std::pair> Symbolic } SymbolicModelDescription SymbolicModelDescription::preprocess(std::string const& constantDefinitionString) const { - std::map substitution = parseConstantDefinitions(constantDefinitionString); - return preprocess(substitution); + return this->preprocess(this->parseConstantDefinitions(constantDefinitionString)); } SymbolicModelDescription SymbolicModelDescription::preprocess( std::map const& constantDefinitions) const { if (this->isJaniModel()) { - storm::jani::Model preparedModel = this->asJaniModel().defineUndefinedConstants(constantDefinitions).substituteConstants(); - // We intentionally do not eliminate function expressions in jani models at this point because that would also remove the function - // declarations from the model. However, those might still be needed to, e.g., process properties that refer to functions. - return SymbolicModelDescription(preparedModel); + return SymbolicModelDescription(this->asJaniModel().preprocess(constantDefinitions)); } else if (this->isPrismProgram()) { - return SymbolicModelDescription( - this->asPrismProgram().defineUndefinedConstants(constantDefinitions).substituteConstantsFormulas().substituteNonStandardPredicates()); + return SymbolicModelDescription(this->asPrismProgram().preprocess(constantDefinitions)); } return *this; } diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 1a2d8065e5..70ef9cba5a 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -2,11 +2,17 @@ #include +#include "storm/exceptions/InvalidArgumentException.h" +#include "storm/exceptions/InvalidOperationException.h" +#include "storm/exceptions/InvalidTypeException.h" +#include "storm/exceptions/NotImplementedException.h" +#include "storm/exceptions/WrongFormatException.h" +#include "storm/solver/SmtSolver.h" #include "storm/storage/expressions/ExpressionManager.h" - -#include "Compositions.h" +#include "storm/storage/expressions/LinearityCheckVisitor.h" #include "storm/storage/jani/Automaton.h" #include "storm/storage/jani/AutomatonComposition.h" +#include "storm/storage/jani/Compositions.h" #include "storm/storage/jani/Edge.h" #include "storm/storage/jani/EdgeDestination.h" #include "storm/storage/jani/Location.h" @@ -20,21 +26,11 @@ #include "storm/storage/jani/visitor/CompositionInformationVisitor.h" #include "storm/storage/jani/visitor/JSONExporter.h" #include "storm/storage/jani/visitor/JaniExpressionSubstitutionVisitor.h" - -#include "storm/storage/expressions/LinearityCheckVisitor.h" - +#include "storm/utility/cli.h" #include "storm/utility/combinatorics.h" - -#include "storm/exceptions/InvalidArgumentException.h" -#include "storm/exceptions/InvalidOperationException.h" -#include "storm/exceptions/InvalidTypeException.h" -#include "storm/exceptions/NotImplementedException.h" -#include "storm/exceptions/WrongFormatException.h" #include "storm/utility/macros.h" #include "storm/utility/vector.h" -#include "storm/solver/SmtSolver.h" - namespace storm { namespace jani { @@ -1156,6 +1152,16 @@ Model Model::substituteConstantsFunctionsTranscendentals() const { return result; } +Model Model::preprocess(std::map const& constantDefinitions) const { + // We intentionally do not eliminate function expressions in jani models at this point because that would also remove the function + // declarations from the model. However, those might still be needed to, e.g., process properties that refer to functions. + return this->defineUndefinedConstants(constantDefinitions).substituteConstants(); +} + +Model Model::preprocess(std::string const& constantDefinitionString) const { + return this->preprocess(storm::utility::cli::parseConstantDefinitionString(this->getManager(), constantDefinitionString)); +} + std::map Model::getConstantsSubstitution() const { std::map result; diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index 168ad4c95a..79ca9a12ef 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -3,6 +3,7 @@ #include #include "Composition.h" +#include "storm/storage/BoostTypes.h" #include "storm/storage/jani/Action.h" #include "storm/storage/jani/Automaton.h" #include "storm/storage/jani/Constant.h" @@ -13,8 +14,6 @@ #include "storm/storage/jani/ModelType.h" #include "storm/storage/jani/TemplateEdge.h" #include "storm/storage/jani/VariableSet.h" - -#include "storm/storage/BoostTypes.h" #include "storm/utility/solver.h" namespace storm { @@ -429,6 +428,23 @@ class Model { */ Model substituteConstants() const; + /*! + * Preprocesses the model by defining the given constant definitions and substituting constants. + * + * @param constantDefinitions A mapping from undefined constant to the expressions they are supposed to be replaced with. + * @return The preprocessed model. + */ + Model preprocess(std::map const& constantDefinitions) const; + + /*! + * Preprocesses the model by parsing the given constant definition string, defining the constants, + * and substituting constants. + * + * @param constantDefinitionString A string of constant definitions, e.g., "p=0.5, n=10". + * @return The preprocessed model. + */ + Model preprocess(std::string const& constantDefinitionString = "") const; + /*! * Retrieves a mapping from expression variables associated with defined constants of the model to their * (the constants') defining expression. diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index 46c3655a62..c8700cf2d6 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -4,9 +4,6 @@ #include #include -#include "storm/storage/jani/Model.h" -#include "storm/storage/jani/Property.h" - #include "storm/exceptions/InternalException.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/InvalidOperationException.h" @@ -15,16 +12,16 @@ #include "storm/exceptions/WrongFormatException.h" #include "storm/solver/SmtSolver.h" #include "storm/storage/expressions/ExpressionManager.h" +#include "storm/storage/jani/Model.h" +#include "storm/storage/jani/Property.h" #include "storm/storage/jani/visitor/JaniExpressionSubstitutionVisitor.h" -#include "storm/utility/macros.h" -#include "storm/utility/solver.h" -#include "storm/utility/vector.h" - #include "storm/storage/prism/CompositionVisitor.h" #include "storm/storage/prism/Compositions.h" #include "storm/storage/prism/ToJaniConverter.h" - +#include "storm/utility/cli.h" #include "storm/utility/macros.h" +#include "storm/utility/solver.h" +#include "storm/utility/vector.h" namespace storm { namespace prism { @@ -1162,6 +1159,14 @@ Program Program::substituteConstantsFormulas(bool substituteConstants, bool subs this->getOptionalSystemCompositionConstruct(), prismCompatibility); } +Program Program::preprocess(std::map const& constantDefinitions) const { + return this->defineUndefinedConstants(constantDefinitions).substituteConstantsFormulas().substituteNonStandardPredicates(); +} + +Program Program::preprocess(std::string const& constantDefinitionString) const { + return this->preprocess(storm::utility::cli::parseConstantDefinitionString(this->getManager(), constantDefinitionString)); +} + Program Program::labelUnlabelledCommands(std::map const& nameSuggestions) const { for (auto const& entry : nameSuggestions) { STORM_LOG_THROW(!hasAction(entry.second), storm::exceptions::InvalidArgumentException, "Cannot suggest names already in the program."); diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h index 05e472f301..7e4a3003a1 100644 --- a/src/storm/storage/prism/Program.h +++ b/src/storm/storage/prism/Program.h @@ -1,5 +1,4 @@ -#ifndef STORM_STORAGE_PRISM_PROGRAM_H_ -#define STORM_STORAGE_PRISM_PROGRAM_H_ +#pragma once #include #include @@ -693,6 +692,24 @@ class Program : public LocatedInformation { */ Program substituteConstantsFormulas(bool substituteConstants = true, bool substituteFormulas = true) const; + /*! + * Preprocesses the program by defining the given constant definitions, substituting constants and formulas, + * and substituting non-standard predicates. + * + * @param constantDefinitions A mapping from undefined constant to the expressions they are supposed to be replaced with. + * @return The preprocessed program. + */ + Program preprocess(std::map const& constantDefinitions) const; + + /*! + * Preprocesses the program by parsing the given constant definition string, defining the constants, + * substituting constants and formulas, and substituting non-standard predicates. + * + * @param constantDefinitionString A string of constant definitions, e.g., "p=0.5, n=10". + * @return The preprocessed program. + */ + Program preprocess(std::string const& constantDefinitionString = "") const; + /*! * Replace the initialization in variables by an init-expression. This should not change the semantics of the program and can be a preprocessing step. * @@ -903,5 +920,3 @@ std::ostream& operator<<(std::ostream& out, Program::ModelType const& type); } // namespace prism } // namespace storm - -#endif /* STORM_STORAGE_PRISM_PROGRAM_H_ */ diff --git a/src/storm/utility/prism.cpp b/src/storm/utility/prism.cpp deleted file mode 100644 index 52f82c4ab3..0000000000 --- a/src/storm/utility/prism.cpp +++ /dev/null @@ -1,24 +0,0 @@ -#include "storm/utility/prism.h" - -#include "storm/storage/expressions/ExpressionManager.h" -#include "storm/storage/prism/Program.h" -#include "storm/utility/cli.h" - -namespace storm { -namespace utility { -namespace prism { - -storm::prism::Program preprocess(storm::prism::Program const& program, - std::map const& constantDefinitions) { - storm::prism::Program result = program.defineUndefinedConstants(constantDefinitions); - result = result.substituteConstantsFormulas(); - return result; -} - -storm::prism::Program preprocess(storm::prism::Program const& program, std::string const& constantDefinitionString) { - return preprocess(program, storm::utility::cli::parseConstantDefinitionString(program.getManager(), constantDefinitionString)); -} - -} // namespace prism -} // namespace utility -} // namespace storm diff --git a/src/storm/utility/prism.h b/src/storm/utility/prism.h deleted file mode 100644 index b835153eab..0000000000 --- a/src/storm/utility/prism.h +++ /dev/null @@ -1,29 +0,0 @@ -#ifndef STORM_UTILITY_PRISM_H_ -#define STORM_UTILITY_PRISM_H_ - -#include -#include - -namespace storm { -namespace expressions { -class Variable; -class Expression; -} // namespace expressions - -namespace prism { -class Program; -} - -namespace utility { -namespace prism { - -storm::prism::Program preprocess(storm::prism::Program const& program, - std::map const& constantDefinitions); - -storm::prism::Program preprocess(storm::prism::Program const& program, std::string const& constantDefinitionString); - -} // namespace prism -} // namespace utility -} // namespace storm - -#endif /* STORM_UTILITY_PRISM_H_ */ From 0c22cd8a2f53c6550da319f44e2408420e3246d9 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 23 Jul 2026 23:56:08 +0200 Subject: [PATCH 2/3] Adapted tests to new proprocess --- .../abstraction/GameBasedMdpModelChecker.cpp | 1 - ...adientDescentInstantiationSearcherTest.cpp | 4 +-- ...erivativeInstantiationModelCheckerTest.cpp | 6 ++-- ...seDtmcParameterLiftingMonotonicityTest.cpp | 18 ++++++------ .../SparseDtmcParameterLiftingTest.cpp | 28 +++++++++---------- .../SparseMdpParameterLiftingTest.cpp | 10 +++---- .../SparseRobustDtmcParameterLiftingTest.cpp | 16 +++++------ .../monotonicity/AssumptionCheckerTest.cpp | 10 +++---- .../monotonicity/AssumptionMakerTest.cpp | 6 ++-- .../monotonicity/MonotonicityCheckerTest.cpp | 10 +++---- .../monotonicity/MonotonicityHelperTest.cpp | 16 +++++------ .../region/monotonicity/OrderExtenderTest.cpp | 18 ++++++------ .../storm-pars/transformer/BigStepTest.cpp | 3 +- .../transformer/BinaryDtmcTransformerTest.cpp | 3 +- ...IntervalEndComponentPreserverCheckTest.cpp | 3 +- .../analysis/QualitativeAnalysisTest.cpp | 8 +++--- .../api/BeliefExplorationAPITest.cpp | 2 +- ...BeliefExplorationPomdpModelCheckerTest.cpp | 2 +- .../tracking/BeliefSupportTrackingTest.cpp | 2 +- .../NondeterministicBeliefTrackerTest.cpp | 2 +- .../transformation/MakeCanonicTest.cpp | 2 +- .../ObservationTraceUnfolderTest.cpp | 2 +- .../builder/ExplicitPrismModelBuilderTest.cpp | 12 ++++---- .../csl/CtmcCslModelCheckerTest.cpp | 4 +-- .../csl/LraCtmcCslModelCheckerTest.cpp | 4 +-- .../MarkovAutomatonCslModelCheckerTest.cpp | 4 +-- .../LexicographicModelCheckingTest.cpp | 4 +-- ...ultiObjectiveSchedRestModelCheckerTest.cpp | 8 +++--- .../PcaaWeightVectorCheckerTest.cpp | 2 +- ...tmcMultiDimensionalRewardUnfoldingTest.cpp | 6 ++-- ...arseMaCbMultiObjectiveModelCheckerTest.cpp | 2 +- ...seMaPcaaMultiObjectiveModelCheckerTest.cpp | 12 ++++---- ...rseMdpCbMultiObjectiveModelCheckerTest.cpp | 6 ++-- ...MdpMultiDimensionalRewardUnfoldingTest.cpp | 24 ++++++++-------- ...eMdpPcaaMultiObjectiveModelCheckerTest.cpp | 20 ++++++------- .../prctl/dtmc/DtmcPrctlModelCheckerTest.cpp | 4 +-- .../dtmc/RobustDtmcPrctlModelCheckerTest.cpp | 8 +++--- .../ConditionalMdpPrctlModelCheckerTest.cpp | 2 +- .../prctl/mdp/LraMdpPrctlModelCheckerTest.cpp | 2 +- .../prctl/mdp/MdpPrctlModelCheckerTest.cpp | 4 +-- .../prctl/mdp/QuantileQueryTest.cpp | 2 +- .../mdp/RobustMdpPrctlModelCheckerTest.cpp | 6 ++-- ...ulerGenerationMdpPrctlModelCheckerTest.cpp | 2 +- src/test/storm/storage/UmbTest.cpp | 2 +- 44 files changed, 154 insertions(+), 158 deletions(-) diff --git a/src/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 163797ffb3..c7353bf7a0 100644 --- a/src/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -36,7 +36,6 @@ #include "storm/storage/jani/ParallelComposition.h" #include "storm/storage/jani/visitor/CompositionInformationVisitor.h" #include "storm/utility/macros.h" -#include "storm/utility/prism.h" #include "storm/utility/vector.h" namespace storm::gbar { diff --git a/src/test/storm-pars/derivative/GradientDescentInstantiationSearcherTest.cpp b/src/test/storm-pars/derivative/GradientDescentInstantiationSearcherTest.cpp index 73de34c839..efd89c8398 100644 --- a/src/test/storm-pars/derivative/GradientDescentInstantiationSearcherTest.cpp +++ b/src/test/storm-pars/derivative/GradientDescentInstantiationSearcherTest.cpp @@ -109,7 +109,7 @@ TYPED_TEST(GradientDescentInstantiationSearcherTest, Simple) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -141,7 +141,7 @@ TYPED_TEST(GradientDescentInstantiationSearcherTest, Crowds) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = diff --git a/src/test/storm-pars/derivative/SparseDerivativeInstantiationModelCheckerTest.cpp b/src/test/storm-pars/derivative/SparseDerivativeInstantiationModelCheckerTest.cpp index 887bed8eac..9b80ac846f 100644 --- a/src/test/storm-pars/derivative/SparseDerivativeInstantiationModelCheckerTest.cpp +++ b/src/test/storm-pars/derivative/SparseDerivativeInstantiationModelCheckerTest.cpp @@ -166,7 +166,7 @@ TYPED_TEST(SparseDerivativeInstantiationModelCheckerTest, Simple) { // We have to create the dtmc and formulas here, because we need its parameters to create the polynomial storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -194,7 +194,7 @@ TYPED_TEST(SparseDerivativeInstantiationModelCheckerTest, Simple2) { // We have to create the dtmc and formulas here, because we need its parameters to create the polynomial storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -224,7 +224,7 @@ TYPED_TEST(SparseDerivativeInstantiationModelCheckerTest, Brp162) { // We have to create the dtmc and formulas here, because we need its parameters to create the polynomial storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = diff --git a/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingMonotonicityTest.cpp b/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingMonotonicityTest.cpp index 0c05be50a1..aebcdd5b12 100644 --- a/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingMonotonicityTest.cpp +++ b/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingMonotonicityTest.cpp @@ -74,7 +74,7 @@ TYPED_TEST(SparseDtmcParameterLiftingMonotonicityTest, Brp_Prob_Mon_LEQ) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -135,7 +135,7 @@ TYPED_TEST(SparseDtmcParameterLiftingMonotonicityTest, Brp_Prob_Mon_GEQ) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -196,7 +196,7 @@ TYPED_TEST(SparseDtmcParameterLiftingMonotonicityTest, Brp_Prob_Mon_LEQ_Incr) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -257,7 +257,7 @@ TYPED_TEST(SparseDtmcParameterLiftingMonotonicityTest, Brp_Prob_Mon_GEQ_Incr) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -318,7 +318,7 @@ TYPED_TEST(SparseDtmcParameterLiftingMonotonicityTest, Parametric_Die_Mon) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -373,7 +373,7 @@ TYPED_TEST(SparseDtmcParameterLiftingMonotonicityTest, Simple1_Mon) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -414,7 +414,7 @@ TYPED_TEST(SparseDtmcParameterLiftingMonotonicityTest, Casestudy1_Mon) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -455,7 +455,7 @@ TYPED_TEST(SparseDtmcParameterLiftingMonotonicityTest, Casestudy2_Mon) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -496,7 +496,7 @@ TYPED_TEST(SparseDtmcParameterLiftingMonotonicityTest, Casestudy3_Mon) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = diff --git a/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp b/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp index d5b5fcd2fb..c06f1ef86c 100644 --- a/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp +++ b/src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp @@ -87,7 +87,7 @@ TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Prob) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -119,7 +119,7 @@ TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Prob_no_simplification) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -150,7 +150,7 @@ TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Rew) { std::string constantsAsString = "pL=0.9,TOAck=0.5"; storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -181,7 +181,7 @@ TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded) { std::string constantsAsString = "pL=0.9,TOAck=0.5"; storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -215,7 +215,7 @@ TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Prob_exactValidation) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -249,7 +249,7 @@ TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Rew_exactValidation) { std::string constantsAsString = "pL=0.9,TOAck=0.5"; storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -284,7 +284,7 @@ TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded_exactValidation) { std::string constantsAsString = "pL=0.9,TOAck=0.5"; storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -315,7 +315,7 @@ TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Infty) { std::string formulaAsString = "R>2.5 [F (s=0&srep=3) ]"; std::string constantsAsString = ""; storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -339,7 +339,7 @@ TYPED_TEST(SparseDtmcParameterLiftingTest, Brp_Rew_4Par) { std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]"; std::string constantsAsString = ""; //!! this model will have 4 parameters storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -370,7 +370,7 @@ TYPED_TEST(SparseDtmcParameterLiftingTest, Crowds_Prob) { std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5 storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -404,7 +404,7 @@ TYPED_TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_stepBounded) { std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5 storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -438,7 +438,7 @@ TYPED_TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_1Par) { std::string constantsAsString = "badC=0.3"; // e.g. pL=0.9,TOACK=0.5 storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -469,7 +469,7 @@ TYPED_TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_Const) { std::string constantsAsString = "PF=0.9,badC=0.2"; storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -495,7 +495,7 @@ TYPED_TEST(SparseDtmcParameterLiftingTest, ZeroConf) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = diff --git a/src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp b/src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp index 6af6b35f8d..4e50e9dd3b 100644 --- a/src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp +++ b/src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp @@ -217,7 +217,7 @@ TYPED_TEST(SparseMdpParameterLiftingTest, brp_Prop) { std::string constantsAsString = "TOMsg=0.0,TOAck=0.0"; storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -248,7 +248,7 @@ TYPED_TEST(SparseMdpParameterLiftingTest, brp_Rew) { std::string constantsAsString = "pL=0.9,TOAck=0.5"; storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -279,7 +279,7 @@ TYPED_TEST(SparseMdpParameterLiftingTest, brp_Rew_bounded) { std::string constantsAsString = "pL=0.9,TOAck=0.5"; storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -309,7 +309,7 @@ TYPED_TEST(SparseMdpParameterLiftingTest, Brp_Rew_Infty) { std::string formulaAsString = "R>2.5 [F (s=0&srep=3) ]"; std::string constantsAsString = ""; storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -332,7 +332,7 @@ TYPED_TEST(SparseMdpParameterLiftingTest, Brp_Rew_4Par) { std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]"; std::string constantsAsString = ""; //!! this model will have 4 parameters storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = diff --git a/src/test/storm-pars/modelchecker/SparseRobustDtmcParameterLiftingTest.cpp b/src/test/storm-pars/modelchecker/SparseRobustDtmcParameterLiftingTest.cpp index b21ff72a19..b7408fe498 100644 --- a/src/test/storm-pars/modelchecker/SparseRobustDtmcParameterLiftingTest.cpp +++ b/src/test/storm-pars/modelchecker/SparseRobustDtmcParameterLiftingTest.cpp @@ -75,7 +75,7 @@ TYPED_TEST(SparseRobustDtmcParameterLiftingTest, Brp_Prob) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -109,7 +109,7 @@ TYPED_TEST(SparseRobustDtmcParameterLiftingTest, Brp_Prob_no_simplification) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -142,7 +142,7 @@ TYPED_TEST(SparseRobustDtmcParameterLiftingTest, Brp_Rew) { std::string constantsAsString = "pL=0.9,TOAck=0.5"; storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -174,7 +174,7 @@ TYPED_TEST(SparseRobustDtmcParameterLiftingTest, Brp_Rew_4Par) { std::string formulaAsString = "R>2.5 [F ((s=5) | (s=0&srep=3)) ]"; std::string constantsAsString = ""; //!! this model will have 4 parameters storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -207,7 +207,7 @@ TYPED_TEST(SparseRobustDtmcParameterLiftingTest, Crowds_Prob) { std::string constantsAsString = ""; // e.g. pL=0.9,TOACK=0.5 storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -243,7 +243,7 @@ TYPED_TEST(SparseRobustDtmcParameterLiftingTest, Crowds_Prob_1Par) { std::string constantsAsString = "badC=0.3"; // e.g. pL=0.9,TOACK=0.5 storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -276,7 +276,7 @@ TYPED_TEST(SparseRobustDtmcParameterLiftingTest, Crowds_Prob_Const) { std::string constantsAsString = "PF=0.9,badC=0.2"; storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -304,7 +304,7 @@ TYPED_TEST(SparseRobustDtmcParameterLiftingTest, ZeroConf) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = diff --git a/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionCheckerTest.cpp b/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionCheckerTest.cpp index 914fa0be98..96428dc0a6 100644 --- a/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionCheckerTest.cpp +++ b/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionCheckerTest.cpp @@ -38,7 +38,7 @@ TEST_F(AssumptionCheckerTest, Brp_no_bisimulation) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -112,7 +112,7 @@ TEST_F(AssumptionCheckerTest, Simple1) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -186,7 +186,7 @@ TEST_F(AssumptionCheckerTest, Casestudy1) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -261,7 +261,7 @@ TEST_F(AssumptionCheckerTest, Casestudy2) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -321,7 +321,7 @@ TEST_F(AssumptionCheckerTest, Casestudy3) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = diff --git a/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionMakerTest.cpp b/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionMakerTest.cpp index 23c22532a5..a16c0ddcc8 100644 --- a/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionMakerTest.cpp +++ b/src/test/storm-pars/modelchecker/region/monotonicity/AssumptionMakerTest.cpp @@ -36,7 +36,7 @@ TEST_F(AssumptionMakerTest, Brp_without_bisimulation) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -87,7 +87,7 @@ TEST_F(AssumptionMakerTest, Simple1) { std::string constantsAsString = ""; storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -140,7 +140,7 @@ TEST_F(AssumptionMakerTest, Casestudy1) { std::string constantsAsString = ""; storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = diff --git a/src/test/storm-pars/modelchecker/region/monotonicity/MonotonicityCheckerTest.cpp b/src/test/storm-pars/modelchecker/region/monotonicity/MonotonicityCheckerTest.cpp index 61369fd18a..82da761fdb 100644 --- a/src/test/storm-pars/modelchecker/region/monotonicity/MonotonicityCheckerTest.cpp +++ b/src/test/storm-pars/modelchecker/region/monotonicity/MonotonicityCheckerTest.cpp @@ -29,7 +29,7 @@ TEST_F(MonotonicityCheckerTest, Simple1_larger_region) { // model storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -78,7 +78,7 @@ TEST_F(MonotonicityCheckerTest, Simple1_small_region) { // model storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -128,7 +128,7 @@ TEST_F(MonotonicityCheckerTest, Casestudy1) { // model storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -182,7 +182,7 @@ TEST_F(MonotonicityCheckerTest, Casestudy2) { // model storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -237,7 +237,7 @@ TEST_F(MonotonicityCheckerTest, Casestudy3) { // model storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = diff --git a/src/test/storm-pars/modelchecker/region/monotonicity/MonotonicityHelperTest.cpp b/src/test/storm-pars/modelchecker/region/monotonicity/MonotonicityHelperTest.cpp index b5645e0df8..e5f2fa1bf9 100644 --- a/src/test/storm-pars/modelchecker/region/monotonicity/MonotonicityHelperTest.cpp +++ b/src/test/storm-pars/modelchecker/region/monotonicity/MonotonicityHelperTest.cpp @@ -112,7 +112,7 @@ TEST_F(MonotonicityHelperTest, Brp_with_bisimulation_no_samples) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -167,7 +167,7 @@ TEST_F(MonotonicityHelperTest, Brp_with_bisimulation_samples) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -222,7 +222,7 @@ TEST_F(MonotonicityHelperTest, zeroconf) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -276,7 +276,7 @@ TEST_F(MonotonicityHelperTest, Simple1) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -322,7 +322,7 @@ TEST_F(MonotonicityHelperTest, Casestudy1) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -364,7 +364,7 @@ TEST_F(MonotonicityHelperTest, CaseStudy2) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -397,7 +397,7 @@ TEST_F(MonotonicityHelperTest, Casestudy3_not_monotone) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -440,7 +440,7 @@ TEST_F(MonotonicityHelperTest, Casestudy3_monotone) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = diff --git a/src/test/storm-pars/modelchecker/region/monotonicity/OrderExtenderTest.cpp b/src/test/storm-pars/modelchecker/region/monotonicity/OrderExtenderTest.cpp index a50109532e..744a201ed0 100644 --- a/src/test/storm-pars/modelchecker/region/monotonicity/OrderExtenderTest.cpp +++ b/src/test/storm-pars/modelchecker/region/monotonicity/OrderExtenderTest.cpp @@ -33,7 +33,7 @@ TEST_F(OrderExtenderTest, Brp_with_bisimulation_on_model) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -85,7 +85,7 @@ TEST_F(OrderExtenderTest, Brp_without_bisimulation_on_model) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -116,7 +116,7 @@ TEST_F(OrderExtenderTest, Brp_with_bisimulation_on_matrix) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -173,7 +173,7 @@ TEST_F(OrderExtenderTest, Brp_without_bisimulation_on_matrix) { // Program and formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -213,7 +213,7 @@ TEST_F(OrderExtenderTest, simple1_on_model) { // model storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -251,7 +251,7 @@ TEST_F(OrderExtenderTest, simple1_on_matrix) { // model storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -305,7 +305,7 @@ TEST_F(OrderExtenderTest, casestudy1_on_model) { // model storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -343,7 +343,7 @@ TEST_F(OrderExtenderTest, casestudy1_on_matrix) { // model storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = @@ -397,7 +397,7 @@ TEST_F(OrderExtenderTest, casestudy2_on_matrix) { // model storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = diff --git a/src/test/storm-pars/transformer/BigStepTest.cpp b/src/test/storm-pars/transformer/BigStepTest.cpp index 6feb6f4f2b..76983aa7e2 100644 --- a/src/test/storm-pars/transformer/BigStepTest.cpp +++ b/src/test/storm-pars/transformer/BigStepTest.cpp @@ -22,11 +22,10 @@ #include "storm/storage/bisimulation/BisimulationType.h" #include "storm/storage/prism/Program.h" #include "storm/utility/constants.h" -#include "storm/utility/prism.h" void testModel(std::string programFile, std::string formulaAsString, std::string constantsAsString) { storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = diff --git a/src/test/storm-pars/transformer/BinaryDtmcTransformerTest.cpp b/src/test/storm-pars/transformer/BinaryDtmcTransformerTest.cpp index fa90e18171..16ec1448a1 100644 --- a/src/test/storm-pars/transformer/BinaryDtmcTransformerTest.cpp +++ b/src/test/storm-pars/transformer/BinaryDtmcTransformerTest.cpp @@ -21,11 +21,10 @@ #include "storm/storage/bisimulation/BisimulationType.h" #include "storm/storage/prism/Program.h" #include "storm/utility/constants.h" -#include "storm/utility/prism.h" void testModelB(std::string programFile, std::string formulaAsString, std::string constantsAsString) { storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = diff --git a/src/test/storm-pars/transformer/IntervalEndComponentPreserverCheckTest.cpp b/src/test/storm-pars/transformer/IntervalEndComponentPreserverCheckTest.cpp index 5c0e9e5ba4..4d8a022aad 100644 --- a/src/test/storm-pars/transformer/IntervalEndComponentPreserverCheckTest.cpp +++ b/src/test/storm-pars/transformer/IntervalEndComponentPreserverCheckTest.cpp @@ -25,12 +25,11 @@ #include "storm/solver/OptimizationDirection.h" #include "storm/storage/prism/Program.h" #include "storm/utility/constants.h" -#include "storm/utility/prism.h" #include "storm/utility/vector.h" void testModelInterval(std::string programFile, std::string formulaAsString, std::string constantsAsString) { storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaAsString, program)); std::shared_ptr> model = diff --git a/src/test/storm-pomdp/analysis/QualitativeAnalysisTest.cpp b/src/test/storm-pomdp/analysis/QualitativeAnalysisTest.cpp index 19db68f76d..6a9a1ce3d1 100644 --- a/src/test/storm-pomdp/analysis/QualitativeAnalysisTest.cpp +++ b/src/test/storm-pomdp/analysis/QualitativeAnalysisTest.cpp @@ -15,7 +15,7 @@ void graphalgorithm_test(std::string const& path, std::string const& constants, std::string formulaString) { storm::prism::Program program = storm::parser::PrismParser::parse(path); - program = storm::utility::prism::preprocess(program, constants); + program = program.preprocess(constants); std::shared_ptr formula = storm::api::parsePropertiesForPrismProgram(formulaString, program).front().getRawFormula(); std::shared_ptr> pomdp = storm::api::buildSparseModel(program, {formula})->as>(); @@ -32,7 +32,7 @@ void graphalgorithm_test(std::string const& path, std::string const& constants, void oneshot_test(std::string const& path, std::string const& constants, std::string formulaString, uint64_t lookahead) { storm::prism::Program program = storm::parser::PrismParser::parse(path); - program = storm::utility::prism::preprocess(program, constants); + program = program.preprocess(constants); std::shared_ptr formula = storm::api::parsePropertiesForPrismProgram(formulaString, program).front().getRawFormula(); std::shared_ptr> pomdp = storm::api::buildSparseModel(program, {formula})->as>(); @@ -52,7 +52,7 @@ void oneshot_test(std::string const& path, std::string const& constants, std::st void iterativesearch_test(std::string const& path, std::string const& constants, std::string formulaString, bool wr) { storm::prism::Program program = storm::parser::PrismParser::parse(path); - program = storm::utility::prism::preprocess(program, constants); + program = program.preprocess(constants); std::shared_ptr formula = storm::api::parsePropertiesForPrismProgram(formulaString, program).front().getRawFormula(); std::shared_ptr> pomdp = storm::api::buildSparseModel(program, {formula})->as>(); @@ -79,7 +79,7 @@ void iterativesearch_test(std::string const& path, std::string const& constants, void symbolicbelsup_test(std::string const& path, std::string const& constants, std::string formulaString, bool wr) { storm::prism::Program program = storm::parser::PrismParser::parse(path); - program = storm::utility::prism::preprocess(program, constants); + program = program.preprocess(constants); std::shared_ptr formula = storm::api::parsePropertiesForPrismProgram(formulaString, program).front().getRawFormula(); std::shared_ptr> pomdp = storm::api::buildSparseModel(program, {formula})->as>(); diff --git a/src/test/storm-pomdp/api/BeliefExplorationAPITest.cpp b/src/test/storm-pomdp/api/BeliefExplorationAPITest.cpp index b0eab0f768..f168ab2a4e 100644 --- a/src/test/storm-pomdp/api/BeliefExplorationAPITest.cpp +++ b/src/test/storm-pomdp/api/BeliefExplorationAPITest.cpp @@ -52,7 +52,7 @@ class BeliefExplorationAPITest : public ::testing::Test { Input buildPrism(std::string const& programFile, std::string const& formulaAsString, std::string const& constantsAsString = "") const { // Parse and build input storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); Input input; input.formula = storm::api::parsePropertiesForPrismProgram(formulaAsString, program).front().getRawFormula(); input.model = storm::api::buildSparseModel(program, {input.formula})->template as>(); diff --git a/src/test/storm-pomdp/modelchecker/BeliefExplorationPomdpModelCheckerTest.cpp b/src/test/storm-pomdp/modelchecker/BeliefExplorationPomdpModelCheckerTest.cpp index 5867968f4a..a8468bcf79 100644 --- a/src/test/storm-pomdp/modelchecker/BeliefExplorationPomdpModelCheckerTest.cpp +++ b/src/test/storm-pomdp/modelchecker/BeliefExplorationPomdpModelCheckerTest.cpp @@ -237,7 +237,7 @@ class BeliefExplorationPomdpModelCheckerTest : public ::testing::Test { Input buildPrism(std::string const& programFile, std::string const& formulaAsString, std::string const& constantsAsString = "") const { // Parse and build input storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsAsString); + program = program.preprocess(constantsAsString); Input input; input.formula = storm::api::parsePropertiesForPrismProgram(formulaAsString, program).front().getRawFormula(); input.model = storm::api::buildSparseModel(program, {input.formula})->template as>(); diff --git a/src/test/storm-pomdp/tracking/BeliefSupportTrackingTest.cpp b/src/test/storm-pomdp/tracking/BeliefSupportTrackingTest.cpp index f623bb5125..2c53e8d754 100644 --- a/src/test/storm-pomdp/tracking/BeliefSupportTrackingTest.cpp +++ b/src/test/storm-pomdp/tracking/BeliefSupportTrackingTest.cpp @@ -20,7 +20,7 @@ TEST(BeliefSupportTracking, Maze) { GTEST_SKIP() << "Z3 not available."; #endif storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism"); - program = storm::utility::prism::preprocess(program, "sl=0.4"); + program = program.preprocess("sl=0.4"); std::shared_ptr formula = storm::api::parsePropertiesForPrismProgram("Pmax=? [F \"goal\" ]", program).front().getRawFormula(); std::shared_ptr> pomdp = storm::api::buildSparseModel(program, {formula})->as>(); diff --git a/src/test/storm-pomdp/tracking/NondeterministicBeliefTrackerTest.cpp b/src/test/storm-pomdp/tracking/NondeterministicBeliefTrackerTest.cpp index a5fe161917..f8d09cf373 100644 --- a/src/test/storm-pomdp/tracking/NondeterministicBeliefTrackerTest.cpp +++ b/src/test/storm-pomdp/tracking/NondeterministicBeliefTrackerTest.cpp @@ -12,7 +12,7 @@ namespace { std::shared_ptr> buildMaze(std::string const& constants = "sl=0.0") { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism"); - program = storm::utility::prism::preprocess(program, constants); + program = program.preprocess(constants); auto formula = storm::api::parsePropertiesForPrismProgram("Pmax=? [F \"goal\" ]", program).front().getRawFormula(); auto model = storm::api::buildSparseModel(program, {formula})->as>(); storm::transformer::MakePOMDPCanonic makeCanonic(*model); diff --git a/src/test/storm-pomdp/transformation/MakeCanonicTest.cpp b/src/test/storm-pomdp/transformation/MakeCanonicTest.cpp index 3ca3ce4b8e..1d5cae0b34 100644 --- a/src/test/storm-pomdp/transformation/MakeCanonicTest.cpp +++ b/src/test/storm-pomdp/transformation/MakeCanonicTest.cpp @@ -15,7 +15,7 @@ TEST(MakeCanonic, Simple) { GTEST_SKIP() << "Z3 not available."; #endif storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism"); - program = storm::utility::prism::preprocess(program, "slippery=0.4"); + program = program.preprocess("slippery=0.4"); std::shared_ptr formula = storm::api::parsePropertiesForPrismProgram("Pmax=? [F \"goal\" ]", program).front().getRawFormula(); std::shared_ptr> pomdp = storm::api::buildSparseModel(program, {formula})->as>(); diff --git a/src/test/storm-pomdp/transformation/ObservationTraceUnfolderTest.cpp b/src/test/storm-pomdp/transformation/ObservationTraceUnfolderTest.cpp index 192aa8544b..f15b39eb51 100644 --- a/src/test/storm-pomdp/transformation/ObservationTraceUnfolderTest.cpp +++ b/src/test/storm-pomdp/transformation/ObservationTraceUnfolderTest.cpp @@ -14,7 +14,7 @@ TEST(ObservationTraceUnfolder, Simple) { GTEST_SKIP() << "Z3 not available."; #endif storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism"); - program = storm::utility::prism::preprocess(program, "slippery=0.4"); + program = program.preprocess("slippery=0.4"); std::shared_ptr formula = storm::api::parsePropertiesForPrismProgram("Pmax=? [F \"goal\" ]", program).front().getRawFormula(); std::shared_ptr> pomdp = storm::api::buildSparseModel(program, {formula})->as>(); diff --git a/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp b/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp index ce248f5a78..5fd16db96d 100644 --- a/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp +++ b/src/test/storm/builder/ExplicitPrismModelBuilderTest.cpp @@ -150,7 +150,7 @@ TEST_F(ExplicitPrismModelBuilderTest, Ma) { TEST_F(ExplicitPrismModelBuilderTest, POMdp) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pomdp/simple.prism"); - program = storm::utility::prism::preprocess(program, "slippery=0.4"); + program = program.preprocess("slippery=0.4"); std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(7ul, model->getNumberOfStates()); EXPECT_EQ(17ul, model->getNumberOfTransitions()); @@ -161,13 +161,13 @@ TEST_F(ExplicitPrismModelBuilderTest, POMdp) { EXPECT_EQ(6ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pomdp/maze2.prism"); - program = storm::utility::prism::preprocess(program, "sl=0.4"); + program = program.preprocess("sl=0.4"); model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(15ul, model->getNumberOfStates()); EXPECT_EQ(91ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pomdp/refuel.prism"); - program = storm::utility::prism::preprocess(program, "N=5"); + program = program.preprocess("N=5"); model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(126ul, model->getNumberOfStates()); EXPECT_EQ(547ul, model->getNumberOfTransitions()); @@ -175,13 +175,13 @@ TEST_F(ExplicitPrismModelBuilderTest, POMdp) { TEST_F(ExplicitPrismModelBuilderTest, Imdp) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/imdp/robot.prism"); - program = storm::utility::prism::preprocess(program, "delta=0.2"); + program = program.preprocess("delta=0.2"); std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(6ul, model->getNumberOfStates()); EXPECT_EQ(17ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/imdp/coin2.prism"); - program = storm::utility::prism::preprocess(program, "K=2,bias1=0.1"); + program = program.preprocess("K=2,bias1=0.1"); model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(272ul, model->getNumberOfStates()); EXPECT_EQ(492ul, model->getNumberOfTransitions()); @@ -189,7 +189,7 @@ TEST_F(ExplicitPrismModelBuilderTest, Imdp) { TEST_F(ExplicitPrismModelBuilderTest, SMG) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/smg/action_labels.prism"); - program = storm::utility::prism::preprocess(program, ""); + program = program.preprocess(""); std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).build(); EXPECT_EQ(3ul, model->getNumberOfStates()); EXPECT_EQ(3ul, model->getNumberOfChoices()); diff --git a/src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp index 2692e8c546..8a50c0e6a5 100644 --- a/src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/csl/CtmcCslModelCheckerTest.cpp @@ -230,7 +230,7 @@ class CtmcCslModelCheckerTest : public ::testing::Test { buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { std::pair, std::vector>> result; storm::prism::Program program = storm::api::parseProgram(pathToPrismFile, true); - program = storm::utility::prism::preprocess(program, constantDefinitionString); + program = program.preprocess(constantDefinitionString); if (TestType::engine == CtmcEngine::PrismSparse) { result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); result.first = storm::api::buildSparseModel(program, result.second)->template as(); @@ -249,7 +249,7 @@ class CtmcCslModelCheckerTest : public ::testing::Test { buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { std::pair, std::vector>> result; storm::prism::Program program = storm::api::parseProgram(pathToPrismFile, true); - program = storm::utility::prism::preprocess(program, constantDefinitionString); + program = program.preprocess(constantDefinitionString); if (TestType::engine == CtmcEngine::PrismHybrid) { result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); result.first = storm::api::buildSymbolicModel(program, result.second)->template as(); diff --git a/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp index 36e162ab5b..930a0cc11d 100644 --- a/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp @@ -294,7 +294,7 @@ class LraCtmcCslModelCheckerTest : public ::testing::Test { buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { std::pair, std::vector>> result; storm::prism::Program program = storm::api::parseProgram(pathToPrismFile, true); - program = storm::utility::prism::preprocess(program, constantDefinitionString); + program = program.preprocess(constantDefinitionString); if (TestType::engine == CtmcEngine::PrismSparse) { result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); result.first = storm::api::buildSparseModel(program, result.second)->template as(); @@ -313,7 +313,7 @@ class LraCtmcCslModelCheckerTest : public ::testing::Test { buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { std::pair, std::vector>> result; storm::prism::Program program = storm::api::parseProgram(pathToPrismFile, true); - program = storm::utility::prism::preprocess(program, constantDefinitionString); + program = program.preprocess(constantDefinitionString); if (TestType::engine == CtmcEngine::JaniHybrid) { auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); janiData.first.substituteFunctions(); diff --git a/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp b/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp index 083ca0d897..f8bdf576a2 100644 --- a/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/csl/MarkovAutomatonCslModelCheckerTest.cpp @@ -160,7 +160,7 @@ class MarkovAutomatonCslModelCheckerTest : public ::testing::Test { buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { std::pair, std::vector>> result; storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); - program = storm::utility::prism::preprocess(program, constantDefinitionString); + program = program.preprocess(constantDefinitionString); if (TestType::engine == MaEngine::PrismSparse) { result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); result.first = storm::api::buildSparseModel(program, result.second)->template as(); @@ -178,7 +178,7 @@ class MarkovAutomatonCslModelCheckerTest : public ::testing::Test { buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { std::pair, std::vector>> result; storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); - program = storm::utility::prism::preprocess(program, constantDefinitionString); + program = program.preprocess(constantDefinitionString); auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); result.second = storm::api::extractFormulasFromProperties(janiData.second); result.first = storm::api::buildSymbolicModel(janiData.first, result.second)->template as(); diff --git a/src/test/storm/modelchecker/lexicographic/LexicographicModelCheckingTest.cpp b/src/test/storm/modelchecker/lexicographic/LexicographicModelCheckingTest.cpp index e76c1f1572..59d1e7d448 100644 --- a/src/test/storm/modelchecker/lexicographic/LexicographicModelCheckingTest.cpp +++ b/src/test/storm/modelchecker/lexicographic/LexicographicModelCheckingTest.cpp @@ -21,7 +21,7 @@ TEST(LexicographicModelCheckingTest, prob_sched1) { std::string pathToPrismFile = STORM_TEST_RESOURCES_DIR "/mdp/prob_sched.prism"; std::pair>, std::vector>> modelFormulas; storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); - program = storm::utility::prism::preprocess(program, ""); + program = program.preprocess(""); modelFormulas.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasString, program)); modelFormulas.first = storm::api::buildSparseModel(program, modelFormulas.second)->template as>(); @@ -57,7 +57,7 @@ TEST(LexicographicModelCheckingTest, prob_sched2) { std::string pathToPrismFile = STORM_TEST_RESOURCES_DIR "/mdp/prob_sched.prism"; std::pair>, std::vector>> modelFormulas; storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); - program = storm::utility::prism::preprocess(program, ""); + program = program.preprocess(""); modelFormulas.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasString, program)); modelFormulas.first = storm::api::buildSparseModel(program, modelFormulas.second)->template as>(); diff --git a/src/test/storm/modelchecker/multiobjective/MultiObjectiveSchedRestModelCheckerTest.cpp b/src/test/storm/modelchecker/multiobjective/MultiObjectiveSchedRestModelCheckerTest.cpp index ddbec4d8c8..eaa5c3f54d 100644 --- a/src/test/storm/modelchecker/multiobjective/MultiObjectiveSchedRestModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/multiobjective/MultiObjectiveSchedRestModelCheckerTest.cpp @@ -263,7 +263,7 @@ TYPED_TEST(MultiObjectiveSchedRestModelCheckerTest, steps) { // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsString); + program = program.preprocess(constantsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = @@ -316,7 +316,7 @@ TYPED_TEST(MultiObjectiveSchedRestModelCheckerTest, mecs) { formulasAsString += "\nmulti(R{\"test\"}<=1 [C], P<=1 [F \"t2\"], P>=0.1 [F \"t1\"]);"; // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsString); + program = program.preprocess(constantsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = @@ -393,7 +393,7 @@ TYPED_TEST(MultiObjectiveSchedRestModelCheckerTest, compromise) { formulasAsString += "\nmulti(R{\"test\"}min=? [C], Pmin=? [F x=2 ], Pmin=? [F x=3]);"; // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsString); + program = program.preprocess(constantsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = @@ -456,7 +456,7 @@ TYPED_TEST(MultiObjectiveSchedRestModelCheckerTest, infrew) { std::string formulasAsString = "multi(R{\"one\"}min=? [ F x=2], R{\"two\"}min=? [ C ]);"; // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsString); + program = program.preprocess(constantsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = diff --git a/src/test/storm/modelchecker/multiobjective/PcaaWeightVectorCheckerTest.cpp b/src/test/storm/modelchecker/multiobjective/PcaaWeightVectorCheckerTest.cpp index 664c80f75f..31ecabb288 100644 --- a/src/test/storm/modelchecker/multiobjective/PcaaWeightVectorCheckerTest.cpp +++ b/src/test/storm/modelchecker/multiobjective/PcaaWeightVectorCheckerTest.cpp @@ -89,7 +89,7 @@ class PcaaWeightVectorCheckerTest : public ::testing::Test { std::pair>, std::vector>> getMdpAndFormulasFromPrism( std::string const& prismFileString, std::string const& constantsString, std::string const& formulasString) const { auto program = storm::api::parseProgram(prismFileString); - program = storm::utility::prism::preprocess(program, constantsString); + program = program.preprocess(constantsString); auto formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasString, program)); auto mdp = storm::api::buildSparseModel(program, formulas)->template as>(); return std::pair(std::move(mdp), std::move(formulas)); diff --git a/src/test/storm/modelchecker/multiobjective/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp b/src/test/storm/modelchecker/multiobjective/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp index f8f21c98f9..69bcb1b3cf 100644 --- a/src/test/storm/modelchecker/multiobjective/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp +++ b/src/test/storm/modelchecker/multiobjective/SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp @@ -29,7 +29,7 @@ TEST_F(SparseDtmcMultiDimensionalRewardUnfoldingTest, cost_bounded_die) { // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, ""); + program = program.preprocess(""); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> dtmc = @@ -63,7 +63,7 @@ TEST_F(SparseDtmcMultiDimensionalRewardUnfoldingTest, cost_bounded_leader) { // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, ""); + program = program.preprocess(""); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> dtmc = @@ -101,7 +101,7 @@ TEST_F(SparseDtmcMultiDimensionalRewardUnfoldingTest, cost_bounded_crowds) { // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, "CrowdSize=4"); + program = program.preprocess("CrowdSize=4"); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> dtmc = diff --git a/src/test/storm/modelchecker/multiobjective/SparseMaCbMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/multiobjective/SparseMaCbMultiObjectiveModelCheckerTest.cpp index 847e881e4e..6b427a526c 100644 --- a/src/test/storm/modelchecker/multiobjective/SparseMaCbMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/multiobjective/SparseMaCbMultiObjectiveModelCheckerTest.cpp @@ -32,7 +32,7 @@ TEST_F(SparseMaCbMultiObjectiveModelCheckerTest, server) { formulasAsString += "; multi(T>=16/9 [ F \"error\" ], P>=7/12 [ F \"processB\" ]) "; // false storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, ""); + program = program.preprocess(""); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> ma = diff --git a/src/test/storm/modelchecker/multiobjective/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/multiobjective/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp index 3acaa42916..b92e1a13b9 100644 --- a/src/test/storm/modelchecker/multiobjective/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/multiobjective/SparseMaPcaaMultiObjectiveModelCheckerTest.cpp @@ -73,7 +73,7 @@ TEST_F(SparseMaPcaaMultiObjectiveModelCheckerTest, server) { std::string formulasAsString = "multi(Tmax=? [ F \"error\" ], Pmax=? [ F \"processB\" ]) "; // pareto storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, ""); + program = program.preprocess(""); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> ma = @@ -124,7 +124,7 @@ TEST_F(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_pareto_3Obj) { "multi(Tmin=? [ F \"all_jobs_finished\" ], Pmax=? [ F<=0.2 \"half_of_jobs_finished\" ], Pmin=? [ F \"slowest_before_fastest\" ]) "; storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, ""); + program = program.preprocess(""); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> ma = @@ -166,7 +166,7 @@ TEST_F(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_achievability_3O "; multi(T<=1.29 [ F \"all_jobs_finished\" ], P>=0.18 [ F<=0.2 \"half_of_jobs_finished\" ], P<=0.29 [ F \"slowest_before_fastest\" ])"; // false storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, ""); + program = program.preprocess(""); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> ma = @@ -195,7 +195,7 @@ TEST_F(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_quantitative_3Ob "; multi(T<=1.26 [ F \"all_jobs_finished\" ], P>=0.2 [ F<=0.2 \"half_of_jobs_finished\" ], Pmin=? [ F \"slowest_before_fastest\" ])"; // false storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, ""); + program = program.preprocess(""); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> ma = @@ -222,7 +222,7 @@ TEST_F(SparseMaPcaaMultiObjectiveModelCheckerTest, jobscheduler_pareto_2Obj) { std::string formulasAsString = "multi( Pmax=? [ F<=0.1 \"one_job_finished\"], Pmin=? [F<=0.2 \"all_jobs_finished\"]) "; storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, ""); + program = program.preprocess(""); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> ma = @@ -426,7 +426,7 @@ TEST_F(SparseMaPcaaMultiObjectiveModelCheckerTest, polling) { // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsDefStr); + program = program.preprocess(constantsDefStr); program.checkValidity(); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); diff --git a/src/test/storm/modelchecker/multiobjective/SparseMdpCbMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/multiobjective/SparseMdpCbMultiObjectiveModelCheckerTest.cpp index 99eb25c299..c3cfa3bf69 100644 --- a/src/test/storm/modelchecker/multiobjective/SparseMdpCbMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/multiobjective/SparseMdpCbMultiObjectiveModelCheckerTest.cpp @@ -32,7 +32,7 @@ TEST_F(SparseMdpCbMultiObjectiveModelCheckerTest, consensus) { // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, ""); + program = program.preprocess(""); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = @@ -59,7 +59,7 @@ TEST_F(SparseMdpCbMultiObjectiveModelCheckerTest, zeroconf) { // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, ""); + program = program.preprocess(""); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = @@ -80,7 +80,7 @@ TEST_F(SparseMdpCbMultiObjectiveModelCheckerTest, team3with3objectives) { // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, ""); + program = program.preprocess(""); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = storm::api::buildSparseModel(program, diff --git a/src/test/storm/modelchecker/multiobjective/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp b/src/test/storm/modelchecker/multiobjective/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp index 9f038905ff..3a8b26b949 100644 --- a/src/test/storm/modelchecker/multiobjective/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp +++ b/src/test/storm/modelchecker/multiobjective/SparseMdpMultiDimensionalRewardUnfoldingTest.cpp @@ -37,7 +37,7 @@ TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_one_dim_walk_sma // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsDef); + program = program.preprocess(constantsDef); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = @@ -84,7 +84,7 @@ TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_one_dim_walk_lar // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsDef); + program = program.preprocess(constantsDef); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = @@ -121,7 +121,7 @@ TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_tiny_ec) { // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsDef); + program = program.preprocess(constantsDef); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = @@ -179,7 +179,7 @@ TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_zeroconf_dl) { // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsDef); + program = program.preprocess(constantsDef); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); @@ -207,7 +207,7 @@ TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_csma) { // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsDef); + program = program.preprocess(constantsDef); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = @@ -239,7 +239,7 @@ TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, single_obj_lower_bounds) { // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsDef); + program = program.preprocess(constantsDef); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = @@ -302,7 +302,7 @@ TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, one_dim_walk_small) { // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsDef); + program = program.preprocess(constantsDef); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = @@ -379,7 +379,7 @@ TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, one_dim_walk_large) { // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsDef); + program = program.preprocess(constantsDef); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = @@ -423,7 +423,7 @@ TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, tiny_ec) { // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsDef); + program = program.preprocess(constantsDef); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = @@ -491,7 +491,7 @@ TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, zeroconf_dl) { // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsDef); + program = program.preprocess(constantsDef); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); @@ -520,7 +520,7 @@ TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, csma) { // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsDef); + program = program.preprocess(constantsDef); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = @@ -558,7 +558,7 @@ TEST_F(SparseMdpMultiDimensionalRewardUnfoldingTest, lower_bounds) { // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsDef); + program = program.preprocess(constantsDef); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = diff --git a/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp b/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp index 9d1fdc66a5..155546df61 100644 --- a/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/multiobjective/SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp @@ -155,7 +155,7 @@ TEST_F(SparseMdpPcaaMultiObjectiveModelCheckerTest, simple_memory) { // program, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, "p=0"); // qualitative version + program = program.preprocess("p=0"); // qualitative version program.checkValidity(); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); @@ -182,7 +182,7 @@ TEST_F(SparseMdpPcaaMultiObjectiveModelCheckerTest, simple_memory) { } program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, "p=0.1"); // quantitative version + program = program.preprocess("p=0.1"); // quantitative version program.checkValidity(); mdp = storm::builder::ExplicitModelBuilder(program, options).build()->as>(); @@ -221,7 +221,7 @@ TEST_F(SparseMdpPcaaMultiObjectiveModelCheckerTest, consensus) { // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, ""); + program = program.preprocess(""); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); @@ -251,7 +251,7 @@ TEST_F(SparseMdpPcaaMultiObjectiveModelCheckerTest, zeroconf) { // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, ""); + program = program.preprocess(""); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); @@ -274,7 +274,7 @@ TEST_F(SparseMdpPcaaMultiObjectiveModelCheckerTest, team3with3objectives) { // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, ""); + program = program.preprocess(""); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); @@ -295,7 +295,7 @@ TEST_F(SparseMdpPcaaMultiObjectiveModelCheckerTest, tiny_rewards_negative) { // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, ""); + program = program.preprocess(""); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); @@ -315,7 +315,7 @@ TEST_F(SparseMdpPcaaMultiObjectiveModelCheckerTest, scheduler) { // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, ""); + program = program.preprocess(""); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); @@ -336,7 +336,7 @@ TEST_F(SparseMdpPcaaMultiObjectiveModelCheckerTest, dpm) { // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, ""); + program = program.preprocess(""); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); std::shared_ptr> mdp = storm::api::buildSparseModel(program, formulas)->as>(); @@ -449,7 +449,7 @@ TEST_F(SparseMdpPcaaMultiObjectiveModelCheckerTest, resource_gathering) { // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsDef); + program = program.preprocess(constantsDef); program.checkValidity(); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); @@ -536,7 +536,7 @@ TEST_F(SparseMdpPcaaMultiObjectiveModelCheckerTest, uav) { std::string const formulasAsString = "multi(Pmax=? [F !\"timeExceeded\" & \"mission\" ], R{\"ROZ\"}min=? [ C ]);\n"; // pareto // programm, model, formula storm::prism::Program program = storm::api::parseProgram(programFile); - program = storm::utility::prism::preprocess(program, constantsDef); + program = program.preprocess(constantsDef); program.checkValidity(); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); diff --git a/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp index aaaaa1c63f..18b587534c 100644 --- a/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp @@ -555,7 +555,7 @@ class DtmcPrctlModelCheckerTest : public ::testing::Test { buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { std::pair, std::vector>> result; storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); - program = storm::utility::prism::preprocess(program, constantDefinitionString); + program = program.preprocess(constantDefinitionString); if (TestType::engine == DtmcEngine::PrismSparse) { result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); result.first = storm::api::buildSparseModel(program, result.second)->template as(); @@ -574,7 +574,7 @@ class DtmcPrctlModelCheckerTest : public ::testing::Test { buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { std::pair, std::vector>> result; storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); - program = storm::utility::prism::preprocess(program, constantDefinitionString); + program = program.preprocess(constantDefinitionString); if (TestType::engine == DtmcEngine::Hybrid || TestType::engine == DtmcEngine::PrismDd) { result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); result.first = storm::api::buildSymbolicModel(program, result.second)->template as(); diff --git a/src/test/storm/modelchecker/prctl/dtmc/RobustDtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/dtmc/RobustDtmcPrctlModelCheckerTest.cpp index 00253380ea..b7523fc7ec 100644 --- a/src/test/storm/modelchecker/prctl/dtmc/RobustDtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/dtmc/RobustDtmcPrctlModelCheckerTest.cpp @@ -61,7 +61,7 @@ void expectThrow(std::string const& path, std::string const& formulaString, void expectThrowPrism(std::string const& path, std::string const& formulaString) { storm::prism::Program program = storm::api::parseProgram(path); - program = storm::utility::prism::preprocess(program, ""); + program = program.preprocess(""); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parseProperties(formulaString)); std::shared_ptr> modelPtr = storm::api::buildSparseModel(program, formulas); @@ -101,7 +101,7 @@ void checkExplicitModelForQuantitativeResult(std::string const& path, std::strin void checkPrismModelForQuantitativeResult(std::string const& path, std::string const& formulaString, double min, double max) { storm::prism::Program program = storm::api::parseProgram(path); - program = storm::utility::prism::preprocess(program, ""); + program = program.preprocess(""); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parseProperties(formulaString)); std::shared_ptr> modelPtr = storm::api::buildSparseModel(program, formulas); @@ -225,7 +225,7 @@ void checkExplicitModelForQuantitativeResultRational(std::string const& path, st void checkPrismModelForQuantitativeResultRational(std::string const& path, std::string const& formulaString, storm::RationalNumber min, storm::RationalNumber max) { storm::prism::Program program = storm::api::parseProgram(path); - program = storm::utility::prism::preprocess(program, ""); + program = program.preprocess(""); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parseProperties(formulaString)); std::shared_ptr> modelPtr = storm::api::buildSparseModel(program, formulas); @@ -251,7 +251,7 @@ void checkPrismModelForQuantitativeResultRational(std::string const& path, std:: void makeUncertainAndCheckRational(std::string const& path, std::string const& formulaString, storm::RationalNumber amountOfUncertainty) { storm::prism::Program program = storm::api::parseProgram(path); - program = storm::utility::prism::preprocess(program, ""); + program = program.preprocess(""); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaString, program)); std::shared_ptr> modelPtr = storm::api::buildSparseModel(program, formulas); diff --git a/src/test/storm/modelchecker/prctl/mdp/ConditionalMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/ConditionalMdpPrctlModelCheckerTest.cpp index 39652c298d..746a45b248 100644 --- a/src/test/storm/modelchecker/prctl/mdp/ConditionalMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/ConditionalMdpPrctlModelCheckerTest.cpp @@ -192,7 +192,7 @@ class ConditionalMdpPrctlModelCheckerTest : public ::testing::Test { std::pair, std::vector>> buildModelFormulas( storm::prism::Program const& inputProgram, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { std::pair, std::vector>> result; - auto program = storm::utility::prism::preprocess(inputProgram, constantDefinitionString); + auto program = inputProgram.preprocess(constantDefinitionString); result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); result.first = storm::api::buildSparseModel(program, result.second)->template as(); return result; diff --git a/src/test/storm/modelchecker/prctl/mdp/LraMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/LraMdpPrctlModelCheckerTest.cpp index 2c8d66f0b2..032eda54aa 100644 --- a/src/test/storm/modelchecker/prctl/mdp/LraMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/LraMdpPrctlModelCheckerTest.cpp @@ -101,7 +101,7 @@ class LraMdpPrctlModelCheckerTest : public ::testing::Test { std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { std::pair, std::vector>> result; storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); - program = storm::utility::prism::preprocess(program, constantDefinitionString); + program = program.preprocess(constantDefinitionString); result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); result.first = storm::api::buildSparseModel(program, result.second)->template as(); return result; diff --git a/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp index bd712dd5fc..f04a4d22bc 100644 --- a/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/MdpPrctlModelCheckerTest.cpp @@ -580,7 +580,7 @@ class MdpPrctlModelCheckerTest : public ::testing::Test { buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { std::pair, std::vector>> result; storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); - program = storm::utility::prism::preprocess(program, constantDefinitionString); + program = program.preprocess(constantDefinitionString); if (TestType::engine == MdpEngine::PrismSparse) { result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); result.first = storm::api::buildSparseModel(program, result.second)->template as(); @@ -599,7 +599,7 @@ class MdpPrctlModelCheckerTest : public ::testing::Test { buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { std::pair, std::vector>> result; storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); - program = storm::utility::prism::preprocess(program, constantDefinitionString); + program = program.preprocess(constantDefinitionString); if (TestType::engine == MdpEngine::Hybrid || TestType::engine == MdpEngine::PrismDd) { result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); result.first = storm::api::buildSymbolicModel(program, result.second)->template as(); diff --git a/src/test/storm/modelchecker/prctl/mdp/QuantileQueryTest.cpp b/src/test/storm/modelchecker/prctl/mdp/QuantileQueryTest.cpp index 3d5d25c397..83bb576097 100644 --- a/src/test/storm/modelchecker/prctl/mdp/QuantileQueryTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/QuantileQueryTest.cpp @@ -75,7 +75,7 @@ class QuantileQueryTest : public ::testing::Test { std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { std::pair, std::vector>> result; storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); - program = storm::utility::prism::preprocess(program, constantDefinitionString); + program = program.preprocess(constantDefinitionString); result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); result.first = storm::api::buildSparseModel(program, result.second)->template as(); return result; diff --git a/src/test/storm/modelchecker/prctl/mdp/RobustMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/RobustMdpPrctlModelCheckerTest.cpp index 55a4dad35c..99da15b45f 100644 --- a/src/test/storm/modelchecker/prctl/mdp/RobustMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/RobustMdpPrctlModelCheckerTest.cpp @@ -113,7 +113,7 @@ void checkModel(std::string const& path, std::string const& formulaString, doubl void checkPrismModelForQuantitativeResult(std::string const& path, std::string const& formulaString, double minmin, double minmax, double maxmin, double maxmax, std::string constantsString) { storm::prism::Program program = storm::api::parseProgram(path); - program = storm::utility::prism::preprocess(program, constantsString); + program = program.preprocess(constantsString); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parseProperties(formulaString)); std::shared_ptr> modelPtr = storm::api::buildSparseModel(program, formulas); @@ -194,7 +194,7 @@ TEST(RobustMdpModelCheckerTest, RobotMinMaxTest) { void makeUncertainAndCheck(std::string const& path, std::string const& formulaString, double amountOfUncertainty) { storm::prism::Program program = storm::api::parseProgram(path); - program = storm::utility::prism::preprocess(program, ""); + program = program.preprocess(""); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaString, program)); std::shared_ptr> modelPtr = storm::api::buildSparseModel(program, formulas); @@ -228,7 +228,7 @@ void makeUncertainAndCheck(std::string const& path, std::string const& formulaSt void makeUncertainAndCheckRational(std::string const& path, std::string const& formulaString, storm::RationalNumber amountOfUncertainty) { storm::prism::Program program = storm::api::parseProgram(path); - program = storm::utility::prism::preprocess(program, ""); + program = program.preprocess(""); std::vector> formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaString, program)); std::shared_ptr> modelPtr = storm::api::buildSparseModel(program, formulas); diff --git a/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp index 92de1ddd40..77a0d3e21d 100644 --- a/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp @@ -90,7 +90,7 @@ class SchedulerGenerationMdpPrctlModelCheckerTest : public ::testing::Test { std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { std::pair>, std::vector>> result; storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); - program = storm::utility::prism::preprocess(program, constantDefinitionString); + program = program.preprocess(constantDefinitionString); result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program)); result.first = storm::api::buildSparseModel(program, result.second)->template as>(); return result; diff --git a/src/test/storm/storage/UmbTest.cpp b/src/test/storm/storage/UmbTest.cpp index 4ea6d72a5b..392eab728c 100644 --- a/src/test/storm/storage/UmbTest.cpp +++ b/src/test/storm/storage/UmbTest.cpp @@ -57,7 +57,7 @@ class UmbRoundTripTest : public ::testing::Test { // build model from prism file storm::prism::Program program = storm::parser::PrismParser::parse(prismfile, true); - program = storm::utility::prism::preprocess(program, constants); + program = program.preprocess(constants); auto builder = storm::builder::ExplicitModelBuilder(program, generatorOptions); auto model = builder.build(); From 7e0ba3173d837ed9c2ae9cafc2cdee9495a6f784 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 24 Jul 2026 00:34:48 +0200 Subject: [PATCH 3/3] Moved functionality from cli.h --- src/storm-parsers/api/properties.cpp | 4 +- .../storage/SymbolicModelDescription.cpp | 77 +++++++++++++-- src/storm/storage/SymbolicModelDescription.h | 11 +++ src/storm/storage/jani/Model.cpp | 4 +- src/storm/storage/prism/Program.cpp | 4 +- src/storm/utility/cli.cpp | 95 ------------------- src/storm/utility/cli.h | 18 ---- src/storm/utility/string.cpp | 14 +++ src/storm/utility/string.h | 5 + .../builder/ExplicitJaniModelBuilderTest.cpp | 6 +- 10 files changed, 110 insertions(+), 128 deletions(-) delete mode 100644 src/storm/utility/cli.cpp delete mode 100644 src/storm/utility/cli.h diff --git a/src/storm-parsers/api/properties.cpp b/src/storm-parsers/api/properties.cpp index 9ff95701c9..15aa0c49de 100644 --- a/src/storm-parsers/api/properties.cpp +++ b/src/storm-parsers/api/properties.cpp @@ -10,7 +10,7 @@ #include "storm/storage/jani/Model.h" #include "storm/storage/jani/Property.h" #include "storm/storage/prism/Program.h" -#include "storm/utility/cli.h" +#include "storm/utility/string.h" namespace storm { namespace api { @@ -19,7 +19,7 @@ boost::optional> parsePropertyFilter(std::string const& pr if (propertyFilter == "all") { return boost::none; } - std::vector propertyNames = storm::utility::cli::parseCommaSeparatedStrings(propertyFilter); + std::vector propertyNames = storm::utility::string::parseCommaSeparatedStrings(propertyFilter); std::set propertyNameSet(propertyNames.begin(), propertyNames.end()); return propertyNameSet; } diff --git a/src/storm/storage/SymbolicModelDescription.cpp b/src/storm/storage/SymbolicModelDescription.cpp index 5b313517da..a3d998a24c 100644 --- a/src/storm/storage/SymbolicModelDescription.cpp +++ b/src/storm/storage/SymbolicModelDescription.cpp @@ -1,12 +1,15 @@ #include "storm/storage/SymbolicModelDescription.h" -#include "storm/storage/jani/Automaton.h" -#include "storm/storage/jani/Model.h" -#include "storm/storage/jani/Property.h" +#include +#include "storm/adapters/RationalNumberAdapter.h" #include "storm/exceptions/InvalidOperationException.h" #include "storm/exceptions/InvalidTypeException.h" -#include "storm/utility/cli.h" +#include "storm/exceptions/WrongFormatException.h" +#include "storm/storage/jani/Automaton.h" +#include "storm/storage/jani/Model.h" +#include "storm/storage/jani/Property.h" +#include "storm/utility/constants.h" #include "storm/utility/macros.h" namespace storm { @@ -173,9 +176,9 @@ SymbolicModelDescription SymbolicModelDescription::preprocess( std::map SymbolicModelDescription::parseConstantDefinitions( std::string const& constantDefinitionString) const { if (this->isJaniModel()) { - return storm::utility::cli::parseConstantDefinitionString(this->asJaniModel().getManager(), constantDefinitionString); + return parseConstantDefinitionString(this->asJaniModel().getManager(), constantDefinitionString); } else { - return storm::utility::cli::parseConstantDefinitionString(this->asPrismProgram().getManager(), constantDefinitionString); + return parseConstantDefinitionString(this->asPrismProgram().getManager(), constantDefinitionString); } } @@ -237,5 +240,67 @@ std::ostream& operator<<(std::ostream& out, SymbolicModelDescription::ModelType } return out; } + +std::map parseConstantDefinitionString(storm::expressions::ExpressionManager const& manager, + std::string const& constantDefinitionString) { + std::map constantDefinitions; + std::set definedConstants; + + if (!constantDefinitionString.empty()) { + std::vector definitions; + boost::split(definitions, constantDefinitionString, boost::is_any_of(",")); + for (auto& definition : definitions) { + boost::trim(definition); + + std::size_t positionOfAssignmentOperator = definition.find('='); + STORM_LOG_THROW(positionOfAssignmentOperator != std::string::npos, storm::exceptions::WrongFormatException, + "Illegal constant definition string: syntax error."); + + std::string constantName = definition.substr(0, positionOfAssignmentOperator); + boost::trim(constantName); + std::string value = definition.substr(positionOfAssignmentOperator + 1); + boost::trim(value); + + if (manager.hasVariable(constantName)) { + auto const& variable = manager.getVariable(constantName); + STORM_LOG_THROW(definedConstants.find(variable) == definedConstants.end(), storm::exceptions::WrongFormatException, + "Illegally trying to define constant '" << constantName << "' twice."); + definedConstants.insert(variable); + + if (manager.hasVariable(value)) { + auto const& valueVariable = manager.getVariable(value); + STORM_LOG_THROW( + variable.getType() == valueVariable.getType(), storm::exceptions::WrongFormatException, + "Illegally trying to define constant '" << constantName << "' by constant '" << valueVariable.getName() << " of different type."); + constantDefinitions[variable] = valueVariable.getExpression(); + } else if (variable.hasBooleanType()) { + if (value == "true") { + constantDefinitions[variable] = manager.boolean(true); + } else if (value == "false") { + constantDefinitions[variable] = manager.boolean(false); + } else { + throw storm::exceptions::WrongFormatException() << "Illegal value for boolean constant: " << value << "."; + } + } else if (variable.hasIntegerType()) { + int_fast64_t integerValue = std::stoll(value); + constantDefinitions[variable] = manager.integer(integerValue); + } else if (variable.hasRationalType()) { + try { + storm::RationalNumber rationalValue = storm::utility::convertNumber(value); + constantDefinitions[variable] = manager.rational(rationalValue); + } catch (std::exception& e) { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, + "Illegal constant definition string '" << constantName << "=" << value << "': " << e.what()); + } + } + } else { + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, + "Illegal constant definition string: unknown undefined constant '" << constantName << "'."); + } + } + } + + return constantDefinitions; +} } // namespace storage } // namespace storm diff --git a/src/storm/storage/SymbolicModelDescription.h b/src/storm/storage/SymbolicModelDescription.h index afd54a5698..476f2e782d 100644 --- a/src/storm/storage/SymbolicModelDescription.h +++ b/src/storm/storage/SymbolicModelDescription.h @@ -1,7 +1,10 @@ #pragma once #include +#include +#include "storm/storage/expressions/Expression.h" +#include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/jani/Model.h" #include "storm/storage/prism/Program.h" @@ -64,5 +67,13 @@ class SymbolicModelDescription { std::ostream& operator<<(std::ostream& out, SymbolicModelDescription const& model); std::ostream& operator<<(std::ostream& out, SymbolicModelDescription::ModelType const& type); + +/*! + * Parses a comma-separated string of constant definitions (e.g. "k=5,epsilon=0.01") + * into a map from variables to their corresponding expressions. + * @throws WrongFormatException if the string is malformed or references unknown constants. + */ +std::map parseConstantDefinitionString(storm::expressions::ExpressionManager const& manager, + std::string const& constantDefinitionString); } // namespace storage } // namespace storm diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 70ef9cba5a..34c3b4391e 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -8,6 +8,7 @@ #include "storm/exceptions/NotImplementedException.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/solver/SmtSolver.h" +#include "storm/storage/SymbolicModelDescription.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/expressions/LinearityCheckVisitor.h" #include "storm/storage/jani/Automaton.h" @@ -26,7 +27,6 @@ #include "storm/storage/jani/visitor/CompositionInformationVisitor.h" #include "storm/storage/jani/visitor/JSONExporter.h" #include "storm/storage/jani/visitor/JaniExpressionSubstitutionVisitor.h" -#include "storm/utility/cli.h" #include "storm/utility/combinatorics.h" #include "storm/utility/macros.h" #include "storm/utility/vector.h" @@ -1159,7 +1159,7 @@ Model Model::preprocess(std::mappreprocess(storm::utility::cli::parseConstantDefinitionString(this->getManager(), constantDefinitionString)); + return this->preprocess(storm::storage::parseConstantDefinitionString(this->getManager(), constantDefinitionString)); } std::map Model::getConstantsSubstitution() const { diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index c8700cf2d6..7793b9479a 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -11,6 +11,7 @@ #include "storm/exceptions/OutOfRangeException.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/solver/SmtSolver.h" +#include "storm/storage/SymbolicModelDescription.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/jani/Model.h" #include "storm/storage/jani/Property.h" @@ -18,7 +19,6 @@ #include "storm/storage/prism/CompositionVisitor.h" #include "storm/storage/prism/Compositions.h" #include "storm/storage/prism/ToJaniConverter.h" -#include "storm/utility/cli.h" #include "storm/utility/macros.h" #include "storm/utility/solver.h" #include "storm/utility/vector.h" @@ -1164,7 +1164,7 @@ Program Program::preprocess(std::mappreprocess(storm::utility::cli::parseConstantDefinitionString(this->getManager(), constantDefinitionString)); + return this->preprocess(storm::storage::parseConstantDefinitionString(this->getManager(), constantDefinitionString)); } Program Program::labelUnlabelledCommands(std::map const& nameSuggestions) const { diff --git a/src/storm/utility/cli.cpp b/src/storm/utility/cli.cpp deleted file mode 100644 index 7e588f61fe..0000000000 --- a/src/storm/utility/cli.cpp +++ /dev/null @@ -1,95 +0,0 @@ -#include "storm/utility/cli.h" - -#include - -#include "storm/adapters/RationalNumberAdapter.h" -#include "storm/exceptions/WrongFormatException.h" -#include "storm/utility/constants.h" -#include "storm/utility/macros.h" - -namespace storm { -namespace utility { -namespace cli { - -std::map parseConstantDefinitionString(storm::expressions::ExpressionManager const& manager, - std::string const& constantDefinitionString) { - std::map constantDefinitions; - std::set definedConstants; - - if (!constantDefinitionString.empty()) { - // Parse the string that defines the undefined constants of the model and make sure that it contains exactly - // one value for each undefined constant of the model. - std::vector definitions; - boost::split(definitions, constantDefinitionString, boost::is_any_of(",")); - for (auto& definition : definitions) { - boost::trim(definition); - - // Check whether the token could be a legal constant definition. - std::size_t positionOfAssignmentOperator = definition.find('='); - STORM_LOG_THROW(positionOfAssignmentOperator != std::string::npos, storm::exceptions::WrongFormatException, - "Illegal constant definition string: syntax error."); - - // Now extract the variable name and the value from the string. - std::string constantName = definition.substr(0, positionOfAssignmentOperator); - boost::trim(constantName); - std::string value = definition.substr(positionOfAssignmentOperator + 1); - boost::trim(value); - - // Check whether the constant is a legal undefined constant of the program and if so, of what type it is. - if (manager.hasVariable(constantName)) { - // Get the actual constant and check whether it's in fact undefined. - auto const& variable = manager.getVariable(constantName); - STORM_LOG_THROW(definedConstants.find(variable) == definedConstants.end(), storm::exceptions::WrongFormatException, - "Illegally trying to define constant '" << constantName << "' twice."); - definedConstants.insert(variable); - - if (manager.hasVariable(value)) { - auto const& valueVariable = manager.getVariable(value); - STORM_LOG_THROW( - variable.getType() == valueVariable.getType(), storm::exceptions::WrongFormatException, - "Illegally trying to define constant '" << constantName << "' by constant '" << valueVariable.getName() << " of different type."); - constantDefinitions[variable] = valueVariable.getExpression(); - } else if (variable.hasBooleanType()) { - if (value == "true") { - constantDefinitions[variable] = manager.boolean(true); - } else if (value == "false") { - constantDefinitions[variable] = manager.boolean(false); - } else { - throw storm::exceptions::WrongFormatException() << "Illegal value for boolean constant: " << value << "."; - } - } else if (variable.hasIntegerType()) { - int_fast64_t integerValue = std::stoll(value); - constantDefinitions[variable] = manager.integer(integerValue); - } else if (variable.hasRationalType()) { - try { - storm::RationalNumber rationalValue = storm::utility::convertNumber(value); - constantDefinitions[variable] = manager.rational(rationalValue); - } catch (std::exception& e) { - STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, - "Illegal constant definition string '" << constantName << "=" << value << "': " << e.what()); - } - } - } else { - STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, - "Illegal constant definition string: unknown undefined constant '" << constantName << "'."); - } - } - } - - return constantDefinitions; -} - -std::vector parseCommaSeparatedStrings(std::string const& input) { - std::vector result; - if (!input.empty()) { - boost::split(result, input, boost::is_any_of(",")); - for (auto& entry : result) { - boost::trim(entry); - } - } - return result; -} - -} // namespace cli -} // namespace utility -} // namespace storm diff --git a/src/storm/utility/cli.h b/src/storm/utility/cli.h deleted file mode 100644 index a32884a806..0000000000 --- a/src/storm/utility/cli.h +++ /dev/null @@ -1,18 +0,0 @@ -#pragma once - -#include - -#include "storm/storage/expressions/Expression.h" -#include "storm/storage/expressions/ExpressionManager.h" - -namespace storm { -namespace utility { -namespace cli { - -std::map parseConstantDefinitionString(storm::expressions::ExpressionManager const& manager, - std::string const& constantDefinitionString); - -std::vector parseCommaSeparatedStrings(std::string const& input); -} // namespace cli -} // namespace utility -} // namespace storm diff --git a/src/storm/utility/string.cpp b/src/storm/utility/string.cpp index 868ad8cc2c..374f3eea96 100644 --- a/src/storm/utility/string.cpp +++ b/src/storm/utility/string.cpp @@ -1,5 +1,8 @@ #include "storm/utility/string.h" + #include +#include +#include namespace storm { namespace utility { @@ -69,6 +72,17 @@ uint64_t levenshteinDistance(std::string const& lhs, std::string const& rhs, boo } return d.back().back(); } + +std::vector parseCommaSeparatedStrings(std::string const& input) { + std::vector result; + if (!input.empty()) { + boost::split(result, input, boost::is_any_of(",")); + for (auto& entry : result) { + boost::trim(entry); + } + } + return result; +} } // namespace string } // namespace utility } // namespace storm diff --git a/src/storm/utility/string.h b/src/storm/utility/string.h index 4bb4c93257..bff21b5f84 100644 --- a/src/storm/utility/string.h +++ b/src/storm/utility/string.h @@ -58,6 +58,11 @@ class SimilarStrings { * Levenstein distance to find similar strings */ uint64_t levenshteinDistance(std::string const& lhs, std::string const& rhs, bool caseSensitive = true); + +/*! + * Splits the input string on commas and trims whitespace from each element. + */ +std::vector parseCommaSeparatedStrings(std::string const& input); } // namespace string } // namespace utility } // namespace storm diff --git a/src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp b/src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp index a401b84160..20d9826e23 100644 --- a/src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp +++ b/src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp @@ -10,8 +10,8 @@ #include "storm/models/sparse/MarkovAutomaton.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/settings/SettingMemento.h" +#include "storm/storage/SymbolicModelDescription.h" #include "storm/storage/jani/Model.h" -#include "storm/utility/cli.h" namespace { @@ -71,7 +71,7 @@ TEST_F(ExplicitJaniModelBuilderTest, Dtmc) { EXPECT_EQ(2505ul, model->getNumberOfTransitions()); janiModel = storm::api::parseJaniModel(STORM_TEST_RESOURCES_DIR "/dtmc/test_trigonometry.jani").first; - auto constants = storm::utility::cli::parseConstantDefinitionString(janiModel.getManager(), "step_size_rad=0.523599"); // step_size = 30 deg + auto constants = storm::storage::parseConstantDefinitionString(janiModel.getManager(), "step_size_rad=0.523599"); // step_size = 30 deg janiModel = janiModel.defineUndefinedConstants(constants); model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(5ul, model->getNumberOfStates()); @@ -199,7 +199,7 @@ TEST_F(ExplicitJaniModelBuilderTest, Ma) { EXPECT_EQ(7ul, model->as>()->getMarkovianStates().getNumberOfSetBits()); janiModel = storm::api::parseJaniModel(STORM_TEST_RESOURCES_DIR "/ma/ftwc.jani").first; - auto constants = storm::utility::cli::parseConstantDefinitionString(janiModel.getManager(), "N=2,TIME_BOUND=1"); + auto constants = storm::storage::parseConstantDefinitionString(janiModel.getManager(), "N=2,TIME_BOUND=1"); janiModel = janiModel.defineUndefinedConstants(constants); model = storm::builder::ExplicitModelBuilder(janiModel).build(); EXPECT_EQ(1536ul, model->getNumberOfStates());