From d9011b5b2b5163228de4dd33edd3903ff09d8434 Mon Sep 17 00:00:00 2001
From: Camil Staps
Date: Fri, 6 Jul 2018 15:30:13 +0200
Subject: Try to let Z3 minimize stuff

---
 Assignment2/src/DTMC.icl | 8 +++++---
 Assignment2/src/Z3.dcl   | 2 +-
 Assignment2/src/Z3.icl   | 8 ++++----
 Assignment2/src/start.sh | 2 --
 4 files changed, 10 insertions(+), 10 deletions(-)

(limited to 'Assignment2')

diff --git a/Assignment2/src/DTMC.icl b/Assignment2/src/DTMC.icl
index c9696cf..bd6f9e1 100644
--- a/Assignment2/src/DTMC.icl
+++ b/Assignment2/src/DTMC.icl
@@ -300,8 +300,8 @@ assertProperty (op, prob, target) dtmc z3 w
 
 z3AddVars :: !*DTMC !Z3 !*World -> (!*DTMC, !*World)
 z3AddVars dtmc z3 w
-# (param,dtmc) = dtmc!parameters
-# w = seqSt (addVariable z3) param w
+# (params,dtmc) = dtmc!parameters
+# w = seqSt (addVariable z3 "Real") params w
 = (dtmc,w)
 
 parenthesise :: !a -> String | toString a
@@ -330,7 +330,9 @@ Start w
 # (dtmc,w) = assertProperties props dtmc z3 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!
+# w = addVariable z3 "Real" "cost" w
+# w = addAssert z3 ("(= cost " +++ config.minimalisation_goal +++ ")") w
+//# w = addMinimize z3 "cost" w // TODO: not supported by Z3!
 
 # (sat,w) = checkSat z3 w
 | sat
diff --git a/Assignment2/src/Z3.dcl b/Assignment2/src/Z3.dcl
index 4708401..0f636f2 100644
--- a/Assignment2/src/Z3.dcl
+++ b/Assignment2/src/Z3.dcl
@@ -7,7 +7,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
+addVariable :: !Z3 !String !String !*World -> *World
 checkSat :: !Z3 !*World -> (!Bool, !*World)
 
 // Note: getModel terminates z3
diff --git a/Assignment2/src/Z3.icl b/Assignment2/src/Z3.icl
index 8494bad..ca869a1 100644
--- a/Assignment2/src/Z3.icl
+++ b/Assignment2/src/Z3.icl
@@ -38,9 +38,9 @@ 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 (trace_id $ "(declare-const " <+ s <+ " Real)\n") z3.Z3.stdIn w
+addVariable :: !Z3 !String !String !*World -> *World
+addVariable z3 type s w
+# (_, w) = writePipe (trace_id $ "(declare-const " <+ s <+ " " <+ type <+ ")\n") z3.Z3.stdIn w
 = w
 
 checkSat :: !Z3 !*World -> (!Bool, !*World)
@@ -49,7 +49,7 @@ checkSat z3 w
 # (out, w) = readPipeBlocking z3.Z3.stdOut w
 # out = fromOk out
 # out = trace_id out
-= (startsWith "sat" out, w)
+= (endsWith "sat\n" out, w)
 
 getModel :: !Z3 !*World -> (!String, !*World)
 getModel z3 w
diff --git a/Assignment2/src/start.sh b/Assignment2/src/start.sh
index 32072b5..ab77900 100755
--- a/Assignment2/src/start.sh
+++ b/Assignment2/src/start.sh
@@ -1,6 +1,5 @@
 #!/bin/bash
 DOCKER_IMAGE=modelrepair
-DOCKER_NAME=modelrepair
 
 docker build -q -t $DOCKER_IMAGE . || exit
 
@@ -9,6 +8,5 @@ docker run\
 	-w /src\
 	--rm\
 	-it\
-	--name $DOCKER_NAME\
 	$DOCKER_IMAGE\
 	$@
-- 
cgit v1.2.3