From 80382da0337689791dd8233972c6a5a1ce50b57b Mon Sep 17 00:00:00 2001
From: tomjanson <tom.janson@rwth-aachen.de>
Date: Wed, 16 Nov 2016 18:34:35 +0100
Subject: [PATCH] adapt KSP test cases to new API; still fail

Former-commit-id: 984f4f9b69363caa3a98dd717fda82d812b92180 [formerly 5de4e31bc8d7a48484b1206aa43f032e91ceed64]
Former-commit-id: c41eea12e8a5d2214b459639b374e8ee26a05289
---
 test/functional/utility/KSPTest.cpp | 35 ++++++++++++++++-------------
 1 file changed, 19 insertions(+), 16 deletions(-)

diff --git a/test/functional/utility/KSPTest.cpp b/test/functional/utility/KSPTest.cpp
index 1e1dd3070..aba8747c3 100644
--- a/test/functional/utility/KSPTest.cpp
+++ b/test/functional/utility/KSPTest.cpp
@@ -1,9 +1,10 @@
 #include "gtest/gtest.h"
 #include "storm-config.h"
 
-#include "src/parser/PrismParser.h"
+#include "src/builder/ExplicitModelBuilder.h"
 #include "src/models/sparse/Dtmc.h"
-#include "src/builder/ExplicitPrismModelBuilder.h"
+#include "src/parser/PrismParser.h"
+#include "src/storage/SymbolicModelDescription.h"
 #include "src/utility/graph.h"
 #include "src/utility/shortestPaths.cpp"
 
@@ -12,9 +13,17 @@
 //       more than that.
 //       An independent verification of the values would be really nice ...
 
+// FIXME: (almost) all of these fail; the question is: is there actually anything wrong or does the new parser yield a different order of states?
+
+std::shared_ptr<storm::models::sparse::Model<double>> buildExampleModel() {
+	std::string prismModelPath = STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm";
+    storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(prismModelPath);
+    storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
+    return storm::builder::ExplicitModelBuilder<double>(program).build();
+}
+
 TEST(KSPTest, dijkstra) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
-    std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+	auto model = buildExampleModel();
 
     storm::storage::sparse::state_type testState = 300;
     storm::utility::ksp::ShortestPathsGenerator<double> spg(model, testState);
@@ -24,8 +33,7 @@ TEST(KSPTest, dijkstra) {
 }
 
 TEST(KSPTest, singleTarget) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
-    std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+	auto model = buildExampleModel();
 
     storm::storage::sparse::state_type testState = 300;
     storm::utility::ksp::ShortestPathsGenerator<double> spg(model, testState);
@@ -35,8 +43,7 @@ TEST(KSPTest, singleTarget) {
 }
 
 TEST(KSPTest, reentry) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
-    std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+	auto model = buildExampleModel();
 
     storm::storage::sparse::state_type testState = 300;
     storm::utility::ksp::ShortestPathsGenerator<double> spg(model, testState);
@@ -50,8 +57,7 @@ TEST(KSPTest, reentry) {
 }
 
 TEST(KSPTest, groupTarget) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
-    std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+	auto model = buildExampleModel();
 
     auto groupTarget = storm::utility::ksp::state_list_t{50, 90};
     auto spg = storm::utility::ksp::ShortestPathsGenerator<double>(model, groupTarget);
@@ -70,8 +76,7 @@ TEST(KSPTest, groupTarget) {
 }
 
 TEST(KSPTest, kTooLargeException) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
-    std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+	auto model = buildExampleModel();
 
     storm::storage::sparse::state_type testState = 1;
     storm::utility::ksp::ShortestPathsGenerator<double> spg(model, testState);
@@ -80,8 +85,7 @@ TEST(KSPTest, kTooLargeException) {
 }
 
 TEST(KSPTest, kspStateSet) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
-    std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+	auto model = buildExampleModel();
 
     storm::storage::sparse::state_type testState = 300;
     storm::utility::ksp::ShortestPathsGenerator<double> spg(model, testState);
@@ -97,8 +101,7 @@ TEST(KSPTest, kspStateSet) {
 }
 
 TEST(KSPTest, kspPathAsList) {
-    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
-    std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitPrismModelBuilder<double>().translateProgram(program);
+	auto model = buildExampleModel();
 
     storm::storage::sparse::state_type testState = 300;
     storm::utility::ksp::ShortestPathsGenerator<double> spg(model, testState);