build sub-POMDP from custom belief

paynt/parser/sketch.py

@@ -60,6 +60,8 @@ def load_sketch(cls, sketch_path, properties_path,
         export=None, relative_error=0, discount_factor=1, precision=1e-4, constraint_bound=None):
 
         assert discount_factor>0 and discount_factor<=1, "discount factor must be in the interval (0,1]"
+        if discount_factor < 1:
+            logger.warning("ignoring non-trivial discount factor")
 
         prism = None
         explicit_quotient = None
@@ -118,25 +120,6 @@ def load_sketch(cls, sketch_path, properties_path,
 
         assert filetype is not None, "unknow format of input file"
         logger.info("sketch parsing OK")
-
-        if filetype=="prism" or filetype =="drn":
-            assert specification is not None
-            if discount_factor < 1:
-                logger.info("applying discount factor transformation")
-                assert specification.is_single_property and specification.all_properties()[0].reward, \
-                    "non-trivial discount factor can only be used in combination with a single reward property"
-                assert explicit_quotient.is_partially_observable, \
-                    "non-trivial discount factor can only be used for POMDPs (for now...)"
-                prop = specification.all_properties()[0]
-                reward_name = prop.formula.reward_name
-                target_label = str(prop.formula.subformula.subformula)
-                subpomdp_builder = payntbind.synthesis.SubPomdpBuilder(explicit_quotient, reward_name, target_label)
-                subpomdp_builder.set_discount_factor(discount_factor)
-                initial_distribution = {explicit_quotient.initial_states[0] : 1}
-                relevant_observations = stormpy.storage.BitVector(explicit_quotient.nr_observations,True)
-                subpomdp_builder.set_relevant_observations(relevant_observations, initial_distribution)
-                explicit_quotient = subpomdp_builder.restrict_pomdp(initial_distribution)
-                logger.debug('WARNING: discount factor transformation has not been properly tested')
 
         paynt.quotient.models.MarkovChain.initialize(specification)
         paynt.verification.property.Property.initialize()

paynt/simulation/pomcp.py

@@ -1,3 +1,5 @@
+# WARNING: this module is currently not maintained
+
 import stormpy
 import payntbind
 

paynt/simulation/simulation.py

@@ -1,3 +1,5 @@
+# WARNING: this module is currently not maintained
+
 import random
 import numpy
 import json