| Summary: | unhandled exception due to model error | ||
|---|---|---|---|
| Product: | UPPAAL TIGA | Reporter: | AndreA Orlandini <andrea.orlandini> |
| Component: | Engine | Assignee: | Alexandre David <adavid> |
| Status: | RESOLVED FIXED | ||
| Severity: | minor | ||
| Priority: | P2 | ||
| Version: | unspecified | ||
| Hardware: | PC | ||
| OS: | Windows XP | ||
| Architecture: | |||
Fixed in rev. 4376 (trunk) and 4377 (4.0.9). |
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