From 7f43a3e64dd8ef839a453039fa412f1bc14fc040 Mon Sep 17 00:00:00 2001
From: Erin van der Veen
Date: Fri, 6 Jul 2018 12:04:42 +0200
Subject: Enforce totality constraints in 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 d9286fd..9d3eda1 100644
--- a/Assignment2/src/DTMC.icl
+++ b/Assignment2/src/DTMC.icl
@@ -282,8 +282,10 @@ Start w
 # dtmc = stateElimination dtmc
 # (z3,w) = startZ3 w
 # (dtmc,w) = assertProperty prop dtmc z3 w
-//# (dtmcs,dtmc) = printDTMC dtmc
-//# (_,w) = writeFile drn_out dtmcs w
+# (rC,dtmc) = repairConfig dtmc
+# (_,w) = mapSt (\s w -> (0, addAssert z3 s w)) rC.totality_restrictions w // Ugly, I know, don't care
+# (dtmcs,dtmc) = printDTMC dtmc
+# (_,w) = writeFile drn_out dtmcs w
 = w
 where
 	prop :: Property
-- 
cgit v1.2.3