From 445168077d96e937f98c116ae6d2ab0993785731 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Tue, 30 Apr 2019 19:59:08 +0100
Subject: [PATCH] Bug fix in symbolic model checking of filters.

The statesOfInterest variables was wrongly not reset to 'reach'.
Not usually caught because the statesOfInterest optimisation is
currently used in very few places. The attached bugfix test shows
an example of where it does go wrong.
---
 .../bugfixes/filters+statesOfInterest.prism   | 23 +++++++++++++++++++
 .../filters+statesOfInterest.prism.args       |  4 ++++
 .../filters+statesOfInterest.prism.props      |  5 ++++
 .../filters+statesOfInterest.prism.props.args |  1 +
 .../filters+statesOfInterest.prism.props.txt  | 13 +++++++++++
 prism/src/prism/StateModelChecker.java        |  2 +-
 6 files changed, 47 insertions(+), 1 deletion(-)
 create mode 100644 prism-tests/bugfixes/filters+statesOfInterest.prism
 create mode 100644 prism-tests/bugfixes/filters+statesOfInterest.prism.args
 create mode 100644 prism-tests/bugfixes/filters+statesOfInterest.prism.props
 create mode 100644 prism-tests/bugfixes/filters+statesOfInterest.prism.props.args
 create mode 100644 prism-tests/bugfixes/filters+statesOfInterest.prism.props.txt

diff --git a/prism-tests/bugfixes/filters+statesOfInterest.prism b/prism-tests/bugfixes/filters+statesOfInterest.prism
new file mode 100644
index 00000000..c0d80eae
--- /dev/null
+++ b/prism-tests/bugfixes/filters+statesOfInterest.prism
@@ -0,0 +1,23 @@
+dtmc
+
+module die
+
+	// local state
+	s : [0..7] init 0;
+	// value of the die
+	d : [0..6] init 0;
+	
+	[] s=0 -> 0.5 : (s'=1) + 0.5 : (s'=2);
+	[] s=1 -> 0.5 : (s'=3) + 0.5 : (s'=4);
+	[] s=2 -> 0.5 : (s'=5) + 0.5 : (s'=6);
+	[] s=3 -> 0.5 : (s'=1) + 0.5 : (s'=7) & (d'=1);
+	[] s=4 -> 0.5 : (s'=7) & (d'=2) + 0.5 : (s'=7) & (d'=3);
+	[] s=5 -> 0.5 : (s'=7) & (d'=4) + 0.5 : (s'=7) & (d'=5);
+	[] s=6 -> 0.5 : (s'=2) + 0.5 : (s'=7) & (d'=6);
+	[] s=7 -> (s'=7);
+	
+endmodule
+
+rewards "coin_flips"
+	[] s<7 : 1;
+endrewards
diff --git a/prism-tests/bugfixes/filters+statesOfInterest.prism.args b/prism-tests/bugfixes/filters+statesOfInterest.prism.args
new file mode 100644
index 00000000..031d5fa5
--- /dev/null
+++ b/prism-tests/bugfixes/filters+statesOfInterest.prism.args
@@ -0,0 +1,4 @@
+-ex
+-m
+-s
+-h
diff --git a/prism-tests/bugfixes/filters+statesOfInterest.prism.props b/prism-tests/bugfixes/filters+statesOfInterest.prism.props
new file mode 100644
index 00000000..0ebdee0c
--- /dev/null
+++ b/prism-tests/bugfixes/filters+statesOfInterest.prism.props
@@ -0,0 +1,5 @@
+// Bug fix test case for filters; see commit for details
+// The "0.0+" is needed because of missing integer-valued vector export
+
+// RESULT: 13
+0.0 + filter(sum, filter(count, true, P>0[ X F s=7]), s=2);
diff --git a/prism-tests/bugfixes/filters+statesOfInterest.prism.props.args b/prism-tests/bugfixes/filters+statesOfInterest.prism.props.args
new file mode 100644
index 00000000..23ce11d9
--- /dev/null
+++ b/prism-tests/bugfixes/filters+statesOfInterest.prism.props.args
@@ -0,0 +1 @@
+-exportvector filters+statesOfInterest.prism.props.txt
diff --git a/prism-tests/bugfixes/filters+statesOfInterest.prism.props.txt b/prism-tests/bugfixes/filters+statesOfInterest.prism.props.txt
new file mode 100644
index 00000000..7a2a6932
--- /dev/null
+++ b/prism-tests/bugfixes/filters+statesOfInterest.prism.props.txt
@@ -0,0 +1,13 @@
+13.0
+13.0
+13.0
+13.0
+13.0
+13.0
+13.0
+13.0
+13.0
+13.0
+13.0
+13.0
+13.0
diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java
index b19bee4f..aa3b4de8 100644
--- a/prism/src/prism/StateModelChecker.java
+++ b/prism/src/prism/StateModelChecker.java
@@ -1140,7 +1140,7 @@ public class StateModelChecker extends PrismComponent implements ModelChecker
 		boolean filterTrue = Expression.isTrue(filter);
 		// Store some more info
 		String filterStatesString = filterTrue ? "all states" : "states satisfying filter";
-		JDDNode ddFilter = checkExpressionDD(filter, statesOfInterest.copy());
+		JDDNode ddFilter = checkExpressionDD(filter,  model.getReach().copy());
 		StateListMTBDD statesFilter = new StateListMTBDD(ddFilter, model);
 		// Check if filter state set is empty; we treat this as an error
 		if (ddFilter.equals(JDD.ZERO)) {