Add minimization goals (not supported by Z3)

7 files changed, 57 insertions, 31 deletions

diff --git a/Assignment2/src/DTMC.dcl b/Assignment2/src/DTMC.dcl
index 98ef581..04243c4 100644
--- a/Assignment2/src/DTMC.dcl
+++ b/Assignment2/src/DTMC.dcl
@@ -35,6 +35,11 @@ addVars :: !*DTMC -> *DTMC
 :: RepairConfig =
 	{ totality_restrictions   :: ![String]
 	, transition_restrictions :: ![String]
+	, minimalisation_goal     :: !String
 	}
 
-repairConfig :: !*DTMC -> *(!RepairConfig, !*DTMC)
+:: CostFunction
+	= SumSquaredErrors
+	| NumberModifiedTransitions
+
+repairConfig :: !CostFunction !*DTMC -> *(!RepairConfig, !*DTMC)
diff --git a/Assignment2/src/DTMC.icl b/Assignment2/src/DTMC.icl
index 9c36b5b..c9696cf 100644
--- a/Assignment2/src/DTMC.icl
+++ b/Assignment2/src/DTMC.icl
@@ -71,15 +71,10 @@ where
 	| i < 0 = ss
 	# (Just s,ss) = ss![i]
 	| s.init || isAbsorbing s = prune (i-1) ss
-	| otherwise               = prune (i-1) $ remove i (nr_states-1) ss
+	| otherwise               = prune (i-1) $ remove i ss
 	where
-		remove :: !Int !Int !*{Maybe State} -> *{Maybe State}
-		remove i j ss
-		| j < 0 = {ss & [i]=Nothing}
-		# (s,ss) = ss![j]
-		| isNothing s = remove i (j-1) ss
-		# s = fromJust s
-		= remove i (j-1) ss
+		remove :: !Int !*{Maybe State} -> *{Maybe State}
+		remove i ss = {ss & [i]=Nothing}
 
 	elim :: !Int !Int !*{Maybe State} -> *{Maybe State}
 	elim s1 s ss
@@ -92,7 +87,7 @@ where
 	| succ.init || isAbsorbing succ = ss
 	# succ = succ.transitions
 
-	# self_prob = fromMaybe "0" $ 'M'.get s succ
+	# self_prob = fromMaybe "0.0" $ 'M'.get s succ
 	# succ = 'M'.toList succ
 	| s1 == s
 		# ss = seqSt (uncurry $ update_eq self_prob) succ ss
@@ -112,7 +107,7 @@ where
 		# ss & [s1] = Just
 			{ s1s
 			& transitions = 'M'.put s2
-				("(" +++ prob2 +++ ")/(1-(" +++ self_prob +++ "))")
+				("(" +++ prob2 +++ ")/(1.0-(" +++ self_prob +++ "))")
 				s1s.transitions
 			}
 		= ss
@@ -121,12 +116,12 @@ where
 		update_ne self_prob s2 prob2 ss
 		| s == s2 = ss
 		# (Just s1s,ss) = ss![s1]
-		# ps1s2 = fromMaybe "0" $ 'M'.get s2 s1s.transitions
-		# ps1s = fromMaybe "0" $ 'M'.get s s1s.transitions
+		# ps1s2 = fromMaybe "0.0" $ 'M'.get s2 s1s.transitions
+		# ps1s = fromMaybe "0.0" $ 'M'.get s s1s.transitions
 		# ss & [s1] = Just
 			{ s1s
 			& transitions = 'M'.put s2
-				(ps1s2 +++ "+(" +++ ps1s +++ ")*(" +++ prob2 +++ ")/(1-(" +++ self_prob +++ "))")
+				(ps1s2 +++ "+(" +++ ps1s +++ ")*(" +++ prob2 +++ ")/(1.0-(" +++ self_prob +++ "))")
 				s1s.transitions
 			}
 		= ss
@@ -226,14 +221,15 @@ where
 	where
 		var = "v" <+ f <+ "x" <+ t
 
