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

Example: overview

Browse Source
This commit is contained in:
Artur Meski
2019-02-22 23:14:57 +00:00
parent beef6c5f4e
commit 9e0ca1d654
2 changed files with 44 additions and 79 deletions
Download Patch File Download Diff File Expand all files Collapse all files

44
doc/overview.py Executable file
View File

@@ -0,0 +1,44 @@
#!/usr/bin/env python
from rs import *
from smt import *
from logics import *
from rsltl_shortcuts import *
def ex():
prs = ReactionSystemWithConcentrationsParam()
ent_with_conc = [("a", 3), ("b",2), ("c",1), ("h",1)]
for ec in ent_with_conc:
prs.add_bg_set_entity(ec)
lda = prs.get_param("lda")
prs.add_reaction([("a",1)],[("h",1)],[("b", 2)])
prs.add_reaction(lda,[("h",1)],[("c",1)])
##
ca = ContextAutomatonWithConcentrations(prs)
ca.add_init_state("0")
ca.add_state("1")
ca.add_transition("0", [("a", 3)], "1")
ca.add_transition("1", [], "1")
ca.add_transition("1", [("h", 1)], "1")
crprs = ReactionSystemWithAutomaton(prs, ca)
crprs.show()
pc = param_entity(lda, "a") == 0
f = ltl_F(bag_entity("h") == 0, "c")
checker = SmtCheckerRSCParam(crprs, optimise=True)
checker.check_rsltl(formulae_list=[f], param_constr=pc)
if __name__ == "__main__":
ex()
# EOF

79
phd_example.py
View File

@@ -1,79 +0,0 @@
#!/usr/bin/env python
from rs import *
from smt import *
from logics import *
from rsltl_shortcuts import *
def gen_expr():
prs = ReactionSystemWithConcentrationsParam()
ent_with_conc = [("a", 3), ("b",2), ("c",1), ("h",1)]
for ec in ent_with_conc:
prs.add_bg_set_entity(ec)
lda = prs.get_param("lda")
prs.add_reaction([("a",1)],[("h",1)],[("b", 2)])
prs.add_reaction(lda,[("h",1)],[("c",1)])
##
ca = ContextAutomatonWithConcentrations(prs)
ca.add_init_state("0")
ca.add_state("1")
ca.add_transition("0", [("a", 3)], "1")
ca.add_transition("1", [], "1")
ca.add_transition("1", [("h", 1)], "1")
crprs = ReactionSystemWithAutomaton(prs, ca)
crprs.show()
print("......")
# cprs is defined in the SMT checker
# reach_y = ltl_F(bag_entity("h") == 0, "y")
# reach_yp = ltl_F(bag_entity("h") == 0, "yp")
# reach_Y = ltl_F(bag_entity("h") == 0, "Y")
#
# # rules
# phi_c1 = ltl_G(bag_entity("h") == 0, ltl_Implies(
# bag_entity("y") > 0,
# ltl_X(True, bag_And(bag_entity("y") > 0, bag_entity("yp") > 0))))
#
# phi_c2 = ltl_G(bag_entity("h") == 0, ltl_Implies(
# bag_And(bag_entity("y") > 0, bag_entity("yp") > 0),
# ltl_F(True, bag_entity("Y") > 0)))
#
# # delayed_Y = ltl_X(True, ltl_And(bag_entity("Y") == 0, ltl_X(True, bag_entity("Y") == 0)))
#
# # delayed_Y = ltl_X(True, bag_entity("Y") == 0)
#
# delayed_Q = ltl_And(bag_entity("Q") == 0, ltl_X(True, ltl_And(bag_entity("Q") == 0, ltl_X(True, ltl_And(bag_entity("Q") == 0, ltl_F(True, bag_entity("Q") > 0))))))
#
# obs_1 = ltl_And(phi_r, phi_c1, phi_c2, delayed_Q)
# obs_2 = ltl_And(f_y2, reach_y, reach_Y, delayed_Y, delayed_Q)
# f_x2 = ltl_G(True, ltl_Implies(
# exact_state(["x", "xp"], all_entities),
# ltl_X(bag_Not("h"), exact_state("X", all_entities))))
#
pc = param_entity(lda, "a") == 0
f = ltl_F(bag_entity("h") == 0, "c")
checker = SmtCheckerRSCParam(crprs, optimise=True)
checker.check_rsltl(formulae_list=[f], param_constr=pc)
gen_expr()