artur/reactics
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Easier formulae

Browse Source
This commit is contained in:
Artur Meski
2017-12-02 00:13:08 +00:00
parent 2c399dc5c1
commit 32d31f9fa1
6 changed files with 131 additions and 35 deletions
Download Patch File Download Diff File Expand all files Collapse all files

18
logics/bags.py
View File

@@ -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)

30
logics/rsltl.py
View File

@@ -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))
@@ -27,33 +28,36 @@ class Formula_rsLTL(object):
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)

10
logics/rsltl_encoder.py
View File

@@ -121,11 +121,17 @@ 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):

4
rs/reaction_system_with_concentrations_param.py
View File

@@ -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

35
rs_testing.py
View File

@@ -42,9 +42,20 @@ def gene_expression(cmd_args):
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) )

67
rsltl_shortcuts.py
View File

@@ -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)