@using jpf-aprop

target = TestPF

# Choice CG for rounds
rounds.class = .jvm.choice.IntIntervalGenerator
rounds.min = 1
rounds.max = 13

# Choice CG for values
value.class = .jvm.choice.IntIntervalGenerator
value.min = 1
value.max = 3

# Add coverage checker
listener+=,.listener.CoverageAnalyzer

# Configure coverage analyzer:
# include class Heap
coverage.include=Heap
# show method coverage
coverage.show_methods = true
# show analysis for method bodies
coverage.show_bodies = true
# don't deal with exception handlers
coverage.exclude_handlers = true


# Stuff for running from outside of JPF project
classpath+=:.
sourcepath+=:.

# Track choices
listener+=,.listener.ChoiceTracker
listener+=,.aprop.listener.NonnullChecker
listener+=,.aprop.listener.ConstChecker
listener+=,.aprop.listener.ContractVerifier
listener+=,.aprop.listener.SandBoxChecker
# But only choices from IntIntervalGenerator or BooleanChoiceGenerator
choice.class=.jvm.choice.IntIntervalGenerator,.jvm.BooleanChoiceGenerator