some cleanup

2016-12-27 20:57:02 +01:00
parent 11a2d2ae46
commit 56218a3596
7 changed files with 36 additions and 427 deletions
--- a/bench_rsc_mem.log
+++ b/bench_rsc_mem.log
@@ -1,104 +0,0 @@
-(2,2,24.9453125)
-(2,4,23.8828125)
-(2,6,23.703125)
-(2,8,24.98046875)
-(2,10,24.8359375)
-(2,12,24.91796875)
-(2,14,25.2265625)
-(2,16,26.0703125)
-(2,18,25.93359375)
-(2,20,27.328125)
-(4,2,23.9140625)
-(4,4,25.234375)
-(4,6,25.0234375)
-(4,8,27.27734375)
-(4,10,29.77734375)
-(4,12,32.92578125)
-(4,14,35.92578125)
-(4,16,39.78125)
-(4,18,43.3359375)
-(4,20,49.38671875)
-(6,2,24.94921875)
-(6,4,27.03515625)
-(6,6,29.890625)
-(6,8,35.92578125)
-(6,10,41.2578125)
-(6,12,49.046875)
-(6,14,54.49609375)
-(6,16,65.44921875)
-(6,18,76.3203125)
-(6,20,84.02734375)
-(8,2,25.328125)
-(8,4,30.578125)
-(8,6,37.89453125)
-(8,8,46.16015625)
-(8,10,61.4453125)
-(8,12,71.0859375)
-(8,14,84.8203125)
-(8,16,107.48828125)
-(8,18,125.99609375)
-(8,20,142.421875)
-(10,2,26.95703125)
-(10,4,37.01953125)
-(10,6,51.7421875)
-(10,8,65.03515625)
-(10,10,82.9453125)
-(10,12,117.609375)
-(10,14,128.96875)
-(10,16,168.6328125)
-(10,18,191.53125)
-(10,20,215.89453125)
-(12,2,29.86328125)
-(12,4,44.515625)
-(12,6,65.70703125)
-(12,8,90.625)
-(12,10,124.71875)
-(12,12,150.05859375)
-(12,14,189.8828125)
-(12,16,217.9921875)
-(12,18,297.3515625)
-(12,20,336.13671875)
-(14,2,33.0859375)
-(14,4,54.890625)
-(14,6,89.5546875)
-(14,8,121.6484375)
-(14,10,153.89453125)
-(14,12,210.78515625)
-(14,14,252.34375)
-(14,16,323.01953125)
-(14,18,377.89453125)
-(14,20,422.3828125)
-(16,2,36.98828125)
-(16,4,65.7421875)
-(16,6,104.17578125)
-(16,8,150.47265625)
-(16,10,222.5625)
-(16,12,266.2578125)
-(16,14,338.49609375)
-(16,16,398.515625)
-(16,18,521.171875)
-(16,20,579.015625)
-(18,2,43.71875)
-(18,4,84.63671875)
-(18,6,136.3515625)
-(18,8,204.0546875)
-(18,10,260.53125)
-(18,12,342.73828125)
-(18,14,413.78125)
-(18,16,546.4140625)
-(18,18,624.328125)
-(18,20,706.109375)
-(20,2,47.14453125)
-(20,4,94.03125)
-(20,6,166.375)
-(20,8,234.64453125)
-(20,10,332.78125)
-(20,12,415.71875)
-(20,14,565.51953125)
-(20,16,654.6328125)
-(20,18,753.8125)
-(20,20,938.97265625)
-(2,2,23.7109375)
-(2,2,25.20703125)
-(2,5,25.203125)
-(2,2,24.328125)
--- a/bench_rsc_time.log
+++ b/bench_rsc_time.log
@@ -1,104 +0,0 @@
-(2,2,0.10206799999999999)
-(2,4,0.226602)
-(2,6,0.35208399999999995)
-(2,8,0.48991399999999996)
-(2,10,0.6223339999999999)
-(2,12,0.7972349999999999)
-(2,14,0.9791019999999999)
-(2,16,1.229864)
-(2,18,1.42371)
-(2,20,1.7030889999999999)
-(4,2,0.424493)
-(4,4,0.948732)
-(4,6,1.524533)
-(4,8,2.2338780000000003)
-(4,10,3.1666860000000003)
-(4,12,4.149034)
-(4,14,5.633842)
-(4,16,6.977568)
-(4,18,8.846132)
-(4,20,11.122121)
-(6,2,0.9760589999999999)
-(6,4,2.2095160000000003)
-(6,6,3.63719)
-(6,8,5.545703)
-(6,10,8.305117000000001)
-(6,12,12.908323)
-(6,14,16.631192000000002)
-(6,16,22.727736999999998)
-(6,18,28.964475)
-(6,20,41.305044)
-(8,2,1.8183259999999999)
-(8,4,4.0452580000000005)
-(8,6,7.385955)
-(8,8,12.017989)
-(8,10,19.545202999999997)
-(8,12,28.101245)
-(8,14,45.434398)
-(8,16,69.276224)
-(8,18,99.903507)
-(8,20,110.68829699999999)
-(10,2,2.848231)
-(10,4,6.889759)
-(10,6,13.220040000000001)
-(10,8,22.788176)
-(10,10,37.889131)
-(10,12,68.919195)
-(10,14,102.681356)
-(10,16,163.758086)
-(10,18,197.76342499999998)
-(10,20,357.782077)
-(12,2,4.2033190000000005)
-(12,4,9.948844000000001)
-(12,6,21.542075)
-(12,8,56.725532)
-(12,10,83.390202)
-(12,12,136.25069100000002)
-(12,14,182.037049)
-(12,16,310.45384900000005)
-(12,18,585.86348)
-(12,20,590.611234)
-(14,2,6.070988)
-(14,4,16.248022)
-(14,6,39.116524)
-(14,8,83.771567)
-(14,10,157.945492)
-(14,12,264.27400900000004)
-(14,14,420.402688)
-(14,16,648.4276659999999)
-(14,18,818.926603)
-(14,20,1075.027804)
-(16,2,7.554279)
-(16,4,22.051052)
-(16,6,57.270727)
-(16,8,124.772359)
-(16,10,307.387928)
-(16,12,428.70768999999996)
-(16,14,673.430847)
-(16,16,1045.510076)
-(16,18,1956.26349)
-(16,20,1599.524667)
-(18,2,9.503306)
-(18,4,30.206544)
-(18,6,90.633059)
-(18,8,246.21323900000002)
-(18,10,359.66055900000003)
-(18,12,697.899287)
-(18,14,1153.317865)
-(18,16,1542.826703)
-(18,18,2165.485455)
-(18,20,2998.797627)
-(20,2,12.152085)
-(20,4,39.030987)
-(20,6,174.76884800000002)
-(20,8,299.275578)
-(20,10,583.4288809999999)
-(20,12,1157.581878)
-(20,14,2155.3847960000003)
-(20,16,2369.33066)
-(20,18,3004.625029)
-(20,20,4562.804035)
-(2,2,0.101849)
-(2,2,0.10391800000000001)
-(2,5,0.281596)
-(2,2,0.102486)
--- a/bench_tr_rs_mem.log
+++ b/bench_tr_rs_mem.log
@@ -1,100 +0,0 @@
-(2,2,23.9453125)
-(2,4,24.8203125)
-(2,6,24.515625)
-(2,8,25.09375)
-(2,10,23.7421875)
-(2,12,25.21484375)
-(2,14,25.81640625)
-(2,16,27.82421875)
-(2,18,30.015625)
-(2,20,32.0078125)
-(4,2,25.140625)
-(4,4,24.69921875)
-(4,6,25.2890625)
-(4,8,27.5625)
-(4,10,31.578125)
-(4,12,37.46875)
-(4,14,42.21875)
-(4,16,54.1875)
-(4,18,61.44921875)
-(4,20,67.7890625)
-(6,2,24.8984375)
-(6,4,25.4453125)
-(6,6,28.1640625)
-(6,8,36.34765625)
-(6,10,43.6171875)
-(6,12,56.8046875)
-(6,14,67.38671875)
-(6,16,92.46484375)
-(6,18,108.9765625)
-(6,20,129.58984375)
-(8,2,24.9609375)
-(8,4,28.0078125)
-(8,6,35.3828125)
-(8,8,49.890625)
-(8,10,60.9140625)
-(8,12,86.8203125)
-(8,14,112.48046875)
-(8,16,151.6796875)
-(8,18,177.2265625)
-(8,20,218.125)
-(10,2,23.85546875)
-(10,4,29.39453125)
-(10,6,41.20703125)
-(10,8,59.6328125)
-(10,10,89.0859375)
-(10,12,117.66015625)
-(10,14,145.39453125)
-(10,16,212.546875)
-(10,18,297.9375)
-(10,20,350.8359375)
-(12,2,23.87109375)
-(12,4,34.44140625)
-(12,6,50.98828125)
-(12,8,83.39453125)
-(12,10,114.50390625)
-(12,12,161.75390625)
-(12,14,218.46484375)
-(12,16,303.609375)
-(12,18,367.1875)
-(12,20,447.86328125)
-(14,2,25.51953125)
-(14,4,38.26171875)
-(14,6,60.9453125)
-(14,8,105.02734375)
-(14,10,160.4765625)
-(14,12,211.46875)
-(14,14,320.59765625)
-(14,16,389.15625)
-(14,18,573.86328125)
-(14,20,624.078125)
-(16,2,25.9609375)
-(16,4,47.11328125)
-(16,6,78.73046875)
-(16,8,142.59375)
-(16,10,188.72265625)
-(16,12,303.9140625)
-(16,14,375.03125)
-(16,16,553.94140625)
-(16,18,632.95703125)
-(16,20,760.89453125)
-(18,2,28.70703125)
-(18,4,49.203125)
-(18,6,91.59765625)
-(18,8,154.87890625)
-(18,10,271.91796875)
-(18,12,336.89453125)
-(18,14,537.96484375)
-(18,16,622.2265625)
-(18,18,788.37109375)
-(18,20,1121.62890625)
-(20,2,29.59765625)
-(20,4,55.80078125)
-(20,6,104.4296875)
-(20,8,182.0390625)
-(20,10,309.54296875)
-(20,12,410.9140625)
-(20,14,594.96875)
-(20,16,735.25390625)
-(20,18,1119.28515625)
-(20,20,1229.5546875)
--- a/bench_tr_rs_time.log
+++ b/bench_tr_rs_time.log
@@ -1,100 +0,0 @@
-(2,2,0.054519999999999985)
-(2,4,0.354827)
-(2,6,1.1460919999999999)
-(2,8,2.5506759999999997)
-(2,10,4.934551)
-(2,12,8.64106)
-(2,14,13.283948)
-(2,16,19.427201)
-(2,18,27.376486)
-(2,20,37.196391)
-(4,2,0.20943299999999998)
-(4,4,1.431114)
-(4,6,4.613182)
-(4,8,10.435462000000001)
-(4,10,19.659764)
-(4,12,33.116163)
-(4,14,53.075277)
-(4,16,76.24887600000001)
-(4,18,110.188715)
-(4,20,148.63516)
-(6,2,0.45857499999999995)
-(6,4,3.229062)
-(6,6,10.091458)
-(6,8,22.600136000000003)
-(6,10,44.123701000000004)
-(6,12,75.34524)
-(6,14,118.401953)
-(6,16,176.291759)
-(6,18,242.856081)
-(6,20,341.841715)
-(8,2,0.7843589999999999)
-(8,4,5.65783)
-(8,6,18.102676000000002)
-(8,8,42.082593)
-(8,10,78.315806)
-(8,12,133.36523699999998)
-(8,14,217.918335)
-(8,16,318.14110999999997)
-(8,18,448.320025)
-(8,20,618.30039)
-(10,2,1.25543)
-(10,4,9.167066)
-(10,6,28.663177)
-(10,8,68.117341)
-(10,10,126.83690800000001)
-(10,12,212.455255)
-(10,14,335.466334)
-(10,16,493.86907)
-(10,18,683.6048949999999)
-(10,20,944.479912)
-(12,2,1.8368069999999999)
-(12,4,12.750900999999999)
-(12,6,40.152637000000006)
-(12,8,93.301741)
-(12,10,177.521237)
-(12,12,299.726631)
-(12,14,474.499801)
-(12,16,729.524784)
-(12,18,1012.350559)
-(12,20,1389.386652)
-(14,2,2.5006769999999996)
-(14,4,18.121582)
-(14,6,55.231598000000005)
-(14,8,127.045458)
-(14,10,241.579853)
-(14,12,415.37652799999995)
-(14,14,670.990456)
-(14,16,993.66643)
-(14,18,1365.3112219999998)
-(14,20,1904.6230409999998)
-(16,2,3.065212)
-(16,4,22.552958999999998)
-(16,6,72.880623)
-(16,8,163.69906200000003)
-(16,10,319.787701)
-(16,12,533.578319)
-(16,14,868.893421)
-(16,16,1259.9049160000002)
-(16,18,1806.458551)
-(16,20,2412.467513)
-(18,2,3.93071)
-(18,4,30.776753999999997)
-(18,6,91.87231899999999)
-(18,8,204.260635)
-(18,10,401.430704)
-(18,12,689.2725369999999)
-(18,14,1093.035868)
-(18,16,1577.999452)
-(18,18,2267.18196)
-(18,20,3034.166354)
-(20,2,4.851229999999999)
-(20,4,34.671031)
-(20,6,114.095545)
-(20,8,259.64426399999996)
-(20,10,501.79533599999996)
-(20,12,847.649677)
-(20,14,1334.1593790000002)
-(20,16,1970.551493)
-(20,18,2785.1852240000003)
-(20,20,3748.3115620000003)
--- a/colour.py
+++ b/colour.py
@@ -7,6 +7,8 @@ C_ENDC = '\033[0m'
 C_BOLD = '\033[1m'
 C_UNDERLINE = '\033[4m'

