From 0782d98f8f55e0f33eac5dc7ae51ddc25b2bc786 Mon Sep 17 00:00:00 2001
From: Erin van der Veen
Date: Fri, 6 Jul 2018 12:22:21 +0200
Subject: Let z3 know that we have parameters

---
 Assignment2/src/DTMC.icl | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'Assignment2/src')

diff --git a/Assignment2/src/DTMC.icl b/Assignment2/src/DTMC.icl
index 0adfa1f..d3010e9 100644
--- a/Assignment2/src/DTMC.icl
+++ b/Assignment2/src/DTMC.icl
@@ -269,6 +269,12 @@ assertProperty (prob, target) dtmc z3 w
 # w = addAssert z3 formula w
 = (dtmc, w)
 
+z3AddVars :: !*DTMC !Z3 !*World -> (!*DTMC, !*World)
+z3AddVars dtmc z3 w
+# (param,dtmc) = dtmc!parameters
+# w = seqSt (addVariable z3) param w
+= (dtmc,w)
+
 Start w
 # ([prog:args],w) = getCommandLine w
 | length args <> 2
@@ -284,6 +290,7 @@ Start w
 # (dtmc,w) = assertProperty prop dtmc z3 w
 # (rC,dtmc) = repairConfig dtmc
 # w = seqSt (addAssert z3) rC.totality_restrictions w
+# (dtmc,w) = z3AddVars dtmc z3 w
 # (dtmcs,dtmc) = printDTMC dtmc
 # (_,w) = writeFile drn_out dtmcs w
 = w
-- 
cgit v1.2.3