Counter Exmaples Generation using Stormpy

[AlanLeAI]

Dear author,

I am building a stormpy model using my transition matrix. I will give a short description of the transition matrix (13 rows, each row contain a probability transition to other states). I label state 0 as "initial", other states are either "safe" or "unsafe" based on the safety values provided by an array. Here us the code to build the model using stormpy. Then, I perform a query 'P=? [F "unsafe"]', and the model return 1.0. In addition to the returned result, I want to get the counterexample that lead to the violation or results. May I ask you if you can provide me with some functions? I have tried the class SMTCounterExampleGenerator to generate counter example but get some errors, I will provide you my code below.

Thank you so much for your help.

this is my DTMC model

---

Storm model for DTMC: -------------------------------------------------------------- Model type: DTMC (sparse) States: 13 Transitions: 16 Reward Models: coin_flips State Labels: 3 labels

• unsafe -> 2 item(s)
• safe -> 10 item(s)
• init -> 1 item(s) Choice Labels: none

---

This is the code to build the model

def build_storm_model(self, safety_critic_max, threshold): rows = len(self.transitions) cols = len(self.transitions[0]) builder = stormpy.SparseMatrixBuilder(rows=0, columns=0, entries=0, force_dimensions=False, has_custom_row_grouping=False) for i in range(rows): if i == rows - 1: builder.add_next_value(row=i, column=i, value=1) for j in range(cols): builder.add_next_value(row=i, column=j, value=self.transitions[i][j])

    transition_matrix = builder.build()

    state_labeling = stormpy.storage.StateLabeling(rows)
    state_labeling.add_label("init")
    state_labeling.add_label("safe")
    state_labeling.add_label("unsafe")

    state_labeling.add_label_to_state("init", 0)
    action_reward = [0]*rows
    
    for i in range(1, rows-1):
        if safety_critic_max[i] >= threshold:
            state_labeling.add_label_to_state("unsafe", i)
            action_reward[i] = 0
        else:
            state_labeling.add_label_to_state("safe", i)
            action_reward[i] = 1
    state_labeling.add_label_to_state("safe", rows-1)

    reward_models = {}
    reward_models["coin_flips"] = stormpy.SparseRewardModel(optional_state_action_reward_vector=action_reward)

    components = stormpy.SparseModelComponents(transition_matrix=transition_matrix, state_labeling=state_labeling, reward_models=reward_models)
    dtmc = stormpy.storage.SparseDtmc(components)

    return dtmc

This is a function to query and generate counter example

def query_storm_model(self, query, dtmc): properties = stormpy.parse_properties(query) formula = properties[0]

    result = stormpy.model_checking(dtmc, formula)
    initial_state = dtmc.initial_states[0]
    probability = result.at(initial_state)

    if probability > 0:
        print("Unsafe state can be reached. Extracting most probable path...")

        # Create SMT environment
        env = stormpy.core.Environment()

        # Precompute counterexample input
        cex_input = stormpy.core.SMTCounterExampleGenerator.precompute(
            env, dtmc, dtmc, formula
        )

        # Configure counterexample options
        options = stormpy.core.SMTCounterExampleGeneratorOptions()
        options.maximum_counterexamples = 1  # Extract only the highest probability path

        # Generate counterexample
        counterexamples = stormpy.core.SMTCounterExampleGenerator.build(
            env, stormpy.core.SMTCounterExampleGeneratorStats(),
            dtmc, dtmc, cex_input, stormpy.core.FlatSet(), options
        )

        # Print extracted paths
        for i, cex in enumerate(counterexamples):
            print(f"Counterexample {i+1}: {cex}")

I have the error of

storm::storage::SymbolicModelDescription, model: storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel >, formula: storm::logic::Formula) -> storm::counterexamples::SMTMinimalLabelSetGenerator::CexInput

Invoked with: <stormpy.core.Environment object at 0x77f3ba96c6b0>, <stormpy.storage.storage.SparseDtmc object at 0x77f3bc031f70>, <stormpy.storage.storage.SparseDtmc object at 0x77f3bc031f70>, <stormpy.core.Property object at 0x77f3bb92ee30>