Ecdar / Ecdar-GUI

A graphical tool for modeling using ECDAR (Environment for Compositional Design and Analysis of Real Time Systems)
MIT License
3 stars 5 forks source link

[Feature] Reachability Queries #156

Open Nielswps opened 1 year ago

Nielswps commented 1 year ago

Description

Reachability queries were implemented during the SW5-2022 multi-project, but have not been updated to the new ProtoBuf version. The new syntax is specified in the following issue in the Ecdar-Common repository: Ecdar/Ecdar-Common#2.

The feature is mainly implemented in ecdar/controllers/SimLocationController.java through the getSimLocationReachableQuery method. In addition, the methods getStartStateString and getEndStateString should also be updated.

After changing these methods, the response highlighting should be tested and possibly fixed. It is triggered in ecdar/abstractions/Query.java inside the handleQueryResponse method. The highlighting is done in ecdar/utility/helpers/SimulationHighlighter.

Reason For Request

When verifying states within the model, it is a powerful feature to both verify whether a location can be reached and also get a trace of the path needed to reach it. The majority of the implementation is already present in the simulator and just needs to be tested and modified to work with the new syntax.