This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

Bug 482

Summary: Random depth first never chooses one of two transitions on first attempt
Product: UPPAAL Reporter: Jacob Illum <illum>
Component: EngineAssignee: Alexandre David <adavid>
Status: RESOLVED FIXED    
Severity: major    
Priority: P2    
Version: 4.0.8   
Hardware: PC   
OS: All   
Architecture:

Description Jacob Illum 2010-01-15 10:41:32 CET 
In the simple example system published with this bug, there is a single template with a diamond like choice to reach the goal. When selecting random depth first for reaching the goal (at least on the command line with verifyta), the resulting trace will never choose one of the two identical paths.

The search method is however still complete, since if the first chosen path doesn't reach the goal, the second path will still be traversed later.

This bug is also present in 4.1.2.
Comment 1 Jacob Illum 2010-01-15 10:49:41 CET 
The attachment service is not working, so I'll write up the system in ASCII:
Template:
     Init
    /    \
   /      \
  A1      A2
   \      /
    \    /
     Goal
Query:
E<> Template.Goal

Command line:
verifyta -sq -o2 -t1 system.{xml,q}

Run the above command until you convince yourself that either A1 or A2 is never chosen as the goal reaching path.
Comment 2 Alexandre David 2010-01-15 15:13:20 CET 
Fixed in rev. 4483 (trunk) & 4484 (4.0).
The permutations didn't allow for identity.