diff --git a/modeling/scripts/z3script b/modeling/scripts/z3script new file mode 100644 index 0000000000000000000000000000000000000000..4ec1e300990ffba709dc52b8264509400fdc2292 --- /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 d869ad561d911410af248c6d6d0dff048cfee544..df8bf4d8e98eefc2f23a60dac888a3d5d0b3a98d 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 {