diff --git a/examples/01-getting-started.py b/examples/01-getting-started.py index fbff4b8..3a5abbc 100644 --- a/examples/01-getting-started.py +++ b/examples/01-getting-started.py @@ -10,4 +10,4 @@ prism_program = stormpy.parse_prism_program(path) model = stormpy.build_model(prism_program) print("Number of states: {}".format(model.nr_states)) print("Number of transitions: {}".format(model.nr_transitions)) -print("Labels: {}".format(model.labels)) \ No newline at end of file +print("Labels: {}".format(model.labels)) diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py index 32e577b..a3d488a 100644 --- a/lib/stormpy/__init__.py +++ b/lib/stormpy/__init__.py @@ -8,7 +8,7 @@ import stormpy.logic core._set_up("") -def build_model(program, properties = None): +def build_model(program, properties=None): """ Build a model from a symbolic description @@ -28,7 +28,8 @@ def build_model(program, properties = None): else: raise RuntimeError("Not supported non-parametric model constructed") -def build_parametric_model(program, properties = None): + +def build_parametric_model(program, properties=None): """ :param PrismProgram program: Prism program with open constants to translate into a parametric model. @@ -47,12 +48,14 @@ def build_parametric_model(program, properties = None): else: raise RuntimeError("Not supported parametric model constructed") + def perform_bisimulation(model, property, bisimulation_type): if model.supports_parameters: return core._perform_parametric_bisimulation(model, property.raw_formula, bisimulation_type) else: return core._perform_bisimulation(model, property.raw_formula, bisimulation_type) + def model_checking(model, property): if model.supports_parameters: return core._parametric_model_checking(model, property.raw_formula) @@ -76,6 +79,7 @@ def compute_prob01_states(model, phi_states, psi_states): else: return core._compute_prob01states_double(model, phi_states, psi_states) + def compute_prob01min_states(model, phi_states, psi_states): if model.model_type == ModelType.DTMC: return compute_prob01_states(model, phi_states, psi_states) @@ -84,6 +88,7 @@ def compute_prob01min_states(model, phi_states, psi_states): else: return core._compute_prob01states_min_double(model, phi_states, psi_states) + def compute_prob01max_states(model, phi_states, psi_states): if model.model_type == ModelType.DTMC: return compute_prob01_states(model, phi_states, psi_states) diff --git a/lib/stormpy/examples/files.py b/lib/stormpy/examples/files.py index d13ca7d..f825f91 100644 --- a/lib/stormpy/examples/files.py +++ b/lib/stormpy/examples/files.py @@ -2,6 +2,7 @@ import os testfile_dir = os.path.join(os.path.dirname(os.path.abspath(__file__)), "files") + def _path(folder, file): """Internal method for simpler listing of examples""" return os.path.join(testfile_dir, folder, file) diff --git a/lib/stormpy/storage/__init__.py b/lib/stormpy/storage/__init__.py index 2eda405..550dbc5 100644 --- a/lib/stormpy/storage/__init__.py +++ b/lib/stormpy/storage/__init__.py @@ -1,6 +1,7 @@ from . import storage from .storage import * -from . import state,action +from . import state, action + class ModelInstantiator: def __init__(self, model): diff --git a/lib/stormpy/storage/state.py b/lib/stormpy/storage/state.py index 6a315e7..40b2806 100644 --- a/lib/stormpy/storage/state.py +++ b/lib/stormpy/storage/state.py @@ -1,5 +1,6 @@ from . import action + class State: """ Represents a state in the model """ diff --git a/setup.py b/setup.py index 5ab038a..6165230 100755 --- a/setup.py +++ b/setup.py @@ -64,6 +64,7 @@ class CMakeBuild(build_ext): subprocess.check_call(['cmake', ext.sourcedir] + cmake_args, cwd=self.build_temp, env=env) subprocess.check_call(['cmake', '--build', '.', '--target', ext.name] + build_args, cwd=self.build_temp) + class PyTest(test): def run_tests(self): #import here, cause outside the eggs aren't loaded diff --git a/src/logic/formulae.cpp b/src/logic/formulae.cpp index 1257126..29c3f1a 100644 --- a/src/logic/formulae.cpp +++ b/src/logic/formulae.cpp @@ -15,7 +15,7 @@ void define_formulae(py::module& m) { .def(vector_indexing_suite>, true>()) ;*/ - + py::class_> formula(m, "Formula", "Generic Storm Formula"); formula.def("__str__", &storm::logic::Formula::toString) ; diff --git a/src/mod_core.cpp b/src/mod_core.cpp index a3c0ae0..f394ab1 100644 --- a/src/mod_core.cpp +++ b/src/mod_core.cpp @@ -14,7 +14,6 @@ PYBIND11_PLUGIN(core) { // options.disable_function_signatures(); #endif - define_core(m); define_property(m); define_parse(m); diff --git a/src/mod_expressions.cpp b/src/mod_expressions.cpp index b876034..87a1d5a 100644 --- a/src/mod_expressions.cpp +++ b/src/mod_expressions.cpp @@ -10,17 +10,15 @@ PYBIND11_PLUGIN(expressions) { options.disable_function_signatures(); #endif - py::class_>(m, "ExpressionManager", "Manages variables for expressions") - ; + py::class_>(m, "ExpressionManager", "Manages variables for expressions"); py::class_(m, "Expression", "Holds an expression") - .def("__str__", &storm::expressions::Expression::toString) - .def_property_readonly("contains_variables", &storm::expressions::Expression::containsVariables) - .def_property_readonly("has_boolean_type", &storm::expressions::Expression::hasBooleanType) - .def_property_readonly("has_integer_type", &storm::expressions::Expression::hasIntegerType) - .def_property_readonly("has_rational_type", &storm::expressions::Expression::hasRationalType) - - ; + .def("__str__", &storm::expressions::Expression::toString) + .def_property_readonly("contains_variables", &storm::expressions::Expression::containsVariables) + .def_property_readonly("has_boolean_type", &storm::expressions::Expression::hasBooleanType) + .def_property_readonly("has_integer_type", &storm::expressions::Expression::hasIntegerType) + .def_property_readonly("has_rational_type", &storm::expressions::Expression::hasRationalType) + ; return m.ptr(); } diff --git a/src/storage/model.cpp b/src/storage/model.cpp index 0f79fe0..8b11429 100644 --- a/src/storage/model.cpp +++ b/src/storage/model.cpp @@ -91,10 +91,12 @@ void define_model(py::module& m) { // Model instantiator void define_model_instantiator(py::module& m) { py::class_,storm::models::sparse::Dtmc>>(m, "PdtmcInstantiator", "Instantiate PDTMCs to DTMCs") - .def(py::init>(), "parametric model"_a) - .def("instantiate", &storm::utility::ModelInstantiator, storm::models::sparse::Dtmc>::instantiate, "Instantiate model with given parameter values"); + .def(py::init>(), "parametric model"_a) + .def("instantiate", &storm::utility::ModelInstantiator, storm::models::sparse::Dtmc>::instantiate, "Instantiate model with given parameter values") + ; py::class_,storm::models::sparse::Mdp>>(m, "PmdpInstantiator", "Instantiate PMDPs to MDPs") - .def(py::init>(), "parametric model"_a) - .def("instantiate", &storm::utility::ModelInstantiator, storm::models::sparse::Mdp>::instantiate, "Instantiate model with given parameter values"); + .def(py::init>(), "parametric model"_a) + .def("instantiate", &storm::utility::ModelInstantiator, storm::models::sparse::Mdp>::instantiate, "Instantiate model with given parameter values") + ; } diff --git a/tests/core/test_bisimulation.py b/tests/core/test_bisimulation.py index ae69462..a30b123 100644 --- a/tests/core/test_bisimulation.py +++ b/tests/core/test_bisimulation.py @@ -2,11 +2,13 @@ import stormpy import stormpy.logic from helpers.helper import get_example_path + class TestBisimulation: def test_bisimulation(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "crowds5_5.pm")) assert program.nr_modules == 1 assert program.model_type == stormpy.PrismModelType.DTMC + prop = "P=? [F \"observe0Greater1\"]" properties = stormpy.parse_properties_for_prism_program(prop, program) model = stormpy.build_model(program, properties) @@ -14,6 +16,7 @@ class TestBisimulation: assert model.nr_transitions == 13041 assert model.model_type == stormpy.ModelType.DTMC assert not model.supports_parameters + model_bisim = stormpy.perform_bisimulation(model, properties[0], stormpy.BisimulationType.STRONG) assert model_bisim.nr_states == 64 assert model_bisim.nr_transitions == 104 @@ -25,6 +28,7 @@ class TestBisimulation: assert program.nr_modules == 1 assert program.model_type == stormpy.PrismModelType.DTMC assert program.has_undefined_constants + prop = "P=? [F \"observe0Greater1\"]" properties = stormpy.parse_properties_for_prism_program(prop, program) model = stormpy.build_parametric_model(program, properties) @@ -32,6 +36,7 @@ class TestBisimulation: assert model.nr_transitions == 2027 assert model.model_type == stormpy.ModelType.DTMC assert model.has_parameters + model_bisim = stormpy.perform_bisimulation(model, properties[0], stormpy.BisimulationType.STRONG) assert model_bisim.nr_states == 80 assert model_bisim.nr_transitions == 120 diff --git a/tests/core/test_core.py b/tests/core/test_core.py index cedd750..84234d0 100644 --- a/tests/core/test_core.py +++ b/tests/core/test_core.py @@ -1,4 +1,3 @@ - class TestCore: def test_init(self): import stormpy diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py index 017b156..60766b6 100644 --- a/tests/core/test_modelchecking.py +++ b/tests/core/test_modelchecking.py @@ -4,6 +4,7 @@ from helpers.helper import get_example_path import math + class TestModelChecking: def test_model_checking_dtmc(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) @@ -71,5 +72,5 @@ class TestModelChecking: assert prob0.number_of_set_bits() == 9 assert prob1.number_of_set_bits() == 1 labelprop = stormpy.core.Property("cora", formulaPsi.raw_formula) - result = stormpy.model_checking(model, labelprop) + result = stormpy.model_checking(model, labelprop) assert result.get_truth_values().number_of_set_bits() == 1 diff --git a/tests/core/test_parse.py b/tests/core/test_parse.py index 56e6bc6..8646beb 100644 --- a/tests/core/test_parse.py +++ b/tests/core/test_parse.py @@ -2,6 +2,7 @@ import stormpy import stormpy.logic from helpers.helper import get_example_path + class TestParse: def test_parse_prism_program(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) diff --git a/tests/expressions/test_expressions.py b/tests/expressions/test_expressions.py index 823186d..e25c90f 100644 --- a/tests/expressions/test_expressions.py +++ b/tests/expressions/test_expressions.py @@ -1,6 +1,7 @@ import stormpy from stormpy.expressions import expressions + class TestExpressions: def test_expression_manager(self): manager = expressions.ExpressionManager diff --git a/tests/helpers/helper.py b/tests/helpers/helper.py index 787a227..37a49f5 100644 --- a/tests/helpers/helper.py +++ b/tests/helpers/helper.py @@ -4,5 +4,6 @@ import stormpy.examples import stormpy.examples.files example_dir = stormpy.examples.files.testfile_dir + def get_example_path(*paths): return os.path.join(example_dir, *paths) diff --git a/tests/info/test_info.py b/tests/info/test_info.py index fd91d68..176e4fd 100644 --- a/tests/info/test_info.py +++ b/tests/info/test_info.py @@ -1,6 +1,7 @@ import stormpy from stormpy.info import info + class TestInfo: def test_version(self): s = info.Version.short diff --git a/tests/logic/test_formulas.py b/tests/logic/test_formulas.py index 453d3f5..f6b38d0 100644 --- a/tests/logic/test_formulas.py +++ b/tests/logic/test_formulas.py @@ -2,8 +2,8 @@ import pycarl import stormpy import stormpy.logic -class TestFormulas: +class TestFormulas: def test_probability_formula(self): formula_str = "P=? [F \"one\"]" properties = stormpy.parse_properties(formula_str) @@ -60,4 +60,3 @@ class TestFormulas: assert type(labelform) == stormpy.logic.AtomicLabelFormula prop = stormpy.core.Property("label-formula", labelform) assert prop.raw_formula == labelform - diff --git a/tests/storage/test_bitvector.py b/tests/storage/test_bitvector.py index ea58fad..e21bc8c 100644 --- a/tests/storage/test_bitvector.py +++ b/tests/storage/test_bitvector.py @@ -1,5 +1,6 @@ import stormpy + class TestBitvector: def test_init_default(self): bit = stormpy.BitVector() diff --git a/tests/storage/test_matrix.py b/tests/storage/test_matrix.py index 4ca2faf..b2c084c 100644 --- a/tests/storage/test_matrix.py +++ b/tests/storage/test_matrix.py @@ -3,6 +3,7 @@ from helpers.helper import get_example_path import math + class TestMatrix: def test_sparse_matrix(self): model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) diff --git a/tests/storage/test_model.py b/tests/storage/test_model.py index 8ca25f4..2b68655 100644 --- a/tests/storage/test_model.py +++ b/tests/storage/test_model.py @@ -2,6 +2,7 @@ import stormpy import stormpy.logic from helpers.helper import get_example_path + class TestModel: def test_build_dtmc_from_prism_program(self): program = stormpy.parse_prism_program(get_example_path("dtmc", "die.pm")) diff --git a/tests/storage/test_model_instantiator.py b/tests/storage/test_model_instantiator.py index fd2c4fc..de6aae9 100644 --- a/tests/storage/test_model_instantiator.py +++ b/tests/storage/test_model_instantiator.py @@ -3,6 +3,7 @@ import stormpy import stormpy.logic from helpers.helper import get_example_path + class TestModel: def test_instantiate_dtmc(self): program = stormpy.parse_prism_program(get_example_path("pdtmc", "brp16_2.pm")) diff --git a/tests/storage/test_model_iterators.py b/tests/storage/test_model_iterators.py index 8023b86..2a97d50 100644 --- a/tests/storage/test_model_iterators.py +++ b/tests/storage/test_model_iterators.py @@ -1,6 +1,7 @@ import stormpy from helpers.helper import get_example_path + class TestModelIterators: def test_states_dtmc(self): model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) @@ -36,11 +37,11 @@ class TestModelIterators: def test_transitions_dtmc(self): transitions_orig = [(0, 0, 0), (0, 1, 0.5), (0, 2, 0.5), (1, 1, 0), (1, 3, 0.5), (1, 4, 0.5), - (2, 2, 0), (2, 5, 0.5), (2, 6, 0.5), (3, 1, 0.5), (3, 3, 0), (3, 7, 0.5), - (4, 4, 0), (4, 8, 0.5), (4, 9, 0.5), (5, 5, 0), (5, 10, 0.5), (5, 11, 0.5), - (6, 2, 0.5), (6, 6, 0), (6, 12, 0.5), (7, 7, 1), (8, 8, 1), - (9, 9, 1), (10, 10, 1), (11, 11, 1), (12, 12, 1) - ] + (2, 2, 0), (2, 5, 0.5), (2, 6, 0.5), (3, 1, 0.5), (3, 3, 0), (3, 7, 0.5), + (4, 4, 0), (4, 8, 0.5), (4, 9, 0.5), (5, 5, 0), (5, 10, 0.5), (5, 11, 0.5), + (6, 2, 0.5), (6, 6, 0), (6, 12, 0.5), (7, 7, 1), (8, 8, 1), + (9, 9, 1), (10, 10, 1), (11, 11, 1), (12, 12, 1) + ] model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) s = stormpy.state.State(0, model) i = 0 @@ -66,11 +67,11 @@ class TestModelIterators: def test_row_iterator(self): transitions_orig = [(0, 0, 0), (0, 1, 0.5), (0, 2, 0.5), (1, 1, 0), (1, 3, 0.5), (1, 4, 0.5), - (2, 2, 0), (2, 5, 0.5), (2, 6, 0.5), (3, 1, 0.5), (3, 3, 0), (3, 7, 0.5), - (4, 4, 0), (4, 8, 0.5), (4, 9, 0.5), (5, 5, 0), (5, 10, 0.5), (5, 11, 0.5), - (6, 2, 0.5), (6, 6, 0), (6, 12, 0.5), (7, 7, 1), (8, 8, 1), - (9, 9, 1), (10, 10, 1), (11, 11, 1), (12, 12, 1) - ] + (2, 2, 0), (2, 5, 0.5), (2, 6, 0.5), (3, 1, 0.5), (3, 3, 0), (3, 7, 0.5), + (4, 4, 0), (4, 8, 0.5), (4, 9, 0.5), (5, 5, 0), (5, 10, 0.5), (5, 11, 0.5), + (6, 2, 0.5), (6, 6, 0), (6, 12, 0.5), (7, 7, 1), (8, 8, 1), + (9, 9, 1), (10, 10, 1), (11, 11, 1), (12, 12, 1) + ] model = stormpy.parse_explicit_model(get_example_path("dtmc", "die.tra"), get_example_path("dtmc", "die.lab")) i = 0 for state in stormpy.state.State(0, model):