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

Bug 469 - unhandled exception due to model error
Summary: unhandled exception due to model error
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL TIGA
Classification: Unclassified
Component: Engine (show other bugs)
Version: unspecified
Hardware: PC Windows XP
: P2 minor
Assignee: Alexandre David
URL:
Depends on:
Blocks:
 
Reported: 2009-04-07 14:51 CEST by AndreA Orlandini
Modified: 2009-08-11 11:47 CEST (History)
0 users

See Also:
Architecture:


Attachments

Note You need to log in before you can comment on or make changes to this bug.
Description AndreA Orlandini 2009-04-07 14:51:01 CEST
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 Alexandre David 2009-08-11 11:47:41 CEST
Fixed in rev. 4376 (trunk) and 4377 (4.0.9).