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

Bug 482 - Random depth first never chooses one of two transitions on first attempt
Summary: Random depth first never chooses one of two transitions on first attempt
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: Engine (show other bugs)
Version: 4.0.8
Hardware: PC All
: P2 major
Assignee: Alexandre David
URL:
Depends on:
Blocks:
 
Reported: 2010-01-15 10:41 CET by Jacob Illum
Modified: 2010-01-15 15:13 CET (History)
0 users

See Also:
Architecture:

Attachments
Add an attachment (proposed patch, testcase, etc.)

Note You need to log in before you can comment on or make changes to this bug.
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.