Merge branch 'master' of gitlab.science.ru.nl:eveen/Model-Checking

4 files changed, 44 insertions, 34 deletions

diff --git a/Assignment2/src/DTMC.dcl b/Assignment2/src/DTMC.dcl
index 233739b..98ef581 100644
--- a/Assignment2/src/DTMC.dcl
+++ b/Assignment2/src/DTMC.dcl
@@ -33,7 +33,8 @@ printDTMC :: !*DTMC -> *(!String, !*DTMC)
 addVars :: !*DTMC -> *DTMC
 
 :: RepairConfig =
-	{ totality_restrictions :: ![String]
+	{ totality_restrictions   :: ![String]
+	, transition_restrictions :: ![String]
 	}
 
 repairConfig :: !*DTMC -> *(!RepairConfig, !*DTMC)
diff --git a/Assignment2/src/DTMC.icl b/Assignment2/src/DTMC.icl
index 29b505c..9c36b5b 100644
--- a/Assignment2/src/DTMC.icl
+++ b/Assignment2/src/DTMC.icl
@@ -21,10 +21,13 @@ import System.CommandLine
 import System.File
 import System.FilePath
 import Text
+import Text.GenParse
 
 import Expression
 import Z3
 
+derive gParse Op, (,,)
+
 paths :: !*DTMC -> *([[Int]], !*DTMC)
 paths dtmc=:{nr_states,states}
 # (inits,states) = getInitStates (nr_states-1) states
@@ -226,9 +229,11 @@ where
 repairConfig :: !*DTMC -> *(!RepairConfig, !*DTMC)
 repairConfig dtmc=:{nr_states,states}
 # (ss,states) = collectStates (nr_states-1) states
+# transs = concatMap collectTransitions ss
 # dtmc & states = states
 # config =
-	{ totality_restrictions = map totality ss
+	{ totality_restrictions   = map totality ss
+	, transition_restrictions = concatMap probabilityBounds transs
 	}
 = (config, dtmc)
 where
@@ -236,16 +241,25 @@ where
 	collectStates i ss
 	| i < 0 = ([], ss)
 	# (s,ss) = ss![i]
-	| isNothing s = ([], ss)
+	| isNothing s = collectStates (i-1) ss
 	# s = fromJust s
 	# (rest,ss) = collectStates (i-1) ss
 	= ([s:rest],ss)
 
+	collectTransitions :: !State -> [(!Int,!Int,!String)]
+	collectTransitions s = [(s.state_id, to, prob) \\ (to,prob) <- 'M'.toList s.transitions]
+
 	totality :: !State -> String
 	totality s = "(= 1 " <+ parenthesise (parseInfix expr) <+ ")"
 	where
 		expr = "(" <+ (join ")+(" $ 'M'.elems s.transitions) <+ ")"
 
+	probabilityBounds :: !(!Int, !Int, !String) -> [String]
+	probabilityBounds (_,_,prob) =
+		[ "(<= 0 " <+ parenthesise (parseInfix prob) <+ ")"
+		, "(>= 1 " <+ parenthesise (parseInfix prob) <+ ")"
+		]
+
 findInitial :: !*DTMC -> (!State, !*DTMC)
 findInitial dtmc=:{nr_states,states}
 # (init,states) = findInitial` (nr_states-1) states
@@ -275,7 +289,7 @@ assertProperty :: !Property !*DTMC !Z3 !*World -> (*DTMC, *World)
 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"
+| isNothing formula = abort "Cannot reach property target from initial state\n"
 # formula = fromJust formula
 # formula = "( " <+ op <+ " " <+ prob <+ " " <+ parenthesise (parseInfix formula) <+ ")"
 # w = addAssert z3 formula w
@@ -290,30 +304,30 @@ z3AddVars dtmc z3 w
 parenthesise :: !a -> String | toString a
 parenthesise x = let s = toString x in if (s.[0] == '(') s ("(" +++ s +++ ")")
 
+parseProperty :: !String -> Property
+parseProperty s = case parseString s of
+	Nothing -> abort $ "Could not parse '" +++ s +++ "' as a property\n"
+	Just p  -> p
+
 Start w
 # ([prog:args],w) = getCommandLine w
-| length args <> 2
-	# (io,w) = stdio w
-	# io = io <<< "Usage: " <<< prog <<< " DRN_IN DRN_OUT\n"
-	# (_,w) = fclose io w
-	= ("", w)
-# [drn_in,drn_out:_] = args
+| length args <> 2 = "Usage: " +++ prog +++ " DRN PROPERTIES\n"
+# [drn_in,props:_] = args
+
 # (dtmc,w) = parseDTMC drn_in w
+# (props,w) = readFileLines props w
+# props = map (parseProperty o trim) $ fromOk props
+
 # dtmc = addVars dtmc
 # dtmc = stateElimination dtmc
 # (z3,w) = startZ3 w
 # (dtmc,w) = z3AddVars dtmc z3 w
-# (dtmc,w) = assertProperties properties dtmc z3 w
+# (dtmc,w) = assertProperties props dtmc z3 w
 # (rC,dtmc) = repairConfig dtmc
 # w = seqSt (addAssert z3) rC.totality_restrictions w
-# (dtmcs,dtmc) = printDTMC dtmc
-# (_,w) = writeFile drn_out dtmcs w
+# w = seqSt (addAssert z3) rC.transition_restrictions w
 # (sat,w) = checkSat z3 w
-| sat = getModel z3 w
-| otherwise = ("Could not satisfy the property", w)
-where
-	properties :: Properties
-	properties = [prop]
-
-	prop :: Property
-	prop = (EQ, 0.5, 7) // Chance to reach state 7 is 0.5
+| sat
+	# (model,w) = getModel z3 w
+	= model
+| otherwise = "Could not satisfy the property\n"
diff --git a/Assignment2/src/Z3.icl b/Assignment2/src/Z3.icl
index cb054e1..b4b7326 100644
--- a/Assignment2/src/Z3.icl
+++ b/Assignment2/src/Z3.icl
@@ -1,11 +1,9 @@
 implementation module Z3
 
-import System.Process
-import Text
-
 import StdString
 
-import StdDebug
+import System.Process
+import Text
 
 :: Z3 =
 	{ handle :: ProcessHandle
@@ -28,29 +26,26 @@ startZ3 w
 
 addAssert :: !Z3 !String !*World -> *World
 addAssert z3 s w
-# (_, w) = writePipe (trace_s ("(assert " <+ s <+ ")\n")) z3.Z3.stdIn w
+# (_, w) = writePipe ("(assert " <+ s <+ ")\n") z3.Z3.stdIn w
 = w
 
 addVariable :: !Z3 !String !*World -> *World
 addVariable z3 s w
-# (_, w) = writePipe (trace_s ("(declare-const " <+ s <+ " Real)\n")) z3.Z3.stdIn w
+# (_, w) = writePipe ("(declare-const " <+ s <+ " Real)\n") z3.Z3.stdIn w
 = w
 
 checkSat :: !Z3 !*World -> (!Bool, !*World)
 checkSat z3 w
-# (_, w) = writePipe (trace_s "(check-sat)\n") z3.Z3.stdIn w
+# (_, w) = writePipe "(check-sat)\n" z3.Z3.stdIn w
 # (out, w) = readPipeBlocking z3.Z3.stdOut w
 # out = fromOk out
 = (startsWith "sat" out, w)
 
 getModel :: !Z3 !*World -> (!String, !*World)
 getModel z3 w
-# (_, w) = writePipe (trace_s "(get-model)\n") z3.Z3.stdIn w
-# (_, w) = writePipe (trace_s "(exit)\n") z3.Z3.stdIn w
+# (_, w) = writePipe "(get-model)\n" z3.Z3.stdIn w
+# (_, w) = writePipe "(exit)\n" z3.Z3.stdIn w
 # (_, w) = waitForProcess z3.Z3.handle w
 # (out, w) = readPipeNonBlocking z3.Z3.stdOut w
 # out = fromOk out
 = (out, w)
-
-trace_s :: String -> String
-trace_s s = trace s s
diff --git a/Assignment2/src/die.properties b/Assignment2/src/die.properties
index c53d02c..f507f66 100644
--- a/Assignment2/src/die.properties
+++ b/Assignment2/src/die.properties
@@ -1 +1 @@
-P=? [F s=7 & d=2]
+(EQ, 0.5, 7)