From befecb4761971ae789ead76ada74c8e1f41d9dbe Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Thu, 30 Nov 2017 17:42:39 +0100
Subject: [PATCH] convenience functions for prob01 states

---
 examples/analysis/01-analysis.py | 20 ++++++++++++++++++++
 lib/stormpy/__init__.py          | 20 +++++++++++++++++++-
 2 files changed, 39 insertions(+), 1 deletion(-)
 create mode 100644 examples/analysis/01-analysis.py

diff --git a/examples/analysis/01-analysis.py b/examples/analysis/01-analysis.py
new file mode 100644
index 0000000..ec32723
--- /dev/null
+++ b/examples/analysis/01-analysis.py
@@ -0,0 +1,20 @@
+import stormpy
+import stormpy.core
+
+import stormpy.examples
+import stormpy.examples.files
+
+
+def example_analysis_01():
+    path = stormpy.examples.files.prism_dtmc_die
+    prism_program = stormpy.parse_prism_program(path)
+
+    formula_str = "P=? [F s=7 & d=2]"
+    properties = stormpy.parse_properties_for_prism_program(formula_str, prism_program)
+    model = stormpy.build_model(prism_program, properties)
+    prob0E, prob1A = stormpy.prob01min_states(model, properties[0].raw_formula.subformula)
+    print(prob0E)
+    print(prob1A)
+
+if __name__ == '__main__':
+    example_analysis_01()
\ No newline at end of file
diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py
index 630001c..8d08d5e 100644
--- a/lib/stormpy/__init__.py
+++ b/lib/stormpy/__init__.py
@@ -150,13 +150,31 @@ def model_checking(model, property):
         return core._model_checking_sparse_engine(model, task)
 
 
+def prob01min_states(model, eventually_formula):
+    assert type(eventually_formula) == logic.EventuallyFormula
+    labelform = eventually_formula.subformula
+    labelprop = core.Property("label-prop", labelform)
+    phiStates = BitVector(model.nr_states, True)
+    psiStates = model_checking(model, labelprop).get_truth_values()
+    return compute_prob01min_states(model, phiStates, psiStates)
+
+
+def prob01max_states(model, eventually_formula):
+    assert type(eventually_formula) == logic.EventuallyFormula
+    labelform = eventually_formula.subformula
+    labelprop = core.Property("label-prop", labelform)
+    phiStates = BitVector(model.nr_states, True)
+    psiStates = model_checking(model, labelprop).get_truth_values()
+    return compute_prob01min_states(model, phiStates, psiStates)
+
+
 def compute_prob01_states(model, phi_states, psi_states):
     """
     Compute prob01 states for properties of the form phi_states until psi_states
 
     :param SparseDTMC model:
     :param BitVector phi_states:
-    :param BitVector psi_states:
+    :param BitVector psi_states: Target states
     """
     if model.model_type != ModelType.DTMC:
         raise StormError("Prob 01 is only defined for DTMCs -- model must be a DTMC")