From ef6f2edd33aa40eb693b12536b195ea031b93f12 Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Sun, 28 Feb 2016 20:12:43 +0100 Subject: [PATCH] Incrementation & decrementation by a specified value. --- mkplotdat.sh | 8 +++ rctsys.py | 155 +++++++++++++++++++++++++++++------------------ rs_examples.py | 17 +++--- rssmt.py | 2 +- smtcheckerrsc.py | 56 +++++++++++++---- 5 files changed, 161 insertions(+), 77 deletions(-) create mode 100755 mkplotdat.sh diff --git a/mkplotdat.sh b/mkplotdat.sh new file mode 100755 index 0000000..5eb1fef --- /dev/null +++ b/mkplotdat.sh @@ -0,0 +1,8 @@ +#!/bin/sh +if [ "$1" = "" ];then + echo "Usage: $0 " + exit 1 +fi +f="$1" +cat $f | tr -d '()' | tr ',' '\t' + diff --git a/rctsys.py b/rctsys.py index d35ed32..9c024a7 100755 --- a/rctsys.py +++ b/rctsys.py @@ -185,7 +185,7 @@ class ContextAutomatonWithConcentrations(ContextAutomaton): for ent,conc in ctx: for i in range(1,conc+1): - n = self._reaction_system.get_entity_name(ent) + "_" + str(i) + n = self._reaction_system.get_entity_name(ent) + "#" + str(i) ca._reaction_system.ensure_bg_set_entity(n) new_ctx.add(n) @@ -207,19 +207,21 @@ class ReactionSystem(object): self.init_contexts = [] self.context_entities = [] - def add_bg_set_entity(self, name): - if not self.is_in_background_set(name): - self.background_set.append(name) - else: + def assume_not_in_bgset(self, name): + if self.is_in_background_set(name): raise RuntimeError("The entity " + name + " is already on the list") + + def add_bg_set_entity(self, name): + self.assume_not_in_bgset(name) + self.background_set.append(name) def ensure_bg_set_entity(self, name): if not self.is_in_background_set(name): self.background_set.append(name) - def add_bg_set_entities(self, names): - for name in names: - self.add_bg_set_entity(name) + def add_bg_set_entities(self, elements): + for e in elements: + self.add_bg_set_entity(e) def is_in_background_set(self, entity): """Checks if the given name is valid wrt the background set=""" @@ -250,7 +252,7 @@ class ReactionSystem(object): """Adds a reaction""" if R == [] or P == []: - raise RuntimeError("No reactants of products defined") + raise RuntimeError("No reactants or products defined") reactants = [] for entity in R: @@ -380,6 +382,28 @@ class ReactionSystemWithConcentrations(ReactionSystem): self.reactions_by_prod = None self.max_concentration = 0 + self.max_conc_per_ent = dict() + + def add_bg_set_entity(self, e): + name = "" + def_max_conc = -1 + if type(e) is tuple and len(e) == 2: + name,def_max_conc = e + elif type(e) is str: + name = e + else: + raise RuntimeError("Bad entity type when adding background set element") + + self.assume_not_in_bgset(name) + self.background_set.append(name) + + if def_max_conc != -1: + ent_id = self.get_entity_id(name) + self.max_conc_per_ent.setdefault(ent_id, 0) + if self.max_conc_per_ent[ent_id] < def_max_conc: + self.max_conc_per_ent[ent_id] = def_max_conc + if self.max_concentration < def_max_conc: + self.max_concentration = def_max_conc def is_valid_entity_with_concentration(self, e): """Sanity check for entities with concentration""" @@ -406,7 +430,7 @@ class ReactionSystemWithConcentrations(ReactionSystem): if elem[1] < 1: raise RuntimeError("Unexpected concentration level in state: " + str(elem)) - def process_rip(self, R, I, P): + def check_rip(self, R, I, P): """Chcecks concentration levels and converts entities names into their ids""" if R == []: @@ -442,24 +466,24 @@ class ReactionSystemWithConcentrations(ReactionSystem): if P == []: raise RuntimeError("No products defined") - reaction = self.process_rip(R,I,P) + reaction = self.check_rip(R,I,P) self.reactions.append(reaction) - def add_reaction_inc(self, incr_entity, R, I): + def add_reaction_inc(self, incr_entity, incrementer, R, I): """Adds a macro/meta reaction for increasing the value of incr_entity""" - reactants,inhibitors,products = self.process_rip(R,I,[]) + reactants,inhibitors,products = self.check_rip(R,I,[]) incr_entity_id = self.get_entity_id(incr_entity) self.meta_reactions.setdefault(incr_entity_id,[]) - self.meta_reactions[incr_entity_id].append(("inc", reactants, inhibitors)) + self.meta_reactions[incr_entity_id].append(("inc", self.get_entity_id(incrementer), reactants, inhibitors)) - def add_reaction_dec(self, incr_entity, R, I): + def add_reaction_dec(self, decr_entity, decrementer, R, I): """Adds a macro/meta reaction for decreasing the value of incr_entity""" - reactants,inhibitors,products = self.process_rip(R,I,[]) + reactants,inhibitors,products = self.check_rip(R,I,[]) decr_entity_id = self.get_entity_id(decr_entity) self.meta_reactions.setdefault(decr_entity_id,[]) - self.meta_reactions[decr_entity_id].append(("dec", reactants, inhibitors)) + self.meta_reactions[decr_entity_id].append(("dec", self.get_entity_id(decrementer), reactants, inhibitors)) def set_context_entities(self, entities): raise NotImplementedError @@ -491,10 +515,10 @@ class ReactionSystemWithConcentrations(ReactionSystem): def show_meta_reactions(self): print("[*] Meta reactions:") for param_ent,reactions in self.meta_reactions.items(): - for r_type,reactants,inhibitors in reactions: + for r_type,command,reactants,inhibitors in reactions: if r_type == "inc" or r_type == "dec": - print("\t - [ Type=" + repr(r_type) + " Parameter=( " + self.get_entity_name(param_ent) + \ - " ) ] -- ( R={" + self.state_to_str(reactants) + "}, \tI={" + self.state_to_str(inhibitors) + "} )") + 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) + "} )") else: raise RuntimeError("Unknown meta-reaction type: " + repr(r_type)) @@ -543,72 +567,87 @@ class ReactionSystemWithConcentrations(ReactionSystem): new_products = [] for ent,conc in reactants: - n = self.get_entity_name(ent) + "_" + str(conc) + n = self.get_entity_name(ent) + "#" + str(conc) rs.ensure_bg_set_entity(n) new_reactants.append(n) for ent,conc in inhibitors: - n = self.get_entity_name(ent) + "_" + str(conc) + n = self.get_entity_name(ent) + "#" + str(conc) rs.ensure_bg_set_entity(n) new_inhibitors.append(n) for ent,conc in products: for i in range(1,conc+1): - n = self.get_entity_name(ent) + "_" + str(i) + n = self.get_entity_name(ent) + "#" + str(i) rs.ensure_bg_set_entity(n) new_products.append(n) rs.add_reaction(new_reactants,new_inhibitors,new_products) for param_ent,reactions in self.meta_reactions.items(): - for r_type,reactants,inhibitors in reactions: + for r_type,command,reactants,inhibitors in reactions: param_ent_name = self.get_entity_name(param_ent) new_reactants = [] new_inhibitors = [] - + for ent,conc in reactants: - n = self.get_entity_name(ent) + "_" + str(conc) + n = self.get_entity_name(ent) + "#" + str(conc) rs.ensure_bg_set_entity(n) new_reactants.append(n) - + for ent,conc in inhibitors: - n = self.get_entity_name(ent) + "_" + str(conc) + n = self.get_entity_name(ent) + "#" + str(conc) rs.ensure_bg_set_entity(n) new_inhibitors.append(n) - - if r_type == "inc": - - # pre_conc -- predecessor concentration - # succ_conc -- successor concentration concentration - - for i in range(1,self.max_concentration): - pre_conc = param_ent_name + "_" + str(i) - rs.ensure_bg_set_entity(pre_conc) - new_products = [] - succ_value = i+1 - for j in range(1,succ_value+1): - new_p = param_ent_name + "_" + str(j) - rs.ensure_bg_set_entity(new_p) - new_products.append(new_p) - rs.add_reaction(new_reactants + [pre_conc], new_inhibitors, new_products) - elif r_type == "dec": - - for i in range(1,self.max_concentration): - pre_conc = param_ent_name + "_" + str(i+1) - rs.ensure_bg_set_entity(pre_conc) - new_products = [] - succ_value = i - for j in range(1,succ_value+1): - new_p = param_ent_name + "_" + str(j) - rs.ensure_bg_set_entity(new_p) - new_products.append(new_p) - rs.add_reaction(new_reactants + [pre_conc], new_inhibitors, new_products) - + max_cmd_c = self.max_concentration + if command in self.max_conc_per_ent: + max_cmd_c = self.max_conc_per_ent[command] else: - raise RuntimeError("Unknown meta-reaction type: " + repr(r_type)) + print("WARNING:\n\tThere is no maximal concentration level defined for " + self.get_entity_name(command)) + print("\tThis is a very bad idea -- expect degraded performance\n") + + for l in range(1,max_cmd_c+1): + + cmd_ent = self.get_entity_name(command) + "#" + str(l) + rs.ensure_bg_set_entity(cmd_ent) + + if r_type == "inc": + + # pre_conc -- predecessor concentration + # succ_conc -- successor concentration concentration + + for i in range(1,self.max_concentration): + pre_conc = param_ent_name + "#" + str(i) + rs.ensure_bg_set_entity(pre_conc) + new_products = [] + succ_value = i+l + for j in range(1,succ_value+1): + if j > self.max_concentration: break + new_p = param_ent_name + "#" + str(j) + rs.ensure_bg_set_entity(new_p) + new_products.append(new_p) + if new_products != []: + rs.add_reaction(set(new_reactants + [pre_conc,cmd_ent]), set(new_inhibitors), set(new_products)) + + elif r_type == "dec": + for i in range(1,self.max_concentration+1): + pre_conc = param_ent_name + "#" + str(i) + rs.ensure_bg_set_entity(pre_conc) + new_products = [] + succ_value = i-l + for j in range(1,succ_value+1): + if j > self.max_concentration: break + new_p = param_ent_name + "#" + str(j) + rs.ensure_bg_set_entity(new_p) + new_products.append(new_p) + if new_products != []: + rs.add_reaction(set(new_reactants + [pre_conc,cmd_ent]), set(new_inhibitors), set(new_products)) + + else: + raise RuntimeError("Unknown meta-reaction type: " + repr(r_type)) return rs diff --git a/rs_examples.py b/rs_examples.py index 5a9df50..fdcb52a 100755 --- a/rs_examples.py +++ b/rs_examples.py @@ -323,15 +323,16 @@ def chain_reaction(print_system=False): exit(1) r = ReactionSystemWithConcentrations() - r.add_bg_set_entity("inc") - r.add_bg_set_entity("dec") + 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)) for i in range(1,chainLen+1): ent = "e_" + str(i) - r.add_reaction_inc(ent, [(ent, 1),("inc",1)],[(ent,maxConc)]) + 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)]) @@ -350,15 +351,17 @@ def chain_reaction(print_system=False): if verify_rsc: smt_rsc = SmtCheckerRSC(rc) - smt_rsc.check_reachability([('e_'+str(chainLen),maxConc)],max_level=maxConc*chainLen+10) - # smt_rsc.show_encoding([('e_'+str(1),1)],print_time=True,max_level=maxConc*chainLen+10) + prop = [('e_'+str(chainLen),maxConc)] + smt_rsc.check_reachability(prop,max_level=maxConc*chainLen+10) + # smt_rsc.show_encoding(prop,print_time=True,max_level=maxConc*chainLen+10) - if not verify_rsc: + else: orc = rc.get_ordinary_reaction_system_with_automaton() if print_system: + print("\nTranslated:") orc.show() smt_tr_rs = SmtCheckerPGRS(orc) - smt_tr_rs.check_reachability(['e_'+str(chainLen)+"_"+str(maxConc)]) + smt_tr_rs.check_reachability(['e_'+str(chainLen)+"#"+str(maxConc)]) # print("Reaction System with Concentrations:", smt_rsc.get_verification_time()) # print("Reaction System from translating RSC:", smt_tr_rs.get_verification_time()) diff --git a/rssmt.py b/rssmt.py index 3250a08..00a1b2b 100755 --- a/rssmt.py +++ b/rssmt.py @@ -29,7 +29,7 @@ rsmc_banner = """ def process(): # rs_examples.run_counter_exp() - rs_examples.chain_reaction() + rs_examples.chain_reaction(print_system=True) ################################################################## diff --git a/smtcheckerrsc.py b/smtcheckerrsc.py index 91e19e9..905a10b 100644 --- a/smtcheckerrsc.py +++ b/smtcheckerrsc.py @@ -8,8 +8,8 @@ from sys import stdout from itertools import chain import resource -# def simplify(x): -# return x +def simplify(x): + return x class SmtCheckerRSC(object): @@ -114,26 +114,59 @@ class SmtCheckerRSC(object): # -------- meta reactions --------------------------------------------------- - for r_type,reactants,inhibitors in meta_reactions: + for r_type,command_entity,reactants,inhibitors in meta_reactions: + + # command entity is e.g. 'inc' for incrementation operation + # (inc,W) gives us the value W by which the given entity's value should be incremented enc_reactants = True enc_inhibitors = True for reactant,concentration in reactants: - enc_reactants = simplify(And(enc_reactants, + enc_reactants = simplify(And(enc_reactants, Or(self.v[level][reactant] >= concentration, self.v_ctx[level][reactant] >= concentration))) + + # command entity needs to be present (with concentration level > 0) in order to perform the operation + enc_reactants = simplify(And(enc_reactants, + Or(self.v[level][command_entity] > 0, self.v_ctx[level][command_entity] > 0))) + for inhibitor,concentration in inhibitors: enc_inhibitors = simplify(And(enc_inhibitors, And(self.v[level][inhibitor] < concentration, self.v_ctx[level][inhibitor] < concentration))) - if r_type == "inc": - - enc_products = self.v[level+1][prod_entity] == self.v[level][prod_entity]+1 + # 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 - elif r_type == "dec": + if r_type == "inc": + enc_products = 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]) + \ + If(self.v[level][command_entity]>self.v_ctx[level][command_entity],self.v[level][command_entity],self.v_ctx[level][command_entity]) + + elif r_type == "dec": + enc_products = 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]) - \ + If(self.v[level][command_entity]>self.v_ctx[level][command_entity],self.v[level][command_entity],self.v_ctx[level][command_entity]) - enc_products = self.v[level+1][prod_entity] == self.v[level][prod_entity]-1 - else: raise RuntimeError("Unknown meta-reaction type: " + repr(r_type)) @@ -355,7 +388,8 @@ class SmtCheckerRSC(object): self.solver.push() s = self.enc_min_state(current_level,state) - print(s) + print("Test: ", s) + self.solver.add(s) result = self.solver.check()