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

Feature checker should accept models with ODEs for symbolic operations where ODEs are not part of the system #175

Open mikucionisaau opened 1 year ago

mikucionisaau commented 1 year ago

Original report: https://github.com/UPPAALModelChecker/UPPAAL-Meta/discussions/174 Is your feature request related to a problem? Please describe. Symbolic Simulator rejects models using ODE expressions. The issue is that Symbolic Simulator also rejects the models where the ODE expressions are used in templates which are not instantiated.

Describe the solution you'd like The checker should be more precise and accept the models which do not use the ODEs even though they are mentioned in a process which is not part of the system.

Describe alternatives you've considered As a workaround one may remove/delete all the instances using the ODEs, but it is not a user friendly option.

thorulf4 commented 1 year ago

Lets expand this to all feature checking where applicable

thorulf4 commented 1 year ago

https://github.com/UPPAALModelChecker/utap/pull/40

magoorden commented 1 year ago

Related to this, one could also perform the syntax check on the templates part of the system when running a query, because the query should only invoke those models part of the system declaration. (If a user performs the generic syntax check F7/cmd+E, Uppaal should check all templates, including those not instantiated.)