+C_MARK_INFO = C_BOLD + "[" + C_GREEN + "*" + C_ENDC + C_BOLD + "]" + C_ENDC
+
 def colour_str(col, s):
    return col + s + C_ENDC
-    
+    
--- a/rctsys.py
+++ b/rctsys.py
@@ -14,6 +14,7 @@
 #

 from sys import exit
+from colour import *

 class ContextAutomaton(object):
    
@@ -109,7 +110,7 @@ class ContextAutomaton(object):
        return s
        
    def show_transitions(self):
-        print("[*] Context automaton transitions:")
+        print(C_MARK_INFO + " Context automaton transitions:")
        for transition in self._transitions:
            str_transition = str(transition[0]) + " --( "
            str_transition += self.context2str(transition[1])
@@ -118,7 +119,7 @@ class ContextAutomaton(object):
    
    def show_states(self):
        init_state_name = self.get_init_state_name()
-        print("[*] Context automaton states:")
+        print(C_MARK_INFO + " Context automaton states:")
        for state in self._states:
            print(" - " + state, end="")
            if state == init_state_name:
@@ -130,7 +131,11 @@ class ContextAutomaton(object):
        self.show_states()
        self.show_transitions()

-
+class ExtendedContextAutomaton(ContextAutomaton):
+    """Extended Context Automaton"""
+    def __init__(self, reaction_system):
+        super(ExtendedContextAutomaton, self).__init__(reaction_system)
+        
 class ContextAutomatonWithConcentrations(ContextAutomaton):

    def __init__(self, reaction_system):
