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: 137bdc8d9b [formerly f0aab7368d]
Former-commit-id: f1ee093be3

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;

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);
 }