From 29cfa574b87f0679a9f032e617cd73cfaa6226ef Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 3 Aug 2017 18:16:44 +0200 Subject: [PATCH] Bindings for instantiating constants in SymbolicModelDescriptions --- lib/stormpy/examples/files/dtmc/die.jani | 358 +++++++++++++++++++++++ src/core/input.cpp | 1 + src/storage/expressions.cpp | 11 + tests/core/test_modelchecking.py | 2 +- tests/core/test_parse.py | 6 +- tests/storage/test_model.py | 22 ++ 6 files changed, 396 insertions(+), 4 deletions(-) create mode 100644 lib/stormpy/examples/files/dtmc/die.jani diff --git a/lib/stormpy/examples/files/dtmc/die.jani b/lib/stormpy/examples/files/dtmc/die.jani new file mode 100644 index 0000000..415a55c --- /dev/null +++ b/lib/stormpy/examples/files/dtmc/die.jani @@ -0,0 +1,358 @@ +{ + "jani-version": 1, + "name": "die.jani", + "type": "dtmc", + "features": [ "derived-operators" ], + "variables": [ + { + "name": "s", + "type": { + "base": "int", + "kind": "bounded", + "lower-bound": 0, + "upper-bound": 7 + }, + "initial-value": 0 + }, + { + "name": "d", + "type": { + "base": "int", + "kind": "bounded", + "lower-bound": 0, + "upper-bound": 6 + }, + "initial-value": 0 + } + ], + "properties": [ + { + "name": "Probability to throw a six", + "expression": { + "op": "filter", + "fun": "max", + "states": { "op": "initial" }, + "values": { + "op": "Pmin", + "exp": { + "op": "U", + "left": true, + "right": { + "op": "∧", + "left": { + "op": "=", + "left": "s", + "right": 7 + }, + "right": { + "op": "=", + "left": "d", + "right": 6 + } + } + } + } + } + }, + { + "name": "Expected number of coin flips", + "expression": { + "op": "filter", + "fun": "max", + "states": { "op": "initial" }, + "values": { + "op": "Emin", + "accumulate": [ "steps" ], + "exp": 1, + "reach": { + "op": "=", + "left": "s", + "right": 7 + } + } + } + } + ], + "automata": [ + { + "name": "die", + "locations": [{ "name": "l" }], + "initial-locations": ["l"], + "edges": [ + { + "location": "l", + "guard": { + "exp": { + "op": "=", + "left": "s", + "right": 0 + } + }, + "destinations": [ + { + "location": "l", + "probability": { "exp": 0.5 }, + "assignments": [ + { + "ref": "s", + "value": 1 + } + ] + }, + { + "location": "l", + "probability": { "exp": 0.5 }, + "assignments": [ + { + "ref": "s", + "value": 2 + } + ] + } + ] + }, + { + "location": "l", + "guard": { + "exp": { + "left": "s", + "op": "=", + "right": 1 + } + }, + "destinations": [ + { + "location": "l", + "probability": { "exp": 0.5 }, + "assignments": [ + { + "ref": "s", + "value": 3 + } + ] + }, + { + "location": "l", + "probability": { "exp": 0.5 }, + "assignments": [ + { + "ref": "s", + "value": 4 + } + ] + } + ] + }, + { + "location": "l", + "guard": { + "exp": { + "left": "s", + "op": "=", + "right": 2 + } + }, + "destinations": [ + { + "location": "l", + "probability": { "exp": 0.5 }, + "assignments": [ + { + "ref": "s", + "value": 5 + } + ] + }, + { + "location": "l", + "probability": { "exp": 0.5 }, + "assignments": [ + { + "ref": "s", + "value": 6 + } + ] + } + ] + }, + { + "location": "l", + "guard": { + "exp": { + "left": "s", + "op": "=", + "right": 3 + } + }, + "destinations": [ + { + "location": "l", + "probability": { "exp": 0.5 }, + "assignments": [ + { + "ref": "s", + "value": 1 + } + ] + }, + { + "location": "l", + "probability": { "exp": 0.5 }, + "assignments": [ + { + "ref": "s", + "value": 7 + }, + { + "ref": "d", + "value": 1 + } + ] + } + ] + }, + { + "location": "l", + "guard": { + "exp": { + "left": "s", + "op": "=", + "right": 4 + } + }, + "destinations": [ + { + "location": "l", + "probability": { "exp": 0.5 }, + "assignments": [ + { + "ref": "s", + "value": 7 + }, + { + "ref": "d", + "value": 2 + } + ] + }, + { + "location": "l", + "probability": { "exp": 0.5 }, + "assignments": [ + { + "ref": "s", + "value": 7 + }, + { + "ref": "d", + "value": 3 + } + ] + } + ] + }, + { + "location": "l", + "guard": { + "exp": { + "left": "s", + "op": "=", + "right": 5 + } + }, + "destinations": [ + { + "location": "l", + "probability": { "exp": 0.5 }, + "assignments": [ + { + "ref": "s", + "value": 7 + }, + { + "ref": "d", + "value": 4 + } + ] + }, + { + "location": "l", + "probability": { "exp": 0.5 }, + "assignments": [ + { + "ref": "s", + "value": 7 + }, + { + "ref": "d", + "value": 5 + } + ] + } + ] + }, + { + "location": "l", + "guard": { + "exp": { + "left": "s", + "op": "=", + "right": 6 + } + }, + "destinations": [ + { + "location": "l", + "probability": { "exp": 0.5 }, + "assignments": [ + { + "ref": "s", + "value": 2 + } + ] + }, + { + "location": "l", + "probability": { "exp": 0.5 }, + "assignments": [ + { + "ref": "s", + "value": 7 + }, + { + "ref": "d", + "value": 6 + } + ] + } + ] + }, + { + "location": "l", + "guard": { + "exp": { + "left": "s", + "op": "=", + "right": 7 + } + }, + "destinations": [ + { + "location": "l", + "assignments": [ + { + "ref": "s", + "value": 7 + } + ] + } + ] + } + ] + + } + ], + "system": { + "elements": [ { "automaton": "die" } ] + } +} diff --git a/src/core/input.cpp b/src/core/input.cpp index 6786588..d9f2705 100644 --- a/src/core/input.cpp +++ b/src/core/input.cpp @@ -67,6 +67,7 @@ void define_input(py::module& m) { .def(py::init(), "Construct from Jani model", py::arg("jani_model")) .def_property_readonly("is_prism_program", &storm::storage::SymbolicModelDescription::isPrismProgram, "Flag if program is in Prism format") .def_property_readonly("is_jani_model", &storm::storage::SymbolicModelDescription::isJaniModel, "Flag if program is in Jani format") + .def("parse_constant_definitions", &storm::storage::SymbolicModelDescription::parseConstantDefinitions, "Parse given constant definitions", py::arg("String containing constants and their values")) .def("instantiate_constants", [](storm::storage::SymbolicModelDescription const& description, std::map const& constantDefinitions) { return description.preprocess(constantDefinitions); }, "Instantiate constants in symbolic model description", py::arg("constant_definitions")) diff --git a/src/storage/expressions.cpp b/src/storage/expressions.cpp index 2c1909c..a12cdc9 100644 --- a/src/storage/expressions.cpp +++ b/src/storage/expressions.cpp @@ -17,6 +17,17 @@ void define_expressions(py::module& m) { }, py::arg("rational"), "Create expression from rational number") ; + // Variable + py::class_>(m, "Variable", "Represents a variable") + .def_property_readonly("name", &storm::expressions::Variable::getName, "Variable name") + .def("has_boolean_type", &storm::expressions::Variable::hasBooleanType, "Check if the variable is of boolean type") + .def("has_integer_type", &storm::expressions::Variable::hasIntegerType, "Check if the variable is of integer type") + .def("has_rational_type", &storm::expressions::Variable::hasRationalType, "Check if the variable is of rational type") + .def("has_numerical_type", &storm::expressions::Variable::hasNumericalType, "Check if the variable is of numerical type") + .def("has_bitvector_type", &storm::expressions::Variable::hasBitVectorType, "Check if the variable is of bitvector type") + .def("get_expression", &storm::expressions::Variable::getExpression, "Get expression from variable") + ; + // Expression py::class_>(m, "Expression", "Holds an expression") .def("contains_variables", &storm::expressions::Expression::containsVariables, "Check if the expression contains variables.") diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index 648b4eb..bc3e707 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -6,7 +6,7 @@ import math class TestModelChecking: - def test_model_checking_dtmc(self): + def test_model_checking_prism_dtmc(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) model = stormpy.build_model(program, formulas) diff --git a/tests/core/test_parse.py b/tests/core/test_parse.py index 22d2737..569a60d 100644 --- a/tests/core/test_parse.py +++ b/tests/core/test_parse.py @@ -20,10 +20,10 @@ class TestParse: assert program.has_undefined_constants def test_parse_jani_model(self): - jani_model, properties = stormpy.parse_jani_model(get_example_path("dtmc", "brp.jani")) - assert jani_model.name == "brp" + jani_model, properties = stormpy.parse_jani_model(get_example_path("dtmc", "die.jani")) + assert jani_model.name == "die.jani" assert jani_model.model_type == stormpy.JaniModelType.DTMC - assert jani_model.has_undefined_constants + assert not jani_model.has_undefined_constants description = stormpy.SymbolicModelDescription(jani_model) assert not description.is_prism_program assert description.is_jani_model diff --git a/tests/storage/test_model.py b/tests/storage/test_model.py index a70fa37..55b70e1 100644 --- a/tests/storage/test_model.py +++ b/tests/storage/test_model.py @@ -36,6 +36,15 @@ class TestModel: assert model.has_parameters assert type(model) is stormpy.SparseParametricDtmc + def test_build_dtmc_from_jani_model(self): + jani_model, properties = stormpy.parse_jani_model(get_example_path("dtmc", "die.jani")) + model = stormpy.build_model(jani_model) + assert model.nr_states == 13 + assert model.nr_transitions == 20 + assert model.model_type == stormpy.ModelType.DTMC + assert not model.supports_parameters + assert type(model) is stormpy.SparseDtmc + def test_build_dtmc(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) formulas = stormpy.parse_properties_for_prism_program("P=? [ F \"one\" ]", program) @@ -46,6 +55,19 @@ class TestModel: assert not model.supports_parameters assert type(model) is stormpy.SparseDtmc + def test_build_instantiated_dtmc(self): + jani_model, properties = stormpy.parse_jani_model(get_example_path("dtmc", "brp.jani")) + assert jani_model.has_undefined_constants + description = stormpy.SymbolicModelDescription(jani_model) + constant_definitions = description.parse_constant_definitions("N=16, MAX=2") + instantiated_jani_model = description.instantiate_constants(constant_definitions) + model = stormpy.build_model(instantiated_jani_model) + assert model.nr_states == 677 + assert model.nr_transitions == 867 + assert model.model_type == stormpy.ModelType.DTMC + assert not model.supports_parameters + assert type(model) is stormpy.SparseDtmc + def test_build_parametric_dtmc(self): program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) formulas = stormpy.parse_properties_for_prism_program("P=? [ F s=5 ]", program)