diff --git a/logics/bags.py b/logics/bags.py index b69d694..fd386e7 100644 --- a/logics/bags.py +++ b/logics/bags.py @@ -19,11 +19,11 @@ class BagDescription(object): if self.f_type == BagDesc_oper.true: return "TRUE" if self.f_type == BagDesc_oper.l_and: - return "( " + repr(self.left_operand) + " & " + repr(self.right_operand) + " )" + return "(" + repr(self.left_operand) + " & " + repr(self.right_operand) + ")" if self.f_type == BagDesc_oper.l_or: - return "( " + repr(self.left_operand) + " | " + repr(self.right_operand) + " )" + return "(" + repr(self.left_operand) + " | " + repr(self.right_operand) + ")" if self.f_type == BagDesc_oper.l_not: - return "~" + repr(self.left_operand) + return "~(" + repr(self.left_operand) + ")" if self.f_type == BagDesc_oper.lt: return repr(self.left_operand) + " < " + repr(self.right_operand) if self.f_type == BagDesc_oper.le: @@ -37,14 +37,14 @@ class BagDescription(object): def sanity_check(self): """Sanity checks""" - for operand in (self.left_operand, self.right_operand): if operand: if not( isinstance(operand, BagDescription) or isinstance(operand, int)): raise RuntimeError( - "Unexpected operand type for a bag: " + str(operand)) + "Unexpected operand type for a bag: {:s} (type: {:s})".format( + str(operand), str(type(operand)))) @classmethod def f_entity(cls, entity_name): @@ -54,6 +54,14 @@ class BagDescription(object): def f_TRUE(cls): return cls(BagDesc_oper.true) + @classmethod + def f_And(cls, arg_L, arg_R): + return cls(BagDesc_oper.l_and, L_oper=arg_L, R_oper=arg_R) + + @classmethod + def f_Not(cls, arg): + return cls(BagDesc_oper.l_not, L_oper=arg) + def __lt__(self, other): return BagDescription(BagDesc_oper.lt, L_oper=self, R_oper=other) diff --git a/logics/rsltl.py b/logics/rsltl.py index 83d61d1..91fdcc1 100644 --- a/logics/rsltl.py +++ b/logics/rsltl.py @@ -18,6 +18,7 @@ class Formula_rsLTL(object): self.sub_operand = sub_oper self.bag_descr = bag + # it's silly, but it's a frequent mistake if callable(sub_oper): raise RuntimeError( "sub_oper should not be a function. Missing () for {0}?".format(sub_oper)) @@ -26,34 +27,37 @@ class Formula_rsLTL(object): self.left_operand = Formula_rsLTL.f_bag(self.left_operand) if isinstance(self.right_operand, BagDescription): self.right_operand = Formula_rsLTL.f_bag(self.right_operand) + + if self.sub_operand is True: + self.sub_operand = BagDescription.f_TRUE() def __repr__(self): if self.f_type == rsLTL_form_type.bag: return repr(self.bag_descr) if self.f_type == rsLTL_form_type.l_not: - return "~( " + repr(self.left_operand) + " )" + return "~(" + repr(self.left_operand) + ")" if self.f_type == rsLTL_form_type.t_globally: - return "G[" + repr(self.sub_operand) + "]( " + repr(self.left_operand) + " )" + return "G[" + repr(self.sub_operand) + "](" + repr(self.left_operand) + ")" if self.f_type == rsLTL_form_type.t_finally: - return "F[" + repr(self.sub_operand) + "]( " + repr(self.left_operand) + " )" + return "F[" + repr(self.sub_operand) + "](" + repr(self.left_operand) + ")" if self.f_type == rsLTL_form_type.t_next: - return "X[" + repr(self.sub_operand) + "]( " + repr(self.left_operand) + " )" + return "X[" + repr(self.sub_operand) + "](" + repr(self.left_operand) + ")" if self.f_type == rsLTL_form_type.l_and: - return "( " + repr(self.left_operand) + " & " + repr(self.right_operand) + " )" + return "(" + repr(self.left_operand) + " & " + repr(self.right_operand) + ")" if self.f_type == rsLTL_form_type.l_or: - return "( " + repr(self.left_operand) + " | " + repr(self.right_operand) + " )" + return "(" + repr(self.left_operand) + " | " + repr(self.right_operand) + ")" if self.f_type == rsLTL_form_type.l_implies: - return "( " + repr(self.left_operand) + " => " + repr(self.right_operand) + " )" + return "(" + repr(self.left_operand) + " => " + repr(self.right_operand) + ")" if self.f_type == rsLTL_form_type.t_until: - return "( " + repr( + return "(" + repr( self.left_operand) + " U[" + repr( self.sub_operand) + "] " + repr( - self.right_operand) + " )" + self.right_operand) + ")" if self.f_type == rsLTL_form_type.t_release: - return "( " + repr( + return "(" + repr( self.left_operand) + " R[" + repr( self.sub_operand) + "] " + repr( - self.right_operand) + " )" + self.right_operand) + ")" @property def is_bag(self): @@ -63,6 +67,10 @@ class Formula_rsLTL(object): def f_bag(cls, bag_descr): return cls(rsLTL_form_type.bag, bag=bag_descr) + @classmethod + def f_Not(cls, arg): + return cls(rsLTL_form_type.l_not, L_oper=arg) + @classmethod def f_And(cls, arg_L, arg_R): return cls(rsLTL_form_type.l_and, L_oper=arg_L, R_oper=arg_R) diff --git a/logics/rsltl_encoder.py b/logics/rsltl_encoder.py index c1f61e7..222535c 100644 --- a/logics/rsltl_encoder.py +++ b/logics/rsltl_encoder.py @@ -120,12 +120,18 @@ class rsLTL_Encoder(object): if bag_formula.f_type == BagDesc_oper.gt: return self.encode_bag(bag_formula.left_operand, level, context) > int(bag_formula.right_operand) + + assert False, "Unsupported case {:s}".format(bag_formula.f_type) def encode_bag_state(self, bag_formula, level): - return self.encode_bag(bag_formula, level) + res = self.encode_bag(bag_formula, level) + assert res is not None + return res def encode_bag_ctx(self, bag_formula, level): - return self.encode_bag(bag_formula, level, context=True) + res = self.encode_bag(bag_formula, level, context=True) + assert res is not None + return res def encode(self, formula, level, bound): @@ -167,7 +173,7 @@ class rsLTL_Encoder(object): elif formula.f_type == rsLTL_form_type.l_implies: enc = Implies( - self.encode(formula.left_operand, level, bound), + self.encode(formula.left_operand, level, bound), self.encode(formula.right_operand, level, bound) ) diff --git a/rs/reaction_system_with_concentrations_param.py b/rs/reaction_system_with_concentrations_param.py index 38dcf11..4ed6726 100644 --- a/rs/reaction_system_with_concentrations_param.py +++ b/rs/reaction_system_with_concentrations_param.py @@ -23,7 +23,6 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem): self.reactions = [] self.parameters = dict() - # self.parametric_reactions = [] self.meta_reactions = dict() self.permanent_entities = dict() self.background_set = [] @@ -91,8 +90,7 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem): if len(e) == 2 and type(e[1]) is int: return True - print("FATAL. Invalid entity+concentration:") - print(e) + print("FATAL. Invalid entity+concentration: {:s}".format(e)) exit(1) return False diff --git a/rs_testing.py b/rs_testing.py index 05586bc..5d0e34b 100644 --- a/rs_testing.py +++ b/rs_testing.py @@ -41,10 +41,21 @@ def gene_expression(cmd_args): r.add_bg_set_entity(("h", 1)) r.add_bg_set_entity(("Q", 1)) r.add_bg_set_entity(("U", 1)) + + all_entities = set(r.background_set) r.add_reaction([("x",1)],[("h",1)],[("x",1)]) - r.add_reaction([("x",1)],[("h",1)],[("xp",1)]) - r.add_reaction([("x",1),("xp",1)],[("h",1)],[("X",1)]) + + # r.add_reaction([("x",1)],[("h",1)],[("xp",1)]) + param_p1 = r.get_param("P1") + r.add_reaction(param_p1,[("h",1)],[("xp",1)]) + + # r.add_reaction([("x",1),("xp",1)],[("h",1)],[("X",1)]) + param_p2_r = r.get_param("P2_r") + param_p2_i = r.get_param("P2_i") + param_p2_p = r.get_param("P2_p") + r.add_reaction(param_p2_r,param_p2_i,param_p2_p) + r.add_reaction([("y",1)],[("h",1)],[("y",1)]) r.add_reaction([("y",1)],[("Q",1)],[("yp",1)]) r.add_reaction([("y",1),("yp",1)],[("h",1)],[("Y",1)]) @@ -66,6 +77,22 @@ def gene_expression(cmd_args): rc = ReactionSystemWithAutomaton(r, c) rc.show() + f_x1 = ltl_G(True, ltl_Implies( + exact_state(["x"], all_entities), + ltl_X(bag_And(bag_Not("Y"), bag_Not("Z"), bag_Not("h")), exact_state(["x", "xp"], all_entities)))) + f_x2 = ltl_G(True, ltl_Implies( + exact_state(["x", "xp"], all_entities), + ltl_X(bag_Not("h"), exact_state("X", all_entities)))) + + reach_xp = ltl_F(True, "xp") + reach_X = ltl_F(True, "X") + + smt_rsc = SmtCheckerRSCParam(rc, optimise=cmd_args.optimise) + + smt_rsc.check_rsltl(formulae_list=[f_x1, f_x2, reach_xp, reach_X]) + + # smt_rsc.check_rsltl(formula=f_x1, print_witness=True) + def trivial_param(): @@ -89,7 +116,7 @@ def trivial_param(): rc.show() smt_rsc = SmtCheckerRSCParam(rc) - f1 = ltl_F(bag_entity("final") >= 1) + f1 = ltl_F(True, bag_entity("final") >= 1) # f1 = Formula_rsLTL.f_F( # BagDescription.f_TRUE(), @@ -207,7 +234,7 @@ def heat_shock_response_param(cmd_args, print_system=True): # # f_reach_mfp = Formula_rsLTL.f_F(BagDescription.f_TRUE(), (BagDescription.f_entity("mfp") > 0) ) - f_reach_mfp = ltl_F(bag_entity("mfp") > 0) + f_reach_mfp = ltl_F(True, bag_entity("mfp") > 0) f_reach_hspmfp = Formula_rsLTL.f_F(BagDescription.f_TRUE(), (BagDescription.f_entity("hsp:mfp") > 0) ) diff --git a/rsltl_shortcuts.py b/rsltl_shortcuts.py index 815dce4..1e3abcc 100644 --- a/rsltl_shortcuts.py +++ b/rsltl_shortcuts.py @@ -8,19 +8,68 @@ def bag_True(): def bag_entity(name): return BagDescription.f_entity(name) -def ltl_F(a0, ctx_arg=None): - if ctx_arg == None: - ctx_arg = bag_True() +def get_bag_if_str(arg): + if isinstance(arg, str): + return bag_entity(arg) > 0 + else: + return arg + +def bag_Not(a0): + a0 = get_bag_if_str(a0) + return BagDescription.f_Not(a0) + +def bag_And(*args): + assert len(args) > 1 + last = get_bag_if_str(args[0]) + for arg in args[1:]: + last = BagDescription.f_And( + last, get_bag_if_str(arg)) + return last + +def exact_state(contained_entities, all_entities): + expr = [] + for ent_str in all_entities: + ent = bag_entity(ent_str) + if ent_str in contained_entities: + expr.append(ent > 0) + else: + expr.append(ent == 0) + + if len(expr) > 0: + + last = expr[0] + for e in expr[1:]: + last = BagDescription.f_And(last, e) + return last + + else: + assert False + +def ltl_F(ctx_arg, a0): + a0 = get_bag_if_str(a0) return Formula_rsLTL.f_F(ctx_arg, a0) -def ltl_G(a0, ctx_arg=None): - if ctx_arg == None: - ctx_arg = bag_True() +def ltl_G(ctx_arg, a0): + a0 = get_bag_if_str(a0) return Formula_rsLTL.f_G(ctx_arg, a0) -def ltl_X(a0, ctx_arg=None): - if ctx_arg == None: - ctx_arg = bag_True() +def ltl_X(ctx_arg, a0): + a0 = get_bag_if_str(a0) return Formula_rsLTL.f_X(ctx_arg, a0) +def ltl_And(*args): + assert len(args) > 1 + last = get_bag_if_str(args[0]) + for arg in args[1:]: + last = Formula_rsLTL.f_And(last, get_bag_if_str(arg)) + return last + +def ltl_Not(a0): + a0 = get_bag_if_str(a0) + return Formula_rsLTL.f_Not(a0) + +def ltl_Implies(a0, a1): + a0 = get_bag_if_str(a0) + a1 = get_bag_if_str(a1) + return Formula_rsLTL.f_Implies(a0, a1)