From 56218a3596d4d874be1c5986f0b68c097e32dcab Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Tue, 27 Dec 2016 20:57:02 +0100 Subject: [PATCH] some cleanup --- bench_rsc_mem.log | 104 ------------------------------------------- bench_rsc_time.log | 104 ------------------------------------------- bench_tr_rs_mem.log | 100 ----------------------------------------- bench_tr_rs_time.log | 100 ----------------------------------------- colour.py | 4 +- rctsys.py | 27 ++++++----- rssmt.py | 24 +++++++--- 7 files changed, 36 insertions(+), 427 deletions(-) delete mode 100644 bench_rsc_mem.log delete mode 100644 bench_rsc_time.log delete mode 100644 bench_tr_rs_mem.log delete mode 100644 bench_tr_rs_time.log diff --git a/bench_rsc_mem.log b/bench_rsc_mem.log deleted file mode 100644 index edd898e..0000000 --- a/bench_rsc_mem.log +++ /dev/null @@ -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) diff --git a/bench_rsc_time.log b/bench_rsc_time.log deleted file mode 100644 index 0e02087..0000000 --- a/bench_rsc_time.log +++ /dev/null @@ -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) diff --git a/bench_tr_rs_mem.log b/bench_tr_rs_mem.log deleted file mode 100644 index 8afe7ed..0000000 --- a/bench_tr_rs_mem.log +++ /dev/null @@ -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) diff --git a/bench_tr_rs_time.log b/bench_tr_rs_time.log deleted file mode 100644 index 5ac36e9..0000000 --- a/bench_tr_rs_time.log +++ /dev/null @@ -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) diff --git a/colour.py b/colour.py index 4bee4fb..3020021 100644 --- 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 - \ No newline at end of file + diff --git a/rctsys.py b/rctsys.py index 8a494b4..c1e190c 100755 --- 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) + "}")) diff --git a/rssmt.py b/rssmt.py index 25d323d..eaa8f75 100755 --- 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 / -""" +Version: """ + version + """ +Author: Artur Męski / """ + +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: