Parameters configuration¶
Parameters in DryVR can be changed by users to get desire result for verification and synthesis. The configuration file is stored in
src/common/constant.py
The following parameters can be changed by users
# Verification constant
SIMUTESTNUM = 1
SIMTRACENUM = 10
REFINETHRES = 10
CHILDREFINETHRES = 2
# Synthesis Constant
RANDMODENUM = 3
RANDSECTIONNUM = 3
Verification constant:
- SIMUTESTNUM is the number of hybrid simulation runs at beginning of the verification algorithm to find counter examples.
- SIMTRACENUM is the number of sumulation traces generated to learn the sensitity (discrepancy function).
- REFINETHRES is the refine threshold for initial set given by user.
- CHILDREFINETHRES is threshold of the refinement times for non-initial vertices of the transition graph
Synthesis Constant:
- RANDMODENUM is the number of random modes picked at each time for each candidate guard
- RANDSECTIONNUM is number of time intervals picked as the next set of candidate guards