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.dcl |  9 +++++++--
 Assignment2/src/DTMC.icl | 12 +++++++++---
 2 files changed, 16 insertions(+), 5 deletions(-)

(limited to 'Assignment2')

diff --git a/Assignment2/src/DTMC.dcl b/Assignment2/src/DTMC.dcl
index b663431..e7d0a78 100644
--- a/Assignment2/src/DTMC.dcl
+++ b/Assignment2/src/DTMC.dcl
@@ -4,6 +4,8 @@ from Data.Map import :: Map
 from Data.Maybe import :: Maybe
 from System.FilePath import :: FilePath
 
+from StdOverloaded import class toString
+
 :: *DTMC =
 	{ nr_states  :: !Int
 	, parameters :: ![String]
@@ -16,9 +18,12 @@ from System.FilePath import :: FilePath
 	, init        :: !Bool
 	}
 
+:: Op = LT | EQ | GT
+instance toString Op
+
 // Note that state_id must be an absorbing state
-// (Probability, state_id)
-:: Property :== (Real, Int)
+// (Operator, Probability, state_id)
+:: Property :== (Op, Real, Int)
 
 stateElimination :: !*DTMC -> *DTMC
 parseDTMC :: !FilePath !*World -> *(!*DTMC, !*World)
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