@@ -307,7 +312,7 @@ class ReactionSystem(object):
        return self.entities_ids_set_to_str(state)

    def show_reactions(self, soft=False):
-        print("[*] Reactions:")
+        print(C_MARK_INFO + " Reactions:")
        if soft and len(self.reactions) > 50:
            print(" -> there are more than 50 reactions (" + str(len(self.reactions)) + ")")
        else:
@@ -319,17 +324,17 @@ class ReactionSystem(object):
                                                            " { " + self.state_to_str(reaction[2]) + " }"))

    def show_background_set(self):
-        print("[*] Background set: {" + self.entities_names_set_to_str(self.background_set) + "}")
+        print(C_MARK_INFO + " Background set: {" + self.entities_names_set_to_str(self.background_set) + "}")

    def show_initial_contexts(self):
        if len(self.init_contexts) > 0:
-            print("[*] Initial context sets:")
+            print(C_MARK_INFO + " Initial context sets:")
            for ctx in self.init_contexts:
                  print(" - {" + self.entities_ids_set_to_str(ctx) + "}")

    def show_context_entities(self):
        if len(self.context_entities) > 0:
-            print("[*] Context entities: " + self.entities_ids_set_to_str(self.context_entities))
+            print(C_MARK_INFO + " Context entities: " + self.entities_ids_set_to_str(self.context_entities))

    def show(self, soft=False):

