Added a test for setting undefined constants in Prism program (#139)

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<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1);
+	[] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1);
+	[] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2);
+	// success
+	[] (s=4) & (i<N) -> (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;

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

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