add example

Author: reb-ddm

examples/incremental_analysis/example_conflict.ka

@@ -0,0 +1,27 @@
+
+
+%agent: A(x,y,z)
+%agent: E(t)
+// global boolean parameter
+%guard_param: P [false]
+// P = x and y are in conflict
+
+// Initial conditions
+%init: 100 A(),E()
+
+// if there is a conflict
+#[[not] P] A(x[.]), E(t[.]) -> A(x[1]), E(t[1]) @ 1
+
+%working_set:[
+
+#[[not] P] A(y[.]), E(t[.]) -> A(y[1]), E(t[1]) @ 1
+
+#[P] A(x[.],y[.]), E(t[.]) -> A(x[1],y[.]), E(t[1]) @ 1
+#[P] A(y[.],x[.]), E(t[.]) -> A(y[1],x[.]), E(t[1]) @ 1
+
+A(x[_], y[_], z[.]), E(t[.]) -> A(x[_], y[_], z[1]), E(t[1]) @ 1
+]
+// Measure amount of A-z-E
+%obs: 'Trimer' |A(z[1]),E(t[1])|
+
+// Static analysis must show that P => z is free