From 25ba6a68d7b5b9ce44b02a5236864a6df0c9b505 Mon Sep 17 00:00:00 2001
From: Erin van der Veen
Date: Fri, 6 Jul 2018 13:12:10 +0200
Subject: Allow more powerfull properties by allowing operators

---
 Assignment2/src/DTMC.icl | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

(limited to 'Assignment2/src/DTMC.icl')

diff --git a/Assignment2/src/DTMC.icl b/Assignment2/src/DTMC.icl
index 45abd4d..c89722b 100644
--- a/Assignment2/src/DTMC.icl
+++ b/Assignment2/src/DTMC.icl
@@ -259,13 +259,19 @@ where
 	| isJust state && (fromJust state).init = (fromJust state, states)
 	| otherwise = findInitial` (i - 1) states
 
+instance toString Op
+where
+	toString LT = "<"
+	toString EQ = "="
+	toString GT = ">"
+
 assertProperty :: !Property !*DTMC !Z3 !*World -> (*DTMC, *World)
-assertProperty (prob, target) dtmc z3 w
+assertProperty (op, prob, target) dtmc z3 w
 # (init, dtmc) = findInitial dtmc
 # formula = 'M'.get target init.transitions
 | isNothing formula = abort "Cannot reach property target from initial state"
 # formula = fromJust formula
-# formula = "(= (" <+ prob <+ ") (" <+ parseInfix formula <+ "))"
+# formula = "(" <+ op <+ " (" <+ prob <+ ") (" <+ parseInfix formula <+ "))"
 # w = addAssert z3 formula w
 = (dtmc, w)
 
@@ -298,4 +304,4 @@ Start w
 = w
 where
 	prop :: Property
-	prop = (0.5, 7) // Chance to reach state 7 is 0.5
+	prop = (EQ, 0.5, 7) // Chance to reach state 7 is 0.5
-- 
cgit v1.2.3