import stormpy
import stormpy.core
import stormpy.info

import pycarl
import pycarl.core

import stormpy.examples
import stormpy.examples.files

import stormpy.pomdp

import stormpy._config as config


def example_parametric_models_01():
    # Check support for parameters
    if not config.storm_with_pars:
        print("Support parameters is missing. Try building storm-pars.")
        return

    import stormpy.pars
    from pycarl.formula import FormulaType, Relation
    if stormpy.info.storm_ratfunc_use_cln():
        import pycarl.cln.formula
    else:
        import pycarl.gmp.formula

    # Prevent curious side effects from earlier runs (for tests only)
    pycarl.clear_pools()
    ###
    # How to apply an unknown FSC to obtain a pMC from a POMDP
    path = stormpy.examples.files.prism_pomdp_maze
    prism_program = stormpy.parse_prism_program(path)

    formula_str = "P=? [\"goal\"]"
    properties = stormpy.parse_properties_for_prism_program(formula_str, prism_program)
    # construct the POMDP
    pomdp = stormpy.build_model(prism_program, properties)
    # make its representation canonic.
    pomdp = stormpy.pomdp.make_canonic(pomdp)
    # make the POMDP simple. This step is optional but often beneficial
    pomdp = stormpy.pomdp.make_simple(pomdp)
    # construct the memory for the FSC
    # in this case, a selective counter with two states
    memory_builder = stormpy.pomdp.PomdpMemoryBuilder()
    memory = memory_builder.build(stormpy.pomdp.PomdpMemoryPattern.selective_counter, 2)
    # apply the memory onto the POMDP to get the cartesian product
    pomdp = stormpy.pomdp.unfold_memory(pomdp, memory)
    # apply the memory onto the POMDP to get the cartesian product
    pmc = stormpy.pomdp.apply_unknown_fsc(pomdp, stormpy.pomdp.PomdpFscApplicationMode.simple_linear)

    ####
    # How to apply an unknown FSC to obtain a pMC from a pPOMDP
    path = stormpy.examples.files.prism_par_pomdp_maze
    prism_program = stormpy.parse_prism_program(path)

    formula_str = "P=? [\"goal\"]"
    properties = stormpy.parse_properties_for_prism_program(formula_str, prism_program)
    # construct the pPOMDP
    pomdp = stormpy.build_parametric_model(prism_program, properties)
    # make its representation canonic.
    pomdp = stormpy.pomdp.make_canonic(pomdp)
    # make the POMDP simple. This step is optional but often beneficial
    pomdp = stormpy.pomdp.make_simple(pomdp)
    # construct the memory for the FSC
    # in this case, a selective counter with two states
    memory_builder = stormpy.pomdp.PomdpMemoryBuilder()
    memory = memory_builder.build(stormpy.pomdp.PomdpMemoryPattern.selective_counter, 2)
    # apply the memory onto the POMDP to get the cartesian product
    pomdp = stormpy.pomdp.unfold_memory(pomdp, memory)
    # apply the unknown FSC to obtain a pmc from the POMDP
    pmc = stormpy.pomdp.apply_unknown_fsc(pomdp, stormpy.pomdp.PomdpFscApplicationMode.simple_linear)

    export_pmc = False # Set to True to export the pMC as drn.
    if export_pmc:
        export_options = stormpy.core.DirectEncodingOptions()
        export_options.allow_placeholders = False
        stormpy.export_parametric_to_drn(pmc, "test.out", export_options)

if __name__ == '__main__':
    example_parametric_models_01()