From 4f25312a6b093f7885609471ea6146185ddc6ca6 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 29 Aug 2014 18:36:43 +0200
Subject: [PATCH] Adapted SMT-based counterexample generator such that it works
 with the new property classes.

Former-commit-id: 359a4c706f98cb162aa92f421d4a4116685f1707
---
 src/counterexamples/SMTMinimalCommandSetGenerator.h | 8 ++++----
 src/storm.cpp                                       | 2 +-
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h
index 06cdfd3a7..bac940957 100644
--- a/src/counterexamples/SMTMinimalCommandSetGenerator.h
+++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h
@@ -1781,11 +1781,11 @@ namespace storm {
 #endif
             }
             
-            static void computeCounterexample(storm::prism::Program program, std::string const& constantDefinitionString, storm::models::Mdp<T> const& labeledMdp,  storm::property::prctl::AbstractPrctlFormula<double> const* formulaPtr) {
+            static void computeCounterexample(storm::prism::Program program, std::string const& constantDefinitionString, storm::models::Mdp<T> const& labeledMdp, std::shared_ptr<storm::properties::prctl::AbstractPrctlFormula<double> const> formula) {
 #ifdef STORM_HAVE_Z3
-                std::cout << std::endl << "Generating minimal label counterexample for formula " << formulaPtr->toString() << std::endl;
+                std::cout << std::endl << "Generating minimal label counterexample for formula " << formula->toString() << std::endl;
                 // First, we need to check whether the current formula is an Until-Formula.
-                std::shared_ptr<storm::properties::prctl::ProbabilisticBoundOperator<double>> probBoundFormula = std::dynamic_pointer_cast<storm::properties::prctl::ProbabilisticBoundOperator<double>>(formulaPtr);
+                std::shared_ptr<storm::properties::prctl::ProbabilisticBoundOperator<double> const> probBoundFormula = std::dynamic_pointer_cast<storm::properties::prctl::ProbabilisticBoundOperator<double>>(formula);
                 if (probBoundFormula.get() == nullptr) {
                     LOG4CPLUS_ERROR(logger, "Illegal formula " << probBoundFormula->toString() << " for counterexample generation.");
                     throw storm::exceptions::InvalidPropertyException() << "Illegal formula " << probBoundFormula->toString() << " for counterexample generation.";
@@ -1800,7 +1800,7 @@ namespace storm {
                 
                 // Now derive the probability threshold we need to exceed as well as the phi and psi states. Simultaneously, check whether the formula is of a valid shape.
                 double bound = probBoundFormula->getBound();
-                std::shared_ptr<storm::properties::prctl::AbstractPathFormula<double>> pathFormula = probBoundFormula->getPathFormula();
+                std::shared_ptr<storm::properties::prctl::AbstractPathFormula<double> const> pathFormula = probBoundFormula->getChild();
                 storm::storage::BitVector phiStates;
                 storm::storage::BitVector psiStates;
                 storm::modelchecker::prctl::SparseMdpPrctlModelChecker<T> modelchecker(labeledMdp);
diff --git a/src/storm.cpp b/src/storm.cpp
index bd3634d76..a3328ae92 100644
--- a/src/storm.cpp
+++ b/src/storm.cpp
@@ -37,7 +37,7 @@
 #include "src/solver/GmmxxNondeterministicLinearEquationSolver.h"
 #include "src/solver/GurobiLpSolver.h"
 #include "src/counterexamples/MILPMinimalLabelSetGenerator.h"
-// #include "src/counterexamples/SMTMinimalCommandSetGenerator.h"
+#include "src/counterexamples/SMTMinimalCommandSetGenerator.h"
 #include "src/counterexamples/PathBasedSubsystemGenerator.h"
 #include "src/parser/AutoParser.h"
 #include "src/parser/MarkovAutomatonParser.h"