diff --git a/README.md b/README.md index 16ae05d..4cdb1dc 100644 --- a/README.md +++ b/README.md @@ -26,10 +26,10 @@ $ ./reactics smt examples/smt/chain_reaction.py 2 3 1 ### Reaction synthesis -To test the reaction synthesis approach on a mutual exclution protocol modelling three processes run the following command: +To test the reaction synthesis approach on a mutual exclution protocol modelling three processes, run the following command: ``` ./reactics smt examples/smt/mutex_param.py -n 3 -s 1 -o ``` -`# EOF` + diff --git a/examples/smt/scalable_chain.py b/examples/smt/scalable_chain.py new file mode 100644 index 0000000..d129704 --- /dev/null +++ b/examples/smt/scalable_chain.py @@ -0,0 +1,173 @@ +#!/usr/bin/env python +# +# Copyright (c) 2015-2019 Artur Meski +# +# Permission is hereby granted, free of charge, to any person obtaining a copy +# of this software and associated documentation files (the "Software"), to deal +# in the Software without restriction, including without limitation the rights +# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +# copies of the Software, and to permit persons to whom the Software is +# furnished to do so, subject to the following conditions: +# +# The above copyright notice and this permission notice shall be included in all +# copies or substantial portions of the Software. +# +# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +# SOFTWARE. +# + +from rs import * +from smt import * +from logics import * +from rsltl_shortcuts import * + +from itertools import chain, combinations + +import sys +import resource + +def generate_system(chainLen, maxConc): + """ + This function generates the reaction system with concentrations + for the scalable chain benchmark + + chainLen is the length of the chain + maxConc is the maximal concentration + """ + + r = ReactionSystemWithConcentrations() + r.add_bg_set_entity(("inc",1)) + r.add_bg_set_entity(("dec",1)) + + for i in range(1,chainLen+1): + r.add_bg_set_entity(("e_" + str(i),maxConc)) + + for i in range(1,chainLen+1): + ent = "e_" + str(i) + r.add_reaction_inc(ent, "inc", [(ent, 1)],[(ent,maxConc)]) + r.add_reaction_dec(ent, "dec", [(ent, 1)],[]) + if i < chainLen: + r.add_reaction([(ent,maxConc)],[],[("e_"+str(i+1),1)]) + + r.add_reaction([("e_" + str(chainLen),maxConc)],[("dec",1)],[("e_" + str(chainLen),maxConc)]) + + 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) + + return rc + +def generate_formula(formula_number, chainLen, maxConc): + """ + This function generates the rsLTL formula + corresponding to the formula_number parameter + """ + + if formula_number == 1: + ret = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0, (BagDescription.f_entity('e_'+str(chainLen)) >= maxConc) ) + + elif formula_number == 2: + f_tmp = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0, (BagDescription.f_entity('e_'+str(chainLen)) == maxConc) ) + for i in range(chainLen-1,0,-1): + f_tmp = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0, f_tmp & (BagDescription.f_entity('e_'+str(i)) == maxConc) ) + ret = f_tmp + + elif formula_number == 3: + ret = Formula_rsLTL.f_G( BagDescription.f_TRUE(), + Formula_rsLTL.f_Implies( + (BagDescription.f_entity('e_1') == 1), + Formula_rsLTL.f_F( + BagDescription.f_entity("inc") > 0, + (BagDescription.f_entity('e_'+str(chainLen)) == maxConc) + ) + ) + ) + + elif formula_number == 4: + ret = Formula_rsLTL.f_F( BagDescription.f_entity("inc") > 0 , BagDescription.f_entity('e_1') == maxConc ) + + elif formula_number == 5: + ret = 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 ) ) + + else: + ret = None + + assert ret is not None, "Unknown formula" + + return ret + + +def save_statistics(smt_rsc, formula_number, chainLen, maxConc): + """ + Saves the statistics fetched from smt_rsc into files + """ + time=0 + mem_usage=resource.getrusage(resource.RUSAGE_SELF).ru_maxrss/(1024*1024) + filename_t="bench_rsc_F" + str(formula_number) + "_time.log" + filename_m="bench_rsc_F" + str(formula_number) + "_mem.log" + time=smt_rsc.get_verification_time() + + f=open(filename_t, 'a') + log_str="(" + str(chainLen) + "," + str(maxConc) + "," + str(time) + ")\n" + f.write(log_str) + f.close() + + f=open(filename_m, 'a') + log_str="(" + str(chainLen) + "," + str(maxConc) + "," + str(mem_usage) + ")\n" + f.write(log_str) + f.close() + + +def scalable_chain(print_system=False): + """ + This is the entry point for the benchmark + """ + if len(sys.argv) < 1+3: + print("arguments: ") + exit(1) + + chainLen=int(sys.argv[1]) # chain length + maxConc=int(sys.argv[2]) # depth (max concentration) + formula_number=int(sys.argv[3]) + + if chainLen < 1 or maxConc < 1: + print("be reasonable") + exit(1) + if not formula_number in range(1,5+1): + print("formulaNumber must be in 1..5") + exit(1) + + # Generate the reaction systems with concentrations + rc = generate_system(chainLen, maxConc) + + # Generate the formula + form = generate_formula(formula_number, chainLen, maxConc) + + # Optional dump/print of the system + if print_system: + rc.show() + + # Create an instance of the SMT checker for RS with concentrations + smt_rsc = SmtCheckerRSC(rc) + + # Start the verification process + smt_rsc.check_rsltl(formula=form) + + save_statistics(smt_rsc, formula_number, chainLen, maxConc) + + +def main(): + scalable_chain(print_system=True) + +if __name__ == "__main__": + main() +