From 44d31e5248ccf58bc107da54e5af7231a3e65d34 Mon Sep 17 00:00:00 2001
From: Erin van der Veen
Date: Fri, 6 Jul 2018 12:43:54 +0200
Subject: Change var naming, change order of commands to Z3

---
 Assignment2/src/DTMC.icl | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'Assignment2')

diff --git a/Assignment2/src/DTMC.icl b/Assignment2/src/DTMC.icl
index d3010e9..45abd4d 100644
--- a/Assignment2/src/DTMC.icl
+++ b/Assignment2/src/DTMC.icl
@@ -221,7 +221,7 @@ where
 	# dtmc & parameters = [var:parameters]
 	= dtmc
 	where
-		var = "v" <+ f <+ "_" <+ t
+		var = "v" <+ f <+ "x" <+ t
 
 repairConfig :: !*DTMC -> *(!RepairConfig, !*DTMC)
 repairConfig dtmc=:{nr_states,states}
@@ -287,10 +287,12 @@ Start w
 # dtmc = addVars dtmc
 # dtmc = stateElimination dtmc
 # (z3,w) = startZ3 w
+# (dtmc,w) = z3AddVars dtmc z3 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
+# (sat,w) = checkSat z3 w
+| sat = abort "test"
 # (dtmcs,dtmc) = printDTMC dtmc
 # (_,w) = writeFile drn_out dtmcs w
 = w
-- 
cgit v1.2.3