-repairConfig :: !*DTMC -> *(!RepairConfig, !*DTMC)
-repairConfig dtmc=:{nr_states,states}
+repairConfig :: !CostFunction !*DTMC -> *(!RepairConfig, !*DTMC)
+repairConfig cf dtmc=:{nr_states,parameters,states}
 # (ss,states) = collectStates (nr_states-1) states
 # transs = concatMap collectTransitions ss
 # dtmc & states = states
 # config =
 	{ totality_restrictions   = map totality ss
 	, transition_restrictions = concatMap probabilityBounds transs
+	, minimalisation_goal     = minimise cf parameters
 	}
 = (config, dtmc)
 where
@@ -250,16 +246,23 @@ where
 	collectTransitions s = [(s.state_id, to, prob) \\ (to,prob) <- 'M'.toList s.transitions]
 
 	totality :: !State -> String
-	totality s = "(= 1 " <+ parenthesise (parseInfix expr) <+ ")"
+	totality s = "(= 1.0 " <+ 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) <+ ")"
+		[ "(<= 0.0 " <+ parenthesise (parseInfix prob) <+ ")"
+		, "(>= 1.0 " <+ parenthesise (parseInfix prob) <+ ")"
 		]
 
+	minimise :: !CostFunction ![String] -> String
+	minimise cf params = foldr1 (\a b -> "(+ " <+ a <+ " " <+ b <+ ")") $ case cf of
+		NumberModifiedTransitions ->
+			["(if (= 0.0 " <+ p <+ ") 0.0 1.0)" \\ p <- params]
+		SumSquaredErrors ->
+			["(* " <+ p <+ " " <+ p <+ ")" \\ p <- params]
+
 findInitial :: !*DTMC -> (!State, !*DTMC)
 findInitial dtmc=:{nr_states,states}
 # (init,states) = findInitial` (nr_states-1) states
@@ -320,14 +323,17 @@ Start w
 
 # dtmc = addVars dtmc
 # dtmc = stateElimination dtmc
+# (config,dtmc) = repairConfig SumSquaredErrors dtmc
+
 # (z3,w) = startZ3 w
 # (dtmc,w) = z3AddVars dtmc z3 w
 # (dtmc,w) = assertProperties props dtmc z3 w
-# (rC,dtmc) = repairConfig dtmc
-# w = seqSt (addAssert z3) rC.totality_restrictions w
-# w = seqSt (addAssert z3) rC.transition_restrictions w
+# w = seqSt (addAssert z3) config.totality_restrictions w
+# w = seqSt (addAssert z3) config.transition_restrictions w
+//# w = addMinimize z3 config.minimalisation_goal w // TODO: not supported by Z3!
+
 # (sat,w) = checkSat z3 w
 | sat
 	# (model,w) = getModel z3 w
 	= model
-| otherwise = "Could not satisfy the property\n"
+= "Could not satisfy the property\n"
diff --git a/Assignment2/src/Dockerfile b/Assignment2/src/Dockerfile
index a654427..39b3c34 100644
--- a/Assignment2/src/Dockerfile
+++ b/Assignment2/src/Dockerfile
@@ -26,6 +26,6 @@ ENV CLEAN_HOME=/opt/clean
 ENV PATH=$PATH:/opt/storm/build/bin:/opt/clean/bin:/opt/clean/exe
 
 COPY DTMC.dcl DTMC.icl Z3.dcl Z3.icl Expression.dcl Expression.icl /tmp/
-RUN cd /tmp; clm -ms -b -nt -IL Platform DTMC -o dtmc
+RUN cd /tmp; clm -tst -ms -b -nt -IL Platform DTMC -o /opt/dtmc
 
 ENTRYPOINT ["/src/repair.sh"]
diff --git a/Assignment2/src/Expression.icl b/Assignment2/src/Expression.icl
index 7622103..53699c0 100644
--- a/Assignment2/src/Expression.icl
+++ b/Assignment2/src/Expression.icl
@@ -1,8 +1,10 @@
 implementation module Expression
 
 from StdChar import instance == Char
