From 9e81dd9ba4998d069d09a3a860a6fef12ad0b9a0 Mon Sep 17 00:00:00 2001
From: Artur Meski <artur.meski@gmail.com>
Date: Sun, 29 Sep 2019 16:19:31 +0100
Subject: [PATCH] Readme, mutex benchmark

---
 README.md                   | 31 +++++++++++++++++++++---
 examples/smt/mutex_param.py | 48 +++++++++++++++++--------------------
 2 files changed, 50 insertions(+), 29 deletions(-)

diff --git a/README.md b/README.md
index a0321af..350c95e 100644
--- a/README.md
+++ b/README.md
@@ -27,7 +27,7 @@ To test the SMT module you can perform reachability verification of the scalable
 Running the benchmark without any arguments tells us what parameters are available:
 
 ```
-./reactics smt examples/smt/scalable_chain.py
+$ ./reactics smt examples/smt/scalable_chain.py
 
  ------------------------------------------------
  -- ReactICS -- Reaction Systems Model Checker --
@@ -49,7 +49,7 @@ To test the SMT module for rsLTL verification the scalable chain system benchmar
 
 
 ```
-./reactics smt examples/smt/scalable_chain.py 2 5 1
+$ ./reactics smt examples/smt/scalable_chain.py 2 5 1
 ```
 
 
@@ -59,7 +59,32 @@ To test the SMT module for rsLTL verification the scalable chain system benchmar
 To test the reaction synthesis approach on a mutual exclution protocol modelling three processes, run the following command:
 
 ```
-./reactics smt examples/smt/mutex_param.py -n 3 -s 1 -o
+$ ./reactics smt examples/smt/mutex_param.py 3 p -o
+```
+
+To check the available parameters for the benchmark, we run it with `-h`:
+
+```
+$ ./reactics smt examples/smt/mutex_param.py -h
+
+ ------------------------------------------------
+ -- ReactICS -- Reaction Systems Model Checker --
+ ------------------------------------------------
+
+usage: mutex_param.py [-h] [-v] [-o] scaling {p,np-p,np-np}
+
+positional arguments:
+  scaling         scaling parameter value
+  {p,np-p,np-np}  Selects the mode: p - parameter synthesis (parametric
+                  implementation), np-p - non-parametric with parametric
+                  implementation (with the parameters substituted), np-np -
+                  non-parametric with non-parametric implementation
+                  (parameters substituted)
+
+optional arguments:
+  -h, --help      show this help message and exit
+  -v, --verbose   turn verbosity on
+  -o, --optimise  minimise the parametric computation result
 ```
 
 
diff --git a/examples/smt/mutex_param.py b/examples/smt/mutex_param.py
index 702ea18..5a5ff15 100644
--- a/examples/smt/mutex_param.py
+++ b/examples/smt/mutex_param.py
@@ -49,10 +49,10 @@ def mutex_param_bench(cmd_args):
     base_entities = ["out", "req", "in", "act"]
     shared_entities = ["lock", "done", "s"]
 
-    if not cmd_args.scaling_parameter:
+    if not cmd_args.scaling:
         print("Missing scaling parameter")
         return
-    n_proc = int(cmd_args.scaling_parameter)
+    n_proc = int(cmd_args.scaling)
 
     r = ReactionSystemWithConcentrationsParam()
 
@@ -196,9 +196,9 @@ def mutex_nonparam_bench(cmd_args):
     base_entities = ["out", "req", "in", "act"]
     shared_entities = ["lock", "done", "s"]
 
-    if not cmd_args.scaling_parameter:
+    if not cmd_args.scaling:
         raise RuntimeError("Missing scaling parameter")
-    n_proc = int(cmd_args.scaling_parameter)
+    n_proc = int(cmd_args.scaling)
 
     r = ReactionSystemWithConcentrationsParam()
 
@@ -304,9 +304,9 @@ def mutex_nonparam_bench_oldimpl(cmd_args):
     base_entities = ["out", "req", "in", "act"]
     shared_entities = ["lock", "done", "s"]
 
-    if not cmd_args.scaling_parameter:
+    if not cmd_args.scaling:
         raise RuntimeError("Missing scaling parameter")
-    n_proc = int(cmd_args.scaling_parameter)
+    n_proc = int(cmd_args.scaling)
 
     r = ReactionSystemWithConcentrations()
 
@@ -408,20 +408,13 @@ def state_translate_rsc2rs(p):
 
 def mutex_bench_main(cmd_args):
 
-    if not cmd_args.special_mode:
-        print("Missing special mode parameter")
-        print("*    1 - parametric")
-        print("*    2 - non-parametric (with parametric implementation)")
-        print("*    3 - non-parametric (with non-parametric implementation)")
-        return
+    mode = cmd_args.mode
 
-    smode = int(cmd_args.special_mode)
-
-    if smode == 1:
+    if mode == "p":
         mutex_param_bench(cmd_args)
-    elif smode == 2:
+    elif mode == "np-p":
         mutex_nonparam_bench(cmd_args)
-    elif smode == 3:
+    elif mode == "np-np":
         mutex_nonparam_bench_oldimpl(cmd_args)
     else:
         print("Unrecognised mode")
@@ -432,6 +425,17 @@ def main():
 
     parser = argparse.ArgumentParser()
 
+    parser.add_argument(
+        "scaling",
+        help="scaling parameter value",
+    )
+    
+    parser.add_argument(
+        "mode",
+        choices=['p', 'np-p', 'np-np'], 
+        help="Selects the mode: p - parameter synthesis (parametric implementation), np-p - non-parametric with parametric implementation (with the parameters substituted), np-np - non-parametric with non-parametric implementation (parameters substituted)",
+    )
+
     parser.add_argument(
         "-v", "--verbose", help="turn verbosity on", action="store_true"
     )
@@ -441,17 +445,9 @@ def main():
         help="minimise the parametric computation result",
         action="store_true",
     )
-    parser.add_argument(
-        "-n",
-        "--scaling-parameter",
-        help="scaling parameter value (used in some benchmarks)",
-    )
-    parser.add_argument(
-        "-s", "--special_mode", help="special mode (used in some benchmarks)"
-    )
 
     args = parser.parse_args()
-
+        
     mutex_bench_main(args)