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

Examples and clean-ups (#1)

Browse Source 
- Attempt at implementing an example for DRS
- Complete reactions set
- New automaton
- Formula
- Fixed automaton scaling
- Proc index in the formula
- Benchmark generators
- Scripts to reproduce experiments for reaction mining
This commit was merged in pull request #1.
This commit is contained in:
Artur Meski
2023-11-06 21:09:08 +00:00
committed by GitHub
parent 888ed4e68e
commit af26ca543b
16 changed files with 1145 additions and 132 deletions
Download Patch File Download Diff File Expand all files Collapse all files

97
experiments/drs_cell_signal/run.sh Executable file
View File

@@ -0,0 +1,97 @@
#!/usr/bin/env bash
x_values="2 3 4"
y_values="`seq 2 20`"
z_values="`seq 2 20`"
aut_values="a b"
reactics="$1"
reactics_opts="-z -x -vv -B -c"
input_generator="../../examples/bdd/generators/gen_drs.py"
benchname="sig"
formname="f0"
outdir="results_${benchname}"
if [[ -z "$1" ]]
then
echo "Usage: $0 <path to reactics>"
exit 1
fi
if [[ ! -x "$reactics" ]]
then
echo "Provided path to ReactICS not executable"
fi
if [[ ! -d "$outdir" ]]
then
echo "Creating output directory: $outdir"
mkdir -p $outdir
fi
#ulimit -t 3600
#ulimit -v 2097152
ulimit -t 3600
#ulimit -v 1000000
for a in $aut_values
do
for z in $z_values
do
for y in $y_values
do
for x in $x_values
do
if [[ $y -lt $z ]]
then
# Skip undesired values
continue
fi
if [[ $y -ne $z ]]
then
# More aggressive skipping
continue
fi
bench_identifier="${benchname}_F${formname}_A${a}"
filename_base="${outdir}/${benchname}_F${formname}__x${x}_y${y}_z${z}_A${a}"
outfile="${filename_base}.out"
infile="${filename_base}.drs"
stopfile="DONE_${bench_identifier}"
if [[ -e "$stopfile" ]]
then
echo "Time limit -- SKIPPING"
continue
fi
$input_generator $x $y $z $a > ${infile}
$reactics $reactics_opts $formname $infile |& tee ${outfile}
exitcode=$?
echo "ReactICS exit code: $exitcode"
result="$(tail -1 $outfile | grep -E '.*;.*;.*;.*'| sed "s/STAT/$n /")"
if [ "$result" = "" ]
then
echo "TIME LIMIT; marking as finished"
#touch $stopfile
else
echo "$x ; $y ; $z ; $a ; $exitcode $result" >> $outdir/summary_${bench_identifier}.txt
echo "$x $y $z $a $(echo $result | sed 's/;/ /g')" >> $outdir/${bench_identifier}.dat
echo $result
fi
done
done
done
done
# EOF

20
experiments/reaction_mining_mutex/bench_mutex_nonparam_mem.dat Normal file
View File

@@ -0,0 +1,20 @@
2 69.171875
3 69.937500
4 86.109375
5 76.093750
6 81.812500
7 97.078125
8 88.562500
9 102.968750
10 93.546875
11 98.515625
12 113.671875
13 115.656250
14 132.140625
15 141.546875
16 149.890625
17 155.125000
18 153.500000
19 166.953125
20 169.750000
21 212.468750

20
experiments/reaction_mining_mutex/bench_mutex_nonparam_oldimpl_mem.dat Normal file
View File

@@ -0,0 +1,20 @@
2 68.765625
3 73.140625
4 71.625000
5 73.359375
6 79.234375
7 75.578125
8 79.812500
9 85.828125
10 81.718750
11 79.828125
12 83.984375
13 80.406250
14 75.859375
15 85.812500
16 89.093750
17 84.296875
18 89.078125
19 87.609375
20 88.281250
21 85.406250

20
experiments/reaction_mining_mutex/bench_mutex_nonparam_oldimpl_time.dat Normal file
View File

@@ -0,0 +1,20 @@
2 0.068995
3 0.110615
4 0.164639
5 0.234950
6 0.322793
7 0.438878
8 0.578109
9 0.752163
10 0.955217
11 1.190432
12 1.519409
13 1.808177
14 2.200211
15 2.654874
16 3.265984
17 3.824895
18 4.413004
19 5.303216
20 6.310782
21 7.038971

20
experiments/reaction_mining_mutex/bench_mutex_nonparam_time.dat Normal file
View File

@@ -0,0 +1,20 @@
2 0.095321
3 0.171177
4 0.272130
5 0.417800
6 0.584877
7 0.766862
8 1.009195
9 1.295766
10 1.741482
11 2.354580
12 2.949242
13 3.127326
14 4.074318
15 4.978959
16 6.690042
17 8.114637
18 12.006410
19 11.929118
20 14.044730
21 15.673520

20
experiments/reaction_mining_mutex/bench_mutex_param_mem.dat Normal file
View File

@@ -0,0 +1,20 @@
2 80.093750
3 76.062500
4 88.312500
5 97.140625
6 95.234375
7 109.843750
8 111.218750
9 132.921875
10 142.546875
11 151.546875
12 175.546875
13 186.109375
14 206.546875
15 235.281250
16 245.515625
17 249.562500
18 260.203125
19 278.796875
20 292.781250
21 300.562500

20
experiments/reaction_mining_mutex/bench_mutex_param_time.dat Normal file
View File

@@ -0,0 +1,20 @@
2 0.487115
3 0.880007
4 1.301547
5 2.172839
6 2.662308
7 3.880329
8 4.491871
9 6.922392
10 8.729740
11 10.901971
12 13.885037
13 18.246820
14 21.987255
15 28.236579
16 41.065607
17 44.456013
18 50.782835
19 59.535617
20 83.400427
21 96.250559

454
experiments/reaction_mining_mutex/pmutex.py Executable file
View File

@@ -0,0 +1,454 @@
#!/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
import argparse
def powerset(iterable, N=None):
if N is None:
N = len(s)
s = list(iterable)
return chain.from_iterable(combinations(s, r) for r in range(N + 1))
def mutex_param_bench(cmd_args):
"""
Mutex Benchmark
Parametric
"""
base_entities = ["out", "req", "in", "act"]
shared_entities = ["lock", "done", "s"]
if not cmd_args.scaling:
print("Missing scaling parameter")
return
n_proc = int(cmd_args.scaling)
r = ReactionSystemWithConcentrationsParam()
def E(a, b, c=1):
return (a + "_" + str(b), c)
for i in range(n_proc):
for ent in base_entities:
max_conc = 1
if ent == "in":
max_conc = 3
elif ent == "req":
max_conc = 2
r.add_bg_set_entity(E(ent, i, max_conc))
for ent in shared_entities:
max_conc = 1
r.add_bg_set_entity((ent, max_conc))
###################################################
Inhib = [("s", 1)]
for i in range(n_proc):
r.add_reaction([E("out", i), E("act", i)], Inhib, [E("req", i)])
r.add_reaction([E("out", i)], [E("act", i)], [E("out", i)])
for j in range(n_proc):
if i != j:
r.add_reaction(
[E("req", i), E("act", i), E("act", j)], Inhib, [E("req", i)]
)
r.add_reaction([E("req", i)], [E("act", i)], [E("req", i, 2)])
enter_inhib = [E("act", j) for j in range(n_proc) if i != j] + [("lock", 1)]
r.add_reaction(
[E("req", i, 2), E("act", i)], enter_inhib, [E("in", i, 3), ("lock", 1)]
)
r.add_reaction([E("in", i, 3), E("act", i)], Inhib, [E("in", i, 2)])
r.add_reaction([E("in", i, 2), E("act", i)], Inhib, [E("in", i, 1)])
r.add_reaction([E("in", i), E("act", i)], Inhib, [E("out", i), ("done", 1)])
r.add_reaction([E("in", i)], [E("act", i)], [E("in", i)])
r.add_reaction([("lock", 1)], [("done", 1)], [("lock", 1)])
lda1 = r.get_param("lda1")
lda2 = r.get_param("lda2")
lda3 = r.get_param("lda3")
r.add_reaction(lda1, lda2, lda3)
###################################################
c = ContextAutomatonWithConcentrations(r)
c.add_init_state("0")
c.add_state("1")
init_ctx = []
for i in range(n_proc):
init_ctx.append(E("out", i))
# the experiments starts with adding x and y:
c.add_transition("0", init_ctx, "1")
all_act = powerset([E("act", i) for i in range(n_proc)], 2)
for actions in all_act:
actions = list(actions)
c.add_transition("1", actions, "1")
# for all the remaining steps we have empty context sequences
# c.add_transition("1", [], "1")
# c.add_transition("1", [("h", 1)], "1")
###################################################
rc = ReactionSystemWithAutomaton(r, c)
rc.show()
f_attack = ltl_F(
True, bag_And(bag_entity("in_0") == 1, bag_entity("in_" + str(n_proc - 1)) == 1)
)
ent_of_Nth_proc = [
ent + "_" + str(n_proc - 1) for ent in base_entities
] + shared_entities
disallow = ["in_" + str(n_proc - 1)]
for ent in r.background_set:
if ent not in ent_of_Nth_proc:
disallow.append(ent)
# disallow.append("act_" + str(n_proc-1))
# disallow = ["in_0", "in_" + str(n_proc)] #, "req_0", "req_1"]
lda1_disallow = [param_entity(lda1, ent) == 0 for ent in disallow]
lda2_disallow = [param_entity(lda2, ent) == 0 for ent in disallow]
lda3_disallow = [param_entity(lda3, ent) == 0 for ent in disallow]
lda_disallow = lda1_disallow + lda2_disallow + lda3_disallow
# for bent in base_entities:
# print(param_entity(lda3, bent + "_0"))
param_constr = param_And(*lda_disallow)
smt_rsc = SmtCheckerRSCParam(rc, optimise=cmd_args.optimise)
smt_rsc.check_rsltl(
formulae_list=[f_attack], param_constr=param_constr
) # , max_level=4, cont_if_sat=True)
log_suffix = ""
if cmd_args.optimise:
log_suffix = "_OPT"
time = 0
mem_usage = resource.getrusage(resource.RUSAGE_SELF).ru_maxrss / (1024 * 1024)
filename_t = "bench_mutex_param" + log_suffix + "_time.dat"
filename_m = "bench_mutex_param" + log_suffix + "_mem.dat"
time = smt_rsc.get_verification_time()
with open(filename_t, "a") as f:
log_str = "{:d} {:f}\n".format(n_proc, time)
f.write(log_str)
with open(filename_m, "a") as f:
log_str = "{:d} {:f}\n".format(n_proc, mem_usage)
f.write(log_str)
def mutex_nonparam_bench(cmd_args):
"""
Mutex Benchmark
Parametric
"""
base_entities = ["out", "req", "in", "act"]
shared_entities = ["lock", "done", "s"]
if not cmd_args.scaling:
raise RuntimeError("Missing scaling parameter")
n_proc = int(cmd_args.scaling)
r = ReactionSystemWithConcentrationsParam()
def E(a, b):
return (a + "_" + str(b), 1)
for i in range(n_proc):
for ent in base_entities:
r.add_bg_set_entity(E(ent, i))
for ent in shared_entities:
r.add_bg_set_entity((ent, 1))
###################################################
Inhib = [("s", 1)]
for i in range(n_proc):
r.add_reaction([E("out", i), E("act", i)], Inhib, [E("req", i)])
r.add_reaction([E("out", i)], [E("act", i)], [E("out", i)])
for j in range(n_proc):
if i != j:
r.add_reaction(
[E("req", i), E("act", i), E("act", j)], Inhib, [E("req", i)]
)
r.add_reaction([E("req", i)], [E("act", i)], [E("req", i)])
enter_inhib = [E("act", j) for j in range(n_proc) if i != j] + [("lock", 1)]
r.add_reaction(
[E("req", i), E("act", i)], enter_inhib, [E("in", i), ("lock", 1)]
)
r.add_reaction([E("in", i), E("act", i)], Inhib, [E("out", i), ("done", 1)])
r.add_reaction([E("in", i)], [E("act", i)], [E("in", i)])
r.add_reaction([("lock", 1)], [("done", 1)], [("lock", 1)])
r.add_reaction(
[E("out", n_proc - 1)], [("s", 1)], [("done", 1), E("req", n_proc - 1)]
)
###################################################
c = ContextAutomatonWithConcentrations(r)
c.add_init_state("0")
c.add_state("1")
init_ctx = []
for i in range(n_proc):
init_ctx.append(E("out", i))
# the experiments starts with adding x and y:
c.add_transition("0", init_ctx, "1")
all_act = powerset([E("act", i) for i in range(n_proc)], 2)
for actions in all_act:
actions = list(actions)
c.add_transition("1", actions, "1")
# for all the remaining steps we have empty context sequences
# c.add_transition("1", [], "1")
# c.add_transition("1", [("h", 1)], "1")
###################################################
rc = ReactionSystemWithAutomaton(r, c)
rc.show()
f_attack = ltl_F(
True, bag_And(bag_entity("in_0") == 1, bag_entity("in_" + str(n_proc - 1)) == 1)
)
smt_rsc = SmtCheckerRSCParam(rc, optimise=cmd_args.optimise)
smt_rsc.check_rsltl(formulae_list=[f_attack])
time = 0
mem_usage = resource.getrusage(resource.RUSAGE_SELF).ru_maxrss / (1024 * 1024)
filename_t = "bench_mutex_nonparam_time.dat"
filename_m = "bench_mutex_nonparam_mem.dat"
time = smt_rsc.get_verification_time()
with open(filename_t, "a") as f:
log_str = "{:d} {:f}\n".format(n_proc, time)
f.write(log_str)
with open(filename_m, "a") as f:
log_str = "{:d} {:f}\n".format(n_proc, mem_usage)
f.write(log_str)
def mutex_nonparam_bench_oldimpl(cmd_args):
"""
Mutex Benchmark
Parametric
"""
base_entities = ["out", "req", "in", "act"]
shared_entities = ["lock", "done", "s"]
if not cmd_args.scaling:
raise RuntimeError("Missing scaling parameter")
n_proc = int(cmd_args.scaling)
r = ReactionSystemWithConcentrations()
def E(a, b):
return (a + "_" + str(b), 1)
for i in range(n_proc):
for ent in base_entities:
r.add_bg_set_entity(E(ent, i))
for ent in shared_entities:
r.add_bg_set_entity((ent, 1))
###################################################
Inhib = [("s", 1)]
for i in range(n_proc):
r.add_reaction([E("out", i), E("act", i)], Inhib, [E("req", i)])
r.add_reaction([E("out", i)], [E("act", i)], [E("out", i)])
for j in range(n_proc):
if i != j:
r.add_reaction(
[E("req", i), E("act", i), E("act", j)], Inhib, [E("req", i)]
)
r.add_reaction([E("req", i)], [E("act", i)], [E("req", i)])
enter_inhib = [E("act", j) for j in range(n_proc) if i != j] + [("lock", 1)]
r.add_reaction(
[E("req", i), E("act", i)], enter_inhib, [E("in", i), ("lock", 1)]
)
r.add_reaction([E("in", i), E("act", i)], Inhib, [E("out", i), ("done", 1)])
r.add_reaction([E("in", i)], [E("act", i)], [E("in", i)])
r.add_reaction([("lock", 1)], [("done", 1)], [("lock", 1)])
r.add_reaction(
[E("out", n_proc - 1)], [("s", 1)], [("done", 1), E("req", n_proc - 1)]
)
###################################################
c = ContextAutomatonWithConcentrations(r)
c.add_init_state("0")
c.add_state("1")
init_ctx = []
for i in range(n_proc):
init_ctx.append(E("out", i))
# the experiments starts with adding x and y:
c.add_transition("0", init_ctx, "1")
all_act = powerset([E("act", i) for i in range(n_proc)], 2)
for actions in all_act:
actions = list(actions)
c.add_transition("1", actions, "1")
# for all the remaining steps we have empty context sequences
# c.add_transition("1", [], "1")
# c.add_transition("1", [("h", 1)], "1")
###################################################
rc = ReactionSystemWithAutomaton(r, c)
rc.show()
f_attack = ltl_F(
True, bag_And(bag_entity("in_0") == 1, bag_entity("in_" + str(n_proc - 1)) == 1)
)
smt_rsc = SmtCheckerRSC(rc)
smt_rsc.check_rsltl(formula=f_attack)
time = 0
mem_usage = resource.getrusage(resource.RUSAGE_SELF).ru_maxrss / (1024 * 1024)
filename_t = "bench_mutex_nonparam_oldimpl_time.dat"
filename_m = "bench_mutex_nonparam_oldimpl_mem.dat"
time = smt_rsc.get_verification_time()
with open(filename_t, "a") as f:
log_str = "{:d} {:f}\n".format(n_proc, time)
f.write(log_str)
with open(filename_m, "a") as f:
log_str = "{:d} {:f}\n".format(n_proc, mem_usage)
f.write(log_str)
def state_translate_rsc2rs(p):
return [e[0] + "#" + str(e[1]) for e in p]
def mutex_bench_main(cmd_args):
mode = cmd_args.mode
if mode == "p":
mutex_param_bench(cmd_args)
elif mode == "np-p":
mutex_nonparam_bench(cmd_args)
elif mode == "np-np":
mutex_nonparam_bench_oldimpl(cmd_args)
else:
print("Unrecognised mode")
return
def main():
parser = argparse.ArgumentParser()
parser.add_argument(
"scaling",
help="scaling parameter value",
)
parser.add_argument(
"mode",
choices=["p", "np-p", "np-np"],
help="Selects the mode: p - parameter synthesis (parametric implementation), np-p - non-parametric with parametric implementation (with the parameters substituted), np-np - non-parametric with non-parametric implementation (parameters substituted)",
)
parser.add_argument(
"-v", "--verbose", help="turn verbosity on", action="store_true"
)
parser.add_argument(
"-o",
"--optimise",
help="minimise the parametric computation result",
action="store_true",
)
args = parser.parse_args()
mutex_bench_main(args)
if __name__ == "__main__":
main()
# EOF

26
experiments/reaction_mining_mutex/run_mutex_param.sh Executable file
View File

@@ -0,0 +1,26 @@
#!/bin/sh
# sudo systemsetup -getcomputersleep
#sudo systemsetup -setcomputersleep Never
# sudo systemsetup -setcomputersleep 1
REACTICS_SMT="../../reactics-smt"
export PYTHONPATH="$PYTHONPATH:$REACTICS_SMT"
REACTICS_SCRIPT="./pmutex.py"
for i in `seq 2 50`
do
for special_mode in "p" "np-p" "np-np"
do
echo "$i (sm=${special_mode})"
if [[ $special_mode -eq 1 ]]
then
$REACTICS_SCRIPT $i $special_mode
$REACTICS_SCRIPT -o $i $special_mode
else
$REACTICS_SCRIPT $i $special_mode
fi
done
done