commit to switch workplace (no, not now)

Former-commit-id: b725946b28

src/abstraction/prism/AbstractProgram.h

@@ -7,6 +7,8 @@
 #include "src/abstraction/MenuGame.h"
 #include "src/abstraction/prism/AbstractModule.h"
 
+#include "src/storage/dd/Add.h"
+
 #include "src/storage/expressions/Expression.h"
 
 namespace storm {

src/abstraction/prism/PrismMenuGameAbstractor.cpp

@@ -8,7 +8,7 @@ namespace storm {
         namespace prism {
             
             template <storm::dd::DdType DdType, typename ValueType>
-            PrismMenuGameAbstractor<DdType, ValueType>::PrismMenuGameAbstractor(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory) : abstractProgram(expressionManager, program, initialPredicates, std::move(smtSolverFactory), storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isAddAllGuardsSet()) {
+            PrismMenuGameAbstractor<DdType, ValueType>::PrismMenuGameAbstractor(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : abstractProgram(expressionManager, program, initialPredicates, std::move(smtSolverFactory), storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isAddAllGuardsSet()) {
                 // Intentionally left empty.
             }
             

src/abstraction/prism/PrismMenuGameAbstractor.h

@@ -11,7 +11,7 @@ namespace storm {
             template <storm::dd::DdType DdType, typename ValueType>
             class PrismMenuGameAbstractor : public MenuGameAbstractor<DdType, ValueType> {
             public:
-                PrismMenuGameAbstractor(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory = std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
+                PrismMenuGameAbstractor(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory);
                 
                 virtual storm::abstraction::MenuGame<DdType, ValueType> abstract() override;
                 virtual void refine(std::vector<storm::expressions::Expression> const& predicates) override;

src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -1,7 +1,11 @@
 #include "src/modelchecker/abstraction/GameBasedMdpModelChecker.h"
 
+#include "src/models/symbolic/StandardRewardModel.h"
+
 #include "src/storage/expressions/ExpressionManager.h"
 
+#include "src/abstraction/prism/PrismMenuGameAbstractor.h"
+
 #include "src/logic/FragmentSpecification.h"
 
 #include "src/utility/macros.h"
@@ -14,7 +18,7 @@
 namespace storm {
     namespace modelchecker {
         template<storm::dd::DdType Type, typename ValueType>
-        GameBasedMdpModelChecker<Type, ValueType>::GameBasedMdpModelChecker(storm::prism::Program const& program, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory) : originalProgram(program), smtSolverFactory(std::move(smtSolverFactory)) {
+        GameBasedMdpModelChecker<Type, ValueType>::GameBasedMdpModelChecker(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory) : originalProgram(program), expressionManager(expressionManager), smtSolverFactory(std::move(smtSolverFactory)) {
             STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only DTMCs/MDPs are supported by the game-based model checker.");
                         
             // Start by preparing the program. That is, we flatten the modules if there is more than one.
@@ -53,6 +57,13 @@ namespace storm {
         std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ValueType>::performGameBasedAbstractionRefinement(CheckTask<storm::logic::Formula> const& checkTask, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) {
             STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidPropertyException, "The game-based abstraction refinement model checker can only compute the result for the initial states.");
 
+            std::vector<storm::expressions::Expression> initialPredicates;
+            initialPredicates.push_back(targetStateExpression);
+            if (!constraintExpression.isTrue() && !constraintExpression.isFalse()) {
+                initialPredicates.push_back(constraintExpression);
+            }
+            storm::abstraction::prism::PrismMenuGameAbstractor<Type, ValueType> abstractor(expressionManager, preprocessedProgram, initialPredicates, *smtSolverFactory);
+            
             // 1. build initial abstraction based on the the constraint expression (if not 'true') and the target state expression.
             
             // 2. solve the game wrt. to min/max as given by checkTask and min/max for the abstraction player to obtain two bounds.

src/modelchecker/abstraction/GameBasedMdpModelChecker.h

@@ -21,7 +21,7 @@ namespace storm {
              * @param program The program that implicitly specifies the model to check.
              * @param smtSolverFactory A factory used to create SMT solver when necessary.
              */
-            explicit GameBasedMdpModelChecker(storm::prism::Program const& program, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory = std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
+            explicit GameBasedMdpModelChecker(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory = std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
             
             virtual ~GameBasedMdpModelChecker() override;
                         
@@ -42,6 +42,9 @@ namespace storm {
             // original program.
             storm::prism::Program preprocessedProgram;
             
+            /// The expression manager over which to build expressions during the abstraction.
+            storm::expressions::ExpressionManager& expressionManager;
+            
             // A factory that is used for creating SMT solvers when needed.
             std::unique_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
         };