First Last Prev Next    No search results available      Search page      Enter new bug
Bug#: 469
Product:
Component:
Status: RESOLVED
Resolution: FIXED
Assigned To: Alexandre David <adavid@cs.aau.dk>
Hardware:
OS:
Version:
Priority:
Severity:
Reporter: AndreA Orlandini <andrea.orlandini@gmail.com>
Add CC:
CC:
URL:
Summary:

Attachment Type Creator Created Size Actions
Create a New Attachment (proposed patch, testcase, etc.) View All

Bug 469 depends on: Show dependency tree
Show dependency graph
Bug 469 blocks:

Additional Comments:







View Bug Activity   |   Format For Printing   |   XML   |   Clone This Bug


Description:   Opened: 2009-04-07 14:51
I experienced a unhandled win32 exception with UPPAAL-TIGA on Windows XP while
using a bad automaton model.

It seems to me that the problem was caused by inconsistent definition in
automaton model. In fact, I defined a set of states, then I considered in the
transition a state that is not defined. 

I obtained an unhandled exception both in using uppaal.jar (java gui) and
verifytga.exe (shell cmd), while I was expecting to get a syntax error.

Here you may find the model and the bad transition definitions.

process POINTING() {

state
    State0 {clock <= 12459}, 
    State1 {clockPlan <= 14259}, 
    ...omissis...
    State14 {clockPlan <= 86399},
    State15; // State15 is referred as goal in the transitions

init State0;

trans
    State0 -> State1 { guard clock >= 12439; sync pulse!; assign step++;  },    
    ... omissis ...
    State14 -> goal { guard clock >= 86399; assign step;  }, // goal should be
State15
    goal -> goal {  }; // goal should be State15
}

best regards

------- Comment #1 From Alexandre David 2009-08-11 11:47:41 -------
Fixed in rev. 4376 (trunk) and 4377 (4.0.9).

First Last Prev Next    No search results available      Search page      Enter new bug