Examples

examples/smt/chain_reaction.py

@@ -26,54 +26,63 @@ from smt import *
 import sys
 import resource
 
+
 def chain_reaction(print_system=False):
-    
+
-    if len(sys.argv) < 1+3:
+    if len(sys.argv) < 1 + 3:
-        print("provide N M B")
+        print("{source} <N> <M> <type>".format(source=sys.argv[0]))
-        print(" B=1 - RSC")
+        print()
-        print(" B=0 - RSC translated into RS")
+        print("* N,M -- integers (scaling parameters)")
+        print("* type:")
+        print("  - 1 - RSC")
+        print("  - 0 - RSC translated into RS")
+        print()
         exit(1)
 
-    chainLen=int(sys.argv[1]) # chain length
+    chainLen = int(sys.argv[1])  
-    maxConc=int(sys.argv[2]) # depth (max concentration)
+    maxConc = int(sys.argv[2])  # depth (max concentration)
+
+    verify_rsc = bool(int(sys.argv[3]))
 
-    verify_rsc=bool(int(sys.argv[3]))
-        
     if chainLen < 1 or maxConc < 1:
         print("be reasonable")
         exit(1)
-    
-    r = ReactionSystemWithConcentrations()
-    r.add_bg_set_entity(("inc",1))
-    r.add_bg_set_entity(("dec",1))
-    
-    for i in range(1,chainLen+1):
-        r.add_bg_set_entity(("e_" + str(i),maxConc))
-    
-    for i in range(1,chainLen+1):
-        ent = "e_" + str(i)
-        r.add_reaction_inc(ent, "inc", [(ent, 1)],[(ent,maxConc)])
-        r.add_reaction_dec(ent, "dec", [(ent, 1)],[])
-        if i < chainLen:
-            r.add_reaction([(ent,maxConc)],[],[("e_"+str(i+1),1)])
 
-    r.add_reaction([("e_" + str(chainLen),maxConc)],[("dec",1)],[("e_" + str(chainLen),maxConc)])
+    r = ReactionSystemWithConcentrations()
-    
+    r.add_bg_set_entity(("inc", 1))
+    r.add_bg_set_entity(("dec", 1))
+
+    for i in range(1, chainLen + 1):
+        r.add_bg_set_entity(("e_" + str(i), maxConc))
+
+    for i in range(1, chainLen + 1):
+        ent = "e_" + str(i)
+        r.add_reaction_inc(ent, "inc", [(ent, 1)], [(ent, maxConc)])
+        r.add_reaction_dec(ent, "dec", [(ent, 1)], [])
+        if i < chainLen:
+            r.add_reaction([(ent, maxConc)], [], [("e_" + str(i + 1), 1)])
+
+    r.add_reaction(
+        [("e_" + str(chainLen), maxConc)],
+        [("dec", 1)],
+        [("e_" + str(chainLen), maxConc)],
+    )
+
     c = ContextAutomatonWithConcentrations(r)
     c.add_init_state("init")
     c.add_state("working")
-    c.add_transition("init", [("e_1",1),("inc",1)], "working")
+    c.add_transition("init", [("e_1", 1), ("inc", 1)], "working")
-    c.add_transition("working", [("inc",1)], "working")
+    c.add_transition("working", [("inc", 1)], "working")
+
+    rc = ReactionSystemWithAutomaton(r, c)
 
-    rc = ReactionSystemWithAutomaton(r,c)
-    
     if print_system:
         rc.show()
-    
+
     if verify_rsc:
         smt_rsc = SmtCheckerRSC(rc)
-        prop = [('e_'+str(chainLen),maxConc)]
+        prop = [("e_" + str(chainLen), maxConc)]
-        smt_rsc.check_reachability((prop,[]),max_level=maxConc*chainLen+10)
+        smt_rsc.check_reachability((prop, []), max_level=maxConc * chainLen + 10)
 
     else:
         orc = rc.get_ordinary_reaction_system_with_automaton()
@@ -81,26 +90,26 @@ def chain_reaction(print_system=False):
             print("\nTranslated:")
             orc.show()
         smt_tr_rs = SmtCheckerRS(orc)
-        smt_tr_rs.check_reachability(['e_'+str(chainLen)+"#"+str(maxConc)])
+        smt_tr_rs.check_reachability(["e_" + str(chainLen) + "#" + str(maxConc)])
-    
-    time=0
-    mem_usage=resource.getrusage(resource.RUSAGE_SELF).ru_maxrss/(1024*1024)
-    if verify_rsc:
-        filename_t="bench_rsc_time.log"
-        filename_m="bench_rsc_mem.log"
-        time=smt_rsc.get_verification_time()
-    else:
-        filename_t="bench_tr_rs_time.log"
-        filename_m="bench_tr_rs_mem.log"
-        time=smt_tr_rs.get_verification_time()
 
-    f=open(filename_t, 'a')    
+    time = 0
-    log_str="(" + str(chainLen) + "," + str(maxConc) + "," + str(time) + ")\n"
+    mem_usage = resource.getrusage(resource.RUSAGE_SELF).ru_maxrss / (1024 * 1024)
+    if verify_rsc:
+        filename_t = "bench_rsc_time.log"
+        filename_m = "bench_rsc_mem.log"
+        time = smt_rsc.get_verification_time()
+    else:
+        filename_t = "bench_tr_rs_time.log"
+        filename_m = "bench_tr_rs_mem.log"
+        time = smt_tr_rs.get_verification_time()
+
+    f = open(filename_t, "a")
+    log_str = "(" + str(chainLen) + "," + str(maxConc) + "," + str(time) + ")\n"
     f.write(log_str)
     f.close()
-    
+
-    f=open(filename_m, 'a')
+    f = open(filename_m, "a")
-    log_str="(" + str(chainLen) + "," + str(maxConc) + "," + str(mem_usage) + ")\n"
+    log_str = "(" + str(chainLen) + "," + str(maxConc) + "," + str(mem_usage) + ")\n"
     f.write(log_str)
     f.close()
 
@@ -109,7 +118,8 @@ def main():
 
     chain_reaction()
 
+
 if __name__ == "__main__":
     main()
-        
+
 # EOF

examples/smt/heat_shock_response.py

@@ -112,6 +112,10 @@ def heat_shock_response(print_system=True, verify_rsc=True):
         smt_tr_rs.check_reachability(rs_prop)
 
 
+def state_translate_rsc2rs(p):
+    return [e[0] + "#" + str(e[1]) for e in p]
+
+
 def main():
 
     heat_shock_response()