diff --git a/rctsys.py b/rctsys.py index 1b1dd0f..cd26164 100755 --- a/rctsys.py +++ b/rctsys.py @@ -114,13 +114,13 @@ class ContextAutomaton(object): str_transition = str(transition[0]) + " --( " str_transition += self.context2str(transition[1]) str_transition += " )--> " + str(transition[2]) - print("\t- " + str_transition) + print(" - " + str_transition) def show_states(self): init_state_name = self.get_init_state_name() print("[*] Context automaton states:") for state in self._states: - print("\t- " + state, end="") + print(" - " + state, end="") if state == init_state_name: print(" [init]") else: @@ -309,10 +309,14 @@ class ReactionSystem(object): def show_reactions(self, soft=False): print("[*] Reactions:") if soft and len(self.reactions) > 50: - print("\t -> there are more than 50 reactions (" + str(len(self.reactions)) + ")") + print(" -> there are more than 50 reactions (" + str(len(self.reactions)) + ")") else: + print(" "*4 + "{0: ^35}{1: ^25}{2: ^15}".format("reactants"," inhibitors"," products")) for reaction in self.reactions: - print("\t - ( R={" + self.state_to_str(reaction[0]) + "}, \tI={" + self.state_to_str(reaction[1]) + "}, \tP={" + self.state_to_str(reaction[2]) + "} )") + # print("\t( R={" + self.state_to_str(reaction[0]) + "}, I={" + self.state_to_str(reaction[1]) + "}, P={" + self.state_to_str(reaction[2]) + "} )") + print(" "*2 + "- {0: ^35}{1: ^25}{2: ^15}".format("{ " + self.state_to_str(reaction[0]) + " }", + " { " + self.state_to_str(reaction[1]) + " }", + " { " + self.state_to_str(reaction[2]) + " }")) def show_background_set(self): print("[*] Background set: {" + self.entities_names_set_to_str(self.background_set) + "}") @@ -321,7 +325,7 @@ class ReactionSystem(object): if len(self.init_contexts) > 0: print("[*] Initial context sets:") for ctx in self.init_contexts: - print("\t - {" + self.entities_ids_set_to_str(ctx) + "}") + print(" - {" + self.entities_ids_set_to_str(ctx) + "}") def show_context_entities(self): if len(self.context_entities) > 0: @@ -523,7 +527,7 @@ class ReactionSystemWithConcentrations(ReactionSystem): def state_to_str(self, state): s = "" for ent,level in state: - s += str((self.get_entity_name(ent),level)) + ", " + s += self.get_entity_name(ent) + "=" + str(level) + ", " s = s[:-2] return s @@ -535,20 +539,20 @@ class ReactionSystemWithConcentrations(ReactionSystem): 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": - print("\t - [ Type=" + repr(r_type) + " Operand=( " + self.get_entity_name(param_ent) + \ - " ) Command=( " + self.get_entity_name(command) + " ) ] -- ( R={" + self.state_to_str(reactants) + "}, \tI={" + self.state_to_str(inhibitors) + "} )") + print(" - [ Type=" + repr(r_type) + " Operand=( " + self.get_entity_name(param_ent) + \ + " ) Command=( " + self.get_entity_name(command) + " ) ] -- ( R={" + self.state_to_str(reactants) + "}, I={" + self.state_to_str(inhibitors) + "} )") else: raise RuntimeError("Unknown meta-reaction type: " + repr(r_type)) def show_max_concentrations(self): print("[*] Maximal allowed concentration levels (for optimized translation to RS):") for e,max_conc in self.max_conc_per_ent.items(): - print("\t - {0:>20} = {1:<6}".format(self.get_entity_name(e),max_conc)) + print(" - {0:^20} = {1:<6}".format(self.get_entity_name(e),max_conc)) def show_permanent_entities(self): print("[*] Permanent entities:") for e,inhibitors in self.permanent_entities.items(): - print("\t - {0:>20}: {1:<6}".format(self.get_entity_name(e),"I={" + self.state_to_str(inhibitors) + "}")) + print(" - {0:^20}{1:<6}".format(self.get_entity_name(e) + ": ","I={" + self.state_to_str(inhibitors) + "}")) def show(self, soft=False): self.show_background_set() diff --git a/smtcheckerrsc.py b/smtcheckerrsc.py index 25bd329..92c18dc 100644 --- a/smtcheckerrsc.py +++ b/smtcheckerrsc.py @@ -7,6 +7,7 @@ from time import time from sys import stdout from itertools import chain import resource +from colour import * # def simplify(x): # return x @@ -138,29 +139,6 @@ class SmtCheckerRSC(object): enc_inhibitors = simplify(And(enc_inhibitors, And(self.v[level][inhibitor] < concentration, self.v_ctx[level][inhibitor] < concentration))) - # if r_type == "inc": - # # depending on if the value of the command entity is greater in the context or in the current RS state - # # we choose to increment by the greater value from v or v_ctx (this is because we take the max value). - # enc_products = Or( - # And(self.v_ctx[level][command_entity] >= self.v[level][command_entity], - # self.v[level+1][prod_entity] == If(self.v[level][command_entity]>self.v_ctx[level][command_entity],self.v[level][command_entity],self.v_ctx[level][command_entity])+self.v_ctx[level][command_entity]), - # And(self.v[level][command_entity] > self.v_ctx[level][command_entity], - # self.v[level+1][prod_entity] == If(self.v[level][prod_entity]>self.v_ctx[level][command_entity],self.v[level][prod_entity],self.v_ctx[level][prod_entity])+self.v[level][command_entity])) - # - # elif r_type == "dec": - # # same happens here, but we decrement with the maximum value encoded at v or v_ctx. - # enc_products = Or( - # And(self.v_ctx[level][command_entity] >= self.v[level][command_entity], - # self.v[level+1][prod_entity] == If(self.v[level][prod_entity]>self.v_ctx[level][command_entity],self.v[level][prod_entity],self.v_ctx[level][prod_entity])-self.v_ctx[level][command_entity]), - # And(self.v[level][command_entity] > self.v_ctx[level][command_entity], - # self.v[level+1][prod_entity] == If(self.v[level][prod_entity]>self.v_ctx[level][command_entity],self.v[level][prod_entity],self.v_ctx[level][prod_entity])-self.v[level][command_entity])) - # - # if r_type == "inc": - # enc_products = self.v[level+1][prod_entity] == self.v[level][prod_entity]+1 - # - # elif r_type == "dec": - # enc_products = self.v[level+1][prod_entity] == self.v[level][prod_entity]-1 - if r_type == "inc": enc_products = simplify(self.v[level+1][prod_entity] == \ If(self.v[level][prod_entity]>self.v_ctx[level][prod_entity],self.v[level][prod_entity],self.v_ctx[level][prod_entity]) + \ @@ -321,7 +299,7 @@ class SmtCheckerRSC(object): for level in range(max_level+1): - print("\n{:-^70}".format("[ level=" + repr(level) + " ]")) + print("\n{: >70}".format("[ level=" + repr(level) + " ]")) print(" State: {", end=""), for var_id in range(len(self.v[level])): @@ -365,24 +343,25 @@ class SmtCheckerRSC(object): stdout.flush() # reachability test: - print("[i] Adding the reachability test...") + print("[" + colour_str(C_BOLD, "i") + "] Adding the reachability test...") self.solver.push() self.solver.add(self.enc_state_with_blocking(current_level,state)) result = self.solver.check() if result == sat: - print("\n[+] SAT at level=" + str(current_level)) + print("[" + colour_str(C_BOLD, "+") + "] " + colour_str(C_GREEN, "SAT at level=" + str(current_level))) if print_witness: + print("\n{:=^70}".format("[ WITNESS ]")) self.decode_witness(current_level) break else: self.solver.pop() - print("[i] Unrolling the transition relation") + print("[" + colour_str(C_BOLD, "i") + "] Unrolling the transition relation") self.solver.add(self.enc_transition_relation(current_level)) - print("\n{:-^70}".format("[ level=" + str(current_level) + " done ]")) + print("{:->70}".format("[ level=" + str(current_level) + " done ]")) current_level += 1 if current_level > max_level: @@ -394,10 +373,10 @@ class SmtCheckerRSC(object): stop = resource.getrusage(resource.RUSAGE_SELF).ru_utime self.verification_time = stop-start print() - print("\n[i] {:_>60}".format(" Time: " + repr(self.verification_time) + " s")) + print("\n[i] {: >60}".format(" Time: " + repr(self.verification_time) + " s")) if print_mem: - print("[i] {:_>60}".format(" Memory: " + repr(resource.getrusage(resource.RUSAGE_SELF).ru_maxrss/(1024*1024)) + " MB")) + print("[i] {: >60}".format(" Memory: " + repr(resource.getrusage(resource.RUSAGE_SELF).ru_maxrss/(1024*1024)) + " MB")) def get_verification_time(self): return self.verification_time @@ -431,7 +410,7 @@ class SmtCheckerRSC(object): result = self.solver.check() if result == sat: - print("\n[+] SAT at level=" + str(current_level)) + print("\n[+] " + colour_str(C_RED, "SAT at level=" + str(current_level))) if print_witness: self.decode_witness(current_level) break