sp
/
tempestpy
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Bindings for instantiating constants in SymbolicModelDescriptions

refactoring
Matthias Volk 7 years ago
parent
219b342da5
commit
29cfa574b8
6 changed files with 396 additions and 4 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 358
      lib/stormpy/examples/files/dtmc/die.jani
  2. 1
      src/core/input.cpp
  3. 11
      src/storage/expressions.cpp
  4. 2
      tests/core/test_modelchecking.py
  5. 6
      tests/core/test_parse.py
  6. 22
      tests/storage/test_model.py

358
lib/stormpy/examples/files/dtmc/die.jani
View File

@ -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" } ]
}
}

1
src/core/input.cpp
View File

@ -67,6 +67,7 @@ void define_input(py::module& m) {
.def(py::init<storm::jani::Model const&>(), "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<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) {
return description.preprocess(constantDefinitions);
}, "Instantiate constants in symbolic model description", py::arg("constant_definitions"))

11
src/storage/expressions.cpp
View File

@ -17,6 +17,17 @@ void define_expressions(py::module& m) {
}, py::arg("rational"), "Create expression from rational number")
;
// Variable
py::class_<storm::expressions::Variable, std::shared_ptr<storm::expressions::Variable>>(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_<storm::expressions::Expression, std::shared_ptr<storm::expressions::Expression>>(m, "Expression", "Holds an expression")
.def("contains_variables", &storm::expressions::Expression::containsVariables, "Check if the expression contains variables.")

2
tests/core/test_modelchecking.py
View File

@ -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)

6
tests/core/test_parse.py
View File

@ -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

22
tests/storage/test_model.py
View File

@ -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)

Write Preview
Loading…
Cancel
Save