diff --git a/resources/examples/testfiles/mdp/unassigned-variables.jani b/resources/examples/testfiles/mdp/unassigned-variables.jani new file mode 100644 index 000000000..365fa726e --- /dev/null +++ b/resources/examples/testfiles/mdp/unassigned-variables.jani @@ -0,0 +1,210 @@ +{ + "actions": [], + "automata": [ + { + "edges": [ + { + "destinations": [ + { + "assignments": [ + { + "comment": "x <- 0", + "ref": "x", + "value": 0 + } + ], + "location": "l", + "probability": { + "comment": "(c / 2)", + "exp": { + "left": "c", + "op": "/", + "right": 2 + } + } + }, + { + "assignments": [ + { + "comment": "x <- (x + 1)", + "ref": "x", + "value": { + "left": "x", + "op": "+", + "right": 1 + } + } + ], + "location": "l", + "probability": { + "comment": "((2 - c) / 2)", + "exp": { + "left": { + "left": 2, + "op": "-", + "right": "c" + }, + "op": "/", + "right": 2 + } + } + } + ], + "guard": { + "comment": "(x < 4)", + "exp": { + "left": "x", + "op": "<", + "right": 4 + } + }, + "location": "l" + } + ], + "initial-locations": [ + "l" + ], + "locations": [ + { + "name": "l" + } + ], + "name": "first", + "variables": [ + { + "initial-value": 0, + "name": "x", + "type": { + "base": "int", + "kind": "bounded", + "lower-bound": 0, + "upper-bound": 4 + } + }, + { + "initial-value": 1, + "name": "c", + "type": "real" + } + ] + }, + { + "edges": [ + { + "destinations": [ + { + "assignments": [ + { + "comment": "y <- 0", + "ref": "y", + "value": 0 + } + ], + "location": "l", + "probability": { + "comment": "((c + 1) / 2)", + "exp": { + "left": { + "left": "c", + "op": "+", + "right": 1 + }, + "op": "/", + "right": 2 + } + } + }, + { + "assignments": [ + { + "comment": "y <- (y + 1)", + "ref": "y", + "value": { + "left": "y", + "op": "+", + "right": 1 + } + } + ], + "location": "l", + "probability": { + "comment": "((1 - c) / 2)", + "exp": { + "left": { + "left": 1, + "op": "-", + "right": "c" + }, + "op": "/", + "right": 2 + } + } + } + ], + "guard": { + "comment": "(y < 4)", + "exp": { + "left": "y", + "op": "<", + "right": 4 + } + }, + "location": "l" + } + ], + "initial-locations": [ + "l" + ], + "locations": [ + { + "name": "l" + } + ], + "name": "second", + "variables": [ + { + "initial-value": 0, + "name": "y", + "type": { + "base": "int", + "kind": "bounded", + "lower-bound": 0, + "upper-bound": 4 + } + }, + { + "name": "c", + "type": "int" + } + ] + } + ], + "constants": [ + { + "name": "c", + "type": "int", + "value": 0 + } + ], + "features": [ + "derived-operators" + ], + "jani-version": 1, + "name": "realVariables", + "properties": [], + "restrict-initial": { + "exp": true + }, + "system": { + "elements": [ + { + "automaton": "first" + }, + { + "automaton": "second" + } + ] + }, + "type": "mdp", + "variables": [] +} diff --git a/src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp b/src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp index 77cb171cd..5d632e56a 100644 --- a/src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp +++ b/src/test/storm/builder/ExplicitJaniModelBuilderTest.cpp @@ -147,3 +147,11 @@ TEST(ExplicitJaniModelBuilderTest, FailComposition) { STORM_SILENT_ASSERT_THROW(storm::builder::ExplicitModelBuilder(janiModel).build(), storm::exceptions::WrongFormatException); } + +TEST(ExplicitJaniModelBuilderTest, unassignedVariables) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/unassigned-variables.jani"); + storm::jani::Model janiModel = program.toJani(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(janiModel).build(); + EXPECT_EQ(25ul, model->getNumberOfStates()); + EXPECT_EQ(81ul, model->getNumberOfTransitions()); +}