Parameters in DryVR can be changed by users to get desire result for verification and synthesis. The configuration file is stored in
The following parameters can be changed by users
# Verification constant SIMUTESTNUM = 1 SIMTRACENUM = 10 REFINETHRES = 10 CHILDREFINETHRES = 2 # Synthesis Constant RANDMODENUM = 3 RANDSECTIONNUM = 3
- 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
- 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