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

New formula, 5

Browse Source
This commit is contained in:
Artur Meski
2017-03-18 18:39:52 +01:00
parent 80f2caea53
commit 15500b7e38
1 changed files with 8 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files

11
rs_testing.py
View File

@@ -112,8 +112,8 @@ def scalable_chain(print_system=False):
if chainLen < 1 or maxConc < 1: if chainLen < 1 or maxConc < 1:
print("be reasonable") print("be reasonable")
exit(1) exit(1)
if not formula_number in range(1,4+1): if not formula_number in range(1,5+1):
print("formulaNumber must be in 1..4") print("formulaNumber must be in 1..5")
exit(1) exit(1)
r = ReactionSystemWithConcentrations() r = ReactionSystemWithConcentrations()
@@ -160,14 +160,19 @@ def scalable_chain(print_system=False):
(BagDescription.f_entity('e_1') == 1), (BagDescription.f_entity('e_1') == 1),
Formula_rsLTL.f_F( Formula_rsLTL.f_F(
BagDescription.f_entity("inc") > 0, BagDescription.f_entity("inc") > 0,
(BagDescription.f_entity('e_'+str(i)) == maxConc) (BagDescription.f_entity('e_'+str(chainLen)) == maxConc)
) )
) )
) )
print(i)
smt_rsc.check_rsltl(formula=f_3) smt_rsc.check_rsltl(formula=f_3)
elif formula_number == 4: elif formula_number == 4:
f_4 = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0 , BagDescription.f_entity('e_1') == maxConc ) f_4 = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0 , BagDescription.f_entity('e_1') == maxConc )
smt_rsc.check_rsltl(formula=f_4) smt_rsc.check_rsltl(formula=f_4)
elif formula_number == 5:
f_5 = Formula_rsLTL.f_X(BagDescription.f_TRUE(), Formula_rsLTL.f_U( BagDescription.f_entity("inc") > 0 , BagDescription.f_entity('e_1') > 0, BagDescription.f_entity('e_2') > 0 ) )
smt_rsc.check_rsltl(formula=f_5)
########################################################################### ###########################################################################