search

UPPAALModelChecker / UPPAAL-Meta

This is the offcial meta repo for issue reporting, feature request and public roadmap for the development of UPPAAL.
http://www.uppaal.org
1 stars 0 forks source link

Type error has bug in error context #74

Open magoorden opened 2 years ago

magoorden commented 2 years ago

Describe the bug Consider a model in which you have declared an integer array

int x[2] = {0,1};

and you perform the (incorrect) query

A[] x > 2

Now Uppaal gives a Type error as a query result. Yet, the error context is broken, so the modeler has no information of what actually is wrong. The Status shows

Error message: Type error
Error context: (bug: lost path to error context)

A MWE demonstrating this: MWE_type_error.xml.zip

To Reproduce Steps to reproduce the behavior:

  1. Open the MWE.
  2. Go to Verifier tab.
  3. Check the query.
  4. Observe the error.

Expected behavior The error context should indicate to the modeler what causes the type error.

Version(s) of UPPAAL tested Uppaal Stratego 9.

Desktop (please complete the following information):

mikucionisaau commented 2 years ago

The issue still persists in Stratego-10 albeit it manifest slightly differently: image

"The successors of this state are not well defined" is missleading.