Testcase for replacing of unassigned variables.

5 years ago · 2b55302a4b
2 changed files with 218 additions and 0 deletions
--- a/resources/examples/testfiles/mdp/unassigned-variables.jani
+++ 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": []
 }
--- 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<double>(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<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
    EXPECT_EQ(25ul, model->getNumberOfStates());
    EXPECT_EQ(81ul, model->getNumberOfTransitions());
 }