From 7035290ed2e7832dae17c7ccfb238046d005f923 Mon Sep 17 00:00:00 2001
From: Ludovic Apvrille <ludovic.apvrille@telecom-paristech.fr>
Date: Thu, 2 May 2019 13:33:33 +0200
Subject: [PATCH] Adding z3 script
---
modeling/scripts/z3script | 7 +++++++
.../interactivesimulation/JFrameInteractiveSimulation.java | 2 +-
2 files changed, 8 insertions(+), 1 deletion(-)
create mode 100644 modeling/scripts/z3script
diff --git a/modeling/scripts/z3script b/modeling/scripts/z3script
new file mode 100644
index 0000000000..4ec1e30099
--- /dev/null
+++ b/modeling/scripts/z3script
@@ -0,0 +1,7 @@
+set model ./../tmlcode/specz3.tmap
+tml load $model
+tml checksyntax
+tml loadz3lib /opt/z3/bin/libz3.dylib:/opt/z3/bin/libz3java.dylib
+tml z3opt
+tml save-result ../tmlcode/z3result
+tml save-result-tml-mapping ../tmlcode/z3result
diff --git a/src/main/java/ui/interactivesimulation/JFrameInteractiveSimulation.java b/src/main/java/ui/interactivesimulation/JFrameInteractiveSimulation.java
index d869ad561d..df8bf4d8e9 100755
--- a/src/main/java/ui/interactivesimulation/JFrameInteractiveSimulation.java
+++ b/src/main/java/ui/interactivesimulation/JFrameInteractiveSimulation.java
@@ -2985,7 +2985,7 @@ public class JFrameInteractiveSimulation extends JFrame implements ActionListene
_state = tasktm.getState(valueTable.get(new Integer(id)));
}
- TraceManager.addDev("state:" + _state);
+ //TraceManager.addDev("state:" + _state);
if ((i != null) && (c != null)) {
try {
--
GitLab