From 5edab042669c68f7357ce3b7aa7f4d21f81446ad Mon Sep 17 00:00:00 2001
From: Artur Meski <artur.meski@gmail.com>
Date: Sun, 22 Jul 2018 14:12:14 +0100
Subject: [PATCH] Benchmarks

---
 in/gen_drs_mutex.py | 27 +++++++++++++++------------
 memtime.hh          | 17 ++++++++++++++++-
 2 files changed, 31 insertions(+), 13 deletions(-)

diff --git a/in/gen_drs_mutex.py b/in/gen_drs_mutex.py
index 35188c0..5cf3dd9 100755
--- a/in/gen_drs_mutex.py
+++ b/in/gen_drs_mutex.py
@@ -33,18 +33,17 @@ context-automaton {{
 """
 
 PROPERTY_STR = """
-rsctlk-property {{ default : {:s} }}
+rsctlk-property {{ {:s} : {:s} }}
 """
 
 
 #################################################################
 
-if len(argv) < 2:
-    print("Usage: {:s} <number of processes> <property number>".format(argv[0]))
+if len(argv) < 1:
+    print("Usage: {:s} <number of processes>".format(argv[0]))
     exit(100)
 
 n = int(argv[1])
-f = int(argv[2])
 
 assert n > 1, "number of proc must be > 1"
 
@@ -72,15 +71,19 @@ for i in range(n):
 
 out += CA_STR.format(transitions)
 
-if f == 1:
-    subf = "~proc1.in"
-    for i in range(2, n):
-        subf += " AND ~proc{:d}.in".format(i)
-    formula = "AG( proc0.in IMPLIES K[proc0]({:s}) )".format(subf)
-else:
-    assert False, "No such formula"
+# f1
+formula = "EF( proc0.in )"
+for i in range(1, n):
+    formula += " AND EF( proc{:d}.in )".format(i)
+out += PROPERTY_STR.format("f1",formula)
 
-out += PROPERTY_STR.format(formula)
+# f2
+subf = "~proc1.in"
+for i in range(2, n):
+    subf += " AND ~proc{:d}.in".format(i)
+formula = "AG( proc0.in IMPLIES K[proc0]({:s}) )".format(subf)
+
+out += PROPERTY_STR.format("f2",formula)
 
 print(out)
 
diff --git a/memtime.hh b/memtime.hh
index fcc4a2f..d257276 100644
--- a/memtime.hh
+++ b/memtime.hh
@@ -21,6 +21,9 @@
 
 #include <sys/time.h>
 #include <sys/resource.h>
+#if defined(__APPLE__)
+#include <malloc/malloc.h>
+#endif
 #include <stdio.h>
 #include <unistd.h>
 #include "macro.hh"
@@ -62,9 +65,21 @@ static inline int64 memUsedInt64()
   return (int64)memReadStat() * (int64)getpagesize();
 }
 
+#if defined(__APPLE__)
+
+static inline double memUsed() {
+    malloc_statistics_t t;
+    malloc_zone_statistics(NULL, &t);
+    return (double)t.max_size_in_use / (1024*1024); }
+
+#else
+
 static inline double memUsed()
 {
-  return memUsedInt64() / 1048576.0;
+  return memUsedInt64() / (1024*1024);
 }
 
 #endif
+
+#endif
+