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

simple rsLTL example for paper

Browse Source
This commit is contained in:
Artur Meski
2017-04-04 22:48:33 +02:00
parent cabe9fc1b8
commit 9c9084e4e2
1 changed files with 80 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

81
rs_testing.py
View File

@@ -10,7 +10,86 @@ def run_tests():
# test_extended_automaton() # test_extended_automaton()
# process() # process()
# heat_shock_response() # heat_shock_response()
scalable_chain(print_system=True) # scalable_chain(print_system=True)
example44()
def example44():
r = ReactionSystemWithConcentrations()
r.add_bg_set_entity(("x",2))
r.add_bg_set_entity(("y",4))
r.add_bg_set_entity(("h",2))
r.add_bg_set_entity(("m",1))
r.add_reaction([("y",1),("x",1)], [("y",2),("h",1)], [("y",2)])
r.add_reaction([("y",2),("x",2)], [("y",3),("h",1)], [("y",3)])
r.add_reaction([("y",3),("h",1)], [("y",4),("h",2)], [("y",4)])
r.add_reaction([("y",4),("h",1)], [("h",2)], [("y",3)])
r.add_reaction([("y",4),("x",2)], [("h",1)], [("y",2)])
r.add_reaction([("m",1)], [("y",3)], [("m",1)])
c = ContextAutomatonWithConcentrations(r)
c.add_init_state("0")
c.add_state("1")
c.add_transition("0", [("y",1),("m",1),("x",1)], "1")
c.add_transition("1", [("x",1)], "1")
c.add_transition("1", [("x",1),("h",1)], "1")
c.add_transition("1", [("x",2)], "1")
c.add_transition("1", [("x",2),("h",1)], "1")
c.add_transition("1", [("h",1)], "1")
rc = ReactionSystemWithAutomaton(r,c)
rc.show()
smt_rsc = SmtCheckerRSC(rc)
# Universal property which seems to be true: (holds also existentially)
f1 = Formula_rsLTL.f_G(BagDescription.f_entity("x") > 0,
Formula_rsLTL.f_Implies(
(BagDescription.f_entity('y') == 2),
Formula_rsLTL.f_X(
(BagDescription.f_entity("x") > 1),
BagDescription.f_entity("y") >= 3
)
)
)
# lets see if we can find a counterexample to this property:
neg_f1 = Formula_rsLTL.f_F(BagDescription.f_entity("x") > 0,
Formula_rsLTL.f_And(
(BagDescription.f_entity('y') == 2),
Formula_rsLTL.f_X(
(BagDescription.f_entity("x") > 1),
BagDescription.f_entity("y") < 3
)
)
)
# we fix the property f1
# this one holds:
f2 = Formula_rsLTL.f_G(BagDescription.f_entity("x") > 0,
Formula_rsLTL.f_Implies(
(BagDescription.f_entity('y') == 2),
Formula_rsLTL.f_X(
(BagDescription.f_entity("x") > 1) & (BagDescription.f_entity("h") < 1),
BagDescription.f_entity("y") >= 3
)
)
)
# neg_f1 = Formula_rsLTL.f_X(BagDescription.f_TRUE(), Formula_rsLTL.f_F(BagDescription.f_entity("x") > 0,
# Formula_rsLTL.f_And(
# (BagDescription.f_entity('y') > 0),
# Formula_rsLTL.f_X(
# BagDescription.f_entity("x") > 0,
# Formula_rsLTL.f_X(
# BagDescription.f_entity("x") > 1,
# BagDescription.f_entity("y") < 3
# )
# )
# )
# ))
smt_rsc.check_rsltl(formula=neg_f1)
def heat_shock_response(print_system=True): def heat_shock_response(print_system=True):