From 249e8ca594c7ab344ca535231e806cd931602278 Mon Sep 17 00:00:00 2001 From: Artur Meski Date: Sun, 28 Feb 2016 22:57:37 +0100 Subject: [PATCH] Just to be sure... --- rs_examples.py | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) diff --git a/rs_examples.py b/rs_examples.py index fdcb52a..53b1381 100755 --- a/rs_examples.py +++ b/rs_examples.py @@ -388,5 +388,34 @@ def chain_reaction(print_system=False): f.write(log_str) f.close() +def blood_glucose_regulation(): + r = ReactionSystemWithConcentrations() + r.add_bg_set_entity(("inc_insulin",1)) + r.add_bg_set_entity(("dec_insulin",1)) + r.add_bg_set_entity(("inc_glycemia",1)) + r.add_bg_set_entities(("inc_")) + + r.add_bg_set_entities([(sugar,1),(aspartame,1),(glycemia,3),(glucagon,1),(insulin,2)]) + + # r.add_reaction([],[],[]) + r.add_reaction([(sugar,1)],[],[(inc_insulin,1),(inc_glycemia,1)]) + r.add_reaction([],[],[]) + r.add_reaction([],[],[]) + + c = ContextAutomatonWithConcentrations(r) + c.add_init_state("init") + c.add_state("working") + c.add_transition("init", [("e_1",1),("inc",1)], "working") + c.add_transition("working", [("inc",1)], "working") + rc = ReactionSystemWithAutomaton(r,c) + + if print_system: + rc.show() + + # if verify_rsc: + # smt_rsc = SmtCheckerRSC(rc) + # 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)