-from StdOverloaded import class toString(toString)
-from StdString import instance toString {#Char}, instance toString Int, instance toString Real
+from StdOverloaded import class toString(toString), class toReal(toReal)
+from StdReal import entier, instance toReal Int, instance == Real
+from StdString import
+	instance toString {#Char}, instance toString Int, instance toString Real
 
 import Data._Array
 from Data.Func import $
@@ -46,6 +48,6 @@ where
 		(e1 - e2) -> "(- " <+ e1 <+ " " <+ e2 <+ ")"
 		(e1 * e2) -> "(* " <+ e1 <+ " " <+ e2 <+ ")"
 		(e1 / e2) -> "(/ " <+ e1 <+ " " <+ e2 <+ ")"
-		LitInt i  -> toString i
-		LitReal r -> toString r
+		LitInt i  -> toString i <+ ".0"
+		LitReal r -> if (toReal (entier r) == r) (r <+ ".0") (toString r)
 		Var v     -> v
diff --git a/Assignment2/src/Z3.dcl b/Assignment2/src/Z3.dcl
index 8628d5d..4708401 100644
--- a/Assignment2/src/Z3.dcl
+++ b/Assignment2/src/Z3.dcl
@@ -6,6 +6,7 @@ from System.Process import :: ProcessHandle, :: ProcessIO
 
 startZ3 :: !*World -> (!Z3, !*World)
 addAssert :: !Z3 !String !*World -> *World
+addMinimize :: !Z3 !String !*World -> *World
 addVariable :: !Z3 !String !*World -> *World
 checkSat :: !Z3 !*World -> (!Bool, !*World)
 
diff --git a/Assignment2/src/Z3.icl b/Assignment2/src/Z3.icl
index b4b7326..8494bad 100644
--- a/Assignment2/src/Z3.icl
+++ b/Assignment2/src/Z3.icl
@@ -5,6 +5,10 @@ import StdString
 import System.Process
 import Text
 
+import StdDebug
+from Data.Func import $
+trace_id x = trace x x
+
 :: Z3 =
 	{ handle :: ProcessHandle
 	, stdIn  :: WritePipe
@@ -26,12 +30,17 @@ startZ3 w
 
 addAssert :: !Z3 !String !*World -> *World
 addAssert z3 s w
-# (_, w) = writePipe ("(assert " <+ s <+ ")\n") z3.Z3.stdIn w
+# (_, w) = writePipe (trace_id $ "(assert " <+ s <+ ")\n") z3.Z3.stdIn w
+= w
+
+addMinimize :: !Z3 !String !*World -> *World
+addMinimize z3 s w
+# (_, w) = writePipe (trace_id $ "(minimize " <+ s <+ ")\n") z3.Z3.stdIn w
 = w
 
 addVariable :: !Z3 !String !*World -> *World
 addVariable z3 s w
-# (_, w) = writePipe ("(declare-const " <+ s <+ " Real)\n") z3.Z3.stdIn w
+# (_, w) = writePipe (trace_id $ "(declare-const " <+ s <+ " Real)\n") z3.Z3.stdIn w
 = w
 
 checkSat :: !Z3 !*World -> (!Bool, !*World)
@@ -39,6 +48,7 @@ checkSat z3 w
 # (_, w) = writePipe "(check-sat)\n" z3.Z3.stdIn w
 # (out, w) = readPipeBlocking z3.Z3.stdOut w
 # out = fromOk out
+# out = trace_id out
 = (startsWith "sat" out, w)
 
 getModel :: !Z3 !*World -> (!String, !*World)
diff --git a/Assignment2/src/repair.sh b/Assignment2/src/repair.sh
index 24cbb37..f4e39a5 100755
--- a/Assignment2/src/repair.sh
+++ b/Assignment2/src/repair.sh
@@ -5,10 +5,12 @@ MODEL="$1"
 DRN="${MODEL/prism/drn}"
 PROPS="$2"
 
+cd /src
+
 echo "Arguments: $@"
 
 echo "Generating DRN..."
 storm --prism "$MODEL" --io:exportexplicit "$DRN" || exit
 
 echo "Repairing model..."
-./dtmc "$DRN" "$PROPS"
+/opt/dtmc "$DRN" "$PROPS"