@@ -540,10 +545,10 @@ class ReactionSystemWithConcentrations(ReactionSystem):
        return s        

    def show_background_set(self):
-        print("[*] Background set: {" + self.entities_names_set_to_str(self.background_set) + "}")
+        print(C_MARK_INFO + " Background set: {" + self.entities_names_set_to_str(self.background_set) + "}")

    def show_meta_reactions(self):
-        print("[*] Meta reactions:")
+        print(C_MARK_INFO + " Meta reactions:")
        for param_ent,reactions in self.meta_reactions.items():
            for r_type,command,reactants,inhibitors in reactions:
                if r_type == "inc" or r_type == "dec":
@@ -553,12 +558,12 @@ class ReactionSystemWithConcentrations(ReactionSystem):
                    raise RuntimeError("Unknown meta-reaction type: " + repr(r_type))

    def show_max_concentrations(self):
-        print("[*] Maximal allowed concentration levels (for optimized translation to RS):")
+        print(C_MARK_INFO + " Maximal allowed concentration levels (for optimized translation to RS):")
        for e,max_conc in self.max_conc_per_ent.items():
            print(" - {0:^20} = {1:<6}".format(self.get_entity_name(e),max_conc))

    def show_permanent_entities(self):
-        print("[*] Permanent entities:")
+        print(C_MARK_INFO + " Permanent entities:")
        for e,inhibitors in self.permanent_entities.items():
            print(" - {0:^20}{1:<6}".format(self.get_entity_name(e) + ": ","I={" + self.state_to_str(inhibitors) + "}"))

