Command line arguments

rs_testing.py

@@ -5,7 +5,7 @@ from logics import *
 import sys
 import resource
 
-def run_tests():
+def run_tests(cmd_args):
     
     # test_extended_automaton()
     # process()
@@ -13,7 +13,7 @@ def run_tests():
     # scalable_chain(print_system=True)
     # example44()
     # example44_param()
-    simple_param()
+    simple_param(cmd_args)
 
 def trivial_param():
 
@@ -47,7 +47,7 @@ def trivial_param():
     smt_rsc.check_rsltl(formula=f1, max_level=10, print_witness=True)
 
 
-def simple_param():
+def simple_param(cmd_args):
 
     r = ReactionSystemWithConcentrationsParam()
     r.add_bg_set_entity(("x", 3))
@@ -72,7 +72,8 @@ def simple_param():
 
     rc = ReactionSystemWithAutomaton(r, c)
     rc.show()
-    smt_rsc = SmtCheckerRSCParam(rc, optimise=True)
+    
+    smt_rsc = SmtCheckerRSCParam(rc, optimise=cmd_args.optimise)
 
     f1 = Formula_rsLTL.f_F(
         BagDescription.f_TRUE(),

rssmt.py

@@ -6,6 +6,8 @@
 
 """
 
+import argparse
+
 from rs import *
 from smt import *
 import sys
@@ -14,10 +16,11 @@ import rs_testing
 
 from colour import *
 
-import resource
-
 profiling = False
 
+if profiling:
+    import resource
+
 ##################################################################
 
 version = "2017/04/08/00"
@@ -43,8 +46,17 @@ def print_banner():
 def main():
     """Main function"""
 
+    parser = argparse.ArgumentParser()
+
+    parser.add_argument("-v", "--verbose", 
+        help="turn verbosity on", action="store_true")
+    parser.add_argument("-o", "--optimise", 
+        help="minimise the parametric computation result", action="store_true")
+
+    args = parser.parse_args()
+
     print_banner()
-    rs_testing.run_tests()
+    rs_testing.run_tests(args)
 
 ##################################################################
 

smt/smt_checker_rsc_param.py

@@ -726,12 +726,17 @@ class SmtCheckerRSCParam(object):
         return loop_enc
     
     def solver_add(self, expression):
+        """
+        This is a solver.add() wrapper
+        """
+    
+        if expression == True:
+            return
     
         if expression == False:
             raise RuntimeError("Trying to assert False.")
         
-        if not (expression == True):
-            self.solver.add(expression)
+        self.solver.add(expression)
 
     def check_reachability(self, state, print_witness=True, 
             print_time=True, print_mem=True, max_level=1000):