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 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> nextStateGenerator = std::make_shared>(janiModel, options); - ASSERT_THROW(storm::builder::ExplicitModelBuilder(janiModel).build(), storm::exceptions::WrongFormatException); + ASSERT_THROW(storm::builder::ExplicitModelBuilder(nextStateGenerator).build(), storm::exceptions::WrongFormatException); }