From e49982d7fe0affa3e83c9934417c314bc1956021 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 15 Nov 2023 17:34:22 +0100 Subject: [PATCH] Added a test for setting undefined constants in Prism program --- lib/stormpy/examples/files/dtmc/brp.pm | 136 +++++++++++++++++++++++++ src/storage/prism.cpp | 1 - tests/storage/test_model.py | 16 ++- 3 files changed, 151 insertions(+), 2 deletions(-) create mode 100644 lib/stormpy/examples/files/dtmc/brp.pm diff --git a/lib/stormpy/examples/files/dtmc/brp.pm b/lib/stormpy/examples/files/dtmc/brp.pm new file mode 100644 index 000000000..4eec09ec7 --- /dev/null +++ b/lib/stormpy/examples/files/dtmc/brp.pm @@ -0,0 +1,136 @@ +// bounded retransmission protocol [D'AJJL01] +// gxn/dxp 23/05/2001 + +dtmc + +// number of chunks +const int N; +// maximum number of retransmissions +const int MAX; + +module sender + + s : [0..6]; + // 0 idle + // 1 next_frame + // 2 wait_ack + // 3 retransmit + // 4 success + // 5 error + // 6 wait sync + srep : [0..3]; + // 0 bottom + // 1 not ok (nok) + // 2 do not know (dk) + // 3 ok (ok) + nrtr : [0..MAX]; + i : [0..N]; + bs : bool; + s_ab : bool; + fs : bool; + ls : bool; + + // idle + [NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0); + // next_frame + [aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0); + // wait_ack + [aB] (s=2) -> (s'=4) & (s_ab'=!s_ab); + [TO_Msg] (s=2) -> (s'=3); + [TO_Ack] (s=2) -> (s'=3); + // retransmit + [aF] (s=3) & (nrtr (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1); + [] (s=3) & (nrtr=MAX) & (i (s'=5) & (srep'=1); + [] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2); + // success + [] (s=4) & (i (s'=1) & (i'=i+1); + [] (s=4) & (i=N) -> (s'=0) & (srep'=3); + // error + [SyncWait] (s=5) -> (s'=6); + // wait sync + [SyncWait] (s=6) -> (s'=0) & (s_ab'=false); + +endmodule + +module receiver + + r : [0..5]; + // 0 new_file + // 1 fst_safe + // 2 frame_received + // 3 frame_reported + // 4 idle + // 5 resync + rrep : [0..4]; + // 0 bottom + // 1 fst + // 2 inc + // 3 ok + // 4 nok + fr : bool; + lr : bool; + br : bool; + r_ab : bool; + recv : bool; + + + // new_file + [SyncWait] (r=0) -> (r'=0); + [aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); + // fst_safe_frame + [] (r=1) -> (r'=2) & (r_ab'=br); + // frame_received + [] (r=2) & (r_ab=br) & (fr=true) & (lr=false) -> (r'=3) & (rrep'=1); + [] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2); + [] (r=2) & (r_ab=br) & (fr=false) & (lr=true) -> (r'=3) & (rrep'=3); + [aA] (r=2) & !(r_ab=br) -> (r'=4); + // frame_reported + [aA] (r=3) -> (r'=4) & (r_ab'=!r_ab); + // idle + [aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T); + [SyncWait] (r=4) & (ls=true) -> (r'=5); + [SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4); + // resync + [SyncWait] (r=5) -> (r'=0) & (rrep'=0); + +endmodule + +module checker // prevents more than one frame being set + + T : bool; + + [NewFile] (T=false) -> (T'=true); + +endmodule + +module channelK + + k : [0..2]; + + // idle + [aF] (k=0) -> 0.98 : (k'=1) + 0.02 : (k'=2); + // sending + [aG] (k=1) -> (k'=0); + // lost + [TO_Msg] (k=2) -> (k'=0); + +endmodule + +module channelL + + l : [0..2]; + + // idle + [aA] (l=0) -> 0.99 : (l'=1) + 0.01 : (l'=2); + // sending + [aB] (l=1) -> (l'=0); + // lost + [TO_Ack] (l=2) -> (l'=0); + +endmodule + +rewards + [aF] i=1 : 1; +endrewards + +label "target" = s=5; diff --git a/src/storage/prism.cpp b/src/storage/prism.cpp index 6362589ab..076fedaf6 100644 --- a/src/storage/prism.cpp +++ b/src/storage/prism.cpp @@ -54,7 +54,6 @@ void define_prism(py::module& m) { .def_property_readonly("reward_models", &Program::getRewardModels, "The defined reward models") .def("get_module", [](Program const& prog, std::string const& name) {return prog.getModule(name);}, py::arg("module_name")) // TODO the following is a duplicate and should be deprecated. - .def_property_readonly("hasUndefinedConstants", &Program::hasUndefinedConstants, "Does the program have undefined constants?") .def_property_readonly("is_deterministic_model", &Program::isDeterministicModel, "Does the program describe a deterministic model?") .def_property_readonly("expression_manager", &Program::getManager, "Get the expression manager for expressions in this program") .def("get_synchronizing_action_indices", &Program::getSynchronizingActionIndices, "Get the synchronizing action indices") diff --git a/tests/storage/test_model.py b/tests/storage/test_model.py index 19af95792..015b70154 100644 --- a/tests/storage/test_model.py +++ b/tests/storage/test_model.py @@ -71,7 +71,21 @@ def test_build_dtmc_with_undefined_constants(self): with pytest.raises(stormpy.StormError): model = stormpy.build_model(jani_model) - def test_build_instantiated_dtmc(self): + def test_build_instantiated_dtmc_prism(self): + program = stormpy.parse_prism_program(get_example_path("dtmc", "brp.pm")) + assert program.has_undefined_constants + assert not program.undefined_constants_are_graph_preserving + description = stormpy.SymbolicModelDescription(program) + constant_definitions = description.parse_constant_definitions("N=16, MAX=2") + instantiated_program = description.instantiate_constants(constant_definitions).as_prism_program() + model = stormpy.build_model(instantiated_program) + 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_instantiated_dtmc_jani(self): jani_model, properties = stormpy.parse_jani_model(get_example_path("dtmc", "brp.jani")) assert jani_model.has_undefined_constants assert not jani_model.undefined_constants_are_graph_preserving