From 812e1c4235cd0aa3e2287901632d8d79166ef771 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Mon, 7 Nov 2016 11:31:26 +0100
Subject: [PATCH] adapted test to new check policy and made jani variable and
 expression variable have the same name in PRISM-to-JANI conversion

Former-commit-id: 137bdc8d9bb6bdcbfcccf56291ab9682abd950f7 [formerly f0aab7368d0d22325095c58d393196ee631a1527]
Former-commit-id: f1ee093be36799308c5200bb62a29e4528962cc3
---
 src/storage/prism/ToJaniConverter.cpp                    | 2 +-
 test/functional/builder/ExplicitJaniModelBuilderTest.cpp | 6 +++++-
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/src/storage/prism/ToJaniConverter.cpp b/src/storage/prism/ToJaniConverter.cpp
index c3297d8d3..bda7ae812 100644
--- a/src/storage/prism/ToJaniConverter.cpp
+++ b/src/storage/prism/ToJaniConverter.cpp
@@ -100,7 +100,7 @@ namespace storm {
             std::vector<storm::jani::Assignment> transientLocationAssignments;
             for (auto const& rewardModel : program.getRewardModels()) {
                 auto newExpressionVariable = manager->declareRationalVariable(rewardModel.getName().empty() ? "default" : rewardModel.getName());
-                storm::jani::RealVariable const& newTransientVariable = janiModel.addVariable(storm::jani::RealVariable(rewardModel.getName().empty() ? "defaultReward" : rewardModel.getName(), newExpressionVariable, manager->rational(0.0), true));
+                storm::jani::RealVariable const& newTransientVariable = janiModel.addVariable(storm::jani::RealVariable(rewardModel.getName().empty() ? "default" : rewardModel.getName(), newExpressionVariable, manager->rational(0.0), true));
                 
                 if (rewardModel.hasStateRewards()) {
                     storm::expressions::Expression transientLocationExpression;
diff --git a/test/functional/builder/ExplicitJaniModelBuilderTest.cpp b/test/functional/builder/ExplicitJaniModelBuilderTest.cpp
index 405b6d248..e4a94eda3 100644
--- a/test/functional/builder/ExplicitJaniModelBuilderTest.cpp
+++ b/test/functional/builder/ExplicitJaniModelBuilderTest.cpp
@@ -5,6 +5,7 @@
 #include "src/settings/SettingMemento.h"
 #include "src/parser/PrismParser.h"
 #include "src/builder/ExplicitModelBuilder.h"
+#include "src/generator/JaniNextStateGenerator.h"
 #include "src/storage/jani/Model.h"
 
 #include "src/settings/modules/IOSettings.h"
@@ -154,7 +155,10 @@ TEST(ExplicitJaniModelBuilderTest, FailComposition) {
 TEST(ExplicitJaniModelBuilderTest, IllegalSynchronizingWrites) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2-illegalSynchronizingWrite.nm");
     storm::jani::Model janiModel = program.toJani();
+    storm::generator::NextStateGeneratorOptions options;
+    options.setExplorationChecks(true);
+    std::shared_ptr<storm::generator::NextStateGenerator<double, uint32_t>> nextStateGenerator = std::make_shared<storm::generator::JaniNextStateGenerator<double, uint32_t>>(janiModel, options);
     
-    ASSERT_THROW(storm::builder::ExplicitModelBuilder<double>(janiModel).build(), storm::exceptions::WrongFormatException);
+    ASSERT_THROW(storm::builder::ExplicitModelBuilder<double>(nextStateGenerator).build(), storm::exceptions::WrongFormatException);
 }