summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDaniel Friesel <daniel.friesel@uos.de>2019-09-25 15:36:20 +0200
committerDaniel Friesel <daniel.friesel@uos.de>2019-09-25 15:36:20 +0200
commit8aa9bdc2ec7832d49a7dde8ee92641df43a37398 (patch)
tree25670d5436597552fe7a0817145a54a46ddf9a85
parentcd38fd1a31526f6667aaf0b4060601a433df9ff1 (diff)
add --shrink option to generate-dfa-benchmark
-rwxr-xr-xbin/generate-dfa-benchmark.py8
1 files changed, 8 insertions, 0 deletions
diff --git a/bin/generate-dfa-benchmark.py b/bin/generate-dfa-benchmark.py
index 65da4be..30f2d20 100755
--- a/bin/generate-dfa-benchmark.py
+++ b/bin/generate-dfa-benchmark.py
@@ -31,6 +31,10 @@ Options:
--sleep=<ms> (default: 0)
How long to sleep between function calls.
+--shrink
+ Decrease amount of parameter values used in state space exploration
+ (only use minimum and maximum for numeric values)
+
--trace-filter=<transition,transition,transition,...>[ <transition,transition,transition,...> ...]
Only consider traces whose beginning matches one of the provided transition sequences.
E.g. --trace-filter='init,foo init,bar' will only consider traces with init as first and foo or bar as second transition,
@@ -210,6 +214,7 @@ if __name__ == '__main__':
'repeat= '
'run= '
'sleep= '
+ 'shrink '
'timer-pin= '
'trace-filter= '
)
@@ -254,6 +259,9 @@ if __name__ == '__main__':
else:
pta = PTA.from_yaml(yaml.safe_load(f))
+ if 'shrink' in opt:
+ pta.shrink_argument_values()
+
if 'timer-pin' in opt:
timer_pin = opt['timer-pin']
else: