From 886718bdb26da397e93f1b2990f6b89fbd269696 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 26 May 2020 16:19:50 -0700 Subject: [PATCH] state generation via stormpy is broken. to avoid compilation problems, this is disabled for now --- src/storage/prism.cpp | 112 ++++++++++++------------- tests/storage/test_state_generation.py | 2 + 2 files changed, 58 insertions(+), 56 deletions(-) diff --git a/src/storage/prism.cpp b/src/storage/prism.cpp index 47b4bc1..6365911 100644 --- a/src/storage/prism.cpp +++ b/src/storage/prism.cpp @@ -122,7 +122,7 @@ void define_prism(py::module& m) { py::class_> boolean_variable(m, "PrismBooleanVariable", variable, "A program boolean variable in a Prism program"); boolean_variable.def("__str__", &streamToString); - define_stateGeneration(m); + //define_stateGeneration(m); } class ValuationMapping { @@ -364,59 +364,59 @@ std::map> simu template void define_stateGeneration(py::module& m) { - py::class_> valuation_mapping(m, "ValuationMapping", "A valuation mapping for a state consists of a mapping from variable to value for each of the three types."); - valuation_mapping - .def_readonly("boolean_values", &ValuationMapping::booleanValues) - .def_readonly("integer_values", &ValuationMapping::integerValues) - .def_readonly("rational_values", &ValuationMapping::rationalValues) - .def("__str__", &ValuationMapping::toString); - - py::class_, - std::shared_ptr>> - generator_choice(m, "GeneratorChoice", R"doc( - Representation of a choice taken by the generator. - - :ivar origins: A list of command ids that generated this choice. - :vartype origins: List[int] - :ivar distribution: The probability distribution of this choice. - :vartype distribution: List[Pair[StateId, Probability]] - )doc"); - generator_choice - .def_readonly("origins", &GeneratorChoice::origins) - .def_readonly("distribution", &GeneratorChoice::distribution); - - py::class_, std::shared_ptr>> state_generator(m, "StateGenerator", R"doc( - Interactively explore states using Storm's PrismNextStateGenerator. - - :ivar program: A PRISM program. - )doc"); - state_generator - .def(py::init()) - .def("load_initial_state", &StateGenerator::loadInitialState, R"doc( - Loads the (unique) initial state. - Multiple initial states are not supported. - - :rtype: the ID of the initial state. - )doc") - .def("load", &StateGenerator::load, R"doc( - :param state_id: The ID of the state to load. - )doc") - .def("current_state_to_valuation", &StateGenerator::currentStateToValuation, R"doc( - Return a valuation for the currently loaded state. - - :rtype: stormpy.ValuationMapping - )doc") - .def("current_state_satisfies", &StateGenerator::satisfies, R"doc( - Check if the currently loaded state satisfies the given expression. - - :param stormpy.Expression expression: The expression to check against. - :rtype: bool - )doc") - .def("expand", &StateGenerator::expand, R"doc( - Expand the currently loaded state and return its successors. - - :rtype: [GeneratorChoice] - )doc"); - - m.def("simulate", &simulate); +// py::class_> valuation_mapping(m, "ValuationMapping", "A valuation mapping for a state consists of a mapping from variable to value for each of the three types."); +// valuation_mapping +// .def_readonly("boolean_values", &ValuationMapping::booleanValues) +// .def_readonly("integer_values", &ValuationMapping::integerValues) +// .def_readonly("rational_values", &ValuationMapping::rationalValues) +// .def("__str__", &ValuationMapping::toString); +// +// py::class_, +// std::shared_ptr>> +// generator_choice(m, "GeneratorChoice", R"doc( +// Representation of a choice taken by the generator. +// +// :ivar origins: A list of command ids that generated this choice. +// :vartype origins: List[int] +// :ivar distribution: The probability distribution of this choice. +// :vartype distribution: List[Pair[StateId, Probability]] +// )doc"); +// generator_choice +// .def_readonly("origins", &GeneratorChoice::origins) +// .def_readonly("distribution", &GeneratorChoice::distribution); +// +// py::class_, std::shared_ptr>> state_generator(m, "StateGenerator", R"doc( +// Interactively explore states using Storm's PrismNextStateGenerator. +// +// :ivar program: A PRISM program. +// )doc"); +// state_generator +// .def(py::init()) +// .def("load_initial_state", &StateGenerator::loadInitialState, R"doc( +// Loads the (unique) initial state. +// Multiple initial states are not supported. +// +// :rtype: the ID of the initial state. +// )doc") +// .def("load", &StateGenerator::load, R"doc( +// :param state_id: The ID of the state to load. +// )doc") +// .def("current_state_to_valuation", &StateGenerator::currentStateToValuation, R"doc( +// Return a valuation for the currently loaded state. +// +// :rtype: stormpy.ValuationMapping +// )doc") +// .def("current_state_satisfies", &StateGenerator::satisfies, R"doc( +// Check if the currently loaded state satisfies the given expression. +// +// :param stormpy.Expression expression: The expression to check against. +// :rtype: bool +// )doc") +// .def("expand", &StateGenerator::expand, R"doc( +// Expand the currently loaded state and return its successors. +// +// :rtype: [GeneratorChoice] +// )doc"); +// +// m.def("simulate", &simulate); } diff --git a/tests/storage/test_state_generation.py b/tests/storage/test_state_generation.py index 4c909de..d139b97 100644 --- a/tests/storage/test_state_generation.py +++ b/tests/storage/test_state_generation.py @@ -1,5 +1,6 @@ import stormpy from stormpy.examples.files import prism_dtmc_die +import pytest class _DfsQueue: def __init__(self): @@ -55,6 +56,7 @@ def _find_variable(program, name): return var return None +@pytest.mark.skipif(True, reason="State generation is broken") def test_knuth_yao_die(): program, expression_parser = _load_program(prism_dtmc_die) s_variable = _find_variable(program, "s")