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>

[volkm]

The counterexample generation using SMTCounterExampleGenerator only works if the input is given as a symbolic model description, for example in the Prism language. As you build the model yourself, this approach cannot be applied.

It seems that you are interested in some of the paths reaching the target state. In this case, stormpy offers the possibility to enumerate the shortest paths leading to a desired state. The documentation provides an example how to use it and I would suggest to try it with this approach.

[AlanLeAI]

Thank you so much for your help, I have tried this method with the following DTMC model

Storm model for DTMC: --------------------------------------------------------------
Model type: DTMC (sparse)
States: 18
Transitions: 20
Reward Models: none
State Labels: 3 labels

• unsafe -> 12 item(s)
• safe -> 5 item(s)
• init -> 1 item(s)
  Choice Labels: none

---

Unsafe States: {1, 2, 3, 4, 5, 10, 11, 12, 13, 14, 15, 16}

when i run the shortest path to each unsafe state, I get the error of "Segmentation fault"

This is my code to query the model

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

    # Model checking
    result = stormpy.model_checking(dtmc, formula)
    initial_state = dtmc.initial_states[0]
    probability = result.at(initial_state)
    print(f"Unsafe state can be reached with probability {probability:.2f}. Extracting most probable paths...")

    if probability > 0:
        unsafe_states = set()
        safety_cric = []
        for state in dtmc.states:
            if "unsafe" in dtmc.labeling.get_labels_of_state(state.id):
                unsafe_states.add(state.id)
                safety_cric.append(safety_critic_max[state.id])

        print(f"Unsafe States: {unsafe_states} with corresponding max safety critic values {safety_cric}")

        for unsafe_state in unsafe_states:
            try:
                spg = ShortestPathsGenerator(dtmc, unsafe_state)
                path = spg.get_path_as_list(1)
                distance = spg.get_distance(1)
                # we refer to the most probable paths as the shortest paths.
                print(f"Shortest path to unsafe state #{unsafe_state}: {path[::-1]}, with probability {distance:.5f}")
            except:
                continue

[volkm]

To better debug the issue, can you send me the complete Python file via email to [email protected] ?