--- a/rssmt.py
+++ b/rssmt.py
@@ -14,17 +14,23 @@ from smtcheckerrsc          import SmtCheckerRSC
 import sys
 import rs_examples

+from colour import *
+
 import resource

 profiling = False

 version = "2016/02/21/00"
-rsmc_banner = """
- *** Reaction Systems SMT-Based Model Checking
+rsmc_banner = """Reaction Systems SMT-Based Model Checking

- *** Version: """ + version + """
- *** Author:  Artur Męski <meski@ipipan.waw.pl> / <artur.meski@ncl.ac.uk>
-"""
+Version: """ + version + """
+Author:  Artur Męski <meski@ipipan.waw.pl> / <artur.meski@ncl.ac.uk>"""
+
+def print_banner():
+    print()
+    for line in rsmc_banner.split("\n"):
+        print(colour_str(C_GREEN, " " + 3*"-" + " "), line)
+    print()

 def process():
    
@@ -36,10 +42,14 @@ def process():

 def main():
            
-    print(rsmc_banner)
+    print_banner()

-    process()
+    # process()
+    r = ReactionSystem()
+    c = ExtendedContextAutomaton(r)
+    rc = ReactionSystemWithAutomaton(r,c)

+    rc.show()
    
 if __name__ == "__main__":
    try: