Browse Source

whitespace / PEP8

refactoring
Tom Janson 8 years ago
parent
commit
6652e4acf1
  1. 2
      examples/01-getting-started.py
  2. 9
      lib/stormpy/__init__.py
  3. 1
      lib/stormpy/examples/files.py
  4. 3
      lib/stormpy/storage/__init__.py
  5. 1
      lib/stormpy/storage/state.py
  6. 1
      setup.py
  7. 2
      src/logic/formulae.cpp
  8. 1
      src/mod_core.cpp
  9. 16
      src/mod_expressions.cpp
  10. 10
      src/storage/model.cpp
  11. 5
      tests/core/test_bisimulation.py
  12. 1
      tests/core/test_core.py
  13. 3
      tests/core/test_modelchecking.py
  14. 1
      tests/core/test_parse.py
  15. 1
      tests/expressions/test_expressions.py
  16. 1
      tests/helpers/helper.py
  17. 1
      tests/info/test_info.py
  18. 3
      tests/logic/test_formulas.py
  19. 1
      tests/storage/test_bitvector.py
  20. 1
      tests/storage/test_matrix.py
  21. 1
      tests/storage/test_model.py
  22. 1
      tests/storage/test_model_instantiator.py
  23. 21
      tests/storage/test_model_iterators.py

2
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))
print("Labels: {}".format(model.labels))

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

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

3
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):

1
lib/stormpy/storage/state.py

@ -1,5 +1,6 @@
from . import action
class State:
""" Represents a state in the model """

1
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

2
src/logic/formulae.cpp

@ -15,7 +15,7 @@ void define_formulae(py::module& m) {
.def(vector_indexing_suite<std::vector<std::shared_ptr<storm::logic::Formula>>, true>())
;*/
py::class_<storm::logic::Formula, std::shared_ptr<storm::logic::Formula>> formula(m, "Formula", "Generic Storm Formula");
formula.def("__str__", &storm::logic::Formula::toString)
;

1
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);

16
src/mod_expressions.cpp

@ -10,17 +10,15 @@ PYBIND11_PLUGIN(expressions) {
options.disable_function_signatures();
#endif
py::class_<std::shared_ptr<storm::expressions::ExpressionManager>>(m, "ExpressionManager", "Manages variables for expressions")
;
py::class_<std::shared_ptr<storm::expressions::ExpressionManager>>(m, "ExpressionManager", "Manages variables for expressions");
py::class_<storm::expressions::Expression>(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();
}

10
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::utility::ModelInstantiator<storm::models::sparse::Dtmc<storm::RationalFunction>,storm::models::sparse::Dtmc<double>>>(m, "PdtmcInstantiator", "Instantiate PDTMCs to DTMCs")
.def(py::init<storm::models::sparse::Dtmc<storm::RationalFunction>>(), "parametric model"_a)
.def("instantiate", &storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::models::sparse::Dtmc<double>>::instantiate, "Instantiate model with given parameter values");
.def(py::init<storm::models::sparse::Dtmc<storm::RationalFunction>>(), "parametric model"_a)
.def("instantiate", &storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::models::sparse::Dtmc<double>>::instantiate, "Instantiate model with given parameter values")
;
py::class_<storm::utility::ModelInstantiator<storm::models::sparse::Mdp<storm::RationalFunction>,storm::models::sparse::Mdp<double>>>(m, "PmdpInstantiator", "Instantiate PMDPs to MDPs")
.def(py::init<storm::models::sparse::Mdp<storm::RationalFunction>>(), "parametric model"_a)
.def("instantiate", &storm::utility::ModelInstantiator<storm::models::sparse::Mdp<storm::RationalFunction>, storm::models::sparse::Mdp<double>>::instantiate, "Instantiate model with given parameter values");
.def(py::init<storm::models::sparse::Mdp<storm::RationalFunction>>(), "parametric model"_a)
.def("instantiate", &storm::utility::ModelInstantiator<storm::models::sparse::Mdp<storm::RationalFunction>, storm::models::sparse::Mdp<double>>::instantiate, "Instantiate model with given parameter values")
;
}

5
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

1
tests/core/test_core.py

@ -1,4 +1,3 @@
class TestCore:
def test_init(self):
import stormpy

3
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

1
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"))

1
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

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

1
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

3
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

1
tests/storage/test_bitvector.py

@ -1,5 +1,6 @@
import stormpy
class TestBitvector:
def test_init_default(self):
bit = stormpy.BitVector()

1
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"))

1
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"))

1
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"))

21
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):

Loading…
Cancel
Save